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.hashUnifEq✝ }

instance DUnif.instInhabitedUnifEq : Inhabited UnifEq

Equations

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

instance DUnif.instBEqUnifEq : BEq UnifEq

Equations

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

instance DUnif.instReprUnifEq : Repr UnifEq

Equations

• DUnif.instReprUnifEq = { reprPrec := DUnif.reprUnifEq✝ }

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

instance DUnif.instInhabitedParentRule : Inhabited ParentRule

Equations

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

instance DUnif.instBEqParentRule : BEq ParentRule

Equations

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

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 ++ toString ""
• DUnif.ParentRule.Succeed.toString = "Succeed"
• (DUnif.ParentRule.Delete ue).toString = toString "Delete " ++ toString ue ++ toString ""
• (DUnif.ParentRule.OracleSucc ue).toString = toString "OracleSucc " ++ toString ue ++ toString ""
• (DUnif.ParentRule.OracleFail ue).toString = toString "OracleFail " ++ toString ue ++ toString ""
• (DUnif.ParentRule.Decompose ue).toString = toString "Decompose " ++ toString ue ++ toString ""
• (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 ++ toString ""
• (DUnif.ParentRule.ImitForall ue F b).toString = toString "ImitForall of " ++ toString F ++ toString " in " ++ toString ue ++ toString " binding " ++ toString b ++ toString ""

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 ++ Lean.toMessageData ""
• (DUnif.ParentRule.OracleSucc ue).toMessageData = Lean.toMessageData "OracleSucc " ++ Lean.toMessageData ue ++ Lean.toMessageData ""
• (DUnif.ParentRule.OracleFail ue).toMessageData = Lean.toMessageData "OracleFail " ++ Lean.toMessageData ue ++ Lean.toMessageData ""
• (DUnif.ParentRule.Decompose ue).toMessageData = Lean.toMessageData "Decompose " ++ Lean.toMessageData ue ++ Lean.toMessageData ""
• (DUnif.ParentRule.OracleInst ue).toMessageData = Lean.toMessageData "OracleInst " ++ Lean.toMessageData ue ++ Lean.toMessageData ""

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

instance DUnif.instInhabitedUnifProblem : Inhabited UnifProblem

Equations

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

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.hashStructType✝ }

instance DUnif.instInhabitedStructType : Inhabited StructType

Equations

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

instance DUnif.instBEqStructType : BEq StructType

Equations

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

instance DUnif.instReprStructType : Repr StructType

Equations

• DUnif.instReprStructType = { reprPrec := DUnif.reprStructType✝ }

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