-
Notifications
You must be signed in to change notification settings - Fork 0
/
expr-fn.sml
194 lines (159 loc) · 7.7 KB
/
expr-fn.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
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
signature EXPR_PARAMS = sig
type var
type cvar
type mod_id
type idx
type sort
type mtype
val get_constr_names : mtype -> Namespaces.name list
type ptrn_constr_tag
type ty
type kind
end
functor ExprFn (Params : EXPR_PARAMS) = struct
open Params
open Unbound
open Namespaces
open Operators
open Region
open Binders
type ptrn = (cvar * ptrn_constr_tag, mtype) Pattern.ptrn
type return = mtype option * idx option * idx option
datatype stbind =
SortingST of ibinder * sort outer
| TypingST of ptrn
type scoping_ctx = ibinder list * tbinder list * cbinder list * ebinder list
type proj_path = (tuple_record_proj * region) list
datatype expr =
EVar of var * (bool(*explicit index arguments (EIA)*) * bool)
| EConst of expr_const * region
| EState of string * region
| EUnOp of expr_un_op * expr * region
| EBinOp of expr_bin_op * expr * expr
| ETriOp of expr_tri_op * expr * expr * expr
| EEI of expr_EI * expr * idx
| EET of expr_ET * expr * mtype
| ET of expr_T * mtype * region
| ERecord of expr SMap.map * region
| ETuple of expr list
| ENewArrayValues of int * mtype * expr list * region
| EAbs of idx StMap.map * (ptrn, expr) bind * (idx * idx) option
| EAbsI of (sort, expr) ibind_anno * region
| EAppConstr of (cvar * (bool * bool)) * mtype list * idx list * expr * (int * mtype) option
| ECase of expr * return * (ptrn, expr) bind list * region
(* | ECaseSumbool of expr * expr ibind * expr ibind * region *)
| EIfi of expr * expr ibind * expr ibind * region
| ELet of return * (decl tele, expr) bind * region
| EGet of string * (expr * proj_path) list * Region.region
| ESet of string * (expr * proj_path) list * expr * Region.region
| EEnv of env_info * region
| EAscState of expr * idx StMap.map
| EDispatch of (string * expr * mtype option * mtype option) list * Region.region
(* | EDebugLog of expr *)
and decl =
DVal of ebinder * ((tbinder * (idx * idx) outer) list, expr) bind outer * region
| DValPtrn of ptrn * expr outer * region
| DRec of ebinder * ((tbinder * (idx * idx) outer) list * stbind tele rebind, (idx StMap.map * idx StMap.map) * (mtype * (idx * idx)) * expr) bind inner * region
| DIdxDef of ibinder * sort option outer * idx outer
| DAbsIdx2 of ibinder * sort outer * idx outer
| DAbsIdx of (ibinder * sort outer * idx outer) * decl tele rebind * region
| DTypeDef of tbinder * mtype outer
| DOpen of mod_id inner * scoping_ctx option
| DConstrDef of cbinder * cvar outer
type name = string * Region.region
datatype spec =
SpecVal of name * ty
| SpecIdx of name * sort
| SpecType of name * kind
| SpecTypeDef of name * mtype
type sgn = spec list * region
(* datatype sgn = *)
(* SigComponents of spec list * region *)
(* | SigVar of id *)
(* | SigWhere of sgn * (id * mtype) *)
(* and sig_comp = *)
(* ScSpec of name * spec * region *)
(* | ScModSpec of name * sgn *)
(* | Include of sgn *)
datatype mod =
ModComponents of (* mod_comp *)decl list * region
(* | ModProjectible of mod_id *)
| ModSeal of mod * sgn
| ModTransparentAsc of mod * sgn
(* | ModFunctorApp of id * mod (* list *) *)
(* and mod_comp = *)
(* McDecl of decl *)
(* | McModBind of name * mod *)
datatype top_bind =
TBMod of mod
(* | TopSigBind of name * sgn *)
(* | TopModSpec of name * sgn *)
| TBFunctor of (name * sgn) (* list *) * mod
| TBFunctorApp of mod_id * mod_id (* list *)
| TBState of mtype
| TBPragma of string
type prog = (name * top_bind) list
(* type ptrn = (cvar * ptrn_constr_tag, mtype) Pattern.ptrn *)
(* type return = mtype option * idx option *)
(* datatype stbind = *)
(* SortingST of Binders.ibinder * sort Unbound.outer *)
(* | TypingST of ptrn *)
(* type scoping_ctx = Binders.ibinder list * Binders.tbinder list * Binders.cbinder list * Binders.ebinder list *)
(* datatype expr = *)
(* EVar of var * bool(*explicit index arguments (EIA)*) *)
(* | EConst of Operators.expr_const * Region.region *)
(* | EUnOp of Operators.expr_un_op * expr * Region.region *)
(* | EBinOp of Operators.bin_op * expr * expr *)
(* | ETriOp of Operators.tri_op * expr * expr * expr *)
(* | EEI of Operators.expr_EI * expr * idx *)
(* | EET of Operators.expr_ET * expr * mtype *)
(* | ET of Operators.expr_T * mtype * Region.region *)
(* | EAbs of (ptrn, expr) Unbound.bind *)
(* | EAbsI of (sort, expr) Binders.ibind_anno * Region.region *)
(* | EAppConstr of (cvar * bool) * mtype list * idx list * expr * (int * mtype) option *)
(* | ECase of expr * return * (ptrn, expr) Unbound.bind list * Region.region *)
(* | ELet of return * (decl Unbound.tele, expr) Unbound.bind * Region.region *)
(* and decl = *)
(* DVal of Binders.ebinder * (Binders.tbinder list, expr) Unbound.bind Unbound.outer * Region.region Unbound.outer *)
(* | DValPtrn of ptrn * expr Unbound.outer * Region.region Unbound.outer *)
(* | DRec of Binders.ebinder * (Binders.tbinder list * stbind Unbound.tele Unbound.rebind, (mtype * idx) * expr) Unbound.bind Unbound.inner * Region.region Unbound.outer *)
(* | DIdxDef of Binders.ibinder * sort Unbound.outer * idx Unbound.outer *)
(* | DAbsIdx2 of Binders.ibinder * sort Unbound.outer * idx Unbound.outer *)
(* | DAbsIdx of (Binders.ibinder * sort Unbound.outer * idx Unbound.outer) * decl Unbound.tele Unbound.rebind * Region.region Unbound.outer *)
(* | DTypeDef of Binders.tbinder * mtype Unbound.outer *)
(* | DOpen of mod_id Unbound.outer * scoping_ctx option *)
(* type name = string * Region.region *)
(* datatype spec = *)
(* SpecVal of name * ty *)
(* | SpecIdx of name * sort *)
(* | SpecType of name * kind *)
(* | SpecTypeDef of name * mtype *)
(* type sgn = spec list * Region.region *)
(* (* datatype sgn = *) *)
(* (* SigComponents of spec list * Region.region *) *)
(* (* | SigVar of id *) *)
(* (* | SigWhere of sgn * (id * mtype) *) *)
(* (* and sig_comp = *) *)
(* (* ScSpec of name * spec * Region.region *) *)
(* (* | ScModSpec of name * sgn *) *)
(* (* | Include of sgn *) *)
(* datatype mod = *)
(* ModComponents of (* mod_comp *)decl list * Region.region *)
(* (* | ModProjectible of mod_id *) *)
(* | ModSeal of mod * sgn *)
(* | ModTransparentAsc of mod * sgn *)
(* (* | ModFunctorApp of id * mod (* list *) *) *)
(* (* and mod_comp = *) *)
(* (* McDecl of decl *) *)
(* (* | McModBind of name * mod *) *)
(* datatype top_bind = *)
(* TopModBind of mod *)
(* (* | TopSigBind of name * sgn *) *)
(* (* | TopModSpec of name * sgn *) *)
(* | TopFunctorBind of (name * sgn) (* list *) * mod *)
(* | TopFunctorApp of mod_id * mod_id (* list *) *)
(* type prog = (name * top_bind) list *)
end
functor TestExprFnSignatures (Params : EXPR_PARAMS) = struct
structure M : EXPR = ExprFn (Params)
end