max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: update stage0

Browse source
This commit is contained in:
Sebastian Ullrich 2020-05-14 14:46:18 +02:00
parent 872d5fc7ba
commit 81784b145e
16 changed files with 459 additions and 1164 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
stage0/src/CMakeLists.txt
View file

@ -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"

4
stage0/src/Init/Lean/Parser/Command.lean
View file

@ -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

4
stage0/src/Init/Lean/PrettyPrinter/Parenthesizer.lean
View file

@ -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.

15
stage0/src/Init/Lean/Util/Path.lean
View file

@ -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

3
stage0/src/Init/System/IO.lean
View file

@ -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;

12
stage0/src/Init/Makefile.in → stage0/src/Makefile.in
View file

@ -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

6
stage0/src/frontends/lean/parser.cpp
View file

@ -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`

0
stage0/src/Init/relative.py → stage0/src/relative.py
View file

10
stage0/src/runtime/io.cpp
View file

@ -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) {

115
stage0/src/shell/CMakeLists.txt
View file

@ -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=$<TARGET_FILE:lean_stage0>"
"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 "$<TARGET_FILE:leanstdlib>" DESTINATION lib)
@ -28,11 +28,11 @@ if(NOT STAGE0)
set(PREV_LEAN "$<TARGET_FILE: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)

29
stage0/src/shell/lean.cpp
View file

@ -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<name> module_name_of_file(std::string const & fname) {
return get_io_result<option_ref<name>>(lean_module_name_of_file(mk_string(fname), io_mk_world())).get();
optional<name> 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<name>();
} else {
return some(get_io_result<name>(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<size_t>((atoi(optarg) / 4) * 4) * static_cast<size_t>(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";

2
stage0/stdlib/CMakeLists.txt
View file

File diff suppressed because one or more lines are too long

6
stage0/stdlib/Init/Lean/Elab/Import.c
View file

@ -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)
{

858
stage0/stdlib/Init/Lean/Parser/Command.c
View file

File diff suppressed because it is too large Load diff

503
stage0/stdlib/Init/Lean/Util/Path.c
View file

@ -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();

50
stage0/stdlib/Init/System/IO.c
View file

@ -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();