structure Duper.Lit : Type

• sign : Bool
• lvl : Lean.Level
• ty : Lean.Expr
• lhs : Lean.Expr
• rhs : Lean.Expr

def Duper.instInhabitedLit.default : Lit

Equations

• Duper.instInhabitedLit.default = { sign := default, lvl := default, ty := default, lhs := default, rhs := default }

instance Duper.instInhabitedLit : Inhabited Lit

Equations

• Duper.instInhabitedLit = { default := Duper.instInhabitedLit.default }

instance Duper.instBEqLit : BEq Lit

Equations

• Duper.instBEqLit = { beq := Duper.instBEqLit.beq }

def Duper.instBEqLit.beq : Lit → Lit → Bool

Equations

• One or more equations did not get rendered due to their size.
• Duper.instBEqLit.beq x✝¹ x✝ = false

def Duper.instHashableLit.hash : Lit → UInt64

Equations

• Duper.instHashableLit.hash { sign := a, lvl := a_1, ty := a_2, lhs := a_3, rhs := a_4 } = mixHash (mixHash (mixHash (mixHash (mixHash 0 (hash a)) (hash a_1)) (hash a_2)) (hash a_3)) (hash a_4)

instance Duper.instHashableLit : Hashable Lit

Equations

• Duper.instHashableLit = { hash := Duper.instHashableLit.hash }

inductive Duper.LitSide : Type

• lhs : LitSide
• rhs : LitSide

def Duper.instInhabitedLitSide.default : LitSide

Equations

• Duper.instInhabitedLitSide.default = Duper.LitSide.lhs

instance Duper.instInhabitedLitSide : Inhabited LitSide

Equations

• Duper.instInhabitedLitSide = { default := Duper.instInhabitedLitSide.default }

def Duper.instBEqLitSide.beq : LitSide → LitSide → Bool

Equations

• Duper.instBEqLitSide.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Duper.instBEqLitSide : BEq LitSide

Equations

• Duper.instBEqLitSide = { beq := Duper.instBEqLitSide.beq }

instance Duper.instHashableLitSide : Hashable LitSide

Equations

• Duper.instHashableLitSide = { hash := Duper.instHashableLitSide.hash }

def Duper.instHashableLitSide.hash : LitSide → UInt64

Equations

• Duper.instHashableLitSide.hash Duper.LitSide.lhs = 0
• Duper.instHashableLitSide.hash Duper.LitSide.rhs = 1

def Duper.Lit.toString (l : Lit) : String

Equations

• l.toString = toString l.lhs ++ if l.sign = true then " = " else " ≠ " ++ toString l.rhs

def Duper.LitSide.format (ls : LitSide) : Lean.MessageData

Equations

• Duper.LitSide.lhs.format = Lean.toMessageData "lhs"
• Duper.LitSide.rhs.format = Lean.toMessageData "rhs"

instance Duper.instToMessageDataLitSide : Lean.ToMessageData LitSide

Equations

• Duper.instToMessageDataLitSide = { toMessageData := Duper.LitSide.format }

def Duper.LitSide.toggleSide (side : LitSide) : LitSide

Equations

• Duper.LitSide.lhs.toggleSide = Duper.LitSide.rhs
• Duper.LitSide.rhs.toggleSide = Duper.LitSide.lhs

structure Duper.LitPos : Type

• side : LitSide
• pos : ExprPos

def Duper.instInhabitedLitPos.default : LitPos

Equations

• Duper.instInhabitedLitPos.default = { side := default, pos := default }

instance Duper.instInhabitedLitPos : Inhabited LitPos

Equations

• Duper.instInhabitedLitPos = { default := Duper.instInhabitedLitPos.default }

instance Duper.instBEqLitPos : BEq LitPos

Equations

• Duper.instBEqLitPos = { beq := Duper.instBEqLitPos.beq }

def Duper.instBEqLitPos.beq : LitPos → LitPos → Bool

Equations

• Duper.instBEqLitPos.beq { side := a, pos := a_1 } { side := b, pos := b_1 } = (a == b && a_1 == b_1)
• Duper.instBEqLitPos.beq x✝¹ x✝ = false

instance Duper.instHashableLitPos : Hashable LitPos

Equations

• Duper.instHashableLitPos = { hash := Duper.instHashableLitPos.hash }

def Duper.instHashableLitPos.hash : LitPos → UInt64

Equations

• Duper.instHashableLitPos.hash { side := a, pos := a_1 } = mixHash (mixHash 0 (hash a)) (hash a_1)

def Duper.Lit.toExpr (lit : Lit) : Lean.Expr

Equations

• lit.toExpr = if lit.sign = true then Lean.mkApp3 (Lean.mkConst `Eq [lit.lvl]) lit.ty lit.lhs lit.rhs else Lean.mkApp3 (Lean.mkConst `Ne [lit.lvl]) lit.ty lit.lhs lit.rhs

def Duper.Lit.fromSingleExpr (e : Lean.Expr) (sign : Bool := true) : Lit

Equations

• One or more equations did not get rendered due to their size.

def Duper.Lit.fromExpr : Lean.Expr → Lit

Equations

• Duper.Lit.fromExpr ((((Lean.Expr.const `Eq lvl).app ty).app lhs).app rhs) = { sign := true, lvl := lvl[0]!, ty := ty, lhs := lhs, rhs := rhs }
• Duper.Lit.fromExpr ((((Lean.Expr.const `Ne lvl).app ty).app lhs).app rhs) = { sign := false, lvl := lvl[0]!, ty := ty, lhs := lhs, rhs := rhs }
• Duper.Lit.fromExpr x✝ = dbgTrace (toString "Lit.fromExpr :: Unexpected Expression: " ++ toString x✝) fun (x : Unit) => Duper.Lit.fromSingleExpr x✝

def Duper.Lit.map (f : Lean.Expr → Lean.Expr) (l : Lit) : Lit

Equations

• Duper.Lit.map f l = { sign := l.sign, lvl := l.lvl, ty := f l.ty, lhs := f l.lhs, rhs := f l.rhs }

def Duper.Lit.instantiateLevelParamsArray (l : Lit) (paramNames : Array Lean.Name) (levels : Array Lean.Level) : Lit

Equations

• One or more equations did not get rendered due to their size.

def Duper.Lit.mapWithPos (f : Lean.Expr → Lean.Expr × Array ExprPos) (l : Lit) : Lit × Array LitPos

Equations

• One or more equations did not get rendered due to their size.

def Duper.Lit.mapMWithPos {m : Type → Type u_1} [Monad m] [MonadLiftT Lean.MetaM m] (f : Lean.Expr → m (Lean.Expr × Array ExprPos)) (l : Lit) : m (Lit × Array LitPos)

Equations

• One or more equations did not get rendered due to their size.

def Duper.Lit.mapByPos (f : Lean.Expr → Array ExprPos → Lean.Expr) (l : Lit) (poses : Array LitPos) : Lit

Equations

• One or more equations did not get rendered due to their size.

def Duper.Lit.mapMByPos {m : Type → Type u_1} [Monad m] [MonadLiftT Lean.MetaM m] (f : Lean.Expr → Array ExprPos → m Lean.Expr) (l : Lit) (poses : Array LitPos) : m Lit

Equations

• One or more equations did not get rendered due to their size.

def Duper.Lit.mapM {m : Type → Type w} [Monad m] (f : Lean.Expr → m Lean.Expr) (l : Lit) : m Lit

Equations

• One or more equations did not get rendered due to their size.

def Duper.Lit.fold {α : Type v} (f : α → Lean.Expr → α) (init : α) (l : Lit) : α

Equations

• Duper.Lit.fold f init l = f (f init l.lhs) l.rhs

def Duper.Lit.foldWithTypeM {β : Type v} {m : Type v → Type w} [Monad m] (f : β → Lean.Expr → m β) (init : β) (l : Lit) : m β

Equations

• Duper.Lit.foldWithTypeM f init l = do let __do_lift ← f init l.ty let __do_lift ← f __do_lift l.lhs f __do_lift l.rhs

def Duper.Lit.foldM {β : Type v} {m : Type v → Type w} [Monad m] (f : β → Lean.Expr → LitPos → m β) (init : β) (l : Lit) : m β

Equations

• Duper.Lit.foldM f init l = do let __do_lift ← f init l.lhs { side := Duper.LitSide.lhs, pos := Duper.ExprPos.empty } f __do_lift l.rhs { side := Duper.LitSide.rhs, pos := Duper.ExprPos.empty }

def Duper.Lit.foldGreenM {m : Type → Type u_1} {β : Type} [Monad m] [MonadLiftT Lean.MetaM m] (f : β → Lean.Expr → LitPos → m β) (init : β) (l : Lit) : m β

Equations

• One or more equations did not get rendered due to their size.

def Duper.Lit.getAtPos! {m : Type → Type u_1} [Monad m] [MonadLiftT Lean.MetaM m] (l : Lit) (pos : LitPos) : m Lean.Expr

Equations

• l.getAtPos! pos = match pos.side with | Duper.LitSide.lhs => l.lhs.getAtPos! pos.pos | Duper.LitSide.rhs => l.rhs.getAtPos! pos.pos

def Duper.Lit.replaceAtPos? {m : Type → Type u_1} [Monad m] [MonadLiftT Lean.MetaM m] (l : Lit) (pos : LitPos) (replacement : Lean.Expr) : m (Option Lit)

Equations

• One or more equations did not get rendered due to their size.

def Duper.Lit.replaceAtPos! {m : Type → Type} [Monad m] [MonadLiftT Lean.MetaM m] [Lean.MonadError m] (l : Lit) (pos : LitPos) (replacement : Lean.Expr) : m Lit

Equations

• One or more equations did not get rendered due to their size.

def Duper.Lit.replaceAtPosUpdateType? (l : Lit) (pos : LitPos) (replacement : Lean.Expr) : Lean.MetaM (Option Lit)

Note : This function will throw error if pos is not a valid pos for l

Equations

• One or more equations did not get rendered due to their size.

def Duper.Lit.abstractAtPos! (l : Lit) (pos : LitPos) : Lean.MetaM Lit

This function acts as Meta.kabstract except that it takes a LitPos rather than Occurrences and expects the given expression to consist only of applications up to the given ExprPos. Additionally, since the exact position is given, we don't need to pass in Meta.kabstract's second argument p

Equations

• One or more equations did not get rendered due to their size.

def Duper.Lit.symm (l : Lit) : Lit

Equations

• l.symm = { sign := l.sign, lvl := l.lvl, ty := l.ty, lhs := l.rhs, rhs := l.lhs }

def Duper.Lit.makeLhs (lit : Lit) (side : LitSide) : Lit

Equations

• lit.makeLhs Duper.LitSide.lhs = lit
• lit.makeLhs Duper.LitSide.rhs = lit.symm

def Duper.Lit.getSide (lit : Lit) (side : LitSide) : Lean.Expr

Equations

• lit.getSide Duper.LitSide.lhs = lit.lhs
• lit.getSide Duper.LitSide.rhs = lit.rhs

def Duper.Lit.getOtherSide (lit : Lit) (side : LitSide) : Lean.Expr

Equations

• lit.getOtherSide side = lit.getSide side.toggleSide

instance Duper.Lit.instToFormat : Std.ToFormat Lit

Equations

• Duper.Lit.instToFormat = { format := fun (lit : Duper.Lit) => Std.format lit.toExpr }

instance Duper.Lit.instToMessageData : Lean.ToMessageData Lit

Equations

• Duper.Lit.instToMessageData = { toMessageData := fun (lit : Duper.Lit) => Lean.MessageData.ofExpr lit.toExpr }

def Duper.Lit.compare (ord : Lean.Expr → Lean.Expr → Bool → Lean.MetaM Comparison) (alreadyReduced : Bool) (l₁ l₂ : Lit) : Lean.MetaM Comparison

Equations

• One or more equations did not get rendered due to their size.

structure Duper.Clause : Type

• paramNames : Array Lean.Name
• bVarTypes : Array Lean.Expr
• lits : Array Lit

def Duper.instInhabitedClause.default : Clause

Equations

• Duper.instInhabitedClause.default = { paramNames := default, bVarTypes := default, lits := default }

instance Duper.instInhabitedClause : Inhabited Clause

Equations

• Duper.instInhabitedClause = { default := Duper.instInhabitedClause.default }

instance Duper.instBEqClause : BEq Clause

Equations

• Duper.instBEqClause = { beq := Duper.instBEqClause.beq }

def Duper.instBEqClause.beq : Clause → Clause → Bool

Equations

• Duper.instBEqClause.beq { paramNames := a, bVarTypes := a_1, lits := a_2 } { paramNames := b, bVarTypes := b_1, lits := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Duper.instBEqClause.beq x✝¹ x✝ = false

def Duper.instHashableClause.hash : Clause → UInt64

Equations

• Duper.instHashableClause.hash { paramNames := a, bVarTypes := a_1, lits := a_2 } = mixHash (mixHash (mixHash 0 (hash a)) (hash a_1)) (hash a_2)

instance Duper.instHashableClause : Hashable Clause

Equations

• Duper.instHashableClause = { hash := Duper.instHashableClause.hash }

structure Duper.ClausePosextends Duper.LitPos : Type

• side : LitSide
• pos : ExprPos
• lit : Nat

instance Duper.instInhabitedClausePos : Inhabited ClausePos

Equations

• Duper.instInhabitedClausePos = { default := Duper.instInhabitedClausePos.default }

def Duper.instInhabitedClausePos.default : ClausePos

Equations

• Duper.instInhabitedClausePos.default = { toLitPos := default, lit := default }

instance Duper.instBEqClausePos : BEq ClausePos

Equations

• Duper.instBEqClausePos = { beq := Duper.instBEqClausePos.beq }

def Duper.instBEqClausePos.beq : ClausePos → ClausePos → Bool

Equations

• Duper.instBEqClausePos.beq { toLitPos := a, lit := a_1 } { toLitPos := b, lit := b_1 } = (a == b && a_1 == b_1)
• Duper.instBEqClausePos.beq x✝¹ x✝ = false

def Duper.instHashableClausePos.hash : ClausePos → UInt64

Equations

• Duper.instHashableClausePos.hash { toLitPos := a, lit := a_1 } = mixHash (mixHash 0 (hash a)) (hash a_1)

instance Duper.instHashableClausePos : Hashable ClausePos

Equations

• Duper.instHashableClausePos = { hash := Duper.instHashableClausePos.hash }

def Duper.ClausePos.format (pos : ClausePos) : Lean.MessageData

Equations

• One or more equations did not get rendered due to their size.

instance Duper.instToMessageDataClausePos : Lean.ToMessageData ClausePos

Equations

• Duper.instToMessageDataClausePos = { toMessageData := Duper.ClausePos.format }

def Duper.Clause.empty : Clause

Equations

• Duper.Clause.empty = { paramNames := #[], bVarTypes := #[], lits := #[] }

def Duper.Clause.fromSingleExpr (paramNames : Array Lean.Name) (e : Lean.Expr) : Clause

Equations

• Duper.Clause.fromSingleExpr paramNames e = { paramNames := paramNames, bVarTypes := #[], lits := #[Duper.Lit.fromSingleExpr e] }

def Duper.Clause.litsToExpr : List Lit → Lean.Expr

Equations

• Duper.Clause.litsToExpr [] = Lean.mkConst `False
• Duper.Clause.litsToExpr [l] = l.toExpr
• Duper.Clause.litsToExpr (l :: ls) = Lean.mkApp2 (Lean.mkConst `Or) l.toExpr (Duper.Clause.litsToExpr ls)

def Duper.Clause.toExpr (c : Clause) : Lean.Expr

Equations

• c.toExpr = Duper.Clause.litsToExpr c.lits.toList

def Duper.Clause.foldM {β : Type v} {m : Type v → Type w} [Monad m] (f : β → Lean.Expr → ClausePos → m β) (init : β) (c : Clause) : m β

Equations

• One or more equations did not get rendered due to their size.

def Duper.Clause.getAtPos! {m : Type → Type u_1} [Monad m] [MonadLiftT Lean.MetaM m] (c : Clause) (pos : ClausePos) : m Lean.Expr

Equations

• c.getAtPos! pos = c.lits[pos.lit]!.getAtPos! { side := pos.side, pos := pos.pos }

def Duper.Clause.mapMUpdateType {m : Type → Type u_1} [instMonad : Monad m] (c : Clause) (f : Lean.Expr → m Lean.Expr) : m Clause

Equations

• c.mapMUpdateType f = do let bVarTypes ← Array.mapM f c.bVarTypes let lits ← Array.mapM (Duper.Lit.mapM f) c.lits pure { paramNames := c.paramNames, bVarTypes := bVarTypes, lits := lits }

def Duper.Clause.instantiateLevelParamsArray (c : Clause) (paramNames : Array Lean.Name) (levels : Array Lean.Level) : Clause

Equations

• One or more equations did not get rendered due to their size.

def Duper.Clause.toForallExpr (c : Clause) : Lean.Expr

Equations

• c.toForallExpr = Array.foldr (fun (ty b : Lean.Expr) => Lean.mkForall Lean.Name.anonymous Lean.BinderInfo.default ty b) c.toExpr c.bVarTypes

def Duper.Clause.toLambdaExpr (c : Clause) : Lean.Expr

Equations

• c.toLambdaExpr = Array.foldr (fun (ty b : Lean.Expr) => Lean.mkLambda Lean.Name.anonymous Lean.BinderInfo.default ty b) c.toExpr c.bVarTypes

def Duper.Clause.fromForallExpr (paramNames : Array Lean.Name) (e : Lean.Expr) : Clause

Equations

• One or more equations did not get rendered due to their size.

def Duper.Clause.fromForallExpr.deForall : Lean.Expr → List Lean.Expr × Lean.Expr

Equations

• Duper.Clause.fromForallExpr.deForall (Lean.Expr.forallE binderName ty body binderInfo) = match Duper.Clause.fromForallExpr.deForall body with | (l, e) => (ty :: l, e)
• Duper.Clause.fromForallExpr.deForall x✝ = ([], x✝)

def Duper.Clause.fromForallExpr.litsFromExpr : Lean.Expr → List Lit

Equations

• Duper.Clause.fromForallExpr.litsFromExpr (((Lean.Expr.const `Or us).app litexpr).app other) = Duper.Lit.fromExpr litexpr :: Duper.Clause.fromForallExpr.litsFromExpr other
• Duper.Clause.fromForallExpr.litsFromExpr (Lean.Expr.const `False us) = []
• Duper.Clause.fromForallExpr.litsFromExpr x✝ = [Duper.Lit.fromExpr x✝]

instance Duper.Clause.instToFormat : Std.ToFormat Clause

Equations

• Duper.Clause.instToFormat = { format := fun (c : Duper.Clause) => Std.format c.toForallExpr }

instance Duper.Clause.instToMessageData : Lean.ToMessageData Clause

Equations

• Duper.Clause.instToMessageData = { toMessageData := fun (c : Duper.Clause) => Lean.MessageData.ofExpr c.toForallExpr }

def Duper.Clause.weight (c : Clause) : Nat

Equations

• c.weight = Array.foldl (fun (acc : Nat) (lit : Duper.Lit) => acc + lit.lhs.weight + lit.rhs.weight) 0 c.lits

def Duper.Clause.selectionPrecedence (c : Clause) (goalDistance : Nat) : Nat

Determines the precedence clause c should have for clause selection. Lower values indicate higher precedence

Equations

• c.selectionPrecedence goalDistance = c.weight + goalDistance

def Duper.Clause.ClauseAndClausePos.format (c : Clause × ClausePos) : Lean.MessageData

Equations

• Duper.Clause.ClauseAndClausePos.format c = Lean.toMessageData "(" ++ Lean.toMessageData c.fst ++ Lean.toMessageData ", " ++ Lean.toMessageData c.snd ++ Lean.toMessageData ")"

instance Duper.Clause.instToMessageDataProdClausePos : Lean.ToMessageData (Clause × ClausePos)

Equations

• Duper.Clause.instToMessageDataProdClausePos = { toMessageData := Duper.Clause.ClauseAndClausePos.format }