Lean.Meta.Tactic.Split

Lean.Meta.Split.applyMatchSplitter mvarId matcherDeclName us params discrs = do let discr ← Lean.Meta.getMatcherInfo? matcherDeclName match discr with | some info => do let matchEqns ← Lean.Meta.Match.getEquationsFor matcherDeclName let us : Array Lean.Level := us let _do_jp : Array Lean.Level → PUnit → Lean.MetaM (List Lean.MVarId) := fun us y => let splitter := Lean.mkAppN (Lean.mkConst matchEqns.splitterName (Array.toList us)) params; do let a ← Lean.Meta.inferType splitter let a ← Lean.Meta.whnfForall a let motiveType : Lean.Expr := Lean.Expr.bindingDomain! a let discr ← Lean.Meta.Split.generalizeMatchDiscrs mvarId discrs let x : Array Lean.FVarId × Lean.MVarId := discr match x with | (discrFVarIds, mvarId) => do let mvarId ← Lean.Meta.generalizeTargetsEq mvarId motiveType (Array.map Lean.mkFVar discrFVarIds) let numEqs : Nat := Array.size discrs let discr ← Lean.Meta.introN mvarId (Array.size discrs) [] false let x : Array Lean.FVarId × Lean.MVarId := discr match x with | (discrFVarIdsNew, mvarId) => let discrsNew := Array.map Lean.mkFVar discrFVarIdsNew; Lean.Meta.withMVarContext mvarId do let a ← Lean.Meta.getMVarType mvarId let motive ← Lean.Meta.mkLambdaFVars discrsNew a false true let splitter : Lean.Expr := Lean.mkAppN (Lean.mkApp splitter motive) discrsNew Lean.Meta.check splitter let mvarIds ← Lean.Meta.apply mvarId splitter let discr ← List.foldlM (fun x mvarId => match x with | (i, mvarIds) => let numParams := Array.getOp matchEqns.splitterAltNumParams i; do let discr ← Lean.Meta.introN mvarId numParams [] false let x : Array Lean.FVarId × Lean.MVarId := discr match x with | (x, mvarId) => do let a ← Lean.Meta.Cases.unifyEqs numEqs mvarId { map := ∅ } none match a with | none => pure (i + 1, mvarIds) | some (mvarId, x) => pure (i + 1, mvarId :: mvarIds)) (0, []) mvarIds let x : Nat × List Lean.MVarId := discr match x with | (x, mvarIds) => pure (List.reverse mvarIds) match info.uElimPos? with | some uElimPos => let us := Array.set! us uElimPos Lean.levelZero; do let y ← pure PUnit.unit _do_jp us y | x => do let y ← pure PUnit.unit _do_jp us y | x => Lean.throwError (Lean.toMessageData "'applyMatchSplitter' failed, '" ++ Lean.toMessageData matcherDeclName ++ Lean.toMessageData "' is not a 'match' auxiliary declaration.")

source

def Lean.Meta.Split.splitMatch (mvarId : Lean.MVarId) (e : Lean.Expr) :

Lean.MetaM (List Lean.MVarId)

Equations

Lean.Meta.Split.splitMatch mvarId e = do let r ← tryCatch (do let discr ← Lean.Meta.matchMatcherApp? e match discr with | some app => do let matchEqns ← Lean.Meta.Match.getEquationsFor app.matcherName let mvarIds ← Lean.Meta.Split.applyMatchSplitter mvarId app.matcherName app.matcherLevels app.params app.discrs let discr ← List.foldlM (fun x mvarId => match x with | (i, mvarIds) => do let mvarId ← Lean.Meta.Split.simpMatchTargetCore mvarId app.matcherName (Array.getOp matchEqns.eqnNames i) pure (i + 1, mvarId :: mvarIds)) (0, []) mvarIds let x : Nat × List Lean.MVarId := discr match x with | (x, mvarIds) => pure (DoResultPR.return (List.reverse mvarIds) PUnit.unit) | x => do let y ← Lean.throwError (Lean.toMessageData "match application expected") pure (DoResultPR.pure y PUnit.unit)) fun ex => do let y ← Lean.Meta.throwNestedTacticEx `splitMatch ex pure (DoResultPR.pure y PUnit.unit) match r with | DoResultPR.pure a u => let x := u; pure a | DoResultPR.return b u => let x := u; pure b

source

partial def Lean.Meta.Split.findSplit? (env : Lean.Environment) (e : Lean.Expr) :

Option Lean.Expr

source

def Lean.Meta.Split.findSplit?.isCandidate (env : Lean.Environment) (e : Lean.Expr) :

Bool

Equations

Lean.Meta.Split.findSplit?.isCandidate env e = Id.run (if (Lean.Expr.isIte e || Lean.Expr.isDIte e) = true then !Lean.Expr.hasLooseBVars (Lean.Expr.getArg! e 1 5) else match Lean.Meta.isMatcherAppCore? env e with | some info => let args := Lean.Expr.getAppArgs e; do let r ← let col := { start := Lean.Meta.Match.MatcherInfo.getFirstDiscrPos info, stop := Lean.Meta.Match.MatcherInfo.getFirstDiscrPos info + info.numDiscrs, step := 1 }; forIn col { fst := none, snd := PUnit.unit } fun i r => let r := r.snd; if Lean.Expr.hasLooseBVars (Array.getOp args i) = 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 → Id Bool := fun y => pure true match r.fst with | none => do let y ← pure PUnit.unit _do_jp y | some a => pure a | x => false)

source

def Lean.Meta.splitTarget? (mvarId : Lean.MVarId) :

Lean.MetaM (Option (List Lean.MVarId))

Equations

Lean.Meta.splitTarget? mvarId = Lean.commitWhenSome? do let a ← Lean.getEnv let a_1 ← Lean.Meta.getMVarType mvarId let a_2 ← Lean.Meta.instantiateMVars a_1 match Lean.Meta.Split.findSplit? a a_2 with | some e => if (Lean.Expr.isIte e || Lean.Expr.isDIte e) = true then do let a ← Lean.Meta.splitIfTarget? mvarId none pure (Option.map (fun x => match x with | (s₁, s₂) => [s₁.mvarId, s₂.mvarId]) a) else Lean.Internal.coeM (Lean.Meta.Split.splitMatch mvarId e) | x => let cls := `Meta.Tactic.split; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM (Option (List Lean.MVarId)) := fun y => pure none if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "did not find term to split\n" ++ Lean.toMessageData (Lean.MessageData.ofGoal mvarId) ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y

source

def Lean.Meta.splitLocalDecl? (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) :

Lean.MetaM (Option (List Lean.MVarId))

Equations

Lean.Meta.splitLocalDecl? mvarId fvarId = Lean.commitWhenSome? (Lean.Meta.withMVarContext mvarId do let a ← Lean.getEnv let a_1 ← Lean.Meta.inferType (Lean.mkFVar fvarId) let a_2 ← Lean.Meta.instantiateMVars a_1 match Lean.Meta.Split.findSplit? a a_2 with | some e => if (Lean.Expr.isIte e || Lean.Expr.isDIte e) = true then do let a ← Lean.Meta.splitIfLocalDecl? mvarId fvarId none pure (Option.map (fun x => match x with | (mvarId₁, mvarId₂) => [mvarId₁, mvarId₂]) a) else do let discr ← Lean.Meta.revert mvarId #[fvarId] false let x : Array Lean.FVarId × Lean.MVarId := discr match x with | (fvarIds, mvarId) => let num := Array.size fvarIds; do let mvarIds ← Lean.Meta.Split.splitMatch mvarId e let mvarIds ← List.mapM (fun mvarId => do let a ← Lean.Meta.introNP mvarId num pure a.snd) mvarIds pure (some mvarIds) | x => pure none)