From bc5902c4dcc804abb3a72508e2be149b483d3605 Mon Sep 17 00:00:00 2001 From: Mio Date: Sun, 3 May 2026 14:17:16 +1000 Subject: [PATCH] Atom for HOTerm --- src/HOTerm.res | 1473 ++++++++++++++++++++++------------------ src/HOTerm.resi | 32 +- src/HOTermMethod.res | 8 +- src/ProofView.res | 140 ++-- src/SidebarContext.res | 2 +- tests/HOTermTest.res | 73 +- tests/RuleTest.res | 56 +- 7 files changed, 1027 insertions(+), 757 deletions(-) diff --git a/src/HOTerm.res b/src/HOTerm.res index 361c792..e97afa6 100644 --- a/src/HOTerm.res +++ b/src/HOTerm.res @@ -3,756 +3,875 @@ module IntCmp = Belt.Id.MakeComparable({ let cmp = Pervasives.compare }) -type rec t = - | Symbol({name: string, constructor: bool}) - | Var({idx: int}) - | Schematic({schematic: int}) - | Lam({name: string, body: t}) - | App({func: t, arg: t}) - // Unallowed is used internally in unify, where Nipkow 1993 uses Var(-infinity) - | Unallowed -type meta = string -type schematic = int -type subst = Belt.Map.Int.t -let substHas = (subst: subst, schematic: schematic) => subst->Belt.Map.Int.has(schematic) -let substGet = (subst: subst, schematic: schematic) => subst->Belt.Map.Int.get(schematic) -let mapSubst = (m: subst, f: t => t): subst => { - m->Belt.Map.Int.map(f) -} -let substEqual = (m1, m2) => m1 == m2 -let makeSubst = () => { - Belt.Map.Int.empty -} -let mergeSubsts = (m1: subst, m2: subst) => - Belt.Map.Int.merge(m1, m2, (_, o1, o2) => - switch (o1, o2) { - | (Some(v), _) | (_, Some(v)) => Some(v) - | (None, None) => None - } - ) -let rec equivalent = (a: t, b: t) => { - switch (a, b) { - | (Symbol({name: na}), Symbol({name: nb})) => na == nb - | (Var({idx: ia}), Var({idx: ib})) => ia == ib - | (Schematic({schematic: sa}), Schematic({schematic: sb})) => sa == sb - | (Lam({name: _, body: ba}), Lam({name: _, body: bb})) => equivalent(ba, bb) - | (App({func: fa, arg: aa}), App({func: fb, arg: ab})) => equivalent(fa, fb) && equivalent(aa, ab) - | (Unallowed, Unallowed) => false - | (_, _) => false - } -} -type gen = ref -let seen = (g: gen, s: int) => { - if s >= g.contents { - g := s + 1 +module type ATOM = AtomDef.ATOM + +module DefaultAtom = { + module BaseAtom = AtomDef.MakeBaseAtom({ + type t = string + }) + type t = string + type subst = Map.t + let unify = (a, b, ~gen as _=?) => + if a == b { + Seq.once(Map.make()) + } else { + Seq.empty + } + let prettyPrint = (name, ~scope as _: array) => name + let symbolRegexpString = "^([^\\s()]+)" + let parse = (str0, ~scope as _: array, ~gen as _=?) => { + let str = str0->String.trimStart + let re = RegExp.fromStringWithFlags(symbolRegexpString, ~flags="y") + switch re->RegExp.exec(str) { + | None => Error("invalid symbol") + | Some(res) => + switch RegExp.Result.matches(res) { + | [name] => Ok((name, String.sliceToEnd(str, ~start=RegExp.lastIndex(re)))) + | _ => Error("invalid symbol") + } + } } + let substitute = (name, _) => name + let substDeBruijn = (name, _, ~from as _=?) => name + let concrete = _ => true + let upshift = (t, _, ~from as _=?) => t + let coerce = _ => None } -let fresh = (g: gen, ~replacing as _=?) => { - let v = g.contents - g := g.contents + 1 - v -} -let rec schematicsIn = (subst: subst, it: t): Belt.Set.t => - switch it { - | Schematic({schematic, _}) if subst->substHas(schematic) => - let found = subst->substGet(schematic)->Option.getExn - schematicsIn(subst, found) - | Schematic({schematic, _}) => Belt.Set.make(~id=module(IntCmp))->Belt.Set.add(schematic) - | Lam({body}) => schematicsIn(subst, body) - | App({func, arg}) => Belt.Set.union(schematicsIn(subst, func), schematicsIn(subst, arg)) - | Unallowed | Symbol(_) | Var(_) => Belt.Set.make(~id=module(IntCmp)) - } -let occ = (schematic: schematic, subst: subst, t: t): bool => { - let set = schematicsIn(subst, t) - set->Belt.Set.has(schematic) -} -let rec freeVarsIn = (subst: subst, it: t): Belt.Set.t => - switch it { - | Schematic({schematic, _}) if subst->substHas(schematic) => - let found = subst->substGet(schematic)->Option.getExn - freeVarsIn(subst, found) - | Var({idx}) => Belt.Set.make(~id=module(IntCmp))->Belt.Set.add(idx) - | Lam({name: _, body}) => - freeVarsIn(subst, body) - ->Belt.Set.toArray - ->Array.filterMap(v => - if v >= 1 { - Some(v - 1) - } else { - None + +module Make = (Atom: AtomDef.ATOM): { + type rec t = + | Symbol({name: Atom.t, constructor: bool}) + | Var({idx: int}) + | Schematic({schematic: int}) + | Lam({name: string, body: t}) + | App({func: t, arg: t}) + | Unallowed + + include Signatures.TERM + with type t := t + and type meta = string + and type schematic = int + and type subst = Belt.Map.Int.t + + let emptySubst: subst + let strip: t => (t, array) + let app: (t, array) => t + let mkvars: int => array + let mapTerms: (t, t => t) => t + exception UnifyFail(string) + let substAdd: (subst, schematic, t) => subst + let unifyTerm: (t, t, subst, ~gen: option) => Seq.t + let reduceSubst: subst => subst + let rewrite: (t, t, t, ~subst: subst, ~gen: option) => (subst, t) +} => { + type rec t = + | Symbol({name: Atom.t, constructor: bool}) + | Var({idx: int}) + | Schematic({schematic: int}) + | Lam({name: string, body: t}) + | App({func: t, arg: t}) + // Unallowed is used internally in unify, where Nipkow 1993 uses Var(-infinity) + | Unallowed + type meta = string + type schematic = int + type subst = Belt.Map.Int.t + let substHas = (subst: subst, schematic: schematic) => subst->Belt.Map.Int.has(schematic) + let substGet = (subst: subst, schematic: schematic) => subst->Belt.Map.Int.get(schematic) + let mapSubst = (m: subst, f: t => t): subst => { + m->Belt.Map.Int.map(f) + } + let substEqual = (m1, m2) => m1 == m2 + let makeSubst = () => { + Belt.Map.Int.empty + } + let mergeSubsts = (m1: subst, m2: subst) => + Belt.Map.Int.merge(m1, m2, (_, o1, o2) => + switch (o1, o2) { + | (Some(v), _) | (_, Some(v)) => Some(v) + | (None, None) => None } ) - ->Belt.Set.fromArray(~id=module(IntCmp)) - | App({func, arg}) => Belt.Set.union(freeVarsIn(subst, func), freeVarsIn(subst, arg)) - | Unallowed | Symbol(_) | Schematic(_) => Belt.Set.make(~id=module(IntCmp)) + let rec equivalent = (a: t, b: t) => { + switch (a, b) { + | (Symbol({name: a}), Symbol({name: b})) => a == b + | (Var({idx: ia}), Var({idx: ib})) => ia == ib + | (Schematic({schematic: sa}), Schematic({schematic: sb})) => sa == sb + | (Lam({name: _, body: ba}), Lam({name: _, body: bb})) => equivalent(ba, bb) + | (App({func: fa, arg: aa}), App({func: fb, arg: ab})) => + equivalent(fa, fb) && equivalent(aa, ab) + | (Unallowed, Unallowed) => false + | (_, _) => false + } } -let freeVarsContains = (term: t, subst: subst, idx: int): bool => { - let set = freeVarsIn(subst, term) - set->Belt.Set.has(idx) -} -// f might map an index to a new one (Ok(newIdx)) or to a term (Error(t) with t(from)). -// 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. -let rec mapbind0 = (term: t, f: int => result t>, ~from: int=0): t => - switch term { - | Symbol(_) => term - | Var({idx}) => - if idx >= from { - switch f(idx - from) { - | Ok(newIdx) => - let new = newIdx + from - if new < 0 { - throw(Util.Err("mapbind: negative index")) - } - Var({ - idx: new, - }) - | Error(t) => t(from) - } - } else { - term + type gen = ref + let seen = (g: gen, s: int) => { + if s >= g.contents { + g := s + 1 } - | Schematic({schematic}) => - Schematic({ - schematic: schematic, - }) - | Lam({name, body}) => - Lam({ - name, - body: mapbind0(body, f, ~from=from + 1), - }) - | App({func, arg}) => - App({ - func: mapbind0(func, f, ~from), - arg: mapbind0(arg, f, ~from), - }) - | Unallowed => Unallowed } -let mapbind = (term: t, f: int => int, ~from: int=0): t => mapbind0(term, idx => Ok(f(idx)), ~from) -let upshift = (term: t, amount: int, ~from: int=0) => mapbind(term, idx => idx + amount, ~from) -let downshift = (term: t, amount: int, ~from: int=1) => { - if amount > from { - throw(Util.Err("downshift amount must be less than from")) + let fresh = (g: gen, ~replacing as _=?) => { + let v = g.contents + g := g.contents + 1 + v + } + let rec schematicsIn = (subst: subst, it: t): Belt.Set.t => + switch it { + | Schematic({schematic, _}) if subst->substHas(schematic) => + let found = subst->substGet(schematic)->Option.getExn + schematicsIn(subst, found) + | Schematic({schematic, _}) => Belt.Set.make(~id=module(IntCmp))->Belt.Set.add(schematic) + | Lam({body}) => schematicsIn(subst, body) + | App({func, arg}) => Belt.Set.union(schematicsIn(subst, func), schematicsIn(subst, arg)) + | Unallowed | Symbol(_) | Var(_) => Belt.Set.make(~id=module(IntCmp)) + } + let occ = (schematic: schematic, subst: subst, t: t): bool => { + let set = schematicsIn(subst, t) + set->Belt.Set.has(schematic) + } + let rec freeVarsIn = (subst: subst, it: t): Belt.Set.t => + switch it { + | Schematic({schematic, _}) if subst->substHas(schematic) => + let found = subst->substGet(schematic)->Option.getExn + freeVarsIn(subst, found) + | Var({idx}) => Belt.Set.make(~id=module(IntCmp))->Belt.Set.add(idx) + | Lam({name: _, body}) => + freeVarsIn(subst, body) + ->Belt.Set.toArray + ->Array.filterMap(v => + if v >= 1 { + Some(v - 1) + } else { + None + } + ) + ->Belt.Set.fromArray(~id=module(IntCmp)) + | App({func, arg}) => Belt.Set.union(freeVarsIn(subst, func), freeVarsIn(subst, arg)) + | Unallowed | Symbol(_) | Schematic(_) => Belt.Set.make(~id=module(IntCmp)) + } + let freeVarsContains = (term: t, subst: subst, idx: int): bool => { + let set = freeVarsIn(subst, term) + set->Belt.Set.has(idx) } - mapbind(term, idx => idx - amount, ~from) -} -let lookup = (term: t, subst: array<(t, t)>): option => { - subst - ->Array.find(((from, _)) => equivalent(term, from)) - ->Option.map(((_, to)) => to) -} -let upshift_tt = (subst: array<(t, t)>, ~amount: int=1): array<(t, t)> => { - subst->Array.map(((a, b)) => (upshift(a, amount), upshift(b, amount))) -} -// where pattern unification used mapbind we will need to use discharge for FCU -// -// When `prune` is true, it marks “dead” variables as Unallowed. Nipkow 1993 uses Var(-infinity) for this in the de Bruijn’s notation implementation. -// Nipkow 1993's non de Bruijn implementation handle this logic in `proj`. Similarly Makoto Hamana's paper uses `elem` and `subst` in `prune` -let rec discharge = (subst: array<(t, t)>, term: t, ~prune: bool): t => { - switch lookup(term, subst) { - | Some(found) => found - | None => + // f might map an index to a new one (Ok(newIdx)) or to a term (Error(t) with t(from)). + // 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. + let rec _mapbind0 = (term: t, f: int => result t>, ~from: int=0): t => switch term { + | Symbol(_) => term + | Var({idx}) => + if idx >= from { + switch f(idx - from) { + | Ok(newIdx) => + let new = newIdx + from + if new < 0 { + throw(Util.Err("mapbind: negative index")) + } + Var({ + idx: new, + }) + | Error(t) => t(from) + } + } else { + term + } + | Schematic({schematic}) => + Schematic({ + schematic: schematic, + }) + | Lam({name, body}) => + Lam({ + name, + body: _mapbind0(body, f, ~from=from + 1), + }) | App({func, arg}) => - App({func: discharge(subst, func, ~prune), arg: discharge(subst, arg, ~prune)}) - // Lam case is not actually needed by FCU - | Lam({name, body}) => Lam({name, body: discharge(upshift_tt(subst), body, ~prune)}) - | Var(_) if prune => Unallowed - | Var(_) | Schematic(_) | Symbol(_) | Unallowed => term + App({ + func: _mapbind0(func, f, ~from), + arg: _mapbind0(arg, f, ~from), + }) + | Unallowed => Unallowed } - } -} -let emptySubst: subst = Belt.Map.Int.empty -let substAdd = (subst: subst, schematic: schematic, term: t) => { - assert(schematic >= 0) - assert(subst->Belt.Map.Int.has(schematic) == false) - subst->Belt.Map.Int.set(schematic, term) -} -let rec substitute = (term: t, subst: subst) => - switch term { - | Schematic({schematic, _}) => - switch Belt.Map.Int.get(subst, schematic) { - | None => term + let rec upshift = (term: t, amount: int, ~from: int=0) => + switch term { + | Symbol({name, constructor}) => Symbol({name: Atom.upshift(name, amount, ~from), constructor}) + | Var({idx}) => + Var({ + idx: if idx >= from { + idx + amount + } else { + idx + }, + }) + | Schematic({schematic}) => Schematic({schematic: schematic}) + | Lam({name, body}) => Lam({name, body: upshift(body, amount, ~from=from + 1)}) + | App({func, arg}) => + App({func: upshift(func, amount, ~from), arg: upshift(arg, amount, ~from)}) + | Unallowed => Unallowed + } + let downshift = (term: t, amount: int, ~from: int=1) => { + if amount > from { + throw(Util.Err("downshift amount must be less than from")) + } + upshift(term, -amount, ~from) + } + let lookup = (term: t, subst: array<(t, t)>): option => { + subst + ->Array.find(((from, _)) => equivalent(term, from)) + ->Option.map(((_, to)) => to) + } + let upshift_tt = (subst: array<(t, t)>, ~amount: int=1): array<(t, t)> => { + subst->Array.map(((a, b)) => (upshift(a, amount), upshift(b, amount))) + } + // where pattern unification used mapbind we will need to use discharge for FCU + // + // When `prune` is true, it marks “dead” variables as Unallowed. Nipkow 1993 uses Var(-infinity) for this in the de Bruijn’s notation implementation. + // Nipkow 1993's non de Bruijn implementation handle this logic in `proj`. Similarly Makoto Hamana's paper uses `elem` and `subst` in `prune` + let rec discharge = (subst: array<(t, t)>, term: t, ~prune: bool): t => { + switch lookup(term, subst) { | Some(found) => found + | None => + switch term { + | App({func, arg}) => + App({func: discharge(subst, func, ~prune), arg: discharge(subst, arg, ~prune)}) + // Lam case is not actually needed by FCU + | Lam({name, body}) => Lam({name, body: discharge(upshift_tt(subst), body, ~prune)}) + | Var(_) if prune => Unallowed + | Var(_) | Schematic(_) | Symbol(_) | Unallowed => term + } } - | Lam({name, body}) => - Lam({ - name, - // upshift is not needed for pattern unification, but it is safer to have upshift here - body: substitute(body, subst->Belt.Map.Int.map(t => upshift(t, 1))), - }) - | App({func, arg}) => - App({ - func: substitute(func, subst), - arg: substitute(arg, subst), - }) - | Var(_) | Unallowed | Symbol(_) => term } + let emptySubst: subst = Belt.Map.Int.empty + let substAdd = (subst: subst, schematic: schematic, term: t) => { + assert(schematic >= 0) + assert(subst->Belt.Map.Int.has(schematic) == false) + subst->Belt.Map.Int.set(schematic, term) + } + let rec substitute = (term: t, subst: subst) => + switch term { + | Schematic({schematic, _}) => + switch Belt.Map.Int.get(subst, schematic) { + | None => term + | Some(found) => found + } + | Lam({name, body}) => + Lam({ + name, + // upshift is not needed for pattern unification, but it is safer to have upshift here + body: substitute(body, subst->Belt.Map.Int.map(t => upshift(t, 1))), + }) + | App({func, arg}) => + App({ + func: substitute(func, subst), + arg: substitute(arg, subst), + }) + | Symbol({name, constructor}) => { + let symbolSubst = subst->Belt.Map.Int.reduce(Map.make(), (acc, k, v) => { + switch v { + | Symbol({name}) => { + acc->Map.set(k, name) + acc + } + | _ => acc + } + }) + Symbol({name: Atom.substitute(name, symbolSubst), constructor}) + } + | Var(_) | Unallowed => term + } -let rec substDeBruijn = (term: t, substs: array, ~from: int=0) => - switch term { - | Symbol(_) => term - | Var({idx: var}) => - if var < from { - term - } else if var - from < Array.length(substs) && var - from >= 0 { - Option.getExn(substs[var - from]) - } else { - Var({idx: var - Array.length(substs)}) + let rec substDeBruijn = (term: t, substs: array, ~from: int=0) => + switch term { + | Symbol({name, constructor}) => + Symbol({ + name: Atom.substDeBruijn( + name, + substs->Array.map(t => + switch t { + | Symbol({name}) => Some(name) + | _ => None + } + ), + ~from, + ), + constructor, + }) + | Var({idx: var}) => + if var < from { + term + } else if var - from < Array.length(substs) && var - from >= 0 { + Option.getExn(substs[var - from]) + } else { + Var({idx: var - Array.length(substs)}) + } + | Schematic({schematic}) => + Schematic({ + schematic: schematic, + }) + | Lam({name, body}) => + Lam({ + name, + body: substDeBruijn(body, substs->Array.map(term => upshift(term, 1)), ~from=from + 1), + }) + | App({func, arg}) => + App({ + func: substDeBruijn(func, substs, ~from), + arg: substDeBruijn(arg, substs, ~from), + }) + | Unallowed => Unallowed } - | Schematic({schematic}) => - Schematic({ - schematic: schematic, - }) - | Lam({name, body}) => - Lam({ - name, - body: substDeBruijn(body, substs->Array.map(term => upshift(term, 1)), ~from=from + 1), - }) - | App({func, arg}) => - App({ - func: substDeBruijn(func, substs, ~from), - arg: substDeBruijn(arg, substs, ~from), - }) - | Unallowed => Unallowed - } -// beta reduced and eta reduced -let rec reduce = (term: t): t => { - switch term { - | Lam({body: App({func, arg: Var({idx: 0})})}) if !(func->freeVarsContains(emptySubst, 0)) => - reduce(downshift(func, 1)) - | App({func, arg}) => - switch reduce(func) { - | Lam({body}) => reduce(substDeBruijn(body, [arg])) - | func => App({func, arg: reduce(arg)}) - } - | Lam({name, body}) => - Lam({ - name, - body: reduce(body), - }) - | Symbol(_) | Var(_) | Schematic(_) => term + // beta reduced and eta reduced + let rec reduce = (term: t): t => { + switch term { + | Lam({body: App({func, arg: Var({idx: 0})})}) if !(func->freeVarsContains(emptySubst, 0)) => + reduce(downshift(func, 1)) + | App({func, arg}) => + switch reduce(func) { + | Lam({body}) => reduce(substDeBruijn(body, [arg])) + | func => App({func, arg: reduce(arg)}) + } + | Lam({name, body}) => + Lam({ + name, + body: reduce(body), + }) + | Symbol(_) | Var(_) | Schematic(_) => term - | Unallowed => Unallowed + | Unallowed => Unallowed + } } -} -let reduceSubst = (subst: subst): subst => { - subst->Belt.Map.Int.map(x => reduce(substitute(x, subst))) -} -let rec lams = (amount: int, term: t): t => { - assert(amount >= 0) - if amount <= 0 { - term - } else { - Lam({ - name: "x", - body: lams(amount - 1, term), - }) + let reduceSubst = (subst: subst): subst => { + subst->Belt.Map.Int.map(x => reduce(substitute(x, subst))) } -} -let rec idx = (is: array, j: t): option => { - if is->Array.length == 0 { - None - } else { - let head = is[0]->Option.getExn - let tail = is->Array.sliceToEnd(~start=1) - if equivalent(head, j) { - Some(tail->Array.length) + let rec lams = (amount: int, term: t): t => { + assert(amount >= 0) + if amount <= 0 { + term } else { - idx(tail, j) + Lam({ + name: "x", + body: lams(amount - 1, term), + }) } } -} -let idx1' = (is: array, j: t): t => { - switch idx(is, j) { - | None => Unallowed - | Some(idx) => Var({idx: idx}) + let rec idx = (is: array, j: t): option => { + if is->Array.length == 0 { + None + } else { + let head = is[0]->Option.getExn + let tail = is->Array.sliceToEnd(~start=1) + if equivalent(head, j) { + Some(tail->Array.length) + } else { + idx(tail, j) + } + } } -} -let _idx1 = (is: array, j: int): t => idx1'(is, Var({idx: j})) -let idx2' = (is: array, j: t): result t> => { - switch idx(is, j) { - | None => Error(_ => Unallowed) - | Some(idx) => Ok(idx) + let idx1' = (is: array, j: t): t => { + switch idx(is, j) { + | None => Unallowed + | Some(idx) => Var({idx: idx}) + } } -} -let _idx2 = (is: array, j: int) => idx2'(is, Var({idx: j})) -let rec app = (term: t, args: array): t => { - if args->Array.length == 0 { - term - } else { - let head = args[0]->Option.getExn - let rest = args->Array.sliceToEnd(~start=1) - app(App({func: term, arg: head}), rest) + let _idx1 = (is: array, j: int): t => idx1'(is, Var({idx: j})) + let idx2' = (is: array, j: t): result t> => { + switch idx(is, j) { + | None => Error(_ => Unallowed) + | Some(idx) => Ok(idx) + } } -} -exception UnifyFail(string) -let rec red = (term: t, is: array): t => { - switch term { - | _ if is->Array.length == 0 => term - | Lam({body}) => red(substDeBruijn(body, [is[0]->Option.getExn]), is->Array.sliceToEnd(~start=1)) - | term => app(term, is) + let _idx2 = (is: array, j: int) => idx2'(is, Var({idx: j})) + let rec app = (term: t, args: array): t => { + if args->Array.length == 0 { + term + } else { + let head = args[0]->Option.getExn + let rest = args->Array.sliceToEnd(~start=1) + app(App({func: term, arg: head}), rest) + } } -} -let lam = (is: array, g: t, js: array): t => { - lams(is->Array.length, app(g, js->Array.map(j => idx1'(is, j)))) -} -let rec strip = (term: t): (t, array) => { - switch term { - | App({func, arg}) => - let (peeledFunc, peeledArgs) = strip(func) - (peeledFunc, Array.concat(peeledArgs, [arg])) - | _ => (term, []) + exception UnifyFail(string) + let rec red = (term: t, is: array): t => { + switch term { + | _ if is->Array.length == 0 => term + | Lam({body}) => + red(substDeBruijn(body, [is[0]->Option.getExn]), is->Array.sliceToEnd(~start=1)) + | term => app(term, is) + } } -} -let rec devar = (subst: subst, term: t): t => { - let (func, args) = strip(term) - switch func { - | Schematic({schematic}) if substHas(subst, schematic) => - devar(subst, red(substGet(subst, schematic)->Option.getExn, args)) - | _ => term + let lam = (is: array, g: t, js: array): t => { + lams(is->Array.length, app(g, js->Array.map(j => idx1'(is, j)))) } -} -let mkvars = (n: int): array => { - Belt.Array.init(n, i => n - i - 1)->Array.map(x => Var({idx: x})) -} -let rec proj_allowed = (subst: subst, term: t): bool => { - let term' = devar(subst, term) - switch term' { - | Lam(_) | Unallowed | Schematic(_) | Symbol(_) => false - | Var(_) => true // pattern unification only allows this - // FCU allows this: - | App(_) => - switch strip(term') { - | (Symbol(_) | Var(_), args) => Array.every(args, x => proj_allowed(subst, x)) - | _ => false + let rec strip = (term: t): (t, array) => { + switch term { + | App({func, arg}) => + let (peeledFunc, peeledArgs) = strip(func) + (peeledFunc, Array.concat(peeledArgs, [arg])) + | _ => (term, []) } } -} -// this function is called proj in Nipkow 1993 and it is called pruning in FCU paper -let rec proj = (subst: subst, term: t, ~gen: option): subst => { - switch strip(devar(subst, term)) { - | (Lam({name: _, body}), args) if args->Array.length == 0 => proj(subst, body, ~gen) - | (Unallowed, _args) => throw(UnifyFail("unallowed")) - | (Symbol(_) | Var(_), args) => Array.reduce(args, subst, (acc, a) => proj(acc, a, ~gen)) - | (Schematic({schematic}), args) => { - assert(!substHas(subst, schematic)) - if gen->Option.isNone { - throw(UnifyFail("no gen provided")) + let rec devar = (subst: subst, term: t): t => { + let (func, args) = strip(term) + switch func { + | Schematic({schematic}) if substHas(subst, schematic) => + devar(subst, red(substGet(subst, schematic)->Option.getExn, args)) + | _ => term + } + } + let mkvars = (n: int): array => { + Belt.Array.init(n, i => n - i - 1)->Array.map(x => Var({idx: x})) + } + let rec proj_allowed = (subst: subst, term: t): bool => { + let term' = devar(subst, term) + switch term' { + | Lam(_) | Unallowed | Schematic(_) | Symbol(_) => false + | Var(_) => true // pattern unification only allows this + // FCU allows this: + | App(_) => + switch strip(term') { + | (Symbol(_) | Var(_), args) => Array.every(args, x => proj_allowed(subst, x)) + | _ => false } - let h = Schematic({schematic: fresh(Option.getExn(gen))}) - subst->substAdd( - schematic, - lams( - args->Array.length, - app( - h, - Belt.Array.init(args->Array.length, j => { - if proj_allowed(subst, args[j]->Option.getExn) { - Some(Var({idx: args->Belt.Array.length - j - 1})) - } else { - None - } - })->Array.keepSome, - ), - ), - ) } - | _ => throw(UnifyFail("not a symbol, var or schematic")) } -} -let flexflex = ( - sa: schematic, - xs: array, - sb: schematic, - ys: array, - subst: subst, - ~gen: option, -): subst => { - if gen->Option.isNone { - throw(UnifyFail("no gen provided")) - } - if sa == sb { - if xs->Array.length != ys->Array.length { - throw(UnifyFail("flexible schematics have different number of arguments")) - } - let len = xs->Array.length - let h = Schematic({schematic: fresh(Option.getExn(gen))}) - let xs = Belt.Array.init(len, k => { - let a = xs[k]->Option.getExn - let b = ys[k]->Option.getExn - if equivalent(a, b) { - Some(Var({idx: len - k - 1})) - } else { - None + // this function is called proj in Nipkow 1993 and it is called pruning in FCU paper + let rec proj = (subst: subst, term: t, ~gen: option): subst => { + switch strip(devar(subst, term)) { + | (Lam({name: _, body}), args) if args->Array.length == 0 => proj(subst, body, ~gen) + | (Unallowed, _args) => throw(UnifyFail("unallowed")) + | (Symbol(_) | Var(_), args) => Array.reduce(args, subst, (acc, a) => proj(acc, a, ~gen)) + | (Schematic({schematic}), args) => { + assert(!substHas(subst, schematic)) + if gen->Option.isNone { + throw(UnifyFail("no gen provided")) + } + let h = Schematic({schematic: fresh(Option.getExn(gen))}) + subst->substAdd( + schematic, + lams( + args->Array.length, + app( + h, + Belt.Array.init(args->Array.length, j => { + if proj_allowed(subst, args[j]->Option.getExn) { + Some(Var({idx: args->Belt.Array.length - j - 1})) + } else { + None + } + })->Array.keepSome, + ), + ), + ) } - })->Array.keepSome - subst->substAdd(sa, lams(len, app(h, xs))) - } else { - let common = xs->Array.filter(x => ys->Belt.Array.some(y => equivalent(x, y))) - let h = Schematic({schematic: fresh(Option.getExn(gen))}) - subst->substAdd(sa, lam(xs, h, common))->substAdd(sb, lam(ys, h, common)) + | _ => throw(UnifyFail("not a symbol, var or schematic")) + } } -} -let flexrigid = (sa: schematic, xs: array, b: t, subst: subst, ~gen: option): subst => { - if occ(sa, subst, b) { - throw(UnifyFail("flexible schematic occurs in rigid term")) - } - // pattern unification - // let u = b->mapbind0(bind => idx2(xs, bind)) - // FCU - let zn = mkvars(xs->Array.length) - // we reversed it so that the last one will be picked if there are duplicates. This behaviour helps certain real world cases. - let u = discharge(Belt.Array.reverse(Belt.Array.zip(xs, zn)), b, ~prune=true) - proj(subst->substAdd(sa, lams(xs->Array.length, u)), u, ~gen) -} -let rec unifyTerm = (a: t, b: t, subst: subst, ~gen: option): subst => - switch (devar(subst, a), devar(subst, b)) { - | (Symbol({name: na}), Symbol({name: nb})) => - if na == nb { - subst + let flexflex = ( + sa: schematic, + xs: array, + sb: schematic, + ys: array, + subst: subst, + ~gen: option, + ): subst => { + if gen->Option.isNone { + throw(UnifyFail("no gen provided")) + } + if sa == sb { + if xs->Array.length != ys->Array.length { + throw(UnifyFail("flexible schematics have different number of arguments")) + } + let len = xs->Array.length + let h = Schematic({schematic: fresh(Option.getExn(gen))}) + let xs = Belt.Array.init(len, k => { + let a = xs[k]->Option.getExn + let b = ys[k]->Option.getExn + if equivalent(a, b) { + Some(Var({idx: len - k - 1})) + } else { + None + } + })->Array.keepSome + subst->substAdd(sa, lams(len, app(h, xs))) } else { - throw(UnifyFail("symbols do not match")) + let common = xs->Array.filter(x => ys->Belt.Array.some(y => equivalent(x, y))) + let h = Schematic({schematic: fresh(Option.getExn(gen))}) + subst->substAdd(sa, lam(xs, h, common))->substAdd(sb, lam(ys, h, common)) + } + } + let flexrigid = (sa: schematic, xs: array, b: t, subst: subst, ~gen: option): subst => { + if occ(sa, subst, b) { + throw(UnifyFail("flexible schematic occurs in rigid term")) + } + // pattern unification + // let u = b->_mapbind0(bind => idx2(xs, bind)) + // FCU + let zn = mkvars(xs->Array.length) + // we reversed it so that the last one will be picked if there are duplicates. This behaviour helps certain real world cases. + let u = discharge(Belt.Array.reverse(Belt.Array.zip(xs, zn)), b, ~prune=true) + proj(subst->substAdd(sa, lams(xs->Array.length, u)), u, ~gen) + } + let rec integrateAtomSubst = (atomSubst: Atom.subst, subst: subst, ~gen: option): subst => + atomSubst + ->Map.entries + ->Iterator.toArray + ->Array.reduce(subst, (acc, (schematic, term)) => + if acc->substHas(schematic) { + unifyTermFirst( + acc->substGet(schematic)->Option.getExn, + Symbol({name: term, constructor: false}), + acc, + ~gen, + ) + } else { + acc->substAdd(schematic, Symbol({name: term, constructor: false})) + } + ) + and unifyAtom = (a: Atom.t, b: Atom.t, subst: subst, ~gen: option): Seq.t => + Atom.unify(a, b)->Seq.filterMap(atomSubst => + try { + Some(integrateAtomSubst(atomSubst, subst, ~gen)) + } catch { + | UnifyFail(_) => None + } + ) + and unifyTerm = (a: t, b: t, subst: subst, ~gen: option): Seq.t => + switch (devar(subst, a), devar(subst, b)) { + | (Symbol({name: a}), Symbol({name: b})) => unifyAtom(a, b, subst, ~gen) + | (Var({idx: ia}), Var({idx: ib})) => + if ia == ib { + Seq.once(subst) + } else { + Seq.empty + } + | (Schematic({schematic: sa}), Schematic({schematic: sb})) if sa == sb => Seq.once(subst) + | (Lam({name: _, body: ba}), Lam({name: _, body: bb})) => unifyTerm(ba, bb, subst, ~gen) + | (Lam({name: _, body: ba}), b) => + unifyTerm(ba, App({func: upshift(b, 1), arg: Var({idx: 0})}), subst, ~gen) + | (a, Lam({name: _, body: bb})) => + unifyTerm(App({func: upshift(a, 1), arg: Var({idx: 0})}), bb, subst, ~gen) + | (a, b) => + switch (strip(a), strip(b)) { + | ((Schematic({schematic: sa}), xs), (Schematic({schematic: sb}), ys)) => + try { + Seq.once(flexflex(sa, xs, sb, ys, subst, ~gen)) + } catch { + | UnifyFail(_) => Seq.empty + } + | ((Schematic({schematic: sa}), xs), _) => + try { + Seq.once(flexrigid(sa, xs, b, subst, ~gen)) + } catch { + | UnifyFail(_) => Seq.empty + } + | (_, (Schematic({schematic: sb}), ys)) => + try { + Seq.once(flexrigid(sb, ys, a, subst, ~gen)) + } catch { + | UnifyFail(_) => Seq.empty + } + | ((a, xs), (b, ys)) => + switch (a, b) { + | (Symbol(_) | Var(_), Symbol(_) | Var(_)) => + unifyTerm(a, b, subst, ~gen)->Seq.flatMap(subst => unifyArray(xs, ys, subst, ~gen)) + | _ => Seq.empty + } + } } - | (Var({idx: ia}), Var({idx: ib})) => - if ia == ib { - subst + and unifyArray = (xs: array, ys: array, subst: subst, ~gen: option): Seq.t => { + if xs->Array.length != ys->Array.length { + Seq.empty + } else if xs->Array.length == 0 { + Seq.once(subst) } else { - throw(UnifyFail("variables do not match")) - } - | (Schematic({schematic: sa}), Schematic({schematic: sb})) if sa == sb => subst - | (Lam({name: _, body: ba}), Lam({name: _, body: bb})) => unifyTerm(ba, bb, subst, ~gen) - | (Lam({name: _, body: ba}), b) => - unifyTerm(ba, App({func: upshift(b, 1), arg: Var({idx: 0})}), subst, ~gen) - | (a, Lam({name: _, body: bb})) => - unifyTerm(App({func: upshift(a, 1), arg: Var({idx: 0})}), bb, subst, ~gen) - | (a, b) => - switch (strip(a), strip(b)) { - | ((Schematic({schematic: sa}), xs), (Schematic({schematic: sb}), ys)) => - flexflex(sa, xs, sb, ys, subst, ~gen) - | ((Schematic({schematic: sa}), xs), _) => flexrigid(sa, xs, b, subst, ~gen) - | (_, (Schematic({schematic: sb}), ys)) => flexrigid(sb, ys, a, subst, ~gen) - | ((a, xs), (b, ys)) => - switch (a, b) { - | (Symbol(_) | Var(_), Symbol(_) | Var(_)) => rigidrigid(a, xs, b, ys, subst, ~gen) + let x = xs[0]->Option.getExn + let y = ys[0]->Option.getExn + let restXs = xs->Array.sliceToEnd(~start=1) + let restYs = ys->Array.sliceToEnd(~start=1) + unifyTerm(x, y, subst, ~gen)->Seq.flatMap(subst => unifyArray(restXs, restYs, subst, ~gen)) + } + } + and unifyTermFirst = (a: t, b: t, subst: subst, ~gen: option): subst => + switch unifyTerm(a, b, subst, ~gen)->Seq.head { + | Some(subst) => subst + | None => + switch (devar(subst, a), devar(subst, b)) { + | (Symbol(_), Symbol(_)) => throw(UnifyFail("symbols do not match")) + | (Var(_), Var(_)) => throw(UnifyFail("variables do not match")) | _ => throw(UnifyFail("no rules match")) } } - } -and unifyArray = (xs: array, ys: array, subst: subst, ~gen: option): subst => { - if xs->Array.length != ys->Array.length { - throw(UnifyFail("arrays have different lengths")) - } - Belt.Array.zip(xs, ys)->Belt.Array.reduce(subst, (acc, (x, y)) => unifyTerm(x, y, acc, ~gen)) -} -and rigidrigid = ( - a: t, - xs: array, - b: t, - ys: array, - subst: subst, - ~gen: option, -): subst => { - if !equivalent(a, b) { - throw(UnifyFail("rigid terms do not match")) - } - if xs->Array.length != ys->Array.length { - throw(UnifyFail("rigid terms have different number of arguments")) - } - unifyArray(xs, ys, subst, ~gen) -} -let unify = (a: t, b: t, ~gen=?) => - Seq.fromArray( + let unify = (a: t, b: t, ~gen=?) => unifyTerm(a, b, emptySubst, ~gen) + let rec rewrite = (term: t, from: t, to: t, ~subst: subst, ~gen: option): (subst, t) => { try { - [unifyTerm(a, b, emptySubst, ~gen)] + let subst1 = unifyTermFirst(term, from, subst, ~gen) + (subst1, to) } catch { - | UnifyFail(_) => [] - }, - ) -let rec rewrite = (term: t, from: t, to: t, ~subst: subst, ~gen: option): (subst, t) => { - try { - let subst1 = unifyTerm(term, from, subst, ~gen) - (subst1, to) - } catch { - | UnifyFail(_) => - switch term { - | Schematic({schematic}) if subst->substHas(schematic) => - rewrite(subst->substGet(schematic)->Option.getExn, from, to, ~subst, ~gen) - | Var(_) | Unallowed | Symbol(_) | Schematic(_) => (subst, term) - | Lam({name, body}) => { - let (subst1, body1) = rewrite(body, from, to, ~subst, ~gen) - (subst1, Lam({name, body: body1})) - } - | App({func, arg}) => { - let (subst1, func') = rewrite(func, from, to, ~subst, ~gen) - let (subst2, arg') = rewrite(arg, from, to, ~subst=subst1, ~gen) - (subst2, App({func: func', arg: arg'})) + | UnifyFail(_) => + switch term { + | Schematic({schematic}) if subst->substHas(schematic) => + rewrite(subst->substGet(schematic)->Option.getExn, from, to, ~subst, ~gen) + | Var(_) | Unallowed | Symbol(_) | Schematic(_) => (subst, term) + | Lam({name, body}) => { + let (subst1, body1) = rewrite(body, from, to, ~subst, ~gen) + (subst1, Lam({name, body: body1})) + } + | App({func, arg}) => { + let (subst1, func') = rewrite(func, from, to, ~subst, ~gen) + let (subst2, arg') = rewrite(arg, from, to, ~subst=subst1, ~gen) + (subst2, App({func: func', arg: arg'})) + } } } } -} -let place = (x: int, ~scope: array) => - app( - Schematic({ - schematic: x, - }), - Array.fromInitializer(~length=Array.length(scope), i => Var({idx: i})), - ) + let place = (x: int, ~scope: array) => + app( + Schematic({ + schematic: x, + }), + Array.fromInitializer(~length=Array.length(scope), i => Var({idx: i})), + ) -let prettyPrintVar = (idx: int, scope: array) => - switch scope[idx] { - | Some(n) if Array.indexOf(scope, n) == idx => n - | _ => "\\"->String.concat(String.make(idx)) + let prettyPrintVar = (idx: int, scope: array) => + switch scope[idx] { + | Some(n) if Array.indexOf(scope, n) == idx => n + | _ => "\\"->String.concat(String.make(idx)) + } + let makeGen = () => { + ref(0) + } + let rec stripLam = (it: t): (array, t) => + switch it { + | Lam({name, body}) => + let (names, body) = stripLam(body) + (Array.concat([name], names), body) + | _ => ([], it) + } + let rec prettyPrint = (it: t, ~scope: array) => + switch it { + | Symbol({name, constructor}) => + if constructor { + String.concat("@", Atom.prettyPrint(name, ~scope)) + } else { + Atom.prettyPrint(name, ~scope) + } + | Var({idx}) => prettyPrintVar(idx, scope) + | Schematic({schematic}) => "?"->String.concat(String.make(schematic)) + | Lam(_) => + let (names, body) = stripLam(it) + let (func, args) = strip(body) + let bodies = Array.concat([func], args) + let innerScope = Array.concat(Array.toReversed(names), scope) + "(" + ->String.concat(Array.join(names->Array.map(name => String.concat(name, ".")), " ")) + ->String.concat(" ") + ->String.concat(Array.join(bodies->Array.map(e => prettyPrint(e, ~scope=innerScope)), " ")) + ->String.concat(")") + | App(_) => + let (func, args) = strip(it) + "(" + ->String.concat(prettyPrint(func, ~scope)) + ->String.concat(" ") + ->String.concat(Array.join(args->Array.map(e => prettyPrint(e, ~scope)), " ")) + ->String.concat(")") + | Unallowed => "" + } + let prettyPrintSubst = (sub: subst, ~scope: array) => + Util.prettyPrintIntMap(sub, ~showV=t => prettyPrint(t, ~scope)) + let nameRES = "^([^\\s.\\[\\]()]+)\\." + exception ParseError(string) + type token = + | LParen + | RParen + | VarT(int) + | SchematicT(int) + | AtomT(Atom.t) + | ConsT(Atom.t) + | NameT(string) + | EOF + let varRegexpString = "^\\\\([0-9]+)" + let schematicRegexpString = "^\\?([0-9]+)" + let atomToken = (str: string, ~scope: array, ~gen=?) => { + switch Atom.parse(str, ~scope, ~gen?) { + | Ok((atom, rest)) => (atom, rest) + | Error(msg) => throw(ParseError(msg)) + } } -let makeGen = () => { - ref(0) -} -let rec stripLam = (it: t): (array, t) => - switch it { - | Lam({name, body}) => - let (names, body) = stripLam(body) - (Array.concat([name], names), body) - | _ => ([], it) - } -let rec prettyPrint = (it: t, ~scope: array) => - switch it { - | Symbol({name, constructor}) => - if constructor { - String.concat("@", name) - } else { - name - } - | Var({idx}) => prettyPrintVar(idx, scope) - | Schematic({schematic}) => "?"->String.concat(String.make(schematic)) - | Lam(_) => - let (names, body) = stripLam(it) - let (func, args) = strip(body) - let bodies = Array.concat([func], args) - let innerScope = Array.concat(Array.toReversed(names), scope) - "(" - ->String.concat(Array.join(names->Array.map(name => String.concat(name, ".")), " ")) - ->String.concat(" ") - ->String.concat(Array.join(bodies->Array.map(e => prettyPrint(e, ~scope=innerScope)), " ")) - ->String.concat(")") - | App(_) => - let (func, args) = strip(it) - "(" - ->String.concat(prettyPrint(func, ~scope)) - ->String.concat(" ") - ->String.concat(Array.join(args->Array.map(e => prettyPrint(e, ~scope)), " ")) - ->String.concat(")") - | Unallowed => "" - } -let prettyPrintSubst = (sub: subst, ~scope: array) => - Util.prettyPrintIntMap(sub, ~showV=t => prettyPrint(t, ~scope)) -let symbolRegexpString = "^([^\\s()]+)" -let nameRES = "^([^\\s.\\[\\]()]+)\\." -exception ParseError(string) -type token = - | LParen - | RParen - | VarT(int) - | SchematicT(int) - | AtomT(string) - | ConsT(string) - | NameT(string) - | EOF -let varRegexpString = "^\\\\([0-9]+)" -let schematicRegexpString = "^\\?([0-9]+)" -let tokenize = (str0: string): (token, string) => { - let str = str0->String.trimStart - if str->String.length == 0 { - (EOF, "") - } else { - let rest = () => str->String.sliceToEnd(~start=1) - switch str->String.charAt(0) { - | "(" => (LParen, rest()) - | ")" => (RParen, rest()) - | "\\" => { - let re = RegExp.fromStringWithFlags(varRegexpString, ~flags="y") - switch re->RegExp.exec(str) { - | None => throw(ParseError("invalid variable")) - | Some(res) => - switch RegExp.Result.matches(res) { - | [n] => ( - VarT(n->Int.fromString->Option.getExn), - String.sliceToEnd(str, ~start=RegExp.lastIndex(re)), - ) - | _ => throw(ParseError("invalid variable")) + let scopeVarToken = (str: string, scope: array): option<(int, string)> => { + let result = ref(None) + scope->Array.forEachWithIndex((name, idx) => { + let len = String.length(name) + let matches = + String.slice(str, ~start=0, ~end=len) == name && + switch str->String.charAt(len) { + | "" | " " | "\t" | "\n" | "\r" | "(" | ")" => true + | _ => false } - } + if result.contents == None && matches { + result := Some((idx, str->String.sliceToEnd(~start=len))) } - | "?" => { - let re = RegExp.fromStringWithFlags(schematicRegexpString, ~flags="y") - switch re->RegExp.exec(str) { - | None => throw(ParseError("invalid schematic")) - | Some(res) => - switch RegExp.Result.matches(res) { - | [n] => ( - SchematicT(n->Int.fromString->Option.getExn), - String.sliceToEnd(str, ~start=RegExp.lastIndex(re)), - ) - | _ => throw(ParseError("invalid schematic")) + }) + result.contents + } + let tokenize = (str0: string, ~scope: array, ~gen=?): (token, string) => { + let str = str0->String.trimStart + if str->String.length == 0 { + (EOF, "") + } else { + let rest = () => str->String.sliceToEnd(~start=1) + switch str->String.charAt(0) { + | "(" => (LParen, rest()) + | ")" => (RParen, rest()) + | "\\" => { + let re = RegExp.fromStringWithFlags(varRegexpString, ~flags="y") + switch re->RegExp.exec(str) { + | None => throw(ParseError("invalid variable")) + | Some(res) => + switch RegExp.Result.matches(res) { + | [n] => ( + VarT(n->Int.fromString->Option.getExn), + String.sliceToEnd(str, ~start=RegExp.lastIndex(re)), + ) + | _ => throw(ParseError("invalid variable")) + } } } - } - | "@" => - let re = RegExp.fromStringWithFlags(symbolRegexpString, ~flags="y") - switch re->RegExp.exec(rest()) { - | None => throw(ParseError("invalid symbol")) - | Some(res) => - switch RegExp.Result.matches(res) { - | [n] => (ConsT(n), String.sliceToEnd(rest(), ~start=RegExp.lastIndex(re))) - | _ => throw(ParseError("invalid symbol")) - } - } - | _ => { - let reName = RegExp.fromStringWithFlags(nameRES, ~flags="y") - switch reName->RegExp.exec(str) { - | Some(res) => - switch RegExp.Result.matches(res) { - | [n] => (NameT(n), String.sliceToEnd(str, ~start=RegExp.lastIndex(reName))) - | _ => throw(ParseError("invalid symbol")) - } - | None => - let re = RegExp.fromStringWithFlags(symbolRegexpString, ~flags="y") + | "?" => { + let re = RegExp.fromStringWithFlags(schematicRegexpString, ~flags="y") switch re->RegExp.exec(str) { - | None => throw(ParseError("invalid symbol")) + | None => throw(ParseError("invalid schematic")) | Some(res) => switch RegExp.Result.matches(res) { - | [n] => (AtomT(n), String.sliceToEnd(str, ~start=RegExp.lastIndex(re))) + | [n] => ( + SchematicT(n->Int.fromString->Option.getExn), + String.sliceToEnd(str, ~start=RegExp.lastIndex(re)), + ) + | _ => throw(ParseError("invalid schematic")) + } + } + } + | "@" => + let (raw, rest) = atomToken(rest(), ~scope, ~gen?) + (ConsT(raw), rest) + | _ => { + let reName = RegExp.fromStringWithFlags(nameRES, ~flags="y") + switch reName->RegExp.exec(str) { + | Some(res) => + switch RegExp.Result.matches(res) { + | [n] => (NameT(n), String.sliceToEnd(str, ~start=RegExp.lastIndex(reName))) | _ => throw(ParseError("invalid symbol")) } + | None => + switch scopeVarToken(str, scope) { + | Some((idx, rest)) => (VarT(idx), rest) + | None => + let (atom, rest) = atomToken(str, ~scope, ~gen?) + (AtomT(atom), rest) + } } } } } } -} -type rec simple = - | ListS({xs: array}) - | AtomS({name: string, constructor: bool}) - | VarS({idx: int}) - | SchematicS({schematic: int}) - | LambdaS({name: string, body: simple}) -let rec parseSimple = (str: string): (simple, string) => { - let (t0, rest) = tokenize(str) - switch t0 { - | LParen => { - let (t1, rest1) = tokenize(rest) - switch t1 { - | NameT(name) => { - let (result, rest2) = parseSimple("("->String.concat(rest1)) - (LambdaS({name, body: result}), rest2) - } - | RParen => (ListS({xs: []}), rest1) - | _ => { - let (head, rest2) = parseSimple(rest) - let (tail, rest3) = parseSimple("("->String.concat(rest2)) - switch tail { - | ListS({xs}) => (ListS({xs: Array.concat([head], xs)}), rest3) - | _ => throw(Util.Unreachable("bug")) + type rec simple = + | ListS({xs: array}) + | AtomS({name: Atom.t, constructor: bool}) + | VarS({idx: int}) + | SchematicS({schematic: int}) + | LambdaS({name: string, body: simple}) + let rec parseSimple = (str: string, ~scope: array, ~gen=?): (simple, string) => { + let (t0, rest) = tokenize(str, ~scope, ~gen?) + switch t0 { + | LParen => { + let (t1, rest1) = tokenize(rest, ~scope, ~gen?) + switch t1 { + | NameT(name) => { + let (result, rest2) = parseSimple( + "("->String.concat(rest1), + ~scope=Array.concat([name], scope), + ~gen?, + ) + (LambdaS({name, body: result}), rest2) + } + | RParen => (ListS({xs: []}), rest1) + | _ => { + let (head, rest2) = parseSimple(rest, ~scope, ~gen?) + let (tail, rest3) = parseSimple("("->String.concat(rest2), ~scope, ~gen?) + switch tail { + | ListS({xs}) => (ListS({xs: Array.concat([head], xs)}), rest3) + | _ => throw(Util.Unreachable("bug")) + } } } } + | RParen => throw(ParseError("unexpected right parenthesis")) + | VarT(idx) => (VarS({idx: idx}), rest) + | SchematicT(schematic) => (SchematicS({schematic: schematic}), rest) + | AtomT(name) => (AtomS({name, constructor: false}), rest) + | ConsT(name) => (AtomS({name, constructor: true}), rest) + | NameT(name) => { + let (result, rest1) = parseSimple(rest, ~scope=Array.concat([name], scope), ~gen?) + (LambdaS({name, body: result}), rest1) + } + | EOF => throw(ParseError("unexpected end of file")) } - | RParen => throw(ParseError("unexpected right parenthesis")) - | VarT(idx) => (VarS({idx: idx}), rest) - | SchematicT(schematic) => (SchematicS({schematic: schematic}), rest) - | AtomT(name) => (AtomS({name, constructor: false}), rest) - | ConsT(name) => (AtomS({name, constructor: true}), rest) - | NameT(name) => { - let (result, rest1) = parseSimple(rest) - (LambdaS({name, body: result}), rest1) - } - | EOF => throw(ParseError("unexpected end of file")) } -} -type env = Map.t -let incrEnv = (env: env): env => { - let nu: env = Map.make() - Map.entries(env)->Iterator.forEach(opt => - switch opt { - | None => () - | Some((key, value)) => nu->Map.set(key, value + 1) - } - ) - nu -} -let envFromScope = (scope: array): env => { - let nu: env = Map.make() - scope->Array.forEachWithIndex((name, idx) => { - nu->Map.set(name, idx) - }) - nu -} -let envPushLambda = (env: env, name: string): env => { - let nu = incrEnv(env) - nu->Map.set(name, 0) - nu -} -let rec parseAll = (simple: simple, ~env: env, ~gen=?): t => { - switch simple { - | ListS({xs}) => { - let ts = xs->Array.map(x => parseAll(x, ~env, ~gen?)) - if ts->Array.length == 0 { - throw(ParseError("empty list")) - } else { - ts - ->Array.sliceToEnd(~start=1) - ->Array.reduce(ts[0]->Option.getExn, (acc, x) => App({func: acc, arg: x})) + let rec parseAll = (simple: simple, ~gen=?): t => { + switch simple { + | ListS({xs}) => { + let ts = xs->Array.map(x => parseAll(x, ~gen?)) + if ts->Array.length == 0 { + throw(ParseError("empty list")) + } else { + ts + ->Array.sliceToEnd(~start=1) + ->Array.reduce(ts[0]->Option.getExn, (acc, x) => App({func: acc, arg: x})) + } } - } - | AtomS({name, constructor}) => - if constructor { - Symbol({name, constructor: true}) - } else if env->Map.has(name) { - let idx = env->Map.get(name)->Option.getExn - Var({idx: idx}) - } else { - Symbol({name, constructor: false}) - } - | VarS({idx}) => Var({idx: idx}) - | SchematicS({schematic}) => - switch gen { - | Some(g) => { - seen(g, schematic) - Schematic({schematic: schematic}) + | AtomS({name, constructor}) => Symbol({name, constructor}) + | VarS({idx}) => Var({idx: idx}) + | SchematicS({schematic}) => + switch gen { + | Some(g) => { + seen(g, schematic) + Schematic({schematic: schematic}) + } + | None => throw(ParseError("Schematics not allowed here")) } - | None => throw(ParseError("Schematics not allowed here")) + | LambdaS({name, body}) => + Lam({ + name, + body: parseAll(body, ~gen?), + }) } - | LambdaS({name, body}) => - Lam({ - name, - body: parseAll(body, ~env=envPushLambda(env, name), ~gen?), - }) } -} -let prettyPrintMeta = (str: string) => { - String.concat(str, ".") -} -let parseMeta = (str: string) => { - let re = RegExp.fromStringWithFlags(nameRES, ~flags="y") - switch re->RegExp.exec(str->String.trim) { - | None => Error("not a meta name") - | Some(res) => - switch RegExp.Result.matches(res) { - | [n] => Ok(n, String.sliceToEnd(str->String.trim, ~start=RegExp.lastIndex(re))) - | _ => Error("impossible happened") + let prettyPrintMeta = (str: string) => { + String.concat(str, ".") + } + let parseMeta = (str: string) => { + let re = RegExp.fromStringWithFlags(nameRES, ~flags="y") + switch re->RegExp.exec(str->String.trim) { + | None => Error("not a meta name") + | Some(res) => + switch RegExp.Result.matches(res) { + | [n] => Ok(n, String.sliceToEnd(str->String.trim, ~start=RegExp.lastIndex(re))) + | _ => Error("impossible happened") + } } } -} -let parse = (str: string, ~scope: array, ~gen=?) => { - try { - let (simple, rest) = parseSimple(str) - Ok((parseAll(simple, ~env=envFromScope(scope), ~gen?), rest)) - } catch { - | ParseError(msg) => Error(msg) + let parse = (str: string, ~scope: array, ~gen=?) => { + try { + let (simple, rest) = parseSimple(str, ~scope, ~gen?) + Ok((parseAll(simple, ~gen?), rest)) + } catch { + | ParseError(msg) => Error(msg) + } } + + let concrete = t => + switch t { + | Schematic(_) => false + | Symbol({name}) => Atom.concrete(name) + | _ => true + } + let mapTerms = (t, f) => f(t) } -let concrete = t => - switch t { - | Schematic(_) => false - | _ => true - } -let mapTerms = (t, f) => f(t) +include Make(DefaultAtom) diff --git a/src/HOTerm.resi b/src/HOTerm.resi index 8d7a3ab..cd30a99 100644 --- a/src/HOTerm.resi +++ b/src/HOTerm.resi @@ -1,3 +1,33 @@ +module type ATOM = AtomDef.ATOM + +module Make: (Atom: AtomDef.ATOM) => +{ + type rec t = + | Symbol({name: Atom.t, constructor: bool}) + | Var({idx: int}) + | Schematic({schematic: int}) + | Lam({name: string, body: t}) + | App({func: t, arg: t}) + | Unallowed + + include Signatures.TERM + with type t := t + and type meta = string + and type schematic = int + and type subst = Belt.Map.Int.t + + let emptySubst: subst + let strip: t => (t, array) + let app: (t, array) => t + let mkvars: int => array + let mapTerms: (t, t => t) => t + exception UnifyFail(string) + let substAdd: (subst, schematic, t) => subst + let unifyTerm: (t, t, subst, ~gen: option) => Seq.t + let reduceSubst: subst => subst + let rewrite: (t, t, t, ~subst: subst, ~gen: option) => (subst, t) +} + type rec t = | Symbol({name: string, constructor: bool}) | Var({idx: int}) @@ -21,6 +51,6 @@ let mapTerms: (t, t => t) => t // exposed for testing purposes exception UnifyFail(string) let substAdd: (subst, schematic, t) => subst -let unifyTerm: (t, t, subst, ~gen: option) => subst +let unifyTerm: (t, t, subst, ~gen: option) => Seq.t let reduceSubst: subst => subst let rewrite: (t, t, t, ~subst: subst, ~gen: option) => (subst, t) diff --git a/src/HOTermMethod.res b/src/HOTermMethod.res index 077feee..85b741b 100644 --- a/src/HOTermMethod.res +++ b/src/HOTermMethod.res @@ -12,7 +12,7 @@ module MakeRewriteHOTerm = ( module Rule = Rule.Make(HOTerm, Judgment) module Context = Context(HOTerm, Judgment) module Results = MethodResults(HOTerm) - + let extractEqualityTermsFromJudgment = (judgment: Judgment.t): option<(HOTerm.t, HOTerm.t)> => { let term: HOTerm.t = judgment switch HOTerm.strip(term) { @@ -202,7 +202,7 @@ module MakeRewriteHOTerm = ( } }) - ret->Dict.toArray->Array.map(((s,(a,b))) => Results.Action(s,a,b)) + ret->Dict.toArray->Array.map(((s, (a, b))) => Results.Action(s, a, b)) } let check = (it: t<'a>, ctx: Context.t, goal: Judgment.t, f: ('a, Rule.t) => 'b) => { @@ -337,7 +337,7 @@ module ConstructorNeq = (Judgment: JUDGMENT with module Term := HOTerm and type ret->Dict.set(`constructor_neq ${lhs} ${rhs}`, ((), HOTerm.makeSubst())) | _ => () } - ret->Dict.toArray->Array.map(((s,(a,b))) => Results.Action(s,a,b)) + ret->Dict.toArray->Array.map(((s, (a, b))) => Results.Action(s, a, b)) } let check = (_it: t<'a>, _ctx: Context.t, goal: Judgment.t, _f: ('a, Rule.t) => 'b) => @@ -446,7 +446,7 @@ module ConstructorInj = (Judgment: JUDGMENT with module Term := HOTerm and type }) | _ => () } - ret->Dict.toArray->Array.map(((s,(a,b))) => Results.Action(s,a,b)) + ret->Dict.toArray->Array.map(((s, (a, b))) => Results.Action(s, a, b)) } let check = (it: t<'a>, ctx: Context.t, goal: Judgment.t, _f: ('a, Rule.t) => 'b) => { diff --git a/src/ProofView.res b/src/ProofView.res index 1868765..b2cc130 100644 --- a/src/ProofView.res +++ b/src/ProofView.res @@ -17,66 +17,84 @@ module Make = ( module ResultsView = { type menuState<'a> = { history: list>>>, // Stack of previous menus - current: array>>, // What is currently visible + current: array>>, // What is currently visible } type props = { initialNodes: array>>, - onApply: (MethodView.Method.t, Term.subst) => (), - onBlur: (ReactEvent.Focus.t) => () + onApply: (MethodView.Method.t, Term.subst) => unit, + onBlur: ReactEvent.Focus.t => unit, } @react.componentWithProps let make = (props: props) => { - let (state, setState) = React.useState(_ => { - history: list{}, - current: props.initialNodes, + let (state, setState) = React.useState(_ => { + history: list{}, + current: props.initialNodes, + }) + + let goBack = _ => { + setState(prev => { + switch prev.history { + | list{parent, ...rest} => {current: parent, history: rest} + | list{} => prev // Already at the root + } + }) + } + + let drillDown = (newNodes: array>) => { + setState(prev => { + history: list{prev.current, ...prev.history}, + current: newNodes, }) - - let goBack = _ => { - setState(prev => { - switch prev.history { - | list{parent, ...rest} => {current: parent, history: rest} - | list{} => prev // Already at the root + } + +
+ {state.history != list{} + ? + : React.null} + +
+ {state.current + ->Array.mapWithIndex((node, i) => { + switch node { + | Action(label, nextTree, subst) => + + + | Group(label, children) => + + + | Delay(label, getChildren) => + } }) - } - - let drillDown = (newNodes: array>) => { - setState(prev => { - history: list{prev.current, ...prev.history}, - current: newNodes, - }) - } - -
- {state.history != list{} - ? - : React.null} - -
- {state.current->Array.mapWithIndex((node, i) => { - switch node { - | Action(label, nextTree, subst) => - - - | Group(label, children) => - - - | Delay(label, getChildren) => - - } - })->React.array} -
+ ->React.array}
- } +
} - - + } + type props = { proof: Proof.checked, scope: array, @@ -118,19 +136,19 @@ module Make = ( let portal = switch sidebarRef.current->Nullable.toOption { | None => React.null | Some(node) => - let res = options(props.gen); - Portal.createPortal( + let res = options(props.gen) + Portal.createPortal( <> - { - - props.onChange( - Proof.Checked({fixes, assumptions, method: Do(opt), rule}), - subst, - )} - > - } + { + props.onChange( + Proof.Checked({fixes, assumptions, method: Do(opt), rule}), + subst, + )} + > + } , node, ) diff --git a/src/SidebarContext.res b/src/SidebarContext.res index e8ffe9e..535cd29 100644 --- a/src/SidebarContext.res +++ b/src/SidebarContext.res @@ -9,4 +9,4 @@ let context = React.createContext({ let make = (~children, ~sidebarRef) => { let value = {sidebarRef: sidebarRef} React.createElement(React.Context.provider(context), {value, children}) -} \ No newline at end of file +} diff --git a/tests/HOTermTest.res b/tests/HOTermTest.res index e994ce8..fbd3529 100644 --- a/tests/HOTermTest.res +++ b/tests/HOTermTest.res @@ -3,12 +3,35 @@ open HOTerm module Util = TestUtil.MakeTerm(HOTerm) +module Symbol = AtomDef.MakeAtomAndView( + Symbolic.Atom, + Symbolic.AtomView, + AtomDef.NilAtomList, + AtomDef.NilAtomListView, +) +module StringSymbol = AtomDef.MakeAtomAndView( + StringA.Atom, + StringA.AtomView, + Symbol.Atom, + Symbol.AtomView, +) +module StringHOTerm = HOTerm.Make(StringSymbol.Atom) +module StringUtil = TestUtil.MakeTerm(StringHOTerm) +let wrapString = s => StringHOTerm.Symbol({ + name: AtomDef.AnyValue(StringA.BaseAtom.Tag, s), + constructor: false, +}) +let wrapSymbol = s => StringHOTerm.Symbol({ + name: AtomDef.AnyValue(Symbolic.BaseAtom.Tag, s), + constructor: false, +}) + let testUnify0 = (t: Zora.t, at: string, bt: string, ~subst=?, ~msg=?, ~reduce=false) => { let gen = HOTerm.makeGen() let (a, _) = HOTerm.parse(at, ~scope=[], ~gen)->Result.getExn let (b, _) = HOTerm.parse(bt, ~scope=[], ~gen)->Result.getExn try { - let res0 = HOTerm.unifyTerm(a, b, HOTerm.emptySubst, ~gen=Some(gen)) + let res0 = HOTerm.unifyTerm(a, b, HOTerm.emptySubst, ~gen=Some(gen))->Seq.head->Option.getExn let res = if reduce { HOTerm.reduceSubst(res0) } else { @@ -58,6 +81,7 @@ zoraBlock("parse symbol", t => { zoraBlock("parse var", t => { t->block("single digit", t => t->Util.testParse("\\1", Var({idx: 1}))) t->block("multi digit", t => t->Util.testParse("\\234", Var({idx: 234}))) + t->block("scope", t => t->Util.testParse("0", ~scope=["0"], Var({idx: 0}))) }) zoraBlock("parse schematic", t => { @@ -144,6 +168,53 @@ zoraBlock("parse and prettyprint", t => { }) }) +zoraBlock("string HOTerm functor", t => { + t->block("parse string atom", t => { + t->StringUtil.testParse(`"x y"`, wrapString([StringA.String("x"), StringA.String("y")])) + t->StringUtil.testParse(`"$s"`, ~scope=["s"], wrapString([StringA.Var({idx: 0})])) + t->StringUtil.testParsePrettyPrint(`"x y"`, `"x y"`) + }) + t->block("parse symbolic atom", t => { + t->StringUtil.testParse("x", wrapSymbol("x")) + t->StringUtil.testParse( + "@cons", + StringHOTerm.Symbol({ + name: AtomDef.AnyValue(Symbolic.BaseAtom.Tag, "cons"), + constructor: true, + }), + ) + t->StringUtil.testParse( + "(x. x)", + StringHOTerm.Lam({name: "x", body: StringHOTerm.Var({idx: 0})}), + ) + }) + t->block("unify string atom", t => { + let parse = input => t->StringUtil.parse(input) + let emptySubst = StringHOTerm.emptySubst + let substAdd = StringHOTerm.substAdd + t->equal( + StringHOTerm.unify(parse(`"a ?0() c"`), parse(`"a b c"`))->Seq.head, + Some(emptySubst->substAdd(0, wrapString([StringA.String("b")]))), + ) + t->equal( + StringHOTerm.unify(parse(`(P "?1() a" "?1()")`), parse(`(P "a ?1()" "a")`))->Seq.head, + Some(emptySubst->substAdd(1, wrapString([StringA.String("a")]))), + ) + let choices = + StringHOTerm.unify(parse(`"?1() a"`), parse(`"a ?1()"`)) + ->Seq.take(2) + ->Seq.toArray + t->equal( + choices, + [ + emptySubst->substAdd(1, wrapString([])), + emptySubst->substAdd(1, wrapString([StringA.String("a")])), + ], + ) + t->equal(StringHOTerm.unify(parse(`"a"`), parse(`"b"`))->Seq.head, None) + }) +}) + zoraBlock("unify test", t => { let testUnifyFail = Util.testUnifyFailString t->block("symbols", t => { diff --git a/tests/RuleTest.res b/tests/RuleTest.res index 5fb39f6..8ecf8e1 100644 --- a/tests/RuleTest.res +++ b/tests/RuleTest.res @@ -31,19 +31,20 @@ module MakeTest = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => { } } +module Symbol = AtomDef.MakeAtomAndView( + Symbolic.Atom, + Symbolic.AtomView, + AtomDef.NilAtomList, + AtomDef.NilAtomListView, +) +module StringSymbol = AtomDef.MakeAtomAndView( + StringA.Atom, + StringA.AtomView, + Symbol.Atom, + Symbol.AtomView, +) + zoraBlock("string terms", t => { - module Symbol = AtomDef.MakeAtomAndView( - Symbolic.Atom, - Symbolic.AtomView, - AtomDef.NilAtomList, - AtomDef.NilAtomListView, - ) - module StringSymbol = AtomDef.MakeAtomAndView( - StringA.Atom, - StringA.AtomView, - Symbol.Atom, - Symbol.AtomView, - ) module StringSExp = SExp.Make(StringSymbol.Atom) let wrapString = (s): StringSExp.t => Atom(AtomDef.AnyValue(StringA.BaseAtom.Tag, s)) let wrapSymbol = (s): StringSExp.t => Atom(AnyValue(Symbolic.BaseAtom.Tag, s)) @@ -70,3 +71,34 @@ zoraBlock("string terms", t => { }, ) }) + +zoraBlock("string HOTerms", t => { + module StringHOTerm = HOTerm.Make(StringSymbol.Atom) + let wrapString = (s): StringHOTerm.t => Symbol({ + name: AtomDef.AnyValue(StringA.BaseAtom.Tag, s), + constructor: false, + }) + let wrapSymbol = (s): StringHOTerm.t => Symbol({ + name: AtomDef.AnyValue(Symbolic.BaseAtom.Tag, s), + constructor: false, + }) + let app = StringHOTerm.app + module T = MakeTest(StringHOTerm, StringHOTerm) + t->T.testParseInner( + `[s1. ("$s1" p) |- ("($s1)" p)]`, + { + vars: ["s1"], + premises: [ + { + vars: [], + premises: [], + conclusion: app(wrapString([StringA.Var({idx: 0})]), [wrapSymbol("p")]), + }, + ], + conclusion: app( + wrapString([StringA.String("("), StringA.Var({idx: 0}), StringA.String(")")]), + [wrapSymbol("p")], + ), + }, + ) +}) -- 2.51.2