Reconstruct data types and apply initial changes (ufmg-smite#221)

* datatypes

* changes

* reconstruction

* all changes and reconstruction

* string tests

* updates

Author: mhk119

.gitignore

@@ -1 +1,2 @@
 /.lake
+/.claude

Smt.lean

@@ -8,6 +8,7 @@ Authors: Abdalrhman Mohamed
 import Smt.BitVec
 import Smt.Bool
 import Smt.Builtin
+import Smt.Datatype
 import Smt.Int
 import Smt.Nat
 import Smt.Options

Smt/Datatype.lean

@@ -0,0 +1,9 @@
+/-
+Copyright (c) 2021-2023 by the authors listed in the file AUTHORS and their
+institutional affiliations. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Abdalrhman Mohamed
+-/
+
+import Smt.Translate.Datatype
+import Smt.Reconstruct.Datatype

Smt/Reconstruct/Datatype.lean

@@ -0,0 +1,136 @@
+/-
+Copyright (c) 2021-2023 by the authors listed in the file AUTHORS and their
+institutional affiliations. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Harun Khan
+-/
+
+import Smt.Reconstruct
+
+namespace Smt.Reconstruct.Datatype
+
+open Lean Meta Qq
+
+/-- Names of types that already have dedicated sort/term/proof reconstructors
+and should not be handled by the generic datatype reconstructor. -/
+private def builtinTypeNames : Std.HashSet Name :=
+  Std.HashSet.ofList [
+    ``Bool, `Prop, ``True, ``False,
+    ``Or, ``And, ``Iff, ``Exists,
+    ``Nat, ``Int, `Rat, `Real,
+    ``String, ``BitVec
+  ]
+
+/-- Return `true` when the name (or its prefix for a constructor) belongs to a
+type with dedicated built-in reconstruction support. -/
+private def isBuiltinName (n : Name) : Bool :=
+  builtinTypeNames.contains n ||
+  -- Also catch constructor names like `Bool.true`, `Nat.zero`, etc.
+  match n with
+  | .str p _ => builtinTypeNames.contains p
+  | _ => false
+
+-- Strip SMT-LIB2 pipe quoting (|name|) from a symbol if present.
+private def stripSMTPipes (s : String) : String :=
+  if s.startsWith "|" && s.endsWith "|" then (s.drop 1 |>.dropEnd 1).toString else s
+
+private def getFVarOrConstExpr! (n : String) : ReconstructM Expr := do
+  match (← read).userNames[n]? with
+  | some e => return e
+  | none   => match (← getLCtx).findFromUserName? n.toName with
+    | some d => return d.toExpr
+    | none   =>
+      let c ← getConstInfo n.toName
+      return .const c.name (c.numLevelParams.repeat (.zero :: ·) [])
+
+@[smt_sort_reconstruct] def reconstructDatatypeSort : SortReconstructor := fun s => do
+  match s.getKind! with
+  | .DATATYPE_SORT =>
+    let name := s.getDatatype!.getName!
+    if isBuiltinName name.toName then return none
+    getFVarOrConstExpr! name
+  | _ => return none
+
+@[smt_term_reconstruct] def reconstructDatatypeTerm : TermReconstructor := fun t => do
+  match t.getKind! with
+  | .APPLY_CONSTRUCTOR =>
+    -- t[0]! is the constructor symbol. It has INTERNAL_KIND in cvc5 (even for non-zero-arity),
+    -- so we look it up by name instead of calling reconstructTerm recursively.
+    -- toString may include SMT-LIB pipe escaping (e.g., "|mynat'.succ|"), so strip it.
+    let ctorName := stripSMTPipes t[0]!.toString
+    if isBuiltinName ctorName.toName then return none
+    let mut curr ← getFVarOrConstExpr! ctorName
+    for i in [1:t.getNumChildren] do
+      curr := .app curr (← reconstructTerm t[i]!)
+    return curr
+  | _ => return none
+
+/-- Build a Lean proof of `(t = s) = False` where `t` and `s` are
+distinct constructors of the same inductive type. Uses the `noConfusion`
+principle that Lean auto-generates for every inductive type. -/
+private def proveConsClash (t s : Expr) : MetaM Expr := do
+  let α ← inferType t
+  let .const αName _ := α.getAppFn
+    | throwError "Smt.Reconstruct.Datatype: expected inductive type, got {α}"
+  let ncName := αName ++ `noConfusion
+  let heq ← mkEq t s
+  -- Forward: (t = s) → False  via noConfusion with motive False
+  let fwd ← withLocalDeclD `h heq fun h => do
+    let nc ← mkAppOptM ncName #[some (mkConst ``False), some t, some s, some h]
+    mkLambdaFVars #[h] nc
+  -- Backward: False → (t = s)  via False.elim
+  let bwd ← withLocalDeclD `h (mkConst ``False) fun h => do
+    let fe ← mkAppOptM ``False.elim #[some heq, some h]
+    mkLambdaFVars #[h] fe
+  let iff_pf ← mkAppM ``Iff.intro #[fwd, bwd]
+  mkAppM ``propext #[iff_pf]
+
+def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
+  match pf.getRewriteRule! with
+  | .MACRO_DT_CONS_EQ
+  | .DT_CONS_EQ_CLASH =>
+    let result := pf.getResult
+    -- Only handle the "clash" case: (t = s) = false (distinct constructors)
+    if result[1]!.getKind! == .CONST_BOOLEAN && !result[1]!.getBooleanValue! then
+      let sort := result[0]![0]!.getSort!
+      if sort.getKind! == .DATATYPE_SORT && isBuiltinName sort.getDatatype!.getName!.toName then
+        return none
+      let (u, (α : Q(Sort u))) ← reconstructSortLevelAndSort sort
+      let t : Q($α) ← reconstructTerm result[0]![0]!
+      let s : Q($α) ← reconstructTerm result[0]![1]!
+      addTac q(($t = $s) = False) fun mv => do
+        let proof ← mv.withContext (proveConsClash t s)
+        mv.assign proof
+    else
+      return none
+  | _ => return none
+
+/-- Build a Lean proof of `¬(t = s)` where `t` and `s` are distinct constructors.
+Uses the `noConfusion` principle: `fun h : t = s => noConfusion False t s h`. -/
+private def proveDistinctValues (t s : Expr) : MetaM Expr := do
+  let α ← inferType t
+  let .const αName _ := α.getAppFn
+    | throwError "Smt.Reconstruct.Datatype: expected inductive type, got {α}"
+  let ncName := αName ++ `noConfusion
+  let heq ← mkEq t s
+  withLocalDeclD `h heq fun h => do
+    let nc ← mkAppOptM ncName #[some (mkConst ``False), some t, some s, some h]
+    mkLambdaFVars #[h] nc
+
+@[smt_proof_reconstruct] def reconstructDatatypeProof : ProofReconstructor := fun pf => do
+  match pf.getRule with
+  | .DSL_REWRITE
+  | .THEORY_REWRITE => reconstructRewrite pf
+  | .DISTINCT_VALUES =>
+    let sort := pf.getArguments[0]!.getSort!
+    if sort.getKind! == .DATATYPE_SORT && isBuiltinName sort.getDatatype!.getName!.toName then
+      return none
+    let (u, (α : Q(Sort u))) ← reconstructSortLevelAndSort sort
+    let t : Q($α) ← reconstructTerm pf.getArguments[0]!
+    let s : Q($α) ← reconstructTerm pf.getArguments[1]!
+    addTac q($t ≠ $s) fun mv => do
+      let proof ← mv.withContext (proveDistinctValues t s)
+      mv.assign proof
+  | _ => return none
+
+end Smt.Reconstruct.Datatype

Smt/Reconstruct/UF.lean

@@ -26,9 +26,12 @@ def getFVarOrConstExpr! (n : String) : ReconstructM Expr := do
   | .UNINTERPRETED_SORT => getFVarOrConstExpr! s.getSymbol!
   | _ =>
     if s.isInstantiated then
-      let base ← reconstructSort s.getUninterpretedSortConstructor!
-      let params ← s.getInstantiatedParameters!.mapM reconstructSort
-      return some (mkAppN base params)
+      if let some ctor := s.getUninterpretedSortConstructor? then
+        let base ← reconstructSort ctor
+        let params ← s.getInstantiatedParameters!.mapM reconstructSort
+        return some (mkAppN base params)
+      else
+        return none
     else
       return none
 

Smt/Tactic/Smt.lean

@@ -227,6 +227,19 @@ macro "smt_show " c:optConfig h:smtHints : tactic => do
 
 declare_config_elab elabConfig Smt.Config
 
+/-- If `nm` names a non-Prop definition with auto-generated equation lemmas `nm.eq_1`, `nm.eq_2`, …,
+return those as expressions.  Returns an empty array for theorems/props or missing lemmas. -/
+private def getEqLemmas (nm : Name) : MetaM (Array Expr) := do
+  let env ← getEnv
+  let some info := env.find? nm | return #[]
+  -- Only expand non-Prop definitions (i.e., functions, not theorems)
+  if info.type.isProp then return #[]
+  -- Use Lean's proper API to retrieve the auto-generated equation lemmas.
+  let some eqNames ← Lean.Meta.getEqnsFor? nm | return #[]
+  return eqNames.map fun eqNm =>
+    let lvls := (env.find? eqNm).map (·.levelParams.map .param) |>.getD []
+    .const eqNm lvls
+
 def elabSmtHintElem : TSyntax ``smtHintElem → TacticM (Array (Expr × (TSyntax ``smtHintElem)) × Array Expr)
   | `(smtHintElem| *) => do
     let fvs ← Smt.Preprocess.getPropHyps
@@ -243,6 +256,22 @@ def elabSmtHintElem : TSyntax ``smtHintElem → TacticM (Array (Expr × (TSyntax
         `(smtHintElem| *)
     return (hs.zip ss, hs)
   | `(smtHintElem| $h:term) => do
+    -- If the hint is a bare identifier naming a non-Prop definition, expand it to its
+    -- auto-generated equation lemmas (nm.eq_1, nm.eq_2, …) automatically.
+    let eqExprs ← do
+      if h.raw.isIdent then
+        let nm := h.raw.getId
+        let env ← getEnv
+        if let some info := env.find? nm then
+          if !info.type.isProp then
+            getEqLemmas nm
+          else pure #[]
+        else pure #[]
+      else pure #[]
+    if !eqExprs.isEmpty then
+      let pairs ← eqExprs.mapM fun e => return (e, ← `(smtHintElem| $h:term))
+      return (pairs, eqExprs)
+    -- Fall through: treat as a regular lemma (prop hypothesis or theorem).
     let h' ← Auto.Prep.elabLemma h (.leaf s!"❰{h}❱")
     return (#[(h'.proof, ← `(smtHintElem| $h:term))], #[h'.proof])
   | _ => throwUnsupportedSyntax

Smt/Translate/Commands.lean

@@ -20,6 +20,8 @@ inductive Command where
   | declareSort (nm : String) (arity : Nat)
   | defineSort (nm : String) (ps : List Term) (tm : Term)
   | declare (nm : String) (st : Term)
+  | declareDatatypes (sorts : List (String × Nat))
+      (dtypes : List (List (String × List (String × Term))))
   | defineFun (nm : String) (ps : List (String × Term)) (cod : Term) (tm : Term) (rec : Bool)
   | assert (tm : Term)
   | checkSat
@@ -52,6 +54,18 @@ protected def toSexp : Command → Sexp
   | .declare nm st                => sexp!{(declare-const {quoteSymbol nm} {st})}
   | .declareSort nm arity         =>
     sexp!{(declare-sort {quoteSymbol nm} {toString arity})}
+  | .declareDatatypes sorts dtypes =>
+    let sortDecls : List Sexp :=
+      sorts.map fun (nm, ar) => sexp!{({quoteSymbol nm} {toString ar})}
+    let dtypeDecls : List Sexp :=
+      dtypes.map fun ctors =>
+        let ctorDecls : List Sexp :=
+          ctors.map fun (ctorNm, fields) =>
+            let flds : List Sexp :=
+              fields.map fun (fnm, fsort) => sexp!{({quoteSymbol fnm} {fsort})}
+            sexp!{({quoteSymbol ctorNm} ...{flds})}
+        sexp!{(...{ctorDecls})}
+    sexp!{(declare-datatypes (...{sortDecls}) (...{dtypeDecls}))}
   | .defineSort nm ps tm          =>
     sexp!{(define-sort {quoteSymbol nm} (...{ps.map toSexp}) {tm})}
   | .defineFun nm ps cod tm false =>

Smt/Translate/Datatype.lean

@@ -0,0 +1,49 @@
+/-
+Copyright (c) 2021-2022 by the authors listed in the file AUTHORS and their
+institutional affiliations. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Abdalrhman Mohamed, Wojciech Nawrocki
+-/
+
+import Smt.Translate
+import Smt.Util
+
+namespace Smt.Translate.Datatype
+
+open Translator Term Lean
+
+/-- Inductive types that have dedicated translators and should not be handled
+as generic SMT-LIB datatypes. -/
+private def builtinInductives : Std.HashSet Name :=
+  Std.HashSet.ofList [
+    ``Bool, ``True, ``False,
+    ``Or, ``And, ``Iff, ``Exists,
+    ``Nat, ``Int, ``String, ``BitVec
+  ]
+
+/-- Translate a constructor of a simple (non-parametric) inductive type.
+The inductive type itself is marked as a dependency so that the query builder will emit a
+`declare-datatypes` command for it. Constructor arguments are translated recursively.
+
+Constructors of parametric inductives, indexed inductives, or inductives whose sort name is
+already known to SMT-LIB (e.g. `Bool`) are left to other translators or the fallthrough
+mechanism. Only fully applied constructors are handled. -/
+@[smt_translate] def translateConstructor : Translator := fun e => do
+  let some (v, args) ← Lean.Meta.constructorApp? e | return none
+  let env ← getEnv
+  let inductName := v.induct
+  -- Skip types that SMT-LIB already knows about or that have dedicated translators.
+  if Util.smtConsts.contains inductName.toString then return none
+  if builtinInductives.contains inductName then return none
+  -- Only handle simple non-parametric, non-indexed inductives.
+  let some (.inductInfo iVal) := env.find? inductName | return none
+  if iVal.numParams != 0 || iVal.numIndices != 0 then return none
+  -- Only handle fully applied constructors.
+  if args.size != v.numFields then return none
+  -- Mark the inductive type as a dependency; the query builder will declare it.
+  modify fun st => { st with depConstants := st.depConstants.insert inductName }
+  -- Translate constructor arguments and build the application.
+  let translatedArgs ← args.mapM applyTranslators!
+  return some (translatedArgs.foldl appT (symbolT v.name.toString))
+
+end Smt.Translate.Datatype

Smt/Translate/Query.lean

@@ -135,12 +135,53 @@ def addDefineCommandFor (nm : String) (e : Expr) (params : Array Expr) (cod : Ex
 def addDeclareCommandFor (nm : String) (e tp : Expr) (params : Array Expr) (cod : Expr)
     : QueryBuilderM (Array Expr) := do
   if cod.isSort && !cod.isProp then
+    -- For simple (non-parametric) inductive types, emit a
+    -- `declare-datatypes` command so the solver has full algebraic datatype support.
+    if params.isEmpty then
+      if let some cname := e.constName? then
+        if let some (.inductInfo iVal) := (← getEnv).find? cname then
+          if iVal.numParams == 0 && iVal.numIndices == 0 then
+            -- Build the list of constructor declarations with field selectors.
+            let mut allDeps : Array Expr := #[]
+            let mut ctorDecls : List (String × List (String × Term)) := []
+            let mut allOk := true
+            for ctorNm in iVal.ctors do
+              match (← getEnv).find? ctorNm with
+              | some (.ctorInfo cVal) =>
+                let fields := ctorFieldTypes cVal.numFields cVal.type
+                let mut fieldDecls : List (String × Term) := []
+                let mut selectorNames : Std.HashSet String := {}
+                let mut idx := 0
+                for (fname, ftype) in fields do
+                  let baseName :=
+                    if fname == Name.anonymous then s!"field{idx + 1}" else fname.toString
+                  let mut selectorName := s!"{ctorNm}.{baseName}"
+                  let mut suffix := 1
+                  while selectorNames.contains selectorName do
+                    selectorName := s!"{ctorNm}.{baseName}_{suffix}"
+                    suffix := suffix + 1
+                  selectorNames := selectorNames.insert selectorName
+                  let (tmSort, deps) ← translateAndFindDeps ftype (fvarDeps := false)
+                  fieldDecls := fieldDecls ++ [(selectorName, tmSort)]
+                  allDeps := allDeps ++ deps
+                  idx := idx + 1
+                ctorDecls := ctorDecls ++ [(ctorNm.toString, fieldDecls)]
+              | _ => allOk := false
+            if allOk then
+              addCommand e <| .declareDatatypes [(nm, 0)] [ctorDecls]
+              return allDeps
     addCommand e <| .declareSort nm params.size
     return #[]
   else
     let (tmTp, deps) ← translateAndFindDeps tp
     addCommand e <| .declare nm tmTp
     return deps
+where
+  /-- Extract the first `n` field name/type pairs from a constructor's type (a chain of `forallE`). -/
+  ctorFieldTypes : Nat → Expr → List (Name × Expr)
+    | 0, _ => []
+    | n + 1, .forallE nm ftype body _ => (nm, ftype) :: ctorFieldTypes n body
+    | _, _ => []
 
 /-- Build the command for `e : tp` and add it to the graph. Return the command's dependencies. -/
 def addCommandFor (e tp : Expr) : QueryBuilderM (Array Expr) := do

Test/Int/DefineSort.expected

@@ -3,11 +3,11 @@ goal: a.add b = b.add a
 query:
 (set-logic ALL)
 (declare-sort MyInt 0)
-(declare-fun |a✝²| (MyInt MyInt) MyInt)
-(declare-sort |a✝¹| 0)
+(declare-fun MyInt.add (MyInt MyInt) MyInt)
+(assert (forall ((a MyInt)) (forall ((b MyInt)) (= (MyInt.add a b) (+ a b)))))
+(assert (= MyInt Int))
 (declare-const b MyInt)
 (declare-const a MyInt)
-(declare-fun MyInt.add (MyInt MyInt) MyInt)
 (assert (not (= (MyInt.add a b) (MyInt.add b a))))
 (check-sat)
 Test/Int/DefineSort.lean:6:0: warning: declaration uses `sorry`