diff --git a/Duper/ClauseStreamHeap.lean b/Duper/ClauseStreamHeap.lean index ab57f1c..ebb0425 100644 --- a/Duper/ClauseStreamHeap.lean +++ b/Duper/ClauseStreamHeap.lean @@ -138,9 +138,9 @@ def ProverM.postProcessInferenceResult (cp : ClauseProof) : ProverM Unit := do let allClauses ← getAllClauses let parentClauseInfoOpts ← proof.parents.mapM (fun p => - match allClauses.find? p.clause with + match allClauses.get? p.clause with | some pi => pure pi - | none => throwError "ProverM.postProcessInferenceResult: Unable to find parent clause {p.clause}") + | none => throwError "ProverM.postProcessInferenceResult: Unable to find parent clause {p.clause.toForallExpr}") -- c's generation number is one greater than the sum of its parents generation numbers let generationNumber := parentClauseInfoOpts.foldl (fun acc parentInfo => acc + parentInfo.generationNumber) 1 -- c's goalDistance is at most maxGoalDistance and is otherwise one greater than the distance of the parent closest to the goal diff --git a/Duper/ProverM.lean b/Duper/ProverM.lean index 9f98598..a2e5096 100644 --- a/Duper/ProverM.lean +++ b/Duper/ProverM.lean @@ -98,9 +98,6 @@ instance : AddMessageContext ProverM where @[inline] def ProverM.run' (x : ProverM α) (ctx : Context := {}) (s : State := {}) : MetaM α := Prod.fst <$> x.run ctx s -instance [MetaEval α] : MetaEval (ProverM α) := - ⟨fun env opts x _ => MetaEval.eval env opts x.run' true⟩ - initialize registerTraceClass `duper.prover.saturate registerTraceClass `duper.createdClauses diff --git a/Duper/Selection.lean b/Duper/Selection.lean index f9e0363..69c0b99 100644 --- a/Duper/Selection.lean +++ b/Duper/Selection.lean @@ -131,7 +131,7 @@ def selectMaxLitComplex (c : MClause) (alreadyReduced : Bool) : RuleM (List Nat) selectMaxLitComplex but uses the number of positive literals with a shared predicate symbol as a tiebreaker (preferring to select literals that share a predicate symbol with as few positive literals as possible). For this, specification, I am defining a predicate symbol as the top symbol for the lhs of a literal of the form `e = True` or `e = False`. - + Note: According to "Extending a Brainiac Prover to Lambda-Free Higher-Order Logic", SelectMaxLComplexAvoidPosPred (aka SelectMLCAPP) should be have very similarly to E's SelectMLCAPPPreferAppVar and SelectMLCAPPAvoidAppVar. So it should be unnecessary to separately implement those two selection functions. -/ @@ -204,7 +204,7 @@ def selectMaxLitComplexAvoidPosPred (c : MClause) (alreadyReduced : Bool) : Rule literal of the form `e = True` or `e = False`). If there are multiple negative literals with the same largest predicate, then the size difference between the lit's lhs and rhs will be the tiebreaker (with larger size differences being preferred). -/ def selectCQIPrecWNTNp (c : MClause) (alreadyReduced : Bool) : RuleM (List Nat) := do - let idxLitPairs := c.lits.mapIdx (fun idx l => (idx.1, l)) + let idxLitPairs := c.lits.mapIdx (fun idx l => (idx, l)) let idxPredPairs := idxLitPairs.filterMap (fun (idx, l) => -- Since we only select negative literals, and since we need a predicate, the only form we allow `l` to have is `e = False` @@ -217,10 +217,10 @@ def selectCQIPrecWNTNp (c : MClause) (alreadyReduced : Bool) : RuleM (List Nat) ) let symbolPrecMap ← getSymbolPrecMap -- Recall that low values in symbolPrecMap correspond to high precedence let idxPredPairsSorted := idxPredPairs.qsort -- Sorting so that highest precedence symbols will be first in idxPredPairsSorted - (fun (idx1, pred1Opt) (idx2, pred2Opt) => + (fun (_idx1, pred1Opt) (_idx2, pred2Opt) => match pred1Opt, pred2Opt with | some pred1, some pred2 => - match symbolPrecMap.find? pred1, symbolPrecMap.find? pred2 with + match symbolPrecMap.get? pred1, symbolPrecMap.get? pred2 with | none, _ => false -- Never sort symbol not found in symbolPrecMap before anything else | some _, none => true -- Symbols found in symbolPrecMap are sorted before symbols found in symbolPrecMap | some prec1, some prec2 => prec1 < prec2 -- Low values in symbolPrecMap correspond to higher precedence @@ -287,12 +287,12 @@ def litSelected (c : MClause) (i : Nat) (alreadyReduced : Bool) : RuleM Bool := return sel.contains i /-- Data type to capture whether a literal in a clause is eligible. -If it is not eligible, we distinguish the cases where there might +If it is not eligible, we distinguish the cases where there might be substitutions that make the literal eligble (`potentiallyEligible`) or not (`notEligible`).-/ -inductive Eligibility - | eligible - | potentiallyEligible +inductive Eligibility + | eligible + | potentiallyEligible | notEligible deriving Inhabited, BEq, Repr, Hashable @@ -343,4 +343,4 @@ def eligibilityPostUnificationCheck (c : MClause) (alreadyReduced := false) (i : else if preUnificationResult == Eligibility.notEligible then return false else c.isMaximalLit (← getOrder) alreadyReduced i (strict := strict) -end Duper \ No newline at end of file +end Duper diff --git a/Duper/Tactic.lean b/Duper/Tactic.lean index e027463..bff210f 100644 --- a/Duper/Tactic.lean +++ b/Duper/Tactic.lean @@ -39,8 +39,8 @@ def getIgnoreUnusableFactsM : CoreM Bool := do for each constructor, a proof of the equation, and the contained level parameters. -/ def addRecAsFact (recVal : RecursorVal): TacticM (List (Expr × Expr × Array Name)) := do - let some (.inductInfo indVal) := (← getEnv).find? recVal.getInduct - | throwError "Expected inductive datatype: {recVal.getInduct}" + let some (.inductInfo indVal) := (← getEnv).find? recVal.getMajorInduct + | throwError "Expected inductive datatype: {recVal.getMajorInduct}" let expr := mkConst recVal.name (recVal.levelParams.map Level.param) let res ← forallBoundedTelescope (← inferType expr) recVal.getMajorIdx fun xs _ => do let expr := mkAppN expr xs diff --git a/lake-manifest.json b/lake-manifest.json index 11a2fd9..5e397fe 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,25 +1,25 @@ {"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover-community/lean-auto.git", + [{"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "", - "rev": "915802517242f70b284fbcd5eac55bdaae29535e", - "name": "auto", + "rev": "8d6c853f11a5172efa0e96b9f2be1a83d861cdd9", + "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "915802517242f70b284fbcd5eac55bdaae29535e", + "inputRev": "v4.14.0", "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/batteries", + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/lean-auto.git", "type": "git", "subDir": null, "scope": "", - "rev": "31a10a332858d6981dbcf55d54ee51680dd75f18", - "name": "batteries", + "rev": "4d73b99262f1ce80a33ac832bef26549cf3c2034", + "name": "auto", "manifestFile": "lake-manifest.json", - "inputRev": "v4.13.0", + "inputRev": "4d73b99262f1ce80a33ac832bef26549cf3c2034", "inherited": false, - "configFile": "lakefile.toml"}], + "configFile": "lakefile.lean"}], "name": "Duper", "lakeDir": ".lake"} diff --git a/lakefile.lean b/lakefile.lean index 98d1a82..93fcd38 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -2,8 +2,8 @@ import Lake open Lake DSL -require auto from git "https://github.com/leanprover-community/lean-auto.git"@"915802517242f70b284fbcd5eac55bdaae29535e" -require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.13.0" +require auto from git "https://github.com/leanprover-community/lean-auto.git"@"4d73b99262f1ce80a33ac832bef26549cf3c2034" +require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.14.0" package Duper { precompileModules := true diff --git a/lean-toolchain b/lean-toolchain index 4f86f95..1e70935 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.13.0 +leanprover/lean4:v4.14.0