opaque DUnif.dUnifDbgOn : Lean.Option Bool

@[inline]

def DUnif.getDUnifDbgOn : Lean.CoreM Bool

Equations

• DUnif.getDUnifDbgOn = do let opts ← Lean.getOptions pure (Lean.Option.get opts DUnif.dUnifDbgOn)

structure DUnif.UnifEq : Type

• lhs : Lean.Expr
• rhs : Lean.Expr
• lflex : Bool
• rflex : Bool

instance DUnif.instHashableUnifEq : Hashable UnifEq

Equations

• DUnif.instHashableUnifEq = { hash := DUnif.instHashableUnifEq.hash }

def DUnif.instHashableUnifEq.hash : UnifEq → UInt64

Equations

• DUnif.instHashableUnifEq.hash { lhs := a, rhs := a_1, lflex := a_2, rflex := a_3 } = mixHash (mixHash (mixHash (mixHash 0 (hash a)) (hash a_1)) (hash a_2)) (hash a_3)

def DUnif.instInhabitedUnifEq.default : UnifEq

Equations

• DUnif.instInhabitedUnifEq.default = { lhs := default, rhs := default, lflex := default, rflex := default }

instance DUnif.instInhabitedUnifEq : Inhabited UnifEq

Equations

• DUnif.instInhabitedUnifEq = { default := DUnif.instInhabitedUnifEq.default }

instance DUnif.instBEqUnifEq : BEq UnifEq

Equations

• DUnif.instBEqUnifEq = { beq := DUnif.instBEqUnifEq.beq }

def DUnif.instBEqUnifEq.beq : UnifEq → UnifEq → Bool

Equations

• DUnif.instBEqUnifEq.beq { lhs := a, rhs := a_1, lflex := a_2, rflex := a_3 } { lhs := b, rhs := b_1, lflex := b_2, rflex := b_3 } = (a == b && (a_1 == b_1 && (a_2 == b_2 && a_3 == b_3)))
• DUnif.instBEqUnifEq.beq x✝¹ x✝ = false

def DUnif.instReprUnifEq.repr : UnifEq → Nat → Std.Format

Equations

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

instance DUnif.instReprUnifEq : Repr UnifEq

Equations

• DUnif.instReprUnifEq = { reprPrec := DUnif.instReprUnifEq.repr }

def DUnif.UnifEq.toString : UnifEq → String

Equations

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

def DUnif.UnifEq.toString.h (b : Bool) : String

Equations

• DUnif.UnifEq.toString.h b = if b = true then "Flex" else "Rigid"

instance DUnif.instToStringUnifEq : ToString UnifEq

Equations

• DUnif.instToStringUnifEq = { toString := DUnif.UnifEq.toString }

def DUnif.UnifEq.toMessageData : UnifEq → Lean.MessageData

Equations

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

def DUnif.UnifEq.toMessageData.h (b : Bool) : String

Equations

• DUnif.UnifEq.toMessageData.h b = if b = true then "Flex" else "Rigid"

instance DUnif.instToMessageDataUnifEq : Lean.ToMessageData UnifEq

Equations

• DUnif.instToMessageDataUnifEq = { toMessageData := DUnif.UnifEq.toMessageData }

def DUnif.UnifEq.fromExprPair (e1 e2 : Lean.Expr) : UnifEq

Equations

• DUnif.UnifEq.fromExprPair e1 e2 = { lhs := e1, rhs := e2, lflex := true, rflex := true }

def DUnif.UnifEq.swapSide (ue : UnifEq) : UnifEq

Equations

• ue.swapSide = { lhs := ue.rhs, rhs := ue.lhs, lflex := ue.rflex, rflex := ue.lflex }

inductive DUnif.ParentRule : Type

• FromExprPairs : Array (Lean.Expr × Lean.Expr) → ParentRule
• Succeed : ParentRule
• Delete : UnifEq → ParentRule
• OracleSucc : UnifEq → ParentRule
• OracleFail : UnifEq → ParentRule
• Decompose : UnifEq → ParentRule
• ForallToLambda : UnifEq → Nat → ParentRule
• OracleInst : UnifEq → ParentRule
• Iteration : UnifEq → Lean.Expr → (argn narg : Nat) → Lean.Expr → ParentRule
• JPProjection : UnifEq → Lean.Expr → (arg : Nat) → Lean.Expr → ParentRule
• HuetProjection : UnifEq → Lean.Expr → (arg : Nat) → Lean.Expr → ParentRule
• ImitForall : UnifEq → Lean.Expr → Lean.Expr → ParentRule
• ImitProj : UnifEq → Lean.Expr → (idx : Nat) → Lean.Expr → ParentRule
• Imitation : UnifEq → (flex rigid : Lean.Expr) → Lean.Expr → ParentRule
• Identification : UnifEq → (e1 e2 : Lean.Expr) → Lean.Expr → Lean.Expr → ParentRule
• Elimination : UnifEq → Lean.Expr → Array Nat → Lean.Expr → ParentRule

def DUnif.instInhabitedParentRule.default : ParentRule

Equations

• DUnif.instInhabitedParentRule.default = DUnif.ParentRule.FromExprPairs default

instance DUnif.instInhabitedParentRule : Inhabited ParentRule

Equations

• DUnif.instInhabitedParentRule = { default := DUnif.instInhabitedParentRule.default }

instance DUnif.instBEqParentRule : BEq ParentRule

Equations

• DUnif.instBEqParentRule = { beq := DUnif.instBEqParentRule.beq }

def DUnif.instBEqParentRule.beq : ParentRule → ParentRule → Bool

Equations

• One or more equations did not get rendered due to their size.
• DUnif.instBEqParentRule.beq (DUnif.ParentRule.FromExprPairs a) (DUnif.ParentRule.FromExprPairs b) = (a == b)
• DUnif.instBEqParentRule.beq DUnif.ParentRule.Succeed DUnif.ParentRule.Succeed = true
• DUnif.instBEqParentRule.beq (DUnif.ParentRule.Delete a) (DUnif.ParentRule.Delete b) = (a == b)
• DUnif.instBEqParentRule.beq (DUnif.ParentRule.OracleSucc a) (DUnif.ParentRule.OracleSucc b) = (a == b)
• DUnif.instBEqParentRule.beq (DUnif.ParentRule.OracleFail a) (DUnif.ParentRule.OracleFail b) = (a == b)
• DUnif.instBEqParentRule.beq (DUnif.ParentRule.Decompose a) (DUnif.ParentRule.Decompose b) = (a == b)
• DUnif.instBEqParentRule.beq (DUnif.ParentRule.ForallToLambda a a_1) (DUnif.ParentRule.ForallToLambda b b_1) = (a == b && a_1 == b_1)
• DUnif.instBEqParentRule.beq (DUnif.ParentRule.OracleInst a) (DUnif.ParentRule.OracleInst b) = (a == b)
• DUnif.instBEqParentRule.beq (DUnif.ParentRule.JPProjection a a_1 a_2 a_3) (DUnif.ParentRule.JPProjection b b_1 b_2 b_3) = (a == b && (a_1 == b_1 && (a_2 == b_2 && a_3 == b_3)))
• DUnif.instBEqParentRule.beq (DUnif.ParentRule.HuetProjection a a_1 a_2 a_3) (DUnif.ParentRule.HuetProjection b b_1 b_2 b_3) = (a == b && (a_1 == b_1 && (a_2 == b_2 && a_3 == b_3)))
• DUnif.instBEqParentRule.beq (DUnif.ParentRule.ImitForall a a_1 a_2) (DUnif.ParentRule.ImitForall b b_1 b_2) = (a == b && (a_1 == b_1 && a_2 == b_2))
• DUnif.instBEqParentRule.beq (DUnif.ParentRule.ImitProj a a_1 a_2 a_3) (DUnif.ParentRule.ImitProj b b_1 b_2 b_3) = (a == b && (a_1 == b_1 && (a_2 == b_2 && a_3 == b_3)))
• DUnif.instBEqParentRule.beq (DUnif.ParentRule.Imitation a a_1 a_2 a_3) (DUnif.ParentRule.Imitation b b_1 b_2 b_3) = (a == b && (a_1 == b_1 && (a_2 == b_2 && a_3 == b_3)))
• DUnif.instBEqParentRule.beq (DUnif.ParentRule.Elimination a a_1 a_2 a_3) (DUnif.ParentRule.Elimination b b_1 b_2 b_3) = (a == b && (a_1 == b_1 && (a_2 == b_2 && a_3 == b_3)))
• DUnif.instBEqParentRule.beq x✝¹ x✝ = false

def DUnif.ParentRule.toString : ParentRule → String

Equations

• One or more equations did not get rendered due to their size.
• (DUnif.ParentRule.FromExprPairs arr).toString = toString "From " ++ toString arr
• DUnif.ParentRule.Succeed.toString = "Succeed"
• (DUnif.ParentRule.Delete ue).toString = toString "Delete " ++ toString ue
• (DUnif.ParentRule.OracleSucc ue).toString = toString "OracleSucc " ++ toString ue
• (DUnif.ParentRule.OracleFail ue).toString = toString "OracleFail " ++ toString ue
• (DUnif.ParentRule.Decompose ue).toString = toString "Decompose " ++ toString ue
• (DUnif.ParentRule.ForallToLambda ue n).toString = toString "ForallToLambda " ++ toString ue ++ toString " for " ++ toString n ++ toString " binders"
• (DUnif.ParentRule.OracleInst ue).toString = toString "OracleInst " ++ toString ue
• (DUnif.ParentRule.ImitForall ue F b).toString = toString "ImitForall of " ++ toString F ++ toString " in " ++ toString ue ++ toString " binding " ++ toString b

instance DUnif.instToStringParentRule : ToString ParentRule

Equations

• DUnif.instToStringParentRule = { toString := DUnif.ParentRule.toString }

def DUnif.ParentRule.toMessageData : ParentRule → Lean.MessageData

Equations

• One or more equations did not get rendered due to their size.
• (DUnif.ParentRule.FromExprPairs arr).toMessageData = (Lean.toMessageData "From ").compose (Duper.ArrayToMessageData arr Duper.ExprPairToMessageData)
• DUnif.ParentRule.Succeed.toMessageData = (Lean.MessageData.ofFormat ∘ Std.format) "Succeed"
• (DUnif.ParentRule.Delete ue).toMessageData = Lean.toMessageData "Delete " ++ Lean.toMessageData ue
• (DUnif.ParentRule.OracleSucc ue).toMessageData = Lean.toMessageData "OracleSucc " ++ Lean.toMessageData ue
• (DUnif.ParentRule.OracleFail ue).toMessageData = Lean.toMessageData "OracleFail " ++ Lean.toMessageData ue
• (DUnif.ParentRule.Decompose ue).toMessageData = Lean.toMessageData "Decompose " ++ Lean.toMessageData ue
• (DUnif.ParentRule.OracleInst ue).toMessageData = Lean.toMessageData "OracleInst " ++ Lean.toMessageData ue

instance DUnif.instToMessageDataParentRule : Lean.ToMessageData ParentRule

Equations

• DUnif.instToMessageDataParentRule = { toMessageData := DUnif.ParentRule.toMessageData }

structure DUnif.UnifProblem : Type

• prioritized : Array UnifEq
• rigidrigid : Array UnifEq
• flexrigid : Array UnifEq
• flexflex : Array UnifEq
• checked : Bool
• mctx : Lean.MetavarContext
• identVar : Std.HashSet Lean.Expr
• elimVar : Std.HashSet Lean.Expr
• parentRules : Lean.PersistentArray ParentRule
• parentClauses : Lean.PersistentArray Nat
• trackedExpr : Array Lean.Expr

def DUnif.instInhabitedUnifProblem.default : UnifProblem

Equations

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

instance DUnif.instInhabitedUnifProblem : Inhabited UnifProblem

Equations

• DUnif.instInhabitedUnifProblem = { default := DUnif.instInhabitedUnifProblem.default }

def DUnif.UnifProblem.toString : UnifProblem → String

Equations

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

instance DUnif.instToStringUnifProblem : ToString UnifProblem

Equations

• DUnif.instToStringUnifProblem = { toString := DUnif.UnifProblem.toString }

def DUnif.UnifProblem.toMessageData : UnifProblem → Lean.MessageData

Equations

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

instance DUnif.instToMessageDataUnifProblem : Lean.ToMessageData UnifProblem

Equations

• DUnif.instToMessageDataUnifProblem = { toMessageData := DUnif.UnifProblem.toMessageData }

def DUnif.UnifProblem.pushPrioritized (p : UnifProblem) (e : UnifEq) : UnifProblem

Equations

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

def DUnif.UnifProblem.appendPrioritized (p : UnifProblem) (es : Array UnifEq) : UnifProblem

Equations

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

def DUnif.UnifProblem.pushUnchecked (p : UnifProblem) (e : UnifEq) (is_prio : Bool := false) : UnifProblem

Equations

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

def DUnif.UnifProblem.appendUnchecked (p : UnifProblem) (es : Array UnifEq) (is_prio : Bool := false) : UnifProblem

Equations

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

def DUnif.UnifProblem.pushChecked (p : UnifProblem) (e : UnifEq) (isprio : Bool) : UnifProblem

Equations

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

@[inline]

def DUnif.UnifProblem.pushParentRule (p : UnifProblem) (pr : ParentRule) : UnifProblem

Equations

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

@[inline]

def DUnif.UnifProblem.pushParentRuleIfDbgOn (p : UnifProblem) (pr : ParentRule) : Lean.CoreM UnifProblem

Equations

• p.pushParentRuleIfDbgOn pr = do let __do_lift ← DUnif.getDUnifDbgOn if __do_lift = true then pure (p.pushParentRule pr) else pure p

@[inline]

def DUnif.UnifProblem.dropParentRulesButLast (p : UnifProblem) (n : Nat) : UnifProblem

Equations

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

@[inline]

def DUnif.UnifProblem.pushParentClause (p : UnifProblem) (c : Nat) : UnifProblem

Equations

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

@[inline]

def DUnif.UnifProblem.pushParentClauseIfDbgOn (p : UnifProblem) (c : Nat) : Lean.CoreM UnifProblem

Equations

• p.pushParentClauseIfDbgOn c = do let __do_lift ← DUnif.getDUnifDbgOn if __do_lift = true then pure (p.pushParentClause c) else pure p

@[inline]

def DUnif.UnifProblem.appendTrackedExpr (p : UnifProblem) (tr : Array Lean.Expr) : UnifProblem

Equations

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

@[inline]

def DUnif.UnifProblem.pushTrackedExprIfDbgOn (p : UnifProblem) (tr : Array Lean.Expr) : Lean.CoreM UnifProblem

Equations

• p.pushTrackedExprIfDbgOn tr = do let __do_lift ← DUnif.getDUnifDbgOn if __do_lift = true then pure (p.appendTrackedExpr tr) else pure p

def DUnif.UnifProblem.fromExprPairs (l : Array (Lean.Expr × Lean.Expr)) : Lean.MetaM (Option UnifProblem)

Equations

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

def DUnif.UnifProblem.pop? (p : UnifProblem) : Option (UnifEq × UnifProblem)

Equations

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

def DUnif.UnifProblem.instantiateTrackedExpr (p : UnifProblem) : Lean.MetaM UnifProblem

Equations

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

inductive DUnif.StructType : Type

• Const : Nat → Nat → Nat → StructType
• Proj : Nat → Nat → Nat → (innerTy outerTy : Lean.Expr) → (name : Lean.Name) → (idx : Nat) → StructType
• Bound : Nat → Nat → Nat → StructType
• MVar : Nat → Nat → Nat → StructType
• Other : Nat → Nat → Nat → StructType

instance DUnif.instHashableStructType : Hashable StructType

Equations

• DUnif.instHashableStructType = { hash := DUnif.instHashableStructType.hash }

def DUnif.instHashableStructType.hash : StructType → UInt64

Equations

• One or more equations did not get rendered due to their size.
• DUnif.instHashableStructType.hash (DUnif.StructType.Const a a_1 a_2) = mixHash (mixHash (mixHash 0 (hash a)) (hash a_1)) (hash a_2)
• DUnif.instHashableStructType.hash (DUnif.StructType.Bound a a_1 a_2) = mixHash (mixHash (mixHash 2 (hash a)) (hash a_1)) (hash a_2)
• DUnif.instHashableStructType.hash (DUnif.StructType.MVar a a_1 a_2) = mixHash (mixHash (mixHash 3 (hash a)) (hash a_1)) (hash a_2)
• DUnif.instHashableStructType.hash (DUnif.StructType.Other a a_1 a_2) = mixHash (mixHash (mixHash 4 (hash a)) (hash a_1)) (hash a_2)

instance DUnif.instInhabitedStructType : Inhabited StructType

Equations

• DUnif.instInhabitedStructType = { default := DUnif.instInhabitedStructType.default }

def DUnif.instInhabitedStructType.default : StructType

Equations

• DUnif.instInhabitedStructType.default = DUnif.StructType.Const default default default

instance DUnif.instBEqStructType : BEq StructType

Equations

• DUnif.instBEqStructType = { beq := DUnif.instBEqStructType.beq }

def DUnif.instBEqStructType.beq : StructType → StructType → Bool

Equations

• One or more equations did not get rendered due to their size.
• DUnif.instBEqStructType.beq (DUnif.StructType.Const a a_1 a_2) (DUnif.StructType.Const b b_1 b_2) = (a == b && (a_1 == b_1 && a_2 == b_2))
• DUnif.instBEqStructType.beq (DUnif.StructType.Bound a a_1 a_2) (DUnif.StructType.Bound b b_1 b_2) = (a == b && (a_1 == b_1 && a_2 == b_2))
• DUnif.instBEqStructType.beq (DUnif.StructType.MVar a a_1 a_2) (DUnif.StructType.MVar b b_1 b_2) = (a == b && (a_1 == b_1 && a_2 == b_2))
• DUnif.instBEqStructType.beq (DUnif.StructType.Other a a_1 a_2) (DUnif.StructType.Other b b_1 b_2) = (a == b && (a_1 == b_1 && a_2 == b_2))
• DUnif.instBEqStructType.beq x✝¹ x✝ = false

instance DUnif.instReprStructType : Repr StructType

Equations

• DUnif.instReprStructType = { reprPrec := DUnif.instReprStructType.repr }

def DUnif.instReprStructType.repr : StructType → Nat → Std.Format

Equations

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

instance DUnif.instToStringStructType : ToString StructType

Equations

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

def DUnif.StructType.getLambdaForall : StructType → Nat × Nat

Equations

• (DUnif.StructType.Const a a_1 a_2).getLambdaForall = (a, a_1)
• (DUnif.StructType.Proj a a_1 a_2 a_3 a_4 a_5 a_6).getLambdaForall = (a, a_1)
• (DUnif.StructType.Bound a a_1 a_2).getLambdaForall = (a, a_1)
• (DUnif.StructType.MVar a a_1 a_2).getLambdaForall = (a, a_1)
• (DUnif.StructType.Other a a_1 a_2).getLambdaForall = (a, a_1)

def DUnif.StructType.getNArgs : StructType → Nat

Equations

• (DUnif.StructType.Const a a_1 a_2).getNArgs = a_2
• (DUnif.StructType.Proj a a_1 a_2 a_3 a_4 a_5 a_6).getNArgs = a_2
• (DUnif.StructType.Bound a a_1 a_2).getNArgs = a_2
• (DUnif.StructType.MVar a a_1 a_2).getNArgs = a_2
• (DUnif.StructType.Other a a_1 a_2).getNArgs = a_2

def DUnif.StructType.isFlex : StructType → Bool

Equations

• (DUnif.StructType.Const a a_1 a_2).isFlex = false
• (DUnif.StructType.Proj a a_1 a_2 a_3 a_4 a_5 a_6).isFlex = false
• (DUnif.StructType.Bound a a_1 a_2).isFlex = false
• (DUnif.StructType.MVar a a_1 a_2).isFlex = true
• (DUnif.StructType.Other a a_1 a_2).isFlex = false

def DUnif.StructType.isRigid : StructType → Bool

Equations

• (DUnif.StructType.Const a a_1 a_2).isRigid = true
• (DUnif.StructType.Proj a a_1 a_2 a_3 a_4 a_5 a_6).isRigid = true
• (DUnif.StructType.Bound a a_1 a_2).isRigid = true
• (DUnif.StructType.MVar a a_1 a_2).isRigid = false
• (DUnif.StructType.Other a a_1 a_2).isRigid = true

def DUnif.projName! : Lean.Expr → Lean.Name

Equations

• DUnif.projName! (Lean.Expr.proj n idx struct) = n
• DUnif.projName! x✝ = panicWithPosWithDecl "Duper.DUnif.UnifProblem" "DUnif.projName!" 361 18 "proj expression expected"

def DUnif.structInfo (p : UnifProblem) (e : Lean.Expr) : Lean.MetaM (Lean.Expr × StructType)

Equations

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

inductive DUnif.UnifRuleResult : Type

• NewArray : Array UnifProblem → UnifRuleResult
• NewLazyList : Duper.LazyList (Lean.MetaM (Array UnifProblem)) → UnifRuleResult
• Succeed : UnifRuleResult