From 47fc76250eb5309e76068ebf5a5d4083827a1963 Mon Sep 17 00:00:00 2001 From: Mio Date: Thu, 13 Nov 2025 14:17:45 +1100 Subject: [PATCH 1/8] add a test case --- tests/HOTermTest.res | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/tests/HOTermTest.res b/tests/HOTermTest.res index e665e94..41ea86d 100644 --- a/tests/HOTermTest.res +++ b/tests/HOTermTest.res @@ -279,6 +279,11 @@ zoraBlock("unify test", t => { let b = "\\0" t->testUnify(a, b, ~subst=emptySubst->substAdd(0, t->Util.parse("(x. x. \\0)"))) }) + t->block("dup var 2", t => { + let a = "(k. ?0 k k)" + let b = "(k. G k)" + t->testUnify(a, b, ~subst=emptySubst->substAdd(0, t->Util.parse("(x. x. G x)"))) + }) // Yokoyama et al.'s example in A Functional Implementation of Function-as-Constructor Higher-Order Unification Makoto Hamana1 t->block("break global resctriction", t => { t->testUnify( From fa85874068909ead378a57adf9561394c742d4d4 Mon Sep 17 00:00:00 2001 From: Mio Date: Sun, 16 Nov 2025 19:34:45 +1100 Subject: [PATCH 2/8] fix cases generation --- src/InductiveSet.res | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/InductiveSet.res b/src/InductiveSet.res index a677e8c..ab5f4de 100644 --- a/src/InductiveSet.res +++ b/src/InductiveSet.res @@ -183,12 +183,20 @@ module Make = ( let caseSubgoal = ((_constructorName: string, constructorRule: Rule.t)): Rule.t => { let offset = Array.length(constructorRule.vars) + // Extract the argument from the constructor conclusion + // e.g., from (Nat 0) extract 0, from (Nat (S n)) extract (S n) + let (_head, args) = HOTerm.strip(constructorRule.conclusion) + let constructorArg = switch args[0] { + | Some(arg) => arg + | None => raise(Unreachable("Constructor conclusion must have at least one argument")) + } + let equalityPremise = { Rule.vars: [], premises: [], conclusion: HOTerm.app( HOTerm.Symbol({name: "="}), - [HOTerm.Var({idx: offset}), constructorRule.conclusion], + [HOTerm.Var({idx: offset}), constructorArg], ), } From 53d3dd6978dcfcd0646a43ca6c4fa382e4c709b5 Mon Sep 17 00:00:00 2001 From: Mio Date: Sun, 16 Nov 2025 19:36:44 +1100 Subject: [PATCH 3/8] Only allow type constructors with arity 1 --- src/InductiveSet.res | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/src/InductiveSet.res b/src/InductiveSet.res index ab5f4de..e5b336f 100644 --- a/src/InductiveSet.res +++ b/src/InductiveSet.res @@ -40,6 +40,8 @@ module Make = ( ->Array.filterMap(((name, rule)) => extractConstructorSignature(rule)->Option.map(sig => (name, rule, sig)) ) + // Only allow type constructors with arity 1 + ->Array.filter(((_, _, (_cname, arity))) => arity == 1) ->Array.reduce(Dict.make(), (acc, (name, rule, (cname, arity))) => { let key = makeKey(cname, arity) Dict.set(acc, key, [(name, rule), ...Dict.get(acc, key)->Option.getOr([])]) @@ -188,7 +190,7 @@ module Make = ( let (_head, args) = HOTerm.strip(constructorRule.conclusion) let constructorArg = switch args[0] { | Some(arg) => arg - | None => raise(Unreachable("Constructor conclusion must have at least one argument")) + | None => raise(Unreachable("Constructor conclusion must have one argument")) } let equalityPremise = { @@ -230,10 +232,7 @@ module Make = ( let mutualComponent = findMutuallyInductiveComponent(group, groupByConstructor(state)) let inductionRule = generateInductionRule(group, mutualComponent) let casesRule = generateCasesRule(group) - [ - ("§induction-" ++ makeKey(group.name, group.arity), inductionRule), - ("§cases-" ++ makeKey(group.name, group.arity), casesRule), - ] + [("§induction-" ++ group.name, inductionRule), ("§cases-" ++ group.name, casesRule)] }) ->Dict.fromArray let serialise = (state: state) => From f9f6a4ae1e5f049b58aacce0936cdceab26836b0 Mon Sep 17 00:00:00 2001 From: Mio Date: Tue, 18 Nov 2025 19:42:39 +1100 Subject: [PATCH 4/8] add the problematic elim case --- index.html | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/index.html b/index.html index a8bcb92..8f9a409 100644 --- a/index.html +++ b/index.html @@ -365,6 +365,16 @@ + + a. + (Even a) + ------- + (Nat a) + + a. asm |- ? + + + a. (Nat a) From 156e992b98362f00461dfb5ad41a1de4d0c84052 Mon Sep 17 00:00:00 2001 From: Mio Date: Tue, 18 Nov 2025 19:50:22 +1100 Subject: [PATCH 5/8] elimination unify pass gen --- src/Method.res | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Method.res b/src/Method.res index 3faeac8..ca6033e 100644 --- a/src/Method.res +++ b/src/Method.res @@ -365,7 +365,7 @@ module Elimination = (Term: TERM, Judgment: JUDGMENT with module Term := Term) = possibleElims->Array.forEach(((elimName, elim)) => { let ruleInsts = rule->Rule.genSchemaInsts(gen, ~scope=ctx.fixes) let rule' = rule->Rule.instantiate(ruleInsts) - Judgment.unify((rule'.premises[0]->Option.getExn).conclusion, elim.conclusion) + Judgment.unify((rule'.premises[0]->Option.getExn).conclusion, elim.conclusion, ~gen) ->Seq.take(seqSizeLimit) ->Seq.forEach( elimSub => { From f41e41058c4deb315f95c4f1a92ae0f6980188ea Mon Sep 17 00:00:00 2001 From: Mio Date: Tue, 18 Nov 2025 19:46:40 +1100 Subject: [PATCH 6/8] fix gen check logic --- src/HOTerm.res | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/HOTerm.res b/src/HOTerm.res index b5725ca..21752ca 100644 --- a/src/HOTerm.res +++ b/src/HOTerm.res @@ -369,13 +369,13 @@ let flexflex = ( subst: subst, ~gen: option, ): subst => { + if gen->Option.isNone { + raise(UnifyFail("no gen provided")) + } if sa == sb { if xs->Array.length != ys->Array.length { raise(UnifyFail("flexible schematics have different number of arguments")) } - if gen->Option.isNone { - raise(UnifyFail("no gen provided")) - } let len = xs->Array.length let h = Schematic({schematic: fresh(Option.getExn(gen))}) let xs = Belt.Array.init(len, k => { From 0edbb74712ae0a0ac984011c9b8075909378abbb Mon Sep 17 00:00:00 2001 From: Mio Date: Tue, 18 Nov 2025 20:04:31 +1100 Subject: [PATCH 7/8] add constructor flag to Symbol --- src/HOTerm.res | 4 ++-- src/HOTerm.resi | 2 +- src/InductiveSet.res | 9 ++++++--- tests/HOTermTest.res | 48 ++++++++++++++++++++++++++++++++------------ 4 files changed, 44 insertions(+), 19 deletions(-) diff --git a/src/HOTerm.res b/src/HOTerm.res index 21752ca..287a703 100644 --- a/src/HOTerm.res +++ b/src/HOTerm.res @@ -5,7 +5,7 @@ module IntCmp = Belt.Id.MakeComparable({ }) type rec t = - | Symbol({name: string}) + | Symbol({name: string, constructor: bool}) | Var({idx: int}) | Schematic({schematic: int}) | Lam({name: string, body: t}) @@ -684,7 +684,7 @@ let rec parseAll = (simple: simple, ~env: env, ~gen=?): t => { let idx = env->Map.get(name)->Option.getExn Var({idx: idx}) } else { - Symbol({name: name}) + Symbol({name, constructor: false}) } | VarS({idx}) => Var({idx: idx}) | SchematicS({schematic}) => diff --git a/src/HOTerm.resi b/src/HOTerm.resi index 901b55e..d56a09e 100644 --- a/src/HOTerm.resi +++ b/src/HOTerm.resi @@ -1,5 +1,5 @@ type rec t = - | Symbol({name: string}) + | Symbol({name: string, constructor: bool}) | Var({idx: int}) | Schematic({schematic: int}) | Lam({name: string, body: t}) diff --git a/src/InductiveSet.res b/src/InductiveSet.res index e5b336f..98c4b4c 100644 --- a/src/InductiveSet.res +++ b/src/InductiveSet.res @@ -113,7 +113,7 @@ module Make = ( { Rule.vars: [], premises: [], - conclusion: HOTerm.app(HOTerm.Symbol({name: str}), HOTerm.mkvars(i)), + conclusion: HOTerm.app(HOTerm.Symbol({name: str, constructor: false}), HOTerm.mkvars(i)), }, ...subgoals, ], @@ -197,7 +197,7 @@ module Make = ( Rule.vars: [], premises: [], conclusion: HOTerm.app( - HOTerm.Symbol({name: "="}), + HOTerm.Symbol({name: "=", constructor: false}), [HOTerm.Var({idx: offset}), constructorArg], ), } @@ -217,7 +217,10 @@ module Make = ( { Rule.vars: [], premises: [], - conclusion: HOTerm.app(HOTerm.Symbol({name: str}), [HOTerm.Var({idx: 0})]), + conclusion: HOTerm.app( + HOTerm.Symbol({name: str, constructor: false}), + [HOTerm.Var({idx: 0})], + ), }, ...subgoals, ], diff --git a/tests/HOTermTest.res b/tests/HOTermTest.res index 41ea86d..c2ea8fd 100644 --- a/tests/HOTermTest.res +++ b/tests/HOTermTest.res @@ -51,8 +51,8 @@ let testUnify = (t: Zora.t, at: string, bt: string, ~subst=?, ~msg=?, ~reduce=fa testUnify0(t, bt, at, ~subst?, ~msg?, ~reduce) } zoraBlock("parse symbol", t => { - t->block("single char", t => t->Util.testParse("x", Symbol({name: "x"}))) - t->block("multi char", t => t->Util.testParse("xyz", Symbol({name: "xyz"}))) + t->block("single char", t => t->Util.testParse("x", Symbol({name: "x", constructor: false}))) + t->block("multi char", t => t->Util.testParse("xyz", Symbol({name: "xyz", constructor: false}))) }) zoraBlock("parse var", t => { @@ -66,14 +66,23 @@ zoraBlock("parse schematic", t => { zoraBlock("parse application", t => { t->block("multiple", t => { - t->Util.testParse("(a b)", App({func: Symbol({name: "a"}), arg: Symbol({name: "b"})})) + t->Util.testParse( + "(a b)", + App({ + func: Symbol({name: "a", constructor: false}), + arg: Symbol({name: "b", constructor: false}), + }), + ) }) t->block("multiple more", t => { t->Util.testParse( "(a b c)", App({ - func: App({func: Symbol({name: "a"}), arg: Symbol({name: "b"})}), - arg: Symbol({name: "c"}), + func: App({ + func: Symbol({name: "a", constructor: false}), + arg: Symbol({name: "b", constructor: false}), + }), + arg: Symbol({name: "c", constructor: false}), }), ) }) @@ -81,7 +90,7 @@ zoraBlock("parse application", t => { t->Util.testParse( "(a \\1 ?1)", App({ - func: App({func: Symbol({name: "a"}), arg: Var({idx: 1})}), + func: App({func: Symbol({name: "a", constructor: false}), arg: Var({idx: 1})}), arg: Schematic({schematic: 1}), }), ) @@ -150,7 +159,7 @@ zoraBlock("unify test", t => { t->block("flex-rigid", t => { let x = "?0" let y = "y" - t->testUnify(x, y, ~subst=emptySubst->substAdd(0, Symbol({name: "y"}))) + t->testUnify(x, y, ~subst=emptySubst->substAdd(0, Symbol({name: "y", constructor: false}))) }) t->block("flex-rigid2", t => { let x = "(x. ?0 x)" @@ -162,15 +171,28 @@ zoraBlock("unify test", t => { ~reduce=false, ~subst=emptySubst->substAdd( 0, - Lam({name: "x", body: App({func: Symbol({name: "y"}), arg: Var({idx: 0})})}), + Lam({ + name: "x", + body: App({func: Symbol({name: "y", constructor: false}), arg: Var({idx: 0})}), + }), ), ) - t->testUnify(x, y, ~reduce=true, ~subst=emptySubst->substAdd(0, Symbol({name: "y"}))) + t->testUnify( + x, + y, + ~reduce=true, + ~subst=emptySubst->substAdd(0, Symbol({name: "y", constructor: false})), + ) }) t->block("flex-rigid3", t => { let x = "(?0 \\10)" let y = "(fst \\10)" - t->testUnify(x, y, ~reduce=true, ~subst=emptySubst->substAdd(0, Symbol({name: "fst"}))) + t->testUnify( + x, + y, + ~reduce=true, + ~subst=emptySubst->substAdd(0, Symbol({name: "fst", constructor: false})), + ) }) t->block("flex-rigid", t => { let x = "(?0 \\10)" @@ -183,8 +205,8 @@ zoraBlock("unify test", t => { Lam({ name: "x", body: App({ - func: Symbol({name: "r"}), - arg: App({func: Symbol({name: "fst"}), arg: Var({idx: 0})}), + func: Symbol({name: "r", constructor: false}), + arg: App({func: Symbol({name: "fst", constructor: false}), arg: Var({idx: 0})}), }), }), ), @@ -265,7 +287,7 @@ zoraBlock("unify test", t => { "(x. ?0 x)", "a", ~reduce=true, - ~subst=emptySubst->substAdd(0, Symbol({name: "a"})), + ~subst=emptySubst->substAdd(0, Symbol({name: "a", constructor: false})), ) }) t->block("divergent", t => { From 02d49788c9da9144265323668514a5e2228a7063 Mon Sep 17 00:00:00 2001 From: Mio Date: Tue, 18 Nov 2025 20:10:24 +1100 Subject: [PATCH 8/8] parse and prettyprint for constructor --- src/HOTerm.res | 38 ++++++++++++++++++++++++++++++++------ tests/HOTermTest.res | 4 ++++ 2 files changed, 36 insertions(+), 6 deletions(-) diff --git a/src/HOTerm.res b/src/HOTerm.res index 287a703..216cc1b 100644 --- a/src/HOTerm.res +++ b/src/HOTerm.res @@ -516,7 +516,12 @@ let rec stripLam = (it: t): (array, t) => } let rec prettyPrint = (it: t, ~scope: array) => switch it { - | Symbol({name}) => name + | Symbol({name, constructor}) => + if constructor { + String.concat("@", name) + } else { + name + } | Var({idx}) => prettyPrintVar(idx, scope) | Schematic({schematic}) => "?"->String.concat(String.make(schematic)) | Lam(_) => @@ -543,7 +548,15 @@ let prettyPrintSubst = (sub: subst, ~scope: array) => let symbolRegexpString = "^([^\\s()]+)" let nameRES = "^([^\\s.\\[\\]()]+)\\." exception ParseError(string) -type token = LParen | RParen | VarT(int) | SchematicT(int) | AtomT(string) | NameT(string) | EOF +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) => { @@ -583,6 +596,16 @@ let tokenize = (str0: string): (token, string) => { } } } + | "@" => + let re = RegExp.fromStringWithFlags(symbolRegexpString, ~flags="y") + switch re->RegExp.exec(rest()) { + | None => raise(ParseError("invalid symbol")) + | Some(res) => + switch RegExp.Result.matches(res) { + | [n] => (ConsT(n), String.sliceToEnd(rest(), ~start=RegExp.lastIndex(re))) + | _ => raise(ParseError("invalid symbol")) + } + } | _ => { let reName = RegExp.fromStringWithFlags(nameRES, ~flags="y") switch reName->RegExp.exec(str) { @@ -608,7 +631,7 @@ let tokenize = (str0: string): (token, string) => { } type rec simple = | ListS({xs: array}) - | AtomS({name: string}) + | AtomS({name: string, constructor: bool}) | VarS({idx: int}) | SchematicS({schematic: int}) | LambdaS({name: string, body: simple}) @@ -636,7 +659,8 @@ let rec parseSimple = (str: string): (simple, string) => { | RParen => raise(ParseError("unexpected right parenthesis")) | VarT(idx) => (VarS({idx: idx}), rest) | SchematicT(schematic) => (SchematicS({schematic: schematic}), rest) - | AtomT(name) => (AtomS({name: name}), 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) @@ -679,8 +703,10 @@ let rec parseAll = (simple: simple, ~env: env, ~gen=?): t => { ->Array.reduce(ts[0]->Option.getExn, (acc, x) => App({func: acc, arg: x})) } } - | AtomS({name}) => - if env->Map.has(name) { + | 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 { diff --git a/tests/HOTermTest.res b/tests/HOTermTest.res index c2ea8fd..038a7b3 100644 --- a/tests/HOTermTest.res +++ b/tests/HOTermTest.res @@ -123,6 +123,9 @@ zoraBlock("parse lambda", t => { Lam({name: "x", body: App({func: Var({idx: 0}), arg: Var({idx: 0})})}), ) }) + t->block("constructor", t => { + t->Util.testParse("@cons", Symbol({name: "cons", constructor: true})) + }) // TODO: test if remaining strings are returned correctly }) @@ -130,6 +133,7 @@ zoraBlock("parse and prettyprint", t => { t->block("examples", t => { t->Util.testParsePrettyPrint("\\1", "\\1") t->Util.testParsePrettyPrint("?1", "?1") + t->Util.testParsePrettyPrint("@cons", "@cons") t->Util.testParsePrettyPrint("(x. x)", "(x. x)") t->Util.testParsePrettyPrint("(x. x. \\0)", "(x. x. x)") t->Util.testParsePrettyPrint("(x. x. \\1)", "(x. x. \\1)")