src/Tools/Metis/src/Parse.sig
author blanchet
Mon, 13 Sep 2010 21:11:59 +0200
changeset 39349 2d0a4361c3ef
parent 39348 6f9c9899f99f
child 39443 e330437cd22a
permissions -rw-r--r--
change license, with Joe Hurd's permission
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     1
(* ========================================================================= *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     2
(* PARSING                                                                   *)
39349
2d0a4361c3ef change license, with Joe Hurd's permission
blanchet
parents: 39348
diff changeset
     3
(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     4
(* ========================================================================= *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     5
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     6
signature Parse =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     7
sig
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     8
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     9
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    10
(* A "cannot parse" exception.                                               *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    11
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    12
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    13
exception NoParse
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    14
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    15
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    16
(* Recursive descent parsing combinators.                                    *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    17
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    18
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    19
(*
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    20
  Recommended fixities:
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    21
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    22
  infixr 9 >>++
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    23
  infixr 8 ++
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    24
  infixr 7 >>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    25
  infixr 6 ||
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    26
*)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    27
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    28
val error : 'a -> 'b * 'a
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    29
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    30
val ++ : ('a -> 'b * 'a) * ('a -> 'c * 'a) -> 'a -> ('b * 'c) * 'a
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    31
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    32
val >> : ('a -> 'b * 'a) * ('b -> 'c) -> 'a -> 'c * 'a
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    33
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    34
val >>++ : ('a -> 'b * 'a) * ('b -> 'a -> 'c * 'a) -> 'a -> 'c * 'a
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    35
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    36
val || : ('a -> 'b * 'a) * ('a -> 'b * 'a) -> 'a -> 'b * 'a
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    37
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    38
val first : ('a -> 'b * 'a) list -> 'a -> 'b * 'a
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    39
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    40
val mmany : ('s -> 'a -> 's * 'a) -> 's -> 'a -> 's * 'a
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    41
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    42
val many : ('a -> 'b * 'a) -> 'a -> 'b list * 'a
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    43
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    44
val atLeastOne : ('a -> 'b * 'a) -> 'a -> 'b list * 'a
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    45
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    46
val nothing : 'a -> unit * 'a
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    47
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    48
val optional : ('a -> 'b * 'a) -> 'a -> 'b option * 'a
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    49
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    50
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    51
(* Stream-based parsers.                                                     *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    52
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    53
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    54
type ('a,'b) parser = 'a Stream.stream -> 'b * 'a Stream.stream
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    55
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    56
val maybe : ('a -> 'b option) -> ('a,'b) parser
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    57
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    58
val finished : ('a,unit) parser
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    59
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    60
val some : ('a -> bool) -> ('a,'a) parser
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    61
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    62
val any : ('a,'a) parser
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    63
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    64
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    65
(* Parsing whole streams.                                                    *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    66
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    67
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    68
val fromStream : ('a,'b) parser -> 'a Stream.stream -> 'b
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    69
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    70
val fromList : ('a,'b) parser -> 'a list -> 'b
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    71
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    72
val everything : ('a, 'b list) parser -> 'a Stream.stream -> 'b Stream.stream
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    73
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    74
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    75
(* Parsing lines of text.                                                    *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    76
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    77
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    78
val initialize :
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    79
    {lines : string Stream.stream} ->
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    80
    {chars : char list Stream.stream,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    81
     parseErrorLocation : unit -> string}
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    82
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    83
val exactChar : char -> (char,unit) parser
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    84
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    85
val exactCharList : char list -> (char,unit) parser
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    86
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    87
val exactString : string -> (char,unit) parser
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    88
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    89
val escapeString : {escape : char list} -> (char,string) parser
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    90
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    91
val manySpace : (char,unit) parser
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    92
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    93
val atLeastOneSpace : (char,unit) parser
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    94
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    95
val fromString : (char,'a) parser -> string -> 'a
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    96
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    97
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    98
(* Infix operators.                                                          *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    99
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   100
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   101
val parseInfixes :
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   102
    Print.infixes -> (string * 'a * 'a -> 'a) -> (string,'a) parser ->
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   103
    (string,'a) parser
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   104
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   105
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   106
(* Quotations.                                                               *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   107
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   108
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   109
type 'a quotation = 'a frag list
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   110
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   111
val parseQuotation : ('a -> string) -> (string -> 'b) -> 'a quotation -> 'b
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   112
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   113
end