diff options
Diffstat (limited to 'plugins/extraction/table.ml')
-rw-r--r-- | plugins/extraction/table.ml | 95 |
1 files changed, 50 insertions, 45 deletions
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index ff66d915..54c6d9d7 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -1,15 +1,17 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names +open ModPath open Term open Declarations -open Nameops open Namegen open Libobject open Goptions @@ -20,6 +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 *) @@ -30,15 +37,14 @@ module Refset' = Refset_env let occur_kn_in_ref kn = function | IndRef (kn',_) - | ConstructRef ((kn',_),_) -> Names.eq_mind kn kn' - | ConstRef _ -> false - | VarRef _ -> assert false + | ConstructRef ((kn',_),_) -> MutInd.equal kn kn' + | ConstRef _ | VarRef _ -> false let repr_of_r = function - | ConstRef kn -> repr_con kn + | ConstRef kn -> Constant.repr3 kn | IndRef (kn,_) - | ConstructRef ((kn,_),_) -> repr_mind kn - | VarRef _ -> assert false + | ConstructRef ((kn,_),_) -> MutInd.repr3 kn + | VarRef v -> KerName.repr (Lib.make_kn v) let modpath_of_r r = let mp,_,_ = repr_of_r r in mp @@ -55,11 +61,11 @@ let is_modfile = function | _ -> false let raw_string_of_modfile = function - | MPfile f -> String.capitalize (Id.to_string (List.hd (DirPath.repr f))) + | MPfile f -> capitalize (Id.to_string (List.hd (DirPath.repr f))) | _ -> assert false let is_toplevel mp = - ModPath.equal mp initial_path || ModPath.equal mp (Lib.current_mp ()) + ModPath.equal mp ModPath.initial || ModPath.equal mp (Lib.current_mp ()) let at_toplevel mp = is_modfile mp || is_toplevel mp @@ -245,6 +251,11 @@ let modular () = !modular_ref let set_library b = library_ref := b let library () = !library_ref +let extrcompute = ref false + +let set_extrcompute b = extrcompute := b +let is_extrcompute () = !extrcompute + (*s Printing. *) (* The following functions work even on objects not in [Global.env ()]. @@ -256,18 +267,18 @@ let safe_basename_of_global r = let last_chance r = try Nametab.basename_of_global r with Not_found -> - anomaly (Pp.str "Inductive object unknown to extraction and not globally visible") + anomaly (Pp.str "Inductive object unknown to extraction and not globally visible.") in match r with - | ConstRef kn -> Label.to_id (con_label kn) - | IndRef (kn,0) -> Label.to_id (mind_label kn) + | ConstRef kn -> Label.to_id (Constant.label kn) + | IndRef (kn,0) -> Label.to_id (MutInd.label kn) | IndRef (kn,i) -> (try (unsafe_lookup_ind kn).ind_packets.(i).ip_typename with Not_found -> last_chance r) | ConstructRef ((kn,i),j) -> (try (unsafe_lookup_ind kn).ind_packets.(i).ip_consnames.(j-1) with Not_found -> last_chance r) - | VarRef _ -> assert false + | VarRef v -> v let string_of_global r = try string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty r) @@ -281,8 +292,8 @@ let safe_pr_long_global r = try Printer.pr_global r with Not_found -> match r with | ConstRef kn -> - let mp,_,l = repr_con kn in - str ((string_of_mp mp)^"."^(Label.to_string l)) + let mp,_,l = Constant.repr3 kn in + str ((ModPath.to_string mp)^"."^(Label.to_string l)) | _ -> assert false let pr_long_mp mp = @@ -293,7 +304,7 @@ let pr_long_global ref = pr_path (Nametab.path_of_global ref) (*S Warning and Error messages. *) -let err s = errorlabstrm "Extraction" s +let err s = user_err ~hdr:"Extraction" s let warn_extraction_axiom_to_realize = CWarnings.create ~name:"extraction-axiom-to-realize" ~category:"extraction" @@ -411,7 +422,7 @@ let error_singleton_become_prop id og = str " (or in its mutual block)" | None -> mt () in - err (str "The informative inductive type " ++ pr_id id ++ + err (str "The informative inductive type " ++ Id.print id ++ str " has a Prop instance" ++ loc ++ str "." ++ fnl () ++ str "This happens when a sort-polymorphic singleton inductive type\n" ++ str "has logical parameters, such as (I,I) : (True * True) : Prop.\n" ++ @@ -439,9 +450,10 @@ let error_MPfile_as_mod mp b = "Please "^s2^"use (Recursive) Extraction Library instead.\n")) let argnames_of_global r = - let typ = Global.type_of_global_unsafe r in + let env = Global.env () in + let typ, _ = Global.type_of_global_in_context env r in let rels,_ = - decompose_prod (Reduction.whd_all (Global.env ()) typ) in + decompose_prod (Reduction.whd_all env typ) in List.rev_map fst rels let msg_of_implicit = function @@ -475,7 +487,7 @@ let check_loaded_modfile mp = match base_mp mp with if not (Library.library_is_loaded dp) then begin match base_mp (Lib.current_mp ()) with | MPfile dp' when not (DirPath.equal dp dp') -> - err (str "Please load library " ++ pr_dirpath dp ++ str " first.") + err (str "Please load library " ++ DirPath.print dp ++ str " first.") | _ -> () end | _ -> () @@ -494,8 +506,7 @@ let my_bool_option name initval = let flag = ref initval in let access = fun () -> !flag in let _ = declare_bool_option - {optsync = true; - optdepr = false; + {optdepr = false; optname = "Extraction "^name; optkey = ["Extraction"; name]; optread = access; @@ -567,16 +578,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 - {optsync = true; - optdepr = false; + {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 - { optsync = true; - optdepr = false; + { optdepr = false; optname = "Extraction Flag"; optkey = ["Extraction";"Flag"]; optread = (fun _ -> Some !int_flag_ref); @@ -590,8 +599,7 @@ let conservative_types_ref = ref false let conservative_types () = !conservative_types_ref let _ = declare_bool_option - {optsync = true; - optdepr = false; + {optdepr = false; optname = "Extraction Conservative Types"; optkey = ["Extraction"; "Conservative"; "Types"]; optread = (fun () -> !conservative_types_ref); @@ -603,8 +611,7 @@ let file_comment_ref = ref "" let file_comment () = !file_comment_ref let _ = declare_string_option - {optsync = true; - optdepr = false; + {optdepr = false; optname = "Extraction File Comment"; optkey = ["Extraction"; "File"; "Comment"]; optread = (fun () -> !file_comment_ref); @@ -721,7 +728,7 @@ let add_implicits r l = let i = List.index Name.equal (Name id) names in Int.Set.add i s with Not_found -> - err (str "No argument " ++ pr_id id ++ str " for " ++ + err (str "No argument " ++ Id.print id ++ str " for " ++ safe_pr_global r) in let ints = List.fold_left add_arg Int.Set.empty l in @@ -749,11 +756,11 @@ let extraction_implicit r l = let blacklist_table = Summary.ref Id.Set.empty ~name:"ExtrBlacklist" -let modfile_ids = ref [] +let modfile_ids = ref Id.Set.empty let modfile_mps = ref MPmap.empty let reset_modfile () = - modfile_ids := Id.Set.elements !blacklist_table; + modfile_ids := !blacklist_table; modfile_mps := MPmap.empty let string_of_modfile mp = @@ -762,7 +769,7 @@ let string_of_modfile mp = let id = Id.of_string (raw_string_of_modfile mp) in let id' = next_ident_away id !modfile_ids in let s' = Id.to_string id' in - modfile_ids := id' :: !modfile_ids; + modfile_ids := Id.Set.add id' !modfile_ids; modfile_mps := MPmap.add mp s' !modfile_mps; s' @@ -773,13 +780,11 @@ let file_of_modfile mp = | MPfile f -> Id.to_string (List.hd (DirPath.repr f)) | _ -> assert false in - let s = String.copy (string_of_modfile mp) in - if s.[0] != s0.[0] then s.[0] <- s0.[0]; - s + String.mapi (fun i c -> if i = 0 then s0.[0] else c) (string_of_modfile mp) let add_blacklist_entries l = blacklist_table := - List.fold_right (fun s -> Id.Set.add (Id.of_string (String.capitalize s))) + List.fold_right (fun s -> Id.Set.add (Id.of_string (capitalize s))) l !blacklist_table (* Registration of operations for rollback. *) @@ -801,7 +806,7 @@ let extraction_blacklist l = (* Printing part *) let print_extraction_blacklist () = - prlist_with_sep fnl pr_id (Id.Set.elements !blacklist_table) + prlist_with_sep fnl Id.print (Id.Set.elements !blacklist_table) (* Reset part *) @@ -879,7 +884,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_unsafe (ConstRef kn) in + let typ, _ = Global.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 @@ -894,7 +899,7 @@ let extract_constant_inline inline r ids s = let extract_inductive r s l optstr = check_inside_section (); let g = Smartlocate.global_with_alias r in - Dumpglob.add_glob (loc_of_reference r) g; + Dumpglob.add_glob ?loc:r.CAst.loc g; match g with | IndRef ((kn,i) as ip) -> let mib = Global.lookup_mind kn in |