chore(stage0): update

library/init/lean/elaborator/basic.lean

@@ -76,11 +76,10 @@ match attrParamSyntaxToIdentifier arg with
   throw (IO.userError ("invalid syntax node kind '" ++ toString k ++ "'"))
 | none   => throw (IO.userError ("syntax node kind is missing"))
 
-
 def declareBuiltinTermElab (env : Environment) (kind : SyntaxNodeKind) (declName : Name) : IO Environment :=
 let name := `_regBuiltinTermElab ++ declName;
 let type := Expr.app (mkConst `IO) (mkConst `Unit);
-let val  := mkCApp `addBuiltinTermElab [toExpr kind, toExpr declName, mkConst declName];
+let val  := mkCApp `Lean.addBuiltinTermElab [toExpr kind, toExpr declName, mkConst declName];
 let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque, isUnsafe := false };
 match env.addAndCompile {} decl with
 | none     => throw (IO.userError ("failed to emit registration code for builtin term elaborator '" ++ toString declName ++ "'"))
@@ -103,6 +102,10 @@ registerAttribute {
  applicationTime := AttributeApplicationTime.afterCompilation
 }
 
+
+-- @[builtinTermElab «do»] def elabDo : TermElab :=
+-- fun stx => pure (default Expr)
+
 namespace Elab
 
 /- Remark: in an ideal world where performance doesn't matter, we would define `Elab` as

src/stage0/init/io.cpp

@@ -29,11 +29,13 @@ obj* l_IO_HasEval(obj*);
 obj* l_IO_Ref_modify(obj*);
 obj* l_IO_Fs_handle_isEof___rarg(obj*, obj*);
 obj* l_getModify___rarg___lambda__1___boxed(obj*, obj*, obj*);
+obj* l_MonadExcept_orelse___at_EIO_HasOrelse___spec__1(obj*, obj*);
 obj* l_IO_Fs_handle_close___rarg(obj*, obj*);
 obj* l_IO_Ref_swap(obj*, obj*);
 obj* l_EIO_Inhabited___rarg(obj*);
 obj* l_HasRepr_HasEval___rarg(obj*, obj*, obj*);
 obj* l_IO_Prim_Ref_swap___boxed(obj*, obj*, obj*, obj*);
+obj* l_EIO_HasOrelse(obj*, obj*);
 obj* l_IO_Fs_handle_mk(obj*, obj*);
 extern "C" obj* lean_io_prim_handle_is_eof(obj*, obj*);
 obj* l_IO_println___at_HasRepr_HasEval___spec__1___boxed(obj*, obj*);
@@ -50,6 +52,7 @@ obj* l_EIO_Inhabited(obj*, obj*);
 obj* l_unsafeIO(obj*);
 obj* l_IO_Prim_iterate___at_IO_Fs_handle_readToEnd___spec__3(obj*, obj*, obj*);
 obj* l_EIO_Monad(obj*);
+obj* l_EIO_HasOrelse___closed__1;
 extern "C" obj* lean_io_prim_put_str(obj*, obj*);
 obj* l_IO_Ref_modify___rarg___lambda__1___boxed(obj*, obj*, obj*, obj*, obj*);
 obj* l_IO_Ref_modify___boxed(obj*);
@@ -66,6 +69,7 @@ obj* l_IO_Ref_swap___rarg(obj*, obj*, obj*, obj*);
 obj* l_IO_Fs_handle_flush(obj*, obj*);
 obj* l_IO_Prim_Ref_get___boxed(obj*, obj*, obj*);
 extern "C" obj* lean_io_prim_get_line(obj*);
+obj* l_MonadExcept_orelse___at_EIO_HasOrelse___spec__1___rarg(obj*, obj*, obj*);
 extern "C" obj* lean_io_allocprof(obj*, obj*, obj*, obj*);
 obj* l_IO_Ref_set___rarg(obj*, obj*, obj*, obj*);
 obj* l_IO_Error_HasToString;
@@ -190,6 +194,71 @@ x_2 = l_EIO_MonadExcept___closed__1;
 return x_2;
 }
 }
+obj* l_MonadExcept_orelse___at_EIO_HasOrelse___spec__1___rarg(obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+obj* x_4; 
+x_4 = lean::apply_1(x_1, x_3);
+if (lean::obj_tag(x_4) == 0)
+{
+lean::dec(x_2);
+return x_4;
+}
+else
+{
+uint8 x_5; 
+x_5 = !lean::is_exclusive(x_4);
+if (x_5 == 0)
+{
+obj* x_6; obj* x_7; obj* x_8; 
+x_6 = lean::cnstr_get(x_4, 0);
+lean::dec(x_6);
+x_7 = lean::box(0);
+lean::cnstr_set_tag(x_4, 0);
+lean::cnstr_set(x_4, 0, x_7);
+x_8 = lean::apply_1(x_2, x_4);
+return x_8;
+}
+else
+{
+obj* x_9; obj* x_10; obj* x_11; obj* x_12; 
+x_9 = lean::cnstr_get(x_4, 1);
+lean::inc(x_9);
+lean::dec(x_4);
+x_10 = lean::box(0);
+x_11 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_11, 0, x_10);
+lean::cnstr_set(x_11, 1, x_9);
+x_12 = lean::apply_1(x_2, x_11);
+return x_12;
+}
+}
+}
+}
+obj* l_MonadExcept_orelse___at_EIO_HasOrelse___spec__1(obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = lean::alloc_closure(reinterpret_cast<void*>(l_MonadExcept_orelse___at_EIO_HasOrelse___spec__1___rarg), 3, 0);
+return x_3;
+}
+}
+obj* _init_l_EIO_HasOrelse___closed__1() {
+_start:
+{
+obj* x_1; 
+x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_MonadExcept_orelse___at_EIO_HasOrelse___spec__1___rarg), 3, 0);
+return x_1;
+}
+}
+obj* l_EIO_HasOrelse(obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = l_EIO_HasOrelse___closed__1;
+return x_3;
+}
+}
 obj* l_EIO_Inhabited___rarg(obj* x_1) {
 _start:
 {
@@ -1749,6 +1818,9 @@ REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name("EIO"), "Monad"),
 l_EIO_MonadExcept___closed__1 = _init_l_EIO_MonadExcept___closed__1();
 lean::mark_persistent(l_EIO_MonadExcept___closed__1);
 REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name("EIO"), "MonadExcept"), 1, l_EIO_MonadExcept);
+l_EIO_HasOrelse___closed__1 = _init_l_EIO_HasOrelse___closed__1();
+lean::mark_persistent(l_EIO_HasOrelse___closed__1);
+REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name("EIO"), "HasOrelse"), 2, l_EIO_HasOrelse);
 REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name("EIO"), "Inhabited"), 2, l_EIO_Inhabited);
 l_IO_Error_HasToString___closed__1 = _init_l_IO_Error_HasToString___closed__1();
 lean::mark_persistent(l_IO_Error_HasToString___closed__1);

src/stage0/init/lean/parser/level.cpp

@@ -148,7 +148,7 @@ obj* l_Lean_Parser_Level_hole___elambda__1(obj*);
 obj* l___regBuiltinParser_Lean_Parser_Level_max(obj*);
 obj* l_Lean_Parser_symbolOrIdentInfo(obj*);
 obj* l_Lean_Parser_Level_paren___elambda__1___rarg___closed__10;
-obj* l_Lean_Parser_nodeInfo(obj*);
+obj* l_Lean_Parser_nodeInfo(obj*, obj*);
 obj* l_Lean_Parser_Level_addLit___elambda__1___closed__6;
 obj* l_Array_size(obj*, obj*);
 obj* l_Lean_Parser_mkLevelParserAttribute___closed__3;
@@ -667,10 +667,11 @@ return x_3;
 obj* _init_l_Lean_Parser_Level_paren___closed__6() {
 _start:
 {
-obj* x_1; obj* x_2; 
-x_1 = l_Lean_Parser_Level_paren___closed__5;
-x_2 = l_Lean_Parser_nodeInfo(x_1);
-return x_2;
+obj* x_1; obj* x_2; obj* x_3; 
+x_1 = l_Lean_Parser_Level_paren___elambda__1___rarg___closed__4;
+x_2 = l_Lean_Parser_Level_paren___closed__5;
+x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
+return x_3;
 }
 }
 obj* _init_l_Lean_Parser_Level_paren___closed__7() {
@@ -907,10 +908,11 @@ return x_3;
 obj* _init_l_Lean_Parser_Level_max___closed__3() {
 _start:
 {
-obj* x_1; obj* x_2; 
-x_1 = l_Lean_Parser_Level_max___closed__2;
-x_2 = l_Lean_Parser_nodeInfo(x_1);
-return x_2;
+obj* x_1; obj* x_2; obj* x_3; 
+x_1 = l_Lean_Parser_Level_max___elambda__1___closed__1;
+x_2 = l_Lean_Parser_Level_max___closed__2;
+x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
+return x_3;
 }
 }
 obj* _init_l_Lean_Parser_Level_max___closed__4() {
@@ -1094,10 +1096,11 @@ return x_3;
 obj* _init_l_Lean_Parser_Level_imax___closed__3() {
 _start:
 {
-obj* x_1; obj* x_2; 
-x_1 = l_Lean_Parser_Level_imax___closed__2;
-x_2 = l_Lean_Parser_nodeInfo(x_1);
-return x_2;
+obj* x_1; obj* x_2; obj* x_3; 
+x_1 = l_Lean_Parser_Level_imax___elambda__1___closed__1;
+x_2 = l_Lean_Parser_Level_imax___closed__2;
+x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
+return x_3;
 }
 }
 obj* _init_l_Lean_Parser_Level_imax___closed__4() {
@@ -1298,10 +1301,11 @@ return x_3;
 obj* _init_l_Lean_Parser_Level_hole___closed__2() {
 _start:
 {
-obj* x_1; obj* x_2; 
-x_1 = l_Lean_Parser_Level_hole___closed__1;
-x_2 = l_Lean_Parser_nodeInfo(x_1);
-return x_2;
+obj* x_1; obj* x_2; obj* x_3; 
+x_1 = l_Lean_Parser_Level_hole___elambda__1___rarg___closed__2;
+x_2 = l_Lean_Parser_Level_hole___closed__1;
+x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
+return x_3;
 }
 }
 obj* _init_l_Lean_Parser_Level_hole___closed__3() {
@@ -1749,10 +1753,11 @@ return x_3;
 obj* _init_l_Lean_Parser_Level_addLit___closed__5() {
 _start:
 {
-obj* x_1; obj* x_2; 
-x_1 = l_Lean_Parser_Level_addLit___closed__4;
-x_2 = l_Lean_Parser_nodeInfo(x_1);
-return x_2;
+obj* x_1; obj* x_2; obj* x_3; 
+x_1 = l_Lean_Parser_Level_addLit___elambda__1___closed__2;
+x_2 = l_Lean_Parser_Level_addLit___closed__4;
+x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
+return x_3;
 }
 }
 obj* _init_l_Lean_Parser_Level_addLit___closed__6() {

src/stage0/init/lean/parser/module.cpp

@@ -140,7 +140,7 @@ obj* l_Lean_Parser_Module_prelude___closed__4;
 obj* l_Lean_Parser_Module_prelude___elambda__1(obj*);
 extern obj* l_Lean_Parser_ParserContextCore_inhabited___closed__1;
 obj* l_List_mfor___main___at___private_init_lean_parser_module_4__testModuleParserAux___main___spec__5(obj*, obj*);
-obj* l_Lean_Parser_nodeInfo(obj*);
+obj* l_Lean_Parser_nodeInfo(obj*, obj*);
 obj* l_Lean_Message_toString(obj*);
 obj* l_Array_size(obj*, obj*);
 obj* l_Lean_Parser_Module_import___elambda__1___closed__5;
@@ -335,10 +335,11 @@ return x_3;
 obj* _init_l_Lean_Parser_Module_prelude___closed__2() {
 _start:
 {
-obj* x_1; obj* x_2; 
-x_1 = l_Lean_Parser_Module_prelude___closed__1;
-x_2 = l_Lean_Parser_nodeInfo(x_1);
-return x_2;
+obj* x_1; obj* x_2; obj* x_3; 
+x_1 = l_Lean_Parser_Module_prelude___elambda__1___rarg___closed__4;
+x_2 = l_Lean_Parser_Module_prelude___closed__1;
+x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
+return x_3;
 }
 }
 obj* _init_l_Lean_Parser_Module_prelude___closed__3() {
@@ -526,10 +527,11 @@ return x_3;
 obj* _init_l_Lean_Parser_Module_importPath___closed__4() {
 _start:
 {
-obj* x_1; obj* x_2; 
-x_1 = l_Lean_Parser_Module_importPath___closed__3;
-x_2 = l_Lean_Parser_nodeInfo(x_1);
-return x_2;
+obj* x_1; obj* x_2; obj* x_3; 
+x_1 = l_Lean_Parser_Module_importPath___elambda__1___closed__2;
+x_2 = l_Lean_Parser_Module_importPath___closed__3;
+x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
+return x_3;
 }
 }
 obj* _init_l_Lean_Parser_Module_importPath___closed__5() {
@@ -850,10 +852,11 @@ return x_4;
 obj* _init_l_Lean_Parser_Module_import___closed__3() {
 _start:
 {
-obj* x_1; obj* x_2; 
-x_1 = l_Lean_Parser_Module_import___closed__2;
-x_2 = l_Lean_Parser_nodeInfo(x_1);
-return x_2;
+obj* x_1; obj* x_2; obj* x_3; 
+x_1 = l_Lean_Parser_Module_import___elambda__1___closed__2;
+x_2 = l_Lean_Parser_Module_import___closed__2;
+x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
+return x_3;
 }
 }
 obj* _init_l_Lean_Parser_Module_import___closed__4() {
@@ -1143,10 +1146,11 @@ return x_3;
 obj* _init_l_Lean_Parser_Module_header___closed__4() {
 _start:
 {
-obj* x_1; obj* x_2; 
-x_1 = l_Lean_Parser_Module_header___closed__3;
-x_2 = l_Lean_Parser_nodeInfo(x_1);
-return x_2;
+obj* x_1; obj* x_2; obj* x_3; 
+x_1 = l_Lean_Parser_Module_header___elambda__1___closed__2;
+x_2 = l_Lean_Parser_Module_header___closed__3;
+x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
+return x_3;
 }
 }
 obj* _init_l_Lean_Parser_Module_header___closed__5() {