From 68bda8c2ca1d01b0eb4c804c403a3350120ee201 Mon Sep 17 00:00:00 2001
From: Josh Brown <joshcarlbrown@gmail.com>
Date: Wed, 18 Mar 2026 08:54:04 +1100
Subject: [PATCH] add concrete term method

---
 src/HOTerm.res     | 5 +++++
 src/Method.res     | 3 +--
 src/SExp.res       | 1 +
 src/SExpFunc.res   | 8 ++++++++
 src/Signatures.res | 3 ++-
 src/StringSExp.res | 5 +++++
 src/StringTerm.res | 7 +++++++
 7 files changed, 29 insertions(+), 3 deletions(-)

diff --git a/src/HOTerm.res b/src/HOTerm.res
index 8021367..a1a22fd 100644
--- a/src/HOTerm.res
+++ b/src/HOTerm.res
@@ -752,4 +752,9 @@ let parse = (str: string, ~scope: array<string>, ~gen=?) => {
 }
 
 let ghostTerm = Unallowed
+let unifiesWithAnything = t =>
+  switch t {
+  | Schematic(_) => true
+  | _ => false
+  }
 let mapTerms = (t, f) => f(t)
diff --git a/src/Method.res b/src/Method.res
index f9fd7ae..90537aa 100644
--- a/src/Method.res
+++ b/src/Method.res
@@ -147,8 +147,7 @@ module Derivation = (Term: TERM, Judgment: JUDGMENT with module Term := Term) =>
     ->Array.filterMap(((key, rule)) => {
       let insts = rule->Rule.genSchemaInsts(gen, ~scope=ctx.fixes)
       let res = rule->Rule.instantiate(insts)
-      let ghostSubs = Judgment.unify(Judgment.ghostTerm, res.conclusion)
-      if ghostSubs->Seq.head->Option.isNone {
+      if !Judgment.unifiesWithAnything(res.conclusion) {
         Some((key, res, insts))
       } else {
         None
diff --git a/src/SExp.res b/src/SExp.res
index 750649a..1b8d1cb 100644
--- a/src/SExp.res
+++ b/src/SExp.res
@@ -19,6 +19,7 @@ module ConstSymbol: SExpFunc.SYMBOL with type t = string = {
   let lowerSchematic = (_, _) => ""
   let ghost = ""
   let substDeBruijn = (name, _, ~from as _) => name
+  let unifiesWithAnything = _ => false
 }
 
 include SExpFunc.Make(ConstSymbol)
diff --git a/src/SExpFunc.res b/src/SExpFunc.res
index c053408..9d825a3 100644
--- a/src/SExpFunc.res
+++ b/src/SExpFunc.res
@@ -10,6 +10,7 @@ module type SYMBOL = {
   let lowerSchematic: (int, array<int>) => t
   let ghost: t
   let substDeBruijn: (t, array<t>, ~from: int) => t
+  let unifiesWithAnything: t => bool
 }
 
 module IntCmp = Belt.Id.MakeComparable({
@@ -426,5 +427,12 @@ module Make = (Symbol: SYMBOL): {
   }
 
   let ghostTerm = Ghost
+  let rec unifiesWithAnything = t =>
+    switch t {
+    | Schematic(_) => true
+    | Symbol(s) => Symbol.unifiesWithAnything(s)
+    | Compound({subexps}) => subexps->Array.every(unifiesWithAnything)
+    | _ => false
+    }
   let mapTerms = (t, f) => f(t)
 }
diff --git a/src/Signatures.res b/src/Signatures.res
index 747856e..7bbe013 100644
--- a/src/Signatures.res
+++ b/src/Signatures.res
@@ -25,6 +25,7 @@ module type TERM = {
   let prettyPrint: (t, ~scope: array<meta>) => string
   let prettyPrintMeta: meta => string
   let ghostTerm: t
+  let unifiesWithAnything: t => bool
 }
 
 module type JUDGMENT = {
@@ -37,11 +38,11 @@ module type JUDGMENT = {
   let reduce: t => t
   let upshift: (t, int, ~from: int=?) => t
   // Map a function over all terms in the judgment
-  // NOTE(josh): we should return to whether this is necessary.
   let mapTerms: (t, Term.t => Term.t) => t
   let parse: (string, ~scope: array<Term.meta>, ~gen: Term.gen=?) => result<(t, string), string>
   let prettyPrint: (t, ~scope: array<Term.meta>) => string
   let ghostTerm: t
+  let unifiesWithAnything: t => bool
 }
 
 module type TERM_VIEW = {
diff --git a/src/StringSExp.res b/src/StringSExp.res
index 22e4161..73dcaf3 100644
--- a/src/StringSExp.res
+++ b/src/StringSExp.res
@@ -53,6 +53,11 @@ module StringSymbol: SExpFunc.SYMBOL with type t = stringSymbol = {
       }
     | ConstS(s) => ConstS(s)
     }
+  let unifiesWithAnything = s =>
+    switch s {
+    | StringS(s) => StringTerm.unifiesWithAnything(s)
+    | ConstS(_) => false
+    }
 }
 
 include SExpFunc.Make(StringSymbol)
diff --git a/src/StringTerm.res b/src/StringTerm.res
index 04322d6..ea0b556 100644
--- a/src/StringTerm.res
+++ b/src/StringTerm.res
@@ -504,3 +504,10 @@ let parse: (string, ~scope: array<meta>, ~gen: gen=?) => result<(t, remaining),
 }
 
 let ghostTerm = [Ghost]
+let unifiesWithAnything = t =>
+  t->Array.every(p =>
+    switch p {
+    | Schematic(_) => true
+    | _ => false
+    }
+  )
-- 
2.51.2