-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathparser.sml
148 lines (132 loc) · 4.55 KB
/
parser.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
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
structure ParserError = struct
exception UnexpectedToken of Token.token option
exception ForbiddenExistentialSignature
end
structure Parser = MakeParser (struct
structure Streamable = StreamStreamable
structure Arg = struct
val disallow_existential_signature = true
open Std
open ParserError
type string = string
type int = int
type program = module
type module = module
type tycon = tycon
type kind = kind
type tvar = tvar
type tvar_opt = tvar option
type sign = sign
type pos_sig = pos_sig
type term = term
type lax_module = lax_module
type existential = kind * tycon
type existentials = (tvar * kind) list
type term_params = (var * tycon) list
type type_params = (tvar * kind) list
type module_params = (tvar_opt * mvar * sign) list
fun program_module x = x
fun module_atom x = x
fun module_app x = x
fun module_paren x = x
fun empty_module_params () = []
fun cons_module_params (vo, mv, s, xs) = (vo, mv, s) :: xs
val mvar = MVar
fun mstar () = MStar
fun mstatic ty = MStatic ty
fun mdynamic e = MDynamic e
fun mpair (x, y) = MPair (x, y)
val mapp = MApp
fun mfst x = MProj(Fst, x)
fun msnd x = MProj(Snd, x)
fun mabs (xs, x) =
let
fun f ((SOME v, mv, s), acc) = MAbs(mv, s, close_at_module 0 v acc)
| f ((NONE, mv, s), acc) = MAbs(mv, s, acc)
in
foldr f x xs
end
fun mlet (v, e, x) = MLet(v, e, x)
fun mletmodule (SOME v, mv, x, y) = MLetModule(mv, x, close_at_module 0 v y)
| mletmodule (NONE, mv, x, y) = MLetModule(mv, x, y)
fun mcirc l = MCirc l
fun lret m = LRet m
fun lseal (m, s) = LSeal(m, s)
fun lbind (SOME v, mv, m, x) = LBind(mv, m, close_at_lax_module 0 v x)
| lbind (NONE, mv, m, x) = LBind(mv, m, x)
fun lunpack (v, ev, e, x) = LUnpack(ev, e, close_at_lax_module 0 v x)
fun type_paren x = x
fun type_bin x = x
fun type_app x = x
fun type_atom x = x
fun empty_type_params () = []
fun cons_type_params (v, k, xs) = (v, k) :: xs
fun quote_ident s = TVar.from_string s
fun tvar_none () = NONE
fun tvar_some v = SOME v
fun tvar_ v = TFree v
fun tabs (xs, ty) = foldr (fn ((v, k), acc) => TAbs(k, close_at_tycon 0 v acc)) ty xs
fun tstar () = TStar
fun tunit () = TUnit
fun tbool () = TBase BBool
fun tint () = TBase BInt
val tpair = TPair
val tapp = TApp
fun tfst x = TProj(Fst, x)
fun tsnd x = TProj(Snd, x)
val tarrow = TArrow
val tprod = TProd
fun tforall (v, k, ty) = TForall(k, close_at_tycon 0 v ty)
fun exist (v, k, ty) = (k, close_at_tycon 0 v ty)
fun texist x = TExist x
fun kind_id x = x
fun kunit () = KUnit
fun ktype () = KType
val ksingleton = KSingleton
fun karrow (v, x, y) = KArrow(x, close_at_kind 0 v y)
fun kprod (v, x, y) = KProd(x, close_at_kind 0 v y)
fun karrow_degenerate (x, y) = KArrow(x, y)
fun kprod_degenerate (x, y) = KProd(x, y)
fun sig_id x = x
fun sunit () = SUnit
val sstatic = SStatic
val sdynamic = SDynamic
fun sarrow (v, x, y) = SArrow(x, close_at_sig 0 v y)
fun sprod (v, x, y) = SProd(x, close_at_sig 0 v y)
fun sarrow_degenerate (x, y) = SArrow(x, y)
fun sprod_degenerate (x, y) = SProd(x, y)
val smonad = SMonad
fun exists_nil () = []
fun exists_cons (v, k, xs) = (v, k) :: xs
fun pos_sig_id x = x
val pdown = PDown
fun pexist (v1, k1, xs, s) =
if disallow_existential_signature
then raise ForbiddenExistentialSignature
else PExist(k1, close_at_pos_sig 0 v1 $ foldr (fn ((v, k), p) => PExist(k, close_at_pos_sig 0 v p)) (PDown s) xs)
fun term_id x = x
fun empty_term_params () = []
fun cons_term_params (v, ty, xs) = (v, ty) :: xs
val evar = EVar
fun estar () = EStar
fun eone () = ELit $ LInt 1
fun enum n = ELit $ LInt n
val epair = EPair
val eapp = EApp
val eext = EExt
val efix = EFix
fun efst x = EProj(Fst, x)
fun esnd x = EProj(Snd, x)
val einst = EInst
fun eabs (xs, e) = foldr (fn ((v, ty), acc) => EAbs(v, ty, acc)) e xs
fun egen (v, k, x) = EGen(k, close_at_term 0 v x)
fun epack (w, x, (k, ty)) = EPack(w, x, k, ty)
val elet = ELet
fun eletlax (SOME v, mv, l, x) = ELetLax(mv, l, close_at_term 0 v x)
| eletlax (NONE, mv, l, x) = ELetLax(mv, l, x)
fun eunpack (v, ev, x, y) = EUnpack(ev, x, close_at_term 0 v y)
val eif = EIf
datatype terminal = datatype Token.token
fun error s = UnexpectedToken(SOME(Stream.hd s) handle Stream.Empty => NONE)
end
end)