diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/coqlib.ml | 88 | ||||
| -rw-r--r-- | interp/coqlib.mli | 20 |
2 files changed, 78 insertions, 30 deletions
diff --git a/interp/coqlib.ml b/interp/coqlib.ml index 087a519826..e110ad00a0 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -82,6 +82,8 @@ let init_reference dir s = gen_reference "Coqlib" ("Init"::dir) s let init_constant dir s = gen_constant "Coqlib" ("Init"::dir) s +let logic_constant dir s = gen_constant "Coqlib" ("Logic"::dir) s + let arith_dir = ["Coq";"Arith"] let arith_modules = [arith_dir] @@ -107,9 +109,18 @@ let datatypes_id = id_of_string "Datatypes" let logic_module_name = ["Coq";"Init";"Logic"] let logic_module = make_dir logic_module_name -let logic_type_module = make_dir ["Coq";"Init";"Logic_Type"] -let datatypes_module = make_dir ["Coq";"Init";"Datatypes"] -let arith_module = make_dir ["Coq";"Arith";"Arith"] + +let logic_type_module_name = ["Coq";"Init";"Logic_Type"] +let logic_type_module = make_dir logic_type_module_name + +let datatypes_module_name = ["Coq";"Init";"Datatypes"] +let datatypes_module = make_dir datatypes_module_name + +let arith_module_name = ["Coq";"Arith";"Arith"] +let arith_module = make_dir arith_module_name + +let jmeq_module_name = ["Coq";"Logic";"JMeq"] +let jmeq_module = make_dir jmeq_module_name (* TODO: temporary hack *) let make_kn dir id = Libnames.encode_kn dir id @@ -145,9 +156,14 @@ let glob_false = ConstructRef path_of_false (** Equality *) let eq_kn = make_kn logic_module (id_of_string "eq") - let glob_eq = IndRef (eq_kn,0) +let identity_kn = make_kn datatypes_module (id_of_string "identity") +let glob_identity = IndRef (identity_kn,0) + +let jmeq_kn = make_kn jmeq_module (id_of_string "JMeq") +let glob_jmeq = IndRef (jmeq_kn,0) + type coq_sigma_data = { proj1 : constr; proj2 : constr; @@ -185,18 +201,24 @@ let build_prod () = typ = init_constant ["Datatypes"] "prod" } (* Equalities *) -type coq_leibniz_eq_data = { +type coq_eq_data = { eq : constr; - refl : constr; ind : constr; + refl : constr; + sym : constr; + trans: constr; + congr: constr } + +type coq_rewrite_data = { rrec : constr option; - rect : constr option; - congr: constr; - sym : constr } + rect : constr option +} let lazy_init_constant dir id = lazy (init_constant dir id) +let lazy_logic_constant dir id = lazy (logic_constant dir id) + +(* Leibniz equality on Type *) -(* Equality on Set *) let coq_eq_eq = lazy_init_constant ["Logic"] "eq" let coq_eq_refl = lazy_init_constant ["Logic"] "eq_refl" let coq_eq_ind = lazy_init_constant ["Logic"] "eq_ind" @@ -204,17 +226,17 @@ let coq_eq_rec = lazy_init_constant ["Logic"] "eq_rec" let coq_eq_rect = lazy_init_constant ["Logic"] "eq_rect" let coq_eq_congr = lazy_init_constant ["Logic"] "f_equal" let coq_eq_sym = lazy_init_constant ["Logic"] "eq_sym" +let coq_eq_trans = lazy_init_constant ["Logic"] "eq_trans" let coq_f_equal2 = lazy_init_constant ["Logic"] "f_equal2" let build_coq_eq_data () = let _ = check_required_library logic_module_name in { eq = Lazy.force coq_eq_eq; - refl = Lazy.force coq_eq_refl; ind = Lazy.force coq_eq_ind; - rrec = Some (Lazy.force coq_eq_rec); - rect = Some (Lazy.force coq_eq_rect); - congr = Lazy.force coq_eq_congr; - sym = Lazy.force coq_eq_sym } + refl = Lazy.force coq_eq_refl; + sym = Lazy.force coq_eq_sym; + trans = Lazy.force coq_eq_trans; + congr = Lazy.force coq_eq_congr } let build_coq_eq () = Lazy.force coq_eq_eq let build_coq_eq_sym () = Lazy.force coq_eq_sym @@ -222,6 +244,26 @@ let build_coq_f_equal2 () = Lazy.force coq_f_equal2 let build_coq_sym_eq = build_coq_eq_sym (* compatibility *) +(* Heterogenous equality on Type *) + +let coq_jmeq_eq = lazy_logic_constant ["JMeq"] "JMeq" +let coq_jmeq_refl = lazy_logic_constant ["JMeq"] "JMeq_refl" +let coq_jmeq_ind = lazy_logic_constant ["JMeq"] "JMeq_ind" +let coq_jmeq_rec = lazy_logic_constant ["JMeq"] "JMeq_rec" +let coq_jmeq_rect = lazy_logic_constant ["JMeq"] "JMeq_rect" +let coq_jmeq_sym = lazy_logic_constant ["JMeq"] "JMeq_sym" +let coq_jmeq_congr = lazy_logic_constant ["JMeq"] "JMeq_congr" +let coq_jmeq_trans = lazy_logic_constant ["JMeq"] "JMeq_trans" + +let build_coq_jmeq_data () = + let _ = check_required_library jmeq_module_name in { + eq = Lazy.force coq_jmeq_eq; + ind = Lazy.force coq_jmeq_ind; + refl = Lazy.force coq_jmeq_refl; + sym = Lazy.force coq_jmeq_sym; + trans = Lazy.force coq_jmeq_trans; + congr = Lazy.force coq_jmeq_congr } + (* Specif *) let coq_sumbool = lazy_init_constant ["Specif"] "sumbool" @@ -235,15 +277,16 @@ let coq_identity_rec = lazy_init_constant ["Datatypes"] "identity_rec" let coq_identity_rect = lazy_init_constant ["Datatypes"] "identity_rect" let coq_identity_congr = lazy_init_constant ["Logic_Type"] "identity_congr" let coq_identity_sym = lazy_init_constant ["Logic_Type"] "identity_sym" +let coq_identity_trans = lazy_init_constant ["Logic_Type"] "identity_trans" -let build_coq_identity_data () = { +let build_coq_identity_data () = + let _ = check_required_library datatypes_module_name in { eq = Lazy.force coq_identity_eq; - refl = Lazy.force coq_identity_refl; ind = Lazy.force coq_identity_ind; - rrec = Some (Lazy.force coq_identity_rec); - rect = Some (Lazy.force coq_identity_rect); - congr = Lazy.force coq_identity_congr; - sym = Lazy.force coq_identity_sym } + refl = Lazy.force coq_identity_refl; + sym = Lazy.force coq_identity_sym; + trans = Lazy.force coq_identity_trans; + congr = Lazy.force coq_identity_congr } (* The False proposition *) let coq_False = lazy_init_constant ["Logic"] "False" @@ -281,7 +324,8 @@ let build_coq_iff_right_proj () = Lazy.force coq_iff_right_proj (* The following is less readable but does not depend on parsing *) let coq_eq_ref = lazy (init_reference ["Logic"] "eq") -let coq_identity_ref = lazy (init_reference ["Datatypes"] "identity") +let coq_identity_ref = lazy (init_reference ["Datatypes"] "identity") +let coq_jmeq_ref = lazy (gen_reference "Coqlib" ["Logic";"JMeq"] "JMeq") let coq_existS_ref = lazy (anomaly "use coq_existT_ref") let coq_existT_ref = lazy (init_reference ["Specif"] "existT") let coq_not_ref = lazy (init_reference ["Logic"] "not") diff --git a/interp/coqlib.mli b/interp/coqlib.mli index 7e13b1b1ed..5b550a86bf 100644 --- a/interp/coqlib.mli +++ b/interp/coqlib.mli @@ -76,6 +76,8 @@ val glob_false : global_reference (* Equality *) val glob_eq : global_reference +val glob_identity : global_reference +val glob_jmeq : global_reference (*s Constructions and patterns related to Coq initial state are unknown at compile time. Therefore, we can only provide methods to build @@ -104,22 +106,23 @@ val build_sigma_type : coq_sigma_data delayed (* Non-dependent pairs in Set from Datatypes *) val build_prod : coq_sigma_data delayed -type coq_leibniz_eq_data = { +type coq_eq_data = { eq : constr; - refl : constr; ind : constr; - rrec : constr option; - rect : constr option; - congr: constr; - sym : constr } + refl : constr; + sym : constr; + trans: constr; + congr: constr } -val build_coq_eq_data : coq_leibniz_eq_data delayed -val build_coq_identity_data : coq_leibniz_eq_data delayed +val build_coq_eq_data : coq_eq_data delayed +val build_coq_identity_data : coq_eq_data delayed +val build_coq_jmeq_data : coq_eq_data delayed val build_coq_eq : constr delayed (* = [(build_coq_eq_data()).eq] *) val build_coq_eq_sym : constr delayed (* = [(build_coq_eq_data()).sym] *) val build_coq_f_equal2 : constr delayed + (* Specif *) val build_coq_sumbool : constr delayed @@ -150,6 +153,7 @@ val build_coq_ex : constr delayed val coq_eq_ref : global_reference lazy_t val coq_identity_ref : global_reference lazy_t +val coq_jmeq_ref : global_reference lazy_t val coq_existS_ref : global_reference lazy_t val coq_existT_ref : global_reference lazy_t val coq_not_ref : global_reference lazy_t |