refactor(builtin/heq): merge cast and heq modules
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
c56df132b8
commit
6be50f0133
26 changed files with 21 additions and 45 deletions
|
|
@ -65,7 +65,7 @@ theorem dep_if_elim_else {A : TypeU} (c : Bool) (t : c → A) (e : ¬ c → A) (
|
|||
theorem dep_if_false {A : TypeU} (t : false → A) (e : ¬ false → A) : dep_if false t e = e not_false_trivial
|
||||
:= dep_if_elim_else false t e not_false_trivial
|
||||
|
||||
import cast
|
||||
import heq
|
||||
|
||||
theorem dep_if_congr {A : TypeM} (c1 c2 : Bool)
|
||||
(t1 : c1 → A) (t2 : c2 → A)
|
||||
|
|
|
|||
|
|
@ -94,11 +94,9 @@ add_theory("Int.lean" "${CMAKE_CURRENT_BINARY_DIR}/Nat.olean")
|
|||
add_theory("Real.lean" "${CMAKE_CURRENT_BINARY_DIR}/Int.olean")
|
||||
add_theory("specialfn.lean" "${CMAKE_CURRENT_BINARY_DIR}/Real.olean")
|
||||
add_theory("heq.lean" "${CMAKE_CURRENT_BINARY_DIR}/Nat.olean")
|
||||
add_theory("cast.lean" "${CMAKE_CURRENT_BINARY_DIR}/heq.olean")
|
||||
|
||||
update_interface("kernel.olean" "kernel" "-n")
|
||||
update_interface("Nat.olean" "library/arith" "-n")
|
||||
update_interface("Int.olean" "library/arith" "")
|
||||
update_interface("Real.olean" "library/arith" "")
|
||||
update_interface("heq.olean" "library" "")
|
||||
update_interface("cast.olean" "library" "")
|
||||
|
|
@ -1 +0,0 @@
|
|||
import heq
|
||||
Binary file not shown.
|
|
@ -1,6 +1,6 @@
|
|||
add_library(library kernel_bindings.cpp deep_copy.cpp
|
||||
context_to_lambda.cpp placeholder.cpp expr_lt.cpp substitution.cpp
|
||||
fo_unify.cpp bin_op.cpp equality.cpp io_state_stream.cpp printer.cpp
|
||||
hop_match.cpp heq_decls.cpp cast_decls.cpp)
|
||||
hop_match.cpp heq_decls.cpp)
|
||||
|
||||
target_link_libraries(library ${LEAN_LIBS})
|
||||
|
|
|
|||
|
|
@ -1,9 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
*/
|
||||
// Automatically generated file, DO NOT EDIT
|
||||
#include "kernel/environment.h"
|
||||
#include "kernel/decl_macros.h"
|
||||
namespace lean {
|
||||
}
|
||||
|
|
@ -1,8 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
*/
|
||||
// Automatically generated file, DO NOT EDIT
|
||||
#include "kernel/expr.h"
|
||||
namespace lean {
|
||||
}
|
||||
|
|
@ -20,7 +20,6 @@ Author: Leonardo de Moura
|
|||
#include "kernel/max_sharing.h"
|
||||
#include "kernel/occurs.h"
|
||||
#include "library/heq_decls.h"
|
||||
#include "library/cast_decls.h"
|
||||
#include "library/kernel_bindings.h"
|
||||
#include "library/expr_pair.h"
|
||||
#include "library/hop_match.h"
|
||||
|
|
@ -131,7 +130,6 @@ class simplifier_cell::imp {
|
|||
options m_options;
|
||||
type_checker m_tc;
|
||||
bool m_has_heq;
|
||||
bool m_has_cast;
|
||||
rule_sets m_rule_sets;
|
||||
cache m_cache;
|
||||
max_sharing_fn m_max_sharing;
|
||||
|
|
@ -460,7 +458,7 @@ class simplifier_cell::imp {
|
|||
}
|
||||
|
||||
result simplify_app(expr const & e) {
|
||||
if (m_has_cast && is_cast(e)) {
|
||||
if (m_has_heq && is_cast(e)) {
|
||||
// e is of the form (cast A B H a)
|
||||
// a : A
|
||||
// e : B
|
||||
|
|
@ -1515,7 +1513,6 @@ public:
|
|||
std::shared_ptr<simplifier_monitor> const & monitor):
|
||||
m_env(env), m_options(o), m_tc(env), m_monitor(monitor) {
|
||||
m_has_heq = m_env->imported("heq");
|
||||
m_has_cast = m_env->imported("cast");
|
||||
set_options(o);
|
||||
if (m_contextual) {
|
||||
// We need an extra rule set if we are performing contextual rewriting
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
import cast
|
||||
import heq
|
||||
variable vec : Nat → Type
|
||||
variable concat {n m : Nat} (v : vec n) (w : vec m) : vec (n + m)
|
||||
infixl 65 ; : concat
|
||||
|
|
@ -26,4 +26,3 @@ print(t2)
|
|||
print(pr)
|
||||
get_environment():type_check(pr)
|
||||
*)
|
||||
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
Set: pp::colors
|
||||
Set: pp::unicode
|
||||
Imported 'cast'
|
||||
Imported 'heq'
|
||||
Assumed: vec
|
||||
Assumed: concat
|
||||
Assumed: concat_assoc
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
import cast
|
||||
import heq
|
||||
variable vec : Nat → Type
|
||||
variable concat {n m : Nat} (v : vec n) (w : vec m) : vec (n + m)
|
||||
infixl 65 ; : concat
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
Set: pp::colors
|
||||
Set: pp::unicode
|
||||
Imported 'cast'
|
||||
Imported 'heq'
|
||||
Assumed: vec
|
||||
Assumed: concat
|
||||
Assumed: concat_assoc
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
import cast
|
||||
import heq
|
||||
rewrite_set simple
|
||||
|
||||
set_option pp::implicit true
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
Set: pp::colors
|
||||
Set: pp::unicode
|
||||
Imported 'cast'
|
||||
Imported 'heq'
|
||||
Set: lean::pp::implicit
|
||||
Assumed: g
|
||||
Assumed: B
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
import cast
|
||||
import heq
|
||||
variable vec : Nat → Type
|
||||
variable concat {n m : Nat} (v : vec n) (w : vec m) : vec (n + m)
|
||||
infixl 65 ; : concat
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
Set: pp::colors
|
||||
Set: pp::unicode
|
||||
Imported 'cast'
|
||||
Imported 'heq'
|
||||
Assumed: vec
|
||||
Assumed: concat
|
||||
Assumed: concat_assoc
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
import cast
|
||||
import heq
|
||||
variable vec : Nat → Type
|
||||
variable concat {n m : Nat} (v : vec n) (w : vec m) : vec (n + m)
|
||||
infixl 65 ; : concat
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
Set: pp::colors
|
||||
Set: pp::unicode
|
||||
Imported 'cast'
|
||||
Imported 'heq'
|
||||
Assumed: vec
|
||||
Assumed: concat
|
||||
Assumed: concat_assoc
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
import cast
|
||||
import heq
|
||||
variable vec : Nat → Type
|
||||
variable concat {n m : Nat} (v : vec n) (w : vec m) : vec (n + m)
|
||||
infixl 65 ; : concat
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
Set: pp::colors
|
||||
Set: pp::unicode
|
||||
Imported 'cast'
|
||||
Imported 'heq'
|
||||
Assumed: vec
|
||||
Assumed: concat
|
||||
Assumed: concat_assoc
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
import cast
|
||||
import heq
|
||||
variable vec : Nat → Type
|
||||
variable concat {n m : Nat} (v : vec n) (w : vec m) : vec (n + m)
|
||||
infixl 65 ; : concat
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
Set: pp::colors
|
||||
Set: pp::unicode
|
||||
Imported 'cast'
|
||||
Imported 'heq'
|
||||
Assumed: vec
|
||||
Assumed: concat
|
||||
Assumed: concat_assoc
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
import cast
|
||||
import heq
|
||||
variable vec : Nat → Type
|
||||
variable concat {n m : Nat} (v : vec n) (w : vec m) : vec (n + m)
|
||||
infixl 65 ; : concat
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
Set: pp::colors
|
||||
Set: pp::unicode
|
||||
Imported 'cast'
|
||||
Imported 'heq'
|
||||
Assumed: vec
|
||||
Assumed: concat
|
||||
Assumed: concat_assoc
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
import tactic
|
||||
import cast
|
||||
import heq
|
||||
set_option pp::implicit true -- to be able to parse output produced by Lean
|
||||
variable vec : Nat → Type
|
||||
variables n m : Nat
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
Set: pp::colors
|
||||
Set: pp::unicode
|
||||
Imported 'tactic'
|
||||
Imported 'cast'
|
||||
Imported 'heq'
|
||||
Set: lean::pp::implicit
|
||||
Assumed: vec
|
||||
Assumed: n
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue