summaryrefslogtreecommitdiff
path: root/interp/coqlib.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
commit5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch)
tree631ad791a7685edafeb1fb2e8faeedc8379318ae /interp/coqlib.ml
parentda178a880e3ace820b41d38b191d3785b82991f5 (diff)
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'interp/coqlib.ml')
-rw-r--r--interp/coqlib.ml202
1 files changed, 156 insertions, 46 deletions
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index ca758458..898369be 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqlib.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id$ *)
open Util
open Pp
@@ -15,6 +15,7 @@ open Term
open Libnames
open Pattern
open Nametab
+open Smartlocate
(************************************************************************)
(* Generic functions to find Coq objects *)
@@ -25,10 +26,8 @@ let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
let find_reference locstr dir s =
let sp = Libnames.make_path (make_dir dir) (id_of_string s) in
- try
- Nametab.absolute_reference sp
- with Not_found ->
- anomaly (locstr^": cannot find "^(string_of_path sp))
+ try global_of_extended_global (Nametab.extended_global_of_path sp)
+ with Not_found -> anomaly (locstr^": cannot find "^(string_of_path sp))
let coq_reference locstr dir s = find_reference locstr ("Coq"::dir) s
let coq_constant locstr dir s = constr_of_global (coq_reference locstr dir s)
@@ -37,25 +36,29 @@ let gen_reference = coq_reference
let gen_constant = coq_constant
let has_suffix_in_dirs dirs ref =
- let dir = dirpath (sp_of_global ref) in
+ let dir = dirpath (path_of_global ref) in
List.exists (fun d -> is_dirpath_prefix_of d dir) dirs
+let global_of_extended q =
+ try Some (global_of_extended_global q) with Not_found -> None
+
let gen_constant_in_modules locstr dirs s =
let dirs = List.map make_dir dirs in
let id = id_of_string s in
- let all = Nametab.locate_all (make_short_qualid id) in
+ let all = Nametab.locate_extended_all (qualid_of_ident id) in
+ let all = list_uniquize (list_map_filter global_of_extended all) in
let these = List.filter (has_suffix_in_dirs dirs) all in
match these with
| [x] -> constr_of_global x
| [] ->
anomalylabstrm "" (str (locstr^": cannot find "^s^
" in module"^(if List.length dirs > 1 then "s " else " ")) ++
- prlist_with_sep pr_coma pr_dirpath dirs)
+ prlist_with_sep pr_comma pr_dirpath dirs)
| l ->
- anomalylabstrm ""
+ anomalylabstrm ""
(str (locstr^": found more than once object of name "^s^
" in module"^(if List.length dirs > 1 then "s " else " ")) ++
- prlist_with_sep pr_coma pr_dirpath dirs)
+ prlist_with_sep pr_comma pr_dirpath dirs)
(* For tactics/commands requiring vernacular libraries *)
@@ -63,21 +66,29 @@ let gen_constant_in_modules locstr dirs s =
let check_required_library d =
let d' = List.map id_of_string d in
let dir = make_dirpath (List.rev d') in
+ let mp = (fst(Lib.current_prefix())) in
+ let current_dir = match mp with
+ | MPfile dp -> (dir=dp)
+ | _ -> false
+ in
if not (Library.library_is_loaded dir) then
+ if not current_dir then
(* Loading silently ...
let m, prefix = list_sep_last d' in
- read_library
+ read_library
(dummy_loc,make_qualid (make_dirpath (List.rev prefix)) m)
*)
(* or failing ...*)
- error ("Library "^(string_of_dirpath dir)^" has to be required first.")
+ error ("Library "^(string_of_dirpath dir)^" has to be required first.")
(************************************************************************)
(* Specific Coq objects *)
let init_reference dir s = gen_reference "Coqlib" ("Init"::dir) s
-let init_constant dir s = gen_constant "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]
@@ -96,7 +107,7 @@ let init_modules = [
init_dir@["Peano"];
init_dir@["Wf"]
]
-
+
let coq_id = id_of_string "Coq"
let init_id = id_of_string "Init"
let arith_id = id_of_string "Arith"
@@ -104,12 +115,21 @@ 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
+let make_kn dir id = Libnames.encode_mind dir id
let make_con dir id = Libnames.encode_con dir id
(** Identity *)
@@ -142,9 +162,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;
@@ -159,7 +184,7 @@ type coq_bool_data = {
type 'a delayed = unit -> 'a
-let build_bool_type () =
+let build_bool_type () =
{ andb = init_constant ["Datatypes"] "andb";
andb_prop = init_constant ["Datatypes"] "andb_prop";
andb_true_intro = init_constant ["Datatypes"] "andb_true_intro" }
@@ -182,41 +207,93 @@ let build_prod () =
typ = init_constant ["Datatypes"] "prod" }
(* Equalities *)
-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 }
+
+(* Data needed for discriminate and injection *)
+type coq_inversion_data = {
+ inv_eq : constr; (* : forall params, t -> Prop *)
+ inv_ind : constr; (* : forall params P y, eq params y -> P y *)
+ inv_congr: constr (* : forall params B (f:t->B) y, eq params y -> f c=f y *)
+}
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"] "refl_equal"
+let coq_eq_refl = lazy_init_constant ["Logic"] "eq_refl"
let coq_eq_ind = lazy_init_constant ["Logic"] "eq_ind"
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"] "sym_eq"
+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 coq_eq_congr_canonical =
+ lazy_init_constant ["Logic"] "f_equal_canonical_form"
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_sym_eq () = Lazy.force coq_eq_sym
+let build_coq_eq_refl () = Lazy.force coq_eq_refl
+let build_coq_eq_sym () = Lazy.force coq_eq_sym
let build_coq_f_equal2 () = Lazy.force coq_f_equal2
+let build_coq_sym_eq = build_coq_eq_sym (* compatibility *)
+
+let build_coq_inversion_eq_data () =
+ let _ = check_required_library logic_module_name in {
+ inv_eq = Lazy.force coq_eq_eq;
+ inv_ind = Lazy.force coq_eq_ind;
+ inv_congr = Lazy.force coq_eq_congr_canonical }
+
+(* 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 coq_jmeq_congr_canonical =
+ lazy_logic_constant ["JMeq"] "JMeq_congr_canonical_form"
+
+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 }
+
+let join_jmeq_types eq =
+ mkLambda(Name (id_of_string "A"),Termops.new_Type(),
+ mkLambda(Name (id_of_string "x"),mkRel 1,
+ mkApp (eq,[|mkRel 2;mkRel 1;mkRel 2|])))
+
+let build_coq_inversion_jmeq_data () =
+ let _ = check_required_library logic_module_name in {
+ inv_eq = join_jmeq_types (Lazy.force coq_jmeq_eq);
+ inv_ind = Lazy.force coq_jmeq_ind;
+ inv_congr = Lazy.force coq_jmeq_congr_canonical }
+
(* Specif *)
let coq_sumbool = lazy_init_constant ["Specif"] "sumbool"
@@ -228,17 +305,38 @@ let coq_identity_refl = lazy_init_constant ["Datatypes"] "refl_identity"
let coq_identity_ind = lazy_init_constant ["Datatypes"] "identity_ind"
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"] "congr_id"
-let coq_identity_sym = lazy_init_constant ["Logic_Type"] "sym_id"
+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 coq_identity_congr_canonical = lazy_init_constant ["Logic_Type"] "identity_congr_canonical_form"
-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 }
+
+let build_coq_inversion_identity_data () =
+ let _ = check_required_library datatypes_module_name in
+ let _ = check_required_library logic_type_module_name in {
+ inv_eq = Lazy.force coq_identity_eq;
+ inv_ind = Lazy.force coq_identity_ind;
+ inv_congr = Lazy.force coq_identity_congr_canonical }
+
+(* Equality to true *)
+let coq_eq_true_eq = lazy_init_constant ["Datatypes"] "eq_true"
+let coq_eq_true_ind = lazy_init_constant ["Datatypes"] "eq_true_ind"
+let coq_eq_true_congr = lazy_init_constant ["Logic"] "eq_true_congr"
+
+let build_coq_inversion_eq_true_data () =
+ let _ = check_required_library datatypes_module_name in
+ let _ = check_required_library logic_module_name in {
+ inv_eq = Lazy.force coq_eq_true_eq;
+ inv_ind = Lazy.force coq_eq_true_ind;
+ inv_congr = Lazy.force coq_eq_true_congr }
(* The False proposition *)
let coq_False = lazy_init_constant ["Logic"] "False"
@@ -253,6 +351,10 @@ let coq_and = lazy_init_constant ["Logic"] "and"
let coq_conj = lazy_init_constant ["Logic"] "conj"
let coq_or = lazy_init_constant ["Logic"] "or"
let coq_ex = lazy_init_constant ["Logic"] "ex"
+let coq_iff = lazy_init_constant ["Logic"] "iff"
+
+let coq_iff_left_proj = lazy_init_constant ["Logic"] "proj1"
+let coq_iff_right_proj = lazy_init_constant ["Logic"] "proj2"
(* Runtime part *)
let build_coq_True () = Lazy.force coq_True
@@ -262,12 +364,19 @@ let build_coq_False () = Lazy.force coq_False
let build_coq_not () = Lazy.force coq_not
let build_coq_and () = Lazy.force coq_and
let build_coq_conj () = Lazy.force coq_conj
-let build_coq_or () = Lazy.force coq_or
-let build_coq_ex () = Lazy.force coq_ex
+let build_coq_or () = Lazy.force coq_or
+let build_coq_ex () = Lazy.force coq_ex
+let build_coq_iff () = Lazy.force coq_iff
+
+let build_coq_iff_left_proj () = Lazy.force coq_iff_left_proj
+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_eq_true_ref = lazy (gen_reference "Coqlib" ["Init";"Datatypes"] "eq_true")
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")
@@ -275,4 +384,5 @@ let coq_False_ref = lazy (init_reference ["Logic"] "False")
let coq_sumbool_ref = lazy (init_reference ["Specif"] "sumbool")
let coq_sig_ref = lazy (init_reference ["Specif"] "sig")
let coq_or_ref = lazy (init_reference ["Logic"] "or")
+let coq_iff_ref = lazy (init_reference ["Logic"] "iff")