-
Notifications
You must be signed in to change notification settings - Fork 3
/
il-machine.sml
144 lines (133 loc) · 4.83 KB
/
il-machine.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
(*
* MixML prototype implementation
*
* Based on: Derek Dreyer, Andreas Rossberg, "Mixin' Up the ML Module System"
*
* (c) 2007-2008 Andreas Rossberg
*)
structure ILMachine =
struct
open IL
datatype value =
IntV of int
| StringV of string
| TupleV of value list
| VariantV of value * int * typ
| LambdaV of var * sign * term
| GenV of typvar list * term
| FoldV of typvar
| UnfoldV of typvar
| ConV of typvar * typ list * value
datatype modval =
VarW of var
| TypW of typ
| TermW of value
| StructW of (lab * modval) list
| LambdaW of var * sign * modl
| GenDownW of (typvar * kind) list * modl
| GenUpW of (typvar * kind) list * modl
datatype frame =
ValF
| PlusF1 of term
| PlusF2 of int
| MinusF1 of term
| MinusF2 of int
| EqualF1 of term
| EqualF2 of int
| LessF1 of term
| LessF2 of int
| CatF1 of term
| CatF2 of string
| TupleF of value list * term list
| ProjF of int
| VariantF of int * typ
| CaseF of (var * term) list
| AppF1 of modl
| AppF2 of value
| InstF of typ list
| ConF1 of typ list * term
| ConF2 of value * typ list
| PrintF
| TermF
| StructF of (lab * modval) list * lab * (lab * modl) list
| DotF of lab
| ApplyF1 of modl
| ApplyF2 of modval
| LetF of var * modl
| InstDownF of typ list
(* todo: real effect system
| InstUpF of typvar list
*)
| InstUpF1 of typvar list * modl
| InstUpF2 of modval * typvar list
| AssignF of modl
| ForceF
| NeededF of var
type continuation = frame list
datatype store_entry =
Evaluated of modval
| Evaluating
| Defined of modl
| Undefined
type store = store_entry context
datatype ('a,'b) ev = EXP of 'a | VAL of 'b
datatype state =
TermSt of typ_context * modl_context * store * continuation * (term, value) ev
| ModSt of typ_context * modl_context * store * continuation * (modl, modval) ev
| BlackHole of var
fun toValue(ValE(m)) = NONE
| toValue(IntE(n)) = SOME(IntV(n))
| toValue(StringE(s)) = SOME(StringV(s))
| toValue(PlusE _) = NONE
| toValue(MinusE _) = NONE
| toValue(EqualE _) = NONE
| toValue(LessE _) = NONE
| toValue(CatE _) = NONE
| toValue(TupleE(es)) = (SOME(TupleV(List.map (valOf o toValue) es)) handle Option => NONE)
| toValue(DotE _) = NONE
| toValue(VariantE(e, i, tau)) = (SOME(VariantV(valOf(toValue e), i, tau)) handle Option => NONE)
| toValue(CaseE _) = NONE
| toValue(LambdaE(x, sigma, e)) = SOME(LambdaV(x, sigma, e))
| toValue(ApplyE _) = NONE
| toValue(GenE(alphas, e)) = SOME(GenV(alphas, e))
| toValue(InstE _) = NONE
| toValue(FoldE(alpha)) = SOME(FoldV(alpha))
| toValue(UnfoldE(alpha)) = SOME(UnfoldV(alpha))
| toValue(ConE(FoldE(alpha), taus, e)) = Option.map (fn v => ConV(alpha, taus, v)) (toValue e)
| toValue(ConE _) = NONE
| toValue(PrintE _) = NONE
fun fromValue(IntV(n)) = IntE(n)
| fromValue(StringV(s)) = StringE(s)
| fromValue(TupleV(vs)) = TupleE(List.map fromValue vs)
| fromValue(VariantV(v, i, tau)) = VariantE(fromValue v, i, tau)
| fromValue(LambdaV(x, sigma, e)) = LambdaE(x, sigma, e)
| fromValue(GenV(alphas, e)) = GenE(alphas, e)
| fromValue(FoldV(alpha)) = FoldE(alpha)
| fromValue(UnfoldV(alpha)) = UnfoldE(alpha)
| fromValue(ConV(alpha, taus, v)) = ConE(FoldE(alpha), taus, fromValue v)
fun toModval(VarM(x)) = SOME(VarW(x))
| toModval(TypM(tau)) = SOME(TypW(tau))
| toModval(TermM(e)) = Option.map TermW (toValue e)
| toModval(StructM(lms)) = (SOME(StructW(List.map (fn(l, m) => (l, valOf(toModval m))) lms)) handle Option => NONE)
| toModval(DotM _) = NONE
| toModval(LambdaM(x, sigma, m)) = SOME(LambdaW(x, sigma, m))
| toModval(ApplyM _) = NONE
| toModval(LetM _) = NONE
| toModval(GenDownM(alphaks, m)) = SOME(GenDownW(alphaks, m))
| toModval(InstDownM _) = NONE
| toModval(GenUpM(alphaks, m)) = SOME(GenUpW(alphaks, m))
| toModval(InstUpM _) = NONE
| toModval(NewTypM _) = NONE
| toModval(DefEquiM _) = NONE
| toModval(DefIsoM _) = NONE
| toModval(NewTermM _) = NONE
| toModval(AssignM _) = NONE
| toModval(ForceM _) = NONE
fun fromModval(VarW(x)) = VarM(x)
| fromModval(TypW(tau)) = TypM(tau)
| fromModval(TermW(v)) = TermM(fromValue v)
| fromModval(StructW(lws)) = StructM(List.map (fn(l, w) => (l, fromModval w)) lws)
| fromModval(LambdaW(x, sigma, m)) = LambdaM(x, sigma, m)
| fromModval(GenDownW(alphaks, m)) = GenDownM(alphaks, m)
| fromModval(GenUpW(alphaks, m)) = GenUpM(alphaks, m)
end