src/Tools/Metis/src/Parser.sig
changeset 39347 50dec19e682b
parent 39346 d837998f1e60
child 39348 6f9c9899f99f
equal deleted inserted replaced
39346:d837998f1e60 39347:50dec19e682b
     1 (* ========================================================================= *)
       
     2 (* PARSING AND PRETTY PRINTING                                               *)
       
     3 (* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
       
     4 (* ========================================================================= *)
       
     5 
       
     6 signature Parser =
       
     7 sig
       
     8 
       
     9 (* ------------------------------------------------------------------------- *)
       
    10 (* Pretty printing for built-in types                                        *)
       
    11 (* ------------------------------------------------------------------------- *)
       
    12 
       
    13 type ppstream = PP.ppstream
       
    14 
       
    15 datatype breakStyle = Consistent | Inconsistent
       
    16 
       
    17 type 'a pp = ppstream -> 'a -> unit
       
    18 
       
    19 val lineLength : int ref
       
    20 
       
    21 val beginBlock : ppstream -> breakStyle -> int -> unit
       
    22 
       
    23 val endBlock : ppstream -> unit
       
    24 
       
    25 val addString : ppstream -> string -> unit
       
    26 
       
    27 val addBreak : ppstream -> int * int -> unit
       
    28 
       
    29 val addNewline : ppstream -> unit
       
    30 
       
    31 val ppMap : ('a -> 'b) -> 'b pp -> 'a pp
       
    32 
       
    33 val ppBracket : string -> string -> 'a pp -> 'a pp
       
    34 
       
    35 val ppSequence : string -> 'a pp -> 'a list pp
       
    36 
       
    37 val ppBinop : string -> 'a pp -> 'b pp -> ('a * 'b) pp
       
    38 
       
    39 val ppChar : char pp
       
    40 
       
    41 val ppString : string pp
       
    42 
       
    43 val ppUnit : unit pp
       
    44 
       
    45 val ppBool : bool pp
       
    46 
       
    47 val ppInt : int pp
       
    48 
       
    49 val ppReal : real pp
       
    50 
       
    51 val ppOrder : order pp
       
    52 
       
    53 val ppList : 'a pp -> 'a list pp
       
    54 
       
    55 val ppOption : 'a pp -> 'a option pp
       
    56 
       
    57 val ppPair : 'a pp -> 'b pp -> ('a * 'b) pp
       
    58 
       
    59 val ppTriple : 'a pp -> 'b pp -> 'c pp -> ('a * 'b * 'c) pp
       
    60 
       
    61 val toString : 'a pp -> 'a -> string  (* Uses !lineLength *)
       
    62 
       
    63 val fromString : ('a -> string) -> 'a pp
       
    64 
       
    65 val ppTrace : 'a pp -> string -> 'a -> unit
       
    66 
       
    67 (* ------------------------------------------------------------------------- *)
       
    68 (* Recursive descent parsing combinators                                     *)
       
    69 (* ------------------------------------------------------------------------- *)
       
    70 
       
    71 (* Generic parsers
       
    72 
       
    73 Recommended fixities:
       
    74   infixr 9 >>++
       
    75   infixr 8 ++
       
    76   infixr 7 >>
       
    77   infixr 6 ||
       
    78 *)
       
    79 
       
    80 exception NoParse
       
    81 
       
    82 val error : 'a -> 'b * 'a
       
    83 
       
    84 val ++ : ('a -> 'b * 'a) * ('a -> 'c * 'a) -> 'a -> ('b * 'c) * 'a
       
    85 
       
    86 val >> : ('a -> 'b * 'a) * ('b -> 'c) -> 'a -> 'c * 'a
       
    87 
       
    88 val >>++ : ('a -> 'b * 'a) * ('b -> 'a -> 'c * 'a) -> 'a -> 'c * 'a
       
    89 
       
    90 val || : ('a -> 'b * 'a) * ('a -> 'b * 'a) -> 'a -> 'b * 'a
       
    91 
       
    92 val first : ('a -> 'b * 'a) list -> 'a -> 'b * 'a
       
    93 
       
    94 val mmany : ('s -> 'a -> 's * 'a) -> 's -> 'a -> 's * 'a
       
    95 
       
    96 val many : ('a -> 'b * 'a) -> 'a -> 'b list * 'a
       
    97 
       
    98 val atLeastOne : ('a -> 'b * 'a) -> 'a -> 'b list * 'a
       
    99 
       
   100 val nothing : 'a -> unit * 'a
       
   101 
       
   102 val optional : ('a -> 'b * 'a) -> 'a -> 'b option * 'a
       
   103 
       
   104 (* Stream based parsers *)
       
   105 
       
   106 type ('a,'b) parser = 'a Stream.stream -> 'b * 'a Stream.stream
       
   107 
       
   108 val everything : ('a, 'b list) parser -> 'a Stream.stream -> 'b Stream.stream
       
   109 
       
   110 val maybe : ('a -> 'b option) -> ('a,'b) parser
       
   111 
       
   112 val finished : ('a,unit) parser
       
   113 
       
   114 val some : ('a -> bool) -> ('a,'a) parser
       
   115 
       
   116 val any : ('a,'a) parser
       
   117 
       
   118 val exact : ''a -> (''a,''a) parser
       
   119 
       
   120 (* ------------------------------------------------------------------------- *)
       
   121 (* Infix operators                                                           *)
       
   122 (* ------------------------------------------------------------------------- *)
       
   123 
       
   124 type infixities = {token : string, precedence : int, leftAssoc : bool} list
       
   125 
       
   126 val infixTokens : infixities -> string list
       
   127 
       
   128 val parseInfixes :
       
   129     infixities -> (string * 'a * 'a -> 'a) -> (string,'a) parser ->
       
   130     (string,'a) parser
       
   131 
       
   132 val ppInfixes :
       
   133     infixities -> ('a -> (string * 'a * 'a) option) -> ('a * bool) pp ->
       
   134     ('a * bool) pp
       
   135 
       
   136 (* ------------------------------------------------------------------------- *)
       
   137 (* Quotations                                                                *)
       
   138 (* ------------------------------------------------------------------------- *)
       
   139 
       
   140 type 'a quotation = 'a frag list
       
   141 
       
   142 val parseQuotation : ('a -> string) -> (string -> 'b) -> 'a quotation -> 'b
       
   143 
       
   144 end