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

feat(library/init/lean/elaborator/command): add #preterm command for testing toPreTerm

Browse source
This commit is contained in:
Leonardo de Moura 2019-08-13 09:52:15 -07:00
parent 94c88e1333
commit 9735b979eb
6 changed files with 1281 additions and 44 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
library/init/lean/elaborator/command.lean
View file

@ -7,6 +7,7 @@ prelude
import init.lean.elaborator.alias
import init.lean.elaborator.basic
import init.lean.elaborator.resolvename
import init.lean.elaborator.preterm
namespace Lean
namespace Elab
@ -195,6 +196,13 @@ fun n => do
runIO (IO.println (toString pos ++ " " ++ toString resolvedIds));
pure ()
@[builtinCommandElab «preterm»] def elabPreTerm : CommandElab :=
fun n => do
let s := n.getArg 1;
pre ← toPreTerm s;
runIO (IO.println pre.dbgToString);
pure ()
/- We just ignore Lean3 notation declaration commands. -/
@[builtinCommandElab «mixfix»] def elabMixfix : CommandElab := fun _ => pure ()
@[builtinCommandElab «reserve»] def elabReserve : CommandElab := fun _ => pure ()

27
library/init/lean/elaborator/preterm.lean
View file

@ -26,7 +26,7 @@ do m ← builtinPreTermElabTable.get;
builtinPreTermElabTable.modify $ fun m => m.insert k elab
def declareBuiltinPreTermElab (env : Environment) (kind : SyntaxNodeKind) (declName : Name) : IO Environment :=
declareBuiltinElab env `Lean.addBuiltinTermElab kind declName
declareBuiltinElab env `Lean.addBuiltinPreTermElab kind declName
@[init] def registerBuiltinPreTermElabAttr : IO Unit :=
registerAttribute {
@ -45,4 +45,29 @@ registerAttribute {
applicationTime := AttributeApplicationTime.afterCompilation
}
def Expr.mkAnnotation (ann : Name) (e : Expr) :=
Expr.mdata (MData.empty.setName `annotation ann) e
private def dummy : Expr := Expr.const `Prop []
namespace Elab
def toPreTerm (stx : Syntax) : Elab PreTerm :=
stx.ifNode
(fun n => do
s ← get;
table ← runIO builtinPreTermElabTable.get;
let k := n.getKind;
match table.find k with
| some fn => fn n
| none => logErrorAndThrow stx ("`toPreTerm` failed, no support for syntax '" ++ toString k ++ "'"))
(fun _ => throw "`toPreTerm` failed, unexpected syntax")
@[builtinPreTermElab «type»] def convertType : PreTermElab :=
fun _ => pure $ Expr.sort $ Level.succ Level.zero
@[builtinPreTermElab «sort»] def convertSort : PreTermElab :=
fun _ => pure $ Expr.sort Level.zero
end Elab
end Lean

1
library/init/lean/parser/command.lean
View file

@ -82,6 +82,7 @@ declModifiers >> («abbrev» <|> «def» <|> «theorem» <|> «constant» <|> «
@[builtinCommandParser] def check := parser! "#check " >> termParser
@[builtinCommandParser] def exit := parser! "#exit"
@[builtinCommandParser] def «resolve_name» := parser! "#resolve_name " >> ident
@[builtinCommandParser] def «preterm» := parser! "#preterm " >> termParser
@[builtinCommandParser] def «init_quot» := parser! "init_quot"
@[builtinCommandParser] def «set_option» := parser! "set_option " >> ident >> (symbolOrIdent "true" <|> symbolOrIdent "false" <|> strLit <|> numLit)
@[builtinCommandParser] def «attribute» := parser! optional "local " >> "attribute " >> "[" >> sepBy1 attrInstance ", " >> "]" >> many1 ident

288
src/stage0/init/lean/elaborator/command.cpp generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: init.lean.elaborator.command
// Imports: init.lean.elaborator.alias init.lean.elaborator.basic init.lean.elaborator.resolvename
// Imports: init.lean.elaborator.alias init.lean.elaborator.basic init.lean.elaborator.resolvename init.lean.elaborator.preterm
#include "runtime/object.h"
#include "runtime/apply.h"
typedef lean::object obj; typedef lean::usize usize;
@ -44,6 +44,7 @@ obj* l_Lean_Elab_elabOpen(obj*, obj*, obj*);
obj* l___regBuiltinTermElab_Lean_Elab_elabMixfix___closed__2;
extern obj* l_Lean_Parser_Command_export___elambda__1___closed__2;
obj* l_List_lengthAux___main___rarg(obj*, obj*);
extern "C" obj* lean_expr_dbg_to_string(obj*);
obj* l___regBuiltinTermElab_Lean_Elab_elabNotation___closed__1;
obj* l_Lean_Elab_elabEnd___closed__4;
obj* l___regBuiltinTermElab_Lean_Elab_elabUniverse___closed__2;
@ -78,6 +79,7 @@ obj* l___regBuiltinTermElab_Lean_Elab_elabOpen___closed__3;
obj* l_Lean_Name_toStringWithSep___main(obj*, obj*);
obj* l___regBuiltinTermElab_Lean_Elab_elabUniverse(obj*);
obj* l___regBuiltinTermElab_Lean_Elab_elabUniverse___closed__3;
extern obj* l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__2;
obj* l_Lean_Elab_addUniverse___closed__1;
obj* l_Lean_Elab_elabOpenOnly___boxed(obj*, obj*, obj*);
obj* l_Lean_Elab_addUniverse(obj*, obj*, obj*);
@ -104,7 +106,6 @@ extern obj* l_List_repr___rarg___closed__2;
obj* l_Lean_Elab_getNamespace___rarg(obj*);
obj* l_Lean_Elab_elabOpenRenaming(obj*, obj*, obj*);
extern obj* l_Lean_Parser_Command_mixfix___elambda__1___closed__2;
obj* l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__5;
extern obj* l_Lean_Parser_Command_openHiding___elambda__1___closed__2;
obj* l_Lean_addAlias(obj*, obj*, obj*);
extern obj* l_Lean_Parser_Command_universes___elambda__1___closed__2;
@ -159,6 +160,7 @@ obj* l_Lean_Elab_elabEnd___closed__6;
uint8 l_Lean_Name_eqStr(obj*, obj*);
uint8 l_List_elem___main___at_Lean_Parser_addBuiltinLeadingParser___spec__4(obj*, obj*);
obj* l_Lean_Elab_elabUniverses___boxed(obj*, obj*, obj*);
obj* l_Lean_Elab_elabPreTerm___boxed(obj*, obj*, obj*);
obj* l_Array_miterateAux___main___at_Lean_Elab_elabExport___spec__1___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
extern obj* l_Sigma_HasRepr___rarg___closed__2;
obj* l_Lean_Syntax_mfoldArgsAux___main___at_Lean_Elab_elabOpenHiding___spec__1___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
@ -176,11 +178,12 @@ obj* l___regBuiltinTermElab_Lean_Elab_elabResolveName___closed__1;
obj* l_Lean_logUnknownDecl(obj*, obj*, obj*, obj*);
obj* l_List_toString___at_Lean_Elab_elabResolveName___spec__1(obj*);
obj* l_Lean_Elab_elabEnd(obj*, obj*, obj*);
obj* l_Lean_Elab_toPreTerm(obj*, obj*, obj*);
obj* l_Lean_Syntax_mfoldArgsAux___main___at_Lean_Elab_elabUniverses___spec__1___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_Lean_Elab_elabEnd___closed__5;
obj* l_Array_size(obj*, obj*);
extern obj* l_Lean_Parser_Command_section___elambda__1___rarg___closed__2;
obj* l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__4;
obj* l___regBuiltinTermElab_Lean_Elab_elabPreTerm___closed__2;
obj* l_Array_get(obj*, obj*, obj*, obj*);
obj* l___regBuiltinTermElab_Lean_Elab_elabNotation___closed__2;
obj* l___regBuiltinTermElab_Lean_Elab_elabExport(obj*);
@ -191,7 +194,7 @@ obj* l___regBuiltinTermElab_Lean_Elab_elabInitQuot___closed__2;
obj* l___regBuiltinTermElab_Lean_Elab_elabNamespace(obj*);
obj* l_Lean_Syntax_mfoldArgsAux___main___at_Lean_Elab_elabOpenSimple___spec__1(obj*, obj*, obj*, obj*, obj*, obj*);
obj* l___regBuiltinTermElab_Lean_Elab_elabSection___closed__1;
extern obj* l_Lean_nameToExprAux___main___closed__4;
obj* l___regBuiltinTermElab_Lean_Elab_elabPreTerm___closed__3;
extern obj* l_Lean_Name_toString___closed__1;
obj* l___private_init_lean_elaborator_command_4__checkEndHeader___boxed(obj*, obj*);
uint8 l_Lean_Environment_contains(obj*, obj*);
@ -207,9 +210,12 @@ extern obj* l_Lean_Parser_Command_reserve___elambda__1___closed__2;
obj* l___regBuiltinTermElab_Lean_Elab_elabEnd___closed__1;
obj* l_Lean_Elab_elabInitQuot___boxed(obj*);
obj* l_Lean_Elab_elabMixfix(obj*, obj*);
obj* l___regBuiltinTermElab_Lean_Elab_elabPreTerm___closed__1;
uint8 l___private_init_lean_elaborator_command_4__checkEndHeader(obj*, obj*);
obj* l_Lean_Elab_elabOpenHiding___boxed(obj*, obj*, obj*);
obj* l_Lean_Elab_elabPreTerm(obj*, obj*, obj*);
obj* l_Lean_Elab_elabNotation(obj*, obj*);
obj* l___regBuiltinTermElab_Lean_Elab_elabPreTerm(obj*);
obj* l_Lean_Elab_modifyScope___boxed(obj*, obj*, obj*);
obj* l_Lean_Elab_elabReserve(obj*, obj*);
obj* l_Lean_Syntax_mfoldArgsAux___main___at_Lean_Elab_elabOpenSimple___spec__1___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
@ -221,6 +227,7 @@ obj* l_Lean_Syntax_mfoldArgsAux___main___at_Lean_Elab_elabOpenRenaming___spec__1
obj* l_Lean_Syntax_mfoldArgsAux___main___at_Lean_Elab_elabOpenOnly___spec__1___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
obj* l___regBuiltinTermElab_Lean_Elab_elabMixfix___closed__3;
extern obj* l_Lean_Parser_Command_universe___elambda__1___rarg___closed__2;
extern obj* l___regBuiltinTermElab_Lean_Elab_convertType___closed__2;
obj* l_Lean_Elab_elabUniverse(obj*, obj*, obj*);
obj* l_Lean_Elab_modifyScope___at_Lean_Elab_addUniverse___spec__1(obj*, obj*, obj*);
extern obj* l_List_repr___rarg___closed__1;
@ -801,7 +808,7 @@ obj* _init_l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__1() {
_start:
{
obj* x_1;
x_1 = lean::mk_string("Elab");
x_1 = lean::mk_string("elabNamespace");
return x_1;
}
}
@ -809,7 +816,7 @@ obj* _init_l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__2() {
_start:
{
obj* x_1; obj* x_2; obj* x_3;
x_1 = l_Lean_nameToExprAux___main___closed__4;
x_1 = l___regBuiltinTermElab_Lean_Elab_convertType___closed__2;
x_2 = l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
@ -819,24 +826,6 @@ obj* _init_l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__3() {
_start:
{
obj* x_1;
x_1 = lean::mk_string("elabNamespace");
return x_1;
}
}
obj* _init_l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__4() {
_start:
{
obj* x_1; obj* x_2; obj* x_3;
x_1 = l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__2;
x_2 = l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__3;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
obj* _init_l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__5() {
_start:
{
obj* x_1;
x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Elab_elabNamespace___boxed), 3, 0);
return x_1;
}
@ -846,8 +835,8 @@ _start:
{
obj* x_2; obj* x_3; obj* x_4; obj* x_5;
x_2 = l_Lean_Parser_Command_namespace___elambda__1___rarg___closed__2;
x_3 = l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__4;
x_4 = l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__5;
x_3 = l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__2;
x_4 = l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__3;
x_5 = l_Lean_addBuiltinCommandElab(x_2, x_3, x_4, x_1);
return x_5;
}
@ -1160,7 +1149,7 @@ obj* _init_l___regBuiltinTermElab_Lean_Elab_elabSection___closed__2() {
_start:
{
obj* x_1; obj* x_2; obj* x_3;
x_1 = l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__2;
x_1 = l___regBuiltinTermElab_Lean_Elab_convertType___closed__2;
x_2 = l___regBuiltinTermElab_Lean_Elab_elabSection___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
@ -1746,7 +1735,7 @@ obj* _init_l___regBuiltinTermElab_Lean_Elab_elabEnd___closed__2() {
_start:
{
obj* x_1; obj* x_2; obj* x_3;
x_1 = l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__2;
x_1 = l___regBuiltinTermElab_Lean_Elab_convertType___closed__2;
x_2 = l___regBuiltinTermElab_Lean_Elab_elabEnd___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
@ -2759,7 +2748,7 @@ obj* _init_l___regBuiltinTermElab_Lean_Elab_elabExport___closed__2() {
_start:
{
obj* x_1; obj* x_2; obj* x_3;
x_1 = l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__2;
x_1 = l___regBuiltinTermElab_Lean_Elab_convertType___closed__2;
x_2 = l___regBuiltinTermElab_Lean_Elab_elabExport___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
@ -5234,7 +5223,7 @@ obj* _init_l___regBuiltinTermElab_Lean_Elab_elabOpen___closed__2() {
_start:
{
obj* x_1; obj* x_2; obj* x_3;
x_1 = l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__2;
x_1 = l___regBuiltinTermElab_Lean_Elab_convertType___closed__2;
x_2 = l___regBuiltinTermElab_Lean_Elab_elabOpen___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
@ -5839,7 +5828,7 @@ obj* _init_l___regBuiltinTermElab_Lean_Elab_elabUniverse___closed__2() {
_start:
{
obj* x_1; obj* x_2; obj* x_3;
x_1 = l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__2;
x_1 = l___regBuiltinTermElab_Lean_Elab_convertType___closed__2;
x_2 = l___regBuiltinTermElab_Lean_Elab_elabUniverse___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
@ -6016,7 +6005,7 @@ obj* _init_l___regBuiltinTermElab_Lean_Elab_elabUniverses___closed__2() {
_start:
{
obj* x_1; obj* x_2; obj* x_3;
x_1 = l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__2;
x_1 = l___regBuiltinTermElab_Lean_Elab_convertType___closed__2;
x_2 = l___regBuiltinTermElab_Lean_Elab_elabUniverses___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
@ -6177,7 +6166,7 @@ obj* _init_l___regBuiltinTermElab_Lean_Elab_elabInitQuot___closed__2() {
_start:
{
obj* x_1; obj* x_2; obj* x_3;
x_1 = l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__2;
x_1 = l___regBuiltinTermElab_Lean_Elab_convertType___closed__2;
x_2 = l___regBuiltinTermElab_Lean_Elab_elabInitQuot___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
@ -6711,7 +6700,7 @@ obj* _init_l___regBuiltinTermElab_Lean_Elab_elabResolveName___closed__2() {
_start:
{
obj* x_1; obj* x_2; obj* x_3;
x_1 = l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__2;
x_1 = l___regBuiltinTermElab_Lean_Elab_convertType___closed__2;
x_2 = l___regBuiltinTermElab_Lean_Elab_elabResolveName___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
@ -6736,6 +6725,216 @@ x_5 = l_Lean_addBuiltinCommandElab(x_2, x_3, x_4, x_1);
return x_5;
}
}
obj* l_Lean_Elab_elabPreTerm(obj* x_1, obj* x_2, obj* x_3) {
_start:
{
obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8;
x_4 = lean::cnstr_get(x_1, 1);
x_5 = lean::box(0);
x_6 = lean::mk_nat_obj(1u);
x_7 = lean::array_get(x_5, x_4, x_6);
lean::inc(x_2);
x_8 = l_Lean_Elab_toPreTerm(x_7, x_2, x_3);
if (lean::obj_tag(x_8) == 0)
{
uint8 x_9;
x_9 = !lean::is_exclusive(x_8);
if (x_9 == 0)
{
obj* x_10; obj* x_11; obj* x_12; obj* x_13; obj* x_14;
x_10 = lean::cnstr_get(x_8, 0);
x_11 = lean::box(0);
lean::cnstr_set(x_8, 0, x_11);
x_12 = lean_expr_dbg_to_string(x_10);
lean::dec(x_10);
x_13 = lean::alloc_closure(reinterpret_cast<void*>(l_IO_println___at_HasRepr_HasEval___spec__1___boxed), 2, 1);
lean::closure_set(x_13, 0, x_12);
x_14 = l_Lean_Elab_runIOUnsafe___rarg(x_13, x_2, x_8);
lean::dec(x_2);
if (lean::obj_tag(x_14) == 0)
{
uint8 x_15;
x_15 = !lean::is_exclusive(x_14);
if (x_15 == 0)
{
obj* x_16;
x_16 = lean::cnstr_get(x_14, 0);
lean::dec(x_16);
lean::cnstr_set(x_14, 0, x_11);
return x_14;
}
else
{
obj* x_17; obj* x_18;
x_17 = lean::cnstr_get(x_14, 1);
lean::inc(x_17);
lean::dec(x_14);
x_18 = lean::alloc_cnstr(0, 2, 0);
lean::cnstr_set(x_18, 0, x_11);
lean::cnstr_set(x_18, 1, x_17);
return x_18;
}
}
else
{
uint8 x_19;
x_19 = !lean::is_exclusive(x_14);
if (x_19 == 0)
{
return x_14;
}
else
{
obj* x_20; obj* x_21; obj* x_22;
x_20 = lean::cnstr_get(x_14, 0);
x_21 = lean::cnstr_get(x_14, 1);
lean::inc(x_21);
lean::inc(x_20);
lean::dec(x_14);
x_22 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_22, 0, x_20);
lean::cnstr_set(x_22, 1, x_21);
return x_22;
}
}
}
else
{
obj* x_23; obj* x_24; obj* x_25; obj* x_26; obj* x_27; obj* x_28; obj* x_29;
x_23 = lean::cnstr_get(x_8, 0);
x_24 = lean::cnstr_get(x_8, 1);
lean::inc(x_24);
lean::inc(x_23);
lean::dec(x_8);
x_25 = lean::box(0);
x_26 = lean::alloc_cnstr(0, 2, 0);
lean::cnstr_set(x_26, 0, x_25);
lean::cnstr_set(x_26, 1, x_24);
x_27 = lean_expr_dbg_to_string(x_23);
lean::dec(x_23);
x_28 = lean::alloc_closure(reinterpret_cast<void*>(l_IO_println___at_HasRepr_HasEval___spec__1___boxed), 2, 1);
lean::closure_set(x_28, 0, x_27);
x_29 = l_Lean_Elab_runIOUnsafe___rarg(x_28, x_2, x_26);
lean::dec(x_2);
if (lean::obj_tag(x_29) == 0)
{
obj* x_30; obj* x_31; obj* x_32;
x_30 = lean::cnstr_get(x_29, 1);
lean::inc(x_30);
if (lean::is_exclusive(x_29)) {
lean::cnstr_release(x_29, 0);
lean::cnstr_release(x_29, 1);
x_31 = x_29;
} else {
lean::dec_ref(x_29);
x_31 = lean::box(0);
}
if (lean::is_scalar(x_31)) {
x_32 = lean::alloc_cnstr(0, 2, 0);
} else {
x_32 = x_31;
}
lean::cnstr_set(x_32, 0, x_25);
lean::cnstr_set(x_32, 1, x_30);
return x_32;
}
else
{
obj* x_33; obj* x_34; obj* x_35; obj* x_36;
x_33 = lean::cnstr_get(x_29, 0);
lean::inc(x_33);
x_34 = lean::cnstr_get(x_29, 1);
lean::inc(x_34);
if (lean::is_exclusive(x_29)) {
lean::cnstr_release(x_29, 0);
lean::cnstr_release(x_29, 1);
x_35 = x_29;
} else {
lean::dec_ref(x_29);
x_35 = lean::box(0);
}
if (lean::is_scalar(x_35)) {
x_36 = lean::alloc_cnstr(1, 2, 0);
} else {
x_36 = x_35;
}
lean::cnstr_set(x_36, 0, x_33);
lean::cnstr_set(x_36, 1, x_34);
return x_36;
}
}
}
else
{
uint8 x_37;
lean::dec(x_2);
x_37 = !lean::is_exclusive(x_8);
if (x_37 == 0)
{
return x_8;
}
else
{
obj* x_38; obj* x_39; obj* x_40;
x_38 = lean::cnstr_get(x_8, 0);
x_39 = lean::cnstr_get(x_8, 1);
lean::inc(x_39);
lean::inc(x_38);
lean::dec(x_8);
x_40 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_40, 0, x_38);
lean::cnstr_set(x_40, 1, x_39);
return x_40;
}
}
}
}
obj* l_Lean_Elab_elabPreTerm___boxed(obj* x_1, obj* x_2, obj* x_3) {
_start:
{
obj* x_4;
x_4 = l_Lean_Elab_elabPreTerm(x_1, x_2, x_3);
lean::dec(x_1);
return x_4;
}
}
obj* _init_l___regBuiltinTermElab_Lean_Elab_elabPreTerm___closed__1() {
_start:
{
obj* x_1;
x_1 = lean::mk_string("elabPreTerm");
return x_1;
}
}
obj* _init_l___regBuiltinTermElab_Lean_Elab_elabPreTerm___closed__2() {
_start:
{
obj* x_1; obj* x_2; obj* x_3;
x_1 = l___regBuiltinTermElab_Lean_Elab_convertType___closed__2;
x_2 = l___regBuiltinTermElab_Lean_Elab_elabPreTerm___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
obj* _init_l___regBuiltinTermElab_Lean_Elab_elabPreTerm___closed__3() {
_start:
{
obj* x_1;
x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Elab_elabPreTerm___boxed), 3, 0);
return x_1;
}
}
obj* l___regBuiltinTermElab_Lean_Elab_elabPreTerm(obj* x_1) {
_start:
{
obj* x_2; obj* x_3; obj* x_4; obj* x_5;
x_2 = l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__2;
x_3 = l___regBuiltinTermElab_Lean_Elab_elabPreTerm___closed__2;
x_4 = l___regBuiltinTermElab_Lean_Elab_elabPreTerm___closed__3;
x_5 = l_Lean_addBuiltinCommandElab(x_2, x_3, x_4, x_1);
return x_5;
}
}
obj* l_Lean_Elab_elabMixfix___rarg(obj* x_1) {
_start:
{
@ -6794,7 +6993,7 @@ obj* _init_l___regBuiltinTermElab_Lean_Elab_elabMixfix___closed__2() {
_start:
{
obj* x_1; obj* x_2; obj* x_3;
x_1 = l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__2;
x_1 = l___regBuiltinTermElab_Lean_Elab_convertType___closed__2;
x_2 = l___regBuiltinTermElab_Lean_Elab_elabMixfix___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
@ -6877,7 +7076,7 @@ obj* _init_l___regBuiltinTermElab_Lean_Elab_elabReserve___closed__2() {
_start:
{
obj* x_1; obj* x_2; obj* x_3;
x_1 = l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__2;
x_1 = l___regBuiltinTermElab_Lean_Elab_convertType___closed__2;
x_2 = l___regBuiltinTermElab_Lean_Elab_elabReserve___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
@ -6960,7 +7159,7 @@ obj* _init_l___regBuiltinTermElab_Lean_Elab_elabNotation___closed__2() {
_start:
{
obj* x_1; obj* x_2; obj* x_3;
x_1 = l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__2;
x_1 = l___regBuiltinTermElab_Lean_Elab_convertType___closed__2;
x_2 = l___regBuiltinTermElab_Lean_Elab_elabNotation___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
@ -6988,6 +7187,7 @@ return x_5;
obj* initialize_init_lean_elaborator_alias(obj*);
obj* initialize_init_lean_elaborator_basic(obj*);
obj* initialize_init_lean_elaborator_resolvename(obj*);
obj* initialize_init_lean_elaborator_preterm(obj*);
static bool _G_initialized = false;
obj* initialize_init_lean_elaborator_command(obj* w) {
if (_G_initialized) return w;
@ -6999,16 +7199,14 @@ w = initialize_init_lean_elaborator_basic(w);
if (io_result_is_error(w)) return w;
w = initialize_init_lean_elaborator_resolvename(w);
if (io_result_is_error(w)) return w;
w = initialize_init_lean_elaborator_preterm(w);
if (io_result_is_error(w)) return w;
l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__1 = _init_l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__1();
lean::mark_persistent(l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__1);
l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__2 = _init_l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__2();
lean::mark_persistent(l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__2);
l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__3 = _init_l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__3();
lean::mark_persistent(l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__3);
l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__4 = _init_l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__4();
lean::mark_persistent(l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__4);
l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__5 = _init_l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__5();
lean::mark_persistent(l___regBuiltinTermElab_Lean_Elab_elabNamespace___closed__5);
w = l___regBuiltinTermElab_Lean_Elab_elabNamespace(w);
if (io_result_is_error(w)) return w;
l___regBuiltinTermElab_Lean_Elab_elabSection___closed__1 = _init_l___regBuiltinTermElab_Lean_Elab_elabSection___closed__1();
@ -7095,6 +7293,14 @@ l___regBuiltinTermElab_Lean_Elab_elabResolveName___closed__3 = _init_l___regBuil
lean::mark_persistent(l___regBuiltinTermElab_Lean_Elab_elabResolveName___closed__3);
w = l___regBuiltinTermElab_Lean_Elab_elabResolveName(w);
if (io_result_is_error(w)) return w;
l___regBuiltinTermElab_Lean_Elab_elabPreTerm___closed__1 = _init_l___regBuiltinTermElab_Lean_Elab_elabPreTerm___closed__1();
lean::mark_persistent(l___regBuiltinTermElab_Lean_Elab_elabPreTerm___closed__1);
l___regBuiltinTermElab_Lean_Elab_elabPreTerm___closed__2 = _init_l___regBuiltinTermElab_Lean_Elab_elabPreTerm___closed__2();
lean::mark_persistent(l___regBuiltinTermElab_Lean_Elab_elabPreTerm___closed__2);
l___regBuiltinTermElab_Lean_Elab_elabPreTerm___closed__3 = _init_l___regBuiltinTermElab_Lean_Elab_elabPreTerm___closed__3();
lean::mark_persistent(l___regBuiltinTermElab_Lean_Elab_elabPreTerm___closed__3);
w = l___regBuiltinTermElab_Lean_Elab_elabPreTerm(w);
if (io_result_is_error(w)) return w;
l___regBuiltinTermElab_Lean_Elab_elabMixfix___closed__1 = _init_l___regBuiltinTermElab_Lean_Elab_elabMixfix___closed__1();
lean::mark_persistent(l___regBuiltinTermElab_Lean_Elab_elabMixfix___closed__1);
l___regBuiltinTermElab_Lean_Elab_elabMixfix___closed__2 = _init_l___regBuiltinTermElab_Lean_Elab_elabMixfix___closed__2();

712
src/stage0/init/lean/elaborator/preterm.cpp generated
View file

@ -14,21 +14,29 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64;
#pragma GCC diagnostic ignored "-Wunused-label"
#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
#endif
extern "C" obj* lean_expr_mk_mdata(obj*, obj*);
obj* l_Lean_addBuiltinPreTermElab(obj*, obj*, obj*, obj*);
obj* l_Lean_registerBuiltinPreTermElabAttr___closed__2;
obj* l_Lean_registerBuiltinPreTermElabAttr___closed__3;
obj* l_Lean_registerBuiltinPreTermElabAttr___closed__5;
extern "C" uint8 lean_name_dec_eq(obj*, obj*);
extern "C" obj* lean_expr_mk_sort(obj*);
obj* l_HashMapImp_find___at_Lean_Elab_toPreTerm___spec__1(obj*, obj*);
obj* l_Lean_Elab_runIOUnsafe___rarg(obj*, obj*, obj*);
obj* l_Array_mkArray(obj*, obj*, obj*);
obj* l_Lean_builtinPreTermElabTable;
extern obj* l_Lean_declareBuiltinTermElab___closed__2;
obj* l_Lean_Elab_convertType___rarg(obj*);
obj* l_Lean_registerBuiltinPreTermElabAttr___lambda__1___closed__4;
extern obj* l_Lean_AttributeImpl_inhabited___closed__5;
obj* l_HashMapImp_insert___at_Lean_addBuiltinPreTermElab___spec__3(obj*, obj*, obj*);
extern obj* l_Lean_addBuiltinTermElab___closed__2;
obj* l_Lean_mkBuiltinPreTermElabTable___closed__1;
obj* l___regBuiltinTermElab_Lean_Elab_convertSort___closed__3;
obj* l_Lean_registerAttribute(obj*, obj*);
obj* l_Lean_registerBuiltinPreTermElabAttr___closed__7;
obj* l_Lean_Elab_convertSort___boxed(obj*, obj*);
obj* l___regBuiltinTermElab_Lean_Elab_convertType___closed__5;
obj* l_Lean_Elab_convertType(obj*, obj*);
obj* l_Array_uget(obj*, obj*, usize, obj*);
obj* l_Lean_Name_toStringWithSep___main(obj*, obj*);
extern obj* l_Lean_mkInitAttr___lambda__1___closed__1;
@ -36,23 +44,44 @@ obj* l_Array_uset(obj*, obj*, usize, obj*, obj*);
uint8 l_AssocList_contains___main___at_Lean_addBuiltinPreTermElab___spec__2(obj*, obj*);
obj* l_IO_Prim_Ref_set(obj*, obj*, obj*, obj*);
obj* l_Lean_registerBuiltinPreTermElabAttr___closed__4;
obj* l_Lean_Elab_toPreTerm___closed__2;
obj* l_Lean_declareBuiltinPreTermElab___closed__2;
obj* l___regBuiltinTermElab_Lean_Elab_convertType___closed__1;
obj* l_AssocList_find___main___at_Lean_Elab_toPreTerm___spec__2(obj*, obj*);
obj* l___private_init_lean_elaborator_preterm_1__dummy___closed__1;
obj* l_IO_Prim_Ref_get___boxed(obj*, obj*, obj*);
obj* l___regBuiltinTermElab_Lean_Elab_convertType___closed__3;
obj* l___regBuiltinTermElab_Lean_Elab_convertSort___closed__2;
obj* l_Lean_registerBuiltinPreTermElabAttr___lambda__1___closed__3;
obj* l_Lean_declareBuiltinPreTermElab___closed__1;
obj* l_mkHashMap___at_Lean_mkBuiltinPreTermElabTable___spec__1(obj*);
extern obj* l_Lean_AttributeImpl_inhabited___closed__4;
obj* l_Lean_registerTagAttribute___lambda__5___boxed(obj*, obj*, obj*, obj*, obj*);
obj* l___private_init_lean_elaborator_preterm_1__dummy;
obj* l_Lean_registerBuiltinPreTermElabAttr___closed__1;
obj* l_HashMapImp_find___at_Lean_Elab_toPreTerm___spec__1___boxed(obj*, obj*);
obj* l_Lean_registerBuiltinPreTermElabAttr(obj*);
extern "C" obj* lean_expr_mk_const(obj*, obj*);
obj* l_Lean_Elab_convertSort(obj*, obj*);
extern "C" usize lean_name_hash_usize(obj*);
obj* l_Lean_Elab_toPreTerm___closed__1;
extern obj* l_Lean_Parser_Term_prop___elambda__1___rarg___closed__3;
namespace lean {
obj* string_append(obj*, obj*);
}
obj* l_Lean_registerBuiltinPreTermElabAttr___lambda__1___boxed(obj*, obj*, obj*, obj*, obj*);
obj* l_Lean_KVMap_setName(obj*, obj*, obj*);
extern obj* l_Lean_Parser_Term_sort___elambda__1___rarg___closed__2;
extern obj* l_Lean_Parser_Term_type___elambda__1___rarg___closed__2;
obj* l_Lean_registerBuiltinPreTermElabAttr___lambda__1___closed__1;
namespace lean {
uint8 nat_dec_lt(obj*, obj*);
}
obj* l_HashMapImp_contains___at_Lean_addBuiltinPreTermElab___spec__1___boxed(obj*, obj*);
extern obj* l_Char_HasRepr___closed__1;
extern obj* l_Lean_addBuiltinTermElab___closed__1;
obj* l___regBuiltinTermElab_Lean_Elab_convertType___closed__4;
obj* l___private_init_lean_elaborator_preterm_1__dummy___closed__2;
obj* l_Array_fget(obj*, obj*, obj*);
extern "C" obj* lean_name_mk_string(obj*, obj*);
obj* l_Lean_registerBuiltinPreTermElabAttr___lambda__1(obj*, obj*, obj*, uint8, obj*);
@ -61,41 +90,58 @@ obj* nat_add(obj*, obj*);
}
uint8 l_HashMapImp_contains___at_Lean_addBuiltinPreTermElab___spec__1(obj*, obj*);
extern obj* l_Lean_Parser_Term_explicitUniv___elambda__1___closed__2;
obj* l_Lean_Elab_convertSort___rarg(obj*);
obj* l_Lean_addBuiltinPreTermElab___boxed(obj*, obj*, obj*, obj*);
obj* l_AssocList_find___main___at_Lean_Elab_toPreTerm___spec__2___boxed(obj*, obj*);
obj* l_Lean_syntaxNodeKindOfAttrParam(obj*, obj*, obj*, obj*);
obj* l_Lean_registerBuiltinPreTermElabAttr___closed__6;
obj* l_IO_Prim_mkRef(obj*, obj*, obj*);
obj* l_HashMapImp_expand___at_Lean_addBuiltinPreTermElab___spec__4(obj*, obj*);
obj* l___regBuiltinTermElab_Lean_Elab_convertType(obj*);
extern obj* l_Lean_Level_one___closed__1;
obj* l_HashMapImp_moveEntries___main___at_Lean_addBuiltinPreTermElab___spec__5(obj*, obj*, obj*);
obj* l_Lean_Elab_toPreTerm___closed__3;
extern obj* l_System_FilePath_dirName___closed__1;
obj* l_IO_Prim_Ref_get(obj*, obj*, obj*);
obj* l_Lean_Expr_mkAnnotation___closed__1;
namespace lean {
usize usize_modn(usize, obj*);
}
obj* l_Lean_ConstantInfo_type(obj*);
obj* l_Lean_Expr_mkAnnotation(obj*, obj*);
obj* l_Lean_mkBuiltinPreTermElabTable(obj*);
namespace lean {
obj* environment_find_core(obj*, obj*);
}
obj* l___regBuiltinTermElab_Lean_Elab_convertSort___closed__1;
obj* l_Lean_Elab_toPreTerm(obj*, obj*, obj*);
obj* l_AssocList_mfoldl___main___at_Lean_addBuiltinPreTermElab___spec__6(obj*, obj*);
obj* l_Array_size(obj*, obj*);
obj* l_Array_fset(obj*, obj*, obj*, obj*);
obj* l_Lean_Elab_convertType___boxed(obj*, obj*);
obj* l_mkHashMapImp___rarg(obj*);
obj* l_Lean_registerBuiltinPreTermElabAttr___lambda__1___closed__2;
extern obj* l_Lean_nameToExprAux___main___closed__4;
namespace lean {
uint8 nat_dec_le(obj*, obj*);
}
obj* l___regBuiltinTermElab_Lean_Elab_convertSort(obj*);
obj* l_AssocList_replace___main___at_Lean_addBuiltinPreTermElab___spec__7(obj*, obj*, obj*);
obj* l_Lean_declareBuiltinElab(obj*, obj*, obj*, obj*, obj*);
namespace lean {
obj* nat_mul(obj*, obj*);
}
obj* l_AssocList_contains___main___at_Lean_addBuiltinPreTermElab___spec__2___boxed(obj*, obj*);
obj* l_Lean_Expr_mkAnnotation___closed__2;
obj* l___regBuiltinTermElab_Lean_Elab_convertType___closed__2;
obj* l_IO_Prim_Ref_reset(obj*, obj*, obj*);
obj* l_Lean_Elab_convertType___rarg___closed__1;
extern obj* l_Lean_exprIsInhabited___closed__1;
obj* l_Lean_registerBuiltinPreTermElabAttr___lambda__1___closed__5;
obj* l_Lean_declareBuiltinPreTermElab(obj*, obj*, obj*, obj*);
obj* l_Lean_logErrorAndThrow___rarg(obj*, obj*, obj*, obj*);
obj* l_Lean_registerTagAttribute___lambda__6___boxed(obj*, obj*, obj*, obj*, obj*);
obj* l_Lean_Elab_toPreTerm___closed__4;
obj* l_mkHashMap___at_Lean_mkBuiltinPreTermElabTable___spec__1(obj* x_1) {
_start:
{
@ -857,11 +903,29 @@ lean::dec(x_2);
return x_5;
}
}
obj* _init_l_Lean_declareBuiltinPreTermElab___closed__1() {
_start:
{
obj* x_1;
x_1 = lean::mk_string("addBuiltinPreTermElab");
return x_1;
}
}
obj* _init_l_Lean_declareBuiltinPreTermElab___closed__2() {
_start:
{
obj* x_1; obj* x_2; obj* x_3;
x_1 = l_Lean_nameToExprAux___main___closed__4;
x_2 = l_Lean_declareBuiltinPreTermElab___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
obj* l_Lean_declareBuiltinPreTermElab(obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
_start:
{
obj* x_5; obj* x_6;
x_5 = l_Lean_declareBuiltinTermElab___closed__2;
x_5 = l_Lean_declareBuiltinPreTermElab___closed__2;
x_6 = l_Lean_declareBuiltinElab(x_1, x_5, x_2, x_3, x_4);
return x_6;
}
@ -1325,6 +1389,606 @@ lean::dec(x_3);
return x_7;
}
}
obj* _init_l_Lean_Expr_mkAnnotation___closed__1() {
_start:
{
obj* x_1;
x_1 = lean::mk_string("annotation");
return x_1;
}
}
obj* _init_l_Lean_Expr_mkAnnotation___closed__2() {
_start:
{
obj* x_1; obj* x_2; obj* x_3;
x_1 = lean::box(0);
x_2 = l_Lean_Expr_mkAnnotation___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
obj* l_Lean_Expr_mkAnnotation(obj* x_1, obj* x_2) {
_start:
{
obj* x_3; obj* x_4; obj* x_5; obj* x_6;
x_3 = lean::box(0);
x_4 = l_Lean_Expr_mkAnnotation___closed__2;
x_5 = l_Lean_KVMap_setName(x_3, x_4, x_1);
x_6 = lean_expr_mk_mdata(x_5, x_2);
return x_6;
}
}
obj* _init_l___private_init_lean_elaborator_preterm_1__dummy___closed__1() {
_start:
{
obj* x_1; obj* x_2; obj* x_3;
x_1 = lean::box(0);
x_2 = l_Lean_Parser_Term_prop___elambda__1___rarg___closed__3;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
obj* _init_l___private_init_lean_elaborator_preterm_1__dummy___closed__2() {
_start:
{
obj* x_1; obj* x_2; obj* x_3;
x_1 = lean::box(0);
x_2 = l___private_init_lean_elaborator_preterm_1__dummy___closed__1;
x_3 = lean_expr_mk_const(x_2, x_1);
return x_3;
}
}
obj* _init_l___private_init_lean_elaborator_preterm_1__dummy() {
_start:
{
obj* x_1;
x_1 = l___private_init_lean_elaborator_preterm_1__dummy___closed__2;
return x_1;
}
}
obj* l_AssocList_find___main___at_Lean_Elab_toPreTerm___spec__2(obj* x_1, obj* x_2) {
_start:
{
if (lean::obj_tag(x_2) == 0)
{
obj* x_3;
x_3 = lean::box(0);
return x_3;
}
else
{
obj* x_4; obj* x_5; obj* x_6; uint8 x_7;
x_4 = lean::cnstr_get(x_2, 0);
x_5 = lean::cnstr_get(x_2, 1);
x_6 = lean::cnstr_get(x_2, 2);
x_7 = lean_name_dec_eq(x_4, x_1);
if (x_7 == 0)
{
x_2 = x_6;
goto _start;
}
else
{
obj* x_9;
lean::inc(x_5);
x_9 = lean::alloc_cnstr(1, 1, 0);
lean::cnstr_set(x_9, 0, x_5);
return x_9;
}
}
}
}
obj* l_HashMapImp_find___at_Lean_Elab_toPreTerm___spec__1(obj* x_1, obj* x_2) {
_start:
{
obj* x_3; obj* x_4; usize x_5; usize x_6; obj* x_7; usize x_8; obj* x_9; obj* x_10;
x_3 = lean::cnstr_get(x_1, 1);
x_4 = lean::array_get_size(x_3);
x_5 = lean_name_hash_usize(x_2);
x_6 = lean::usize_modn(x_5, x_4);
lean::dec(x_4);
x_7 = lean::box_size_t(x_6);
x_8 = lean::unbox_size_t(x_7);
lean::dec(x_7);
x_9 = lean::array_uget(x_3, x_8);
x_10 = l_AssocList_find___main___at_Lean_Elab_toPreTerm___spec__2(x_2, x_9);
lean::dec(x_9);
return x_10;
}
}
obj* _init_l_Lean_Elab_toPreTerm___closed__1() {
_start:
{
obj* x_1;
x_1 = lean::mk_string("`toPreTerm` failed, unexpected syntax");
return x_1;
}
}
obj* _init_l_Lean_Elab_toPreTerm___closed__2() {
_start:
{
obj* x_1; obj* x_2;
x_1 = l_Lean_Elab_toPreTerm___closed__1;
x_2 = lean::alloc_cnstr(3, 1, 0);
lean::cnstr_set(x_2, 0, x_1);
return x_2;
}
}
obj* _init_l_Lean_Elab_toPreTerm___closed__3() {
_start:
{
obj* x_1; obj* x_2;
x_1 = l_Lean_builtinPreTermElabTable;
x_2 = lean::alloc_closure(reinterpret_cast<void*>(l_IO_Prim_Ref_get___boxed), 3, 2);
lean::closure_set(x_2, 0, lean::box(0));
lean::closure_set(x_2, 1, x_1);
return x_2;
}
}
obj* _init_l_Lean_Elab_toPreTerm___closed__4() {
_start:
{
obj* x_1;
x_1 = lean::mk_string("`toPreTerm` failed, no support for syntax '");
return x_1;
}
}
obj* l_Lean_Elab_toPreTerm(obj* x_1, obj* x_2, obj* x_3) {
_start:
{
if (lean::obj_tag(x_1) == 1)
{
obj* x_4; uint8 x_5;
x_4 = lean::cnstr_get(x_1, 0);
lean::inc(x_4);
x_5 = !lean::is_exclusive(x_3);
if (x_5 == 0)
{
obj* x_6; obj* x_7; obj* x_8; obj* x_9;
x_6 = lean::cnstr_get(x_3, 0);
lean::dec(x_6);
x_7 = lean::box(0);
lean::cnstr_set(x_3, 0, x_7);
x_8 = l_Lean_Elab_toPreTerm___closed__3;
x_9 = l_Lean_Elab_runIOUnsafe___rarg(x_8, x_2, x_3);
if (lean::obj_tag(x_9) == 0)
{
uint8 x_10;
x_10 = !lean::is_exclusive(x_9);
if (x_10 == 0)
{
obj* x_11; obj* x_12;
x_11 = lean::cnstr_get(x_9, 0);
lean::cnstr_set(x_9, 0, x_7);
x_12 = l_HashMapImp_find___at_Lean_Elab_toPreTerm___spec__1(x_11, x_4);
lean::dec(x_11);
if (lean::obj_tag(x_12) == 0)
{
obj* x_13; obj* x_14; obj* x_15; obj* x_16; obj* x_17; obj* x_18; obj* x_19;
x_13 = l_System_FilePath_dirName___closed__1;
x_14 = l_Lean_Name_toStringWithSep___main(x_13, x_4);
x_15 = l_Lean_Elab_toPreTerm___closed__4;
x_16 = lean::string_append(x_15, x_14);
lean::dec(x_14);
x_17 = l_Char_HasRepr___closed__1;
x_18 = lean::string_append(x_16, x_17);
x_19 = l_Lean_logErrorAndThrow___rarg(x_1, x_18, x_2, x_9);
lean::dec(x_2);
lean::dec(x_1);
return x_19;
}
else
{
obj* x_20; obj* x_21;
lean::dec(x_4);
x_20 = lean::cnstr_get(x_12, 0);
lean::inc(x_20);
lean::dec(x_12);
x_21 = lean::apply_3(x_20, x_1, x_2, x_9);
return x_21;
}
}
else
{
obj* x_22; obj* x_23; obj* x_24; obj* x_25;
x_22 = lean::cnstr_get(x_9, 0);
x_23 = lean::cnstr_get(x_9, 1);
lean::inc(x_23);
lean::inc(x_22);
lean::dec(x_9);
x_24 = lean::alloc_cnstr(0, 2, 0);
lean::cnstr_set(x_24, 0, x_7);
lean::cnstr_set(x_24, 1, x_23);
x_25 = l_HashMapImp_find___at_Lean_Elab_toPreTerm___spec__1(x_22, x_4);
lean::dec(x_22);
if (lean::obj_tag(x_25) == 0)
{
obj* x_26; obj* x_27; obj* x_28; obj* x_29; obj* x_30; obj* x_31; obj* x_32;
x_26 = l_System_FilePath_dirName___closed__1;
x_27 = l_Lean_Name_toStringWithSep___main(x_26, x_4);
x_28 = l_Lean_Elab_toPreTerm___closed__4;
x_29 = lean::string_append(x_28, x_27);
lean::dec(x_27);
x_30 = l_Char_HasRepr___closed__1;
x_31 = lean::string_append(x_29, x_30);
x_32 = l_Lean_logErrorAndThrow___rarg(x_1, x_31, x_2, x_24);
lean::dec(x_2);
lean::dec(x_1);
return x_32;
}
else
{
obj* x_33; obj* x_34;
lean::dec(x_4);
x_33 = lean::cnstr_get(x_25, 0);
lean::inc(x_33);
lean::dec(x_25);
x_34 = lean::apply_3(x_33, x_1, x_2, x_24);
return x_34;
}
}
}
else
{
uint8 x_35;
lean::dec(x_4);
lean::dec(x_2);
lean::dec(x_1);
x_35 = !lean::is_exclusive(x_9);
if (x_35 == 0)
{
return x_9;
}
else
{
obj* x_36; obj* x_37; obj* x_38;
x_36 = lean::cnstr_get(x_9, 0);
x_37 = lean::cnstr_get(x_9, 1);
lean::inc(x_37);
lean::inc(x_36);
lean::dec(x_9);
x_38 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_38, 0, x_36);
lean::cnstr_set(x_38, 1, x_37);
return x_38;
}
}
}
else
{
obj* x_39; obj* x_40; obj* x_41; obj* x_42; obj* x_43;
x_39 = lean::cnstr_get(x_3, 1);
lean::inc(x_39);
lean::dec(x_3);
x_40 = lean::box(0);
x_41 = lean::alloc_cnstr(0, 2, 0);
lean::cnstr_set(x_41, 0, x_40);
lean::cnstr_set(x_41, 1, x_39);
x_42 = l_Lean_Elab_toPreTerm___closed__3;
x_43 = l_Lean_Elab_runIOUnsafe___rarg(x_42, x_2, x_41);
if (lean::obj_tag(x_43) == 0)
{
obj* x_44; obj* x_45; obj* x_46; obj* x_47; obj* x_48;
x_44 = lean::cnstr_get(x_43, 0);
lean::inc(x_44);
x_45 = lean::cnstr_get(x_43, 1);
lean::inc(x_45);
if (lean::is_exclusive(x_43)) {
lean::cnstr_release(x_43, 0);
lean::cnstr_release(x_43, 1);
x_46 = x_43;
} else {
lean::dec_ref(x_43);
x_46 = lean::box(0);
}
if (lean::is_scalar(x_46)) {
x_47 = lean::alloc_cnstr(0, 2, 0);
} else {
x_47 = x_46;
}
lean::cnstr_set(x_47, 0, x_40);
lean::cnstr_set(x_47, 1, x_45);
x_48 = l_HashMapImp_find___at_Lean_Elab_toPreTerm___spec__1(x_44, x_4);
lean::dec(x_44);
if (lean::obj_tag(x_48) == 0)
{
obj* x_49; obj* x_50; obj* x_51; obj* x_52; obj* x_53; obj* x_54; obj* x_55;
x_49 = l_System_FilePath_dirName___closed__1;
x_50 = l_Lean_Name_toStringWithSep___main(x_49, x_4);
x_51 = l_Lean_Elab_toPreTerm___closed__4;
x_52 = lean::string_append(x_51, x_50);
lean::dec(x_50);
x_53 = l_Char_HasRepr___closed__1;
x_54 = lean::string_append(x_52, x_53);
x_55 = l_Lean_logErrorAndThrow___rarg(x_1, x_54, x_2, x_47);
lean::dec(x_2);
lean::dec(x_1);
return x_55;
}
else
{
obj* x_56; obj* x_57;
lean::dec(x_4);
x_56 = lean::cnstr_get(x_48, 0);
lean::inc(x_56);
lean::dec(x_48);
x_57 = lean::apply_3(x_56, x_1, x_2, x_47);
return x_57;
}
}
else
{
obj* x_58; obj* x_59; obj* x_60; obj* x_61;
lean::dec(x_4);
lean::dec(x_2);
lean::dec(x_1);
x_58 = lean::cnstr_get(x_43, 0);
lean::inc(x_58);
x_59 = lean::cnstr_get(x_43, 1);
lean::inc(x_59);
if (lean::is_exclusive(x_43)) {
lean::cnstr_release(x_43, 0);
lean::cnstr_release(x_43, 1);
x_60 = x_43;
} else {
lean::dec_ref(x_43);
x_60 = lean::box(0);
}
if (lean::is_scalar(x_60)) {
x_61 = lean::alloc_cnstr(1, 2, 0);
} else {
x_61 = x_60;
}
lean::cnstr_set(x_61, 0, x_58);
lean::cnstr_set(x_61, 1, x_59);
return x_61;
}
}
}
else
{
uint8 x_62;
lean::dec(x_2);
lean::dec(x_1);
x_62 = !lean::is_exclusive(x_3);
if (x_62 == 0)
{
obj* x_63; obj* x_64;
x_63 = lean::cnstr_get(x_3, 0);
lean::dec(x_63);
x_64 = l_Lean_Elab_toPreTerm___closed__2;
lean::cnstr_set_tag(x_3, 1);
lean::cnstr_set(x_3, 0, x_64);
return x_3;
}
else
{
obj* x_65; obj* x_66; obj* x_67;
x_65 = lean::cnstr_get(x_3, 1);
lean::inc(x_65);
lean::dec(x_3);
x_66 = l_Lean_Elab_toPreTerm___closed__2;
x_67 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_67, 0, x_66);
lean::cnstr_set(x_67, 1, x_65);
return x_67;
}
}
}
}
obj* l_AssocList_find___main___at_Lean_Elab_toPreTerm___spec__2___boxed(obj* x_1, obj* x_2) {
_start:
{
obj* x_3;
x_3 = l_AssocList_find___main___at_Lean_Elab_toPreTerm___spec__2(x_1, x_2);
lean::dec(x_2);
lean::dec(x_1);
return x_3;
}
}
obj* l_HashMapImp_find___at_Lean_Elab_toPreTerm___spec__1___boxed(obj* x_1, obj* x_2) {
_start:
{
obj* x_3;
x_3 = l_HashMapImp_find___at_Lean_Elab_toPreTerm___spec__1(x_1, x_2);
lean::dec(x_2);
lean::dec(x_1);
return x_3;
}
}
obj* _init_l_Lean_Elab_convertType___rarg___closed__1() {
_start:
{
obj* x_1; obj* x_2;
x_1 = l_Lean_Level_one___closed__1;
x_2 = lean_expr_mk_sort(x_1);
return x_2;
}
}
obj* l_Lean_Elab_convertType___rarg(obj* x_1) {
_start:
{
uint8 x_2;
x_2 = !lean::is_exclusive(x_1);
if (x_2 == 0)
{
obj* x_3; obj* x_4;
x_3 = lean::cnstr_get(x_1, 0);
lean::dec(x_3);
x_4 = l_Lean_Elab_convertType___rarg___closed__1;
lean::cnstr_set(x_1, 0, x_4);
return x_1;
}
else
{
obj* x_5; obj* x_6; obj* x_7;
x_5 = lean::cnstr_get(x_1, 1);
lean::inc(x_5);
lean::dec(x_1);
x_6 = l_Lean_Elab_convertType___rarg___closed__1;
x_7 = lean::alloc_cnstr(0, 2, 0);
lean::cnstr_set(x_7, 0, x_6);
lean::cnstr_set(x_7, 1, x_5);
return x_7;
}
}
}
obj* l_Lean_Elab_convertType(obj* x_1, obj* x_2) {
_start:
{
obj* x_3;
x_3 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Elab_convertType___rarg), 1, 0);
return x_3;
}
}
obj* l_Lean_Elab_convertType___boxed(obj* x_1, obj* x_2) {
_start:
{
obj* x_3;
x_3 = l_Lean_Elab_convertType(x_1, x_2);
lean::dec(x_2);
lean::dec(x_1);
return x_3;
}
}
obj* _init_l___regBuiltinTermElab_Lean_Elab_convertType___closed__1() {
_start:
{
obj* x_1;
x_1 = lean::mk_string("Elab");
return x_1;
}
}
obj* _init_l___regBuiltinTermElab_Lean_Elab_convertType___closed__2() {
_start:
{
obj* x_1; obj* x_2; obj* x_3;
x_1 = l_Lean_nameToExprAux___main___closed__4;
x_2 = l___regBuiltinTermElab_Lean_Elab_convertType___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
obj* _init_l___regBuiltinTermElab_Lean_Elab_convertType___closed__3() {
_start:
{
obj* x_1;
x_1 = lean::mk_string("convertType");
return x_1;
}
}
obj* _init_l___regBuiltinTermElab_Lean_Elab_convertType___closed__4() {
_start:
{
obj* x_1; obj* x_2; obj* x_3;
x_1 = l___regBuiltinTermElab_Lean_Elab_convertType___closed__2;
x_2 = l___regBuiltinTermElab_Lean_Elab_convertType___closed__3;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
obj* _init_l___regBuiltinTermElab_Lean_Elab_convertType___closed__5() {
_start:
{
obj* x_1;
x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Elab_convertType___boxed), 2, 0);
return x_1;
}
}
obj* l___regBuiltinTermElab_Lean_Elab_convertType(obj* x_1) {
_start:
{
obj* x_2; obj* x_3; obj* x_4; obj* x_5;
x_2 = l_Lean_Parser_Term_type___elambda__1___rarg___closed__2;
x_3 = l___regBuiltinTermElab_Lean_Elab_convertType___closed__4;
x_4 = l___regBuiltinTermElab_Lean_Elab_convertType___closed__5;
x_5 = l_Lean_addBuiltinPreTermElab(x_2, x_3, x_4, x_1);
return x_5;
}
}
obj* l_Lean_Elab_convertSort___rarg(obj* x_1) {
_start:
{
uint8 x_2;
x_2 = !lean::is_exclusive(x_1);
if (x_2 == 0)
{
obj* x_3; obj* x_4;
x_3 = lean::cnstr_get(x_1, 0);
lean::dec(x_3);
x_4 = l_Lean_exprIsInhabited___closed__1;
lean::cnstr_set(x_1, 0, x_4);
return x_1;
}
else
{
obj* x_5; obj* x_6; obj* x_7;
x_5 = lean::cnstr_get(x_1, 1);
lean::inc(x_5);
lean::dec(x_1);
x_6 = l_Lean_exprIsInhabited___closed__1;
x_7 = lean::alloc_cnstr(0, 2, 0);
lean::cnstr_set(x_7, 0, x_6);
lean::cnstr_set(x_7, 1, x_5);
return x_7;
}
}
}
obj* l_Lean_Elab_convertSort(obj* x_1, obj* x_2) {
_start:
{
obj* x_3;
x_3 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Elab_convertSort___rarg), 1, 0);
return x_3;
}
}
obj* l_Lean_Elab_convertSort___boxed(obj* x_1, obj* x_2) {
_start:
{
obj* x_3;
x_3 = l_Lean_Elab_convertSort(x_1, x_2);
lean::dec(x_2);
lean::dec(x_1);
return x_3;
}
}
obj* _init_l___regBuiltinTermElab_Lean_Elab_convertSort___closed__1() {
_start:
{
obj* x_1;
x_1 = lean::mk_string("convertSort");
return x_1;
}
}
obj* _init_l___regBuiltinTermElab_Lean_Elab_convertSort___closed__2() {
_start:
{
obj* x_1; obj* x_2; obj* x_3;
x_1 = l___regBuiltinTermElab_Lean_Elab_convertType___closed__2;
x_2 = l___regBuiltinTermElab_Lean_Elab_convertSort___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
obj* _init_l___regBuiltinTermElab_Lean_Elab_convertSort___closed__3() {
_start:
{
obj* x_1;
x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Elab_convertSort___boxed), 2, 0);
return x_1;
}
}
obj* l___regBuiltinTermElab_Lean_Elab_convertSort(obj* x_1) {
_start:
{
obj* x_2; obj* x_3; obj* x_4; obj* x_5;
x_2 = l_Lean_Parser_Term_sort___elambda__1___rarg___closed__2;
x_3 = l___regBuiltinTermElab_Lean_Elab_convertSort___closed__2;
x_4 = l___regBuiltinTermElab_Lean_Elab_convertSort___closed__3;
x_5 = l_Lean_addBuiltinPreTermElab(x_2, x_3, x_4, x_1);
return x_5;
}
}
obj* initialize_init_lean_elaborator_basic(obj*);
static bool _G_initialized = false;
obj* initialize_init_lean_elaborator_preterm(obj* w) {
@ -1339,6 +2003,10 @@ w = l_Lean_mkBuiltinPreTermElabTable(w);
if (io_result_is_error(w)) return w;
l_Lean_builtinPreTermElabTable = io_result_get_value(w);
lean::mark_persistent(l_Lean_builtinPreTermElabTable);
l_Lean_declareBuiltinPreTermElab___closed__1 = _init_l_Lean_declareBuiltinPreTermElab___closed__1();
lean::mark_persistent(l_Lean_declareBuiltinPreTermElab___closed__1);
l_Lean_declareBuiltinPreTermElab___closed__2 = _init_l_Lean_declareBuiltinPreTermElab___closed__2();
lean::mark_persistent(l_Lean_declareBuiltinPreTermElab___closed__2);
l_Lean_registerBuiltinPreTermElabAttr___lambda__1___closed__1 = _init_l_Lean_registerBuiltinPreTermElabAttr___lambda__1___closed__1();
lean::mark_persistent(l_Lean_registerBuiltinPreTermElabAttr___lambda__1___closed__1);
l_Lean_registerBuiltinPreTermElabAttr___lambda__1___closed__2 = _init_l_Lean_registerBuiltinPreTermElabAttr___lambda__1___closed__2();
@ -1365,5 +2033,45 @@ l_Lean_registerBuiltinPreTermElabAttr___closed__7 = _init_l_Lean_registerBuiltin
lean::mark_persistent(l_Lean_registerBuiltinPreTermElabAttr___closed__7);
w = l_Lean_registerBuiltinPreTermElabAttr(w);
if (io_result_is_error(w)) return w;
l_Lean_Expr_mkAnnotation___closed__1 = _init_l_Lean_Expr_mkAnnotation___closed__1();
lean::mark_persistent(l_Lean_Expr_mkAnnotation___closed__1);
l_Lean_Expr_mkAnnotation___closed__2 = _init_l_Lean_Expr_mkAnnotation___closed__2();
lean::mark_persistent(l_Lean_Expr_mkAnnotation___closed__2);
l___private_init_lean_elaborator_preterm_1__dummy___closed__1 = _init_l___private_init_lean_elaborator_preterm_1__dummy___closed__1();
lean::mark_persistent(l___private_init_lean_elaborator_preterm_1__dummy___closed__1);
l___private_init_lean_elaborator_preterm_1__dummy___closed__2 = _init_l___private_init_lean_elaborator_preterm_1__dummy___closed__2();
lean::mark_persistent(l___private_init_lean_elaborator_preterm_1__dummy___closed__2);
l___private_init_lean_elaborator_preterm_1__dummy = _init_l___private_init_lean_elaborator_preterm_1__dummy();
lean::mark_persistent(l___private_init_lean_elaborator_preterm_1__dummy);
l_Lean_Elab_toPreTerm___closed__1 = _init_l_Lean_Elab_toPreTerm___closed__1();
lean::mark_persistent(l_Lean_Elab_toPreTerm___closed__1);
l_Lean_Elab_toPreTerm___closed__2 = _init_l_Lean_Elab_toPreTerm___closed__2();
lean::mark_persistent(l_Lean_Elab_toPreTerm___closed__2);
l_Lean_Elab_toPreTerm___closed__3 = _init_l_Lean_Elab_toPreTerm___closed__3();
lean::mark_persistent(l_Lean_Elab_toPreTerm___closed__3);
l_Lean_Elab_toPreTerm___closed__4 = _init_l_Lean_Elab_toPreTerm___closed__4();
lean::mark_persistent(l_Lean_Elab_toPreTerm___closed__4);
l_Lean_Elab_convertType___rarg___closed__1 = _init_l_Lean_Elab_convertType___rarg___closed__1();
lean::mark_persistent(l_Lean_Elab_convertType___rarg___closed__1);
l___regBuiltinTermElab_Lean_Elab_convertType___closed__1 = _init_l___regBuiltinTermElab_Lean_Elab_convertType___closed__1();
lean::mark_persistent(l___regBuiltinTermElab_Lean_Elab_convertType___closed__1);
l___regBuiltinTermElab_Lean_Elab_convertType___closed__2 = _init_l___regBuiltinTermElab_Lean_Elab_convertType___closed__2();
lean::mark_persistent(l___regBuiltinTermElab_Lean_Elab_convertType___closed__2);
l___regBuiltinTermElab_Lean_Elab_convertType___closed__3 = _init_l___regBuiltinTermElab_Lean_Elab_convertType___closed__3();
lean::mark_persistent(l___regBuiltinTermElab_Lean_Elab_convertType___closed__3);
l___regBuiltinTermElab_Lean_Elab_convertType___closed__4 = _init_l___regBuiltinTermElab_Lean_Elab_convertType___closed__4();
lean::mark_persistent(l___regBuiltinTermElab_Lean_Elab_convertType___closed__4);
l___regBuiltinTermElab_Lean_Elab_convertType___closed__5 = _init_l___regBuiltinTermElab_Lean_Elab_convertType___closed__5();
lean::mark_persistent(l___regBuiltinTermElab_Lean_Elab_convertType___closed__5);
w = l___regBuiltinTermElab_Lean_Elab_convertType(w);
if (io_result_is_error(w)) return w;
l___regBuiltinTermElab_Lean_Elab_convertSort___closed__1 = _init_l___regBuiltinTermElab_Lean_Elab_convertSort___closed__1();
lean::mark_persistent(l___regBuiltinTermElab_Lean_Elab_convertSort___closed__1);
l___regBuiltinTermElab_Lean_Elab_convertSort___closed__2 = _init_l___regBuiltinTermElab_Lean_Elab_convertSort___closed__2();
lean::mark_persistent(l___regBuiltinTermElab_Lean_Elab_convertSort___closed__2);
l___regBuiltinTermElab_Lean_Elab_convertSort___closed__3 = _init_l___regBuiltinTermElab_Lean_Elab_convertSort___closed__3();
lean::mark_persistent(l___regBuiltinTermElab_Lean_Elab_convertSort___closed__3);
w = l___regBuiltinTermElab_Lean_Elab_convertSort(w);
if (io_result_is_error(w)) return w;
return w;
}

289
src/stage0/init/lean/parser/command.cpp generated
View file

@ -38,6 +38,7 @@ obj* l_Lean_Parser_Command_reserve___elambda__1___closed__5;
obj* l_Lean_Parser_Command_declId___closed__7;
obj* l_Lean_Parser_Command_unsafe___elambda__1___rarg___closed__2;
obj* l_Lean_Parser_Command_private___elambda__1___rarg___closed__7;
obj* l___regBuiltinParser_Lean_Parser_Command_preterm(obj*);
obj* l_Lean_Parser_Command_export;
obj* l_Lean_Parser_Command_docComment___closed__2;
obj* l_Lean_Parser_Command_openRenaming___closed__2;
@ -129,6 +130,7 @@ obj* l___private_init_lean_parser_parser_2__sepByFnAux___main___at_Lean_Parser_C
obj* l_Lean_Parser_Command_attributes___elambda__1___closed__1;
obj* l_Lean_Parser_Command_set__option___closed__6;
obj* l_Lean_Parser_Command_open___elambda__1___closed__3;
obj* l_Lean_Parser_Command_preterm___closed__5;
obj* l_Lean_Parser_Command_commentBody___elambda__1___boxed(obj*, obj*, obj*);
obj* l_Lean_Parser_regBuiltinCommandParserAttr___closed__1;
obj* l_Lean_Parser_Command_universe___elambda__1___rarg___closed__5;
@ -205,6 +207,7 @@ obj* l_Lean_Parser_Command_infix___elambda__1___rarg___closed__2;
obj* l_Lean_Parser_Command_structImplicitBinder___elambda__1___closed__2;
obj* l_Lean_Parser_Command_end___closed__5;
obj* l_Lean_Parser_Command_openSimple___elambda__1(obj*, obj*, obj*);
obj* l_Lean_Parser_Command_preterm___closed__3;
extern obj* l_Lean_Parser_Term_typeAscription___elambda__1___rarg___closed__4;
obj* l_Lean_Parser_Command_strictInferMod___closed__1;
obj* l_Lean_Parser_Command_resolve__name___elambda__1___rarg___closed__6;
@ -221,6 +224,7 @@ obj* l_Lean_Parser_Command_open___closed__8;
obj* l_Lean_Parser_Command_structCtor___elambda__1___rarg(obj*, obj*);
obj* l_Lean_Parser_Command_commentBody;
obj* l_Lean_Parser_Command_docComment___elambda__1___closed__2;
obj* l_Lean_Parser_Command_preterm___elambda__1___boxed(obj*);
obj* l_Lean_Parser_Command_unsafe___elambda__1(obj*);
obj* l_Lean_Parser_Command_declId___elambda__1(obj*, obj*, obj*);
obj* l_Lean_Parser_Command_abbrev___elambda__1___closed__4;
@ -286,14 +290,17 @@ obj* l_Lean_Parser_Command_structExplicitBinder___closed__10;
obj* l_Lean_Parser_Command_infix___closed__1;
obj* l_Lean_Parser_Command_classTk___elambda__1___rarg___closed__1;
obj* l_Lean_Parser_Command_declValSimple___elambda__1(obj*);
obj* l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__1;
obj* l_Lean_Parser_Command_declValSimple;
obj* l_Lean_Parser_Command_strictInferMod;
obj* l_Lean_Parser_Command_namespace;
obj* l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__5;
obj* l_Lean_Parser_Command_structImplicitBinder___closed__4;
obj* l_Lean_Parser_Command_prefix___elambda__1___rarg(obj*, obj*);
obj* l_Lean_Parser_Command_introRule___closed__6;
obj* l_Lean_Parser_Command_constant___closed__5;
obj* l_Lean_Parser_Command_postfix___elambda__1___rarg___closed__3;
obj* l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__2;
obj* l_Lean_Parser_Command_notation___closed__3;
obj* l_Lean_Parser_Command_commentBody___closed__2;
obj* l_Lean_Parser_Command_universes___closed__4;
@ -457,12 +464,14 @@ obj* l_Lean_Parser_Command_infix___closed__3;
obj* l_Lean_Parser_Command_exit___elambda__1___rarg___closed__1;
obj* l_Lean_Parser_Command_attribute___elambda__1___closed__1;
obj* l_Lean_Parser_Term_binderDefault___elambda__1___rarg(obj*, obj*);
obj* l_Lean_Parser_Command_preterm___closed__2;
obj* l_Lean_Parser_Command_visibility___elambda__1(obj*);
obj* l_Lean_Parser_Command_openHiding___closed__6;
obj* l_Lean_Parser_Command_docComment;
obj* l_Lean_Parser_Command_openHiding___elambda__1___closed__2;
obj* l_Lean_Parser_Command_example___elambda__1___closed__4;
obj* l_Lean_Parser_Command_protected___closed__3;
obj* l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__6;
obj* l_Lean_Parser_Command_partial___closed__4;
obj* l_Lean_Parser_ParserState_mkNode(obj*, obj*, obj*);
obj* l_Lean_Parser_Command_mixfixKind___elambda__1___boxed(obj*);
@ -489,6 +498,7 @@ obj* l_Lean_Parser_Command_attrInstance___closed__3;
obj* l_Lean_Parser_Command_openHiding___closed__4;
obj* l_Lean_Parser_Command_unsafe___closed__1;
obj* l_Lean_Parser_Command_identPrec___closed__4;
obj* l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__4;
obj* l_Lean_Parser_Command_inductive___closed__3;
obj* l_Lean_Parser_Command_set__option___elambda__1___rarg___closed__13;
obj* l_Lean_Parser_Command_declaration___closed__12;
@ -525,6 +535,7 @@ obj* l_Lean_Parser_Command_attrInstance;
obj* l_Lean_Parser_Command_theorem___elambda__1___closed__6;
obj* l_Lean_Parser_Command_attributes___elambda__1___closed__3;
obj* l_Lean_Parser_Command_openOnly___elambda__1___closed__1;
obj* l_Lean_Parser_Command_preterm;
obj* l_Lean_Parser_Command_resolve__name___elambda__1___rarg___closed__4;
obj* l_Lean_Parser_Command_export___closed__1;
obj* l_Lean_Parser_Command_exit___elambda__1___rarg___closed__6;
@ -826,6 +837,7 @@ obj* l_Lean_Parser_Command_namespace___closed__3;
obj* l_Lean_Parser_Command_resolve__name___closed__2;
obj* l_Lean_Parser_manyAux___main___at_Lean_Parser_Command_notation___elambda__1___spec__1___boxed(obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_Command_partial___elambda__1___boxed(obj*);
obj* l_Lean_Parser_Command_preterm___elambda__1(obj*);
obj* l_Lean_Parser_Command_example___elambda__1(obj*, obj*, obj*);
obj* l_Lean_Parser_Command_universe___closed__5;
obj* l_Lean_Parser_Command_structureTk___closed__4;
@ -840,6 +852,7 @@ obj* l_Lean_Parser_identFn___rarg(obj*, obj*);
obj* l_Lean_Parser_Command_maxPrec___elambda__1___boxed(obj*);
obj* l_Lean_Parser_Command_infixr___elambda__1___boxed(obj*);
obj* l_Lean_Parser_Command_structExplicitBinder___closed__8;
obj* l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__3;
obj* l_Lean_Parser_manyAux___main___at_Lean_Parser_Command_declValEqns___spec__2(obj*, uint8, obj*, obj*, obj*);
obj* l_String_trim(obj*);
obj* l_Lean_Parser_Command_universes___closed__3;
@ -868,6 +881,7 @@ obj* l_Lean_Parser_Command_constant___closed__7;
obj* l_Lean_Parser_Command_infixl___elambda__1___rarg___closed__2;
obj* l_Lean_Parser_Command_quotedSymbolPrec___closed__3;
obj* l_Lean_Parser_Command_strictInferMod___elambda__1___rarg(obj*, obj*);
obj* l_Lean_Parser_Command_preterm___closed__1;
obj* l_Lean_Parser_Command_declVal___elambda__1___boxed(obj*, obj*, obj*);
obj* l_Lean_Parser_Command_openRenaming___elambda__1___closed__6;
obj* l_Lean_Parser_Command_attribute___closed__9;
@ -906,6 +920,7 @@ obj* l_Lean_Parser_Command_structureTk___elambda__1___boxed(obj*);
obj* l_Lean_Parser_Command_protected___elambda__1___rarg___closed__7;
obj* l_Lean_Parser_Command_universes;
obj* l_Lean_Parser_Command_declModifiers___closed__6;
obj* l_Lean_Parser_Command_preterm___closed__4;
obj* l_Lean_Parser_Command_set__option___elambda__1___rarg(obj*, obj*);
obj* l_Lean_Parser_Command_openSimple___closed__2;
obj* l_Lean_Parser_Command_classInductive___elambda__1___closed__6;
@ -963,6 +978,7 @@ obj* l_Lean_Parser_Command_declaration;
obj* l_Lean_Parser_Command_private___elambda__1___rarg___closed__5;
obj* l_Lean_Parser_Command_section___elambda__1___rarg___closed__2;
obj* l_Lean_Parser_Command_unsafe___elambda__1___rarg___closed__3;
obj* l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__7;
obj* l_Lean_Parser_Command_structure___closed__5;
obj* l_Lean_Parser_Command_openHiding___elambda__1___closed__4;
obj* l_Lean_Parser_Command_structExplicitBinder___elambda__1___closed__1;
@ -1045,6 +1061,7 @@ obj* l_Lean_Parser_Command_variable___elambda__1___closed__3;
obj* l___regBuiltinParser_Lean_Parser_Command_end(obj*);
obj* l_Lean_Parser_Command_declId___closed__3;
obj* l_Lean_Parser_Command_noncomputable___elambda__1___rarg___closed__7;
obj* l_Lean_Parser_Command_preterm___elambda__1___rarg(obj*, obj*);
obj* l_Lean_Parser_Command_structInstBinder___closed__4;
obj* l_Lean_Parser_Command_attribute___closed__5;
obj* l_Lean_Parser_Command_openRenamingItem___elambda__1(obj*);
@ -15909,6 +15926,250 @@ x_5 = l_Lean_Parser_addBuiltinLeadingParser(x_2, x_3, x_4, x_1);
return x_5;
}
}
obj* _init_l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__1() {
_start:
{
obj* x_1;
x_1 = lean::mk_string("preterm");
return x_1;
}
}
obj* _init_l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__2() {
_start:
{
obj* x_1; obj* x_2; obj* x_3;
x_1 = l_Lean_Parser_Command_docComment___elambda__1___closed__2;
x_2 = l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
obj* _init_l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__3() {
_start:
{
obj* x_1;
x_1 = lean::mk_string("#preterm ");
return x_1;
}
}
obj* _init_l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__4() {
_start:
{
obj* x_1; obj* x_2;
x_1 = l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__3;
x_2 = l_String_trim(x_1);
return x_2;
}
}
obj* _init_l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__5() {
_start:
{
obj* x_1; obj* x_2; obj* x_3;
x_1 = l_Char_HasRepr___closed__1;
x_2 = l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__4;
x_3 = lean::string_append(x_1, x_2);
return x_3;
}
}
obj* _init_l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__6() {
_start:
{
obj* x_1; obj* x_2; obj* x_3;
x_1 = l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__5;
x_2 = l_Char_HasRepr___closed__1;
x_3 = lean::string_append(x_1, x_2);
return x_3;
}
}
obj* _init_l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__7() {
_start:
{
obj* x_1; obj* x_2; obj* x_3;
x_1 = lean::box(0);
x_2 = l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__6;
x_3 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_3, 0, x_2);
lean::cnstr_set(x_3, 1, x_1);
return x_3;
}
}
obj* l_Lean_Parser_Command_preterm___elambda__1___rarg(obj* x_1, obj* x_2) {
_start:
{
obj* x_3; obj* x_4; obj* x_5; obj* x_15; obj* x_16; obj* x_17;
x_3 = lean::cnstr_get(x_2, 0);
lean::inc(x_3);
x_4 = lean::array_get_size(x_3);
lean::dec(x_3);
x_15 = lean::cnstr_get(x_2, 1);
lean::inc(x_15);
lean::inc(x_1);
x_16 = l_Lean_Parser_tokenFn(x_1, x_2);
x_17 = lean::cnstr_get(x_16, 3);
lean::inc(x_17);
if (lean::obj_tag(x_17) == 0)
{
obj* x_18; obj* x_19;
x_18 = lean::cnstr_get(x_16, 0);
lean::inc(x_18);
x_19 = l_Array_back___at___private_init_lean_parser_parser_6__updateCache___spec__1(x_18);
lean::dec(x_18);
if (lean::obj_tag(x_19) == 2)
{
obj* x_20; obj* x_21; uint8 x_22;
x_20 = lean::cnstr_get(x_19, 1);
lean::inc(x_20);
lean::dec(x_19);
x_21 = l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__4;
x_22 = lean::string_dec_eq(x_20, x_21);
lean::dec(x_20);
if (x_22 == 0)
{
obj* x_23; obj* x_24;
x_23 = l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__7;
x_24 = l_Lean_Parser_ParserState_mkErrorsAt(x_16, x_23, x_15);
x_5 = x_24;
goto block_14;
}
else
{
lean::dec(x_15);
x_5 = x_16;
goto block_14;
}
}
else
{
obj* x_25; obj* x_26;
lean::dec(x_19);
x_25 = l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__7;
x_26 = l_Lean_Parser_ParserState_mkErrorsAt(x_16, x_25, x_15);
x_5 = x_26;
goto block_14;
}
}
else
{
obj* x_27; obj* x_28;
lean::dec(x_17);
x_27 = l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__7;
x_28 = l_Lean_Parser_ParserState_mkErrorsAt(x_16, x_27, x_15);
x_5 = x_28;
goto block_14;
}
block_14:
{
obj* x_6;
x_6 = lean::cnstr_get(x_5, 3);
lean::inc(x_6);
if (lean::obj_tag(x_6) == 0)
{
obj* x_7; obj* x_8; obj* x_9; obj* x_10; obj* x_11;
x_7 = l_Lean_Parser_termParserAttribute;
x_8 = lean::mk_nat_obj(0u);
x_9 = l_Lean_Parser_ParserAttribute_runParser(x_7, x_8, x_1, x_5);
x_10 = l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__2;
x_11 = l_Lean_Parser_ParserState_mkNode(x_9, x_10, x_4);
return x_11;
}
else
{
obj* x_12; obj* x_13;
lean::dec(x_6);
lean::dec(x_1);
x_12 = l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__2;
x_13 = l_Lean_Parser_ParserState_mkNode(x_5, x_12, x_4);
return x_13;
}
}
}
}
obj* l_Lean_Parser_Command_preterm___elambda__1(obj* x_1) {
_start:
{
obj* x_2;
x_2 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Command_preterm___elambda__1___rarg), 2, 0);
return x_2;
}
}
obj* _init_l_Lean_Parser_Command_preterm___closed__1() {
_start:
{
obj* x_1; obj* x_2; obj* x_3;
x_1 = lean::box(0);
x_2 = l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__4;
x_3 = l_Lean_Parser_symbolInfo(x_2, x_1);
return x_3;
}
}
obj* _init_l_Lean_Parser_Command_preterm___closed__2() {
_start:
{
obj* x_1; obj* x_2; obj* x_3;
x_1 = l_Lean_Parser_Command_preterm___closed__1;
x_2 = l_Lean_Parser_Parser_inhabited___closed__1;
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
return x_3;
}
}
obj* _init_l_Lean_Parser_Command_preterm___closed__3() {
_start:
{
obj* x_1; obj* x_2; obj* x_3;
x_1 = l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__2;
x_2 = l_Lean_Parser_Command_preterm___closed__2;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
}
}
obj* _init_l_Lean_Parser_Command_preterm___closed__4() {
_start:
{
obj* x_1;
x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Command_preterm___elambda__1___boxed), 1, 0);
return x_1;
}
}
obj* _init_l_Lean_Parser_Command_preterm___closed__5() {
_start:
{
obj* x_1; obj* x_2; obj* x_3;
x_1 = l_Lean_Parser_Command_preterm___closed__3;
x_2 = l_Lean_Parser_Command_preterm___closed__4;
x_3 = lean::alloc_cnstr(0, 2, 0);
lean::cnstr_set(x_3, 0, x_1);
lean::cnstr_set(x_3, 1, x_2);
return x_3;
}
}
obj* _init_l_Lean_Parser_Command_preterm() {
_start:
{
obj* x_1;
x_1 = l_Lean_Parser_Command_preterm___closed__5;
return x_1;
}
}
obj* l_Lean_Parser_Command_preterm___elambda__1___boxed(obj* x_1) {
_start:
{
obj* x_2;
x_2 = l_Lean_Parser_Command_preterm___elambda__1(x_1);
lean::dec(x_1);
return x_2;
}
}
obj* l___regBuiltinParser_Lean_Parser_Command_preterm(obj* x_1) {
_start:
{
obj* x_2; obj* x_3; obj* x_4; obj* x_5;
x_2 = l_Lean_Parser_builtinCommandParsingTable;
x_3 = l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__2;
x_4 = l_Lean_Parser_Command_preterm;
x_5 = l_Lean_Parser_addBuiltinLeadingParser(x_2, x_3, x_4, x_1);
return x_5;
}
}
obj* _init_l_Lean_Parser_Command_init__quot___elambda__1___rarg___closed__1() {
_start:
{
@ -24147,6 +24408,34 @@ l_Lean_Parser_Command_resolve__name = _init_l_Lean_Parser_Command_resolve__name(
lean::mark_persistent(l_Lean_Parser_Command_resolve__name);
w = l___regBuiltinParser_Lean_Parser_Command_resolve__name(w);
if (io_result_is_error(w)) return w;
l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__1 = _init_l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__1();
lean::mark_persistent(l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__1);
l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__2 = _init_l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__2();
lean::mark_persistent(l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__2);
l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__3 = _init_l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__3();
lean::mark_persistent(l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__3);
l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__4 = _init_l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__4();
lean::mark_persistent(l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__4);
l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__5 = _init_l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__5();
lean::mark_persistent(l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__5);
l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__6 = _init_l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__6();
lean::mark_persistent(l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__6);
l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__7 = _init_l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__7();
lean::mark_persistent(l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__7);
l_Lean_Parser_Command_preterm___closed__1 = _init_l_Lean_Parser_Command_preterm___closed__1();
lean::mark_persistent(l_Lean_Parser_Command_preterm___closed__1);
l_Lean_Parser_Command_preterm___closed__2 = _init_l_Lean_Parser_Command_preterm___closed__2();
lean::mark_persistent(l_Lean_Parser_Command_preterm___closed__2);
l_Lean_Parser_Command_preterm___closed__3 = _init_l_Lean_Parser_Command_preterm___closed__3();
lean::mark_persistent(l_Lean_Parser_Command_preterm___closed__3);
l_Lean_Parser_Command_preterm___closed__4 = _init_l_Lean_Parser_Command_preterm___closed__4();
lean::mark_persistent(l_Lean_Parser_Command_preterm___closed__4);
l_Lean_Parser_Command_preterm___closed__5 = _init_l_Lean_Parser_Command_preterm___closed__5();
lean::mark_persistent(l_Lean_Parser_Command_preterm___closed__5);
l_Lean_Parser_Command_preterm = _init_l_Lean_Parser_Command_preterm();
lean::mark_persistent(l_Lean_Parser_Command_preterm);
w = l___regBuiltinParser_Lean_Parser_Command_preterm(w);
if (io_result_is_error(w)) return w;
l_Lean_Parser_Command_init__quot___elambda__1___rarg___closed__1 = _init_l_Lean_Parser_Command_init__quot___elambda__1___rarg___closed__1();
lean::mark_persistent(l_Lean_Parser_Command_init__quot___elambda__1___rarg___closed__1);
l_Lean_Parser_Command_init__quot___elambda__1___rarg___closed__2 = _init_l_Lean_Parser_Command_init__quot___elambda__1___rarg___closed__2();