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 2022-02-19 08:11:17 -08:00
parent 7a81589c49
commit 7a13eaea8d
16 changed files with 16609 additions and 9097 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
stage0/src/Init/Data/Array/Basic.lean generated
View file

@ -633,6 +633,29 @@ def indexOf? [BEq α] (a : Array α) (v : α) : Option (Fin a.size) :=
@[simp] theorem size_pop (a : Array α) : a.pop.size = a.size - 1 :=
List.length_dropLast ..
def popWhile (p : α → Bool) (as : Array α) : Array α :=
if h : as.size > 0 then
if p (as.get ⟨as.size - 1, Nat.sub_lt h (by decide)⟩) then
popWhile p as.pop
else
as
else
as
termination_by popWhile as => as.size
def takeWhile (p : α → Bool) (as : Array α) : Array α :=
let rec go (i : Nat) (r : Array α) : Array α :=
if h : i < as.size then
let a := as.get ⟨i, h⟩
if p a then
go (i+1) (r.push a)
else
r
else
r
go 0 #[]
termination_by go i r => as.size - i
def eraseIdxAux (i : Nat) (a : Array α) : Array α :=
if h : i < a.size then
let idx : Fin a.size := ⟨i, h⟩;

10
stage0/src/Lean/Elab/Match.lean generated
View file

@ -568,7 +568,15 @@ private def elabMatchAltView (alt : MatchAltView) (matchType : Expr) : ExceptT P
withPatternVars patternVars fun patternVarDecls => do
withElaboratedLHS alt.ref patternVarDecls alt.patterns matchType fun altLHS matchType => do
withLocalInstances altLHS.fvarDecls do
let rhs ← elabTermEnsuringType alt.rhs matchType
trace[Elab.match] "elabMatchAltView: {matchType}"
let matchType ← instantiateMVars matchType
-- If `matchType` is of the form `@m ...`, we create a new metavariable with the current scope.
-- This improves the effectiveness of the `isDefEq` default approximations
let matchType' ← if matchType.getAppFn.isMVar then mkFreshTypeMVar else pure matchType
let rhs ← elabTermEnsuringType alt.rhs matchType'
-- We use all approximations to ensure the auxiliary type is defeq to the original one.
unless (← fullApproxDefEq <| isDefEq matchType' matchType) do
throwError "type mistmatch, alternative {← mkHasTypeButIsExpectedMsg matchType' matchType}"
let xs := altLHS.fvarDecls.toArray.map LocalDecl.toExpr
let rhs ← if xs.isEmpty then pure <| mkSimpleThunk rhs else mkLambdaFVars xs rhs
trace[Elab.match] "rhs: {rhs}"

31
stage0/src/Lean/Elab/PreDefinition/WF/Fix.lean generated
View file

@ -29,7 +29,7 @@ private def mkDecreasingProof (decreasingProp : Expr) (decrTactic? : Option Synt
| some decrTactic => Term.runTactic mvarId decrTactic
instantiateMVars mvar
private partial def replaceRecApps (recFnName : Name) (decrTactic? : Option Syntax) (F : Expr) (e : Expr) : TermElabM Expr :=
private partial def replaceRecApps (recFnName : Name) (fixedPrefixSize : Nat) (decrTactic? : Option Syntax) (F : Expr) (e : Expr) : TermElabM Expr :=
let rec loop (F : Expr) (e : Expr) : TermElabM Expr := do
match e with
| Expr.lam n d b c =>
@ -50,8 +50,8 @@ private partial def replaceRecApps (recFnName : Name) (decrTactic? : Option Synt
| Expr.app _ _ _ =>
let processApp (e : Expr) : TermElabM Expr :=
e.withApp fun f args => do
if f.isConstOf recFnName && args.size == 1 then
let r := mkApp F (← loop F args[0])
if f.isConstOf recFnName && args.size == fixedPrefixSize + 1 then
let r := mkApp F (← loop F args.back)
let decreasingProp := (← whnf (← inferType r)).bindingDomain!
return mkApp r (← mkDecreasingProof decreasingProp decrTactic?)
else
@ -59,7 +59,7 @@ private partial def replaceRecApps (recFnName : Name) (decrTactic? : Option Synt
let matcherApp? ← matchMatcherApp? e
match matcherApp? with
| some matcherApp =>
if !Structural.recArgHasLooseBVarsAt recFnName 0 e then
if !Structural.recArgHasLooseBVarsAt recFnName fixedPrefixSize e then
processApp e
else
let matcherApp ← mapError (matcherApp.addArg F) (fun msg => "failed to add functional argument to 'matcher' application" ++ indentD msg)
@ -77,9 +77,9 @@ private partial def replaceRecApps (recFnName : Name) (decrTactic? : Option Synt
| e => ensureNoRecFn recFnName e
loop F e
/-- Refine `F` over `Sum.casesOn` -/
/-- Refine `F` over `PSum.casesOn` -/
private partial def processSumCasesOn (x F val : Expr) (k : (x : Expr) → (F : Expr) → (val : Expr) → TermElabM Expr) : TermElabM Expr := do
if x.isFVar && val.isAppOfArity ``Sum.casesOn 6 && val.getArg! 3 == x && (val.getArg! 4).isLambda && (val.getArg! 5).isLambda then
if x.isFVar && val.isAppOfArity ``PSum.casesOn 6 && val.getArg! 3 == x && (val.getArg! 4).isLambda && (val.getArg! 5).isLambda then
let args := val.getAppArgs
let α := args[0]
let β := args[1]
@ -94,9 +94,9 @@ private partial def processSumCasesOn (x F val : Expr) (k : (x : Expr) → (F :
let FTypeNew := FDecl.type.replaceFVar x (← mkAppOptM ctorName #[α, β, xNew])
withLocalDeclD FDecl.userName FTypeNew fun FNew => do
mkLambdaFVars #[xNew, FNew] (← processSumCasesOn xNew FNew valNew k)
let minorLeft ← mkMinorNew ``Sum.inl args[4]
let minorRight ← mkMinorNew ``Sum.inr args[5]
let result := mkAppN (mkConst ``Sum.casesOn [u, (← getDecLevel α), (← getDecLevel β)]) #[α, β, motiveNew, x, minorLeft, minorRight, F]
let minorLeft ← mkMinorNew ``PSum.inl args[4]
let minorRight ← mkMinorNew ``PSum.inr args[5]
let result := mkAppN (mkConst ``PSum.casesOn [u, (← getLevel α), (← getLevel β)]) #[α, β, motiveNew, x, minorLeft, minorRight, F]
return result
else
k x F val
@ -124,8 +124,9 @@ private partial def processPSigmaCasesOn (x F val : Expr) (k : (F : Expr) → (v
else
k F val
def mkFix (preDef : PreDefinition) (wfRel : Expr) (decrTactic? : Option Syntax) : TermElabM PreDefinition := do
let wfFix ← forallBoundedTelescope preDef.type (some 1) fun x type => do
def mkFix (preDef : PreDefinition) (prefixArgs : Array Expr) (wfRel : Expr) (decrTactic? : Option Syntax) : TermElabM Expr := do
let type ← instantiateForall preDef.type prefixArgs
let wfFix ← forallBoundedTelescope type (some 1) fun x type => do
let x := x[0]
let α ← inferType x
let u ← getLevel α
@ -137,8 +138,10 @@ def mkFix (preDef : PreDefinition) (wfRel : Expr) (decrTactic? : Option Syntax)
forallBoundedTelescope (← whnf (← inferType wfFix)).bindingDomain! (some 2) fun xs _ => do
let x := xs[0]
let F := xs[1]
let val := preDef.value.betaRev #[x]
let val ← processSumCasesOn x F val fun x F val => processPSigmaCasesOn x F val (replaceRecApps preDef.declName decrTactic?)
return { preDef with value := mkApp wfFix (← mkLambdaFVars #[x, F] val) }
let val := preDef.value.beta (prefixArgs.push x)
trace[Elab.definition.wf] ">> val: {val}"
let val ← processSumCasesOn x F val fun x F val => do
processPSigmaCasesOn x F val (replaceRecApps preDef.declName prefixArgs.size decrTactic?)
mkLambdaFVars prefixArgs (mkApp wfFix (← mkLambdaFVars #[x, F] val))
end Lean.Elab.WF

71
stage0/src/Lean/Elab/PreDefinition/WF/Main.lean generated
View file

@ -15,22 +15,22 @@ namespace Lean.Elab
open WF
open Meta
private def isOnlyOneUnaryDef (preDefs : Array PreDefinition) : MetaM Bool := do
private def isOnlyOneUnaryDef (preDefs : Array PreDefinition) (fixedPrefixSize : Nat) : MetaM Bool := do
if preDefs.size == 1 then
lambdaTelescope preDefs[0].value fun xs _ => return xs.size == 1
lambdaTelescope preDefs[0].value fun xs _ => return xs.size == fixedPrefixSize + 1
else
return false
private partial def addNonRecPreDefs (preDefs : Array PreDefinition) (preDefNonRec : PreDefinition) : TermElabM Unit := do
if (← isOnlyOneUnaryDef preDefs) then
private partial def addNonRecPreDefs (preDefs : Array PreDefinition) (preDefNonRec : PreDefinition) (fixedPrefixSize : Nat) : TermElabM Unit := do
if (← isOnlyOneUnaryDef preDefs fixedPrefixSize) then
return ()
let Expr.forallE _ domain _ _ := preDefNonRec.type | unreachable!
let us := preDefNonRec.levelParams.map mkLevelParam
for fidx in [:preDefs.size] do
let preDef := preDefs[fidx]
let value ← lambdaTelescope preDef.value fun xs _ => do
let packedArgs : Array Expr := xs[fixedPrefixSize:]
let mkProd (type : Expr) : MetaM Expr := do
mkUnaryArg type xs
mkUnaryArg type packedArgs
let rec mkSum (i : Nat) (type : Expr) : MetaM Expr := do
if i == preDefs.size - 1 then
mkProd type
@ -38,30 +38,67 @@ private partial def addNonRecPreDefs (preDefs : Array PreDefinition) (preDefNonR
(← whnfD type).withApp fun f args => do
assert! args.size == 2
if i == fidx then
return mkApp3 (mkConst ``Sum.inl f.constLevels!) args[0] args[1] (← mkProd args[0])
return mkApp3 (mkConst ``PSum.inl f.constLevels!) args[0] args[1] (← mkProd args[0])
else
let r ← mkSum (i+1) args[1]
return mkApp3 (mkConst ``Sum.inr f.constLevels!) args[0] args[1] r
return mkApp3 (mkConst ``PSum.inr f.constLevels!) args[0] args[1] r
let Expr.forallE _ domain _ _ := (← instantiateForall preDefNonRec.type xs[:fixedPrefixSize]) | unreachable!
let arg ← mkSum 0 domain
mkLambdaFVars xs (mkApp (mkConst preDefNonRec.declName us) arg)
mkLambdaFVars xs (mkApp (mkAppN (mkConst preDefNonRec.declName us) xs[:fixedPrefixSize]) arg)
trace[Elab.definition.wf] "{preDef.declName} := {value}"
addNonRec { preDef with value } (applyAttrAfterCompilation := false)
partial def withCommonTelescope (preDefs : Array PreDefinition) (k : Array Expr → Array Expr → TermElabM α) : TermElabM α :=
go #[] (preDefs.map (·.value))
where
go (fvars : Array Expr) (vals : Array Expr) : TermElabM α := do
if !(vals.all fun val => val.isLambda) then
k fvars vals
else if !(← vals.allM fun val => return val.bindingName! == vals[0].bindingName! && val.binderInfo == vals[0].binderInfo && (← isDefEq val.bindingDomain! vals[0].bindingDomain!)) then
k fvars vals
else
withLocalDecl vals[0].bindingName! vals[0].binderInfo vals[0].bindingDomain! fun x =>
go (fvars.push x) (vals.map fun val => val.bindingBody!.instantiate1 x)
def getFixedPrefix (preDefs : Array PreDefinition) : TermElabM Nat :=
withCommonTelescope preDefs fun xs vals => do
let resultRef ← IO.mkRef xs.size
for val in vals do
if (← resultRef.get) == 0 then return 0
forEachExpr' val fun e => do
if preDefs.any fun preDef => e.isAppOf preDef.declName then
let args := e.getAppArgs
resultRef.modify (min args.size .)
for arg in args, x in xs do
if !(← withoutProofIrrelevance <| withReducible <| isDefEq arg x) then
-- We continue searching if e's arguments are not a prefix of `xs`
return true
return false
else
return true
resultRef.get
def wfRecursion (preDefs : Array PreDefinition) (wf? : Option TerminationWF) (decrTactic? : Option Syntax) : TermElabM Unit := do
let fixedPrefixSize ← getFixedPrefix preDefs
trace[Elab.definition.wf] "fixed prefix: {fixedPrefixSize}"
let unaryPreDef ← withoutModifyingEnv do
for preDef in preDefs do
addAsAxiom preDef
let unaryPreDefs ← packDomain preDefs
packMutual unaryPreDefs
let wfRel ← elabWFRel preDefs unaryPreDef wf?
let preDefNonRec ← withoutModifyingEnv do
addAsAxiom unaryPreDef
mkFix unaryPreDef wfRel decrTactic?
let preDefNonRec ← eraseRecAppSyntax preDefNonRec
let unaryPreDefs ← packDomain fixedPrefixSize preDefs
packMutual fixedPrefixSize unaryPreDefs
let preDefNonRec ← forallBoundedTelescope unaryPreDef.type fixedPrefixSize fun prefixArgs type => do
let packedArgType := type.bindingDomain!
let wfRel ← elabWFRel preDefs unaryPreDef.declName fixedPrefixSize packedArgType wf?
trace[Elab.definition.wf] "wfRel: {wfRel}"
withoutModifyingEnv do
addAsAxiom unaryPreDef
let value ← mkFix unaryPreDef prefixArgs wfRel decrTactic?
let value ← eraseRecAppSyntaxExpr value
return { unaryPreDef with value }
trace[Elab.definition.wf] ">> {preDefNonRec.declName} :=\n{preDefNonRec.value}"
let preDefs ← preDefs.mapM fun d => eraseRecAppSyntax d
addNonRec preDefNonRec
addNonRecPreDefs preDefs preDefNonRec
addNonRecPreDefs preDefs preDefNonRec fixedPrefixSize
registerEqnsInfo preDefs preDefNonRec.declName
for preDef in preDefs do
applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation

34
stage0/src/Lean/Elab/PreDefinition/WF/PackDomain.lean generated
View file

@ -57,17 +57,20 @@ private partial def mkPSigmaCasesOn (y : Expr) (codomain : Expr) (xs : Array Exp
Convert the given pre-definitions into unary functions.
We "pack" the arguments using `PSigma`.
-/
partial def packDomain (preDefs : Array PreDefinition) : MetaM (Array PreDefinition) := do
partial def packDomain (fixedPrefix : Nat) (preDefs : Array PreDefinition) : MetaM (Array PreDefinition) := do
let mut preDefsNew := #[]
let mut arities := #[]
let mut modified := false
for preDef in preDefs do
let (preDefNew, arity, modifiedCurr) ← lambdaTelescope preDef.value fun xs body => do
if xs.size == 0 then
throwError "well-founded recursion cannot be used, '{preDef.declName}' does not take any arguments"
if xs.size > 1 then
if xs.size == fixedPrefix then
throwError "well-founded recursion cannot be used, '{preDef.declName}' does not take any (non-fixed) arguments"
let arity := xs.size
if arity > fixedPrefix + 1 then
let bodyType ← instantiateForall preDef.type xs
let mut d ← inferType xs.back
let ys : Array Expr := xs[:fixedPrefix]
let xs : Array Expr := xs[fixedPrefix:]
for x in xs.pop.reverse do
d ← mkAppOptM ``PSigma #[some (← inferType x), some (← mkLambdaFVars #[x] d)]
withLocalDeclD (← mkFreshUserName `_x) d fun tuple => do
@ -75,12 +78,12 @@ partial def packDomain (preDefs : Array PreDefinition) : MetaM (Array PreDefinit
let codomain := bodyType.replaceFVars xs elems
let preDefNew:= { preDef with
declName := preDef.declName ++ `_unary
type := (← mkForallFVars #[tuple] codomain)
type := (← mkForallFVars (ys.push tuple) codomain)
}
addAsAxiom preDefNew
return (preDefNew, xs.size, true)
return (preDefNew, arity, true)
else
return (preDef, 1, false)
return (preDef, arity, false)
modified := modified || modifiedCurr
arities := arities.push arity
preDefsNew := preDefsNew.push preDefNew
@ -92,14 +95,17 @@ partial def packDomain (preDefs : Array PreDefinition) : MetaM (Array PreDefinit
let preDefNew := preDefsNew[i]
let arity := arities[i]
let valueNew ← lambdaTelescope preDef.value fun xs body => do
forallBoundedTelescope preDefNew.type (some 1) fun y codomain => do
let y := y[0]
let newBody ← mkPSigmaCasesOn y codomain xs body
mkLambdaFVars #[y] (← packApplications newBody arities preDefsNew)
let ys : Array Expr := xs[:fixedPrefix]
let xs : Array Expr := xs[fixedPrefix:]
let type ← instantiateForall preDefNew.type ys
forallBoundedTelescope type (some 1) fun z codomain => do
let z := z[0]
let newBody ← mkPSigmaCasesOn z codomain xs body
mkLambdaFVars (ys.push z) (← packApplications newBody arities preDefsNew)
let isBad (e : Expr) : Bool :=
match isAppOfPreDef? e with
| none => false
| some i => e.getAppNumArgs > 1 || preDefsNew[i].declName != preDefs[i].declName
| some i => e.getAppNumArgs > fixedPrefix + 1 || preDefsNew[i].declName != preDefs[i].declName
if let some bad := valueNew.find? isBad then
if let some i := isAppOfPreDef? bad then
throwErrorAt preDef.ref "well-founded recursion cannot be used, function '{preDef.declName}' contains application of function '{preDefs[i].declName}' with #{bad.getAppNumArgs} argument(s), but function has arity {arities[i]}"
@ -115,9 +121,11 @@ where
packApplications (e : Expr) (arities : Array Nat) (preDefsNew : Array PreDefinition) : MetaM Expr := do
let pack (e : Expr) (funIdx : Nat) : MetaM Expr := do
let f := e.getAppFn
let args := e.getAppArgs
let fNew := mkConst preDefsNew[funIdx].declName f.constLevels!
let fNew := mkAppN fNew args[:fixedPrefix]
let Expr.forallE _ d .. ← inferType fNew | unreachable!
let argNew ← mkUnaryArg d e.getAppArgs
let argNew ← mkUnaryArg d args[fixedPrefix:]
return mkApp fNew argNew
let rec
visit (e : Expr) : MonadCacheT ExprStructEq Expr MetaM Expr := do

140
stage0/src/Lean/Elab/PreDefinition/WF/PackMutual.lean generated
View file

@ -8,81 +8,78 @@ import Lean.Elab.PreDefinition.Basic
namespace Lean.Elab.WF
open Meta
private def getDomains (preDefs : Array PreDefinition) : Array Expr :=
preDefs.map fun preDef => preDef.type.bindingDomain!
/-- Combine different function domains `ds` using `Sum`s -/
/-- Combine different function domains `ds` using `PSum`s -/
private def mkNewDomain (ds : Array Expr) : MetaM Expr := do
let mut r := ds.back
for d in ds.pop.reverse do
r ← mkAppM ``Sum #[d, r]
r ← mkAppM ``PSum #[d, r]
return r
private def getCodomainLevel (preDef : PreDefinition) : MetaM Level :=
forallBoundedTelescope preDef.type (some 1) fun _ body => getLevel body
private def getCodomainLevel (preDefType : Expr) : MetaM Level :=
forallBoundedTelescope preDefType (some 1) fun _ body => getLevel body
/--
Return the universe level for the codomain of the given definitions.
This method produces an error if the codomains are in different universe levels.
-/
private def getCodomainsLevel (preDefs : Array PreDefinition) : MetaM Level := do
let r ← getCodomainLevel preDefs[0]
for preDef in preDefs[1:] do
private def getCodomainsLevel (preDefTypes : Array Expr) : MetaM Level := do
let r ← getCodomainLevel preDefTypes[0]
for preDef in preDefTypes[1:] do
unless (← isLevelDefEq r (← getCodomainLevel preDef)) do
throwError "invalid mutual definition, result types must be in the same universe level"
return r
/--
Create the codomain for the new function that "combines" different `preDefs`
Create the codomain for the new function that "combines" different `preDef` types
See: `packMutual`
-/
private partial def mkNewCoDomain (x : Expr) (preDefs : Array PreDefinition) : MetaM Expr := do
let u ← getCodomainsLevel preDefs
private partial def mkNewCoDomain (x : Expr) (preDefTypes : Array Expr) : MetaM Expr := do
let u ← getCodomainsLevel preDefTypes
let rec go (x : Expr) (i : Nat) : MetaM Expr := do
if i < preDefs.size - 1 then
if i < preDefTypes.size - 1 then
let xType ← whnfD (← inferType x)
assert! xType.isAppOfArity ``Sum 2
assert! xType.isAppOfArity ``PSum 2
let xTypeArgs := xType.getAppArgs
let casesOn := mkConst (mkCasesOnName ``Sum) (mkLevelSucc u :: xType.getAppFn.constLevels!)
let casesOn := mkConst (mkCasesOnName ``PSum) (mkLevelSucc u :: xType.getAppFn.constLevels!)
let casesOn := mkAppN casesOn xTypeArgs -- parameters
let casesOn := mkApp casesOn (← mkLambdaFVars #[x] (mkSort u)) -- motive
let casesOn := mkApp casesOn x -- major
let minor1 ← withLocalDeclD (← mkFreshUserName `_x) xTypeArgs[0] fun x =>
mkLambdaFVars #[x] (preDefs[i].type.bindingBody!.instantiate1 x)
mkLambdaFVars #[x] (preDefTypes[i].bindingBody!.instantiate1 x)
let minor2 ← withLocalDeclD (← mkFreshUserName `_x) xTypeArgs[1] fun x => do
mkLambdaFVars #[x] (← go x (i+1))
return mkApp2 casesOn minor1 minor2
else
return preDefs[i].type.bindingBody!.instantiate1 x
return preDefTypes[i].bindingBody!.instantiate1 x
go x 0
/--
Combine/pack the values of the different definitions in a single value
`x` is `Sum`, and we use `Sum.casesOn` to select the appropriate `preDefs.value`.
`x` is `PSum`, and we use `PSum.casesOn` to select the appropriate `preDefs.value`.
See: `packMutual`.
Remark: this method does not replace the nested recursive `preDefs` applications.
Remark: this method does not replace the nested recursive `preDefValues` applications.
This step is performed by `transform` with the following `post` method.
-/
private partial def packValues (x : Expr) (codomain : Expr) (preDefs : Array PreDefinition) : MetaM Expr := do
let varNames := preDefs.map fun preDef =>
assert! preDef.value.isLambda
preDef.value.bindingName!
private partial def packValues (x : Expr) (codomain : Expr) (preDefValues : Array Expr) : MetaM Expr := do
let varNames := preDefValues.map fun val =>
assert! val.isLambda
val.bindingName!
let mvar ← mkFreshExprSyntheticOpaqueMVar codomain
let rec go (mvarId : MVarId) (x : FVarId) (i : Nat) : MetaM Unit := do
if i < preDefs.size - 1 then
if i < preDefValues.size - 1 then
/-
Names for the `cases` tactics. The names are important to preserve the user provided names (unary functions).
-/
let givenNames : Array AltVarNames :=
if i == preDefs.size - 2 then
if i == preDefValues.size - 2 then
#[{ varNames := [varNames[i]] }, { varNames := [varNames[i+1]] }]
else
#[{ varNames := [varNames[i]] }]
let #[s₁, s₂] ← cases mvarId x (givenNames := givenNames) | unreachable!
assignExprMVar s₁.mvarId (mkApp preDefs[i].value s₁.fields[0]).headBeta
assignExprMVar s₁.mvarId (mkApp preDefValues[i] s₁.fields[0]).headBeta
go s₂.mvarId s₂.fields[0].fvarId! (i+1)
else
assignExprMVar mvarId (mkApp preDefs[i].value (mkFVar x)).headBeta
assignExprMVar mvarId (mkApp preDefValues[i] (mkFVar x)).headBeta
go mvar.mvarId! x.fvarId! 0
instantiateMVars mvar
@ -90,25 +87,44 @@ private partial def packValues (x : Expr) (codomain : Expr) (preDefs : Array Pre
Auxiliary function for replacing nested `preDefs` recursive calls in `e` with the new function `newFn`.
See: `packMutual`
-/
private partial def post (preDefs : Array PreDefinition) (domain : Expr) (newFn : Name) (e : Expr) : MetaM TransformStep := do
if let Expr.app (Expr.const declName us _) arg _ := e then
if let some fidx := preDefs.findIdx? (·.declName == declName) then
let rec mkNewArg (i : Nat) (type : Expr) : MetaM Expr := do
if i == preDefs.size - 1 then
return arg
else
(← whnfD type).withApp fun f args => do
assert! args.size == 2
if i == fidx then
return mkApp3 (mkConst ``Sum.inl f.constLevels!) args[0] args[1] arg
else
let r ← mkNewArg (i+1) args[1]
return mkApp3 (mkConst ``Sum.inr f.constLevels!) args[0] args[1] r
return TransformStep.done <| mkApp (mkConst newFn us) (← mkNewArg 0 domain)
private partial def post (fixedPrefix : Nat) (preDefs : Array PreDefinition) (domain : Expr) (newFn : Name) (e : Expr) : MetaM TransformStep := do
if e.getAppNumArgs != fixedPrefix + 1 then
return TransformStep.done e
let f := e.getAppFn
if !f.isConst then
return TransformStep.done e
let declName := f.constName!
let us := f.constLevels!
if let some fidx := preDefs.findIdx? (·.declName == declName) then
let args := e.getAppArgs
let fixedArgs := args[:fixedPrefix]
let arg := args.back
let rec mkNewArg (i : Nat) (type : Expr) : MetaM Expr := do
if i == preDefs.size - 1 then
return arg
else
(← whnfD type).withApp fun f args => do
assert! args.size == 2
if i == fidx then
return mkApp3 (mkConst ``PSum.inl f.constLevels!) args[0] args[1] arg
else
let r ← mkNewArg (i+1) args[1]
return mkApp3 (mkConst ``PSum.inr f.constLevels!) args[0] args[1] r
return TransformStep.done <| mkApp (mkAppN (mkConst newFn us) fixedArgs) (← mkNewArg 0 domain)
return TransformStep.done e
partial def withFixedPrefix (fixedPrefix : Nat) (preDefs : Array PreDefinition) (k : Array Expr → Array Expr → Array Expr → MetaM α) : MetaM α :=
go fixedPrefix #[] (preDefs.map (·.value))
where
go (i : Nat) (fvars : Array Expr) (vals : Array Expr) : MetaM α := do
match i with
| 0 => k fvars (← preDefs.mapM fun preDef => instantiateForall preDef.type fvars) vals
| i+1 =>
withLocalDecl vals[0].bindingName! vals[0].binderInfo vals[0].bindingDomain! fun x =>
go i (fvars.push x) (vals.map fun val => val.bindingBody!.instantiate1 x)
/--
If `preDefs.size > 1`, combine different functions in a single one using `Sum`.
If `preDefs.size > 1`, combine different functions in a single one using `PSum`.
This method assumes all `preDefs` have arity 1, and have already been processed using `packDomain`.
Here is a small example. Suppose the input is
```
@ -128,36 +144,38 @@ private partial def post (preDefs : Array PreDefinition) (domain : Expr) (newFn
this method produces the following pre definition
```
f._mutual x :=
Sum.casesOn x
PSum.casesOn x
(fun val =>
match val.2.1, val.2.2.1, val.2.2.2 with
| 0, a, b => a
| Nat.succ n, a, b => (f._mutual (Sum.inr (Sum.inl ⟨val.1, n, a, b⟩))).fst
| Nat.succ n, a, b => (f._mutual (PSum.inr (PSum.inl ⟨val.1, n, a, b⟩))).fst
fun val =>
Sum.casesOn val
PSum.casesOn val
(fun val =>
match val.2.1, val.2.2.1, val.2.2.2 with
| 0, a, b => (a, b)
| Nat.succ n, a, b => (f._mutual (Sum.inr (Sum.inr ⟨val.1, n, a, b⟩)), a)
| Nat.succ n, a, b => (f._mutual (PSum.inr (PSum.inr ⟨val.1, n, a, b⟩)), a)
fun val =>
match val.2.1, val.2.2.1, val.2.2.2 with
| 0, a, b => b
| Nat.succ n, a, b =>
f._mutual (Sum.inl ⟨val.1, n, a, b⟩)
f._mutual (PSum.inl ⟨val.1, n, a, b⟩)
```
-/
def packMutual (preDefs : Array PreDefinition) : MetaM PreDefinition := do
def packMutual (fixedPrefix : Nat) (preDefs : Array PreDefinition) : MetaM PreDefinition := do
if preDefs.size == 1 then return preDefs[0]
let domain ← mkNewDomain (getDomains preDefs)
withLocalDeclD (← mkFreshUserName `_x) domain fun x => do
let codomain ← mkNewCoDomain x preDefs
let type ← mkForallFVars #[x] codomain
let value ← packValues x codomain preDefs
let newFn := preDefs[0].declName ++ `_mutual
let preDefNew := { preDefs[0] with declName := newFn, type, value }
addAsAxiom preDefNew
let value ← transform value (post := post preDefs domain newFn)
let value ← mkLambdaFVars #[x] value
return { preDefNew with value }
withFixedPrefix fixedPrefix preDefs fun ys types vals => do
let domains := types.map fun type => type.bindingDomain!
let domain ← mkNewDomain domains
withLocalDeclD (← mkFreshUserName `_x) domain fun x => do
let codomain ← mkNewCoDomain x types
let type ← mkForallFVars (ys.push x) codomain
let value ← packValues x codomain vals
let newFn := preDefs[0].declName ++ `_mutual
let preDefNew := { preDefs[0] with declName := newFn, type, value }
addAsAxiom preDefNew
let value ← transform value (post := post fixedPrefix preDefs domain newFn)
let value ← mkLambdaFVars (ys.push x) value
return { preDefNew with value }
end Lean.Elab.WF

23
stage0/src/Lean/Elab/PreDefinition/WF/Rel.lean generated
View file

@ -29,7 +29,7 @@ private partial def unpackMutual (preDefs : Array PreDefinition) (mvarId : MVarI
return result.push (fvarId, mvarId)
go 0 mvarId fvarId #[]
private partial def unpackUnary (preDef : PreDefinition) (mvarId : MVarId) (fvarId : FVarId) (element : TerminationByElement) : TermElabM MVarId := do
private partial def unpackUnary (preDef : PreDefinition) (prefixSize : Nat) (mvarId : MVarId) (fvarId : FVarId) (element : TerminationByElement) : TermElabM MVarId := do
let varNames ← lambdaTelescope preDef.value fun xs body => do
let mut varNames ← xs.mapM fun x => return (← getLocalDecl x.fvarId!).userName
if element.vars.size > varNames.size then
@ -39,31 +39,38 @@ private partial def unpackUnary (preDef : PreDefinition) (mvarId : MVarId) (fvar
if varStx.isIdent then
varNames := varNames.set! (varNames.size - element.vars.size + i) varStx.getId
return varNames
let mut mvarId := mvarId
for localDecl in (← Term.getMVarDecl mvarId).lctx, varName in varNames[:prefixSize] do
unless localDecl.userName == varName do
mvarId ← rename mvarId localDecl.fvarId varName
let numPackedArgs := varNames.size - prefixSize
let rec go (i : Nat) (mvarId : MVarId) (fvarId : FVarId) : TermElabM MVarId := do
if i < varNames.size - 1 then
let #[s] ← cases mvarId fvarId #[{ varNames := [varNames[i]] }] | unreachable!
trace[Elab.definition.wf] "i: {i}, varNames: {varNames}, goal: {mvarId}"
if i < numPackedArgs - 1 then
let #[s] ← cases mvarId fvarId #[{ varNames := [varNames[prefixSize + i]] }] | unreachable!
go (i+1) s.mvarId s.fields[1].fvarId!
else
rename mvarId fvarId varNames.back
go 0 mvarId fvarId
def elabWFRel (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition) (wf? : Option TerminationWF) : TermElabM Expr := do
let α := unaryPreDef.type.bindingDomain!
def elabWFRel (preDefs : Array PreDefinition) (unaryPreDefName : Name) (fixedPrefixSize : Nat) (argType : Expr) (wf? : Option TerminationWF) : TermElabM Expr := do
let α := argType
let u ← getLevel α
let expectedType := mkApp (mkConst ``WellFoundedRelation [u]) α
trace[Elab.definition.wf] "elabWFRel start: {(← mkFreshTypeMVar).mvarId!}"
match wf? with
| some (TerminationWF.core wfStx) => withDeclName unaryPreDef.declName do
| some (TerminationWF.core wfStx) => withDeclName unaryPreDefName do
let wfRel ← instantiateMVars (← withSynthesize <| elabTermEnsuringType wfStx expectedType)
let pendingMVarIds ← getMVars wfRel
discard <| logUnassignedUsingErrorInfos pendingMVarIds
return wfRel
| some (TerminationWF.ext elements) => withDeclName unaryPreDef.declName <| withRef (getRefFromElems elements) do
| some (TerminationWF.ext elements) => withDeclName unaryPreDefName <| withRef (getRefFromElems elements) do
let mainMVarId := (← mkFreshExprSyntheticOpaqueMVar expectedType).mvarId!
let [fMVarId, wfRelMVarId, _] ← apply mainMVarId (← mkConstWithFreshMVarLevels ``invImage) | throwError "failed to apply 'invImage'"
let (d, fMVarId) ← intro1 fMVarId
let subgoals ← unpackMutual preDefs fMVarId d
for (d, mvarId) in subgoals, element in elements, preDef in preDefs do
let mvarId ← unpackUnary preDef mvarId d element
let mvarId ← unpackUnary preDef fixedPrefixSize mvarId d element
withMVarContext mvarId do
let value ← Term.withSynthesize <| elabTermEnsuringType element.body (← getMVarType mvarId)
assignExprMVar mvarId value

58
stage0/src/Lean/Meta/ExprDefEq.lean generated
View file

@ -920,14 +920,60 @@ private def assignConst (mvar : Expr) (numArgs : Nat) (v : Expr) : MetaM Bool :=
trace[Meta.isDefEq.constApprox] "{mvar} := {v}"
checkTypesAndAssign mvar v
private def processConstApprox (mvar : Expr) (numArgs : Nat) (v : Expr) : MetaM Bool := do
/--
Auxiliary procedure for solving `?m args =?= v` when `args[:patternVarPrefix]` contains
only pairwise distinct free variables.
Let `args[:patternVarPrefix] = #[a₁, ..., aₙ]`, and `args[patternVarPrefix:] = #[b₁, ..., bᵢ]`,
this procedure first reduces the constraint to
```
?m a₁ ... aₙ =?= fun x₁ ... xᵢ => v
```
where the left-hand-side is a constant function.
Then, it tries to find the longest prefix `#[a₁, ..., aⱼ]` of `#[a₁, ..., aₙ]` such that the following assignment is valid.
```
?m := fun y₁ ... y‌ⱼ => (fun y_{j+1} ... yₙ x₁ ... xᵢ => v)[a₁/y₁, .., aⱼ/yⱼ]
```
That is, after the longest prefix is found, we solve the contraint as the lhs was a pattern. See the definition of "pattern" above.
-/
private partial def processConstApprox (mvar : Expr) (args : Array Expr) (patternVarPrefix : Nat) (v : Expr) : MetaM Bool := do
trace[Meta.isDefEq.constApprox] "{mvar} {args} := {v}"
let rec defaultCase : MetaM Bool := assignConst mvar args.size v
let cfg ← getConfig
let mvarId := mvar.mvarId!
let mvarDecl ← getMVarDecl mvarId
if mvarDecl.numScopeArgs == numArgs || cfg.constApprox then
assignConst mvar numArgs v
let numArgs := args.size
if mvarDecl.numScopeArgs != numArgs && !cfg.constApprox then
return false
else if patternVarPrefix == 0 then
defaultCase
else
pure false
let argsPrefix : Array Expr := args[:patternVarPrefix]
let type ← instantiateForall mvarDecl.type argsPrefix
let suffixSize := numArgs - argsPrefix.size
forallBoundedTelescope type suffixSize fun xs _ => do
if xs.size != suffixSize then
defaultCase
else
let some v ← mkLambdaFVarsWithLetDeps xs v | defaultCase
let rec go (argsPrefix : Array Expr) (v : Expr) : MetaM Bool := do
trace[Meta.isDefEq] "processConstApprox.go {mvar} {argsPrefix} := {v}"
let rec cont : MetaM Bool := do
if argsPrefix.isEmpty then
defaultCase
else
let some v ← mkLambdaFVarsWithLetDeps #[argsPrefix.back] v | defaultCase
go argsPrefix.pop v
match (← checkAssignment mvarId argsPrefix v) with
| none => cont
| some vNew =>
let some vNew ← mkLambdaFVarsWithLetDeps argsPrefix vNew | cont
if argsPrefix.any (fun arg => mvarDecl.lctx.containsFVar arg) then
/- We need to type check `vNew` because abstraction using `mkLambdaFVars` may have produced
a type incorrect term. See discussion at A2 -/
(isTypeCorrect vNew <&&> checkTypesAndAssign mvar vNew) <||> cont
else
checkTypesAndAssign mvar vNew <||> cont
go argsPrefix v
/-- Tries to solve `?m a₁ ... aₙ =?= v` by assigning `?m`.
It assumes `?m` is unassigned. -/
@ -939,7 +985,7 @@ private partial def processAssignment (mvarApp : Expr) (v : Expr) : MetaM Bool :
let rec process (i : Nat) (args : Array Expr) (v : Expr) := do
let cfg ← getConfig
let useFOApprox (args : Array Expr) : MetaM Bool :=
processAssignmentFOApprox mvar args v <||> processConstApprox mvar args.size v
processAssignmentFOApprox mvar args v <||> processConstApprox mvar args i v
if h : i < args.size then
let arg := args.get ⟨i, h⟩
let arg ← simpAssignmentArg arg
@ -1273,7 +1319,7 @@ private def isDefEqProofIrrel (t s : Expr) : MetaM LBool := do
/- Try to solve constraint of the form `?m args₁ =?= ?m args₂`.
- First try to unify `args₁` and `args₂`, and return true if successful
- Otherwise, try to assign `?m` to a constant function of the form `fun x_1 ... x_n => ?n`
where `?n` is a fresh metavariable. See `processConstApprox`. -/
where `?n` is a fresh metavariable. See `assignConst`. -/
private def isDefEqMVarSelf (mvar : Expr) (args₁ args₂ : Array Expr) : MetaM Bool := do
if args₁.size != args₂.size then
pure false

145
stage0/stdlib/Init/Data/Array/Basic.c generated
View file

@ -19,6 +19,7 @@ LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Array_concatMap___spec__
LEAN_EXPORT lean_object* l_Array_forM(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_findM_x3f(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_findSomeRevM_x3f_find___at_Array_findRevM_x3f___spec__1___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_takeWhile___rarg___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Array_getEvenElems___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_getMax_x3f___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Array_findIdxM_x3f___spec__1___rarg___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -163,7 +164,9 @@ LEAN_EXPORT lean_object* l_Array_zip___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_partition(lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_zipWithAux___at_Array_zip___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_popWhile___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapIdx___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_takeWhile(lean_object*);
LEAN_EXPORT lean_object* l_Array_getMax_x3f___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_swap___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___aux__Init__Data__Array__Basic______macroRules__term_x23_x5b___x2c_x5d__1___closed__12;
@ -199,9 +202,11 @@ LEAN_EXPORT lean_object* l___private_Init_Data_Array_Basic_0__Array_allDiffAuxAu
LEAN_EXPORT lean_object* l_Array_forInUnsafe(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_findSomeM_x3f___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
static lean_object* l_Array_instAppendArray___closed__1;
LEAN_EXPORT lean_object* l_Array_takeWhile_go___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___aux__Init__Data__Array__Basic______macroRules__term_x23_x5b___x2c_x5d__1___closed__16;
LEAN_EXPORT lean_object* l_Array_toArrayLit___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_sub(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_takeWhile___rarg(lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Array_all___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_filter___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_eraseIdx_x27___rarg___boxed(lean_object*, lean_object*);
@ -340,6 +345,7 @@ LEAN_EXPORT lean_object* l_Array_foldrMUnsafe_fold___at_Array_toList___spec__1(l
LEAN_EXPORT lean_object* l_Array_findSome_x21___rarg___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Array_map___spec__1(lean_object*, lean_object*);
static lean_object* l_Array_findSome_x21___rarg___closed__1;
LEAN_EXPORT lean_object* l_Array_takeWhile_go___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Array_insertAt___rarg___closed__2;
LEAN_EXPORT lean_object* l_Array_modifyMUnsafe___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_addMacroScope(lean_object*, lean_object*, lean_object*);
@ -349,6 +355,7 @@ LEAN_EXPORT lean_object* l_Array_findSomeRevM_x3f_find___at_Array_findSomeRev_x3
LEAN_EXPORT lean_object* l_Array_zipWith___rarg___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldrMUnsafe_fold___at_Array_foldr___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapIdxM_map(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_takeWhile_go(lean_object*);
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Array_partition___spec__1___rarg(lean_object*, lean_object*, size_t, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Array_swapAt___rarg___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_feraseIdx___rarg(lean_object*, lean_object*);
@ -444,6 +451,7 @@ LEAN_EXPORT lean_object* l_Array_foldrMUnsafe_fold___at_Array_forRevM___spec__2_
LEAN_EXPORT lean_object* l_Array_eraseIdx___rarg___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_findSomeRevM_x3f_find___at_Array_findSomeRev_x3f___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Array_filterM___spec__1___rarg___lambda__2(size_t, lean_object*, lean_object*, lean_object*, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Array_popWhile(lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Array_append___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_modifyMUnsafe___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_concatMapM___rarg(lean_object*, lean_object*, lean_object*);
@ -8466,6 +8474,141 @@ lean_dec(x_2);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Array_popWhile___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; uint8_t x_5;
x_3 = lean_array_get_size(x_2);
x_4 = lean_unsigned_to_nat(0u);
x_5 = lean_nat_dec_lt(x_4, x_3);
if (x_5 == 0)
{
lean_dec(x_3);
lean_dec(x_1);
return x_2;
}
else
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; uint8_t x_10;
x_6 = lean_unsigned_to_nat(1u);
x_7 = lean_nat_sub(x_3, x_6);
lean_dec(x_3);
x_8 = lean_array_fget(x_2, x_7);
lean_dec(x_7);
lean_inc(x_1);
x_9 = lean_apply_1(x_1, x_8);
x_10 = lean_unbox(x_9);
lean_dec(x_9);
if (x_10 == 0)
{
lean_dec(x_1);
return x_2;
}
else
{
lean_object* x_11;
x_11 = lean_array_pop(x_2);
x_2 = x_11;
goto _start;
}
}
}
}
LEAN_EXPORT lean_object* l_Array_popWhile(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Array_popWhile___rarg), 2, 0);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Array_takeWhile_go___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; uint8_t x_6;
x_5 = lean_array_get_size(x_2);
x_6 = lean_nat_dec_lt(x_3, x_5);
lean_dec(x_5);
if (x_6 == 0)
{
lean_dec(x_3);
lean_dec(x_1);
return x_4;
}
else
{
lean_object* x_7; lean_object* x_8; uint8_t x_9;
x_7 = lean_array_fget(x_2, x_3);
lean_inc(x_1);
lean_inc(x_7);
x_8 = lean_apply_1(x_1, x_7);
x_9 = lean_unbox(x_8);
lean_dec(x_8);
if (x_9 == 0)
{
lean_dec(x_7);
lean_dec(x_3);
lean_dec(x_1);
return x_4;
}
else
{
lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_10 = lean_unsigned_to_nat(1u);
x_11 = lean_nat_add(x_3, x_10);
lean_dec(x_3);
x_12 = lean_array_push(x_4, x_7);
x_3 = x_11;
x_4 = x_12;
goto _start;
}
}
}
}
LEAN_EXPORT lean_object* l_Array_takeWhile_go(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Array_takeWhile_go___rarg___boxed), 4, 0);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Array_takeWhile_go___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = l_Array_takeWhile_go___rarg(x_1, x_2, x_3, x_4);
lean_dec(x_2);
return x_5;
}
}
LEAN_EXPORT lean_object* l_Array_takeWhile___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_3 = lean_unsigned_to_nat(0u);
x_4 = l_Array_instEmptyCollectionArray___closed__1;
x_5 = l_Array_takeWhile_go___rarg(x_1, x_2, x_3, x_4);
return x_5;
}
}
LEAN_EXPORT lean_object* l_Array_takeWhile(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Array_takeWhile___rarg___boxed), 2, 0);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Array_takeWhile___rarg___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Array_takeWhile___rarg(x_1, x_2);
lean_dec(x_2);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Array_eraseIdxAux___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -8753,7 +8896,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Array_swapAt_x21___rarg___closed__3;
x_2 = l_Array_insertAt___rarg___closed__1;
x_3 = lean_unsigned_to_nat(682u);
x_3 = lean_unsigned_to_nat(705u);
x_4 = lean_unsigned_to_nat(22u);
x_5 = l_Array_insertAt___rarg___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

797
stage0/stdlib/Lean/Elab/Match.c generated
View file

File diff suppressed because it is too large Load diff

6772
stage0/stdlib/Lean/Elab/PreDefinition/WF/Fix.c generated
View file

File diff suppressed because it is too large Load diff

4789
stage0/stdlib/Lean/Elab/PreDefinition/WF/Main.c generated
View file

File diff suppressed because it is too large Load diff

2139
stage0/stdlib/Lean/Elab/PreDefinition/WF/PackDomain.c generated
View file

File diff suppressed because it is too large Load diff

2963
stage0/stdlib/Lean/Elab/PreDefinition/WF/PackMutual.c generated
View file

File diff suppressed because it is too large Load diff

4896
stage0/stdlib/Lean/Elab/PreDefinition/WF/Rel.c generated
View file

File diff suppressed because it is too large Load diff

2815
stage0/stdlib/Lean/Meta/ExprDefEq.c generated
View file

File diff suppressed because it is too large Load diff