From 9da4f09c6788fe38313b62486df9baee7792da41 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 19 May 2020 11:24:49 -0700 Subject: [PATCH] chore: update stage0 --- stage0/src/{Init/Default.lean => Init.lean} | 0 stage0/src/Init/Lean/Elab/Import.lean | 4 +- stage0/src/Init/Lean/Util/Path.lean | 14 +- stage0/src/Makefile.in | 2 +- stage0/src/initialize/init.cpp | 4 +- stage0/stdlib/CMakeLists.txt | 2 +- stage0/stdlib/{Init/Default.c => Init.c} | 4 +- stage0/stdlib/Init/Lean/Elab/Import.c | 119 +++++------ stage0/stdlib/Init/Lean/Util/Path.c | 220 +++++++------------- 9 files changed, 132 insertions(+), 237 deletions(-) rename stage0/src/{Init/Default.lean => Init.lean} (100%) rename stage0/stdlib/{Init/Default.c => Init.c} (96%) diff --git a/stage0/src/Init/Default.lean b/stage0/src/Init.lean similarity index 100% rename from stage0/src/Init/Default.lean rename to stage0/src/Init.lean diff --git a/stage0/src/Init/Lean/Elab/Import.lean b/stage0/src/Init/Lean/Elab/Import.lean index 4d5ac679e0..6c43d75af6 100644 --- a/stage0/src/Init/Lean/Elab/Import.lean +++ b/stage0/src/Init/Lean/Elab/Import.lean @@ -11,12 +11,12 @@ namespace Elab def headerToImports (header : Syntax) : List Import := let header := header.asNode; -let imports := if (header.getArg 0).isNone then [{Import . module := `Init.Default}] else []; +let imports := if (header.getArg 0).isNone then [{Import . module := `Init}] else []; imports ++ (header.getArg 1).getArgs.toList.map (fun stx => -- `stx` is of the form `(Module.import "import" "runtime"? id) let runtime := !(stx.getArg 1).isNone; let id := stx.getIdAt 2; - { module := normalizeModuleName id, runtimeOnly := runtime }) + { module := id, runtimeOnly := runtime }) def processHeader (header : Syntax) (messages : MessageLog) (inputCtx : Parser.InputContext) (trustLevel : UInt32 := 0) : IO (Environment × MessageLog) := catch diff --git a/stage0/src/Init/Lean/Util/Path.lean b/stage0/src/Init/Lean/Util/Path.lean index 7477de7844..6b01372943 100644 --- a/stage0/src/Init/Lean/Util/Path.lean +++ b/stage0/src/Init/Lean/Util/Path.lean @@ -5,10 +5,8 @@ Authors: Leonardo de Moura, Sebastian Ullrich Management of the Lean search path (`LEAN_PATH`), which is a list of `pkg=path` mappings from package name to root path. An import `A.B.C` -given an `A=path` entry resolves to `path/B/C.olean`. A package-only -import `A` is normalized to `A.Default`. For the input file, we also -need the reverse direction of finding a (unique) module path from a -file path. +given an `A=path` entry resolves to `path/B/C.olean`, and just `A` to +`path.olean` (meaning that `path` should probably end with `/A`). -/ prelude import Init.System.IO @@ -72,7 +70,6 @@ match path with searchPathRef.set sp def modPathToFilePath : Name → String -| Name.str Name.anonymous h _ => h | Name.str p h _ => modPathToFilePath p ++ pathSep ++ h | Name.anonymous => "" | Name.num p _ _ => panic! "ill-formed import" @@ -90,7 +87,7 @@ sp ← searchPathRef.get; let (pkg, path) := splitAtRoot mod; some root ← pure $ sp.find? pkg | throw $ IO.userError $ "unknown package '" ++ pkg ++ "'"; -let fname := root ++ pathSep ++ modPathToFilePath path ++ ".olean"; +let fname := root ++ modPathToFilePath path ++ ".olean"; pure fname def findAtSearchPath (fname : String) : IO (Option (String × String)) := do @@ -121,9 +118,4 @@ let parts := modNameStr.splitOn pathSep; let modName := parts.foldl mkNameStr Name.anonymous; pure modName --- normalize `A` to `A.Default` -def normalizeModuleName : Name → Name -| Name.str Name.anonymous pkg _ => mkNameSimple pkg ++ "Default" -| m => m - end Lean diff --git a/stage0/src/Makefile.in b/stage0/src/Makefile.in index 82328de09f..78415db2b4 100644 --- a/stage0/src/Makefile.in +++ b/stage0/src/Makefile.in @@ -11,7 +11,7 @@ STATIC_LIB_NAME = lib$(PKG).a LEAN_OPTS = @LEAN_EXTRA_MAKE_OPTS@ LEANC_OPTS = -O3 -DNDEBUG -SRCS = $(shell find $(PKG) -name '*.lean' || true; find $(PKG).lean 2> /dev/null) +SRCS = $(shell find $(PKG) -name '*.lean' 2> /dev/null || true; find $(PKG).lean 2> /dev/null) DEPS = $(addprefix $(TEMP_OUT)/,$(SRCS:.lean=.depend)) export LEAN_PATH=$(PKG)=$(OLEAN_OUT)/$(PKG) OBJS = $(addprefix $(OLEAN_OUT)/, $(SRCS:.lean=.olean)) diff --git a/stage0/src/initialize/init.cpp b/stage0/src/initialize/init.cpp index 43f1f3646b..0189c23c1d 100644 --- a/stage0/src/initialize/init.cpp +++ b/stage0/src/initialize/init.cpp @@ -20,13 +20,13 @@ Author: Leonardo de Moura #include "initialize/init.h" namespace lean { -extern "C" object* initialize_Init_Default(object* w); +extern "C" object* initialize_Init(object* w); extern "C" object* initialize_Init_Lean(object* w); extern "C" void lean_initialize() { save_stack_info(); initialize_util_module(); - consume_io_result(initialize_Init_Default(io_mk_world())); + consume_io_result(initialize_Init(io_mk_world())); consume_io_result(initialize_Init_Lean(io_mk_world())); initialize_kernel_module(); init_default_print_fn(); diff --git a/stage0/stdlib/CMakeLists.txt b/stage0/stdlib/CMakeLists.txt index ac00d9dd38..2418223aa5 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/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/Float.c Init/Data/FloatArray.c Init/Data/FloatArray/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/String/Extra.c Init/Data/ToString.c Init/Data/UInt.c Init/Default.c Init/Fix.c Init/HasCoe.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/Json.c Init/Lean/Data/Json/Basic.c Init/Lean/Data/Json/FromToJson.c Init/Lean/Data/Json/Parser.c Init/Lean/Data/Json/Printer.c Init/Lean/Data/KVMap.c Init/Lean/Data/LBool.c Init/Lean/Data/LOption.c Init/Lean/Data/Name.c Init/Lean/Data/Occurrences.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/Delaborator.c Init/Lean/Elab.c Init/Lean/Elab/Alias.c Init/Lean/Elab/App.c Init/Lean/Elab/Binders.c Init/Lean/Elab/BuiltinNotation.c Init/Lean/Elab/Command.c Init/Lean/Elab/DeclModifiers.c Init/Lean/Elab/Declaration.c Init/Lean/Elab/Definition.c Init/Lean/Elab/DoNotation.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/Match.c Init/Lean/Elab/Quotation.c Init/Lean/Elab/ResolveName.c Init/Lean/Elab/StrategyAttrs.c Init/Lean/Elab/StructInst.c Init/Lean/Elab/Syntax.c Init/Lean/Elab/SyntheticMVars.c Init/Lean/Elab/Tactic.c Init/Lean/Elab/Tactic/Basic.c Init/Lean/Elab/Tactic/ElabTerm.c Init/Lean/Elab/Tactic/Generalize.c Init/Lean/Elab/Tactic/Induction.c Init/Lean/Elab/Tactic/Injection.c Init/Lean/Elab/Term.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/HeadIndex.c Init/Lean/Hygiene.c Init/Lean/KeyedDeclsAttribute.c Init/Lean/Level.c Init/Lean/Linter.c Init/Lean/LocalContext.c Init/Lean/Message.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/GeneralizeTelescope.c Init/Lean/Meta/InferType.c Init/Lean/Meta/Instances.c Init/Lean/Meta/KAbstract.c Init/Lean/Meta/LevelDefEq.c Init/Lean/Meta/Message.c Init/Lean/Meta/Offset.c Init/Lean/Meta/RecursorInfo.c Init/Lean/Meta/Reduce.c Init/Lean/Meta/SynthInstance.c Init/Lean/Meta/Tactic.c Init/Lean/Meta/Tactic/Apply.c Init/Lean/Meta/Tactic/Assert.c Init/Lean/Meta/Tactic/Assumption.c Init/Lean/Meta/Tactic/Cases.c Init/Lean/Meta/Tactic/Clear.c Init/Lean/Meta/Tactic/FVarSubst.c Init/Lean/Meta/Tactic/Generalize.c Init/Lean/Meta/Tactic/Induction.c Init/Lean/Meta/Tactic/Injection.c Init/Lean/Meta/Tactic/Intro.c Init/Lean/Meta/Tactic/LocalDecl.c Init/Lean/Meta/Tactic/Revert.c Init/Lean/Meta/Tactic/Rewrite.c Init/Lean/Meta/Tactic/Subst.c Init/Lean/Meta/Tactic/Target.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/Level.c Init/Lean/Parser/Module.c Init/Lean/Parser/Parser.c Init/Lean/Parser/Syntax.c Init/Lean/Parser/Tactic.c Init/Lean/Parser/Term.c Init/Lean/Parser/Transform.c Init/Lean/PrettyPrinter.c Init/Lean/PrettyPrinter/Parenthesizer.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.c Init/Lean/Util/Closure.c Init/Lean/Util/CollectFVars.c Init/Lean/Util/CollectLevelParams.c Init/Lean/Util/CollectMVars.c Init/Lean/Util/FindExpr.c Init/Lean/Util/FindMVar.c Init/Lean/Util/FoldConsts.c Init/Lean/Util/MonadCache.c Init/Lean/Util/PPExt.c Init/Lean/Util/PPGoal.c Init/Lean/Util/Path.c Init/Lean/Util/Profile.c Init/Lean/Util/RecDepth.c Init/Lean/Util/Recognizers.c Init/Lean/Util/ReplaceExpr.c Init/Lean/Util/Sorry.c Init/Lean/Util/Trace.c Init/Lean/Util/WHNF.c Init/LeanInit.c Init/ShareCommon.c Init/System.c Init/System/FilePath.c Init/System/IO.c Init/System/IOError.c Init/System/Platform.c Init/Util.c Init/WF.c ) +add_library (stage0 OBJECT ./Init.c ./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/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/Float.c ./Init/Data/FloatArray.c ./Init/Data/FloatArray/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/String/Extra.c ./Init/Data/ToString.c ./Init/Data/UInt.c ./Init/Fix.c ./Init/HasCoe.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/Json.c ./Init/Lean/Data/Json/Basic.c ./Init/Lean/Data/Json/FromToJson.c ./Init/Lean/Data/Json/Parser.c ./Init/Lean/Data/Json/Printer.c ./Init/Lean/Data/KVMap.c ./Init/Lean/Data/LBool.c ./Init/Lean/Data/LOption.c ./Init/Lean/Data/Name.c ./Init/Lean/Data/Occurrences.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/Delaborator.c ./Init/Lean/Elab.c ./Init/Lean/Elab/Alias.c ./Init/Lean/Elab/App.c ./Init/Lean/Elab/Binders.c ./Init/Lean/Elab/BuiltinNotation.c ./Init/Lean/Elab/Command.c ./Init/Lean/Elab/DeclModifiers.c ./Init/Lean/Elab/Declaration.c ./Init/Lean/Elab/Definition.c ./Init/Lean/Elab/DoNotation.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/Match.c ./Init/Lean/Elab/Quotation.c ./Init/Lean/Elab/ResolveName.c ./Init/Lean/Elab/StrategyAttrs.c ./Init/Lean/Elab/StructInst.c ./Init/Lean/Elab/Syntax.c ./Init/Lean/Elab/SyntheticMVars.c ./Init/Lean/Elab/Tactic.c ./Init/Lean/Elab/Tactic/Basic.c ./Init/Lean/Elab/Tactic/ElabTerm.c ./Init/Lean/Elab/Tactic/Generalize.c ./Init/Lean/Elab/Tactic/Induction.c ./Init/Lean/Elab/Tactic/Injection.c ./Init/Lean/Elab/Term.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/HeadIndex.c ./Init/Lean/Hygiene.c ./Init/Lean/KeyedDeclsAttribute.c ./Init/Lean/Level.c ./Init/Lean/Linter.c ./Init/Lean/LocalContext.c ./Init/Lean/Message.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/GeneralizeTelescope.c ./Init/Lean/Meta/InferType.c ./Init/Lean/Meta/Instances.c ./Init/Lean/Meta/KAbstract.c ./Init/Lean/Meta/LevelDefEq.c ./Init/Lean/Meta/Message.c ./Init/Lean/Meta/Offset.c ./Init/Lean/Meta/RecursorInfo.c ./Init/Lean/Meta/Reduce.c ./Init/Lean/Meta/SynthInstance.c ./Init/Lean/Meta/Tactic.c ./Init/Lean/Meta/Tactic/Apply.c ./Init/Lean/Meta/Tactic/Assert.c ./Init/Lean/Meta/Tactic/Assumption.c ./Init/Lean/Meta/Tactic/Cases.c ./Init/Lean/Meta/Tactic/Clear.c ./Init/Lean/Meta/Tactic/FVarSubst.c ./Init/Lean/Meta/Tactic/Generalize.c ./Init/Lean/Meta/Tactic/Induction.c ./Init/Lean/Meta/Tactic/Injection.c ./Init/Lean/Meta/Tactic/Intro.c ./Init/Lean/Meta/Tactic/LocalDecl.c ./Init/Lean/Meta/Tactic/Revert.c ./Init/Lean/Meta/Tactic/Rewrite.c ./Init/Lean/Meta/Tactic/Subst.c ./Init/Lean/Meta/Tactic/Target.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/Level.c ./Init/Lean/Parser/Module.c ./Init/Lean/Parser/Parser.c ./Init/Lean/Parser/Syntax.c ./Init/Lean/Parser/Tactic.c ./Init/Lean/Parser/Term.c ./Init/Lean/Parser/Transform.c ./Init/Lean/PrettyPrinter.c ./Init/Lean/PrettyPrinter/Parenthesizer.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.c ./Init/Lean/Util/Closure.c ./Init/Lean/Util/CollectFVars.c ./Init/Lean/Util/CollectLevelParams.c ./Init/Lean/Util/CollectMVars.c ./Init/Lean/Util/FindExpr.c ./Init/Lean/Util/FindMVar.c ./Init/Lean/Util/FoldConsts.c ./Init/Lean/Util/MonadCache.c ./Init/Lean/Util/PPExt.c ./Init/Lean/Util/PPGoal.c ./Init/Lean/Util/Path.c ./Init/Lean/Util/Profile.c ./Init/Lean/Util/RecDepth.c ./Init/Lean/Util/Recognizers.c ./Init/Lean/Util/ReplaceExpr.c ./Init/Lean/Util/Sorry.c ./Init/Lean/Util/Trace.c ./Init/Lean/Util/WHNF.c ./Init/LeanInit.c ./Init/ShareCommon.c ./Init/System.c ./Init/System/FilePath.c ./Init/System/IO.c ./Init/System/IOError.c ./Init/System/Platform.c ./Init/Util.c ./Init/WF.c ) diff --git a/stage0/stdlib/Init/Default.c b/stage0/stdlib/Init.c similarity index 96% rename from stage0/stdlib/Init/Default.c rename to stage0/stdlib/Init.c index b491740823..f3576b7b31 100644 --- a/stage0/stdlib/Init/Default.c +++ b/stage0/stdlib/Init.c @@ -1,5 +1,5 @@ // Lean compiler output -// Module: Init.Default +// Module: Init // Imports: Init.Core Init.Control Init.Data.Basic Init.WF Init.Data Init.System Init.Util Init.Fix Init.LeanInit Init.ShareCommon #include #if defined(__clang__) @@ -24,7 +24,7 @@ lean_object* initialize_Init_Fix(lean_object*); lean_object* initialize_Init_LeanInit(lean_object*); lean_object* initialize_Init_ShareCommon(lean_object*); static bool _G_initialized = false; -lean_object* initialize_Init_Default(lean_object* w) { +lean_object* initialize_Init(lean_object* w) { lean_object * res; if (_G_initialized) return lean_mk_io_result(lean_box(0)); _G_initialized = true; diff --git a/stage0/stdlib/Init/Lean/Elab/Import.c b/stage0/stdlib/Init/Lean/Elab/Import.c index b05aed0850..04b9d65883 100644 --- a/stage0/stdlib/Init/Lean/Elab/Import.c +++ b/stage0/stdlib/Init/Lean/Elab/Import.c @@ -13,7 +13,6 @@ #ifdef __cplusplus extern "C" { #endif -lean_object* l_Lean_Elab_headerToImports___closed__4; lean_object* l_Lean_Parser_parseHeader(lean_object*, lean_object*); lean_object* lean_io_error_to_string(lean_object*); lean_object* l_List_map___main___at_Lean_Elab_headerToImports___spec__1(lean_object*); @@ -41,7 +40,6 @@ lean_object* l_Lean_FileMap_ofString(lean_object*); lean_object* lean_mk_empty_environment(uint32_t, lean_object*); lean_object* lean_import_modules(lean_object*, uint32_t, lean_object*); extern lean_object* l_Lean_Syntax_inhabited; -extern lean_object* l_Lean_normalizeModuleName___closed__1; lean_object* l_Lean_Syntax_getArgs(lean_object*); extern lean_object* l_Lean_getBuiltinSearchPath___closed__4; lean_object* lean_parse_imports(lean_object*, lean_object*, lean_object*); @@ -52,7 +50,6 @@ lean_object* l_Lean_Elab_parseImports(lean_object*, lean_object*, lean_object*); lean_object* l_List_forM___main___at_Lean_Elab_printDeps___spec__1(lean_object*, lean_object*); lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*); lean_object* l_Lean_Syntax_asNode(lean_object*); -lean_object* l_Lean_normalizeModuleName(lean_object*); lean_object* l_List_map___main___at_Lean_Elab_headerToImports___spec__1(lean_object* x_1) { _start: { @@ -68,7 +65,7 @@ uint8_t x_3; x_3 = !lean_is_exclusive(x_1); if (x_3 == 0) { -lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; uint8_t x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; +lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; uint8_t x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; x_4 = lean_ctor_get(x_1, 0); x_5 = lean_ctor_get(x_1, 1); x_6 = lean_unsigned_to_nat(1u); @@ -78,71 +75,69 @@ lean_dec(x_7); x_9 = lean_unsigned_to_nat(2u); x_10 = l_Lean_Syntax_getIdAt(x_4, x_9); lean_dec(x_4); -x_11 = l_Lean_normalizeModuleName(x_10); -x_12 = l_List_map___main___at_Lean_Elab_headerToImports___spec__1(x_5); +x_11 = l_List_map___main___at_Lean_Elab_headerToImports___spec__1(x_5); if (x_8 == 0) { -uint8_t x_13; lean_object* x_14; -x_13 = 1; -x_14 = lean_alloc_ctor(0, 1, 1); -lean_ctor_set(x_14, 0, x_11); -lean_ctor_set_uint8(x_14, sizeof(void*)*1, x_13); -lean_ctor_set(x_1, 1, x_12); -lean_ctor_set(x_1, 0, x_14); +uint8_t x_12; lean_object* x_13; +x_12 = 1; +x_13 = lean_alloc_ctor(0, 1, 1); +lean_ctor_set(x_13, 0, x_10); +lean_ctor_set_uint8(x_13, sizeof(void*)*1, x_12); +lean_ctor_set(x_1, 1, x_11); +lean_ctor_set(x_1, 0, x_13); return x_1; } else { -uint8_t x_15; lean_object* x_16; -x_15 = 0; -x_16 = lean_alloc_ctor(0, 1, 1); -lean_ctor_set(x_16, 0, x_11); -lean_ctor_set_uint8(x_16, sizeof(void*)*1, x_15); -lean_ctor_set(x_1, 1, x_12); -lean_ctor_set(x_1, 0, x_16); +uint8_t x_14; lean_object* x_15; +x_14 = 0; +x_15 = lean_alloc_ctor(0, 1, 1); +lean_ctor_set(x_15, 0, x_10); +lean_ctor_set_uint8(x_15, sizeof(void*)*1, x_14); +lean_ctor_set(x_1, 1, x_11); +lean_ctor_set(x_1, 0, x_15); return x_1; } } else { -lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; uint8_t x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; -x_17 = lean_ctor_get(x_1, 0); -x_18 = lean_ctor_get(x_1, 1); -lean_inc(x_18); +lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; uint8_t x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; +x_16 = lean_ctor_get(x_1, 0); +x_17 = lean_ctor_get(x_1, 1); lean_inc(x_17); +lean_inc(x_16); lean_dec(x_1); -x_19 = lean_unsigned_to_nat(1u); -x_20 = l_Lean_Syntax_getArg(x_17, x_19); -x_21 = l_Lean_Syntax_isNone(x_20); -lean_dec(x_20); -x_22 = lean_unsigned_to_nat(2u); -x_23 = l_Lean_Syntax_getIdAt(x_17, x_22); -lean_dec(x_17); -x_24 = l_Lean_normalizeModuleName(x_23); -x_25 = l_List_map___main___at_Lean_Elab_headerToImports___spec__1(x_18); -if (x_21 == 0) +x_18 = lean_unsigned_to_nat(1u); +x_19 = l_Lean_Syntax_getArg(x_16, x_18); +x_20 = l_Lean_Syntax_isNone(x_19); +lean_dec(x_19); +x_21 = lean_unsigned_to_nat(2u); +x_22 = l_Lean_Syntax_getIdAt(x_16, x_21); +lean_dec(x_16); +x_23 = l_List_map___main___at_Lean_Elab_headerToImports___spec__1(x_17); +if (x_20 == 0) { -uint8_t x_26; lean_object* x_27; lean_object* x_28; -x_26 = 1; -x_27 = lean_alloc_ctor(0, 1, 1); -lean_ctor_set(x_27, 0, x_24); -lean_ctor_set_uint8(x_27, sizeof(void*)*1, x_26); -x_28 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_28, 0, x_27); -lean_ctor_set(x_28, 1, x_25); -return x_28; +uint8_t x_24; lean_object* x_25; lean_object* x_26; +x_24 = 1; +x_25 = lean_alloc_ctor(0, 1, 1); +lean_ctor_set(x_25, 0, x_22); +lean_ctor_set_uint8(x_25, sizeof(void*)*1, x_24); +x_26 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_26, 0, x_25); +lean_ctor_set(x_26, 1, x_23); +return x_26; } else { -uint8_t x_29; lean_object* x_30; lean_object* x_31; -x_29 = 0; -x_30 = lean_alloc_ctor(0, 1, 1); -lean_ctor_set(x_30, 0, x_24); -lean_ctor_set_uint8(x_30, sizeof(void*)*1, x_29); -x_31 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_31, 0, x_30); -lean_ctor_set(x_31, 1, x_25); -return x_31; +uint8_t x_27; lean_object* x_28; lean_object* x_29; +x_27 = 0; +x_28 = lean_alloc_ctor(0, 1, 1); +lean_ctor_set(x_28, 0, x_22); +lean_ctor_set_uint8(x_28, sizeof(void*)*1, x_27); +x_29 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_29, 0, x_28); +lean_ctor_set(x_29, 1, x_23); +return x_29; } } } @@ -161,18 +156,8 @@ return x_3; lean_object* _init_l_Lean_Elab_headerToImports___closed__2() { _start: { -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Elab_headerToImports___closed__1; -x_2 = l_Lean_normalizeModuleName___closed__1; -x_3 = lean_name_mk_string(x_1, x_2); -return x_3; -} -} -lean_object* _init_l_Lean_Elab_headerToImports___closed__3() { -_start: -{ lean_object* x_1; uint8_t x_2; lean_object* x_3; -x_1 = l_Lean_Elab_headerToImports___closed__2; +x_1 = l_Lean_Elab_headerToImports___closed__1; x_2 = 0; x_3 = lean_alloc_ctor(0, 1, 1); lean_ctor_set(x_3, 0, x_1); @@ -180,12 +165,12 @@ lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2); return x_3; } } -lean_object* _init_l_Lean_Elab_headerToImports___closed__4() { +lean_object* _init_l_Lean_Elab_headerToImports___closed__3() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(0); -x_2 = l_Lean_Elab_headerToImports___closed__3; +x_2 = l_Lean_Elab_headerToImports___closed__2; x_3 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_3, 0, x_2); lean_ctor_set(x_3, 1, x_1); @@ -231,7 +216,7 @@ lean_dec(x_16); x_18 = l_Array_toList___rarg(x_17); lean_dec(x_17); x_19 = l_List_map___main___at_Lean_Elab_headerToImports___spec__1(x_18); -x_20 = l_Lean_Elab_headerToImports___closed__4; +x_20 = l_Lean_Elab_headerToImports___closed__3; x_21 = l_List_append___rarg(x_20, x_19); return x_21; } @@ -1124,8 +1109,6 @@ l_Lean_Elab_headerToImports___closed__2 = _init_l_Lean_Elab_headerToImports___cl lean_mark_persistent(l_Lean_Elab_headerToImports___closed__2); l_Lean_Elab_headerToImports___closed__3 = _init_l_Lean_Elab_headerToImports___closed__3(); lean_mark_persistent(l_Lean_Elab_headerToImports___closed__3); -l_Lean_Elab_headerToImports___closed__4 = _init_l_Lean_Elab_headerToImports___closed__4(); -lean_mark_persistent(l_Lean_Elab_headerToImports___closed__4); l_Lean_Elab_parseImports___closed__1 = _init_l_Lean_Elab_parseImports___closed__1(); lean_mark_persistent(l_Lean_Elab_parseImports___closed__1); return lean_mk_io_result(lean_box(0)); diff --git a/stage0/stdlib/Init/Lean/Util/Path.c b/stage0/stdlib/Init/Lean/Util/Path.c index b59d05a7ea..9d473761b3 100644 --- a/stage0/stdlib/Init/Lean/Util/Path.c +++ b/stage0/stdlib/Init/Lean/Util/Path.c @@ -51,7 +51,6 @@ lean_object* l_IO_currentDir___at_Lean_moduleNameOfFileName___spec__1(lean_objec lean_object* lean_array_fget(lean_object*, lean_object*); lean_object* l_Lean_findAtSearchPath(lean_object*, lean_object*); lean_object* l_Array_iterateMAux___main___at_Lean_findAtSearchPath___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Name_append___main(lean_object*, lean_object*); lean_object* lean_io_current_dir(lean_object*); lean_object* l_Lean_getBuiltinSearchPath___closed__1; lean_object* l_Lean_addSearchPathFromEnv___closed__1; @@ -71,7 +70,6 @@ lean_object* l_Lean_findOLean___closed__2; lean_object* l_Lean_modPathToFilePath___boxed(lean_object*); lean_object* l_Lean_modPathToFilePath___main___boxed(lean_object*); lean_object* l_Lean_moduleNameOfFileName___closed__4; -lean_object* l_Lean_normalizeModuleName___closed__2; extern uint32_t l_System_FilePath_pathSeparator; uint32_t lean_string_utf8_get(lean_object*, lean_object*); lean_object* lean_module_name_of_file(lean_object*, lean_object*); @@ -93,7 +91,6 @@ lean_object* l_Lean_findOLean___closed__1; uint8_t l_UInt32_decEq(uint32_t, uint32_t); lean_object* l_String_intercalate(lean_object*, lean_object*); lean_object* l_List_map___main___at_Lean_findAtSearchPath___spec__3(lean_object*); -lean_object* l_Lean_normalizeModuleName___closed__1; uint8_t l_String_isPrefixOf(lean_object*, lean_object*); uint8_t lean_nat_dec_le(lean_object*, lean_object*); lean_object* l_AssocList_find_x3f___main___at_Lean_findOLean___spec__2___boxed(lean_object*, lean_object*); @@ -126,7 +123,6 @@ extern lean_object* l_HashMap_Inhabited___closed__1; lean_object* l_Lean_getBuiltinSearchPath___closed__3; extern lean_object* l_String_Inhabited; lean_object* l_Lean_splitAtRoot___main___closed__2; -lean_object* l_Lean_normalizeModuleName(lean_object*); size_t lean_string_hash(lean_object*); lean_object* l_IO_realPath___at_Lean_realPathNormalized___spec__1(lean_object*, lean_object*); lean_object* l_Array_iterateMAux___main___at_Lean_findAtSearchPath___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -1344,7 +1340,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; x_1 = l_Lean_modPathToFilePath___main___closed__1; -x_2 = lean_unsigned_to_nat(78u); +x_2 = lean_unsigned_to_nat(75u); x_3 = lean_unsigned_to_nat(33u); x_4 = l_Lean_modPathToFilePath___main___closed__2; x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4); @@ -1363,39 +1359,22 @@ return x_2; } case 1: { -lean_object* x_3; lean_object* x_4; lean_object* x_5; +lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; x_3 = lean_ctor_get(x_1, 0); x_4 = lean_ctor_get(x_1, 1); -if (lean_obj_tag(x_3) == 0) -{ -lean_inc(x_4); -return x_4; -} -else -{ -lean_object* x_11; -x_11 = lean_box(0); -x_5 = x_11; -goto block_10; -} -block_10: -{ -lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; -lean_dec(x_5); -x_6 = l_Lean_modPathToFilePath___main(x_3); -x_7 = l___private_Init_Lean_Util_Path_1__pathSep; -x_8 = lean_string_append(x_6, x_7); -x_9 = lean_string_append(x_8, x_4); -return x_9; -} +x_5 = l_Lean_modPathToFilePath___main(x_3); +x_6 = l___private_Init_Lean_Util_Path_1__pathSep; +x_7 = lean_string_append(x_5, x_6); +x_8 = lean_string_append(x_7, x_4); +return x_8; } default: { -lean_object* x_12; lean_object* x_13; lean_object* x_14; -x_12 = l_String_Inhabited; -x_13 = l_Lean_modPathToFilePath___main___closed__3; -x_14 = lean_panic_fn(x_12, x_13); -return x_14; +lean_object* x_9; lean_object* x_10; lean_object* x_11; +x_9 = l_String_Inhabited; +x_10 = l_Lean_modPathToFilePath___main___closed__3; +x_11 = lean_panic_fn(x_9, x_10); +return x_11; } } } @@ -1443,7 +1422,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; x_1 = l_Lean_modPathToFilePath___main___closed__1; -x_2 = lean_unsigned_to_nat(86u); +x_2 = lean_unsigned_to_nat(83u); x_3 = lean_unsigned_to_nat(20u); x_4 = l_Lean_modPathToFilePath___main___closed__2; x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4); @@ -1627,98 +1606,94 @@ return x_4; } else { -lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; +lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_dec(x_8); x_16 = lean_ctor_get(x_10, 0); lean_inc(x_16); lean_dec(x_10); -x_17 = l___private_Init_Lean_Util_Path_1__pathSep; -x_18 = lean_string_append(x_16, x_17); -x_19 = l_Lean_modPathToFilePath___main(x_9); +x_17 = l_Lean_modPathToFilePath___main(x_9); lean_dec(x_9); +x_18 = lean_string_append(x_16, x_17); +lean_dec(x_17); +x_19 = l_Lean_findOLean___closed__2; x_20 = lean_string_append(x_18, x_19); -lean_dec(x_19); -x_21 = l_Lean_findOLean___closed__2; -x_22 = lean_string_append(x_20, x_21); -lean_ctor_set(x_4, 0, x_22); +lean_ctor_set(x_4, 0, x_20); return x_4; } } else { -lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; -x_23 = lean_ctor_get(x_4, 0); -x_24 = lean_ctor_get(x_4, 1); +lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; +x_21 = lean_ctor_get(x_4, 0); +x_22 = lean_ctor_get(x_4, 1); +lean_inc(x_22); +lean_inc(x_21); +lean_dec(x_4); +x_23 = l_Lean_splitAtRoot___main(x_1); +x_24 = lean_ctor_get(x_23, 0); lean_inc(x_24); -lean_inc(x_23); -lean_dec(x_4); -x_25 = l_Lean_splitAtRoot___main(x_1); -x_26 = lean_ctor_get(x_25, 0); -lean_inc(x_26); -x_27 = lean_ctor_get(x_25, 1); -lean_inc(x_27); -lean_dec(x_25); -x_28 = l_HashMapImp_find_x3f___at_Lean_findOLean___spec__1(x_23, x_26); +x_25 = lean_ctor_get(x_23, 1); +lean_inc(x_25); lean_dec(x_23); -if (lean_obj_tag(x_28) == 0) +x_26 = l_HashMapImp_find_x3f___at_Lean_findOLean___spec__1(x_21, x_24); +lean_dec(x_21); +if (lean_obj_tag(x_26) == 0) { -lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; -lean_dec(x_27); -x_29 = l_Lean_findOLean___closed__1; -x_30 = lean_string_append(x_29, x_26); -lean_dec(x_26); -x_31 = l_Char_HasRepr___closed__1; -x_32 = lean_string_append(x_30, x_31); -x_33 = lean_alloc_ctor(18, 1, 0); -lean_ctor_set(x_33, 0, x_32); -x_34 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_34, 0, x_33); -lean_ctor_set(x_34, 1, x_24); -return x_34; +lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; +lean_dec(x_25); +x_27 = l_Lean_findOLean___closed__1; +x_28 = lean_string_append(x_27, x_24); +lean_dec(x_24); +x_29 = l_Char_HasRepr___closed__1; +x_30 = lean_string_append(x_28, x_29); +x_31 = lean_alloc_ctor(18, 1, 0); +lean_ctor_set(x_31, 0, x_30); +x_32 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_32, 0, x_31); +lean_ctor_set(x_32, 1, x_22); +return x_32; } else { -lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; +lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; +lean_dec(x_24); +x_33 = lean_ctor_get(x_26, 0); +lean_inc(x_33); lean_dec(x_26); -x_35 = lean_ctor_get(x_28, 0); -lean_inc(x_35); -lean_dec(x_28); -x_36 = l___private_Init_Lean_Util_Path_1__pathSep; +x_34 = l_Lean_modPathToFilePath___main(x_25); +lean_dec(x_25); +x_35 = lean_string_append(x_33, x_34); +lean_dec(x_34); +x_36 = l_Lean_findOLean___closed__2; x_37 = lean_string_append(x_35, x_36); -x_38 = l_Lean_modPathToFilePath___main(x_27); -lean_dec(x_27); -x_39 = lean_string_append(x_37, x_38); -lean_dec(x_38); -x_40 = l_Lean_findOLean___closed__2; -x_41 = lean_string_append(x_39, x_40); -x_42 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_42, 0, x_41); -lean_ctor_set(x_42, 1, x_24); -return x_42; +x_38 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_38, 0, x_37); +lean_ctor_set(x_38, 1, x_22); +return x_38; } } } else { -uint8_t x_43; +uint8_t x_39; lean_dec(x_1); -x_43 = !lean_is_exclusive(x_4); -if (x_43 == 0) +x_39 = !lean_is_exclusive(x_4); +if (x_39 == 0) { return x_4; } else { -lean_object* x_44; lean_object* x_45; lean_object* x_46; -x_44 = lean_ctor_get(x_4, 0); -x_45 = lean_ctor_get(x_4, 1); -lean_inc(x_45); -lean_inc(x_44); +lean_object* x_40; lean_object* x_41; lean_object* x_42; +x_40 = lean_ctor_get(x_4, 0); +x_41 = lean_ctor_get(x_4, 1); +lean_inc(x_41); +lean_inc(x_40); lean_dec(x_4); -x_46 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_46, 0, x_44); -lean_ctor_set(x_46, 1, x_45); -return x_46; +x_42 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_42, 0, x_40); +lean_ctor_set(x_42, 1, x_41); +return x_42; } } } @@ -2591,57 +2566,6 @@ return x_93; } } } -lean_object* _init_l_Lean_normalizeModuleName___closed__1() { -_start: -{ -lean_object* x_1; -x_1 = lean_mk_string("Default"); -return x_1; -} -} -lean_object* _init_l_Lean_normalizeModuleName___closed__2() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_normalizeModuleName___closed__1; -x_3 = lean_name_mk_string(x_1, x_2); -return x_3; -} -} -lean_object* l_Lean_normalizeModuleName(lean_object* x_1) { -_start: -{ -if (lean_obj_tag(x_1) == 1) -{ -lean_object* x_2; -x_2 = lean_ctor_get(x_1, 0); -lean_inc(x_2); -if (lean_obj_tag(x_2) == 0) -{ -lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; -x_3 = lean_ctor_get(x_1, 1); -lean_inc(x_3); -lean_dec(x_1); -x_4 = lean_box(0); -x_5 = lean_name_mk_string(x_4, x_3); -x_6 = l_Lean_normalizeModuleName___closed__2; -x_7 = l_Lean_Name_append___main(x_5, x_6); -lean_dec(x_5); -return x_7; -} -else -{ -lean_dec(x_2); -return x_1; -} -} -else -{ -return x_1; -} -} -} lean_object* initialize_Init_System_IO(lean_object*); lean_object* initialize_Init_System_FilePath(lean_object*); lean_object* initialize_Init_Data_Array(lean_object*); @@ -2730,10 +2654,6 @@ l_Lean_moduleNameOfFileName___closed__3 = _init_l_Lean_moduleNameOfFileName___cl lean_mark_persistent(l_Lean_moduleNameOfFileName___closed__3); l_Lean_moduleNameOfFileName___closed__4 = _init_l_Lean_moduleNameOfFileName___closed__4(); lean_mark_persistent(l_Lean_moduleNameOfFileName___closed__4); -l_Lean_normalizeModuleName___closed__1 = _init_l_Lean_normalizeModuleName___closed__1(); -lean_mark_persistent(l_Lean_normalizeModuleName___closed__1); -l_Lean_normalizeModuleName___closed__2 = _init_l_Lean_normalizeModuleName___closed__2(); -lean_mark_persistent(l_Lean_normalizeModuleName___closed__2); return lean_mk_io_result(lean_box(0)); } #ifdef __cplusplus