Merge pull request #13 from leanprover-community/dev

Dev

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

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

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

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
+end DUnif

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

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,14 +207,14 @@ 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
     else continue
   return false
 
 end MClause
-end Duper
+end Duper

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

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

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

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

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

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]!

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
 

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

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)

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 }
+  pure { paramNames := s.paramNames, numMVars := s.fvars.size, expr := e }

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"
+    panic! s!"ClauseStreamHeap.deleteMinWithNProbed :: The id of selected heap >= number of heaps"

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

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