diff options
Diffstat (limited to 'plugins/extraction/table.ml')
| -rw-r--r-- | plugins/extraction/table.ml | 113 |
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. *) |