From e0fd89e1652155a6e337c445c77024fbf3d7ed23 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 15 Feb 2019 16:05:55 -0800 Subject: [PATCH] feat(library/init/lean/compiler): fold nat predicates --- library/init/lean/compiler/const_folding.lean | 54 +- library/init/lean/compiler/util.lean | 19 + library/init/lean/expr.lean | 18 +- library/init/lean/level.lean | 2 + src/boot/CMakeLists.txt | 2 +- src/boot/init/lean/compiler/const_folding.cpp | 1082 +++++++++++++---- src/boot/init/lean/compiler/util.cpp | 107 ++ src/boot/init/lean/expr.cpp | 75 +- src/boot/init/lean/level.cpp | 11 + src/library/compiler/csimp.cpp | 80 +- 10 files changed, 1094 insertions(+), 356 deletions(-) create mode 100644 library/init/lean/compiler/util.lean create mode 100644 src/boot/init/lean/compiler/util.cpp diff --git a/library/init/lean/compiler/const_folding.lean b/library/init/lean/compiler/const_folding.lean index a8c9ff741e..467f82fcd6 100644 --- a/library/init/lean/compiler/const_folding.lean +++ b/library/init/lean/compiler/const_folding.lean @@ -4,12 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ prelude -import init.lean.expr init.platform init.data.rbmap +import init.lean.expr init.platform +import init.lean.compiler.util /- Constant folding for primitives that have special runtime support. -/ namespace lean -namespace const_folding +namespace compiler def bin_fold_fn := bool → expr → expr → option expr @@ -67,22 +68,53 @@ def pre_uint_bin_fold_fns : list (name × bin_fold_fn) := def uint_bin_fold_fns : list (name × bin_fold_fn) := num_scalar_types.foldl (λ r info, r ++ (pre_uint_bin_fold_fns.map (λ ⟨suffix, fn⟩, (info.id ++ suffix, fn)))) [] -def fold_bin_nat (fn : nat → nat → nat) (a₁ a₂ : expr) : option expr := +def fold_nat_bin_op (fn : nat → nat → nat) (a₁ a₂ : expr) : option expr := do n₁ ← get_num_lit a₁, n₂ ← get_num_lit a₂, pure $ expr.lit (literal.nat_val (fn n₁ n₂)) -def fold_nat_add (_ : bool) := fold_bin_nat (+) -def fold_nat_mul (_ : bool) := fold_bin_nat (*) -def fold_nat_div (_ : bool) := fold_bin_nat (/) -def fold_nat_mod (_ : bool) := fold_bin_nat (%) +def fold_nat_add (_ : bool) := fold_nat_bin_op (+) +def fold_nat_mul (_ : bool) := fold_nat_bin_op (*) +def fold_nat_div (_ : bool) := fold_nat_bin_op (/) +def fold_nat_mod (_ : bool) := fold_nat_bin_op (%) -def bin_fold_fns : list (name × bin_fold_fn) := -uint_bin_fold_fns ++ +def mk_nat_eq (a b : expr) : expr := +mk_bin_app (expr.app (expr.const `eq [level.one]) (expr.const `nat [])) a b + +def mk_nat_lt (a b : expr) : expr := +mk_bin_app (mk_bin_app (expr.const `has_lt.lt [level.zero]) (expr.const `nat []) (expr.const `nat.has_lt [])) a b + +def mk_nat_le (a b : expr) : expr := +mk_bin_app (mk_bin_app (expr.const `has_lt.le [level.zero]) (expr.const `nat []) (expr.const `nat.has_le [])) a b + +def to_decidable_expr (before_erasure : bool) (pred : expr) (r : bool) : expr := +match before_erasure, r with +| ff, tt := mk_dec_is_true neutral_expr neutral_expr +| ff, ff := mk_dec_is_false neutral_expr neutral_expr +| tt, tt := mk_dec_is_true pred (mk_lc_proof pred) +| tt, ff := mk_dec_is_false pred (mk_lc_proof pred) + +def fold_nat_bin_pred (mk_pred : expr → expr → expr) (fn : nat → nat → bool) + (before_erasure : bool) (a₁ a₂ : expr) : option expr := +do n₁ ← get_num_lit a₁, + n₂ ← get_num_lit a₂, + pure $ to_decidable_expr before_erasure (mk_pred a₁ a₂) (fn n₁ n₂) + +def fold_nat_dec_eq := fold_nat_bin_pred mk_nat_eq (λ a b, a = b) +def fold_nat_dec_lt := fold_nat_bin_pred mk_nat_lt (λ a b, a < b) +def fold_nat_dec_le := fold_nat_bin_pred mk_nat_le (λ a b, a ≤ b) + +def nat_fold_fns : list (name × bin_fold_fn) := [(`nat.add, fold_nat_add), (`nat.mul, fold_nat_mul), (`nat.div, fold_nat_div), - (`nat.mod, fold_nat_mod)] + (`nat.mod, fold_nat_mod), + (`nat.dec_eq, fold_nat_dec_eq), + (`nat.dec_lt, fold_nat_dec_lt), + (`nat.dec_le, fold_nat_dec_le)] + +def bin_fold_fns : list (name × bin_fold_fn) := +uint_bin_fold_fns ++ nat_fold_fns def find_bin_fold_fn_aux (fn : name) : list (name × bin_fold_fn) → option bin_fold_fn | [] := none @@ -100,5 +132,5 @@ match f with fold_fn before_erasure a b | _ := none -end const_folding +end compiler end lean diff --git a/library/init/lean/compiler/util.lean b/library/init/lean/compiler/util.lean new file mode 100644 index 0000000000..478df8ba0f --- /dev/null +++ b/library/init/lean/compiler/util.lean @@ -0,0 +1,19 @@ +/- +Copyright (c) 2019 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +prelude +import init.lean.expr + +namespace lean +namespace compiler + +def neutral_expr : expr := expr.const `_neutral [] +def unreachable_expr : expr := expr.const `_unreachable [] +def object_type : expr := expr.const `_obj [] +def void_type : expr := expr.const `_void [] +def mk_lc_proof (pred : expr) := expr.app (expr.const `lc_proof []) pred + +end compiler +end lean diff --git a/library/init/lean/expr.lean b/library/init/lean/expr.lean index 2a2cb0f652..f90ecee012 100644 --- a/library/init/lean/expr.lean +++ b/library/init/lean/expr.lean @@ -79,9 +79,19 @@ protected def hash (n : @& expr) : usize := protected def dbg_to_string (e : @& expr) : string := "" -- dummy implementation -def get_app_fn : expr → expr -| (app f a) := get_app_fn f -| e := e - end expr + +def get_app_fn : expr → expr +| (expr.app f a) := get_app_fn f +| e := e + +def mk_bin_app (f a b : expr) := +expr.app (expr.app f a) b + +def mk_dec_is_true (pred proof : expr) := +mk_bin_app (expr.const `decidable.is_true []) pred proof + +def mk_dec_is_false (pred proof : expr) := +mk_bin_app (expr.const `decidable.is_false []) pred proof + end lean diff --git a/library/init/lean/level.lean b/library/init/lean/level.lean index e6c98ff34a..9cd2191e03 100644 --- a/library/init/lean/level.lean +++ b/library/init/lean/level.lean @@ -25,6 +25,8 @@ attribute [extern "level_mk_mvar"] level.mvar instance level_is_inhabited : inhabited level := ⟨level.zero⟩ +def level.one : level := level.succ level.zero + def level.has_param : level → bool | (level.param _) := tt | (level.succ l) := level.has_param l diff --git a/src/boot/CMakeLists.txt b/src/boot/CMakeLists.txt index b860c2a10c..8e68ace994 100644 --- a/src/boot/CMakeLists.txt +++ b/src/boot/CMakeLists.txt @@ -1 +1 @@ -add_library (boot OBJECT ./init/coe.cpp ./init/control/alternative.cpp ./init/control/applicative.cpp ./init/control/combinators.cpp ./init/control/coroutine.cpp ./init/control/default.cpp ./init/control/except.cpp ./init/control/functor.cpp ./init/control/id.cpp ./init/control/lift.cpp ./init/control/monad.cpp ./init/control/monad_fail.cpp ./init/control/option.cpp ./init/control/reader.cpp ./init/control/state.cpp ./init/core.cpp ./init/data/array/basic.cpp ./init/data/array/default.cpp ./init/data/basic.cpp ./init/data/char/basic.cpp ./init/data/char/default.cpp ./init/data/default.cpp ./init/data/dlist.cpp ./init/data/fin/basic.cpp ./init/data/fin/default.cpp ./init/data/hashable.cpp ./init/data/hashmap/basic.cpp ./init/data/int/basic.cpp ./init/data/int/default.cpp ./init/data/list/basic.cpp ./init/data/list/default.cpp ./init/data/list/instances.cpp ./init/data/nat/basic.cpp ./init/data/nat/default.cpp ./init/data/nat/div.cpp ./init/data/option/basic.cpp ./init/data/option/instances.cpp ./init/data/ordering/basic.cpp ./init/data/ordering/default.cpp ./init/data/rbmap/basic.cpp ./init/data/rbmap/default.cpp ./init/data/rbtree/basic.cpp ./init/data/rbtree/default.cpp ./init/data/repr.cpp ./init/data/string/basic.cpp ./init/data/string/default.cpp ./init/data/to_string.cpp ./init/data/uint.cpp ./init/data/usize.cpp ./init/default.cpp ./init/env_ext.cpp ./init/function.cpp ./init/io.cpp ./init/lean/compiler/const_folding.cpp ./init/lean/compiler/default.cpp ./init/lean/config.cpp ./init/lean/declaration.cpp ./init/lean/default.cpp ./init/lean/disjoint_set.cpp ./init/lean/elaborator.cpp ./init/lean/expander.cpp ./init/lean/expr.cpp ./init/lean/extern.cpp ./init/lean/format.cpp ./init/lean/frontend.cpp ./init/lean/ir/elim_phi.cpp ./init/lean/ir/extract_cpp.cpp ./init/lean/ir/format.cpp ./init/lean/ir/instances.cpp ./init/lean/ir/ir.cpp ./init/lean/ir/lirc.cpp ./init/lean/ir/parser.cpp ./init/lean/ir/reserved.cpp ./init/lean/ir/ssa_check.cpp ./init/lean/ir/type_check.cpp ./init/lean/kvmap.cpp ./init/lean/level.cpp ./init/lean/message.cpp ./init/lean/name.cpp ./init/lean/name_mangling.cpp ./init/lean/options.cpp ./init/lean/parser/basic.cpp ./init/lean/parser/combinators.cpp ./init/lean/parser/command.cpp ./init/lean/parser/declaration.cpp ./init/lean/parser/identifier.cpp ./init/lean/parser/level.cpp ./init/lean/parser/module.cpp ./init/lean/parser/notation.cpp ./init/lean/parser/parsec.cpp ./init/lean/parser/pratt.cpp ./init/lean/parser/rec.cpp ./init/lean/parser/string_literal.cpp ./init/lean/parser/syntax.cpp ./init/lean/parser/term.cpp ./init/lean/parser/token.cpp ./init/lean/parser/trie.cpp ./init/lean/position.cpp ./init/lean/trace.cpp ./init/platform.cpp ./init/wf.cpp) +add_library (boot OBJECT ./init/coe.cpp ./init/control/alternative.cpp ./init/control/applicative.cpp ./init/control/combinators.cpp ./init/control/coroutine.cpp ./init/control/default.cpp ./init/control/except.cpp ./init/control/functor.cpp ./init/control/id.cpp ./init/control/lift.cpp ./init/control/monad.cpp ./init/control/monad_fail.cpp ./init/control/option.cpp ./init/control/reader.cpp ./init/control/state.cpp ./init/core.cpp ./init/data/array/basic.cpp ./init/data/array/default.cpp ./init/data/basic.cpp ./init/data/char/basic.cpp ./init/data/char/default.cpp ./init/data/default.cpp ./init/data/dlist.cpp ./init/data/fin/basic.cpp ./init/data/fin/default.cpp ./init/data/hashable.cpp ./init/data/hashmap/basic.cpp ./init/data/int/basic.cpp ./init/data/int/default.cpp ./init/data/list/basic.cpp ./init/data/list/default.cpp ./init/data/list/instances.cpp ./init/data/nat/basic.cpp ./init/data/nat/default.cpp ./init/data/nat/div.cpp ./init/data/option/basic.cpp ./init/data/option/instances.cpp ./init/data/ordering/basic.cpp ./init/data/ordering/default.cpp ./init/data/rbmap/basic.cpp ./init/data/rbmap/default.cpp ./init/data/rbtree/basic.cpp ./init/data/rbtree/default.cpp ./init/data/repr.cpp ./init/data/string/basic.cpp ./init/data/string/default.cpp ./init/data/to_string.cpp ./init/data/uint.cpp ./init/data/usize.cpp ./init/default.cpp ./init/env_ext.cpp ./init/function.cpp ./init/io.cpp ./init/lean/compiler/const_folding.cpp ./init/lean/compiler/default.cpp ./init/lean/compiler/util.cpp ./init/lean/config.cpp ./init/lean/declaration.cpp ./init/lean/default.cpp ./init/lean/disjoint_set.cpp ./init/lean/elaborator.cpp ./init/lean/expander.cpp ./init/lean/expr.cpp ./init/lean/extern.cpp ./init/lean/format.cpp ./init/lean/frontend.cpp ./init/lean/ir/elim_phi.cpp ./init/lean/ir/extract_cpp.cpp ./init/lean/ir/format.cpp ./init/lean/ir/instances.cpp ./init/lean/ir/ir.cpp ./init/lean/ir/lirc.cpp ./init/lean/ir/parser.cpp ./init/lean/ir/reserved.cpp ./init/lean/ir/ssa_check.cpp ./init/lean/ir/type_check.cpp ./init/lean/kvmap.cpp ./init/lean/level.cpp ./init/lean/message.cpp ./init/lean/name.cpp ./init/lean/name_mangling.cpp ./init/lean/options.cpp ./init/lean/parser/basic.cpp ./init/lean/parser/combinators.cpp ./init/lean/parser/command.cpp ./init/lean/parser/declaration.cpp ./init/lean/parser/identifier.cpp ./init/lean/parser/level.cpp ./init/lean/parser/module.cpp ./init/lean/parser/notation.cpp ./init/lean/parser/parsec.cpp ./init/lean/parser/pratt.cpp ./init/lean/parser/rec.cpp ./init/lean/parser/string_literal.cpp ./init/lean/parser/syntax.cpp ./init/lean/parser/term.cpp ./init/lean/parser/token.cpp ./init/lean/parser/trie.cpp ./init/lean/position.cpp ./init/lean/trace.cpp ./init/platform.cpp ./init/wf.cpp) diff --git a/src/boot/init/lean/compiler/const_folding.cpp b/src/boot/init/lean/compiler/const_folding.cpp index 89d3c13d31..dc60fd80d7 100644 --- a/src/boot/init/lean/compiler/const_folding.cpp +++ b/src/boot/init/lean/compiler/const_folding.cpp @@ -1,6 +1,6 @@ // Lean compiler output // Module: init.lean.compiler.const_folding -// Imports: init.lean.expr init.platform init.data.rbmap.default +// Imports: init.lean.expr init.platform init.lean.compiler.util #include "runtime/object.h" #include "runtime/apply.h" typedef lean::object obj; typedef lean::usize usize; @@ -14,110 +14,156 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64; #pragma GCC diagnostic ignored "-Wunused-label" #pragma GCC diagnostic ignored "-Wunused-but-set-variable" #endif -namespace lean { -obj* fold_bin_op_core(uint8, obj*, obj*, obj*); -} +obj* l_lean_compiler_get__info__from__fn(obj*, obj*); +obj* l_lean_compiler_fold__uint__mul___lambda__1___boxed(obj*, obj*, obj*, obj*); +obj* l_lean_compiler_mk__nat__lt(obj*, obj*); +obj* l_lean_compiler_bin__fold__fns; obj* l_nat_mod___boxed(obj*, obj*); -obj* l_lean_const__folding_find__bin__fold__fn(obj*); -obj* l_lean_const__folding_bin__fold__fns; -obj* l_lean_const__folding_fold__nat__add___rarg___closed__1; -obj* l_lean_const__folding_fold__nat__mul(uint8); -namespace lean { -obj* get_num_lit_core(obj*); -} +obj* l_lean_compiler_fold__nat__add(uint8); +extern obj* l_lean_mk__dec__is__true___closed__1; +obj* l_lean_compiler_fold__nat__dec__lt___closed__2; +obj* l_lean_compiler_is__of__nat(obj*); +obj* l_lean_compiler_num__scalar__types; +obj* l_lean_compiler_mk__nat__eq___closed__1; namespace lean { obj* nat_add(obj*, obj*); } -obj* l_lean_const__folding_mk__uint__type__name(obj*); -obj* l_lean_const__folding_fold__nat__div___rarg___closed__1; -obj* l_lean_const__folding_fold__uint__sub___lambda__1___boxed(obj*, obj*, obj*, obj*); -obj* l_lean_const__folding_fold__nat__div___boxed(obj*); +obj* l_lean_compiler_mk__nat__le(obj*, obj*); +obj* l_lean_compiler_fold__nat__div___rarg(obj*, obj*); +obj* l_lean_compiler_find__bin__fold__fn__aux(obj*, obj*); obj* l_nat_mul___boxed(obj*, obj*); -obj* l_lean_const__folding_fold__uint__mod___closed__1; +extern obj* l_lean_compiler_mk__lc__proof___closed__1; +obj* l_lean_compiler_fold__uint__div___boxed(obj*, obj*, obj*); +obj* l_lean_compiler_to__decidable__expr___closed__2; namespace lean { obj* nat_mod(obj*, obj*); } -obj* l_lean_const__folding_fold__uint__mod___lambda__1___boxed(obj*, obj*, obj*, obj*); -obj* l_lean_const__folding_get__info__from__fn___main(obj*, obj*); -obj* l_lean_const__folding_fold__bin__nat(obj*, obj*, obj*); -obj* l_lean_const__folding_fold__uint__mul(uint8, obj*, obj*); -obj* l_lean_const__folding_fold__uint__mul___lambda__1(obj*, uint8, obj*, obj*); -obj* l_lean_const__folding_fold__nat__mod___rarg(obj*, obj*); +obj* l_lean_compiler_fold__uint__add___lambda__1(obj*, uint8, obj*, obj*); +obj* l_lean_compiler_mk__nat__le___closed__1; +namespace lean { +obj* fold_bin_op_core(uint8, obj*, obj*, obj*); +} +obj* l_lean_compiler_fold__uint__add___lambda__1___boxed(obj*, obj*, obj*, obj*); +obj* l_lean_compiler_mk__uint__type__name___closed__1; +obj* l_lean_compiler_fold__nat__dec__eq___lambda__1___boxed(obj*, obj*); extern obj* l_system_platform_nbits; extern "C" obj* lean_name_mk_string(obj*, obj*); -obj* l_lean_const__folding_fold__uint__sub___closed__1; -obj* l_list_map___main___at_lean_const__folding_uint__bin__fold__fns___spec__1(obj*, obj*); -obj* l_lean_const__folding_fold__uint__sub___boxed(obj*, obj*, obj*); +obj* l_lean_compiler_fold__uint__mod(uint8, obj*, obj*); extern "C" obj* lean_expr_mk_lit(obj*); -obj* l_lean_const__folding_fold__uint__mod___boxed(obj*, obj*, obj*); obj* l_nat_add___boxed(obj*, obj*); -obj* l_lean_const__folding_mk__uint__type__name___closed__1; -obj* l_lean_const__folding_fold__bin__uint(obj*, uint8, obj*, obj*); -obj* l_lean_const__folding_fold__uint__add___boxed(obj*, obj*, obj*); -obj* l_lean_const__folding_fold__nat__div___rarg(obj*, obj*); -obj* l_lean_const__folding_fold__uint__div(uint8, obj*, obj*); +obj* l_list_foldr___main___at_lean_compiler_is__of__nat___spec__1(obj*, obj*); +obj* l_lean_compiler_fold__uint__div___lambda__1___boxed(obj*, obj*, obj*, obj*); +obj* l_lean_compiler_get__info__from__fn___main(obj*, obj*); +obj* l_lean_compiler_uint__bin__fold__fns; +obj* l_lean_compiler_fold__nat__dec__eq(uint8, obj*, obj*); +obj* l_lean_compiler_fold__nat__dec__le___closed__2; +obj* l_lean_compiler_fold__uint__sub(uint8, obj*, obj*); +obj* l_lean_compiler_fold__nat__add___boxed(obj*); +obj* l_lean_compiler_fold__uint__mod___lambda__1(obj*, uint8, obj*, obj*); +obj* l_lean_compiler_fold__nat__dec__eq___closed__2; +obj* l_lean_compiler_fold__nat__dec__le___closed__1; namespace lean { obj* string_append(obj*, obj*); } extern "C" obj* lean_expr_mk_const(obj*, obj*); -obj* l_lean_const__folding_fold__bin__uint___boxed(obj*, obj*, obj*, obj*); -obj* l_lean_const__folding_fold__uint__sub(uint8, obj*, obj*); -obj* l_lean_const__folding_fold__uint__add(uint8, obj*, obj*); -obj* l_lean_const__folding_uint__bin__fold__fns; -obj* l_lean_const__folding_fold__nat__add(uint8); -obj* l_lean_const__folding_get__info__from__val___main(obj*); -obj* l_lean_const__folding_fold__nat__mod(uint8); -obj* l_lean_const__folding_fold__uint__sub___lambda__1(obj*, uint8, obj*, obj*); -obj* l_lean_const__folding_get__info__from__val(obj*); -obj* l_lean_const__folding_fold__uint__div___lambda__1___boxed(obj*, obj*, obj*, obj*); -obj* l_lean_const__folding_fold__uint__mul___boxed(obj*, obj*, obj*); -obj* l_lean_const__folding_fold__uint__add___closed__1; -obj* l_lean_const__folding_fold__nat__mul___rarg(obj*, obj*); +obj* l_lean_compiler_to__decidable__expr___boxed(obj*, obj*, obj*); +obj* l_lean_compiler_to__decidable__expr(uint8, obj*, uint8); +obj* l_lean_compiler_fold__uint__div(uint8, obj*, obj*); +uint8 l_lean_compiler_fold__nat__dec__eq___lambda__1(obj*, obj*); +obj* l_lean_compiler_fold__nat__div___rarg___closed__1; +obj* l_lean_compiler_get__info__from__val(obj*); +obj* l_lean_compiler_fold__nat__mul___rarg___closed__1; +namespace lean { +obj* get_num_lit_core(obj*); +} +obj* l_lean_compiler_fold__nat__dec__le(uint8, obj*, obj*); +obj* l_lean_compiler_fold__uint__mod___lambda__1___boxed(obj*, obj*, obj*, obj*); +obj* l_lean_compiler_nat__fold__fns; +obj* l_lean_compiler_fold__nat__dec__le___boxed(obj*, obj*, obj*); +obj* l_lean_compiler_fold__nat__dec__eq___closed__1; +obj* l_list_map___main___at_lean_compiler_uint__bin__fold__fns___spec__1(obj*, obj*); +obj* l_lean_compiler_fold__nat__dec__lt___lambda__1___boxed(obj*, obj*); +obj* l_lean_compiler_fold__nat__add___rarg___closed__1; +obj* l_lean_compiler_fold__nat__mod___rarg(obj*, obj*); +obj* l_lean_compiler_fold__bin__uint___boxed(obj*, obj*, obj*, obj*); +namespace lean { +uint8 nat_dec_eq(obj*, obj*); +} +obj* l_lean_compiler_fold__nat__bin__pred(obj*, obj*, uint8, obj*, obj*); +obj* l_lean_compiler_fold__nat__mod___boxed(obj*); +obj* l_lean_compiler_fold__nat__bin__op(obj*, obj*, obj*); +obj* l_lean_compiler_fold__uint__sub___closed__1; +obj* l_lean_compiler_fold__nat__dec__lt___boxed(obj*, obj*, obj*); +obj* l_lean_compiler_fold__uint__add___boxed(obj*, obj*, obj*); +obj* l_lean_compiler_fold__uint__sub___lambda__1(obj*, uint8, obj*, obj*); +obj* l_lean_compiler_fold__nat__dec__lt___closed__1; obj* l_lean_name_append___main(obj*, obj*); -obj* l_list_foldl___main___at_lean_const__folding_uint__bin__fold__fns___spec__2(obj*, obj*); -obj* l_lean_const__folding_find__bin__fold__fn__aux(obj*, obj*); -obj* l_lean_const__folding_find__bin__fold__fn__aux___main(obj*, obj*); -obj* l_lean_const__folding_fold__uint__mod(uint8, obj*, obj*); -obj* l_lean_const__folding_get__info__from__fn(obj*, obj*); -obj* l_lean_const__folding_bin__fold__fn; -obj* l_lean_const__folding_fold__uint__div___closed__1; -obj* l_lean_const__folding_pre__uint__bin__fold__fns; +obj* l_lean_compiler_fold__nat__mod(uint8); +namespace lean { +uint8 nat_dec_le(obj*, obj*); +} +uint8 l_lean_compiler_fold__nat__dec__le___lambda__1(obj*, obj*); +obj* l_lean_compiler_fold__uint__mul___closed__1; +obj* l_lean_compiler_fold__nat__mod___rarg___closed__1; +obj* l_lean_compiler_mk__nat__eq(obj*, obj*); +obj* l_lean_compiler_mk__uint__lit(obj*, obj*); +obj* l_lean_compiler_fold__bin__uint(obj*, uint8, obj*, obj*); namespace lean { obj* nat_div(obj*, obj*); } -obj* l_lean_const__folding_fold__nat__div(uint8); -obj* l_lean_const__folding_fold__uint__mod___lambda__1(obj*, uint8, obj*, obj*); +obj* l_lean_compiler_fold__uint__mul___lambda__1(obj*, uint8, obj*, obj*); +obj* l_lean_compiler_fold__nat__div(uint8); +obj* l_lean_mk__bin__app(obj*, obj*, obj*); +obj* l_lean_compiler_fold__nat__mul(uint8); extern "C" uint8 lean_name_dec_eq(obj*, obj*); -obj* l_lean_const__folding_fold__uint__div___boxed(obj*, obj*, obj*); obj* l_nat_pow___main(obj*, obj*); -obj* l_lean_const__folding_fold__uint__div___lambda__1(obj*, uint8, obj*, obj*); -obj* l_lean_const__folding_fold__bin__op___boxed(obj*, obj*, obj*, obj*); -obj* l_lean_const__folding_mk__uint__lit(obj*, obj*); -obj* l_lean_const__folding_fold__uint__mul___closed__1; -obj* l_lean_const__folding_fold__nat__add___boxed(obj*); -obj* l_lean_const__folding_fold__nat__mul___boxed(obj*); -obj* l_lean_const__folding_fold__nat__mul___rarg___closed__1; +obj* l_lean_compiler_fold__uint__mul(uint8, obj*, obj*); +uint8 l_lean_compiler_fold__nat__dec__lt___lambda__1(obj*, obj*); +obj* l_lean_compiler_get__num__lit___main(obj*); +obj* l_lean_compiler_get__info__from__val___main(obj*); +obj* l_lean_compiler_fold__nat__bin__pred___boxed(obj*, obj*, obj*, obj*, obj*); +obj* l_lean_compiler_fold__nat__mul___boxed(obj*); +obj* l_lean_compiler_to__decidable__expr___closed__1; +extern obj* l_lean_compiler_neutral__expr; +obj* l_lean_compiler_find__bin__fold__fn(obj*); +obj* l_lean_compiler_fold__nat__add___rarg(obj*, obj*); extern "C" obj* lean_expr_mk_app(obj*, obj*); -obj* l_lean_const__folding_fold__uint__add___lambda__1___boxed(obj*, obj*, obj*, obj*); +obj* l_lean_compiler_fold__uint__mod___closed__1; +extern obj* l_lean_level_one; +obj* l_lean_compiler_find__bin__fold__fn__aux___main(obj*, obj*); +obj* l_lean_compiler_fold__nat__div___boxed(obj*); obj* l_nat_repr(obj*); +obj* l_lean_compiler_bin__fold__fn; namespace lean { obj* nat_mul(obj*, obj*); } -obj* l_lean_const__folding_get__num__lit___main(obj*); -obj* l_lean_const__folding_fold__uint__add___lambda__1(obj*, uint8, obj*, obj*); -obj* l_lean_const__folding_is__of__nat(obj*); -obj* l_list_foldr___main___at_lean_const__folding_is__of__nat___spec__1(obj*, obj*); -obj* l_lean_const__folding_fold__nat__add___rarg(obj*, obj*); +obj* l_lean_compiler_fold__nat__dec__eq___boxed(obj*, obj*, obj*); +obj* l_lean_compiler_fold__nat__dec__le___lambda__1___boxed(obj*, obj*); +obj* l_lean_compiler_fold__nat__dec__lt(uint8, obj*, obj*); +obj* l_list_foldl___main___at_lean_compiler_uint__bin__fold__fns___spec__2(obj*, obj*); +obj* l_lean_compiler_fold__uint__sub___lambda__1___boxed(obj*, obj*, obj*, obj*); namespace lean { obj* nat_sub(obj*, obj*); } -obj* l_lean_const__folding_fold__uint__mul___lambda__1___boxed(obj*, obj*, obj*, obj*); -obj* l_lean_const__folding_num__scalar__types; +obj* l_lean_compiler_fold__uint__div___closed__1; +obj* l_lean_compiler_fold__nat__mul___rarg(obj*, obj*); +obj* l_lean_compiler_fold__uint__mul___boxed(obj*, obj*, obj*); +obj* l_lean_compiler_mk__uint__type__name(obj*); obj* l_list_append___rarg(obj*, obj*); -obj* l_lean_const__folding_fold__nat__mod___rarg___closed__1; +obj* l_lean_compiler_fold__uint__mod___boxed(obj*, obj*, obj*); +obj* l_lean_compiler_fold__uint__sub___boxed(obj*, obj*, obj*); +obj* l_lean_compiler_fold__bin__op___boxed(obj*, obj*, obj*, obj*); +obj* l_lean_compiler_pre__uint__bin__fold__fns; +obj* l_lean_compiler_mk__nat__lt___closed__1; +obj* l_lean_compiler_fold__uint__div___lambda__1(obj*, uint8, obj*, obj*); obj* l_nat_div___boxed(obj*, obj*); -obj* l_lean_const__folding_fold__nat__mod___boxed(obj*); -obj* _init_l_lean_const__folding_bin__fold__fn() { +namespace lean { +uint8 nat_dec_lt(obj*, obj*); +} +extern obj* l_lean_mk__dec__is__false___closed__1; +obj* l_lean_compiler_fold__uint__add___closed__1; +obj* l_lean_compiler_fold__uint__add(uint8, obj*, obj*); +obj* _init_l_lean_compiler_bin__fold__fn() { _start: { obj* x_0; @@ -126,7 +172,7 @@ lean::inc(x_0); return x_0; } } -obj* _init_l_lean_const__folding_mk__uint__type__name___closed__1() { +obj* _init_l_lean_compiler_mk__uint__type__name___closed__1() { _start: { obj* x_0; @@ -134,12 +180,12 @@ x_0 = lean::mk_string("uint"); return x_0; } } -obj* l_lean_const__folding_mk__uint__type__name(obj* x_0) { +obj* l_lean_compiler_mk__uint__type__name(obj* x_0) { _start: { obj* x_1; obj* x_2; obj* x_4; obj* x_6; obj* x_7; x_1 = l_nat_repr(x_0); -x_2 = l_lean_const__folding_mk__uint__type__name___closed__1; +x_2 = l_lean_compiler_mk__uint__type__name___closed__1; lean::inc(x_2); x_4 = lean::string_append(x_2, x_1); lean::dec(x_1); @@ -148,13 +194,13 @@ x_7 = lean_name_mk_string(x_6, x_4); return x_7; } } -obj* _init_l_lean_const__folding_num__scalar__types() { +obj* _init_l_lean_compiler_num__scalar__types() { _start: { obj* x_0; obj* x_2; obj* x_3; obj* x_6; obj* x_7; obj* x_10; obj* x_11; obj* x_12; obj* x_14; obj* x_17; obj* x_20; obj* x_21; obj* x_22; obj* x_24; obj* x_27; obj* x_30; obj* x_31; obj* x_32; obj* x_34; obj* x_37; obj* x_40; obj* x_41; obj* x_42; obj* x_43; obj* x_45; obj* x_47; obj* x_48; obj* x_50; obj* x_52; obj* x_53; obj* x_54; obj* x_55; obj* x_56; obj* x_57; x_0 = lean::mk_nat_obj(8u); lean::inc(x_0); -x_2 = l_lean_const__folding_mk__uint__type__name(x_0); +x_2 = l_lean_compiler_mk__uint__type__name(x_0); x_3 = lean::mk_string("of_nat"); lean::inc(x_3); lean::inc(x_2); @@ -170,7 +216,7 @@ lean::cnstr_set(x_11, 2, x_6); lean::cnstr_set(x_11, 3, x_10); x_12 = lean::mk_nat_obj(16u); lean::inc(x_12); -x_14 = l_lean_const__folding_mk__uint__type__name(x_12); +x_14 = l_lean_compiler_mk__uint__type__name(x_12); lean::inc(x_3); lean::inc(x_14); x_17 = lean_name_mk_string(x_14, x_3); @@ -184,7 +230,7 @@ lean::cnstr_set(x_21, 2, x_17); lean::cnstr_set(x_21, 3, x_20); x_22 = lean::mk_nat_obj(32u); lean::inc(x_22); -x_24 = l_lean_const__folding_mk__uint__type__name(x_22); +x_24 = l_lean_compiler_mk__uint__type__name(x_22); lean::inc(x_3); lean::inc(x_24); x_27 = lean_name_mk_string(x_24, x_3); @@ -198,7 +244,7 @@ lean::cnstr_set(x_31, 2, x_27); lean::cnstr_set(x_31, 3, x_30); x_32 = lean::mk_nat_obj(64u); lean::inc(x_32); -x_34 = l_lean_const__folding_mk__uint__type__name(x_32); +x_34 = l_lean_compiler_mk__uint__type__name(x_32); lean::inc(x_3); lean::inc(x_34); x_37 = lean_name_mk_string(x_34, x_3); @@ -243,7 +289,7 @@ lean::cnstr_set(x_57, 1, x_56); return x_57; } } -obj* l_list_foldr___main___at_lean_const__folding_is__of__nat___spec__1(obj* x_0, obj* x_1) { +obj* l_list_foldr___main___at_lean_compiler_is__of__nat___spec__1(obj* x_0, obj* x_1) { _start: { if (lean::obj_tag(x_1) == 0) @@ -285,17 +331,17 @@ return x_20; } } } -obj* l_lean_const__folding_is__of__nat(obj* x_0) { +obj* l_lean_compiler_is__of__nat(obj* x_0) { _start: { obj* x_1; obj* x_3; -x_1 = l_lean_const__folding_num__scalar__types; +x_1 = l_lean_compiler_num__scalar__types; lean::inc(x_1); -x_3 = l_list_foldr___main___at_lean_const__folding_is__of__nat___spec__1(x_0, x_1); +x_3 = l_list_foldr___main___at_lean_compiler_is__of__nat___spec__1(x_0, x_1); return x_3; } } -obj* l_lean_const__folding_get__info__from__fn___main(obj* x_0, obj* x_1) { +obj* l_lean_compiler_get__info__from__fn___main(obj* x_0, obj* x_1) { _start: { if (lean::obj_tag(x_1) == 0) @@ -336,15 +382,15 @@ return x_18; } } } -obj* l_lean_const__folding_get__info__from__fn(obj* x_0, obj* x_1) { +obj* l_lean_compiler_get__info__from__fn(obj* x_0, obj* x_1) { _start: { obj* x_2; -x_2 = l_lean_const__folding_get__info__from__fn___main(x_0, x_1); +x_2 = l_lean_compiler_get__info__from__fn___main(x_0, x_1); return x_2; } } -obj* l_lean_const__folding_get__info__from__val___main(obj* x_0) { +obj* l_lean_compiler_get__info__from__val___main(obj* x_0) { _start: { switch (lean::obj_tag(x_0)) { @@ -424,9 +470,9 @@ obj* x_22; obj* x_25; obj* x_27; x_22 = lean::cnstr_get(x_11, 0); lean::inc(x_22); lean::dec(x_11); -x_25 = l_lean_const__folding_num__scalar__types; +x_25 = l_lean_compiler_num__scalar__types; lean::inc(x_25); -x_27 = l_lean_const__folding_get__info__from__fn___main(x_22, x_25); +x_27 = l_lean_compiler_get__info__from__fn___main(x_22, x_25); return x_27; } case 5: @@ -525,15 +571,15 @@ return x_53; } } } -obj* l_lean_const__folding_get__info__from__val(obj* x_0) { +obj* l_lean_compiler_get__info__from__val(obj* x_0) { _start: { obj* x_1; -x_1 = l_lean_const__folding_get__info__from__val___main(x_0); +x_1 = l_lean_compiler_get__info__from__val___main(x_0); return x_1; } } -obj* l_lean_const__folding_get__num__lit___main(obj* x_0) { +obj* l_lean_compiler_get__num__lit___main(obj* x_0) { _start: { switch (lean::obj_tag(x_0)) { @@ -619,9 +665,9 @@ obj* x_28; obj* x_31; obj* x_33; uint8 x_34; x_28 = lean::cnstr_get(x_11, 0); lean::inc(x_28); lean::dec(x_11); -x_31 = l_lean_const__folding_num__scalar__types; +x_31 = l_lean_compiler_num__scalar__types; lean::inc(x_31); -x_33 = l_list_foldr___main___at_lean_const__folding_is__of__nat___spec__1(x_28, x_31); +x_33 = l_list_foldr___main___at_lean_compiler_is__of__nat___spec__1(x_28, x_31); x_34 = lean::unbox(x_33); lean::dec(x_33); if (x_34 == 0) @@ -762,12 +808,12 @@ obj* get_num_lit_core(obj* x_0) { _start: { obj* x_1; -x_1 = l_lean_const__folding_get__num__lit___main(x_0); +x_1 = l_lean_compiler_get__num__lit___main(x_0); return x_1; } } } -obj* l_lean_const__folding_mk__uint__lit(obj* x_0, obj* x_1) { +obj* l_lean_compiler_mk__uint__lit(obj* x_0, obj* x_1) { _start: { obj* x_2; obj* x_4; obj* x_5; obj* x_6; obj* x_9; obj* x_12; obj* x_13; obj* x_14; @@ -788,12 +834,12 @@ x_14 = lean_expr_mk_app(x_5, x_13); return x_14; } } -obj* l_lean_const__folding_fold__bin__uint(obj* x_0, uint8 x_1, obj* x_2, obj* x_3) { +obj* l_lean_compiler_fold__bin__uint(obj* x_0, uint8 x_1, obj* x_2, obj* x_3) { _start: { obj* x_5; lean::inc(x_2); -x_5 = l_lean_const__folding_get__num__lit___main(x_2); +x_5 = l_lean_compiler_get__num__lit___main(x_2); if (lean::obj_tag(x_5) == 0) { obj* x_10; @@ -816,7 +862,7 @@ if (lean::is_shared(x_5)) { lean::cnstr_release(x_5, 0); x_13 = x_5; } -x_14 = l_lean_const__folding_get__num__lit___main(x_3); +x_14 = l_lean_compiler_get__num__lit___main(x_3); if (lean::obj_tag(x_14) == 0) { obj* x_20; @@ -834,7 +880,7 @@ obj* x_21; obj* x_24; x_21 = lean::cnstr_get(x_14, 0); lean::inc(x_21); lean::dec(x_14); -x_24 = l_lean_const__folding_get__info__from__val___main(x_2); +x_24 = l_lean_compiler_get__info__from__val___main(x_2); if (lean::obj_tag(x_24) == 0) { obj* x_30; @@ -855,7 +901,7 @@ lean::dec(x_24); x_34 = lean::box(x_1); lean::inc(x_31); x_36 = lean::apply_4(x_0, x_31, x_34, x_11, x_21); -x_37 = l_lean_const__folding_mk__uint__lit(x_31, x_36); +x_37 = l_lean_compiler_mk__uint__lit(x_31, x_36); if (lean::is_scalar(x_13)) { x_38 = lean::alloc_cnstr(1, 1, 0); } else { @@ -868,16 +914,16 @@ return x_38; } } } -obj* l_lean_const__folding_fold__bin__uint___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) { +obj* l_lean_compiler_fold__bin__uint___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) { _start: { uint8 x_4; obj* x_5; x_4 = lean::unbox(x_1); -x_5 = l_lean_const__folding_fold__bin__uint(x_0, x_4, x_2, x_3); +x_5 = l_lean_compiler_fold__bin__uint(x_0, x_4, x_2, x_3); return x_5; } } -obj* l_lean_const__folding_fold__uint__add___lambda__1(obj* x_0, uint8 x_1, obj* x_2, obj* x_3) { +obj* l_lean_compiler_fold__uint__add___lambda__1(obj* x_0, uint8 x_1, obj* x_2, obj* x_3) { _start: { obj* x_5; @@ -888,43 +934,43 @@ lean::dec(x_2); return x_5; } } -obj* _init_l_lean_const__folding_fold__uint__add___closed__1() { +obj* _init_l_lean_compiler_fold__uint__add___closed__1() { _start: { obj* x_0; -x_0 = lean::alloc_closure(reinterpret_cast(l_lean_const__folding_fold__uint__add___lambda__1___boxed), 4, 0); +x_0 = lean::alloc_closure(reinterpret_cast(l_lean_compiler_fold__uint__add___lambda__1___boxed), 4, 0); return x_0; } } -obj* l_lean_const__folding_fold__uint__add(uint8 x_0, obj* x_1, obj* x_2) { +obj* l_lean_compiler_fold__uint__add(uint8 x_0, obj* x_1, obj* x_2) { _start: { obj* x_3; obj* x_5; -x_3 = l_lean_const__folding_fold__uint__add___closed__1; +x_3 = l_lean_compiler_fold__uint__add___closed__1; lean::inc(x_3); -x_5 = l_lean_const__folding_fold__bin__uint(x_3, x_0, x_1, x_2); +x_5 = l_lean_compiler_fold__bin__uint(x_3, x_0, x_1, x_2); return x_5; } } -obj* l_lean_const__folding_fold__uint__add___lambda__1___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) { +obj* l_lean_compiler_fold__uint__add___lambda__1___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) { _start: { uint8 x_4; obj* x_5; x_4 = lean::unbox(x_1); -x_5 = l_lean_const__folding_fold__uint__add___lambda__1(x_0, x_4, x_2, x_3); +x_5 = l_lean_compiler_fold__uint__add___lambda__1(x_0, x_4, x_2, x_3); return x_5; } } -obj* l_lean_const__folding_fold__uint__add___boxed(obj* x_0, obj* x_1, obj* x_2) { +obj* l_lean_compiler_fold__uint__add___boxed(obj* x_0, obj* x_1, obj* x_2) { _start: { uint8 x_3; obj* x_4; x_3 = lean::unbox(x_0); -x_4 = l_lean_const__folding_fold__uint__add(x_3, x_1, x_2); +x_4 = l_lean_compiler_fold__uint__add(x_3, x_1, x_2); return x_4; } } -obj* l_lean_const__folding_fold__uint__mul___lambda__1(obj* x_0, uint8 x_1, obj* x_2, obj* x_3) { +obj* l_lean_compiler_fold__uint__mul___lambda__1(obj* x_0, uint8 x_1, obj* x_2, obj* x_3) { _start: { obj* x_5; @@ -935,43 +981,43 @@ lean::dec(x_2); return x_5; } } -obj* _init_l_lean_const__folding_fold__uint__mul___closed__1() { +obj* _init_l_lean_compiler_fold__uint__mul___closed__1() { _start: { obj* x_0; -x_0 = lean::alloc_closure(reinterpret_cast(l_lean_const__folding_fold__uint__mul___lambda__1___boxed), 4, 0); +x_0 = lean::alloc_closure(reinterpret_cast(l_lean_compiler_fold__uint__mul___lambda__1___boxed), 4, 0); return x_0; } } -obj* l_lean_const__folding_fold__uint__mul(uint8 x_0, obj* x_1, obj* x_2) { +obj* l_lean_compiler_fold__uint__mul(uint8 x_0, obj* x_1, obj* x_2) { _start: { obj* x_3; obj* x_5; -x_3 = l_lean_const__folding_fold__uint__mul___closed__1; +x_3 = l_lean_compiler_fold__uint__mul___closed__1; lean::inc(x_3); -x_5 = l_lean_const__folding_fold__bin__uint(x_3, x_0, x_1, x_2); +x_5 = l_lean_compiler_fold__bin__uint(x_3, x_0, x_1, x_2); return x_5; } } -obj* l_lean_const__folding_fold__uint__mul___lambda__1___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) { +obj* l_lean_compiler_fold__uint__mul___lambda__1___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) { _start: { uint8 x_4; obj* x_5; x_4 = lean::unbox(x_1); -x_5 = l_lean_const__folding_fold__uint__mul___lambda__1(x_0, x_4, x_2, x_3); +x_5 = l_lean_compiler_fold__uint__mul___lambda__1(x_0, x_4, x_2, x_3); return x_5; } } -obj* l_lean_const__folding_fold__uint__mul___boxed(obj* x_0, obj* x_1, obj* x_2) { +obj* l_lean_compiler_fold__uint__mul___boxed(obj* x_0, obj* x_1, obj* x_2) { _start: { uint8 x_3; obj* x_4; x_3 = lean::unbox(x_0); -x_4 = l_lean_const__folding_fold__uint__mul(x_3, x_1, x_2); +x_4 = l_lean_compiler_fold__uint__mul(x_3, x_1, x_2); return x_4; } } -obj* l_lean_const__folding_fold__uint__div___lambda__1(obj* x_0, uint8 x_1, obj* x_2, obj* x_3) { +obj* l_lean_compiler_fold__uint__div___lambda__1(obj* x_0, uint8 x_1, obj* x_2, obj* x_3) { _start: { obj* x_5; @@ -982,43 +1028,43 @@ lean::dec(x_2); return x_5; } } -obj* _init_l_lean_const__folding_fold__uint__div___closed__1() { +obj* _init_l_lean_compiler_fold__uint__div___closed__1() { _start: { obj* x_0; -x_0 = lean::alloc_closure(reinterpret_cast(l_lean_const__folding_fold__uint__div___lambda__1___boxed), 4, 0); +x_0 = lean::alloc_closure(reinterpret_cast(l_lean_compiler_fold__uint__div___lambda__1___boxed), 4, 0); return x_0; } } -obj* l_lean_const__folding_fold__uint__div(uint8 x_0, obj* x_1, obj* x_2) { +obj* l_lean_compiler_fold__uint__div(uint8 x_0, obj* x_1, obj* x_2) { _start: { obj* x_3; obj* x_5; -x_3 = l_lean_const__folding_fold__uint__div___closed__1; +x_3 = l_lean_compiler_fold__uint__div___closed__1; lean::inc(x_3); -x_5 = l_lean_const__folding_fold__bin__uint(x_3, x_0, x_1, x_2); +x_5 = l_lean_compiler_fold__bin__uint(x_3, x_0, x_1, x_2); return x_5; } } -obj* l_lean_const__folding_fold__uint__div___lambda__1___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) { +obj* l_lean_compiler_fold__uint__div___lambda__1___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) { _start: { uint8 x_4; obj* x_5; x_4 = lean::unbox(x_1); -x_5 = l_lean_const__folding_fold__uint__div___lambda__1(x_0, x_4, x_2, x_3); +x_5 = l_lean_compiler_fold__uint__div___lambda__1(x_0, x_4, x_2, x_3); return x_5; } } -obj* l_lean_const__folding_fold__uint__div___boxed(obj* x_0, obj* x_1, obj* x_2) { +obj* l_lean_compiler_fold__uint__div___boxed(obj* x_0, obj* x_1, obj* x_2) { _start: { uint8 x_3; obj* x_4; x_3 = lean::unbox(x_0); -x_4 = l_lean_const__folding_fold__uint__div(x_3, x_1, x_2); +x_4 = l_lean_compiler_fold__uint__div(x_3, x_1, x_2); return x_4; } } -obj* l_lean_const__folding_fold__uint__mod___lambda__1(obj* x_0, uint8 x_1, obj* x_2, obj* x_3) { +obj* l_lean_compiler_fold__uint__mod___lambda__1(obj* x_0, uint8 x_1, obj* x_2, obj* x_3) { _start: { obj* x_5; @@ -1029,43 +1075,43 @@ lean::dec(x_2); return x_5; } } -obj* _init_l_lean_const__folding_fold__uint__mod___closed__1() { +obj* _init_l_lean_compiler_fold__uint__mod___closed__1() { _start: { obj* x_0; -x_0 = lean::alloc_closure(reinterpret_cast(l_lean_const__folding_fold__uint__mod___lambda__1___boxed), 4, 0); +x_0 = lean::alloc_closure(reinterpret_cast(l_lean_compiler_fold__uint__mod___lambda__1___boxed), 4, 0); return x_0; } } -obj* l_lean_const__folding_fold__uint__mod(uint8 x_0, obj* x_1, obj* x_2) { +obj* l_lean_compiler_fold__uint__mod(uint8 x_0, obj* x_1, obj* x_2) { _start: { obj* x_3; obj* x_5; -x_3 = l_lean_const__folding_fold__uint__mod___closed__1; +x_3 = l_lean_compiler_fold__uint__mod___closed__1; lean::inc(x_3); -x_5 = l_lean_const__folding_fold__bin__uint(x_3, x_0, x_1, x_2); +x_5 = l_lean_compiler_fold__bin__uint(x_3, x_0, x_1, x_2); return x_5; } } -obj* l_lean_const__folding_fold__uint__mod___lambda__1___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) { +obj* l_lean_compiler_fold__uint__mod___lambda__1___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) { _start: { uint8 x_4; obj* x_5; x_4 = lean::unbox(x_1); -x_5 = l_lean_const__folding_fold__uint__mod___lambda__1(x_0, x_4, x_2, x_3); +x_5 = l_lean_compiler_fold__uint__mod___lambda__1(x_0, x_4, x_2, x_3); return x_5; } } -obj* l_lean_const__folding_fold__uint__mod___boxed(obj* x_0, obj* x_1, obj* x_2) { +obj* l_lean_compiler_fold__uint__mod___boxed(obj* x_0, obj* x_1, obj* x_2) { _start: { uint8 x_3; obj* x_4; x_3 = lean::unbox(x_0); -x_4 = l_lean_const__folding_fold__uint__mod(x_3, x_1, x_2); +x_4 = l_lean_compiler_fold__uint__mod(x_3, x_1, x_2); return x_4; } } -obj* l_lean_const__folding_fold__uint__sub___lambda__1(obj* x_0, uint8 x_1, obj* x_2, obj* x_3) { +obj* l_lean_compiler_fold__uint__sub___lambda__1(obj* x_0, uint8 x_1, obj* x_2, obj* x_3) { _start: { obj* x_4; obj* x_7; obj* x_10; @@ -1081,43 +1127,43 @@ lean::dec(x_2); return x_10; } } -obj* _init_l_lean_const__folding_fold__uint__sub___closed__1() { +obj* _init_l_lean_compiler_fold__uint__sub___closed__1() { _start: { obj* x_0; -x_0 = lean::alloc_closure(reinterpret_cast(l_lean_const__folding_fold__uint__sub___lambda__1___boxed), 4, 0); +x_0 = lean::alloc_closure(reinterpret_cast(l_lean_compiler_fold__uint__sub___lambda__1___boxed), 4, 0); return x_0; } } -obj* l_lean_const__folding_fold__uint__sub(uint8 x_0, obj* x_1, obj* x_2) { +obj* l_lean_compiler_fold__uint__sub(uint8 x_0, obj* x_1, obj* x_2) { _start: { obj* x_3; obj* x_5; -x_3 = l_lean_const__folding_fold__uint__sub___closed__1; +x_3 = l_lean_compiler_fold__uint__sub___closed__1; lean::inc(x_3); -x_5 = l_lean_const__folding_fold__bin__uint(x_3, x_0, x_1, x_2); +x_5 = l_lean_compiler_fold__bin__uint(x_3, x_0, x_1, x_2); return x_5; } } -obj* l_lean_const__folding_fold__uint__sub___lambda__1___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) { +obj* l_lean_compiler_fold__uint__sub___lambda__1___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) { _start: { uint8 x_4; obj* x_5; x_4 = lean::unbox(x_1); -x_5 = l_lean_const__folding_fold__uint__sub___lambda__1(x_0, x_4, x_2, x_3); +x_5 = l_lean_compiler_fold__uint__sub___lambda__1(x_0, x_4, x_2, x_3); return x_5; } } -obj* l_lean_const__folding_fold__uint__sub___boxed(obj* x_0, obj* x_1, obj* x_2) { +obj* l_lean_compiler_fold__uint__sub___boxed(obj* x_0, obj* x_1, obj* x_2) { _start: { uint8 x_3; obj* x_4; x_3 = lean::unbox(x_0); -x_4 = l_lean_const__folding_fold__uint__sub(x_3, x_1, x_2); +x_4 = l_lean_compiler_fold__uint__sub(x_3, x_1, x_2); return x_4; } } -obj* _init_l_lean_const__folding_pre__uint__bin__fold__fns() { +obj* _init_l_lean_compiler_pre__uint__bin__fold__fns() { _start: { obj* x_0; obj* x_1; obj* x_3; obj* x_4; obj* x_5; obj* x_6; obj* x_8; obj* x_9; obj* x_10; obj* x_11; obj* x_13; obj* x_14; obj* x_15; obj* x_16; obj* x_18; obj* x_19; obj* x_20; obj* x_21; obj* x_23; obj* x_24; obj* x_25; obj* x_26; obj* x_27; obj* x_28; obj* x_29; obj* x_30; @@ -1125,35 +1171,35 @@ x_0 = lean::box(0); x_1 = lean::mk_string("add"); lean::inc(x_0); x_3 = lean_name_mk_string(x_0, x_1); -x_4 = lean::alloc_closure(reinterpret_cast(l_lean_const__folding_fold__uint__add___boxed), 3, 0); +x_4 = lean::alloc_closure(reinterpret_cast(l_lean_compiler_fold__uint__add___boxed), 3, 0); x_5 = lean::alloc_cnstr(0, 2, 0); lean::cnstr_set(x_5, 0, x_3); lean::cnstr_set(x_5, 1, x_4); x_6 = lean::mk_string("mul"); lean::inc(x_0); x_8 = lean_name_mk_string(x_0, x_6); -x_9 = lean::alloc_closure(reinterpret_cast(l_lean_const__folding_fold__uint__mul___boxed), 3, 0); +x_9 = lean::alloc_closure(reinterpret_cast(l_lean_compiler_fold__uint__mul___boxed), 3, 0); x_10 = lean::alloc_cnstr(0, 2, 0); lean::cnstr_set(x_10, 0, x_8); lean::cnstr_set(x_10, 1, x_9); x_11 = lean::mk_string("div"); lean::inc(x_0); x_13 = lean_name_mk_string(x_0, x_11); -x_14 = lean::alloc_closure(reinterpret_cast(l_lean_const__folding_fold__uint__div___boxed), 3, 0); +x_14 = lean::alloc_closure(reinterpret_cast(l_lean_compiler_fold__uint__div___boxed), 3, 0); x_15 = lean::alloc_cnstr(0, 2, 0); lean::cnstr_set(x_15, 0, x_13); lean::cnstr_set(x_15, 1, x_14); x_16 = lean::mk_string("mod"); lean::inc(x_0); x_18 = lean_name_mk_string(x_0, x_16); -x_19 = lean::alloc_closure(reinterpret_cast(l_lean_const__folding_fold__uint__mod___boxed), 3, 0); +x_19 = lean::alloc_closure(reinterpret_cast(l_lean_compiler_fold__uint__mod___boxed), 3, 0); x_20 = lean::alloc_cnstr(0, 2, 0); lean::cnstr_set(x_20, 0, x_18); lean::cnstr_set(x_20, 1, x_19); x_21 = lean::mk_string("sub"); lean::inc(x_0); x_23 = lean_name_mk_string(x_0, x_21); -x_24 = lean::alloc_closure(reinterpret_cast(l_lean_const__folding_fold__uint__sub___boxed), 3, 0); +x_24 = lean::alloc_closure(reinterpret_cast(l_lean_compiler_fold__uint__sub___boxed), 3, 0); x_25 = lean::alloc_cnstr(0, 2, 0); lean::cnstr_set(x_25, 0, x_23); lean::cnstr_set(x_25, 1, x_24); @@ -1175,7 +1221,7 @@ lean::cnstr_set(x_30, 1, x_29); return x_30; } } -obj* l_list_map___main___at_lean_const__folding_uint__bin__fold__fns___spec__1(obj* x_0, obj* x_1) { +obj* l_list_map___main___at_lean_compiler_uint__bin__fold__fns___spec__1(obj* x_0, obj* x_1) { _start: { if (lean::obj_tag(x_1) == 0) @@ -1214,7 +1260,7 @@ if (lean::is_shared(x_5)) { x_14 = x_5; } lean::inc(x_0); -x_16 = l_list_map___main___at_lean_const__folding_uint__bin__fold__fns___spec__1(x_0, x_7); +x_16 = l_list_map___main___at_lean_compiler_uint__bin__fold__fns___spec__1(x_0, x_7); x_17 = lean::cnstr_get(x_0, 1); lean::inc(x_17); lean::dec(x_0); @@ -1237,7 +1283,7 @@ return x_22; } } } -obj* l_list_foldl___main___at_lean_const__folding_uint__bin__fold__fns___spec__2(obj* x_0, obj* x_1) { +obj* l_list_foldl___main___at_lean_compiler_uint__bin__fold__fns___spec__2(obj* x_0, obj* x_1) { _start: { if (lean::obj_tag(x_1) == 0) @@ -1253,9 +1299,9 @@ lean::inc(x_3); x_5 = lean::cnstr_get(x_1, 1); lean::inc(x_5); lean::dec(x_1); -x_8 = l_lean_const__folding_pre__uint__bin__fold__fns; +x_8 = l_lean_compiler_pre__uint__bin__fold__fns; lean::inc(x_8); -x_10 = l_list_map___main___at_lean_const__folding_uint__bin__fold__fns___spec__1(x_3, x_8); +x_10 = l_list_map___main___at_lean_compiler_uint__bin__fold__fns___spec__1(x_3, x_8); x_11 = l_list_append___rarg(x_0, x_10); x_0 = x_11; x_1 = x_5; @@ -1263,22 +1309,22 @@ goto _start; } } } -obj* _init_l_lean_const__folding_uint__bin__fold__fns() { +obj* _init_l_lean_compiler_uint__bin__fold__fns() { _start: { obj* x_0; obj* x_1; obj* x_3; x_0 = lean::box(0); -x_1 = l_lean_const__folding_num__scalar__types; +x_1 = l_lean_compiler_num__scalar__types; lean::inc(x_1); -x_3 = l_list_foldl___main___at_lean_const__folding_uint__bin__fold__fns___spec__2(x_0, x_1); +x_3 = l_list_foldl___main___at_lean_compiler_uint__bin__fold__fns___spec__2(x_0, x_1); return x_3; } } -obj* l_lean_const__folding_fold__bin__nat(obj* x_0, obj* x_1, obj* x_2) { +obj* l_lean_compiler_fold__nat__bin__op(obj* x_0, obj* x_1, obj* x_2) { _start: { obj* x_3; -x_3 = l_lean_const__folding_get__num__lit___main(x_1); +x_3 = l_lean_compiler_get__num__lit___main(x_1); if (lean::obj_tag(x_3) == 0) { obj* x_7; @@ -1300,7 +1346,7 @@ if (lean::is_shared(x_3)) { lean::cnstr_release(x_3, 0); x_10 = x_3; } -x_11 = l_lean_const__folding_get__num__lit___main(x_2); +x_11 = l_lean_compiler_get__num__lit___main(x_2); if (lean::obj_tag(x_11) == 0) { obj* x_16; @@ -1332,7 +1378,7 @@ return x_23; } } } -obj* _init_l_lean_const__folding_fold__nat__add___rarg___closed__1() { +obj* _init_l_lean_compiler_fold__nat__add___rarg___closed__1() { _start: { obj* x_0; @@ -1340,34 +1386,34 @@ x_0 = lean::alloc_closure(reinterpret_cast(l_nat_add___boxed), 2, 0); return x_0; } } -obj* l_lean_const__folding_fold__nat__add___rarg(obj* x_0, obj* x_1) { +obj* l_lean_compiler_fold__nat__add___rarg(obj* x_0, obj* x_1) { _start: { obj* x_2; obj* x_4; -x_2 = l_lean_const__folding_fold__nat__add___rarg___closed__1; +x_2 = l_lean_compiler_fold__nat__add___rarg___closed__1; lean::inc(x_2); -x_4 = l_lean_const__folding_fold__bin__nat(x_2, x_0, x_1); +x_4 = l_lean_compiler_fold__nat__bin__op(x_2, x_0, x_1); return x_4; } } -obj* l_lean_const__folding_fold__nat__add(uint8 x_0) { +obj* l_lean_compiler_fold__nat__add(uint8 x_0) { _start: { obj* x_1; -x_1 = lean::alloc_closure(reinterpret_cast(l_lean_const__folding_fold__nat__add___rarg), 2, 0); +x_1 = lean::alloc_closure(reinterpret_cast(l_lean_compiler_fold__nat__add___rarg), 2, 0); return x_1; } } -obj* l_lean_const__folding_fold__nat__add___boxed(obj* x_0) { +obj* l_lean_compiler_fold__nat__add___boxed(obj* x_0) { _start: { uint8 x_1; obj* x_2; x_1 = lean::unbox(x_0); -x_2 = l_lean_const__folding_fold__nat__add(x_1); +x_2 = l_lean_compiler_fold__nat__add(x_1); return x_2; } } -obj* _init_l_lean_const__folding_fold__nat__mul___rarg___closed__1() { +obj* _init_l_lean_compiler_fold__nat__mul___rarg___closed__1() { _start: { obj* x_0; @@ -1375,34 +1421,34 @@ x_0 = lean::alloc_closure(reinterpret_cast(l_nat_mul___boxed), 2, 0); return x_0; } } -obj* l_lean_const__folding_fold__nat__mul___rarg(obj* x_0, obj* x_1) { +obj* l_lean_compiler_fold__nat__mul___rarg(obj* x_0, obj* x_1) { _start: { obj* x_2; obj* x_4; -x_2 = l_lean_const__folding_fold__nat__mul___rarg___closed__1; +x_2 = l_lean_compiler_fold__nat__mul___rarg___closed__1; lean::inc(x_2); -x_4 = l_lean_const__folding_fold__bin__nat(x_2, x_0, x_1); +x_4 = l_lean_compiler_fold__nat__bin__op(x_2, x_0, x_1); return x_4; } } -obj* l_lean_const__folding_fold__nat__mul(uint8 x_0) { +obj* l_lean_compiler_fold__nat__mul(uint8 x_0) { _start: { obj* x_1; -x_1 = lean::alloc_closure(reinterpret_cast(l_lean_const__folding_fold__nat__mul___rarg), 2, 0); +x_1 = lean::alloc_closure(reinterpret_cast(l_lean_compiler_fold__nat__mul___rarg), 2, 0); return x_1; } } -obj* l_lean_const__folding_fold__nat__mul___boxed(obj* x_0) { +obj* l_lean_compiler_fold__nat__mul___boxed(obj* x_0) { _start: { uint8 x_1; obj* x_2; x_1 = lean::unbox(x_0); -x_2 = l_lean_const__folding_fold__nat__mul(x_1); +x_2 = l_lean_compiler_fold__nat__mul(x_1); return x_2; } } -obj* _init_l_lean_const__folding_fold__nat__div___rarg___closed__1() { +obj* _init_l_lean_compiler_fold__nat__div___rarg___closed__1() { _start: { obj* x_0; @@ -1410,34 +1456,34 @@ x_0 = lean::alloc_closure(reinterpret_cast(l_nat_div___boxed), 2, 0); return x_0; } } -obj* l_lean_const__folding_fold__nat__div___rarg(obj* x_0, obj* x_1) { +obj* l_lean_compiler_fold__nat__div___rarg(obj* x_0, obj* x_1) { _start: { obj* x_2; obj* x_4; -x_2 = l_lean_const__folding_fold__nat__div___rarg___closed__1; +x_2 = l_lean_compiler_fold__nat__div___rarg___closed__1; lean::inc(x_2); -x_4 = l_lean_const__folding_fold__bin__nat(x_2, x_0, x_1); +x_4 = l_lean_compiler_fold__nat__bin__op(x_2, x_0, x_1); return x_4; } } -obj* l_lean_const__folding_fold__nat__div(uint8 x_0) { +obj* l_lean_compiler_fold__nat__div(uint8 x_0) { _start: { obj* x_1; -x_1 = lean::alloc_closure(reinterpret_cast(l_lean_const__folding_fold__nat__div___rarg), 2, 0); +x_1 = lean::alloc_closure(reinterpret_cast(l_lean_compiler_fold__nat__div___rarg), 2, 0); return x_1; } } -obj* l_lean_const__folding_fold__nat__div___boxed(obj* x_0) { +obj* l_lean_compiler_fold__nat__div___boxed(obj* x_0) { _start: { uint8 x_1; obj* x_2; x_1 = lean::unbox(x_0); -x_2 = l_lean_const__folding_fold__nat__div(x_1); +x_2 = l_lean_compiler_fold__nat__div(x_1); return x_2; } } -obj* _init_l_lean_const__folding_fold__nat__mod___rarg___closed__1() { +obj* _init_l_lean_compiler_fold__nat__mod___rarg___closed__1() { _start: { obj* x_0; @@ -1445,37 +1491,510 @@ x_0 = lean::alloc_closure(reinterpret_cast(l_nat_mod___boxed), 2, 0); return x_0; } } -obj* l_lean_const__folding_fold__nat__mod___rarg(obj* x_0, obj* x_1) { +obj* l_lean_compiler_fold__nat__mod___rarg(obj* x_0, obj* x_1) { _start: { obj* x_2; obj* x_4; -x_2 = l_lean_const__folding_fold__nat__mod___rarg___closed__1; +x_2 = l_lean_compiler_fold__nat__mod___rarg___closed__1; lean::inc(x_2); -x_4 = l_lean_const__folding_fold__bin__nat(x_2, x_0, x_1); +x_4 = l_lean_compiler_fold__nat__bin__op(x_2, x_0, x_1); return x_4; } } -obj* l_lean_const__folding_fold__nat__mod(uint8 x_0) { +obj* l_lean_compiler_fold__nat__mod(uint8 x_0) { _start: { obj* x_1; -x_1 = lean::alloc_closure(reinterpret_cast(l_lean_const__folding_fold__nat__mod___rarg), 2, 0); +x_1 = lean::alloc_closure(reinterpret_cast(l_lean_compiler_fold__nat__mod___rarg), 2, 0); return x_1; } } -obj* l_lean_const__folding_fold__nat__mod___boxed(obj* x_0) { +obj* l_lean_compiler_fold__nat__mod___boxed(obj* x_0) { _start: { uint8 x_1; obj* x_2; x_1 = lean::unbox(x_0); -x_2 = l_lean_const__folding_fold__nat__mod(x_1); +x_2 = l_lean_compiler_fold__nat__mod(x_1); return x_2; } } -obj* _init_l_lean_const__folding_bin__fold__fns() { +obj* _init_l_lean_compiler_mk__nat__eq___closed__1() { _start: { -obj* x_0; obj* x_1; obj* x_3; obj* x_4; obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_16; obj* x_17; obj* x_18; obj* x_19; obj* x_20; obj* x_21; obj* x_22; obj* x_23; obj* x_24; obj* x_25; obj* x_26; obj* x_27; obj* x_29; +obj* x_0; obj* x_1; obj* x_3; obj* x_4; obj* x_7; obj* x_8; obj* x_9; obj* x_11; obj* x_12; obj* x_13; +x_0 = lean::box(0); +x_1 = lean::mk_string("eq"); +lean::inc(x_0); +x_3 = lean_name_mk_string(x_0, x_1); +x_4 = l_lean_level_one; +lean::inc(x_0); +lean::inc(x_4); +x_7 = lean::alloc_cnstr(1, 2, 0); +lean::cnstr_set(x_7, 0, x_4); +lean::cnstr_set(x_7, 1, x_0); +x_8 = lean_expr_mk_const(x_3, x_7); +x_9 = lean::mk_string("nat"); +lean::inc(x_0); +x_11 = lean_name_mk_string(x_0, x_9); +x_12 = lean_expr_mk_const(x_11, x_0); +x_13 = lean_expr_mk_app(x_8, x_12); +return x_13; +} +} +obj* l_lean_compiler_mk__nat__eq(obj* x_0, obj* x_1) { +_start: +{ +obj* x_2; obj* x_4; +x_2 = l_lean_compiler_mk__nat__eq___closed__1; +lean::inc(x_2); +x_4 = l_lean_mk__bin__app(x_2, x_0, x_1); +return x_4; +} +} +obj* _init_l_lean_compiler_mk__nat__lt___closed__1() { +_start: +{ +obj* x_0; obj* x_1; obj* x_4; obj* x_5; obj* x_6; obj* x_9; obj* x_10; obj* x_11; obj* x_13; obj* x_16; obj* x_17; obj* x_18; obj* x_19; +x_0 = lean::box(0); +x_1 = lean::mk_string("has_lt"); +lean::inc(x_1); +lean::inc(x_0); +x_4 = lean_name_mk_string(x_0, x_1); +x_5 = lean::mk_string("lt"); +x_6 = lean_name_mk_string(x_4, x_5); +lean::inc(x_0); +lean::inc(x_0); +x_9 = lean::alloc_cnstr(1, 2, 0); +lean::cnstr_set(x_9, 0, x_0); +lean::cnstr_set(x_9, 1, x_0); +x_10 = lean_expr_mk_const(x_6, x_9); +x_11 = lean::mk_string("nat"); +lean::inc(x_0); +x_13 = lean_name_mk_string(x_0, x_11); +lean::inc(x_0); +lean::inc(x_13); +x_16 = lean_expr_mk_const(x_13, x_0); +x_17 = lean_name_mk_string(x_13, x_1); +x_18 = lean_expr_mk_const(x_17, x_0); +x_19 = l_lean_mk__bin__app(x_10, x_16, x_18); +return x_19; +} +} +obj* l_lean_compiler_mk__nat__lt(obj* x_0, obj* x_1) { +_start: +{ +obj* x_2; obj* x_4; +x_2 = l_lean_compiler_mk__nat__lt___closed__1; +lean::inc(x_2); +x_4 = l_lean_mk__bin__app(x_2, x_0, x_1); +return x_4; +} +} +obj* _init_l_lean_compiler_mk__nat__le___closed__1() { +_start: +{ +obj* x_0; obj* x_1; obj* x_3; obj* x_4; obj* x_5; obj* x_8; obj* x_9; obj* x_10; obj* x_12; obj* x_15; obj* x_16; obj* x_17; obj* x_18; obj* x_19; +x_0 = lean::box(0); +x_1 = lean::mk_string("has_lt"); +lean::inc(x_0); +x_3 = lean_name_mk_string(x_0, x_1); +x_4 = lean::mk_string("le"); +x_5 = lean_name_mk_string(x_3, x_4); +lean::inc(x_0); +lean::inc(x_0); +x_8 = lean::alloc_cnstr(1, 2, 0); +lean::cnstr_set(x_8, 0, x_0); +lean::cnstr_set(x_8, 1, x_0); +x_9 = lean_expr_mk_const(x_5, x_8); +x_10 = lean::mk_string("nat"); +lean::inc(x_0); +x_12 = lean_name_mk_string(x_0, x_10); +lean::inc(x_0); +lean::inc(x_12); +x_15 = lean_expr_mk_const(x_12, x_0); +x_16 = lean::mk_string("has_le"); +x_17 = lean_name_mk_string(x_12, x_16); +x_18 = lean_expr_mk_const(x_17, x_0); +x_19 = l_lean_mk__bin__app(x_9, x_15, x_18); +return x_19; +} +} +obj* l_lean_compiler_mk__nat__le(obj* x_0, obj* x_1) { +_start: +{ +obj* x_2; obj* x_4; +x_2 = l_lean_compiler_mk__nat__le___closed__1; +lean::inc(x_2); +x_4 = l_lean_mk__bin__app(x_2, x_0, x_1); +return x_4; +} +} +obj* _init_l_lean_compiler_to__decidable__expr___closed__1() { +_start: +{ +obj* x_0; obj* x_1; obj* x_5; +x_0 = l_lean_mk__dec__is__false___closed__1; +x_1 = l_lean_compiler_neutral__expr; +lean::inc(x_1); +lean::inc(x_1); +lean::inc(x_0); +x_5 = l_lean_mk__bin__app(x_0, x_1, x_1); +return x_5; +} +} +obj* _init_l_lean_compiler_to__decidable__expr___closed__2() { +_start: +{ +obj* x_0; obj* x_1; obj* x_5; +x_0 = l_lean_mk__dec__is__true___closed__1; +x_1 = l_lean_compiler_neutral__expr; +lean::inc(x_1); +lean::inc(x_1); +lean::inc(x_0); +x_5 = l_lean_mk__bin__app(x_0, x_1, x_1); +return x_5; +} +} +obj* l_lean_compiler_to__decidable__expr(uint8 x_0, obj* x_1, uint8 x_2) { +_start: +{ +if (x_0 == 0) +{ +lean::dec(x_1); +if (x_2 == 0) +{ +obj* x_4; +x_4 = l_lean_compiler_to__decidable__expr___closed__1; +lean::inc(x_4); +return x_4; +} +else +{ +obj* x_6; +x_6 = l_lean_compiler_to__decidable__expr___closed__2; +lean::inc(x_6); +return x_6; +} +} +else +{ +if (x_2 == 0) +{ +obj* x_8; obj* x_11; obj* x_12; obj* x_14; +x_8 = l_lean_compiler_mk__lc__proof___closed__1; +lean::inc(x_1); +lean::inc(x_8); +x_11 = lean_expr_mk_app(x_8, x_1); +x_12 = l_lean_mk__dec__is__false___closed__1; +lean::inc(x_12); +x_14 = l_lean_mk__bin__app(x_12, x_1, x_11); +return x_14; +} +else +{ +obj* x_15; obj* x_18; obj* x_19; obj* x_21; +x_15 = l_lean_compiler_mk__lc__proof___closed__1; +lean::inc(x_1); +lean::inc(x_15); +x_18 = lean_expr_mk_app(x_15, x_1); +x_19 = l_lean_mk__dec__is__true___closed__1; +lean::inc(x_19); +x_21 = l_lean_mk__bin__app(x_19, x_1, x_18); +return x_21; +} +} +} +} +obj* l_lean_compiler_to__decidable__expr___boxed(obj* x_0, obj* x_1, obj* x_2) { +_start: +{ +uint8 x_3; uint8 x_4; obj* x_5; +x_3 = lean::unbox(x_0); +x_4 = lean::unbox(x_2); +x_5 = l_lean_compiler_to__decidable__expr(x_3, x_1, x_4); +return x_5; +} +} +obj* l_lean_compiler_fold__nat__bin__pred(obj* x_0, obj* x_1, uint8 x_2, obj* x_3, obj* x_4) { +_start: +{ +obj* x_6; +lean::inc(x_3); +x_6 = l_lean_compiler_get__num__lit___main(x_3); +if (lean::obj_tag(x_6) == 0) +{ +obj* x_12; +lean::dec(x_6); +lean::dec(x_4); +lean::dec(x_1); +lean::dec(x_3); +lean::dec(x_0); +x_12 = lean::box(0); +return x_12; +} +else +{ +obj* x_13; obj* x_15; obj* x_17; +x_13 = lean::cnstr_get(x_6, 0); +lean::inc(x_13); +if (lean::is_shared(x_6)) { + lean::dec(x_6); + x_15 = lean::box(0); +} else { + lean::cnstr_release(x_6, 0); + x_15 = x_6; +} +lean::inc(x_4); +x_17 = l_lean_compiler_get__num__lit___main(x_4); +if (lean::obj_tag(x_17) == 0) +{ +obj* x_25; +lean::dec(x_17); +lean::dec(x_15); +lean::dec(x_13); +lean::dec(x_4); +lean::dec(x_1); +lean::dec(x_3); +lean::dec(x_0); +x_25 = lean::box(0); +return x_25; +} +else +{ +obj* x_26; obj* x_29; obj* x_30; uint8 x_31; obj* x_33; obj* x_34; +x_26 = lean::cnstr_get(x_17, 0); +lean::inc(x_26); +lean::dec(x_17); +x_29 = lean::apply_2(x_0, x_3, x_4); +x_30 = lean::apply_2(x_1, x_13, x_26); +x_31 = lean::unbox(x_30); +lean::dec(x_30); +x_33 = l_lean_compiler_to__decidable__expr(x_2, x_29, x_31); +if (lean::is_scalar(x_15)) { + x_34 = lean::alloc_cnstr(1, 1, 0); +} else { + x_34 = x_15; +} +lean::cnstr_set(x_34, 0, x_33); +return x_34; +} +} +} +} +obj* l_lean_compiler_fold__nat__bin__pred___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) { +_start: +{ +uint8 x_5; obj* x_6; +x_5 = lean::unbox(x_2); +x_6 = l_lean_compiler_fold__nat__bin__pred(x_0, x_1, x_5, x_3, x_4); +return x_6; +} +} +uint8 l_lean_compiler_fold__nat__dec__eq___lambda__1(obj* x_0, obj* x_1) { +_start: +{ +uint8 x_2; +x_2 = lean::nat_dec_eq(x_0, x_1); +lean::dec(x_1); +lean::dec(x_0); +if (x_2 == 0) +{ +uint8 x_5; +x_5 = 0; +return x_5; +} +else +{ +uint8 x_6; +x_6 = 1; +return x_6; +} +} +} +obj* _init_l_lean_compiler_fold__nat__dec__eq___closed__1() { +_start: +{ +obj* x_0; +x_0 = lean::alloc_closure(reinterpret_cast(l_lean_compiler_mk__nat__eq), 2, 0); +return x_0; +} +} +obj* _init_l_lean_compiler_fold__nat__dec__eq___closed__2() { +_start: +{ +obj* x_0; +x_0 = lean::alloc_closure(reinterpret_cast(l_lean_compiler_fold__nat__dec__eq___lambda__1___boxed), 2, 0); +return x_0; +} +} +obj* l_lean_compiler_fold__nat__dec__eq(uint8 x_0, obj* x_1, obj* x_2) { +_start: +{ +obj* x_3; obj* x_4; obj* x_7; +x_3 = l_lean_compiler_fold__nat__dec__eq___closed__1; +x_4 = l_lean_compiler_fold__nat__dec__eq___closed__2; +lean::inc(x_4); +lean::inc(x_3); +x_7 = l_lean_compiler_fold__nat__bin__pred(x_3, x_4, x_0, x_1, x_2); +return x_7; +} +} +obj* l_lean_compiler_fold__nat__dec__eq___lambda__1___boxed(obj* x_0, obj* x_1) { +_start: +{ +uint8 x_2; obj* x_3; +x_2 = l_lean_compiler_fold__nat__dec__eq___lambda__1(x_0, x_1); +x_3 = lean::box(x_2); +return x_3; +} +} +obj* l_lean_compiler_fold__nat__dec__eq___boxed(obj* x_0, obj* x_1, obj* x_2) { +_start: +{ +uint8 x_3; obj* x_4; +x_3 = lean::unbox(x_0); +x_4 = l_lean_compiler_fold__nat__dec__eq(x_3, x_1, x_2); +return x_4; +} +} +uint8 l_lean_compiler_fold__nat__dec__lt___lambda__1(obj* x_0, obj* x_1) { +_start: +{ +uint8 x_2; +x_2 = lean::nat_dec_lt(x_0, x_1); +lean::dec(x_1); +lean::dec(x_0); +if (x_2 == 0) +{ +uint8 x_5; +x_5 = 0; +return x_5; +} +else +{ +uint8 x_6; +x_6 = 1; +return x_6; +} +} +} +obj* _init_l_lean_compiler_fold__nat__dec__lt___closed__1() { +_start: +{ +obj* x_0; +x_0 = lean::alloc_closure(reinterpret_cast(l_lean_compiler_mk__nat__lt), 2, 0); +return x_0; +} +} +obj* _init_l_lean_compiler_fold__nat__dec__lt___closed__2() { +_start: +{ +obj* x_0; +x_0 = lean::alloc_closure(reinterpret_cast(l_lean_compiler_fold__nat__dec__lt___lambda__1___boxed), 2, 0); +return x_0; +} +} +obj* l_lean_compiler_fold__nat__dec__lt(uint8 x_0, obj* x_1, obj* x_2) { +_start: +{ +obj* x_3; obj* x_4; obj* x_7; +x_3 = l_lean_compiler_fold__nat__dec__lt___closed__1; +x_4 = l_lean_compiler_fold__nat__dec__lt___closed__2; +lean::inc(x_4); +lean::inc(x_3); +x_7 = l_lean_compiler_fold__nat__bin__pred(x_3, x_4, x_0, x_1, x_2); +return x_7; +} +} +obj* l_lean_compiler_fold__nat__dec__lt___lambda__1___boxed(obj* x_0, obj* x_1) { +_start: +{ +uint8 x_2; obj* x_3; +x_2 = l_lean_compiler_fold__nat__dec__lt___lambda__1(x_0, x_1); +x_3 = lean::box(x_2); +return x_3; +} +} +obj* l_lean_compiler_fold__nat__dec__lt___boxed(obj* x_0, obj* x_1, obj* x_2) { +_start: +{ +uint8 x_3; obj* x_4; +x_3 = lean::unbox(x_0); +x_4 = l_lean_compiler_fold__nat__dec__lt(x_3, x_1, x_2); +return x_4; +} +} +uint8 l_lean_compiler_fold__nat__dec__le___lambda__1(obj* x_0, obj* x_1) { +_start: +{ +uint8 x_2; +x_2 = lean::nat_dec_le(x_0, x_1); +lean::dec(x_1); +lean::dec(x_0); +if (x_2 == 0) +{ +uint8 x_5; +x_5 = 0; +return x_5; +} +else +{ +uint8 x_6; +x_6 = 1; +return x_6; +} +} +} +obj* _init_l_lean_compiler_fold__nat__dec__le___closed__1() { +_start: +{ +obj* x_0; +x_0 = lean::alloc_closure(reinterpret_cast(l_lean_compiler_mk__nat__le), 2, 0); +return x_0; +} +} +obj* _init_l_lean_compiler_fold__nat__dec__le___closed__2() { +_start: +{ +obj* x_0; +x_0 = lean::alloc_closure(reinterpret_cast(l_lean_compiler_fold__nat__dec__le___lambda__1___boxed), 2, 0); +return x_0; +} +} +obj* l_lean_compiler_fold__nat__dec__le(uint8 x_0, obj* x_1, obj* x_2) { +_start: +{ +obj* x_3; obj* x_4; obj* x_7; +x_3 = l_lean_compiler_fold__nat__dec__le___closed__1; +x_4 = l_lean_compiler_fold__nat__dec__le___closed__2; +lean::inc(x_4); +lean::inc(x_3); +x_7 = l_lean_compiler_fold__nat__bin__pred(x_3, x_4, x_0, x_1, x_2); +return x_7; +} +} +obj* l_lean_compiler_fold__nat__dec__le___lambda__1___boxed(obj* x_0, obj* x_1) { +_start: +{ +uint8 x_2; obj* x_3; +x_2 = l_lean_compiler_fold__nat__dec__le___lambda__1(x_0, x_1); +x_3 = lean::box(x_2); +return x_3; +} +} +obj* l_lean_compiler_fold__nat__dec__le___boxed(obj* x_0, obj* x_1, obj* x_2) { +_start: +{ +uint8 x_3; obj* x_4; +x_3 = lean::unbox(x_0); +x_4 = l_lean_compiler_fold__nat__dec__le(x_3, x_1, x_2); +return x_4; +} +} +obj* _init_l_lean_compiler_nat__fold__fns() { +_start: +{ +obj* x_0; obj* x_1; obj* x_3; obj* x_4; obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_16; obj* x_17; obj* x_18; obj* x_19; obj* x_21; obj* x_22; obj* x_23; obj* x_24; obj* x_26; obj* x_27; obj* x_28; obj* x_29; obj* x_31; obj* x_32; obj* x_33; obj* x_34; obj* x_35; obj* x_36; obj* x_37; obj* x_38; obj* x_39; obj* x_40; obj* x_41; obj* x_42; obj* x_43; obj* x_44; x_0 = lean::box(0); x_1 = lean::mk_string("nat"); lean::inc(x_0); @@ -1483,49 +2002,88 @@ x_3 = lean_name_mk_string(x_0, x_1); x_4 = lean::mk_string("add"); lean::inc(x_3); x_6 = lean_name_mk_string(x_3, x_4); -x_7 = lean::alloc_closure(reinterpret_cast(l_lean_const__folding_fold__nat__add___boxed), 1, 0); +x_7 = lean::alloc_closure(reinterpret_cast(l_lean_compiler_fold__nat__add___boxed), 1, 0); x_8 = lean::alloc_cnstr(0, 2, 0); lean::cnstr_set(x_8, 0, x_6); lean::cnstr_set(x_8, 1, x_7); x_9 = lean::mk_string("mul"); lean::inc(x_3); x_11 = lean_name_mk_string(x_3, x_9); -x_12 = lean::alloc_closure(reinterpret_cast(l_lean_const__folding_fold__nat__mul___boxed), 1, 0); +x_12 = lean::alloc_closure(reinterpret_cast(l_lean_compiler_fold__nat__mul___boxed), 1, 0); x_13 = lean::alloc_cnstr(0, 2, 0); lean::cnstr_set(x_13, 0, x_11); lean::cnstr_set(x_13, 1, x_12); x_14 = lean::mk_string("div"); lean::inc(x_3); x_16 = lean_name_mk_string(x_3, x_14); -x_17 = lean::alloc_closure(reinterpret_cast(l_lean_const__folding_fold__nat__div___boxed), 1, 0); +x_17 = lean::alloc_closure(reinterpret_cast(l_lean_compiler_fold__nat__div___boxed), 1, 0); x_18 = lean::alloc_cnstr(0, 2, 0); lean::cnstr_set(x_18, 0, x_16); lean::cnstr_set(x_18, 1, x_17); x_19 = lean::mk_string("mod"); -x_20 = lean_name_mk_string(x_3, x_19); -x_21 = lean::alloc_closure(reinterpret_cast(l_lean_const__folding_fold__nat__mod___boxed), 1, 0); -x_22 = lean::alloc_cnstr(0, 2, 0); -lean::cnstr_set(x_22, 0, x_20); -lean::cnstr_set(x_22, 1, x_21); -x_23 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_23, 0, x_22); -lean::cnstr_set(x_23, 1, x_0); -x_24 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_24, 0, x_18); -lean::cnstr_set(x_24, 1, x_23); -x_25 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_25, 0, x_13); -lean::cnstr_set(x_25, 1, x_24); -x_26 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_26, 0, x_8); -lean::cnstr_set(x_26, 1, x_25); -x_27 = l_lean_const__folding_uint__bin__fold__fns; -lean::inc(x_27); -x_29 = l_list_append___rarg(x_27, x_26); -return x_29; +lean::inc(x_3); +x_21 = lean_name_mk_string(x_3, x_19); +x_22 = lean::alloc_closure(reinterpret_cast(l_lean_compiler_fold__nat__mod___boxed), 1, 0); +x_23 = lean::alloc_cnstr(0, 2, 0); +lean::cnstr_set(x_23, 0, x_21); +lean::cnstr_set(x_23, 1, x_22); +x_24 = lean::mk_string("dec_eq"); +lean::inc(x_3); +x_26 = lean_name_mk_string(x_3, x_24); +x_27 = lean::alloc_closure(reinterpret_cast(l_lean_compiler_fold__nat__dec__eq___boxed), 3, 0); +x_28 = lean::alloc_cnstr(0, 2, 0); +lean::cnstr_set(x_28, 0, x_26); +lean::cnstr_set(x_28, 1, x_27); +x_29 = lean::mk_string("dec_lt"); +lean::inc(x_3); +x_31 = lean_name_mk_string(x_3, x_29); +x_32 = lean::alloc_closure(reinterpret_cast(l_lean_compiler_fold__nat__dec__lt___boxed), 3, 0); +x_33 = lean::alloc_cnstr(0, 2, 0); +lean::cnstr_set(x_33, 0, x_31); +lean::cnstr_set(x_33, 1, x_32); +x_34 = lean::mk_string("dec_le"); +x_35 = lean_name_mk_string(x_3, x_34); +x_36 = lean::alloc_closure(reinterpret_cast(l_lean_compiler_fold__nat__dec__le___boxed), 3, 0); +x_37 = lean::alloc_cnstr(0, 2, 0); +lean::cnstr_set(x_37, 0, x_35); +lean::cnstr_set(x_37, 1, x_36); +x_38 = lean::alloc_cnstr(1, 2, 0); +lean::cnstr_set(x_38, 0, x_37); +lean::cnstr_set(x_38, 1, x_0); +x_39 = lean::alloc_cnstr(1, 2, 0); +lean::cnstr_set(x_39, 0, x_33); +lean::cnstr_set(x_39, 1, x_38); +x_40 = lean::alloc_cnstr(1, 2, 0); +lean::cnstr_set(x_40, 0, x_28); +lean::cnstr_set(x_40, 1, x_39); +x_41 = lean::alloc_cnstr(1, 2, 0); +lean::cnstr_set(x_41, 0, x_23); +lean::cnstr_set(x_41, 1, x_40); +x_42 = lean::alloc_cnstr(1, 2, 0); +lean::cnstr_set(x_42, 0, x_18); +lean::cnstr_set(x_42, 1, x_41); +x_43 = lean::alloc_cnstr(1, 2, 0); +lean::cnstr_set(x_43, 0, x_13); +lean::cnstr_set(x_43, 1, x_42); +x_44 = lean::alloc_cnstr(1, 2, 0); +lean::cnstr_set(x_44, 0, x_8); +lean::cnstr_set(x_44, 1, x_43); +return x_44; } } -obj* l_lean_const__folding_find__bin__fold__fn__aux___main(obj* x_0, obj* x_1) { +obj* _init_l_lean_compiler_bin__fold__fns() { +_start: +{ +obj* x_0; obj* x_1; obj* x_4; +x_0 = l_lean_compiler_uint__bin__fold__fns; +x_1 = l_lean_compiler_nat__fold__fns; +lean::inc(x_1); +lean::inc(x_0); +x_4 = l_list_append___rarg(x_0, x_1); +return x_4; +} +} +obj* l_lean_compiler_find__bin__fold__fn__aux___main(obj* x_0, obj* x_1) { _start: { if (lean::obj_tag(x_1) == 0) @@ -1569,21 +2127,21 @@ return x_21; } } } -obj* l_lean_const__folding_find__bin__fold__fn__aux(obj* x_0, obj* x_1) { +obj* l_lean_compiler_find__bin__fold__fn__aux(obj* x_0, obj* x_1) { _start: { obj* x_2; -x_2 = l_lean_const__folding_find__bin__fold__fn__aux___main(x_0, x_1); +x_2 = l_lean_compiler_find__bin__fold__fn__aux___main(x_0, x_1); return x_2; } } -obj* l_lean_const__folding_find__bin__fold__fn(obj* x_0) { +obj* l_lean_compiler_find__bin__fold__fn(obj* x_0) { _start: { obj* x_1; obj* x_3; -x_1 = l_lean_const__folding_bin__fold__fns; +x_1 = l_lean_compiler_bin__fold__fns; lean::inc(x_1); -x_3 = l_lean_const__folding_find__bin__fold__fn__aux___main(x_0, x_1); +x_3 = l_lean_compiler_find__bin__fold__fn__aux___main(x_0, x_1); return x_3; } } @@ -1634,9 +2192,9 @@ obj* x_20; obj* x_23; obj* x_25; x_20 = lean::cnstr_get(x_1, 0); lean::inc(x_20); lean::dec(x_1); -x_23 = l_lean_const__folding_bin__fold__fns; +x_23 = l_lean_compiler_bin__fold__fns; lean::inc(x_23); -x_25 = l_lean_const__folding_find__bin__fold__fn__aux___main(x_20, x_23); +x_25 = l_lean_compiler_find__bin__fold__fn__aux___main(x_20, x_23); if (lean::obj_tag(x_25) == 0) { obj* x_29; @@ -1724,7 +2282,7 @@ return x_62; } } } -obj* l_lean_const__folding_fold__bin__op___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) { +obj* l_lean_compiler_fold__bin__op___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) { _start: { uint8 x_4; obj* x_5; @@ -1735,27 +2293,39 @@ return x_5; } void initialize_init_lean_expr(); void initialize_init_platform(); -void initialize_init_data_rbmap_default(); +void initialize_init_lean_compiler_util(); static bool _G_initialized = false; void initialize_init_lean_compiler_const__folding() { if (_G_initialized) return; _G_initialized = true; initialize_init_lean_expr(); initialize_init_platform(); - initialize_init_data_rbmap_default(); - l_lean_const__folding_bin__fold__fn = _init_l_lean_const__folding_bin__fold__fn(); - l_lean_const__folding_mk__uint__type__name___closed__1 = _init_l_lean_const__folding_mk__uint__type__name___closed__1(); - l_lean_const__folding_num__scalar__types = _init_l_lean_const__folding_num__scalar__types(); - l_lean_const__folding_fold__uint__add___closed__1 = _init_l_lean_const__folding_fold__uint__add___closed__1(); - l_lean_const__folding_fold__uint__mul___closed__1 = _init_l_lean_const__folding_fold__uint__mul___closed__1(); - l_lean_const__folding_fold__uint__div___closed__1 = _init_l_lean_const__folding_fold__uint__div___closed__1(); - l_lean_const__folding_fold__uint__mod___closed__1 = _init_l_lean_const__folding_fold__uint__mod___closed__1(); - l_lean_const__folding_fold__uint__sub___closed__1 = _init_l_lean_const__folding_fold__uint__sub___closed__1(); - l_lean_const__folding_pre__uint__bin__fold__fns = _init_l_lean_const__folding_pre__uint__bin__fold__fns(); - l_lean_const__folding_uint__bin__fold__fns = _init_l_lean_const__folding_uint__bin__fold__fns(); - l_lean_const__folding_fold__nat__add___rarg___closed__1 = _init_l_lean_const__folding_fold__nat__add___rarg___closed__1(); - l_lean_const__folding_fold__nat__mul___rarg___closed__1 = _init_l_lean_const__folding_fold__nat__mul___rarg___closed__1(); - l_lean_const__folding_fold__nat__div___rarg___closed__1 = _init_l_lean_const__folding_fold__nat__div___rarg___closed__1(); - l_lean_const__folding_fold__nat__mod___rarg___closed__1 = _init_l_lean_const__folding_fold__nat__mod___rarg___closed__1(); - l_lean_const__folding_bin__fold__fns = _init_l_lean_const__folding_bin__fold__fns(); + initialize_init_lean_compiler_util(); + l_lean_compiler_bin__fold__fn = _init_l_lean_compiler_bin__fold__fn(); + l_lean_compiler_mk__uint__type__name___closed__1 = _init_l_lean_compiler_mk__uint__type__name___closed__1(); + l_lean_compiler_num__scalar__types = _init_l_lean_compiler_num__scalar__types(); + l_lean_compiler_fold__uint__add___closed__1 = _init_l_lean_compiler_fold__uint__add___closed__1(); + l_lean_compiler_fold__uint__mul___closed__1 = _init_l_lean_compiler_fold__uint__mul___closed__1(); + l_lean_compiler_fold__uint__div___closed__1 = _init_l_lean_compiler_fold__uint__div___closed__1(); + l_lean_compiler_fold__uint__mod___closed__1 = _init_l_lean_compiler_fold__uint__mod___closed__1(); + l_lean_compiler_fold__uint__sub___closed__1 = _init_l_lean_compiler_fold__uint__sub___closed__1(); + l_lean_compiler_pre__uint__bin__fold__fns = _init_l_lean_compiler_pre__uint__bin__fold__fns(); + l_lean_compiler_uint__bin__fold__fns = _init_l_lean_compiler_uint__bin__fold__fns(); + l_lean_compiler_fold__nat__add___rarg___closed__1 = _init_l_lean_compiler_fold__nat__add___rarg___closed__1(); + l_lean_compiler_fold__nat__mul___rarg___closed__1 = _init_l_lean_compiler_fold__nat__mul___rarg___closed__1(); + l_lean_compiler_fold__nat__div___rarg___closed__1 = _init_l_lean_compiler_fold__nat__div___rarg___closed__1(); + l_lean_compiler_fold__nat__mod___rarg___closed__1 = _init_l_lean_compiler_fold__nat__mod___rarg___closed__1(); + l_lean_compiler_mk__nat__eq___closed__1 = _init_l_lean_compiler_mk__nat__eq___closed__1(); + l_lean_compiler_mk__nat__lt___closed__1 = _init_l_lean_compiler_mk__nat__lt___closed__1(); + l_lean_compiler_mk__nat__le___closed__1 = _init_l_lean_compiler_mk__nat__le___closed__1(); + l_lean_compiler_to__decidable__expr___closed__1 = _init_l_lean_compiler_to__decidable__expr___closed__1(); + l_lean_compiler_to__decidable__expr___closed__2 = _init_l_lean_compiler_to__decidable__expr___closed__2(); + l_lean_compiler_fold__nat__dec__eq___closed__1 = _init_l_lean_compiler_fold__nat__dec__eq___closed__1(); + l_lean_compiler_fold__nat__dec__eq___closed__2 = _init_l_lean_compiler_fold__nat__dec__eq___closed__2(); + l_lean_compiler_fold__nat__dec__lt___closed__1 = _init_l_lean_compiler_fold__nat__dec__lt___closed__1(); + l_lean_compiler_fold__nat__dec__lt___closed__2 = _init_l_lean_compiler_fold__nat__dec__lt___closed__2(); + l_lean_compiler_fold__nat__dec__le___closed__1 = _init_l_lean_compiler_fold__nat__dec__le___closed__1(); + l_lean_compiler_fold__nat__dec__le___closed__2 = _init_l_lean_compiler_fold__nat__dec__le___closed__2(); + l_lean_compiler_nat__fold__fns = _init_l_lean_compiler_nat__fold__fns(); + l_lean_compiler_bin__fold__fns = _init_l_lean_compiler_bin__fold__fns(); } diff --git a/src/boot/init/lean/compiler/util.cpp b/src/boot/init/lean/compiler/util.cpp new file mode 100644 index 0000000000..7b0fa08150 --- /dev/null +++ b/src/boot/init/lean/compiler/util.cpp @@ -0,0 +1,107 @@ +// Lean compiler output +// Module: init.lean.compiler.util +// Imports: init.lean.expr +#include "runtime/object.h" +#include "runtime/apply.h" +typedef lean::object obj; typedef lean::usize usize; +typedef lean::uint8 uint8; typedef lean::uint16 uint16; +typedef lean::uint32 uint32; typedef lean::uint64 uint64; +#if defined(__clang__) +#pragma clang diagnostic ignored "-Wunused-parameter" +#pragma clang diagnostic ignored "-Wunused-label" +#elif defined(__GNUC__) && !defined(__CLANG__) +#pragma GCC diagnostic ignored "-Wunused-parameter" +#pragma GCC diagnostic ignored "-Wunused-label" +#pragma GCC diagnostic ignored "-Wunused-but-set-variable" +#endif +obj* l_lean_compiler_mk__lc__proof___closed__1; +extern "C" obj* lean_name_mk_string(obj*, obj*); +obj* l_lean_compiler_object__type; +extern "C" obj* lean_expr_mk_const(obj*, obj*); +obj* l_lean_compiler_void__type; +obj* l_lean_compiler_mk__lc__proof(obj*); +obj* l_lean_compiler_neutral__expr; +extern "C" obj* lean_expr_mk_app(obj*, obj*); +obj* l_lean_compiler_unreachable__expr; +obj* _init_l_lean_compiler_neutral__expr() { +_start: +{ +obj* x_0; obj* x_1; obj* x_3; obj* x_4; +x_0 = lean::box(0); +x_1 = lean::mk_string("_neutral"); +lean::inc(x_0); +x_3 = lean_name_mk_string(x_0, x_1); +x_4 = lean_expr_mk_const(x_3, x_0); +return x_4; +} +} +obj* _init_l_lean_compiler_unreachable__expr() { +_start: +{ +obj* x_0; obj* x_1; obj* x_3; obj* x_4; +x_0 = lean::box(0); +x_1 = lean::mk_string("_unreachable"); +lean::inc(x_0); +x_3 = lean_name_mk_string(x_0, x_1); +x_4 = lean_expr_mk_const(x_3, x_0); +return x_4; +} +} +obj* _init_l_lean_compiler_object__type() { +_start: +{ +obj* x_0; obj* x_1; obj* x_3; obj* x_4; +x_0 = lean::box(0); +x_1 = lean::mk_string("_obj"); +lean::inc(x_0); +x_3 = lean_name_mk_string(x_0, x_1); +x_4 = lean_expr_mk_const(x_3, x_0); +return x_4; +} +} +obj* _init_l_lean_compiler_void__type() { +_start: +{ +obj* x_0; obj* x_1; obj* x_3; obj* x_4; +x_0 = lean::box(0); +x_1 = lean::mk_string("_void"); +lean::inc(x_0); +x_3 = lean_name_mk_string(x_0, x_1); +x_4 = lean_expr_mk_const(x_3, x_0); +return x_4; +} +} +obj* _init_l_lean_compiler_mk__lc__proof___closed__1() { +_start: +{ +obj* x_0; obj* x_1; obj* x_3; obj* x_4; +x_0 = lean::box(0); +x_1 = lean::mk_string("lc_proof"); +lean::inc(x_0); +x_3 = lean_name_mk_string(x_0, x_1); +x_4 = lean_expr_mk_const(x_3, x_0); +return x_4; +} +} +obj* l_lean_compiler_mk__lc__proof(obj* x_0) { +_start: +{ +obj* x_1; obj* x_3; +x_1 = l_lean_compiler_mk__lc__proof___closed__1; +lean::inc(x_1); +x_3 = lean_expr_mk_app(x_1, x_0); +return x_3; +} +} +void initialize_init_lean_expr(); +static bool _G_initialized = false; +void initialize_init_lean_compiler_util() { + if (_G_initialized) return; + _G_initialized = true; + initialize_init_lean_expr(); + l_lean_compiler_neutral__expr = _init_l_lean_compiler_neutral__expr(); + l_lean_compiler_unreachable__expr = _init_l_lean_compiler_unreachable__expr(); + l_lean_compiler_object__type = _init_l_lean_compiler_object__type(); + l_lean_compiler_void__type = _init_l_lean_compiler_void__type(); + l_lean_compiler_mk__lc__proof___closed__1 = _init_l_lean_compiler_mk__lc__proof___closed__1(); +} diff --git a/src/boot/init/lean/expr.cpp b/src/boot/init/lean/expr.cpp index 9519f31fc5..5cc6073b7a 100644 --- a/src/boot/init/lean/expr.cpp +++ b/src/boot/init/lean/expr.cpp @@ -14,18 +14,24 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64; #pragma GCC diagnostic ignored "-Wunused-label" #pragma GCC diagnostic ignored "-Wunused-but-set-variable" #endif +obj* l_lean_mk__dec__is__true___closed__1; obj* l_lean_expr_dbg__to__string___boxed(obj*); obj* l_lean_expr_mk__app(obj*, obj*); obj* l_list_foldl___main___at_lean_expr_mk__app___spec__1(obj*, obj*); +extern "C" obj* lean_name_mk_string(obj*, obj*); +obj* l_lean_mk__dec__is__true(obj*, obj*); +obj* l_lean_mk__dec__is__false(obj*, obj*); extern "C" obj* lean_expr_mk_const(obj*, obj*); +obj* l_lean_get__app__fn___main(obj*); extern "C" obj* lean_expr_dbg_to_string(obj*); -obj* l_lean_expr_get__app__fn(obj*); obj* l_lean_expr__is__inhabited; -obj* l_lean_expr_get__app__fn___main(obj*); +obj* l_lean_get__app__fn(obj*); +obj* l_lean_mk__bin__app(obj*, obj*, obj*); obj* l_lean_expr_mk__capp(obj*, obj*); extern "C" obj* lean_expr_mk_app(obj*, obj*); obj* l_lean_expr_hash___boxed(obj*); extern "C" usize lean_expr_hash(obj*); +obj* l_lean_mk__dec__is__false___closed__1; obj* _init_l_lean_expr__is__inhabited() { _start: { @@ -94,7 +100,7 @@ x_1 = lean_expr_dbg_to_string(x_0); return x_1; } } -obj* l_lean_expr_get__app__fn___main(obj* x_0) { +obj* l_lean_get__app__fn___main(obj* x_0) { _start: { switch (lean::obj_tag(x_0)) { @@ -154,14 +160,71 @@ return x_0; } } } -obj* l_lean_expr_get__app__fn(obj* x_0) { +obj* l_lean_get__app__fn(obj* x_0) { _start: { obj* x_1; -x_1 = l_lean_expr_get__app__fn___main(x_0); +x_1 = l_lean_get__app__fn___main(x_0); return x_1; } } +obj* l_lean_mk__bin__app(obj* x_0, obj* x_1, obj* x_2) { +_start: +{ +obj* x_3; obj* x_4; +x_3 = lean_expr_mk_app(x_0, x_1); +x_4 = lean_expr_mk_app(x_3, x_2); +return x_4; +} +} +obj* _init_l_lean_mk__dec__is__true___closed__1() { +_start: +{ +obj* x_0; obj* x_1; obj* x_3; obj* x_4; obj* x_5; obj* x_6; +x_0 = lean::box(0); +x_1 = lean::mk_string("decidable"); +lean::inc(x_0); +x_3 = lean_name_mk_string(x_0, x_1); +x_4 = lean::mk_string("is_true"); +x_5 = lean_name_mk_string(x_3, x_4); +x_6 = lean_expr_mk_const(x_5, x_0); +return x_6; +} +} +obj* l_lean_mk__dec__is__true(obj* x_0, obj* x_1) { +_start: +{ +obj* x_2; obj* x_4; +x_2 = l_lean_mk__dec__is__true___closed__1; +lean::inc(x_2); +x_4 = l_lean_mk__bin__app(x_2, x_0, x_1); +return x_4; +} +} +obj* _init_l_lean_mk__dec__is__false___closed__1() { +_start: +{ +obj* x_0; obj* x_1; obj* x_3; obj* x_4; obj* x_5; obj* x_6; +x_0 = lean::box(0); +x_1 = lean::mk_string("decidable"); +lean::inc(x_0); +x_3 = lean_name_mk_string(x_0, x_1); +x_4 = lean::mk_string("is_false"); +x_5 = lean_name_mk_string(x_3, x_4); +x_6 = lean_expr_mk_const(x_5, x_0); +return x_6; +} +} +obj* l_lean_mk__dec__is__false(obj* x_0, obj* x_1) { +_start: +{ +obj* x_2; obj* x_4; +x_2 = l_lean_mk__dec__is__false___closed__1; +lean::inc(x_2); +x_4 = l_lean_mk__bin__app(x_2, x_0, x_1); +return x_4; +} +} void initialize_init_lean_level(); void initialize_init_lean_kvmap(); static bool _G_initialized = false; @@ -171,4 +234,6 @@ void initialize_init_lean_expr() { initialize_init_lean_level(); initialize_init_lean_kvmap(); l_lean_expr__is__inhabited = _init_l_lean_expr__is__inhabited(); + l_lean_mk__dec__is__true___closed__1 = _init_l_lean_mk__dec__is__true___closed__1(); + l_lean_mk__dec__is__false___closed__1 = _init_l_lean_mk__dec__is__false___closed__1(); } diff --git a/src/boot/init/lean/level.cpp b/src/boot/init/lean/level.cpp index 319f380475..4d98b4e8f4 100644 --- a/src/boot/init/lean/level.cpp +++ b/src/boot/init/lean/level.cpp @@ -76,6 +76,7 @@ obj* l_lean_level__to__format_level__has__to__string; obj* l_lean_level__to__format_result__list_to__format___main(obj*); extern "C" usize lean_level_hash(obj*); obj* l_lean_level_to__nat(obj*); +obj* l_lean_level_one; obj* l_nat_repr(obj*); obj* l_lean_level__to__format_result_imax(obj*, obj*); namespace lean { @@ -93,6 +94,15 @@ x_0 = lean::box(0); return x_0; } } +obj* _init_l_lean_level_one() { +_start: +{ +obj* x_0; obj* x_1; +x_0 = lean::box(0); +x_1 = level_mk_succ(x_0); +return x_1; +} +} obj* l_lean_level_has__param___main(obj* x_0) { _start: { @@ -1358,6 +1368,7 @@ void initialize_init_lean_level() { initialize_init_lean_name(); initialize_init_data_option_basic(); l_lean_level__is__inhabited = _init_l_lean_level__is__inhabited(); + l_lean_level_one = _init_l_lean_level_one(); l_lean_level_to__nat___main___closed__1 = _init_l_lean_level_to__nat___main___closed__1(); l_lean_level_to__nat___main___closed__2 = _init_l_lean_level_to__nat___main___closed__2(); l_lean_level_to__nat___main___closed__3 = _init_l_lean_level_to__nat___main___closed__3(); diff --git a/src/library/compiler/csimp.cpp b/src/library/compiler/csimp.cpp index 6a330d3040..43ac27658a 100644 --- a/src/library/compiler/csimp.cpp +++ b/src/library/compiler/csimp.cpp @@ -1399,70 +1399,6 @@ class csimp_fn { } } - expr visit_nat_add(expr const & e) { - nat a, b; - if (!get_binary_nat_lits(e, a, b)) return visit_app_default(e); - return to_nat_expr(a+b); - } - - expr visit_nat_mul(expr const & e) { - nat a, b; - if (!get_binary_nat_lits(e, a, b)) return visit_app_default(e); - return to_nat_expr(a*b); - } - - expr visit_nat_sub(expr const & e) { - nat a, b; - if (!get_binary_nat_lits(e, a, b)) return visit_app_default(e); - return to_nat_expr(a-b); - } - - expr to_bool_expr(bool b) { - return b ? mk_bool_tt() : mk_bool_ff(); - } - - expr visit_nat_beq(expr const & e) { - nat a, b; - if (!get_binary_nat_lits(e, a, b)) return visit_app_default(e); - return to_bool_expr(a == b); - } - - expr visit_nat_ble(expr const & e) { - nat a, b; - if (!get_binary_nat_lits(e, a, b)) return visit_app_default(e); - return to_bool_expr(a <= b); - } - - expr to_decidable_expr(bool b, expr const & e) { - if (m_before_erasure) { - expr type = whnf_infer_type(e); - expr const & p = app_arg(type); - if (b) { - return mk_app(mk_constant(get_decidable_is_true_name()), p, mk_app(mk_constant(get_lc_proof_name()), p)); - } else { - return mk_app(mk_constant(get_decidable_is_false_name()), p, mk_app(mk_constant(get_lc_proof_name()), p)); - } - } else { - if (b) { - return mk_app(mk_constant(get_decidable_is_true_name()), mk_enf_neutral(), mk_enf_neutral()); - } else { - return mk_app(mk_constant(get_decidable_is_false_name()), mk_enf_neutral(), mk_enf_neutral()); - } - } - } - - expr visit_nat_dec_eq(expr const & e) { - nat a, b; - if (!get_binary_nat_lits(e, a, b)) return visit_app_default(e); - return to_decidable_expr(a == b, e); - } - - expr visit_nat_decidable_lt(expr const & e) { - nat a, b; - if (!get_binary_nat_lits(e, a, b)) return visit_app_default(e); - return to_decidable_expr(a < b, e); - } - expr visit_app_default(expr const & e) { if (already_simplified(e)) return e; buffer args; @@ -1508,21 +1444,7 @@ class csimp_fn { } } name const & n = const_name(fn); - if (n == get_nat_add_name()) { - return visit_nat_add(e); - } else if (n == get_nat_mul_name()) { - return visit_nat_mul(e); - } else if (n == get_nat_sub_name()) { - return visit_nat_sub(e); - } else if (n == get_nat_dec_eq_name()) { - return visit_nat_dec_eq(e); - } else if (n == get_nat_decidable_lt_name()) { - return visit_nat_decidable_lt(e); - } else if (n == get_nat_beq_name()) { - return visit_nat_beq(e); - } else if (n == get_nat_ble_name()) { - return visit_nat_ble(e); - } else if (n == get_nat_succ_name()) { + if (n == get_nat_succ_name()) { return visit_nat_succ(e); } else if (n == get_nat_zero_name()) { return mk_lit(literal(nat(0)));