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