diff options
Diffstat (limited to 'plugins/extraction/table.ml')
| -rw-r--r-- | plugins/extraction/table.ml | 64 |
1 files changed, 29 insertions, 35 deletions
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 54c6d9d729..16890ea260 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -22,16 +22,11 @@ open Util open Pp open Miniml -[@@@ocaml.warning "-3"] (* String.capitalize_ascii since 4.03.0 GPR#124 *) -let capitalize = String.capitalize -[@@@ocaml.warning "+3"] - - (** Sets and maps for [global_reference] that use the "user" [kernel_name] instead of the canonical one *) -module Refmap' = Refmap_env -module Refset' = Refset_env +module Refmap' = GlobRef.Map_env +module Refset' = GlobRef.Set_env (*S Utilities about [module_path] and [kernel_names] and [global_reference] *) @@ -41,16 +36,16 @@ let occur_kn_in_ref kn = function | ConstRef _ | VarRef _ -> false let repr_of_r = function - | ConstRef kn -> Constant.repr3 kn + | ConstRef kn -> Constant.repr2 kn | IndRef (kn,_) - | ConstructRef ((kn,_),_) -> MutInd.repr3 kn + | ConstructRef ((kn,_),_) -> MutInd.repr2 kn | VarRef v -> KerName.repr (Lib.make_kn v) let modpath_of_r r = - let mp,_,_ = repr_of_r r in mp + let mp,_ = repr_of_r r in mp let label_of_r r = - let _,_,l = repr_of_r r in l + let _,l = repr_of_r r in l let rec base_mp = function | MPdot (mp,l) -> base_mp mp @@ -61,7 +56,7 @@ let is_modfile = function | _ -> false let raw_string_of_modfile = function - | MPfile f -> capitalize (Id.to_string (List.hd (DirPath.repr f))) + | MPfile f -> String.capitalize_ascii (Id.to_string (List.hd (DirPath.repr f))) | _ -> assert false let is_toplevel mp = @@ -100,7 +95,7 @@ let rec parse_labels2 ll mp1 = function let labels_of_ref r = let mp_top = Lib.current_mp () in - let mp,_,l = repr_of_r r in + let mp,l = repr_of_r r in parse_labels2 [l] mp_top mp @@ -194,7 +189,7 @@ let init_recursors () = recursors := KNset.empty let add_recursors env ind = let kn = MutInd.canonical ind in let mk_kn id = - KerName.make (KerName.modpath kn) DirPath.empty (Label.of_id id) + KerName.make (KerName.modpath kn) (Label.of_id id) in let mib = Environ.lookup_mind ind env in Array.iter @@ -213,12 +208,12 @@ let is_recursor = function (* NB: here, working modulo name equivalence is ok *) -let projs = ref (Refmap.empty : (inductive*int) Refmap.t) -let init_projs () = projs := Refmap.empty -let add_projection n kn ip = projs := Refmap.add (ConstRef kn) (ip,n) !projs -let is_projection r = Refmap.mem r !projs -let projection_arity r = snd (Refmap.find r !projs) -let projection_info r = Refmap.find r !projs +let projs = ref (GlobRef.Map.empty : (inductive*int) GlobRef.Map.t) +let init_projs () = projs := GlobRef.Map.empty +let add_projection n kn ip = projs := GlobRef.Map.add (ConstRef kn) (ip,n) !projs +let is_projection r = GlobRef.Map.mem r !projs +let projection_arity r = snd (GlobRef.Map.find r !projs) +let projection_info r = GlobRef.Map.find r !projs (*s Table of used axioms *) @@ -292,7 +287,7 @@ let safe_pr_long_global r = try Printer.pr_global r with Not_found -> match r with | ConstRef kn -> - let mp,_,l = Constant.repr3 kn in + let mp,l = Constant.repr2 kn in str ((ModPath.to_string mp)^"."^(Label.to_string l)) | _ -> assert false @@ -451,7 +446,7 @@ let error_MPfile_as_mod mp b = let argnames_of_global r = let env = Global.env () in - let typ, _ = Global.type_of_global_in_context env r in + let typ, _ = Typeops.type_of_global_in_context env r in let rels,_ = decompose_prod (Reduction.whd_all env typ) in List.rev_map fst rels @@ -505,7 +500,7 @@ let info_file f = let my_bool_option name initval = let flag = ref initval in let access = fun () -> !flag in - let _ = declare_bool_option + let () = declare_bool_option {optdepr = false; optname = "Extraction "^name; optkey = ["Extraction"; name]; @@ -577,14 +572,14 @@ let chg_flag n = int_flag_ref := n; opt_flag_ref := flag_of_int n let optims () = !opt_flag_ref -let _ = declare_bool_option +let () = declare_bool_option {optdepr = false; optname = "Extraction Optimize"; optkey = ["Extraction"; "Optimize"]; optread = (fun () -> not (Int.equal !int_flag_ref 0)); optwrite = (fun b -> chg_flag (if b then int_flag_init else 0))} -let _ = declare_int_option +let () = declare_int_option { optdepr = false; optname = "Extraction Flag"; optkey = ["Extraction";"Flag"]; @@ -598,7 +593,7 @@ let _ = declare_int_option let conservative_types_ref = ref false let conservative_types () = !conservative_types_ref -let _ = declare_bool_option +let () = declare_bool_option {optdepr = false; optname = "Extraction Conservative Types"; optkey = ["Extraction"; "Conservative"; "Types"]; @@ -610,7 +605,7 @@ let _ = declare_bool_option let file_comment_ref = ref "" let file_comment () = !file_comment_ref -let _ = declare_string_option +let () = declare_string_option {optdepr = false; optname = "Extraction File Comment"; optkey = ["Extraction"; "File"; "Comment"]; @@ -652,14 +647,13 @@ let add_inline_entries b l = (* Registration of operations for rollback. *) -let inline_extraction : bool * global_reference list -> obj = +let inline_extraction : bool * GlobRef.t list -> obj = declare_object {(default_object "Extraction Inline") with cache_function = (fun (_,(b,l)) -> add_inline_entries b l); load_function = (fun _ (_,(b,l)) -> add_inline_entries b l); classify_function = (fun o -> Substitute o); - discharge_function = - (fun (_,(b,l)) -> Some (b, List.map pop_global_reference l)); + discharge_function = (fun (_,x) -> Some x); subst_function = (fun (s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l))) } @@ -736,7 +730,7 @@ let add_implicits r l = (* Registration of operations for rollback. *) -let implicit_extraction : global_reference * int_or_id list -> obj = +let implicit_extraction : GlobRef.t * int_or_id list -> obj = declare_object {(default_object "Extraction Implicit") with cache_function = (fun (_,(r,l)) -> add_implicits r l); @@ -784,7 +778,7 @@ let file_of_modfile mp = let add_blacklist_entries l = blacklist_table := - List.fold_right (fun s -> Id.Set.add (Id.of_string (capitalize s))) + List.fold_right (fun s -> Id.Set.add (Id.of_string (String.capitalize_ascii s))) l !blacklist_table (* Registration of operations for rollback. *) @@ -857,7 +851,7 @@ let find_custom_match pv = (* Registration of operations for rollback. *) -let in_customs : global_reference * string list * string -> obj = +let in_customs : GlobRef.t * string list * string -> obj = declare_object {(default_object "ML extractions") with cache_function = (fun (_,(r,ids,s)) -> add_custom r ids s); @@ -867,7 +861,7 @@ let in_customs : global_reference * string list * string -> obj = (fun (s,(r,ids,str)) -> (fst (subst_global s r), ids, str)) } -let in_custom_matchs : global_reference * string -> obj = +let in_custom_matchs : GlobRef.t * string -> obj = declare_object {(default_object "ML extractions custom matchs") with cache_function = (fun (_,(r,s)) -> add_custom_match r s); @@ -884,7 +878,7 @@ let extract_constant_inline inline r ids s = match g with | ConstRef kn -> let env = Global.env () in - let typ, _ = Global.type_of_global_in_context env (ConstRef kn) in + let typ, _ = Typeops.type_of_global_in_context env (ConstRef kn) in let typ = Reduction.whd_all env typ in if Reduction.is_arity env typ then begin |