diff options
Diffstat (limited to 'plugins/extraction/table.ml')
| -rw-r--r-- | plugins/extraction/table.ml | 48 |
1 files changed, 27 insertions, 21 deletions
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 2642aeefa4..c3f4cfe654 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -1,12 +1,13 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * 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 API open Names open ModPath open Term @@ -37,14 +38,13 @@ module Refset' = Refset_env let occur_kn_in_ref kn = function | IndRef (kn',_) | ConstructRef ((kn',_),_) -> MutInd.equal kn kn' - | ConstRef _ -> false - | VarRef _ -> assert false + | ConstRef _ | VarRef _ -> false let repr_of_r = function | ConstRef kn -> Constant.repr3 kn | IndRef (kn,_) | ConstructRef ((kn,_),_) -> MutInd.repr3 kn - | VarRef _ -> assert false + | VarRef v -> KerName.repr (Lib.make_kn v) let modpath_of_r r = let mp,_,_ = repr_of_r r in mp @@ -251,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 ()]. @@ -273,7 +278,7 @@ let safe_basename_of_global 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) @@ -445,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 @@ -481,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 | _ -> () @@ -646,7 +652,7 @@ 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); @@ -730,7 +736,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); @@ -750,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 = @@ -763,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' @@ -851,7 +857,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); @@ -861,7 +867,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); @@ -878,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 @@ -893,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:(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 |