max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2020-03-06 13:03:42 -08:00
parent 88a62f9f7e
commit 1854f5796b
22 changed files with 13494 additions and 5016 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

109
stage0/src/Init/Lean/Elab/Tactic/Induction.lean
View file

@ -6,6 +6,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich
prelude
import Init.Lean.Meta.RecursorInfo
import Init.Lean.Meta.Tactic.Induction
import Init.Lean.Meta.Tactic.Cases
import Init.Lean.Elab.Tactic.ElabTerm
import Init.Lean.Elab.Tactic.Generalize
@ -149,6 +150,35 @@ match recInfo? with
(fun _ => throwError ref ("invalid recursor name '" ++ baseRecName ++ "'"))
| _ => throwError ref ("invalid recursor name '" ++ baseRecName ++ "'")
/- Create `RecInfo` assuming builtin recursor -/
private def getRecInfoDefault (ref : Syntax) (major : Expr) (withAlts : Syntax) : TacticM RecInfo := do
indVal ← getInductiveValFromMajor ref major;
let recName := mkRecFor indVal.name;
if withAlts.isNone then pure { recName := recName }
else do
let ctorNames := indVal.ctors;
let alts := getAlts withAlts;
checkAltCtorNames alts ctorNames;
(altVars, altRHSs, remainingAlts, _) ← ctorNames.foldlM
(fun (result : Array (List Name) × Array Syntax × Array Syntax × Option Syntax) (ctorName : Name) => do
let (altVars, altRHSs, remainingAlts, prevAnonymousAlt?) := result;
match remainingAlts.findIdx? (fun alt => (getAltName alt).isSuffixOf ctorName) with
| some idx =>
let newAlt := remainingAlts.get! idx;
pure (altVars.push (getAltVarNames newAlt).toList, altRHSs.push (getAltRHS newAlt), remainingAlts.eraseIdx idx, prevAnonymousAlt?)
| none => match remainingAlts.findIdx? (fun alt => getAltName alt == `_) with
| some idx =>
let newAlt := remainingAlts.get! idx;
pure (altVars.push (getAltVarNames newAlt).toList, altRHSs.push (getAltRHS newAlt), remainingAlts.eraseIdx idx, some newAlt)
| none => match prevAnonymousAlt? with
| some alt =>
pure (altVars.push (getAltVarNames alt).toList, altRHSs.push (getAltRHS alt), remainingAlts, prevAnonymousAlt?)
| none => throwError ref ("alternative for constructor '" ++ toString ctorName ++ "' is missing"))
(#[], #[], alts, none);
unless remainingAlts.isEmpty $
throwError (remainingAlts.get! 0) "unused alternative";
pure { recName := recName, altVars := altVars, altRHSs := altRHSs }
/-
Recall that
```
@ -162,32 +192,7 @@ let ref := stx;
let usingRecStx := stx.getArg 2;
let withAlts := stx.getArg 4;
if usingRecStx.isNone then do
indVal ← getInductiveValFromMajor ref major;
let recName := mkRecFor indVal.name;
if withAlts.isNone then pure { recName := recName }
else do
let ctorNames := indVal.ctors;
let alts := getAlts withAlts;
checkAltCtorNames alts ctorNames;
(altVars, altRHSs, remainingAlts, _) ← ctorNames.foldlM
(fun (result : Array (List Name) × Array Syntax × Array Syntax × Option Syntax) (ctorName : Name) => do
let (altVars, altRHSs, remainingAlts, prevAnonymousAlt?) := result;
match remainingAlts.findIdx? (fun alt => (getAltName alt).isSuffixOf ctorName) with
| some idx =>
let newAlt := remainingAlts.get! idx;
pure (altVars.push (getAltVarNames newAlt).toList, altRHSs.push (getAltRHS newAlt), remainingAlts.eraseIdx idx, prevAnonymousAlt?)
| none => match remainingAlts.findIdx? (fun alt => getAltName alt == `_) with
| some idx =>
let newAlt := remainingAlts.get! idx;
pure (altVars.push (getAltVarNames newAlt).toList, altRHSs.push (getAltRHS newAlt), remainingAlts.eraseIdx idx, some newAlt)
| none => match prevAnonymousAlt? with
| some alt =>
pure (altVars.push (getAltVarNames alt).toList, altRHSs.push (getAltRHS alt), remainingAlts, prevAnonymousAlt?)
| none => throwError ref ("alternative for constructor '" ++ toString ctorName ++ "' is missing"))
(#[], #[], alts, none);
unless remainingAlts.isEmpty $
throwError (remainingAlts.get! 0) "unused alternative";
pure { recName := recName, altVars := altVars, altRHSs := altRHSs }
getRecInfoDefault ref major withAlts
else do
let baseRecName := (usingRecStx.getIdAt 1).eraseMacroScopes;
recInfo ← getRecFromUsing ref major baseRecName;
@ -220,6 +225,26 @@ else do
throwError (remainingAlts.get! 0) "unused alternative";
pure { recName := recName, altVars := altVars, altRHSs := altRHSs }
private def processResult (ref : Syntax) (recInfo : RecInfo) (result : Array Meta.InductionSubgoal) : TacticM Unit := do
if recInfo.altRHSs.isEmpty then
setGoals $ result.toList.map $ fun s => s.mvarId
else do
unless (recInfo.altRHSs.size == result.size) $
throwError ref ("mistmatch on the number of subgoals produced (" ++ toString result.size ++ ") and " ++
"alternatives provided (" ++ toString recInfo.altRHSs.size ++ ")");
result.size.forM $ fun i => do
let subgoal := result.get! i;
let rhs := recInfo.altRHSs.get! i;
let mvarId := subgoal.mvarId;
withMVarContext mvarId $ do
mvarDecl ← getMVarDecl mvarId;
val ← elabTerm rhs mvarDecl.type;
val ← ensureHasType rhs mvarDecl.type val;
assignExprMVar mvarId val;
gs' ← collectMVars rhs val;
tagUntaggedGoals mvarDecl.userName `induction gs';
appendGoals gs'
@[builtinTactic «induction»] def evalInduction : Tactic :=
fun stx => focusAux stx $ do
let h? := getAuxHypothesisName stx;
@ -229,24 +254,20 @@ fun stx => focusAux stx $ do
recInfo ← getRecInfo stx major;
(mvarId, _) ← getMainGoal stx;
result ← liftMetaM stx $ Meta.induction mvarId major.fvarId! recInfo.recName recInfo.altVars;
if recInfo.altRHSs.isEmpty then
setGoals $ result.toList.map $ fun s => s.mvarId
else do
unless (recInfo.altRHSs.size == result.size) $
throwError stx ("mistmatch on the number of subgoals produced (" ++ toString result.size ++ ") and " ++
"alternatives provided (" ++ toString recInfo.altRHSs.size ++ ")");
result.size.forM $ fun i => do
let subgoal := result.get! i;
let rhs := recInfo.altRHSs.get! i;
let mvarId := subgoal.mvarId;
withMVarContext mvarId $ do
mvarDecl ← getMVarDecl mvarId;
val ← elabTerm rhs mvarDecl.type;
val ← ensureHasType rhs mvarDecl.type val;
assignExprMVar mvarId val;
gs' ← collectMVars rhs val;
tagUntaggedGoals mvarDecl.userName `induction gs';
appendGoals gs'
processResult stx recInfo result
@[builtinTactic «cases»] def evalCases : Tactic :=
fun stx => focusAux stx $ do
-- parser! nonReservedSymbol "cases " >> majorPremise >> withAlts
let h? := getAuxHypothesisName stx;
major ← elabMajor stx h? (getMajor stx);
major ← generalizeMajor stx major;
(mvarId, _) ← getMainGoal stx;
let withAlts := stx.getArg 2;
recInfo ← getRecInfoDefault stx major withAlts;
result ← liftMetaM stx $ Meta.cases mvarId major.fvarId! recInfo.altVars;
let result := result.map (fun s => s.toInductionSubgoal);
processResult stx recInfo result
end Tactic
end Elab

9
stage0/src/Init/Lean/Expr.lean
View file

@ -694,14 +694,17 @@ def betaRev (f : Expr) (revArgs : Array Expr) : Expr :=
if revArgs.size == 0 then f
else betaRevAux revArgs revArgs.size f 0
def isHeadBetaTarget : Expr → Bool
def isHeadBetaTargetFn : Expr → Bool
| Expr.lam _ _ _ _ => true
| Expr.mdata _ b _ => isHeadBetaTarget b
| Expr.mdata _ b _ => isHeadBetaTargetFn b
| _ => false
def headBeta (e : Expr) : Expr :=
let f := e.getAppFn;
if f.isHeadBetaTarget then betaRev f e.getAppRevArgs else e
if f.isHeadBetaTargetFn then betaRev f e.getAppRevArgs else e
def isHeadBetaTarget (e : Expr) : Bool :=
e.getAppFn.isHeadBetaTargetFn
private def etaExpandedBody : Expr → Nat → Nat → Option Expr
| app f (bvar j _) _, n+1, i => if j == i then etaExpandedBody f n (i+1) else none

26
stage0/src/Init/Lean/Meta/AppBuilder.lean
View file

@ -94,6 +94,16 @@ else do
u ← getLevel α; pure $ mkApp8 (mkConst `HEq.trans [u]) α β γ a b c h₁ h₂
| _, _ => throwEx $ Exception.appBuilder `HEq.trans "heterogeneous equality proof expected" #[h₁, h₂]
def mkEqOfHEq (h : Expr) : MetaM Expr := do
hType ← infer h;
match hType.heq? with
| some (α, a, β, b) => do
unlessM (isDefEq α β) $ throwEx $ Exception.appBuilder `eqOfHEq "heterogeneous equality types are not definitionally equal" #[α, β];
u ← getLevel α;
pure $ mkApp4 (mkConst `eqOfHEq [u]) α a b h
| _ =>
throwEx $ Exception.appBuilder `HEq.trans "heterogeneous equality proof expected" #[h]
def mkCongrArg (f h : Expr) : MetaM Expr := do
hType ← infer h;
fType ← infer f;
@ -208,5 +218,21 @@ mkAppM `Eq.mp #[eqProof, pr]
def mkEqMPR (eqProof pr : Expr) : MetaM Expr :=
mkAppM `Eq.mpr #[eqProof, pr]
def mkNoConfusion (target : Expr) (h : Expr) : MetaM Expr := do
type ← inferType h;
type ← whnf type;
match type.eq? with
| none => throwEx $ Exception.appBuilder `noConfusion "equality expected" #[h]
| some (α, a, b) => do
α ← whnf α;
env ← getEnv;
let f := α.getAppFn;
matchConst env f (fun _ => throwEx $ Exception.appBuilder `noConfusion "inductive type expected" #[α]) $ fun cinfo us =>
match cinfo with
| ConstantInfo.inductInfo v => do
u ← getLevel target;
pure $ mkAppN (mkConst (mkNameStr v.name "noConfusion") (u :: us)) (α.getAppArgs ++ #[target, a, b, h])
| _ => throwEx $ Exception.appBuilder `noConfusion "inductive type expected" #[α]
end Meta
end Lean

89
stage0/src/Init/Lean/Meta/ExprDefEq.lean
View file

@ -566,13 +566,16 @@ match v with
-/
private partial def processAssignmentFOApprox (mvar : Expr) (args : Array Expr) : Expr → MetaM Bool
| v => do
trace! `Meta.isDefEq.foApprox (mvar ++ " " ++ args ++ " := " ++ v);
condM (commitWhen $ processAssignmentFOApproxAux mvar args v)
(pure true)
(do v? ← unfoldDefinition? v;
match v? with
| none => pure false
| some v => processAssignmentFOApprox v)
cfg ← getConfig;
if !cfg.foApprox then pure false
else do
trace! `Meta.isDefEq.foApprox (mvar ++ " " ++ args ++ " := " ++ v);
condM (commitWhen $ processAssignmentFOApproxAux mvar args v)
(pure true)
(do v? ← unfoldDefinition? v;
match v? with
| none => pure false
| some v => processAssignmentFOApprox v)
private partial def simpAssignmentArgAux : Expr → MetaM Expr
| Expr.mdata _ e _ => simpAssignmentArgAux e
@ -591,63 +594,51 @@ arg ← if arg.getAppFn.hasExprMVar then instantiateMVars arg else pure arg;
simpAssignmentArgAux arg
private def processConstApprox (mvar : Expr) (numArgs : Nat) (v : Expr) : MetaM Bool := do
let mvarId := mvar.mvarId!;
v? ← checkAssignment mvarId #[] v;
match v? with
| none => pure false
| some v => do
mvarDecl ← getMVarDecl mvarId;
forallBoundedTelescope mvarDecl.type numArgs $ fun xs _ =>
if xs.size != numArgs then pure false
else do
v ← mkLambda xs v;
checkTypesAndAssign mvar v
cfg ← getConfig;
if cfg.constApprox then do
let mvarId := mvar.mvarId!;
v? ← checkAssignment mvarId #[] v;
match v? with
| none => pure false
| some v => do
mvarDecl ← getMVarDecl mvarId;
forallBoundedTelescope mvarDecl.type numArgs $ fun xs _ =>
if xs.size != numArgs then pure false
else do
v ← mkLambda xs v;
checkTypesAndAssign mvar v
else
pure false
private partial def processAssignmentAux (mvar : Expr) (mvarDecl : MetavarDecl) (v : Expr) : Nat → Array Expr → MetaM Bool
| i, args =>
private partial def processAssignmentAux (mvar : Expr) (mvarDecl : MetavarDecl) : Nat → Array Expr → Expr → MetaM Bool
| i, args, v => do
cfg ← getConfig;
let useFOApprox (args : Array Expr) : MetaM Bool :=
processAssignmentFOApprox mvar args v <||> processConstApprox mvar args.size v;
if h : i < args.size then do
cfg ← getConfig;
let arg := args.get ⟨i, h⟩;
arg ← simpAssignmentArg arg;
let args := args.set ⟨i, h⟩ arg;
let useConstApprox : Unit → MetaM Bool := fun _ =>
if cfg.constApprox || (not args.isEmpty && not v.isApp) then
processConstApprox mvar args.size v
else
pure false;
let useFOApprox : Unit → MetaM Bool := fun _ =>
if cfg.foApprox && v.isApp then
condM (processAssignmentFOApprox mvar args v)
(pure true)
(useConstApprox ())
else
useConstApprox ();
match arg with
| Expr.fvar fvarId _ =>
if args.anyRange 0 i (fun prevArg => prevArg == arg) then
useFOApprox ()
useFOApprox args
else if mvarDecl.lctx.contains fvarId && !cfg.quasiPatternApprox then
useFOApprox ()
useFOApprox args
else
processAssignmentAux (i+1) args
processAssignmentAux (i+1) args v
| _ =>
useFOApprox ()
useFOApprox args
else do
cfg ← getConfig;
v ← instantiateMVars v; -- enforce A4
if cfg.foApprox && !args.isEmpty && v.getAppFn == mvar then
if v.getAppFn == mvar then
-- using A6
processAssignmentFOApprox mvar args v
useFOApprox args
else do
let useFOApprox : Unit → MetaM Bool := fun _ =>
if cfg.foApprox && !args.isEmpty then
processAssignmentFOApprox mvar args v
else
pure false;
let mvarId := mvar.mvarId!;
v? ← checkAssignment mvarId args v;
match v? with
| none => useFOApprox ()
| none => useFOApprox args
| some v => do
trace `Meta.isDefEq.assign.beforeMkLambda $ fun _ => mvar ++ " " ++ args ++ " := " ++ v;
v ← mkLambda args v;
@ -657,7 +648,7 @@ private partial def processAssignmentAux (mvar : Expr) (mvarDecl : MetavarDecl)
condM (isTypeCorrect v)
(checkTypesAndAssign mvar v)
(do trace `Meta.isDefEq.assign.typeError $ fun _ => mvar ++ " := " ++ v;
useFOApprox ())
useFOApprox args)
else
checkTypesAndAssign mvar v
@ -668,7 +659,7 @@ traceCtx `Meta.isDefEq.assign $ do
trace! `Meta.isDefEq.assign (mvarApp ++ " := " ++ v);
let mvar := mvarApp.getAppFn;
mvarDecl ← getMVarDecl mvar.mvarId!;
processAssignmentAux mvar mvarDecl v 0 mvarApp.getAppArgs
processAssignmentAux mvar mvarDecl 0 mvarApp.getAppArgs v
private def isDeltaCandidate (t : Expr) : MetaM (Option ConstantInfo) :=
match t.getAppFn with
@ -992,9 +983,9 @@ partial def isExprDefEqAuxImpl : Expr → Expr → MetaM Bool
whenUndefDo (isDefEqQuick t s) $
whenUndefDo (isDefEqProofIrrel t s) $
isDefEqWHNF t s $ fun t s => do
condM (isDefEqEta t s <||> isDefEqEta s t) (pure true) $
whenUndefDo (isDefEqOffset t s) $ do
whenUndefDo (isDefEqDelta t s) $
condM (isDefEqEta t s <||> isDefEqEta s t) (pure true) $
match t, s with
| Expr.const c us _, Expr.const d vs _ => if c == d then isListLevelDefEqAux us vs else pure false
| Expr.app _ _ _, Expr.app _ _ _ =>

12
stage0/src/Init/Lean/Meta/RecursorInfo.lean
View file

@ -13,6 +13,14 @@ import Init.Lean.Meta.Message
namespace Lean
namespace Meta
def casesOnSuffix := "casesOn"
def recOnSuffix := "recOn"
def brecOnSuffix := "brecOn"
def mkCasesOnFor (indDeclName : Name) : Name := mkNameStr indDeclName casesOnSuffix
def mkRecOnFor (indDeclName : Name) : Name := mkNameStr indDeclName recOnSuffix
def mkBRecOnFor (indDeclName : Name) : Name := mkNameStr indDeclName brecOnSuffix
inductive RecursorUnivLevelPos
| motive -- marks where the universe of the motive should go
| majorType (idx : Nat) -- marks where the #idx universe of the major premise type goes
@ -104,12 +112,12 @@ else do
if !isAuxRecursor env declName then pure none
else match declName with
| Name.str p s _ =>
if s != "recOn" && s != "casesOn" && s != "brecOn" then
if s != recOnSuffix && s != casesOnSuffix && s != brecOnSuffix then
pure none
else do
recInfo ← getConstInfo (mkRecFor p);
match recInfo with
| ConstantInfo.recInfo val => pure (some (val.nparams + val.nindices + (if s == "casesOn" then 1 else val.nmotives)))
| ConstantInfo.recInfo val => pure (some (val.nparams + val.nindices + (if s == casesOnSuffix then 1 else val.nmotives)))
| _ => throw $ Exception.other "unexpected recursor information"
| _ => pure none

110
stage0/src/Init/Lean/Meta/Tactic/Cases.lean
View file

@ -4,12 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Lean.Meta.AppBuilder
import Init.Lean.Meta.Tactic.Induction
import Init.Lean.Meta.Tactic.Assert
import Init.Lean.Meta.Tactic.Subst
namespace Lean
namespace Meta
private def mkEq (lhs rhs : Expr) : MetaM (Expr × Expr) := do
private def mkEqAndProof (lhs rhs : Expr) : MetaM (Expr × Expr) := do
lhsType ← inferType lhs;
rhsType ← inferType rhs;
u ← getLevel lhsType;
@ -22,7 +25,7 @@ private partial def withNewIndexEqsAux {α} (indices newIndices : Array Expr) (k
if h : i < indices.size then do
let index := indices.get! i;
let newIndex := newIndices.get! i;
(newEqType, newRefl) ← mkEq index newIndex;
(newEqType, newRefl) ← mkEqAndProof index newIndex;
withLocalDecl `h newEqType BinderInfo.default $ fun newEq => do
withNewIndexEqsAux (i+1) (newEqs.push newEq) (newRefls.push newRefl)
else
@ -74,7 +77,7 @@ withMVarContext mvarId $ do
let newType := mkAppN IA newIndices;
withLocalDecl fvarDecl.userName newType BinderInfo.default $ fun h' =>
withNewIndexEqs indices newIndices $ fun newEqs newRefls => do
(newEqType, newRefl) ← mkEq fvarDecl.toExpr h';
(newEqType, newRefl) ← mkEqAndProof fvarDecl.toExpr h';
let newRefls := newRefls.push newRefl;
withLocalDecl `h newEqType BinderInfo.default $ fun newEq => do
let newEqs := newEqs.push newEq;
@ -87,8 +90,8 @@ withMVarContext mvarId $ do
newMVar ← mkFreshExprMVarAt lctx localInsts auxType tag MetavarKind.syntheticOpaque;
/- assign mvarId := newMVar indices h refls -/
assignExprMVar mvarId (mkAppN (mkApp (mkAppN newMVar indices) fvarDecl.toExpr) newRefls);
(indicesFVarIds, newMVarId) ← introN newMVar.mvarId! newIndices.size;
(fvarId, newMVarId) ← intro1 newMVarId;
(indicesFVarIds, newMVarId) ← introN newMVar.mvarId! newIndices.size [] false;
(fvarId, newMVarId) ← intro1 newMVarId false;
pure {
mvarId := newMVarId,
indicesFVarIds := indicesFVarIds,
@ -97,11 +100,8 @@ withMVarContext mvarId $ do
}
| _ => throwTacticEx `generalizeIndices mvarId "inductive type expected"
structure CasesSubgoal :=
structure CasesSubgoal extends InductionSubgoal :=
(ctorName : Name)
(mvarId : MVarId)
(fields : Array FVarId := #[])
(subst : FVarSubst := {})
namespace Cases
@ -116,7 +116,7 @@ structure Context :=
private def mkCasesContext? (majorFVarId : FVarId) : MetaM (Option Context) := do
env ← getEnv;
if !env.contains `Eq || env.contains `HEq then pure none
if !env.contains `Eq || !env.contains `HEq then pure none
else do
majorDecl ← getLocalDecl majorFVarId;
majorType ← whnf majorDecl.type;
@ -158,11 +158,95 @@ else do
ctx.majorTypeIndices.any (fun index => decl.fvarId == index.fvarId!) || -- decl is one of the indices
mctx.findLocalDeclDependsOn decl (fun fvarId => ctx.majorTypeIndices.all $ fun idx => idx.fvarId! != fvarId) -- or does not depend on any index
private def elimAuxIndices (s₁ : GeneralizeIndicesSubgoal) (s₂ : Array InductionSubgoal) : MetaM (Array InductionSubgoal) :=
let indicesFVarIds := s₁.indicesFVarIds;
s₂.mapM $ fun s => do
indicesFVarIds.foldlM
(fun s indexFVarId =>
let indexFVarId' := s.subst.get indexFVarId;
(do mvarId ← clear s.mvarId indexFVarId'; pure { mvarId := mvarId, subst := s.subst.erase indexFVarId, .. s })
<|>
(pure s))
s
private def toCasesSubgoals (s : Array InductionSubgoal) (ctorNames : Array Name) : Array CasesSubgoal :=
s.mapIdx $ fun i s => { ctorName := ctorNames.get! i, toInductionSubgoal := s }
private partial def unifyEqsAux : Nat → CasesSubgoal → MetaM (Option CasesSubgoal)
| 0, s => do
trace! `Meta.cases ("unifyEqs " ++ MessageData.ofGoal s.mvarId);
pure (some s)
| n+1, s => do
trace! `Meta.cases ("unifyEqs [" ++ toString (n+1) ++ "] " ++ MessageData.ofGoal s.mvarId);
(eqFVarId, mvarId) ← intro1 s.mvarId;
withMVarContext mvarId $ do
eqDecl ← getLocalDecl eqFVarId;
match eqDecl.type.heq? with
| some (α, a, β, b) => do
prf ← mkEqOfHEq (mkFVar eqFVarId);
aEqb ← mkEq a b;
mvarId ← assert mvarId eqDecl.userName aEqb prf;
mvarId ← clear mvarId eqFVarId;
unifyEqsAux (n+1) { mvarId := mvarId, .. s }
| none => match eqDecl.type.eq? with
| some (α, a, b) =>
let skip : Unit → MetaM (Option CasesSubgoal) := fun _ => do {
mvarId ← clear mvarId eqFVarId;
unifyEqsAux n { mvarId := mvarId, .. s }
};
let substEq (symm : Bool) : MetaM (Option CasesSubgoal) := do {
(newSubst, mvarId) ← substCore mvarId eqFVarId false true;
unifyEqsAux n {
mvarId := mvarId,
subst := newSubst.compose s.subst,
fields := s.fields.map $ fun fvarId => newSubst.get fvarId,
.. s
}
};
condM (isDefEq a b) (skip ()) $
match a, b with
| Expr.fvar aFVarId _, Expr.fvar bFVarId _ => do aDecl ← getLocalDecl aFVarId; bDecl ← getLocalDecl bFVarId; substEq (aDecl.index < bDecl.index)
| Expr.fvar _ _, _ => substEq false
| _, Expr.fvar _ _ => substEq true
| _, _ =>
-- TODO
pure $ some { mvarId := mvarId, .. s }
| none => throwTacticEx `cases mvarId "equality expected"
private def unifyEqs (numEqs : Nat) (subgoals : Array CasesSubgoal) : MetaM (Array CasesSubgoal) :=
subgoals.foldlM
(fun subgoals s => do
s? ← unifyEqsAux numEqs s;
match s? with
| none => pure $ subgoals
| some s => pure $ subgoals.push s)
#[]
def cases (mvarId : MVarId) (majorFVarId : FVarId) (givenNames : Array (List Name) := #[]) (useUnusedNames := false) : MetaM (Array CasesSubgoal) :=
withMVarContext mvarId $ do
checkNotAssigned mvarId `cases;
context? ← mkCasesContext? majorFVarId;
match context? with
| none => throwTacticEx `cases mvarId "not applicable to the given hypothesis"
| some ctx =>
let ctors := ctx.inductiveVal.ctors.toArray;
let casesOn := mkCasesOnFor ctx.inductiveVal.name;
condM (hasIndepIndices ctx)
(do
s ← induction mvarId majorFVarId casesOn givenNames useUnusedNames;
pure $ toCasesSubgoals s ctors)
(do
s₁ ← generalizeIndices mvarId majorFVarId;
trace! `Meta.cases ("after generalizeIndices" ++ Format.line ++ MessageData.ofGoal s₁.mvarId);
s₂ ← induction s₁.mvarId s₁.fvarId casesOn givenNames useUnusedNames;
s₂ ← elimAuxIndices s₁ s₂;
let s₂ := toCasesSubgoals s₂ ctors;
unifyEqs s₁.numEqs s₂)
end Cases
def cases (mvarId : MVarId) (majorFVarId : FVarId) (givenNames : Array (List Name) := #[]) (useUnusedNames := false) :
MetaM (Array CasesSubgoal) :=
throw $ arbitrary _ -- TODO
def cases (mvarId : MVarId) (majorFVarId : FVarId) (givenNames : Array (List Name) := #[]) (useUnusedNames := false) : MetaM (Array CasesSubgoal) :=
Cases.cases mvarId majorFVarId givenNames useUnusedNames
end Meta
end Lean

33
stage0/src/Init/Lean/Meta/Tactic/FVarSubst.lean
View file

@ -10,30 +10,39 @@ import Init.Lean.Util.ReplaceExpr
namespace Lean
namespace Meta
/-
Some tactics substitute hypotheses with new ones and/or terms.
Some tactics substitute hypotheses with new ones.
We track these substitutions using `FVarSubst`.
It is just a mapping from the original FVarId (internal) name
to an expression. The new expression should be well-formed with
respect to the new goal. -/
to the new one. The new free variable should be defined in the new goal. -/
structure FVarSubst :=
(map : NameMap Expr := {})
(map : NameMap FVarId := {})
namespace FVarSubst
def empty : FVarSubst := {}
def insert (s : FVarSubst) (fvarId : FVarId) (e : Expr) : FVarSubst :=
{ map := s.map.insert fvarId e }
def insert (s : FVarSubst) (fvarId : FVarId) (fvarIdNew : FVarId) : FVarSubst :=
{ map := s.map.insert fvarId fvarIdNew }
def contains (s : FVarSubst) (fvarId : FVarId) : Bool :=
s.map.contains fvarId
def erase (s : FVarSubst) (fvarId : FVarId) : FVarSubst :=
{ map := s.map.erase fvarId }
def get (s : FVarSubst) (fvarId : FVarId) : FVarId :=
match s.map.find? fvarId with
| none => fvarId -- it has not been replaced
| some fvarId' => fvarId'
/-- Given `e`, for each `(x => v)` in `s` replace `x` with `v` in `e` -/
def apply (s : FVarSubst) (e : Expr) : Expr :=
if s.map.isEmpty then e
else if !e.hasFVar then e
else e.replace $ fun e => match e with
| Expr.fvar fvarId _ => s.map.find? fvarId
| Expr.fvar fvarId _ => match s.map.find? fvarId with
| none => e
| some fvarId' => mkFVar fvarId'
| _ => none
/--
@ -44,7 +53,15 @@ else e.replace $ fun e => match e with
def compose (newS oldS : FVarSubst) : FVarSubst :=
if newS.map.isEmpty then oldS
else if oldS.map.isEmpty then newS
else oldS.map.fold (fun m fvarId e => if m.map.contains fvarId then m else m.insert fvarId (m.apply e)) newS
else oldS.map.fold
(fun m fvarId fvarId' =>
match m.map.find? fvarId with
| some _ => m -- newS already has a substitution for fvarId
| none =>
match m.map.find? fvarId' with
| none => m.insert fvarId fvarId'
| some fvarId'' => m.insert fvarId fvarId'')
newS
end FVarSubst
end Meta

4
stage0/src/Init/Lean/Meta/Tactic/Induction.lean
View file

@ -108,7 +108,7 @@ private partial def finalizeAux
else
let revertedFVarId := reverted.get! i;
let newFVarId := extra.get! (i - indices.size - 1);
subst.insert revertedFVarId (mkFVar newFVarId))
subst.insert revertedFVarId newFVarId)
baseSubst;
finalizeAux (pos+1) (minorIdx+1) rec recType consumedMajor (subgoals.push { mvarId := mvarId', fields := fields, subst := subst })
| _ => unreachable!
@ -170,7 +170,7 @@ withMVarContext mvarId $ do
(indices', mvarId) ← introN mvarId indices.size [] false;
(majorFVarId', mvarId) ← intro1 mvarId false;
-- Create FVarSubst with indices
let baseSubst : FVarSubst := indices.iterate {} (fun i index subst => subst.insert index.fvarId! (mkFVar (indices'.get! i.val)));
let baseSubst : FVarSubst := indices.iterate {} (fun i index subst => subst.insert index.fvarId! (indices'.get! i.val));
-- Update indices and major
let indices := indices'.map mkFVar;
let majorFVarId := majorFVarId';

2
stage0/src/Init/Lean/Meta/Tactic/Subst.lean
View file

@ -61,7 +61,7 @@ withMVarContext mvarId $ do
(fun i (fvarSubst : FVarSubst) =>
let var := vars.get! i;
let newFVar := newFVars.get! i;
pure $ fvarSubst.insert var (mkFVar newFVar))
pure $ fvarSubst.insert var newFVar)
FVarSubst.empty;
pure (fvarSubst, mvarId)
};

2
stage0/src/Init/Lean/Meta/Tactic/Util.lean
View file

@ -37,7 +37,7 @@ mctx ← getMCtx;
opts ← getOptions;
pure $ ppGoal env mctx opts mvarId
@[inline] protected def orelse{α} (x y : MetaM α) : MetaM α := do
@[inline] protected def orelse {α} (x y : MetaM α) : MetaM α := do
s ← get; catch x (fun _ => do restore s.env s.mctx s.postponed; y)
instance Meta.hasOrelse {α} : HasOrelse (MetaM α) := ⟨Meta.orelse⟩

1
stage0/src/library/equations_compiler/elim_match.cpp
View file

@ -610,6 +610,7 @@ struct elim_match_fn {
hsubstitution add_subst(hsubstitution subst, expr const & src, expr const & target) {
lean_assert(is_fvar(src));
lean_assert(is_fvar(target));
if (!subst.contains(fvar_name(src)))
subst.insert(fvar_name(src), target);
return subst;

12
stage0/src/library/type_context.cpp
View file

@ -1918,8 +1918,16 @@ bool type_context_old::process_assignment(expr const & m, expr const & v) {
use_fo = true;
}
if (use_fo && (is_app(new_v) || !m_unifier_cfg.m_const_approx)) {
return process_assignment_fo_approx(mvar, args, new_v);
if (use_fo) {
if (is_app(new_v) || !m_unifier_cfg.m_const_approx) {
return process_assignment_fo_approx(mvar, args, new_v);
} else {
scope s(*this);
if (process_assignment_fo_approx(mvar, args, new_v)) {
s.commit();
return true;
}
}
}
if (optional<expr> new_new_v = check_assignment(locals, in_ctx_locals, mvar, new_v))

5
stage0/src/util/file_lock.cpp
View file

@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <string>
#include <cstring>
#include <errno.h>
#include <fcntl.h>
#include "runtime/exception.h"
@ -85,12 +86,12 @@ file_lock::file_lock(char const * fname, bool exclusive):
// fname is probably part of the Lean installation in a system directory.
// So, we ignore the file_lock in this case.
} else {
throw exception(sstream() << "failed to lock file '" << fname << "'");
throw exception(sstream() << "failed to open lock file for '" << fname << "': " << strerror(errno));
}
} else {
int status = flock(m_fd, exclusive ? LOCK_EX : LOCK_SH);
if (status == -1)
throw exception(sstream() << "failed to lock file '" << fname << "'");
throw exception(sstream() << "failed to lock file '" << fname << "': " << strerror(errno));
}
#endif
}

3990
stage0/stdlib/Init/Lean/Elab/Tactic/Induction.c
View file

File diff suppressed because it is too large Load diff

62
stage0/stdlib/Init/Lean/Expr.c
View file

@ -32,6 +32,7 @@ lean_object* l_Lean_Expr_getAppNumArgs___boxed(lean_object*);
lean_object* lean_mk_empty_array_with_capacity(lean_object*);
lean_object* l_Lean_Expr_isAppOf___boxed(lean_object*, lean_object*);
lean_object* l_Lean_mkSort(lean_object*);
uint8_t l_Lean_Expr_isHeadBetaTargetFn(lean_object*);
uint8_t l_UInt64_decEq(uint64_t, uint64_t);
lean_object* l_Lean_Expr_HasBeq___closed__1;
lean_object* l_Lean_Expr_abstract___boxed(lean_object*, lean_object*);
@ -143,7 +144,6 @@ lean_object* l_Lean_Expr_isAppOfArity___main___boxed(lean_object*, lean_object*,
lean_object* l_Lean_BinderInfo_hashable___closed__1;
lean_object* l_Lean_Expr_letName_x21___boxed(lean_object*);
lean_object* l_Lean_Expr_updateForall_x21(lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Expr_isHeadBetaTarget___main___boxed(lean_object*);
lean_object* l_Lean_Expr_looseBVarRange___boxed(lean_object*);
lean_object* l___private_Init_Lean_Expr_12__getParamSubstArray___main___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_mkDataForBinder___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -300,6 +300,7 @@ lean_object* l_Lean_Expr_Data_hasLevelMVar___boxed(lean_object*);
uint8_t l_Lean_Expr_Data_nonDepLet(uint64_t);
lean_object* l_Lean_Literal_hasBeq___closed__1;
lean_object* l_Lean_Level_instantiateParams___main___at_Lean_Expr_instantiateLevelParamsArray___spec__3___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_isHeadBetaTargetFn___boxed(lean_object*);
lean_object* l_Lean_Expr_consumeMData(lean_object*);
uint64_t l_UInt64_land(uint64_t, uint64_t);
lean_object* l___private_Init_Lean_Expr_3__getAppArgsAux___main(lean_object*, lean_object*, lean_object*);
@ -398,6 +399,7 @@ extern uint8_t l_Bool_Inhabited;
lean_object* l_Lean_Expr_bvarIdx_x21___closed__1;
lean_object* lean_panic_fn(lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_mkAppN___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Expr_isHeadBetaTargetFn___main(lean_object*);
uint32_t l_USize_toUInt32(size_t);
lean_object* l_Lean_Expr_withApp___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Expr_isAppOfArity___boxed(lean_object*, lean_object*, lean_object*);
@ -474,6 +476,7 @@ lean_object* l_Lean_BinderInfo_hashable;
lean_object* l_Lean_Expr_InstantiateLevelParams_instantiate___main(lean_object*, lean_object*);
lean_object* l_Lean_Expr_mkData___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_BinderInfo_isExplicit___boxed(lean_object*);
lean_object* l_Lean_Expr_isHeadBetaTargetFn___main___boxed(lean_object*);
lean_object* l_Lean_Expr_HasToString___closed__1;
uint64_t l_Lean_Expr_mkData___closed__1;
lean_object* l_Lean_Expr_hashEx___boxed(lean_object*);
@ -490,7 +493,6 @@ uint8_t l_List_foldr___main___at_Lean_mkConst___spec__4(uint8_t, lean_object*);
lean_object* l_Lean_Expr_etaExpandedStrict_x3f(lean_object*);
lean_object* l_Lean_Expr_updateLambdaE_x21(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_hasLooseBVar___boxed(lean_object*, lean_object*);
uint8_t l_Lean_Expr_isHeadBetaTarget___main(lean_object*);
lean_object* l___private_Init_Lean_Expr_1__Expr_mkDataCore___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Nat_Inhabited;
uint64_t l_UInt64_shiftRight(uint64_t, uint64_t);
@ -6978,7 +6980,7 @@ lean_dec(x_1);
return x_3;
}
}
uint8_t l_Lean_Expr_isHeadBetaTarget___main(lean_object* x_1) {
uint8_t l_Lean_Expr_isHeadBetaTargetFn___main(lean_object* x_1) {
_start:
{
switch (lean_obj_tag(x_1)) {
@ -7004,29 +7006,29 @@ return x_5;
}
}
}
lean_object* l_Lean_Expr_isHeadBetaTarget___main___boxed(lean_object* x_1) {
lean_object* l_Lean_Expr_isHeadBetaTargetFn___main___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = l_Lean_Expr_isHeadBetaTarget___main(x_1);
x_2 = l_Lean_Expr_isHeadBetaTargetFn___main(x_1);
lean_dec(x_1);
x_3 = lean_box(x_2);
return x_3;
}
}
uint8_t l_Lean_Expr_isHeadBetaTarget(lean_object* x_1) {
uint8_t l_Lean_Expr_isHeadBetaTargetFn(lean_object* x_1) {
_start:
{
uint8_t x_2;
x_2 = l_Lean_Expr_isHeadBetaTarget___main(x_1);
x_2 = l_Lean_Expr_isHeadBetaTargetFn___main(x_1);
return x_2;
}
}
lean_object* l_Lean_Expr_isHeadBetaTarget___boxed(lean_object* x_1) {
lean_object* l_Lean_Expr_isHeadBetaTargetFn___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = l_Lean_Expr_isHeadBetaTarget(x_1);
x_2 = l_Lean_Expr_isHeadBetaTargetFn(x_1);
lean_dec(x_1);
x_3 = lean_box(x_2);
return x_3;
@ -7037,7 +7039,7 @@ _start:
{
lean_object* x_2; uint8_t x_3;
x_2 = l_Lean_Expr_getAppFn___main(x_1);
x_3 = l_Lean_Expr_isHeadBetaTarget___main(x_2);
x_3 = l_Lean_Expr_isHeadBetaTargetFn___main(x_2);
if (x_3 == 0)
{
lean_dec(x_2);
@ -7058,6 +7060,26 @@ return x_8;
}
}
}
uint8_t l_Lean_Expr_isHeadBetaTarget(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3;
x_2 = l_Lean_Expr_getAppFn___main(x_1);
x_3 = l_Lean_Expr_isHeadBetaTargetFn___main(x_2);
lean_dec(x_2);
return x_3;
}
}
lean_object* l_Lean_Expr_isHeadBetaTarget___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = l_Lean_Expr_isHeadBetaTarget(x_1);
lean_dec(x_1);
x_3 = lean_box(x_2);
return x_3;
}
}
lean_object* l___private_Init_Lean_Expr_8__etaExpandedBody___main(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
@ -7622,7 +7644,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(781u);
x_2 = lean_unsigned_to_nat(784u);
x_3 = lean_unsigned_to_nat(18u);
x_4 = l_Lean_Expr_appFn_x21___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -7664,7 +7686,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(790u);
x_2 = lean_unsigned_to_nat(793u);
x_3 = lean_unsigned_to_nat(18u);
x_4 = l_Lean_Expr_constName_x21___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -7713,7 +7735,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(799u);
x_2 = lean_unsigned_to_nat(802u);
x_3 = lean_unsigned_to_nat(14u);
x_4 = l_Lean_Expr_updateSort_x21___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -7770,7 +7792,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(816u);
x_2 = lean_unsigned_to_nat(819u);
x_3 = lean_unsigned_to_nat(17u);
x_4 = l_Lean_Expr_updateMData_x21___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -7811,7 +7833,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(821u);
x_2 = lean_unsigned_to_nat(824u);
x_3 = lean_unsigned_to_nat(18u);
x_4 = l_Lean_Expr_updateProj_x21___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -7862,7 +7884,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(830u);
x_2 = lean_unsigned_to_nat(833u);
x_3 = lean_unsigned_to_nat(21u);
x_4 = l_Lean_Expr_updateForall_x21___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -7906,7 +7928,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(835u);
x_2 = lean_unsigned_to_nat(838u);
x_3 = lean_unsigned_to_nat(21u);
x_4 = l_Lean_Expr_updateForall_x21___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -7960,7 +7982,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(844u);
x_2 = lean_unsigned_to_nat(847u);
x_3 = lean_unsigned_to_nat(17u);
x_4 = l_Lean_Expr_updateLambda_x21___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -8004,7 +8026,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(849u);
x_2 = lean_unsigned_to_nat(852u);
x_3 = lean_unsigned_to_nat(17u);
x_4 = l_Lean_Expr_updateLambda_x21___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -8048,7 +8070,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(858u);
x_2 = lean_unsigned_to_nat(861u);
x_3 = lean_unsigned_to_nat(20u);
x_4 = l_Lean_Expr_letName_x21___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);

1346
stage0/stdlib/Init/Lean/Meta/AppBuilder.c
View file

File diff suppressed because it is too large Load diff

8240
stage0/stdlib/Init/Lean/Meta/ExprDefEq.c
View file

File diff suppressed because it is too large Load diff

139
stage0/stdlib/Init/Lean/Meta/RecursorInfo.c
View file

@ -16,6 +16,7 @@ extern "C" {
lean_object* l_Lean_Meta_RecursorInfo_HasToString___closed__7;
lean_object* l_Lean_Meta_recursorAttribute;
extern lean_object* l_Lean_Name_toString___closed__1;
lean_object* l_Lean_Meta_brecOnSuffix___closed__1;
lean_object* lean_array_set(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Option_HasRepr___rarg___closed__2;
lean_object* l_Lean_Syntax_isNatLitAux(lean_object*, lean_object*);
@ -54,6 +55,7 @@ lean_object* lean_io_ref_get(lean_object*, lean_object*);
lean_object* l_Array_findIdxMAux___main___at___private_Init_Lean_Meta_RecursorInfo_7__getIndicesPos___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Meta_RecursorInfo_isMinor(lean_object*, lean_object*);
lean_object* l_Lean_Meta_RecursorInfo_HasToString___closed__14;
lean_object* l_Lean_Meta_recOnSuffix;
lean_object* l_Lean_Meta_RecursorInfo_HasToString___closed__5;
lean_object* l_Lean_Meta_RecursorInfo_numParams(lean_object*);
lean_object* l___private_Init_Data_Array_QSort_1__partitionAux___main___at_Lean_Meta_mkRecursorAttr___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -103,6 +105,7 @@ lean_object* l_Lean_Meta_RecursorInfo_HasToString___closed__4;
lean_object* l___private_Init_Lean_Meta_RecursorInfo_10__getProduceMotiveAndRecursive(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_getAppNumArgsAux___main(lean_object*, lean_object*);
lean_object* l_List_replicate___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Meta_casesOnSuffix;
lean_object* l_Lean_Meta_RecursorInfo_numParams___boxed(lean_object*);
lean_object* l___private_Init_Lean_Meta_RecursorInfo_3__checkMotive___closed__2;
lean_object* l___private_Init_Lean_Meta_RecursorInfo_5__getMajorPosDepElim___closed__7;
@ -110,6 +113,7 @@ lean_object* l_Lean_Expr_withAppAux___main___at___private_Init_Lean_Meta_Recurso
lean_object* l_Array_binSearchAux___main___at_Lean_Meta_getMajorPos_x3f___spec__3(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_RecursorInfo_HasToString___closed__13;
lean_object* l_Lean_RecursorVal_getMajorIdx(lean_object*);
lean_object* l_Lean_Meta_brecOnSuffix;
lean_object* l_List_toStringAux___main___at_Lean_Meta_RecursorInfo_HasToString___spec__6(uint8_t, lean_object*);
lean_object* l_Lean_registerParametricAttribute___at_Lean_Meta_mkRecursorAttr___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
lean_object* lean_array_fget(lean_object*, lean_object*);
@ -138,7 +142,6 @@ lean_object* l_Nat_foldMAux___main___at___private_Init_Lean_Meta_RecursorInfo_10
lean_object* l_Nat_foldMAux___main___at___private_Init_Lean_Meta_RecursorInfo_6__getParamsPos___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_fvarId_x21(lean_object*);
lean_object* l___private_Init_Lean_Meta_RecursorInfo_2__getMajorPosIfAuxRecursor_x3f___closed__3;
lean_object* l_List_lengthAux___main___rarg(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_RecursorInfo_9__getUnivLevelPos___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_ConstantInfo_name(lean_object*);
@ -170,6 +173,7 @@ lean_object* l_addParenHeuristic(lean_object*);
lean_object* l_List_toStringAux___main___at_Lean_Meta_RecursorInfo_HasToString___spec__8___boxed(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_RecursorInfo_3__checkMotive___closed__1;
lean_object* l_List_foldlM___main___at___private_Init_Lean_Meta_RecursorInfo_9__getUnivLevelPos___spec__2___closed__1;
lean_object* l_Lean_Meta_mkRecOnFor(lean_object*);
extern lean_object* l_Lean_mkRecFor___closed__1;
extern lean_object* l_Lean_registerParametricAttribute___rarg___closed__1;
lean_object* l_Lean_Meta_RecursorUnivLevelPos_hasToString___closed__1;
@ -203,9 +207,11 @@ lean_object* l___private_Init_Lean_Meta_RecursorInfo_11__checkMotiveResultType__
lean_object* l___private_Init_Data_Array_QSort_1__partitionAux___main___at_Lean_Meta_mkRecursorAttr___spec__4___closed__1;
lean_object* l___private_Init_Lean_Meta_RecursorInfo_3__checkMotive(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
size_t l_USize_mod(size_t, size_t);
lean_object* l_Lean_Meta_mkBRecOnFor(lean_object*);
lean_object* l_Lean_RecursorVal_getInduct(lean_object*);
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
lean_object* l_Lean_ConstantInfo_lparams(lean_object*);
lean_object* l_Lean_Meta_casesOnSuffix___closed__1;
lean_object* l___private_Init_Lean_Meta_RecursorInfo_5__getMajorPosDepElim___closed__3;
extern lean_object* l_Option_HasRepr___rarg___closed__3;
lean_object* l_Lean_Meta_RecursorInfo_HasToString___closed__11;
@ -237,6 +243,7 @@ lean_object* lean_io_ref_reset(lean_object*, lean_object*);
extern lean_object* l_Lean_registerEnvExtensionUnsafe___rarg___closed__2;
lean_object* l_Lean_registerParametricAttribute___at_Lean_Meta_mkRecursorAttr___spec__1___closed__1;
lean_object* l_Lean_registerParametricAttribute___at_Lean_Meta_mkRecursorAttr___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkCasesOnFor(lean_object*);
lean_object* l_Lean_Meta_RecursorInfo_motivePos(lean_object*);
uint8_t l_Lean_Expr_isFVar(lean_object*);
lean_object* l_Lean_Expr_withAppAux___main___at___private_Init_Lean_Meta_RecursorInfo_10__getProduceMotiveAndRecursive___spec__3(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -263,7 +270,6 @@ lean_object* l_Lean_PersistentEnvExtension_getState___rarg(lean_object*, lean_ob
lean_object* lean_io_initializing(lean_object*);
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__2;
lean_object* l_Array_findIdxMAux___main___at___private_Init_Lean_Meta_RecursorInfo_6__getParamsPos___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_RecursorInfo_2__getMajorPosIfAuxRecursor_x3f___closed__4;
lean_object* l_Lean_Expr_withAppAux___main___at___private_Init_Lean_Meta_RecursorInfo_12__mkRecursorInfoAux___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_foldMAux___main___at___private_Init_Lean_Meta_RecursorInfo_7__getIndicesPos___spec__2___closed__1;
lean_object* l___private_Init_Lean_Meta_RecursorInfo_6__getParamsPos(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -291,9 +297,9 @@ lean_object* l_Array_anyRangeMAux___main___at___private_Init_Lean_Meta_RecursorI
lean_object* l_Array_findIdxMAux___main___at___private_Init_Lean_Meta_RecursorInfo_7__getIndicesPos___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_RecursorInfo_13__syntaxToMajorPos___closed__1;
lean_object* l_Lean_Meta_mkRecursorAttr___closed__2;
lean_object* l___private_Init_Lean_Meta_RecursorInfo_2__getMajorPosIfAuxRecursor_x3f___closed__5;
lean_object* l_Lean_Expr_withAppAux___main___at___private_Init_Lean_Meta_RecursorInfo_12__mkRecursorInfoAux___spec__1___lambda__1___boxed(lean_object**);
uint8_t l_Array_anyRangeMAux___main___at_Lean_Meta_mkRecursorAttr___spec__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_recOnSuffix___closed__1;
lean_object* l_Lean_registerParametricAttribute___at_Lean_Meta_mkRecursorAttr___spec__1___lambda__1(lean_object*);
lean_object* l_Lean_Meta_mkRecursorAttr___closed__1;
lean_object* l_Lean_Meta_forallTelescopeReducing___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@ -303,6 +309,81 @@ uint8_t l_Lean_Expr_isSort(lean_object*);
lean_object* l_Lean_Meta_RecursorInfo_numIndices___boxed(lean_object*);
uint8_t lean_string_dec_eq(lean_object*, lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
lean_object* _init_l_Lean_Meta_casesOnSuffix___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("casesOn");
return x_1;
}
}
lean_object* _init_l_Lean_Meta_casesOnSuffix() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Meta_casesOnSuffix___closed__1;
return x_1;
}
}
lean_object* _init_l_Lean_Meta_recOnSuffix___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("recOn");
return x_1;
}
}
lean_object* _init_l_Lean_Meta_recOnSuffix() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Meta_recOnSuffix___closed__1;
return x_1;
}
}
lean_object* _init_l_Lean_Meta_brecOnSuffix___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("brecOn");
return x_1;
}
}
lean_object* _init_l_Lean_Meta_brecOnSuffix() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Meta_brecOnSuffix___closed__1;
return x_1;
}
}
lean_object* l_Lean_Meta_mkCasesOnFor(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_Meta_casesOnSuffix;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Meta_mkRecOnFor(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_Meta_recOnSuffix;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Meta_mkBRecOnFor(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_Meta_brecOnSuffix;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Meta_RecursorUnivLevelPos_hasToString___closed__1() {
_start:
{
@ -1738,30 +1819,6 @@ lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* _init_l___private_Init_Lean_Meta_RecursorInfo_2__getMajorPosIfAuxRecursor_x3f___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("casesOn");
return x_1;
}
}
lean_object* _init_l___private_Init_Lean_Meta_RecursorInfo_2__getMajorPosIfAuxRecursor_x3f___closed__4() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("recOn");
return x_1;
}
}
lean_object* _init_l___private_Init_Lean_Meta_RecursorInfo_2__getMajorPosIfAuxRecursor_x3f___closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("brecOn");
return x_1;
}
}
lean_object* l___private_Init_Lean_Meta_RecursorInfo_2__getMajorPosIfAuxRecursor_x3f(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
@ -1793,17 +1850,17 @@ lean_inc(x_10);
x_11 = lean_ctor_get(x_1, 1);
lean_inc(x_11);
lean_dec(x_1);
x_57 = l___private_Init_Lean_Meta_RecursorInfo_2__getMajorPosIfAuxRecursor_x3f___closed__4;
x_57 = l_Lean_Meta_recOnSuffix;
x_58 = lean_string_dec_eq(x_11, x_57);
if (x_58 == 0)
{
lean_object* x_59; uint8_t x_60;
x_59 = l___private_Init_Lean_Meta_RecursorInfo_2__getMajorPosIfAuxRecursor_x3f___closed__3;
x_59 = l_Lean_Meta_casesOnSuffix;
x_60 = lean_string_dec_eq(x_11, x_59);
if (x_60 == 0)
{
lean_object* x_61; uint8_t x_62;
x_61 = l___private_Init_Lean_Meta_RecursorInfo_2__getMajorPosIfAuxRecursor_x3f___closed__5;
x_61 = l_Lean_Meta_brecOnSuffix;
x_62 = lean_string_dec_eq(x_11, x_61);
if (x_62 == 0)
{
@ -1870,7 +1927,7 @@ lean_inc(x_21);
x_22 = lean_nat_add(x_20, x_21);
lean_dec(x_21);
lean_dec(x_20);
x_23 = l___private_Init_Lean_Meta_RecursorInfo_2__getMajorPosIfAuxRecursor_x3f___closed__3;
x_23 = l_Lean_Meta_casesOnSuffix;
x_24 = lean_string_dec_eq(x_11, x_23);
lean_dec(x_11);
if (x_24 == 0)
@ -1916,7 +1973,7 @@ lean_inc(x_34);
x_35 = lean_nat_add(x_33, x_34);
lean_dec(x_34);
lean_dec(x_33);
x_36 = l___private_Init_Lean_Meta_RecursorInfo_2__getMajorPosIfAuxRecursor_x3f___closed__3;
x_36 = l_Lean_Meta_casesOnSuffix;
x_37 = lean_string_dec_eq(x_11, x_36);
lean_dec(x_11);
if (x_37 == 0)
@ -9771,6 +9828,18 @@ lean_dec_ref(res);
res = initialize_Init_Lean_Meta_Message(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Meta_casesOnSuffix___closed__1 = _init_l_Lean_Meta_casesOnSuffix___closed__1();
lean_mark_persistent(l_Lean_Meta_casesOnSuffix___closed__1);
l_Lean_Meta_casesOnSuffix = _init_l_Lean_Meta_casesOnSuffix();
lean_mark_persistent(l_Lean_Meta_casesOnSuffix);
l_Lean_Meta_recOnSuffix___closed__1 = _init_l_Lean_Meta_recOnSuffix___closed__1();
lean_mark_persistent(l_Lean_Meta_recOnSuffix___closed__1);
l_Lean_Meta_recOnSuffix = _init_l_Lean_Meta_recOnSuffix();
lean_mark_persistent(l_Lean_Meta_recOnSuffix);
l_Lean_Meta_brecOnSuffix___closed__1 = _init_l_Lean_Meta_brecOnSuffix___closed__1();
lean_mark_persistent(l_Lean_Meta_brecOnSuffix___closed__1);
l_Lean_Meta_brecOnSuffix = _init_l_Lean_Meta_brecOnSuffix();
lean_mark_persistent(l_Lean_Meta_brecOnSuffix);
l_Lean_Meta_RecursorUnivLevelPos_hasToString___closed__1 = _init_l_Lean_Meta_RecursorUnivLevelPos_hasToString___closed__1();
lean_mark_persistent(l_Lean_Meta_RecursorUnivLevelPos_hasToString___closed__1);
l_List_toStringAux___main___at_Lean_Meta_RecursorInfo_HasToString___spec__2___closed__1 = _init_l_List_toStringAux___main___at_Lean_Meta_RecursorInfo_HasToString___spec__2___closed__1();
@ -9821,12 +9890,6 @@ l___private_Init_Lean_Meta_RecursorInfo_2__getMajorPosIfAuxRecursor_x3f___closed
lean_mark_persistent(l___private_Init_Lean_Meta_RecursorInfo_2__getMajorPosIfAuxRecursor_x3f___closed__1);
l___private_Init_Lean_Meta_RecursorInfo_2__getMajorPosIfAuxRecursor_x3f___closed__2 = _init_l___private_Init_Lean_Meta_RecursorInfo_2__getMajorPosIfAuxRecursor_x3f___closed__2();
lean_mark_persistent(l___private_Init_Lean_Meta_RecursorInfo_2__getMajorPosIfAuxRecursor_x3f___closed__2);
l___private_Init_Lean_Meta_RecursorInfo_2__getMajorPosIfAuxRecursor_x3f___closed__3 = _init_l___private_Init_Lean_Meta_RecursorInfo_2__getMajorPosIfAuxRecursor_x3f___closed__3();
lean_mark_persistent(l___private_Init_Lean_Meta_RecursorInfo_2__getMajorPosIfAuxRecursor_x3f___closed__3);
l___private_Init_Lean_Meta_RecursorInfo_2__getMajorPosIfAuxRecursor_x3f___closed__4 = _init_l___private_Init_Lean_Meta_RecursorInfo_2__getMajorPosIfAuxRecursor_x3f___closed__4();
lean_mark_persistent(l___private_Init_Lean_Meta_RecursorInfo_2__getMajorPosIfAuxRecursor_x3f___closed__4);
l___private_Init_Lean_Meta_RecursorInfo_2__getMajorPosIfAuxRecursor_x3f___closed__5 = _init_l___private_Init_Lean_Meta_RecursorInfo_2__getMajorPosIfAuxRecursor_x3f___closed__5();
lean_mark_persistent(l___private_Init_Lean_Meta_RecursorInfo_2__getMajorPosIfAuxRecursor_x3f___closed__5);
l___private_Init_Lean_Meta_RecursorInfo_3__checkMotive___closed__1 = _init_l___private_Init_Lean_Meta_RecursorInfo_3__checkMotive___closed__1();
lean_mark_persistent(l___private_Init_Lean_Meta_RecursorInfo_3__checkMotive___closed__1);
l___private_Init_Lean_Meta_RecursorInfo_3__checkMotive___closed__2 = _init_l___private_Init_Lean_Meta_RecursorInfo_3__checkMotive___closed__2();

3805
stage0/stdlib/Init/Lean/Meta/Tactic/Cases.c
View file

File diff suppressed because it is too large Load diff

432
stage0/stdlib/Init/Lean/Meta/Tactic/FVarSubst.c
View file

@ -14,35 +14,49 @@
extern "C" {
#endif
lean_object* lean_expr_update_forall(lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_RBNode_find___main___at_Lean_Meta_FVarSubst_apply___spec__1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Meta_FVarSubst_apply___boxed(lean_object*, lean_object*);
lean_object* l_unreachable_x21___rarg(lean_object*);
uint8_t l_USize_decEq(size_t, size_t);
lean_object* lean_array_uget(lean_object*, size_t);
lean_object* lean_expr_update_mdata(lean_object*, lean_object*);
uint8_t l_Lean_Name_quickLt(lean_object*, lean_object*);
lean_object* l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___at_Lean_Meta_FVarSubst_apply___spec__2(lean_object*, size_t, lean_object*, lean_object*);
lean_object* l_Lean_Meta_FVarSubst_erase(lean_object*, lean_object*);
lean_object* lean_array_uset(lean_object*, size_t, lean_object*);
lean_object* l_RBNode_del___main___at_Lean_Meta_FVarSubst_erase___spec__2___boxed(lean_object*, lean_object*);
lean_object* l_RBNode_fold___main___at_Lean_Meta_FVarSubst_compose___spec__1(lean_object*, lean_object*);
lean_object* l_RBNode_find___main___at_Lean_Meta_FVarSubst_get___spec__1(lean_object*, lean_object*);
lean_object* l_RBNode_balRight___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_NameMap_contains___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___at_Lean_Meta_FVarSubst_apply___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_FVarSubst_apply(lean_object*, lean_object*);
lean_object* l_RBNode_find___main___at_Lean_Meta_FVarSubst_apply___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___at_Lean_Meta_FVarSubst_apply___spec__1(lean_object*, size_t, lean_object*, lean_object*);
lean_object* l_Lean_Meta_FVarSubst_get___boxed(lean_object*, lean_object*);
extern lean_object* l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___closed__2;
uint8_t l_Lean_Meta_FVarSubst_contains(lean_object*, lean_object*);
lean_object* lean_expr_update_let(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkFVar(lean_object*);
uint8_t l_Lean_Expr_Data_binderInfo(uint64_t);
lean_object* l_Lean_Meta_FVarSubst_contains___boxed(lean_object*, lean_object*);
lean_object* lean_expr_update_proj(lean_object*, lean_object*);
size_t l_USize_mod(size_t, size_t);
lean_object* l_Lean_Meta_FVarSubst_get(lean_object*, lean_object*);
size_t lean_ptr_addr(lean_object*);
lean_object* l_Lean_Meta_FVarSubst_empty;
lean_object* l_RBNode_erase___at_Lean_Meta_FVarSubst_erase___spec__1___boxed(lean_object*, lean_object*);
lean_object* l_RBNode_appendTrees___main___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Meta_FVarSubst_insert(lean_object*, lean_object*, lean_object*);
lean_object* l_RBNode_balLeft___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_RBNode_find___main___at_Lean_Meta_FVarSubst_get___spec__1___boxed(lean_object*, lean_object*);
lean_object* l_RBNode_setBlack___rarg(lean_object*);
lean_object* lean_expr_update_lambda(lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Meta_FVarSubst_compose(lean_object*, lean_object*);
lean_object* l_RBNode_del___main___at_Lean_Meta_FVarSubst_erase___spec__2(lean_object*, lean_object*);
lean_object* l_Lean_Meta_FVarSubst_erase___boxed(lean_object*, lean_object*);
lean_object* lean_expr_update_app(lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Expr_hasFVar(lean_object*);
lean_object* l_RBNode_erase___at_Lean_Meta_FVarSubst_erase___spec__1(lean_object*, lean_object*);
uint8_t l_RBNode_isBlack___rarg(lean_object*);
lean_object* l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___at_Lean_Meta_FVarSubst_apply___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Expr_ReplaceImpl_initCache;
lean_object* _init_l_Lean_Meta_FVarSubst_empty() {
_start:
@ -79,7 +93,209 @@ x_4 = lean_box(x_3);
return x_4;
}
}
lean_object* l_RBNode_find___main___at_Lean_Meta_FVarSubst_apply___spec__1(lean_object* x_1, lean_object* x_2) {
lean_object* l_RBNode_del___main___at_Lean_Meta_FVarSubst_erase___spec__2(lean_object* x_1, lean_object* x_2) {
_start:
{
if (lean_obj_tag(x_2) == 0)
{
return x_2;
}
else
{
uint8_t x_3;
x_3 = !lean_is_exclusive(x_2);
if (x_3 == 0)
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; uint8_t x_8;
x_4 = lean_ctor_get(x_2, 0);
x_5 = lean_ctor_get(x_2, 1);
x_6 = lean_ctor_get(x_2, 2);
x_7 = lean_ctor_get(x_2, 3);
x_8 = l_Lean_Name_quickLt(x_1, x_5);
if (x_8 == 0)
{
uint8_t x_9;
x_9 = l_Lean_Name_quickLt(x_5, x_1);
if (x_9 == 0)
{
lean_object* x_10;
lean_free_object(x_2);
lean_dec(x_6);
lean_dec(x_5);
x_10 = l_RBNode_appendTrees___main___rarg(x_4, x_7);
return x_10;
}
else
{
uint8_t x_11;
x_11 = l_RBNode_isBlack___rarg(x_7);
if (x_11 == 0)
{
lean_object* x_12; uint8_t x_13;
x_12 = l_RBNode_del___main___at_Lean_Meta_FVarSubst_erase___spec__2(x_1, x_7);
x_13 = 0;
lean_ctor_set(x_2, 3, x_12);
lean_ctor_set_uint8(x_2, sizeof(void*)*4, x_13);
return x_2;
}
else
{
lean_object* x_14; lean_object* x_15;
lean_free_object(x_2);
x_14 = l_RBNode_del___main___at_Lean_Meta_FVarSubst_erase___spec__2(x_1, x_7);
x_15 = l_RBNode_balRight___rarg(x_4, x_5, x_6, x_14);
return x_15;
}
}
}
else
{
uint8_t x_16;
x_16 = l_RBNode_isBlack___rarg(x_4);
if (x_16 == 0)
{
lean_object* x_17; uint8_t x_18;
x_17 = l_RBNode_del___main___at_Lean_Meta_FVarSubst_erase___spec__2(x_1, x_4);
x_18 = 0;
lean_ctor_set(x_2, 0, x_17);
lean_ctor_set_uint8(x_2, sizeof(void*)*4, x_18);
return x_2;
}
else
{
lean_object* x_19; lean_object* x_20;
lean_free_object(x_2);
x_19 = l_RBNode_del___main___at_Lean_Meta_FVarSubst_erase___spec__2(x_1, x_4);
x_20 = l_RBNode_balLeft___rarg(x_19, x_5, x_6, x_7);
return x_20;
}
}
}
else
{
lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; uint8_t x_25;
x_21 = lean_ctor_get(x_2, 0);
x_22 = lean_ctor_get(x_2, 1);
x_23 = lean_ctor_get(x_2, 2);
x_24 = lean_ctor_get(x_2, 3);
lean_inc(x_24);
lean_inc(x_23);
lean_inc(x_22);
lean_inc(x_21);
lean_dec(x_2);
x_25 = l_Lean_Name_quickLt(x_1, x_22);
if (x_25 == 0)
{
uint8_t x_26;
x_26 = l_Lean_Name_quickLt(x_22, x_1);
if (x_26 == 0)
{
lean_object* x_27;
lean_dec(x_23);
lean_dec(x_22);
x_27 = l_RBNode_appendTrees___main___rarg(x_21, x_24);
return x_27;
}
else
{
uint8_t x_28;
x_28 = l_RBNode_isBlack___rarg(x_24);
if (x_28 == 0)
{
lean_object* x_29; uint8_t x_30; lean_object* x_31;
x_29 = l_RBNode_del___main___at_Lean_Meta_FVarSubst_erase___spec__2(x_1, x_24);
x_30 = 0;
x_31 = lean_alloc_ctor(1, 4, 1);
lean_ctor_set(x_31, 0, x_21);
lean_ctor_set(x_31, 1, x_22);
lean_ctor_set(x_31, 2, x_23);
lean_ctor_set(x_31, 3, x_29);
lean_ctor_set_uint8(x_31, sizeof(void*)*4, x_30);
return x_31;
}
else
{
lean_object* x_32; lean_object* x_33;
x_32 = l_RBNode_del___main___at_Lean_Meta_FVarSubst_erase___spec__2(x_1, x_24);
x_33 = l_RBNode_balRight___rarg(x_21, x_22, x_23, x_32);
return x_33;
}
}
}
else
{
uint8_t x_34;
x_34 = l_RBNode_isBlack___rarg(x_21);
if (x_34 == 0)
{
lean_object* x_35; uint8_t x_36; lean_object* x_37;
x_35 = l_RBNode_del___main___at_Lean_Meta_FVarSubst_erase___spec__2(x_1, x_21);
x_36 = 0;
x_37 = lean_alloc_ctor(1, 4, 1);
lean_ctor_set(x_37, 0, x_35);
lean_ctor_set(x_37, 1, x_22);
lean_ctor_set(x_37, 2, x_23);
lean_ctor_set(x_37, 3, x_24);
lean_ctor_set_uint8(x_37, sizeof(void*)*4, x_36);
return x_37;
}
else
{
lean_object* x_38; lean_object* x_39;
x_38 = l_RBNode_del___main___at_Lean_Meta_FVarSubst_erase___spec__2(x_1, x_21);
x_39 = l_RBNode_balLeft___rarg(x_38, x_22, x_23, x_24);
return x_39;
}
}
}
}
}
}
lean_object* l_RBNode_erase___at_Lean_Meta_FVarSubst_erase___spec__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4;
x_3 = l_RBNode_del___main___at_Lean_Meta_FVarSubst_erase___spec__2(x_1, x_2);
x_4 = l_RBNode_setBlack___rarg(x_3);
return x_4;
}
}
lean_object* l_Lean_Meta_FVarSubst_erase(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_RBNode_erase___at_Lean_Meta_FVarSubst_erase___spec__1(x_2, x_1);
return x_3;
}
}
lean_object* l_RBNode_del___main___at_Lean_Meta_FVarSubst_erase___spec__2___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_RBNode_del___main___at_Lean_Meta_FVarSubst_erase___spec__2(x_1, x_2);
lean_dec(x_1);
return x_3;
}
}
lean_object* l_RBNode_erase___at_Lean_Meta_FVarSubst_erase___spec__1___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_RBNode_erase___at_Lean_Meta_FVarSubst_erase___spec__1(x_1, x_2);
lean_dec(x_1);
return x_3;
}
}
lean_object* l_Lean_Meta_FVarSubst_erase___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_Meta_FVarSubst_erase(x_1, x_2);
lean_dec(x_2);
return x_3;
}
}
lean_object* l_RBNode_find___main___at_Lean_Meta_FVarSubst_get___spec__1(lean_object* x_1, lean_object* x_2) {
_start:
{
if (lean_obj_tag(x_1) == 0)
@ -122,78 +338,106 @@ goto _start;
}
}
}
lean_object* l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___at_Lean_Meta_FVarSubst_apply___spec__2(lean_object* x_1, size_t x_2, lean_object* x_3, lean_object* x_4) {
lean_object* l_Lean_Meta_FVarSubst_get(lean_object* x_1, lean_object* x_2) {
_start:
{
size_t x_5; size_t x_6; lean_object* x_7; lean_object* x_159; lean_object* x_160; size_t x_161; uint8_t x_162;
lean_object* x_3;
x_3 = l_RBNode_find___main___at_Lean_Meta_FVarSubst_get___spec__1(x_1, x_2);
if (lean_obj_tag(x_3) == 0)
{
lean_inc(x_2);
return x_2;
}
else
{
lean_object* x_4;
x_4 = lean_ctor_get(x_3, 0);
lean_inc(x_4);
lean_dec(x_3);
return x_4;
}
}
}
lean_object* l_RBNode_find___main___at_Lean_Meta_FVarSubst_get___spec__1___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_RBNode_find___main___at_Lean_Meta_FVarSubst_get___spec__1(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
return x_3;
}
}
lean_object* l_Lean_Meta_FVarSubst_get___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_Meta_FVarSubst_get(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
return x_3;
}
}
lean_object* l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___at_Lean_Meta_FVarSubst_apply___spec__1(lean_object* x_1, size_t x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
size_t x_5; size_t x_6; lean_object* x_7; lean_object* x_159; lean_object* x_160; lean_object* x_167; size_t x_168; uint8_t x_169;
x_5 = lean_ptr_addr(x_3);
x_6 = x_2 == 0 ? 0 : x_5 % x_2;
x_159 = lean_ctor_get(x_4, 0);
lean_inc(x_159);
x_160 = lean_array_uget(x_159, x_6);
x_161 = lean_ptr_addr(x_160);
lean_dec(x_160);
x_162 = x_161 == x_5;
if (x_162 == 0)
x_167 = lean_array_uget(x_159, x_6);
x_168 = lean_ptr_addr(x_167);
lean_dec(x_167);
x_169 = x_168 == x_5;
if (x_169 == 0)
{
if (lean_obj_tag(x_3) == 1)
{
lean_object* x_163; lean_object* x_164;
x_163 = lean_ctor_get(x_3, 0);
lean_inc(x_163);
x_164 = l_RBNode_find___main___at_Lean_Meta_FVarSubst_apply___spec__1(x_1, x_163);
lean_dec(x_163);
if (lean_obj_tag(x_164) == 0)
lean_object* x_170; lean_object* x_171;
x_170 = lean_ctor_get(x_3, 0);
lean_inc(x_170);
x_171 = l_RBNode_find___main___at_Lean_Meta_FVarSubst_get___spec__1(x_1, x_170);
lean_dec(x_170);
if (lean_obj_tag(x_171) == 0)
{
lean_object* x_165;
lean_dec(x_159);
x_165 = lean_box(0);
x_7 = x_165;
goto block_158;
lean_inc(x_3);
x_160 = x_3;
goto block_166;
}
else
{
lean_object* x_166; lean_object* x_167; lean_object* x_168; lean_object* x_169; lean_object* x_170; lean_object* x_171;
x_166 = lean_ctor_get(x_164, 0);
lean_inc(x_166);
lean_dec(x_164);
x_167 = lean_array_uset(x_159, x_6, x_3);
x_168 = lean_ctor_get(x_4, 1);
lean_inc(x_168);
lean_dec(x_4);
lean_inc(x_166);
x_169 = lean_array_uset(x_168, x_6, x_166);
x_170 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_170, 0, x_167);
lean_ctor_set(x_170, 1, x_169);
x_171 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_171, 0, x_166);
lean_ctor_set(x_171, 1, x_170);
return x_171;
lean_object* x_172; lean_object* x_173;
x_172 = lean_ctor_get(x_171, 0);
lean_inc(x_172);
lean_dec(x_171);
x_173 = l_Lean_mkFVar(x_172);
x_160 = x_173;
goto block_166;
}
}
else
{
lean_object* x_172;
lean_object* x_174;
lean_dec(x_159);
x_172 = lean_box(0);
x_7 = x_172;
x_174 = lean_box(0);
x_7 = x_174;
goto block_158;
}
}
else
{
lean_object* x_173; lean_object* x_174; lean_object* x_175;
lean_object* x_175; lean_object* x_176; lean_object* x_177;
lean_dec(x_159);
lean_dec(x_3);
x_173 = lean_ctor_get(x_4, 1);
lean_inc(x_173);
x_174 = lean_array_uget(x_173, x_6);
lean_dec(x_173);
x_175 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_175, 0, x_174);
lean_ctor_set(x_175, 1, x_4);
return x_175;
x_175 = lean_ctor_get(x_4, 1);
lean_inc(x_175);
x_176 = lean_array_uget(x_175, x_6);
lean_dec(x_175);
x_177 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_177, 0, x_176);
lean_ctor_set(x_177, 1, x_4);
return x_177;
}
block_158:
{
@ -206,13 +450,13 @@ x_8 = lean_ctor_get(x_3, 0);
lean_inc(x_8);
x_9 = lean_ctor_get(x_3, 1);
lean_inc(x_9);
x_10 = l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___at_Lean_Meta_FVarSubst_apply___spec__2(x_1, x_2, x_8, x_4);
x_10 = l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___at_Lean_Meta_FVarSubst_apply___spec__1(x_1, x_2, x_8, x_4);
x_11 = lean_ctor_get(x_10, 0);
lean_inc(x_11);
x_12 = lean_ctor_get(x_10, 1);
lean_inc(x_12);
lean_dec(x_10);
x_13 = l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___at_Lean_Meta_FVarSubst_apply___spec__2(x_1, x_2, x_9, x_12);
x_13 = l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___at_Lean_Meta_FVarSubst_apply___spec__1(x_1, x_2, x_9, x_12);
x_14 = !lean_is_exclusive(x_13);
if (x_14 == 0)
{
@ -271,13 +515,13 @@ lean_inc(x_32);
x_33 = lean_ctor_get(x_3, 2);
lean_inc(x_33);
x_34 = lean_ctor_get_uint64(x_3, sizeof(void*)*3);
x_35 = l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___at_Lean_Meta_FVarSubst_apply___spec__2(x_1, x_2, x_32, x_4);
x_35 = l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___at_Lean_Meta_FVarSubst_apply___spec__1(x_1, x_2, x_32, x_4);
x_36 = lean_ctor_get(x_35, 0);
lean_inc(x_36);
x_37 = lean_ctor_get(x_35, 1);
lean_inc(x_37);
lean_dec(x_35);
x_38 = l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___at_Lean_Meta_FVarSubst_apply___spec__2(x_1, x_2, x_33, x_37);
x_38 = l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___at_Lean_Meta_FVarSubst_apply___spec__1(x_1, x_2, x_33, x_37);
x_39 = !lean_is_exclusive(x_38);
if (x_39 == 0)
{
@ -338,13 +582,13 @@ lean_inc(x_59);
x_60 = lean_ctor_get(x_3, 2);
lean_inc(x_60);
x_61 = lean_ctor_get_uint64(x_3, sizeof(void*)*3);
x_62 = l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___at_Lean_Meta_FVarSubst_apply___spec__2(x_1, x_2, x_59, x_4);
x_62 = l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___at_Lean_Meta_FVarSubst_apply___spec__1(x_1, x_2, x_59, x_4);
x_63 = lean_ctor_get(x_62, 0);
lean_inc(x_63);
x_64 = lean_ctor_get(x_62, 1);
lean_inc(x_64);
lean_dec(x_62);
x_65 = l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___at_Lean_Meta_FVarSubst_apply___spec__2(x_1, x_2, x_60, x_64);
x_65 = l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___at_Lean_Meta_FVarSubst_apply___spec__1(x_1, x_2, x_60, x_64);
x_66 = !lean_is_exclusive(x_65);
if (x_66 == 0)
{
@ -406,19 +650,19 @@ x_87 = lean_ctor_get(x_3, 2);
lean_inc(x_87);
x_88 = lean_ctor_get(x_3, 3);
lean_inc(x_88);
x_89 = l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___at_Lean_Meta_FVarSubst_apply___spec__2(x_1, x_2, x_86, x_4);
x_89 = l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___at_Lean_Meta_FVarSubst_apply___spec__1(x_1, x_2, x_86, x_4);
x_90 = lean_ctor_get(x_89, 0);
lean_inc(x_90);
x_91 = lean_ctor_get(x_89, 1);
lean_inc(x_91);
lean_dec(x_89);
x_92 = l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___at_Lean_Meta_FVarSubst_apply___spec__2(x_1, x_2, x_87, x_91);
x_92 = l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___at_Lean_Meta_FVarSubst_apply___spec__1(x_1, x_2, x_87, x_91);
x_93 = lean_ctor_get(x_92, 0);
lean_inc(x_93);
x_94 = lean_ctor_get(x_92, 1);
lean_inc(x_94);
lean_dec(x_92);
x_95 = l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___at_Lean_Meta_FVarSubst_apply___spec__2(x_1, x_2, x_88, x_94);
x_95 = l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___at_Lean_Meta_FVarSubst_apply___spec__1(x_1, x_2, x_88, x_94);
x_96 = !lean_is_exclusive(x_95);
if (x_96 == 0)
{
@ -474,7 +718,7 @@ case 10:
lean_object* x_114; lean_object* x_115; uint8_t x_116;
x_114 = lean_ctor_get(x_3, 1);
lean_inc(x_114);
x_115 = l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___at_Lean_Meta_FVarSubst_apply___spec__2(x_1, x_2, x_114, x_4);
x_115 = l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___at_Lean_Meta_FVarSubst_apply___spec__1(x_1, x_2, x_114, x_4);
x_116 = !lean_is_exclusive(x_115);
if (x_116 == 0)
{
@ -530,7 +774,7 @@ case 11:
lean_object* x_134; lean_object* x_135; uint8_t x_136;
x_134 = lean_ctor_get(x_3, 2);
lean_inc(x_134);
x_135 = l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___at_Lean_Meta_FVarSubst_apply___spec__2(x_1, x_2, x_134, x_4);
x_135 = l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___at_Lean_Meta_FVarSubst_apply___spec__1(x_1, x_2, x_134, x_4);
x_136 = !lean_is_exclusive(x_135);
if (x_136 == 0)
{
@ -600,6 +844,23 @@ return x_157;
}
}
}
block_166:
{
lean_object* x_161; lean_object* x_162; lean_object* x_163; lean_object* x_164; lean_object* x_165;
x_161 = lean_array_uset(x_159, x_6, x_3);
x_162 = lean_ctor_get(x_4, 1);
lean_inc(x_162);
lean_dec(x_4);
lean_inc(x_160);
x_163 = lean_array_uset(x_162, x_6, x_160);
x_164 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_164, 0, x_161);
lean_ctor_set(x_164, 1, x_163);
x_165 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_165, 0, x_160);
lean_ctor_set(x_165, 1, x_164);
return x_165;
}
}
}
lean_object* l_Lean_Meta_FVarSubst_apply(lean_object* x_1, lean_object* x_2) {
@ -622,7 +883,7 @@ else
size_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_4 = 8192;
x_5 = l_Lean_Expr_ReplaceImpl_initCache;
x_6 = l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___at_Lean_Meta_FVarSubst_apply___spec__2(x_1, x_4, x_2, x_5);
x_6 = l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___at_Lean_Meta_FVarSubst_apply___spec__1(x_1, x_4, x_2, x_5);
x_7 = lean_ctor_get(x_6, 0);
lean_inc(x_7);
lean_dec(x_6);
@ -631,23 +892,13 @@ return x_7;
}
}
}
lean_object* l_RBNode_find___main___at_Lean_Meta_FVarSubst_apply___spec__1___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_RBNode_find___main___at_Lean_Meta_FVarSubst_apply___spec__1(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
return x_3;
}
}
lean_object* l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___at_Lean_Meta_FVarSubst_apply___spec__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
lean_object* l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___at_Lean_Meta_FVarSubst_apply___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
size_t x_5; lean_object* x_6;
x_5 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_6 = l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___at_Lean_Meta_FVarSubst_apply___spec__2(x_1, x_5, x_3, x_4);
x_6 = l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___at_Lean_Meta_FVarSubst_apply___spec__1(x_1, x_5, x_3, x_4);
lean_dec(x_1);
return x_6;
}
@ -670,7 +921,7 @@ return x_1;
}
else
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; uint8_t x_8;
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_3 = lean_ctor_get(x_2, 0);
lean_inc(x_3);
x_4 = lean_ctor_get(x_2, 1);
@ -681,18 +932,35 @@ x_6 = lean_ctor_get(x_2, 3);
lean_inc(x_6);
lean_dec(x_2);
x_7 = l_RBNode_fold___main___at_Lean_Meta_FVarSubst_compose___spec__1(x_1, x_3);
x_8 = l_Lean_NameMap_contains___rarg(x_7, x_4);
if (x_8 == 0)
x_8 = l_RBNode_find___main___at_Lean_Meta_FVarSubst_get___spec__1(x_7, x_4);
if (lean_obj_tag(x_8) == 0)
{
lean_object* x_9; lean_object* x_10;
x_9 = l_Lean_Meta_FVarSubst_apply(x_7, x_5);
x_10 = l_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(x_7, x_4, x_9);
lean_object* x_9;
x_9 = l_RBNode_find___main___at_Lean_Meta_FVarSubst_get___spec__1(x_7, x_5);
if (lean_obj_tag(x_9) == 0)
{
lean_object* x_10;
x_10 = l_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(x_7, x_4, x_5);
x_1 = x_10;
x_2 = x_6;
goto _start;
}
else
{
lean_object* x_12; lean_object* x_13;
lean_dec(x_5);
x_12 = lean_ctor_get(x_9, 0);
lean_inc(x_12);
lean_dec(x_9);
x_13 = l_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(x_7, x_4, x_12);
x_1 = x_13;
x_2 = x_6;
goto _start;
}
}
else
{
lean_dec(x_8);
lean_dec(x_5);
lean_dec(x_4);
x_1 = x_7;

31
stage0/stdlib/Init/Lean/Meta/Tactic/Induction.c
View file

@ -80,6 +80,7 @@ lean_object* l_Lean_Expr_fvarId_x21(lean_object*);
lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
lean_object* l_List_foldlM___main___at_Lean_Meta_induction___spec__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_lengthAux___main___rarg(lean_object*, lean_object*);
uint8_t l_Lean_Expr_isHeadBetaTarget(lean_object*);
lean_object* l_Array_umapMAux___main___at_Lean_Meta_induction___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_repr(lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
@ -151,7 +152,6 @@ lean_object* l_Lean_Expr_withAppAux___main___at_Lean_Meta_induction___spec__7___
lean_object* l_Nat_forMAux___main___at_Lean_Meta_induction___spec__3___closed__5;
extern lean_object* l_Lean_mkOptionalNode___closed__2;
extern lean_object* l_Lean_Meta_isClassQuick___main___closed__1;
uint8_t l_Lean_Expr_isHeadBetaTarget___main(lean_object*);
lean_object* l_Nat_forMAux___main___at_Lean_Meta_induction___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_toArrayAux___main___rarg(lean_object*, lean_object*);
lean_object* l_Nat_forMAux___main___at_Lean_Meta_induction___spec__3___closed__4;
@ -210,7 +210,7 @@ block_7:
{
uint8_t x_3;
lean_dec(x_2);
x_3 = l_Lean_Expr_isHeadBetaTarget___main(x_1);
x_3 = l_Lean_Expr_isHeadBetaTarget(x_1);
if (x_3 == 0)
{
lean_object* x_4;
@ -667,7 +667,7 @@ x_14 = lean_nat_dec_le(x_12, x_13);
lean_dec(x_13);
if (x_14 == 0)
{
lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21;
lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20;
x_15 = l_Lean_Name_inhabited;
x_16 = lean_array_get(x_15, x_1, x_12);
x_17 = lean_nat_sub(x_12, x_3);
@ -676,10 +676,9 @@ x_18 = lean_nat_sub(x_17, x_10);
lean_dec(x_17);
x_19 = lean_array_get(x_15, x_4, x_18);
lean_dec(x_18);
x_20 = l_Lean_mkFVar(x_19);
x_21 = l_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(x_7, x_16, x_20);
x_20 = l_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(x_7, x_16, x_19);
x_6 = x_11;
x_7 = x_21;
x_7 = x_20;
goto _start;
}
else
@ -714,7 +713,7 @@ x_14 = lean_nat_dec_le(x_12, x_13);
lean_dec(x_13);
if (x_14 == 0)
{
lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21;
lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20;
x_15 = l_Lean_Name_inhabited;
x_16 = lean_array_get(x_15, x_1, x_12);
x_17 = lean_nat_sub(x_12, x_3);
@ -723,10 +722,9 @@ x_18 = lean_nat_sub(x_17, x_10);
lean_dec(x_17);
x_19 = lean_array_get(x_15, x_4, x_18);
lean_dec(x_18);
x_20 = l_Lean_mkFVar(x_19);
x_21 = l_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(x_7, x_16, x_20);
x_20 = l_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(x_7, x_16, x_19);
x_6 = x_11;
x_7 = x_21;
x_7 = x_20;
goto _start;
}
else
@ -2902,19 +2900,18 @@ return x_5;
}
else
{
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15;
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_8 = lean_array_fget(x_3, x_4);
x_9 = l_Lean_Expr_fvarId_x21(x_8);
lean_dec(x_8);
x_10 = l_Lean_Name_inhabited;
x_11 = lean_array_get(x_10, x_2, x_4);
x_12 = l_Lean_mkFVar(x_11);
x_13 = l_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(x_5, x_9, x_12);
x_14 = lean_unsigned_to_nat(1u);
x_15 = lean_nat_add(x_4, x_14);
x_12 = l_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(x_5, x_9, x_11);
x_13 = lean_unsigned_to_nat(1u);
x_14 = lean_nat_add(x_4, x_13);
lean_dec(x_4);
x_4 = x_15;
x_5 = x_13;
x_4 = x_14;
x_5 = x_12;
goto _start;
}
}

51
stage0/stdlib/Init/Lean/Meta/Tactic/Subst.c
View file

@ -134,7 +134,7 @@ x_8 = lean_unsigned_to_nat(0u);
x_9 = lean_nat_dec_eq(x_4, x_8);
if (x_9 == 0)
{
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18;
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_10 = lean_unsigned_to_nat(1u);
x_11 = lean_nat_sub(x_4, x_10);
lean_dec(x_4);
@ -145,20 +145,19 @@ x_14 = l_Lean_Name_inhabited;
x_15 = lean_array_get(x_14, x_1, x_13);
x_16 = lean_array_get(x_14, x_2, x_13);
lean_dec(x_13);
x_17 = l_Lean_mkFVar(x_16);
x_18 = l_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(x_5, x_15, x_17);
x_17 = l_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(x_5, x_15, x_16);
x_4 = x_11;
x_5 = x_18;
x_5 = x_17;
goto _start;
}
else
{
lean_object* x_20;
lean_object* x_19;
lean_dec(x_4);
x_20 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_20, 0, x_5);
lean_ctor_set(x_20, 1, x_7);
return x_20;
x_19 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_19, 0, x_5);
lean_ctor_set(x_19, 1, x_7);
return x_19;
}
}
}
@ -170,7 +169,7 @@ x_8 = lean_unsigned_to_nat(0u);
x_9 = lean_nat_dec_eq(x_4, x_8);
if (x_9 == 0)
{
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18;
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_10 = lean_unsigned_to_nat(1u);
x_11 = lean_nat_sub(x_4, x_10);
lean_dec(x_4);
@ -181,20 +180,19 @@ x_14 = l_Lean_Name_inhabited;
x_15 = lean_array_get(x_14, x_1, x_13);
x_16 = lean_array_get(x_14, x_2, x_13);
lean_dec(x_13);
x_17 = l_Lean_mkFVar(x_16);
x_18 = l_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(x_5, x_15, x_17);
x_17 = l_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(x_5, x_15, x_16);
x_4 = x_11;
x_5 = x_18;
x_5 = x_17;
goto _start;
}
else
{
lean_object* x_20;
lean_object* x_19;
lean_dec(x_4);
x_20 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_20, 0, x_5);
lean_ctor_set(x_20, 1, x_7);
return x_20;
x_19 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_19, 0, x_5);
lean_ctor_set(x_19, 1, x_7);
return x_19;
}
}
}
@ -206,7 +204,7 @@ x_8 = lean_unsigned_to_nat(0u);
x_9 = lean_nat_dec_eq(x_4, x_8);
if (x_9 == 0)
{
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18;
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_10 = lean_unsigned_to_nat(1u);
x_11 = lean_nat_sub(x_4, x_10);
lean_dec(x_4);
@ -217,20 +215,19 @@ x_14 = l_Lean_Name_inhabited;
x_15 = lean_array_get(x_14, x_1, x_13);
x_16 = lean_array_get(x_14, x_2, x_13);
lean_dec(x_13);
x_17 = l_Lean_mkFVar(x_16);
x_18 = l_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(x_5, x_15, x_17);
x_17 = l_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(x_5, x_15, x_16);
x_4 = x_11;
x_5 = x_18;
x_5 = x_17;
goto _start;
}
else
{
lean_object* x_20;
lean_object* x_19;
lean_dec(x_4);
x_20 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_20, 0, x_5);
lean_ctor_set(x_20, 1, x_7);
return x_20;
x_19 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_19, 0, x_5);
lean_ctor_set(x_19, 1, x_7);
return x_19;
}
}
}