From 6be50f0133a0168cd2d22f00a2bd407490359704 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 2 Feb 2014 15:01:48 -0800 Subject: [PATCH] refactor(builtin/heq): merge cast and heq modules Signed-off-by: Leonardo de Moura --- examples/lean/dep_if.lean | 2 +- src/builtin/CMakeLists.txt | 2 -- src/builtin/cast.lean | 1 - src/builtin/obj/cast.olean | Bin 62 -> 0 bytes src/library/CMakeLists.txt | 2 +- src/library/cast_decls.cpp | 9 --------- src/library/cast_decls.h | 8 -------- src/library/simplifier/simplifier.cpp | 5 +---- tests/lean/simp18.lean | 3 +-- tests/lean/simp18.lean.expected.out | 2 +- tests/lean/simp19.lean | 2 +- tests/lean/simp19.lean.expected.out | 2 +- tests/lean/simp20.lean | 2 +- tests/lean/simp20.lean.expected.out | 2 +- tests/lean/simp22.lean | 2 +- tests/lean/simp22.lean.expected.out | 2 +- tests/lean/simp23.lean | 2 +- tests/lean/simp23.lean.expected.out | 2 +- tests/lean/simp28.lean | 2 +- tests/lean/simp28.lean.expected.out | 2 +- tests/lean/simp30.lean | 2 +- tests/lean/simp30.lean.expected.out | 2 +- tests/lean/simp32.lean | 2 +- tests/lean/simp32.lean.expected.out | 2 +- tests/lean/tactic_at_types.lean | 2 +- tests/lean/tactic_at_types.lean.expected.out | 2 +- 26 files changed, 21 insertions(+), 45 deletions(-) delete mode 100644 src/builtin/cast.lean delete mode 100644 src/builtin/obj/cast.olean delete mode 100644 src/library/cast_decls.cpp delete mode 100644 src/library/cast_decls.h diff --git a/examples/lean/dep_if.lean b/examples/lean/dep_if.lean index e89113c322..4ce6681c58 100644 --- a/examples/lean/dep_if.lean +++ b/examples/lean/dep_if.lean @@ -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) diff --git a/src/builtin/CMakeLists.txt b/src/builtin/CMakeLists.txt index 5ea6cf10f5..e426fab09a 100644 --- a/src/builtin/CMakeLists.txt +++ b/src/builtin/CMakeLists.txt @@ -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" "") \ No newline at end of file diff --git a/src/builtin/cast.lean b/src/builtin/cast.lean deleted file mode 100644 index 2fc7ea68e0..0000000000 --- a/src/builtin/cast.lean +++ /dev/null @@ -1 +0,0 @@ -import heq diff --git a/src/builtin/obj/cast.olean b/src/builtin/obj/cast.olean deleted file mode 100644 index 431b4fac16891182e3728aaeb05c7d944a9d9e51..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 62 ycmd1LNlna4%gjk-fC9$M+=Bd~5{B&5qP)}`1}M)ju>{7Y&f7!vyc diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index c30e4b17be..f1004af735 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -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}) diff --git a/src/library/cast_decls.cpp b/src/library/cast_decls.cpp deleted file mode 100644 index 13acd55d38..0000000000 --- a/src/library/cast_decls.cpp +++ /dev/null @@ -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 { -} diff --git a/src/library/cast_decls.h b/src/library/cast_decls.h deleted file mode 100644 index 2776d59c2c..0000000000 --- a/src/library/cast_decls.h +++ /dev/null @@ -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 { -} diff --git a/src/library/simplifier/simplifier.cpp b/src/library/simplifier/simplifier.cpp index 4bca471684..df0abebb2c 100644 --- a/src/library/simplifier/simplifier.cpp +++ b/src/library/simplifier/simplifier.cpp @@ -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 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 diff --git a/tests/lean/simp18.lean b/tests/lean/simp18.lean index b33e78550c..d880fb62c6 100644 --- a/tests/lean/simp18.lean +++ b/tests/lean/simp18.lean @@ -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) *) - diff --git a/tests/lean/simp18.lean.expected.out b/tests/lean/simp18.lean.expected.out index deab11cf49..e70b78cf6b 100644 --- a/tests/lean/simp18.lean.expected.out +++ b/tests/lean/simp18.lean.expected.out @@ -1,6 +1,6 @@ Set: pp::colors Set: pp::unicode - Imported 'cast' + Imported 'heq' Assumed: vec Assumed: concat Assumed: concat_assoc diff --git a/tests/lean/simp19.lean b/tests/lean/simp19.lean index 24780bef37..49ef4c4530 100644 --- a/tests/lean/simp19.lean +++ b/tests/lean/simp19.lean @@ -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 diff --git a/tests/lean/simp19.lean.expected.out b/tests/lean/simp19.lean.expected.out index e9f7dd999e..49f8d48b39 100644 --- a/tests/lean/simp19.lean.expected.out +++ b/tests/lean/simp19.lean.expected.out @@ -1,6 +1,6 @@ Set: pp::colors Set: pp::unicode - Imported 'cast' + Imported 'heq' Assumed: vec Assumed: concat Assumed: concat_assoc diff --git a/tests/lean/simp20.lean b/tests/lean/simp20.lean index f400ea93ce..3e33da300e 100644 --- a/tests/lean/simp20.lean +++ b/tests/lean/simp20.lean @@ -1,4 +1,4 @@ -import cast +import heq rewrite_set simple set_option pp::implicit true diff --git a/tests/lean/simp20.lean.expected.out b/tests/lean/simp20.lean.expected.out index 30526eb0ce..d754b383e9 100644 --- a/tests/lean/simp20.lean.expected.out +++ b/tests/lean/simp20.lean.expected.out @@ -1,6 +1,6 @@ Set: pp::colors Set: pp::unicode - Imported 'cast' + Imported 'heq' Set: lean::pp::implicit Assumed: g Assumed: B diff --git a/tests/lean/simp22.lean b/tests/lean/simp22.lean index c459e69e12..c891353702 100644 --- a/tests/lean/simp22.lean +++ b/tests/lean/simp22.lean @@ -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 diff --git a/tests/lean/simp22.lean.expected.out b/tests/lean/simp22.lean.expected.out index 45756fdd4a..e9f9764ec1 100644 --- a/tests/lean/simp22.lean.expected.out +++ b/tests/lean/simp22.lean.expected.out @@ -1,6 +1,6 @@ Set: pp::colors Set: pp::unicode - Imported 'cast' + Imported 'heq' Assumed: vec Assumed: concat Assumed: concat_assoc diff --git a/tests/lean/simp23.lean b/tests/lean/simp23.lean index 39a6bb1855..f7a7b36ee9 100644 --- a/tests/lean/simp23.lean +++ b/tests/lean/simp23.lean @@ -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 diff --git a/tests/lean/simp23.lean.expected.out b/tests/lean/simp23.lean.expected.out index 92a019b691..b8ac13d2b7 100644 --- a/tests/lean/simp23.lean.expected.out +++ b/tests/lean/simp23.lean.expected.out @@ -1,6 +1,6 @@ Set: pp::colors Set: pp::unicode - Imported 'cast' + Imported 'heq' Assumed: vec Assumed: concat Assumed: concat_assoc diff --git a/tests/lean/simp28.lean b/tests/lean/simp28.lean index 1e4693e4f2..723d30e09e 100644 --- a/tests/lean/simp28.lean +++ b/tests/lean/simp28.lean @@ -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 diff --git a/tests/lean/simp28.lean.expected.out b/tests/lean/simp28.lean.expected.out index 242982b1d8..bfa0fe07c7 100644 --- a/tests/lean/simp28.lean.expected.out +++ b/tests/lean/simp28.lean.expected.out @@ -1,6 +1,6 @@ Set: pp::colors Set: pp::unicode - Imported 'cast' + Imported 'heq' Assumed: vec Assumed: concat Assumed: concat_assoc diff --git a/tests/lean/simp30.lean b/tests/lean/simp30.lean index dd71d6d441..47c7c0821f 100644 --- a/tests/lean/simp30.lean +++ b/tests/lean/simp30.lean @@ -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 diff --git a/tests/lean/simp30.lean.expected.out b/tests/lean/simp30.lean.expected.out index f2433ceb2a..7058cc614a 100644 --- a/tests/lean/simp30.lean.expected.out +++ b/tests/lean/simp30.lean.expected.out @@ -1,6 +1,6 @@ Set: pp::colors Set: pp::unicode - Imported 'cast' + Imported 'heq' Assumed: vec Assumed: concat Assumed: concat_assoc diff --git a/tests/lean/simp32.lean b/tests/lean/simp32.lean index 398fc5cee7..348905b280 100644 --- a/tests/lean/simp32.lean +++ b/tests/lean/simp32.lean @@ -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 diff --git a/tests/lean/simp32.lean.expected.out b/tests/lean/simp32.lean.expected.out index 3d469f871a..74155a10b1 100644 --- a/tests/lean/simp32.lean.expected.out +++ b/tests/lean/simp32.lean.expected.out @@ -1,6 +1,6 @@ Set: pp::colors Set: pp::unicode - Imported 'cast' + Imported 'heq' Assumed: vec Assumed: concat Assumed: concat_assoc diff --git a/tests/lean/tactic_at_types.lean b/tests/lean/tactic_at_types.lean index 2b89f4904a..380be9fb41 100644 --- a/tests/lean/tactic_at_types.lean +++ b/tests/lean/tactic_at_types.lean @@ -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 diff --git a/tests/lean/tactic_at_types.lean.expected.out b/tests/lean/tactic_at_types.lean.expected.out index 5fc950481c..7c2a7e140d 100644 --- a/tests/lean/tactic_at_types.lean.expected.out +++ b/tests/lean/tactic_at_types.lean.expected.out @@ -1,7 +1,7 @@ Set: pp::colors Set: pp::unicode Imported 'tactic' - Imported 'cast' + Imported 'heq' Set: lean::pp::implicit Assumed: vec Assumed: n