Lean.Meta.ACLt

source

def Lean.Expr.ctorWeight :

Lean.Expr → UInt8

Equations

Lean.Expr.ctorWeight x = match x with | Lean.Expr.bvar x x_1 => 0 | Lean.Expr.fvar x x_1 => 1 | Lean.Expr.mvar x x_1 => 2 | Lean.Expr.sort x x_1 => 3 | Lean.Expr.const x x_1 x_2 => 4 | Lean.Expr.lit x x_1 => 5 | Lean.Expr.mdata x x_1 x_2 => 6 | Lean.Expr.proj x x_1 x_2 x_3 => 7 | Lean.Expr.app x x_1 x_2 => 8 | Lean.Expr.lam x x_1 x_2 x_3 => 9 | Lean.Expr.forallE x x_1 x_2 x_3 => 10 | Lean.Expr.letE x x_1 x_2 x_3 x_4 => 11

source

unsafe def Lean.Meta.ACLt.lt (a : Lean.Expr) (b : Lean.Expr) :

Lean.MetaM Bool

Equations

Lean.Meta.ACLt.lt a b = (fun ltPair lpo => if (ptrAddrUnsafe a == ptrAddrUnsafe b) = true then pure false else if Lean.Expr.isMData a = true then Lean.Meta.ACLt.lt (Lean.Expr.mdataExpr! a) b else if Lean.Expr.isMData b = true then Lean.Meta.ACLt.lt a (Lean.Expr.mdataExpr! b) else lpo a b) Lean.Meta.ACLt.lt.ltPair Lean.Meta.ACLt.lt.ltApp Lean.Meta.ACLt.lt.lexSameCtor Lean.Meta.ACLt.lt.lex Lean.Meta.ACLt.lt.allChildrenLt Lean.Meta.ACLt.lt.someChildGe Lean.Meta.ACLt.lt.lpo

source

unsafe def Lean.Meta.ACLt.lt.ltPair (a₁ : Lean.Expr) (a₂ : Lean.Expr) (b₁ : Lean.Expr) (b₂ : Lean.Expr) :

Lean.MetaM Bool

Equations

Lean.Meta.ACLt.lt.ltPair a₁ a₂ b₁ b₂ = do let a ← Lean.Meta.ACLt.lt a₁ b₁ if a = true then pure true else do let a ← Lean.Meta.ACLt.lt b₁ a₁ if a = true then pure false else Lean.Meta.ACLt.lt a₂ b₂

source

unsafe def Lean.Meta.ACLt.lt.ltApp (a : Lean.Expr) (b : Lean.Expr) :

Lean.MetaM Bool

Equations

Lean.Meta.ACLt.lt.ltApp a b = let aFn := Lean.Expr.getAppFn a; let bFn := Lean.Expr.getAppFn b; do let a ← Lean.Meta.ACLt.lt aFn bFn if a = true then pure true else do let a ← Lean.Meta.ACLt.lt bFn aFn if a = true then pure false else let aArgs := Lean.Expr.getAppArgs a; let bArgs := Lean.Expr.getAppArgs b; if Array.size aArgs < Array.size bArgs then pure true else if Array.size aArgs > Array.size bArgs then pure false else do let a ← Lean.Meta.getFunInfoNArgs aFn (Array.size aArgs) let infos : Array Lean.Meta.ParamInfo := a.paramInfo let r ← let col := { start := 0, stop := Array.size infos, step := 1 }; forIn col { fst := none, snd := PUnit.unit } fun i r => let r := r.snd; if (!Lean.Meta.ParamInfo.isInstImplicit (Array.getOp infos i)) = true then do let a ← Lean.Meta.ACLt.lt (Array.getOp aArgs i) (Array.getOp bArgs i) if a = true then pure (ForInStep.done { fst := some true, snd := PUnit.unit }) else do let a ← Lean.Meta.ACLt.lt (Array.getOp bArgs i) (Array.getOp aArgs i) if a = true then pure (ForInStep.done { fst := some false, snd := PUnit.unit }) else do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := PUnit.unit }) else do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := PUnit.unit }) let x : PUnit := r.snd let _do_jp : PUnit → Lean.MetaM Bool := fun y => do let r ← let col := { start := Array.size infos, stop := Array.size aArgs, step := 1 }; forIn col { fst := none, snd := PUnit.unit } fun i r => let r := r.snd; do let a ← Lean.Meta.ACLt.lt (Array.getOp aArgs i) (Array.getOp bArgs i) if a = true then pure (ForInStep.done { fst := some true, snd := PUnit.unit }) else do let a ← Lean.Meta.ACLt.lt (Array.getOp bArgs i) (Array.getOp aArgs i) if a = true then pure (ForInStep.done { fst := some false, snd := PUnit.unit }) else do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := PUnit.unit }) let x : PUnit := r.snd let _do_jp : PUnit → Lean.MetaM Bool := fun y => pure false match r.fst with | none => do let y ← pure PUnit.unit _do_jp y | some a => pure a match r.fst with | none => do let y ← pure PUnit.unit _do_jp y | some a => pure a

source

unsafe def Lean.Meta.ACLt.lt.lexSameCtor (a : Lean.Expr) (b : Lean.Expr) :

Lean.MetaM Bool

Equations

Lean.Meta.ACLt.lt.lexSameCtor a b = match a with | Lean.Expr.bvar i x => pure (decide (i < Lean.Expr.bvarIdx! b)) | Lean.Expr.fvar id x => pure (Lean.Name.lt id.name (Lean.Expr.fvarId! b).name) | Lean.Expr.mvar id x => pure (Lean.Name.lt id.name (Lean.Expr.mvarId! b).name) | Lean.Expr.sort u x => pure (Lean.Level.normLt u (Lean.Expr.sortLevel! b)) | Lean.Expr.const n x x_1 => pure (Lean.Name.lt n (Lean.Expr.constName! b)) | Lean.Expr.lit v x => pure (Lean.Literal.lt v (Lean.Expr.litValue! b)) | Lean.Expr.proj x i e x_1 => if (i != Lean.Expr.projIdx! b) = true then pure (decide (i < Lean.Expr.projIdx! b)) else Lean.Meta.ACLt.lt e (Lean.Expr.projExpr! b) | Lean.Expr.app x x_1 x_2 => Lean.Meta.ACLt.lt.ltApp a b | Lean.Expr.lam x d e x_1 => Lean.Meta.ACLt.lt.ltPair d e (Lean.Expr.bindingDomain! b) (Lean.Expr.bindingBody! b) | Lean.Expr.forallE x d e x_1 => Lean.Meta.ACLt.lt.ltPair d e (Lean.Expr.bindingDomain! b) (Lean.Expr.bindingBody! b) | Lean.Expr.letE x x_1 v e x_2 => Lean.Meta.ACLt.lt.ltPair v e (Lean.Expr.letValue! b) (Lean.Expr.letBody! b) | Lean.Expr.mdata x x_1 x_2 => panicWithPosWithDecl "Lean.Meta.ACLt" "Lean.Meta.ACLt.lt.lexSameCtor" 111 31 "unreachable code has been reached"

source

unsafe def Lean.Meta.ACLt.lt.lex (a : Lean.Expr) (b : Lean.Expr) :

Lean.MetaM Bool

Equations

Lean.Meta.ACLt.lt.lex a b = if Lean.Expr.ctorWeight a < Lean.Expr.ctorWeight b then pure true else if Lean.Expr.ctorWeight a > Lean.Expr.ctorWeight b then pure false else Lean.Meta.ACLt.lt.lexSameCtor a b

source

unsafe def Lean.Meta.ACLt.lt.allChildrenLt (a : Lean.Expr) (b : Lean.Expr) :

Lean.MetaM Bool

Equations

Lean.Meta.ACLt.lt.allChildrenLt a b = match a with | Lean.Expr.proj x x_1 e x_2 => Lean.Meta.ACLt.lt e b | Lean.Expr.app x x_1 x_2 => Lean.Expr.withApp a fun f args => do let a ← Lean.Meta.getFunInfoNArgs f (Array.size args) let infos : Array Lean.Meta.ParamInfo := a.paramInfo let r ← let col := { start := 0, stop := Array.size infos, step := 1 }; forIn col { fst := none, snd := PUnit.unit } fun i r => let r := r.snd; if (!Lean.Meta.ParamInfo.isInstImplicit (Array.getOp infos i)) = true then do let a ← Lean.Meta.ACLt.lt (Array.getOp args i) b if (!a) = true then pure (ForInStep.done { fst := some false, snd := PUnit.unit }) else do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := PUnit.unit }) else do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := PUnit.unit }) let x : PUnit := r.snd let _do_jp : PUnit → Lean.MetaM Bool := fun y => do let r ← let col := { start := Array.size infos, stop := Array.size args, step := 1 }; forIn col { fst := none, snd := PUnit.unit } fun i r => let r := r.snd; do let a ← Lean.Meta.ACLt.lt (Array.getOp args i) b if (!a) = true then pure (ForInStep.done { fst := some false, snd := PUnit.unit }) else do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := PUnit.unit }) let x : PUnit := r.snd let _do_jp : PUnit → Lean.MetaM Bool := fun y => pure true match r.fst with | none => do let y ← pure PUnit.unit _do_jp y | some a => pure a match r.fst with | none => do let y ← pure PUnit.unit _do_jp y | some a => pure a | Lean.Expr.lam x d e x_1 => Lean.Meta.ACLt.lt d b <&&> Lean.Meta.ACLt.lt e b | Lean.Expr.forallE x d e x_1 => Lean.Meta.ACLt.lt d b <&&> Lean.Meta.ACLt.lt e b | Lean.Expr.letE x x_1 v e x_2 => Lean.Meta.ACLt.lt v b <&&> Lean.Meta.ACLt.lt e b | x => pure true

source

unsafe def Lean.Meta.ACLt.lt.someChildGe (a : Lean.Expr) (b : Lean.Expr) :

Lean.MetaM Bool

Equations

Lean.Meta.ACLt.lt.someChildGe a b = do let a ← Lean.Meta.ACLt.lt.allChildrenLt a b pure !a

source

unsafe def Lean.Meta.ACLt.lt.lpo (a : Lean.Expr) (b : Lean.Expr) :

Lean.MetaM Bool

Equations

Lean.Meta.ACLt.lt.lpo a b = do let a ← Lean.Meta.ACLt.lt.someChildGe b a if a = true then pure true else if Lean.Expr.ctorWeight a > Lean.Expr.ctorWeight b then pure false else do let a ← Lean.Meta.ACLt.lt.allChildrenLt a b if (!a) = true then pure false else if Lean.Expr.ctorWeight a < Lean.Expr.ctorWeight b then pure true else Lean.Meta.ACLt.lt.lexSameCtor a b

source

@[implementedBy Lean.Meta.ACLt.lt]

constant Lean.Meta.Expr.acLt :

Lean.Expr → Lean.Expr → Lean.MetaM Bool