chore: update stage0

stage0/src/Init/Lean/Data/Name.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
-import Init.Data.String.Basic
+import Init.LeanExt
 import Init.Coe
 import Init.Data.UInt
 import Init.Data.ToString
@@ -14,11 +14,6 @@ import Init.Data.RBTree
 
 namespace Lean
 
-inductive Name
-| anonymous : Name
-| str : Name → String → USize → Name
-| num : Name → Nat → USize → Name
-
 instance Name.inhabited : Inhabited Name :=
 ⟨Name.anonymous⟩
 

stage0/src/Init/Lean/Parser/Parser.lean

@@ -1461,7 +1461,7 @@ registerAttribute {
      match decl.type with
      | Expr.const `Lean.Parser.TrailingParser _ _ =>
        declareTrailingBuiltinParser env refDeclName declName
-     | Expr.app (Expr.const `Lean.Parser.Parser _ _) (Expr.const `Lean.Parser.ParserKind.leading _ _) _ =>
+     | Expr.app (Expr.const `Lean.Parser.Parser _ _) (Expr.const `Lean.ParserKind.leading _ _) _ =>
        declareLeadingBuiltinParser env refDeclName declName
      | _ =>
        throw (IO.userError ("unexpected parser type at '" ++ toString declName ++ "' (`Parser` or `TrailingParser` expected"))

stage0/src/Init/LeanExt.lean

@@ -0,0 +1,43 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Data.String.Basic
+import Init.Data.UInt
+
+namespace Lean
+/-
+Basic Lean types used to implement basic extensions.
+Note that this file is part of the Lean `Init` library instead of
+`Lean` actual implementation.
+The idea is to allow users to implement simple parsers, macros and tactics
+without importing the whole `Lean` module.
+It also allow us to use extensions to develop the `Init` library.
+-/
+
+/- Hierarchical names -/
+inductive Name
+| anonymous : Name
+| str : Name → String → USize → Name
+| num : Name → Nat → USize → Name
+
+/-
+  Small DSL for describing parsers. We implement an interpreter for it
+  at `Parser.lean` -/
+inductive ParserDescr
+| andthen       : ParserDescr → ParserDescr → ParserDescr
+| orelse        : ParserDescr → ParserDescr → ParserDescr
+| optional      : ParserDescr → ParserDescr
+| lookahead     : ParserDescr → ParserDescr
+| try           : ParserDescr → ParserDescr
+| many          : ParserDescr → ParserDescr
+| many1         : ParserDescr → ParserDescr
+| sepBy         : ParserDescr → ParserDescr → ParserDescr
+| sepBy1        : ParserDescr → ParserDescr → ParserDescr
+| symbol        : String → Nat → ParserDescr
+| unicodeSymbol : String → String → Nat → ParserDescr
+| parser        : Name → ParserDescr
+
+end Lean

stage0/stdlib/Init/Lean/Data/Name.c

@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Init.Lean.Data.Name
-// Imports: Init.Data.String.Basic Init.Coe Init.Data.UInt Init.Data.ToString Init.Data.Hashable Init.Data.RBMap Init.Data.RBTree
+// Imports: Init.LeanExt Init.Coe Init.Data.UInt Init.Data.ToString Init.Data.Hashable Init.Data.RBMap Init.Data.RBTree
 #include "runtime/lean.h"
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@@ -9075,7 +9075,7 @@ lean_dec(x_2);
 return x_3;
 }
 }
-lean_object* initialize_Init_Data_String_Basic(lean_object*);
+lean_object* initialize_Init_LeanExt(lean_object*);
 lean_object* initialize_Init_Coe(lean_object*);
 lean_object* initialize_Init_Data_UInt(lean_object*);
 lean_object* initialize_Init_Data_ToString(lean_object*);
@@ -9087,7 +9087,7 @@ lean_object* initialize_Init_Lean_Data_Name(lean_object* w) {
 lean_object * res;
 if (_G_initialized) return lean_mk_io_result(lean_box(0));
 _G_initialized = true;
-res = initialize_Init_Data_String_Basic(lean_io_mk_world());
+res = initialize_Init_LeanExt(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
 res = initialize_Init_Coe(lean_io_mk_world());

stage0/stdlib/Init/Lean/Parser/Parser.c

@@ -27221,105 +27221,125 @@ if (lean_obj_tag(x_77) == 1)
 lean_object* x_78; 
 x_78 = lean_ctor_get(x_77, 0);
 lean_inc(x_78);
-if (lean_obj_tag(x_78) == 1)
+if (lean_obj_tag(x_78) == 0)
 {
-lean_object* x_79; 
-x_79 = lean_ctor_get(x_78, 0);
+lean_object* x_79; lean_object* x_80; lean_object* x_81; uint8_t x_82; 
+x_79 = lean_ctor_get(x_75, 1);
 lean_inc(x_79);
-if (lean_obj_tag(x_79) == 0)
-{
-lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83; uint8_t x_84; 
-x_80 = lean_ctor_get(x_75, 1);
-lean_inc(x_80);
 lean_dec(x_75);
-x_81 = lean_ctor_get(x_76, 1);
-lean_inc(x_81);
+x_80 = lean_ctor_get(x_76, 1);
+lean_inc(x_80);
 lean_dec(x_76);
-x_82 = lean_ctor_get(x_77, 1);
-lean_inc(x_82);
+x_81 = lean_ctor_get(x_77, 1);
+lean_inc(x_81);
 lean_dec(x_77);
-x_83 = lean_ctor_get(x_78, 1);
-lean_inc(x_83);
-lean_dec(x_78);
-x_84 = lean_string_dec_eq(x_83, x_67);
-lean_dec(x_83);
-if (x_84 == 0)
-{
-lean_object* x_85; 
-lean_dec(x_82);
+x_82 = lean_string_dec_eq(x_81, x_67);
 lean_dec(x_81);
+if (x_82 == 0)
+{
+lean_object* x_83; 
 lean_dec(x_80);
+lean_dec(x_79);
 lean_dec(x_3);
 lean_dec(x_2);
-x_85 = lean_box(0);
-x_23 = x_85;
+x_83 = lean_box(0);
+x_23 = x_83;
 goto block_31;
 }
 else
 {
-uint8_t x_86; 
-x_86 = lean_string_dec_eq(x_82, x_70);
-lean_dec(x_82);
-if (x_86 == 0)
-{
-lean_object* x_87; 
-lean_dec(x_81);
+lean_object* x_84; uint8_t x_85; 
+x_84 = l_Lean_Parser_registerBuiltinParserAttribute___lambda__1___closed__4;
+x_85 = lean_string_dec_eq(x_80, x_84);
 lean_dec(x_80);
+if (x_85 == 0)
+{
+lean_object* x_86; 
+lean_dec(x_79);
 lean_dec(x_3);
 lean_dec(x_2);
-x_87 = lean_box(0);
-x_23 = x_87;
+x_86 = lean_box(0);
+x_23 = x_86;
 goto block_31;
 }
 else
 {
-lean_object* x_88; uint8_t x_89; 
-x_88 = l_Lean_Parser_registerBuiltinParserAttribute___lambda__1___closed__4;
-x_89 = lean_string_dec_eq(x_81, x_88);
-lean_dec(x_81);
-if (x_89 == 0)
+lean_object* x_87; uint8_t x_88; 
+x_87 = l_Lean_Parser_registerBuiltinParserAttribute___lambda__1___closed__5;
+x_88 = lean_string_dec_eq(x_79, x_87);
+lean_dec(x_79);
+if (x_88 == 0)
+{
+lean_object* x_89; 
+lean_dec(x_3);
+lean_dec(x_2);
+x_89 = lean_box(0);
+x_23 = x_89;
+goto block_31;
+}
+else
 {
 lean_object* x_90; 
-lean_dec(x_80);
-lean_dec(x_3);
-lean_dec(x_2);
-x_90 = lean_box(0);
-x_23 = x_90;
-goto block_31;
+x_90 = l_Lean_Parser_declareLeadingBuiltinParser(x_3, x_2, x_4, x_7);
+return x_90;
+}
+}
+}
 }
 else
 {
-lean_object* x_91; uint8_t x_92; 
-x_91 = l_Lean_Parser_registerBuiltinParserAttribute___lambda__1___closed__5;
-x_92 = lean_string_dec_eq(x_80, x_91);
-lean_dec(x_80);
-if (x_92 == 0)
+lean_object* x_91; 
+lean_dec(x_78);
+lean_dec(x_77);
+lean_dec(x_76);
+lean_dec(x_75);
+lean_dec(x_3);
+lean_dec(x_2);
+x_91 = lean_box(0);
+x_23 = x_91;
+goto block_31;
+}
+}
+else
+{
+lean_object* x_92; 
+lean_dec(x_77);
+lean_dec(x_76);
+lean_dec(x_75);
+lean_dec(x_3);
+lean_dec(x_2);
+x_92 = lean_box(0);
+x_23 = x_92;
+goto block_31;
+}
+}
+else
 {
 lean_object* x_93; 
+lean_dec(x_76);
+lean_dec(x_75);
 lean_dec(x_3);
 lean_dec(x_2);
 x_93 = lean_box(0);
 x_23 = x_93;
 goto block_31;
 }
+}
 else
 {
 lean_object* x_94; 
-x_94 = l_Lean_Parser_declareLeadingBuiltinParser(x_3, x_2, x_4, x_7);
-return x_94;
-}
-}
-}
+lean_dec(x_75);
+lean_dec(x_3);
+lean_dec(x_2);
+x_94 = lean_box(0);
+x_23 = x_94;
+goto block_31;
 }
 }
 else
 {
 lean_object* x_95; 
-lean_dec(x_79);
-lean_dec(x_78);
-lean_dec(x_77);
-lean_dec(x_76);
-lean_dec(x_75);
+lean_dec(x_63);
 lean_dec(x_3);
 lean_dec(x_2);
 x_95 = lean_box(0);
@@ -27327,13 +27347,17 @@ x_23 = x_95;
 goto block_31;
 }
 }
+}
+}
+}
 else
 {
 lean_object* x_96; 
-lean_dec(x_78);
-lean_dec(x_77);
-lean_dec(x_76);
-lean_dec(x_75);
+lean_dec(x_62);
+lean_dec(x_61);
+lean_dec(x_60);
+lean_dec(x_59);
+lean_dec(x_36);
 lean_dec(x_3);
 lean_dec(x_2);
 x_96 = lean_box(0);
@@ -27344,9 +27368,10 @@ goto block_31;
 else
 {
 lean_object* x_97; 
-lean_dec(x_77);
-lean_dec(x_76);
-lean_dec(x_75);
+lean_dec(x_61);
+lean_dec(x_60);
+lean_dec(x_59);
+lean_dec(x_36);
 lean_dec(x_3);
 lean_dec(x_2);
 x_97 = lean_box(0);
@@ -27357,8 +27382,9 @@ goto block_31;
 else
 {
 lean_object* x_98; 
-lean_dec(x_76);
-lean_dec(x_75);
+lean_dec(x_60);
+lean_dec(x_59);
+lean_dec(x_36);
 lean_dec(x_3);
 lean_dec(x_2);
 x_98 = lean_box(0);
@@ -27369,7 +27395,8 @@ goto block_31;
 else
 {
 lean_object* x_99; 
-lean_dec(x_75);
+lean_dec(x_59);
+lean_dec(x_36);
 lean_dec(x_3);
 lean_dec(x_2);
 x_99 = lean_box(0);
@@ -27380,7 +27407,8 @@ goto block_31;
 else
 {
 lean_object* x_100; 
-lean_dec(x_63);
+lean_dec(x_58);
+lean_dec(x_36);
 lean_dec(x_3);
 lean_dec(x_2);
 x_100 = lean_box(0);
@@ -27388,16 +27416,9 @@ x_23 = x_100;
 goto block_31;
 }
 }
-}
-}
-}
-else
+default: 
 {
 lean_object* x_101; 
-lean_dec(x_62);
-lean_dec(x_61);
-lean_dec(x_60);
-lean_dec(x_59);
 lean_dec(x_36);
 lean_dec(x_3);
 lean_dec(x_2);
@@ -27406,68 +27427,6 @@ x_23 = x_101;
 goto block_31;
 }
 }
-else
-{
-lean_object* x_102; 
-lean_dec(x_61);
-lean_dec(x_60);
-lean_dec(x_59);
-lean_dec(x_36);
-lean_dec(x_3);
-lean_dec(x_2);
-x_102 = lean_box(0);
-x_23 = x_102;
-goto block_31;
-}
-}
-else
-{
-lean_object* x_103; 
-lean_dec(x_60);
-lean_dec(x_59);
-lean_dec(x_36);
-lean_dec(x_3);
-lean_dec(x_2);
-x_103 = lean_box(0);
-x_23 = x_103;
-goto block_31;
-}
-}
-else
-{
-lean_object* x_104; 
-lean_dec(x_59);
-lean_dec(x_36);
-lean_dec(x_3);
-lean_dec(x_2);
-x_104 = lean_box(0);
-x_23 = x_104;
-goto block_31;
-}
-}
-else
-{
-lean_object* x_105; 
-lean_dec(x_58);
-lean_dec(x_36);
-lean_dec(x_3);
-lean_dec(x_2);
-x_105 = lean_box(0);
-x_23 = x_105;
-goto block_31;
-}
-}
-default: 
-{
-lean_object* x_106; 
-lean_dec(x_36);
-lean_dec(x_3);
-lean_dec(x_2);
-x_106 = lean_box(0);
-x_23 = x_106;
-goto block_31;
-}
-}
 }
 block_31:
 {

stage0/stdlib/Init/LeanExt.c

@@ -0,0 +1,33 @@
+// Lean compiler output
+// Module: Init.LeanExt
+// Imports: Init.Data.String.Basic Init.Data.UInt
+#include "runtime/lean.h"
+#if defined(__clang__)
+#pragma clang diagnostic ignored "-Wunused-parameter"
+#pragma clang diagnostic ignored "-Wunused-label"
+#elif defined(__GNUC__) && !defined(__CLANG__)
+#pragma GCC diagnostic ignored "-Wunused-parameter"
+#pragma GCC diagnostic ignored "-Wunused-label"
+#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
+#endif
+#ifdef __cplusplus
+extern "C" {
+#endif
+lean_object* initialize_Init_Data_String_Basic(lean_object*);
+lean_object* initialize_Init_Data_UInt(lean_object*);
+static bool _G_initialized = false;
+lean_object* initialize_Init_LeanExt(lean_object* w) {
+lean_object * res;
+if (_G_initialized) return lean_mk_io_result(lean_box(0));
+_G_initialized = true;
+res = initialize_Init_Data_String_Basic(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+res = initialize_Init_Data_UInt(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+return lean_mk_io_result(lean_box(0));
+}
+#ifdef __cplusplus
+}
+#endif