From d81253b40a2dbca7d0aac8a5dd4b8e6493148db4 Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Mon, 29 Apr 2024 18:53:13 -0400 Subject: [PATCH 1/3] Updating lean-auto --- lake-manifest.json | 4 ++-- lakefile.lean | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index a1df85f..a0a4133 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -13,10 +13,10 @@ {"url": "https://github.com/leanprover-community/lean-auto.git", "type": "git", "subDir": null, - "rev": "df285d9950123b2799ea71d9772d1a806f7d1e7a", + "rev": "29d65a800b84cf2abe49c918acdfef7114b911ba", "name": "auto", "manifestFile": "lake-manifest.json", - "inputRev": "df285d9950123b2799ea71d9772d1a806f7d1e7a", + "inputRev": "29d65a800b84cf2abe49c918acdfef7114b911ba", "inherited": false, "configFile": "lakefile.lean"}], "name": "Duper", diff --git a/lakefile.lean b/lakefile.lean index b6e5c49..c2708a1 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -2,7 +2,7 @@ import Lake open Lake DSL -require auto from git "https://github.com/leanprover-community/lean-auto.git"@"df285d9950123b2799ea71d9772d1a806f7d1e7a" +require auto from git "https://github.com/leanprover-community/lean-auto.git"@"29d65a800b84cf2abe49c918acdfef7114b911ba" package Duper { precompileModules := true From 85318120db1fdd725a0bbe140f7c6405381c7c33 Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Mon, 20 May 2024 01:15:36 -0400 Subject: [PATCH 2/3] Updating lean-auto --- lake-manifest.json | 4 ++-- lakefile.lean | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index a0a4133..a39fcb8 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -13,10 +13,10 @@ {"url": "https://github.com/leanprover-community/lean-auto.git", "type": "git", "subDir": null, - "rev": "29d65a800b84cf2abe49c918acdfef7114b911ba", + "rev": "3a973bb913c5b2db346a7e47b0b9bb6e3277e9b9", "name": "auto", "manifestFile": "lake-manifest.json", - "inputRev": "29d65a800b84cf2abe49c918acdfef7114b911ba", + "inputRev": "3a973bb913c5b2db346a7e47b0b9bb6e3277e9b9", "inherited": false, "configFile": "lakefile.lean"}], "name": "Duper", diff --git a/lakefile.lean b/lakefile.lean index c2708a1..446c81c 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -2,7 +2,7 @@ import Lake open Lake DSL -require auto from git "https://github.com/leanprover-community/lean-auto.git"@"29d65a800b84cf2abe49c918acdfef7114b911ba" +require auto from git "https://github.com/leanprover-community/lean-auto.git"@"3a973bb913c5b2db346a7e47b0b9bb6e3277e9b9" package Duper { precompileModules := true From 37ab86979e8a2f4b2b7ca5d06cf962a48b5ba1c8 Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Mon, 27 May 2024 02:14:57 -0400 Subject: [PATCH 3/3] Update to lean v4.8.0-rc2 --- Duper/Clause.lean | 12 +++++------ Duper/ClauseStreamHeap.lean | 2 +- Duper/DUnif/Bindings.lean | 10 ++++----- Duper/DUnif/Utils.lean | 3 +-- Duper/Fingerprint.lean | 2 +- Duper/MClause.lean | 34 +++++++++++++++---------------- Duper/ProofReconstruction.lean | 4 ++-- Duper/ProverM.lean | 2 +- Duper/RuleM.lean | 11 +++++++--- Duper/Rules/Demodulation.lean | 6 +++--- Duper/Rules/FluidSup.lean | 6 +++--- Duper/Rules/Superposition.lean | 12 +++++------ Duper/Saturate.lean | 2 -- Duper/TPTPParser/PrattParser.lean | 13 ++++++------ Duper/Tests/test_regression.lean | 2 +- Duper/Util/AbstractMVars.lean | 7 ++++--- Duper/Util/IdStrategyHeap.lean | 6 +++--- Duper/Util/OccursCheck.lean | 2 +- Duper/Util/StrategyHeap.lean | 4 ++-- lake-manifest.json | 18 ++++++++-------- lakefile.lean | 3 ++- lean-toolchain | 2 +- 22 files changed, 84 insertions(+), 79 deletions(-) diff --git a/Duper/Clause.lean b/Duper/Clause.lean index a2892f9..9747405 100644 --- a/Duper/Clause.lean +++ b/Duper/Clause.lean @@ -209,12 +209,12 @@ instance : ToMessageData Lit := open Comparison def compare (ord : Expr → Expr → Bool → MetaM Comparison) (alreadyReduced : Bool) (l₁ l₂ : Lit) : MetaM Comparison := do - let l₁ := - if alreadyReduced then l₁ - else ← l₁.mapM (fun e => betaEtaReduceInstMVars e) - let l₂ := - if alreadyReduced then l₂ - else ← l₂.mapM (fun e => betaEtaReduceInstMVars e) + let l₁ ← + if alreadyReduced then pure l₁ + else l₁.mapM (fun e => betaEtaReduceInstMVars e) + let l₂ ← + if alreadyReduced then pure l₂ + else l₂.mapM (fun e => betaEtaReduceInstMVars e) let cll ← ord l₁.lhs l₂.lhs true if cll == Incomparable then return Incomparable diff --git a/Duper/ClauseStreamHeap.lean b/Duper/ClauseStreamHeap.lean index a5b58c3..ab57f1c 100644 --- a/Duper/ClauseStreamHeap.lean +++ b/Duper/ClauseStreamHeap.lean @@ -1,4 +1,4 @@ -import Std.Data.BinomialHeap +import Batteries.Data.BinomialHeap import Duper.Util.IdStrategyHeap import Duper.Clause import Duper.DUnif.UnifRules diff --git a/Duper/DUnif/Bindings.lean b/Duper/DUnif/Bindings.lean index 880297b..d19cda4 100644 --- a/Duper/DUnif/Bindings.lean +++ b/Duper/DUnif/Bindings.lean @@ -58,7 +58,7 @@ def iteration (F : Expr) (p : UnifProblem) (eq : UnifEq) (funcArgOnly : Bool) : let yty ← withReader (fun ctx : Meta.Context => { ctx with lctx := lctx }) do Meta.mkFreshExprMVar (mkSort yty_ty) let fvarId ← mkFreshFVarId - lctx := lctx.mkLocalDecl fvarId s!"iter{i}.{j}" yty .default + lctx := lctx.mkLocalDecl fvarId s!"iter{i}.{j}".toName yty .default let fvar := mkFVar fvarId ys := ys.push fvar -- Make Gᵢs @@ -69,7 +69,7 @@ def iteration (F : Expr) (p : UnifProblem) (eq : UnifEq) (funcArgOnly : Bool) : -- Make H let lastExprTy ← Meta.inferType lastExpr -- Assuming that β₂ contains no loose bound variables - let Hty : Expr ← Meta.withLocalDeclD s!"iter{i}.last" lastExprTy <| fun fv => + let Hty : Expr ← Meta.withLocalDeclD s!"iter{i}.last".toName lastExprTy <| fun fv => Meta.mkForallFVars #[fv] β₁ let mH ← Meta.mkFreshExprMVar Hty let mt ← Meta.mkLambdaFVars xs (mkApp mH lastExpr) @@ -143,7 +143,7 @@ def imitForall (F : Expr) (p : UnifProblem) (eq : UnifEq) : MetaM (Array UnifPro -- BinderType let bty_ty ← Meta.mkFreshLevelMVar let bty ← Meta.mkFreshExprMVar (mkSort bty_ty) - let newt ← Meta.withLocalDeclD "imf" bty fun fv => do + let newt ← Meta.withLocalDeclD "imf".toName bty fun fv => do let newMVar ← Meta.mkFreshExprMVar β Meta.mkForallFVars #[fv] newMVar let mt ← Meta.mkLambdaFVars xs newt @@ -220,8 +220,8 @@ def imitation (F : Expr) (g : Expr) (p : UnifProblem) (eq : UnifEq) : MetaM (Arr MVarId.assign F.mvarId! mt return #[{(← p.pushParentRuleIfDbgOn (.Imitation eq F g mt)) with checked := false, mctx := ← getMCtx}] else - let βAbst := - if imitDepFn.get (← getOptions) then ← mkGeneralFnTy (h - ys.size) β else ← mkImplication (h - ys.size) β + let βAbst ← + if imitDepFn.get (← getOptions) then mkGeneralFnTy (h - ys.size) β else mkImplication (h - ys.size) β -- Put them in a block so as not to affect `βAbst` and `β` on the outside if true then let βAbst ← Meta.mkLambdaFVars xs βAbst diff --git a/Duper/DUnif/Utils.lean b/Duper/DUnif/Utils.lean index 2813b20..c35ec83 100644 --- a/Duper/DUnif/Utils.lean +++ b/Duper/DUnif/Utils.lean @@ -1,5 +1,4 @@ import Lean -import Std.Data.Array.Basic open Lean namespace DUnif @@ -73,4 +72,4 @@ def mkImplication (n : Nat) (resTy : Option Expr := .none) : MetaM Expr := do | .none => Meta.mkFreshTypeMVar) Meta.withLocalDeclsD declInfos fun xs => Meta.mkForallFVars xs resTy -end DUnif \ No newline at end of file +end DUnif diff --git a/Duper/Fingerprint.lean b/Duper/Fingerprint.lean index 0c85f50..9838178 100644 --- a/Duper/Fingerprint.lean +++ b/Duper/Fingerprint.lean @@ -144,7 +144,7 @@ def transformToUntypedFirstOrderTerm [Monad m] [MonadLiftT MetaM m] (e : Expr) : match e.getTopSymbol with | Expr.mvar mvarId => return .mvar mvarId | _ => return .app (← transformToUntypedFirstOrderTerm f) (← transformToUntypedFirstOrderTerm a) - | Expr.proj tyName idx e => return .app (.const (s!"proj_{idx}_" ++ tyName) []) (← transformToUntypedFirstOrderTerm e) + | Expr.proj tyName idx e => return .app (.const (s!"proj_{idx}_".toName ++ tyName) []) (← transformToUntypedFirstOrderTerm e) | Expr.bvar bvarNum => /- The specification of ⌊e⌋ calls for a fresh constant for each type and bvarNum, but since there isn't a diff --git a/Duper/MClause.lean b/Duper/MClause.lean index 041f201..1b6f568 100644 --- a/Duper/MClause.lean +++ b/Duper/MClause.lean @@ -63,7 +63,7 @@ def fold {β : Type v} (f : β → Expr → β) (init : β) (c : MClause) : β : acc := c.lits[i]!.fold f' acc return acc -def foldM {β : Type v} {m : Type v → Type w} [Monad m] +def foldM {β : Type v} {m : Type v → Type w} [Monad m] (f : β → Expr → ClausePos → m β) (init : β) (c : MClause) : m β := do let mut acc := init for i in [:c.lits.size] do @@ -126,9 +126,9 @@ open Comparison /-- Returns the list of minimal literal indices that satisfy the provided filter_fn -/ def getMinimalLits (ord : Expr → Expr → Bool → MetaM Comparison) (alreadyReduced : Bool) (c : MClause) (filter_fn : Lit → Bool) : MetaM (Array Nat) := do - let c := - if alreadyReduced then c - else ← c.mapM (fun e => betaEtaReduceInstMVars e) + let c ← + if alreadyReduced then pure c + else c.mapM (fun e => betaEtaReduceInstMVars e) let mut minLits : Array Nat := #[] for i in [:c.lits.size] do let curLit := c.lits[i]! @@ -145,9 +145,9 @@ def getMinimalLits (ord : Expr → Expr → Bool → MetaM Comparison) (alreadyR /-- Returns the list of maximal literal indices that satisfy the provided filter_fn -/ def getMaximalLits (ord : Expr → Expr → Bool → MetaM Comparison) (alreadyReduced : Bool) (c : MClause) (filter_fn : Lit → Bool) : MetaM (Array Nat) := do - let c := - if alreadyReduced then c - else ← c.mapM (fun e => betaEtaReduceInstMVars e) + let c ← + if alreadyReduced then pure c + else c.mapM (fun e => betaEtaReduceInstMVars e) let mut maxLits : Array Nat := #[] for i in [:c.lits.size] do let curLit := c.lits[i]! @@ -166,9 +166,9 @@ def getMaximalLits (ord : Expr → Expr → Bool → MetaM Comparison) (alreadyR selection functions. -/ def getMaxDiffLits (getNetWeight : Expr → Expr → Bool → MetaM Order.Weight) (alreadyReduced : Bool) (c : MClause) (filter_fn : Lit → Nat → Bool) : MetaM (Array Nat) := do - let c := - if alreadyReduced then c - else ← c.mapM (fun e => betaEtaReduceInstMVars e) + let c ← + if alreadyReduced then pure c + else c.mapM (fun e => betaEtaReduceInstMVars e) let mut maxDiffLits : Array Nat := #[] let mut maxDiff : Order.Weight := 0 for i in [:c.lits.size] do @@ -190,9 +190,9 @@ def getMaxDiffLits (getNetWeight : Expr → Expr → Bool → MetaM Order.Weight /-- Determines whether c.lits[idx]! is maximal in c. If strict is set to true, then there can be no idx' such that c.lits[idx]! and c.lits[idx']! are evaluated as equal by the comparison function -/ def isMaximalLit (ord : Expr → Expr → Bool → MetaM Comparison) (alreadyReduced : Bool) (c : MClause) (idx : Nat) (strict := false) : MetaM Bool := do - let c := - if alreadyReduced then c - else ← c.mapM (fun e => betaEtaReduceInstMVars e) + let c ← + if alreadyReduced then pure c + else c.mapM (fun e => betaEtaReduceInstMVars e) for j in [:c.lits.size] do if j == idx then continue let cmp ← Lit.compare ord true c.lits[idx]! c.lits[j]! @@ -207,9 +207,9 @@ def isMaximalLit (ord : Expr → Expr → Bool → MetaM Comparison) (alreadyRed Note that for this function, strictness does not actually matter, because regardless of whether we are considering potential strict maximality or potential nonstrict maximality, we can only determine that idx can never be maximal if we find an idx' that is strictly gerater than it -/ def canNeverBeMaximal (ord : Expr → Expr → Bool → MetaM Comparison) (alreadyReduced : Bool) (c : MClause) (idx : Nat) : MetaM Bool := do - let c := - if alreadyReduced then c - else ← c.mapM (fun e => betaEtaReduceInstMVars e) + let c ← + if alreadyReduced then pure c + else c.mapM (fun e => betaEtaReduceInstMVars e) for j in [:c.lits.size] do if j != idx && (← Lit.compare ord true c.lits[idx]! c.lits[j]!) == LessThan then return true @@ -217,4 +217,4 @@ def canNeverBeMaximal (ord : Expr → Expr → Bool → MetaM Comparison) (alrea return false end MClause -end Duper \ No newline at end of file +end Duper diff --git a/Duper/ProofReconstruction.lean b/Duper/ProofReconstruction.lean index b59500e..5a9ee0f 100644 --- a/Duper/ProofReconstruction.lean +++ b/Duper/ProofReconstruction.lean @@ -35,7 +35,7 @@ partial def printProof (state : ProverM.State) : MetaM Unit := do trace[duper.printProof] "Clause #{info.number} (by {info.proof.ruleName} {parentIds}): {c}" -- println! s!"Clause #{info.number} (by {info.proof.ruleName} {parentIds}): {toString (← ppExpr c.toForallExpr)}" -abbrev ClauseHeap := Std.BinomialHeap (Nat × Clause) fun c d => c.1 ≤ d.1 +abbrev ClauseHeap := Batteries.BinomialHeap (Nat × Clause) fun c d => c.1 ≤ d.1 partial def collectClauses (state : ProverM.State) (c : Clause) (acc : (Array Nat × ClauseHeap)) : MetaM (Array Nat × ClauseHeap) := do Core.checkMaxHeartbeats "collectClauses" @@ -241,7 +241,7 @@ partial def mkAllProof (state : ProverM.State) (cs : List Clause) : MetaM Expr : def reconstructProof (state : ProverM.State) : MetaM Expr := do let some emptyClause := state.emptyClause | throwError "applyProof :: Can't find empty clause in ProverM's state" - let l := (← collectClauses state emptyClause (#[], Std.BinomialHeap.empty)).2.toList.eraseDups.map Prod.snd + let l := (← collectClauses state emptyClause (#[], Batteries.BinomialHeap.empty)).2.toList.eraseDups.map Prod.snd trace[duper.proofReconstruction] "Collected clauses: {l}" -- First make proof for skolems, then make proof for clauses let proof ← mkAllProof state l diff --git a/Duper/ProverM.lean b/Duper/ProverM.lean index 27f7ea9..574ea0a 100644 --- a/Duper/ProverM.lean +++ b/Duper/ProverM.lean @@ -1,5 +1,5 @@ import Duper.Clause -import Std.Data.BinomialHeap +import Batteries.Data.BinomialHeap import Duper.Fingerprint import Duper.Selection import Duper.SubsumptionTrie diff --git a/Duper/RuleM.lean b/Duper/RuleM.lean index f616d35..90be31e 100644 --- a/Duper/RuleM.lean +++ b/Duper/RuleM.lean @@ -379,12 +379,17 @@ def neutralizeMClauseInhabitedReasoningOn (c : MClause) (loadedClauses : Array L def yieldClause (mc : MClause) (ruleName : String) (mkProof : Option ProofReconstructor) (transferExprs : Array Expr := #[]) (mvarIdsToRemove : List MVarId := []) : RuleM (Clause × Proof) := do -- Refer to `Lean.Meta.abstractMVars` + let loadedClauses ← getLoadedClauses + let inhabitationClauses ← getInhabitationClauses + let mctx ← getMCtx + let lctx ← getLCtx + let ngen ← getNGen let ((c, proofParents, transferExprs), st) := if ← getInhabitationReasoningM then - neutralizeMClauseInhabitedReasoningOn mc (← getLoadedClauses) (← getInhabitationClauses) transferExprs mvarIdsToRemove - { mctx := (← getMCtx), lctx := (← getLCtx), ngen := (← getNGen) } + neutralizeMClauseInhabitedReasoningOn mc loadedClauses inhabitationClauses transferExprs mvarIdsToRemove + { mctx := mctx, lctx := lctx, ngen := ngen } else - neutralizeMClause mc (← getLoadedClauses) transferExprs { mctx := (← getMCtx), lctx := (← getLCtx), ngen := (← getNGen) } + neutralizeMClause mc loadedClauses transferExprs { mctx := mctx, lctx := lctx, ngen := ngen } setNGen st.ngen -- This is redundant because the `mctx` won't change -- We should not reset `lctx` because fvars introduced by diff --git a/Duper/Rules/Demodulation.lean b/Duper/Rules/Demodulation.lean index 232b494..e7600fb 100644 --- a/Duper/Rules/Demodulation.lean +++ b/Duper/Rules/Demodulation.lean @@ -27,9 +27,9 @@ def mkDemodulationProof (sidePremiseLhs : LitSide) (mainPremisePos : ClausePos) let proof ← Meta.withLocalDeclD `heq eqLit.toExpr fun heq => do let mut caseProofs : Array Expr := Array.mkEmpty mainParentLits.size - let eq := - if sidePremiseLhs == LitSide.rhs then ← Meta.mkAppM ``Eq.symm #[heq] - else heq + let eq ← + if sidePremiseLhs == LitSide.rhs then Meta.mkAppM ``Eq.symm #[heq] + else pure heq for i in [:mainParentLits.size] do let lit := mainParentLits[i]! let pr : Expr ← Meta.withLocalDeclD `h lit.toExpr fun h => do diff --git a/Duper/Rules/FluidSup.lean b/Duper/Rules/FluidSup.lean index ad2440b..b98e57c 100644 --- a/Duper/Rules/FluidSup.lean +++ b/Duper/Rules/FluidSup.lean @@ -29,9 +29,9 @@ def mkFluidSupProof (sidePremiseLitIdx : Nat) (sidePremiseLitSide : LitSide) (ma if j == sidePremiseLitIdx then let eqLit := sideParentLits[j]! let pr ← Meta.withLocalDeclD `heq eqLit.toExpr fun heq => do - let eq := - if sidePremiseLitSide == LitSide.rhs then ← Meta.mkAppM ``Eq.symm #[heq] - else heq + let eq ← + if sidePremiseLitSide == LitSide.rhs then Meta.mkAppM ``Eq.symm #[heq] + else pure heq let eq ← mkAppM ``congrArg #[freshFunctionVar, eq] let mut caseProofsMain : Array Expr := Array.mkEmpty mainParentLits.size for i in [:mainParentLits.size] do diff --git a/Duper/Rules/Superposition.lean b/Duper/Rules/Superposition.lean index 8b68a5e..2ca0719 100644 --- a/Duper/Rules/Superposition.lean +++ b/Duper/Rules/Superposition.lean @@ -76,9 +76,9 @@ def mkSuperpositionProof (sidePremiseLitIdx : Nat) (sidePremiseLitSide : LitSide if j == sidePremiseLitIdx then let eqLit := sideParentLits[j]! let pr ← Meta.withLocalDeclD `heq eqLit.toExpr fun heq => do - let eq := - if sidePremiseLitSide == LitSide.rhs then ← Meta.mkAppM ``Eq.symm #[heq] - else heq + let eq ← + if sidePremiseLitSide == LitSide.rhs then Meta.mkAppM ``Eq.symm #[heq] + else pure heq let mut caseProofsMain : Array Expr := Array.mkEmpty mainParentLits.size for i in [:mainParentLits.size] do let lit := mainParentLits[i]! @@ -130,9 +130,9 @@ def mkSimultaneousSuperpositionProof (sidePremiseLitIdx : Nat) (sidePremiseLitSi if j == sidePremiseLitIdx then let eqLit := sideParentLits[j]! let pr ← Meta.withLocalDeclD `heq eqLit.toExpr fun heq => do - let eq := - if sidePremiseLitSide == LitSide.rhs then ← Meta.mkAppM ``Eq.symm #[heq] - else heq + let eq ← + if sidePremiseLitSide == LitSide.rhs then Meta.mkAppM ``Eq.symm #[heq] + else pure heq let mut caseProofsMain : Array Expr := Array.mkEmpty mainParentLits.size for i in [:mainParentLits.size] do let lit := mainParentLits[i]! diff --git a/Duper/Saturate.lean b/Duper/Saturate.lean index 27818da..790b505 100644 --- a/Duper/Saturate.lean +++ b/Duper/Saturate.lean @@ -1,4 +1,3 @@ -import Std.Data.BinomialHeap import Duper.ClauseStreamHeap import Duper.RuleM import Duper.MClause @@ -41,7 +40,6 @@ open Lean open Meta open Lean.Core open Result -open Std open ProverM open RuleM diff --git a/Duper/TPTPParser/PrattParser.lean b/Duper/TPTPParser/PrattParser.lean index 33397ba..5a8ae01 100644 --- a/Duper/TPTPParser/PrattParser.lean +++ b/Duper/TPTPParser/PrattParser.lean @@ -350,7 +350,7 @@ partial def toLeanExpr (t : Parser.Term) : MetaM Expr := do | ⟨.ident "$true", []⟩ => return mkConst `True | ⟨.ident "$false", []⟩ => return mkConst `False | ⟨.ident n, as⟩ => do - let some decl := (← getLCtx).findFromUserName? n + let some decl := (← getLCtx).findFromUserName? n.toName | throwError "Unknown variable name {n}" return mkAppN (mkFVar decl.fvarId) (← as.mapM toLeanExpr).toArray | ⟨.op "!", body :: var :: tail⟩ => @@ -413,7 +413,7 @@ where | [ty] => ty.toLeanExpr | [] => pure $ mkConst `Iota | _ => throwError "invalid bound var: {repr var}" - withLocalDeclD v ty k + withLocalDeclD v.toName ty k | _ => throwError "invalid bound var: {repr var}" end Term @@ -473,13 +473,14 @@ def compileCmds (cmds : List Parser.Command) (acc : Formulas) (k : Formulas → | "thf" | "tff" | "cnf" | "fof" => match args with | [_, ⟨.ident "type", _⟩, ⟨.ident id, [ty]⟩] => - withLocalDeclD id (← ty.toLeanExpr) fun _ => do + withLocalDeclD id.toName (← ty.toLeanExpr) fun _ => do compileCmds cs acc k | [⟨.ident name, []⟩, ⟨.ident kind, _⟩, val] => let val ← val.toLeanExpr - let val := if kind == "conjecture" then ← mkAppM ``Not #[val] else val + let notVal ← mkAppM ``Not #[val] + let val := if kind == "conjecture" then notVal else val let isFromGoal := kind == "conjecture" - withLocalDeclD ("H_" ++ name) val fun x => do + withLocalDeclD ("H_".toName ++ name.toName) val fun x => do let acc := acc.push (val, ← mkAppM ``eq_true #[x], #[], isFromGoal) compileCmds cs acc k | _ => throwError "Unknown declaration kind: {args.map repr}" @@ -531,7 +532,7 @@ def compile [Inhabited α] (code : String) (dir : System.FilePath) (k : Formulas let cmds ← Parser.parse code let cmds ← resolveIncludes cmds dir let constants ← collectCnfFofConstants cmds - withLocalDeclsD (constants.toArray.map fun (n, ty) => (n, fun _ => pure ty)) fun _ => do + withLocalDeclsD (constants.toArray.map fun (n, ty) => (n.toName, fun _ => pure ty)) fun _ => do compileCmds cmds #[] k def compileFile [Inhabited α] (path : String) (k : Formulas → MetaM α) : MetaM α := do diff --git a/Duper/Tests/test_regression.lean b/Duper/Tests/test_regression.lean index 53d99d6..c06d789 100644 --- a/Duper/Tests/test_regression.lean +++ b/Duper/Tests/test_regression.lean @@ -539,7 +539,7 @@ end NegativeBoolSimpTests /- ClauseStreamHeap tests -/ tptp MGT008 "../TPTP-v8.0.0/Problems/MGT/MGT008+1.p" - by duper [*] {portfolioInstance := 5} -- Runs out of time if run in portfolio mode + by duper [*] example (f : Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat) (g : Nat → Nat → Nat → Nat → Nat → Nat) diff --git a/Duper/Util/AbstractMVars.lean b/Duper/Util/AbstractMVars.lean index 849a57d..2b0d4d4 100644 --- a/Duper/Util/AbstractMVars.lean +++ b/Duper/Util/AbstractMVars.lean @@ -99,8 +99,9 @@ partial def abstractExprMVars (e : Expr) : M Expr := do | none => let type ← abstractExprMVars decl.type let fvarId ← mkFreshFVarId - let fvar := mkFVar fvarId; - let userName := if decl.userName.isAnonymous then (`x).appendIndexAfter (← get).fvars.size else decl.userName + let fvar := mkFVar fvarId + let fvarsSize := (← get).fvars.size + let userName := if decl.userName.isAnonymous then (`x).appendIndexAfter fvarsSize else decl.userName modify fun s => { s with emap := s.emap.insert mvarId fvar, @@ -180,4 +181,4 @@ def abstractMVarsLambda (e : Expr) : MetaM AbstractMVarsResult := do setNGen s.ngen setMCtx s.mctx let e := s.lctx.mkLambda s.fvars e - pure { paramNames := s.paramNames, numMVars := s.fvars.size, expr := e } \ No newline at end of file + pure { paramNames := s.paramNames, numMVars := s.fvars.size, expr := e } diff --git a/Duper/Util/IdStrategyHeap.lean b/Duper/Util/IdStrategyHeap.lean index a10919e..cbb730d 100644 --- a/Duper/Util/IdStrategyHeap.lean +++ b/Duper/Util/IdStrategyHeap.lean @@ -1,8 +1,8 @@ -import Std.Data.BinomialHeap +import Batteries.Data.BinomialHeap import Lean open Lean -open Std +open Batteries namespace Duper @@ -136,4 +136,4 @@ abbrev ClauseStreamHeap.empty σ : ClauseStreamHeap σ := break panic! s!"ClauseStreamHeap.deleteMinWithNProbed :: Map of size {oh.map.size} is not empty, but deletion failed" else - panic! s!"ClauseStreamHeap.deleteMinWithNProbed :: The id of selected heap >= number of heaps" \ No newline at end of file + panic! s!"ClauseStreamHeap.deleteMinWithNProbed :: The id of selected heap >= number of heaps" diff --git a/Duper/Util/OccursCheck.lean b/Duper/Util/OccursCheck.lean index 489174c..2bbbe90 100644 --- a/Duper/Util/OccursCheck.lean +++ b/Duper/Util/OccursCheck.lean @@ -20,7 +20,7 @@ partial def mustNotOccursCheck (mvarId : MVarId) (e : Expr) : MetaM Bool := do where visitMVar (mvarId' : MVarId) : ExceptT Unit (StateT ExprSet MetaM) Unit := do if mvarId == mvarId' then - throw (self:=instMonadExcept _ _) () -- found + throw (self:=instMonadExceptOfMonadExceptOf _ _) () -- found else let mvarTy' ← Meta.inferType (mkMVar mvarId') -- Modification : We also need to check whether metavariables diff --git a/Duper/Util/StrategyHeap.lean b/Duper/Util/StrategyHeap.lean index ce8f7e0..703e889 100644 --- a/Duper/Util/StrategyHeap.lean +++ b/Duper/Util/StrategyHeap.lean @@ -1,8 +1,8 @@ -import Std.Data.BinomialHeap +import Batteries.Data.BinomialHeap import Lean open Lean -open Std +open Batteries namespace Duper diff --git a/lake-manifest.json b/lake-manifest.json index a39fcb8..31d5b02 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,22 +1,22 @@ {"version": 7, "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover/std4.git", + [{"url": "https://github.com/leanprover-community/lean-auto.git", "type": "git", "subDir": null, - "rev": "6b203c31b414beb758ef9b7fdc71b01d144504ad", - "name": "std", + "rev": "91cd0e81ec8bd16baa2c08e3d00a7f8e473477b4", + "name": "auto", "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, + "inputRev": "91cd0e81ec8bd16baa2c08e3d00a7f8e473477b4", + "inherited": false, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/lean-auto.git", + {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, - "rev": "3a973bb913c5b2db346a7e47b0b9bb6e3277e9b9", - "name": "auto", + "rev": "7b3c48b58fa0ae1c8f27889bdb086ea5e4b27b06", + "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "3a973bb913c5b2db346a7e47b0b9bb6e3277e9b9", + "inputRev": "v4.8.0-rc2", "inherited": false, "configFile": "lakefile.lean"}], "name": "Duper", diff --git a/lakefile.lean b/lakefile.lean index 446c81c..51bbe9e 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -2,7 +2,8 @@ import Lake open Lake DSL -require auto from git "https://github.com/leanprover-community/lean-auto.git"@"3a973bb913c5b2db346a7e47b0b9bb6e3277e9b9" +require auto from git "https://github.com/leanprover-community/lean-auto.git"@"91cd0e81ec8bd16baa2c08e3d00a7f8e473477b4" +require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.8.0-rc2" package Duper { precompileModules := true diff --git a/lean-toolchain b/lean-toolchain index e35881c..78f39e2 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.7.0-rc2 +leanprover/lean4:v4.8.0-rc2