the next generation of the in-browser educational proof assistant
upshift downshift in reduce
+35
-1
+35
-1
src/HOTerm.res
+35
-1
src/HOTerm.res
···
87
87
arg: upshift(arg, amount, ~from),
88
88
})
89
89
}
90
+
let rec downshift = (term: t, amount: int, ~from: int=1) => {
91
+
switch term {
92
+
| Symbol(_) => term
93
+
| Var({idx}) =>
94
+
Var({
95
+
idx: if idx >= from {
96
+
idx - amount
97
+
} else {
98
+
idx
99
+
},
100
+
})
101
+
| Schematic({schematic, allowed}) =>
102
+
Schematic({
103
+
schematic,
104
+
allowed: Array.map(allowed, i =>
105
+
if i >= from {
106
+
i - amount
107
+
} else {
108
+
i
109
+
}
110
+
),
111
+
})
112
+
| Lam({name, body}) =>
113
+
Lam({
114
+
name,
115
+
body: downshift(body, amount, ~from=from + 1),
116
+
})
117
+
| App({func, arg}) =>
118
+
App({
119
+
func: downshift(func, amount, ~from),
120
+
arg: downshift(arg, amount, ~from),
121
+
})
122
+
}
123
+
}
90
124
let rec upshiftSubst = (subst: subst, amount: int, ~from: int=0) => {
91
125
let nu = Map.make()
92
126
Map.entries(subst)->Iterator.forEach(opt =>
···
202
236
switch term {
203
237
| App({func, arg}) =>
204
238
switch reduce(func) {
205
-
| Lam({body}) => reduce(substitute(body, singletonSubst(0, arg)))
239
+
| Lam({body}) => reduce(downshift(substitute(body, singletonSubst(0, upshift(arg, 1))), 1))
206
240
| _ => term
207
241
}
208
242
| term => term