the next generation of the in-browser educational proof assistant
Merge pull request #13 from mio-19/mio
add reduce and do reduce after substDeBruijn
authored by
Liam O'Connor
and committed by
GitHub
4171a932
3159d19e
+17
-14
+10
-12
src/HOTerm.res
+10
-12
src/HOTerm.res
···
83
83
let set = freeVarsIn(subst, term)
84
84
set->Belt.Set.has(idx)
85
85
}
86
-
// f might map an index to a new one or to a term. when mapping to a term the real index without shifting is passed
86
+
// f might map an index to a new one (Ok(newIdx)) or to a term (Error(t) with t(from)).
87
+
// Note that Ok and Error here are not used for success or failure; they are just two cases distinguishing between an index and a term.
87
88
let rec mapbind0 = (term: t, f: int => result<int, int => t>, ~from: int=0): t =>
88
89
switch term {
89
90
| Symbol(_) => term
···
208
209
| Unallowed => Unallowed
209
210
}
210
211
// beta reduced and eta reduced
211
-
let rec reduceFull = (term: t, subst: subst): t => {
212
+
let rec reduce = (term: t): t => {
212
213
switch term {
213
-
| Schematic({schematic}) if subst->substHas(schematic) =>
214
-
let found = subst->substGet(schematic)->Option.getExn
215
-
reduceFull(found, subst)
216
-
| Lam({body: App({func, arg: Var({idx: 0})})}) if !(func->freeVarsContains(subst, 0)) =>
217
-
reduceFull(downshift(func, 1), subst)
214
+
| Lam({body: App({func, arg: Var({idx: 0})})}) if !(func->freeVarsContains(emptySubst, 0)) =>
215
+
reduce(downshift(func, 1))
218
216
| App({func, arg}) =>
219
-
switch reduceFull(func, subst) {
220
-
| Lam({body}) => reduceFull(substDeBruijn(body, [arg]), subst)
221
-
| func => App({func, arg: reduceFull(arg, subst)})
217
+
switch reduce(func) {
218
+
| Lam({body}) => reduce(substDeBruijn(body, [arg]))
219
+
| func => App({func, arg: reduce(arg)})
222
220
}
223
221
| Lam({name, body}) =>
224
222
Lam({
225
223
name,
226
-
body: reduceFull(body, subst),
224
+
body: reduce(body),
227
225
})
228
226
| Symbol(_) | Var(_) | Schematic(_) => term
229
227
···
231
229
}
232
230
}
233
231
let reduceSubst = (subst: subst): subst => {
234
-
subst->Belt.Map.Int.map(x => reduceFull(x, subst))
232
+
subst->Belt.Map.Int.map(x => reduce(substitute(x, subst)))
235
233
}
236
234
let rec lams = (amount: int, term: t): t => {
237
235
assert(amount >= 0)
+4
-2
src/Rule.res
+4
-2
src/Rule.res
···
21
21
premises: rule.premises->Array.map(premise =>
22
22
premise->substDeBruijn(substs', ~from=from + len)
23
23
),
24
-
conclusion: rule.conclusion->Judgment.substDeBruijn(substs', ~from=from + len),
24
+
conclusion: rule.conclusion
25
+
->Judgment.substDeBruijn(substs', ~from=from + len)
26
+
->Judgment.reduce,
25
27
}
26
28
}
27
29
let rec upshift = (rule: t, amount: int, ~from: int=0) => {
···
39
41
Array.reverse(terms')
40
42
{
41
43
premises: rule.premises->Array.map(r => r->substDeBruijn(terms')),
42
-
conclusion: rule.conclusion->Judgment.substDeBruijn(terms'),
44
+
conclusion: rule.conclusion->Judgment.substDeBruijn(terms')->Judgment.reduce,
43
45
}
44
46
}
45
47
let parseRuleName = str => {
+1
src/SExp.res
+1
src/SExp.res
+2
src/Signatures.res
+2
src/Signatures.res
···
11
11
// law: unify(a,b) == [{}] iff equivalent(a,b)
12
12
let equivalent: (t, t) => bool
13
13
let substDeBruijn: (t, array<t>, ~from: int=?) => t
14
+
let reduce: t => t
14
15
let upshift: (t, int, ~from: int=?) => t
15
16
let fresh: (gen, ~replacing: meta=?) => schematic
16
17
let seen: (gen, schematic) => unit
···
29
30
let equivalent: (t, t) => bool
30
31
let unify: (t, t, ~gen: Term.gen=?) => array<Term.subst>
31
32
let substDeBruijn: (t, array<Term.t>, ~from: int=?) => t
33
+
let reduce: t => t
32
34
let upshift: (t, int, ~from: int=?) => t
33
35
let parse: (string, ~scope: array<Term.meta>, ~gen: Term.gen=?) => result<(t, string), string>
34
36
let prettyPrint: (t, ~scope: array<Term.meta>) => string