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

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2022-07-08 17:30:07 -07:00
parent bdaabd4e7b
commit 7e578bc122
4 changed files with 2511 additions and 1953 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

52
stage0/src/Lean/Elab/Do.lean generated
View file

@ -87,24 +87,24 @@ private partial def hasLiftMethod : Syntax → Bool
structure ExtractMonadResult where
m : Expr
α : Expr
returnType : Expr
expectedType : Expr
private def mkUnknownMonadResult : MetaM ExtractMonadResult := do
let u ← mkFreshLevelMVar
let v ← mkFreshLevelMVar
let m ← mkFreshExprMVar (← mkArrow (mkSort (mkLevelSucc u)) (mkSort (mkLevelSucc v)))
let α ← mkFreshExprMVar (mkSort (mkLevelSucc u))
return { m, α, expectedType := mkApp m α }
let returnType ← mkFreshExprMVar (mkSort (mkLevelSucc u))
return { m, returnType, expectedType := mkApp m returnType }
private partial def extractBind (expectedType? : Option Expr) : TermElabM ExtractMonadResult := do
let some expectedType := expectedType? | mkUnknownMonadResult
let extractStep? (type : Expr) : MetaM (Option ExtractMonadResult) := do
let .app m α _ := type | return none
let .app m returnType _ := type | return none
try
let bindInstType ← mkAppM ``Bind #[m]
discard <| Meta.synthInstance bindInstType
return some { m, α, expectedType }
return some { m, returnType, expectedType }
catch _ =>
return none
let rec extract? (type : Expr) : MetaM (Option ExtractMonadResult) := do
@ -863,9 +863,12 @@ def Kind.isRegular : Kind → Bool
| _ => false
structure Context where
m : Syntax -- Syntax to reference the monad associated with the do notation.
uvars : Array Var
kind : Kind
/-- Syntax to reference the monad associated with the do notation. -/
m : Syntax
/-- Syntax to reference the result of the monadic computation performed by the do notation. -/
returnType : Syntax
uvars : Array Var
kind : Kind
abbrev M := ReaderT Context MacroM
@ -1031,8 +1034,8 @@ partial def toTerm (c : Code) : M Syntax := do
let termMatchAlts := mkNode `Lean.Parser.Term.matchAlts #[mkNullNode termAlts]
return mkNode `Lean.Parser.Term.«match» #[mkAtomFrom ref "match", genParam, optMotive, discrs, mkAtomFrom ref "with", termMatchAlts]
def run (code : Code) (m : Syntax) (uvars : Array Var := #[]) (kind := Kind.regular) : MacroM Syntax :=
toTerm code { m := m, kind := kind, uvars := uvars }
def run (code : Code) (m : Syntax) (returnType : Syntax) (uvars : Array Var := #[]) (kind := Kind.regular) : MacroM Syntax :=
toTerm code { m, returnType, kind, uvars }
/- Given
- `a` is true if the code block has a `Code.action _` exit point
@ -1051,8 +1054,8 @@ def mkNestedKind (a r bc : Bool) : Kind :=
| true, true, true => .nestedPRBC
| false, false, false => unreachable!
def mkNestedTerm (code : Code) (m : Syntax) (uvars : Array Var) (a r bc : Bool) : MacroM Syntax := do
ToTerm.run code m uvars (mkNestedKind a r bc)
def mkNestedTerm (code : Code) (m : Syntax) (returnType : Syntax) (uvars : Array Var) (a r bc : Bool) : MacroM Syntax := do
ToTerm.run code m returnType uvars (mkNestedKind a r bc)
/- Given a term `term` produced by `ToTerm.run`, pattern match on its result.
See comment at the beginning of the `ToTerm` namespace.
@ -1119,7 +1122,10 @@ namespace ToCodeBlock
structure Context where
ref : Syntax
m : Syntax -- Syntax representing the monad associated with the do notation.
/-- Syntax representing the monad associated with the do notation. -/
m : Syntax
/-- Syntax to reference the result of the monadic computation performed by the do notation. -/
returnType : Syntax
mutableVars : VarSet := {}
insideFor : Bool := false
@ -1155,7 +1161,7 @@ def mkForInBody (_ : Syntax) (forInBody : CodeBlock) : M ToForInTermResult := d
let ctx ← read
let uvars := forInBody.uvars
let uvars := varSetToArray uvars
let term ← liftMacroM <| ToTerm.run forInBody.code ctx.m uvars (if hasReturn forInBody.code then ToTerm.Kind.forInWithReturn else ToTerm.Kind.forIn)
let term ← liftMacroM <| ToTerm.run forInBody.code ctx.m ctx.returnType uvars (if hasReturn forInBody.code then ToTerm.Kind.forInWithReturn else ToTerm.Kind.forIn)
return ⟨uvars, term⟩
def ensureInsideFor : M Unit :=
@ -1413,10 +1419,11 @@ mutual
let uvarsTuple ← liftMacroM do mkTuple uvars
if hasReturn forInBodyCodeBlock.code then
let forInBody ← liftMacroM <| destructTuple uvars (← `(r)) forInBody
let optType ← `(Option $((← read).returnType))
let forInTerm ← if let some h := h? then
`(for_in'% $(xs) (MProd.mk none $uvarsTuple) fun $x $h r => let r := r.2; $forInBody)
`(for_in'% $(xs) (MProd.mk (none : $optType) $uvarsTuple) fun $x $h (r : MProd $optType _) => let r := r.2; $forInBody)
else
`(for_in% $(xs) (MProd.mk none $uvarsTuple) fun $x r => let r := r.2; $forInBody)
`(for_in% $(xs) (MProd.mk (none : $optType) $uvarsTuple) fun $x (r : MProd $optType _) => let r := r.2; $forInBody)
let auxDo ← `(do let r ← $forInTerm:term;
$uvarsTuple:term := r.2;
match r.1 with
@ -1495,7 +1502,7 @@ mutual
let bc := tryCatchPred tryCode catches finallyCode? hasBreakContinue
let toTerm (codeBlock : CodeBlock) : M Syntax := do
let codeBlock ← liftM $ extendUpdatedVars codeBlock ws
liftMacroM <| ToTerm.mkNestedTerm codeBlock.code ctx.m uvars a r bc
liftMacroM <| ToTerm.mkNestedTerm codeBlock.code ctx.m ctx.returnType uvars a r bc
let term ← toTerm tryCode
let term ← catches.foldlM (init := term) fun term «catch» => do
let catchTerm ← toTerm «catch».codeBlock
@ -1511,7 +1518,7 @@ mutual
throwError "'finally' currently does not support reassignments"
if hasBreakContinueReturn finallyCode.code then
throwError "'finally' currently does 'return', 'break', nor 'continue'"
let finallyTerm ← liftMacroM <| ToTerm.run finallyCode.code ctx.m {} ToTerm.Kind.regular
let finallyTerm ← liftMacroM <| ToTerm.run finallyCode.code ctx.m ctx.returnType {} ToTerm.Kind.regular
``(tryFinally $term $finallyTerm)
let doElemsNew ← liftMacroM <| ToTerm.matchNestedTermResult term uvars a r bc
doSeqToCode (doElemsNew ++ doElems)
@ -1592,8 +1599,8 @@ mutual
throwError "unexpected do-element of kind {doElem.getKind}:\n{doElem}"
end
def run (doStx : Syntax) (m : Syntax) : TermElabM CodeBlock :=
(doSeqToCode <| getDoSeqElems <| getDoSeq doStx).run { ref := doStx, m }
def run (doStx : Syntax) (m : Syntax) (returnType : Syntax) : TermElabM CodeBlock :=
(doSeqToCode <| getDoSeqElems <| getDoSeq doStx).run { ref := doStx, m, returnType }
end ToCodeBlock
@ -1601,8 +1608,9 @@ end ToCodeBlock
tryPostponeIfNoneOrMVar expectedType?
let bindInfo ← extractBind expectedType?
let m ← Term.exprToSyntax bindInfo.m
let codeBlock ← ToCodeBlock.run stx m
let stxNew ← liftMacroM <| ToTerm.run codeBlock.code m
let returnType ← Term.exprToSyntax bindInfo.returnType
let codeBlock ← ToCodeBlock.run stx m returnType
let stxNew ← liftMacroM <| ToTerm.run codeBlock.code m returnType
trace[Elab.do] stxNew
withMacroExpansion stx stxNew <| elabTermEnsuringType stxNew bindInfo.expectedType

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

@ -1797,7 +1797,7 @@ def expandDeclId (currNamespace : Name) (currLevelNames : List Name) (declId : S
`(Nat.succ $(← exprToSyntax e))
```
-/
def exprToSyntax (e : Expr) : TermElabM Term := do
def exprToSyntax (e : Expr) : TermElabM Term := withFreshMacroScope do
let result ← `(?m)
let eType ← inferType e
let mvar ← elabTerm result eType

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

File diff suppressed because it is too large Load diff

101
stage0/stdlib/Lean/Elab/Term.c generated
View file

@ -117,6 +117,7 @@ static lean_object* l_Lean_logTrace___at_Lean_Elab_Term_traceAtCmdPos___spec__1_
LEAN_EXPORT lean_object* l_Lean_Elab_Term_resolveName___lambda__2___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Term_collectUnassignedMVars_go___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_exprToSyntax___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_MetavarContext_0__Lean_DependsOn_dep_visitMain___at_Lean_Elab_Term_addAutoBoundImplicits_go___spec__35(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_liftExcept___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__8(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_throwMaxRecDepthAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -155,6 +156,7 @@ static lean_object* l_Lean_getConstInfo___at_Lean_Elab_Term_mkConst___spec__1___
static lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___lambda__5___closed__3;
LEAN_EXPORT lean_object* l_Std_PersistentArray_anyM___at_Lean_Elab_Term_addAutoBoundImplicits_go___spec__13___boxed(lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_isTacticBlock___closed__5;
static lean_object* l_Lean_Elab_Term_exprToSyntax___lambda__1___closed__3;
LEAN_EXPORT lean_object* l_Lean_Elab_checkNotAlreadyDeclared___at_Lean_Elab_Term_expandDeclId___spec__6___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_getDeclName_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_MetavarContext_0__Lean_DependsOn_dep_visitMain___at_Lean_Elab_Term_addAutoBoundImplicits_go___spec__43(lean_object*, lean_object*, lean_object*);
@ -262,6 +264,7 @@ LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Term_withoutModif
LEAN_EXPORT lean_object* l_Lean_Elab_Term_withoutModifyingElabMetaStateWithInfo___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_withDeclName(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_GetOpKind_noConfusion___rarg(uint8_t, uint8_t, lean_object*);
static lean_object* l_Lean_Elab_Term_exprToSyntax___lambda__1___closed__2;
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Term_0__Lean_Elab_Term_withoutModifyingStateWithInfoAndMessagesImpl___spec__4(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_name_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Elab_Term_mkAuxName___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -289,6 +292,7 @@ LEAN_EXPORT lean_object* l_ReaderT_map___at_Lean_Elab_Term_instMetaEvalTermElabM
static lean_object* l_Lean_Elab_checkNotAlreadyDeclared___at_Lean_Elab_Term_expandDeclId___spec__6___lambda__1___closed__2;
lean_object* l_Lean_Meta_isMonad_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_isNoImplicitLambda___closed__2;
static lean_object* l_Lean_Elab_Term_exprToSyntax___lambda__1___closed__4;
LEAN_EXPORT lean_object* l_Lean_Elab_Term_getMVarDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Std_PersistentArray_anyMAux___at_Lean_Elab_Term_addAutoBoundImplicits_go___spec__22(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__12;
@ -313,7 +317,6 @@ LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Elab_Term_throwMVarError___
lean_object* lean_string_append(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_getSyntheticMVarDecl_x3f___lambda__1___boxed(lean_object*, lean_object*);
lean_object* l_Std_RBNode_findCore___at___private_Lean_MetavarContext_0__Lean_MetavarContext_MkBinding_elimApp___spec__5(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_exprToSyntax___closed__4;
LEAN_EXPORT lean_object* l_Lean_Elab_Term_ensureType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Term_withoutModifyingElabMetaStateWithInfo___spec__14___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MessageData_ofList(lean_object*);
@ -344,7 +347,6 @@ lean_object* l_Std_mkHashSetImp___rarg(lean_object*);
static lean_object* l_Lean_Elab_Tactic_instInhabitedSnapshot___closed__1;
static lean_object* l_Lean_Elab_Term_isLetRecAuxMVar___lambda__2___closed__2;
static lean_object* l_Lean_Elab_Term_mkTermElabAttributeUnsafe___closed__7;
static lean_object* l_Lean_Elab_Term_exprToSyntax___closed__1;
lean_object* l_Std_PersistentHashMap_insert___at_Lean_assignExprMVar___spec__1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_getLevelNames___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFnsAux(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -379,7 +381,6 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Term_collectUnassignedMVars_go___boxed(lean
static lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___lambda__5___closed__6;
LEAN_EXPORT lean_object* l_Lean_Elab_Term_resolveLocalName_go(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_instMonadMacroAdapterTermElabM___closed__2;
static lean_object* l_Lean_Elab_Term_exprToSyntax___closed__2;
LEAN_EXPORT lean_object* l_Std_PersistentArray_anyM___at_Lean_Elab_Term_addAutoBoundImplicits_go___spec__29___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_markUsedAssignment___at_Lean_Elab_Term_ContainsPendingMVar_visit___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Term_instMetaEvalTermElabM___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -584,6 +585,7 @@ LEAN_EXPORT lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabImplic
LEAN_EXPORT lean_object* l_Lean_logAt___at_Lean_Elab_Term_traceAtCmdPos___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_throwAbortTerm___at_Lean_Elab_Term_throwMVarError___spec__2___rarg___closed__2;
LEAN_EXPORT lean_object* l_Lean_Elab_Term_withAuxDecl___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_exprToSyntax___lambda__1___closed__1;
LEAN_EXPORT lean_object* l_Lean_Elab_withMacroExpansionInfo___at_Lean_Elab_Term_withMacroExpansion___spec__1___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_PersistentArray_mapM___at_Lean_Elab_Term_withoutModifyingElabMetaStateWithInfo___spec__10(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_mkNoImplicitLambdaAnnotation(lean_object*);
@ -607,7 +609,6 @@ LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Lean_Elab_Term_addAutoBound
lean_object* l_Std_PersistentArray_get_x21___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_useImplicitLambda_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_mkConst___closed__2;
static lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15914____closed__2;
LEAN_EXPORT lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_mkSyntheticSorryFor___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_decorateErrorMessageWithLambdaImplicitVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_synthesizeInstMVarCore___lambda__2___closed__3;
@ -635,6 +636,7 @@ lean_object* l_Lean_ResolveName_resolveNamespace(lean_object*, lean_object*, lea
LEAN_EXPORT lean_object* l_Lean_markUsedAssignment___at_Lean_Elab_Term_synthesizeInstMVarCore___spec__3___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_mkTypeMismatchError___closed__3;
LEAN_EXPORT lean_object* l_Lean_Elab_Term_levelMVarToParam___lambda__1___boxed(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15915____closed__2;
static lean_object* l_Lean_Elab_Tactic_instInhabitedSnapshot___closed__21;
static lean_object* l_Lean_Elab_mkDeclName___at_Lean_Elab_Term_expandDeclId___spec__2___closed__4;
lean_object* l_Lean_Meta_mkLambdaFVars(lean_object*, lean_object*, uint8_t, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -684,7 +686,6 @@ lean_object* l_Nat_repr(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_withAuxDecl(lean_object*);
lean_object* l_Lean_Meta_getDecLevel(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_PersistentArray_mapM___at___private_Lean_Elab_Term_0__Lean_Elab_Term_withoutModifyingStateWithInfoAndMessagesImpl___spec__7___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15914____closed__1;
LEAN_EXPORT lean_object* l_Lean_Elab_addCompletionInfo___at_Lean_Elab_Term_addDotCompletionInfo___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_GetOpKind_noConfusion___rarg___lambda__1(lean_object*);
LEAN_EXPORT lean_object* l_Std_PersistentArray_anyMAux___at_Lean_Elab_Term_addAutoBoundImplicits_go___spec__14___boxed(lean_object*, lean_object*);
@ -722,6 +723,7 @@ LEAN_EXPORT lean_object* l_Std_PersistentArray_anyMAux___at_Lean_Elab_Term_addAu
static lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryCoeSort___lambda__1___closed__8;
LEAN_EXPORT lean_object* l_Lean_Elab_mkDeclName___at_Lean_Elab_Term_expandDeclId___spec__2___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*);
lean_object* l_Lean_Syntax_getId(lean_object*);
static lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15915____closed__1;
LEAN_EXPORT lean_object* l_Lean_Elab_addMacroStack___at_Lean_Elab_Term_instAddErrorMessageContextTermElabM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Tactic_instInhabitedSnapshot___closed__22;
static lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryCoeSort___lambda__1___closed__9;
@ -1015,7 +1017,6 @@ LEAN_EXPORT lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryLiftAnd
static lean_object* l_Lean_Elab_Tactic_instInhabitedSnapshot___closed__15;
static lean_object* l_Lean_Elab_Term_logUnassignedUsingErrorInfos___closed__1;
LEAN_EXPORT lean_object* l_Lean_Elab_Term_addDotCompletionInfo(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_exprToSyntax___closed__3;
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_getResetInfoTrees___at_Lean_Elab_Term_withoutModifyingElabMetaStateWithInfo___spec__2___boxed(lean_object*);
static lean_object* l_Lean_Elab_Term_MVarErrorInfo_logError___closed__12;
@ -1277,7 +1278,7 @@ static lean_object* l_Lean_Elab_Tactic_instInhabitedSnapshot___closed__17;
LEAN_EXPORT lean_object* l_ReaderT_pure___at_Lean_Elab_Term_addTermInfo___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_throwErrorIfErrors(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_getDelayedMVarAssignment_x3f___at_Lean_Elab_Term_isLetRecAuxMVar___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15914_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15915_(lean_object*);
LEAN_EXPORT lean_object* l_Std_PersistentArray_mapM___at_Lean_Elab_Term_withoutModifyingElabMetaStateWithInfo___spec__10___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_addAutoBoundImplicits(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Lean_Elab_Term_addAutoBoundImplicits_go___spec__9___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -63260,7 +63261,7 @@ return x_65;
}
}
}
static lean_object* _init_l_Lean_Elab_Term_exprToSyntax___closed__1() {
static lean_object* _init_l_Lean_Elab_Term_exprToSyntax___lambda__1___closed__1() {
_start:
{
lean_object* x_1;
@ -63268,22 +63269,22 @@ x_1 = lean_mk_string_from_bytes("m", 1);
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Term_exprToSyntax___closed__2() {
static lean_object* _init_l_Lean_Elab_Term_exprToSyntax___lambda__1___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Elab_Term_exprToSyntax___closed__1;
x_1 = l_Lean_Elab_Term_exprToSyntax___lambda__1___closed__1;
x_2 = lean_string_utf8_byte_size(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Elab_Term_exprToSyntax___closed__3() {
static lean_object* _init_l_Lean_Elab_Term_exprToSyntax___lambda__1___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Elab_Term_exprToSyntax___closed__1;
x_1 = l_Lean_Elab_Term_exprToSyntax___lambda__1___closed__1;
x_2 = lean_unsigned_to_nat(0u);
x_3 = l_Lean_Elab_Term_exprToSyntax___closed__2;
x_3 = l_Lean_Elab_Term_exprToSyntax___lambda__1___closed__2;
x_4 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -63291,17 +63292,17 @@ lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Elab_Term_exprToSyntax___closed__4() {
static lean_object* _init_l_Lean_Elab_Term_exprToSyntax___lambda__1___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Elab_Term_exprToSyntax___closed__1;
x_2 = l_Lean_Elab_Term_exprToSyntax___lambda__1___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Term_exprToSyntax(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
LEAN_EXPORT lean_object* l_Lean_Elab_Term_exprToSyntax___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
_start:
{
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31;
@ -63329,10 +63330,10 @@ lean_inc(x_10);
x_19 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_19, 0, x_10);
lean_ctor_set(x_19, 1, x_18);
x_20 = l_Lean_Elab_Term_exprToSyntax___closed__4;
x_20 = l_Lean_Elab_Term_exprToSyntax___lambda__1___closed__4;
x_21 = l_Lean_addMacroScope(x_17, x_20, x_12);
x_22 = lean_box(0);
x_23 = l_Lean_Elab_Term_exprToSyntax___closed__3;
x_23 = l_Lean_Elab_Term_exprToSyntax___lambda__1___closed__3;
x_24 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_24, 0, x_10);
lean_ctor_set(x_24, 1, x_23);
@ -63349,10 +63350,10 @@ lean_ctor_set(x_30, 1, x_29);
lean_ctor_set(x_30, 2, x_27);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_1);
x_31 = lean_infer_type(x_1, x_4, x_5, x_6, x_7, x_15);
lean_inc(x_3);
lean_inc(x_5);
x_31 = lean_infer_type(x_5, x_3, x_4, x_6, x_7, x_15);
if (lean_obj_tag(x_31) == 0)
{
lean_object* x_32; lean_object* x_33; lean_object* x_34; uint8_t x_35; lean_object* x_36;
@ -63366,12 +63367,12 @@ lean_ctor_set(x_34, 0, x_32);
x_35 = 1;
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
lean_inc(x_2);
lean_inc(x_1);
lean_inc(x_30);
x_36 = l_Lean_Elab_Term_elabTerm(x_30, x_34, x_35, x_35, x_2, x_3, x_4, x_5, x_6, x_7, x_33);
x_36 = l_Lean_Elab_Term_elabTerm(x_30, x_34, x_35, x_35, x_1, x_2, x_3, x_4, x_6, x_7, x_33);
if (lean_obj_tag(x_36) == 0)
{
lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; uint8_t x_41;
@ -63382,13 +63383,13 @@ lean_inc(x_38);
lean_dec(x_36);
x_39 = l_Lean_Expr_mvarId_x21(x_37);
lean_dec(x_37);
x_40 = l_Lean_assignExprMVar___at_Lean_Elab_Term_exprToSyntax___spec__2(x_39, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_38);
x_40 = l_Lean_assignExprMVar___at_Lean_Elab_Term_exprToSyntax___spec__2(x_39, x_5, x_1, x_2, x_3, x_4, x_6, x_7, x_38);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_41 = !lean_is_exclusive(x_40);
if (x_41 == 0)
{
@ -63473,6 +63474,20 @@ return x_52;
}
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Term_exprToSyntax(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
_start:
{
lean_object* x_9; lean_object* x_10;
x_9 = lean_alloc_closure((void*)(l_Lean_Elab_Term_exprToSyntax___lambda__1), 8, 5);
lean_closure_set(x_9, 0, x_2);
lean_closure_set(x_9, 1, x_3);
lean_closure_set(x_9, 2, x_4);
lean_closure_set(x_9, 3, x_5);
lean_closure_set(x_9, 4, x_1);
x_10 = l_Lean_Core_withFreshMacroScope___rarg(x_9, x_6, x_7, x_8);
return x_10;
}
}
LEAN_EXPORT lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Term_exprToSyntax___spec__1___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
@ -63545,7 +63560,7 @@ x_3 = lean_alloc_closure((void*)(l_Lean_Elab_withoutModifyingStateWithInfoAndMes
return x_3;
}
}
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15914____closed__1() {
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15915____closed__1() {
_start:
{
lean_object* x_1;
@ -63553,17 +63568,17 @@ x_1 = lean_mk_string_from_bytes("debug", 5);
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15914____closed__2() {
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15915____closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Term_MVarErrorInfo_logError___closed__11;
x_2 = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15914____closed__1;
x_2 = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15915____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15914_(lean_object* x_1) {
LEAN_EXPORT lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15915_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
@ -63583,7 +63598,7 @@ lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_7 = lean_ctor_get(x_6, 1);
lean_inc(x_7);
lean_dec(x_6);
x_8 = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15914____closed__2;
x_8 = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15915____closed__2;
x_9 = l_Lean_registerTraceClass(x_8, x_7);
return x_9;
}
@ -64605,19 +64620,19 @@ l_Lean_Elab_Term_expandDeclId___closed__1 = _init_l_Lean_Elab_Term_expandDeclId_
lean_mark_persistent(l_Lean_Elab_Term_expandDeclId___closed__1);
l_Lean_Elab_Term_expandDeclId___closed__2 = _init_l_Lean_Elab_Term_expandDeclId___closed__2();
lean_mark_persistent(l_Lean_Elab_Term_expandDeclId___closed__2);
l_Lean_Elab_Term_exprToSyntax___closed__1 = _init_l_Lean_Elab_Term_exprToSyntax___closed__1();
lean_mark_persistent(l_Lean_Elab_Term_exprToSyntax___closed__1);
l_Lean_Elab_Term_exprToSyntax___closed__2 = _init_l_Lean_Elab_Term_exprToSyntax___closed__2();
lean_mark_persistent(l_Lean_Elab_Term_exprToSyntax___closed__2);
l_Lean_Elab_Term_exprToSyntax___closed__3 = _init_l_Lean_Elab_Term_exprToSyntax___closed__3();
lean_mark_persistent(l_Lean_Elab_Term_exprToSyntax___closed__3);
l_Lean_Elab_Term_exprToSyntax___closed__4 = _init_l_Lean_Elab_Term_exprToSyntax___closed__4();
lean_mark_persistent(l_Lean_Elab_Term_exprToSyntax___closed__4);
l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15914____closed__1 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15914____closed__1();
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15914____closed__1);
l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15914____closed__2 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15914____closed__2();
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15914____closed__2);
res = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15914_(lean_io_mk_world());
l_Lean_Elab_Term_exprToSyntax___lambda__1___closed__1 = _init_l_Lean_Elab_Term_exprToSyntax___lambda__1___closed__1();
lean_mark_persistent(l_Lean_Elab_Term_exprToSyntax___lambda__1___closed__1);
l_Lean_Elab_Term_exprToSyntax___lambda__1___closed__2 = _init_l_Lean_Elab_Term_exprToSyntax___lambda__1___closed__2();
lean_mark_persistent(l_Lean_Elab_Term_exprToSyntax___lambda__1___closed__2);
l_Lean_Elab_Term_exprToSyntax___lambda__1___closed__3 = _init_l_Lean_Elab_Term_exprToSyntax___lambda__1___closed__3();
lean_mark_persistent(l_Lean_Elab_Term_exprToSyntax___lambda__1___closed__3);
l_Lean_Elab_Term_exprToSyntax___lambda__1___closed__4 = _init_l_Lean_Elab_Term_exprToSyntax___lambda__1___closed__4();
lean_mark_persistent(l_Lean_Elab_Term_exprToSyntax___lambda__1___closed__4);
l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15915____closed__1 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15915____closed__1();
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15915____closed__1);
l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15915____closed__2 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15915____closed__2();
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15915____closed__2);
res = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15915_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));