feat(library/init/lean/compiler): fold nat predicates
This commit is contained in:
Leonardo de Moura
parent
90a1616cff
commit
e0fd89e165
10 changed files with 1094 additions and 356 deletions
|
|
@ -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
|
||||
|
|
|
|||
19
library/init/lean/compiler/util.lean
Normal file
19
library/init/lean/compiler/util.lean
Normal file
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load diff
107
src/boot/init/lean/compiler/util.cpp
Normal file
107
src/boot/init/lean/compiler/util.cpp
Normal file
|
|
@ -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();
|
||||
}
|
||||
|
|
@ -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();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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();
|
||||
|
|
|
|||
|
|
@ -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<expr> 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)));
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue