Merge pull request #33 from leanprover-community/dev

Dev

Duper/Clause.lean

@@ -68,7 +68,7 @@ def map (f : Expr → Expr) (l : Lit) :=
   {l with ty := f l.ty, lhs := f l.lhs, rhs := f l.rhs}
 
 def instantiateLevelParamsArray (l : Lit) (paramNames : Array Name) (levels : Array Level) :=
-  {l with lvl := l.lvl.instantiateParams paramNames.data levels.data
+  {l with lvl := l.lvl.instantiateParams paramNames.toList levels.toList
           ty := l.ty.instantiateLevelParamsArray paramNames levels
           lhs := l.lhs.instantiateLevelParamsArray paramNames levels
           rhs := l.rhs.instantiateLevelParamsArray paramNames levels}
@@ -294,7 +294,7 @@ def litsToExpr : List Lit → Expr
 | l :: ls => mkApp2 (mkConst ``Or) l.toExpr (litsToExpr ls)
 
 def toExpr (c : Clause) : Expr :=
-  litsToExpr c.lits.data
+  litsToExpr c.lits.toList
 
 def foldM {β : Type v} {m : Type v → Type w} [Monad m]
     (f : β → Expr → ClausePos → m β) (init : β) (c : Clause) : m β := do

Duper/Expr.lean

@@ -180,11 +180,11 @@ private partial def replaceAtPosHelper [Monad m] [MonadLiftT MetaM m] (e : Expr)
 
 /-- Attempts to put replacement at pos in e. Returns some res if successful, and returns none otherwise -/
 partial def replaceAtPos? [Monad m] [MonadLiftT MetaM m] (e : Expr) (pos : ExprPos) (replacement : Expr) : m (Option Expr) :=
-  replaceAtPosHelper e pos.data replacement
+  replaceAtPosHelper e pos.toList replacement
 
 /-- Attempts to put replacement at pos in e. Returns the result if successful and throws and error otherwise -/
 partial def replaceAtPos! [Monad m] [MonadLiftT MetaM m] [MonadError m] (e : Expr) (pos : ExprPos) (replacement : Expr) : m Expr := do
-  match ← replaceAtPosHelper e pos.data replacement with
+  match ← replaceAtPosHelper e pos.toList replacement with
   | some res => return res
   | none => throwError "replaceAtPos error: Invalid position {pos} given for expression {e}"
 
@@ -270,7 +270,7 @@ private partial def abstractAtPosHelper! [Monad m] [MonadLiftT MetaM m] [MonadEr
     the given expression to consist only of applications up to the given ExprPos. Additionally, since the exact
     ExprPos is given, we don't need to pass in Meta.kabstract's second argument p -/
 partial def abstractAtPos! [Monad m] [MonadLiftT MetaM m] [MonadError m] (e : Expr) (pos : ExprPos) : m Expr := do
-  abstractAtPosHelper! e pos.data 0
+  abstractAtPosHelper! e pos.toList 0
 
 private partial def abstractAtPosesHelper! [Monad m] [MonadLiftT MetaM m] [MonadError m] (e : Expr)
   (poses : Array (List Nat)) (numBindersUnder : Nat) : m Expr := do
@@ -322,7 +322,7 @@ private partial def abstractAtPosesHelper! [Monad m] [MonadLiftT MetaM m] [Monad
     return e
 
 partial def abstractAtPoses! [Monad m] [MonadLiftT MetaM m] [MonadError m] (e : Expr) (poses : Array ExprPos) : m Expr :=
-  abstractAtPosesHelper! e (poses.map (fun x => x.data)) 0
+  abstractAtPosesHelper! e (poses.map (fun x => x.toList)) 0
 
 /-
   Note: this function may require revision to be more similar to Zipperposition's ho_weight function once we actually

Duper/Interface.lean

@@ -374,15 +374,15 @@ def unfoldDefinitions (formulas : List (Expr × Expr × Array Name × Bool)) : M
 
 def printSaturation (state : ProverM.State) : MetaM Unit := do
   trace[duper.prover.saturate] "Final Active Set: {state.activeSet.toArray}"
-  trace[duper.saturate.debug] "Final active set numbers: {state.activeSet.toArray.map (fun c => (state.allClauses.find! c).number)}"
+  trace[duper.saturate.debug] "Final active set numbers: {state.activeSet.toArray.map (fun c => (state.allClauses.get! c).number)}"
   trace[duper.saturate.debug] "Final Active Set: {state.activeSet.toArray}"
   trace[duper.saturate.debug] "Verified Inhabited Types: {state.verifiedInhabitedTypes.map (fun x => x.expr)}"
   trace[duper.saturate.debug] "Verified Nonempty Types: {state.verifiedNonemptyTypes.map (fun x => x.1.expr)}"
   trace[duper.saturate.debug] "Potentially Uninhabited Types: {state.potentiallyUninhabitedTypes.map (fun x => x.expr)}"
   trace[duper.saturate.debug] "Potentially Vacuous Clauses: {state.potentiallyVacuousClauses.toArray}"
 
 def formulasToMessageData : Expr × Expr × Array Name × Bool → MessageData
-| (ty, term, names, isFromGoal) => .compose (.compose m!"{names} @ " m!"{term} : ") m!"{ty}"
+| (ty, term, names, _isFromGoal) => .compose (.compose m!"{names} @ " m!"{term} : ") m!"{ty}"
 
 /-- Entry point for calling a single instance of duper using the options determined by (← getOptions).
 
@@ -455,7 +455,7 @@ def runDuperInstanceWithMonomorphization (formulas : List (Expr × Expr × Array
   let lemmas ← lemmas.mapM (m:=MetaM) (Auto.unfoldConstAndPreprocessLemma #[])
   let inhFacts ← Auto.Inhabitation.getInhFactsFromLCtx
   let prover : Array Auto.Lemma → Array Auto.Lemma → MetaM Expr :=
-    fun lemmas inhLemmas => do
+    fun lemmas _inhLemmas => do
       let monomorphizedFormulas ← autoLemmasToFormulas lemmas
       trace[duper.monomorphization.debug] "Original formulas: {formulas.map (fun f => (f.1, f.2.2.2))}"
       trace[duper.monomorphization.debug] "Auto lemmas: {lemmas.map (fun l => (l.type, l.proof, l.deriv))}"
@@ -472,7 +472,7 @@ def runDuperInstanceWithFullPreprocessing (formulas : List (Expr × Expr × Arra
   let lemmas ← lemmas.mapM (m:=MetaM) (Auto.unfoldConstAndPreprocessLemma #[])
   let inhFacts ← Auto.Inhabitation.getInhFactsFromLCtx
   let prover : Array Auto.Lemma → Array Auto.Lemma → MetaM Expr :=
-    fun lemmas inhLemmas => do
+    fun lemmas _inhLemmas => do
       let monomorphizedFormulas ← autoLemmasToFormulas lemmas
       trace[duper.monomorphization.debug] "Original formulas: {formulas.map (fun f => (f.1, f.2.2.2))}"
       trace[duper.monomorphization.debug] "Auto lemmas: {lemmas.map (fun l => (l.type, l.proof, l.deriv))}"

Duper/MClause.lean

@@ -10,7 +10,7 @@ deriving Inhabited, BEq, Hashable
 namespace MClause
 
 def toExpr (c : MClause) : Expr :=
-  litsToExpr c.lits.data
+  litsToExpr c.lits.toList
 where litsToExpr : List Lit → Expr
 | [] => mkConst ``False
 | [l] => l.toExpr

Duper/Order.lean

@@ -29,7 +29,7 @@ def Symbol.toString : Symbol → String
 instance : ToMessageData Symbol := ⟨Symbol.format⟩
 instance : ToString Symbol := ⟨Symbol.toString⟩
 
-abbrev SymbolPrecMap := HashMap Symbol Nat -- Maps symbols to their precedence. Lower numbers indicate higher precedence
+abbrev SymbolPrecMap := Std.HashMap Symbol Nat -- Maps symbols to their precedence. Lower numbers indicate higher precedence
 
 namespace Comparison
 
@@ -67,13 +67,13 @@ def absWeight (w : Weight) : Weight := (Int.natAbs w.1, Int.natAbs w.2)
 
 local notation "ω" => ((1,0) : Weight)
 
-def VarBalance := HashMap (Expr × Bool) Weight
+def VarBalance := Std.HashMap (Expr × Bool) Weight
 
 def VarBalance.addPosVar (vb : VarBalance) (t : Expr × Bool) : VarBalance :=
-  vb.insert t $ vb.findD t 0 + 1
+  vb.insert t $ vb.getD t 0 + 1
 
 def VarBalance.addNegVar (vb : VarBalance) (t : Expr × Bool) : VarBalance :=
-  vb.insert t $ vb.findD t 0 - 1
+  vb.insert t $ vb.getD t 0 - 1
 
 -- The orderings treat lambda-expressions like a "LAM" symbol applied to the
 -- type and body of the lambda-expression
@@ -112,14 +112,14 @@ def headWeight (f : Expr) (symbolPrecMap : SymbolPrecMap) (highesetPrecSymbolHas
       if belowLam then 1 else ω
     else
       let fSymbol := Symbol.Const name
-      match symbolPrecMap.find? fSymbol with
+      match symbolPrecMap.get? fSymbol with
       | some 0 => -- The symbol with the highest precedence in symbolPrecMap is mapped to 0 (unless it has arity zero)
         if highesetPrecSymbolHasArityZero then 1
         else 0
       | _ => 1
   | Expr.fvar fVarId =>
     let fSymbol := Symbol.FVarId fVarId
-    match symbolPrecMap.find? fSymbol with
+    match symbolPrecMap.get? fSymbol with
     | some 0 => -- The symbol with the highest precedence in symbolPrecMap is mapped to 0 (unless it has arity zero)
       if highesetPrecSymbolHasArityZero then 1
       else 0
@@ -180,7 +180,7 @@ def symbolPrecCompare (e1 : Expr) (e2 : Expr) (s1 : Symbol) (s2 : Symbol) (symbo
     so that the firstmaximal0 weight generation scheme can determine if a symbol is maximal simply by checking whether it maps
     to 0 in symbolPrecMap
   -/
-  match symbolPrecMap.find? s1, symbolPrecMap.find? s2 with
+  match symbolPrecMap.get? s1, symbolPrecMap.get? s2 with
   | some n1, some n2 =>
     if n1 > n2 then return LessThan -- n1 is larger than n2 so s1 has a lower precedence
     else if n1 < n2 then return GreaterThan -- n1 is smaller than n2 so s1 has a higher precedence
@@ -407,13 +407,13 @@ mutual
   partial def kbo (t1 t2 : Expr) (alreadyReduced : Bool) (symbolPrecMap : SymbolPrecMap)
     (highesetPrecSymbolHasArityZero : Bool) : MetaM Comparison := do
     if alreadyReduced then
-      let (_, _, res) ← tckbo 0 HashMap.empty t1 t2 (belowLam := false) symbolPrecMap highesetPrecSymbolHasArityZero
+      let (_, _, res) ← tckbo 0 Std.HashMap.empty t1 t2 (belowLam := false) symbolPrecMap highesetPrecSymbolHasArityZero
       trace[duper.unaryFirst.debug] "Result of comparing {t1} with {t2} (alreadyReduced: {alreadyReduced}) is {res}"
       return res
     else
       let t1 ← betaEtaReduceInstMVars t1
       let t2 ← betaEtaReduceInstMVars t2
-      let (_, _, res) ← tckbo 0 HashMap.empty t1 t2 (belowLam := false) symbolPrecMap highesetPrecSymbolHasArityZero
+      let (_, _, res) ← tckbo 0 Std.HashMap.empty t1 t2 (belowLam := false) symbolPrecMap highesetPrecSymbolHasArityZero
       trace[duper.unaryFirst.debug] "Result of comparing {t1} with {t2} (alreadyReduced: {alreadyReduced}) is {res}"
       return res
 
@@ -555,12 +555,12 @@ end
     the two expressions' weights. -/
 def getNetWeight (t1 t2 : Expr) (alreadyReduced : Bool) (symbolPrecMap : SymbolPrecMap) (highesetPrecSymbolHasArityZero : Bool) : MetaM Weight := do
   if alreadyReduced then
-    let (netWeight, _, _) ← tckbo 0 HashMap.empty t1 t2 (belowLam := false) symbolPrecMap highesetPrecSymbolHasArityZero
+    let (netWeight, _, _) ← tckbo 0 Std.HashMap.empty t1 t2 (belowLam := false) symbolPrecMap highesetPrecSymbolHasArityZero
     return netWeight
   else
     let t1 ← betaEtaReduceInstMVars t1
     let t2 ← betaEtaReduceInstMVars t2
-    let (netWeight, _, _) ← tckbo 0 HashMap.empty t1 t2 (belowLam := false) symbolPrecMap highesetPrecSymbolHasArityZero
+    let (netWeight, _, _) ← tckbo 0 Std.HashMap.empty t1 t2 (belowLam := false) symbolPrecMap highesetPrecSymbolHasArityZero
     return netWeight
 
 end Order

Duper/Preprocessing.lean

@@ -55,12 +55,12 @@ partial def preprocessingClausification : ProverM Unit := do
     times, then updates f's result in symbolFreqMap to be n greater than it was originally). Note that as with Expr.weight,
     this function may require revision to be more similar to Zipperposition's implementation once we actually start working
     on higher order things. -/
-partial def updateSymbolFreqArityMap (f : Expr) (symbolFreqArityMap : HashMap Symbol (Nat × Nat)) :
-  ProverM (HashMap Symbol (Nat × Nat)) := do
+partial def updateSymbolFreqArityMap (f : Expr) (symbolFreqArityMap : Std.HashMap Symbol (Nat × Nat)) :
+  ProverM (Std.HashMap Symbol (Nat × Nat)) := do
   match f with
   | Expr.fvar fVarId =>
     let fSymbol := Symbol.FVarId fVarId
-    match symbolFreqArityMap.find? fSymbol with
+    match symbolFreqArityMap.get? fSymbol with
     | some (fFreq, fArity) => return symbolFreqArityMap.insert fSymbol (fFreq + 1, fArity)
     | none =>
       match (← getLCtx).fvarIdToDecl.find? fVarId with
@@ -70,7 +70,7 @@ partial def updateSymbolFreqArityMap (f : Expr) (symbolFreqArityMap : HashMap Sy
       | none => throwError s!"Unable to find {fVarId.name} in local context"
   | Expr.const name _ =>
     let fSymbol := Symbol.Const name
-    match symbolFreqArityMap.find? fSymbol with
+    match symbolFreqArityMap.get? fSymbol with
     | some (fFreq, fArity) => return symbolFreqArityMap.insert fSymbol (fFreq + 1, fArity)
     | none =>
       let fType ← inferType f
@@ -107,13 +107,13 @@ def isInductiveAndNonPropAndNotTypeClass (t : Expr) : ProverM Bool := do
     on higher order things. Additionally, updates datatypeList to make sure that all inductive datatypes that appear
     in the problem are contained in the datatypeList. The format in which inductive datatypes are recorded as elements of
     type `Expr × Array Name` is described in the comment above `buildSymbolFreqArityMapAndDatatypeList` -/
-partial def updateSymbolFreqArityMapAndDatatypeList (f : Expr) (symbolFreqArityMap : HashMap Symbol (Nat × Nat))
+partial def updateSymbolFreqArityMapAndDatatypeList (f : Expr) (symbolFreqArityMap : Std.HashMap Symbol (Nat × Nat))
   (datatypeList : List (Expr × Array Name)) (paramNames : Array Name) :
-  ProverM (HashMap Symbol (Nat × Nat) × List (Expr × Array Name)) := do
+  ProverM (Std.HashMap Symbol (Nat × Nat) × List (Expr × Array Name)) := do
   match f with
   | Expr.fvar fVarId =>
     let fSymbol := Symbol.FVarId fVarId
-    match symbolFreqArityMap.find? fSymbol with
+    match symbolFreqArityMap.get? fSymbol with
     | some (fFreq, fArity) => return (symbolFreqArityMap.insert fSymbol (fFreq + 1, fArity), datatypeList)
     | none =>
       match (← getLCtx).fvarIdToDecl.find? fVarId with
@@ -127,7 +127,7 @@ partial def updateSymbolFreqArityMapAndDatatypeList (f : Expr) (symbolFreqArityM
       | none => throwError s!"Unable to find {fVarId.name} in local context"
   | Expr.const name _ =>
     let fSymbol := Symbol.Const name
-    match symbolFreqArityMap.find? fSymbol with
+    match symbolFreqArityMap.get? fSymbol with
     | some (fFreq, fArity) => -- fSymbol has already been seen so datatypeList does not need to be updated
       return (symbolFreqArityMap.insert fSymbol (fFreq + 1, fArity), datatypeList)
     | none =>
@@ -216,8 +216,8 @@ partial def updateSymbolFreqArityMapAndDatatypeList (f : Expr) (symbolFreqArityM
 /-- Builds a HashMap that maps each symbol to a tuple containing:
     - The number of times they appear in formulas
     - Its arity -/
-partial def buildSymbolFreqArityMap (clauses : List Clause) : ProverM (HashMap Symbol (Nat × Nat)) := do
-  let mut symbolFreqArityMap := HashMap.empty
+partial def buildSymbolFreqArityMap (clauses : List Clause) : ProverM (Std.HashMap Symbol (Nat × Nat)) := do
+  let mut symbolFreqArityMap := Std.HashMap.empty
   for c in clauses do
     for l in c.lits do
       symbolFreqArityMap ← updateSymbolFreqArityMap l.lhs symbolFreqArityMap
@@ -232,8 +232,8 @@ partial def buildSymbolFreqArityMap (clauses : List Clause) : ProverM (HashMap S
     - A list containing every inductive datatype that appears in any clause. Polymorphic inductive datatypes are represented as universally
     quantified types paired with an array of parameters that can appear in the inductive datatype. For example, the polymorphic list datatype
     `List α` of where `α : Type u` is represented via `((∀ (α : Type u), List α), #[u])` -/
-partial def buildSymbolFreqArityMapAndDatatypeList (clauses : List Clause) : ProverM (HashMap Symbol (Nat × Nat) × List (Expr × Array Name)) := do
-  let mut symbolFreqArityMap := HashMap.empty
+partial def buildSymbolFreqArityMapAndDatatypeList (clauses : List Clause) : ProverM (Std.HashMap Symbol (Nat × Nat) × List (Expr × Array Name)) := do
+  let mut symbolFreqArityMap := Std.HashMap.empty
   let mut datatypeList := []
   for c in clauses do
     trace[duper.collectDatatypes.debug] "Loaded clause c: {c.lits}"
@@ -289,7 +289,7 @@ def buildSymbolPrecMap (clauses : List Clause) : ProverM (SymbolPrecMap × Bool)
     -- We use unaryFirstGt as the lt argument for binInsert so that symbols with higher precedence come first in symbolPrecArray
     symbolPrecArr := symbolPrecArr.binInsert unaryFirstGt (s, sFreq, sArity)
   trace[duper.unaryFirst.debug] "symbolPrecArr: {symbolPrecArr}"
-  let mut symbolPrecMap := HashMap.empty
+  let mut symbolPrecMap := Std.HashMap.empty
   let mut counter := 0
   let mut highesetPrecSymbolHasArityZero := false
   for (s, _, sArity) in symbolPrecArr do
@@ -343,7 +343,7 @@ def buildSymbolPrecMapAndDatatypeList (clauses : List Clause) : ProverM (SymbolP
     -- We use unaryFirstGt as the lt argument for binInsert so that symbols with higher precedence come first in symbolPrecArray
     symbolPrecArr := symbolPrecArr.binInsert unaryFirstGt (s, sFreq, sArity)
   trace[duper.unaryFirst.debug] "symbolPrecArr: {symbolPrecArr}"
-  let mut symbolPrecMap := HashMap.empty
+  let mut symbolPrecMap := Std.HashMap.empty
   let mut counter := 0
   let mut highesetPrecSymbolHasArityZero := false
   for (s, _, sArity) in symbolPrecArr do