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-13 19:02:10 -07:00
parent 08061137a8
commit 6eaba0dc6f
5 changed files with 17310 additions and 17163 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

602
stage0/src/Lean/Elab/App.lean generated
View file

@ -7,13 +7,9 @@ import Lean.Util.FindMVar
import Lean.Elab.Term
import Lean.Elab.Binders
import Lean.Elab.SyntheticMVars
new_frontend
namespace Lean
namespace MonadResolveName end MonadResolveName -- Hack for old frontend
open MonadResolveName (getCurrNamespace getOpenDecls) -- HACK for old frontend
namespace Elab
namespace Term
namespace Lean.Elab.Term
open Meta
/--
@ -26,7 +22,7 @@ inductive Arg
instance Arg.inhabited : Inhabited Arg := ⟨Arg.stx (arbitrary _)⟩
instance Arg.hasToString : HasToString Arg :=
⟨fun arg => match arg with
⟨fun
| Arg.stx val => toString val
| Arg.expr val => toString val⟩
@ -43,12 +39,12 @@ instance NamedArg.inhabited : Inhabited NamedArg := ⟨{ name := arbitrary _, va
Add a new named argument to `namedArgs`, and throw an error if it already contains a named argument
with the same name. -/
def addNamedArg (namedArgs : Array NamedArg) (namedArg : NamedArg) : TermElabM (Array NamedArg) := do
when (namedArgs.any $ fun namedArg' => namedArg.name == namedArg'.name) $
throwError ("argument '" ++ toString namedArg.name ++ "' was already set");
if namedArgs.any (namedArg.name == ·.name) then
throwError! "argument '{namedArg.name}' was already set"
pure $ namedArgs.push namedArg
private def ensureArgType (f : Expr) (arg : Expr) (expectedType : Expr) : TermElabM Expr := do
argType ← inferType arg;
let argType ← inferType arg
ensureHasTypeAux expectedType argType arg f
/-
@ -58,27 +54,27 @@ ensureHasTypeAux expectedType argType arg f
abbrev coeFun {α : Sort u} {γ : α → Sort v} (a : α) [CoeFun α γ] : γ a
``` -/
private def tryCoeFun (α : Expr) (a : Expr) : TermElabM Expr := do
v ← mkFreshLevelMVar;
type ← mkArrow α (mkSort v);
γ ← mkFreshExprMVar type;
u ← getLevel α;
let coeFunInstType := mkAppN (Lean.mkConst `CoeFun [u, v]) #[α, γ];
mvar ← mkFreshExprMVar coeFunInstType MetavarKind.synthetic;
let mvarId := mvar.mvarId!;
synthesized ←
catch (withoutMacroStackAtErr $ synthesizeInstMVarCore mvarId)
(fun ex =>
match ex with
| Exception.error _ msg => throwError $ "function expected" ++ Format.line ++ msg
| _ => throwError "function expected");
let v ← mkFreshLevelMVar
let type ← mkArrow α (mkSort v)
let γ ← mkFreshExprMVar type
let u ← getLevel α
let coeFunInstType := mkAppN (Lean.mkConst `CoeFun [u, v]) #[α, γ]
let mvar ← mkFreshExprMVar coeFunInstType MetavarKind.synthetic
let mvarId := mvar.mvarId!
let synthesized ←
try
withoutMacroStackAtErr $ synthesizeInstMVarCore mvarId
catch
| Exception.error _ msg => throwError! "function expected\n{msg}"
| _ => throwError "function expected"
if synthesized then
pure $ mkAppN (Lean.mkConst `coeFun [u, v]) #[α, γ, a, mvar]
else
throwError "function expected"
def synthesizeAppInstMVars (instMVars : Array MVarId) : TermElabM Unit :=
instMVars.forM $ fun mvarId =>
unlessM (synthesizeInstMVarCore mvarId) $
def synthesizeAppInstMVars (instMVars : Array MVarId) : TermElabM Unit := do
for mvarId in instMVars do
unless (← synthesizeInstMVarCore mvarId) do
registerSyntheticMVarWithCurrRef mvarId SyntheticMVarKind.typeClass
namespace ElabAppArgs
@ -109,39 +105,39 @@ modify fun s => { s with instMVars := s.instMVars.push mvarId }
The ones that cannot be synthesized yet are registered.
Remark: we use this method before trying to apply coercions to function. -/
def synthesizeAppInstMVars : M Unit := do
s ← get;
let instMVars := s.instMVars;
modify fun s => { s with instMVars := #[] };
liftM $ Lean.Elab.Term.synthesizeAppInstMVars instMVars
let s ← get
let instMVars := s.instMVars
modify fun s => { s with instMVars := #[] }
Lean.Elab.Term.synthesizeAppInstMVars instMVars
/- fType may become a forallE after we synthesize pending metavariables. -/
private def synthesizePendingAndNormalizeFunType : M Unit := do
synthesizeAppInstMVars;
liftM $ synthesizeSyntheticMVars;
s ← get;
fType ← whnfForall s.fType;
synthesizeAppInstMVars
synthesizeSyntheticMVars
let s ← get
let fType ← whnfForall s.fType
match fType with
| Expr.forallE _ _ _ _ => modify fun s => { s with fType := fType }
| _ => do
f ← liftM $ tryCoeFun fType s.f;
fType ← inferType f;
| _ =>
let f ← tryCoeFun fType s.f
let fType ← inferType f
modify fun s => { s with f := f, fType := fType }
/- Normalize and return the function type. -/
private def normalizeFunType : M Expr := do
s ← get;
fType ← whnfForall s.fType;
modify fun s => { s with fType := fType };
let s ← get
let fType ← whnfForall s.fType
modify fun s => { s with fType := fType }
pure fType
/- Return the binder name at `fType`. This method assumes `fType` is a function type. -/
private def getBindingName : M Name := do s ← get; pure s.fType.bindingName!
private def getBindingName : M Name := do return (← get).fType.bindingName!
/- Return the next argument expected type. This method assumes `fType` is a function type. -/
private def getArgExpectedType : M Expr := do s ← get; pure s.fType.bindingDomain!
private def getArgExpectedType : M Expr := do return (← get).fType.bindingDomain!
def eraseNamedArgCore (namedArgs : List NamedArg) (binderName : Name) : List NamedArg :=
namedArgs.filter fun namedArg => namedArg.name != binderName
namedArgs.filter (·.name != binderName)
/- Remove named argument with name `binderName` from `namedArgs`. -/
def eraseNamedArg (binderName : Name) : M Unit :=
@ -149,7 +145,7 @@ modify fun s => { s with namedArgs := eraseNamedArgCore s.namedArgs binderName }
/- Return true if the next argument at `args` is of the form `_` -/
private def isNextArgHole : M Bool := do
s ← get;
let s ← get
match s.args with
| Arg.stx (Syntax.node `Lean.Parser.Term.hole _) :: _ => pure true
| _ => pure false
@ -164,27 +160,27 @@ modify fun s => { s with f := mkApp s.f arg, fType := s.fType.bindingBody!.insta
Elaborate the given `Arg` and add it to the result. See `addNewArg`.
Recall that, `Arg` may be wrapping an already elaborated `Expr`. -/
private def elabAndAddNewArg (arg : Arg) : M Unit := do
s ← get;
expectedType ← getArgExpectedType;
let s ← get
let expectedType ← getArgExpectedType
match arg with
| Arg.expr val => do
arg ← liftM $ ensureArgType s.f val expectedType;
| Arg.expr val =>
let arg ← ensureArgType s.f val expectedType
addNewArg arg
| Arg.stx val => do
val ← liftM $ elabTerm val expectedType;
arg ← liftM $ ensureArgType s.f val expectedType;
| Arg.stx val =>
let val ← elabTerm val expectedType
let arg ← ensureArgType s.f val expectedType
addNewArg arg
/- Return true if the given type contains `OptParam` or `AutoParams` -/
private def hasOptAutoParams (type : Expr) : M Bool := do
forallTelescopeReducing type fun xs type =>
xs.anyM fun x => do
xType ← inferType x;
let xType ← inferType x
pure $ xType.getOptParamDefault?.isSome || xType.getAutoParamTactic?.isSome
/- Return true if `fType` contains `OptParam` or `AutoParams` -/
private def fTypeHasOptAutoParams : M Bool := do
s ← get;
let s ← get
hasOptAutoParams s.fType
/- Auxiliary function for retrieving the resulting type of a function application.
@ -253,106 +249,99 @@ private partial def getForallBody : Nat → List NamedArg → Expr → Option Ex
`bv 64` is **not** definitionally equal to `bv 32`.
-/
private def propagateExpectedType : M Unit := do
s ← get;
let s ← get
-- TODO: handle s.etaArgs.size > 0
unless (s.explicit || !s.etaArgs.isEmpty || s.alreadyPropagated || s.typeMVars.isEmpty) $ do
modify fun s => { s with alreadyPropagated := true };
unless s.explicit || !s.etaArgs.isEmpty || s.alreadyPropagated || s.typeMVars.isEmpty do
modify fun s => { s with alreadyPropagated := true }
match s.expectedType? with
| none => pure ()
| some expectedType => do
let numRemainingArgs := s.args.length;
trace `Elab.app.propagateExpectedType fun _ =>
"etaArgs.size: " ++ toString s.etaArgs.size ++ ", numRemainingArgs: " ++ toString numRemainingArgs ++ ", fType: " ++ s.fType;
| some expectedType =>
let numRemainingArgs := s.args.length
trace[Elab.app.propagateExpectedType]! "etaArgs.size: {s.etaArgs.size}, numRemainingArgs: {numRemainingArgs}, fType: {s.fType}"
match getForallBody numRemainingArgs s.namedArgs s.fType with
| none => pure ()
| some fTypeBody =>
unless fTypeBody.hasLooseBVars do
let hasTypeMVar := (fTypeBody.findMVar? fun mvarId => s.typeMVars.contains mvarId).isSome;
let hasOnlyTypeMVar := (fTypeBody.findMVar? fun mvarId => !s.typeMVars.contains mvarId).isNone;
when (hasTypeMVar && hasOnlyTypeMVar) $
unlessM (hasOptAutoParams fTypeBody) do
trace `Elab.app.propagateExpectedType fun _ => expectedType ++ " =?= " ++ fTypeBody;
isDefEq expectedType fTypeBody;
let hasTypeMVar := (fTypeBody.findMVar? fun mvarId => s.typeMVars.contains mvarId).isSome
let hasOnlyTypeMVar := (fTypeBody.findMVar? fun mvarId => !s.typeMVars.contains mvarId).isNone
if hasTypeMVar && hasOnlyTypeMVar then
unless (← hasOptAutoParams fTypeBody) do
trace[Elab.app.propagateExpectedType]! "{expectedType} =?= {fTypeBody}"
isDefEq expectedType fTypeBody
pure ()
/-
Create a fresh local variable with the current binder name and argument type, add it to `etaArgs` and `f`,
and then execute the continuation `k`.-/
private def addEtaArg (k : Unit → M Expr) : M Expr := do
n ← getBindingName;
type ← getArgExpectedType;
let n ← getBindingName
let type ← getArgExpectedType
withLocalDeclD n type fun x => do
modify fun s => { s with etaArgs := s.etaArgs.push x };
addNewArg x;
modify fun s => { s with etaArgs := s.etaArgs.push x }
addNewArg x
k ()
/- This method execute after all application arguments have been processed. -/
private def finalize : M Expr := do
s ← get;
let e := s.f;
let eType := s.fType;
let s ← get
let e := s.f
let eType := s.fType
-- all user explicit arguments have been consumed
trace `Elab.app.finalize $ fun _ => e;
ref ← getRef;
trace[Elab.app.finalize]! e
let ref ← getRef
-- Register the error context of implicits
s.toSetErrorCtx.forM fun mvarId => liftM $ registerMVarErrorImplicitArgInfo mvarId ref e;
(e, eType) ←
if s.etaArgs.isEmpty then
pure (e, eType)
else do {
e ← mkLambdaFVars s.etaArgs e;
eType ← inferType e;
pure (e, eType)
};
trace `Elab.app.finalize $ fun _ => "after etaArgs: " ++ e ++ " : " ++ eType;
for mvarId in s.toSetErrorCtx do
registerMVarErrorImplicitArgInfo mvarId ref e
if !s.etaArgs.isEmpty then
e ← mkLambdaFVars s.etaArgs e
eType ← inferType e
trace[Elab.app.finalize]! "after etaArgs, {e} : {eType}"
match s.expectedType? with
| none => pure ()
| some expectedType => do {
trace `Elab.app.finalize $ fun _ => "expected type: " ++ expectedType;
| some expectedType =>
trace[Elab.app.finalize]! "expected type: {expectedType}"
-- Try to propagate expected type. Ignore if types are not definitionally equal, caller must handle it.
isDefEq expectedType eType;
isDefEq expectedType eType
pure ()
};
synthesizeAppInstMVars;
synthesizeAppInstMVars
pure e
/-
Process a `fType` of the form `(x : A) → B x`.
This method assume `fType` is a function type -/
private def processExplictArg (k : Unit → M Expr) : M Expr := do
s ← get;
let s ← get
match s.args with
| arg::args => do
propagateExpectedType;
modify fun s => { s with args := args };
elabAndAddNewArg arg;
| arg::args =>
propagateExpectedType
modify fun s => { s with args := args }
elabAndAddNewArg arg
k ()
| _ => do
argType ← getArgExpectedType;
| _ =>
let argType ← getArgExpectedType
match s.explicit, argType.getOptParamDefault?, argType.getAutoParamTactic? with
| false, some defVal, _ => do addNewArg defVal; k()
| false, _, some (Expr.const tacticDecl _ _) => do
env ← getEnv;
| false, some defVal, _ => addNewArg defVal; k ()
| false, _, some (Expr.const tacticDecl _ _) =>
let env ← getEnv
match evalSyntaxConstant env tacticDecl with
| Except.error err => throwError err
| Except.ok tacticSyntax => do
tacticBlock ← `(by { $(tacticSyntax.getArgs)* });
| Except.ok tacticSyntax =>
let tacticBlock ← `(by { $(tacticSyntax.getArgs)* })
-- tacticBlock does not have any position information.
-- So, we use the current ref
ref ← getRef;
let tacticBlock := tacticBlock.copyInfo ref;
let argType := argType.getArg! 0; -- `autoParam type := by tactic` ==> `type`
propagateExpectedType;
elabAndAddNewArg (Arg.stx tacticBlock);
let ref ← getRef
let tacticBlock := tacticBlock.copyInfo ref
let argType := argType.getArg! 0 -- `autoParam type := by tactic` ==> `type`
propagateExpectedType
elabAndAddNewArg (Arg.stx tacticBlock)
k ()
| false, _, some _ =>
throwError "invalid autoParam, argument must be a constant"
| _, _, _ =>
if !s.namedArgs.isEmpty then do
if !s.namedArgs.isEmpty then
addEtaArg k
else if !s.explicit then do
hasOptAuto ← fTypeHasOptAutoParams;
if hasOptAuto then
else if !s.explicit then
if (← fTypeHasOptAutoParams) then
addEtaArg k
else
finalize
@ -363,64 +352,67 @@ match s.args with
Process a `fType` of the form `{x : A} → B x`.
This method assume `fType` is a function type -/
private def processImplicitArg (k : Unit → M Expr) : M Expr := do
s ← get;
let s ← get
if s.explicit then
processExplictArg k
else do
argType ← getArgExpectedType;
arg ← mkFreshExprMVar argType;
whenM (isTypeFormer arg) $
modify fun s => { s with typeMVars := s.typeMVars.push arg.mvarId!, toSetErrorCtx := s.toSetErrorCtx.push arg.mvarId! };
addNewArg arg;
else
let argType ← getArgExpectedType
let arg ← mkFreshExprMVar argType
if (← isTypeFormer arg) then
modify fun s => { s with typeMVars := s.typeMVars.push arg.mvarId!, toSetErrorCtx := s.toSetErrorCtx.push arg.mvarId! }
addNewArg arg
k ()
/-
Process a `fType` of the form `[x : A] → B x`.
This method assume `fType` is a function type -/
private def processInstImplicitArg (k : Unit → M Expr) : M Expr := do
s ← get;
argType ← getArgExpectedType;
if s.explicit then do
isHole ← isNextArgHole;
if isHole then do
let s ← get
let argType ← getArgExpectedType
if s.explicit then
let isHole ← isNextArgHole
if isHole then
/- Recall that if '@' has been used, and the argument is '_', then we still use type class resolution -/
arg ← mkFreshExprMVar argType MetavarKind.synthetic;
modify fun s => { s with args := s.args.tail! };
addInstMVar arg.mvarId!;
addNewArg arg;
let arg ← mkFreshExprMVar argType MetavarKind.synthetic
modify fun s => { s with args := s.args.tail! }
addInstMVar arg.mvarId!
addNewArg arg
k ()
else
processExplictArg k
else do
arg ← mkFreshExprMVar argType MetavarKind.synthetic;
addInstMVar arg.mvarId!;
addNewArg arg;
else
let arg ← mkFreshExprMVar argType MetavarKind.synthetic
addInstMVar arg.mvarId!
addNewArg arg
k ()
/- Return true if there are regular or named arguments to be processed. -/
private def hasArgsToProcess : M Bool := do
s ← get;
let s ← get
pure $ !s.args.isEmpty || !s.namedArgs.isEmpty
/- Elaborate function application arguments. -/
partial def main : Unit → M Expr
| _ => do
s ← get;
fType ← normalizeFunType;
let s ← get
let fType ← normalizeFunType
match fType with
| Expr.forallE binderName _ _ c => do
s ← get;
| Expr.forallE binderName _ _ c =>
let s ← get
match s.namedArgs.find? fun (namedArg : NamedArg) => namedArg.name == binderName with
| some namedArg => do propagateExpectedType; eraseNamedArg binderName; elabAndAddNewArg namedArg.val; main()
| none => do
| some namedArg =>
propagateExpectedType
eraseNamedArg binderName
elabAndAddNewArg namedArg.val
main ()
| none =>
match c.binderInfo with
| BinderInfo.implicit => processImplicitArg main
| BinderInfo.instImplicit => processInstImplicitArg main
| _ => processExplictArg main
| _ => do
cont ← hasArgsToProcess;
if cont then do
synthesizePendingAndNormalizeFunType;
| _ =>
if (← hasArgsToProcess) then
synthesizePendingAndNormalizeFunType
main ()
else
finalize
@ -429,11 +421,11 @@ end ElabAppArgs
private def elabAppArgs (f : Expr) (namedArgs : Array NamedArg) (args : Array Arg)
(expectedType? : Option Expr) (explicit : Bool) : TermElabM Expr := do
fType ← inferType f;
fType ← instantiateMVars fType;
trace `Elab.app.args $ fun _ => "explicit: " ++ toString explicit ++ ", " ++ f ++ " : " ++ fType;
unless (namedArgs.isEmpty && args.isEmpty) $
tryPostponeIfMVar fType;
let fType ← inferType f
let fType ← instantiateMVars fType
trace[Elab.app.args]! "explicit: {explicit}, {f} : {fType}"
unless namedArgs.isEmpty && args.isEmpty do
tryPostponeIfMVar fType
(ElabAppArgs.main ()).run' { args := args.toList, expectedType? := expectedType?, explicit := explicit, namedArgs := namedArgs.toList, f := f, fType := fType }
/-- Auxiliary inductive datatype that represents the resolution of an `LVal`. -/
@ -445,7 +437,7 @@ inductive LValResolution
| getOp (fullName : Name) (idx : Syntax)
private def throwLValError {α} (e : Expr) (eType : Expr) (msg : MessageData) : TermElabM α :=
throwError $ msg ++ indentExpr e ++ Format.line ++ "has type" ++ indentExpr eType
throwError! "{msg}{indentExpr e}\nhas type{indentExpr eType}"
/-- `findMethod? env S fName`.
1- If `env` contains `S ++ fName`, return `(S, S++fName)`
@ -453,28 +445,28 @@ throwError $ msg ++ indentExpr e ++ Format.line ++ "has type" ++ indentExpr eTyp
3- Otherwise for each parent structure `S'` of `S`, we try `findMethod? env S' fname` -/
private partial def findMethod? (env : Environment) : Name → Name → Option (Name × Name)
| structName, fieldName =>
let fullName := structName ++ fieldName;
let fullName := structName ++ fieldName
match env.find? fullName with
| some _ => some (structName, fullName)
| none =>
let fullNamePrv := mkPrivateName env fullName;
let fullNamePrv := mkPrivateName env fullName
match env.find? fullNamePrv with
| some _ => some (structName, fullNamePrv)
| none =>
if isStructureLike env structName then
(getParentStructures env structName).findSome? fun parentStructName => findMethod? parentStructName fieldName
(getParentStructures env structName).findSome? fun parentStructName => findMethod? env parentStructName fieldName
else
none
private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM LValResolution :=
private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM LValResolution := do
match eType.getAppFn, lval with
| Expr.const structName _ _, LVal.fieldIdx idx => do
when (idx == 0) $
throwError "invalid projection, index must be greater than 0";
env ← getEnv;
unless (isStructureLike env structName) $
throwLValError e eType "invalid projection, structure expected";
let fieldNames := getStructureFields env structName;
| Expr.const structName _ _, LVal.fieldIdx idx =>
if idx == 0 then
throwError "invalid projection, index must be greater than 0"
let env ← getEnv
unless isStructureLike env structName do
throwLValError e eType "invalid projection, structure expected"
let fieldNames := getStructureFields env structName
if h : idx - 1 < fieldNames.size then
if isStructure env structName then
pure $ LValResolution.projFn structName structName (fieldNames.get ⟨idx - 1, h⟩)
@ -483,21 +475,20 @@ match eType.getAppFn, lval with
So, we don't projection functions for it. Thus, we use `Expr.proj` -/
pure $ LValResolution.projIdx structName (idx - 1)
else
throwLValError e eType ("invalid projection, structure has only " ++ toString fieldNames.size ++ " field(s)")
| Expr.const structName _ _, LVal.fieldName fieldName => do
env ← getEnv;
let searchEnv : Unit → TermElabM LValResolution := fun _ => do {
match findMethod? env structName fieldName with
throwLValError e eType msg!"invalid projection, structure has only {fieldNames.size} field(s)"
| Expr.const structName _ _, LVal.fieldName fieldName =>
let env ← getEnv
let searchEnv : Unit → TermElabM LValResolution := fun _ => do
match findMethod? env structName (mkNameSimple fieldName) with
| some (baseStructName, fullName) => pure $ LValResolution.const baseStructName structName fullName
| none => throwLValError e eType $
"invalid field notation, '" ++ fieldName ++ "' is not a valid \"field\" because environment does not contain '" ++ (structName ++ fieldName : Name) ++ "'"
};
| none =>
throwLValError e eType msg!"invalid field notation, '{fieldName}' is not a valid \"field\" because environment does not contain '{mkNameStr structName fieldName}'"
-- search local context first, then environment
let searchCtx : Unit → TermElabM LValResolution := fun _ => do {
let fullName := structName ++ fieldName;
currNamespace ← getCurrNamespace;
let localName := fullName.replacePrefix currNamespace Name.anonymous;
lctx ← getLCtx;
let searchCtx : Unit → TermElabM LValResolution := fun _ => do
let fullName := mkNameStr structName fieldName
let currNamespace ← getCurrNamespace
let localName := fullName.replacePrefix currNamespace Name.anonymous
let lctx ← getLCtx
match lctx.findFromUserName? localName with
| some localDecl =>
if localDecl.binderInfo == BinderInfo.auxDecl then
@ -506,19 +497,18 @@ match eType.getAppFn, lval with
else
searchEnv ()
| none => searchEnv ()
};
if isStructure env structName then
match findField? env structName fieldName with
| some baseStructName => pure $ LValResolution.projFn baseStructName structName fieldName
match findField? env structName (mkNameSimple fieldName) with
| some baseStructName => pure $ LValResolution.projFn baseStructName structName (mkNameSimple fieldName)
| none => searchCtx ()
else
searchCtx ()
| Expr.const structName _ _, LVal.getOp idx => do
env ← getEnv;
let fullName := mkNameStr structName "getOp";
| Expr.const structName _ _, LVal.getOp idx =>
let env ← getEnv
let fullName := mkNameStr structName "getOp"
match env.find? fullName with
| some _ => pure $ LValResolution.getOp fullName idx
| none => throwLValError e eType $ "invalid [..] notation because environment does not contain '" ++ fullName ++ "'"
| none => throwLValError e eType msg!"invalid [..] notation because environment does not contain '{fullName}'"
| _, LVal.getOp idx =>
throwLValError e eType "invalid [..] notation, type is not of the form (C ...) where C is a constant"
| _, _ =>
@ -528,11 +518,11 @@ match eType.getAppFn, lval with
Example: given `e` with `eType := {α : Type} → (fun β => List β) α `, it produces `(e ?m, List ?m)` where `?m` is fresh metavariable. -/
private partial def consumeImplicits : Expr → Expr → TermElabM (Expr × Expr)
| e, eType => do
eType ← whnfCore eType;
let eType ← whnfCore eType
match eType with
| Expr.forallE n d b c =>
if !c.binderInfo.isExplicit then do
mvar ← mkFreshExprMVar d;
if !c.binderInfo.isExplicit then
let mvar ← mkFreshExprMVar d
consumeImplicits (mkApp e mvar) (b.instantiate1 mvar)
else match d.getOptParamDefault? with
| some defVal => consumeImplicits (mkApp e defVal) (b.instantiate1 defVal)
@ -542,35 +532,34 @@ private partial def consumeImplicits : Expr → Expr → TermElabM (Expr × Expr
private partial def resolveLValLoop (lval : LVal) : Expr → Expr → Array Exception → TermElabM (Expr × LValResolution)
| e, eType, previousExceptions => do
(e, eType) ← consumeImplicits e eType;
tryPostponeIfMVar eType;
let (e, eType) ← consumeImplicits e eType
tryPostponeIfMVar eType
try
let lvalRes ← resolveLValAux e eType lval
pure (e, lvalRes)
catch
(do lvalRes ← resolveLValAux e eType lval; pure (e, lvalRes))
(fun ex =>
match ex with
| Exception.error _ _ => do
eType? ← unfoldDefinition? eType;
match eType? with
| some eType => resolveLValLoop e eType (previousExceptions.push ex)
| none => do
previousExceptions.forM $ fun ex => logException ex;
throw ex
| Exception.internal _ => throw ex)
| ex@(Exception.error _ _) =>
let eType? ← unfoldDefinition? eType
match eType? with
| some eType => resolveLValLoop lval e eType (previousExceptions.push ex)
| none =>
previousExceptions.forM fun ex => logException ex
throw ex
| ex@(Exception.internal _) => throw ex
private def resolveLVal (e : Expr) (lval : LVal) : TermElabM (Expr × LValResolution) := do
eType ← inferType e;
let eType ← inferType e
resolveLValLoop lval e eType #[]
private partial def mkBaseProjections (baseStructName : Name) (structName : Name) (e : Expr) : TermElabM Expr := do
env ← getEnv;
let env ← getEnv
match getPathToBaseStructure? env baseStructName structName with
| none => throwError "failed to access field in parent structure"
| some path =>
path.foldlM
(fun e projFunName => do
projFn ← mkConst projFunName;
elabAppArgs projFn #[{ name := `self, val := Arg.expr e }] #[] none false)
e
for projFunName in path do
let projFn ← mkConst projFunName
e ← elabAppArgs projFn #[{ name := `self, val := Arg.expr e }] (args := #[]) (expectedType? := none) (explicit := false)
return e
/- Auxiliary method for field notation. It tries to add `e` to `args` as the first explicit parameter
which takes an element of type `(C ...)` where `C` is `baseName`.
@ -578,81 +567,79 @@ match getPathToBaseStructure? env baseStructName structName with
private def addLValArg (baseName : Name) (fullName : Name) (e : Expr) (args : Array Arg) : Nat → Array NamedArg → Expr → TermElabM (Array Arg)
| i, namedArgs, Expr.forallE n d b c =>
if !c.binderInfo.isExplicit then
addLValArg i namedArgs b
addLValArg baseName fullName e args i namedArgs b
else
/- If there is named argument with name `n`, then we should skip. -/
match namedArgs.findIdx? (fun namedArg => namedArg.name == n) with
| some idx => do
let namedArgs := namedArgs.eraseIdx idx;
addLValArg i namedArgs b
let namedArgs := namedArgs.eraseIdx idx
addLValArg baseName fullName e args i namedArgs b
| none => do
if d.consumeMData.isAppOf baseName then
pure $ args.insertAt i (Arg.expr e)
else if i < args.size then
addLValArg (i+1) namedArgs b
addLValArg baseName fullName e args (i+1) namedArgs b
else
throwError $ "invalid field notation, insufficient number of arguments for '" ++ fullName ++ "'"
throwError! "invalid field notation, insufficient number of arguments for '{fullName}'"
| _, _, fType =>
throwError $
"invalid field notation, function '" ++ fullName ++ "' does not have explicit argument with type (" ++ baseName ++ " ...)"
throwError! "invalid field notation, function '{fullName}' does not have explicit argument with type ({baseName} ...)"
private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (expectedType? : Option Expr) (explicit : Bool)
: Expr → List LVal → TermElabM Expr
(f : Expr) (lvals : List LVal) : TermElabM Expr :=
let rec loop : Expr → List LVal → TermElabM Expr
| f, [] => elabAppArgs f namedArgs args expectedType? explicit
| f, lval::lvals => do
(f, lvalRes) ← resolveLVal f lval;
let (f, lvalRes) ← resolveLVal f lval
match lvalRes with
| LValResolution.projIdx structName idx =>
let f := mkProj structName idx f;
elabAppLValsAux f lvals
| LValResolution.projFn baseStructName structName fieldName => do
f ← mkBaseProjections baseStructName structName f;
projFn ← mkConst (baseStructName ++ fieldName);
if lvals.isEmpty then do
namedArgs ← addNamedArg namedArgs { name := `self, val := Arg.expr f };
let f := mkProj structName idx f
loop f lvals
| LValResolution.projFn baseStructName structName fieldName =>
let f ← mkBaseProjections baseStructName structName f
let projFn ← mkConst (baseStructName ++ fieldName)
if lvals.isEmpty then
let namedArgs ← addNamedArg namedArgs { name := `self, val := Arg.expr f }
elabAppArgs projFn namedArgs args expectedType? explicit
else do
f ← elabAppArgs projFn #[{ name := `self, val := Arg.expr f }] #[] none false;
elabAppLValsAux f lvals
| LValResolution.const baseStructName structName constName => do
f ← if baseStructName != structName then mkBaseProjections baseStructName structName f else pure f;
projFn ← mkConst constName;
if lvals.isEmpty then do
projFnType ← inferType projFn;
args ← addLValArg baseStructName constName f args 0 namedArgs projFnType;
else
let f ← elabAppArgs projFn #[{ name := `self, val := Arg.expr f }] #[] (expectedType? := none) (explicit := false)
loop f lvals
| LValResolution.const baseStructName structName constName =>
let f ← if baseStructName != structName then mkBaseProjections baseStructName structName f else pure f
let projFn ← mkConst constName
if lvals.isEmpty then
let projFnType ← inferType projFn
let args ← addLValArg baseStructName constName f args 0 namedArgs projFnType
elabAppArgs projFn namedArgs args expectedType? explicit
else do
f ← elabAppArgs projFn #[] #[Arg.expr f] none false;
elabAppLValsAux f lvals
else
let f ← elabAppArgs projFn #[] #[Arg.expr f] (expectedType? := none) (explicit := false)
loop f lvals
| LValResolution.localRec baseName fullName fvar =>
if lvals.isEmpty then do
fvarType ← inferType fvar;
args ← addLValArg baseName fullName f args 0 namedArgs fvarType;
if lvals.isEmpty then
let fvarType ← inferType fvar
let args ← addLValArg baseName fullName f args 0 namedArgs fvarType
elabAppArgs fvar namedArgs args expectedType? explicit
else do
f ← elabAppArgs fvar #[] #[Arg.expr f] none false;
elabAppLValsAux f lvals
| LValResolution.getOp fullName idx => do
getOpFn ← mkConst fullName;
if lvals.isEmpty then do
namedArgs ← addNamedArg namedArgs { name := `self, val := Arg.expr f };
namedArgs ← addNamedArg namedArgs { name := `idx, val := Arg.stx idx };
else
let f ← elabAppArgs fvar #[] #[Arg.expr f] (expectedType? := none) (explicit := false)
loop f lvals
| LValResolution.getOp fullName idx =>
let getOpFn ← mkConst fullName
if lvals.isEmpty then
let namedArgs ← addNamedArg namedArgs { name := `self, val := Arg.expr f }
let namedArgs ← addNamedArg namedArgs { name := `idx, val := Arg.stx idx }
elabAppArgs getOpFn namedArgs args expectedType? explicit
else do
f ← elabAppArgs getOpFn #[{ name := `self, val := Arg.expr f }, { name := `idx, val := Arg.stx idx }] #[] none false;
elabAppLValsAux f lvals
else
let f ← elabAppArgs getOpFn #[{ name := `self, val := Arg.expr f }, { name := `idx, val := Arg.stx idx }] #[] (expectedType? := none) (explicit := false)
loop f lvals
loop f lvals
private def elabAppLVals (f : Expr) (lvals : List LVal) (namedArgs : Array NamedArg) (args : Array Arg)
(expectedType? : Option Expr) (explicit : Bool) : TermElabM Expr := do
when (!lvals.isEmpty && explicit) $ throwError "invalid use of field notation with `@` modifier";
if !lvals.isEmpty && explicit then
throwError "invalid use of field notation with `@` modifier"
elabAppLValsAux namedArgs args expectedType? explicit f lvals
def elabExplicitUnivs (lvls : Array Syntax) : TermElabM (List Level) := do
lvls.foldrM
(fun stx lvls => do
lvl ← elabLevel stx;
pure (lvl::lvls))
[]
lvls.foldrM (fun stx lvls => do pure ((← elabLevel stx)::lvls)) []
/-
Interaction between `errToSorry` and `observing`.
@ -677,20 +664,19 @@ false, no elaboration function executed by `x` will reset it to
private partial def elabAppFnId (fIdent : Syntax) (fExplicitUnivs : List Level) (lvals : List LVal)
(namedArgs : Array NamedArg) (args : Array Arg) (expectedType? : Option Expr) (explicit : Bool) (overloaded : Bool) (acc : Array TermElabResult)
: TermElabM (Array TermElabResult) :=
: TermElabM (Array TermElabResult) := do
match fIdent with
| Syntax.ident _ _ n preresolved => do
funLVals ← withRef fIdent $ resolveName n preresolved fExplicitUnivs;
let overloaded := overloaded || funLVals.length > 1;
| Syntax.ident _ _ n preresolved =>
let funLVals ← withRef fIdent $ resolveName n preresolved fExplicitUnivs
let overloaded := overloaded || funLVals.length > 1
-- Set `errToSorry` to `false` if `funLVals` > 1. See comment above about the interaction between `errToSorry` and `observing`.
withReader (fun ctx => { ctx with errToSorry := funLVals.length == 1 && ctx.errToSorry }) $
withReader (fun ctx => { ctx with errToSorry := funLVals.length == 1 && ctx.errToSorry }) do
funLVals.foldlM
(fun acc ⟨f, fields⟩ => do
let lvals' := fields.map LVal.fieldName;
s ← observing do {
e ← elabAppLVals f (lvals' ++ lvals) namedArgs args expectedType? explicit;
let lvals' := fields.map LVal.fieldName
let s ← observing do
let e ← elabAppLVals f (lvals' ++ lvals) namedArgs args expectedType? explicit
if overloaded then ensureHasType expectedType? e else pure e
};
pure $ acc.push s)
acc
| _ => throwUnsupportedSyntax
@ -703,13 +689,13 @@ private partial def elabAppFn : Syntax → List LVal → Array NamedArg → Arra
f.getArgs.foldlM (fun acc f => elabAppFn f lvals namedArgs args expectedType? explicit true acc) acc
else match_syntax f with
| `($(e).$idx:fieldIdx) =>
let idx := idx.isFieldIdx?.get!;
let idx := idx.isFieldIdx?.get!
elabAppFn e (LVal.fieldIdx idx :: lvals) namedArgs args expectedType? explicit overloaded acc
| `($e $.$field) => do
f ← `($(e).$field);
let f ← `($(e).$field)
elabAppFn f lvals namedArgs args expectedType? explicit overloaded acc
| `($(e).$field:ident) =>
let newLVals := field.getId.eraseMacroScopes.components.map (fun n => LVal.fieldName (toString n));
let newLVals := field.getId.eraseMacroScopes.components.map (fun n => LVal.fieldName (toString n))
elabAppFn e (newLVals ++ lvals) namedArgs args expectedType? explicit overloaded acc
| `($e[$idx]) =>
elabAppFn e (LVal.getOp idx :: lvals) namedArgs args expectedType? explicit overloaded acc
@ -718,7 +704,7 @@ private partial def elabAppFn : Syntax → List LVal → Array NamedArg → Arra
| `($id:ident) => do
elabAppFnId id [] lvals namedArgs args expectedType? explicit overloaded acc
| `($id:ident.{$us*}) => do
us ← elabExplicitUnivs us.getSepElems;
let us ← elabExplicitUnivs us.getSepElems
elabAppFnId id us lvals namedArgs args expectedType? explicit overloaded acc
| `(@$id:ident) =>
elabAppFn id lvals namedArgs args expectedType? true overloaded acc
@ -727,24 +713,23 @@ private partial def elabAppFn : Syntax → List LVal → Array NamedArg → Arra
| `(@$t) => throwUnsupportedSyntax -- invalid occurrence of `@`
| `(_) => throwError "placeholders '_' cannot be used where a function is expected"
| _ =>
let catchPostpone := !overloaded;
let catchPostpone := !overloaded
/- If we are processing a choice node, then we should use `catchPostpone == false` when elaborating terms.
Recall that `observing` does not catch `postponeExceptionId`. -/
if lvals.isEmpty && namedArgs.isEmpty && args.isEmpty then do
/- Recall that elabAppFn is used for elaborating atomics terms **and** choice nodes that may contain
arbitrary terms. If they are not being used as a function, we should elaborate using the expectedType. -/
s ←
let s ←
if overloaded then
observing $ elabTermEnsuringType f expectedType? catchPostpone
else
observing $ elabTerm f expectedType?;
observing $ elabTerm f expectedType?
pure $ acc.push s
else do
s ← observing do {
f ← elabTerm f none catchPostpone;
e ← elabAppLVals f lvals namedArgs args expectedType? explicit;
let s ← observing do
let f ← elabTerm f none catchPostpone
let e ← elabAppLVals f lvals namedArgs args expectedType? explicit
if overloaded then ensureHasType expectedType? e else pure e
};
pure $ acc.push s
private def isSuccess (candidate : TermElabResult) : Bool :=
@ -756,77 +741,77 @@ private def getSuccess (candidates : Array TermElabResult) : Array TermElabResul
candidates.filter isSuccess
private def toMessageData (ex : Exception) : TermElabM MessageData := do
pos ← getRefPos;
let pos ← getRefPos
match ex.getRef.getPos with
| none => pure ex.toMessageData
| some exPos =>
if pos == exPos then
pure ex.toMessageData
else do
fileMap ← MonadLog.getFileMap; -- Remove `MonadLog.` it is a workaround for old frontend
let exPosition := fileMap.toPosition exPos;
pure $ toString exPosition.line ++ ":" ++ toString exPosition.column ++ " " ++ ex.toMessageData
else
let fileMap ← MonadLog.getFileMap -- Remove `MonadLog.` it is a workaround for old frontend
let exPosition := fileMap.toPosition exPos
pure msg!"{exPosition.line}:{exPosition.column} {ex.toMessageData}"
private def toMessageList (msgs : Array MessageData) : MessageData :=
indentD (MessageData.joinSep msgs.toList (Format.line ++ Format.line))
private def mergeFailures {α} (failures : Array TermElabResult) : TermElabM α := do
msgs ← failures.mapM $ fun failure =>
let msgs ← failures.mapM fun failure =>
match failure with
| EStateM.Result.ok _ _ => unreachable!
| EStateM.Result.error ex _ => toMessageData ex;
throwError ("overloaded, errors " ++ toMessageList msgs)
| EStateM.Result.error ex _ => toMessageData ex
throwError! "overloaded, errors {toMessageList msgs}"
private def elabAppAux (f : Syntax) (namedArgs : Array NamedArg) (args : Array Arg) (expectedType? : Option Expr) : TermElabM Expr := do
let explicit := false;
let overloaded := false;
candidates ← elabAppFn f [] namedArgs args expectedType? explicit overloaded #[];
let explicit := false
let overloaded := false
let candidates ← elabAppFn f [] namedArgs args expectedType? explicit overloaded #[]
if candidates.size == 1 then
applyResult $ candidates.get! 0
applyResult candidates[0]
else
let successes := getSuccess candidates;
if successes.size == 1 then do
e ← applyResult $ successes.get! 0;
let successes := getSuccess candidates
if successes.size == 1 then
let e ← applyResult successes[0]
pure e
else if successes.size > 1 then do
lctx ← getLCtx;
opts ← getOptions;
let msgs : Array MessageData := successes.map $ fun success => match success with
else if successes.size > 1 then
let lctx ← getLCtx
let opts ← getOptions
let msgs : Array MessageData := successes.map fun success => match success with
| EStateM.Result.ok e s => MessageData.withContext { env := s.core.env, mctx := s.meta.mctx, lctx := lctx, opts := opts } e
| _ => unreachable!;
| _ => unreachable!
throwErrorAt f ("ambiguous, possible interpretations " ++ toMessageList msgs)
else
withRef f $ mergeFailures candidates
partial def expandApp (stx : Syntax) (pattern := false) : TermElabM (Syntax × Array NamedArg × Array Arg × Bool) := do
let f := stx.getArg 0;
let args := (stx.getArg 1).getArgs;
let f := stx[0]
let args := stx[1].getArgs
let (args, ellipsis) :=
if args.back.isOfKind `Lean.Parser.Term.ellipsis then
(args.pop, true)
else
(args, false);
unless (pattern || !ellipsis) $
throwErrorAt args.back "'..' is only allowed in patterns";
(namedArgs, args) ← args.foldlM
(args, false)
unless pattern || !ellipsis do
throwErrorAt args.back "'..' is only allowed in patterns"
let (namedArgs, args) ← args.foldlM
(fun (acc : Array NamedArg × Array Arg) (stx : Syntax) => do
let (namedArgs, args) := acc;
if stx.getKind == `Lean.Parser.Term.namedArgument then do
let (namedArgs, args) := acc
if stx.getKind == `Lean.Parser.Term.namedArgument then
-- tparser! try ("(" >> ident >> " := ") >> termParser >> ")"
let name := (stx.getArg 1).getId.eraseMacroScopes;
let val := stx.getArg 3;
namedArgs ← addNamedArg namedArgs { name := name, val := Arg.stx val };
let name := stx[1].getId.eraseMacroScopes
let val := stx[3]
let namedArgs ← addNamedArg namedArgs { name := name, val := Arg.stx val }
pure (namedArgs, args)
else if stx.getKind == `Lean.Parser.Term.ellipsis then do
else if stx.getKind == `Lean.Parser.Term.ellipsis then
throwErrorAt stx "unexpected '..'"
else
pure (namedArgs, args.push $ Arg.stx stx))
(#[], #[]);
(#[], #[])
pure (f, namedArgs, args, ellipsis)
@[builtinTermElab app] def elabApp : TermElab :=
fun stx expectedType? => do
(f, namedArgs, args, _) ← expandApp stx;
let (f, namedArgs, args, _) ← expandApp stx
elabAppAux f namedArgs args expectedType?
private def elabAtom : TermElab :=
@ -849,10 +834,7 @@ fun stx expectedType? => match_syntax stx with
@[builtinTermElab proj] def elabProj : TermElab := elabAtom
@[builtinTermElab arrayRef] def elabArrayRef : TermElab := elabAtom
@[init] private def regTraceClasses : IO Unit := do
registerTraceClass `Elab.app;
pure ()
initialize
registerTraceClass `Elab.app
end Term
end Elab
end Lean
end Lean.Elab.Term

33561
stage0/stdlib/Lean/Elab/App.c generated
View file

File diff suppressed because it is too large Load diff

28
stage0/stdlib/Lean/Elab/Do.c generated
View file

@ -234,7 +234,6 @@ lean_object* l___private_Lean_Elab_Do_9__mkUnit___closed__3;
extern lean_object* l___private_Lean_Elab_Quotation_6__compileStxMatch___main___closed__25;
lean_object* l_Lean_Elab_Term_Do_eraseVars(lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Term_elabParen___closed__5;
extern lean_object* l___private_Lean_Elab_App_33__elabAppFn___main___closed__9;
lean_object* l_Lean_Elab_Term_Do_mkAuxDeclFor___at_Lean_Elab_Term_Do_convertTerminalActionIntoJmpAux___main___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Do_mkFreshJP___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_expandLiftMethod(lean_object*, lean_object*, lean_object*);
@ -486,6 +485,7 @@ extern lean_object* l___private_Lean_Meta_Closure_1__mkAuxDefinitionImp___lambda
lean_object* l_Array_umapMAux___main___at_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___spec__1___closed__6;
lean_object* l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__46;
lean_object* l_Lean_Elab_Term_Do_toMessageDataAux___main___closed__14;
extern lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__13;
lean_object* l_Lean_Elab_Term_Do_extendUpdatedVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTermCore___closed__5;
lean_object* l___private_Lean_Elab_Do_15__mkMonadAlias___closed__1;
@ -526,6 +526,7 @@ lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_ensureEOS___closed__2;
lean_object* l___regBuiltin_Lean_Elab_Term_Do_elabDo(lean_object*);
lean_object* l_Std_RBNode_appendTrees___main___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_withNewVars___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__16;
lean_object* l_Lean_Elab_Term_Do_toMessageDataAux___main___closed__28;
lean_object* l_Lean_Elab_Term_Do_ToTerm_breakToTermCore___closed__3;
lean_object* l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__6;
@ -839,7 +840,6 @@ lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Term_Do_concat___
lean_object* l_Array_umapMAux___main___at_Lean_Elab_Term_Do_ToCodeBlock_doMatchToCode___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadTracer_trace___at_Lean_Elab_Term_Do_elabDo___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Do_toMessageDataAux___main___closed__1;
extern lean_object* l___private_Lean_Elab_App_33__elabAppFn___main___closed__14;
lean_object* l_Lean_indentD(lean_object*);
extern lean_object* l___private_Lean_Elab_Binders_12__expandFunBindersAux___main___closed__11;
extern lean_object* l_Lean_Elab_Term_elabLetDeclCore___closed__9;
@ -26221,12 +26221,12 @@ x_317 = lean_array_push(x_316, x_296);
x_318 = lean_array_push(x_317, x_296);
x_319 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_301____closed__20;
x_320 = lean_array_push(x_318, x_319);
x_321 = l___private_Lean_Elab_App_33__elabAppFn___main___closed__14;
x_321 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__16;
x_322 = lean_array_push(x_295, x_321);
x_323 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__37;
lean_inc(x_322);
x_324 = lean_array_push(x_322, x_323);
x_325 = l___private_Lean_Elab_App_33__elabAppFn___main___closed__9;
x_325 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__13;
x_326 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_326, 0, x_325);
lean_ctor_set(x_326, 1, x_324);
@ -26439,12 +26439,12 @@ x_445 = lean_array_push(x_444, x_424);
x_446 = lean_array_push(x_445, x_424);
x_447 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_301____closed__20;
x_448 = lean_array_push(x_446, x_447);
x_449 = l___private_Lean_Elab_App_33__elabAppFn___main___closed__14;
x_449 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__16;
x_450 = lean_array_push(x_423, x_449);
x_451 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__37;
lean_inc(x_450);
x_452 = lean_array_push(x_450, x_451);
x_453 = l___private_Lean_Elab_App_33__elabAppFn___main___closed__9;
x_453 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__13;
x_454 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_454, 0, x_453);
lean_ctor_set(x_454, 1, x_452);
@ -27260,12 +27260,12 @@ x_910 = lean_array_push(x_909, x_889);
x_911 = lean_array_push(x_910, x_889);
x_912 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_301____closed__20;
x_913 = lean_array_push(x_911, x_912);
x_914 = l___private_Lean_Elab_App_33__elabAppFn___main___closed__14;
x_914 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__16;
x_915 = lean_array_push(x_888, x_914);
x_916 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__37;
lean_inc(x_915);
x_917 = lean_array_push(x_915, x_916);
x_918 = l___private_Lean_Elab_App_33__elabAppFn___main___closed__9;
x_918 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__13;
x_919 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_919, 0, x_918);
lean_ctor_set(x_919, 1, x_917);
@ -27447,12 +27447,12 @@ x_1016 = lean_array_push(x_1015, x_995);
x_1017 = lean_array_push(x_1016, x_995);
x_1018 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_301____closed__20;
x_1019 = lean_array_push(x_1017, x_1018);
x_1020 = l___private_Lean_Elab_App_33__elabAppFn___main___closed__14;
x_1020 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__16;
x_1021 = lean_array_push(x_994, x_1020);
x_1022 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__37;
lean_inc(x_1021);
x_1023 = lean_array_push(x_1021, x_1022);
x_1024 = l___private_Lean_Elab_App_33__elabAppFn___main___closed__9;
x_1024 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__13;
x_1025 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_1025, 0, x_1024);
lean_ctor_set(x_1025, 1, x_1023);
@ -34170,7 +34170,7 @@ lean_inc(x_45);
lean_dec(x_43);
x_46 = l_Array_empty___closed__1;
x_47 = lean_array_push(x_46, x_15);
x_48 = l___private_Lean_Elab_App_33__elabAppFn___main___closed__14;
x_48 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__16;
x_49 = lean_array_push(x_47, x_48);
x_50 = l_Lean_Elab_Term_Do_ToCodeBlock_doForToCode___closed__4;
x_51 = l_Lean_addMacroScope(x_44, x_50, x_41);
@ -34184,7 +34184,7 @@ lean_ctor_set(x_56, 1, x_54);
lean_ctor_set(x_56, 2, x_51);
lean_ctor_set(x_56, 3, x_55);
x_57 = lean_array_push(x_49, x_56);
x_58 = l___private_Lean_Elab_App_33__elabAppFn___main___closed__9;
x_58 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__13;
x_59 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_59, 0, x_58);
lean_ctor_set(x_59, 1, x_57);
@ -34481,7 +34481,7 @@ lean_inc(x_229);
lean_dec(x_227);
x_230 = l_Array_empty___closed__1;
x_231 = lean_array_push(x_230, x_15);
x_232 = l___private_Lean_Elab_App_33__elabAppFn___main___closed__14;
x_232 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__16;
x_233 = lean_array_push(x_231, x_232);
x_234 = l_Lean_Elab_Term_Do_ToCodeBlock_doForToCode___closed__4;
lean_inc(x_225);
@ -34497,7 +34497,7 @@ lean_ctor_set(x_240, 1, x_238);
lean_ctor_set(x_240, 2, x_235);
lean_ctor_set(x_240, 3, x_239);
x_241 = lean_array_push(x_233, x_240);
x_242 = l___private_Lean_Elab_App_33__elabAppFn___main___closed__9;
x_242 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__13;
x_243 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_243, 0, x_242);
lean_ctor_set(x_243, 1, x_241);

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

@ -65,6 +65,7 @@ lean_object* l___private_Lean_Elab_Match_5__mkUserNameFor(lean_object*, lean_obj
lean_object* l___private_Lean_Elab_Match_13__mkMVarSyntax___rarg(lean_object*, lean_object*);
lean_object* l___private_Init_LeanInit_17__mapSepElemsMAux___main___at_Lean_Elab_Term_CollectPatternVars_collect___main___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapSepElemsM___at_Lean_Elab_Term_CollectPatternVars_collect___main___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_forallTelescopeReducing___at___private_Lean_Elab_App_0__Lean_Elab_Term_ElabAppArgs_hasOptAutoParams___spec__2___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Match_13__mkMVarSyntax___rarg___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Meta_inferType___at___private_Lean_Elab_Match_38__mkLocalDeclFor___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l___private_Lean_Elab_Match_6__isAuxDiscrName(lean_object*);
@ -75,6 +76,7 @@ lean_object* l___regBuiltin_Lean_Elab_Term_elabInaccessible___closed__1;
extern lean_object* l_Lean_Elab_throwUnsupportedSyntax___rarg___closed__1;
uint8_t lean_name_eq(lean_object*, lean_object*);
lean_object* l___private_Lean_HeadIndex_1__headNumArgsAux___main(lean_object*, lean_object*);
extern lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__11;
uint8_t l_Array_anyRangeMAux___main___at_Lean_Elab_Term_elabMatch___spec__25(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Array_myMacro____x40_Init_Data_Array_Macros___hyg_464____closed__2;
uint8_t l_Array_anyRangeMAux___main___at_Lean_Elab_Term_elabMatch___spec__5(lean_object*, lean_object*, lean_object*, lean_object*);
@ -106,6 +108,7 @@ lean_object* lean_environment_find(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Match_27__processVar___closed__1;
lean_object* l___private_Lean_Elab_Match_23__pushNewArg___closed__1;
lean_object* l_Array_forMAux___main___at___private_Lean_Elab_Match_46__tryPostponeIfDiscrTypeIsMVar___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__12;
lean_object* l_Array_anyRangeMAux___main___at_Lean_Elab_Term_elabMatch___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_checkTraceOption(lean_object*, lean_object*);
extern lean_object* l_Array_myMacro____x40_Init_Data_Array_Macros___hyg_464____closed__4;
@ -247,7 +250,6 @@ lean_object* l___private_Lean_Elab_Match_37__throwInvalidPattern___rarg___closed
lean_object* l_Lean_Meta_whnf___at_Lean_Elab_Term_ToDepElimPattern_main___main___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_st_ref_take(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Match_37__throwInvalidPattern(lean_object*);
lean_object* l_Lean_Meta_forallTelescopeReducing___at___private_Lean_Elab_App_11__hasOptAutoParams___spec__2___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_logAt___at_Lean_Elab_Term_CollectPatternVars_main___spec__3(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Array_anyRangeMAux___main___at_Lean_Elab_Term_elabMatch___spec__18(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_numLitKind;
@ -424,7 +426,6 @@ lean_object* l_Lean_Elab_Term_PatternVar_hasToString___closed__1;
lean_object* l___private_Lean_Elab_Match_40__elabMatchAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkFreshId___at___private_Lean_Elab_Match_38__mkLocalDeclFor___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Lean_Meta_ExprDefEq_8__checkTypesAndAssign___lambda__1___closed__1;
extern lean_object* l___private_Lean_Elab_App_33__elabAppFn___main___closed__13;
lean_object* l_Lean_throwError___at_Lean_Meta_mkWHNFRef___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_LocalDecl_fvarId(lean_object*);
uint8_t l_Array_anyRangeMAux___main___at_Lean_Elab_Term_elabMatch___spec__13(lean_object*, lean_object*, lean_object*, lean_object*);
@ -458,6 +459,7 @@ extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_301____clos
lean_object* l_List_toStringAux___main___at___private_Lean_Elab_Match_3__elabDiscrsWitMatchTypeAux___main___spec__2___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabMatchAltView___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_getPatternVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__8;
extern lean_object* l_Lean_Elab_elabAttr___rarg___closed__3;
uint8_t l_Array_anyRangeMAux___main___at_Lean_Elab_Term_elabMatch___spec__10(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Match_32__withPatternVarsAux___main___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -631,7 +633,6 @@ lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
lean_object* l_Lean_Meta_whnf___at_Lean_Elab_Term_ToDepElimPattern_main___main___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_mkOptionalNode___closed__2;
lean_object* l___private_Lean_Elab_Match_17__throwAmbiguous___rarg___closed__3;
extern lean_object* l___private_Lean_Elab_App_33__elabAppFn___main___closed__5;
lean_object* lean_nat_mod(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_CollectPatternVars_main(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Match_3__elabDiscrsWitMatchTypeAux___main___closed__9;
@ -712,7 +713,6 @@ uint8_t l_Array_anyRangeMAux___main___at_Lean_Elab_Term_elabMatch___spec__3(lean
lean_object* l___private_Lean_Elab_Match_3__elabDiscrsWitMatchTypeAux___main___closed__6;
uint8_t l_Array_anyRangeMAux___main___at_Lean_Elab_Term_elabMatch___spec__24(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_anyRangeMAux___main___at_Lean_Elab_Term_elabMatch___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Lean_Elab_App_33__elabAppFn___main___closed__12;
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_reportMatcherResultErrors___closed__1;
extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_907____closed__1;
@ -5958,7 +5958,7 @@ lean_object* l_Lean_Meta_forallTelescopeReducing___at_Lean_Elab_Term_CollectPatt
_start:
{
lean_object* x_11; lean_object* x_12;
x_11 = lean_alloc_closure((void*)(l_Lean_Meta_forallTelescopeReducing___at___private_Lean_Elab_App_11__hasOptAutoParams___spec__2___rarg___lambda__1), 11, 4);
x_11 = lean_alloc_closure((void*)(l_Lean_Meta_forallTelescopeReducing___at___private_Lean_Elab_App_0__Lean_Elab_Term_ElabAppArgs_hasOptAutoParams___spec__2___rarg___lambda__1), 11, 4);
lean_closure_set(x_11, 0, x_2);
lean_closure_set(x_11, 1, x_3);
lean_closure_set(x_11, 2, x_4);
@ -7988,7 +7988,7 @@ static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___main___c
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Elab_App_33__elabAppFn___main___closed__12;
x_1 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__11;
x_2 = lean_string_utf8_byte_size(x_1);
return x_2;
}
@ -7997,7 +7997,7 @@ static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___main___c
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l___private_Lean_Elab_App_33__elabAppFn___main___closed__12;
x_1 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__11;
x_2 = lean_unsigned_to_nat(0u);
x_3 = l_Lean_Elab_Term_CollectPatternVars_collect___main___closed__6;
x_4 = lean_alloc_ctor(0, 3, 0);
@ -8012,7 +8012,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l___private_Lean_Elab_App_33__elabAppFn___main___closed__12;
x_2 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__11;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
@ -8189,12 +8189,12 @@ if (x_40 == 0)
{
lean_object* x_41; uint8_t x_42;
lean_dec(x_11);
x_41 = l___private_Lean_Elab_App_33__elabAppFn___main___closed__5;
x_41 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__8;
x_42 = lean_name_eq(x_10, x_41);
if (x_42 == 0)
{
lean_object* x_43; uint8_t x_44;
x_43 = l___private_Lean_Elab_App_33__elabAppFn___main___closed__13;
x_43 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__12;
x_44 = lean_name_eq(x_10, x_43);
if (x_44 == 0)
{
@ -9773,12 +9773,12 @@ if (x_424 == 0)
{
lean_object* x_425; uint8_t x_426;
lean_dec(x_11);
x_425 = l___private_Lean_Elab_App_33__elabAppFn___main___closed__5;
x_425 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__8;
x_426 = lean_name_eq(x_10, x_425);
if (x_426 == 0)
{
lean_object* x_427; uint8_t x_428;
x_427 = l___private_Lean_Elab_App_33__elabAppFn___main___closed__13;
x_427 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__12;
x_428 = lean_name_eq(x_10, x_427);
if (x_428 == 0)
{
@ -10781,12 +10781,12 @@ if (x_634 == 0)
{
lean_object* x_635; uint8_t x_636;
lean_dec(x_11);
x_635 = l___private_Lean_Elab_App_33__elabAppFn___main___closed__5;
x_635 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__8;
x_636 = lean_name_eq(x_10, x_635);
if (x_636 == 0)
{
lean_object* x_637; uint8_t x_638;
x_637 = l___private_Lean_Elab_App_33__elabAppFn___main___closed__13;
x_637 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__12;
x_638 = lean_name_eq(x_10, x_637);
if (x_638 == 0)
{
@ -11820,12 +11820,12 @@ if (x_858 == 0)
{
lean_object* x_859; uint8_t x_860;
lean_dec(x_11);
x_859 = l___private_Lean_Elab_App_33__elabAppFn___main___closed__5;
x_859 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__8;
x_860 = lean_name_eq(x_10, x_859);
if (x_860 == 0)
{
lean_object* x_861; uint8_t x_862;
x_861 = l___private_Lean_Elab_App_33__elabAppFn___main___closed__13;
x_861 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__12;
x_862 = lean_name_eq(x_10, x_861);
if (x_862 == 0)
{
@ -12953,12 +12953,12 @@ if (x_1102 == 0)
{
lean_object* x_1103; uint8_t x_1104;
lean_dec(x_11);
x_1103 = l___private_Lean_Elab_App_33__elabAppFn___main___closed__5;
x_1103 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__8;
x_1104 = lean_name_eq(x_10, x_1103);
if (x_1104 == 0)
{
lean_object* x_1105; uint8_t x_1106;
x_1105 = l___private_Lean_Elab_App_33__elabAppFn___main___closed__13;
x_1105 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__12;
x_1106 = lean_name_eq(x_10, x_1105);
if (x_1106 == 0)
{

246
stage0/stdlib/Lean/Elab/StructInst.c generated
View file

@ -75,7 +75,6 @@ lean_object* l___regBuiltin_Lean_Elab_Term_StructInst_elabStructInst___closed__1
lean_object* l_List_mapM___main___at___private_Lean_Elab_StructInst_9__expandNumLitFields___spec__1___closed__3;
lean_object* lean_array_fswap(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_StructInst_throwFailedToElabField___rarg___closed__3;
extern lean_object* l___private_Lean_Elab_App_30__elabAppLValsAux___main___closed__1;
lean_object* l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__19;
lean_object* l_Array_extract___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_List_foldl___main___at_Lean_Elab_Term_StructInst_DefaultFields_collectStructNames___main___spec__1(lean_object*, lean_object*);
@ -135,6 +134,7 @@ lean_object* l_Lean_Elab_Term_StructInst_formatField(lean_object*, lean_object*)
lean_object* l___private_Lean_Elab_StructInst_8__expandCompositeFields___closed__1;
lean_object* l_Lean_Elab_Term_StructInst_Field_hasFormat___closed__1;
lean_object* l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__11;
lean_object* l_Lean_Elab_Term_synthesizeAppInstMVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_StructInst_expandStructInstExpectedType(lean_object*);
lean_object* l_Lean_Elab_Term_StructInst_formatStruct___main___closed__1;
lean_object* l_List_foldlM___main___at___private_Lean_Elab_StructInst_24__elabStruct___main___spec__1___closed__1;
@ -156,7 +156,6 @@ lean_object* l___private_Lean_Elab_StructInst_5__getStructName___rarg___closed__
lean_object* l___private_Lean_Elab_StructInst_26__regTraceClasses(lean_object*);
lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_propagate(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_mapM___main___at___private_Lean_Elab_StructInst_10__expandParentFields___spec__2___closed__7;
extern lean_object* l___private_Lean_Elab_App_33__elabAppFn___main___closed__9;
lean_object* l___private_Lean_Elab_StructInst_18__addMissingFields___lambda__1___boxed(lean_object**);
lean_object* l___private_Lean_Elab_StructInst_17__groupFields___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__26;
@ -183,6 +182,7 @@ lean_object* l_Lean_Elab_Term_StructInst_FieldLHS_hasFormat(lean_object*);
lean_object* l_List_mapM___main___at___private_Lean_Elab_StructInst_23__mkCtorHeader___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_StructInst_Source_isNone___boxed(lean_object*);
lean_object* l_Lean_Elab_Term_StructInst_Struct_inhabited;
extern lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppLValsAux_loop___closed__1;
lean_object* l_List_mapM___main___at___private_Lean_Elab_StructInst_9__expandNumLitFields___spec__1___closed__6;
lean_object* l_Std_HashMapImp_find_x3f___at___private_Lean_Elab_StructInst_12__mkFieldMap___spec__1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_StructInst_Struct_structName(lean_object*);
@ -194,6 +194,7 @@ lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_mkDefaultValueAux_x3f___m
lean_object* l___private_Lean_Elab_StructInst_25__elabStructInstAux___closed__2;
lean_object* l___private_Lean_Elab_StructInst_17__groupFields___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_propagateLoop___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppLValsAux_loop___closed__2;
lean_object* l_Lean_Meta_assignExprMVar___at_Lean_Elab_Term_synthesizeInstMVarCore___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_StructInst_25__elabStructInstAux___closed__4;
lean_object* l_Lean_Elab_Term_tryPostponeIfNoneOrMVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -234,7 +235,6 @@ lean_object* l___private_Lean_Elab_StructInst_22__propagateExpectedType___boxed(
lean_object* l___private_Lean_Elab_StructInst_1__expandNonAtomicExplicitSource___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabTerm(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_head_x21___at___private_Lean_Elab_StructInst_19__expandStruct___main___spec__3___boxed(lean_object*);
extern lean_object* l___private_Lean_Elab_App_30__elabAppLValsAux___main___closed__2;
lean_object* l_Lean_mkAnnotation(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_StructInst_1__expandNonAtomicExplicitSource___closed__1;
lean_object* l_Lean_replaceRef(lean_object*, lean_object*);
@ -309,6 +309,7 @@ lean_object* lean_expr_dbg_to_string(lean_object*);
lean_object* l_Lean_Elab_Term_StructInst_defaultMissing_x3f(lean_object*);
lean_object* l_Lean_getPathToBaseStructure_x3f(lean_object*, lean_object*, lean_object*);
lean_object* l_List_mapM___main___at___private_Lean_Elab_StructInst_9__expandNumLitFields___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__13;
size_t lean_usize_modn(size_t, lean_object*);
lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_findDefaultMissing_x3f___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_isRoundDone___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -322,6 +323,7 @@ lean_object* l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__7;
lean_object* l___private_Lean_Elab_StructInst_8__expandCompositeFields(lean_object*);
lean_object* l_List_redLength___main___rarg(lean_object*);
lean_object* l___private_Lean_Elab_StructInst_10__expandParentFields(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__16;
uint8_t l_Lean_Elab_Term_StructInst_Field_isSimple___rarg(lean_object*);
lean_object* l_List_head_x21___at___private_Lean_Elab_StructInst_19__expandStruct___main___spec__5___boxed(lean_object*);
lean_object* l_Lean_Elab_Term_StructInst_Struct_fields(lean_object*);
@ -355,6 +357,7 @@ lean_object* l_List_map___main___at_Lean_Elab_Term_StructInst_formatStruct___mai
lean_object* l_Lean_mkAtomFrom(lean_object*, lean_object*);
size_t l_USize_mod(size_t, size_t);
lean_object* l_Lean_Elab_Term_StructInst_FieldLHS_inhabited;
lean_object* l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__28;
lean_object* l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__15;
lean_object* l___private_Lean_Elab_StructInst_9__expandNumLitFields___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_ConstantInfo_lparams(lean_object*);
@ -407,7 +410,6 @@ lean_object* lean_panic_fn(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_step___main(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_foldlStepMAux___main___at___private_Lean_Elab_StructInst_3__isModifyOp_x3f___spec__1___closed__2;
lean_object* l_List_mapM___main___at___private_Lean_Elab_StructInst_9__expandNumLitFields___spec__1___closed__4;
lean_object* l_Array_forMAux___main___at_Lean_Elab_Term_synthesizeAppInstMVars___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__14;
lean_object* l_Array_foldlStepMAux___main___at___private_Lean_Elab_StructInst_3__isModifyOp_x3f___spec__1___closed__1;
lean_object* l___private_Lean_Elab_StructInst_19__expandStruct(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -450,6 +452,7 @@ lean_object* l___private_Lean_Elab_StructInst_20__mkCtorHeaderAux___main(lean_ob
lean_object* l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__6;
lean_object* l___private_Lean_Elab_StructInst_17__groupFields___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_propagateLoop(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Array_iterateMAux___main___at_Lean_Elab_Term_expandApp___spec__1___closed__1;
extern lean_object* l_PUnit_Inhabited;
extern lean_object* l_Lean_mkOptionalNode___closed__1;
lean_object* l___private_Lean_Elab_StructInst_17__groupFields___lambda__3___closed__1;
@ -483,7 +486,6 @@ lean_object* l___private_Lean_Elab_StructInst_14__getFieldIdx(lean_object*, lean
lean_object* l___private_Lean_Elab_StructInst_5__getStructName___rarg___closed__5;
lean_object* l___private_Lean_Elab_StructInst_18__addMissingFields___at___private_Lean_Elab_StructInst_19__expandStruct___main___spec__10(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Lean_Meta_AppBuilder_1__mkIdImp___closed__2;
extern lean_object* l___private_Lean_Elab_App_33__elabAppFn___main___closed__14;
lean_object* l_List_map___main___at_Lean_Elab_Term_StructInst_formatStruct___main___spec__1___closed__1;
lean_object* l_List_mapM___main___at___private_Lean_Elab_StructInst_10__expandParentFields___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_StructInst_25__elabStructInstAux___closed__6;
@ -526,7 +528,6 @@ lean_object* l_Array_iterateMAux___main___at_Lean_mkAppN___spec__1(lean_object*,
lean_object* l_Lean_throwError___at_Lean_Elab_Term_StructInst_DefaultFields_propagateLoop___main___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__8;
lean_object* l_Lean_Elab_Term_StructInst_Field_hasFormat;
extern lean_object* l_Array_iterateMAux___main___at_Lean_Elab_Term_expandApp___spec__1___closed__2;
lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefaultAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_StructInst_19__expandStruct___main___spec__8(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_StructInst_6__toFieldLHS(lean_object*);
@ -2270,19 +2271,29 @@ return x_3;
static lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__15() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Elab_App_30__elabAppLValsAux___main___closed__1;
x_2 = lean_string_utf8_byte_size(x_1);
return x_2;
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_mkAppStx___closed__6;
x_2 = l_Array_iterateMAux___main___at_Lean_Elab_Term_expandApp___spec__1___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__16() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppLValsAux_loop___closed__1;
x_2 = lean_string_utf8_byte_size(x_1);
return x_2;
}
}
static lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__17() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l___private_Lean_Elab_App_30__elabAppLValsAux___main___closed__1;
x_1 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppLValsAux_loop___closed__1;
x_2 = lean_unsigned_to_nat(0u);
x_3 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__15;
x_3 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__16;
x_4 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -2290,7 +2301,7 @@ lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__17() {
static lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__18() {
_start:
{
lean_object* x_1;
@ -2298,22 +2309,12 @@ x_1 = lean_mk_string("\n===>\n");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__18() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__17;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__19() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__18;
x_2 = lean_alloc_ctor(0, 1, 0);
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
@ -2321,19 +2322,19 @@ return x_2;
static lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__20() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("\nval: ");
return x_1;
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__19;
x_2 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__21() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__20;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
lean_object* x_1;
x_1 = lean_mk_string("\nval: ");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__22() {
@ -2341,7 +2342,7 @@ _start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__21;
x_2 = lean_alloc_ctor(0, 1, 0);
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
@ -2349,6 +2350,16 @@ return x_2;
static lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__23() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__22;
x_2 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__24() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__12;
@ -2358,19 +2369,19 @@ lean_ctor_set(x_3, 1, x_1);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__24() {
static lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__25() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__23;
x_2 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__24;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__25() {
static lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__26() {
_start:
{
lean_object* x_1;
@ -2378,21 +2389,21 @@ x_1 = lean_mk_string("\nSource: ");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__26() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__25;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__27() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__26;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__28() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__27;
x_2 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
@ -2418,7 +2429,7 @@ lean_object* x_306; lean_object* x_307; lean_object* x_308; lean_object* x_309;
lean_inc(x_2);
x_306 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_306, 0, x_2);
x_307 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__27;
x_307 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__28;
x_308 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_308, 0, x_306);
lean_ctor_set(x_308, 1, x_307);
@ -2568,7 +2579,7 @@ lean_object* x_163; lean_object* x_164; lean_object* x_165; lean_object* x_166;
lean_inc(x_1);
x_163 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_163, 0, x_1);
x_164 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__22;
x_164 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__23;
x_165 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_165, 0, x_163);
lean_ctor_set(x_165, 1, x_164);
@ -2608,7 +2619,7 @@ lean_inc(x_60);
lean_dec(x_58);
x_61 = l_Array_empty___closed__1;
x_62 = lean_array_push(x_61, x_54);
x_63 = l___private_Lean_Elab_App_33__elabAppFn___main___closed__14;
x_63 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__16;
x_64 = lean_array_push(x_62, x_63);
x_65 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__11;
lean_inc(x_56);
@ -2622,16 +2633,16 @@ lean_ctor_set(x_69, 1, x_67);
lean_ctor_set(x_69, 2, x_66);
lean_ctor_set(x_69, 3, x_68);
x_70 = lean_array_push(x_64, x_69);
x_71 = l___private_Lean_Elab_App_33__elabAppFn___main___closed__9;
x_71 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__13;
x_72 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_72, 0, x_71);
lean_ctor_set(x_72, 1, x_70);
x_73 = lean_array_push(x_61, x_72);
x_74 = l___private_Lean_Elab_App_30__elabAppLValsAux___main___closed__2;
x_74 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppLValsAux_loop___closed__2;
lean_inc(x_56);
lean_inc(x_59);
x_75 = l_Lean_addMacroScope(x_59, x_74, x_56);
x_76 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__16;
x_76 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__17;
x_77 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_77, 0, x_25);
lean_ctor_set(x_77, 1, x_76);
@ -2644,7 +2655,7 @@ x_81 = lean_array_push(x_79, x_80);
x_82 = lean_array_push(x_81, x_53);
x_83 = l_myMacro____x40_Init_Data_ToString_Macro___hyg_39____closed__15;
x_84 = lean_array_push(x_82, x_83);
x_85 = l_Array_iterateMAux___main___at_Lean_Elab_Term_expandApp___spec__1___closed__2;
x_85 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__15;
x_86 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_86, 0, x_85);
lean_ctor_set(x_86, 1, x_84);
@ -2761,7 +2772,7 @@ lean_object* x_134; lean_object* x_135; lean_object* x_136; lean_object* x_137;
lean_inc(x_1);
x_134 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_134, 0, x_1);
x_135 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__19;
x_135 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__20;
x_136 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_136, 0, x_134);
lean_ctor_set(x_136, 1, x_135);
@ -2868,7 +2879,7 @@ lean_inc(x_193);
lean_dec(x_191);
x_194 = l_Array_empty___closed__1;
x_195 = lean_array_push(x_194, x_187);
x_196 = l___private_Lean_Elab_App_33__elabAppFn___main___closed__14;
x_196 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__16;
x_197 = lean_array_push(x_195, x_196);
x_198 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__11;
lean_inc(x_189);
@ -2877,23 +2888,23 @@ x_199 = l_Lean_addMacroScope(x_192, x_198, x_189);
x_200 = lean_box(0);
x_201 = l_Lean_SourceInfo_inhabited___closed__1;
x_202 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__10;
x_203 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__24;
x_203 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__25;
x_204 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_204, 0, x_201);
lean_ctor_set(x_204, 1, x_202);
lean_ctor_set(x_204, 2, x_199);
lean_ctor_set(x_204, 3, x_203);
x_205 = lean_array_push(x_197, x_204);
x_206 = l___private_Lean_Elab_App_33__elabAppFn___main___closed__9;
x_206 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__13;
x_207 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_207, 0, x_206);
lean_ctor_set(x_207, 1, x_205);
x_208 = lean_array_push(x_194, x_207);
x_209 = l___private_Lean_Elab_App_30__elabAppLValsAux___main___closed__2;
x_209 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppLValsAux_loop___closed__2;
lean_inc(x_189);
lean_inc(x_192);
x_210 = l_Lean_addMacroScope(x_192, x_209, x_189);
x_211 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__16;
x_211 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__17;
x_212 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_212, 0, x_201);
lean_ctor_set(x_212, 1, x_211);
@ -2906,7 +2917,7 @@ x_216 = lean_array_push(x_214, x_215);
x_217 = lean_array_push(x_216, x_186);
x_218 = l_myMacro____x40_Init_Data_ToString_Macro___hyg_39____closed__15;
x_219 = lean_array_push(x_217, x_218);
x_220 = l_Array_iterateMAux___main___at_Lean_Elab_Term_expandApp___spec__1___closed__2;
x_220 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__15;
x_221 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_221, 0, x_220);
lean_ctor_set(x_221, 1, x_219);
@ -3030,7 +3041,7 @@ lean_object* x_274; lean_object* x_275; lean_object* x_276; lean_object* x_277;
lean_inc(x_1);
x_274 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_274, 0, x_1);
x_275 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__19;
x_275 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__20;
x_276 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_276, 0, x_274);
lean_ctor_set(x_276, 1, x_275);
@ -13828,7 +13839,7 @@ x_6 = l___private_Lean_Elab_Term_5__tryCoe___closed__3;
x_7 = lean_array_push(x_6, x_1);
x_8 = lean_array_push(x_7, x_4);
x_9 = lean_array_push(x_8, x_5);
x_10 = l___private_Lean_Elab_App_33__elabAppFn___main___closed__9;
x_10 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__13;
x_11 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_11, 0, x_10);
lean_ctor_set(x_11, 1, x_9);
@ -18090,95 +18101,94 @@ lean_inc(x_5);
x_26 = l___private_Lean_Elab_StructInst_22__propagateExpectedType(x_24, x_25, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_23);
if (lean_obj_tag(x_26) == 0)
{
lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30;
lean_object* x_27; lean_object* x_28; lean_object* x_29;
x_27 = lean_ctor_get(x_26, 1);
lean_inc(x_27);
lean_dec(x_26);
x_28 = lean_ctor_get(x_22, 2);
lean_inc(x_28);
x_29 = lean_unsigned_to_nat(0u);
x_30 = l_Array_forMAux___main___at_Lean_Elab_Term_synthesizeAppInstMVars___spec__1(x_28, x_29, x_3, x_4, x_5, x_6, x_7, x_8, x_27);
x_29 = l_Lean_Elab_Term_synthesizeAppInstMVars(x_28, x_3, x_4, x_5, x_6, x_7, x_8, x_27);
lean_dec(x_28);
if (lean_obj_tag(x_30) == 0)
if (lean_obj_tag(x_29) == 0)
{
uint8_t x_31;
x_31 = !lean_is_exclusive(x_30);
if (x_31 == 0)
uint8_t x_30;
x_30 = !lean_is_exclusive(x_29);
if (x_30 == 0)
{
lean_object* x_32;
x_32 = lean_ctor_get(x_30, 0);
lean_dec(x_32);
lean_ctor_set(x_30, 0, x_22);
return x_30;
lean_object* x_31;
x_31 = lean_ctor_get(x_29, 0);
lean_dec(x_31);
lean_ctor_set(x_29, 0, x_22);
return x_29;
}
else
{
lean_object* x_33; lean_object* x_34;
x_33 = lean_ctor_get(x_30, 1);
lean_inc(x_33);
lean_dec(x_30);
x_34 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_34, 0, x_22);
lean_ctor_set(x_34, 1, x_33);
return x_34;
lean_object* x_32; lean_object* x_33;
x_32 = lean_ctor_get(x_29, 1);
lean_inc(x_32);
lean_dec(x_29);
x_33 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_33, 0, x_22);
lean_ctor_set(x_33, 1, x_32);
return x_33;
}
}
else
{
uint8_t x_35;
uint8_t x_34;
lean_dec(x_22);
x_35 = !lean_is_exclusive(x_30);
if (x_35 == 0)
x_34 = !lean_is_exclusive(x_29);
if (x_34 == 0)
{
return x_30;
return x_29;
}
else
{
lean_object* x_36; lean_object* x_37; lean_object* x_38;
x_36 = lean_ctor_get(x_30, 0);
x_37 = lean_ctor_get(x_30, 1);
lean_inc(x_37);
lean_object* x_35; lean_object* x_36; lean_object* x_37;
x_35 = lean_ctor_get(x_29, 0);
x_36 = lean_ctor_get(x_29, 1);
lean_inc(x_36);
lean_dec(x_30);
x_38 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_38, 0, x_36);
lean_ctor_set(x_38, 1, x_37);
return x_38;
lean_inc(x_35);
lean_dec(x_29);
x_37 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_37, 0, x_35);
lean_ctor_set(x_37, 1, x_36);
return x_37;
}
}
}
else
{
uint8_t x_39;
uint8_t x_38;
lean_dec(x_22);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_3);
x_39 = !lean_is_exclusive(x_26);
if (x_39 == 0)
x_38 = !lean_is_exclusive(x_26);
if (x_38 == 0)
{
return x_26;
}
else
{
lean_object* x_40; lean_object* x_41; lean_object* x_42;
x_40 = lean_ctor_get(x_26, 0);
x_41 = lean_ctor_get(x_26, 1);
lean_inc(x_41);
lean_object* x_39; lean_object* x_40; lean_object* x_41;
x_39 = lean_ctor_get(x_26, 0);
x_40 = lean_ctor_get(x_26, 1);
lean_inc(x_40);
lean_inc(x_39);
lean_dec(x_26);
x_42 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_42, 0, x_40);
lean_ctor_set(x_42, 1, x_41);
return x_42;
x_41 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_41, 0, x_39);
lean_ctor_set(x_41, 1, x_40);
return x_41;
}
}
}
else
{
uint8_t x_43;
uint8_t x_42;
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
@ -18186,23 +18196,23 @@ lean_dec(x_5);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_43 = !lean_is_exclusive(x_21);
if (x_43 == 0)
x_42 = !lean_is_exclusive(x_21);
if (x_42 == 0)
{
return x_21;
}
else
{
lean_object* x_44; lean_object* x_45; lean_object* x_46;
x_44 = lean_ctor_get(x_21, 0);
x_45 = lean_ctor_get(x_21, 1);
lean_inc(x_45);
lean_object* x_43; lean_object* x_44; lean_object* x_45;
x_43 = lean_ctor_get(x_21, 0);
x_44 = lean_ctor_get(x_21, 1);
lean_inc(x_44);
lean_inc(x_43);
lean_dec(x_21);
x_46 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_46, 0, x_44);
lean_ctor_set(x_46, 1, x_45);
return x_46;
x_45 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_45, 0, x_43);
lean_ctor_set(x_45, 1, x_44);
return x_45;
}
}
}
@ -27999,6 +28009,8 @@ l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__26 = _init_l___privat
lean_mark_persistent(l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__26);
l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__27 = _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__27();
lean_mark_persistent(l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__27);
l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__28 = _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__28();
lean_mark_persistent(l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__28);
l___private_Lean_Elab_StructInst_5__getStructName___rarg___closed__1 = _init_l___private_Lean_Elab_StructInst_5__getStructName___rarg___closed__1();
lean_mark_persistent(l___private_Lean_Elab_StructInst_5__getStructName___rarg___closed__1);
l___private_Lean_Elab_StructInst_5__getStructName___rarg___closed__2 = _init_l___private_Lean_Elab_StructInst_5__getStructName___rarg___closed__2();