Fixing LazyList name clash and adding Duper.lean

Duper.lean

@@ -0,0 +1 @@
+import Duper.Tactic

Duper/DUnif/Bindings.lean

@@ -29,7 +29,7 @@ def withoutModifyingMCtx (x : MetaM α) : MetaM α := do
   finally
     setMCtx s
 
-def iteration (F : Expr) (p : UnifProblem) (eq : UnifEq) (funcArgOnly : Bool) : MetaM (LazyList <| MetaM (Array UnifProblem)) := do
+def iteration (F : Expr) (p : UnifProblem) (eq : UnifEq) (funcArgOnly : Bool) : MetaM (Duper.LazyList <| MetaM (Array UnifProblem)) := do
   setMCtx p.mctx
   let Fty ← Meta.inferType F
   Meta.forallTelescopeReducing Fty fun xs β₁ => (do
@@ -79,8 +79,8 @@ def iteration (F : Expr) (p : UnifProblem) (eq : UnifEq) (funcArgOnly : Bool) :
       )
       -- Get rid of metavariables in `xys`
       setMCtx p.mctx
-    let iterAtIArr := iterAtIFuns.map (fun f => (LazyList.nats 0).map f)
-    return LazyList.interleaveN iterAtIArr
+    let iterAtIArr := iterAtIFuns.map (fun f => (Duper.LazyList.nats 0).map f)
+    return Duper.LazyList.interleaveN iterAtIArr
   )
 
 /-- `F` is a metavariable -/
@@ -185,7 +185,7 @@ def imitProj (F : Expr) (nLam : Nat) (iTy : Expr) (oTy : Expr) (name : Name) (id
     the left-hand side, we will see that `h + n - k - len(bin_F) = m - len(bin_g)`, i.e.
   · `h = m + k + len(bin_F) - n - len(bin_g)`
   The above equation can be used to determine the value of `h`.
-  
+
   Now we specify the types of fresh metavariables and the resulting equations
   · The type of `?Hᵢ (1 ≤ i ≤ min (l, h))` is taken care of by `forallMetaTelescopeReducing`
   · If `h ≤ l`, the type of `binding` should be unified with the type of `F`. This
@@ -233,7 +233,7 @@ 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}]
 
-def elimination (F : Expr) (p : UnifProblem) (eq : UnifEq) : MetaM (LazyList <| MetaM (Array UnifProblem)) := do
+def elimination (F : Expr) (p : UnifProblem) (eq : UnifEq) : MetaM (Duper.LazyList <| MetaM (Array UnifProblem)) := do
   setMCtx p.mctx
   let lctx₀ ← getLCtx
   let Fty ← Meta.inferType F
@@ -341,4 +341,4 @@ def identification (F : Expr) (G : Expr) (p : UnifProblem) (eq : UnifEq) : MetaM
   MVarId.assign G.mvarId! mtG
   let up' := {(← p.pushParentRuleIfDbgOn (.Identification eq F G mtF mtG))
               with checked := false, mctx := ← getMCtx, identVar := p.identVar.insert mH}
-  return .NewArray #[up']
+  return .NewArray #[up']

Duper/DUnif/UnifProblem.lean

@@ -400,5 +400,5 @@ def structInfo (p : UnifProblem) (e : Expr) : MetaM (Expr × StructType) := do
 -- Bool : True -> Succeed, False -> Fail
 inductive UnifRuleResult
 | NewArray : Array UnifProblem → UnifRuleResult
-| NewLazyList : LazyList (MetaM (Array UnifProblem)) → UnifRuleResult
+| NewLazyList : Duper.LazyList (MetaM (Array UnifProblem)) → UnifRuleResult
 | Succeed : UnifRuleResult

Duper/DUnif/UnifRules.lean

@@ -329,14 +329,14 @@ def applyRules (p : UnifProblem) (config : Config) : MetaM UnifRuleResult := do
         if config.iterationOn then
           let liter ← DUnif.iteration lh p eq false
           let riter ← DUnif.iteration rh p eq false
-          return LazyList.interleave liter riter
+          return Duper.LazyList.interleave liter riter
         else
-          return LazyList.nil)
+          return Duper.LazyList.nil)
       -- Identification
       let mut arr := #[]
       match (← DUnif.identification lh rh p eq) with
       | .NewArray a => arr := arr.append a
-      | .NewLazyList l => ll := LazyList.interleave l ll
+      | .NewLazyList l => ll := Duper.LazyList.interleave l ll
       | .Succeed => throwError "applyRules :: identification never succeeds"
       -- JP style projection
       if ¬ p.identVar.contains lh then
@@ -355,10 +355,10 @@ def applyRules (p : UnifProblem) (config : Config) : MetaM UnifRuleResult := do
         if config.iterationOn then
           DUnif.iteration lh p eq true
         else
-          return LazyList.nil)
+          return Duper.LazyList.nil)
       -- Eliminations
       let elims ← DUnif.elimination lh p eq
-      return .NewLazyList (LazyList.cons (pure decomp) (LazyList.interleave elims iters))
+      return .NewLazyList (Duper.LazyList.cons (pure decomp) (Duper.LazyList.interleave elims iters))
   else
     -- No equations left
     return .Succeed
@@ -369,7 +369,7 @@ def applyRules (p : UnifProblem) (config : Config) : MetaM UnifRuleResult := do
 
 inductive QueueElement
 | Problem : UnifProblem → QueueElement
-| LazyListOfProblem : LazyList (MetaM (Array UnifProblem)) → QueueElement
+| LazyListOfProblem : Duper.LazyList (MetaM (Array UnifProblem)) → QueueElement
 deriving Inhabited
 
 structure UnifierGenerator where

Duper/SubsumptionTrie.lean

@@ -229,7 +229,7 @@ def emptyNode : SubsumptionTrie := node #[]
 
 def singleton (c : Clause) (features : FeatureVector) : SubsumptionTrie :=
   match features with
-  | nil => leaf (HashSet.empty.insert c)
+  | [] => leaf (HashSet.empty.insert c)
   | fstFeature :: restFeatures => node #[(fstFeature, singleton c restFeatures)]
 
 private def insertHelper (t : SubsumptionTrie) (c : Clause) (features : FeatureVector) : RuleM SubsumptionTrie :=
@@ -243,7 +243,7 @@ private def insertHelper (t : SubsumptionTrie) (c : Clause) (features : FeatureV
         return node children'
       curIdx := curIdx + 1
     return node (children.push (fstFeature, singleton c restFeatures))
-  | leaf vals, nil => return leaf (vals.insert c)
+  | leaf vals, [] => return leaf (vals.insert c)
   | _, _ => throwError "Features: {features} length does not match depth of trie {t}"
 
 def insert (t : SubsumptionTrie) (c : Clause) : RuleM SubsumptionTrie :=
@@ -260,7 +260,7 @@ private def deleteHelper (t : SubsumptionTrie) (c : Clause) (features : FeatureV
         return node children'
       curIdx := curIdx + 1
     return node children -- c not found in t, so just return original t
-  | leaf vals, nil => return leaf (vals.erase c)
+  | leaf vals, [] => return leaf (vals.erase c)
   | _, _ => throwError "Features: {features} length does not match depth of trie {t}"
 
 def delete (t : SubsumptionTrie) (c : Clause) : RuleM SubsumptionTrie :=
@@ -274,7 +274,7 @@ private def getPotentialSubsumingClausesHelper (t : SubsumptionTrie) (features :
       if SubsumptionTrieFeatureValueLe childFeature fstFeature then
         potentialSubsumingClauses := potentialSubsumingClauses.append (← getPotentialSubsumingClausesHelper childTrie restFeatures)
     return potentialSubsumingClauses
-  | leaf vals, nil => return vals.toArray
+  | leaf vals, [] => return vals.toArray
   | _, _ => throwError "Features: {features} length does not match depth of trie {t}"
 
 def getPotentialSubsumingClauses (t : SubsumptionTrie) (c : Clause) : RuleM (Array Clause) :=
@@ -292,7 +292,7 @@ private def getPotentialSubsumedClausesHelper (t : SubsumptionTrie) (features :
       if SubsumptionTrieFeatureValueLe fstFeature childFeature then
         potentialSubsumingClauses := potentialSubsumingClauses.append (← getPotentialSubsumedClausesHelper childTrie restFeatures)
     return potentialSubsumingClauses
-  | leaf vals, nil => return vals.toArray
+  | leaf vals, [] => return vals.toArray
   | _, _ => throwError "Features: {features} length does not match depth of trie {t}"
 
 def getPotentialSubsumedClauses (t : SubsumptionTrie) (c : Clause) : RuleM (Array Clause) :=

Duper/Util/LazyList.lean

@@ -4,20 +4,20 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 
-inductive LazyList (α : Type u)
+inductive Duper.LazyList (α : Type u)
 | nil                             : LazyList α
 | cons (hd : α) (tl : LazyList α) : LazyList α
 | delayed (t : Thunk (LazyList α)): LazyList α
 
 -- @[extern cpp inline "#2"]
-def List.toLazy {α : Type u} : List α → LazyList α
-| []     => LazyList.nil
-| (h::t) => LazyList.cons h (List.toLazy t)
+def Duper.List.toLazy {α : Type u} : List α → Duper.LazyList α
+| []     => Duper.LazyList.nil
+| (h::t) => Duper.LazyList.cons h (Duper.List.toLazy t)
 
-namespace LazyList
+namespace Duper.LazyList
 variable {α : Type u} {β : Type v} {δ : Type w}
 
-instance : Inhabited (LazyList α) :=
+instance : Inhabited (Duper.LazyList α) :=
 ⟨nil⟩
 
 partial def nats i := cons i (delayed (nats (i + 1)))
@@ -178,43 +178,40 @@ def approxToString [ToString α] (as : LazyList α) (n : Nat := 10) : String :=
 
 instance [ToString α] : ToString (LazyList α) := ⟨approxToString⟩
 
-end LazyList
-
-
+end Duper.LazyList
 
 -- Other utilities
 
-def List.lazySubsequences {α : Type u} : List α → LazyList (List α)
+def List.lazySubsequences {α : Type u} : List α → Duper.LazyList (List α)
 | .nil => .cons .nil .nil
-| .cons a as => List.lazySubsequences as ++ .delayed (LazyList.map (List.cons a) (lazySubsequences as))
+| .cons a as => List.lazySubsequences as ++ .delayed (Duper.LazyList.map (List.cons a) (lazySubsequences as))
 
 
 
 -- Testing
+def fib : Duper.LazyList Nat :=
+  Duper.LazyList.iterate₂ (·+·) 0 1
 
-def fib : LazyList Nat :=
-  LazyList.iterate₂ (·+·) 0 1
-
-def tst : LazyList String := do
-  let x ← [1, 2, 3].toLazy
-  let y ← [2, 3, 4].toLazy
+def tst : Duper.LazyList String := do
+  let x ← Duper.List.toLazy [1, 2, 3]
+  let y ← Duper.List.toLazy [2, 3, 4]
   -- dbgTrace (toString x ++ " " ++ toString y) $ λ _,
   guard (x + y > 5)
   pure (toString x ++ " + " ++ toString y ++ " = " ++ toString (x+y))
 
-open LazyList
+open Duper.LazyList
 
-def iota (i : UInt32 := 0) : LazyList UInt32 :=
+def iota (i : UInt32 := 0) : Duper.LazyList UInt32 :=
   iterate (·+1) i
 
 set_option pp.explicit true
 
-partial def sieve : LazyList UInt32 → LazyList UInt32
+partial def sieve : Duper.LazyList UInt32 → Duper.LazyList UInt32
 | nil          => nil
 | (cons a as)  => cons a (delayed (sieve (filter (λ b => b % a != 0) as)))
 | (delayed as) => sieve as.get
 
-partial def primes : LazyList UInt32 :=
+partial def primes : Duper.LazyList UInt32 :=
   sieve (iota 2)
 
 def maintest : IO Unit := do
@@ -229,4 +226,4 @@ def maintest : IO Unit := do
   -- IO.println $ ((iota.map (+10)).filter (λ v, v % 2 == 0)),
   pure ()
 
-partial def natuple := LazyList.bindω (LazyList.nats 0) (fun i => (LazyList.nats 0).zip (repeats i))
+partial def natuple := Duper.LazyList.bindω (Duper.LazyList.nats 0) (fun i => (Duper.LazyList.nats 0).zip (repeats i))

Main.lean

@@ -1,4 +1,4 @@
-import Duper.Tactic
+import Duper
 import Duper.TPTP -- Note: this import is needed to make sure that TPTP is compiled for the github actions
 import Duper.TPTPParser.PrattParser