bug fixes and constructors

index.html

@@ -365,6 +365,16 @@
 
     </hol-proof>
 
+    <hol-proof id="index.html/prooftest-elim-bug" deps="index.html/myconfig index.html/baz index.html/nat">
+    a.
+      (Even a)
+      ------- 
+      (Nat a)
+
+    a. asm |- ?
+
+    </hol-proof>
+
     <hol-proof id="index.html/prooftest" deps="index.html/myconfig index.html/baz index.html/nat">
     a.
       (Nat a)

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})
@@ -369,13 +369,13 @@ let flexflex = (
   subst: subst,
   ~gen: option<gen>,
 ): 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 => {
@@ -516,7 +516,12 @@ let rec stripLam = (it: t): (array<string>, t) =>
   }
 let rec prettyPrint = (it: t, ~scope: array<string>) =>
   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<string>) =>
 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<simple>})
-  | 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,12 +703,14 @@ 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 {
-      Symbol({name: name})
+      Symbol({name, constructor: false})
     }
   | VarS({idx}) => Var({idx: idx})
   | SchematicS({schematic}) =>

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})

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([])])
@@ -111,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,
       ],
@@ -183,12 +185,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 one argument"))
+      }
+
       let equalityPremise = {
         Rule.vars: [],
         premises: [],
         conclusion: HOTerm.app(
-          HOTerm.Symbol({name: "="}),
-          [HOTerm.Var({idx: offset}), constructorRule.conclusion],
+          HOTerm.Symbol({name: "=", constructor: false}),
+          [HOTerm.Var({idx: offset}), constructorArg],
         ),
       }
 
@@ -207,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,
       ],
@@ -222,10 +235,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) =>

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 => {

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,22 +66,31 @@ 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}),
       }),
     )
   })
   t->block("multiple var", 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}),
       }),
     )
@@ -114,13 +123,17 @@ 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
 })
 
 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)")
@@ -150,7 +163,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 +175,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 +209,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 +291,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 => {
@@ -279,6 +305,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(