-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathUnifier.sml
172 lines (161 loc) · 6.15 KB
/
Unifier.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
signature Unifier =
sig
type repr
type reprrepr
eqtype str
structure ExpTypeSemantics : Semantics
where type repr = repr
structure ExpTypeSubsSemantics : SubsSemantics
where type repr = repr
structure ExpTypeSimpleConvention : SubsConvention
where type repr = repr
and type exstate = ExpTypeSubsSemantics.state
structure FreeVariables : FreeVariables
where type repr = repr
and type str = str
structure SimpleExpTypeSubstitute : Substitute
where type repr = repr
structure Occurs : OccursCheck
where type repr = repr
structure ReprEmbedding : ReprEmbedding
where type str = str
and type repr = repr
and type reprrepr = reprrepr
structure UnifySubsSemantics : Semantics
where type repr = repr
structure UnifySemantics : UnifySemantics
where type repr = repr
and type exstate = UnifySubsSemantics.state
structure Unify : Unify
where type repr = repr
and type exstate = UnifySemantics.state
end
functor Unifier
(type repr
type reprrepr
eqtype str
val incVar : str -> str
structure Induction : Induction
where type repr = repr
and type reprrepr = reprrepr
and type str = str
structure Deconstructor : Deconstructor
where type repr = repr
structure Constructor : Constructor
where type repr = repr
datatype maparg = Copy of int | Update of int
val map : ((string * string) * string * int list * maparg list) list
) :> Unifier
where type repr = repr
and type reprrepr = reprrepr
and type str = str =
struct
type repr = repr
type reprrepr = reprrepr
type str = str
structure ExpTypeSemantics =
MapJoinSemantics
(val module_name = "ExpTypeSemantics"
datatype maparg = datatype maparg
type repr = repr
val map_name = "unify"
val map = map
structure Induction : Induction = Induction
structure Deconstructor : Deconstructor = Deconstructor
structure Constructor : Constructor = Constructor
) :> Semantics where type repr = repr
structure ExpTypeSubsSemantics =
SubsSemantics
(val module_name = "ExpTypeSubsSemantics"
type repr = repr
structure Semantics : Semantics = ExpTypeSemantics
structure Induction : Induction = Induction
) :> SubsSemantics where type repr = repr
structure ExpTypeSimpleConvention =
SimpleSubs
(val module_name = "ExpTypeSimpleConvention"
type repr = repr
type str = str
val map_name = "unify"
val incVar = incVar
structure Semantics : Semantics = ExpTypeSubsSemantics
structure Induction : Induction = Induction
structure Deconstructor : Deconstructor = Deconstructor
) :> SubsConvention where type repr = repr
and type exstate = ExpTypeSubsSemantics.state
structure FreeVariables =
FreeVariables
(type repr = repr
type str = str
structure Induction : Induction = Induction
structure Deconstructor : Deconstructor = Deconstructor) :> FreeVariables
where type repr = repr
and type str = str
structure SimpleExpTypeSubstitute =
Substitute
(val module_name = "SimpleExpTypeSubstitute"
type repr = repr
type state = unit
val map_name = "substitute"
val initstate = ()
type str = str
val incVar = incVar
structure SubsSemantics : SubsSemantics = ExpTypeSubsSemantics
structure SubsConvention : SubsConvention = ExpTypeSimpleConvention
structure FreeVariables : FreeVariables = FreeVariables
structure Semantics : Semantics = ExpTypeSemantics
structure Induction : Induction = Induction
structure Deconstructor : Deconstructor = Deconstructor
) :> Substitute where type repr = repr
structure Occurs = OccursCheck(type repr = repr
val map_name = "berendregt"
structure Induction : Induction = Induction
structure Deconstructor : Deconstructor = Deconstructor
) :> OccursCheck where type repr = repr
structure ReprEmbedding = ReprEmbedding
(val module_name = "ReprEmbedding"
type str = str
type repr = repr
type reprrepr = reprrepr
structure Deconstructor : Deconstructor = Deconstructor
structure Constructor : Constructor = Constructor
structure Induction : Induction = Induction
) :> ReprEmbedding
where type str = str
and type repr = repr
and type reprrepr = reprrepr
structure UnifySubsSemantics =
MapJoinSemantics
(val module_name = "UnifySubsSemantics"
datatype maparg = datatype maparg
type repr = repr
val map_name = "unify"
val map = map
structure Induction : Induction = Induction
structure Deconstructor : Deconstructor = Deconstructor
structure Constructor : Constructor = Constructor
) :> Semantics where type repr = repr
structure UnifySemantics = UnifySemantics
(val module_name = "UnifySemantics"
type repr = repr
type state = ExpTypeSemantics.state
structure Substitute : Substitute = SimpleExpTypeSubstitute
structure Semantics : Semantics = UnifySubsSemantics
structure Deconstructor : Deconstructor = ReprEmbedding.Deconstructor
structure Induction : Induction = Induction
) :> UnifySemantics
where type repr = repr
and type exstate = UnifySubsSemantics.state
structure Unify = Unify
(val module_name = "Unify"
type repr = repr
val map_name = "unify"
structure Induction : Induction = Induction
structure Constructor : Constructor = ReprEmbedding.Constructor
structure Deconstructor : Deconstructor = Deconstructor
structure Occurs : OccursCheck = Occurs
structure Semantics : Semantics = UnifySemantics
) :> Unify
where type repr = repr
and type exstate = UnifySemantics.state
end