From c5d096bdda8426a7b2dbe97cff4f6d4eaca578cb Mon Sep 17 00:00:00 2001 From: Liam O'Connor Date: Fri, 28 Aug 2026 18:34:16 +1000 Subject: [PATCH] =?UTF-8?q?fixing=20bugs.=20added=20=E2=80=9Csimple=20ho?= =?UTF-8?q?=20terms=E2=80=9D=20because=20I=20can=E2=80=99t=20debug=20HOTer?= =?UTF-8?q?m.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- build.sh | 1 + src/HOTermView.res | 56 ++-- src/Method.res | 6 +- src/SHOTerm.res | 624 ++++++++++++++++++++++++++++++++++++++++++ src/SHOTerm.resi | 15 + src/SHOTermView.res | 95 +++++++ src/SHOTermView.resi | 1 + src/Scratch.res | 50 +--- src/componentgraph.ts | 21 +- src/testcomponent.tsx | 2 + tests/SHOTermTest.res | 14 + 11 files changed, 817 insertions(+), 68 deletions(-) create mode 100755 build.sh create mode 100644 src/SHOTerm.res create mode 100644 src/SHOTerm.resi create mode 100644 src/SHOTermView.res create mode 100644 src/SHOTermView.resi create mode 100644 tests/SHOTermTest.res diff --git a/build.sh b/build.sh new file mode 100755 index 0000000..d83f4cb --- /dev/null +++ b/build.sh @@ -0,0 +1 @@ +npm run res:build && npm run build && cp dist/assets/index-*.js forest/theme/index-bsTLl1gN.js && cd forest && forester build && cd .. diff --git a/src/HOTermView.res b/src/HOTermView.res index 056148f..a1913da 100644 --- a/src/HOTermView.res +++ b/src/HOTermView.res @@ -4,16 +4,29 @@ module Make = ( AtomView: AtomDef.ATOM_VIEW with module Atom := Atom, HOTerm: HOTerm.S with module Atom := Atom, ) => { - type idx_props = {idx: int, scope: array} + type idx_props = {idx: int, scope: array, local_scope: array} let viewVar = (props: idx_props) => - switch props.scope[props.idx] { - | Some(n) if Array.indexOf(props.scope, n) == props.idx => - {React.string(n)} - | _ => - - {React.string("\\")} - {React.int(props.idx)} - + if props.idx < Array.length(props.local_scope) { + switch props.local_scope[props.idx] { + | Some(n) if Array.indexOf(props.local_scope, n) == props.idx => + {React.string(n)} + | _ => + + {React.string("\\")} + {React.int(props.idx)} + + } + } else { + let idx2 = props.idx - Array.length(props.local_scope) + switch props.scope[idx2] { + | Some(n) if Array.indexOf(props.scope, n) == idx2 => + {React.string(n)} + | _ => + + {React.string("\\")} + {React.int(props.idx)} + + } } let makeMeta = (str: string) => @@ -21,6 +34,11 @@ module Make = ( {React.string(str)} {React.string(".")} + let makeLocalBinder = (str: string) => + + {React.string(str)} + {React.string(".")} + let parenthesise = f => [ @@ -37,11 +55,11 @@ module Make = ( [React.string(" "), e] } ) - type props1 = {term: HOTerm.t, scope: array, brackets: bool} + type props1 = {term: HOTerm.t, scope: array, local_scope: array, brackets: bool} @react.componentWithProps - let rec make1 = ({term, scope, brackets}) => + let rec make1 = ({term, scope, local_scope,brackets}) => switch term { - | Var({idx}) => viewVar({idx, scope}) + | Var({idx}) => viewVar({idx, scope, local_scope}) | Symbol({name: s}) => {AtomView.make({atom: s, scope})} | Schematic({schematic: s}) => @@ -52,9 +70,9 @@ module Make = ( switch HOTerm.strip(term) { | (Symbol({name: s}), args) if HOTerm.isEqualityAtom(s) && Array.length(args) == 2 => - {React.createElement(make1, {term: args->Array.getUnsafe(0), scope, brackets: true})} + {React.createElement(make1, {term: args->Array.getUnsafe(0), scope, local_scope, brackets: true})} {React.string("=")} - {React.createElement(make1, {term: args->Array.getUnsafe(1), scope, brackets: true})} + {React.createElement(make1, {term: args->Array.getUnsafe(1), scope, local_scope, brackets: true})} | (func, args) => let xs = Array.concat([func], args) @@ -62,7 +80,7 @@ module Make = ( {xs ->Array.mapWithIndex((t, i) => - React.createElement(make1, withKey({term: t, scope, brackets: true}, i)) + React.createElement(make1, withKey({term: t, scope, local_scope, brackets: true}, i)) ) ->intersperse ->React.array} @@ -74,15 +92,15 @@ module Make = ( } } | Lam({name, body}) => { - let newScope = Array.concat([name], scope) + let new_scope = Array.concat([name], local_scope) - {React.string(name)} - {React.createElement(make1, {term: body, scope: newScope, brackets: false})} + {[makeLocalBinder(name), + React.createElement(make1, {term: body, scope, local_scope: new_scope, brackets: false})]->parenthesise->React.array} } | Unallowed =>

{React.string("Internal error: unallowed")}

} type props = {term: HOTerm.t, scope: array} @react.componentWithProps - let make = ({term, scope}) => make1({term, scope, brackets: false}) + let make = ({term, scope}) => make1({term, scope, local_scope: [], brackets: false}) } diff --git a/src/Method.res b/src/Method.res index 2ffac6f..42d7da4 100644 --- a/src/Method.res +++ b/src/Method.res @@ -213,7 +213,7 @@ module Derivation = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => | None => Error("Cannot find rule '"->String.concat(it.ruleName)->String.concat("'")) | Some(rule) if Array.length(rule.vars) == Array.length(it.instantiation) => { let {premises, conclusion} = Rule.instantiate(rule, it.instantiation) - if Judgment.equivalent(conclusion, j) { + if Judgment.equivalent(Judgment.reduce(conclusion), Judgment.reduce(j)) { if Array.length(it.subgoals) == Array.length(premises) { Ok({ ruleName: it.ruleName, @@ -368,9 +368,9 @@ module Elimination = (Term: TERM, Judgment: JUDGMENT with module Term := Term) = Error(`Premise to eliminate in rule ${it.ruleName} has non-empty premises`) } else if elim.premises->Array.length > 0 { Error(`Elimination motive (?) ${it.elimName} has non-empty premises`) - } else if !Judgment.equivalent(elimPremise.conclusion, elim.conclusion) { + } else if !Judgment.equivalent(Judgment.reduce(elimPremise.conclusion), Judgment.reduce(elim.conclusion)) { Error(`Premise to eliminate and elimination motive (?) ${it.elimName} do not match`) - } else if !Judgment.equivalent(conclusion, j) { + } else if !Judgment.equivalent(Judgment.reduce(conclusion), Judgment.reduce(j)) { let concString = Judgment.prettyPrint(conclusion, ~scope=ctx.fixes) let goalString = Judgment.prettyPrint(j, ~scope=ctx.fixes) Error(`Conclusion of rule '${concString}' doesn't match goal '${goalString}'`) diff --git a/src/SHOTerm.res b/src/SHOTerm.res new file mode 100644 index 0000000..d8a3203 --- /dev/null +++ b/src/SHOTerm.res @@ -0,0 +1,624 @@ +/** + * Simple pattern-unification term module. + * + * Representation notes: + * - `meta` and bound-variable de Bruijn indices are literally the same + * thing: `int`. `scope: array` given to `place` is a spine of + * distinct bound-variable indices. + * - `schematic` is just an `int` id for a metavariable. + * - `subst` maps schematic id -> a *closed* solution term. If schematic + * `n` was created via `place(n, ~scope)` = `n x_s0 ... x_s(k-1)`, its + * solution is stored as `Lam(...Lam(body))` with k lambdas, i.e. the + * thing you'd apply to x_s0..x_s(k-1) to get the value back. This + * means `substitute` just swaps in the closed term, and application + * spines redex away via `reduce`. + * - Only genuine *pattern* unification is attempted: a metavariable is + * only ever solved when it's applied to a spine of *distinct* bound + * variables. Anything else (a metavariable applied to a non-variable, + * or to a repeated variable) is treated as rigid and unification + * fails rather than attempting Huet-style pruning/backtracking. + * Because of that, `unify` never needs genuine choice points, so the + * returned `Seq.t` always has 0 or 1 elements. + * - `gen` is only needed for the flex-flex "same schematic, different + * spines" case (`M x y =?= M y x`), where a smaller fresh + * metavariable has to be invented for the positions that agree. + * Without a `~gen`, that specific case just fails. + */ + + +type rec t = + | Symbol({name: string, constructor: bool}) + | Var({idx: int}) + | Schematic({schematic: int}) + | Lam({name: string, body: t}) + | App({func: t, arg: t}) + +type schematic = int +type meta = string +type subst = Belt.Map.Int.t + +// Fresh-name counter. `seen` bumps it above any externally-encountered +// schematic id so freshly generated ones never collide with them. +type gen = {mutable next: int} + +let makeGen = () => {next: 0} + +let fresh = (g, ~replacing as _=?) => { + // `replacing` is accepted for callers that want to record *why* a + // schematic was generated (e.g. during pruning), but the generator + // itself doesn't need it: freshness is just "next global int". + let s = g.next + g.next = g.next + 1 + s +} + +let seen = (g, s) => + if s >= g.next { + g.next = s + 1 + } + +let place = (schematic, ~scope) => { + let n = Belt.Array.length(scope) + Belt.Array.reduceWithIndex(scope, Schematic({schematic: schematic}), (acc, _name, i) => App({ + func: acc, + arg: Var({idx: n - 1 - i}), + })) +} + +// ---------- de Bruijn machinery ---------- + +let rec upshift = (term, n, ~from=0) => + switch term { + | Symbol(_) | Schematic(_) => term + | Var({idx}) => idx >= from ? Var({idx: idx + n}) : term + | Lam({name, body}) => Lam({name, body: upshift(body, n, ~from=from + 1)}) + | App({func, arg}) => App({func: upshift(func, n, ~from), arg: upshift(arg, n, ~from)}) + } + +// Simultaneous substitution: replaces Var(from), Var(from+1), ..., +// Var(from+len-1) with values[0..len-1] (each correctly shifted for +// the depth at which it's inserted), and downshifts any free +// variable above that range by len. With from=0 and a single value +// this is ordinary single-variable substitution/beta-reduction. +let substDeBruijn = (term, values, ~from=0) => { + let len = Belt.Array.length(values) + let rec go = (term, depth) => + switch term { + | Symbol(_) | Schematic(_) => term + | Var({idx}) => + if idx < from + depth { + term + } else if idx < from + depth + len { + upshift(Belt.Array.getExn(values, idx - from - depth), depth, ~from=0) + } else { + Var({idx: idx - len}) + } + | Lam({name, body}) => Lam({name, body: go(body, depth + 1)}) + | App({func, arg}) => App({func: go(func, depth), arg: go(arg, depth)}) + } + go(term, 0) +} + +let rec reduce = term => + switch term { + | Symbol(_) | Var(_) | Schematic(_) => term + | Lam({name, body}) => Lam({name, body: reduce(body)}) + | App({func, arg}) => + let func' = reduce(func) + let arg' = reduce(arg) + switch func' { + | Lam({body}) => reduce(substDeBruijn(body, [arg'], ~from=0)) + | _ => App({func: func', arg: arg'}) + } + } + +let rec concrete = term => true /* term => + switch term { + | Symbol(_) | Var(_) => true + | Schematic(_) => false + | Lam({body}) => concrete(body) + | App({func, arg}) => concrete(func) && concrete(arg) + }*/ + + +let rec structEqual = (a, b) => + switch (a, b) { + | (Symbol({name: n1, constructor: c1}), Symbol({name: n2, constructor: c2})) => + n1 == n2 && c1 == c2 + | (Var({idx: i1}), Var({idx: i2})) => i1 == i2 + | (Schematic({schematic: s1}), Schematic({schematic: s2})) => s1 == s2 + | (Lam({body: b1}), Lam({body: b2})) => structEqual(b1, b2) + | (App({func: f1, arg: a1}), App({func: f2, arg: a2})) => + structEqual(f1, f2) && structEqual(a1, a2) + | _ => false + } + +// alpha-equivalence is free (de Bruijn); this is beta-normal-form +// structural equality. Lam's `name` field is just a display hint and +// is ignored, as it should be. +let equivalent = (a, b) => structEqual(reduce(a), reduce(b)) + +// ---------- substitutions ---------- + +let makeSubst = () => Belt.Map.Int.empty + +let rec substitute = (term, s) => + switch term { + | Symbol(_) | Var(_) => term + | Schematic({schematic}) => + switch Belt.Map.Int.get(s, schematic) { + // recurse so a subst that itself contains chained schematic + // solutions resolves in one call; assumes s is acyclic (an + // occurs-check-respecting subst always is). + | Some(t) => substitute(t, s) + | None => term + } + | Lam({name, body}) => Lam({name, body: substitute(body, s)}) + | App({func, arg}) => App({func: substitute(func, s), arg: substitute(arg, s)}) + } + +let mapSubst = (s, f) => Belt.Map.Int.map(s, f) + +// Composition: s2 "after" s1 — push s2 into s1's range, then union +// in s2's own bindings. Assumes domains don't genuinely conflict +// (true for substitutions produced while unifying independent +// subterms of the same problem). +let mergeSubsts = (s1, s2) => { + let s1' = mapSubst(s1, t => substitute(t, s2)) + Belt.Map.Int.merge(s1', s2, (_, a, b) => + switch (a, b) { + | (Some(t), _) => Some(t) + | (None, Some(t)) => Some(t) + | (None, None) => None + } + ) +} + +let substEqual = (s1, s2) => + Belt.Map.Int.size(s1) == Belt.Map.Int.size(s2) && + Belt.Map.Int.every(s1, (k, v) => + switch Belt.Map.Int.get(s2, k) { + | Some(v2) => equivalent(v, v2) + | None => false + } + ) + +// ---------- unification ---------- + +// Application spine: head plus args in application order. +let rec spineList = t => + switch t { + | App({func, arg}) => + let (h, args) = spineList(func) + (h, Belt.List.concat(args, list{arg})) + | _ => (t, list{}) + } + +// Is `t` of the form `Schematic(n)[x_i0, ..., x_i(k-1)]` with the +// x_ij *distinct* bound variables? If so, (n, [i0..i(k-1)]). +let asPattern = t => { + let (head, args) = spineList(t) + switch head { + | Schematic({schematic}) => + let idxs = Belt.List.map(args, a => + switch a { + | Var({idx}) => Some(idx) + | _ => None + } + ) + if Belt.List.every(idxs, Belt.Option.isSome) { + let idxArr = idxs->Belt.List.map(Belt.Option.getExn)->Belt.List.toArray + let distinct = Belt.Set.Int.fromArray(idxArr) + Belt.Set.Int.size(distinct) == Belt.Array.length(idxArr) + ? Some((schematic, idxArr)) + : None + } else { + None + } + | _ => None + } +} + +let rec occurs = (n, t) => + switch t { + | Symbol(_) | Var(_) => false + | Schematic({schematic}) => schematic == n + | Lam({body}) => occurs(n, body) + | App({func, arg}) => occurs(n, func) || occurs(n, arg) + } + +let freeVars = t => { + let acc = ref(Belt.Set.Int.empty) + let rec go = (t, depth) => + switch t { + | Symbol(_) | Schematic(_) => () + | Var({idx}) => + if idx >= depth { + acc := Belt.Set.Int.add(acc.contents, idx - depth) + } + | Lam({body}) => go(body, depth + 1) + | App({func, arg}) => { + go(func, depth) + go(arg, depth) + } + } + go(t, 0) + acc.contents +} + +// Build the closed solution `λ x0' .. x(k-1)'. body` for +// `Schematic(n)[spine] := rhs`, given rhs's free vars ⊆ spine. +// spine[j] (an ambient bound-var index) becomes the (k-1-j)-th +// innermost bound variable of the solution, matching how `place` +// applies args left-to-right (outermost lambda binds the first arg). +let makeSolution = (rhs, spineArr) => { + let k = Belt.Array.length(spineArr) + let maxIdx = Belt.Array.reduce(spineArr, -1, (m, i) => max(m, i)) + let values = Belt.Array.makeBy(maxIdx + 1, p => + switch Belt.Array.getIndexBy(spineArr, x => x == p) { + | Some(j) => Var({idx: k - 1 - j}) + | None => Symbol({name: "_unused", constructor: false}) // never read, by the scope check + } + ) + let body = substDeBruijn(rhs, values, ~from=0) + let rec wrapLams = (m, b) => m <= 0 ? b : wrapLams(m - 1, Lam({name: "x", body: b})) + wrapLams(k, body) +} + +// Try to solve `a` (assumed reduced) as a pattern for `b` (also +// reduced). Occurs check + scope check (b's free vars ⊆ a's spine). +let tryFlexSolve = (a, b) => + switch asPattern(a) { + | Some((n, spineArr)) => + if occurs(n, b) { + None + } else { + let spineSet = Belt.Set.Int.fromArray(spineArr) + if Belt.Set.Int.subset(freeVars(b), spineSet) { + Some(Belt.Map.Int.fromArray([(n, makeSolution(b, spineArr))])) + } else { + None + } + } + | None => None + } + +// M[spine1] =?= M[spine2], same M, spines differ: keep only the +// positions where they agree, solve M in terms of a smaller fresh +// metavariable applied to just those positions. +let tryFlexFlexSame = (n, spine1, spine2, gen) => + switch gen { + | None => None + | Some(g) => + let k = Belt.Array.length(spine1) + if k != Belt.Array.length(spine2) { + None + } else { + let agree = + Belt.Array.range(0, k - 1)->Belt.Array.keep(i => + Belt.Array.getExn(spine1, i) == Belt.Array.getExn(spine2, i) + ) + let n' = fresh(g) + let body = Belt.Array.reduce(agree, Schematic({schematic: n'}), (acc, i) => App({ + func: acc, + arg: Var({idx: k - 1 - i}), + })) + let rec wrapLams = (m, b) => m <= 0 ? b : wrapLams(m - 1, Lam({name: "x", body: b})) + Some(Belt.Map.Int.fromArray([(n, wrapLams(k, body))])) + } + } + + +let unifyRigidHeaded = (t1, t2, gen, unifyStep) => { + let (h1, args1) = spineList(t1) + let (h2, args2) = spineList(t2) + let headsMatch = switch (h1, h2) { + | (Symbol({name: n1, constructor: c1}), Symbol({name: n2, constructor: c2})) => + n1 == n2 && c1 == c2 + | (Var({idx: i1}), Var({idx: i2})) => i1 == i2 + | _ => false + } + let a1 = Belt.List.toArray(args1) + let a2 = Belt.List.toArray(args2) + if headsMatch && Belt.Array.length(a1) == Belt.Array.length(a2) { + let n = Belt.Array.length(a1) + let rec loop = (i, acc) => + if i >= n { + Some(acc) + } else { + switch unifyStep( + substitute(Belt.Array.getExn(a1, i), acc), + substitute(Belt.Array.getExn(a2, i), acc), + gen, + ) { + | None => None + | Some(s) => loop(i + 1, mergeSubsts(acc, s)) + } + } + loop(0, makeSubst()) + } else { + None + } +} + +let rec unifyStep = (t1, t2, gen) => { + let t1 = reduce(t1) + let t2 = reduce(t2) + if structEqual(t1, t2) { + Some(makeSubst()) + } else { + switch (t1, t2) { + | (Lam({body: b1}), Lam({body: b2})) => unifyStep(b1, b2, gen) + // eta: unify λ.b1 against t2 by comparing b1 to (t2 shifted) applied to a fresh bound var + | (Lam({body: b1}), _) => unifyStep(b1, App({func: upshift(t2, 1), arg: Var({idx: 0})}), gen) + | (_, Lam({body: b2})) => unifyStep(App({func: upshift(t1, 1), arg: Var({idx: 0})}), b2, gen) + | _ => + switch (asPattern(t1), asPattern(t2)) { + | (Some((n1, s1)), Some((n2, s2))) if n1 == n2 => tryFlexFlexSame(n1, s1, s2, gen) + | _ => + switch tryFlexSolve(t1, t2) { + | Some(s) => Some(s) + | None => + switch tryFlexSolve(t2, t1) { + | Some(s) => Some(s) + | None => unifyRigidHeaded(t1, t2, gen, unifyStep) + } + } + } + } + } +} + +let unify = (t1, t2, ~gen=?) => + switch unifyStep(t1, t2, gen) { + | Some(s) => Seq.cons(s, Seq.empty) + | None => Seq.empty + } + +let prettyPrintVar = (idx: int, scope: array) => + switch scope[idx] { + | Some(n) if Array.indexOf(scope, n) == idx => n + | _ => "\\"->String.concat(String.make(idx)) + } +let rec strip = (term: t): (t, array) => { + switch term { + | App({func, arg}) => + let (peeledFunc, peeledArgs) = strip(func) + (peeledFunc, Array.concat(peeledArgs, [arg])) + | _ => (term, []) + } +} +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(")") + } +let prettyPrintMeta = (str: string) => { + String.concat(str, ".") + } +let prettyPrintSubst = (sub: subst, ~scope: array) => + Util.prettyPrintIntMap(sub, ~showV=t => prettyPrint(t, ~scope)) + + + + +let nameRES = "^([^\\s.\\[\\]()]+)\\." +let symbolRES = "^([^\\s.\\[\\]()]+)" +exception ParseError(string) +type token = + | LParen + | RParen + | VarT(int) + | SchematicT(int) + | ConsT(string) + | NameT(string) + | AtomT(string) + | EOF +let varRegexpString = "^\\\\([0-9]+)" +let schematicRegexpString = "^\\?([0-9]+)" + +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))) + } + }) + 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(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")) + } + } + } + | _ => { + let reName = RegExp.fromStringWithFlags(symbolRES, ~flags="y") + switch scopeVarToken(str, scope) { + | Some((idx, rest)) => (VarT(idx), rest) + | None => switch reName->RegExp.exec(str) { + | Some(res) => { + let rest = String.sliceToEnd(str, ~start=RegExp.lastIndex(reName)) + switch RegExp.Result.matches(res) { + | [n] => if n->String.charAt(0)=="@" { + (ConsT(n), rest) + } else if rest->String.charAt(0)=="." { + (NameT(n), rest->String.sliceToEnd(~start=1)) + } else { + (AtomT(n), rest) + } + + | _ => throw(ParseError("invalid symbol")) + } + } + | None => throw(ParseError("unrecognised input")) + } + } + } + } + } +} +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, ~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")) + } +} +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}) => 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")) + } + | LambdaS({name, body}) => + Lam({ + name, + body: parseAll(body, ~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 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 mapTerms = (t, f) => f(t) \ No newline at end of file diff --git a/src/SHOTerm.resi b/src/SHOTerm.resi new file mode 100644 index 0000000..c2d6d25 --- /dev/null +++ b/src/SHOTerm.resi @@ -0,0 +1,15 @@ +type rec t = + | Symbol({name: string, constructor: bool}) + | Var({idx: int}) + | Schematic({schematic: int}) + | Lam({name: string, body: t}) + | App({func: t, arg: t}) + +include Signatures.TERM + with type t := t + and type meta = string + and type schematic = int + and type subst = Belt.Map.Int.t + +let mapTerms: (t, t => t) => t +let strip: t => (t, array) \ No newline at end of file diff --git a/src/SHOTermView.res b/src/SHOTermView.res new file mode 100644 index 0000000..0302fad --- /dev/null +++ b/src/SHOTermView.res @@ -0,0 +1,95 @@ +open Util + +type idx_props = {idx: int, scope: array, local_scope: array} +let viewVar = (props: idx_props) => + if props.idx < Array.length(props.local_scope) { + switch props.local_scope[props.idx] { + | Some(n) if Array.indexOf(props.local_scope, n) == props.idx => + {React.string(n)} + | _ => + + {React.string("\\")} + {React.int(props.idx)} + + } + } else { + let idx2 = props.idx - Array.length(props.local_scope) + switch props.scope[idx2] { + | Some(n) if Array.indexOf(props.scope, n) == idx2 => + {React.string(n)} + | _ => + + {React.string("\\")} + {React.int(props.idx)} + + } + } + +let makeMeta = (str: string) => + + {React.string(str)} + {React.string(".")} + +let makeLocalBinder = (str: string) => + + {React.string(str)} + {React.string(".")} + + +let parenthesise = f => + [ + {React.string("(")} , + ...f, + {React.string(")")} , + ] + +let intersperse = a => + a->Array.flatMapWithIndex((e, i) => + if i == 0 { + [e] + } else { + [React.string(" "), e] + } + ) +type props1 = {term: SHOTerm.t, scope: array, local_scope: array, brackets: bool} +@react.componentWithProps +let rec make1 = ({term, scope, local_scope,brackets}) => + switch term { + | Var({idx}) => viewVar({idx, scope, local_scope}) + | Symbol({name: s}) => {React.string(s)} + | Schematic({schematic: s}) => + + {React.string("?")} + {React.int(s)} + + | App(_) => + switch SHOTerm.strip(term) { + | (func, args) => + let xs = Array.concat([func], args) + let a = + + {xs + ->Array.mapWithIndex((t, i) => + React.createElement(make1, withKey({term: t, scope, local_scope, brackets: true}, i)) + ) + ->intersperse + ->React.array} + + if brackets { + [a]->parenthesise->React.array + } else { + a + } + } + | Lam({name, body}) => { + let new_scope = Array.concat([name], local_scope) + + {[makeLocalBinder(name), + React.createElement(make1, {term: body, scope, local_scope: new_scope, brackets: false})]->parenthesise->React.array} + + } + } +type props = {term: SHOTerm.t, scope: array} +@react.componentWithProps +let make = ({term, scope}) => make1({term, scope, local_scope: [], brackets: false}) + diff --git a/src/SHOTermView.resi b/src/SHOTermView.resi new file mode 100644 index 0000000..e86852b --- /dev/null +++ b/src/SHOTermView.resi @@ -0,0 +1 @@ + include Signatures.TERM_VIEW with module Term := SHOTerm \ No newline at end of file diff --git a/src/Scratch.res b/src/Scratch.res index ff638a1..b1d1203 100644 --- a/src/Scratch.res +++ b/src/Scratch.res @@ -26,50 +26,24 @@ module Final = AtomDef.MakeAtomChoiceAndView( module HOTerm = HOTerm.Make(StringSymbol.Atom) module HOTermView = HOTermView.Make(StringSymbol.Atom, StringSymbol.AtomView, HOTerm) -module HOTermJView = TermViewAsJudgmentView.Make(HOTerm, HOTerm, HOTermView) -module AxiomS = Editable.TextArea(AxiomSet.Make(HOTerm, HOTerm, HOTermJView)) -module InductiveS = Editable.TextArea(InductiveSet.Make(HOTerm, HOTerm, HOTermJView)) - -module EqualityViews = MethodView.CombineMethodView( - HOTerm, - HOTerm, - MethodView.RewriteView(HOTerm, HOTerm), - MethodView.RewriteReverseView(HOTerm, HOTerm), -) -module ConstructorEqualityViews = MethodView.CombineMethodView( - HOTerm, - HOTerm, - EqualityViews, - MethodView.ConstructorNeqView(HOTerm, HOTerm), -) -module RewritesView = MethodView.CombineMethodView( - HOTerm, - HOTerm, - ConstructorEqualityViews, - MethodView.ConstructorInjView(HOTerm, HOTerm), -) +module SHOTermJView = TermViewAsJudgmentView.Make(SHOTerm, SHOTerm, SHOTermView) +module AxiomS = Editable.TextArea(AxiomSet.Make(SHOTerm, SHOTerm, SHOTermJView)) +module InductiveS = Editable.TextArea(AxiomSet.Make(SHOTerm, SHOTerm, SHOTermJView)) module DerivationsOrLemmasView = MethodView.CombineMethodView( - HOTerm, - HOTerm, + SHOTerm, + SHOTerm, MethodView.CombineMethodView( - HOTerm, - HOTerm, - MethodView.DerivationView(HOTerm, HOTerm), - MethodView.LemmaView(HOTerm, HOTerm, HOTermJView), + SHOTerm, + SHOTerm, + MethodView.DerivationView(SHOTerm, SHOTerm), + MethodView.LemmaView(SHOTerm, SHOTerm, SHOTermJView), ), - MethodView.EliminationView(HOTerm, HOTerm), -) -module DLRView = MethodView.CombineMethodView(HOTerm, HOTerm, DerivationsOrLemmasView, RewritesView) -module DLREView = MethodView.CombineMethodView( - HOTerm, - HOTerm, - DLRView, - MethodView.EliminationView(HOTerm, HOTerm), + MethodView.EliminationView(SHOTerm, SHOTerm), ) // Temporarily use DLRView (without Elimination) due to HOTerm unification bug -module TheoremS = Editable.TextArea(Theorem.Make(HOTerm, HOTerm, HOTermJView, DLRView)) -module ConfS = ConfigBlock.Make(HOTerm, HOTerm) +module TheoremS = Editable.TextArea(Theorem.Make(SHOTerm, SHOTerm, SHOTermJView, DerivationsOrLemmasView)) +module ConfS = ConfigBlock.Make(SHOTerm, SHOTerm) module StringSExp = SExp.Make(Final.Atom) module TermView = SExpView.Make(Final.Atom, Final.AtomView, StringSExp) diff --git a/src/componentgraph.ts b/src/componentgraph.ts index 031fa27..a9a9b80 100644 --- a/src/componentgraph.ts +++ b/src/componentgraph.ts @@ -113,15 +113,20 @@ class Handler { } - let setupComponent = (text : string, deps: Record) => { + let setupComponent = (text : string, deps: Record, notifyReady: boolean) => { + console.log("Setting up ", text, deps) this.component = new maker(text, deps, (msg) => { this.notifySubscribers(msg) }, (msg) => { this.status = "ready"; - for (let sub of this.subscribers) { - sub.dependencyReady(this.url); - } + if (notifyReady) { + queueMicrotask(() => { + for (let sub of this.subscribers) { + sub.dependencyReady(this.url); + } + }) + } }, (msg) => { - setupComponent(original_str, deps); + setupComponent(original_str, deps, false); this.notifySubscribers(msg); }, view); } @@ -134,7 +139,7 @@ class Handler { }) } if (awaiting.length == 0) { - setupComponent(textual, {}) + setupComponent(textual, {}, true) } } this.dependencyReady = function(url) { @@ -151,7 +156,7 @@ class Handler { deps2[dep] = v; } } - setupComponent(textual, deps2); + setupComponent(textual, deps2, true); } } } @@ -181,7 +186,7 @@ export function setup( .trim() .split(/\s+/) .filter(Boolean); - console.log(deps); + deps = [...new Set(deps)]; let original_str = this.innerHTML; let text = window.localStorage.getItem(id) ?? this.innerHTML; this.innerHTML = "loading"; diff --git a/src/testcomponent.tsx b/src/testcomponent.tsx index 211bf37..0029515 100644 --- a/src/testcomponent.tsx +++ b/src/testcomponent.tsx @@ -33,6 +33,7 @@ function HolComp(RComp : any) { this.root.render( { + console.log("Reset invoked on " + this.original_str) reset(0) }} onChange={ (state, exports) => { @@ -48,6 +49,7 @@ function HolComp(RComp : any) { } constructor(str: string, deps : Record, signal : (msg: any) => void, loaded : (msg: any) => void, reset : (msg : any) => void, view? : HTMLElement) { this.deps = deps + this.original_str = str; this.loaded = false if (view != null) { const newDiv = document.createElement("div"); diff --git a/tests/SHOTermTest.res b/tests/SHOTermTest.res new file mode 100644 index 0000000..756bdbd --- /dev/null +++ b/tests/SHOTermTest.res @@ -0,0 +1,14 @@ +open Zora + +module Util = TestUtil.MakeTerm(SHOTerm) + + +let parse = (input: string) => + SHOTerm.parse(input, ~scope=[], ~gen=SHOTerm.makeGen())->Result.getExn->Pair.first + +zoraBlock("unification", t => { + let x = parse("(Implies A B)") + let y = parse("(Implies ?0 ?1)") + t->Util.testUnify(x, y, ~expect=[Belt.Map.Int.fromArray([(0, parse("A")), (1, parse("B"))])]) + +}) -- 2.51.2