-
Notifications
You must be signed in to change notification settings - Fork 0
/
parse.sml
112 lines (96 loc) · 3.55 KB
/
parse.sml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
signature PARSE =
sig
exception Parse of Pos.t * string
val parse: (string * Pos.t) Stream.stream -> string PosDatum.t Stream.stream
end
structure Parse:> PARSE =
struct
structure Parse =
ParseDatumFn
(structure Datum = PosDatumFn (type whitespace = unit)
structure Tok = StringHashable
type name = unit)
fun series [] = raise Fail "Invariant (series)"
| series [x] = (x, Schema.DONE ())
| series (x :: xs) = (x, Schema.MUST_SEE [ series xs ])
fun optional_annotation_binding extras =
Schema.MUST_SEE
[ (".", Schema.MAY_SEE ([], extras, ())),
(":", Schema.MUST_SEE [ (".", Schema.MAY_SEE ([], extras, ())) ]) ]
val sls_schema =
[
series ["(", ")"],
series ["{", "}"],
("All", optional_annotation_binding []),
("Pi", optional_annotation_binding []),
("Exists", optional_annotation_binding []),
("\\", optional_annotation_binding
[">->", "->>", "-o", "->", "<-<", "<<-", "o-", "<-", "=="]),
(* Fixity 1 *)
("&", Schema.DONE ()),
(* Fixity 2 *)
("<-<", Schema.DONE ()),
("<<-", Schema.DONE ()),
("o-", Schema.DONE ()),
("<-", Schema.DONE ()),
(* Fixity 3 *)
("->>", Schema.DONE ()),
("-o", Schema.DONE ()),
("->", Schema.DONE ()),
(">->", Schema.DONE ()),
(* Fixity 4 *)
("*", Schema.DONE ()),
(* Fixity 5 *)
("==", Schema.DONE ()),
("!", Schema.DONE ()),
("@", Schema.DONE ()),
("$", Schema.DONE ()),
(* Application is fixity 6 *)
("type", Schema.DONE ()),
("one", Schema.DONE ()),
("prop", Schema.MAY_SEE ([], [], ())),
("ord", Schema.DONE ()),
("lin", Schema.DONE ()),
("aff", Schema.DONE ()),
("pers", Schema.DONE ())
]
exception Parse of Pos.pos * string
fun demand tok pos str =
case str of
Stream.Nil =>
raise Parse (pos, "'"^tok^"' expected, found end of input")
| Stream.Cons ((s, pos), str) =>
if s = tok then Stream.front str
else raise Parse (pos, "'"^tok^"' expected, found '"^s^"'")
(* Turns a stream of tokens into a stream of declarations. *)
fun stream_transform str =
Stream.lazy (fn () => (
case str of
Stream.Nil => Stream.Nil
| Stream.Cons ((s, pos), str) =>
(if String.sub (s, 0) = #"#"
then (* DIRECTIVE: do hierarchical parsing, then expect "." *)
let
val s = String.extract (s, 1, NONE)
val (ds, str) = Parse.parseMany (sls_schema, ["."])
(Stream.front str)
val ds_pos = PosDatum.poss ds
in Stream.Cons
(PosDatum.List [ (s, ds, Pos.union pos ds_pos) ],
stream_transform (demand "." ds_pos str))
end
else (* CONDEC: expect a ":", then do hierarchical parsing *)
let
val str = demand ":" pos (Stream.front str)
val (ds, str) = Parse.parseMany (sls_schema, ["."]) str
val ds_pos = PosDatum.poss ds
in
Stream.Cons
(PosDatum.List [ ("condec", [PosDatum.Atom (s, pos)], pos),
(":", ds, ds_pos) ],
stream_transform (demand "." ds_pos str))
end)))
fun parse str =
Stream.lazy (fn () => (
Stream.front (stream_transform (Stream.front str))))
end