opaque Duper.RuleM.inhabitationReasoning : Lean.Option Bool

opaque Duper.RuleM.firstOrderUnifierGenerator : Lean.Option Bool

opaque Duper.RuleM.selFunction : Lean.Option Nat

opaque Duper.RuleM.includeExpensiveRules : Lean.Option Bool

opaque Duper.RuleM.includeDatatypeRules : Lean.Option Bool

opaque Duper.RuleM.includeUnsafeAcyclicity : Lean.Option Bool

def Duper.RuleM.getInhabitationReasoning (opts : Lean.Options) : Bool

Equations

• Duper.RuleM.getInhabitationReasoning opts = Lean.Option.get opts Duper.RuleM.inhabitationReasoning

def Duper.RuleM.getFirstOrderUnifierGenerator (opts : Lean.Options) : Bool

Equations

• Duper.RuleM.getFirstOrderUnifierGenerator opts = Lean.Option.get opts Duper.RuleM.firstOrderUnifierGenerator

def Duper.RuleM.getSelFunction (opts : Lean.Options) : Nat

Equations

• Duper.RuleM.getSelFunction opts = Lean.Option.get opts Duper.RuleM.selFunction

def Duper.RuleM.getIncludeExpensiveRules (opts : Lean.Options) : Bool

Equations

• Duper.RuleM.getIncludeExpensiveRules opts = Lean.Option.get opts Duper.RuleM.includeExpensiveRules

def Duper.RuleM.getIncludeDatatypeRules (opts : Lean.Options) : Bool

Equations

• Duper.RuleM.getIncludeDatatypeRules opts = Lean.Option.get opts Duper.RuleM.includeDatatypeRules

def Duper.RuleM.getIncludeUnsafeAcyclicity (opts : Lean.Options) : Bool

Equations

• Duper.RuleM.getIncludeUnsafeAcyclicity opts = Lean.Option.get opts Duper.RuleM.includeUnsafeAcyclicity

def Duper.RuleM.getInhabitationReasoningM : Lean.CoreM Bool

Equations

• Duper.RuleM.getInhabitationReasoningM = do let opts ← Lean.getOptions pure (Duper.RuleM.getInhabitationReasoning opts)

def Duper.RuleM.getFirstOrderUnifierGeneratorM : Lean.CoreM Bool

Equations

• Duper.RuleM.getFirstOrderUnifierGeneratorM = do let opts ← Lean.getOptions pure (Duper.RuleM.getFirstOrderUnifierGenerator opts)

def Duper.RuleM.getSelFunctionM : Lean.CoreM Nat

Equations

• Duper.RuleM.getSelFunctionM = do let opts ← Lean.getOptions pure (Duper.RuleM.getSelFunction opts)

def Duper.RuleM.getIncludeExpensiveRulesM : Lean.CoreM Bool

Equations

• Duper.RuleM.getIncludeExpensiveRulesM = do let opts ← Lean.getOptions pure (Duper.RuleM.getIncludeExpensiveRules opts)

def Duper.RuleM.getIncludeDatatypeRulesM : Lean.CoreM Bool

Equations

• Duper.RuleM.getIncludeDatatypeRulesM = do let opts ← Lean.getOptions pure (Duper.RuleM.getIncludeDatatypeRules opts)

def Duper.RuleM.getIncludeUnsafeAcyclicityM : Lean.CoreM Bool

Equations

• Duper.RuleM.getIncludeUnsafeAcyclicityM = do let opts ← Lean.getOptions pure (Duper.RuleM.getIncludeUnsafeAcyclicity opts)

structure Duper.RuleM.Context : Type

• order : Lean.Expr → Lean.Expr → Bool → Lean.MetaM Comparison
• symbolPrecMap : SymbolPrecMap
• getNetWeight : Lean.Expr → Lean.Expr → Bool → Lean.MetaM Order.Weight
• skolemSorryName : Lean.Name

instance Duper.RuleM.instInhabitedContext : Inhabited Context

Equations

• Duper.RuleM.instInhabitedContext = { default := { order := default, symbolPrecMap := default, getNetWeight := default, skolemSorryName := default } }

structure Duper.RuleM.ProofParent : Type

• expr : Lean.Expr
• clause : Clause
• paramSubst : Array Lean.Level

instance Duper.RuleM.instInhabitedProofParent : Inhabited ProofParent

Equations

• Duper.RuleM.instInhabitedProofParent = { default := { expr := default, clause := default, paramSubst := default } }

structure Duper.RuleM.SkolemInfo : Type

• expr : Lean.Expr
• params : Array Lean.Name

instance Duper.RuleM.instInhabitedSkolemInfo : Inhabited SkolemInfo

Equations

• Duper.RuleM.instInhabitedSkolemInfo = { default := { expr := default, params := default } }

@[reducible, inline]

abbrev Duper.RuleM.ProofReconstructor : Type

Takes: Proofs of the parent clauses, ProofParent information, the transported Expressions (which will be turned into bvars in the clause) introduced by the rule, and the target clause

Equations

• Duper.RuleM.ProofReconstructor = (List Lean.Expr → List Duper.RuleM.ProofParent → Array Lean.Expr → Duper.Clause → Lean.MetaM Lean.Expr)

structure Duper.RuleM.Proof : Type

• parents : Array ProofParent
• ruleName : String
• mkProof : ProofReconstructor
• transferExprs : Array Lean.Expr

instance Duper.RuleM.instInhabitedProof : Inhabited Proof

Equations

• Duper.RuleM.instInhabitedProof = { default := { parents := default, ruleName := default, mkProof := default, transferExprs := default } }

structure Duper.RuleM.LoadedClause : Type

• clause : Clause
• lmVarIds : Array Lean.LMVarId
• mVarIds : Array Lean.MVarId

structure Duper.RuleM.State : Type

• loadedClauses : Array LoadedClause
• inhabitationClauses : Array LoadedClause
• skolemMap : Std.HashMap Nat SkolemInfo

instance Duper.RuleM.instInhabitedState : Inhabited State

Equations

• Duper.RuleM.instInhabitedState = { default := { loadedClauses := default, inhabitationClauses := default, skolemMap := default } }

@[reducible, inline]

abbrev Duper.RuleM.RuleM (α : Type) : Type

Equations

• Duper.RuleM.RuleM = ReaderT Duper.RuleM.Context (StateRefT' IO.RealWorld Duper.RuleM.State Lean.MetaM)

structure Duper.ClauseStream : Type

• ug : DUnif.UnifierGenerator
• simplifiedGivenClause : Clause
• postUnification : RuleM.RuleM (Option (Clause × RuleM.Proof))
• ruleName : String

@[inline]

def Duper.RuleM.RuleM.run {α : Type} (x : RuleM α) (ctx : Context) (s : State) : Lean.MetaM (α × State)

Equations

• x.run ctx s = (x ctx).run s

@[inline]

def Duper.RuleM.RuleM.run' {α : Type} (x : RuleM α) (ctx : Context) (s : State) : Lean.MetaM α

Equations

• x.run' ctx s = Prod.fst <$> x.run ctx s

def Duper.RuleM.getOrder : RuleM (Lean.Expr → Lean.Expr → Bool → Lean.MetaM Comparison)

Equations

• Duper.RuleM.getOrder = do let __do_lift ← read pure __do_lift.order

def Duper.RuleM.getSymbolPrecMap : RuleM SymbolPrecMap

Equations

• Duper.RuleM.getSymbolPrecMap = do let __do_lift ← read pure __do_lift.symbolPrecMap

def Duper.RuleM.getGetNetWeight : RuleM (Lean.Expr → Lean.Expr → Bool → Lean.MetaM Order.Weight)

Equations

• Duper.RuleM.getGetNetWeight = do let __do_lift ← read pure __do_lift.getNetWeight

def Duper.RuleM.getSkolemSorryName : RuleM Lean.Name

Equations

• Duper.RuleM.getSkolemSorryName = do let __do_lift ← read pure __do_lift.skolemSorryName

def Duper.RuleM.getLoadedClauses : RuleM (Array LoadedClause)

Equations

• Duper.RuleM.getLoadedClauses = do let __do_lift ← get pure __do_lift.loadedClauses

def Duper.RuleM.getInhabitationClauses : RuleM (Array LoadedClause)

Equations

• Duper.RuleM.getInhabitationClauses = do let __do_lift ← get pure __do_lift.inhabitationClauses

def Duper.RuleM.getSkolemMap : RuleM (Std.HashMap Nat SkolemInfo)

Equations

• Duper.RuleM.getSkolemMap = do let __do_lift ← get pure __do_lift.skolemMap

def Duper.RuleM.setLoadedClauses (loadedClauses : Array LoadedClause) : RuleM Unit

Equations

• Duper.RuleM.setLoadedClauses loadedClauses = modify fun (s : Duper.RuleM.State) => { loadedClauses := loadedClauses, inhabitationClauses := s.inhabitationClauses, skolemMap := s.skolemMap }

def Duper.RuleM.setInhabitationClauses (inhabitationClauses : Array LoadedClause) : RuleM Unit

Equations

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

def Duper.RuleM.setState (s : State) : RuleM Unit

Equations

• Duper.RuleM.setState s = modify fun (x : Duper.RuleM.State) => s

def Duper.RuleM.setSkolemMap (skmap : Std.HashMap Nat SkolemInfo) : RuleM Unit

Equations

• Duper.RuleM.setSkolemMap skmap = modify fun (s : Duper.RuleM.State) => { loadedClauses := s.loadedClauses, inhabitationClauses := s.inhabitationClauses, skolemMap := skmap }

def Duper.RuleM.conditionallyModifyingMCtx {α : Type} (x : RuleM (Bool × α)) : RuleM α

Runs x and only modifes the MCtx if the first argument returned by x is true (on failure, does not modify MCtx)

Equations

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

def Duper.RuleM.withoutModifyingLoadedClauses {α : Type} (x : RuleM α) : RuleM α

Equations

• Duper.RuleM.withoutModifyingLoadedClauses x = do let s ← Duper.RuleM.getLoadedClauses tryFinally (Lean.Meta.withoutModifyingMCtx x) (Duper.RuleM.setLoadedClauses s)

def Duper.RuleM.conditionallyModifyingLoadedClauses {α : Type} (x : RuleM (Bool × α)) : RuleM α

Runs x and only modifies loadedClauses if the first argument returned by x is true (on failure, does not modify loadedClauses)

Equations

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

instance Duper.RuleM.instAddMessageContextRuleM : Lean.AddMessageContext RuleM

Equations

• Duper.RuleM.instAddMessageContextRuleM = { addMessageContext := Lean.addMessageContextFull }

def Duper.RuleM.unifierGenerator (l : Array (Lean.Expr × Lean.Expr)) : Lean.MetaM DUnif.UnifierGenerator

Equations

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

def Duper.RuleM.replace (e target replacement : Lean.Expr) : RuleM Lean.Expr

Equations

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

def Duper.RuleM.wrapSort (paramNames : Array Lean.Name) : RuleM Lean.Expr

Equations

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

def Duper.RuleM.unWrapSort (e : Lean.Expr) : Lean.MetaM (Array Lean.Level)

Equations

• Duper.RuleM.unWrapSort e = Lean.Meta.forallTelescope e fun (xs : Array Lean.Expr) (x : Lean.Expr) => do let tys ← Array.mapM Lean.Meta.inferType xs pure (Array.map Lean.Expr.sortLevel! tys)

def Duper.RuleM.loadClauseCore (c : Clause) : RuleM (Array Lean.Expr × MClause)

Suppose c : Clause = ⟨bs, ls⟩, (mVars, m) ← loadClauseCore c then m = c.instantiateRev mVars m ≝ mkAppN c.toForallExpr mVars

Equations

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

def Duper.RuleM.loadClause (c : Clause) : RuleM MClause

Equations

• Duper.RuleM.loadClause c = do let __discr ← Duper.RuleM.loadClauseCore c match __discr with | (fst, mclause) => pure mclause

def Duper.RuleM.loadInhabitationClauseCore (c : Clause) : RuleM (Array Lean.Expr × MClause)

Does the same thing as loadClauseCore but adds c to inhabitationClauses rather than loadedClauses

Equations

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

def Duper.RuleM.loadInhabitationClause (c : Clause) : RuleM MClause

Does the same thing as loadClause but adds c to inhabitationClauses rather than loadedClauses

Equations

• Duper.RuleM.loadInhabitationClause c = do let __discr ← Duper.RuleM.loadInhabitationClauseCore c match __discr with | (fst, mclause) => pure mclause

def Duper.RuleM.prepLoadClause (c : Clause) : RuleM (MClause × LoadedClause)

Returns the MClause that would be returned by calling loadClause c and the Clause × Array MVarId pair that would be added to loadedClauses if loadClause c were called, but does not actually change the set of loaded clauses. The purpose of this function is to process a clause and turn it into an MClause while delaying the decision of whether to actually load it

Equations

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

def Duper.RuleM.neutralizeMClause (c : MClause) (loadedClauses : Array LoadedClause) (transferExprs : Array Lean.Expr) : AbstractMVars.M (Clause × Array ProofParent × Array Lean.Expr)

Equations

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

def Duper.RuleM.neutralizeMClauseInhabitedReasoningOn (c : MClause) (loadedClauses inhabitationClauses : Array LoadedClause) (transferExprs : Array Lean.Expr) (mvarIdsToRemove : List Lean.MVarId) : AbstractMVars.M (Clause × Array ProofParent × Array Lean.Expr)

Equations

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

def Duper.RuleM.yieldClause (mc : MClause) (ruleName : String) (mkProof : Option ProofReconstructor) (transferExprs : Array Lean.Expr := #[]) (mvarIdsToRemove : List Lean.MVarId := []) : RuleM (Clause × Proof)

Equations

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

def Duper.RuleM.compare (s t : Lean.Expr) (alreadyReduced : Bool) : RuleM Comparison

Equations

• Duper.RuleM.compare s t alreadyReduced = do let ord ← Duper.RuleM.getOrder liftM (ord s t alreadyReduced)