Equations
-
Lean.Elab.WF.packDomain preDefs = let preDefsNew := #[];
let arities := #[];
let modified := false;
do
let r ←
forIn preDefs { fst := arities, snd := { fst := preDefsNew, snd := modified } } fun preDef r =>
let arities := r.fst;
let x := r.snd;
let preDefsNew := x.fst;
let modified := x.snd;
do
let discr ←
Lean.Meta.lambdaTelescope preDef.value fun xs body =>
let _do_jp := fun y =>
if Array.size xs > 1 then do
let bodyType ← Lean.Meta.instantiateForall preDef.type xs
let d ← Lean.Meta.inferType (Array.back xs)
let r ←
let col := Array.reverse (Array.pop xs);
forIn col d fun x r =>
let d := r;
do
let a ← Lean.Meta.inferType x
let a_1 ← Lean.Meta.mkLambdaFVars #[x] d false true
let r ← Lean.Meta.mkAppOptM `PSigma #[some a, some a_1]
let d : Lean.Expr := r
pure PUnit.unit
pure (ForInStep.yield d)
let x : Lean.Expr := r
let d : Lean.Expr := x
let a ← liftM (Lean.mkFreshUserName `_x)
Lean.Meta.withLocalDeclD a d fun tuple =>
let elems := Lean.Elab.WF.mkTupleElems tuple (Array.size xs);
let codomain := Lean.Expr.replaceFVars bodyType xs elems;
do
let a ← Lean.Meta.mkForallFVars #[tuple] codomain false true
let preDefNew : Lean.Elab.PreDefinition :=
{ ref := preDef.ref, kind := preDef.kind, levelParams := preDef.levelParams,
modifiers := preDef.modifiers, declName := preDef.declName ++ `_unary, type := a,
value := preDef.value }
Lean.Elab.addAsAxiom preDefNew
pure (preDefNew, Array.size xs, true)
else pure (preDef, 1, false);
if (Array.size xs == 0) = true then do
let y ←
Lean.throwError
(Lean.toMessageData "well-founded recursion cannot be used, '" ++ Lean.toMessageData preDef.declName ++ Lean.toMessageData "' does not take any arguments")
_do_jp y
else do
let y ← pure PUnit.unit
_do_jp y
let x : Lean.Elab.PreDefinition × Nat × Bool := discr
match x with
| (preDefNew, arity, modifiedCurr) =>
let modified := modified || modifiedCurr;
let arities := Array.push arities arity;
let preDefsNew := Array.push preDefsNew preDefNew;
do
pure PUnit.unit
pure (ForInStep.yield { fst := arities, snd := { fst := preDefsNew, snd := modified } })
let x : MProd (Array Nat) (MProd (Array Lean.Elab.PreDefinition) Bool) := r
match x with
| { fst := arities, snd := { fst := preDefsNew, snd := modified } } =>
let _do_jp := fun preDefsNew y =>
let isAppOfPreDef? := fun e =>
let f := Lean.Expr.getAppFn e;
do
guard (Lean.Expr.isConst f = true)
Array.findIdx? preDefs fun a => a.declName == Lean.Expr.constName! f;
let isTargetApp? := fun e => do
let i ← isAppOfPreDef? e
guard ((Lean.Expr.getAppNumArgs e == Array.getOp arities i) = true)
pure i;
do
let r ←
let col := { start := 0, stop := Array.size preDefs, step := 1 };
forIn col preDefsNew fun i r =>
let preDefsNew := r;
let preDef := Array.getOp preDefs i;
let preDefNew := Array.getOp preDefsNew i;
let arity := Array.getOp arities i;
do
let valueNew ←
Lean.Meta.lambdaTelescope preDef.value fun xs body =>
Lean.Meta.forallBoundedTelescope preDefNew.type (some 1) fun y codomain =>
let y := Array.getOp y 0;
do
let newBody ← Lean.Elab.WF.mkPSigmaCasesOn y codomain xs body
let visit : Lean.Expr → Lean.MetaM Lean.TransformStep := fun e =>
match OptionM.run (isTargetApp? e) with
| some idx =>
let f := Lean.Expr.getAppFn e;
let fNew := Lean.mkConst (Array.getOp preDefsNew idx).declName (Lean.Expr.constLevels! f);
do
let discr ← Lean.Meta.inferType fNew
match discr with
| Lean.Expr.forallE x d x_1 x_2 => do
let argNew ← Lean.Elab.WF.mkUnaryArg d (Lean.Expr.getAppArgs e)
pure (Lean.TransformStep.done (Lean.mkApp fNew argNew))
| x =>
panicWithPosWithDecl "Lean.Elab.PreDefinition.WF.PackDomain" "Lean.Elab.WF.packDomain" 112
55 "unreachable code has been reached"
| x => pure (Lean.TransformStep.done e)
let a ← Lean.Meta.transform newBody (fun e => pure (Lean.TransformStep.visit e)) visit
Lean.Meta.mkLambdaFVars #[y] a false true
let _do_jp :
Array Lean.Elab.PreDefinition → PUnit → Lean.MetaM (ForInStep (Array Lean.Elab.PreDefinition)) :=
fun preDefsNew y =>
let preDefsNew :=
Array.set! preDefsNew i
{ ref := preDefNew.ref, kind := preDefNew.kind, levelParams := preDefNew.levelParams,
modifiers := preDefNew.modifiers, declName := preDefNew.declName, type := preDefNew.type,
value := valueNew };
do
pure PUnit.unit
pure (ForInStep.yield preDefsNew)
match
Lean.Expr.find? (fun e => Option.isSome (isAppOfPreDef? e) && decide (Lean.Expr.getAppNumArgs e > 1))
valueNew with
| some bad =>
match isAppOfPreDef? bad with
| some i => do
let y ←
Lean.throwErrorAt preDef.ref
(Lean.toMessageData "well-founded recursion cannot be used, function '" ++ Lean.toMessageData preDef.declName ++ Lean.toMessageData "' contains application of function '" ++ Lean.toMessageData (Array.getOp preDefs i).declName ++ Lean.toMessageData "' with #" ++ Lean.toMessageData (Lean.Expr.getAppNumArgs bad) ++ Lean.toMessageData " argument(s), but function has arity " ++ Lean.toMessageData (Array.getOp arities i) ++ Lean.toMessageData "")
_do_jp preDefsNew y
| x => do
let y ← pure PUnit.unit
_do_jp preDefsNew y
| x => do
let y ← pure PUnit.unit
_do_jp preDefsNew y
let x : Array Lean.Elab.PreDefinition := r
let preDefsNew : Array Lean.Elab.PreDefinition := x
pure preDefsNew;
if (!modified) = true then pure preDefs
else do
let y ← pure PUnit.unit
_do_jp preDefsNew y