continue refactoring

Auto/Tactic.lean

@@ -313,6 +313,77 @@ def querySMT (exportFacts : Array REntry) (exportInds : Array MutualIndInfo) : L
   else
     return .none
 
+open LamReif Embedding.Lam in
+/--
+  Given
+  · `nonempties = #[s₀, s₁, ⋯, sᵤ₋₁]`
+  · `valids = #[t₀, t₁, ⋯, kₖ₋₁]`
+  Invoke prover to get a proof of
+    `proof : (∀ (_ : v₀) (_ : v₁) ⋯ (_ : vᵤ₋₁), w₀ → w₁ → ⋯ → wₗ₋₁ → ⊥).interp`
+  and returns
+  · `fun etoms => proof`
+  · `∀ etoms, ∀ (_ : v₀) (_ : v₁) ⋯ (_ : vᵤ₋₁), w₀ → w₁ → ⋯ → wₗ₋₁ → ⊥)`
+  · `etoms`
+  · `[s₀, s₁, ⋯, sᵤ₋₁]`
+  · `[w₀, w₁, ⋯, wₗ₋₁]`
+  Here
+  · `[v₀, v₁, ⋯, vᵤ₋₁]` is a subsequence of `[s₀, s₁, ⋯, sᵤ₋₁]`
+  · `[w₀, w₁, ⋯, wₗ₋₁]` is a subsequence of `[t₀, t₁, ⋯, kₖ₋₁]`
+  · `etoms` are all the etoms present in `w₀ → w₁ → ⋯ → wₗ₋₁ → ⊥`
+
+  Note that `MetaState.withTemporaryLCtx` is used to isolate the prover from the
+  current local context. This is necessary because `lean-auto` assumes that the prover
+  does not use free variables introduced during monomorphization
+-/
+def callNative_checker
+  (nonempties : Array REntry) (valids : Array REntry) (prover : Array Lemma → MetaM Expr) :
+  ReifM (Expr × LamTerm × Array Nat × Array REntry × Array REntry) := do
+  let tyVal ← LamReif.getTyVal
+  let varVal ← LamReif.getVarVal
+  let lamEVarTy ← LamReif.getLamEVarTy
+  let validsWithDTr ← valids.mapM (fun re =>
+    do return (re, ← collectDerivFor re))
+  MetaState.runAtMetaM' <| (Lam2DU.callNativeWithAtomAsFVar nonempties validsWithDTr prover).run'
+    { tyVal := tyVal, varVal := varVal, lamEVarTy := lamEVarTy }
+
+open LamReif Embedding.Lam in
+/--
+  Similar in functionality compared to `callNative_checker`, but
+    all `valid` entries are supposed to be reified facts (so there should
+    be no `etom`s). We invoke the prover to get the same `proof` as
+    `callNativeChecker`, but we return a proof of `⊥` by applying `proof`
+    to un-reified facts.
+
+  Note that `MetaState.withTemporaryLCtx` is used to isolate the prover from the
+  current local context. This is necessary because `lean-auto` assumes that the prover
+  does not use free variables introduced during monomorphization
+-/
+def callNative_direct
+  (nonempties : Array REntry) (valids : Array REntry) (prover : Array Lemma → MetaM Expr) : ReifM Expr := do
+  let tyVal ← LamReif.getTyVal
+  let varVal ← LamReif.getVarVal
+  let lamEVarTy ← LamReif.getLamEVarTy
+  let validsWithDTr ← valids.mapM (fun re =>
+    do return (re, ← collectDerivFor re))
+  let (proof, _, usedEtoms, usedInhs, usedHyps) ← MetaState.runAtMetaM' <|
+    (Lam2DU.callNativeWithAtomAsFVar nonempties validsWithDTr prover).run'
+      { tyVal := tyVal, varVal := varVal, lamEVarTy := lamEVarTy }
+  if usedEtoms.size != 0 then
+    throwError "callNative_direct :: etoms should not occur here"
+  let ss ← usedInhs.mapM (fun re => do
+    match ← lookupREntryProof! re with
+    | .inhabitation e _ _ => return e
+    | .chkStep (.n (.nonemptyOfAtom n)) =>
+      match varVal[n]? with
+      | .some (e, _) => return e
+      | .none => throwError "callNative_direct :: Unexpected error"
+    | _ => throwError "callNative_direct :: Cannot find external proof of {re}")
+  let ts ← usedHyps.mapM (fun re => do
+    let .assertion e _ _ ← lookupREntryProof! re
+      | throwError "callNative_direct :: Cannot find external proof of {re}"
+    return e)
+  return mkAppN proof (ss ++ ts)
+
 open Embedding.Lam in
 /--
   If `prover?` is specified, use the specified one.
@@ -322,7 +393,7 @@ def queryNative
   (declName? : Option Name) (exportFacts exportInhs : Array REntry)
   (prover? : Option (Array Lemma → MetaM Expr) := .none) : LamReif.ReifM (Option Expr) := do
   let (proof, proofLamTerm, usedEtoms, usedInhs, unsatCore) ←
-    Lam2D.callNative_checker exportInhs exportFacts (prover?.getD Solver.Native.queryNative)
+    callNative_checker exportInhs exportFacts (prover?.getD Solver.Native.queryNative)
   LamReif.newAssertion proof (.leaf "by_native::queryNative") proofLamTerm
   let etomInstantiated ← LamReif.validOfInstantiateForall (.valid [] proofLamTerm) (usedEtoms.map .etom)
   let forallElimed ← LamReif.validOfElimForalls etomInstantiated usedInhs
@@ -432,7 +503,7 @@ def monoInterface
     let exportInhs := (← LamReif.getRst).nonemptyMap.toArray.map
       (fun (s, _) => Embedding.Lam.REntry.nonempty s)
     LamReif.printValuation
-    Lam2D.callNative_direct exportInhs exportFacts prover)
+    callNative_direct exportInhs exportFacts prover)
   let (proof, _) ← Monomorphization.monomorphize lemmas inhFacts (@id (Reif.ReifM Expr) do
     let uvalids ← liftM <| Reif.getFacts
     let uinhs ← liftM <| Reif.getInhTys

Auto/Translation.lean

@@ -4,4 +4,4 @@ import Auto.Translation.Monomorphization
 import Auto.Translation.LamReif
 import Auto.Translation.LamFOL2SMT
 import Auto.Translation.Lam2TH0
-import Auto.Translation.Lam2D
+import Auto.Translation.Lam2DUninterpreted

Auto/Translation/Lam2D.lean → Auto/Translation/Lam2DUninterpreted.lean

@@ -3,9 +3,9 @@ import Auto.Lib.ExprExtra
 import Auto.Lib.MetaExtra
 import Auto.Lib.MetaState
 import Auto.Lib.ToExprExtra
-import Auto.Embedding.LamBase
-import Auto.Translation.LamReif
-import Auto.Translation.Lam2DBase
+import Auto.Embedding.LamChecker
+import Auto.Translation.Assumptions
+import Auto.Translation.LamUtils
 open Lean
 
 initialize
@@ -28,10 +28,9 @@ initialize
     in `LamReif.lean`.
 -/
 
-namespace Auto.Lam2D
+namespace Auto.Lam2DU
 
-open LamReif
-open Embedding.Lam MetaState
+open Embedding.Lam LamExportUtils MetaState
 
 /--
   All the type atoms and term atoms are interpreted as fvars, which
@@ -145,7 +144,7 @@ def interpOtherConstAsUnlifted (oc : OtherConst) : ExternM Expr := do
       | throwError "interpOtherConstAsUnlifted :: Unexpected sort {sortterm}"
     return Lean.mkApp2 (constIdExpr [lvlattr, lvlterm]) tyattr tyterm
 
-open Embedding in
+open Embedding Lam2D in
 def interpLamBaseTermAsUnlifted : LamBaseTerm → ExternM Expr
 | .pcst pc    => interpPropConstAsUnlifted pc
 | .bcst bc    => return interpBoolConstAsUnlifted bc
@@ -239,14 +238,13 @@ def withHyps (hyps : Array Expr) : ExternM (Array FVarId) := do
   current local context. This is necessary because `lean-auto` assumes that the prover
   does not use free variables introduced during monomorphization
 -/
-private def callNativeExternMAction
+def callNativeWithAtomAsFVar
   (nonempties : Array REntry) (validsWithDTr : Array (REntry × DTr)) (prover : Array Lemma → MetaM Expr) :
-  ExternM (Expr × LamTerm × Array Nat ×
-    Array REntry × Array REntry) := MetaState.withTemporaryLCtx {} {} <| do
+  ExternM (Expr × LamTerm × Array Nat × Array REntry × Array REntry) := MetaState.withTemporaryLCtx {} {} <| do
   let ss ← nonempties.mapM (fun re => do
     match re with
     | .nonempty s => return s
-    | _ => throwError "callNativeExternMAction :: {re} is not a `nonempty` entry")
+    | _ => throwError "callNativeWithAtomAsFVar :: {re} is not a `nonempty` entry")
   let inhs ← withTranslatedLamSorts ss
   for inh in inhs do
     trace[auto.printInhs] "{inh}"
@@ -256,7 +254,7 @@ private def callNativeExternMAction
   let ts ← valids.mapM (fun re => do
     match re with
     | .valid [] t => return t
-    | _ => throwError "callNativeExternMAction :: {re} is not a `valid` entry")
+    | _ => throwError "callNativeWithAtomAsFVar :: {re} is not a `valid` entry")
   let hyps ← withTranslatedLamTerms ts
   for hyp in hyps do
     if !(← runMetaM <| Meta.isTypeCorrect hyp) then
@@ -310,73 +308,4 @@ private def callNativeExternMAction
     trace[auto.lam2D.printProof] "Found proof of {proofLamTerm}\n\n{proof}"
     return (proof, proofLamTerm, ⟨usedEtoms⟩, ⟨usedInhs.map Prod.fst⟩, ⟨usedHyps.map Prod.fst⟩))
 
-/--
-  Given
-  · `nonempties = #[s₀, s₁, ⋯, sᵤ₋₁]`
-  · `valids = #[t₀, t₁, ⋯, kₖ₋₁]`
-  Invoke prover to get a proof of
-    `proof : (∀ (_ : v₀) (_ : v₁) ⋯ (_ : vᵤ₋₁), w₀ → w₁ → ⋯ → wₗ₋₁ → ⊥).interp`
-  and returns
-  · `fun etoms => proof`
-  · `∀ etoms, ∀ (_ : v₀) (_ : v₁) ⋯ (_ : vᵤ₋₁), w₀ → w₁ → ⋯ → wₗ₋₁ → ⊥)`
-  · `etoms`
-  · `[s₀, s₁, ⋯, sᵤ₋₁]`
-  · `[w₀, w₁, ⋯, wₗ₋₁]`
-  Here
-  · `[v₀, v₁, ⋯, vᵤ₋₁]` is a subsequence of `[s₀, s₁, ⋯, sᵤ₋₁]`
-  · `[w₀, w₁, ⋯, wₗ₋₁]` is a subsequence of `[t₀, t₁, ⋯, kₖ₋₁]`
-  · `etoms` are all the etoms present in `w₀ → w₁ → ⋯ → wₗ₋₁ → ⊥`
-
-  Note that `MetaState.withTemporaryLCtx` is used to isolate the prover from the
-  current local context. This is necessary because `lean-auto` assumes that the prover
-  does not use free variables introduced during monomorphization
--/
-def callNative_checker
-  (nonempties : Array REntry) (valids : Array REntry) (prover : Array Lemma → MetaM Expr) :
-  ReifM (Expr × LamTerm × Array Nat × Array REntry × Array REntry) := do
-  let tyVal ← LamReif.getTyVal
-  let varVal ← LamReif.getVarVal
-  let lamEVarTy ← LamReif.getLamEVarTy
-  let validsWithDTr ← valids.mapM (fun re =>
-    do return (re, ← collectDerivFor re))
-  runAtMetaM' <| (callNativeExternMAction nonempties validsWithDTr prover).run'
-    { tyVal := tyVal, varVal := varVal, lamEVarTy := lamEVarTy }
-
-/--
-  Similar in functionality compared to `callNative_checker`, but
-    all `valid` entries are supposed to be reified facts (so there should
-    be no `etom`s). We invoke the prover to get the same `proof` as
-    `callNativeChecker`, but we return a proof of `⊥` by applying `proof`
-    to un-reified facts.
-
-  Note that `MetaState.withTemporaryLCtx` is used to isolate the prover from the
-  current local context. This is necessary because `lean-auto` assumes that the prover
-  does not use free variables introduced during monomorphization
--/
-def callNative_direct
-  (nonempties : Array REntry) (valids : Array REntry) (prover : Array Lemma → MetaM Expr) : ReifM Expr := do
-  let tyVal ← LamReif.getTyVal
-  let varVal ← LamReif.getVarVal
-  let lamEVarTy ← LamReif.getLamEVarTy
-  let validsWithDTr ← valids.mapM (fun re =>
-    do return (re, ← collectDerivFor re))
-  let (proof, _, usedEtoms, usedInhs, usedHyps) ← runAtMetaM' <|
-    (callNativeExternMAction nonempties validsWithDTr prover).run'
-      { tyVal := tyVal, varVal := varVal, lamEVarTy := lamEVarTy }
-  if usedEtoms.size != 0 then
-    throwError "callNative_direct :: etoms should not occur here"
-  let ss ← usedInhs.mapM (fun re => do
-    match ← lookupREntryProof! re with
-    | .inhabitation e _ _ => return e
-    | .chkStep (.n (.nonemptyOfAtom n)) =>
-      match varVal[n]? with
-      | .some (e, _) => return e
-      | .none => throwError "callNative_direct :: Unexpected error"
-    | _ => throwError "callNative_direct :: Cannot find external proof of {re}")
-  let ts ← usedHyps.mapM (fun re => do
-    let .assertion e _ _ ← lookupREntryProof! re
-      | throwError "callNative_direct :: Cannot find external proof of {re}"
-    return e)
-  return mkAppN proof (ss ++ ts)
-
-end Auto.Lam2D
+end Auto.Lam2DU

Auto/Translation/Lam2TH0.lean

@@ -5,13 +5,13 @@ namespace Auto
 open Lean Embedding.Lam Lam2TH0
 
 def lam2TH0 (lamVarTy : Array LamSort) (lamEVarTy : Array LamSort) (facts : Array LamTerm) : CoreM String := do
-  let (typeHs, termHs, etomHs) ← LamReif.collectLamTermsAtoms lamVarTy lamEVarTy facts
-  let bvHs := LamReif.collectLamTermsBitvecs facts
-  let bvLengthHs := LamReif.collectLamSortsBitVecLengths (
+  let (typeHs, termHs, etomHs) ← LamExportUtils.collectLamTermsAtoms lamVarTy lamEVarTy facts
+  let bvHs := LamExportUtils.collectLamTermsBitvecs facts
+  let bvLengthHs := LamExportUtils.collectLamSortsBitVecLengths (
     bvHs.toArray.map BitVecConst.lamCheck ++ lamVarTy ++ lamEVarTy)
-  let ncHs := LamReif.collectLamTermsNatConsts facts
-  let icHs := LamReif.collectLamTermsIntConsts facts
-  let scHs := LamReif.collectLamTermsStringConsts facts
+  let ncHs := LamExportUtils.collectLamTermsNatConsts facts
+  let icHs := LamExportUtils.collectLamTermsIntConsts facts
+  let scHs := LamExportUtils.collectLamTermsStringConsts facts
   let sorts :=
     ["thf(sortdecl_nat, type, s_nat: $tType).",
      "thf(sortdecl_int, type, s_int: $tType).",