diff --git a/stage0/src/CMakeLists.txt b/stage0/src/CMakeLists.txt index ba360fd6b3..560245e850 100644 --- a/stage0/src/CMakeLists.txt +++ b/stage0/src/CMakeLists.txt @@ -489,7 +489,7 @@ configure_file("${LEAN_SOURCE_DIR}/version.h.in" "${LEAN_BINARY_DIR}/version.h") configure_file("${LEAN_SOURCE_DIR}/config.h.in" "${LEAN_SOURCE_DIR}/config.h") install(FILES "${LEAN_SOURCE_DIR}/config.h" DESTINATION "${INCLUDE_DIR}") if(NOT STAGE0) - configure_file("${LEAN_SOURCE_DIR}/Init/Makefile.in" "${LEAN_SOURCE_DIR}/Init/Makefile") + configure_file("${LEAN_SOURCE_DIR}/Makefile.in" "${LEAN_SOURCE_DIR}/Makefile") endif() include_directories("${LEAN_BINARY_DIR}") @@ -618,7 +618,7 @@ add_test(NAME style_check COMMAND "${PYTHON_EXECUTABLE}" "${LEAN_SOURCE_DIR}/cma endif() add_custom_target(clean-stdlib - WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/Init" + WORKING_DIRECTORY "${LEAN_SOURCE_DIR}" COMMAND find . -name '*.olean' -delete COMMAND find . -name '*.depend' -delete COMMAND rm -rf ../stage1 "${CMAKE_BINARY_DIR}/stage2" "${CMAKE_BINARY_DIR}/stage3" || true @@ -627,7 +627,7 @@ add_custom_target(clean-stdlib add_custom_target(clean-olean DEPENDS clean-stdlib) -install(DIRECTORY "${CMAKE_SOURCE_DIR}/Init" DESTINATION "${LIBRARY_DIR}" +install(DIRECTORY "${CMAKE_SOURCE_DIR}" DESTINATION "${LIBRARY_DIR}" FILES_MATCHING PATTERN "*.lean" PATTERN "*.olean" diff --git a/stage0/src/Init/Lean/Parser/Command.lean b/stage0/src/Init/Lean/Parser/Command.lean index 694cba02d7..aa04e19670 100644 --- a/stage0/src/Init/Lean/Parser/Command.lean +++ b/stage0/src/Init/Lean/Parser/Command.lean @@ -54,9 +54,7 @@ def «constant» := parser! "constant " >> declId >> declSig >> optional d def «instance» := parser! "instance " >> optional declId >> declSig >> declVal def «axiom» := parser! "axiom " >> declId >> declSig def «example» := parser! "example " >> declSig >> declVal -def relaxedInferMod := parser! try ("{" >> "}") -def strictInferMod := parser! try ("(" >> ")") -def inferMod := relaxedInferMod <|> strictInferMod +def inferMod := parser! try ("{" >> "}") def introRule := parser! " | " >> ident >> optional inferMod >> optDeclSig def «inductive» := parser! "inductive " >> declId >> optDeclSig >> many introRule def classInductive := parser! try ("class " >> "inductive ") >> declId >> optDeclSig >> many introRule diff --git a/stage0/src/Init/Lean/PrettyPrinter/Parenthesizer.lean b/stage0/src/Init/Lean/PrettyPrinter/Parenthesizer.lean index b899b4df89..f827d3812f 100644 --- a/stage0/src/Init/Lean/PrettyPrinter/Parenthesizer.lean +++ b/stage0/src/Init/Lean/PrettyPrinter/Parenthesizer.lean @@ -30,12 +30,12 @@ produced by `p rbp` if Note that in case 2, it is also sufficient to parenthesize a *parent* node as long as the offending token is still to the right of that node. For example, imagine the tree structure of `(f $ fun x => x) y` without parentheses. We need to -insert *some* parentheses between `x` and `y` since the lambda body is parse with precedence 0, while `y` as an +insert *some* parentheses between `x` and `y` since the lambda body is parsed with precedence 0, while `y` as an identifier has precedence `appPrec`. But we need to parenthesize the `$` node anyway since the precedence of its RHS (0) again is smaller than that of `y`. So it's better to only parenthesize the outer node than ending up with `(f $ (fun x => x)) y`. -Unfortunately, we cannot determine the precedence of a token just by looking at the syntax tree because it can actually +Unfortunately, we cannot determine the precedence of a token just by looking at the token table because it can actually have different precedences in different contexts (e.g. because of whitespace sensitivity). Thus we need to look at the parser that produced the token as well. diff --git a/stage0/src/Init/Lean/Util/Path.lean b/stage0/src/Init/Lean/Util/Path.lean index d032ba6fea..5e132a4bf7 100644 --- a/stage0/src/Init/Lean/Util/Path.lean +++ b/stage0/src/Init/Lean/Util/Path.lean @@ -110,23 +110,24 @@ match results with | [] => pure none | _ => throw (IO.userError ("file '" ++ fname ++ "' is contained in multiple packages: " ++ ", ".intercalate (results.map Prod.fst))) +/-- Infer module name of source file name, assuming that `lean` is called from the package source root. -/ @[export lean_module_name_of_file] -def moduleNameOfFileName (fname : String) : IO (Option Name) := do -some (pkg, path) ← findAtSearchPath fname - | pure none; +def moduleNameOfFileName (fname : String) : IO Name := do fname ← realPathNormalized fname; -let fnameSuffix := fname.drop path.length; +root ← IO.currentDir >>= realPathNormalized; +when (!root.isPrefixOf fname) $ + throw $ IO.userError $ "input file '" ++ fname ++ "' must be contained in current directory (" ++ root ++ ")"; +let fnameSuffix := fname.drop root.length; let fnameSuffix := if fnameSuffix.get 0 == pathSeparator then fnameSuffix.drop 1 else fnameSuffix; some extPos ← pure (fnameSuffix.revPosOf '.') - | throw (IO.userError ("failed to convert file '" ++ fname ++ "' to module name, extension is missing")); + | throw (IO.userError ("failed to convert file name '" ++ fname ++ "' to module name, extension is missing")); let modNameStr := fnameSuffix.extract 0 extPos; let extStr := fnameSuffix.extract (extPos + 1) fnameSuffix.bsize; let parts := modNameStr.splitOn pathSep; -let modName := parts.foldl mkNameStr pkg; +let modName := parts.foldl mkNameStr Name.anonymous; pure modName -- normalize `A` to `A.Default` -@[export lean_normalize_module_name] def normalizeModuleName : Name → Name | Name.str Name.anonymous pkg _ => mkNameSimple pkg ++ "Default" | m => m diff --git a/stage0/src/Init/System/IO.lean b/stage0/src/Init/System/IO.lean index f52d4e3dc9..497ca064d2 100644 --- a/stage0/src/Init/System/IO.lean +++ b/stage0/src/Init/System/IO.lean @@ -139,6 +139,8 @@ constant isDir (fname : @& String) : IO Bool := arbitrary _ constant fileExists (fname : @& String) : IO Bool := arbitrary _ @[extern "lean_io_app_dir"] constant appPath : IO String := arbitrary _ +@[extern "lean_io_current_dir"] +constant currentDir : IO String := arbitrary _ @[inline] def liftIO {m : Type → Type} {α : Type} [MonadIO m] (x : IO α) : m α := monadLift x @@ -157,6 +159,7 @@ def realPath : String → m String := Prim.liftIO ∘ Prim.realPath def isDir : String → m Bool := Prim.liftIO ∘ Prim.isDir def fileExists : String → m Bool := Prim.liftIO ∘ Prim.fileExists def appPath : m String := Prim.liftIO Prim.appPath +def currentDir : m String := Prim.liftIO Prim.currentDir def appDir : m String := do p ← appPath; diff --git a/stage0/src/Init/Makefile.in b/stage0/src/Makefile.in similarity index 84% rename from stage0/src/Init/Makefile.in rename to stage0/src/Makefile.in index 8cdd95940a..fbc658b217 100644 --- a/stage0/src/Init/Makefile.in +++ b/stage0/src/Makefile.in @@ -1,8 +1,8 @@ # Copyright (c) 2018 Simon Hudon. All rights reserved. # Released under Apache 2.0 license as described in the file LICENSE. # Authors: Simon Hudon, Sebastian Ullrich, Leonardo de Moura -LEAN ?= ../../bin/lean -LEANC ?= ../../bin/leanc +LEAN ?= ../bin/lean +LEANC ?= ../bin/leanc LEAN_ROOT ?= . # Even though we copy the sources into a new directory for stage2/3, we # read the list of files to compile from the original directory to avoid @@ -10,14 +10,14 @@ LEAN_ROOT ?= . SRCS = $(shell cd $(LEAN_ROOT); find . -name '*.lean') DEPS = $(addprefix $(LEAN_ROOT)/,$(SRCS:.lean=.depend)) OPTS = @LEAN_EXTRA_MAKE_OPTS@ -STAGE0_DIR = ../../stage0 +STAGE0_DIR = ../stage0 C_OUT ?= . ifndef OUT $(error "`OUT` must be set (use cmake)") endif OBJS = $(SRCS:.lean=.olean) # ensure deterministic ordering -CS_CORE=$(addprefix Init/,$(sort $(SRCS:.lean=.c))) +CS_CORE=$(sort $(SRCS:.lean=.c)) SHELL = /usr/bin/env bash -eo pipefail @@ -55,10 +55,10 @@ $(OUT)/libleanstdlib.a: $(addprefix $(OUT)/,$(SRCS:.lean=.o)) update-stage0: -rm -r $(STAGE0_DIR) -mkdir -p $(STAGE0_DIR)/stdlib - for f in $(SRCS:.lean=.c); do mkdir -p `dirname $(STAGE0_DIR)/stdlib/Init/$$f`; cp $(C_OUT)/$$f $(STAGE0_DIR)/stdlib/Init/$$f; done + for f in $(SRCS:.lean=.c); do mkdir -p `dirname $(STAGE0_DIR)/stdlib/$$f`; cp $(C_OUT)/$$f $(STAGE0_DIR)/stdlib/$$f; done echo "add_library (stage0 OBJECT $(CS_CORE))" > $(STAGE0_DIR)/stdlib/CMakeLists.txt # don't copy untracked crap - cd ..; git ls-files -z . | xargs -0 -I '{}' bash -c 'mkdir -p `dirname ../stage0/src/{}` && cp {} ../stage0/src/{}' + git ls-files -z . | xargs -0 -I '{}' bash -c 'mkdir -p `dirname ../stage0/src/{}` && cp {} ../stage0/src/{}' -git add $(STAGE0_DIR) .PRECIOUS: %.depend $(C_OUT)/%.c diff --git a/stage0/src/frontends/lean/parser.cpp b/stage0/src/frontends/lean/parser.cpp index 02a40f7e55..b7e58b6061 100644 --- a/stage0/src/frontends/lean/parser.cpp +++ b/stage0/src/frontends/lean/parser.cpp @@ -2158,12 +2158,6 @@ void parser::parse_new_frontend_cmd() { #endif -extern "C" object* lean_normalize_module_name(object* m); - -name normalize_module_name(name m) { - return name(lean_normalize_module_name(m.to_obj_arg())); -} - void parser::process_imports() { // we assume the Lean parser has already imported the modules into `m_env` diff --git a/stage0/src/Init/relative.py b/stage0/src/relative.py similarity index 100% rename from stage0/src/Init/relative.py rename to stage0/src/relative.py diff --git a/stage0/src/runtime/io.cpp b/stage0/src/runtime/io.cpp index 8a25a4e425..1afebd2fe2 100644 --- a/stage0/src/runtime/io.cpp +++ b/stage0/src/runtime/io.cpp @@ -477,6 +477,16 @@ extern "C" obj_res lean_io_app_dir(obj_arg) { #endif } +extern "C" obj_res lean_io_current_dir(obj_arg) { + char buffer[PATH_MAX]; + char * cwd = getcwd(buffer, sizeof(buffer)); + if (cwd) { + return set_io_result(mk_string(cwd)); + } else { + return set_io_error("failed to retrieve current working directory"); + } +} + // ======================================= // IO ref primitives extern "C" obj_res lean_io_mk_ref(obj_arg a, obj_arg) { diff --git a/stage0/src/shell/CMakeLists.txt b/stage0/src/shell/CMakeLists.txt index 4cbd9b5536..22f3b1a21a 100644 --- a/stage0/src/shell/CMakeLists.txt +++ b/stage0/src/shell/CMakeLists.txt @@ -11,16 +11,16 @@ if(NOT STAGE0) set(LEANC_OPTS "${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}}") add_custom_target(make_stdlib - WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/Init" - COMMAND ${CMAKE_COMMAND} -E env "LEAN_PATH=Init=." $(MAKE) "${CMAKE_BINARY_DIR}/stage1/Init/libleanstdlib.a" + WORKING_DIRECTORY "${LEAN_SOURCE_DIR}" + COMMAND ${CMAKE_COMMAND} -E env "LEAN_PATH=Init=Init" $(MAKE) "${CMAKE_BINARY_DIR}/stage1/libleanstdlib.a" "LEAN=$" "LEANC_OPTS=${LEANC_OPTS}" - "OUT=${CMAKE_BINARY_DIR}/stage1/Init" + "OUT=${CMAKE_BINARY_DIR}/stage1" # share .c files between different build configurations - "C_OUT=${LEAN_SOURCE_DIR}/stage1/Init" + "C_OUT=${LEAN_SOURCE_DIR}/stage1" DEPENDS stage0) set_target_properties(leanstdlib PROPERTIES - IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/stage1/Init/libleanstdlib.a" + IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/stage1/libleanstdlib.a" IMPORTED_LINK_INTERFACE_LIBRARIES leanstatic) add_dependencies(leanstdlib make_stdlib) install(FILES "$" DESTINATION lib) @@ -28,11 +28,11 @@ if(NOT STAGE0) set(PREV_LEAN "$") foreach(STAGE RANGE 2 3) add_custom_target(make_stdlib_stage${STAGE} - COMMAND cd "${LEAN_SOURCE_DIR}/Init" && find . '\(' -name Makefile -o -name relative.py -o -name '*.lean' '\)' -exec "${CMAKE_COMMAND}" -E copy_if_different '{}' ${CMAKE_BINARY_DIR}/stage${STAGE}/Init/'{}' '\;' - COMMAND cd "${CMAKE_BINARY_DIR}/stage${STAGE}/Init" && LEAN_PATH=Init=. $(MAKE) ./libleanstdlib.a + COMMAND cd "${LEAN_SOURCE_DIR}" && find . '\(' -name Makefile -o -name relative.py -o -name '*.lean' '\)' -exec "${CMAKE_COMMAND}" -E copy_if_different '{}' ${CMAKE_BINARY_DIR}/stage${STAGE}/'{}' '\;' + COMMAND cd "${CMAKE_BINARY_DIR}/stage${STAGE}" && LEAN_PATH=Init=Init $(MAKE) ./libleanstdlib.a "LEAN=${PREV_LEAN}" "LEANC=${LEAN_SOURCE_DIR}/../bin/leanc" - "LEAN_ROOT=${LEAN_SOURCE_DIR}/Init" + "LEAN_ROOT=${LEAN_SOURCE_DIR}" "LEANC_OPTS=${LEANC_OPTS}" "OUT=." # recreate everything if the previous compiler has changed @@ -40,7 +40,7 @@ if(NOT STAGE0) ) add_library(leanstdlib_stage${STAGE} STATIC IMPORTED) set_target_properties(leanstdlib_stage${STAGE} PROPERTIES - IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/stage${STAGE}/Init/libleanstdlib.a" + IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/stage${STAGE}/libleanstdlib.a" IMPORTED_LINK_INTERFACE_LIBRARIES leanstatic) add_dependencies(leanstdlib_stage${STAGE} make_stdlib_stage${STAGE}) add_executable(lean_stage${STAGE} EXCLUDE_FROM_ALL lean.cpp) @@ -54,10 +54,10 @@ if(NOT STAGE0) add_custom_target(update-stage0 COMMAND make update-stage0 - "OUT=${CMAKE_BINARY_DIR}/stage1/Init" - "C_OUT=${LEAN_SOURCE_DIR}/stage1/Init" + "OUT=${CMAKE_BINARY_DIR}/stage1" + "C_OUT=${LEAN_SOURCE_DIR}/stage1" DEPENDS leanstdlib - WORKING_DIRECTORY "${CMAKE_SOURCE_DIR}/Init") + WORKING_DIRECTORY "${CMAKE_SOURCE_DIR}") endif() add_executable(lean lean.cpp) @@ -143,15 +143,6 @@ add_test(lean_ghash2 "${CMAKE_CURRENT_BINARY_DIR}/lean" --githash) # add_test(lean_new_frontend "${LEAN_SOURCE_DIR}/../bin/lean" --new-frontend "${LEAN_SOURCE_DIR}/Init/Core.lean") add_test(lean_unknown_option bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "-z") add_test(lean_unknown_file1 bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "boofoo.lean") -if (NOT(${CMAKE_SYSTEM_NAME} MATCHES "Windows")) - # The following test cannot be executed on Windows because of the - # bash script timeout.sh - - # We need to cache failures at type_context to be able to process the following test in a reasonable amount of time - # add_test(NAME "normalizer_perf" - # WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra" - # COMMAND bash "./timeout.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "1" "slow1.lean") -endif() # LEAN TESTS file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean") @@ -160,7 +151,7 @@ FOREACH(T ${LEANTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leantest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean" - COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME}) + COMMAND bash -c "PATH=${LEAN_SOURCE_DIR}/../bin:$PATH ./test_single.sh ${T_NAME}") endif() ENDFOREACH(T) @@ -171,7 +162,7 @@ FOREACH(T ${LEANRUNTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leanruntest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/run" - COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME}) + COMMAND bash -c "PATH=${LEAN_SOURCE_DIR}/../bin:$PATH ./test_single.sh ${T_NAME}") endif() ENDFOREACH(T) @@ -182,32 +173,17 @@ FOREACH(T ${LEANNEWFRONTENDTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leannewfrontendtest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/newfrontend" - COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME}) + COMMAND bash -c "PATH=${LEAN_SOURCE_DIR}/../bin:$PATH ./test_single.sh ${T_NAME}") endif() ENDFOREACH(T) -# LEAN FAIL TESTS -file(GLOB LEANFAILTESTS "${LEAN_SOURCE_DIR}/../tests/lean/fail/*.lean") -FOREACH(T ${LEANFAILTESTS}) - if(NOT T MATCHES "\\.#") - GET_FILENAME_COMPONENT(T_NAME ${T} NAME) - # test twice, once with runner, and once without - add_test(NAME "leanfailtest_${T_NAME}" - WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/fail" - COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME}) - add_test(NAME "leanfailtest2_${T_NAME}" - WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/fail" - COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME}) - endif() -ENDFOREACH(T) - # LEAN COMPILER TESTS file(GLOB LEANCOMPTESTS "${LEAN_SOURCE_DIR}/../tests/compiler/*.lean") FOREACH(T ${LEANCOMPTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leancomptest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/compiler" - COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME}) + COMMAND bash -c "PATH=${LEAN_SOURCE_DIR}/../bin:$PATH ./test_single.sh ${T_NAME}") ENDFOREACH(T) # LEAN INTERPRETER TESTS @@ -217,7 +193,7 @@ FOREACH(T ${LEANINTERPTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leaninterptest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/compiler" - COMMAND bash "./test_single_interpret.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME}) + COMMAND bash -c "PATH=${LEAN_SOURCE_DIR}/../bin:$PATH ./test_single_interpret.sh ${T_NAME}") endif() ENDFOREACH(T) @@ -229,7 +205,7 @@ FOREACH(T_OUT ${LEANBENCHTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leanbenchtest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/bench" - COMMAND bash "./test_single.sh" ${T_NAME}) + COMMAND bash -c "PATH=${LEAN_SOURCE_DIR}/../bin:$PATH ./test_single.sh ${T_NAME}") ENDFOREACH(T_OUT) # LEAN PLUGIN TESTS @@ -238,7 +214,7 @@ FOREACH(T ${LEANINTERPTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leanplugintest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/plugin" - COMMAND bash "./test_single.sh" ${T_NAME}) + COMMAND bash -c "PATH=${LEAN_SOURCE_DIR}/../bin:$PATH ./test_single.sh ${T_NAME}") ENDFOREACH(T) # LEAN TESTS using --trust=0 @@ -247,56 +223,5 @@ FOREACH(T ${LEANT0TESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leant0test_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/trust0" - COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME} "-t 0") + COMMAND bash -c "PATH=${LEAN_SOURCE_DIR}/../bin:$PATH ./test_single.sh ${T_NAME}") ENDFOREACH(T) - -# LEAN TESTS using --trust=10 -file(GLOB LEANT0TESTS "${LEAN_SOURCE_DIR}/../tests/lean/trust10/*.lean") -FOREACH(T ${LEANT0TESTS}) - GET_FILENAME_COMPONENT(T_NAME ${T} NAME) - add_test(NAME "leant10test_${T_NAME}" - WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/trust10" - COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME} "-t 10") -ENDFOREACH(T) - -if("${MULTI_THREAD}" MATCHES "ON") -# LEAN INTERACTIVE TESTS -file(GLOB LEANITTESTS "${LEAN_SOURCE_DIR}/../tests/lean/interactive/*.input" "${LEAN_SOURCE_DIR}/../tests/lean/interactive/*.lean") -FOREACH(T ${LEANITTESTS}) - GET_FILENAME_COMPONENT(T_NAME ${T} NAME) - add_test(NAME "leanittest_${T_NAME}" - WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/interactive" - COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME}) -ENDFOREACH(T) -endif() - -# LEAN SLOW TESTS -file(GLOB LEANSLOWTESTS "${LEAN_SOURCE_DIR}/../tests/lean/slow/*.lean") -FOREACH(T ${LEANSLOWTESTS}) - GET_FILENAME_COMPONENT(T_NAME ${T} NAME) - add_test(NAME "leanslowtest_${T_NAME}" - WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/slow" - COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME}) - set_tests_properties("leanslowtest_${T_NAME}" PROPERTIES LABELS "expensive") -ENDFOREACH(T) - -# file(GLOB LEANNATIVETESTS "${LEAN_SOURCE_DIR}/../tests/lean/native_run/*.lean") -# FOREACH(T ${LEANNATIVETESTS}) -# GET_FILENAME_COMPONENT(T_NAME ${T} NAME) -# add_test(NAME "leannativetest_${T_NAME}" -# WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/native_run" -# COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME}) -# ENDFOREACH(T) - - -# # Create the script lean.sh -# # This is used to create a soft dependency on the Lean executable -# # Some rules can only be applied if the lean executable exists, -# # but we don't want a dependency on the executable because -# # the rules would be applied whenever the executable is rebuilt. -# # These are the rules for automatically generating .olean files and -# # C++/Lean interface files. -# add_custom_command(OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/lean.sh -# COMMAND ${CMAKE_CURRENT_SOURCE_DIR}/mk_lean_sh.sh ${CMAKE_CURRENT_BINARY_DIR} -# DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/lean) -# add_custom_target(lean_sh DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/lean.sh) diff --git a/stage0/src/shell/lean.cpp b/stage0/src/shell/lean.cpp index b03968807c..c5b763b012 100644 --- a/stage0/src/shell/lean.cpp +++ b/stage0/src/shell/lean.cpp @@ -194,8 +194,7 @@ static void display_help(std::ostream & out) { std::cout << " --githash display the git commit hash number used to build this binary\n"; std::cout << " --run executes the 'main' definition\n"; std::cout << " --make create olean file\n"; - std::cout << " --cpp=fname -c name of the C++ output file\n"; // TODO(Leo): delete - std::cout << " --c=fname -C name of the C output file\n"; + std::cout << " --c=fname -c name of the C output file\n"; std::cout << " --stdin take input from stdin\n"; std::cout << " --trust=num -t trust level (default: max) 0 means do not trust any macro,\n" << " and type check all imported modules\n"; @@ -239,8 +238,7 @@ static struct option g_long_options[] = { {"quiet", no_argument, 0, 'q'}, {"deps", no_argument, 0, 'd'}, {"timeout", optional_argument, 0, 'T'}, - {"cpp", optional_argument, 0, 'c'}, - {"c", optional_argument, 0, 'C'}, + {"c", optional_argument, 0, 'c'}, {"exitOnPanic", no_argument, 0, 'e'}, #if defined(LEAN_JSON) {"json", no_argument, 0, 'J'}, @@ -304,7 +302,7 @@ void load_plugin(std::string path) { // we never want to look up plugins using the system library search path = lrealpath(path); std::string pkg = stem(path); - std::string sym = "initialize_" + pkg + "_Default"; + std::string sym = "initialize_" + pkg; #ifdef LEAN_WINDOWS HMODULE h = LoadLibrary(path.c_str()); if (!h) { @@ -354,8 +352,13 @@ void init_search_path() { } extern "C" object* lean_module_name_of_file(object* fname, object* w); -optional module_name_of_file(std::string const & fname) { - return get_io_result>(lean_module_name_of_file(mk_string(fname), io_mk_world())).get(); +optional module_name_of_file(std::string const & fname, bool optional) { + object * o = lean_module_name_of_file(mk_string(fname), io_mk_world()); + if (io_result_is_error(o) && optional) { + return lean::optional(); + } else { + return some(get_io_result(o)); + } } /* def parseImports (input : String) (fileName : Option String := none) : IO (Array Import × Position × MessageLog) */ @@ -469,10 +472,6 @@ int main(int argc, char ** argv) { check_optarg("c"); c_output = optarg; break; - case 'C': - check_optarg("C"); - c_output = optarg; - break; case 's': lean::lthread::set_thread_stack_size( static_cast((atoi(optarg) / 4) * 4) * static_cast(1024)); @@ -595,9 +594,9 @@ int main(int argc, char ** argv) { display_help(std::cerr); return 1; } - mod_fn = lrealpath(argv[optind++]); + mod_fn = argv[optind++]; contents = read_file(mod_fn); - main_module_name = module_name_of_file(mod_fn); + main_module_name = module_name_of_file(mod_fn, /* optional */ !c_output); } bool ok = true; @@ -682,10 +681,6 @@ int main(int argc, char ** argv) { } if (c_output && ok) { - if (!main_module_name) { - std::cerr << "cannot extract code, module name of input file is not known\n"; - return 1; - } std::ofstream out(*c_output); if (out.fail()) { std::cerr << "failed to create '" << *c_output << "'\n"; diff --git a/stage0/stdlib/CMakeLists.txt b/stage0/stdlib/CMakeLists.txt index 519877d7f7..677dcc73bc 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/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) diff --git a/stage0/stdlib/Init/Lean/Elab/Import.c b/stage0/stdlib/Init/Lean/Elab/Import.c index 9662cb08b7..9d733a7a49 100644 --- a/stage0/stdlib/Init/Lean/Elab/Import.c +++ b/stage0/stdlib/Init/Lean/Elab/Import.c @@ -52,7 +52,7 @@ lean_object* l_List_forM___main___at_Lean_Elab_printDeps___spec__1(lean_object*, lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*); lean_object* l_Lean_Syntax_asNode(lean_object*); extern lean_object* l_Lean_getBuiltinSearchPath___closed__3; -lean_object* lean_normalize_module_name(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: { @@ -78,7 +78,7 @@ 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 = lean_normalize_module_name(x_10); +x_11 = l_Lean_normalizeModuleName(x_10); x_12 = l_List_map___main___at_Lean_Elab_headerToImports___spec__1(x_5); if (x_8 == 0) { @@ -118,7 +118,7 @@ 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 = lean_normalize_module_name(x_23); +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) { diff --git a/stage0/stdlib/Init/Lean/Parser/Command.c b/stage0/stdlib/Init/Lean/Parser/Command.c index 7cff417ef7..12d78e48ba 100644 --- a/stage0/stdlib/Init/Lean/Parser/Command.c +++ b/stage0/stdlib/Init/Lean/Parser/Command.c @@ -30,7 +30,6 @@ lean_object* l_Lean_Parser_Command_structImplicitBinder___closed__8; lean_object* l_Lean_Parser_Command_structureTk___closed__2; lean_object* l_Lean_Parser_Command_instance___closed__2; extern lean_object* l_Lean_Parser_manyAux___main___closed__1; -lean_object* l_Lean_Parser_Command_strictInferMod; lean_object* l_Lean_Parser_Command_declModifiers___elambda__1___closed__3; lean_object* l_Lean_Parser_Command_resolve__name___elambda__1___closed__8; lean_object* l_Lean_Parser_Command_extends___elambda__1___closed__3; @@ -215,6 +214,7 @@ lean_object* l_Lean_Parser_Command_visibility___closed__2; lean_object* l_Lean_Parser_Command_classInductive___elambda__1___closed__3; lean_object* l_Lean_Parser_Command_declId___closed__4; lean_object* l_Lean_Parser_Command_end; +lean_object* l_Lean_Parser_Command_inferMod___elambda__1___closed__3; lean_object* l_Lean_Parser_Command_def___elambda__1___closed__5; lean_object* l_Lean_Parser_Command_openHiding___closed__7; lean_object* l_Lean_Parser_Command_instance___elambda__1___closed__3; @@ -230,7 +230,6 @@ lean_object* lean_array_get_size(lean_object*); lean_object* l_Lean_Parser_Command_structFields; lean_object* l_Lean_Parser_Command_abbrev___closed__3; lean_object* l_Lean_Parser_Command_declId___closed__9; -lean_object* l_Lean_Parser_Command_strictInferMod___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Command_declId___closed__8; lean_object* lean_string_append(lean_object*, lean_object*); lean_object* l_Lean_Parser_Command_declValEqns___elambda__1___closed__2; @@ -259,6 +258,7 @@ lean_object* l_Lean_Parser_Command_openRenamingItem___elambda__1___closed__1; lean_object* l_Lean_Parser_Command_instance; lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Command_openRenaming___elambda__1___spec__2(uint8_t, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*); lean_object* l_Lean_Parser_Command_instance___closed__8; +lean_object* l_Lean_Parser_Command_inferMod___closed__4; lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Command_openRenaming___elambda__1___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Command_openOnly___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Command_structFields___elambda__1(lean_object*, lean_object*); @@ -271,7 +271,6 @@ lean_object* l_Lean_Parser_Command_instance___elambda__1(lean_object*, lean_obje lean_object* l_Lean_Parser_Command_docComment___closed__2; lean_object* l_Lean_Parser_regBuiltinCommandParserAttr___closed__2; lean_object* l_Lean_Parser_Command_constant___closed__1; -lean_object* l_Lean_Parser_Command_strictInferMod___closed__1; lean_object* l_Lean_Parser_Command_structFields___elambda__1___closed__1; extern lean_object* l_Lean_mkAppStx___closed__4; lean_object* l_Lean_Parser_ParserState_mkErrorsAt(lean_object*, lean_object*, lean_object*); @@ -296,7 +295,6 @@ lean_object* l_Lean_Parser_Command_declSig___closed__4; lean_object* l_Lean_Parser_Command_declValEqns___closed__4; lean_object* l_Lean_Parser_Command_constant___closed__7; lean_object* l_Lean_Parser_Command_def___closed__6; -lean_object* l_Lean_Parser_Command_strictInferMod___closed__4; lean_object* l_Lean_Parser_Term_stxQuot___closed__6; lean_object* l_Lean_Parser_Command_declSig___closed__1; extern lean_object* l_Lean_Parser_Term_explicitUniv___elambda__1___closed__14; @@ -322,11 +320,9 @@ lean_object* l_Lean_Parser_Command_attribute___elambda__1___closed__7; lean_object* l_Lean_Parser_finishCommentBlock___main(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Command_declId___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Command_declaration___closed__12; -lean_object* l_Lean_Parser_Command_strictInferMod___elambda__1___closed__4; lean_object* l_Lean_Parser_Command_protected; lean_object* l_Lean_Parser_Command_universes___closed__6; lean_object* l_Lean_Parser_Command_namespace___closed__2; -lean_object* l_Lean_Parser_Command_strictInferMod___elambda__1___closed__1; lean_object* l_Lean_Parser_Command_openRenaming___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Command_theorem___closed__6; lean_object* l_Lean_Parser_Command_openHiding___closed__4; @@ -347,6 +343,7 @@ lean_object* l_Lean_Parser_strLit___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Command_classInductive___elambda__1___closed__2; lean_object* l_Lean_Parser_Command_openRenamingItem___closed__7; lean_object* l_Lean_Parser_Command_attribute___elambda__1___closed__10; +lean_object* l_Lean_Parser_Command_inferMod___elambda__1___closed__4; lean_object* l_Lean_Parser_Command_protected___elambda__1___closed__9; lean_object* l_Lean_Parser_Command_check___elambda__1___closed__1; lean_object* l_Lean_Parser_Command_set__option___elambda__1___closed__4; @@ -362,6 +359,7 @@ lean_object* l_Lean_Parser_Command_inferMod___closed__3; lean_object* l_Lean_Parser_Command_openHiding___elambda__1___closed__3; lean_object* l_Lean_Parser_Command_noncomputable___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Command_resolve__name___elambda__1___closed__4; +lean_object* l_Lean_Parser_Command_inferMod___closed__5; lean_object* l_Lean_Parser_Command_variables___closed__5; lean_object* l_Lean_Parser_Command_attributes___elambda__1___closed__3; lean_object* l_Lean_Parser_Command_synth; @@ -401,7 +399,6 @@ lean_object* l_Lean_Parser_Command_end___closed__5; extern lean_object* l_Lean_Parser_Term_optType; lean_object* l_Lean_Parser_Command_declId___closed__2; lean_object* l_Lean_Parser_Command_classInductive___closed__5; -lean_object* l_Lean_Parser_Command_relaxedInferMod; lean_object* l_Lean_Parser_Command_open___closed__2; lean_object* l_Lean_Parser_Command_structCtor___closed__6; lean_object* l_Lean_Parser_regBuiltinCommandParserAttr(lean_object*); @@ -457,6 +454,7 @@ lean_object* l_Lean_Parser_Command_structFields___elambda__1___closed__2; lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Command_declId___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Command_universes___elambda__1___closed__6; lean_object* l_Lean_Parser_Command_structExplicitBinder; +lean_object* l_Lean_Parser_Command_inferMod___elambda__1___closed__2; lean_object* l_Lean_Parser_Command_axiom___closed__7; lean_object* l_Lean_Parser_Command_optDeclSig___elambda__1___closed__3; lean_object* l_Lean_Parser_Command_check__failure___closed__4; @@ -491,6 +489,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Command_check__failure(lean_object lean_object* l_Lean_Parser_Command_namespace___elambda__1___closed__2; lean_object* l_Lean_Parser_Command_section___elambda__1___closed__3; lean_object* l_Lean_Parser_Command_introRule___closed__4; +lean_object* l_Lean_Parser_Command_inferMod___elambda__1___closed__1; lean_object* l_Lean_Parser_Command_end___closed__3; lean_object* l_Lean_Parser_Command_extends___elambda__1___closed__5; lean_object* l_Lean_Parser_Command_inductive___closed__2; @@ -539,7 +538,6 @@ lean_object* l_Lean_Parser_Command_declValSimple___elambda__1___closed__4; lean_object* l_Lean_Parser_Command_variable___closed__4; lean_object* l_Lean_Parser_Command_example___elambda__1___closed__3; lean_object* l_Lean_Parser_Command_variable___elambda__1___closed__8; -lean_object* l_Lean_Parser_Command_strictInferMod___elambda__1___closed__3; lean_object* l_Lean_Parser_Command_partial___closed__3; lean_object* l_Lean_Parser_Command_structExplicitBinder___closed__2; lean_object* l_Lean_Parser_Command_openRenaming___elambda__1___closed__1; @@ -566,7 +564,6 @@ lean_object* l___regBuiltinParser_Lean_Parser_Command_universes(lean_object*); lean_object* l_Lean_Parser_Term_stxQuot___closed__7; lean_object* l_Lean_Parser_Command_structInstBinder___closed__4; lean_object* l_Lean_Parser_Command_inductive___closed__3; -lean_object* l_Lean_Parser_Command_strictInferMod___elambda__1___closed__2; lean_object* l_Lean_Parser_Command_section; lean_object* l_Lean_Parser_Command_openRenaming___elambda__1___closed__2; lean_object* l_Lean_Parser_Command_structExplicitBinder___closed__1; @@ -585,7 +582,6 @@ lean_object* l_Lean_Parser_Command_declaration___closed__4; lean_object* l_Lean_Parser_Command_theorem___closed__7; lean_object* l_Lean_Parser_Command_structInstBinder___closed__2; lean_object* l_Lean_Parser_Command_instance___elambda__1___closed__1; -lean_object* l_Lean_Parser_Command_relaxedInferMod___closed__4; lean_object* l_Lean_Parser_Command_inferMod; lean_object* l_Lean_Parser_Command_declValEqns___elambda__1___closed__3; lean_object* l_Lean_Parser_Command_axiom___elambda__1___closed__4; @@ -642,7 +638,6 @@ lean_object* l_Lean_Parser_Command_universes___closed__4; lean_object* l_Lean_Parser_Command_classTk___elambda__1___closed__4; lean_object* l_Lean_Parser_Command_constant___elambda__1___closed__6; extern lean_object* l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2; -lean_object* l_Lean_Parser_Command_relaxedInferMod___elambda__1___closed__4; lean_object* l_Lean_Parser_Command_declSig___elambda__1(lean_object*, lean_object*); extern lean_object* l_Lean_Parser_Term_haveAssign___elambda__1___closed__8; lean_object* l_Lean_Parser_Command_theorem___elambda__1___closed__5; @@ -654,7 +649,6 @@ lean_object* l_Lean_Parser_ParserState_restore(lean_object*, lean_object*, lean_ lean_object* l_Lean_Parser_Command_variable___elambda__1___closed__1; lean_object* l_Lean_Parser_Command_optDeclSig___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Command_variable___closed__6; -lean_object* l_Lean_Parser_Command_relaxedInferMod___elambda__1___closed__2; lean_object* l_Lean_Parser_Command_extends___elambda__1___closed__9; lean_object* l_Lean_Parser_Command_protected___closed__3; lean_object* l_Lean_Parser_Command_exit___elambda__1___closed__5; @@ -704,8 +698,6 @@ lean_object* l_Lean_Parser_Command_structInstBinder___closed__1; extern lean_object* l_Lean_Parser_Term_letIdLhs___closed__2; lean_object* l_Lean_Parser_Command_noncomputable___closed__5; lean_object* l_Lean_Parser_Command_structCtor___closed__7; -lean_object* l_Lean_Parser_Command_relaxedInferMod___closed__5; -lean_object* l_Lean_Parser_Command_relaxedInferMod___elambda__1___closed__1; lean_object* l_Lean_Parser_Command_openRenaming___elambda__1___closed__9; lean_object* l_Lean_Parser_Command_instance___elambda__1___closed__2; lean_object* l_Lean_Parser_Command_noncomputable___elambda__1___closed__3; @@ -716,7 +708,6 @@ lean_object* l_Lean_Parser_Command_inductive___closed__4; lean_object* l_Lean_Parser_Command_private; lean_object* l_Lean_Parser_Command_check___closed__6; lean_object* l_Lean_Parser_Command_openRenamingItem___elambda__1___closed__7; -lean_object* l_Lean_Parser_Command_relaxedInferMod___closed__3; lean_object* l_Lean_Parser_Command_extends___closed__4; lean_object* l_Lean_Parser_Command_attrInstance___closed__5; lean_object* l_Lean_Parser_Command_noncomputable___elambda__1___closed__5; @@ -743,7 +734,6 @@ lean_object* l_Lean_Parser_Command_set__option___closed__4; lean_object* l_Lean_Parser_Command_example___elambda__1___closed__9; lean_object* l_Lean_Parser_Command_declVal___closed__1; lean_object* l_Lean_Parser_Command_openRenaming___closed__1; -lean_object* l_Lean_Parser_Command_strictInferMod___closed__3; extern lean_object* l_Bool_HasRepr___closed__1; lean_object* l_Lean_Parser_Command_check; lean_object* l_Lean_Parser_Command_inductive___elambda__1___closed__4; @@ -931,7 +921,6 @@ lean_object* l_Lean_Parser_Command_exit___closed__5; lean_object* l_Lean_Parser_Command_declValSimple; lean_object* l_Lean_Parser_Command_attributes; lean_object* l_Lean_Parser_Command_resolve__name___closed__5; -lean_object* l_Lean_Parser_Command_relaxedInferMod___closed__1; lean_object* l_Lean_Parser_Command_openOnly___elambda__1___closed__2; lean_object* l_Lean_Parser_Command_declaration___elambda__1___closed__1; lean_object* l_Lean_Parser_Command_attribute___elambda__1___closed__1; @@ -953,14 +942,12 @@ lean_object* l_Lean_Parser_Command_set__option___closed__1; lean_object* l_Lean_Parser_Command_protected___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Command_introRule___closed__5; lean_object* l_Lean_Parser_Command_set__option___elambda__1___closed__7; -lean_object* l_Lean_Parser_Command_relaxedInferMod___closed__2; lean_object* l_Lean_Parser_Command_unsafe___elambda__1___closed__1; lean_object* l_Lean_Parser_Command_classTk___closed__3; lean_object* l_Lean_Parser_Command_variables___elambda__1___closed__7; lean_object* l_Lean_Parser_Command_structFields___closed__5; lean_object* l_Lean_Parser_Command_variable___closed__2; lean_object* l_Lean_Parser_Command_unsafe___elambda__1___closed__2; -lean_object* l_Lean_Parser_Command_strictInferMod___closed__2; lean_object* l_Lean_Parser_Command_synth___elambda__1___closed__6; lean_object* l_Lean_Parser_Command_structImplicitBinder___elambda__1___closed__1; lean_object* l_Lean_Parser_Command_classInductive___elambda__1___closed__4; @@ -977,7 +964,6 @@ lean_object* l_Lean_Parser_Command_universe___closed__6; lean_object* l_Lean_Parser_Command_universes; lean_object* l_Lean_Parser_Command_attribute___closed__11; lean_object* l_Lean_Parser_Command_attribute___elambda__1___closed__8; -lean_object* l_Lean_Parser_Command_relaxedInferMod___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Command_variables; lean_object* l_Lean_Parser_Command_set__option___elambda__1___closed__10; lean_object* l_Lean_Parser_Command_universes___elambda__1___closed__8; @@ -1006,7 +992,6 @@ lean_object* l_Lean_Parser_Command_openHiding___elambda__1___closed__1; lean_object* l_Lean_Parser_Command_structCtor___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Command_partial; lean_object* l_Lean_Parser_Command_declId___elambda__1___closed__4; -lean_object* l_Lean_Parser_Command_strictInferMod___closed__5; lean_object* l_Lean_Parser_Command_declModifiers___closed__11; lean_object* l_Lean_Parser_Command_end___elambda__1___closed__5; lean_object* l_Lean_Parser_Command_variable___elambda__1___closed__3; @@ -1018,7 +1003,6 @@ lean_object* l_Lean_Parser_Command_structExplicitBinder___elambda__1(lean_object lean_object* l_Lean_Parser_Command_attrArg___closed__2; lean_object* l_Lean_Parser_Command_declaration___elambda__1___closed__4; lean_object* l_Lean_Parser_Command_attribute___elambda__1___closed__9; -lean_object* l_Lean_Parser_Command_relaxedInferMod___elambda__1___closed__3; lean_object* l_Lean_Parser_Command_structureTk___elambda__1___closed__9; lean_object* l_Lean_Parser_Command_universe___elambda__1___closed__4; lean_object* l_Lean_Parser_Command_optDeclSig___elambda__1___closed__2; @@ -12326,50 +12310,50 @@ x_1 = l_Lean_Parser_Command_example___closed__6; return x_1; } } -lean_object* _init_l_Lean_Parser_Command_relaxedInferMod___elambda__1___closed__1() { +lean_object* _init_l_Lean_Parser_Command_inferMod___elambda__1___closed__1() { _start: { lean_object* x_1; -x_1 = lean_mk_string("relaxedInferMod"); +x_1 = lean_mk_string("inferMod"); return x_1; } } -lean_object* _init_l_Lean_Parser_Command_relaxedInferMod___elambda__1___closed__2() { +lean_object* _init_l_Lean_Parser_Command_inferMod___elambda__1___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Command_docComment___elambda__1___closed__2; -x_2 = l_Lean_Parser_Command_relaxedInferMod___elambda__1___closed__1; +x_2 = l_Lean_Parser_Command_inferMod___elambda__1___closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -lean_object* _init_l_Lean_Parser_Command_relaxedInferMod___elambda__1___closed__3() { +lean_object* _init_l_Lean_Parser_Command_inferMod___elambda__1___closed__3() { _start: { lean_object* x_1; lean_object* x_2; -x_1 = l_Lean_Parser_Command_relaxedInferMod___elambda__1___closed__2; +x_1 = l_Lean_Parser_Command_inferMod___elambda__1___closed__2; x_2 = lean_alloc_ctor(1, 1, 0); lean_ctor_set(x_2, 0, x_1); return x_2; } } -lean_object* _init_l_Lean_Parser_Command_relaxedInferMod___elambda__1___closed__4() { +lean_object* _init_l_Lean_Parser_Command_inferMod___elambda__1___closed__4() { _start: { lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; -x_1 = l_Lean_Parser_Command_relaxedInferMod___elambda__1___closed__1; -x_2 = l_Lean_Parser_Command_relaxedInferMod___elambda__1___closed__3; +x_1 = l_Lean_Parser_Command_inferMod___elambda__1___closed__1; +x_2 = l_Lean_Parser_Command_inferMod___elambda__1___closed__3; x_3 = 1; x_4 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3); return x_4; } } -lean_object* l_Lean_Parser_Command_relaxedInferMod___elambda__1(lean_object* x_1, lean_object* x_2) { +lean_object* l_Lean_Parser_Command_inferMod___elambda__1(lean_object* x_1, lean_object* x_2) { _start: { lean_object* x_3; lean_object* x_4; uint8_t x_5; -x_3 = l_Lean_Parser_Command_relaxedInferMod___elambda__1___closed__4; +x_3 = l_Lean_Parser_Command_inferMod___elambda__1___closed__4; x_4 = lean_ctor_get(x_3, 1); lean_inc(x_4); lean_inc(x_2); @@ -12449,7 +12433,7 @@ lean_object* x_13; lean_object* x_14; lean_dec(x_11); lean_dec(x_10); lean_dec(x_7); -x_13 = l_Lean_Parser_Command_relaxedInferMod___elambda__1___closed__2; +x_13 = l_Lean_Parser_Command_inferMod___elambda__1___closed__2; x_14 = l_Lean_Parser_ParserState_mkNode(x_9, x_13, x_8); return x_14; } @@ -12463,7 +12447,7 @@ lean_ctor_set(x_16, 0, x_15); lean_ctor_set(x_16, 1, x_7); lean_ctor_set(x_16, 2, x_11); lean_ctor_set(x_16, 3, x_12); -x_17 = l_Lean_Parser_Command_relaxedInferMod___elambda__1___closed__2; +x_17 = l_Lean_Parser_Command_inferMod___elambda__1___closed__2; x_18 = l_Lean_Parser_ParserState_mkNode(x_16, x_17, x_8); return x_18; } @@ -12713,7 +12697,7 @@ lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_dec(x_79); lean_dec(x_78); lean_dec(x_69); -x_81 = l_Lean_Parser_Command_relaxedInferMod___elambda__1___closed__2; +x_81 = l_Lean_Parser_Command_inferMod___elambda__1___closed__2; x_82 = l_Lean_Parser_ParserState_mkNode(x_77, x_81, x_76); x_83 = l_Lean_Parser_mergeOrElseErrors(x_82, x_71, x_66); lean_dec(x_66); @@ -12734,7 +12718,7 @@ lean_ctor_set(x_85, 0, x_84); lean_ctor_set(x_85, 1, x_66); lean_ctor_set(x_85, 2, x_79); lean_ctor_set(x_85, 3, x_80); -x_86 = l_Lean_Parser_Command_relaxedInferMod___elambda__1___closed__2; +x_86 = l_Lean_Parser_Command_inferMod___elambda__1___closed__2; x_87 = l_Lean_Parser_ParserState_mkNode(x_85, x_86, x_76); x_88 = l_Lean_Parser_mergeOrElseErrors(x_87, x_71, x_66); lean_dec(x_66); @@ -12865,7 +12849,7 @@ goto block_89; } } } -lean_object* _init_l_Lean_Parser_Command_relaxedInferMod___closed__1() { +lean_object* _init_l_Lean_Parser_Command_inferMod___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; @@ -12875,736 +12859,42 @@ x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); return x_3; } } -lean_object* _init_l_Lean_Parser_Command_relaxedInferMod___closed__2() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Command_relaxedInferMod___elambda__1___closed__2; -x_2 = l_Lean_Parser_Command_relaxedInferMod___closed__1; -x_3 = l_Lean_Parser_nodeInfo(x_1, x_2); -return x_3; -} -} -lean_object* _init_l_Lean_Parser_Command_relaxedInferMod___closed__3() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_Command_relaxedInferMod___elambda__1___closed__4; -x_2 = lean_ctor_get(x_1, 0); -lean_inc(x_2); -x_3 = l_Lean_Parser_Command_relaxedInferMod___closed__2; -x_4 = l_Lean_Parser_orelseInfo(x_2, x_3); -return x_4; -} -} -lean_object* _init_l_Lean_Parser_Command_relaxedInferMod___closed__4() { -_start: -{ -lean_object* x_1; -x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Command_relaxedInferMod___elambda__1), 2, 0); -return x_1; -} -} -lean_object* _init_l_Lean_Parser_Command_relaxedInferMod___closed__5() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Command_relaxedInferMod___closed__3; -x_2 = l_Lean_Parser_Command_relaxedInferMod___closed__4; -x_3 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_3, 0, x_1); -lean_ctor_set(x_3, 1, x_2); -return x_3; -} -} -lean_object* _init_l_Lean_Parser_Command_relaxedInferMod() { -_start: -{ -lean_object* x_1; -x_1 = l_Lean_Parser_Command_relaxedInferMod___closed__5; -return x_1; -} -} -lean_object* _init_l_Lean_Parser_Command_strictInferMod___elambda__1___closed__1() { -_start: -{ -lean_object* x_1; -x_1 = lean_mk_string("strictInferMod"); -return x_1; -} -} -lean_object* _init_l_Lean_Parser_Command_strictInferMod___elambda__1___closed__2() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Command_docComment___elambda__1___closed__2; -x_2 = l_Lean_Parser_Command_strictInferMod___elambda__1___closed__1; -x_3 = lean_name_mk_string(x_1, x_2); -return x_3; -} -} -lean_object* _init_l_Lean_Parser_Command_strictInferMod___elambda__1___closed__3() { -_start: -{ -lean_object* x_1; lean_object* x_2; -x_1 = l_Lean_Parser_Command_strictInferMod___elambda__1___closed__2; -x_2 = lean_alloc_ctor(1, 1, 0); -lean_ctor_set(x_2, 0, x_1); -return x_2; -} -} -lean_object* _init_l_Lean_Parser_Command_strictInferMod___elambda__1___closed__4() { -_start: -{ -lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; -x_1 = l_Lean_Parser_Command_strictInferMod___elambda__1___closed__1; -x_2 = l_Lean_Parser_Command_strictInferMod___elambda__1___closed__3; -x_3 = 1; -x_4 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3); -return x_4; -} -} -lean_object* l_Lean_Parser_Command_strictInferMod___elambda__1(lean_object* x_1, lean_object* x_2) { -_start: -{ -lean_object* x_3; lean_object* x_4; uint8_t x_5; -x_3 = l_Lean_Parser_Command_strictInferMod___elambda__1___closed__4; -x_4 = lean_ctor_get(x_3, 1); -lean_inc(x_4); -lean_inc(x_2); -lean_inc(x_1); -x_5 = l_Lean_Parser_tryAnti(x_1, x_2); -if (x_5 == 0) -{ -lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_20; lean_object* x_52; lean_object* x_53; -lean_dec(x_4); -x_6 = lean_ctor_get(x_2, 0); -lean_inc(x_6); -x_7 = lean_ctor_get(x_2, 1); -lean_inc(x_7); -x_8 = lean_array_get_size(x_6); -lean_dec(x_6); -lean_inc(x_1); -x_52 = l_Lean_Parser_tokenFn(x_1, x_2); -x_53 = lean_ctor_get(x_52, 3); -lean_inc(x_53); -if (lean_obj_tag(x_53) == 0) -{ -lean_object* x_54; lean_object* x_55; -x_54 = lean_ctor_get(x_52, 0); -lean_inc(x_54); -x_55 = l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(x_54); -lean_dec(x_54); -if (lean_obj_tag(x_55) == 2) -{ -lean_object* x_56; lean_object* x_57; uint8_t x_58; -x_56 = lean_ctor_get(x_55, 1); -lean_inc(x_56); -lean_dec(x_55); -x_57 = l___private_Init_Lean_Parser_Parser_11__antiquotNestedExpr___elambda__1___closed__3; -x_58 = lean_string_dec_eq(x_56, x_57); -lean_dec(x_56); -if (x_58 == 0) -{ -lean_object* x_59; lean_object* x_60; -x_59 = l___private_Init_Lean_Parser_Parser_11__antiquotNestedExpr___elambda__1___closed__10; -lean_inc(x_7); -x_60 = l_Lean_Parser_ParserState_mkErrorsAt(x_52, x_59, x_7); -x_20 = x_60; -goto block_51; -} -else -{ -x_20 = x_52; -goto block_51; -} -} -else -{ -lean_object* x_61; lean_object* x_62; -lean_dec(x_55); -x_61 = l___private_Init_Lean_Parser_Parser_11__antiquotNestedExpr___elambda__1___closed__10; -lean_inc(x_7); -x_62 = l_Lean_Parser_ParserState_mkErrorsAt(x_52, x_61, x_7); -x_20 = x_62; -goto block_51; -} -} -else -{ -lean_object* x_63; lean_object* x_64; -lean_dec(x_53); -x_63 = l___private_Init_Lean_Parser_Parser_11__antiquotNestedExpr___elambda__1___closed__10; -lean_inc(x_7); -x_64 = l_Lean_Parser_ParserState_mkErrorsAt(x_52, x_63, x_7); -x_20 = x_64; -goto block_51; -} -block_19: -{ -if (lean_obj_tag(x_12) == 0) -{ -lean_object* x_13; lean_object* x_14; -lean_dec(x_11); -lean_dec(x_10); -lean_dec(x_7); -x_13 = l_Lean_Parser_Command_strictInferMod___elambda__1___closed__2; -x_14 = l_Lean_Parser_ParserState_mkNode(x_9, x_13, x_8); -return x_14; -} -else -{ -lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; -lean_dec(x_9); -x_15 = l_Array_shrink___main___rarg(x_10, x_8); -x_16 = lean_alloc_ctor(0, 4, 0); -lean_ctor_set(x_16, 0, x_15); -lean_ctor_set(x_16, 1, x_7); -lean_ctor_set(x_16, 2, x_11); -lean_ctor_set(x_16, 3, x_12); -x_17 = l_Lean_Parser_Command_strictInferMod___elambda__1___closed__2; -x_18 = l_Lean_Parser_ParserState_mkNode(x_16, x_17, x_8); -return x_18; -} -} -block_51: -{ -lean_object* x_21; -x_21 = lean_ctor_get(x_20, 3); -lean_inc(x_21); -if (lean_obj_tag(x_21) == 0) -{ -lean_object* x_22; lean_object* x_23; lean_object* x_24; -x_22 = lean_ctor_get(x_20, 1); -lean_inc(x_22); -x_23 = l_Lean_Parser_tokenFn(x_1, x_20); -x_24 = lean_ctor_get(x_23, 3); -lean_inc(x_24); -if (lean_obj_tag(x_24) == 0) -{ -lean_object* x_25; lean_object* x_26; -x_25 = lean_ctor_get(x_23, 0); -lean_inc(x_25); -x_26 = l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(x_25); -lean_dec(x_25); -if (lean_obj_tag(x_26) == 2) -{ -lean_object* x_27; lean_object* x_28; uint8_t x_29; -x_27 = lean_ctor_get(x_26, 1); -lean_inc(x_27); -lean_dec(x_26); -x_28 = l___private_Init_Lean_Parser_Parser_11__antiquotNestedExpr___elambda__1___closed__4; -x_29 = lean_string_dec_eq(x_27, x_28); -lean_dec(x_27); -if (x_29 == 0) -{ -lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; -x_30 = l___private_Init_Lean_Parser_Parser_11__antiquotNestedExpr___elambda__1___closed__7; -x_31 = l_Lean_Parser_ParserState_mkErrorsAt(x_23, x_30, x_22); -x_32 = lean_ctor_get(x_31, 0); -lean_inc(x_32); -x_33 = lean_ctor_get(x_31, 2); -lean_inc(x_33); -x_34 = lean_ctor_get(x_31, 3); -lean_inc(x_34); -x_9 = x_31; -x_10 = x_32; -x_11 = x_33; -x_12 = x_34; -goto block_19; -} -else -{ -lean_object* x_35; lean_object* x_36; lean_object* x_37; -lean_dec(x_22); -x_35 = lean_ctor_get(x_23, 0); -lean_inc(x_35); -x_36 = lean_ctor_get(x_23, 2); -lean_inc(x_36); -x_37 = lean_ctor_get(x_23, 3); -lean_inc(x_37); -x_9 = x_23; -x_10 = x_35; -x_11 = x_36; -x_12 = x_37; -goto block_19; -} -} -else -{ -lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; -lean_dec(x_26); -x_38 = l___private_Init_Lean_Parser_Parser_11__antiquotNestedExpr___elambda__1___closed__7; -x_39 = l_Lean_Parser_ParserState_mkErrorsAt(x_23, x_38, x_22); -x_40 = lean_ctor_get(x_39, 0); -lean_inc(x_40); -x_41 = lean_ctor_get(x_39, 2); -lean_inc(x_41); -x_42 = lean_ctor_get(x_39, 3); -lean_inc(x_42); -x_9 = x_39; -x_10 = x_40; -x_11 = x_41; -x_12 = x_42; -goto block_19; -} -} -else -{ -lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; -lean_dec(x_24); -x_43 = l___private_Init_Lean_Parser_Parser_11__antiquotNestedExpr___elambda__1___closed__7; -x_44 = l_Lean_Parser_ParserState_mkErrorsAt(x_23, x_43, x_22); -x_45 = lean_ctor_get(x_44, 0); -lean_inc(x_45); -x_46 = lean_ctor_get(x_44, 2); -lean_inc(x_46); -x_47 = lean_ctor_get(x_44, 3); -lean_inc(x_47); -x_9 = x_44; -x_10 = x_45; -x_11 = x_46; -x_12 = x_47; -goto block_19; -} -} -else -{ -lean_object* x_48; lean_object* x_49; lean_object* x_50; -lean_dec(x_21); -lean_dec(x_1); -x_48 = lean_ctor_get(x_20, 0); -lean_inc(x_48); -x_49 = lean_ctor_get(x_20, 2); -lean_inc(x_49); -x_50 = lean_ctor_get(x_20, 3); -lean_inc(x_50); -x_9 = x_20; -x_10 = x_48; -x_11 = x_49; -x_12 = x_50; -goto block_19; -} -} -} -else -{ -lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; -x_65 = lean_ctor_get(x_2, 0); -lean_inc(x_65); -x_66 = lean_ctor_get(x_2, 1); -lean_inc(x_66); -x_67 = lean_array_get_size(x_65); -lean_dec(x_65); -lean_inc(x_2); -lean_inc(x_1); -x_68 = lean_apply_2(x_4, x_1, x_2); -if (lean_is_exclusive(x_2)) { - lean_ctor_release(x_2, 0); - lean_ctor_release(x_2, 1); - lean_ctor_release(x_2, 2); - lean_ctor_release(x_2, 3); - x_69 = x_2; -} else { - lean_dec_ref(x_2); - x_69 = lean_box(0); -} -x_70 = lean_ctor_get(x_68, 3); -lean_inc(x_70); -if (lean_obj_tag(x_70) == 0) -{ -lean_dec(x_69); -lean_dec(x_67); -lean_dec(x_66); -lean_dec(x_1); -return x_68; -} -else -{ -lean_object* x_71; lean_object* x_72; uint8_t x_73; -x_71 = lean_ctor_get(x_70, 0); -lean_inc(x_71); -lean_dec(x_70); -x_72 = lean_ctor_get(x_68, 1); -lean_inc(x_72); -x_73 = lean_nat_dec_eq(x_72, x_66); -lean_dec(x_72); -if (x_73 == 0) -{ -lean_dec(x_71); -lean_dec(x_69); -lean_dec(x_67); -lean_dec(x_66); -lean_dec(x_1); -return x_68; -} -else -{ -lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79; lean_object* x_80; lean_object* x_90; lean_object* x_122; lean_object* x_123; -lean_inc(x_66); -x_74 = l_Lean_Parser_ParserState_restore(x_68, x_67, x_66); -lean_dec(x_67); -x_75 = lean_ctor_get(x_74, 0); -lean_inc(x_75); -x_76 = lean_array_get_size(x_75); -lean_dec(x_75); -lean_inc(x_1); -x_122 = l_Lean_Parser_tokenFn(x_1, x_74); -x_123 = lean_ctor_get(x_122, 3); -lean_inc(x_123); -if (lean_obj_tag(x_123) == 0) -{ -lean_object* x_124; lean_object* x_125; -x_124 = lean_ctor_get(x_122, 0); -lean_inc(x_124); -x_125 = l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(x_124); -lean_dec(x_124); -if (lean_obj_tag(x_125) == 2) -{ -lean_object* x_126; lean_object* x_127; uint8_t x_128; -x_126 = lean_ctor_get(x_125, 1); -lean_inc(x_126); -lean_dec(x_125); -x_127 = l___private_Init_Lean_Parser_Parser_11__antiquotNestedExpr___elambda__1___closed__3; -x_128 = lean_string_dec_eq(x_126, x_127); -lean_dec(x_126); -if (x_128 == 0) -{ -lean_object* x_129; lean_object* x_130; -x_129 = l___private_Init_Lean_Parser_Parser_11__antiquotNestedExpr___elambda__1___closed__10; -lean_inc(x_66); -x_130 = l_Lean_Parser_ParserState_mkErrorsAt(x_122, x_129, x_66); -x_90 = x_130; -goto block_121; -} -else -{ -x_90 = x_122; -goto block_121; -} -} -else -{ -lean_object* x_131; lean_object* x_132; -lean_dec(x_125); -x_131 = l___private_Init_Lean_Parser_Parser_11__antiquotNestedExpr___elambda__1___closed__10; -lean_inc(x_66); -x_132 = l_Lean_Parser_ParserState_mkErrorsAt(x_122, x_131, x_66); -x_90 = x_132; -goto block_121; -} -} -else -{ -lean_object* x_133; lean_object* x_134; -lean_dec(x_123); -x_133 = l___private_Init_Lean_Parser_Parser_11__antiquotNestedExpr___elambda__1___closed__10; -lean_inc(x_66); -x_134 = l_Lean_Parser_ParserState_mkErrorsAt(x_122, x_133, x_66); -x_90 = x_134; -goto block_121; -} -block_89: -{ -if (lean_obj_tag(x_80) == 0) -{ -lean_object* x_81; lean_object* x_82; lean_object* x_83; -lean_dec(x_79); -lean_dec(x_78); -lean_dec(x_69); -x_81 = l_Lean_Parser_Command_strictInferMod___elambda__1___closed__2; -x_82 = l_Lean_Parser_ParserState_mkNode(x_77, x_81, x_76); -x_83 = l_Lean_Parser_mergeOrElseErrors(x_82, x_71, x_66); -lean_dec(x_66); -return x_83; -} -else -{ -lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88; -lean_dec(x_77); -x_84 = l_Array_shrink___main___rarg(x_78, x_76); -lean_inc(x_66); -if (lean_is_scalar(x_69)) { - x_85 = lean_alloc_ctor(0, 4, 0); -} else { - x_85 = x_69; -} -lean_ctor_set(x_85, 0, x_84); -lean_ctor_set(x_85, 1, x_66); -lean_ctor_set(x_85, 2, x_79); -lean_ctor_set(x_85, 3, x_80); -x_86 = l_Lean_Parser_Command_strictInferMod___elambda__1___closed__2; -x_87 = l_Lean_Parser_ParserState_mkNode(x_85, x_86, x_76); -x_88 = l_Lean_Parser_mergeOrElseErrors(x_87, x_71, x_66); -lean_dec(x_66); -return x_88; -} -} -block_121: -{ -lean_object* x_91; -x_91 = lean_ctor_get(x_90, 3); -lean_inc(x_91); -if (lean_obj_tag(x_91) == 0) -{ -lean_object* x_92; lean_object* x_93; lean_object* x_94; -x_92 = lean_ctor_get(x_90, 1); -lean_inc(x_92); -x_93 = l_Lean_Parser_tokenFn(x_1, x_90); -x_94 = lean_ctor_get(x_93, 3); -lean_inc(x_94); -if (lean_obj_tag(x_94) == 0) -{ -lean_object* x_95; lean_object* x_96; -x_95 = lean_ctor_get(x_93, 0); -lean_inc(x_95); -x_96 = l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(x_95); -lean_dec(x_95); -if (lean_obj_tag(x_96) == 2) -{ -lean_object* x_97; lean_object* x_98; uint8_t x_99; -x_97 = lean_ctor_get(x_96, 1); -lean_inc(x_97); -lean_dec(x_96); -x_98 = l___private_Init_Lean_Parser_Parser_11__antiquotNestedExpr___elambda__1___closed__4; -x_99 = lean_string_dec_eq(x_97, x_98); -lean_dec(x_97); -if (x_99 == 0) -{ -lean_object* x_100; lean_object* x_101; lean_object* x_102; lean_object* x_103; lean_object* x_104; -x_100 = l___private_Init_Lean_Parser_Parser_11__antiquotNestedExpr___elambda__1___closed__7; -x_101 = l_Lean_Parser_ParserState_mkErrorsAt(x_93, x_100, x_92); -x_102 = lean_ctor_get(x_101, 0); -lean_inc(x_102); -x_103 = lean_ctor_get(x_101, 2); -lean_inc(x_103); -x_104 = lean_ctor_get(x_101, 3); -lean_inc(x_104); -x_77 = x_101; -x_78 = x_102; -x_79 = x_103; -x_80 = x_104; -goto block_89; -} -else -{ -lean_object* x_105; lean_object* x_106; lean_object* x_107; -lean_dec(x_92); -x_105 = lean_ctor_get(x_93, 0); -lean_inc(x_105); -x_106 = lean_ctor_get(x_93, 2); -lean_inc(x_106); -x_107 = lean_ctor_get(x_93, 3); -lean_inc(x_107); -x_77 = x_93; -x_78 = x_105; -x_79 = x_106; -x_80 = x_107; -goto block_89; -} -} -else -{ -lean_object* x_108; lean_object* x_109; lean_object* x_110; lean_object* x_111; lean_object* x_112; -lean_dec(x_96); -x_108 = l___private_Init_Lean_Parser_Parser_11__antiquotNestedExpr___elambda__1___closed__7; -x_109 = l_Lean_Parser_ParserState_mkErrorsAt(x_93, x_108, x_92); -x_110 = lean_ctor_get(x_109, 0); -lean_inc(x_110); -x_111 = lean_ctor_get(x_109, 2); -lean_inc(x_111); -x_112 = lean_ctor_get(x_109, 3); -lean_inc(x_112); -x_77 = x_109; -x_78 = x_110; -x_79 = x_111; -x_80 = x_112; -goto block_89; -} -} -else -{ -lean_object* x_113; lean_object* x_114; lean_object* x_115; lean_object* x_116; lean_object* x_117; -lean_dec(x_94); -x_113 = l___private_Init_Lean_Parser_Parser_11__antiquotNestedExpr___elambda__1___closed__7; -x_114 = l_Lean_Parser_ParserState_mkErrorsAt(x_93, x_113, x_92); -x_115 = lean_ctor_get(x_114, 0); -lean_inc(x_115); -x_116 = lean_ctor_get(x_114, 2); -lean_inc(x_116); -x_117 = lean_ctor_get(x_114, 3); -lean_inc(x_117); -x_77 = x_114; -x_78 = x_115; -x_79 = x_116; -x_80 = x_117; -goto block_89; -} -} -else -{ -lean_object* x_118; lean_object* x_119; lean_object* x_120; -lean_dec(x_91); -lean_dec(x_1); -x_118 = lean_ctor_get(x_90, 0); -lean_inc(x_118); -x_119 = lean_ctor_get(x_90, 2); -lean_inc(x_119); -x_120 = lean_ctor_get(x_90, 3); -lean_inc(x_120); -x_77 = x_90; -x_78 = x_118; -x_79 = x_119; -x_80 = x_120; -goto block_89; -} -} -} -} -} -} -} -lean_object* _init_l_Lean_Parser_Command_strictInferMod___closed__1() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l___private_Init_Lean_Parser_Parser_11__antiquotNestedExpr___closed__1; -x_2 = l___private_Init_Lean_Parser_Parser_11__antiquotNestedExpr___closed__3; -x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); -return x_3; -} -} -lean_object* _init_l_Lean_Parser_Command_strictInferMod___closed__2() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Command_strictInferMod___elambda__1___closed__2; -x_2 = l_Lean_Parser_Command_strictInferMod___closed__1; -x_3 = l_Lean_Parser_nodeInfo(x_1, x_2); -return x_3; -} -} -lean_object* _init_l_Lean_Parser_Command_strictInferMod___closed__3() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_Command_strictInferMod___elambda__1___closed__4; -x_2 = lean_ctor_get(x_1, 0); -lean_inc(x_2); -x_3 = l_Lean_Parser_Command_strictInferMod___closed__2; -x_4 = l_Lean_Parser_orelseInfo(x_2, x_3); -return x_4; -} -} -lean_object* _init_l_Lean_Parser_Command_strictInferMod___closed__4() { -_start: -{ -lean_object* x_1; -x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Command_strictInferMod___elambda__1), 2, 0); -return x_1; -} -} -lean_object* _init_l_Lean_Parser_Command_strictInferMod___closed__5() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Command_strictInferMod___closed__3; -x_2 = l_Lean_Parser_Command_strictInferMod___closed__4; -x_3 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_3, 0, x_1); -lean_ctor_set(x_3, 1, x_2); -return x_3; -} -} -lean_object* _init_l_Lean_Parser_Command_strictInferMod() { -_start: -{ -lean_object* x_1; -x_1 = l_Lean_Parser_Command_strictInferMod___closed__5; -return x_1; -} -} -lean_object* l_Lean_Parser_Command_inferMod___elambda__1(lean_object* x_1, lean_object* x_2) { -_start: -{ -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_2, 0); -lean_inc(x_3); -x_4 = lean_array_get_size(x_3); -lean_dec(x_3); -x_5 = lean_ctor_get(x_2, 1); -lean_inc(x_5); -lean_inc(x_1); -x_6 = l_Lean_Parser_Command_relaxedInferMod___elambda__1(x_1, x_2); -x_7 = lean_ctor_get(x_6, 3); -lean_inc(x_7); -if (lean_obj_tag(x_7) == 0) -{ -lean_dec(x_5); -lean_dec(x_4); -lean_dec(x_1); -return x_6; -} -else -{ -lean_object* x_8; lean_object* x_9; uint8_t x_10; -x_8 = lean_ctor_get(x_7, 0); -lean_inc(x_8); -lean_dec(x_7); -x_9 = lean_ctor_get(x_6, 1); -lean_inc(x_9); -x_10 = lean_nat_dec_eq(x_9, x_5); -lean_dec(x_9); -if (x_10 == 0) -{ -lean_dec(x_8); -lean_dec(x_5); -lean_dec(x_4); -lean_dec(x_1); -return x_6; -} -else -{ -lean_object* x_11; lean_object* x_12; lean_object* x_13; -lean_inc(x_5); -x_11 = l_Lean_Parser_ParserState_restore(x_6, x_4, x_5); -lean_dec(x_4); -x_12 = l_Lean_Parser_Command_strictInferMod___elambda__1(x_1, x_11); -x_13 = l_Lean_Parser_mergeOrElseErrors(x_12, x_8, x_5); -lean_dec(x_5); -return x_13; -} -} -} -} -lean_object* _init_l_Lean_Parser_Command_inferMod___closed__1() { -_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_Parser_Command_relaxedInferMod; -x_2 = lean_ctor_get(x_1, 0); -lean_inc(x_2); -x_3 = l_Lean_Parser_Command_strictInferMod; -x_4 = lean_ctor_get(x_3, 0); -lean_inc(x_4); -x_5 = l_Lean_Parser_orelseInfo(x_2, x_4); -return x_5; -} -} lean_object* _init_l_Lean_Parser_Command_inferMod___closed__2() { _start: { +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Command_inferMod___elambda__1___closed__2; +x_2 = l_Lean_Parser_Command_inferMod___closed__1; +x_3 = l_Lean_Parser_nodeInfo(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Command_inferMod___closed__3() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Parser_Command_inferMod___elambda__1___closed__4; +x_2 = lean_ctor_get(x_1, 0); +lean_inc(x_2); +x_3 = l_Lean_Parser_Command_inferMod___closed__2; +x_4 = l_Lean_Parser_orelseInfo(x_2, x_3); +return x_4; +} +} +lean_object* _init_l_Lean_Parser_Command_inferMod___closed__4() { +_start: +{ lean_object* x_1; x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Command_inferMod___elambda__1), 2, 0); return x_1; } } -lean_object* _init_l_Lean_Parser_Command_inferMod___closed__3() { +lean_object* _init_l_Lean_Parser_Command_inferMod___closed__5() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Command_inferMod___closed__1; -x_2 = l_Lean_Parser_Command_inferMod___closed__2; +x_1 = l_Lean_Parser_Command_inferMod___closed__3; +x_2 = l_Lean_Parser_Command_inferMod___closed__4; x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); lean_ctor_set(x_3, 1, x_2); @@ -13615,7 +12905,7 @@ lean_object* _init_l_Lean_Parser_Command_inferMod() { _start: { lean_object* x_1; -x_1 = l_Lean_Parser_Command_inferMod___closed__3; +x_1 = l_Lean_Parser_Command_inferMod___closed__5; return x_1; } } @@ -34877,52 +34167,24 @@ l_Lean_Parser_Command_example___closed__6 = _init_l_Lean_Parser_Command_example_ lean_mark_persistent(l_Lean_Parser_Command_example___closed__6); l_Lean_Parser_Command_example = _init_l_Lean_Parser_Command_example(); lean_mark_persistent(l_Lean_Parser_Command_example); -l_Lean_Parser_Command_relaxedInferMod___elambda__1___closed__1 = _init_l_Lean_Parser_Command_relaxedInferMod___elambda__1___closed__1(); -lean_mark_persistent(l_Lean_Parser_Command_relaxedInferMod___elambda__1___closed__1); -l_Lean_Parser_Command_relaxedInferMod___elambda__1___closed__2 = _init_l_Lean_Parser_Command_relaxedInferMod___elambda__1___closed__2(); -lean_mark_persistent(l_Lean_Parser_Command_relaxedInferMod___elambda__1___closed__2); -l_Lean_Parser_Command_relaxedInferMod___elambda__1___closed__3 = _init_l_Lean_Parser_Command_relaxedInferMod___elambda__1___closed__3(); -lean_mark_persistent(l_Lean_Parser_Command_relaxedInferMod___elambda__1___closed__3); -l_Lean_Parser_Command_relaxedInferMod___elambda__1___closed__4 = _init_l_Lean_Parser_Command_relaxedInferMod___elambda__1___closed__4(); -lean_mark_persistent(l_Lean_Parser_Command_relaxedInferMod___elambda__1___closed__4); -l_Lean_Parser_Command_relaxedInferMod___closed__1 = _init_l_Lean_Parser_Command_relaxedInferMod___closed__1(); -lean_mark_persistent(l_Lean_Parser_Command_relaxedInferMod___closed__1); -l_Lean_Parser_Command_relaxedInferMod___closed__2 = _init_l_Lean_Parser_Command_relaxedInferMod___closed__2(); -lean_mark_persistent(l_Lean_Parser_Command_relaxedInferMod___closed__2); -l_Lean_Parser_Command_relaxedInferMod___closed__3 = _init_l_Lean_Parser_Command_relaxedInferMod___closed__3(); -lean_mark_persistent(l_Lean_Parser_Command_relaxedInferMod___closed__3); -l_Lean_Parser_Command_relaxedInferMod___closed__4 = _init_l_Lean_Parser_Command_relaxedInferMod___closed__4(); -lean_mark_persistent(l_Lean_Parser_Command_relaxedInferMod___closed__4); -l_Lean_Parser_Command_relaxedInferMod___closed__5 = _init_l_Lean_Parser_Command_relaxedInferMod___closed__5(); -lean_mark_persistent(l_Lean_Parser_Command_relaxedInferMod___closed__5); -l_Lean_Parser_Command_relaxedInferMod = _init_l_Lean_Parser_Command_relaxedInferMod(); -lean_mark_persistent(l_Lean_Parser_Command_relaxedInferMod); -l_Lean_Parser_Command_strictInferMod___elambda__1___closed__1 = _init_l_Lean_Parser_Command_strictInferMod___elambda__1___closed__1(); -lean_mark_persistent(l_Lean_Parser_Command_strictInferMod___elambda__1___closed__1); -l_Lean_Parser_Command_strictInferMod___elambda__1___closed__2 = _init_l_Lean_Parser_Command_strictInferMod___elambda__1___closed__2(); -lean_mark_persistent(l_Lean_Parser_Command_strictInferMod___elambda__1___closed__2); -l_Lean_Parser_Command_strictInferMod___elambda__1___closed__3 = _init_l_Lean_Parser_Command_strictInferMod___elambda__1___closed__3(); -lean_mark_persistent(l_Lean_Parser_Command_strictInferMod___elambda__1___closed__3); -l_Lean_Parser_Command_strictInferMod___elambda__1___closed__4 = _init_l_Lean_Parser_Command_strictInferMod___elambda__1___closed__4(); -lean_mark_persistent(l_Lean_Parser_Command_strictInferMod___elambda__1___closed__4); -l_Lean_Parser_Command_strictInferMod___closed__1 = _init_l_Lean_Parser_Command_strictInferMod___closed__1(); -lean_mark_persistent(l_Lean_Parser_Command_strictInferMod___closed__1); -l_Lean_Parser_Command_strictInferMod___closed__2 = _init_l_Lean_Parser_Command_strictInferMod___closed__2(); -lean_mark_persistent(l_Lean_Parser_Command_strictInferMod___closed__2); -l_Lean_Parser_Command_strictInferMod___closed__3 = _init_l_Lean_Parser_Command_strictInferMod___closed__3(); -lean_mark_persistent(l_Lean_Parser_Command_strictInferMod___closed__3); -l_Lean_Parser_Command_strictInferMod___closed__4 = _init_l_Lean_Parser_Command_strictInferMod___closed__4(); -lean_mark_persistent(l_Lean_Parser_Command_strictInferMod___closed__4); -l_Lean_Parser_Command_strictInferMod___closed__5 = _init_l_Lean_Parser_Command_strictInferMod___closed__5(); -lean_mark_persistent(l_Lean_Parser_Command_strictInferMod___closed__5); -l_Lean_Parser_Command_strictInferMod = _init_l_Lean_Parser_Command_strictInferMod(); -lean_mark_persistent(l_Lean_Parser_Command_strictInferMod); +l_Lean_Parser_Command_inferMod___elambda__1___closed__1 = _init_l_Lean_Parser_Command_inferMod___elambda__1___closed__1(); +lean_mark_persistent(l_Lean_Parser_Command_inferMod___elambda__1___closed__1); +l_Lean_Parser_Command_inferMod___elambda__1___closed__2 = _init_l_Lean_Parser_Command_inferMod___elambda__1___closed__2(); +lean_mark_persistent(l_Lean_Parser_Command_inferMod___elambda__1___closed__2); +l_Lean_Parser_Command_inferMod___elambda__1___closed__3 = _init_l_Lean_Parser_Command_inferMod___elambda__1___closed__3(); +lean_mark_persistent(l_Lean_Parser_Command_inferMod___elambda__1___closed__3); +l_Lean_Parser_Command_inferMod___elambda__1___closed__4 = _init_l_Lean_Parser_Command_inferMod___elambda__1___closed__4(); +lean_mark_persistent(l_Lean_Parser_Command_inferMod___elambda__1___closed__4); l_Lean_Parser_Command_inferMod___closed__1 = _init_l_Lean_Parser_Command_inferMod___closed__1(); lean_mark_persistent(l_Lean_Parser_Command_inferMod___closed__1); l_Lean_Parser_Command_inferMod___closed__2 = _init_l_Lean_Parser_Command_inferMod___closed__2(); lean_mark_persistent(l_Lean_Parser_Command_inferMod___closed__2); l_Lean_Parser_Command_inferMod___closed__3 = _init_l_Lean_Parser_Command_inferMod___closed__3(); lean_mark_persistent(l_Lean_Parser_Command_inferMod___closed__3); +l_Lean_Parser_Command_inferMod___closed__4 = _init_l_Lean_Parser_Command_inferMod___closed__4(); +lean_mark_persistent(l_Lean_Parser_Command_inferMod___closed__4); +l_Lean_Parser_Command_inferMod___closed__5 = _init_l_Lean_Parser_Command_inferMod___closed__5(); +lean_mark_persistent(l_Lean_Parser_Command_inferMod___closed__5); l_Lean_Parser_Command_inferMod = _init_l_Lean_Parser_Command_inferMod(); lean_mark_persistent(l_Lean_Parser_Command_inferMod); l_Lean_Parser_Command_introRule___elambda__1___closed__1 = _init_l_Lean_Parser_Command_introRule___elambda__1___closed__1(); diff --git a/stage0/stdlib/Init/Lean/Util/Path.c b/stage0/stdlib/Init/Lean/Util/Path.c index 6ec6fd53e4..c2755429db 100644 --- a/stage0/stdlib/Init/Lean/Util/Path.c +++ b/stage0/stdlib/Init/Lean/Util/Path.c @@ -47,10 +47,12 @@ lean_object* l_Lean_findOLean(lean_object*, lean_object*); lean_object* lean_nat_add(lean_object*, lean_object*); lean_object* l_Lean_modPathToFilePath___main___closed__1; lean_object* l_Lean_modPathToFilePath___main(lean_object*); +lean_object* l_IO_currentDir___at_Lean_moduleNameOfFileName___spec__1(lean_object*); 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; lean_object* l_List_foldlM___main___at_Lean_parseSearchPath___spec__8(lean_object*, lean_object*, lean_object*); @@ -69,6 +71,7 @@ extern lean_object* l_List_reprAux___main___rarg___closed__1; 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*); @@ -83,10 +86,12 @@ lean_object* l_mkHashMapImp___rarg(lean_object*); lean_object* l_Lean_findAtSearchPath___closed__2; lean_object* l_IO_getEnv___at_Lean_addSearchPathFromEnv___spec__1(lean_object*, lean_object*); lean_object* lean_init_search_path(lean_object*, lean_object*); +lean_object* l_List_foldl___main___at_Lean_moduleNameOfFileName___spec__2(lean_object*, lean_object*); +lean_object* l_Lean_moduleNameOfFileName___closed__3; lean_object* l_Lean_splitAtRoot(lean_object*); +extern lean_object* l_Option_HasRepr___rarg___closed__3; lean_object* l_Lean_findOLean___closed__1; uint8_t l_UInt32_decEq(uint32_t, uint32_t); -lean_object* l_List_foldl___main___at_Lean_moduleNameOfFileName___spec__1(lean_object*, lean_object*); 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; @@ -122,7 +127,7 @@ 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* lean_normalize_module_name(lean_object*); +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*); @@ -2306,7 +2311,15 @@ lean_dec(x_1); return x_7; } } -lean_object* l_List_foldl___main___at_Lean_moduleNameOfFileName___spec__1(lean_object* x_1, lean_object* x_2) { +lean_object* l_IO_currentDir___at_Lean_moduleNameOfFileName___spec__1(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_io_current_dir(x_1); +return x_2; +} +} +lean_object* l_List_foldl___main___at_Lean_moduleNameOfFileName___spec__2(lean_object* x_1, lean_object* x_2) { _start: { if (lean_obj_tag(x_2) == 0) @@ -2332,7 +2345,7 @@ lean_object* _init_l_Lean_moduleNameOfFileName___closed__1() { _start: { lean_object* x_1; -x_1 = lean_mk_string("failed to convert file '"); +x_1 = lean_mk_string("failed to convert file name '"); return x_1; } } @@ -2344,259 +2357,278 @@ x_1 = lean_mk_string("' to module name, extension is missing"); return x_1; } } +lean_object* _init_l_Lean_moduleNameOfFileName___closed__3() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("input file '"); +return x_1; +} +} +lean_object* _init_l_Lean_moduleNameOfFileName___closed__4() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("' must be contained in current directory ("); +return x_1; +} +} lean_object* lean_module_name_of_file(lean_object* x_1, lean_object* x_2) { _start: { lean_object* x_3; -lean_inc(x_1); -x_3 = l_Lean_findAtSearchPath(x_1, x_2); +x_3 = l_Lean_realPathNormalized(x_1, x_2); if (lean_obj_tag(x_3) == 0) { -lean_object* x_4; +lean_object* x_4; lean_object* x_5; lean_object* x_6; x_4 = lean_ctor_get(x_3, 0); lean_inc(x_4); -if (lean_obj_tag(x_4) == 0) +x_5 = lean_ctor_get(x_3, 1); +lean_inc(x_5); +lean_dec(x_3); +x_6 = lean_io_current_dir(x_5); +if (lean_obj_tag(x_6) == 0) { -uint8_t x_5; -lean_dec(x_1); -x_5 = !lean_is_exclusive(x_3); -if (x_5 == 0) -{ -lean_object* x_6; lean_object* x_7; -x_6 = lean_ctor_get(x_3, 0); -lean_dec(x_6); -x_7 = lean_box(0); -lean_ctor_set(x_3, 0, x_7); -return x_3; -} -else -{ -lean_object* x_8; lean_object* x_9; lean_object* x_10; -x_8 = lean_ctor_get(x_3, 1); +lean_object* x_7; lean_object* x_8; lean_object* x_9; +x_7 = lean_ctor_get(x_6, 0); +lean_inc(x_7); +x_8 = lean_ctor_get(x_6, 1); lean_inc(x_8); -lean_dec(x_3); -x_9 = lean_box(0); -x_10 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_10, 0, x_9); -lean_ctor_set(x_10, 1, x_8); -return x_10; -} -} -else +lean_dec(x_6); +x_9 = l_Lean_realPathNormalized(x_7, x_8); +if (lean_obj_tag(x_9) == 0) { -lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; -x_11 = lean_ctor_get(x_4, 0); +lean_object* x_10; lean_object* x_11; lean_object* x_12; uint8_t x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; uint32_t x_17; uint32_t x_18; uint8_t x_19; uint8_t x_20; +x_10 = lean_ctor_get(x_9, 0); +lean_inc(x_10); +x_11 = lean_ctor_get(x_9, 1); lean_inc(x_11); -lean_dec(x_4); -x_12 = lean_ctor_get(x_3, 1); -lean_inc(x_12); -lean_dec(x_3); -x_13 = lean_ctor_get(x_11, 0); -lean_inc(x_13); -x_14 = lean_ctor_get(x_11, 1); -lean_inc(x_14); -lean_dec(x_11); -x_15 = l_Lean_realPathNormalized(x_1, x_12); -if (lean_obj_tag(x_15) == 0) -{ -lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; uint32_t x_22; uint32_t x_23; uint8_t x_24; uint32_t x_25; uint8_t x_26; -x_16 = lean_ctor_get(x_15, 0); -lean_inc(x_16); -x_17 = lean_ctor_get(x_15, 1); -lean_inc(x_17); -if (lean_is_exclusive(x_15)) { - lean_ctor_release(x_15, 0); - lean_ctor_release(x_15, 1); - x_18 = x_15; +if (lean_is_exclusive(x_9)) { + lean_ctor_release(x_9, 0); + lean_ctor_release(x_9, 1); + x_12 = x_9; } else { - lean_dec_ref(x_15); - x_18 = lean_box(0); + lean_dec_ref(x_9); + x_12 = lean_box(0); } -x_19 = lean_string_length(x_14); +x_13 = l_String_isPrefixOf(x_10, x_4); +x_14 = lean_string_length(x_10); +x_15 = l_String_drop(x_4, x_14); lean_dec(x_14); -x_20 = l_String_drop(x_16, x_19); -lean_dec(x_19); -x_21 = lean_unsigned_to_nat(0u); -x_22 = lean_string_utf8_get(x_20, x_21); -x_23 = l_System_FilePath_pathSeparator; -x_24 = x_22 == x_23; -x_25 = 46; -if (x_24 == 0) +x_16 = lean_unsigned_to_nat(0u); +x_17 = lean_string_utf8_get(x_15, x_16); +x_18 = l_System_FilePath_pathSeparator; +x_19 = x_17 == x_18; +if (x_13 == 0) { uint8_t x_80; -x_80 = 0; -x_26 = x_80; +x_80 = 1; +x_20 = x_80; goto block_79; } else { uint8_t x_81; -x_81 = 1; -x_26 = x_81; +x_81 = 0; +x_20 = x_81; goto block_79; } block_79: { -if (x_26 == 0) +uint8_t x_21; +if (x_20 == 0) { -lean_object* x_27; -x_27 = l_String_revPosOf(x_20, x_25); -if (lean_obj_tag(x_27) == 0) -{ -lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; -lean_dec(x_20); -lean_dec(x_13); -x_28 = l_Lean_moduleNameOfFileName___closed__1; -x_29 = lean_string_append(x_28, x_16); -lean_dec(x_16); -x_30 = l_Lean_moduleNameOfFileName___closed__2; -x_31 = lean_string_append(x_29, x_30); -x_32 = lean_alloc_ctor(18, 1, 0); -lean_ctor_set(x_32, 0, x_31); -if (lean_is_scalar(x_18)) { - x_33 = lean_alloc_ctor(1, 2, 0); -} else { - x_33 = x_18; - lean_ctor_set_tag(x_33, 1); -} -lean_ctor_set(x_33, 0, x_32); -lean_ctor_set(x_33, 1, x_17); -return x_33; +uint8_t x_77; +x_77 = 0; +x_21 = x_77; +goto block_76; } else { -uint8_t x_34; -lean_dec(x_16); -x_34 = !lean_is_exclusive(x_27); -if (x_34 == 0) -{ -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; -x_35 = lean_ctor_get(x_27, 0); -x_36 = lean_string_utf8_extract(x_20, x_21, x_35); -lean_dec(x_35); -lean_dec(x_20); -x_37 = l___private_Init_Lean_Util_Path_1__pathSep; -x_38 = l_String_splitOn(x_36, x_37); -x_39 = lean_box(0); -x_40 = lean_name_mk_string(x_39, x_13); -x_41 = l_List_foldl___main___at_Lean_moduleNameOfFileName___spec__1(x_40, x_38); -lean_ctor_set(x_27, 0, x_41); -if (lean_is_scalar(x_18)) { - x_42 = lean_alloc_ctor(0, 2, 0); -} else { - x_42 = x_18; +uint8_t x_78; +x_78 = 1; +x_21 = x_78; +goto block_76; } -lean_ctor_set(x_42, 0, x_27); -lean_ctor_set(x_42, 1, x_17); -return x_42; +block_76: +{ +uint8_t x_22; +if (x_19 == 0) +{ +uint8_t x_74; +x_74 = 0; +x_22 = x_74; +goto block_73; } else { -lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; -x_43 = lean_ctor_get(x_27, 0); -lean_inc(x_43); -lean_dec(x_27); -x_44 = lean_string_utf8_extract(x_20, x_21, x_43); -lean_dec(x_43); -lean_dec(x_20); -x_45 = l___private_Init_Lean_Util_Path_1__pathSep; -x_46 = l_String_splitOn(x_44, x_45); -x_47 = lean_box(0); -x_48 = lean_name_mk_string(x_47, x_13); -x_49 = l_List_foldl___main___at_Lean_moduleNameOfFileName___spec__1(x_48, x_46); -x_50 = lean_alloc_ctor(1, 1, 0); -lean_ctor_set(x_50, 0, x_49); -if (lean_is_scalar(x_18)) { - x_51 = lean_alloc_ctor(0, 2, 0); +uint8_t x_75; +x_75 = 1; +x_22 = x_75; +goto block_73; +} +block_73: +{ +if (x_22 == 0) +{ +if (x_21 == 0) +{ +uint32_t x_23; lean_object* x_24; +lean_dec(x_10); +x_23 = 46; +x_24 = l_String_revPosOf(x_15, x_23); +if (lean_obj_tag(x_24) == 0) +{ +lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; +lean_dec(x_15); +x_25 = l_Lean_moduleNameOfFileName___closed__1; +x_26 = lean_string_append(x_25, x_4); +lean_dec(x_4); +x_27 = l_Lean_moduleNameOfFileName___closed__2; +x_28 = lean_string_append(x_26, x_27); +x_29 = lean_alloc_ctor(18, 1, 0); +lean_ctor_set(x_29, 0, x_28); +if (lean_is_scalar(x_12)) { + x_30 = lean_alloc_ctor(1, 2, 0); } else { - x_51 = x_18; + x_30 = x_12; + lean_ctor_set_tag(x_30, 1); } -lean_ctor_set(x_51, 0, x_50); -lean_ctor_set(x_51, 1, x_17); -return x_51; +lean_ctor_set(x_30, 0, x_29); +lean_ctor_set(x_30, 1, x_11); +return x_30; } +else +{ +lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; +lean_dec(x_4); +x_31 = lean_ctor_get(x_24, 0); +lean_inc(x_31); +lean_dec(x_24); +x_32 = lean_string_utf8_extract(x_15, x_16, x_31); +lean_dec(x_31); +lean_dec(x_15); +x_33 = l___private_Init_Lean_Util_Path_1__pathSep; +x_34 = l_String_splitOn(x_32, x_33); +x_35 = lean_box(0); +x_36 = l_List_foldl___main___at_Lean_moduleNameOfFileName___spec__2(x_35, x_34); +if (lean_is_scalar(x_12)) { + x_37 = lean_alloc_ctor(0, 2, 0); +} else { + x_37 = x_12; +} +lean_ctor_set(x_37, 0, x_36); +lean_ctor_set(x_37, 1, x_11); +return x_37; } } else { -lean_object* x_52; lean_object* x_53; lean_object* x_54; -x_52 = lean_unsigned_to_nat(1u); -x_53 = l_String_drop(x_20, x_52); -lean_dec(x_20); -x_54 = l_String_revPosOf(x_53, x_25); -if (lean_obj_tag(x_54) == 0) -{ -lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; -lean_dec(x_53); -lean_dec(x_13); -x_55 = l_Lean_moduleNameOfFileName___closed__1; -x_56 = lean_string_append(x_55, x_16); -lean_dec(x_16); -x_57 = l_Lean_moduleNameOfFileName___closed__2; -x_58 = lean_string_append(x_56, x_57); -x_59 = lean_alloc_ctor(18, 1, 0); -lean_ctor_set(x_59, 0, x_58); -if (lean_is_scalar(x_18)) { - x_60 = lean_alloc_ctor(1, 2, 0); +lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; +lean_dec(x_15); +x_38 = l_Lean_moduleNameOfFileName___closed__3; +x_39 = lean_string_append(x_38, x_4); +lean_dec(x_4); +x_40 = l_Lean_moduleNameOfFileName___closed__4; +x_41 = lean_string_append(x_39, x_40); +x_42 = lean_string_append(x_41, x_10); +lean_dec(x_10); +x_43 = l_Option_HasRepr___rarg___closed__3; +x_44 = lean_string_append(x_42, x_43); +x_45 = lean_alloc_ctor(18, 1, 0); +lean_ctor_set(x_45, 0, x_44); +if (lean_is_scalar(x_12)) { + x_46 = lean_alloc_ctor(1, 2, 0); } else { - x_60 = x_18; - lean_ctor_set_tag(x_60, 1); + x_46 = x_12; + lean_ctor_set_tag(x_46, 1); +} +lean_ctor_set(x_46, 0, x_45); +lean_ctor_set(x_46, 1, x_11); +return x_46; } -lean_ctor_set(x_60, 0, x_59); -lean_ctor_set(x_60, 1, x_17); -return x_60; } else { -uint8_t x_61; -lean_dec(x_16); -x_61 = !lean_is_exclusive(x_54); -if (x_61 == 0) +if (x_21 == 0) { -lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; -x_62 = lean_ctor_get(x_54, 0); -x_63 = lean_string_utf8_extract(x_53, x_21, x_62); -lean_dec(x_62); -lean_dec(x_53); -x_64 = l___private_Init_Lean_Util_Path_1__pathSep; -x_65 = l_String_splitOn(x_63, x_64); -x_66 = lean_box(0); -x_67 = lean_name_mk_string(x_66, x_13); -x_68 = l_List_foldl___main___at_Lean_moduleNameOfFileName___spec__1(x_67, x_65); -lean_ctor_set(x_54, 0, x_68); -if (lean_is_scalar(x_18)) { - x_69 = lean_alloc_ctor(0, 2, 0); +lean_object* x_47; lean_object* x_48; uint32_t x_49; lean_object* x_50; +lean_dec(x_10); +x_47 = lean_unsigned_to_nat(1u); +x_48 = l_String_drop(x_15, x_47); +lean_dec(x_15); +x_49 = 46; +x_50 = l_String_revPosOf(x_48, x_49); +if (lean_obj_tag(x_50) == 0) +{ +lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; +lean_dec(x_48); +x_51 = l_Lean_moduleNameOfFileName___closed__1; +x_52 = lean_string_append(x_51, x_4); +lean_dec(x_4); +x_53 = l_Lean_moduleNameOfFileName___closed__2; +x_54 = lean_string_append(x_52, x_53); +x_55 = lean_alloc_ctor(18, 1, 0); +lean_ctor_set(x_55, 0, x_54); +if (lean_is_scalar(x_12)) { + x_56 = lean_alloc_ctor(1, 2, 0); } else { - x_69 = x_18; + x_56 = x_12; + lean_ctor_set_tag(x_56, 1); } -lean_ctor_set(x_69, 0, x_54); -lean_ctor_set(x_69, 1, x_17); -return x_69; +lean_ctor_set(x_56, 0, x_55); +lean_ctor_set(x_56, 1, x_11); +return x_56; } else { -lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; -x_70 = lean_ctor_get(x_54, 0); -lean_inc(x_70); -lean_dec(x_54); -x_71 = lean_string_utf8_extract(x_53, x_21, x_70); -lean_dec(x_70); -lean_dec(x_53); -x_72 = l___private_Init_Lean_Util_Path_1__pathSep; -x_73 = l_String_splitOn(x_71, x_72); -x_74 = lean_box(0); -x_75 = lean_name_mk_string(x_74, x_13); -x_76 = l_List_foldl___main___at_Lean_moduleNameOfFileName___spec__1(x_75, x_73); -x_77 = lean_alloc_ctor(1, 1, 0); -lean_ctor_set(x_77, 0, x_76); -if (lean_is_scalar(x_18)) { - x_78 = lean_alloc_ctor(0, 2, 0); +lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; +lean_dec(x_4); +x_57 = lean_ctor_get(x_50, 0); +lean_inc(x_57); +lean_dec(x_50); +x_58 = lean_string_utf8_extract(x_48, x_16, x_57); +lean_dec(x_57); +lean_dec(x_48); +x_59 = l___private_Init_Lean_Util_Path_1__pathSep; +x_60 = l_String_splitOn(x_58, x_59); +x_61 = lean_box(0); +x_62 = l_List_foldl___main___at_Lean_moduleNameOfFileName___spec__2(x_61, x_60); +if (lean_is_scalar(x_12)) { + x_63 = lean_alloc_ctor(0, 2, 0); } else { - x_78 = x_18; + x_63 = x_12; +} +lean_ctor_set(x_63, 0, x_62); +lean_ctor_set(x_63, 1, x_11); +return x_63; +} +} +else +{ +lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; +lean_dec(x_15); +x_64 = l_Lean_moduleNameOfFileName___closed__3; +x_65 = lean_string_append(x_64, x_4); +lean_dec(x_4); +x_66 = l_Lean_moduleNameOfFileName___closed__4; +x_67 = lean_string_append(x_65, x_66); +x_68 = lean_string_append(x_67, x_10); +lean_dec(x_10); +x_69 = l_Option_HasRepr___rarg___closed__3; +x_70 = lean_string_append(x_68, x_69); +x_71 = lean_alloc_ctor(18, 1, 0); +lean_ctor_set(x_71, 0, x_70); +if (lean_is_scalar(x_12)) { + x_72 = lean_alloc_ctor(1, 2, 0); +} else { + x_72 = x_12; + lean_ctor_set_tag(x_72, 1); +} +lean_ctor_set(x_72, 0, x_71); +lean_ctor_set(x_72, 1, x_11); +return x_72; } -lean_ctor_set(x_78, 0, x_77); -lean_ctor_set(x_78, 1, x_17); -return x_78; } } } @@ -2605,21 +2637,20 @@ return x_78; else { uint8_t x_82; -lean_dec(x_14); -lean_dec(x_13); -x_82 = !lean_is_exclusive(x_15); +lean_dec(x_4); +x_82 = !lean_is_exclusive(x_9); if (x_82 == 0) { -return x_15; +return x_9; } else { lean_object* x_83; lean_object* x_84; lean_object* x_85; -x_83 = lean_ctor_get(x_15, 0); -x_84 = lean_ctor_get(x_15, 1); +x_83 = lean_ctor_get(x_9, 0); +x_84 = lean_ctor_get(x_9, 1); lean_inc(x_84); lean_inc(x_83); -lean_dec(x_15); +lean_dec(x_9); x_85 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_85, 0, x_83); lean_ctor_set(x_85, 1, x_84); @@ -2627,28 +2658,50 @@ return x_85; } } } -} else { uint8_t x_86; -lean_dec(x_1); -x_86 = !lean_is_exclusive(x_3); +lean_dec(x_4); +x_86 = !lean_is_exclusive(x_6); if (x_86 == 0) { +return x_6; +} +else +{ +lean_object* x_87; lean_object* x_88; lean_object* x_89; +x_87 = lean_ctor_get(x_6, 0); +x_88 = lean_ctor_get(x_6, 1); +lean_inc(x_88); +lean_inc(x_87); +lean_dec(x_6); +x_89 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_89, 0, x_87); +lean_ctor_set(x_89, 1, x_88); +return x_89; +} +} +} +else +{ +uint8_t x_90; +x_90 = !lean_is_exclusive(x_3); +if (x_90 == 0) +{ return x_3; } else { -lean_object* x_87; lean_object* x_88; lean_object* x_89; -x_87 = lean_ctor_get(x_3, 0); -x_88 = lean_ctor_get(x_3, 1); -lean_inc(x_88); -lean_inc(x_87); +lean_object* x_91; lean_object* x_92; lean_object* x_93; +x_91 = lean_ctor_get(x_3, 0); +x_92 = lean_ctor_get(x_3, 1); +lean_inc(x_92); +lean_inc(x_91); lean_dec(x_3); -x_89 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_89, 0, x_87); -lean_ctor_set(x_89, 1, x_88); -return x_89; +x_93 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_93, 0, x_91); +lean_ctor_set(x_93, 1, x_92); +return x_93; } } } @@ -2671,7 +2724,7 @@ x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -lean_object* lean_normalize_module_name(lean_object* x_1) { +lean_object* l_Lean_normalizeModuleName(lean_object* x_1) { _start: { if (lean_obj_tag(x_1) == 1) @@ -2790,6 +2843,10 @@ l_Lean_moduleNameOfFileName___closed__1 = _init_l_Lean_moduleNameOfFileName___cl lean_mark_persistent(l_Lean_moduleNameOfFileName___closed__1); l_Lean_moduleNameOfFileName___closed__2 = _init_l_Lean_moduleNameOfFileName___closed__2(); lean_mark_persistent(l_Lean_moduleNameOfFileName___closed__2); +l_Lean_moduleNameOfFileName___closed__3 = _init_l_Lean_moduleNameOfFileName___closed__3(); +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(); diff --git a/stage0/stdlib/Init/System/IO.c b/stage0/stdlib/Init/System/IO.c index 54c7272282..8893e992c4 100644 --- a/stage0/stdlib/Init/System/IO.c +++ b/stage0/stdlib/Init/System/IO.c @@ -33,6 +33,7 @@ lean_object* l_IO_Prim_getEnv___boxed(lean_object*, lean_object*); lean_object* lean_io_prim_put_str(lean_object*, lean_object*); lean_object* l_IO_println(lean_object*); lean_object* l_Lean_Unit_hasEval(lean_object*); +lean_object* l_IO_currentDir___rarg___closed__1; lean_object* l_IO_Prim_fopenFlags___closed__12; lean_object* l_EIO_Monad___closed__1; lean_object* l_IO_FS_Handle_read___boxed(lean_object*, lean_object*); @@ -110,6 +111,7 @@ lean_object* l_IO_FS_Handle_read___rarg___boxed(lean_object*, lean_object*, lean lean_object* l_IO_Prim_liftIO___rarg(lean_object*, lean_object*); lean_object* l_IO_println___at_Lean_HasRepr_hasEval___spec__1(lean_object*, lean_object*); uint32_t l_IO_AccessRight_flags___closed__4; +lean_object* lean_io_current_dir(lean_object*); lean_object* l_EIO_MonadExcept(lean_object*); lean_object* l_IO_Prim_fopenFlags___closed__10; lean_object* l_IO_Ref_reset___rarg(lean_object*, lean_object*, lean_object*); @@ -173,6 +175,7 @@ lean_object* lean_io_file_exists(lean_object*, lean_object*); lean_object* l_Lean_IO_HasEval(lean_object*); lean_object* l_EStateM_nonBacktrackable(lean_object*); uint8_t l_UInt32_decEq(uint32_t, uint32_t); +lean_object* l_IO_currentDir(lean_object*, lean_object*); lean_object* l_IO_Prim_isDir___boxed(lean_object*, lean_object*); lean_object* l_IO_FS_Handle_putStr(lean_object*, lean_object*); lean_object* l_IO_Prim_setAccessRights___boxed(lean_object*, lean_object*, lean_object*); @@ -185,6 +188,7 @@ lean_object* l_EStateM_Monad(lean_object*, lean_object*); lean_object* l_IO_FS_Handle_mk___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_MonadExcept_orelse___at_EIO_HasOrelse___spec__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* lean_io_ref_ptr_eq(lean_object*, lean_object*, lean_object*); +lean_object* l_IO_Prim_currentDir___boxed(lean_object*); lean_object* l_IO_FS_Handle_write___boxed(lean_object*, lean_object*); lean_object* l_IO_Prim_fopenFlags___closed__5; lean_object* l_IO_Prim_fopenFlags___closed__14; @@ -237,6 +241,7 @@ lean_object* lean_io_app_dir(lean_object*); lean_object* l_IO_FS_Handle_isEof___rarg(lean_object*, lean_object*); lean_object* l_IO_FS_Handle_flush(lean_object*, lean_object*); uint32_t l_IO_AccessRight_flags___closed__12; +lean_object* l_IO_currentDir___boxed(lean_object*, lean_object*); lean_object* l_IO_Prim_fopenFlags___boxed(lean_object*, lean_object*); lean_object* l_IO_mkRef___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_HasRepr_hasEval___rarg(lean_object*, lean_object*, uint8_t, lean_object*); @@ -255,6 +260,7 @@ lean_object* l___private_Init_System_IO_1__putStr___rarg(lean_object*, lean_obje uint32_t l_IO_AccessRight_flags___closed__5; lean_object* lean_io_prim_handle_mk(lean_object*, lean_object*, lean_object*); lean_object* l_IO_appDir___rarg(lean_object*, lean_object*); +lean_object* l_IO_currentDir___rarg(lean_object*); lean_object* l_IO_Prim_iterate___main___rarg(lean_object*, lean_object*, lean_object*); uint32_t l_IO_AccessRight_flags___closed__7; uint32_t l_IO_FileRight_flags(lean_object*); @@ -1057,6 +1063,14 @@ x_2 = lean_io_app_dir(x_1); return x_2; } } +lean_object* l_IO_Prim_currentDir___boxed(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_io_current_dir(x_1); +return x_2; +} +} lean_object* l_IO_Prim_liftIO___rarg(lean_object* x_1, lean_object* x_2) { _start: { @@ -1302,6 +1316,40 @@ lean_dec(x_2); return x_3; } } +lean_object* _init_l_IO_currentDir___rarg___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_IO_Prim_currentDir___boxed), 1, 0); +return x_1; +} +} +lean_object* l_IO_currentDir___rarg(lean_object* x_1) { +_start: +{ +lean_object* x_2; lean_object* x_3; +x_2 = l_IO_currentDir___rarg___closed__1; +x_3 = lean_apply_2(x_1, lean_box(0), x_2); +return x_3; +} +} +lean_object* l_IO_currentDir(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = lean_alloc_closure((void*)(l_IO_currentDir___rarg), 1, 0); +return x_3; +} +} +lean_object* l_IO_currentDir___boxed(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = l_IO_currentDir(x_1, x_2); +lean_dec(x_2); +return x_3; +} +} lean_object* l_IO_appDir___rarg___lambda__1(lean_object* x_1, lean_object* x_2) { _start: { @@ -2903,6 +2951,8 @@ l_IO_println___rarg___closed__1 = _init_l_IO_println___rarg___closed__1(); lean_mark_persistent(l_IO_println___rarg___closed__1); l_IO_appPath___rarg___closed__1 = _init_l_IO_appPath___rarg___closed__1(); lean_mark_persistent(l_IO_appPath___rarg___closed__1); +l_IO_currentDir___rarg___closed__1 = _init_l_IO_currentDir___rarg___closed__1(); +lean_mark_persistent(l_IO_currentDir___rarg___closed__1); l_IO_AccessRight_flags___closed__1 = _init_l_IO_AccessRight_flags___closed__1(); l_IO_AccessRight_flags___closed__2 = _init_l_IO_AccessRight_flags___closed__2(); l_IO_AccessRight_flags___closed__3 = _init_l_IO_AccessRight_flags___closed__3();