Imported Upstream version 8.3upstream/8.3

1 files changed, 66 insertions, 47 deletions

diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index fd640388..a7e636ff 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: table.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: table.ml 13420 2010-09-16 15:47:08Z letouzey $ i*)
 
 open Names
 open Term
@@ -21,6 +21,13 @@ open Util
 open Pp
 open Miniml
 
+(** Sets and maps for [global_reference] that do _not_ work modulo
+    name equivalence (otherwise use Refset / Refmap ) *)
+
+module RefOrd = struct type t = global_reference let compare = compare end
+module Refmap' = Map.Make(RefOrd)
+module Refset' = Set.Make(RefOrd)
+
 (*S Utilities about [module_path] and [kernel_names] and [global_reference] *)
 
 let occur_kn_in_ref kn = function
@@ -119,37 +126,47 @@ let rec add_labels_mp mp = function
 
 (*s Constants tables. *)
 
-let terms = ref (Cmap.empty : ml_decl Cmap.t)
-let init_terms () = terms := Cmap.empty
-let add_term kn d = terms := Cmap.add kn d !terms
-let lookup_term kn = Cmap.find kn !terms
+let terms = ref (Cmap_env.empty : ml_decl Cmap_env.t)
+let init_terms () = terms := Cmap_env.empty
+let add_term kn d = terms := Cmap_env.add kn d !terms
+let lookup_term kn = Cmap_env.find kn !terms
 
-let types = ref (Cmap.empty : ml_schema Cmap.t)
-let init_types () = types := Cmap.empty
-let add_type kn s = types := Cmap.add kn s !types
-let lookup_type kn = Cmap.find kn !types
+let types = ref (Cmap_env.empty : ml_schema Cmap_env.t)
+let init_types () = types := Cmap_env.empty
+let add_type kn s = types := Cmap_env.add kn s !types
+let lookup_type kn = Cmap_env.find kn !types
 
 (*s Inductives table. *)
 
-let inductives = ref (Mindmap.empty : (mutual_inductive_body * ml_ind) Mindmap.t)
-let init_inductives () = inductives := Mindmap.empty
-let add_ind kn mib ml_ind = inductives := Mindmap.add kn (mib,ml_ind) !inductives
-let lookup_ind kn = Mindmap.find kn !inductives
+let inductives =
+  ref (Mindmap_env.empty : (mutual_inductive_body * ml_ind) Mindmap_env.t)
+let init_inductives () = inductives := Mindmap_env.empty
+let add_ind kn mib ml_ind =
+  inductives := Mindmap_env.add kn (mib,ml_ind) !inductives
+let lookup_ind kn = Mindmap_env.find kn !inductives
 
 (*s Recursors table. *)
 
+(* NB: here we can use the equivalence between canonical
+   and user constant names : Cset is fine, no need for [Cset_env] *)
+
 let recursors = ref Cset.empty
 let init_recursors () = recursors := Cset.empty
 
 let add_recursors env kn =
-  let make_kn id = make_con (mind_modpath kn) empty_dirpath (label_of_id id) in
+  let mk_con id =
+    make_con_equiv
+      (modpath (user_mind kn))
+      (modpath (canonical_mind kn))
+      empty_dirpath (label_of_id id)
+  in
   let mib = Environ.lookup_mind kn env in
   Array.iter
     (fun mip ->
        let id = mip.mind_typename in
-       let kn_rec = make_kn (Nameops.add_suffix id "_rec")
-       and kn_rect = make_kn (Nameops.add_suffix id "_rect") in
-       recursors := Cset.add kn_rec (Cset.add kn_rect !recursors))
+       let c_rec = mk_con (Nameops.add_suffix id "_rec")
+       and c_rect = mk_con (Nameops.add_suffix id "_rect") in
+       recursors := Cset.add c_rec (Cset.add c_rect !recursors))
     mib.mind_packets
 
 let is_recursor = function
@@ -158,6 +175,8 @@ let is_recursor = function
 
 (*s Record tables. *)
 
+(* NB: here, working modulo name equivalence is ok *)
+
 let projs = ref (Refmap.empty : int Refmap.t)
 let init_projs () = projs := Refmap.empty
 let add_projection n kn = projs := Refmap.add (ConstRef kn) n !projs
@@ -166,12 +185,12 @@ let projection_arity r = Refmap.find r !projs
 
 (*s Table of used axioms *)
 
-let info_axioms = ref Refset.empty
-let log_axioms = ref Refset.empty
-let init_axioms () = info_axioms := Refset.empty; log_axioms := Refset.empty
-let add_info_axiom r = info_axioms := Refset.add r !info_axioms
-let remove_info_axiom r = info_axioms := Refset.remove r !info_axioms
-let add_log_axiom r = log_axioms := Refset.add r !log_axioms
+let info_axioms = ref Refset'.empty
+let log_axioms = ref Refset'.empty
+let init_axioms () = info_axioms := Refset'.empty; log_axioms := Refset'.empty
+let add_info_axiom r = info_axioms := Refset'.add r !info_axioms
+let remove_info_axiom r = info_axioms := Refset'.remove r !info_axioms
+let add_log_axiom r = log_axioms := Refset'.add r !log_axioms
 
 (*s Extraction mode: modular or monolithic *)
 
@@ -220,7 +239,7 @@ let pr_long_global ref = pr_path (Nametab.path_of_global ref)
 let err s = errorlabstrm "Extraction" s
 
 let warning_axioms () =
-  let info_axioms = Refset.elements !info_axioms in
+  let info_axioms = Refset'.elements !info_axioms in
   if info_axioms = [] then ()
   else begin
     let s = if List.length info_axioms = 1 then "axiom" else "axioms" in
@@ -229,7 +248,7 @@ let warning_axioms () =
        ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global info_axioms)
        ++ str "." ++ fnl ())
   end;
-  let log_axioms = Refset.elements !log_axioms in
+  let log_axioms = Refset'.elements !log_axioms in
   if log_axioms = [] then ()
   else begin
     let s = if List.length log_axioms = 1 then "axiom was" else "axioms were"
@@ -457,16 +476,16 @@ let extraction_language x = Lib.add_anonymous_leaf (extr_lang x)
 
 (*s Extraction Inline/NoInline *)
 
-let empty_inline_table = (Refset.empty,Refset.empty)
+let empty_inline_table = (Refset'.empty,Refset'.empty)
 
 let inline_table = ref empty_inline_table
 
-let to_inline r = Refset.mem r (fst !inline_table)
+let to_inline r = Refset'.mem r (fst !inline_table)
 
-let to_keep r = Refset.mem r (snd !inline_table)
+let to_keep r = Refset'.mem r (snd !inline_table)
 
 let add_inline_entries b l =
-  let f b = if b then Refset.add else Refset.remove in
+  let f b = if b then Refset'.add else Refset'.remove in
   let i,k = !inline_table in
   inline_table :=
   (List.fold_right (f b) l i),
@@ -504,14 +523,14 @@ let extraction_inline b l =
 
 let print_extraction_inline () =
   let (i,n)= !inline_table in
-  let i'= Refset.filter (function ConstRef _ -> true | _ -> false) i in
+  let i'= Refset'.filter (function ConstRef _ -> true | _ -> false) i in
   msg
     (str "Extraction Inline:" ++ fnl () ++
-     Refset.fold
+     Refset'.fold
        (fun r p ->
 	  (p ++ str "  " ++ safe_pr_long_global r ++ fnl ())) i' (mt ()) ++
      str "Extraction NoInline:" ++ fnl () ++
-     Refset.fold
+     Refset'.fold
        (fun r p ->
 	  (p ++ str "  " ++ safe_pr_long_global r ++ fnl ())) n (mt ()))
 
@@ -529,10 +548,10 @@ let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ())
 
 type int_or_id = ArgInt of int | ArgId of identifier
 
-let implicits_table = ref Refmap.empty
+let implicits_table = ref Refmap'.empty
 
 let implicits_of_global r =
- try Refmap.find r !implicits_table with Not_found -> []
+ try Refmap'.find r !implicits_table with Not_found -> []
 
 let add_implicits r l =
   let typ = Global.type_of_global r in
@@ -552,7 +571,7 @@ let add_implicits r l =
 		safe_pr_global r))
   in
   let l' = List.map check l in
-  implicits_table := Refmap.add r l' !implicits_table
+  implicits_table := Refmap'.add r l' !implicits_table
 
 (* Registration of operations for rollback. *)
 
@@ -568,7 +587,7 @@ let (implicit_extraction,_) =
 let _ = declare_summary "Extraction Implicit"
 	  { freeze_function = (fun () -> !implicits_table);
 	    unfreeze_function = ((:=) implicits_table);
-	    init_function = (fun () -> implicits_table := Refmap.empty) }
+	    init_function = (fun () -> implicits_table := Refmap'.empty) }
 
 (* Grammar entries. *)
 
@@ -658,22 +677,22 @@ let reset_extraction_blacklist () = Lib.add_anonymous_leaf (reset_blacklist ())
 let use_type_scheme_nb_args, register_type_scheme_nb_args =
   let r = ref (fun _ _ -> 0) in (fun x y -> !r x y), (:=) r
 
-let customs = ref Refmap.empty
+let customs = ref Refmap'.empty
 
-let add_custom r ids s = customs := Refmap.add r (ids,s) !customs
+let add_custom r ids s = customs := Refmap'.add r (ids,s) !customs
 
-let is_custom r = Refmap.mem r !customs
+let is_custom r = Refmap'.mem r !customs
 
 let is_inline_custom r = (is_custom r) && (to_inline r)
 
-let find_custom r = snd (Refmap.find r !customs)
+let find_custom r = snd (Refmap'.find r !customs)
 
-let find_type_custom r = Refmap.find r !customs
+let find_type_custom r = Refmap'.find r !customs
 
-let custom_matchs = ref Refmap.empty
+let custom_matchs = ref Refmap'.empty
 
 let add_custom_match r s =
-  custom_matchs := Refmap.add r s !custom_matchs
+  custom_matchs := Refmap'.add r s !custom_matchs
 
 let indref_of_match pv =
   if Array.length pv = 0 then raise Not_found;
@@ -682,11 +701,11 @@ let indref_of_match pv =
     | _ -> raise Not_found
 
 let is_custom_match pv =
-  try Refmap.mem (indref_of_match pv) !custom_matchs
+  try Refmap'.mem (indref_of_match pv) !custom_matchs
   with Not_found -> false
 
 let find_custom_match pv =
-  Refmap.find (indref_of_match pv) !custom_matchs
+  Refmap'.find (indref_of_match pv) !custom_matchs
 
 (* Registration of operations for rollback. *)
 
@@ -703,7 +722,7 @@ let (in_customs,_) =
 let _ = declare_summary "ML extractions"
 	  { freeze_function = (fun () -> !customs);
 	    unfreeze_function = ((:=) customs);
-	    init_function = (fun () -> customs := Refmap.empty) }
+	    init_function = (fun () -> customs := Refmap'.empty) }
 
 let (in_custom_matchs,_) =
   declare_object
@@ -717,7 +736,7 @@ let (in_custom_matchs,_) =
 let _ = declare_summary "ML extractions custom match"
 	  { freeze_function = (fun () -> !custom_matchs);
 	    unfreeze_function = ((:=) custom_matchs);
-	    init_function = (fun () -> custom_matchs := Refmap.empty) }
+	    init_function = (fun () -> custom_matchs := Refmap'.empty) }
 
 (* Grammar entries. *)