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-10-24 07:21:55 -07:00
parent 0af4b6fb6f
commit 01fbe709cf
20 changed files with 2214 additions and 2979 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

190
stage0/src/Lean/Elab/PreDefinition/Basic.lean generated
View file

@ -19,134 +19,134 @@ A (potentially recursive) definition.
The elaborator converts it into Kernel definitions using many different strategies.
-/
structure PreDefinition :=
(kind : DefKind)
(lparams : List Name)
(modifiers : Modifiers)
(declName : Name)
(type : Expr)
(value : Expr)
(kind : DefKind)
(lparams : List Name)
(modifiers : Modifiers)
(declName : Name)
(type : Expr)
(value : Expr)
instance : Inhabited PreDefinition :=
⟨⟨DefKind.«def», [], {}, arbitrary _, arbitrary _, arbitrary _⟩⟩
⟨⟨DefKind.«def», [], {}, arbitrary _, arbitrary _, arbitrary _⟩⟩
def instantiateMVarsAtPreDecls (preDefs : Array PreDefinition) : TermElabM (Array PreDefinition) :=
preDefs.mapM fun preDef => do
pure { preDef with type := (← instantiateMVars preDef.type), value := (← instantiateMVars preDef.value) }
preDefs.mapM fun preDef => do
pure { preDef with type := (← instantiateMVars preDef.type), value := (← instantiateMVars preDef.value) }
private def levelMVarToParamExpr (e : Expr) : StateRefT Nat TermElabM Expr := do
let nextIdx ← get;
let (e, nextIdx) ← levelMVarToParam e nextIdx;
set nextIdx;
pure e
let nextIdx ← get
let (e, nextIdx) ← levelMVarToParam e nextIdx;
set nextIdx;
pure e
private def levelMVarToParamPreDeclsAux (preDefs : Array PreDefinition) : StateRefT Nat TermElabM (Array PreDefinition) :=
preDefs.mapM fun preDef => do
pure { preDef with type := (← levelMVarToParamExpr preDef.type), value := (← levelMVarToParamExpr preDef.value) }
preDefs.mapM fun preDef => do
pure { preDef with type := (← levelMVarToParamExpr preDef.type), value := (← levelMVarToParamExpr preDef.value) }
def levelMVarToParamPreDecls (preDefs : Array PreDefinition) : TermElabM (Array PreDefinition) :=
(levelMVarToParamPreDeclsAux preDefs).run' 1
(levelMVarToParamPreDeclsAux preDefs).run' 1
private def getLevelParamsPreDecls (preDefs : Array PreDefinition) (scopeLevelNames allUserLevelNames : List Name) : TermElabM (List Name) := do
let s : CollectLevelParams.State := {}
for preDef in preDefs do
s := collectLevelParams s preDef.type
s := collectLevelParams s preDef.value
match sortDeclLevelParams scopeLevelNames allUserLevelNames s.params with
| Except.error msg => throwError msg
| Except.ok levelParams => pure levelParams
let s : CollectLevelParams.State := {}
for preDef in preDefs do
s := collectLevelParams s preDef.type
s := collectLevelParams s preDef.value
match sortDeclLevelParams scopeLevelNames allUserLevelNames s.params with
| Except.error msg => throwError msg
| Except.ok levelParams => pure levelParams
private def shareCommon (preDefs : Array PreDefinition) : Array PreDefinition :=
let result : Std.ShareCommonM (Array PreDefinition) :=
preDefs.mapM fun preDef => do
pure { preDef with type := (← Std.withShareCommon preDef.type), value := (← Std.withShareCommon preDef.value) }
result.run
let result : Std.ShareCommonM (Array PreDefinition) :=
preDefs.mapM fun preDef => do
pure { preDef with type := (← Std.withShareCommon preDef.type), value := (← Std.withShareCommon preDef.value) }
result.run
def fixLevelParams (preDefs : Array PreDefinition) (scopeLevelNames allUserLevelNames : List Name) : TermElabM (Array PreDefinition) := do
let preDefs := shareCommon preDefs
let lparams ← getLevelParamsPreDecls preDefs scopeLevelNames allUserLevelNames
let us := lparams.map mkLevelParam
let fixExpr (e : Expr) : Expr :=
e.replace fun c => match c with
| Expr.const declName _ _ => if preDefs.any fun preDef => preDef.declName == declName then some $ Lean.mkConst declName us else none
| _ => none
pure $ preDefs.map fun preDef =>
{ preDef with
type := fixExpr preDef.type,
value := fixExpr preDef.value,
lparams := lparams }
let preDefs := shareCommon preDefs
let lparams ← getLevelParamsPreDecls preDefs scopeLevelNames allUserLevelNames
let us := lparams.map mkLevelParam
let fixExpr (e : Expr) : Expr :=
e.replace fun c => match c with
| Expr.const declName _ _ => if preDefs.any fun preDef => preDef.declName == declName then some $ Lean.mkConst declName us else none
| _ => none
pure $ preDefs.map fun preDef =>
{ preDef with
type := fixExpr preDef.type,
value := fixExpr preDef.value,
lparams := lparams }
def applyAttributesOf (preDefs : Array PreDefinition) (applicationTime : AttributeApplicationTime) : TermElabM Unit := do
for preDef in preDefs do
applyAttributesAt preDef.declName preDef.modifiers.attrs applicationTime
for preDef in preDefs do
applyAttributesAt preDef.declName preDef.modifiers.attrs applicationTime
def abstractNestedProofs (preDef : PreDefinition) : MetaM PreDefinition :=
if preDef.kind.isTheorem || preDef.kind.isExample then
pure preDef
else do
let value ← Meta.abstractNestedProofs preDef.declName preDef.value
pure { preDef with value := value }
if preDef.kind.isTheorem || preDef.kind.isExample then
pure preDef
else do
let value ← Meta.abstractNestedProofs preDef.declName preDef.value
pure { preDef with value := value }
/- Auxiliary method for (temporarily) adding pre definition as an axiom -/
def addAsAxiom (preDef : PreDefinition) : MetaM Unit := do
addDecl $ Declaration.axiomDecl { name := preDef.declName, lparams := preDef.lparams, type := preDef.type, isUnsafe := preDef.modifiers.isUnsafe }
addDecl $ Declaration.axiomDecl { name := preDef.declName, lparams := preDef.lparams, type := preDef.type, isUnsafe := preDef.modifiers.isUnsafe }
private def addNonRecAux (preDef : PreDefinition) (compile : Bool) : TermElabM Unit := do
let preDef ← abstractNestedProofs preDef
let env ← getEnv
let decl :=
match preDef.kind with
| DefKind.«example» => unreachable!
| DefKind.«theorem» =>
Declaration.thmDecl { name := preDef.declName, lparams := preDef.lparams, type := preDef.type, value := preDef.value }
| DefKind.«opaque» =>
Declaration.opaqueDecl { name := preDef.declName, lparams := preDef.lparams, type := preDef.type, value := preDef.value,
let preDef ← abstractNestedProofs preDef
let env ← getEnv
let decl :=
match preDef.kind with
| DefKind.«example» => unreachable!
| DefKind.«theorem» =>
Declaration.thmDecl { name := preDef.declName, lparams := preDef.lparams, type := preDef.type, value := preDef.value }
| DefKind.«opaque» =>
Declaration.opaqueDecl { name := preDef.declName, lparams := preDef.lparams, type := preDef.type, value := preDef.value,
isUnsafe := preDef.modifiers.isUnsafe }
| DefKind.«abbrev» =>
Declaration.defnDecl { name := preDef.declName, lparams := preDef.lparams, type := preDef.type, value := preDef.value,
hints := ReducibilityHints.«abbrev», isUnsafe := preDef.modifiers.isUnsafe }
| DefKind.«def» =>
Declaration.defnDecl { name := preDef.declName, lparams := preDef.lparams, type := preDef.type, value := preDef.value,
hints := ReducibilityHints.regular (getMaxHeight env preDef.value + 1),
isUnsafe := preDef.modifiers.isUnsafe }
| DefKind.«abbrev» =>
Declaration.defnDecl { name := preDef.declName, lparams := preDef.lparams, type := preDef.type, value := preDef.value,
hints := ReducibilityHints.«abbrev», isUnsafe := preDef.modifiers.isUnsafe }
| DefKind.«def» =>
Declaration.defnDecl { name := preDef.declName, lparams := preDef.lparams, type := preDef.type, value := preDef.value,
hints := ReducibilityHints.regular (getMaxHeight env preDef.value + 1),
isUnsafe := preDef.modifiers.isUnsafe }
addDecl decl
applyAttributesOf #[preDef] AttributeApplicationTime.afterTypeChecking
when (compile && !preDef.kind.isTheorem) $
compileDecl decl
applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation
pure ()
addDecl decl
applyAttributesOf #[preDef] AttributeApplicationTime.afterTypeChecking
if compile && !preDef.kind.isTheorem then
compileDecl decl
applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation
pure ()
def addAndCompileNonRec (preDef : PreDefinition) : TermElabM Unit := do
addNonRecAux preDef true
addNonRecAux preDef true
def addNonRec (preDef : PreDefinition) : TermElabM Unit := do
addNonRecAux preDef false
addNonRecAux preDef false
def addAndCompileUnsafe (preDefs : Array PreDefinition) : TermElabM Unit := do
let decl := Declaration.mutualDefnDecl $ preDefs.toList.map fun preDef => {
name := preDef.declName,
lparams := preDef.lparams,
type := preDef.type,
value := preDef.value,
isUnsafe := true,
hints := ReducibilityHints.opaque
}
addDecl decl
applyAttributesOf preDefs AttributeApplicationTime.afterTypeChecking
compileDecl decl
applyAttributesOf preDefs AttributeApplicationTime.afterCompilation
pure ()
let decl := Declaration.mutualDefnDecl $ preDefs.toList.map fun preDef => {
name := preDef.declName,
lparams := preDef.lparams,
type := preDef.type,
value := preDef.value,
isUnsafe := true,
hints := ReducibilityHints.opaque
}
addDecl decl
applyAttributesOf preDefs AttributeApplicationTime.afterTypeChecking
compileDecl decl
applyAttributesOf preDefs AttributeApplicationTime.afterCompilation
pure ()
def addAndCompileUnsafeRec (preDefs : Array PreDefinition) : TermElabM Unit := do
addAndCompileUnsafe $ preDefs.map fun preDef =>
{ preDef with
declName := Compiler.mkUnsafeRecName preDef.declName,
value := preDef.value.replace fun e => match e with
| Expr.const declName us _ =>
if preDefs.any fun preDef => preDef.declName == declName then
some $ mkConst (Compiler.mkUnsafeRecName declName) us
else
none
| _ => none,
modifiers := {} }
addAndCompileUnsafe $ preDefs.map fun preDef =>
{ preDef with
declName := Compiler.mkUnsafeRecName preDef.declName,
value := preDef.value.replace fun e => match e with
| Expr.const declName us _ =>
if preDefs.any fun preDef => preDef.declName == declName then
some $ mkConst (Compiler.mkUnsafeRecName declName) us
else
none
| _ => none,
modifiers := {} }
end Lean.Elab

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

@ -12,69 +12,70 @@ open Meta
open Term
private def addAndCompilePartial (preDefs : Array PreDefinition) : TermElabM Unit := do
for preDef in preDefs do
trace[Elab.definition]! "processing {preDef.declName}"
forallTelescope preDef.type fun xs type => do
let inh ← liftM $ mkInhabitantFor preDef.declName xs type
trace[Elab.definition]! "inhabitant for {preDef.declName}"
addNonRec { preDef with
kind := DefKind.«opaque»,
value := inh }
addAndCompileUnsafeRec preDefs
for preDef in preDefs do
trace[Elab.definition]! "processing {preDef.declName}"
forallTelescope preDef.type fun xs type => do
let inh ← liftM $ mkInhabitantFor preDef.declName xs type
trace[Elab.definition]! "inhabitant for {preDef.declName}"
addNonRec { preDef with
kind := DefKind.«opaque»,
value := inh
}
addAndCompileUnsafeRec preDefs
private def isNonRecursive (preDef : PreDefinition) : Bool :=
Option.isNone $ preDef.value.find? fun
| Expr.const declName _ _ => preDef.declName == declName
| _ => false
Option.isNone $ preDef.value.find? fun
| Expr.const declName _ _ => preDef.declName == declName
| _ => false
private def partitionPreDefs (preDefs : Array PreDefinition) : Array (Array PreDefinition) :=
let getPreDef := fun declName => (preDefs.find? fun preDef => preDef.declName == declName).get!
let vertices := preDefs.toList.map (·.declName)
let successorsOf := fun declName => (getPreDef declName).value.foldConsts [] fun declName successors =>
if preDefs.any fun preDef => preDef.declName == declName then
declName :: successors
else
successors
let sccs := SCC.scc vertices successorsOf
sccs.toArray.map fun scc => scc.toArray.map getPreDef
let getPreDef := fun declName => (preDefs.find? fun preDef => preDef.declName == declName).get!
let vertices := preDefs.toList.map (·.declName)
let successorsOf := fun declName => (getPreDef declName).value.foldConsts [] fun declName successors =>
if preDefs.any fun preDef => preDef.declName == declName then
declName :: successors
else
successors
let sccs := SCC.scc vertices successorsOf
sccs.toArray.map fun scc => scc.toArray.map getPreDef
private def collectMVarsAtPreDef (preDef : PreDefinition) : StateRefT CollectMVars.State MetaM Unit := do
collectMVars preDef.value
collectMVars preDef.type
collectMVars preDef.value
collectMVars preDef.type
private def getMVarsAtPreDef (preDef : PreDefinition) : MetaM (Array MVarId) := do
let (_, s) ← (collectMVarsAtPreDef preDef).run {}
pure s.result
let (_, s) ← (collectMVarsAtPreDef preDef).run {}
pure s.result
private def ensureNoUnassignedMVarsAtPreDef (preDef : PreDefinition) : TermElabM Unit := do
let pendingMVarIds ← liftMetaM $ getMVarsAtPreDef preDef
if ← logUnassignedUsingErrorInfos pendingMVarIds then
throwAbort
let pendingMVarIds ← liftMetaM $ getMVarsAtPreDef preDef
if ← logUnassignedUsingErrorInfos pendingMVarIds then
throwAbort
def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := do
for preDef in preDefs do
trace[Elab.definition.body]! "{preDef.declName} : {preDef.type} :=\n{preDef.value}"
for preDef in preDefs do
ensureNoUnassignedMVarsAtPreDef preDef
for preDefs in partitionPreDefs preDefs do
trace[Elab.definition.scc]! "{preDefs.map (·.declName)}"
if preDefs.size == 1 && isNonRecursive preDefs[0] then
let preDef := preDefs[0]
if preDef.modifiers.isNoncomputable then
addNonRec preDef
for preDef in preDefs do
trace[Elab.definition.body]! "{preDef.declName} : {preDef.type} :=\n{preDef.value}"
for preDef in preDefs do
ensureNoUnassignedMVarsAtPreDef preDef
for preDefs in partitionPreDefs preDefs do
trace[Elab.definition.scc]! "{preDefs.map (·.declName)}"
if preDefs.size == 1 && isNonRecursive preDefs[0] then
let preDef := preDefs[0]
if preDef.modifiers.isNoncomputable then
addNonRec preDef
else
addAndCompileNonRec preDef
else if preDefs.any (·.modifiers.isUnsafe) then
addAndCompileUnsafe preDefs
else if preDefs.any (·.modifiers.isPartial) then
addAndCompilePartial preDefs
else
addAndCompileNonRec preDef
else if preDefs.any (·.modifiers.isUnsafe) then
addAndCompileUnsafe preDefs
else if preDefs.any (·.modifiers.isPartial) then
addAndCompilePartial preDefs
else
mapError
(orelseMergeErrors
(structuralRecursion preDefs)
(WFRecursion preDefs))
(fun msg =>
let preDefMsgs := preDefs.toList.map (MessageData.ofExpr $ mkConst ·.declName)
msg!"fail to show termination for{indentD (MessageData.joinSep preDefMsgs Format.line)}\nwith errors\n{msg}")
mapError
(orelseMergeErrors
(structuralRecursion preDefs)
(WFRecursion preDefs))
(fun msg =>
let preDefMsgs := preDefs.toList.map (MessageData.ofExpr $ mkConst ·.declName)
msg!"fail to show termination for{indentD (MessageData.joinSep preDefMsgs Format.line)}\nwith errors\n{msg}")
end Lean.Elab

46
stage0/src/Lean/Elab/PreDefinition/MkInhabitant.lean generated
View file

@ -9,36 +9,36 @@ namespace Lean.Elab
open Meta
private def mkInhabitant? (type : Expr) : MetaM (Option Expr) := do
try
pure $ some (← mkAppM `arbitrary #[type])
catch _ =>
pure none
try
pure $ some (← mkAppM `arbitrary #[type])
catch _ =>
pure none
private def findAssumption? (xs : Array Expr) (type : Expr) : MetaM (Option Expr) := do
xs.findM? fun x => do isDefEq (← inferType x) type
xs.findM? fun x => do isDefEq (← inferType x) type
private def mkFnInhabitant? (xs : Array Expr) (type : Expr) : MetaM (Option Expr) :=
let rec loop
| 0, type => mkInhabitant? type
| i+1, type => do
let x := xs[i]
let type ← mkForallFVars #[x] type;
match ← mkInhabitant? type with
| none => loop i type
| some val => pure $ some (← mkLambdaFVars xs[0:i] val)
loop xs.size type
let rec loop
| 0, type => mkInhabitant? type
| i+1, type => do
let x := xs[i]
let type ← mkForallFVars #[x] type;
match ← mkInhabitant? type with
| none => loop i type
| some val => pure $ some (← mkLambdaFVars xs[0:i] val)
loop xs.size type
/- TODO: add a global IO.Ref to let users customize/extend this procedure -/
def mkInhabitantFor (declName : Name) (xs : Array Expr) (type : Expr) : MetaM Expr := do
match ← mkInhabitant? type with
| some val => mkLambdaFVars xs val
| none =>
match ← findAssumption? xs type with
| some x => mkLambdaFVars xs x
| none =>
match ← mkFnInhabitant? xs type with
| some val => pure val
| none => throwError! "failed to compile partial definition '{declName}', failed to show that type is inhabited"
match ← mkInhabitant? type with
| some val => mkLambdaFVars xs val
| none =>
match ← findAssumption? xs type with
| some x => mkLambdaFVars xs x
| none =>
match ← mkFnInhabitant? xs type with
| some val => pure val
| none => throwError! "failed to compile partial definition '{declName}', failed to show that type is inhabited"
end Lean.Elab

542
stage0/src/Lean/Elab/PreDefinition/Structural.lean generated
View file

@ -13,173 +13,173 @@ namespace Lean.Elab
open Meta
private def getFixedPrefix (declName : Name) (xs : Array Expr) (value : Expr) : Nat :=
let visitor {ω} : StateRefT Nat (ST ω) Unit :=
value.forEach' fun e =>
if e.isAppOf declName then do
let args := e.getAppArgs
modify fun numFixed => if args.size < numFixed then args.size else numFixed
-- we continue searching if the e's arguments are not a prefix of `xs`
pure !args.isPrefixOf xs
else
pure true
runST fun _ => do let (_, numFixed) ← visitor.run xs.size; pure numFixed
let visitor {ω} : StateRefT Nat (ST ω) Unit :=
value.forEach' fun e =>
if e.isAppOf declName then do
let args := e.getAppArgs
modify fun numFixed => if args.size < numFixed then args.size else numFixed
-- we continue searching if the e's arguments are not a prefix of `xs`
pure !args.isPrefixOf xs
else
pure true
runST fun _ => do let (_, numFixed) ← visitor.run xs.size; pure numFixed
structure RecArgInfo :=
/- `fixedParams ++ ys` are the arguments of the function we are trying to justify termination using structural recursion. -/
(fixedParams : Array Expr)
(ys : Array Expr) -- recursion arguments
(pos : Nat) -- position in `ys` of the argument we are recursing on
(indicesPos : Array Nat) -- position in `ys` of the inductive datatype indices we are recursing on
(indName : Name) -- inductive datatype name of the argument we are recursing on
(indLevels : List Level) -- inductice datatype universe levels of the argument we are recursing on
(indParams : Array Expr) -- inductive datatype parameters of the argument we are recursing on
(indIndices : Array Expr) -- inductive datatype indices of the argument we are recursing on, it is equal to `indicesPos.map fun i => ys.get! i`
(reflexive : Bool) -- true if we are recursing over a reflexive inductive datatype
/- `fixedParams ++ ys` are the arguments of the function we are trying to justify termination using structural recursion. -/
(fixedParams : Array Expr)
(ys : Array Expr) -- recursion arguments
(pos : Nat) -- position in `ys` of the argument we are recursing on
(indicesPos : Array Nat) -- position in `ys` of the inductive datatype indices we are recursing on
(indName : Name) -- inductive datatype name of the argument we are recursing on
(indLevels : List Level) -- inductice datatype universe levels of the argument we are recursing on
(indParams : Array Expr) -- inductive datatype parameters of the argument we are recursing on
(indIndices : Array Expr) -- inductive datatype indices of the argument we are recursing on, it is equal to `indicesPos.map fun i => ys.get! i`
(reflexive : Bool) -- true if we are recursing over a reflexive inductive datatype
private def getIndexMinPos (xs : Array Expr) (indices : Array Expr) : Nat := do
let minPos := xs.size
for index in indices do
match xs.indexOf? index with
| some pos => if pos.val < minPos then minPos := pos.val
| _ => pure ()
return minPos
let minPos := xs.size
for index in indices do
match xs.indexOf? index with
| some pos => if pos.val < minPos then minPos := pos.val
| _ => pure ()
return minPos
-- Indices can only depend on other indices
private def hasBadIndexDep? (ys : Array Expr) (indices : Array Expr) : MetaM (Option (Expr × Expr)) := do
for index in indices do
let indexType ← inferType index
for y in ys do
if !indices.contains y && (← dependsOn indexType y.fvarId!) then
return some (index, y)
return none
for index in indices do
let indexType ← inferType index
for y in ys do
if !indices.contains y && (← dependsOn indexType y.fvarId!) then
return some (index, y)
return none
-- Inductive datatype parameters cannot depend on ys
private def hasBadParamDep? (ys : Array Expr) (indParams : Array Expr) : MetaM (Option (Expr × Expr)) := do
for p in indParams do
let pType ← inferType p
for y in ys do
if ← dependsOn pType y.fvarId! then
return some (p, y)
return none
for p in indParams do
let pType ← inferType p
for y in ys do
if ← dependsOn pType y.fvarId! then
return some (p, y)
return none
private def throwStructuralFailed {α} : MetaM α :=
throwError "structural recursion cannot be used"
throwError "structural recursion cannot be used"
private partial def findRecArg {α} (numFixed : Nat) (xs : Array Expr) (k : RecArgInfo → MetaM α) : MetaM α :=
let rec loop (i : Nat) : MetaM α := do
if h : i < xs.size then
let x := xs.get ⟨i, h⟩
let localDecl ← getFVarLocalDecl x
if localDecl.isLet then
throwStructuralFailed
else
let xType ← whnfD localDecl.type
matchConstInduct xType.getAppFn (fun _ => loop (i+1)) fun indInfo us => do
if !(← hasConst (mkBRecOnFor indInfo.name)) then
loop (i+1)
else if indInfo.isReflexive && !(← hasConst (mkBInductionOnFor indInfo.name)) then
loop (i+1)
let rec loop (i : Nat) : MetaM α := do
if h : i < xs.size then
let x := xs.get ⟨i, h⟩
let localDecl ← getFVarLocalDecl x
if localDecl.isLet then
throwStructuralFailed
else
let indArgs := xType.getAppArgs
let indParams := indArgs.extract 0 indInfo.nparams
let indIndices := indArgs.extract indInfo.nparams indArgs.size
if !indIndices.all Expr.isFVar then
orelseMergeErrors
(throwError! "argument #{i+1} was not used because its type is an inductive family and indices are not variables{indentExpr xType}")
(loop (i+1))
else if !indIndices.allDiff then
orelseMergeErrors
(throwError! "argument #{i+1} was not used because its type is an inductive family and indices are not pairwise distinct{indentExpr xType}")
(loop (i+1))
let xType ← whnfD localDecl.type
matchConstInduct xType.getAppFn (fun _ => loop (i+1)) fun indInfo us => do
if !(← hasConst (mkBRecOnFor indInfo.name)) then
loop (i+1)
else if indInfo.isReflexive && !(← hasConst (mkBInductionOnFor indInfo.name)) then
loop (i+1)
else
let indexMinPos := getIndexMinPos xs indIndices
let numFixed := if indexMinPos < numFixed then indexMinPos else numFixed
let fixedParams := xs.extract 0 numFixed
let ys := xs.extract numFixed xs.size
match ← hasBadIndexDep? ys indIndices with
| some (index, y) =>
let indArgs := xType.getAppArgs
let indParams := indArgs.extract 0 indInfo.nparams
let indIndices := indArgs.extract indInfo.nparams indArgs.size
if !indIndices.all Expr.isFVar then
orelseMergeErrors
(throwError! "argument #{i+1} was not used because its type is an inductive family{indentExpr xType}\nand index{indentExpr index}\ndepends on the non index{indentExpr y}")
(throwError! "argument #{i+1} was not used because its type is an inductive family and indices are not variables{indentExpr xType}")
(loop (i+1))
| none =>
match ← hasBadParamDep? ys indParams with
| some (indParam, y) =>
else if !indIndices.allDiff then
orelseMergeErrors
(throwError! "argument #{i+1} was not used because its type is an inductive family and indices are not pairwise distinct{indentExpr xType}")
(loop (i+1))
else
let indexMinPos := getIndexMinPos xs indIndices
let numFixed := if indexMinPos < numFixed then indexMinPos else numFixed
let fixedParams := xs.extract 0 numFixed
let ys := xs.extract numFixed xs.size
match ← hasBadIndexDep? ys indIndices with
| some (index, y) =>
orelseMergeErrors
(throwError! "argument #{i+1} was not used because its type is an inductive datatype{indentExpr xType}\nand parameter{indentExpr indParam}\ndepends on{indentExpr y}")
(throwError! "argument #{i+1} was not used because its type is an inductive family{indentExpr xType}\nand index{indentExpr index}\ndepends on the non index{indentExpr y}")
(loop (i+1))
| none =>
let indicesPos := indIndices.map fun index => match ys.indexOf? index with | some i => i.val | none => unreachable!
orelseMergeErrors
(k { fixedParams := fixedParams, ys := ys, pos := i - fixedParams.size,
indicesPos := indicesPos,
indName := indInfo.name,
indLevels := us,
indParams := indParams,
indIndices := indIndices,
reflexive := indInfo.isReflexive })
(loop (i+1))
else
throwStructuralFailed
loop numFixed
match ← hasBadParamDep? ys indParams with
| some (indParam, y) =>
orelseMergeErrors
(throwError! "argument #{i+1} was not used because its type is an inductive datatype{indentExpr xType}\nand parameter{indentExpr indParam}\ndepends on{indentExpr y}")
(loop (i+1))
| none =>
let indicesPos := indIndices.map fun index => match ys.indexOf? index with | some i => i.val | none => unreachable!
orelseMergeErrors
(k { fixedParams := fixedParams, ys := ys, pos := i - fixedParams.size,
indicesPos := indicesPos,
indName := indInfo.name,
indLevels := us,
indParams := indParams,
indIndices := indIndices,
reflexive := indInfo.isReflexive })
(loop (i+1))
else
throwStructuralFailed
loop numFixed
private def containsRecFn (recFnName : Name) (e : Expr) : Bool :=
(e.find? fun e => e.isConstOf recFnName).isSome
(e.find? fun e => e.isConstOf recFnName).isSome
private def ensureNoRecFn (recFnName : Name) (e : Expr) : MetaM Expr := do
if containsRecFn recFnName e then
Meta.forEachExpr e fun e => do
if e.isAppOf recFnName then
throwError! "unexpected occurrence of recursive application{indentExpr e}"
pure e
else
pure e
if containsRecFn recFnName e then
Meta.forEachExpr e fun e => do
if e.isAppOf recFnName then
throwError! "unexpected occurrence of recursive application{indentExpr e}"
pure e
else
pure e
private def throwToBelowFailed {α} : MetaM α :=
throwError "toBelow failed"
throwError "toBelow failed"
/- See toBelow -/
private partial def toBelowAux (C : Expr) : Expr → Expr → Expr → MetaM Expr
| belowDict, arg, F => do
belowDict ← whnf belowDict
trace[Elab.definition.structural]! "belowDict: {belowDict}, arg: {arg}"
match belowDict with
| Expr.app (Expr.app (Expr.const `PProd _ _) d1 _) d2 _ =>
(do toBelowAux C d1 arg (← mkAppM `PProd.fst #[F]))
<|>
(do toBelowAux C d2 arg (← mkAppM `PProd.snd #[F]))
| Expr.app (Expr.app (Expr.const `And _ _) d1 _) d2 _ =>
(do toBelowAux C d1 arg (← mkAppM `And.left #[F]))
<|>
(do toBelowAux C d2 arg (← mkAppM `And.right #[F]))
| _ => forallTelescopeReducing belowDict fun xs belowDict => do
let argArgs := arg.getAppArgs
unless argArgs.size >= xs.size do throwToBelowFailed
let n := argArgs.size
let argTailArgs := argArgs.extract (n - xs.size) n
let belowDict := belowDict.replaceFVars xs argTailArgs
| belowDict, arg, F => do
belowDict ← whnf belowDict
trace[Elab.definition.structural]! "belowDict: {belowDict}, arg: {arg}"
match belowDict with
| Expr.app belowDictFun belowDictArg _ =>
unless belowDictFun.getAppFn == C do throwToBelowFailed
unless ← isDefEq belowDictArg arg do throwToBelowFailed
pure (mkAppN F argTailArgs)
| _ => throwToBelowFailed
| Expr.app (Expr.app (Expr.const `PProd _ _) d1 _) d2 _ =>
(do toBelowAux C d1 arg (← mkAppM `PProd.fst #[F]))
<|>
(do toBelowAux C d2 arg (← mkAppM `PProd.snd #[F]))
| Expr.app (Expr.app (Expr.const `And _ _) d1 _) d2 _ =>
(do toBelowAux C d1 arg (← mkAppM `And.left #[F]))
<|>
(do toBelowAux C d2 arg (← mkAppM `And.right #[F]))
| _ => forallTelescopeReducing belowDict fun xs belowDict => do
let argArgs := arg.getAppArgs
unless argArgs.size >= xs.size do throwToBelowFailed
let n := argArgs.size
let argTailArgs := argArgs.extract (n - xs.size) n
let belowDict := belowDict.replaceFVars xs argTailArgs
match belowDict with
| Expr.app belowDictFun belowDictArg _ =>
unless belowDictFun.getAppFn == C do throwToBelowFailed
unless ← isDefEq belowDictArg arg do throwToBelowFailed
pure (mkAppN F argTailArgs)
| _ => throwToBelowFailed
/- See toBelow -/
private def withBelowDict {α} (below : Expr) (numIndParams : Nat) (k : Expr → Expr → MetaM α) : MetaM α := do
let belowType ← inferType below
trace[Elab.definition.structural]! "belowType: {belowType}"
belowType.withApp fun f args => do
let motivePos := numIndParams + 1
unless motivePos < args.size do throwError! "unexpected 'below' type{indentExpr belowType}"
let pre := mkAppN f (args.extract 0 numIndParams)
let preType ← inferType pre
forallBoundedTelescope preType (some 1) fun x _ => do
let motiveType ← inferType x[0]
let C ← mkFreshUserName `C
withLocalDeclD C motiveType fun C =>
let belowDict := mkApp pre C
let belowDict := mkAppN belowDict (args.extract (numIndParams + 1) args.size)
k C belowDict
let belowType ← inferType below
trace[Elab.definition.structural]! "belowType: {belowType}"
belowType.withApp fun f args => do
let motivePos := numIndParams + 1
unless motivePos < args.size do throwError! "unexpected 'below' type{indentExpr belowType}"
let pre := mkAppN f (args.extract 0 numIndParams)
let preType ← inferType pre
forallBoundedTelescope preType (some 1) fun x _ => do
let motiveType ← inferType x[0]
let C ← mkFreshUserName `C
withLocalDeclD C motiveType fun C =>
let belowDict := mkApp pre C
let belowDict := mkAppN belowDict (args.extract (numIndParams + 1) args.size)
k C belowDict
/-
`below` is a free variable with type of the form `I.below indParams motive indices major`,
@ -202,160 +202,158 @@ belowType.withApp fun f args => do
The dictionary is built using the `PProd` (`And` for inductive predicates).
We keep searching it until we find `C recArg`, where `C` is the auxiliary fresh variable created at `withBelowDict`. -/
private partial def toBelow (below : Expr) (numIndParams : Nat) (recArg : Expr) : MetaM Expr := do
withBelowDict below numIndParams fun C belowDict =>
toBelowAux C belowDict recArg below
withBelowDict below numIndParams fun C belowDict =>
toBelowAux C belowDict recArg below
private partial def replaceRecApps (recFnName : Name) (recArgInfo : RecArgInfo) (below : Expr) (e : Expr) : MetaM Expr :=
let rec loop : Expr → Expr → MetaM Expr
| below, e@(Expr.lam n d b c) => do
withLocalDecl n c.binderInfo (← loop below d) fun x => do
mkLambdaFVars #[x] (← loop below (b.instantiate1 x))
| below, e@(Expr.forallE n d b c) => do
withLocalDecl n c.binderInfo (← loop below d) fun x => do
mkForallFVars #[x] (← loop below (b.instantiate1 x))
| below, Expr.letE n type val body _ => do
withLetDecl n (← loop below type) (← loop below val) fun x => do
mkLetFVars #[x] (← loop below (body.instantiate1 x))
| below, Expr.mdata d e _ => do pure $ mkMData d (← loop below e)
| below, Expr.proj n i e _ => do pure $ mkProj n i (← loop below e)
| below, e@(Expr.app _ _ _) => do
let processApp (e : Expr) : MetaM Expr :=
e.withApp fun f args => do
if f.isConstOf recFnName then
let numFixed := recArgInfo.fixedParams.size
let recArgPos := recArgInfo.fixedParams.size + recArgInfo.pos
if recArgPos >= args.size then
throwError! "insufficient number of parameters at recursive application {indentExpr e}"
let recArg := args[recArgPos]
let f ← try toBelow below recArgInfo.indParams.size recArg catch _ => throwError! "failed to eliminate recursive application{indentExpr e}"
-- Recall that the fixed parameters are not in the scope of the `brecOn`. So, we skip them.
let argsNonFixed := args.extract numFixed args.size
-- The function `f` does not explicitly take `recArg` and its indices as arguments. So, we skip them too.
let fArgs := #[]
for i in [:argsNonFixed.size] do
if recArgInfo.pos != i && !recArgInfo.indicesPos.contains i then
let arg := argsNonFixed[i]
let arg ← replaceRecApps recFnName recArgInfo below arg
fArgs := fArgs.push arg
pure $ mkAppN f fArgs
let rec loop : Expr → Expr → MetaM Expr
| below, e@(Expr.lam n d b c) => do
withLocalDecl n c.binderInfo (← loop below d) fun x => do
mkLambdaFVars #[x] (← loop below (b.instantiate1 x))
| below, e@(Expr.forallE n d b c) => do
withLocalDecl n c.binderInfo (← loop below d) fun x => do
mkForallFVars #[x] (← loop below (b.instantiate1 x))
| below, Expr.letE n type val body _ => do
withLetDecl n (← loop below type) (← loop below val) fun x => do
mkLetFVars #[x] (← loop below (body.instantiate1 x))
| below, Expr.mdata d e _ => do pure $ mkMData d (← loop below e)
| below, Expr.proj n i e _ => do pure $ mkProj n i (← loop below e)
| below, e@(Expr.app _ _ _) => do
let processApp (e : Expr) : MetaM Expr :=
e.withApp fun f args => do
if f.isConstOf recFnName then
let numFixed := recArgInfo.fixedParams.size
let recArgPos := recArgInfo.fixedParams.size + recArgInfo.pos
if recArgPos >= args.size then
throwError! "insufficient number of parameters at recursive application {indentExpr e}"
let recArg := args[recArgPos]
let f ← try toBelow below recArgInfo.indParams.size recArg catch _ => throwError! "failed to eliminate recursive application{indentExpr e}"
-- Recall that the fixed parameters are not in the scope of the `brecOn`. So, we skip them.
let argsNonFixed := args.extract numFixed args.size
-- The function `f` does not explicitly take `recArg` and its indices as arguments. So, we skip them too.
let fArgs := #[]
for i in [:argsNonFixed.size] do
if recArgInfo.pos != i && !recArgInfo.indicesPos.contains i then
let arg := argsNonFixed[i]
let arg ← replaceRecApps recFnName recArgInfo below arg
fArgs := fArgs.push arg
pure $ mkAppN f fArgs
else
pure $ mkAppN (← loop below f) (← args.mapM (loop below))
let matcherApp? ← matchMatcherApp? e
match matcherApp? with
| some matcherApp =>
if !containsRecFn recFnName e then
processApp e
else
pure $ mkAppN (← loop below f) (← args.mapM (loop below))
let matcherApp? ← matchMatcherApp? e
match matcherApp? with
| some matcherApp =>
if !containsRecFn recFnName e then
processApp e
else
/- If we first try to process the `match` as a regular application. If it fails, then we try to `push` the below over the dependent `match`.
This is useful for examples such as:
```
def f (xs : List Nat) : Nat :=
match xs with
| [] => 0
| y::ys =>
match ys with
| [] => 1
| zs => f ys + 1
```
We are matching on `ys`, but still using `ys` in the second alternative.
If we push the `below` argument over the dependent match it will be able to eliminate recursive call using `zs`.
This trick is not sufficient for the slightly more complicated example:
```
def g (xs : List Nat) : Nat :=
match xs with
| [] => 0
| y::ys =>
match ys with
| [] => 1
| _::_::zs => g zs + 1
| _ => g ys + 2
```
To make it work, users would have to write the last alternative as
```
| zs => g zs + 2
```
If this is too annoying in practice, we may replace `ys` with the matching term.
This may generate weird error messages, when it doesn't work.
-/
processApp e
<|>
do let matcherApp ← mapError (matcherApp.addArg below) (fun msg => "failed to add `below` argument to 'matcher' application" ++ indentD msg)
let altsNew ← (Array.zip matcherApp.alts matcherApp.altNumParams).mapM fun (alt, numParams) =>
/- Here is an example we currently not handle
```
def f (xs : List Nat) : Nat :=
match xs with
| [] => 0
| y::ys =>
match ys with
| [] => 1
| zs => f ys + 1
```
We are matching on `ys`, but still using `ys` in the second alternative.
If we push the `below` argument over the dependent match it will be able to eliminate recursive call using `zs`.
To make it work, users have to write the second alternative as `| zs => f zs + 1`
We considered trying `processApp e` first, and only if fails trying the code below.
This trick is sufficient for solving the example above, but it is not sufficient for the slightly more complicated example:
```
def g (xs : List Nat) : Nat :=
match xs with
| [] => 0
| y::ys =>
match ys with
| [] => 1
| _::_::zs => g zs + 1
| _ => g ys + 2
```
To make it work, users would have to write the last alternative as
```
| zs => g zs + 2
```
If this is too annoying in practice, we may replace `ys` with the matching term.
This may generate weird error messages, when it doesn't work.
-/
let matcherApp ← mapError (matcherApp.addArg below) (fun msg => "failed to add `below` argument to 'matcher' application" ++ indentD msg)
let altsNew ← (Array.zip matcherApp.alts matcherApp.altNumParams).mapM fun (alt, numParams) =>
lambdaTelescope alt fun xs altBody => do
trace[Elab.definition.structural]! "altNumParams: {numParams}, xs: {xs}"
unless xs.size >= numParams do
throwError! "unexpected matcher application alternative{indentExpr alt}\nat application{indentExpr e}"
let belowForAlt := xs[numParams - 1]
mkLambdaFVars xs (← loop belowForAlt altBody)
pure { matcherApp with alts := altsNew }.toExpr
| none => processApp e
| _, e => ensureNoRecFn recFnName e
loop below e
pure { matcherApp with alts := altsNew }.toExpr
| none => processApp e
| _, e => ensureNoRecFn recFnName e
loop below e
private def mkBRecOn (recFnName : Name) (recArgInfo : RecArgInfo) (value : Expr) : MetaM Expr := do
let type := (← inferType value).headBeta
let major := recArgInfo.ys[recArgInfo.pos]
let otherArgs := recArgInfo.ys.filter fun y => y != major && !recArgInfo.indIndices.contains y
let motive ← mkForallFVars otherArgs type
let brecOnUniv ← getLevel motive
trace[Elab.definition.structural]! "brecOn univ: {brecOnUniv}"
let useBInductionOn := recArgInfo.reflexive && brecOnUniv == levelZero
if recArgInfo.reflexive && brecOnUniv != levelZero then
brecOnUniv ← decLevel brecOnUniv
let motive ← mkLambdaFVars (recArgInfo.indIndices.push major) motive
trace[Elab.definition.structural]! "brecOn motive: {motive}"
let brecOn :=
if useBInductionOn then
Lean.mkConst (mkBInductionOnFor recArgInfo.indName) recArgInfo.indLevels
else
Lean.mkConst (mkBRecOnFor recArgInfo.indName) (brecOnUniv :: recArgInfo.indLevels)
let brecOn := mkAppN brecOn recArgInfo.indParams
let brecOn := mkApp brecOn motive
let brecOn := mkAppN brecOn recArgInfo.indIndices
let brecOn := mkApp brecOn major
check brecOn
let brecOnType ← inferType brecOn
trace[Elab.definition.structural]! "brecOn {brecOn}"
trace[Elab.definition.structural]! "brecOnType {brecOnType}"
forallBoundedTelescope brecOnType (some 1) fun F _ => do
let F := F[0]
let FType ← inferType F
let numIndices := recArgInfo.indIndices.size
forallBoundedTelescope FType (some $ numIndices + 1 /- major -/ + 1 /- below -/ + otherArgs.size) fun Fargs _ => do
let indicesNew := Fargs.extract 0 numIndices
let majorNew := Fargs[numIndices]
let below := Fargs[numIndices+1]
let otherArgsNew := Fargs.extract (numIndices+2) Fargs.size
let valueNew := value.replaceFVars recArgInfo.indIndices indicesNew
let valueNew := valueNew.replaceFVar major majorNew
let valueNew := valueNew.replaceFVars otherArgs otherArgsNew
let valueNew ← replaceRecApps recFnName recArgInfo below valueNew
let Farg ← mkLambdaFVars Fargs valueNew
let brecOn := mkApp brecOn Farg
pure $ mkAppN brecOn otherArgs
let type := (← inferType value).headBeta
let major := recArgInfo.ys[recArgInfo.pos]
let otherArgs := recArgInfo.ys.filter fun y => y != major && !recArgInfo.indIndices.contains y
let motive ← mkForallFVars otherArgs type
let brecOnUniv ← getLevel motive
trace[Elab.definition.structural]! "brecOn univ: {brecOnUniv}"
let useBInductionOn := recArgInfo.reflexive && brecOnUniv == levelZero
if recArgInfo.reflexive && brecOnUniv != levelZero then
brecOnUniv ← decLevel brecOnUniv
let motive ← mkLambdaFVars (recArgInfo.indIndices.push major) motive
trace[Elab.definition.structural]! "brecOn motive: {motive}"
let brecOn :=
if useBInductionOn then
Lean.mkConst (mkBInductionOnFor recArgInfo.indName) recArgInfo.indLevels
else
Lean.mkConst (mkBRecOnFor recArgInfo.indName) (brecOnUniv :: recArgInfo.indLevels)
let brecOn := mkAppN brecOn recArgInfo.indParams
let brecOn := mkApp brecOn motive
let brecOn := mkAppN brecOn recArgInfo.indIndices
let brecOn := mkApp brecOn major
check brecOn
let brecOnType ← inferType brecOn
trace[Elab.definition.structural]! "brecOn {brecOn}"
trace[Elab.definition.structural]! "brecOnType {brecOnType}"
forallBoundedTelescope brecOnType (some 1) fun F _ => do
let F := F[0]
let FType ← inferType F
let numIndices := recArgInfo.indIndices.size
forallBoundedTelescope FType (some $ numIndices + 1 /- major -/ + 1 /- below -/ + otherArgs.size) fun Fargs _ => do
let indicesNew := Fargs.extract 0 numIndices
let majorNew := Fargs[numIndices]
let below := Fargs[numIndices+1]
let otherArgsNew := Fargs.extract (numIndices+2) Fargs.size
let valueNew := value.replaceFVars recArgInfo.indIndices indicesNew
let valueNew := valueNew.replaceFVar major majorNew
let valueNew := valueNew.replaceFVars otherArgs otherArgsNew
let valueNew ← replaceRecApps recFnName recArgInfo below valueNew
let Farg ← mkLambdaFVars Fargs valueNew
let brecOn := mkApp brecOn Farg
pure $ mkAppN brecOn otherArgs
private def elimRecursion (preDef : PreDefinition) : MetaM PreDefinition :=
withoutModifyingEnv do lambdaTelescope preDef.value fun xs value => do
addAsAxiom preDef
trace[Elab.definition.structural]! "{preDef.declName} {xs} :=\n{value}"
let numFixed := getFixedPrefix preDef.declName xs value
findRecArg numFixed xs fun recArgInfo => do
-- when (recArgInfo.indName == `Nat) throwStructuralFailed -- HACK to skip Nat argument
let valueNew ← mkBRecOn preDef.declName recArgInfo value
let valueNew ← mkLambdaFVars xs valueNew
trace[Elab.definition.structural]! "result: {valueNew}"
-- Recursive applications may still occur in expressions that were not visited by replaceRecApps (e.g., in types)
let valueNew ← ensureNoRecFn preDef.declName valueNew
pure { preDef with value := valueNew }
withoutModifyingEnv do lambdaTelescope preDef.value fun xs value => do
addAsAxiom preDef
trace[Elab.definition.structural]! "{preDef.declName} {xs} :=\n{value}"
let numFixed := getFixedPrefix preDef.declName xs value
findRecArg numFixed xs fun recArgInfo => do
-- when (recArgInfo.indName == `Nat) throwStructuralFailed -- HACK to skip Nat argument
let valueNew ← mkBRecOn preDef.declName recArgInfo value
let valueNew ← mkLambdaFVars xs valueNew
trace[Elab.definition.structural]! "result: {valueNew}"
-- Recursive applications may still occur in expressions that were not visited by replaceRecApps (e.g., in types)
let valueNew ← ensureNoRecFn preDef.declName valueNew
pure { preDef with value := valueNew }
def structuralRecursion (preDefs : Array PreDefinition) : TermElabM Unit :=
if preDefs.size != 1 then
throwError "structural recursion does not handle mutually recursive functions"
else do
let preDefNonRec ← elimRecursion preDefs[0]
addNonRec preDefNonRec
addAndCompileUnsafeRec preDefs
if preDefs.size != 1 then
throwError "structural recursion does not handle mutually recursive functions"
else do
let preDefNonRec ← elimRecursion preDefs[0]
addNonRec preDefNonRec
addAndCompileUnsafeRec preDefs
builtin_initialize
registerTraceClass `Elab.definition.structural

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

@ -10,7 +10,7 @@ namespace Elab
open Meta
def WFRecursion (preDefs : Array PreDefinition) : TermElabM Unit :=
throwError "well founded recursion has not been implemented yet"
throwError "well founded recursion has not been implemented yet"
end Elab
end Lean

868
stage0/src/Lean/Expr.lean generated
View file

File diff suppressed because it is too large Load diff

28
stage0/src/Lean/InternalExceptionId.lean generated
View file

@ -7,30 +7,30 @@ Authors: Leonardo de Moura
namespace Lean
structure InternalExceptionId :=
(idx : Nat := 0)
(idx : Nat := 0)
instance : Inhabited InternalExceptionId := ⟨{}⟩
instance : HasBeq InternalExceptionId :=
⟨fun id₁ id₂ => id₁.idx == id₂.idx⟩
⟨fun id₁ id₂ => id₁.idx == id₂.idx⟩
builtin_initialize internalExceptionsRef : IO.Ref (Array Name) ← IO.mkRef #[]
def registerInternalExceptionId (name : Name) : IO InternalExceptionId := do
let exs ← internalExceptionsRef.get
if exs.contains name then throw $ IO.userError s!"invalid internal exception id, '{name}' has already been used"
let nextIdx := exs.size
internalExceptionsRef.modify fun a => a.push name
pure { idx := nextIdx }
let exs ← internalExceptionsRef.get
if exs.contains name then throw $ IO.userError s!"invalid internal exception id, '{name}' has already been used"
let nextIdx := exs.size
internalExceptionsRef.modify fun a => a.push name
pure { idx := nextIdx }
def InternalExceptionId.toString (id : InternalExceptionId) : String :=
s!"internal exception #{id.idx}"
s!"internal exception #{id.idx}"
def InternalExceptionId.getName (id : InternalExceptionId) : IO Name := do
let exs ← internalExceptionsRef.get
let i := id.idx;
if h : i < exs.size then
pure $ exs.get ⟨i, h⟩
else
throw $ IO.userError "invalid internal exception id"
let exs ← internalExceptionsRef.get
let i := id.idx;
if h : i < exs.size then
pure $ exs.get ⟨i, h⟩
else
throw $ IO.userError "invalid internal exception id"
end Lean

180
stage0/src/Lean/KeyedDeclsAttribute.lean generated
View file

@ -29,140 +29,140 @@ abbrev Key := Name
Important: `mkConst valueTypeName` and `γ` must be definitionally equal. -/
structure Def (γ : Type) :=
(builtinName : Name) -- Builtin attribute name (e.g., `builtinTermElab)
(name : Name) -- Attribute name (e.g., `termElab)
(descr : String) -- Attribute description
(valueTypeName : Name)
-- Convert `Syntax` into a `Key`, the default implementation expects an identifier.
(evalKey : Bool → Syntax → AttrM Key :=
fun builtin arg => match attrParamSyntaxToIdentifier arg with
| some id => pure id
| none => throwError "invalid attribute argument, expected identifier")
(builtinName : Name) -- Builtin attribute name (e.g., `builtinTermElab)
(name : Name) -- Attribute name (e.g., `termElab)
(descr : String) -- Attribute description
(valueTypeName : Name)
-- Convert `Syntax` into a `Key`, the default implementation expects an identifier.
(evalKey : Bool → Syntax → AttrM Key :=
fun builtin arg => match attrParamSyntaxToIdentifier arg with
| some id => pure id
| none => throwError "invalid attribute argument, expected identifier")
instance {γ} : Inhabited (Def γ) :=
⟨{ builtinName := arbitrary _, name := arbitrary _, descr := arbitrary _, valueTypeName := arbitrary _ }⟩
⟨{ builtinName := arbitrary _, name := arbitrary _, descr := arbitrary _, valueTypeName := arbitrary _ }⟩
structure OLeanEntry :=
(key : Key)
(decl : Name) -- Name of a declaration stored in the environment which has type `mkConst Def.valueTypeName`.
(key : Key)
(decl : Name) -- Name of a declaration stored in the environment which has type `mkConst Def.valueTypeName`.
structure AttributeEntry (γ : Type) extends OLeanEntry :=
/- Recall that we cannot store `γ` into .olean files because it is a closure.
Given `OLeanEntry.decl`, we convert it into a `γ` by using the unsafe function `evalConstCheck`. -/
(value : γ)
/- Recall that we cannot store `γ` into .olean files because it is a closure.
Given `OLeanEntry.decl`, we convert it into a `γ` by using the unsafe function `evalConstCheck`. -/
(value : γ)
abbrev Table (γ : Type) := SMap Key (List γ)
structure ExtensionState (γ : Type) :=
(newEntries : List OLeanEntry := [])
(table : Table γ := {})
(newEntries : List OLeanEntry := [])
(table : Table γ := {})
abbrev Extension (γ : Type) := PersistentEnvExtension OLeanEntry (AttributeEntry γ) (ExtensionState γ)
end KeyedDeclsAttribute
structure KeyedDeclsAttribute (γ : Type) :=
(defn : KeyedDeclsAttribute.Def γ)
-- imported/builtin instances
(tableRef : IO.Ref (KeyedDeclsAttribute.Table γ))
-- instances from current module
(ext : KeyedDeclsAttribute.Extension γ)
(defn : KeyedDeclsAttribute.Def γ)
-- imported/builtin instances
(tableRef : IO.Ref (KeyedDeclsAttribute.Table γ))
-- instances from current module
(ext : KeyedDeclsAttribute.Extension γ)
namespace KeyedDeclsAttribute
def Table.insert {γ : Type} (table : Table γ) (k : Key) (v : γ) : Table γ :=
match table.find? k with
| some vs => SMap.insert table k (v::vs)
| none => SMap.insert table k [v]
match table.find? k with
| some vs => SMap.insert table k (v::vs)
| none => SMap.insert table k [v]
instance {γ} : Inhabited (ExtensionState γ) := ⟨{}⟩
instance {γ} : Inhabited (KeyedDeclsAttribute γ) :=
⟨{ defn := arbitrary _, tableRef := arbitrary _, ext := arbitrary _ }⟩
⟨{ defn := arbitrary _, tableRef := arbitrary _, ext := arbitrary _ }⟩
private def mkInitial {γ} (tableRef : IO.Ref (Table γ)) : IO (ExtensionState γ) := do
let table ← tableRef.get
pure { table := table }
let table ← tableRef.get
pure { table := table }
private unsafe def addImported {γ} (df : Def γ) (tableRef : IO.Ref (Table γ)) (es : Array (Array OLeanEntry)) : ImportM (ExtensionState γ) := do
let ctx ← read
let table ← tableRef.get
let table ← es.foldlM
(fun table entries =>
entries.foldlM
(fun (table : Table γ) entry =>
match ctx.env.evalConstCheck γ ctx.opts df.valueTypeName entry.decl with
| Except.ok f => pure $ table.insert entry.key f
| Except.error ex => throw (IO.userError ex))
table)
table
pure { table := table }
let ctx ← read
let table ← tableRef.get
let table ← es.foldlM
(fun table entries =>
entries.foldlM
(fun (table : Table γ) entry =>
match ctx.env.evalConstCheck γ ctx.opts df.valueTypeName entry.decl with
| Except.ok f => pure $ table.insert entry.key f
| Except.error ex => throw (IO.userError ex))
table)
table
pure { table := table }
private def addExtensionEntry {γ} (s : ExtensionState γ) (e : AttributeEntry γ) : ExtensionState γ :=
{ table := s.table.insert e.key e.value, newEntries := e.toOLeanEntry :: s.newEntries }
{ table := s.table.insert e.key e.value, newEntries := e.toOLeanEntry :: s.newEntries }
def addBuiltin {γ} (attr : KeyedDeclsAttribute γ) (key : Key) (val : γ) : IO Unit :=
attr.tableRef.modify $ fun m => m.insert key val
attr.tableRef.modify $ fun m => m.insert key val
/--
def _regBuiltin$(declName) : IO Unit :=
@addBuiltin $(mkConst valueTypeName) $(mkConst attrDeclName) $(key) $(mkConst declName)
-/
def declareBuiltin {γ} (df : Def γ) (attrDeclName : Name) (env : Environment) (key : Key) (declName : Name) : IO Environment :=
let name := `_regBuiltin ++ declName
let type := mkApp (mkConst `IO) (mkConst `Unit)
let val := mkAppN (mkConst `Lean.KeyedDeclsAttribute.addBuiltin) #[mkConst df.valueTypeName, mkConst attrDeclName, toExpr key, mkConst declName]
let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque, isUnsafe := false }
match env.addAndCompile {} decl with
-- TODO: pretty print error
| Except.error e => do
let msg ← (e.toMessageData {}).toString
throw (IO.userError s!"failed to emit registration code for builtin '{declName}': {msg}")
| Except.ok env => IO.ofExcept (setBuiltinInitAttr env name)
let name := `_regBuiltin ++ declName
let type := mkApp (mkConst `IO) (mkConst `Unit)
let val := mkAppN (mkConst `Lean.KeyedDeclsAttribute.addBuiltin) #[mkConst df.valueTypeName, mkConst attrDeclName, toExpr key, mkConst declName]
let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque, isUnsafe := false }
match env.addAndCompile {} decl with
-- TODO: pretty print error
| Except.error e => do
let msg ← (e.toMessageData {}).toString
throw (IO.userError s!"failed to emit registration code for builtin '{declName}': {msg}")
| Except.ok env => IO.ofExcept (setBuiltinInitAttr env name)
/- TODO: add support for scoped attributes -/
protected unsafe def init {γ} (df : Def γ) (attrDeclName : Name) : IO (KeyedDeclsAttribute γ) := do
let tableRef ← IO.mkRef ({} : Table γ)
let ext : Extension γ ← registerPersistentEnvExtension {
name := df.name,
mkInitial := mkInitial tableRef,
addImportedFn := addImported df tableRef,
addEntryFn := addExtensionEntry,
exportEntriesFn := fun s => s.newEntries.reverse.toArray,
statsFn := fun s => f!"number of local entries: {s.newEntries.length}"
}
registerBuiltinAttribute {
name := df.builtinName,
descr := "(builtin) " ++ df.descr,
add := fun declName arg persistent => do
unless persistent do throwError! "invalid attribute '{df.builtinName}', must be persistent"
let key ← df.evalKey true arg
let decl ← getConstInfo declName
match decl.type with
| Expr.const c _ _ =>
if c != df.valueTypeName then throwError! "unexpected type at '{declName}', '{df.valueTypeName}' expected"
else
let env ← getEnv
let env ← liftIO $ declareBuiltin df attrDeclName env key declName
setEnv env
| _ => throwError! "unexpected type at '{declName}', '{df.valueTypeName}' expected",
applicationTime := AttributeApplicationTime.afterCompilation
}
registerBuiltinAttribute {
name := df.name,
descr := df.descr,
add := fun constName arg persistent => do
let key ← df.evalKey false arg
let val ← evalConstCheck γ df.valueTypeName constName
let env ← getEnv
setEnv $ ext.addEntry env { key := key, decl := constName, value := val },
applicationTime := AttributeApplicationTime.afterCompilation
}
pure { defn := df, tableRef := tableRef, ext := ext }
let tableRef ← IO.mkRef ({} : Table γ)
let ext : Extension γ ← registerPersistentEnvExtension {
name := df.name,
mkInitial := mkInitial tableRef,
addImportedFn := addImported df tableRef,
addEntryFn := addExtensionEntry,
exportEntriesFn := fun s => s.newEntries.reverse.toArray,
statsFn := fun s => f!"number of local entries: {s.newEntries.length}"
}
registerBuiltinAttribute {
name := df.builtinName,
descr := "(builtin) " ++ df.descr,
add := fun declName arg persistent => do
unless persistent do throwError! "invalid attribute '{df.builtinName}', must be persistent"
let key ← df.evalKey true arg
let decl ← getConstInfo declName
match decl.type with
| Expr.const c _ _ =>
if c != df.valueTypeName then throwError! "unexpected type at '{declName}', '{df.valueTypeName}' expected"
else
let env ← getEnv
let env ← liftIO $ declareBuiltin df attrDeclName env key declName
setEnv env
| _ => throwError! "unexpected type at '{declName}', '{df.valueTypeName}' expected",
applicationTime := AttributeApplicationTime.afterCompilation
}
registerBuiltinAttribute {
name := df.name,
descr := df.descr,
add := fun constName arg persistent => do
let key ← df.evalKey false arg
let val ← evalConstCheck γ df.valueTypeName constName
let env ← getEnv
setEnv $ ext.addEntry env { key := key, decl := constName, value := val },
applicationTime := AttributeApplicationTime.afterCompilation
}
pure { defn := df, tableRef := tableRef, ext := ext }
/-- Retrieve values tagged with `[attr key]` or `[builtinAttr key]`. -/
def getValues {γ} (attr : KeyedDeclsAttribute γ) (env : Environment) (key : Name) : List γ :=
(attr.ext.getState env).table.findD key []
(attr.ext.getState env).table.findD key []
end KeyedDeclsAttribute

402
stage0/src/Lean/Level.lean generated
View file

@ -25,62 +25,62 @@ namespace Lean
def Level.Data := UInt64
instance : Inhabited Level.Data :=
inferInstanceAs (Inhabited UInt64)
inferInstanceAs (Inhabited UInt64)
def Level.Data.hash (c : Level.Data) : USize :=
c.toUInt32.toUSize
c.toUInt32.toUSize
instance : HasBeq Level.Data :=
⟨fun (a b : UInt64) => a == b⟩
⟨fun (a b : UInt64) => a == b⟩
def Level.Data.depth (c : Level.Data) : UInt32 :=
(c.shiftRight 40).toUInt32
(c.shiftRight 40).toUInt32
def Level.Data.hasMVar (c : Level.Data) : Bool :=
((c.shiftRight 32).land 1) == 1
((c.shiftRight 32).land 1) == 1
def Level.Data.hasParam (c : Level.Data) : Bool :=
((c.shiftRight 33).land 1) == 1
((c.shiftRight 33).land 1) == 1
def Level.mkData (h : USize) (depth : Nat) (hasMVar hasParam : Bool) : Level.Data :=
if depth > Nat.pow 2 24 - 1 then panic! "universe level depth is too big"
else
let r : UInt64 := h.toUInt32.toUInt64 + hasMVar.toUInt64.shiftLeft 32 + hasParam.toUInt64.shiftLeft 33 + depth.toUInt64.shiftLeft 40
r
if depth > Nat.pow 2 24 - 1 then panic! "universe level depth is too big"
else
let r : UInt64 := h.toUInt32.toUInt64 + hasMVar.toUInt64.shiftLeft 32 + hasParam.toUInt64.shiftLeft 33 + depth.toUInt64.shiftLeft 40
r
open Level
inductive Level
| zero : Data → Level
| succ : Level → Data → Level
| max : Level → Level → Data → Level
| imax : Level → Level → Data → Level
| param : Name → Data → Level
| mvar : Name → Data → Level
| zero : Data → Level
| succ : Level → Data → Level
| max : Level → Level → Data → Level
| imax : Level → Level → Data → Level
| param : Name → Data → Level
| mvar : Name → Data → Level
namespace Level
@[inline] def data : Level → Data
| zero d => d
| mvar _ d => d
| param _ d => d
| succ _ d => d
| max _ _ d => d
| imax _ _ d => d
| zero d => d
| mvar _ d => d
| param _ d => d
| succ _ d => d
| max _ _ d => d
| imax _ _ d => d
protected def hash (u : Level) : USize :=
u.data.hash
u.data.hash
instance : Hashable Level := ⟨Level.hash⟩
def depth (u : Level) : Nat :=
u.data.depth.toNat
u.data.depth.toNat
def hasMVar (u : Level) : Bool :=
u.data.hasMVar
u.data.hasMVar
def hasParam (u : Level) : Bool :=
u.data.hasParam
u.data.hasParam
@[export lean_level_hash] def hashEx : Level → USize := Level.hash
@[export lean_level_has_mvar] def hasMVarEx : Level → Bool := hasMVar
@ -90,26 +90,26 @@ u.data.hasParam
end Level
def levelZero :=
Level.zero $ mkData 2221 0 false false
Level.zero $ mkData 2221 0 false false
def mkLevelMVar (mvarId : Name) :=
Level.mvar mvarId $ mkData (mixHash 2237 $ hash mvarId) 0 true false
Level.mvar mvarId $ mkData (mixHash 2237 $ hash mvarId) 0 true false
def mkLevelParam (name : Name) :=
Level.param name $ mkData (mixHash 2239 $ hash name) 0 false true
Level.param name $ mkData (mixHash 2239 $ hash name) 0 false true
def mkLevelSucc (u : Level) :=
Level.succ u $ mkData (mixHash 2243 $ hash u) (u.depth + 1) u.hasMVar u.hasParam
Level.succ u $ mkData (mixHash 2243 $ hash u) (u.depth + 1) u.hasMVar u.hasParam
def mkLevelMax (u v : Level) :=
Level.max u v $ mkData (mixHash 2251 $ mixHash (hash u) (hash v)) (Nat.max u.depth v.depth + 1)
(u.hasMVar || v.hasMVar)
(u.hasParam || v.hasParam)
Level.max u v $ mkData (mixHash 2251 $ mixHash (hash u) (hash v)) (Nat.max u.depth v.depth + 1)
(u.hasMVar || v.hasMVar)
(u.hasParam || v.hasParam)
def mkLevelIMax (u v : Level) :=
Level.imax u v $ mkData (mixHash 2267 $ mixHash (hash u) (hash v)) (Nat.max u.depth v.depth + 1)
(u.hasMVar || v.hasMVar)
(u.hasParam || v.hasParam)
Level.imax u v $ mkData (mixHash 2267 $ mixHash (hash u) (hash v)) (Nat.max u.depth v.depth + 1)
(u.hasMVar || v.hasMVar)
(u.hasParam || v.hasParam)
def levelOne := mkLevelSucc levelZero
@ -125,79 +125,79 @@ namespace Level
instance : Inhabited Level := ⟨levelZero⟩
def isZero : Level → Bool
| zero _ => true
| _ => false
| zero _ => true
| _ => false
def isSucc : Level → Bool
| succ _ _ => true
| _ => false
| succ .. => true
| _ => false
def isMax : Level → Bool
| max _ _ _ => true
| _ => false
| max .. => true
| _ => false
def isIMax : Level → Bool
| imax _ _ _ => true
| _ => false
| imax .. => true
| _ => false
def isMaxIMax : Level → Bool
| max _ _ _ => true
| imax _ _ _ => true
| _ => false
| max .. => true
| imax .. => true
| _ => false
def isParam : Level → Bool
| param _ _ => true
| _ => false
| param .. => true
| _ => false
def isMVar : Level → Bool
| mvar _ _ => true
| _ => false
| mvar .. => true
| _ => false
def mvarId! : Level → Name
| mvar mvarId _ => mvarId
| _ => panic! "metavariable expected"
| mvar mvarId _ => mvarId
| _ => panic! "metavariable expected"
/-- If result is true, then forall assignments `A` which assigns all parameters and metavariables occuring
in `l`, `l[A] != zero` -/
def isNeverZero : Level → Bool
| zero _ => false
| param _ _ => false
| mvar _ _ => false
| succ _ _ => true
| max l₁ l₂ _ => isNeverZero l₁ || isNeverZero l₂
| imax l₁ l₂ _ => isNeverZero l₂
| zero _ => false
| param .. => false
| mvar .. => false
| succ .. => true
| max l₁ l₂ _ => isNeverZero l₁ || isNeverZero l₂
| imax l₁ l₂ _ => isNeverZero l₂
def ofNat : Nat → Level
| 0 => levelZero
| n+1 => mkLevelSucc (ofNat n)
| 0 => levelZero
| n+1 => mkLevelSucc (ofNat n)
def addOffsetAux : Nat → Level → Level
| 0, u => u
| (n+1), u => addOffsetAux n (mkLevelSucc u)
| 0, u => u
| (n+1), u => addOffsetAux n (mkLevelSucc u)
def addOffset (u : Level) (n : Nat) : Level :=
u.addOffsetAux n
u.addOffsetAux n
def isExplicit : Level → Bool
| zero _ => true
| succ u _ => !u.hasMVar && !u.hasParam && isExplicit u
| _ => false
| zero _ => true
| succ u _ => !u.hasMVar && !u.hasParam && isExplicit u
| _ => false
def getOffsetAux : Level → Nat → Nat
| succ u _, r => getOffsetAux u (r+1)
| _, r => r
| succ u _, r => getOffsetAux u (r+1)
| _, r => r
def getOffset (lvl : Level) : Nat :=
getOffsetAux lvl 0
getOffsetAux lvl 0
def getLevelOffset : Level → Level
| succ u _ => getLevelOffset u
| u => u
| succ u _ => getLevelOffset u
| u => u
def toNat (lvl : Level) : Option Nat :=
match lvl.getLevelOffset with
| zero _ => lvl.getOffset
| _ => none
match lvl.getLevelOffset with
| zero _ => lvl.getOffset
| _ => none
@[extern "lean_level_eq"]
protected constant beq (a : @& Level) (b : @& Level) : Bool := arbitrary _
@ -206,34 +206,34 @@ instance : HasBeq Level := ⟨Level.beq⟩
/-- `occurs u l` return `true` iff `u` occurs in `l`. -/
def occurs : Level → Level → Bool
| u, v@(succ v₁ _) => u == v || occurs u v₁
| u, v@(max v₁ v₂ _) => u == v || occurs u v₁ || occurs u v₂
| u, v@(imax v₁ v₂ _) => u == v || occurs u v₁ || occurs u v₂
| u, v => u == v
| u, v@(succ v₁ _) => u == v || occurs u v₁
| u, v@(max v₁ v₂ _) => u == v || occurs u v₁ || occurs u v₂
| u, v@(imax v₁ v₂ _) => u == v || occurs u v₁ || occurs u v₂
| u, v => u == v
def ctorToNat : Level → Nat
| zero _ => 0
| param _ _ => 1
| mvar _ _ => 2
| succ _ _ => 3
| max _ _ _ => 4
| imax _ _ _ => 5
| zero .. => 0
| param .. => 1
| mvar .. => 2
| succ .. => 3
| max .. => 4
| imax .. => 5
/- TODO: use well founded recursion. -/
partial def normLtAux : Level → Nat → Level → Nat → Bool
| succ l₁ _, k₁, l₂, k₂ => normLtAux l₁ (k₁+1) l₂ k₂
| l₁, k₁, succ l₂ _, k₂ => normLtAux l₁ k₁ l₂ (k₂+1)
| l₁@(max l₁₁ l₁₂ _), k₁, l₂@(max l₂₁ l₂₂ _), k₂ =>
if l₁ == l₂ then k₁ < k₂
else if l₁₁ == l₂₁ then normLtAux l₁₁ 0 l₂₁ 0
else normLtAux l₁₂ 0 l₂₂ 0
| l₁@(imax l₁₁ l₁₂ _), k₁, l₂@(imax l₂₁ l₂₂ _), k₂ =>
if l₁ == l₂ then k₁ < k₂
else if l₁₁ == l₂₁ then normLtAux l₁₁ 0 l₂₁ 0
else normLtAux l₁₂ 0 l₂₂ 0
| param n₁ _, k₁, param n₂ _, k₂ => if n₁ == n₂ then k₁ < k₂ else Name.lt n₁ n₂ -- use Name.lt because it is lexicographical
| mvar n₁ _, k₁, mvar n₂ _, k₂ => if n₁ == n₂ then k₁ < k₂ else Name.quickLt n₁ n₂ -- metavariables are temporary, the actual order doesn't matter
| l₁, k₁, l₂, k₂ => if l₁ == l₂ then k₁ < k₂ else ctorToNat l₁ < ctorToNat l₂
| succ l₁ _, k₁, l₂, k₂ => normLtAux l₁ (k₁+1) l₂ k₂
| l₁, k₁, succ l₂ _, k₂ => normLtAux l₁ k₁ l₂ (k₂+1)
| l₁@(max l₁₁ l₁₂ _), k₁, l₂@(max l₂₁ l₂₂ _), k₂ =>
if l₁ == l₂ then k₁ < k₂
else if l₁₁ == l₂₁ then normLtAux l₁₁ 0 l₂₁ 0
else normLtAux l₁₂ 0 l₂₂ 0
| l₁@(imax l₁₁ l₁₂ _), k₁, l₂@(imax l₂₁ l₂₂ _), k₂ =>
if l₁ == l₂ then k₁ < k₂
else if l₁₁ == l₂₁ then normLtAux l₁₁ 0 l₂₁ 0
else normLtAux l₁₂ 0 l₂₂ 0
| param n₁ _, k₁, param n₂ _, k₂ => if n₁ == n₂ then k₁ < k₂ else Name.lt n₁ n₂ -- use Name.lt because it is lexicographical
| mvar n₁ _, k₁, mvar n₂ _, k₂ => if n₁ == n₂ then k₁ < k₂ else Name.quickLt n₁ n₂ -- metavariables are temporary, the actual order doesn't matter
| l₁, k₁, l₂, k₂ => if l₁ == l₂ then k₁ < k₂ else ctorToNat l₁ < ctorToNat l₂
/--
A total order on level expressions that has the following properties
@ -241,30 +241,30 @@ partial def normLtAux : Level → Nat → Level → Nat → Bool
- `zero` is the minimal element.
This total order is used in the normalization procedure. -/
def normLt (l₁ l₂ : Level) : Bool :=
normLtAux l₁ 0 l₂ 0
normLtAux l₁ 0 l₂ 0
private def isAlreadyNormalizedCheap : Level → Bool
| zero _ => true
| param _ _ => true
| mvar _ _ => true
| succ u _ => isAlreadyNormalizedCheap u
| _ => false
| zero _ => true
| param _ _ => true
| mvar _ _ => true
| succ u _ => isAlreadyNormalizedCheap u
| _ => false
/- Auxiliary function used at `normalize` -/
private def mkIMaxAux : Level → Level → Level
| _, u@(zero _) => u
| zero _, u => u
| u₁, u₂ => if u₁ == u₂ then u₁ else mkLevelIMax u₁ u₂
| _, u@(zero _) => u
| zero _, u => u
| u₁, u₂ => if u₁ == u₂ then u₁ else mkLevelIMax u₁ u₂
/- Auxiliary function used at `normalize` -/
@[specialize] private partial def getMaxArgsAux (normalize : Level → Level) : Level → Bool → Array Level → Array Level
| max l₁ l₂ _, alreadyNormalized, lvls => getMaxArgsAux normalize l₂ alreadyNormalized (getMaxArgsAux normalize l₁ alreadyNormalized lvls)
| l, false, lvls => getMaxArgsAux normalize (normalize l) true lvls
| l, true, lvls => lvls.push l
| max l₁ l₂ _, alreadyNormalized, lvls => getMaxArgsAux normalize l₂ alreadyNormalized (getMaxArgsAux normalize l₁ alreadyNormalized lvls)
| l, false, lvls => getMaxArgsAux normalize (normalize l) true lvls
| l, true, lvls => lvls.push l
private def accMax (result : Level) (prev : Level) (offset : Nat) : Level :=
if result.isZero then prev.addOffset offset
else mkLevelMax result (prev.addOffset offset)
if result.isZero then prev.addOffset offset
else mkLevelMax result (prev.addOffset offset)
/- Auxiliary function used at `normalize`.
Remarks:
@ -275,26 +275,26 @@ else mkLevelMax result (prev.addOffset offset)
- `result` is the accumulator
-/
private partial def mkMaxAux (lvls : Array Level) (extraK : Nat) (i : Nat) (prev : Level) (prevK : Nat) (result : Level) : Level :=
if h : i < lvls.size then
let lvl := lvls.get ⟨i, h⟩
let curr := lvl.getLevelOffset
let currK := lvl.getOffset
if curr == prev then
mkMaxAux lvls extraK (i+1) curr currK result
if h : i < lvls.size then
let lvl := lvls.get ⟨i, h⟩
let curr := lvl.getLevelOffset
let currK := lvl.getOffset
if curr == prev then
mkMaxAux lvls extraK (i+1) curr currK result
else
mkMaxAux lvls extraK (i+1) curr currK (accMax result prev (extraK + prevK))
else
mkMaxAux lvls extraK (i+1) curr currK (accMax result prev (extraK + prevK))
else
accMax result prev (extraK + prevK)
accMax result prev (extraK + prevK)
/-
Auxiliary function for `normalize`. It assumes `lvls` has been sorted using `normLt`.
It finds the first position that is not an explicit universe. -/
private partial def skipExplicit (lvls : Array Level) (i : Nat) : Nat :=
if h : i < lvls.size then
let lvl := lvls.get ⟨i, h⟩
if lvl.getLevelOffset.isZero then skipExplicit lvls (i+1) else i
else
i
if h : i < lvls.size then
let lvl := lvls.get ⟨i, h⟩
if lvl.getLevelOffset.isZero then skipExplicit lvls (i+1) else i
else
i
/-
Auxiliary function for `normalize`.
@ -303,19 +303,19 @@ else
`i` starts at the first non explict level.
It assumes `lvls` has been sorted using `normLt`. -/
private partial def isExplicitSubsumedAux (lvls : Array Level) (maxExplicit : Nat) (i : Nat) : Bool :=
if h : i < lvls.size then
let lvl := lvls.get ⟨i, h⟩
if lvl.getOffset ≥ maxExplicit then true
else isExplicitSubsumedAux lvls maxExplicit (i+1)
else
false
if h : i < lvls.size then
let lvl := lvls.get ⟨i, h⟩
if lvl.getOffset ≥ maxExplicit then true
else isExplicitSubsumedAux lvls maxExplicit (i+1)
else
false
/- Auxiliary function for `normalize`. See `isExplicitSubsumedAux` -/
private def isExplicitSubsumed (lvls : Array Level) (firstNonExplicit : Nat) : Bool :=
if firstNonExplicit == 0 then false
else
let max := (lvls.get! (firstNonExplicit - 1)).getOffset;
isExplicitSubsumedAux lvls max firstNonExplicit
if firstNonExplicit == 0 then false
else
let max := (lvls.get! (firstNonExplicit - 1)).getOffset;
isExplicitSubsumedAux lvls max firstNonExplicit
partial def normalize (l : Level) : Level :=
if isAlreadyNormalizedCheap l then l
@ -344,74 +344,74 @@ partial def normalize (l : Level) : Level :=
/- Return true if `u` and `v` denote the same level.
Check is currently incomplete. -/
def isEquiv (u v : Level) : Bool :=
u == v || u.normalize == v.normalize
u == v || u.normalize == v.normalize
/-- Reduce (if possible) universe level by 1 -/
def dec : Level → Option Level
| zero _ => none
| param _ _ => none
| mvar _ _ => none
| succ l _ => l
| max l₁ l₂ _ => mkLevelMax <$> dec l₁ <*> dec l₂
/- Remark: `mkLevelMax` in the following line is not a typo.
If `dec l₂` succeeds, then `imax l₁ l₂` is equivalent to `max l₁ l₂`. -/
| imax l₁ l₂ _ => mkLevelMax <$> dec l₁ <*> dec l₂
| zero _ => none
| param _ _ => none
| mvar _ _ => none
| succ l _ => l
| max l₁ l₂ _ => mkLevelMax <$> dec l₁ <*> dec l₂
/- Remark: `mkLevelMax` in the following line is not a typo.
If `dec l₂` succeeds, then `imax l₁ l₂` is equivalent to `max l₁ l₂`. -/
| imax l₁ l₂ _ => mkLevelMax <$> dec l₁ <*> dec l₂
/- Level to Format -/
namespace LevelToFormat
inductive Result
| leaf : Format → Result
| num : Nat → Result
| offset : Result → Nat → Result
| maxNode : List Result → Result
| imaxNode : List Result → Result
| leaf : Format → Result
| num : Nat → Result
| offset : Result → Nat → Result
| maxNode : List Result → Result
| imaxNode : List Result → Result
def Result.succ : Result → Result
| Result.offset f k => Result.offset f (k+1)
| Result.num k => Result.num (k+1)
| f => Result.offset f 1
| Result.offset f k => Result.offset f (k+1)
| Result.num k => Result.num (k+1)
| f => Result.offset f 1
def Result.max : Result → Result → Result
| f, Result.maxNode Fs => Result.maxNode (f::Fs)
| f₁, f₂ => Result.maxNode [f₁, f₂]
| f, Result.maxNode Fs => Result.maxNode (f::Fs)
| f₁, f₂ => Result.maxNode [f₁, f₂]
def Result.imax : Result → Result → Result
| f, Result.imaxNode Fs => Result.imaxNode (f::Fs)
| f₁, f₂ => Result.imaxNode [f₁, f₂]
| f, Result.imaxNode Fs => Result.imaxNode (f::Fs)
| f₁, f₂ => Result.imaxNode [f₁, f₂]
def parenIfFalse : Format → Bool → Format
| f, true => f
| f, false => f.paren
| f, true => f
| f, false => f.paren
@[specialize] private def formatLst (fmt : Result → Format) : List Result → Format
| [] => Format.nil
| r::rs => Format.line ++ fmt r ++ formatLst fmt rs
| [] => Format.nil
| r::rs => Format.line ++ fmt r ++ formatLst fmt rs
partial def Result.format : Result → Bool → Format
| Result.leaf f, _ => f
| Result.num k, _ => toString k
| Result.offset f 0, r => format f r
| Result.offset f (k+1), r =>
let f' := format f false;
parenIfFalse (f' ++ "+" ++ fmt (k+1)) r
| Result.maxNode fs, r => parenIfFalse (Format.group $ "max" ++ formatLst (fun r => format r false) fs) r
| Result.imaxNode fs, r => parenIfFalse (Format.group $ "imax" ++ formatLst (fun r => format r false) fs) r
| Result.leaf f, _ => f
| Result.num k, _ => toString k
| Result.offset f 0, r => format f r
| Result.offset f (k+1), r =>
let f' := format f false;
parenIfFalse (f' ++ "+" ++ fmt (k+1)) r
| Result.maxNode fs, r => parenIfFalse (Format.group $ "max" ++ formatLst (fun r => format r false) fs) r
| Result.imaxNode fs, r => parenIfFalse (Format.group $ "imax" ++ formatLst (fun r => format r false) fs) r
def toResult : Level → Result
| zero _ => Result.num 0
| succ l _ => Result.succ (toResult l)
| max l₁ l₂ _ => Result.max (toResult l₁) (toResult l₂)
| imax l₁ l₂ _ => Result.imax (toResult l₁) (toResult l₂)
| param n _ => Result.leaf (fmt n)
| mvar n _ =>
let n := n.replacePrefix `_uniq `u;
Result.leaf ("?" ++ fmt n)
| zero _ => Result.num 0
| succ l _ => Result.succ (toResult l)
| max l₁ l₂ _ => Result.max (toResult l₁) (toResult l₂)
| imax l₁ l₂ _ => Result.imax (toResult l₁) (toResult l₂)
| param n _ => Result.leaf (fmt n)
| mvar n _ =>
let n := n.replacePrefix `_uniq `u;
Result.leaf ("?" ++ fmt n)
end LevelToFormat
protected def format (l : Level) : Format :=
(LevelToFormat.toResult l).format true
(LevelToFormat.toResult l).format true
instance : HasFormat Level := ⟨Level.format⟩
instance : HasToString Level := ⟨Format.pretty ∘ Level.format⟩
@ -427,47 +427,47 @@ instance : HasToString Level := ⟨Format.pretty ∘ Level.format⟩
@[extern "lean_level_update_succ"]
def updateSucc (lvl : Level) (newLvl : Level) (h : lvl.isSucc = true) : Level :=
mkLevelSucc newLvl
mkLevelSucc newLvl
@[inline] def updateSucc! (lvl : Level) (newLvl : Level) : Level :=
match lvl with
| succ lvl d => updateSucc (succ lvl d) newLvl rfl
| _ => panic! "succ level expected"
| succ lvl d => updateSucc (succ lvl d) newLvl rfl
| _ => panic! "succ level expected"
@[extern "lean_level_update_max"]
def updateMax (lvl : Level) (newLhs : Level) (newRhs : Level) (h : lvl.isMax = true) : Level :=
mkLevelMax newLhs newRhs
mkLevelMax newLhs newRhs
@[inline] def updateMax! (lvl : Level) (newLhs : Level) (newRhs : Level) : Level :=
match lvl with
| max lhs rhs d => updateMax (max lhs rhs d) newLhs newRhs rfl
| _ => panic! "max level expected"
match lvl with
| max lhs rhs d => updateMax (max lhs rhs d) newLhs newRhs rfl
| _ => panic! "max level expected"
@[extern "lean_level_update_imax"]
def updateIMax (lvl : Level) (newLhs : Level) (newRhs : Level) (h : lvl.isIMax = true) : Level :=
mkLevelIMax newLhs newRhs
mkLevelIMax newLhs newRhs
@[inline] def updateIMax! (lvl : Level) (newLhs : Level) (newRhs : Level) : Level :=
match lvl with
| imax lhs rhs d => updateIMax (imax lhs rhs d) newLhs newRhs rfl
| _ => panic! "imax level expected"
match lvl with
| imax lhs rhs d => updateIMax (imax lhs rhs d) newLhs newRhs rfl
| _ => panic! "imax level expected"
def mkNaryMax : List Level → Level
| [] => levelZero
| [u] => u
| u::us => mkLevelMax u (mkNaryMax us)
| [] => levelZero
| [u] => u
| u::us => mkLevelMax u (mkNaryMax us)
/- Level to Format -/
@[specialize] def instantiateParams (s : Name → Option Level) : Level → Level
| u@(zero _) => u
| u@(succ v _) => if u.hasParam then u.updateSucc! (instantiateParams s v) else u
| u@(max v₁ v₂ _) => if u.hasParam then u.updateMax! (instantiateParams s v₁) (instantiateParams s v₂) else u
| u@(imax v₁ v₂ _) => if u.hasParam then u.updateIMax! (instantiateParams s v₁) (instantiateParams s v₂) else u
| u@(param n _) => match s n with
| some u' => u'
| none => u
| u => u
| u@(zero _) => u
| u@(succ v _) => if u.hasParam then u.updateSucc! (instantiateParams s v) else u
| u@(max v₁ v₂ _) => if u.hasParam then u.updateMax! (instantiateParams s v₁) (instantiateParams s v₂) else u
| u@(imax v₁ v₂ _) => if u.hasParam then u.updateIMax! (instantiateParams s v₁) (instantiateParams s v₂) else u
| u@(param n _) => match s n with
| some u' => u'
| none => u
| u => u
end Level
@ -482,4 +482,4 @@ abbrev PLevelSet := PersistentLevelSet
end Lean
abbrev Nat.toLevel (n : Nat) : Lean.Level :=
Lean.Level.ofNat n
Lean.Level.ofNat n

42
stage0/src/Lean/Modifiers.lean generated
View file

@ -12,11 +12,11 @@ builtin_initialize protectedExt : TagDeclarationExtension ← mkTagDeclarationEx
@[export lean_add_protected]
def addProtected (env : Environment) (n : Name) : Environment :=
protectedExt.tag env n
protectedExt.tag env n
@[export lean_is_protected]
def isProtected (env : Environment) (n : Name) : Bool :=
protectedExt.isTagged env n
protectedExt.isTagged env n
builtin_initialize privateExt : EnvExtension Nat ← registerEnvExtension (pure 1)
@ -36,44 +36,44 @@ def privateHeader : Name := `_private
@[export lean_mk_private_prefix]
def mkUniquePrivatePrefix (env : Environment) : Environment × Name :=
let idx := privateExt.getState env
let p := mkNameNum (privateHeader ++ env.mainModule) idx
let env := privateExt.setState env (idx+1)
(env, p)
let idx := privateExt.getState env
let p := mkNameNum (privateHeader ++ env.mainModule) idx
let env := privateExt.setState env (idx+1)
(env, p)
@[export lean_mk_private_name]
def mkUniquePrivateName (env : Environment) (n : Name) : Environment × Name :=
let (env, p) := mkUniquePrivatePrefix env
(env, p ++ n)
let (env, p) := mkUniquePrivatePrefix env
(env, p ++ n)
def mkPrivateName (env : Environment) (n : Name) : Name :=
mkNameNum (privateHeader ++ env.mainModule) 0 ++ n
mkNameNum (privateHeader ++ env.mainModule) 0 ++ n
def isPrivateName : Name → Bool
| n@(Name.str p _ _) => n == privateHeader || isPrivateName p
| Name.num p _ _ => isPrivateName p
| _ => false
| n@(Name.str p _ _) => n == privateHeader || isPrivateName p
| Name.num p _ _ => isPrivateName p
| _ => false
@[export lean_is_private_name]
def isPrivateNameExport (n : Name) : Bool :=
isPrivateName n
isPrivateName n
private def privateToUserNameAux : Name → Name
| Name.str p s _ => mkNameStr (privateToUserNameAux p) s
| _ => Name.anonymous
| Name.str p s _ => mkNameStr (privateToUserNameAux p) s
| _ => Name.anonymous
@[export lean_private_to_user_name]
def privateToUserName? (n : Name) : Option Name :=
if isPrivateName n then privateToUserNameAux n
else none
if isPrivateName n then privateToUserNameAux n
else none
private def privatePrefixAux : Name → Name
| Name.str p _ _ => privatePrefixAux p
| n => n
| Name.str p _ _ => privatePrefixAux p
| n => n
@[export lean_private_prefix]
def privatePrefix (n : Name) : Option Name :=
if isPrivateName n then privatePrefixAux n
else none
if isPrivateName n then privatePrefixAux n
else none
end Lean

114
stage0/src/Lean/MonadEnv.lean generated
View file

@ -14,107 +14,107 @@ section Methods
variables {m : Type → Type} [MonadEnv m]
def setEnv (env : Environment) : m Unit :=
modifyEnv fun _ => env
modifyEnv fun _ => env
@[inline] def withoutModifyingEnv [Monad m] [MonadFinally m] {α : Type} (x : m α) : m α := do
let env ← getEnv
try x finally setEnv env
let env ← getEnv
try x finally setEnv env
@[inline] def matchConst [Monad m] {α : Type} (e : Expr) (failK : Unit → m α) (k : ConstantInfo → List Level → m α) : m α := do
match e with
| Expr.const constName us _ => do
match (← getEnv).find? constName with
| some cinfo => k cinfo us
| none => failK ()
| _ => failK ()
match e with
| Expr.const constName us _ => do
match (← getEnv).find? constName with
| some cinfo => k cinfo us
| none => failK ()
| _ => failK ()
@[inline] def matchConstInduct [Monad m] {α : Type} (e : Expr) (failK : Unit → m α) (k : InductiveVal → List Level → m α) : m α :=
matchConst e failK fun cinfo us =>
match cinfo with
| ConstantInfo.inductInfo val => k val us
| _ => failK ()
matchConst e failK fun cinfo us =>
match cinfo with
| ConstantInfo.inductInfo val => k val us
| _ => failK ()
@[inline] def matchConstCtor [Monad m] {α : Type} (e : Expr) (failK : Unit → m α) (k : ConstructorVal → List Level → m α) : m α :=
matchConst e failK fun cinfo us =>
match cinfo with
| ConstantInfo.ctorInfo val => k val us
| _ => failK ()
matchConst e failK fun cinfo us =>
match cinfo with
| ConstantInfo.ctorInfo val => k val us
| _ => failK ()
@[inline] def matchConstRec [Monad m] {α : Type} (e : Expr) (failK : Unit → m α) (k : RecursorVal → List Level → m α) : m α :=
matchConst e failK fun cinfo us =>
match cinfo with
| ConstantInfo.recInfo val => k val us
| _ => failK ()
matchConst e failK fun cinfo us =>
match cinfo with
| ConstantInfo.recInfo val => k val us
| _ => failK ()
section
variables [Monad m]
def hasConst (constName : Name) : m Bool := do
return (← getEnv).contains constName
return (← getEnv).contains constName
private partial def mkAuxNameAux (env : Environment) (base : Name) (i : Nat) : Name :=
let candidate := base.appendIndexAfter i
if env.contains candidate then
mkAuxNameAux env base (i+1)
else
candidate
let candidate := base.appendIndexAfter i
if env.contains candidate then
mkAuxNameAux env base (i+1)
else
candidate
def mkAuxName (baseName : Name) (idx : Nat) : m Name := do
return mkAuxNameAux (← getEnv) baseName idx
return mkAuxNameAux (← getEnv) baseName idx
variables [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m]
def getConstInfo (constName : Name) : m ConstantInfo := do
match (← getEnv).find? constName with
| some info => pure info
| none => throwError! "unknown constant '{mkConst constName}'"
match (← getEnv).find? constName with
| some info => pure info
| none => throwError! "unknown constant '{mkConst constName}'"
def getConstInfoInduct (constName : Name) : m InductiveVal := do
match (← getConstInfo constName) with
| ConstantInfo.inductInfo v => pure v
| _ => throwError! "'{mkConst constName}' is not a inductive type"
match (← getConstInfo constName) with
| ConstantInfo.inductInfo v => pure v
| _ => throwError! "'{mkConst constName}' is not a inductive type"
def getConstInfoCtor (constName : Name) : m ConstructorVal := do
match (← getConstInfo constName) with
| ConstantInfo.ctorInfo v => pure v
| _ => throwError! "'{mkConst constName}' is not a constructor"
match (← getConstInfo constName) with
| ConstantInfo.ctorInfo v => pure v
| _ => throwError! "'{mkConst constName}' is not a constructor"
def getConstInfoRec (constName : Name) : m RecursorVal := do
match (← getConstInfo constName) with
| ConstantInfo.recInfo v => pure v
| _ => throwError! "'{mkConst constName}' is not a recursor"
match (← getConstInfo constName) with
| ConstantInfo.recInfo v => pure v
| _ => throwError! "'{mkConst constName}' is not a recursor"
@[inline] def matchConstStruct {α : Type} (e : Expr) (failK : Unit → m α) (k : InductiveVal → List Level → ConstructorVal → m α) : m α :=
matchConstInduct e failK fun ival us => do
if ival.isRec then failK ()
else match ival.ctors with
| [ctor] =>
match (← getConstInfo ctor) with
| ConstantInfo.ctorInfo cval => k ival us cval
matchConstInduct e failK fun ival us => do
if ival.isRec then failK ()
else match ival.ctors with
| [ctor] =>
match (← getConstInfo ctor) with
| ConstantInfo.ctorInfo cval => k ival us cval
| _ => failK ()
| _ => failK ()
| _ => failK ()
def addDecl [MonadOptions m] (decl : Declaration) : m Unit := do
match (← getEnv).addDecl decl with
| Except.ok env => setEnv env
| Except.error ex => throwKernelException ex
match (← getEnv).addDecl decl with
| Except.ok env => setEnv env
| Except.error ex => throwKernelException ex
def compileDecl [MonadOptions m] (decl : Declaration) : m Unit := do
match (← getEnv).compileDecl (← getOptions) decl with
| Except.ok env => setEnv env
| Except.error ex => throwKernelException ex
match (← getEnv).compileDecl (← getOptions) decl with
| Except.ok env => setEnv env
| Except.error ex => throwKernelException ex
def addAndCompile [MonadOptions m] (decl : Declaration) : m Unit := do
addDecl decl;
compileDecl decl
addDecl decl;
compileDecl decl
variables [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m] [MonadOptions m]
unsafe def evalConst (α) (constName : Name) : m α := do
ofExcept $ (← getEnv).evalConst α (← getOptions) constName
ofExcept $ (← getEnv).evalConst α (← getOptions) constName
unsafe def evalConstCheck (α) (typeName : Name) (constName : Name) : m α := do
ofExcept $ (← getEnv).evalConstCheck α (← getOptions) typeName constName
ofExcept $ (← getEnv).evalConstCheck α (← getOptions) typeName constName
end

50
stage0/src/Lean/PrettyPrinter.lean generated
View file

@ -12,51 +12,51 @@ import Lean.Parser.Module
namespace Lean
def PPContext.runCoreM {α : Type} (ppCtx : PPContext) (x : CoreM α) : IO α :=
Prod.fst <$> x.toIO { options := ppCtx.opts } { env := ppCtx.env }
Prod.fst <$> x.toIO { options := ppCtx.opts } { env := ppCtx.env }
def PPContext.runMetaM {α : Type} (ppCtx : PPContext) (x : MetaM α) : IO α :=
ppCtx.runCoreM $ x.run' { lctx := ppCtx.lctx } { mctx := ppCtx.mctx }
ppCtx.runCoreM $ x.run' { lctx := ppCtx.lctx } { mctx := ppCtx.mctx }
namespace PrettyPrinter
def ppTerm (stx : Syntax) : CoreM Format := do
let opts ← getOptions
let stx := (sanitizeSyntax stx).run' { options := opts }
parenthesizeTerm stx >>= formatTerm
let opts ← getOptions
let stx := (sanitizeSyntax stx).run' { options := opts }
parenthesizeTerm stx >>= formatTerm
def ppExpr (currNamespace : Name) (openDecls : List OpenDecl) (e : Expr) : MetaM Format := do
let lctx ← getLCtx
let opts ← getOptions
let lctx := lctx.sanitizeNames.run' { options := opts }
Meta.withLCtx lctx #[] do
let stx ← delab currNamespace openDecls e
ppTerm stx
let lctx ← getLCtx
let opts ← getOptions
let lctx := lctx.sanitizeNames.run' { options := opts }
Meta.withLCtx lctx #[] do
let stx ← delab currNamespace openDecls e
ppTerm stx
@[export lean_pp_expr]
def ppExprLegacy (env : Environment) (mctx : MetavarContext) (lctx : LocalContext) (opts : Options) (e : Expr) : IO Format :=
Prod.fst <$> ((ppExpr Name.anonymous [] e).run' { lctx := lctx } { mctx := mctx }).toIO { options := opts } { env := env }
Prod.fst <$> ((ppExpr Name.anonymous [] e).run' { lctx := lctx } { mctx := mctx }).toIO { options := opts } { env := env }
def ppCommand (stx : Syntax) : CoreM Format :=
parenthesizeCommand stx >>= formatCommand
parenthesizeCommand stx >>= formatCommand
def ppModule (stx : Syntax) : CoreM Format := do
parenthesize Lean.Parser.Module.module.parenthesizer stx >>= format Lean.Parser.Module.module.formatter
parenthesize Lean.Parser.Module.module.parenthesizer stx >>= format Lean.Parser.Module.module.formatter
private partial def noContext : MessageData → MessageData
| MessageData.withContext ctx msg => noContext msg
| MessageData.withNamingContext ctx msg => MessageData.withNamingContext ctx (noContext msg)
| MessageData.nest n msg => MessageData.nest n (noContext msg)
| MessageData.group msg => MessageData.group (noContext msg)
| MessageData.compose msg₁ msg₂ => MessageData.compose (noContext msg₁) (noContext msg₂)
| MessageData.tagged tag msg => MessageData.tagged tag (noContext msg)
| MessageData.node msgs => MessageData.node (msgs.map noContext)
| msg => msg
| MessageData.withContext ctx msg => noContext msg
| MessageData.withNamingContext ctx msg => MessageData.withNamingContext ctx (noContext msg)
| MessageData.nest n msg => MessageData.nest n (noContext msg)
| MessageData.group msg => MessageData.group (noContext msg)
| MessageData.compose msg₁ msg₂ => MessageData.compose (noContext msg₁) (noContext msg₂)
| MessageData.tagged tag msg => MessageData.tagged tag (noContext msg)
| MessageData.node msgs => MessageData.node (msgs.map noContext)
| msg => msg
-- strip context (including environments with registered pretty printers) to prevent infinite recursion when pretty printing pretty printer error
private def withoutContext {m} [MonadExcept Exception m] (x : m Format) : m Format :=
tryCatch x fun
| Exception.error ref msg => throw $ Exception.error ref (noContext msg)
| ex => throw ex
tryCatch x fun
| Exception.error ref msg => throw $ Exception.error ref (noContext msg)
| ex => throw ex
builtin_initialize
ppFnsRef.set {

46
stage0/src/Lean/ProjFns.lean generated
View file

@ -11,19 +11,19 @@ namespace Lean
/- Given a structure `S`, Lean automatically creates an auxiliary definition (projection function)
for each field. This structure caches information about these auxiliary definitions. -/
structure ProjectionFunctionInfo :=
(ctorName : Name) -- Constructor associated with the auxiliary projection function.
(nparams : Nat) -- Number of parameters in the structure
(i : Nat) -- The field index associated with the auxiliary projection function.
(fromClass : Bool) -- `true` if the structure is a class
(ctorName : Name) -- Constructor associated with the auxiliary projection function.
(nparams : Nat) -- Number of parameters in the structure
(i : Nat) -- The field index associated with the auxiliary projection function.
(fromClass : Bool) -- `true` if the structure is a class
@[export lean_mk_projection_info]
def mkProjectionInfoEx (ctorName : Name) (nparams : Nat) (i : Nat) (fromClass : Bool) : ProjectionFunctionInfo :=
{ctorName := ctorName, nparams := nparams, i := i, fromClass := fromClass }
{ctorName := ctorName, nparams := nparams, i := i, fromClass := fromClass }
@[export lean_projection_info_from_class]
def ProjectionFunctionInfo.fromClassEx (info : ProjectionFunctionInfo) : Bool := info.fromClass
def ProjectionFunctionInfo.fromClassEx (info : ProjectionFunctionInfo) : Bool := info.fromClass
instance : Inhabited ProjectionFunctionInfo :=
⟨{ ctorName := arbitrary _, nparams := arbitrary _, i := 0, fromClass := false }⟩
⟨{ ctorName := arbitrary _, nparams := arbitrary _, i := 0, fromClass := false }⟩
builtin_initialize projectionFnInfoExt : SimplePersistentEnvExtension (Name × ProjectionFunctionInfo) (NameMap ProjectionFunctionInfo) ←
registerSimplePersistentEnvExtension {
@ -35,32 +35,32 @@ builtin_initialize projectionFnInfoExt : SimplePersistentEnvExtension (Name × P
@[export lean_add_projection_info]
def addProjectionFnInfo (env : Environment) (projName : Name) (ctorName : Name) (nparams : Nat) (i : Nat) (fromClass : Bool) : Environment :=
projectionFnInfoExt.addEntry env (projName, { ctorName := ctorName, nparams := nparams, i := i, fromClass := fromClass })
projectionFnInfoExt.addEntry env (projName, { ctorName := ctorName, nparams := nparams, i := i, fromClass := fromClass })
namespace Environment
@[export lean_get_projection_info]
def getProjectionFnInfo? (env : Environment) (projName : Name) : Option ProjectionFunctionInfo :=
match env.getModuleIdxFor? projName with
| some modIdx =>
match (projectionFnInfoExt.getModuleEntries env modIdx).binSearch (projName, arbitrary _) (fun a b => Name.quickLt a.1 b.1) with
| some e => some e.2
| none => none
| none => (projectionFnInfoExt.getState env).find? projName
match env.getModuleIdxFor? projName with
| some modIdx =>
match (projectionFnInfoExt.getModuleEntries env modIdx).binSearch (projName, arbitrary _) (fun a b => Name.quickLt a.1 b.1) with
| some e => some e.2
| none => none
| none => (projectionFnInfoExt.getState env).find? projName
def isProjectionFn (env : Environment) (n : Name) : Bool :=
match env.getModuleIdxFor? n with
| some modIdx => (projectionFnInfoExt.getModuleEntries env modIdx).binSearchContains (n, arbitrary _) (fun a b => Name.quickLt a.1 b.1)
| none => (projectionFnInfoExt.getState env).contains n
match env.getModuleIdxFor? n with
| some modIdx => (projectionFnInfoExt.getModuleEntries env modIdx).binSearchContains (n, arbitrary _) (fun a b => Name.quickLt a.1 b.1)
| none => (projectionFnInfoExt.getState env).contains n
/-- If `projName` is the name of a projection function, return the associated structure name -/
def getProjectionStructureName? (env : Environment) (projName : Name) : Option Name :=
match env.getProjectionFnInfo? projName with
| none => none
| some projInfo =>
match env.find? projInfo.ctorName with
| some (ConstantInfo.ctorInfo val) => some val.induct
| _ => none
match env.getProjectionFnInfo? projName with
| none => none
| some projInfo =>
match env.find? projInfo.ctorName with
| some (ConstantInfo.ctorInfo val) => some val.induct
| _ => none
end Environment
end Lean

20
stage0/src/Lean/ReducibilityAttrs.lean generated
View file

@ -9,7 +9,7 @@ import Lean.Attributes
namespace Lean
inductive ReducibilityStatus
| reducible | semireducible | irreducible
| reducible | semireducible | irreducible
instance : Inhabited ReducibilityStatus := ⟨ReducibilityStatus.semireducible⟩
@ -21,19 +21,19 @@ builtin_initialize reducibilityAttrs : EnumAttributes ReducibilityStatus ←
@[export lean_get_reducibility_status]
def getReducibilityStatus (env : Environment) (n : Name) : ReducibilityStatus :=
match reducibilityAttrs.getValue env n with
| some s => s
| none => ReducibilityStatus.semireducible
match reducibilityAttrs.getValue env n with
| some s => s
| none => ReducibilityStatus.semireducible
@[export lean_set_reducibility_status]
def setReducibilityStatus (env : Environment) (n : Name) (s : ReducibilityStatus) : Environment :=
match reducibilityAttrs.setValue env n s with
| Except.ok env => env
| _ => env -- TODO(Leo): we should extend EnumAttributes.setValue in the future and ensure it never fails
match reducibilityAttrs.setValue env n s with
| Except.ok env => env
| _ => env -- TODO(Leo): we should extend EnumAttributes.setValue in the future and ensure it never fails
def isReducible (env : Environment) (n : Name) : Bool :=
match getReducibilityStatus env n with
| ReducibilityStatus.reducible => true
| _ => false
match getReducibilityStatus env n with
| ReducibilityStatus.reducible => true
| _ => false
end Lean

185
stage0/src/Lean/ResolveName.lean generated
View file

@ -18,9 +18,9 @@ abbrev AliasState := SMap Name (List Name)
abbrev AliasEntry := Name × Name
def addAliasEntry (s : AliasState) (e : AliasEntry) : AliasState :=
match s.find? e.1 with
| none => s.insert e.1 [e.2]
| some es => if es.elem e.2 then s else s.insert e.1 (e.2 :: es)
match s.find? e.1 with
| none => s.insert e.1 [e.2]
| some es => if es.elem e.2 then s else s.insert e.1 (e.2 :: es)
builtin_initialize aliasExtension : SimplePersistentEnvExtension AliasEntry AliasState ←
registerSimplePersistentEnvExtension {
@ -31,101 +31,101 @@ builtin_initialize aliasExtension : SimplePersistentEnvExtension AliasEntry Alia
/- Add alias `a` for `e` -/
@[export lean_add_alias] def addAlias (env : Environment) (a : Name) (e : Name) : Environment :=
aliasExtension.addEntry env (a, e)
aliasExtension.addEntry env (a, e)
def getAliases (env : Environment) (a : Name) : List Name :=
match aliasExtension.getState env $.find? a with
| none => []
| some es => es
match aliasExtension.getState env $.find? a with
| none => []
| some es => es
-- slower, but only used in the pretty printer
def getRevAliases (env : Environment) (e : Name) : List Name :=
(aliasExtension.getState env).fold (fun as a es => if List.contains es e then a :: as else as) []
(aliasExtension.getState env).fold (fun as a es => if List.contains es e then a :: as else as) []
/- Global name resolution -/
namespace ResolveName
/- Check whether `ns ++ id` is a valid namepace name and/or there are aliases names `ns ++ id`. -/
private def resolveQualifiedName (env : Environment) (ns : Name) (id : Name) : List Name :=
let resolvedId := ns ++ id
let resolvedIds := getAliases env resolvedId
if env.contains resolvedId && (!id.isAtomic || !isProtected env resolvedId) then
resolvedId :: resolvedIds
else
-- Check whether environment contains the private version. That is, `_private.<module_name>.ns.id`.
let resolvedIdPrv := mkPrivateName env resolvedId
if env.contains resolvedIdPrv then resolvedIdPrv :: resolvedIds
else resolvedIds
let resolvedId := ns ++ id
let resolvedIds := getAliases env resolvedId
if env.contains resolvedId && (!id.isAtomic || !isProtected env resolvedId) then
resolvedId :: resolvedIds
else
-- Check whether environment contains the private version. That is, `_private.<module_name>.ns.id`.
let resolvedIdPrv := mkPrivateName env resolvedId
if env.contains resolvedIdPrv then resolvedIdPrv :: resolvedIds
else resolvedIds
/- Check surrounding namespaces -/
private def resolveUsingNamespace (env : Environment) (id : Name) : Name → List Name
| ns@(Name.str p _ _) =>
match resolveQualifiedName env ns id with
| [] => resolveUsingNamespace env id p
| resolvedIds => resolvedIds
| _ => []
| ns@(Name.str p _ _) =>
match resolveQualifiedName env ns id with
| [] => resolveUsingNamespace env id p
| resolvedIds => resolvedIds
| _ => []
/- Check exact name -/
private def resolveExact (env : Environment) (id : Name) : Option Name :=
if id.isAtomic then none
else
let resolvedId := id.replacePrefix rootNamespace Name.anonymous
if env.contains resolvedId then some resolvedId
if id.isAtomic then none
else
-- We also allow `_root` when accessing private declarations.
-- If we change our minds, we should just replace `resolvedId` with `id`
let resolvedIdPrv := mkPrivateName env resolvedId
if env.contains resolvedIdPrv then some resolvedIdPrv
else none
let resolvedId := id.replacePrefix rootNamespace Name.anonymous
if env.contains resolvedId then some resolvedId
else
-- We also allow `_root` when accessing private declarations.
-- If we change our minds, we should just replace `resolvedId` with `id`
let resolvedIdPrv := mkPrivateName env resolvedId
if env.contains resolvedIdPrv then some resolvedIdPrv
else none
/- Check open namespaces -/
private def resolveOpenDecls (env : Environment) (id : Name) : List OpenDecl → List Name → List Name
| [], resolvedIds => resolvedIds
| OpenDecl.simple ns exs :: openDecls, resolvedIds =>
if exs.elem id then
| [], resolvedIds => resolvedIds
| OpenDecl.simple ns exs :: openDecls, resolvedIds =>
if exs.elem id then
resolveOpenDecls env id openDecls resolvedIds
else
let newResolvedIds := resolveQualifiedName env ns id
resolveOpenDecls env id openDecls (newResolvedIds ++ resolvedIds)
| OpenDecl.explicit openedId resolvedId :: openDecls, resolvedIds =>
let resolvedIds := if id == openedId then resolvedId :: resolvedIds else resolvedIds
resolveOpenDecls env id openDecls resolvedIds
else
let newResolvedIds := resolveQualifiedName env ns id
resolveOpenDecls env id openDecls (newResolvedIds ++ resolvedIds)
| OpenDecl.explicit openedId resolvedId :: openDecls, resolvedIds =>
let resolvedIds := if id == openedId then resolvedId :: resolvedIds else resolvedIds
resolveOpenDecls env id openDecls resolvedIds
def resolveGlobalName (env : Environment) (ns : Name) (openDecls : List OpenDecl) (id : Name) : List (Name × List String) :=
-- decode macro scopes from name before recursion
let extractionResult := extractMacroScopes id
let rec loop : Name → List String → List (Name × List String)
| id@(Name.str p s _), projs =>
-- NOTE: we assume that macro scopes always belong to the projected constant, not the projections
let id := { extractionResult with name := id }.review
match resolveUsingNamespace env id ns with
| resolvedIds@(_ :: _) => resolvedIds.eraseDups.map fun id => (id, projs)
| [] =>
match resolveExact env id with
| some newId => [(newId, projs)]
| none =>
let resolvedIds := if env.contains id then [id] else []
let idPrv := mkPrivateName env id
let resolvedIds := if env.contains idPrv then [idPrv] ++ resolvedIds else resolvedIds
let resolvedIds := resolveOpenDecls env id openDecls resolvedIds
let resolvedIds := getAliases env id ++ resolvedIds
match resolvedIds with
| _ :: _ => resolvedIds.eraseDups.map fun id => (id, projs)
| [] => loop p (s::projs)
| _, _ => []
loop extractionResult.name []
-- decode macro scopes from name before recursion
let extractionResult := extractMacroScopes id
let rec loop : Name → List String → List (Name × List String)
| id@(Name.str p s _), projs =>
-- NOTE: we assume that macro scopes always belong to the projected constant, not the projections
let id := { extractionResult with name := id }.review
match resolveUsingNamespace env id ns with
| resolvedIds@(_ :: _) => resolvedIds.eraseDups.map fun id => (id, projs)
| [] =>
match resolveExact env id with
| some newId => [(newId, projs)]
| none =>
let resolvedIds := if env.contains id then [id] else []
let idPrv := mkPrivateName env id
let resolvedIds := if env.contains idPrv then [idPrv] ++ resolvedIds else resolvedIds
let resolvedIds := resolveOpenDecls env id openDecls resolvedIds
let resolvedIds := getAliases env id ++ resolvedIds
match resolvedIds with
| _ :: _ => resolvedIds.eraseDups.map fun id => (id, projs)
| [] => loop p (s::projs)
| _, _ => []
loop extractionResult.name []
/- Namespace resolution -/
def resolveNamespaceUsingScope (env : Environment) (n : Name) : Name → Option Name
| Name.anonymous => none
| ns@(Name.str p _ _) => if env.isNamespace (ns ++ n) then some (ns ++ n) else resolveNamespaceUsingScope env n p
| _ => unreachable!
| Name.anonymous => none
| ns@(Name.str p _ _) => if env.isNamespace (ns ++ n) then some (ns ++ n) else resolveNamespaceUsingScope env n p
| _ => unreachable!
def resolveNamespaceUsingOpenDecls (env : Environment) (n : Name) : List OpenDecl → Option Name
| [] => none
| OpenDecl.simple ns [] :: ds => if env.isNamespace (ns ++ n) then some (ns ++ n) else resolveNamespaceUsingOpenDecls env n ds
| _ :: ds => resolveNamespaceUsingOpenDecls env n ds
| [] => none
| OpenDecl.simple ns [] :: ds => if env.isNamespace (ns ++ n) then some (ns ++ n) else resolveNamespaceUsingOpenDecls env n ds
| _ :: ds => resolveNamespaceUsingOpenDecls env n ds
/-
Given a name `id` try to find namespace it refers to. The resolution procedure works as follows
@ -136,24 +136,25 @@ Given a name `id` try to find namespace it refers to. The resolution procedure w
We search "backwards" again. That is, we try the most recent `open` command first.
We only consider simple `open` commands. -/
def resolveNamespace? (env : Environment) (ns : Name) (openDecls : List OpenDecl) (id : Name) : Option Name :=
if env.isNamespace id then some id
else match resolveNamespaceUsingScope env id ns with
| some n => some n
| none =>
match resolveNamespaceUsingOpenDecls env id openDecls with
if env.isNamespace id then some id
else match resolveNamespaceUsingScope env id ns with
| some n => some n
| none => none
end ResolveName
| none =>
match resolveNamespaceUsingOpenDecls env id openDecls with
| some n => some n
| none => none
end ResolveName
class MonadResolveName (m : Type → Type) :=
(getCurrNamespace : m Name)
(getOpenDecls : m (List OpenDecl))
(getCurrNamespace : m Name)
(getOpenDecls : m (List OpenDecl))
export MonadResolveName (getCurrNamespace getOpenDecls)
instance (m n) [MonadResolveName m] [MonadLift m n] : MonadResolveName n :=
{ getCurrNamespace := liftM (getCurrNamespace : m _),
getOpenDecls := liftM (getOpenDecls : m _) }
instance (m n) [MonadResolveName m] [MonadLift m n] : MonadResolveName n := {
getCurrNamespace := liftM (getCurrNamespace : m _),
getOpenDecls := liftM (getOpenDecls : m _)
}
section Methods
@ -182,27 +183,27 @@ variables {m : Type → Type} [Monad m] [MonadResolveName m] [MonadEnv m]
- `resolveGlobalName x.z.w` => `[(Foo.x, [z, w]), (Boo.x, [z, w])]`
-/
def resolveGlobalName (id : Name) : m (List (Name × List String)) := do
return ResolveName.resolveGlobalName (← getEnv) (← getCurrNamespace) (← getOpenDecls) id
return ResolveName.resolveGlobalName (← getEnv) (← getCurrNamespace) (← getOpenDecls) id
variables [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m]
def resolveNamespace (id : Name) : m Name := do
match ResolveName.resolveNamespace? (← getEnv) (← getCurrNamespace) (← getOpenDecls) id with
| some ns => return ns
| none => throwError s!"unknown namespace '{id}'"
match ResolveName.resolveNamespace? (← getEnv) (← getCurrNamespace) (← getOpenDecls) id with
| some ns => return ns
| none => throwError s!"unknown namespace '{id}'"
/- Similar to `resolveGlobalName`, but discard any candidate whose `fieldList` is not empty. -/
def resolveGlobalConst (n : Name) : m (List Name) := do
let cs ← resolveGlobalName n
let cs := cs.filter fun (_, fieldList) => fieldList.isEmpty
if cs.isEmpty then throwUnknownConstant n
return cs.map (·.1)
let cs ← resolveGlobalName n
let cs := cs.filter fun (_, fieldList) => fieldList.isEmpty
if cs.isEmpty then throwUnknownConstant n
return cs.map (·.1)
def resolveGlobalConstNoOverload (n : Name) : m Name := do
let cs ← resolveGlobalConst n
match cs with
| [c] => pure c
| _ => throwError s!"ambiguous identifier '{mkConst n}', possible interpretations: {cs.map mkConst}"
let cs ← resolveGlobalConst n
match cs with
| [c] => pure c
| _ => throwError s!"ambiguous identifier '{mkConst n}', possible interpretations: {cs.map mkConst}"
end Methods
end Lean

508
stage0/stdlib/Lean/Elab/PreDefinition/Basic.c generated
View file

@ -82,6 +82,7 @@ uint8_t l_Lean_Elab_DefKind_isTheorem(uint8_t);
lean_object* l___private_Lean_Elab_PreDefinition_Basic_0__Lean_Elab_addNonRecAux_match__1___rarg(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_PreDefinition_Basic_0__Lean_Elab_addNonRecAux___closed__3;
lean_object* l_Lean_Elab_addAndCompileUnsafeRec___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_PreDefinition_Basic_0__Lean_Elab_addNonRecAux___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_PreDefinition_Basic_0__Lean_Elab_levelMVarToParamExpr(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_fixLevelParams_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_umapMAux___at___private_Lean_Elab_PreDefinition_Basic_0__Lean_Elab_shareCommon___spec__2(lean_object*, lean_object*, lean_object*);
@ -104,6 +105,7 @@ uint8_t l_Array_anyRangeMAux___at_Lean_Elab_fixLevelParams___spec__1(lean_object
lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Basic_0__Lean_Elab_getLevelParamsPreDecls___spec__1___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* l_Lean_Elab_instantiateMVarsAtPreDecls(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_anyRangeMAux___at_Lean_Elab_addAndCompileUnsafeRec___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_PreDefinition_Basic_0__Lean_Elab_addNonRecAux___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Expr_Lean_Expr___instance__11___closed__1;
lean_object* l___private_Lean_Elab_PreDefinition_Basic_0__Lean_Elab_levelMVarToParamExpr_match__1___rarg(lean_object*, lean_object*);
extern lean_object* l_Lean_mkOptionalNode___closed__2;
@ -1875,6 +1877,62 @@ x_8 = l___private_Lean_Elab_PreDefinition_Basic_0__Lean_Elab_addNonRecAux_match_
return x_8;
}
}
lean_object* l___private_Lean_Elab_PreDefinition_Basic_0__Lean_Elab_addNonRecAux___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
_start:
{
uint8_t x_10; lean_object* x_11;
x_10 = 1;
x_11 = l_Lean_Elab_applyAttributesOf(x_1, x_10, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
if (lean_obj_tag(x_11) == 0)
{
uint8_t x_12;
x_12 = !lean_is_exclusive(x_11);
if (x_12 == 0)
{
lean_object* x_13; lean_object* x_14;
x_13 = lean_ctor_get(x_11, 0);
lean_dec(x_13);
x_14 = lean_box(0);
lean_ctor_set(x_11, 0, x_14);
return x_11;
}
else
{
lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_15 = lean_ctor_get(x_11, 1);
lean_inc(x_15);
lean_dec(x_11);
x_16 = lean_box(0);
x_17 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_17, 0, x_16);
lean_ctor_set(x_17, 1, x_15);
return x_17;
}
}
else
{
uint8_t x_18;
x_18 = !lean_is_exclusive(x_11);
if (x_18 == 0)
{
return x_11;
}
else
{
lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_19 = lean_ctor_get(x_11, 0);
x_20 = lean_ctor_get(x_11, 1);
lean_inc(x_20);
lean_inc(x_19);
lean_dec(x_11);
x_21 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_21, 0, x_19);
lean_ctor_set(x_21, 1, x_20);
return x_21;
}
}
}
}
static lean_object* _init_l___private_Lean_Elab_PreDefinition_Basic_0__Lean_Elab_addNonRecAux___closed__1() {
_start:
{
@ -1898,7 +1956,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj
x_1 = l___private_Lean_Elab_PreDefinition_Basic_0__Lean_Elab_addNonRecAux___closed__1;
x_2 = l___private_Lean_Elab_PreDefinition_Basic_0__Lean_Elab_addNonRecAux___closed__2;
x_3 = lean_unsigned_to_nat(98u);
x_4 = lean_unsigned_to_nat(25u);
x_4 = lean_unsigned_to_nat(27u);
x_5 = l___private_Init_LeanInit_0__Lean_eraseMacroScopesAux___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
return x_6;
@ -1944,105 +2002,105 @@ lean_inc(x_22);
switch (x_17) {
case 0:
{
lean_object* x_84; lean_object* x_85; uint32_t x_86; uint32_t x_87; uint32_t x_88; lean_object* x_89; uint8_t x_90; lean_object* x_91; lean_object* x_92;
x_84 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_84, 0, x_20);
lean_ctor_set(x_84, 1, x_18);
lean_ctor_set(x_84, 2, x_21);
lean_object* x_54; lean_object* x_55; uint32_t x_56; uint32_t x_57; uint32_t x_58; lean_object* x_59; uint8_t x_60; lean_object* x_61; lean_object* x_62;
x_54 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_54, 0, x_20);
lean_ctor_set(x_54, 1, x_18);
lean_ctor_set(x_54, 2, x_21);
lean_inc(x_22);
x_85 = l_Lean_getMaxHeight(x_16, x_22);
x_86 = lean_unbox_uint32(x_85);
lean_dec(x_85);
x_87 = 1;
x_88 = x_86 + x_87;
x_89 = lean_alloc_ctor(2, 0, 4);
lean_ctor_set_uint32(x_89, 0, x_88);
x_90 = lean_ctor_get_uint8(x_19, sizeof(void*)*2 + 3);
x_55 = l_Lean_getMaxHeight(x_16, x_22);
x_56 = lean_unbox_uint32(x_55);
lean_dec(x_55);
x_57 = 1;
x_58 = x_56 + x_57;
x_59 = lean_alloc_ctor(2, 0, 4);
lean_ctor_set_uint32(x_59, 0, x_58);
x_60 = lean_ctor_get_uint8(x_19, sizeof(void*)*2 + 3);
lean_dec(x_19);
x_91 = lean_alloc_ctor(0, 3, 1);
lean_ctor_set(x_91, 0, x_84);
lean_ctor_set(x_91, 1, x_22);
lean_ctor_set(x_91, 2, x_89);
lean_ctor_set_uint8(x_91, sizeof(void*)*3, x_90);
x_92 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_92, 0, x_91);
x_23 = x_92;
goto block_83;
x_61 = lean_alloc_ctor(0, 3, 1);
lean_ctor_set(x_61, 0, x_54);
lean_ctor_set(x_61, 1, x_22);
lean_ctor_set(x_61, 2, x_59);
lean_ctor_set_uint8(x_61, sizeof(void*)*3, x_60);
x_62 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_62, 0, x_61);
x_23 = x_62;
goto block_53;
}
case 1:
{
lean_object* x_93; lean_object* x_94; lean_object* x_95;
lean_object* x_63; lean_object* x_64; lean_object* x_65;
lean_dec(x_19);
lean_dec(x_16);
x_93 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_93, 0, x_20);
lean_ctor_set(x_93, 1, x_18);
lean_ctor_set(x_93, 2, x_21);
x_94 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_94, 0, x_93);
lean_ctor_set(x_94, 1, x_22);
x_95 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_95, 0, x_94);
x_23 = x_95;
goto block_83;
x_63 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_63, 0, x_20);
lean_ctor_set(x_63, 1, x_18);
lean_ctor_set(x_63, 2, x_21);
x_64 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_64, 0, x_63);
lean_ctor_set(x_64, 1, x_22);
x_65 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_65, 0, x_64);
x_23 = x_65;
goto block_53;
}
case 2:
{
lean_object* x_96; lean_object* x_97; lean_object* x_98;
lean_object* x_66; lean_object* x_67; lean_object* x_68;
lean_dec(x_22);
lean_dec(x_21);
lean_dec(x_20);
lean_dec(x_19);
lean_dec(x_18);
lean_dec(x_16);
x_96 = l_Lean_Lean_Declaration___instance__3;
x_97 = l___private_Lean_Elab_PreDefinition_Basic_0__Lean_Elab_addNonRecAux___closed__3;
x_98 = lean_panic_fn(x_96, x_97);
x_23 = x_98;
goto block_83;
x_66 = l_Lean_Lean_Declaration___instance__3;
x_67 = l___private_Lean_Elab_PreDefinition_Basic_0__Lean_Elab_addNonRecAux___closed__3;
x_68 = lean_panic_fn(x_66, x_67);
x_23 = x_68;
goto block_53;
}
case 3:
{
lean_object* x_99; uint8_t x_100; lean_object* x_101; lean_object* x_102;
lean_object* x_69; uint8_t x_70; lean_object* x_71; lean_object* x_72;
lean_dec(x_16);
x_99 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_99, 0, x_20);
lean_ctor_set(x_99, 1, x_18);
lean_ctor_set(x_99, 2, x_21);
x_100 = lean_ctor_get_uint8(x_19, sizeof(void*)*2 + 3);
x_69 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_69, 0, x_20);
lean_ctor_set(x_69, 1, x_18);
lean_ctor_set(x_69, 2, x_21);
x_70 = lean_ctor_get_uint8(x_19, sizeof(void*)*2 + 3);
lean_dec(x_19);
x_101 = lean_alloc_ctor(0, 2, 1);
lean_ctor_set(x_101, 0, x_99);
lean_ctor_set(x_101, 1, x_22);
lean_ctor_set_uint8(x_101, sizeof(void*)*2, x_100);
x_102 = lean_alloc_ctor(3, 1, 0);
lean_ctor_set(x_102, 0, x_101);
x_23 = x_102;
goto block_83;
x_71 = lean_alloc_ctor(0, 2, 1);
lean_ctor_set(x_71, 0, x_69);
lean_ctor_set(x_71, 1, x_22);
lean_ctor_set_uint8(x_71, sizeof(void*)*2, x_70);
x_72 = lean_alloc_ctor(3, 1, 0);
lean_ctor_set(x_72, 0, x_71);
x_23 = x_72;
goto block_53;
}
default:
{
lean_object* x_103; uint8_t x_104; lean_object* x_105; lean_object* x_106; lean_object* x_107;
lean_object* x_73; uint8_t x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77;
lean_dec(x_16);
x_103 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_103, 0, x_20);
lean_ctor_set(x_103, 1, x_18);
lean_ctor_set(x_103, 2, x_21);
x_104 = lean_ctor_get_uint8(x_19, sizeof(void*)*2 + 3);
x_73 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_73, 0, x_20);
lean_ctor_set(x_73, 1, x_18);
lean_ctor_set(x_73, 2, x_21);
x_74 = lean_ctor_get_uint8(x_19, sizeof(void*)*2 + 3);
lean_dec(x_19);
x_105 = lean_box(1);
x_106 = lean_alloc_ctor(0, 3, 1);
lean_ctor_set(x_106, 0, x_103);
lean_ctor_set(x_106, 1, x_22);
lean_ctor_set(x_106, 2, x_105);
lean_ctor_set_uint8(x_106, sizeof(void*)*3, x_104);
x_107 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_107, 0, x_106);
x_23 = x_107;
goto block_83;
x_75 = lean_box(1);
x_76 = lean_alloc_ctor(0, 3, 1);
lean_ctor_set(x_76, 0, x_73);
lean_ctor_set(x_76, 1, x_22);
lean_ctor_set(x_76, 2, x_75);
lean_ctor_set_uint8(x_76, sizeof(void*)*3, x_74);
x_77 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_77, 0, x_76);
x_23 = x_77;
goto block_53;
}
}
block_83:
block_53:
{
lean_object* x_24;
lean_inc(x_7);
@ -2065,58 +2123,69 @@ if (lean_obj_tag(x_29) == 0)
{
if (x_2 == 0)
{
lean_object* x_30; uint8_t x_31; lean_object* x_32;
lean_object* x_30; lean_object* x_31; lean_object* x_32;
lean_dec(x_23);
x_30 = lean_ctor_get(x_29, 1);
lean_inc(x_30);
lean_dec(x_29);
x_31 = 1;
x_32 = l_Lean_Elab_applyAttributesOf(x_27, x_31, x_3, x_4, x_5, x_6, x_7, x_8, x_30);
x_31 = lean_box(0);
x_32 = l___private_Lean_Elab_PreDefinition_Basic_0__Lean_Elab_addNonRecAux___lambda__1(x_27, x_31, x_3, x_4, x_5, x_6, x_7, x_8, x_30);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_27);
if (lean_obj_tag(x_32) == 0)
{
uint8_t x_33;
x_33 = !lean_is_exclusive(x_32);
if (x_33 == 0)
{
lean_object* x_34; lean_object* x_35;
x_34 = lean_ctor_get(x_32, 0);
lean_dec(x_34);
x_35 = lean_box(0);
lean_ctor_set(x_32, 0, x_35);
return x_32;
}
else
{
lean_object* x_33; uint8_t x_34;
x_33 = lean_ctor_get(x_29, 1);
lean_inc(x_33);
lean_dec(x_29);
x_34 = l_Lean_Elab_DefKind_isTheorem(x_17);
if (x_34 == 0)
{
lean_object* x_35;
lean_inc(x_7);
lean_inc(x_3);
x_35 = l_Lean_compileDecl___at_Lean_Elab_Term_declareTacticSyntax___spec__4(x_23, x_3, x_4, x_5, x_6, x_7, x_8, x_33);
lean_dec(x_23);
if (lean_obj_tag(x_35) == 0)
{
lean_object* x_36; lean_object* x_37; lean_object* x_38;
x_36 = lean_ctor_get(x_32, 1);
x_36 = lean_ctor_get(x_35, 0);
lean_inc(x_36);
lean_dec(x_32);
x_37 = lean_box(0);
x_38 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_38, 0, x_37);
lean_ctor_set(x_38, 1, x_36);
x_37 = lean_ctor_get(x_35, 1);
lean_inc(x_37);
lean_dec(x_35);
x_38 = l___private_Lean_Elab_PreDefinition_Basic_0__Lean_Elab_addNonRecAux___lambda__1(x_27, x_36, x_3, x_4, x_5, x_6, x_7, x_8, x_37);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_36);
lean_dec(x_27);
return x_38;
}
}
else
{
uint8_t x_39;
x_39 = !lean_is_exclusive(x_32);
lean_dec(x_27);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_3);
x_39 = !lean_is_exclusive(x_35);
if (x_39 == 0)
{
return x_32;
return x_35;
}
else
{
lean_object* x_40; lean_object* x_41; lean_object* x_42;
x_40 = lean_ctor_get(x_32, 0);
x_41 = lean_ctor_get(x_32, 1);
x_40 = lean_ctor_get(x_35, 0);
x_41 = lean_ctor_get(x_35, 1);
lean_inc(x_41);
lean_inc(x_40);
lean_dec(x_32);
lean_dec(x_35);
x_42 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_42, 0, x_40);
lean_ctor_set(x_42, 1, x_41);
@ -2126,170 +2195,20 @@ return x_42;
}
else
{
lean_object* x_43; uint8_t x_44;
x_43 = lean_ctor_get(x_29, 1);
lean_inc(x_43);
lean_dec(x_29);
x_44 = l_Lean_Elab_DefKind_isTheorem(x_17);
if (x_44 == 0)
{
lean_object* x_45;
lean_inc(x_7);
lean_inc(x_3);
x_45 = l_Lean_compileDecl___at_Lean_Elab_Term_declareTacticSyntax___spec__4(x_23, x_3, x_4, x_5, x_6, x_7, x_8, x_43);
lean_object* x_43; lean_object* x_44;
lean_dec(x_23);
if (lean_obj_tag(x_45) == 0)
{
lean_object* x_46; uint8_t x_47; lean_object* x_48;
x_46 = lean_ctor_get(x_45, 1);
lean_inc(x_46);
lean_dec(x_45);
x_47 = 1;
x_48 = l_Lean_Elab_applyAttributesOf(x_27, x_47, x_3, x_4, x_5, x_6, x_7, x_8, x_46);
x_43 = lean_box(0);
x_44 = l___private_Lean_Elab_PreDefinition_Basic_0__Lean_Elab_addNonRecAux___lambda__1(x_27, x_43, x_3, x_4, x_5, x_6, x_7, x_8, x_33);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_27);
if (lean_obj_tag(x_48) == 0)
{
uint8_t x_49;
x_49 = !lean_is_exclusive(x_48);
if (x_49 == 0)
{
lean_object* x_50; lean_object* x_51;
x_50 = lean_ctor_get(x_48, 0);
lean_dec(x_50);
x_51 = lean_box(0);
lean_ctor_set(x_48, 0, x_51);
return x_48;
}
else
{
lean_object* x_52; lean_object* x_53; lean_object* x_54;
x_52 = lean_ctor_get(x_48, 1);
lean_inc(x_52);
lean_dec(x_48);
x_53 = lean_box(0);
x_54 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_54, 0, x_53);
lean_ctor_set(x_54, 1, x_52);
return x_54;
}
}
else
{
uint8_t x_55;
x_55 = !lean_is_exclusive(x_48);
if (x_55 == 0)
{
return x_48;
}
else
{
lean_object* x_56; lean_object* x_57; lean_object* x_58;
x_56 = lean_ctor_get(x_48, 0);
x_57 = lean_ctor_get(x_48, 1);
lean_inc(x_57);
lean_inc(x_56);
lean_dec(x_48);
x_58 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_58, 0, x_56);
lean_ctor_set(x_58, 1, x_57);
return x_58;
return x_44;
}
}
}
else
{
uint8_t x_59;
lean_dec(x_27);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_3);
x_59 = !lean_is_exclusive(x_45);
if (x_59 == 0)
{
return x_45;
}
else
{
lean_object* x_60; lean_object* x_61; lean_object* x_62;
x_60 = lean_ctor_get(x_45, 0);
x_61 = lean_ctor_get(x_45, 1);
lean_inc(x_61);
lean_inc(x_60);
lean_dec(x_45);
x_62 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_62, 0, x_60);
lean_ctor_set(x_62, 1, x_61);
return x_62;
}
}
}
else
{
uint8_t x_63; lean_object* x_64;
lean_dec(x_23);
x_63 = 1;
x_64 = l_Lean_Elab_applyAttributesOf(x_27, x_63, x_3, x_4, x_5, x_6, x_7, x_8, x_43);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_27);
if (lean_obj_tag(x_64) == 0)
{
uint8_t x_65;
x_65 = !lean_is_exclusive(x_64);
if (x_65 == 0)
{
lean_object* x_66; lean_object* x_67;
x_66 = lean_ctor_get(x_64, 0);
lean_dec(x_66);
x_67 = lean_box(0);
lean_ctor_set(x_64, 0, x_67);
return x_64;
}
else
{
lean_object* x_68; lean_object* x_69; lean_object* x_70;
x_68 = lean_ctor_get(x_64, 1);
lean_inc(x_68);
lean_dec(x_64);
x_69 = lean_box(0);
x_70 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_70, 0, x_69);
lean_ctor_set(x_70, 1, x_68);
return x_70;
}
}
else
{
uint8_t x_71;
x_71 = !lean_is_exclusive(x_64);
if (x_71 == 0)
{
return x_64;
}
else
{
lean_object* x_72; lean_object* x_73; lean_object* x_74;
x_72 = lean_ctor_get(x_64, 0);
x_73 = lean_ctor_get(x_64, 1);
lean_inc(x_73);
lean_inc(x_72);
lean_dec(x_64);
x_74 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_74, 0, x_72);
lean_ctor_set(x_74, 1, x_73);
return x_74;
}
}
}
}
}
else
{
uint8_t x_75;
uint8_t x_45;
lean_dec(x_27);
lean_dec(x_23);
lean_dec(x_8);
@ -2297,29 +2216,29 @@ lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_3);
x_75 = !lean_is_exclusive(x_29);
if (x_75 == 0)
x_45 = !lean_is_exclusive(x_29);
if (x_45 == 0)
{
return x_29;
}
else
{
lean_object* x_76; lean_object* x_77; lean_object* x_78;
x_76 = lean_ctor_get(x_29, 0);
x_77 = lean_ctor_get(x_29, 1);
lean_inc(x_77);
lean_inc(x_76);
lean_object* x_46; lean_object* x_47; lean_object* x_48;
x_46 = lean_ctor_get(x_29, 0);
x_47 = lean_ctor_get(x_29, 1);
lean_inc(x_47);
lean_inc(x_46);
lean_dec(x_29);
x_78 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_78, 0, x_76);
lean_ctor_set(x_78, 1, x_77);
return x_78;
x_48 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_48, 0, x_46);
lean_ctor_set(x_48, 1, x_47);
return x_48;
}
}
}
else
{
uint8_t x_79;
uint8_t x_49;
lean_dec(x_23);
lean_dec(x_11);
lean_dec(x_8);
@ -2327,56 +2246,69 @@ lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_3);
x_79 = !lean_is_exclusive(x_24);
if (x_79 == 0)
x_49 = !lean_is_exclusive(x_24);
if (x_49 == 0)
{
return x_24;
}
else
{
lean_object* x_80; lean_object* x_81; lean_object* x_82;
x_80 = lean_ctor_get(x_24, 0);
x_81 = lean_ctor_get(x_24, 1);
lean_inc(x_81);
lean_inc(x_80);
lean_object* x_50; lean_object* x_51; lean_object* x_52;
x_50 = lean_ctor_get(x_24, 0);
x_51 = lean_ctor_get(x_24, 1);
lean_inc(x_51);
lean_inc(x_50);
lean_dec(x_24);
x_82 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_82, 0, x_80);
lean_ctor_set(x_82, 1, x_81);
return x_82;
x_52 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_52, 0, x_50);
lean_ctor_set(x_52, 1, x_51);
return x_52;
}
}
}
}
else
{
uint8_t x_108;
uint8_t x_78;
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_3);
x_108 = !lean_is_exclusive(x_10);
if (x_108 == 0)
x_78 = !lean_is_exclusive(x_10);
if (x_78 == 0)
{
return x_10;
}
else
{
lean_object* x_109; lean_object* x_110; lean_object* x_111;
x_109 = lean_ctor_get(x_10, 0);
x_110 = lean_ctor_get(x_10, 1);
lean_inc(x_110);
lean_inc(x_109);
lean_object* x_79; lean_object* x_80; lean_object* x_81;
x_79 = lean_ctor_get(x_10, 0);
x_80 = lean_ctor_get(x_10, 1);
lean_inc(x_80);
lean_inc(x_79);
lean_dec(x_10);
x_111 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_111, 0, x_109);
lean_ctor_set(x_111, 1, x_110);
return x_111;
x_81 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_81, 0, x_79);
lean_ctor_set(x_81, 1, x_80);
return x_81;
}
}
}
}
lean_object* l___private_Lean_Elab_PreDefinition_Basic_0__Lean_Elab_addNonRecAux___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
_start:
{
lean_object* x_10;
x_10 = l___private_Lean_Elab_PreDefinition_Basic_0__Lean_Elab_addNonRecAux___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
return x_10;
}
}
lean_object* l___private_Lean_Elab_PreDefinition_Basic_0__Lean_Elab_addNonRecAux___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
_start:
{

1779
stage0/stdlib/Lean/Elab/PreDefinition/Structural.c generated
View file

File diff suppressed because it is too large Load diff

76
stage0/stdlib/Lean/Expr.c generated
View file

@ -2159,7 +2159,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__1;
x_2 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2;
x_3 = lean_unsigned_to_nat(143u);
x_4 = lean_unsigned_to_nat(42u);
x_4 = lean_unsigned_to_nat(44u);
x_5 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
return x_6;
@ -8021,7 +8021,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__1;
x_2 = l_Lean_Expr_getRevArg_x21___closed__1;
x_3 = lean_unsigned_to_nat(507u);
x_4 = lean_unsigned_to_nat(20u);
x_4 = lean_unsigned_to_nat(22u);
x_5 = l_List_get_x21___rarg___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
return x_6;
@ -8404,7 +8404,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__1;
x_2 = l_Lean_Expr_appFn_x21___closed__1;
x_3 = lean_unsigned_to_nat(527u);
x_4 = lean_unsigned_to_nat(15u);
x_4 = lean_unsigned_to_nat(17u);
x_5 = l_Lean_Expr_appFn_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
return x_6;
@ -8488,7 +8488,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__1;
x_2 = l_Lean_Expr_appArg_x21___closed__1;
x_3 = lean_unsigned_to_nat(531u);
x_4 = lean_unsigned_to_nat(15u);
x_4 = lean_unsigned_to_nat(17u);
x_5 = l_Lean_Expr_appFn_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
return x_6;
@ -8906,7 +8906,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__1;
x_2 = l_Lean_Expr_constName_x21___closed__1;
x_3 = lean_unsigned_to_nat(550u);
x_4 = lean_unsigned_to_nat(17u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l_Lean_Expr_constName_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
return x_6;
@ -9053,7 +9053,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__1;
x_2 = l_Lean_Expr_constLevels_x21___closed__1;
x_3 = lean_unsigned_to_nat(558u);
x_4 = lean_unsigned_to_nat(18u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_Expr_constName_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
return x_6;
@ -9143,7 +9143,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__1;
x_2 = l_Lean_Expr_bvarIdx_x21___closed__1;
x_3 = lean_unsigned_to_nat(562u);
x_4 = lean_unsigned_to_nat(16u);
x_4 = lean_unsigned_to_nat(18u);
x_5 = l_Lean_Expr_bvarIdx_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
return x_6;
@ -9233,7 +9233,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__1;
x_2 = l_Lean_Expr_fvarId_x21___closed__1;
x_3 = lean_unsigned_to_nat(566u);
x_4 = lean_unsigned_to_nat(14u);
x_4 = lean_unsigned_to_nat(16u);
x_5 = l_Lean_Expr_fvarId_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
return x_6;
@ -9323,7 +9323,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__1;
x_2 = l_Lean_Expr_mvarId_x21___closed__1;
x_3 = lean_unsigned_to_nat(570u);
x_4 = lean_unsigned_to_nat(14u);
x_4 = lean_unsigned_to_nat(16u);
x_5 = l_Lean_Expr_mvarId_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
return x_6;
@ -9438,7 +9438,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__1;
x_2 = l_Lean_Expr_bindingName_x21___closed__1;
x_3 = lean_unsigned_to_nat(575u);
x_4 = lean_unsigned_to_nat(21u);
x_4 = lean_unsigned_to_nat(23u);
x_5 = l_Lean_Expr_bindingName_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
return x_6;
@ -9554,7 +9554,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__1;
x_2 = l_Lean_Expr_bindingDomain_x21___closed__1;
x_3 = lean_unsigned_to_nat(580u);
x_4 = lean_unsigned_to_nat(21u);
x_4 = lean_unsigned_to_nat(23u);
x_5 = l_Lean_Expr_bindingName_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
return x_6;
@ -9670,7 +9670,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__1;
x_2 = l_Lean_Expr_bindingBody_x21___closed__1;
x_3 = lean_unsigned_to_nat(585u);
x_4 = lean_unsigned_to_nat(21u);
x_4 = lean_unsigned_to_nat(23u);
x_5 = l_Lean_Expr_bindingName_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
return x_6;
@ -9786,7 +9786,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__1;
x_2 = l_Lean_Expr_bindingInfo_x21___closed__1;
x_3 = lean_unsigned_to_nat(590u);
x_4 = lean_unsigned_to_nat(21u);
x_4 = lean_unsigned_to_nat(23u);
x_5 = l_Lean_Expr_bindingName_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
return x_6;
@ -9895,7 +9895,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__1;
x_2 = l_Lean_Expr_letName_x21___closed__1;
x_3 = lean_unsigned_to_nat(594u);
x_4 = lean_unsigned_to_nat(20u);
x_4 = lean_unsigned_to_nat(22u);
x_5 = l_Lean_Expr_letName_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
return x_6;
@ -12107,8 +12107,8 @@ _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___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__1;
x_2 = l_Lean_Expr_hasAnyFVar_visit___closed__1;
x_3 = lean_unsigned_to_nat(853u);
x_4 = lean_unsigned_to_nat(30u);
x_3 = lean_unsigned_to_nat(851u);
x_4 = lean_unsigned_to_nat(32u);
x_5 = l___private_Init_LeanInit_0__Lean_eraseMacroScopesAux___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
return x_6;
@ -12374,8 +12374,8 @@ _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___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__1;
x_2 = l_Lean_Expr_updateApp_x21___closed__1;
x_3 = lean_unsigned_to_nat(875u);
x_4 = lean_unsigned_to_nat(18u);
x_3 = lean_unsigned_to_nat(873u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_Expr_appFn_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
return x_6;
@ -12480,8 +12480,8 @@ _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___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__1;
x_2 = l_Lean_Expr_updateConst_x21___closed__1;
x_3 = lean_unsigned_to_nat(884u);
x_4 = lean_unsigned_to_nat(18u);
x_3 = lean_unsigned_to_nat(882u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_Expr_constName_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
return x_6;
@ -12591,8 +12591,8 @@ _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___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__1;
x_2 = l_Lean_Expr_updateSort_x21___closed__1;
x_3 = lean_unsigned_to_nat(893u);
x_4 = lean_unsigned_to_nat(14u);
x_3 = lean_unsigned_to_nat(891u);
x_4 = lean_unsigned_to_nat(16u);
x_5 = l_Lean_Expr_updateSort_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
return x_6;
@ -12779,8 +12779,8 @@ _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___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__1;
x_2 = l_Lean_Expr_updateMData_x21___closed__1;
x_3 = lean_unsigned_to_nat(910u);
x_4 = lean_unsigned_to_nat(17u);
x_3 = lean_unsigned_to_nat(908u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l_Lean_Expr_updateMData_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
return x_6;
@ -12886,8 +12886,8 @@ _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___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__1;
x_2 = l_Lean_Expr_updateProj_x21___closed__1;
x_3 = lean_unsigned_to_nat(915u);
x_4 = lean_unsigned_to_nat(18u);
x_3 = lean_unsigned_to_nat(913u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_Expr_updateProj_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
return x_6;
@ -13006,8 +13006,8 @@ _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___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__1;
x_2 = l_Lean_Expr_updateForall_x21___closed__1;
x_3 = lean_unsigned_to_nat(924u);
x_4 = lean_unsigned_to_nat(21u);
x_3 = lean_unsigned_to_nat(922u);
x_4 = lean_unsigned_to_nat(23u);
x_5 = l_Lean_Expr_updateForall_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
return x_6;
@ -13119,8 +13119,8 @@ _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___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__1;
x_2 = l_Lean_Expr_updateForallE_x21___closed__1;
x_3 = lean_unsigned_to_nat(929u);
x_4 = lean_unsigned_to_nat(21u);
x_3 = lean_unsigned_to_nat(927u);
x_4 = lean_unsigned_to_nat(23u);
x_5 = l_Lean_Expr_updateForall_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
return x_6;
@ -13243,8 +13243,8 @@ _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___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__1;
x_2 = l_Lean_Expr_updateLambda_x21___closed__1;
x_3 = lean_unsigned_to_nat(938u);
x_4 = lean_unsigned_to_nat(17u);
x_3 = lean_unsigned_to_nat(936u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l_Lean_Expr_updateLambda_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
return x_6;
@ -13356,8 +13356,8 @@ _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___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__1;
x_2 = l_Lean_Expr_updateLambdaE_x21___closed__1;
x_3 = lean_unsigned_to_nat(943u);
x_4 = lean_unsigned_to_nat(17u);
x_3 = lean_unsigned_to_nat(941u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l_Lean_Expr_updateLambda_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
return x_6;
@ -13472,8 +13472,8 @@ _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___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__1;
x_2 = l_Lean_Expr_updateLet_x21___closed__1;
x_3 = lean_unsigned_to_nat(952u);
x_4 = lean_unsigned_to_nat(20u);
x_3 = lean_unsigned_to_nat(950u);
x_4 = lean_unsigned_to_nat(22u);
x_5 = l_Lean_Expr_letName_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
return x_6;
@ -13869,8 +13869,8 @@ _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___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__1;
x_2 = l_Lean_Expr_instantiateLevelParamsCore_visit___closed__1;
x_3 = lean_unsigned_to_nat(972u);
x_4 = lean_unsigned_to_nat(23u);
x_3 = lean_unsigned_to_nat(970u);
x_4 = lean_unsigned_to_nat(25u);
x_5 = l___private_Init_LeanInit_0__Lean_eraseMacroScopesAux___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
return x_6;

10
stage0/stdlib/Lean/Level.c generated
View file

@ -509,7 +509,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj
x_1 = l_Lean_Level_mkData___closed__2;
x_2 = l_Lean_Level_mkData___closed__3;
x_3 = lean_unsigned_to_nat(46u);
x_4 = lean_unsigned_to_nat(33u);
x_4 = lean_unsigned_to_nat(35u);
x_5 = l_Lean_Level_mkData___closed__4;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
return x_6;
@ -1845,7 +1845,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj
x_1 = l_Lean_Level_mkData___closed__2;
x_2 = l_Lean_Level_mvarId_x21___closed__1;
x_3 = lean_unsigned_to_nat(158u);
x_4 = lean_unsigned_to_nat(19u);
x_4 = lean_unsigned_to_nat(21u);
x_5 = l_Lean_Level_mvarId_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
return x_6;
@ -5890,7 +5890,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj
x_1 = l_Lean_Level_mkData___closed__2;
x_2 = l_Lean_Level_updateSucc_x21___closed__1;
x_3 = lean_unsigned_to_nat(435u);
x_4 = lean_unsigned_to_nat(16u);
x_4 = lean_unsigned_to_nat(18u);
x_5 = l_Lean_Level_updateSucc_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
return x_6;
@ -6000,7 +6000,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj
x_1 = l_Lean_Level_mkData___closed__2;
x_2 = l_Lean_Level_updateMax_x21___closed__1;
x_3 = lean_unsigned_to_nat(444u);
x_4 = lean_unsigned_to_nat(19u);
x_4 = lean_unsigned_to_nat(21u);
x_5 = l_Lean_Level_updateMax_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
return x_6;
@ -6114,7 +6114,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj
x_1 = l_Lean_Level_mkData___closed__2;
x_2 = l_Lean_Level_updateIMax_x21___closed__1;
x_3 = lean_unsigned_to_nat(453u);
x_4 = lean_unsigned_to_nat(20u);
x_4 = lean_unsigned_to_nat(22u);
x_5 = l_Lean_Level_updateIMax_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
return x_6;

2
stage0/stdlib/Lean/ResolveName.c generated
View file

@ -3770,7 +3770,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj
x_1 = l_Lean_ResolveName_resolveNamespaceUsingScope___closed__1;
x_2 = l_Lean_ResolveName_resolveNamespaceUsingScope___closed__2;
x_3 = lean_unsigned_to_nat(123u);
x_4 = lean_unsigned_to_nat(25u);
x_4 = lean_unsigned_to_nat(27u);
x_5 = l___private_Init_LeanInit_0__Lean_eraseMacroScopesAux___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
return x_6;