Imported Upstream snapshot 8.3~beta0+13298

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")