-
Notifications
You must be signed in to change notification settings - Fork 6
/
idx-type-expr-fn.sml
160 lines (130 loc) · 4.53 KB
/
idx-type-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
(* This functor is just an assembly of functionalities from many other modules, a Swiss-Army-knife kind of thing. *)
signature IDX_TYPE_EXPR_PARAMS = sig
type v
structure UVarI : UVAR_I
structure UVarT : UVAR_T
type ptrn_constr_tag
end
functor IdxTypeExprFn (Params : IDX_TYPE_EXPR_PARAMS) = struct
open Params
open UVarI
open UVarT
open BaseSorts
open BaseTypes
open Util
open LongId
open Operators
open Region
open Bind
infixr 0 $
type id = v * region
type name = string * region
type long_id = v long_id
structure IdxOfExpr = IdxFn (structure UVarI = UVarI
type base_sort = base_sort
type var = long_id
type name = name
type region = region
type 'idx exists_anno = ('idx -> unit) option
)
structure Idx = IdxOfExpr
open Idx
structure TypeOfExpr = TypeFn (structure Idx = Idx
structure UVarT = UVarT
type base_type = base_type
)
structure Type = TypeOfExpr
open Type
structure IdxUtil = IdxUtilFn (Idx)
open IdxUtil
structure TypeUtil = TypeUtilFn (Type)
open TypeUtil
type cvar = var
open Pattern
structure ExprCore = ExprFn (
type var = var
type cvar = var
type mod_id = name
type idx = idx
type sort = sort
type mtype = mtype
val get_constr_names = get_constr_names
type ptrn_constr_tag = ptrn_constr_tag
type ty = ty
type kind = kind
)
open ExprCore
structure ExprUtil = ExprUtilFn (ExprCore)
open ExprUtil
(* some shorthands *)
val STime = Basic (Base Time, dummy)
val SNat = Basic (Base Nat, dummy)
val SBool = Basic (Base BoolSort, dummy)
val SUnit = Basic (Base UnitSort, dummy)
val Type = (0, [])
(* notations *)
infix 9 %@
infix 8 %^
infix 7 %*
infix 6 %+
infix 4 %<=
infix 4 %>=
infix 4 %=
infixr 3 /\
infixr 2 \/
infixr 1 -->
infix 1 <->
(* useful functions *)
open Bind
val VarT = MtVar
fun constr_type (VarT : int LongId.long_id -> mtype) shiftx_long_id ((family, tbinds) : mtype constr_info) =
let
val (tname_kinds, ibinds) = unfold_binds tbinds
val tnames = map fst tname_kinds
val (ns, (t, is)) = unfold_binds ibinds
val ts = map (fn x => VarT (ID (x, dummy))) $ rev $ range $ length tnames
val t2 = AppV (shiftx_long_id 0 (length tnames) family, ts, is, dummy)
val t = Arrow (t, T0 dummy, t2)
val t = foldr (fn ((name, s), t) => UniI (s, Bind (name, t), dummy)) t ns
val t = Mono t
val t = foldr (fn (name, t) => Uni (Bind (name, t), dummy)) t tnames
in
t
end
(* region calculations *)
fun get_region_long_id id =
case id of
ID x => snd x
| QID (m, x) => combine_region (snd m) (snd x)
fun set_region_long_id id r =
case id of
ID (x, _) => ID (x, r)
| QID ((m, _), (x, _)) => QID ((m, r), (x, r))
structure IdxGetRegion = IdxGetRegionFn (structure Idx = Idx
val get_region_var = get_region_long_id
val set_region_var = set_region_long_id)
open IdxGetRegion
structure TypeGetRegion = TypeGetRegionFn (structure Type = Type
val get_region_var = get_region_long_id
val get_region_i = get_region_i)
open TypeGetRegion
structure ExprGetRegion = ExprGetRegionFn (structure Expr = ExprCore
val get_region_var = get_region_long_id
val get_region_cvar = get_region_long_id
val get_region_i = get_region_i
val get_region_mt = get_region_mt
)
open ExprGetRegion
(* mlton needs these lines *)
structure Idx = IdxOfExpr
open Idx
structure Type = TypeOfExpr
open Type
end
(* Test that the result of [ExprFun] matches some signatures. We don't use a signature ascription because signature ascription (transparent or opaque) hides components that are not in the signature. SML should have a "signature check" kind of ascription. *)
functor TestIdxTypeExprFnSignatures (Params : IDX_TYPE_EXPR_PARAMS) = struct
structure M : IDX = IdxTypeExprFn (Params)
structure M2 : TYPE = IdxTypeExprFn (Params)
structure M3 : EXPR = IdxTypeExprFn (Params)
structure M4 : IDX_TYPE_EXPR = IdxTypeExprFn (Params)
end