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-15 17:05:34 -07:00
parent 14414e3400
commit 765319e94a
22 changed files with 9583 additions and 9403 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

494
stage0/src/Lean/Elab/Structure.lean generated
View file

@ -1,3 +1,4 @@
#lang lean4
/-
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
@ -9,9 +10,7 @@ import Lean.Elab.DeclModifiers
import Lean.Elab.DeclUtil
import Lean.Elab.Inductive
namespace Lean
namespace Elab
namespace Command
namespace Lean.Elab.Command
open Meta
@ -100,36 +99,35 @@ parser! try (declModifiers >> ident >> optional inferMod >> " :: ")
```
-/
private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (structDeclName : Name) : CommandElabM StructCtorView :=
let optCtor := structStx.getArg 6;
let optCtor := structStx[6]
if optCtor.isNone then
pure { ref := structStx, modifiers := {}, inferMod := false, name := defaultCtorName, declName := structDeclName ++ defaultCtorName }
else
let ctor := optCtor.getArg 0;
let ctor := optCtor[0]
withRef ctor do
ctorModifiers ← elabModifiers (ctor.getArg 0);
checkValidCtorModifier ctorModifiers;
when (ctorModifiers.isPrivate && structModifiers.isPrivate) $
throwError "invalid 'private' constructor in a 'private' structure";
when (ctorModifiers.isProtected && structModifiers.isPrivate) $
throwError "invalid 'protected' constructor in a 'private' structure";
let inferMod := !(ctor.getArg 2).isNone;
let name := ctor.getIdAt 1;
let declName := structDeclName ++ name;
declName ← applyVisibility ctorModifiers.visibility declName;
let ctorModifiers ← elabModifiers ctor[0]
checkValidCtorModifier ctorModifiers
if ctorModifiers.isPrivate && structModifiers.isPrivate then
throwError "invalid 'private' constructor in a 'private' structure"
if ctorModifiers.isProtected && structModifiers.isPrivate then
throwError "invalid 'protected' constructor in a 'private' structure"
let inferMod := !ctor[2].isNone
let name := ctor[1].getId
let declName := structDeclName ++ name
let declName ← applyVisibility ctorModifiers.visibility declName
pure { ref := ctor, name := name, modifiers := ctorModifiers, inferMod := inferMod, declName := declName }
def checkValidFieldModifier (modifiers : Modifiers) : CommandElabM Unit := do
when modifiers.isNoncomputable $
throwError "invalid use of 'noncomputable' in field declaration";
when modifiers.isPartial $
throwError "invalid use of 'partial' in field declaration";
when modifiers.isUnsafe $
throwError "invalid use of 'unsafe' in field declaration";
when (modifiers.attrs.size != 0) $
throwError "invalid use of attributes in field declaration";
when modifiers.isPrivate $
throwError "private fields are not supported yet";
pure ()
if modifiers.isNoncomputable then
throwError "invalid use of 'noncomputable' in field declaration"
if modifiers.isPartial then
throwError "invalid use of 'partial' in field declaration"
if modifiers.isUnsafe then
throwError "invalid use of 'unsafe' in field declaration"
if modifiers.attrs.size != 0 then
throwError "invalid use of attributes in field declaration"
if modifiers.isPrivate then
throwError "private fields are not supported yet"
/-
```
@ -140,56 +138,53 @@ def structFields := parser! many (structExplicitBinder <|> structImplici
```
-/
private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (structDeclName : Name) : CommandElabM (Array StructFieldView) :=
let fieldBinders := ((structStx.getArg 7).getArg 0).getArgs;
fieldBinders.foldlM
(fun (views : Array StructFieldView) fieldBinder => withRef fieldBinder do
let k := fieldBinder.getKind;
binfo ←
if k == `Lean.Parser.Command.structExplicitBinder then pure BinderInfo.default
else if k == `Lean.Parser.Command.structImplicitBinder then pure BinderInfo.implicit
else if k == `Lean.Parser.Command.structInstBinder then pure BinderInfo.instImplicit
else throwError "unexpected kind of structure field";
fieldModifiers ← elabModifiers (fieldBinder.getArg 0);
checkValidFieldModifier fieldModifiers;
when (fieldModifiers.isPrivate && structModifiers.isPrivate) $
throwError "invalid 'private' field in a 'private' structure";
when (fieldModifiers.isProtected && structModifiers.isPrivate) $
throwError "invalid 'protected' field in a 'private' structure";
let inferMod := !(fieldBinder.getArg 3).isNone;
let (binders, type?) :=
if binfo == BinderInfo.default then
expandOptDeclSig (fieldBinder.getArg 4)
let fieldBinders := structStx[7][0].getArgs
fieldBinders.foldlM (init := #[]) fun (views : Array StructFieldView) fieldBinder => withRef fieldBinder do
let k := fieldBinder.getKind
let binfo ←
if k == `Lean.Parser.Command.structExplicitBinder then pure BinderInfo.default
else if k == `Lean.Parser.Command.structImplicitBinder then pure BinderInfo.implicit
else if k == `Lean.Parser.Command.structInstBinder then pure BinderInfo.instImplicit
else throwError "unexpected kind of structure field"
let fieldModifiers ← elabModifiers fieldBinder[0]
checkValidFieldModifier fieldModifiers
if fieldModifiers.isPrivate && structModifiers.isPrivate then
throwError "invalid 'private' field in a 'private' structure"
if fieldModifiers.isProtected && structModifiers.isPrivate then
throwError "invalid 'protected' field in a 'private' structure"
let inferMod := !fieldBinder[3].isNone
let (binders, type?) :=
if binfo == BinderInfo.default then
expandOptDeclSig fieldBinder[4]
else
let (binders, type) := expandDeclSig fieldBinder[4]
(binders, some type)
let value? :=
if binfo != BinderInfo.default then none
else
let optBinderDefault := fieldBinder[5]
if optBinderDefault.isNone then none
else
let (binders, type) := expandDeclSig (fieldBinder.getArg 4);
(binders, some type);
let value? :=
if binfo != BinderInfo.default then none
else
let optBinderDefault := fieldBinder.getArg 5;
if optBinderDefault.isNone then none
else
-- binderDefault := parser! " := " >> termParser
some $ (optBinderDefault.getArg 0).getArg 1;
let idents := (fieldBinder.getArg 2).getArgs;
idents.foldlM
(fun (views : Array StructFieldView) ident => withRef ident do
let name := ident.getId;
when (isInternalSubobjectFieldName name) $
throwError ("invalid field name '" ++ name ++ "', identifiers starting with '_' are reserved to the system");
let declName := structDeclName ++ name;
declName ← applyVisibility fieldModifiers.visibility declName;
pure $ views.push {
ref := ident,
modifiers := fieldModifiers,
binderInfo := binfo,
inferMod := inferMod,
declName := declName,
name := name,
binders := binders,
type? := type?,
value? := value? })
views)
#[]
-- binderDefault := parser! " := " >> termParser
some optBinderDefault[0][1]
let idents := fieldBinder[2].getArgs
idents.foldlM (init := views) fun (views : Array StructFieldView) ident => withRef ident do
let name := ident.getId
if isInternalSubobjectFieldName name then
throwError! "invalid field name '{name}', identifiers starting with '_' are reserved to the system"
let declName := structDeclName ++ name
let declName ← applyVisibility fieldModifiers.visibility declName
pure $ views.push {
ref := ident,
modifiers := fieldModifiers,
binderInfo := binfo,
inferMod := inferMod,
declName := declName,
name := name,
binders := binders,
type? := type?,
value? := value? }
private def validStructType (type : Expr) : Bool :=
match type with
@ -199,11 +194,10 @@ match type with
private def checkParentIsStructure (parent : Expr) : TermElabM Name :=
match parent.getAppFn with
| Expr.const c _ _ => do
env ← getEnv;
unless (isStructure env c) $
throwError $ "'" ++ toString c ++ "' is not a structure";
unless isStructure (← getEnv) c do
throwError! "'{c}' is not a structure"
pure c
| _ => throwError $ "expected structure"
| _ => throwError "expected structure"
private def findFieldInfo? (infos : Array StructFieldInfo) (fieldName : Name) : Option StructFieldInfo :=
infos.find? fun info => info.name == fieldName
@ -212,40 +206,40 @@ private def containsFieldName (infos : Array StructFieldInfo) (fieldName : Name)
(findFieldInfo? infos fieldName).isSome
private partial def processSubfields {α} (structDeclName : Name) (parentFVar : Expr) (parentStructName : Name) (subfieldNames : Array Name)
: Nat → Array StructFieldInfo → (Array StructFieldInfo → TermElabM α) → TermElabM α
| i, infos, k =>
if h : i < subfieldNames.size then do
let subfieldName := subfieldNames.get ⟨i, h⟩;
env ← getEnv;
when (containsFieldName infos subfieldName) $
throwError ("field '" ++ subfieldName ++ "' from '" ++ parentStructName ++ "' has already been declared");
val ← mkProjection parentFVar subfieldName;
type ← inferType val;
(infos : Array StructFieldInfo) (k : Array StructFieldInfo → TermElabM α) : TermElabM α :=
let rec loop (i : Nat) (infos : Array StructFieldInfo) := do
if h : i < subfieldNames.size then
let subfieldName := subfieldNames.get ⟨i, h⟩
if containsFieldName infos subfieldName then
throwError! "field '{subfieldName}' from '{parentStructName}' has already been declared"
let val ← mkProjection parentFVar subfieldName
let type ← inferType val
withLetDecl subfieldName type val fun subfieldFVar =>
/- The following `declName` is only used for creating the `_default` auxiliary declaration name when
its default value is overwritten in the structure. -/
let declName := structDeclName ++ subfieldName;
let infos := infos.push { name := subfieldName, declName := declName, fvar := subfieldFVar, kind := StructFieldKind.fromParent };
processSubfields (i+1) infos k
let declName := structDeclName ++ subfieldName
let infos := infos.push { name := subfieldName, declName := declName, fvar := subfieldFVar, kind := StructFieldKind.fromParent }
loop (i+1) infos
else
k infos
loop 0 infos
private partial def withParents {α} (view : StructView) : Nat → Array StructFieldInfo → (Array StructFieldInfo → TermElabM α) → TermElabM α
| i, infos, k =>
if h : i < view.parents.size then
let parentStx := view.parents.get ⟨i, h⟩;
let parentStx := view.parents.get ⟨i, h⟩
withRef parentStx do
parent ← Term.elabType parentStx;
parentName ← checkParentIsStructure parent;
let toParentName := mkNameSimple $ "to" ++ parentName.eraseMacroScopes.getString!; -- erase macro scopes?
when (containsFieldName infos toParentName) $
throwErrorAt parentStx ("field '" ++ toParentName ++ "' has already been declared");
env ← getEnv;
let binfo := if view.isClass && isClass env parentName then BinderInfo.instImplicit else BinderInfo.default;
withLocalDecl toParentName binfo parent $ fun parentFVar =>
let infos := infos.push { name := toParentName, declName := view.declName ++ toParentName, fvar := parentFVar, kind := StructFieldKind.subobject };
let subfieldNames := getStructureFieldsFlattened env parentName;
processSubfields view.declName parentFVar parentName subfieldNames 0 infos fun infos => withParents (i+1) infos k
let parent ← Term.elabType parentStx
let parentName ← checkParentIsStructure parent
let toParentName := mkNameSimple $ "to" ++ parentName.eraseMacroScopes.getString! -- erase macro scopes?
if containsFieldName infos toParentName then
throwErrorAt! parentStx "field '{toParentName}' has already been declared"
let env ← getEnv
let binfo := if view.isClass && isClass env parentName then BinderInfo.instImplicit else BinderInfo.default
withLocalDecl toParentName binfo parent fun parentFVar =>
let infos := infos.push { name := toParentName, declName := view.declName ++ toParentName, fvar := parentFVar, kind := StructFieldKind.subobject }
let subfieldNames := getStructureFieldsFlattened env parentName
processSubfields view.declName parentFVar parentName subfieldNames infos fun infos => withParents view (i+1) infos k
else
k infos
@ -254,91 +248,89 @@ match view.type? with
| none =>
match view.value? with
| none => pure (none, none)
| some valStx => do
value ← Term.elabTerm valStx none;
value ← mkLambdaFVars params value;
| some valStx =>
let value ← Term.elabTerm valStx none
let value ← mkLambdaFVars params value
pure (none, value)
| some typeStx => do
type ← Term.elabType typeStx;
| some typeStx =>
let type ← Term.elabType typeStx
match view.value? with
| none => do
type ← mkForallFVars params type;
| none =>
let type ← mkForallFVars params type
pure (type, none)
| some valStx => do
value ← Term.elabTermEnsuringType valStx type;
type ← mkForallFVars params type;
value ← mkLambdaFVars params value;
| some valStx =>
let value ← Term.elabTermEnsuringType valStx type
let type ← mkForallFVars params type
let value ← mkLambdaFVars params value
pure (type, value)
private partial def withFields {α} (views : Array StructFieldView) : Nat → Array StructFieldInfo → (Array StructFieldInfo → TermElabM α) → TermElabM α
| i, infos, k =>
if h : i < views.size then do
let view := views.get ⟨i, h⟩;
let view := views.get ⟨i, h⟩
withRef view.ref $
match findFieldInfo? infos view.name with
| none => do
(type?, value?) ← Term.elabBinders view.binders.getArgs $ fun params => elabFieldTypeValue view params;
let (type?, value?) ← Term.elabBinders view.binders.getArgs fun params => elabFieldTypeValue view params
match type?, value? with
| none, none => throwError "invalid field, type expected"
| some type, _ =>
withLocalDecl view.name view.binderInfo type $ fun fieldFVar =>
let infos := infos.push { name := view.name, declName := view.declName, fvar := fieldFVar, value? := value?,
kind := StructFieldKind.newField, inferMod := view.inferMod };
withFields (i+1) infos k
| none, some value => do
type ← inferType value;
withLocalDecl view.name view.binderInfo type $ fun fieldFVar =>
let infos := infos.push { name := view.name, declName := view.declName, fvar := fieldFVar, kind := StructFieldKind.newField, inferMod := view.inferMod };
withFields (i+1) infos k
kind := StructFieldKind.newField, inferMod := view.inferMod }
withFields views (i+1) infos k
| none, some value =>
let type ← inferType value
withLocalDecl view.name view.binderInfo type fun fieldFVar =>
let infos := infos.push { name := view.name, declName := view.declName, fvar := fieldFVar, kind := StructFieldKind.newField, inferMod := view.inferMod }
withFields views (i+1) infos k
| some info =>
match info.kind with
| StructFieldKind.newField => throwError ("field '" ++ view.name ++ "' has already been declared")
| StructFieldKind.newField => throwError! "field '{view.name}' has already been declared"
| StructFieldKind.fromParent =>
match view.value? with
| none => throwError ("field '" ++ view.name ++ "' has been declared in parent structure")
| none => throwError! "field '{view.name}' has been declared in parent structure"
| some valStx => do
when (!view.binders.getArgs.isEmpty || view.type?.isSome) $
throwErrorAt view.type?.get! ("omit field '" ++ view.name ++ "' type to set default value");
fvarType ← inferType info.fvar;
value ← Term.elabTermEnsuringType valStx fvarType;
let infos := infos.push { info with value? := value };
withFields (i+1) infos k
if !view.binders.getArgs.isEmpty || view.type?.isSome then
throwErrorAt! view.type?.get! "omit field '{view.name}' type to set default value"
let fvarType ← inferType info.fvar
let value ← Term.elabTermEnsuringType valStx fvarType
let infos := infos.push { info with value? := value }
withFields views (i+1) infos k
| StructFieldKind.subobject => unreachable!
else
k infos
private def getResultUniverse (type : Expr) : TermElabM Level := do
type ← whnf type;
let type ← whnf type
match type with
| Expr.sort u _ => pure u
| _ => throwError "unexpected structure resulting type"
private def collectUsed (params : Array Expr) (fieldInfos : Array StructFieldInfo) : StateRefT CollectFVars.State TermElabM Unit := do
params.forM fun p => do {
type ← inferType p;
params.forM fun p => do
let type ← inferType p
Term.collectUsedFVars type
};
fieldInfos.forM fun info => do {
fvarType ← inferType info.fvar;
Term.collectUsedFVars fvarType;
fieldInfos.forM fun info => do
let fvarType ← inferType info.fvar
Term.collectUsedFVars fvarType
match info.value? with
| none => pure ()
| some value => Term.collectUsedFVars value
}
private def removeUnused (scopeVars : Array Expr) (params : Array Expr) (fieldInfos : Array StructFieldInfo)
: TermElabM (LocalContext × LocalInstances × Array Expr) := do
(_, used) ← (collectUsed params fieldInfos).run {};
let (_, used) ← (collectUsed params fieldInfos).run {}
Term.removeUnused scopeVars used
private def withUsed {α} (scopeVars : Array Expr) (params : Array Expr) (fieldInfos : Array StructFieldInfo) (k : Array Expr → TermElabM α)
: TermElabM α := do
(lctx, localInsts, vars) ← removeUnused scopeVars params fieldInfos;
let (lctx, localInsts, vars) ← removeUnused scopeVars params fieldInfos
withLCtx lctx localInsts $ k vars
private def levelMVarToParamFVar (fvar : Expr) : StateRefT Nat TermElabM Unit := do
type ← inferType fvar;
_ ← Term.levelMVarToParam' type;
let type ← inferType fvar
Term.levelMVarToParam' type
pure ()
private def levelMVarToParamFVars (fvars : Array Expr) : StateRefT Nat TermElabM Unit :=
@ -346,165 +338,157 @@ fvars.forM levelMVarToParamFVar
private def levelMVarToParamAux (scopeVars : Array Expr) (params : Array Expr) (fieldInfos : Array StructFieldInfo)
: StateRefT Nat TermElabM (Array StructFieldInfo) := do
levelMVarToParamFVars scopeVars;
levelMVarToParamFVars params;
levelMVarToParamFVars scopeVars
levelMVarToParamFVars params
fieldInfos.mapM fun info => do
levelMVarToParamFVar info.fvar;
levelMVarToParamFVar info.fvar
match info.value? with
| none => pure info
| some value => do
value ← Term.levelMVarToParam' value;
| some value =>
let value ← Term.levelMVarToParam' value
pure { info with value? := value }
private def levelMVarToParam (scopeVars : Array Expr) (params : Array Expr) (fieldInfos : Array StructFieldInfo) : TermElabM (Array StructFieldInfo) :=
(levelMVarToParamAux scopeVars params fieldInfos).run' 1
private partial def collectUniversesFromFields (r : Level) (rOffset : Nat) (fieldInfos : Array StructFieldInfo) : TermElabM (Array Level) := do
fieldInfos.foldlM
(fun (us : Array Level) (info : StructFieldInfo) => do
type ← inferType info.fvar;
u ← getLevel type;
u ← instantiateLevelMVars u;
match accLevelAtCtor u r rOffset us with
| Except.error msg => throwError msg
| Except.ok us => pure us)
#[]
fieldInfos.foldlM (init := #[]) fun (us : Array Level) (info : StructFieldInfo) => do
let type ← inferType info.fvar
let u ← getLevel type
let u ← instantiateLevelMVars u
match accLevelAtCtor u r rOffset us with
| Except.error msg => throwError msg
| Except.ok us => pure us
private def updateResultingUniverse (fieldInfos : Array StructFieldInfo) (type : Expr) : TermElabM Expr := do
r ← getResultUniverse type;
let rOffset : Nat := r.getOffset;
let r : Level := r.getLevelOffset;
let r ← getResultUniverse type
let rOffset : Nat := r.getOffset
let r : Level := r.getLevelOffset
match r with
| Level.mvar mvarId _ => do
us ← collectUniversesFromFields r rOffset fieldInfos;
let rNew := Level.mkNaryMax us.toList;
assignLevelMVar mvarId rNew;
| Level.mvar mvarId _ =>
let us ← collectUniversesFromFields r rOffset fieldInfos
let rNew := Level.mkNaryMax us.toList
assignLevelMVar mvarId rNew
instantiateMVars type
| _ => throwError "failed to compute resulting universe level of structure, provide universe explicitly"
private def collectLevelParamsInFVar (s : CollectLevelParams.State) (fvar : Expr) : TermElabM CollectLevelParams.State := do
type ← inferType fvar;
type ← instantiateMVars type;
let type ← inferType fvar
let type ← instantiateMVars type
pure $ collectLevelParams s type
private def collectLevelParamsInFVars (fvars : Array Expr) (s : CollectLevelParams.State) : TermElabM CollectLevelParams.State :=
fvars.foldlM collectLevelParamsInFVar s
private def collectLevelParamsInStructure (scopeVars : Array Expr) (params : Array Expr) (fieldInfos : Array StructFieldInfo) : TermElabM (Array Name) := do
s ← collectLevelParamsInFVars scopeVars {};
s ← collectLevelParamsInFVars params s;
s ← fieldInfos.foldlM (fun (s : CollectLevelParams.State) info => collectLevelParamsInFVar s info.fvar) s;
let s ← collectLevelParamsInFVars scopeVars {}
let s ← collectLevelParamsInFVars params s
let s ← fieldInfos.foldlM (fun (s : CollectLevelParams.State) info => collectLevelParamsInFVar s info.fvar) s
pure s.params
private def addCtorFields (fieldInfos : Array StructFieldInfo) : Nat → Expr → TermElabM Expr
| 0, type => pure type
| i+1, type => do
let info := fieldInfos.get! i;
decl ← Term.getFVarLocalDecl! info.fvar;
type ← instantiateMVars type;
let type := type.abstract #[info.fvar];
let info := fieldInfos[i]
let decl ← Term.getFVarLocalDecl! info.fvar
let type ← instantiateMVars type
let type := type.abstract #[info.fvar]
match info.kind with
| StructFieldKind.fromParent =>
let val := decl.value;
addCtorFields i (type.instantiate1 val)
let val := decl.value
addCtorFields fieldInfos i (type.instantiate1 val)
| StructFieldKind.subobject =>
let n := mkInternalSubobjectFieldName $ decl.userName;
addCtorFields i (mkForall n decl.binderInfo decl.type type)
let n := mkInternalSubobjectFieldName $ decl.userName
addCtorFields fieldInfos i (mkForall n decl.binderInfo decl.type type)
| StructFieldKind.newField =>
addCtorFields i (mkForall decl.userName decl.binderInfo decl.type type)
addCtorFields fieldInfos i (mkForall decl.userName decl.binderInfo decl.type type)
private def mkCtor (view : StructView) (levelParams : List Name) (params : Array Expr) (fieldInfos : Array StructFieldInfo) : TermElabM Constructor :=
withRef view.ref do
let type := mkAppN (mkConst view.declName (levelParams.map mkLevelParam)) params;
type ← addCtorFields fieldInfos fieldInfos.size type;
type ← mkForallFVars params type;
type ← instantiateMVars type;
let type := type.inferImplicit params.size !view.ctor.inferMod;
let type := mkAppN (mkConst view.declName (levelParams.map mkLevelParam)) params
let type ← addCtorFields fieldInfos fieldInfos.size type
let type ← mkForallFVars params type
let type ← instantiateMVars type
let type := type.inferImplicit params.size !view.ctor.inferMod
pure { name := view.ctor.declName, type := type }
@[extern "lean_mk_projections"]
private constant mkProjections (env : Environment) (structName : @& Name) (projs : @& List ProjectionInfo) (isClass : Bool) : Except String Environment := arbitrary _
private constant mkProjections (env : Environment) (structName : Name) (projs : List ProjectionInfo) (isClass : Bool) : Except String Environment := arbitrary _
private def addProjections (structName : Name) (projs : List ProjectionInfo) (isClass : Bool) : TermElabM Unit := do
env ← getEnv;
let env ← getEnv
match mkProjections env structName projs isClass with
| Except.ok env => setEnv env
| Except.error msg => throwError msg
private def mkAuxConstructions (declName : Name) : TermElabM Unit := do
env ← getEnv;
let hasUnit := env.contains `PUnit;
let hasEq := env.contains `Eq;
let hasHEq := env.contains `HEq;
modifyEnv fun env => mkRecOn env declName;
when hasUnit $ modifyEnv fun env => mkCasesOn env declName;
when (hasUnit && hasEq && hasHEq) $ modifyEnv fun env => mkNoConfusion env declName
let env ← getEnv
let hasUnit := env.contains `PUnit
let hasEq := env.contains `Eq
let hasHEq := env.contains `HEq
modifyEnv fun env => mkRecOn env declName
if hasUnit then modifyEnv fun env => mkCasesOn env declName
if hasUnit && hasEq && hasHEq then modifyEnv fun env => mkNoConfusion env declName
private def addDefaults (lctx : LocalContext) (defaultAuxDecls : Array (Name × Expr × Expr)) : TermElabM Unit := do
localInsts ← getLocalInstances;
let localInsts ← getLocalInstances
withLCtx lctx localInsts do
defaultAuxDecls.forM fun ⟨declName, type, value⟩ => do
defaultAuxDecls.forM fun (declName, type, value) => do
/- The identity function is used as "marker". -/
value ← mkId value;
let zeta := true; -- expand `let-declarations`
_ ← mkAuxDefinition declName type value zeta;
modifyEnv fun env => setReducibilityStatus env declName ReducibilityStatus.reducible;
pure ()
let value ← mkId value
mkAuxDefinition declName type value (zeta := true)
modifyEnv fun env => setReducibilityStatus env declName ReducibilityStatus.reducible
private def elabStructureView (view : StructView) : TermElabM Unit := do
let numExplicitParams := view.params.size;
type ← Term.elabType view.type;
unless (validStructType type) $ throwErrorAt view.type "expected Type";
let numExplicitParams := view.params.size
let type ← Term.elabType view.type
unless validStructType type do throwErrorAt view.type "expected Type"
withRef view.ref do
withParents view 0 #[] fun fieldInfos =>
withFields view.fields 0 fieldInfos fun fieldInfos => do
Term.synthesizeSyntheticMVarsNoPostponing;
u ← getResultUniverse type;
inferLevel ← shouldInferResultUniverse u;
Term.synthesizeSyntheticMVarsNoPostponing
let u ← getResultUniverse type
let inferLevel ← shouldInferResultUniverse u
withUsed view.scopeVars view.params fieldInfos $ fun scopeVars => do
let numParams := scopeVars.size + numExplicitParams;
fieldInfos ← levelMVarToParam scopeVars view.params fieldInfos;
type ← if inferLevel then updateResultingUniverse fieldInfos type else pure type;
usedLevelNames ← collectLevelParamsInStructure scopeVars view.params fieldInfos;
let numParams := scopeVars.size + numExplicitParams
let fieldInfos ← levelMVarToParam scopeVars view.params fieldInfos
let type ← if inferLevel then updateResultingUniverse fieldInfos type else pure type
let usedLevelNames ← collectLevelParamsInStructure scopeVars view.params fieldInfos
match sortDeclLevelParams view.scopeLevelNames view.allUserLevelNames usedLevelNames with
| Except.error msg => throwError msg
| Except.ok levelParams => do
let params := scopeVars ++ view.params;
ctor ← mkCtor view levelParams params fieldInfos;
type ← mkForallFVars params type;
type ← instantiateMVars type;
let indType := { name := view.declName, type := type, ctors := [ctor] : InductiveType };
let decl := Declaration.inductDecl levelParams params.size [indType] view.modifiers.isUnsafe;
Term.ensureNoUnassignedMVars decl;
addDecl decl;
| Except.ok levelParams =>
let params := scopeVars ++ view.params
let ctor ← mkCtor view levelParams params fieldInfos
let type ← mkForallFVars params type
let type ← instantiateMVars type
let indType := { name := view.declName, type := type, ctors := [ctor] : InductiveType }
let decl := Declaration.inductDecl levelParams params.size [indType] view.modifiers.isUnsafe
Term.ensureNoUnassignedMVars decl
addDecl decl
let projInfos := (fieldInfos.filter fun (info : StructFieldInfo) => !info.isFromParent).toList.map fun (info : StructFieldInfo) =>
{ declName := info.declName, inferMod := info.inferMod : ProjectionInfo };
addProjections view.declName projInfos view.isClass;
mkAuxConstructions view.declName;
instParents ← fieldInfos.filterM fun info => do {
decl ← Term.getFVarLocalDecl! info.fvar;
{ declName := info.declName, inferMod := info.inferMod : ProjectionInfo }
addProjections view.declName projInfos view.isClass
mkAuxConstructions view.declName
let instParents ← fieldInfos.filterM fun info => do
let decl ← Term.getFVarLocalDecl! info.fvar
pure (info.isSubobject && decl.binderInfo.isInstImplicit)
};
let projInstances := instParents.toList.map fun info => info.declName;
Term.applyAttributesAt view.declName view.modifiers.attrs AttributeApplicationTime.afterTypeChecking;
projInstances.forM addGlobalInstance;
lctx ← getLCtx;
let fieldsWithDefault := fieldInfos.filter fun info => info.value?.isSome;
defaultAuxDecls ← fieldsWithDefault.mapM fun info => do {
type ← inferType info.fvar;
let projInstances := instParents.toList.map fun info => info.declName
Term.applyAttributesAt view.declName view.modifiers.attrs AttributeApplicationTime.afterTypeChecking
projInstances.forM addGlobalInstance
let lctx ← getLCtx
let fieldsWithDefault := fieldInfos.filter fun info => info.value?.isSome
let defaultAuxDecls ← fieldsWithDefault.mapM fun info => do
let type ← inferType info.fvar
pure (info.declName ++ `_default, type, info.value?.get!)
};
/- The `lctx` and `defaultAuxDecls` are used to create the auxiliary `_default` declarations
The parameters `params` for these definitions must be marked as implicit, and all others as explicit. -/
let lctx := params.foldl
(fun (lctx : LocalContext) (p : Expr) =>
lctx.updateBinderInfo p.fvarId! BinderInfo.implicit)
lctx;
let lctx := fieldInfos.foldl
(fun (lctx : LocalContext) (info : StructFieldInfo) =>
let lctx :=
params.foldl (init := lctx) fun (lctx : LocalContext) (p : Expr) =>
lctx.updateBinderInfo p.fvarId! BinderInfo.implicit
let lctx :=
fieldInfos.foldl (init := lctx) fun (lctx : LocalContext) (info : StructFieldInfo) =>
if info.isFromParent then lctx -- `fromParent` fields are elaborated as let-decls, and are zeta-expanded when creating `_default`.
else lctx.updateBinderInfo info.fvar.fvarId! BinderInfo.default)
lctx;
else lctx.updateBinderInfo info.fvar.fvarId! BinderInfo.default
addDefaults lctx defaultAuxDecls
/-
@ -520,19 +504,19 @@ def structCtor := parser! try (declModifiers >> ident >> optional infe
-/
def elabStructure (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
checkValidInductiveModifier modifiers;
let isClass := (stx.getArg 0).getKind == `Lean.Parser.Command.classTk;
let modifiers := if isClass then modifiers.addAttribute { name := `class } else modifiers;
let declId := stx.getArg 1;
let params := (stx.getArg 2).getArgs;
let exts := stx.getArg 3;
let parents := if exts.isNone then #[] else ((exts.getArg 0).getArg 1).getSepArgs;
let optType := stx.getArg 4;
type ← if optType.isNone then `(Type _) else pure $ (optType.getArg 0).getArg 1;
scopeLevelNames ← getLevelNames;
⟨name, declName, allUserLevelNames⟩ ← expandDeclId declId modifiers;
ctor ← expandCtor stx modifiers declName;
fields ← expandFields stx modifiers declName;
checkValidInductiveModifier modifiers
let isClass := stx[0].getKind == `Lean.Parser.Command.classTk
let modifiers := if isClass then modifiers.addAttribute { name := `class } else modifiers
let declId := stx[1]
let params := stx[2].getArgs
let exts := stx[3]
let parents := if exts.isNone then #[] else exts[0][1].getSepArgs
let optType := stx[4]
let type ← if optType.isNone then `(Type _) else pure optType[0][1]
let scopeLevelNames ← getLevelNames
let ⟨name, declName, allUserLevelNames⟩ ← expandDeclId declId modifiers
let ctor ← expandCtor stx modifiers declName
let fields ← expandFields stx modifiers declName
runTermElabM declName $ fun scopeVars => Term.withLevelNames allUserLevelNames $ Term.elabBinders params fun params => elabStructureView {
ref := stx,
modifiers := modifiers,
@ -548,6 +532,4 @@ runTermElabM declName $ fun scopeVars => Term.withLevelNames allUserLevelNames $
fields := fields
}
end Command
end Elab
end Lean
end Lean.Elab.Command

11
stage0/src/Lean/Parser/Basic.lean generated
View file

@ -488,7 +488,7 @@ fun c s =>
{ info := p.info,
fn := lookaheadFn p.fn }
@[inline] def notFollowedByFn (p : ParserFn) : ParserFn :=
@[inline] def notFollowedByFn (p : ParserFn) (msg : String) : ParserFn :=
fun c s =>
let iniSz := s.stackSize;
let iniPos := s.pos;
@ -497,10 +497,10 @@ fun c s =>
s.restore iniSz iniPos
else
let s := s.restore iniSz iniPos;
s.mkError "notFollowedBy"
s.mkUnexpectedError ("unexpected " ++ msg)
@[inline] def notFollowedBy (p : Parser) : Parser :=
{ fn := notFollowedByFn p.fn }
@[inline] def notFollowedBy (p : Parser) (msg : String) : Parser :=
{ fn := notFollowedByFn p.fn msg }
@[specialize] partial def manyAux (p : ParserFn) : ParserFn
| c, s =>
@ -1035,6 +1035,9 @@ let sym := sym.trim;
{ info := symbolInfo sym,
fn := symbolFn sym }
abbrev notSymbol (s : String) : Parser :=
notFollowedBy (symbol s) s
/-- Check if the following token is the symbol _or_ identifier `sym`. Useful for
parsing local tokens that have not been added to the token table (but may have
been so by some unrelated code).

2
stage0/src/Lean/Parser/Command.lean generated
View file

@ -87,7 +87,7 @@ def openOnly := parser! try (ident >> "(") >> many1 ident >> ")"
def openSimple := parser! many1 ident
@[builtinCommandParser] def «open» := parser! "open " >> (openHiding <|> openRenaming <|> openOnly <|> openSimple)
@[builtinCommandParser] def «mutual» := parser! "mutual " >> many1 (notFollowedBy «end» >> commandParser) >> "end"
@[builtinCommandParser] def «mutual» := parser! "mutual " >> many1 (notSymbol "end" >> commandParser) >> "end"
@[builtinCommandParser] def «initialize» := parser! "initialize " >> optional («try» (ident >> Term.typeSpec >> Term.leftArrow)) >> Term.doSeq
@[builtinCommandParser] def «in» := tparser! " in " >> commandParser

4
stage0/src/Lean/Parser/Do.lean generated
View file

@ -25,7 +25,8 @@ def doSeqIndent := parser! many1Indent $ group (doElemParser >> optional "; "
def doSeqBracketed := parser! "{" >> withoutPosition (many1 (group (doElemParser >> optional "; "))) >> "}"
def doSeq := doSeqBracketed <|> doSeqIndent
def notFollowedByRedefinedTermToken := notFollowedBy ("if" <|> "match" <|> "let" <|> "have" <|> "do" <|> "dbgTrace!" <|> "assert!")
def notFollowedByRedefinedTermToken :=
notFollowedBy ("if" <|> "match" <|> "let" <|> "have" <|> "do" <|> "dbgTrace!" <|> "assert!") "token at 'do' element"
@[builtinDoElemParser] def doLet := parser! "let " >> letDecl
@[builtinDoElemParser] def doLetRec := parser! group ("let " >> nonReservedSymbol "rec ") >> letRecDecls
@ -94,6 +95,7 @@ Note that parser priorities would not solve this problem since the `doIf` parser
parser is succeeding.
-/
@[builtinDoElemParser] def doExpr := parser! notFollowedByRedefinedTermToken >> termParser
@[builtinDoElemParser] def doNested := parser! "do " >> doSeq
@[builtinTermParser] def «do» := parser!:maxPrec "do " >> doSeq

4
stage0/src/Lean/Parser/Extension.lean generated
View file

@ -203,7 +203,7 @@ partial def compileParserDescr (env : Environment) (categories : ParserCategorie
| ParserDescr.optional d => optional <$> compileParserDescr d
| ParserDescr.lookahead d => lookahead <$> compileParserDescr d
| ParserDescr.try d => try <$> compileParserDescr d
| ParserDescr.notFollowedBy d => notFollowedBy <$> compileParserDescr d
| ParserDescr.notFollowedBy d => do p ← compileParserDescr d; pure $ notFollowedBy p "element" -- TODO allow user to set msg at ParserDescr
| ParserDescr.many d => many <$> compileParserDescr d
| ParserDescr.many1 d => many1 <$> compileParserDescr d
| ParserDescr.sepBy d₁ d₂ => sepBy <$> compileParserDescr d₁ <*> compileParserDescr d₂
@ -487,7 +487,7 @@ fun ctx s =>
| some (Syntax.atom _ sym) =>
if ctx.insideQuot && sym == "$" then s
else match cat.tables.leadingTable.find? (mkNameSimple sym) with
| some _ => s.mkError "notFollowedByCategoryToken"
| some _ => s.mkUnexpectedError (toString catName)
| _ => s
| _ => s

5
stage0/src/Lean/Parser/Tactic.lean generated
View file

@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Sebastian Ullrich
-/
import Lean.Parser.Term
import Lean.Parser.Command
namespace Lean
namespace Parser
@ -25,7 +26,7 @@ fun c s =>
def ident' : Parser := ident <|> underscore
@[builtinTacticParser] def «intro» := parser! nonReservedSymbol "intro " >> notFollowedBy "|" >> many (checkColGt >> termParser maxPrec)
@[builtinTacticParser] def «intro» := parser! nonReservedSymbol "intro " >> notSymbol "|" >> many (checkColGt >> termParser maxPrec)
@[builtinTacticParser] def «intros» := parser! nonReservedSymbol "intros " >> many (checkColGt >> ident')
@[builtinTacticParser] def «revert» := parser! nonReservedSymbol "revert " >> many1 (checkColGt >> ident)
@[builtinTacticParser] def «clear» := parser! nonReservedSymbol "clear " >> many1 (checkColGt >> ident)
@ -55,7 +56,7 @@ def location := parser! "at " >> (locationWildcard <|> locationTarget <|
def rwRule := parser! optional (unicodeSymbol "←" "<-") >> termParser
def rwRuleSeq := parser! "[" >> sepBy1 rwRule ", " true >> "]"
@[builtinTacticParser] def «rewrite» := parser! (nonReservedSymbol "rewrite" <|> nonReservedSymbol "rw") >> notFollowedBy "[" >> rwRule >> optional location
@[builtinTacticParser] def «rewrite» := parser! (nonReservedSymbol "rewrite" <|> nonReservedSymbol "rw") >> notSymbol "[" >> rwRule >> optional location
@[builtinTacticParser] def «rewriteSeq» := parser! (nonReservedSymbol "rewrite" <|> nonReservedSymbol "rw") >> rwRuleSeq >> optional location
def majorPremise := parser! optional (try (ident >> " : ")) >> termParser

2
stage0/src/Lean/Parser/Term.lean generated
View file

@ -157,7 +157,7 @@ def letIdDecl := node `Lean.Parser.Term.letIdDecl $ try (letIdLhs >> " := ")
def letPatDecl := node `Lean.Parser.Term.letPatDecl $ try (termParser >> pushNone >> optType >> " := ") >> termParser
def letEqnsDecl := node `Lean.Parser.Term.letEqnsDecl $ letIdLhs >> matchAlts false
-- Remark: we use `nodeWithAntiquot` here to make sure anonymous antiquotations (e.g., `$x`) are not `letDecl`
def letDecl := nodeWithAntiquot "letDecl" `Lean.Parser.Term.letDecl (notFollowedBy (nonReservedSymbol "rec") >> (letIdDecl <|> letPatDecl <|> letEqnsDecl))
def letDecl := nodeWithAntiquot "letDecl" `Lean.Parser.Term.letDecl (notFollowedBy (nonReservedSymbol "rec") "rec" >> (letIdDecl <|> letPatDecl <|> letEqnsDecl))
@[builtinTermParser] def «let» := parser!:leadPrec withPosition ("let " >> letDecl) >> optSemicolon termParser
@[builtinTermParser] def «let!» := parser!:leadPrec withPosition ("let! " >> letDecl) >> optSemicolon termParser
@[builtinTermParser] def «let*» := parser!:leadPrec withPosition ("let* " >> letDecl) >> optSemicolon termParser

4
stage0/src/Lean/PrettyPrinter/Formatter.lean generated
View file

@ -191,6 +191,10 @@ st ← get;
let stx := st.stxTrav.parents.back.getArg (st.stxTrav.idxs.back - offset);
categoryParser.formatter stx.getId
@[combinatorFormatter Lean.Parser.error]
def error.formatter (msg : String) : Formatter :=
pure ()
@[combinatorFormatter Lean.Parser.try]
def try.formatter (p : Formatter) : Formatter :=
p

4
stage0/src/Lean/PrettyPrinter/Parenthesizer.lean generated
View file

@ -320,6 +320,10 @@ def level.parenthesizer : CategoryParenthesizer | prec => do
maybeParenthesize `level (fun stx => Unhygienic.run `(level|($stx))) prec $
parenthesizeCategoryCore `level prec
@[combinatorParenthesizer Lean.Parser.error]
def error.parenthesizer (msg : String) : Parenthesizer :=
pure ()
@[combinatorParenthesizer Lean.Parser.try]
def try.parenthesizer (p : Parenthesizer) : Parenthesizer :=
p

4
stage0/src/library/constructions/projection.cpp generated
View file

@ -113,8 +113,8 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
extern "C" object * lean_mk_projections(object * env, object * struct_name, object * proj_infos, uint8 inst_implicit) {
environment new_env(env);
name n(struct_name, true);
list_ref<object_ref> ps(proj_infos, true);
name n(struct_name);
list_ref<object_ref> ps(proj_infos);
buffer<name> proj_names;
buffer<implicit_infer_kind> infer_kinds;
for (auto p : ps) {

665
stage0/stdlib/Lean/Elab/Declaration.c generated
View file

File diff suppressed because it is too large Load diff

13205
stage0/stdlib/Lean/Elab/Structure.c generated
View file

File diff suppressed because it is too large Load diff

1460
stage0/stdlib/Lean/Elab/Syntax.c generated
View file

File diff suppressed because it is too large Load diff

104
stage0/stdlib/Lean/Parser/Basic.c generated
View file

@ -54,6 +54,7 @@ lean_object* l_Lean_Parser_notFollowedByFn___closed__1;
lean_object* l_Lean_Syntax_foldSepRevArgsM(lean_object*, lean_object*);
extern lean_object* l_Lean_nullKind;
lean_object* l_Lean_Parser_leadPrec;
lean_object* l_Lean_Parser_notFollowedByFn___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_strLitNoAntiquot;
lean_object* l_Lean_Parser_octalNumberFn___closed__1;
lean_object* l_Lean_Parser_many(lean_object*);
@ -153,7 +154,7 @@ extern uint32_t l_Lean_idEndEscape;
lean_object* l_Lean_Parser_mkAntiquot___closed__9;
lean_object* l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__8;
lean_object* l_Lean_Parser_pushNone___elambda__1___boxed(lean_object*);
lean_object* l_Lean_Parser_notFollowedByFn(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_notFollowedByFn(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_foldSepByM(lean_object*, lean_object*);
lean_object* l_Lean_Parser_orelseFn(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_RBNode_find___main___at_Lean_Parser_indexed___spec__1___rarg___boxed(lean_object*, lean_object*);
@ -174,7 +175,7 @@ lean_object* l_Lean_Parser_mkAntiquot___closed__27;
lean_object* l_Lean_Parser_tokenFn(lean_object*, lean_object*);
lean_object* l_Lean_Parser_withoutForbidden___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_mkAtomicInfo(lean_object*);
lean_object* l_Lean_Parser_notFollowedBy(lean_object*);
lean_object* l_Lean_Parser_notFollowedBy(lean_object*, lean_object*);
lean_object* l_Lean_Parser_satisfyFn___at_Lean_Parser_binNumberFn___spec__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_charLit___elambda__1___closed__1;
lean_object* lean_string_utf8_extract(lean_object*, lean_object*, lean_object*);
@ -560,6 +561,7 @@ lean_object* l_Lean_Parser_nameLit___elambda__1___closed__1;
lean_object* l_Lean_Parser_mkAntiquot___elambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_EnvExtensionInterfaceUnsafe_Ext_inhabitedExt___closed__2;
lean_object* l_Lean_Parser_checkOutsideQuotFn(lean_object*, lean_object*);
lean_object* l_Lean_Parser_notSymbol(lean_object*);
lean_object* l_Lean_Parser_categoryParserFn(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_foldlStepMAux___main___at_Array_foldSepByM___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_checkInsideQuot___closed__1;
@ -5046,58 +5048,69 @@ static lean_object* _init_l_Lean_Parser_notFollowedByFn___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("notFollowedBy");
x_1 = lean_mk_string("unexpected ");
return x_1;
}
}
lean_object* l_Lean_Parser_notFollowedByFn(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_Lean_Parser_notFollowedByFn(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_4 = lean_ctor_get(x_3, 0);
lean_inc(x_4);
x_5 = lean_array_get_size(x_4);
lean_dec(x_4);
x_6 = lean_ctor_get(x_3, 1);
lean_inc(x_6);
x_7 = lean_apply_2(x_1, x_2, x_3);
x_8 = lean_ctor_get(x_7, 3);
lean_inc(x_8);
if (lean_obj_tag(x_8) == 0)
{
lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_9 = l_Lean_Parser_ParserState_restore(x_7, x_5, x_6);
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_5 = lean_ctor_get(x_4, 0);
lean_inc(x_5);
x_6 = lean_array_get_size(x_5);
lean_dec(x_5);
x_10 = l_Lean_Parser_notFollowedByFn___closed__1;
x_11 = l_Lean_Parser_ParserState_mkError(x_9, x_10);
return x_11;
x_7 = lean_ctor_get(x_4, 1);
lean_inc(x_7);
x_8 = lean_apply_2(x_1, x_3, x_4);
x_9 = lean_ctor_get(x_8, 3);
lean_inc(x_9);
if (lean_obj_tag(x_9) == 0)
{
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_10 = l_Lean_Parser_ParserState_restore(x_8, x_6, x_7);
lean_dec(x_6);
x_11 = l_Lean_Parser_notFollowedByFn___closed__1;
x_12 = lean_string_append(x_11, x_2);
x_13 = l_Lean_Parser_ParserState_mkUnexpectedError(x_10, x_12);
return x_13;
}
else
{
lean_object* x_12;
lean_dec(x_8);
x_12 = l_Lean_Parser_ParserState_restore(x_7, x_5, x_6);
lean_dec(x_5);
return x_12;
lean_object* x_14;
lean_dec(x_9);
x_14 = l_Lean_Parser_ParserState_restore(x_8, x_6, x_7);
lean_dec(x_6);
return x_14;
}
}
}
lean_object* l_Lean_Parser_notFollowedBy(lean_object* x_1) {
lean_object* l_Lean_Parser_notFollowedByFn___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_2 = lean_ctor_get(x_1, 1);
lean_inc(x_2);
lean_dec(x_1);
x_3 = lean_alloc_closure((void*)(l_Lean_Parser_notFollowedByFn), 3, 1);
lean_closure_set(x_3, 0, x_2);
x_4 = l_Lean_Parser_Parser_inhabited___closed__1;
x_5 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_5, 0, x_4);
lean_ctor_set(x_5, 1, x_3);
lean_object* x_5;
x_5 = l_Lean_Parser_notFollowedByFn(x_1, x_2, x_3, x_4);
lean_dec(x_2);
return x_5;
}
}
lean_object* l_Lean_Parser_notFollowedBy(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_3 = lean_ctor_get(x_1, 1);
lean_inc(x_3);
lean_dec(x_1);
x_4 = lean_alloc_closure((void*)(l_Lean_Parser_notFollowedByFn___boxed), 4, 2);
lean_closure_set(x_4, 0, x_3);
lean_closure_set(x_4, 1, x_2);
x_5 = l_Lean_Parser_Parser_inhabited___closed__1;
x_6 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_6, 0, x_5);
lean_ctor_set(x_6, 1, x_4);
return x_6;
}
}
static lean_object* _init_l_Lean_Parser_manyAux___main___closed__1() {
_start:
{
@ -10133,6 +10146,23 @@ lean_dec(x_1);
return x_2;
}
}
lean_object* l_Lean_Parser_notSymbol(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_2 = l_String_trim(x_1);
x_3 = lean_alloc_closure((void*)(l_Lean_Parser_symbolFn___boxed), 3, 1);
lean_closure_set(x_3, 0, x_2);
x_4 = lean_alloc_closure((void*)(l_Lean_Parser_notFollowedByFn___boxed), 4, 2);
lean_closure_set(x_4, 0, x_3);
lean_closure_set(x_4, 1, x_1);
x_5 = l_Lean_Parser_Parser_inhabited___closed__1;
x_6 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_6, 0, x_5);
lean_ctor_set(x_6, 1, x_4);
return x_6;
}
}
lean_object* l_Lean_Parser_nonReservedSymbolFnAux(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{

1054
stage0/stdlib/Lean/Parser/Command.c generated
View file

File diff suppressed because it is too large Load diff

703
stage0/stdlib/Lean/Parser/Do.c generated
View file

File diff suppressed because it is too large Load diff

529
stage0/stdlib/Lean/Parser/Extension.c generated
View file

@ -43,6 +43,7 @@ lean_object* l_unreachable_x21___rarg(lean_object*);
lean_object* l_Lean_Parser_mkParserExtension___closed__2;
lean_object* l_Array_iterateMAux___main___at___private_Lean_Parser_Extension_10__ParserExtension_addImported___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_insertAux___main___at___private_Lean_Parser_Extension_3__addParserCategoryCore___spec__4(lean_object*, size_t, size_t, lean_object*, lean_object*);
lean_object* l_Lean_Parser_notFollowedByFn___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_IO_ofExcept___at___private_Lean_Parser_Extension_10__ParserExtension_addImported___spec__1(lean_object*, lean_object*);
lean_object* lean_io_error_to_string(lean_object*);
lean_object* l___private_Lean_Parser_Extension_6__addTokenConfig___closed__2;
@ -81,7 +82,6 @@ lean_object* l_Lean_Parser_nonReservedSymbolFn(lean_object*, lean_object*, lean_
lean_object* l___private_Lean_Parser_Extension_2__throwParserCategoryAlreadyDefined___rarg___closed__1;
lean_object* l_Lean_Parser_mkParserState(lean_object*);
lean_object* l_Lean_Parser_mkParserExtension___lambda__2(lean_object*);
lean_object* l_Lean_Parser_notFollowedByFn(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Parser_Extension_13__registerParserAttributeImplBuilder___closed__1;
lean_object* l_Lean_Parser_declareBuiltinParser___closed__3;
lean_object* l_Std_PersistentHashMap_contains___at___private_Lean_Parser_Extension_3__addParserCategoryCore___spec__1___boxed(lean_object*, lean_object*);
@ -154,7 +154,6 @@ lean_object* l_List_forM___main___at_Lean_Parser_runParserAttributeHooks___spec_
lean_object* l_Lean_Parser_setCategoryParserFnRef(lean_object*);
extern lean_object* l_Lean_registerTagAttribute___lambda__4___closed__3;
lean_object* l_Lean_Parser_throwUnknownParserCategory(lean_object*);
lean_object* l_Lean_Parser_notFollowedByCategoryTokenFn___closed__1;
extern lean_object* l_Lean_Parser_PrattParsingTables_inhabited___closed__1;
lean_object* l_Lean_Parser_compileParserDescr___main___closed__3;
lean_object* l_Lean_Parser_throwUnknownParserCategory___rarg___closed__1;
@ -303,6 +302,7 @@ lean_object* l_Lean_Parser_sepBy1Info(lean_object*, lean_object*);
lean_object* l_Lean_Parser_sepBy1Fn___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_mkAppStx___closed__3;
uint8_t l_Array_anyRangeMAux___main___at_Lean_Parser_mkParserExtension___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_compileParserDescr___main___closed__9;
lean_object* l_List_forM___main___at___private_Lean_Parser_Extension_12__ParserAttribute_add___spec__1___closed__2;
lean_object* l___private_Lean_Parser_Extension_12__ParserAttribute_add___boxed(lean_object*);
lean_object* l_Lean_Parser_declareLeadingBuiltinParser(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -3634,6 +3634,14 @@ lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Parser_compileParserDescr___main___closed__9() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("element");
return x_1;
}
}
lean_object* l_Lean_Parser_compileParserDescr___main(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
@ -4998,38 +5006,42 @@ uint8_t x_340;
x_340 = !lean_is_exclusive(x_336);
if (x_340 == 0)
{
lean_object* x_341; lean_object* x_342; lean_object* x_343; lean_object* x_344; lean_object* x_345;
lean_object* x_341; lean_object* x_342; lean_object* x_343; lean_object* x_344; lean_object* x_345; lean_object* x_346;
x_341 = lean_ctor_get(x_336, 0);
x_342 = lean_ctor_get(x_341, 1);
lean_inc(x_342);
lean_dec(x_341);
x_343 = lean_alloc_closure((void*)(l_Lean_Parser_notFollowedByFn), 3, 1);
lean_closure_set(x_343, 0, x_342);
x_344 = l_Lean_Parser_Parser_inhabited___closed__1;
x_345 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_345, 0, x_344);
lean_ctor_set(x_345, 1, x_343);
lean_ctor_set(x_336, 0, x_345);
x_343 = l_Lean_Parser_compileParserDescr___main___closed__9;
x_344 = lean_alloc_closure((void*)(l_Lean_Parser_notFollowedByFn___boxed), 4, 2);
lean_closure_set(x_344, 0, x_342);
lean_closure_set(x_344, 1, x_343);
x_345 = l_Lean_Parser_Parser_inhabited___closed__1;
x_346 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_346, 0, x_345);
lean_ctor_set(x_346, 1, x_344);
lean_ctor_set(x_336, 0, x_346);
return x_336;
}
else
{
lean_object* x_346; lean_object* x_347; lean_object* x_348; lean_object* x_349; lean_object* x_350; lean_object* x_351;
x_346 = lean_ctor_get(x_336, 0);
lean_inc(x_346);
lean_dec(x_336);
x_347 = lean_ctor_get(x_346, 1);
lean_object* x_347; lean_object* x_348; lean_object* x_349; lean_object* x_350; lean_object* x_351; lean_object* x_352; lean_object* x_353;
x_347 = lean_ctor_get(x_336, 0);
lean_inc(x_347);
lean_dec(x_346);
x_348 = lean_alloc_closure((void*)(l_Lean_Parser_notFollowedByFn), 3, 1);
lean_closure_set(x_348, 0, x_347);
x_349 = l_Lean_Parser_Parser_inhabited___closed__1;
x_350 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_350, 0, x_349);
lean_ctor_set(x_350, 1, x_348);
x_351 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_351, 0, x_350);
return x_351;
lean_dec(x_336);
x_348 = lean_ctor_get(x_347, 1);
lean_inc(x_348);
lean_dec(x_347);
x_349 = l_Lean_Parser_compileParserDescr___main___closed__9;
x_350 = lean_alloc_closure((void*)(l_Lean_Parser_notFollowedByFn___boxed), 4, 2);
lean_closure_set(x_350, 0, x_348);
lean_closure_set(x_350, 1, x_349);
x_351 = l_Lean_Parser_Parser_inhabited___closed__1;
x_352 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_352, 0, x_351);
lean_ctor_set(x_352, 1, x_350);
x_353 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_353, 0, x_352);
return x_353;
}
}
}
@ -9693,14 +9705,6 @@ goto _start;
}
}
}
static lean_object* _init_l_Lean_Parser_notFollowedByCategoryTokenFn___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("notFollowedByCategoryToken");
return x_1;
}
}
lean_object* l_Lean_Parser_notFollowedByCategoryTokenFn(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
@ -9731,45 +9735,44 @@ return x_15;
else
{
uint8_t x_16;
lean_dec(x_1);
x_16 = !lean_is_exclusive(x_8);
if (x_16 == 0)
{
lean_object* x_17; lean_object* x_18; lean_object* x_45; lean_object* x_46; lean_object* x_47; uint8_t x_48;
lean_object* x_17; lean_object* x_18; lean_object* x_47; lean_object* x_48; lean_object* x_49; uint8_t x_50;
x_17 = lean_ctor_get(x_8, 0);
x_45 = lean_ctor_get(x_3, 2);
lean_inc(x_45);
x_46 = lean_ctor_get(x_45, 0);
lean_inc(x_46);
x_47 = lean_ctor_get(x_3, 1);
x_47 = lean_ctor_get(x_3, 2);
lean_inc(x_47);
x_48 = lean_nat_dec_eq(x_46, x_47);
lean_dec(x_47);
lean_dec(x_46);
if (x_48 == 0)
x_48 = lean_ctor_get(x_47, 0);
lean_inc(x_48);
x_49 = lean_ctor_get(x_3, 1);
lean_inc(x_49);
x_50 = lean_nat_dec_eq(x_48, x_49);
lean_dec(x_49);
lean_dec(x_48);
if (x_50 == 0)
{
lean_object* x_49;
lean_dec(x_45);
lean_object* x_51;
lean_dec(x_47);
lean_free_object(x_8);
lean_inc(x_2);
x_49 = l_Lean_Parser_peekTokenAux(x_2, x_3);
x_18 = x_49;
goto block_44;
x_51 = l_Lean_Parser_peekTokenAux(x_2, x_3);
x_18 = x_51;
goto block_46;
}
else
{
lean_object* x_50; lean_object* x_51;
x_50 = lean_ctor_get(x_45, 2);
lean_inc(x_50);
lean_dec(x_45);
lean_ctor_set(x_8, 0, x_50);
x_51 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_51, 0, x_3);
lean_ctor_set(x_51, 1, x_8);
x_18 = x_51;
goto block_44;
lean_object* x_52; lean_object* x_53;
x_52 = lean_ctor_get(x_47, 2);
lean_inc(x_52);
lean_dec(x_47);
lean_ctor_set(x_8, 0, x_52);
x_53 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_53, 0, x_3);
lean_ctor_set(x_53, 1, x_8);
x_18 = x_53;
goto block_46;
}
block_44:
block_46:
{
lean_object* x_19;
x_19 = lean_ctor_get(x_18, 1);
@ -9779,6 +9782,7 @@ if (lean_obj_tag(x_19) == 0)
lean_object* x_20;
lean_dec(x_17);
lean_dec(x_2);
lean_dec(x_1);
x_20 = lean_ctor_get(x_18, 0);
lean_inc(x_20);
lean_dec(x_18);
@ -9817,230 +9821,243 @@ lean_dec(x_28);
lean_dec(x_26);
if (lean_obj_tag(x_29) == 0)
{
lean_dec(x_1);
return x_23;
}
else
{
lean_object* x_30; lean_object* x_31;
lean_object* x_30; lean_object* x_31; lean_object* x_32;
lean_dec(x_29);
x_30 = l_Lean_Parser_notFollowedByCategoryTokenFn___closed__1;
x_31 = l_Lean_Parser_ParserState_mkError(x_23, x_30);
return x_31;
x_30 = l_System_FilePath_dirName___closed__1;
x_31 = l_Lean_Name_toStringWithSep___main(x_30, x_1);
x_32 = l_Lean_Parser_ParserState_mkUnexpectedError(x_23, x_31);
return x_32;
}
}
else
{
lean_object* x_32; lean_object* x_33; lean_object* x_34; uint8_t x_35;
x_32 = lean_ctor_get(x_18, 0);
lean_inc(x_32);
lean_dec(x_18);
x_33 = lean_ctor_get(x_21, 1);
lean_object* x_33; lean_object* x_34; lean_object* x_35; uint8_t x_36;
x_33 = lean_ctor_get(x_18, 0);
lean_inc(x_33);
lean_dec(x_21);
x_34 = l_Lean_Parser_mkAntiquot___closed__8;
x_35 = lean_string_dec_eq(x_33, x_34);
if (x_35 == 0)
{
lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40;
x_36 = lean_ctor_get(x_17, 0);
lean_inc(x_36);
lean_dec(x_17);
x_37 = lean_ctor_get(x_36, 0);
lean_inc(x_37);
lean_dec(x_36);
x_38 = lean_box(0);
x_39 = lean_name_mk_string(x_38, x_33);
x_40 = l_Std_RBNode_find___main___at_Lean_Parser_notFollowedByCategoryTokenFn___spec__1(x_37, x_39);
lean_dec(x_39);
lean_dec(x_37);
if (lean_obj_tag(x_40) == 0)
{
return x_32;
}
else
{
lean_object* x_41; lean_object* x_42;
lean_dec(x_40);
x_41 = l_Lean_Parser_notFollowedByCategoryTokenFn___closed__1;
x_42 = l_Lean_Parser_ParserState_mkError(x_32, x_41);
return x_42;
}
}
else
{
lean_dec(x_33);
lean_dec(x_17);
return x_32;
}
}
}
else
{
lean_object* x_43;
lean_dec(x_21);
lean_dec(x_17);
lean_dec(x_2);
x_43 = lean_ctor_get(x_18, 0);
lean_inc(x_43);
lean_dec(x_18);
return x_43;
x_34 = lean_ctor_get(x_21, 1);
lean_inc(x_34);
lean_dec(x_21);
x_35 = l_Lean_Parser_mkAntiquot___closed__8;
x_36 = lean_string_dec_eq(x_34, x_35);
if (x_36 == 0)
{
lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41;
x_37 = lean_ctor_get(x_17, 0);
lean_inc(x_37);
lean_dec(x_17);
x_38 = lean_ctor_get(x_37, 0);
lean_inc(x_38);
lean_dec(x_37);
x_39 = lean_box(0);
x_40 = lean_name_mk_string(x_39, x_34);
x_41 = l_Std_RBNode_find___main___at_Lean_Parser_notFollowedByCategoryTokenFn___spec__1(x_38, x_40);
lean_dec(x_40);
lean_dec(x_38);
if (lean_obj_tag(x_41) == 0)
{
lean_dec(x_1);
return x_33;
}
else
{
lean_object* x_42; lean_object* x_43; lean_object* x_44;
lean_dec(x_41);
x_42 = l_System_FilePath_dirName___closed__1;
x_43 = l_Lean_Name_toStringWithSep___main(x_42, x_1);
x_44 = l_Lean_Parser_ParserState_mkUnexpectedError(x_33, x_43);
return x_44;
}
}
else
{
lean_dec(x_34);
lean_dec(x_17);
lean_dec(x_1);
return x_33;
}
}
}
else
{
lean_object* x_52; lean_object* x_53; lean_object* x_80; lean_object* x_81; lean_object* x_82; uint8_t x_83;
x_52 = lean_ctor_get(x_8, 0);
lean_inc(x_52);
lean_dec(x_8);
x_80 = lean_ctor_get(x_3, 2);
lean_inc(x_80);
x_81 = lean_ctor_get(x_80, 0);
lean_inc(x_81);
x_82 = lean_ctor_get(x_3, 1);
lean_inc(x_82);
x_83 = lean_nat_dec_eq(x_81, x_82);
lean_dec(x_82);
lean_dec(x_81);
if (x_83 == 0)
{
lean_object* x_84;
lean_dec(x_80);
lean_inc(x_2);
x_84 = l_Lean_Parser_peekTokenAux(x_2, x_3);
x_53 = x_84;
goto block_79;
}
else
{
lean_object* x_85; lean_object* x_86; lean_object* x_87;
x_85 = lean_ctor_get(x_80, 2);
lean_inc(x_85);
lean_dec(x_80);
x_86 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_86, 0, x_85);
x_87 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_87, 0, x_3);
lean_ctor_set(x_87, 1, x_86);
x_53 = x_87;
goto block_79;
}
block_79:
{
lean_object* x_54;
x_54 = lean_ctor_get(x_53, 1);
lean_inc(x_54);
if (lean_obj_tag(x_54) == 0)
{
lean_object* x_55;
lean_dec(x_52);
lean_object* x_45;
lean_dec(x_21);
lean_dec(x_17);
lean_dec(x_2);
x_55 = lean_ctor_get(x_53, 0);
lean_inc(x_55);
lean_dec(x_53);
return x_55;
lean_dec(x_1);
x_45 = lean_ctor_get(x_18, 0);
lean_inc(x_45);
lean_dec(x_18);
return x_45;
}
}
}
}
else
{
lean_object* x_54; lean_object* x_55; lean_object* x_84; lean_object* x_85; lean_object* x_86; uint8_t x_87;
x_54 = lean_ctor_get(x_8, 0);
lean_inc(x_54);
lean_dec(x_8);
x_84 = lean_ctor_get(x_3, 2);
lean_inc(x_84);
x_85 = lean_ctor_get(x_84, 0);
lean_inc(x_85);
x_86 = lean_ctor_get(x_3, 1);
lean_inc(x_86);
x_87 = lean_nat_dec_eq(x_85, x_86);
lean_dec(x_86);
lean_dec(x_85);
if (x_87 == 0)
{
lean_object* x_88;
lean_dec(x_84);
lean_inc(x_2);
x_88 = l_Lean_Parser_peekTokenAux(x_2, x_3);
x_55 = x_88;
goto block_83;
}
else
{
lean_object* x_89; lean_object* x_90; lean_object* x_91;
x_89 = lean_ctor_get(x_84, 2);
lean_inc(x_89);
lean_dec(x_84);
x_90 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_90, 0, x_89);
x_91 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_91, 0, x_3);
lean_ctor_set(x_91, 1, x_90);
x_55 = x_91;
goto block_83;
}
block_83:
{
lean_object* x_56;
x_56 = lean_ctor_get(x_54, 0);
x_56 = lean_ctor_get(x_55, 1);
lean_inc(x_56);
if (lean_obj_tag(x_56) == 0)
{
lean_object* x_57;
lean_dec(x_54);
if (lean_obj_tag(x_56) == 2)
{
uint8_t x_57;
x_57 = lean_ctor_get_uint8(x_2, sizeof(void*)*6);
lean_dec(x_2);
if (x_57 == 0)
lean_dec(x_1);
x_57 = lean_ctor_get(x_55, 0);
lean_inc(x_57);
lean_dec(x_55);
return x_57;
}
else
{
lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64;
x_58 = lean_ctor_get(x_53, 0);
lean_object* x_58;
x_58 = lean_ctor_get(x_56, 0);
lean_inc(x_58);
lean_dec(x_53);
x_59 = lean_ctor_get(x_56, 1);
lean_inc(x_59);
lean_dec(x_56);
x_60 = lean_ctor_get(x_52, 0);
lean_inc(x_60);
lean_dec(x_52);
x_61 = lean_ctor_get(x_60, 0);
lean_inc(x_61);
lean_dec(x_60);
x_62 = lean_box(0);
x_63 = lean_name_mk_string(x_62, x_59);
x_64 = l_Std_RBNode_find___main___at_Lean_Parser_notFollowedByCategoryTokenFn___spec__1(x_61, x_63);
lean_dec(x_63);
lean_dec(x_61);
if (lean_obj_tag(x_64) == 0)
if (lean_obj_tag(x_58) == 2)
{
return x_58;
}
else
{
lean_object* x_65; lean_object* x_66;
lean_dec(x_64);
x_65 = l_Lean_Parser_notFollowedByCategoryTokenFn___closed__1;
x_66 = l_Lean_Parser_ParserState_mkError(x_58, x_65);
return x_66;
}
}
else
{
lean_object* x_67; lean_object* x_68; lean_object* x_69; uint8_t x_70;
x_67 = lean_ctor_get(x_53, 0);
lean_inc(x_67);
lean_dec(x_53);
x_68 = lean_ctor_get(x_56, 1);
lean_inc(x_68);
lean_dec(x_56);
x_69 = l_Lean_Parser_mkAntiquot___closed__8;
x_70 = lean_string_dec_eq(x_68, x_69);
if (x_70 == 0)
{
lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75;
x_71 = lean_ctor_get(x_52, 0);
lean_inc(x_71);
lean_dec(x_52);
x_72 = lean_ctor_get(x_71, 0);
lean_inc(x_72);
lean_dec(x_71);
x_73 = lean_box(0);
x_74 = lean_name_mk_string(x_73, x_68);
x_75 = l_Std_RBNode_find___main___at_Lean_Parser_notFollowedByCategoryTokenFn___spec__1(x_72, x_74);
lean_dec(x_74);
lean_dec(x_72);
if (lean_obj_tag(x_75) == 0)
{
return x_67;
}
else
{
lean_object* x_76; lean_object* x_77;
lean_dec(x_75);
x_76 = l_Lean_Parser_notFollowedByCategoryTokenFn___closed__1;
x_77 = l_Lean_Parser_ParserState_mkError(x_67, x_76);
return x_77;
}
}
else
{
lean_dec(x_68);
lean_dec(x_52);
return x_67;
}
}
}
else
{
lean_object* x_78;
lean_dec(x_56);
lean_dec(x_52);
uint8_t x_59;
x_59 = lean_ctor_get_uint8(x_2, sizeof(void*)*6);
lean_dec(x_2);
x_78 = lean_ctor_get(x_53, 0);
lean_inc(x_78);
lean_dec(x_53);
return x_78;
if (x_59 == 0)
{
lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66;
x_60 = lean_ctor_get(x_55, 0);
lean_inc(x_60);
lean_dec(x_55);
x_61 = lean_ctor_get(x_58, 1);
lean_inc(x_61);
lean_dec(x_58);
x_62 = lean_ctor_get(x_54, 0);
lean_inc(x_62);
lean_dec(x_54);
x_63 = lean_ctor_get(x_62, 0);
lean_inc(x_63);
lean_dec(x_62);
x_64 = lean_box(0);
x_65 = lean_name_mk_string(x_64, x_61);
x_66 = l_Std_RBNode_find___main___at_Lean_Parser_notFollowedByCategoryTokenFn___spec__1(x_63, x_65);
lean_dec(x_65);
lean_dec(x_63);
if (lean_obj_tag(x_66) == 0)
{
lean_dec(x_1);
return x_60;
}
else
{
lean_object* x_67; lean_object* x_68; lean_object* x_69;
lean_dec(x_66);
x_67 = l_System_FilePath_dirName___closed__1;
x_68 = l_Lean_Name_toStringWithSep___main(x_67, x_1);
x_69 = l_Lean_Parser_ParserState_mkUnexpectedError(x_60, x_68);
return x_69;
}
}
else
{
lean_object* x_70; lean_object* x_71; lean_object* x_72; uint8_t x_73;
x_70 = lean_ctor_get(x_55, 0);
lean_inc(x_70);
lean_dec(x_55);
x_71 = lean_ctor_get(x_58, 1);
lean_inc(x_71);
lean_dec(x_58);
x_72 = l_Lean_Parser_mkAntiquot___closed__8;
x_73 = lean_string_dec_eq(x_71, x_72);
if (x_73 == 0)
{
lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78;
x_74 = lean_ctor_get(x_54, 0);
lean_inc(x_74);
lean_dec(x_54);
x_75 = lean_ctor_get(x_74, 0);
lean_inc(x_75);
lean_dec(x_74);
x_76 = lean_box(0);
x_77 = lean_name_mk_string(x_76, x_71);
x_78 = l_Std_RBNode_find___main___at_Lean_Parser_notFollowedByCategoryTokenFn___spec__1(x_75, x_77);
lean_dec(x_77);
lean_dec(x_75);
if (lean_obj_tag(x_78) == 0)
{
lean_dec(x_1);
return x_70;
}
else
{
lean_object* x_79; lean_object* x_80; lean_object* x_81;
lean_dec(x_78);
x_79 = l_System_FilePath_dirName___closed__1;
x_80 = l_Lean_Name_toStringWithSep___main(x_79, x_1);
x_81 = l_Lean_Parser_ParserState_mkUnexpectedError(x_70, x_80);
return x_81;
}
}
else
{
lean_dec(x_71);
lean_dec(x_54);
lean_dec(x_1);
return x_70;
}
}
}
else
{
lean_object* x_82;
lean_dec(x_58);
lean_dec(x_54);
lean_dec(x_2);
lean_dec(x_1);
x_82 = lean_ctor_get(x_55, 0);
lean_inc(x_82);
lean_dec(x_55);
return x_82;
}
}
}
@ -10214,6 +10231,8 @@ l_Lean_Parser_compileParserDescr___main___closed__7 = _init_l_Lean_Parser_compil
lean_mark_persistent(l_Lean_Parser_compileParserDescr___main___closed__7);
l_Lean_Parser_compileParserDescr___main___closed__8 = _init_l_Lean_Parser_compileParserDescr___main___closed__8();
lean_mark_persistent(l_Lean_Parser_compileParserDescr___main___closed__8);
l_Lean_Parser_compileParserDescr___main___closed__9 = _init_l_Lean_Parser_compileParserDescr___main___closed__9();
lean_mark_persistent(l_Lean_Parser_compileParserDescr___main___closed__9);
res = l_Lean_Parser_mkParserAttributeHooks(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
l_Lean_Parser_parserAttributeHooks = lean_io_result_get_value(res);
@ -10371,8 +10390,6 @@ lean_mark_persistent(l_Lean_Parser_regCommandParserAttribute___closed__2);
res = l_Lean_Parser_regCommandParserAttribute(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Parser_notFollowedByCategoryTokenFn___closed__1 = _init_l_Lean_Parser_notFollowedByCategoryTokenFn___closed__1();
lean_mark_persistent(l_Lean_Parser_notFollowedByCategoryTokenFn___closed__1);
l_Lean_Parser_notFollowedByCommandToken___closed__1 = _init_l_Lean_Parser_notFollowedByCommandToken___closed__1();
lean_mark_persistent(l_Lean_Parser_notFollowedByCommandToken___closed__1);
l_Lean_Parser_notFollowedByCommandToken___closed__2 = _init_l_Lean_Parser_notFollowedByCommandToken___closed__2();

128
stage0/stdlib/Lean/Parser/Syntax.c generated
View file

@ -108,7 +108,6 @@ lean_object* l_Lean_Parser_Command_notation_formatter___closed__2;
lean_object* l_Lean_Parser_Command_syntaxAbbrev___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_withAntiquot_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_maxSymbol___elambda__1___closed__3;
extern lean_object* l_Lean_Parser_notFollowedByFn___closed__1;
extern lean_object* l_Lean_nullKind;
lean_object* l_Lean_Parser_Command_macroTailCommand_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_quot___closed__2;
@ -328,7 +327,6 @@ lean_object* l___regBuiltin_Lean_Parser_Syntax_try_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Command_macroTailDefault___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_maxSymbol___closed__6;
lean_object* l_Lean_Parser_Syntax_paren_parenthesizer___closed__1;
extern lean_object* l_Lean_Parser_Tactic_generalize_parenthesizer___closed__3;
lean_object* l_Lean_Parser_Command_elab___closed__3;
lean_object* l_Lean_Parser_Command_syntax_formatter___closed__1;
lean_object* l_Lean_PrettyPrinter_Formatter_try_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -619,6 +617,7 @@ lean_object* l_Lean_Parser_Syntax_orelse_parenthesizer___closed__2;
lean_object* l_Lean_Parser_noFirstTokenInfo(lean_object*);
lean_object* l_Lean_Parser_Command_infix___elambda__1___closed__8;
lean_object* l_Lean_Parser_Syntax_paren_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__8;
lean_object* l_Lean_Parser_Command_prefix___elambda__1___closed__7;
lean_object* l_Lean_Parser_Command_macroTailCommand_parenthesizer___closed__5;
lean_object* l_Lean_Parser_Command_macro__rules___closed__4;
@ -793,6 +792,7 @@ lean_object* l_Lean_Parser_Command_parserKind_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Command_notationItem___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_stx_quot___closed__1;
lean_object* l_Lean_Parser_Command_parserKindPrio___closed__1;
extern lean_object* l_Lean_Parser_Command_openHiding_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Command_syntaxCat_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Syntax_noWs___closed__6;
lean_object* l_Lean_Parser_Command_macroTailTactic;
@ -885,7 +885,6 @@ lean_object* l___regBuiltin_Lean_Parser_Command_syntax_formatter(lean_object*);
lean_object* l_Lean_Parser_precedence_parenthesizer___closed__4;
lean_object* l_Lean_Parser_Command_syntax_parenthesizer___closed__4;
lean_object* l_Lean_Parser_Command_elab_parenthesizer___closed__4;
extern lean_object* l_Lean_Parser_Tactic_generalize_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Syntax_paren_formatter___closed__2;
lean_object* l_Lean_Parser_Command_identPrec___elambda__1___closed__2;
lean_object* l_Lean_Parser_Command_optKindPrio_parenthesizer___closed__1;
@ -1044,7 +1043,6 @@ extern lean_object* l_Lean_Parser_Tactic_seq1___closed__4;
extern lean_object* l_Lean_Parser_Term_forall_formatter___closed__6;
lean_object* l_Lean_Parser_Command_mixfix_parenthesizer___closed__9;
lean_object* l_Lean_Parser_toggleInsideQuotFn(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Tactic_generalize_parenthesizer___closed__6;
lean_object* l_Lean_Parser_unquotedSymbolFn(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Syntax_notFollowedBy_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_identPrec___elambda__1___closed__4;
@ -1107,6 +1105,7 @@ lean_object* l_Lean_Parser_Command_infixl___elambda__1(lean_object*, lean_object
lean_object* l_Lean_Parser_Syntax_ident_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Syntax_atom_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Command_postfix___closed__4;
extern lean_object* l_Lean_Parser_Command_namespace_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Command_notation___closed__2;
lean_object* l_Lean_Parser_precedenceLit_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_syntaxCat___closed__3;
@ -1452,6 +1451,7 @@ lean_object* l_Lean_Parser_Command_prefix_formatter(lean_object*, lean_object*,
extern lean_object* l___regBuiltinParser_Lean_Parser_Level_num___closed__1;
lean_object* l_Lean_Parser_Syntax_atom___closed__2;
lean_object* l_Lean_Parser_precedence___closed__2;
extern lean_object* l_Lean_Parser_Command_openHiding_parenthesizer___closed__3;
lean_object* l_Lean_Parser_Command_parserKind___closed__2;
lean_object* l_Lean_Parser_Syntax_char___elambda__1(lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Parser_Syntax_optional_parenthesizer___closed__1;
@ -8960,35 +8960,43 @@ return x_5;
static lean_object* _init_l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Syntax_paren___elambda__1___closed__2;
x_2 = l_Lean_Parser_notFollowedByFn___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
lean_object* x_1;
x_1 = lean_mk_string("notFollowedBy");
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__1;
x_2 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Syntax_paren___elambda__1___closed__2;
x_2 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__2;
x_2 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4;
x_1 = l_Lean_Parser_notFollowedByFn___closed__1;
x_2 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__2;
x_1 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__1;
x_2 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__3;
x_3 = 1;
x_4 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__4() {
static lean_object* _init_l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__5() {
_start:
{
lean_object* x_1;
@ -8996,30 +9004,30 @@ x_1 = lean_mk_string("notFollowedBy ");
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__4;
x_2 = l_String_trim(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Char_HasRepr___closed__1;
x_2 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__5;
x_3 = lean_string_append(x_1, x_2);
return x_3;
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__5;
x_2 = l_String_trim(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__6;
x_1 = l_Char_HasRepr___closed__1;
x_2 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__6;
x_3 = lean_string_append(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__7;
x_2 = l_Char_HasRepr___closed__1;
x_3 = lean_string_append(x_1, x_2);
return x_3;
@ -9029,7 +9037,7 @@ lean_object* l_Lean_Parser_Syntax_notFollowedBy___elambda__1(lean_object* x_1, l
_start:
{
lean_object* x_3; lean_object* x_4; uint8_t x_5;
x_3 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__3;
x_3 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__4;
x_4 = lean_ctor_get(x_3, 1);
lean_inc(x_4);
lean_inc(x_2);
@ -9050,8 +9058,8 @@ x_9 = lean_ctor_get(x_7, 0);
lean_inc(x_9);
x_10 = lean_array_get_size(x_9);
lean_dec(x_9);
x_11 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__5;
x_12 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__7;
x_11 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__6;
x_12 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__8;
lean_inc(x_1);
x_13 = l_Lean_Parser_nonReservedSymbolFnAux(x_11, x_12, x_1, x_7);
x_14 = lean_ctor_get(x_13, 3);
@ -9062,7 +9070,7 @@ lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean
x_15 = l_Lean_Parser_categoryParserFnImpl___closed__4;
x_16 = l_Lean_Parser_maxPrec;
x_17 = l_Lean_Parser_categoryParser___elambda__1(x_15, x_16, x_1, x_13);
x_18 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__1;
x_18 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__2;
x_19 = l_Lean_Parser_ParserState_mkNode(x_17, x_18, x_10);
return x_19;
}
@ -9071,7 +9079,7 @@ else
lean_object* x_20; lean_object* x_21;
lean_dec(x_14);
lean_dec(x_1);
x_20 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__1;
x_20 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__2;
x_21 = l_Lean_Parser_ParserState_mkNode(x_13, x_20, x_10);
return x_21;
}
@ -9138,8 +9146,8 @@ x_34 = lean_ctor_get(x_32, 0);
lean_inc(x_34);
x_35 = lean_array_get_size(x_34);
lean_dec(x_34);
x_36 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__5;
x_37 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__7;
x_36 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__6;
x_37 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__8;
lean_inc(x_1);
x_38 = l_Lean_Parser_nonReservedSymbolFnAux(x_36, x_37, x_1, x_32);
x_39 = lean_ctor_get(x_38, 3);
@ -9150,7 +9158,7 @@ lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean
x_40 = l_Lean_Parser_categoryParserFnImpl___closed__4;
x_41 = l_Lean_Parser_maxPrec;
x_42 = l_Lean_Parser_categoryParser___elambda__1(x_40, x_41, x_1, x_38);
x_43 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__1;
x_43 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__2;
x_44 = l_Lean_Parser_ParserState_mkNode(x_42, x_43, x_35);
x_45 = 1;
x_46 = l_Lean_Parser_mergeOrElseErrors(x_44, x_27, x_24, x_45);
@ -9162,7 +9170,7 @@ else
lean_object* x_47; lean_object* x_48; uint8_t x_49; lean_object* x_50;
lean_dec(x_39);
lean_dec(x_1);
x_47 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__1;
x_47 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__2;
x_48 = l_Lean_Parser_ParserState_mkNode(x_38, x_47, x_35);
x_49 = 1;
x_50 = l_Lean_Parser_mergeOrElseErrors(x_48, x_27, x_24, x_49);
@ -9189,7 +9197,7 @@ static lean_object* _init_l_Lean_Parser_Syntax_notFollowedBy___closed__1() {
_start:
{
lean_object* x_1; uint8_t x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__5;
x_1 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__6;
x_2 = 0;
x_3 = l_Lean_Parser_nonReservedSymbolInfo(x_1, x_2);
return x_3;
@ -9211,7 +9219,7 @@ static lean_object* _init_l_Lean_Parser_Syntax_notFollowedBy___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__1;
x_1 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__2;
x_2 = l_Lean_Parser_Syntax_notFollowedBy___closed__2;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
@ -9231,7 +9239,7 @@ static lean_object* _init_l_Lean_Parser_Syntax_notFollowedBy___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__3;
x_1 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__4;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Syntax_notFollowedBy___closed__4;
@ -9272,7 +9280,7 @@ _start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = l_Lean_Parser_categoryParserFnImpl___closed__4;
x_3 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__1;
x_3 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Syntax_notFollowedBy;
x_6 = lean_unsigned_to_nat(0u);
@ -9284,8 +9292,8 @@ static lean_object* _init_l_Lean_Parser_Syntax_notFollowedBy_formatter___closed_
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_1 = l_Lean_Parser_notFollowedByFn___closed__1;
x_2 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__2;
x_1 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__1;
x_2 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__3;
x_3 = 1;
x_4 = lean_box(x_3);
x_5 = lean_alloc_closure((void*)(l_Lean_Parser_mkAntiquot_formatter___boxed), 8, 3);
@ -9299,7 +9307,7 @@ static lean_object* _init_l_Lean_Parser_Syntax_notFollowedBy_formatter___closed_
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__4;
x_1 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__5;
x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_nonReservedSymbol_formatter___boxed), 6, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
@ -9321,7 +9329,7 @@ static lean_object* _init_l_Lean_Parser_Syntax_notFollowedBy_formatter___closed_
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__1;
x_1 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__2;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Syntax_notFollowedBy_formatter___closed__3;
x_4 = lean_alloc_closure((void*)(l_Lean_Parser_leadingNode_formatter___boxed), 8, 3);
@ -9354,7 +9362,7 @@ _start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_2 = l_Lean_PrettyPrinter_formatterAttribute;
x_3 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__1;
x_3 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__2;
x_4 = l___regBuiltin_Lean_Parser_Syntax_notFollowedBy_formatter___closed__1;
x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
@ -9364,7 +9372,7 @@ static lean_object* _init_l_Lean_Parser_Syntax_notFollowedBy_parenthesizer___clo
_start:
{
lean_object* x_1; uint8_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__2;
x_1 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__3;
x_2 = 1;
x_3 = lean_box(x_2);
x_4 = lean_alloc_closure((void*)(l_Lean_Parser_mkAntiquot_parenthesizer___rarg___boxed), 7, 2);
@ -9377,7 +9385,7 @@ static lean_object* _init_l_Lean_Parser_Syntax_notFollowedBy_parenthesizer___clo
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__1;
x_1 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__2;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Syntax_interpolatedStr_parenthesizer___closed__3;
x_4 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_leadingNode_parenthesizer___boxed), 8, 3);
@ -9410,7 +9418,7 @@ _start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_2 = l_Lean_PrettyPrinter_parenthesizerAttribute;
x_3 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__1;
x_3 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__2;
x_4 = l___regBuiltin_Lean_Parser_Syntax_notFollowedBy_parenthesizer___closed__1;
x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
@ -19041,7 +19049,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_antiquotNestedExpr_parenthesizer___closed__3;
x_2 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__2;
x_2 = l_Lean_Parser_Command_openHiding_parenthesizer___closed__2;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
@ -21693,7 +21701,7 @@ static lean_object* _init_l_Lean_Parser_Command_parserKindPrio_parenthesizer___c
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__3;
x_1 = l_Lean_Parser_Command_openHiding_parenthesizer___closed__3;
x_2 = l_Lean_Parser_Level_num_parenthesizer___closed__2;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 7, 2);
lean_closure_set(x_3, 0, x_1);
@ -21898,7 +21906,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Syntax_paren_parenthesizer___closed__3;
x_2 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__6;
x_2 = l_Lean_Parser_Command_namespace_parenthesizer___closed__2;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
@ -23388,7 +23396,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__2;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__6;
x_3 = l_Lean_Parser_Command_namespace_parenthesizer___closed__2;
x_4 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_leadingNode_parenthesizer___boxed), 8, 3);
lean_closure_set(x_4, 0, x_1);
lean_closure_set(x_4, 1, x_2);
@ -27314,7 +27322,7 @@ static lean_object* _init_l_Lean_Parser_Command_macroTailDefault_parenthesizer__
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__6;
x_1 = l_Lean_Parser_Command_namespace_parenthesizer___closed__2;
x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_try_parenthesizer), 6, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
@ -28591,7 +28599,7 @@ static lean_object* _init_l_Lean_Parser_Command_elab__rules_parenthesizer___clos
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__6;
x_1 = l_Lean_Parser_Command_namespace_parenthesizer___closed__2;
x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_optional_parenthesizer), 6, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
@ -31104,6 +31112,8 @@ l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__6 = _init_l_Lean_Parse
lean_mark_persistent(l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__6);
l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__7 = _init_l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__7();
lean_mark_persistent(l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__7);
l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__8 = _init_l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__8();
lean_mark_persistent(l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__8);
l_Lean_Parser_Syntax_notFollowedBy___closed__1 = _init_l_Lean_Parser_Syntax_notFollowedBy___closed__1();
lean_mark_persistent(l_Lean_Parser_Syntax_notFollowedBy___closed__1);
l_Lean_Parser_Syntax_notFollowedBy___closed__2 = _init_l_Lean_Parser_Syntax_notFollowedBy___closed__2();

522
stage0/stdlib/Lean/Parser/Tactic.c generated
View file

File diff suppressed because it is too large Load diff

12
stage0/stdlib/Lean/Parser/Term.c generated
View file

@ -293,6 +293,7 @@ lean_object* l_Lean_Parser_Term_namedArgument_formatter(lean_object*, lean_objec
lean_object* l_Lean_Parser_Term_structInstArrayRef___closed__4;
lean_object* l_Lean_Parser_Term_simpleBinder___closed__5;
extern lean_object* l_Lean_Parser_leadPrec;
lean_object* l_Lean_Parser_notFollowedByFn___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_funBinder_quot_parenthesizer___closed__5;
lean_object* l_Lean_Parser_Term_lt___elambda__1___closed__4;
lean_object* l_Lean_Parser_Term_funBinder_quot___closed__4;
@ -750,7 +751,6 @@ lean_object* l_Lean_Parser_Term_attributes___closed__7;
lean_object* l_Lean_Parser_Term_letPatDecl_parenthesizer___closed__5;
lean_object* l_Lean_Parser_Term_matchAlts_parenthesizer___closed__6;
lean_object* l_Lean_Parser_Term_nativeDecide___elambda__1___closed__2;
lean_object* l_Lean_Parser_notFollowedByFn(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_structInst___elambda__1___closed__12;
lean_object* l_Lean_Parser_Term_match__syntax___closed__3;
lean_object* l_Lean_Parser_Term_ensureExpectedType___closed__4;
@ -50632,11 +50632,13 @@ return x_2;
static lean_object* _init_l_Lean_Parser_Term_letDecl___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2;
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_letDecl___closed__2;
x_2 = lean_alloc_closure((void*)(l_Lean_Parser_notFollowedByFn), 3, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
x_2 = l_Lean_mkRecFor___closed__1;
x_3 = lean_alloc_closure((void*)(l_Lean_Parser_notFollowedByFn___boxed), 4, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Term_letDecl___closed__4() {

35
stage0/stdlib/Lean/PrettyPrinter/Formatter.c generated
View file

@ -218,6 +218,7 @@ lean_object* l_Lean_PrettyPrinter_Formatter_formatterForKind___closed__1;
lean_object* l_Lean_MonadTracer_trace___at_Lean_PrettyPrinter_Formatter_checkKind___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Formatter_quotedSymbol_formatter___closed__1;
lean_object* l_Lean_Syntax_MonadTraverser_goUp___at_Lean_PrettyPrinter_Formatter_visitArgs___spec__4___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Formatter_error_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_attrParamSyntaxToIdentifier(lean_object*);
uint8_t l_Lean_Syntax_structEq___main(lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Formatter_lookahead_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -229,6 +230,7 @@ uint8_t l_Array_isEqvAux___main___at_Lean_PrettyPrinter_Formatter_identNoAntiquo
lean_object* l_Lean_PrettyPrinter_Formatter_pushToken___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Substring_beq(lean_object*, lean_object*);
extern lean_object* l_String_Iterator_HasRepr___closed__2;
lean_object* l_Lean_PrettyPrinter_Formatter_error_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Formatter_checkTailWs_formatter(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_FileMap_ofString(lean_object*);
extern lean_object* l_Lean_Format_Inhabited;
@ -305,6 +307,7 @@ uint8_t l_String_isPrefixOf(lean_object*, lean_object*);
extern lean_object* l_Lean_ParserCompiler_CombinatorAttribute_Inhabited___closed__1;
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Formatter_symbol_formatter___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Formatter_error_formatter___rarg(lean_object*);
lean_object* l_Lean_PrettyPrinter_Formatter_pushToken(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadTracer_trace___at_Lean_PrettyPrinter_Formatter_checkKind___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getArgs(lean_object*);
@ -3698,6 +3701,38 @@ lean_dec(x_1);
return x_7;
}
}
lean_object* l_Lean_PrettyPrinter_Formatter_error_formatter___rarg(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = lean_box(0);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
return x_3;
}
}
lean_object* l_Lean_PrettyPrinter_Formatter_error_formatter(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6;
x_6 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_error_formatter___rarg), 1, 0);
return x_6;
}
}
lean_object* l_Lean_PrettyPrinter_Formatter_error_formatter___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6;
x_6 = l_Lean_PrettyPrinter_Formatter_error_formatter(x_1, x_2, x_3, x_4, x_5);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
return x_6;
}
}
lean_object* l_Lean_PrettyPrinter_Formatter_try_formatter(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{

35
stage0/stdlib/Lean/PrettyPrinter/Parenthesizer.c generated
View file

@ -161,6 +161,7 @@ lean_object* l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__4;
lean_object* l_Nat_forMAux___main___at_Lean_PrettyPrinter_Parenthesizer_parenthesizeCategoryCore___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___lambda__1___closed__5;
lean_object* l_Lean_PrettyPrinter_parenthesizerAttribute;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_error_parenthesizer___rarg(lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_setExpected_parenthesizer___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_Traverser_setCur(lean_object*, lean_object*);
extern lean_object* l_ULift_HasRepr___rarg___closed__2;
@ -284,6 +285,7 @@ lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute___lambda__1(uint8_t,
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkColGe_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_symbol_parenthesizer___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_fieldIdx_parenthesizer___boxed(lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_error_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkTailWs_parenthesizer___rarg(lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_ParenthesizerM_monadTraverser___closed__6;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_monadQuotation___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -460,6 +462,7 @@ lean_object* l_Lean_MonadTracer_trace___at_Lean_PrettyPrinter_Parenthesizer_mayb
lean_object* l_Lean_PrettyPrinter_Parenthesizer_strLitNoAntiquot_parenthesizer___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_level_parenthesizer___closed__1;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_identEq_parenthesizer___boxed(lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_error_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___lambda__3(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_parenthesize___closed__2;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_level_parenthesizer___closed__2;
@ -7137,6 +7140,38 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
}
}
lean_object* l_Lean_PrettyPrinter_Parenthesizer_error_parenthesizer___rarg(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = lean_box(0);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
return x_3;
}
}
lean_object* l_Lean_PrettyPrinter_Parenthesizer_error_parenthesizer(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6;
x_6 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_error_parenthesizer___rarg), 1, 0);
return x_6;
}
}
lean_object* l_Lean_PrettyPrinter_Parenthesizer_error_parenthesizer___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6;
x_6 = l_Lean_PrettyPrinter_Parenthesizer_error_parenthesizer(x_1, x_2, x_3, x_4, x_5);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
return x_6;
}
}
lean_object* l_Lean_PrettyPrinter_Parenthesizer_try_parenthesizer(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{