diff --git a/Duper/DUnif/Bindings.lean b/Duper/DUnif/Bindings.lean index d19cda4..47ca814 100644 --- a/Duper/DUnif/Bindings.lean +++ b/Duper/DUnif/Bindings.lean @@ -55,14 +55,14 @@ def iteration (F : Expr) (p : UnifProblem) (eq : UnifEq) (funcArgOnly : Bool) : let mut lctx ← getLCtx for j in List.range i do let yty_ty ← Meta.mkFreshLevelMVar - let yty ← withReader (fun ctx : Meta.Context => { ctx with lctx := lctx }) do + let yty ← Meta.withLCtx' lctx do Meta.mkFreshExprMVar (mkSort yty_ty) let fvarId ← mkFreshFVarId lctx := lctx.mkLocalDecl fvarId s!"iter{i}.{j}".toName yty .default let fvar := mkFVar fvarId ys := ys.push fvar -- Make Gᵢs - let lastExpr ← withReader (fun ctx : Meta.Context => { ctx with lctx := lctx }) do + let lastExpr ← Meta.withLCtx' lctx do let (xys, _, _) ← Meta.forallMetaTelescopeReducing αi let body := mkAppN xi xys Meta.mkLambdaFVars ys body diff --git a/Duper/MClause.lean b/Duper/MClause.lean index bc93bd7..f7d2b42 100644 --- a/Duper/MClause.lean +++ b/Duper/MClause.lean @@ -27,7 +27,7 @@ def appendLits (c : MClause) (lits : Array Lit) : MClause := ⟨c.lits.append lits⟩ def eraseLit (c : MClause) (idx : Nat) : MClause := - ⟨c.lits.eraseIdx idx⟩ + ⟨c.lits.eraseIdxIfInBounds idx⟩ def replaceLit? (c : MClause) (idx : Nat) (l : Lit) : Option MClause := if idx >= c.lits.size then @@ -45,7 +45,7 @@ def mapWithPos (f : Expr → Expr × Array ExprPos) (c : MClause) : MClause × A let mapres := c.lits.map (fun l => l.mapWithPos f) let c' := ⟨mapres.map (fun x => x.fst)⟩ let cps := mapres.mapIdx (fun i x => x.snd.map (fun pos => {pos with lit := i})) - (c', cps.concatMap id) + (c', cps.flatMap id) def mapMWithPos [Monad m] [MonadLiftT MetaM m] (f : Expr → m (Expr × Array ExprPos)) (c : MClause) : m (MClause × Array ClausePos) := do let mapres ← c.lits.mapM (fun l => l.mapMWithPos f) @@ -112,7 +112,7 @@ def abstractAtPos! (c : MClause) (pos : ClausePos) : MetaM MClause := do def append (c : MClause) (d : MClause) : MClause := ⟨c.lits.append d.lits⟩ -def eraseIdx (i : Nat) (c : MClause) : MClause := ⟨c.lits.eraseIdx i⟩ +def eraseIdx (i : Nat) (c : MClause) : MClause := ⟨c.lits.eraseIdxIfInBounds i⟩ def isTrivial (c : MClause) : Bool := Id.run do -- TODO: Also check if it contains the same literal positively and negatively? diff --git a/Duper/Rules/Clausification.lean b/Duper/Rules/Clausification.lean index a95a503..c34f4d5 100644 --- a/Duper/Rules/Clausification.lean +++ b/Duper/Rules/Clausification.lean @@ -458,7 +458,7 @@ def clausificationStep : MSimpRule := fun c => do let r ← orCases (parentLits.map Lit.toExpr) caseProofs let r ← Meta.mkLambdaFVars xs $ mkApp r appliedPremise return r - let newClause := ⟨c.lits.eraseIdx i ++ d⟩ + let newClause := ⟨c.lits.eraseIdxIfInBounds i ++ d⟩ trace[duper.rule.clausification] "Yielding newClause: {newClause.lits}" let newResult ← yieldClause newClause "clausification" mkProof tr resultClauses := resultClauses.push newResult diff --git a/Duper/Util/Misc.lean b/Duper/Util/Misc.lean index 4134ddb..e76211c 100644 --- a/Duper/Util/Misc.lean +++ b/Duper/Util/Misc.lean @@ -11,7 +11,7 @@ def List.subsequences (xs : List α) := -- replace `whnf e` with `e`. private partial def instantiateForallAux (ps : Array Expr) (i : Nat) (e : Expr) : MetaM Expr := do if h : i < ps.size then - let p := ps.get ⟨i, h⟩ + let p := ps.get i h match e with | Expr.forallE _ _ b _ => instantiateForallAux ps (i+1) (b.instantiate1 p) | _ => throwError "invalid instantiateForallNoReducing, too many parameters" @@ -20,7 +20,7 @@ private partial def instantiateForallAux (ps : Array Expr) (i : Nat) (e : Expr) private partial def instantiateForallAuxNoError (ps : Array Expr) (i : Nat) (e : Expr) : Expr := if h : i < ps.size then - let p := ps.get ⟨i, h⟩ + let p := ps.get i h match e with | Expr.forallE _ _ b _ => instantiateForallAuxNoError ps (i+1) (b.instantiate1 p) | _ => panic! "Called instantiateForallAuxNoError with too many parameters" @@ -185,7 +185,7 @@ partial def getArity (e : Expr) : Nat := `Meta.kabstract` invokes definitional equality, there were some instances in which `Meta.kabstract` performed an abstraction at a position where `RuleM.replace` would not perform a replacement. This was an issue because it created inconsistencies between the clauses produced by superposition's main code and proof reconstruction. - + `abstractAtExpr` is written to follow the implementation of `Meta.kabstract` without invoking definitional equality (instead testing for equality after instantiating metavariables). -/ def Lean.Meta.abstractAtExpr (e : Expr) (p : Expr) (occs : Occurrences := .all) : MetaM Expr := do @@ -219,4 +219,4 @@ def Lean.Meta.abstractAtExpr (e : Expr) (p : Expr) (occs : Occurrences := .all) visitChildren () else visitChildren () - visit e 0 |>.run' 1 \ No newline at end of file + visit e 0 |>.run' 1 diff --git a/lake-manifest.json b/lake-manifest.json index 5e397fe..d22d856 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,20 +5,20 @@ "type": "git", "subDir": null, "scope": "", - "rev": "8d6c853f11a5172efa0e96b9f2be1a83d861cdd9", + "rev": "e8dc5fc16c625fc4fe08f42d625523275ddbbb4b", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.14.0", + "inputRev": "v4.15.0", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/lean-auto.git", "type": "git", "subDir": null, "scope": "", - "rev": "4d73b99262f1ce80a33ac832bef26549cf3c2034", + "rev": "997d810f10945740fb68923fbfa0cdf84636d07c", "name": "auto", "manifestFile": "lake-manifest.json", - "inputRev": "4d73b99262f1ce80a33ac832bef26549cf3c2034", + "inputRev": "997d810f10945740fb68923fbfa0cdf84636d07c", "inherited": false, "configFile": "lakefile.lean"}], "name": "Duper", diff --git a/lakefile.lean b/lakefile.lean index 93fcd38..2dae6ff 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"@"4d73b99262f1ce80a33ac832bef26549cf3c2034" -require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.14.0" +require auto from git "https://github.com/leanprover-community/lean-auto.git"@"997d810f10945740fb68923fbfa0cdf84636d07c" +require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.15.0" package Duper { precompileModules := true diff --git a/lean-toolchain b/lean-toolchain index 1e70935..d0eb99f 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.14.0 +leanprover/lean4:v4.15.0