the next generation of the in-browser educational proof assistant
do we need to subst var for flex-rigid unification
+40
+40
src/HOTerm.res
+40
src/HOTerm.res
···
97
97
)
98
98
nu
99
99
}
100
+
type substVar = Map.t<int, int>
101
+
let incrSubstVar = (subst: substVar) => {
102
+
let nu = Map.make()
103
+
Map.entries(subst)->Iterator.forEach(opt =>
104
+
switch opt {
105
+
| None => ()
106
+
| Some((key, value)) => nu->Map.set(key + 1, value + 1)
107
+
}
108
+
)
109
+
nu
110
+
}
111
+
let rec substVar = (term: t, subst: substVar) =>
112
+
switch term {
113
+
| Symbol(_) => term
114
+
| Var({idx}) =>
115
+
switch Map.get(subst, idx) {
116
+
| None => term
117
+
| Some(newIdx) => Var({idx: newIdx})
118
+
}
119
+
| Schematic({schematic, allowed}) =>
120
+
Schematic({
121
+
schematic,
122
+
allowed: Array.map(allowed, i =>
123
+
switch Map.get(subst, i) {
124
+
| None => i
125
+
| Some(newIdx) => newIdx
126
+
}
127
+
),
128
+
})
129
+
| Lam({name, body}) =>
130
+
Lam({
131
+
name,
132
+
body: substVar(body, incrSubstVar(subst)),
133
+
})
134
+
| App({func, arg}) =>
135
+
App({
136
+
func: substVar(func, subst),
137
+
arg: substVar(arg, subst),
138
+
})
139
+
}
100
140
let rec substitute = (term: t, subst: subst) =>
101
141
switch term {
102
142
| Schematic({schematic, _}) =>