From 607749e26397a8b5c4f4fac85a04b3e2fa7ce8d5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 30 Dec 2019 19:42:57 -0800 Subject: [PATCH] chore: update stage0 --- stage0/src/Init/Lean/Data/Name.lean | 7 +- stage0/src/Init/Lean/Parser/Parser.lean | 2 +- stage0/src/Init/LeanExt.lean | 43 +++++ stage0/stdlib/CMakeLists.txt | 2 +- stage0/stdlib/Init/Lean/Data/Name.c | 6 +- stage0/stdlib/Init/Lean/Parser/Parser.c | 237 ++++++++++-------------- stage0/stdlib/Init/LeanExt.c | 33 ++++ 7 files changed, 180 insertions(+), 150 deletions(-) create mode 100644 stage0/src/Init/LeanExt.lean create mode 100644 stage0/stdlib/Init/LeanExt.c diff --git a/stage0/src/Init/Lean/Data/Name.lean b/stage0/src/Init/Lean/Data/Name.lean index 16a91eda37..6f3bf554cd 100644 --- a/stage0/src/Init/Lean/Data/Name.lean +++ b/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⟩ diff --git a/stage0/src/Init/Lean/Parser/Parser.lean b/stage0/src/Init/Lean/Parser/Parser.lean index f4201dbc30..00115a7f09 100644 --- a/stage0/src/Init/Lean/Parser/Parser.lean +++ b/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")) diff --git a/stage0/src/Init/LeanExt.lean b/stage0/src/Init/LeanExt.lean new file mode 100644 index 0000000000..edc3d3bcef --- /dev/null +++ b/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 diff --git a/stage0/stdlib/CMakeLists.txt b/stage0/stdlib/CMakeLists.txt index 3e416a4f07..e18e5eb88a 100644 --- a/stage0/stdlib/CMakeLists.txt +++ b/stage0/stdlib/CMakeLists.txt @@ -1 +1 @@ -add_library (stage0 OBJECT Init/./Coe.c Init/./Control.c Init/./Control/Alternative.c Init/./Control/Applicative.c Init/./Control/Conditional.c Init/./Control/EState.c Init/./Control/Except.c Init/./Control/Functor.c Init/./Control/Id.c Init/./Control/Lift.c Init/./Control/Monad.c Init/./Control/MonadFail.c Init/./Control/Option.c Init/./Control/Reader.c Init/./Control/State.c Init/./Core.c Init/./Data.c Init/./Data/Array.c Init/./Data/Array/Basic.c Init/./Data/Array/BinSearch.c Init/./Data/Array/QSort.c Init/./Data/AssocList.c Init/./Data/Basic.c Init/./Data/BinomialHeap.c Init/./Data/BinomialHeap/Basic.c Init/./Data/ByteArray.c Init/./Data/ByteArray/Basic.c Init/./Data/Char.c Init/./Data/Char/Basic.c Init/./Data/DList.c Init/./Data/Fin.c Init/./Data/Fin/Basic.c Init/./Data/HashMap.c Init/./Data/HashMap/Basic.c Init/./Data/HashSet.c Init/./Data/Hashable.c Init/./Data/Int.c Init/./Data/Int/Basic.c Init/./Data/List.c Init/./Data/List/Basic.c Init/./Data/List/BasicAux.c Init/./Data/List/Control.c Init/./Data/List/Instances.c Init/./Data/Nat.c Init/./Data/Nat/Basic.c Init/./Data/Nat/Bitwise.c Init/./Data/Nat/Control.c Init/./Data/Nat/Div.c Init/./Data/Option.c Init/./Data/Option/Basic.c Init/./Data/Option/BasicAux.c Init/./Data/Option/Instances.c Init/./Data/PersistentArray.c Init/./Data/PersistentArray/Basic.c Init/./Data/PersistentHashMap.c Init/./Data/PersistentHashMap/Basic.c Init/./Data/PersistentHashSet.c Init/./Data/Queue.c Init/./Data/Queue/Basic.c Init/./Data/RBMap.c Init/./Data/RBMap/Basic.c Init/./Data/RBMap/BasicAux.c Init/./Data/RBTree.c Init/./Data/RBTree/Basic.c Init/./Data/Random.c Init/./Data/Repr.c Init/./Data/Stack.c Init/./Data/Stack/Basic.c Init/./Data/String.c Init/./Data/String/Basic.c Init/./Data/ToString.c Init/./Data/UInt.c Init/./Default.c Init/./Fix.c Init/./Lean.c Init/./Lean/Attributes.c Init/./Lean/AuxRecursor.c Init/./Lean/Class.c Init/./Lean/Compiler.c Init/./Lean/Compiler/ClosedTermCache.c Init/./Lean/Compiler/ConstFolding.c Init/./Lean/Compiler/ExportAttr.c Init/./Lean/Compiler/ExternAttr.c Init/./Lean/Compiler/IR.c Init/./Lean/Compiler/IR/Basic.c Init/./Lean/Compiler/IR/Borrow.c Init/./Lean/Compiler/IR/Boxing.c Init/./Lean/Compiler/IR/Checker.c Init/./Lean/Compiler/IR/CompilerM.c Init/./Lean/Compiler/IR/CtorLayout.c Init/./Lean/Compiler/IR/ElimDeadBranches.c Init/./Lean/Compiler/IR/ElimDeadVars.c Init/./Lean/Compiler/IR/EmitC.c Init/./Lean/Compiler/IR/EmitUtil.c Init/./Lean/Compiler/IR/ExpandResetReuse.c Init/./Lean/Compiler/IR/Format.c Init/./Lean/Compiler/IR/FreeVars.c Init/./Lean/Compiler/IR/LiveVars.c Init/./Lean/Compiler/IR/NormIds.c Init/./Lean/Compiler/IR/PushProj.c Init/./Lean/Compiler/IR/RC.c Init/./Lean/Compiler/IR/ResetReuse.c Init/./Lean/Compiler/IR/SimpCase.c Init/./Lean/Compiler/IR/UnboxResult.c Init/./Lean/Compiler/ImplementedByAttr.c Init/./Lean/Compiler/InitAttr.c Init/./Lean/Compiler/InlineAttrs.c Init/./Lean/Compiler/NameMangling.c Init/./Lean/Compiler/NeverExtractAttr.c Init/./Lean/Compiler/Specialize.c Init/./Lean/Compiler/Util.c Init/./Lean/Data/Format.c Init/./Lean/Data/KVMap.c Init/./Lean/Data/LBool.c Init/./Lean/Data/LOption.c Init/./Lean/Data/Name.c Init/./Lean/Data/NameGenerator.c Init/./Lean/Data/Options.c Init/./Lean/Data/Position.c Init/./Lean/Data/SMap.c Init/./Lean/Data/Trie.c Init/./Lean/Declaration.c Init/./Lean/Elab.c Init/./Lean/Elab/Alias.c Init/./Lean/Elab/BuiltinNotation.c Init/./Lean/Elab/Command.c Init/./Lean/Elab/ElabStrategyAttrs.c Init/./Lean/Elab/Exception.c Init/./Lean/Elab/Frontend.c Init/./Lean/Elab/Import.c Init/./Lean/Elab/Level.c Init/./Lean/Elab/Log.c Init/./Lean/Elab/Quotation.c Init/./Lean/Elab/ResolveName.c Init/./Lean/Elab/Term.c Init/./Lean/Elab/TermApp.c Init/./Lean/Elab/TermBinders.c Init/./Lean/Elab/Util.c Init/./Lean/Environment.c Init/./Lean/EqnCompiler.c Init/./Lean/EqnCompiler/MatchPattern.c Init/./Lean/Eval.c Init/./Lean/Expr.c Init/./Lean/Hygiene.c Init/./Lean/Level.c Init/./Lean/Linter.c Init/./Lean/LocalContext.c Init/./Lean/Meta.c Init/./Lean/Meta/AbstractMVars.c Init/./Lean/Meta/AppBuilder.c Init/./Lean/Meta/Basic.c Init/./Lean/Meta/Check.c Init/./Lean/Meta/DiscrTree.c Init/./Lean/Meta/DiscrTreeTypes.c Init/./Lean/Meta/Exception.c Init/./Lean/Meta/ExprDefEq.c Init/./Lean/Meta/FunInfo.c Init/./Lean/Meta/InferType.c Init/./Lean/Meta/Instances.c Init/./Lean/Meta/LevelDefEq.c Init/./Lean/Meta/Message.c Init/./Lean/Meta/Offset.c Init/./Lean/Meta/Reduce.c Init/./Lean/Meta/SynthInstance.c Init/./Lean/Meta/Tactic.c Init/./Lean/Meta/Tactic/Assumption.c Init/./Lean/Meta/Tactic/Intro.c Init/./Lean/Meta/Tactic/Util.c Init/./Lean/Meta/WHNF.c Init/./Lean/MetavarContext.c Init/./Lean/Modifiers.c Init/./Lean/Parser.c Init/./Lean/Parser/Command.c Init/./Lean/Parser/Identifier.c Init/./Lean/Parser/Level.c Init/./Lean/Parser/Module.c Init/./Lean/Parser/Parser.c Init/./Lean/Parser/Term.c Init/./Lean/Parser/Transform.c Init/./Lean/ProjFns.c Init/./Lean/ReducibilityAttrs.c Init/./Lean/Runtime.c Init/./Lean/Scopes.c Init/./Lean/Structure.c Init/./Lean/Syntax.c Init/./Lean/ToExpr.c Init/./Lean/Util/Message.c Init/./Lean/Util/MonadCache.c Init/./Lean/Util/Path.c Init/./Lean/Util/Profile.c Init/./Lean/Util/Sorry.c Init/./Lean/Util/Trace.c Init/./Lean/Util/WHNF.c Init/./System.c Init/./System/FilePath.c Init/./System/IO.c Init/./System/Platform.c Init/./Util.c Init/./WF.c) +add_library (stage0 OBJECT Init/./Coe.c Init/./Control.c Init/./Control/Alternative.c Init/./Control/Applicative.c Init/./Control/Conditional.c Init/./Control/EState.c Init/./Control/Except.c Init/./Control/Functor.c Init/./Control/Id.c Init/./Control/Lift.c Init/./Control/Monad.c Init/./Control/MonadFail.c Init/./Control/Option.c Init/./Control/Reader.c Init/./Control/State.c Init/./Core.c Init/./Data.c Init/./Data/Array.c Init/./Data/Array/Basic.c Init/./Data/Array/BinSearch.c Init/./Data/Array/QSort.c Init/./Data/AssocList.c Init/./Data/Basic.c Init/./Data/BinomialHeap.c Init/./Data/BinomialHeap/Basic.c Init/./Data/ByteArray.c Init/./Data/ByteArray/Basic.c Init/./Data/Char.c Init/./Data/Char/Basic.c Init/./Data/DList.c Init/./Data/Fin.c Init/./Data/Fin/Basic.c Init/./Data/HashMap.c Init/./Data/HashMap/Basic.c Init/./Data/HashSet.c Init/./Data/Hashable.c Init/./Data/Int.c Init/./Data/Int/Basic.c Init/./Data/List.c Init/./Data/List/Basic.c Init/./Data/List/BasicAux.c Init/./Data/List/Control.c Init/./Data/List/Instances.c Init/./Data/Nat.c Init/./Data/Nat/Basic.c Init/./Data/Nat/Bitwise.c Init/./Data/Nat/Control.c Init/./Data/Nat/Div.c Init/./Data/Option.c Init/./Data/Option/Basic.c Init/./Data/Option/BasicAux.c Init/./Data/Option/Instances.c Init/./Data/PersistentArray.c Init/./Data/PersistentArray/Basic.c Init/./Data/PersistentHashMap.c Init/./Data/PersistentHashMap/Basic.c Init/./Data/PersistentHashSet.c Init/./Data/Queue.c Init/./Data/Queue/Basic.c Init/./Data/RBMap.c Init/./Data/RBMap/Basic.c Init/./Data/RBMap/BasicAux.c Init/./Data/RBTree.c Init/./Data/RBTree/Basic.c Init/./Data/Random.c Init/./Data/Repr.c Init/./Data/Stack.c Init/./Data/Stack/Basic.c Init/./Data/String.c Init/./Data/String/Basic.c Init/./Data/ToString.c Init/./Data/UInt.c Init/./Default.c Init/./Fix.c Init/./Lean.c Init/./Lean/Attributes.c Init/./Lean/AuxRecursor.c Init/./Lean/Class.c Init/./Lean/Compiler.c Init/./Lean/Compiler/ClosedTermCache.c Init/./Lean/Compiler/ConstFolding.c Init/./Lean/Compiler/ExportAttr.c Init/./Lean/Compiler/ExternAttr.c Init/./Lean/Compiler/IR.c Init/./Lean/Compiler/IR/Basic.c Init/./Lean/Compiler/IR/Borrow.c Init/./Lean/Compiler/IR/Boxing.c Init/./Lean/Compiler/IR/Checker.c Init/./Lean/Compiler/IR/CompilerM.c Init/./Lean/Compiler/IR/CtorLayout.c Init/./Lean/Compiler/IR/ElimDeadBranches.c Init/./Lean/Compiler/IR/ElimDeadVars.c Init/./Lean/Compiler/IR/EmitC.c Init/./Lean/Compiler/IR/EmitUtil.c Init/./Lean/Compiler/IR/ExpandResetReuse.c Init/./Lean/Compiler/IR/Format.c Init/./Lean/Compiler/IR/FreeVars.c Init/./Lean/Compiler/IR/LiveVars.c Init/./Lean/Compiler/IR/NormIds.c Init/./Lean/Compiler/IR/PushProj.c Init/./Lean/Compiler/IR/RC.c Init/./Lean/Compiler/IR/ResetReuse.c Init/./Lean/Compiler/IR/SimpCase.c Init/./Lean/Compiler/IR/UnboxResult.c Init/./Lean/Compiler/ImplementedByAttr.c Init/./Lean/Compiler/InitAttr.c Init/./Lean/Compiler/InlineAttrs.c Init/./Lean/Compiler/NameMangling.c Init/./Lean/Compiler/NeverExtractAttr.c Init/./Lean/Compiler/Specialize.c Init/./Lean/Compiler/Util.c Init/./Lean/Data/Format.c Init/./Lean/Data/KVMap.c Init/./Lean/Data/LBool.c Init/./Lean/Data/LOption.c Init/./Lean/Data/Name.c Init/./Lean/Data/NameGenerator.c Init/./Lean/Data/Options.c Init/./Lean/Data/Position.c Init/./Lean/Data/SMap.c Init/./Lean/Data/Trie.c Init/./Lean/Declaration.c Init/./Lean/Elab.c Init/./Lean/Elab/Alias.c Init/./Lean/Elab/BuiltinNotation.c Init/./Lean/Elab/Command.c Init/./Lean/Elab/ElabStrategyAttrs.c Init/./Lean/Elab/Exception.c Init/./Lean/Elab/Frontend.c Init/./Lean/Elab/Import.c Init/./Lean/Elab/Level.c Init/./Lean/Elab/Log.c Init/./Lean/Elab/Quotation.c Init/./Lean/Elab/ResolveName.c Init/./Lean/Elab/Term.c Init/./Lean/Elab/TermApp.c Init/./Lean/Elab/TermBinders.c Init/./Lean/Elab/Util.c Init/./Lean/Environment.c Init/./Lean/EqnCompiler.c Init/./Lean/EqnCompiler/MatchPattern.c Init/./Lean/Eval.c Init/./Lean/Expr.c Init/./Lean/Hygiene.c Init/./Lean/Level.c Init/./Lean/Linter.c Init/./Lean/LocalContext.c Init/./Lean/Meta.c Init/./Lean/Meta/AbstractMVars.c Init/./Lean/Meta/AppBuilder.c Init/./Lean/Meta/Basic.c Init/./Lean/Meta/Check.c Init/./Lean/Meta/DiscrTree.c Init/./Lean/Meta/DiscrTreeTypes.c Init/./Lean/Meta/Exception.c Init/./Lean/Meta/ExprDefEq.c Init/./Lean/Meta/FunInfo.c Init/./Lean/Meta/InferType.c Init/./Lean/Meta/Instances.c Init/./Lean/Meta/LevelDefEq.c Init/./Lean/Meta/Message.c Init/./Lean/Meta/Offset.c Init/./Lean/Meta/Reduce.c Init/./Lean/Meta/SynthInstance.c Init/./Lean/Meta/Tactic.c Init/./Lean/Meta/Tactic/Assumption.c Init/./Lean/Meta/Tactic/Intro.c Init/./Lean/Meta/Tactic/Util.c Init/./Lean/Meta/WHNF.c Init/./Lean/MetavarContext.c Init/./Lean/Modifiers.c Init/./Lean/Parser.c Init/./Lean/Parser/Command.c Init/./Lean/Parser/Identifier.c Init/./Lean/Parser/Level.c Init/./Lean/Parser/Module.c Init/./Lean/Parser/Parser.c Init/./Lean/Parser/Term.c Init/./Lean/Parser/Transform.c Init/./Lean/ProjFns.c Init/./Lean/ReducibilityAttrs.c Init/./Lean/Runtime.c Init/./Lean/Scopes.c Init/./Lean/Structure.c Init/./Lean/Syntax.c Init/./Lean/ToExpr.c Init/./Lean/Util/Message.c Init/./Lean/Util/MonadCache.c Init/./Lean/Util/Path.c Init/./Lean/Util/Profile.c Init/./Lean/Util/Sorry.c Init/./Lean/Util/Trace.c Init/./Lean/Util/WHNF.c Init/./LeanExt.c Init/./System.c Init/./System/FilePath.c Init/./System/IO.c Init/./System/Platform.c Init/./Util.c Init/./WF.c) diff --git a/stage0/stdlib/Init/Lean/Data/Name.c b/stage0/stdlib/Init/Lean/Data/Name.c index 6800643b98..4e9afb3d5d 100644 --- a/stage0/stdlib/Init/Lean/Data/Name.c +++ b/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()); diff --git a/stage0/stdlib/Init/Lean/Parser/Parser.c b/stage0/stdlib/Init/Lean/Parser/Parser.c index fd5e2ec752..2a2b12a925 100644 --- a/stage0/stdlib/Init/Lean/Parser/Parser.c +++ b/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: { diff --git a/stage0/stdlib/Init/LeanExt.c b/stage0/stdlib/Init/LeanExt.c new file mode 100644 index 0000000000..6fad47d0f5 --- /dev/null +++ b/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