Lean.Meta.Tactic.ElimInfo

source

structure Lean.Meta.ElimAltInfo :

Type

name : Lean.Name
numFields : Nat

source

instance Lean.Meta.instReprElimAltInfo :

Repr Lean.Meta.ElimAltInfo

Equations

Lean.Meta.instReprElimAltInfo = { reprPrec := [anonymous] }

source

structure Lean.Meta.ElimInfo :

Type

name : Lean.Name
motivePos : Nat
targetsPos : Array Nat
altsInfo : Array Lean.Meta.ElimAltInfo

source

instance Lean.Meta.instReprElimInfo :

Repr Lean.Meta.ElimInfo

Equations

Lean.Meta.instReprElimInfo = { reprPrec := [anonymous] }

source

def Lean.Meta.getElimInfo (declName : Lean.Name) :

Lean.MetaM Lean.Meta.ElimInfo

Equations

Lean.Meta.getElimInfo declName = do let declInfo ← Lean.getConstInfo declName Lean.Meta.forallTelescopeReducing (Lean.ConstantInfo.type declInfo) fun xs type => let motive := Lean.Expr.getAppFn type; let targets := Lean.Expr.getAppArgs type; let _do_jp := fun y => do let motiveType ← Lean.Meta.inferType motive Lean.Meta.forallTelescopeReducing motiveType fun motiveArgs motiveResultType => let _do_jp := fun y => if Lean.Expr.isSort motiveResultType = true then pure PUnit.unit else Lean.throwError (Lean.toMessageData "motive result type must be a sort" ++ Lean.toMessageData (Lean.indentExpr motiveType) ++ Lean.toMessageData ""); if (Array.size motiveArgs == Array.size targets) = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.throwError (Lean.toMessageData "unexpected number of arguments at motive type" ++ Lean.toMessageData (Lean.indentExpr motiveType) ++ Lean.toMessageData "") _do_jp y let discr ← pure (Array.indexOf? xs motive) match discr with | some motivePos => do let targetsPos ← Array.mapM (fun target => match Array.indexOf? xs target with | none => Lean.throwError (Lean.toMessageData "unexpected eliminator type" ++ Lean.toMessageData (Lean.indentExpr (Lean.ConstantInfo.type declInfo)) ++ Lean.toMessageData "") | some targetPos => pure targetPos.val) targets let altsInfo : Array Lean.Meta.ElimAltInfo := #[] let r ← let col := { start := 0, stop := Array.size xs, step := 1 }; forIn col altsInfo fun i r => let altsInfo := r; let x := Array.getOp xs i; if (x != motive && !Array.contains targets x) = true then do let xDecl ← Lean.Meta.getLocalDecl (Lean.Expr.fvarId! x) if Lean.BinderInfo.isExplicit (Lean.LocalDecl.binderInfo xDecl) = true then do let numFields ← Lean.Meta.forallTelescopeReducing (Lean.LocalDecl.type xDecl) fun args x => pure (Array.size args) let altsInfo : Array Lean.Meta.ElimAltInfo := Array.push altsInfo { name := Lean.LocalDecl.userName xDecl, numFields := numFields } pure PUnit.unit pure (ForInStep.yield altsInfo) else do pure PUnit.unit pure (ForInStep.yield altsInfo) else do pure PUnit.unit pure (ForInStep.yield altsInfo) let x : Array Lean.Meta.ElimAltInfo := r let altsInfo : Array Lean.Meta.ElimAltInfo := x pure { name := declName, motivePos := motivePos.val, targetsPos := targetsPos, altsInfo := altsInfo } | x => Lean.throwError (Lean.toMessageData "unexpected eliminator type" ++ Lean.toMessageData (Lean.indentExpr (Lean.ConstantInfo.type declInfo)) ++ Lean.toMessageData ""); if (Lean.Expr.isFVar motive && Array.all targets (fun a => Lean.Expr.isFVar a) 0 (Array.size targets) && decide (Array.size targets > 0)) = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.throwError (Lean.toMessageData "unexpected eliminator resulting type" ++ Lean.toMessageData (Lean.indentExpr type) ++ Lean.toMessageData "") _do_jp y

source

def Lean.Meta.addImplicitTargets (elimInfo : Lean.Meta.ElimInfo) (targets : Array Lean.Expr) :

Lean.MetaM (Array Lean.Expr)

Equations

Lean.Meta.addImplicitTargets elimInfo targets = (fun collect => Lean.Meta.withNewMCtxDepth do let f ← Lean.Meta.mkConstWithFreshMVarLevels elimInfo.name let a ← Lean.Meta.inferType f let targets ← collect a 0 0 #[] let targets ← Array.mapM Lean.Meta.instantiateMVars targets let r ← forIn targets PUnit.unit fun target r => do let a ← Lean.Meta.hasAssignableMVar target if a = true then do Lean.throwError (Lean.toMessageData "failed to infer implicit target, it contains unresolved metavariables" ++ Lean.toMessageData (Lean.indentExpr target) ++ Lean.toMessageData "") pure (ForInStep.yield PUnit.unit) else do pure PUnit.unit pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure targets) (Lean.Meta.addImplicitTargets.collect elimInfo targets)

source

partial def Lean.Meta.addImplicitTargets.collect (elimInfo : Lean.Meta.ElimInfo) (targets : Array Lean.Expr) (type : Lean.Expr) (argIdx : Nat) (targetIdx : Nat) (targets' : Array Lean.Expr) :

Lean.MetaM (Array Lean.Expr)