From afceace455a4b37ced7e29175ca3424996195f7b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 14 Nov 2017 22:36:47 +0100 Subject: [api] Rename `global_reference` to `GlobRef.t` to follow kernel style. In #6092, `global_reference` was moved to `kernel`. It makes sense to go further and use the current kernel style for names. This has a good effect on the dependency graph, as some core modules don't depend on library anymore. A question about providing equality for the GloRef module remains, as there are two different notions of equality for constants. In that sense, `KerPair` seems suspicious and at some point it should be looked at. --- plugins/extraction/common.mli | 3 +- plugins/extraction/extract_env.ml | 2 +- plugins/extraction/extract_env.mli | 3 +- plugins/extraction/miniml.ml | 25 +++++++------- plugins/extraction/miniml.mli | 25 +++++++------- plugins/extraction/mlutil.ml | 16 ++++----- plugins/extraction/mlutil.mli | 5 ++- plugins/extraction/modutil.ml | 2 +- plugins/extraction/modutil.mli | 7 ++-- plugins/extraction/table.ml | 8 ++--- plugins/extraction/table.mli | 69 +++++++++++++++++++------------------- 11 files changed, 79 insertions(+), 86 deletions(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli index 78545c8bd..07237d750 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Globnames open Miniml (** By default, in module Format, you can do horizontal placing of blocks @@ -54,7 +53,7 @@ val opened_libraries : unit -> ModPath.t list type kind = Term | Type | Cons | Mod -val pp_global : kind -> global_reference -> string +val pp_global : kind -> GlobRef.t -> string val pp_module : ModPath.t -> string val top_visible_mp : unit -> ModPath.t diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 397cb2920..bebd27e11 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -79,7 +79,7 @@ module type VISIT = sig (* Add reference / ... in the visit lists. These functions silently add the mp of their arg in the mp list *) - val add_ref : global_reference -> unit + val add_ref : GlobRef.t -> unit val add_kn : KerName.t -> unit val add_decl_deps : ml_decl -> unit val add_spec_deps : ml_spec -> unit diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index 591d3bb86..77f1fb5ef 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -12,7 +12,6 @@ open Names open Libnames -open Globnames val simple_extraction : reference -> unit val full_extraction : string option -> reference list -> unit @@ -26,7 +25,7 @@ val extract_and_compile : reference list -> unit (* For debug / external output via coqtop.byte + Drop : *) val mono_environment : - global_reference list -> ModPath.t list -> Miniml.ml_structure + GlobRef.t list -> ModPath.t list -> Miniml.ml_structure (* Used by the Relation Extraction plugin *) diff --git a/plugins/extraction/miniml.ml b/plugins/extraction/miniml.ml index e1e49d926..ce920ad6a 100644 --- a/plugins/extraction/miniml.ml +++ b/plugins/extraction/miniml.ml @@ -11,7 +11,6 @@ (*s Target language for extraction: a core ML called MiniML. *) open Names -open Globnames (* The [signature] type is used to know how many arguments a CIC object expects, and what these arguments will become in the ML @@ -26,7 +25,7 @@ open Globnames type kill_reason = | Ktype | Kprop - | Kimplicit of global_reference * int (* n-th arg of a cst or construct *) + | Kimplicit of GlobRef.t * int (* n-th arg of a cst or construct *) type sign = Keep | Kill of kill_reason @@ -39,7 +38,7 @@ type signature = sign list type ml_type = | Tarr of ml_type * ml_type - | Tglob of global_reference * ml_type list + | Tglob of GlobRef.t * ml_type list | Tvar of int | Tvar' of int (* same as Tvar, used to avoid clash *) | Tmeta of ml_meta (* used during ML type reconstruction *) @@ -60,7 +59,7 @@ type inductive_kind = | Singleton | Coinductive | Standard - | Record of global_reference option list (* None for anonymous field *) + | Record of GlobRef.t option list (* None for anonymous field *) (* A [ml_ind_packet] is the miniml counterpart of a [one_inductive_body]. If the inductive is logical ([ip_logical = false]), then all other fields @@ -118,8 +117,8 @@ and ml_ast = | MLapp of ml_ast * ml_ast list | MLlam of ml_ident * ml_ast | MLletin of ml_ident * ml_ast * ml_ast - | MLglob of global_reference - | MLcons of ml_type * global_reference * ml_ast list + | MLglob of GlobRef.t + | MLcons of ml_type * GlobRef.t * ml_ast list | MLtuple of ml_ast list | MLcase of ml_type * ml_ast * ml_branch array | MLfix of int * Id.t array * ml_ast array @@ -129,24 +128,24 @@ and ml_ast = | MLmagic of ml_ast and ml_pattern = - | Pcons of global_reference * ml_pattern list + | Pcons of GlobRef.t * ml_pattern list | Ptuple of ml_pattern list | Prel of int (** Cf. the idents in the branch. [Prel 1] is the last one. *) | Pwild - | Pusual of global_reference (** Shortcut for Pcons (r,[Prel n;...;Prel 1]) **) + | Pusual of GlobRef.t (** Shortcut for Pcons (r,[Prel n;...;Prel 1]) **) (*s ML declarations. *) type ml_decl = | Dind of MutInd.t * ml_ind - | Dtype of global_reference * Id.t list * ml_type - | Dterm of global_reference * ml_ast * ml_type - | Dfix of global_reference array * ml_ast array * ml_type array + | Dtype of GlobRef.t * Id.t list * ml_type + | Dterm of GlobRef.t * ml_ast * ml_type + | Dfix of GlobRef.t array * ml_ast array * ml_type array type ml_spec = | Sind of MutInd.t * ml_ind - | Stype of global_reference * Id.t list * ml_type option - | Sval of global_reference * ml_type + | Stype of GlobRef.t * Id.t list * ml_type option + | Sval of GlobRef.t * ml_type type ml_specif = | Spec of ml_spec diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index e1e49d926..ce920ad6a 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -11,7 +11,6 @@ (*s Target language for extraction: a core ML called MiniML. *) open Names -open Globnames (* The [signature] type is used to know how many arguments a CIC object expects, and what these arguments will become in the ML @@ -26,7 +25,7 @@ open Globnames type kill_reason = | Ktype | Kprop - | Kimplicit of global_reference * int (* n-th arg of a cst or construct *) + | Kimplicit of GlobRef.t * int (* n-th arg of a cst or construct *) type sign = Keep | Kill of kill_reason @@ -39,7 +38,7 @@ type signature = sign list type ml_type = | Tarr of ml_type * ml_type - | Tglob of global_reference * ml_type list + | Tglob of GlobRef.t * ml_type list | Tvar of int | Tvar' of int (* same as Tvar, used to avoid clash *) | Tmeta of ml_meta (* used during ML type reconstruction *) @@ -60,7 +59,7 @@ type inductive_kind = | Singleton | Coinductive | Standard - | Record of global_reference option list (* None for anonymous field *) + | Record of GlobRef.t option list (* None for anonymous field *) (* A [ml_ind_packet] is the miniml counterpart of a [one_inductive_body]. If the inductive is logical ([ip_logical = false]), then all other fields @@ -118,8 +117,8 @@ and ml_ast = | MLapp of ml_ast * ml_ast list | MLlam of ml_ident * ml_ast | MLletin of ml_ident * ml_ast * ml_ast - | MLglob of global_reference - | MLcons of ml_type * global_reference * ml_ast list + | MLglob of GlobRef.t + | MLcons of ml_type * GlobRef.t * ml_ast list | MLtuple of ml_ast list | MLcase of ml_type * ml_ast * ml_branch array | MLfix of int * Id.t array * ml_ast array @@ -129,24 +128,24 @@ and ml_ast = | MLmagic of ml_ast and ml_pattern = - | Pcons of global_reference * ml_pattern list + | Pcons of GlobRef.t * ml_pattern list | Ptuple of ml_pattern list | Prel of int (** Cf. the idents in the branch. [Prel 1] is the last one. *) | Pwild - | Pusual of global_reference (** Shortcut for Pcons (r,[Prel n;...;Prel 1]) **) + | Pusual of GlobRef.t (** Shortcut for Pcons (r,[Prel n;...;Prel 1]) **) (*s ML declarations. *) type ml_decl = | Dind of MutInd.t * ml_ind - | Dtype of global_reference * Id.t list * ml_type - | Dterm of global_reference * ml_ast * ml_type - | Dfix of global_reference array * ml_ast array * ml_type array + | Dtype of GlobRef.t * Id.t list * ml_type + | Dterm of GlobRef.t * ml_ast * ml_type + | Dfix of GlobRef.t array * ml_ast array * ml_type array type ml_spec = | Sind of MutInd.t * ml_ind - | Stype of global_reference * Id.t list * ml_type option - | Sval of global_reference * ml_type + | Stype of GlobRef.t * Id.t list * ml_type option + | Sval of GlobRef.t * ml_type type ml_specif = | Spec of ml_spec diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 0656d487a..0901acc7d 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -59,7 +59,7 @@ let rec eq_ml_type t1 t2 = match t1, t2 with | Tarr (tl1, tr1), Tarr (tl2, tr2) -> eq_ml_type tl1 tl2 && eq_ml_type tr1 tr2 | Tglob (gr1, t1), Tglob (gr2, t2) -> - eq_gr gr1 gr2 && List.equal eq_ml_type t1 t2 + GlobRef.equal gr1 gr2 && List.equal eq_ml_type t1 t2 | Tvar i1, Tvar i2 -> Int.equal i1 i2 | Tvar' i1, Tvar' i2 -> Int.equal i1 i2 | Tmeta m1, Tmeta m2 -> eq_ml_meta m1 m2 @@ -120,7 +120,7 @@ let rec mgu = function | None -> m.contents <- Some t) | Tarr(a, b), Tarr(a', b') -> mgu (a, a'); mgu (b, b') - | Tglob (r,l), Tglob (r',l') when Globnames.eq_gr r r' -> + | Tglob (r,l), Tglob (r',l') when GlobRef.equal r r' -> List.iter mgu (List.combine l l') | Tdummy _, Tdummy _ -> () | Tvar i, Tvar j when Int.equal i j -> () @@ -270,7 +270,7 @@ let rec var2var' = function | Tglob (r,l) -> Tglob (r, List.map var2var' l) | a -> a -type abbrev_map = global_reference -> ml_type option +type abbrev_map = GlobRef.t -> ml_type option (*s Delta-reduction of type constants everywhere in a ML type [t]. [env] is a function of type [ml_type_env]. *) @@ -381,9 +381,9 @@ let rec eq_ml_ast t1 t2 = match t1, t2 with eq_ml_ident na1 na2 && eq_ml_ast t1 t2 | MLletin (na1, c1, t1), MLletin (na2, c2, t2) -> eq_ml_ident na1 na2 && eq_ml_ast c1 c2 && eq_ml_ast t1 t2 -| MLglob gr1, MLglob gr2 -> eq_gr gr1 gr2 +| MLglob gr1, MLglob gr2 -> GlobRef.equal gr1 gr2 | MLcons (t1, gr1, c1), MLcons (t2, gr2, c2) -> - eq_ml_type t1 t2 && eq_gr gr1 gr2 && List.equal eq_ml_ast c1 c2 + eq_ml_type t1 t2 && GlobRef.equal gr1 gr2 && List.equal eq_ml_ast c1 c2 | MLtuple t1, MLtuple t2 -> List.equal eq_ml_ast t1 t2 | MLcase (t1, c1, p1), MLcase (t2, c2, p2) -> @@ -398,13 +398,13 @@ let rec eq_ml_ast t1 t2 = match t1, t2 with and eq_ml_pattern p1 p2 = match p1, p2 with | Pcons (gr1, p1), Pcons (gr2, p2) -> - eq_gr gr1 gr2 && List.equal eq_ml_pattern p1 p2 + GlobRef.equal gr1 gr2 && List.equal eq_ml_pattern p1 p2 | Ptuple p1, Ptuple p2 -> List.equal eq_ml_pattern p1 p2 | Prel i1, Prel i2 -> Int.equal i1 i2 | Pwild, Pwild -> true -| Pusual gr1, Pusual gr2 -> eq_gr gr1 gr2 +| Pusual gr1, Pusual gr2 -> GlobRef.equal gr1 gr2 | _ -> false and eq_ml_branch (id1, p1, t1) (id2, p2, t2) = @@ -984,7 +984,7 @@ let rec iota_red i lift br ((typ,r,a) as cons) = if i >= Array.length br then raise Impossible; let (ids,p,c) = br.(i) in match p with - | Pusual r' | Pcons (r',_) when not (Globnames.eq_gr r' r) -> iota_red (i+1) lift br cons + | Pusual r' | Pcons (r',_) when not (GlobRef.equal r' r) -> iota_red (i+1) lift br cons | Pusual r' -> let c = named_lams (List.rev ids) c in let c = ast_lift lift c diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli index 55a1ee893..d23fdb3d5 100644 --- a/plugins/extraction/mlutil.mli +++ b/plugins/extraction/mlutil.mli @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Globnames open Miniml open Table @@ -59,7 +58,7 @@ val type_recomp : ml_type list * ml_type -> ml_type val var2var' : ml_type -> ml_type -type abbrev_map = global_reference -> ml_type option +type abbrev_map = GlobRef.t -> ml_type option val type_expand : abbrev_map -> ml_type -> ml_type val type_simpl : ml_type -> ml_type @@ -117,7 +116,7 @@ val dump_unused_vars : ml_ast -> ml_ast val normalize : ml_ast -> ml_ast val optimize_fix : ml_ast -> ml_ast -val inline : global_reference -> ml_ast -> bool +val inline : GlobRef.t -> ml_ast -> bool val is_basic_pattern : ml_pattern -> bool val has_deep_pattern : ml_branch array -> bool diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index f33a59edf..b398bc07a 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -76,7 +76,7 @@ let struct_iter do_decl do_spec do_mp s = (*s Apply some fonctions upon all references in [ml_type], [ml_ast], [ml_decl], [ml_spec] and [ml_structure]. *) -type do_ref = global_reference -> unit +type do_ref = GlobRef.t -> unit let record_iter_references do_term = function | Record l -> List.iter (Option.iter do_term) l diff --git a/plugins/extraction/modutil.mli b/plugins/extraction/modutil.mli index 6a81f2705..f45773f09 100644 --- a/plugins/extraction/modutil.mli +++ b/plugins/extraction/modutil.mli @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Globnames open Miniml (*s Functions upon ML modules. *) @@ -17,7 +16,7 @@ open Miniml val struct_ast_search : (ml_ast -> bool) -> ml_structure -> bool val struct_type_search : (ml_type -> bool) -> ml_structure -> bool -type do_ref = global_reference -> unit +type do_ref = GlobRef.t -> unit val type_iter_references : do_ref -> ml_type -> unit val ast_iter_references : do_ref -> do_ref -> do_ref -> ml_ast -> unit @@ -30,7 +29,7 @@ val mtyp_of_mexpr : ml_module_expr -> ml_module_type val msid_of_mt : ml_module_type -> ModPath.t -val get_decl_in_structure : global_reference -> ml_structure -> ml_decl +val get_decl_in_structure : GlobRef.t -> ml_structure -> ml_decl (* Some transformations of ML terms. [optimize_struct] simplify all beta redexes (when the argument does not occur, it is just @@ -39,5 +38,5 @@ val get_decl_in_structure : global_reference -> ml_structure -> ml_decl optimizations. The first argument is the list of objects we want to appear. *) -val optimize_struct : global_reference list * ModPath.t list -> +val optimize_struct : GlobRef.t list * ModPath.t list -> ml_structure -> ml_structure diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 54c6d9d72..c3f4cfe65 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -652,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); @@ -736,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); @@ -857,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); @@ -867,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); diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 906dfd96e..5bf944434 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -10,31 +10,30 @@ open Names open Libnames -open Globnames open Miniml open Declarations -module Refset' : CSig.SetS with type elt = global_reference -module Refmap' : CSig.MapS with type key = global_reference +module Refset' : CSig.SetS with type elt = GlobRef.t +module Refmap' : CSig.MapS with type key = GlobRef.t -val safe_basename_of_global : global_reference -> Id.t +val safe_basename_of_global : GlobRef.t -> Id.t (*s Warning and Error messages. *) val warning_axioms : unit -> unit val warning_opaques : bool -> unit -val warning_ambiguous_name : ?loc:Loc.t -> qualid * ModPath.t * global_reference -> unit +val warning_ambiguous_name : ?loc:Loc.t -> qualid * ModPath.t * GlobRef.t -> unit val warning_id : string -> unit -val error_axiom_scheme : global_reference -> int -> 'a -val error_constant : global_reference -> 'a -val error_inductive : global_reference -> 'a +val error_axiom_scheme : GlobRef.t -> int -> 'a +val error_constant : GlobRef.t -> 'a +val error_inductive : GlobRef.t -> 'a val error_nb_cons : unit -> 'a val error_module_clash : ModPath.t -> ModPath.t -> 'a val error_no_module_expr : ModPath.t -> 'a -val error_singleton_become_prop : Id.t -> global_reference option -> 'a +val error_singleton_become_prop : Id.t -> GlobRef.t option -> 'a val error_unknown_module : qualid -> 'a val error_scheme : unit -> 'a -val error_not_visible : global_reference -> 'a +val error_not_visible : GlobRef.t -> 'a val error_MPfile_as_mod : ModPath.t -> bool -> 'a val check_inside_module : unit -> unit val check_inside_section : unit -> unit @@ -44,12 +43,12 @@ val err_or_warn_remaining_implicit : kill_reason -> unit val info_file : string -> unit -(*s utilities about [module_path] and [kernel_names] and [global_reference] *) +(*s utilities about [module_path] and [kernel_names] and [GlobRef.t] *) -val occur_kn_in_ref : MutInd.t -> global_reference -> bool -val repr_of_r : global_reference -> ModPath.t * DirPath.t * Label.t -val modpath_of_r : global_reference -> ModPath.t -val label_of_r : global_reference -> Label.t +val occur_kn_in_ref : MutInd.t -> GlobRef.t -> bool +val repr_of_r : GlobRef.t -> ModPath.t * DirPath.t * Label.t +val modpath_of_r : GlobRef.t -> ModPath.t +val label_of_r : GlobRef.t -> Label.t val base_mp : ModPath.t -> ModPath.t val is_modfile : ModPath.t -> bool val string_of_modfile : ModPath.t -> string @@ -61,7 +60,7 @@ val prefixes_mp : ModPath.t -> MPset.t val common_prefix_from_list : ModPath.t -> ModPath.t list -> ModPath.t option val get_nth_label_mp : int -> ModPath.t -> Label.t -val labels_of_ref : global_reference -> ModPath.t * Label.t list +val labels_of_ref : GlobRef.t -> ModPath.t * Label.t list (*s Some table-related operations *) @@ -83,27 +82,27 @@ val add_ind : MutInd.t -> mutual_inductive_body -> ml_ind -> unit val lookup_ind : MutInd.t -> mutual_inductive_body -> ml_ind option val add_inductive_kind : MutInd.t -> inductive_kind -> unit -val is_coinductive : global_reference -> bool +val is_coinductive : GlobRef.t -> bool val is_coinductive_type : ml_type -> bool (* What are the fields of a record (empty for a non-record) *) val get_record_fields : - global_reference -> global_reference option list -val record_fields_of_type : ml_type -> global_reference option list + GlobRef.t -> GlobRef.t option list +val record_fields_of_type : ml_type -> GlobRef.t option list val add_recursors : Environ.env -> MutInd.t -> unit -val is_recursor : global_reference -> bool +val is_recursor : GlobRef.t -> bool val add_projection : int -> Constant.t -> inductive -> unit -val is_projection : global_reference -> bool -val projection_arity : global_reference -> int -val projection_info : global_reference -> inductive * int (* arity *) +val is_projection : GlobRef.t -> bool +val projection_arity : GlobRef.t -> int +val projection_info : GlobRef.t -> inductive * int (* arity *) -val add_info_axiom : global_reference -> unit -val remove_info_axiom : global_reference -> unit -val add_log_axiom : global_reference -> unit +val add_info_axiom : GlobRef.t -> unit +val remove_info_axiom : GlobRef.t -> unit +val add_log_axiom : GlobRef.t -> unit -val add_opaque : global_reference -> unit -val remove_opaque : global_reference -> unit +val add_opaque : GlobRef.t -> unit +val remove_opaque : GlobRef.t -> unit val reset_tables : unit -> unit @@ -172,22 +171,22 @@ val is_extrcompute : unit -> bool (*s Table for custom inlining *) -val to_inline : global_reference -> bool -val to_keep : global_reference -> bool +val to_inline : GlobRef.t -> bool +val to_keep : GlobRef.t -> bool (*s Table for implicits arguments *) -val implicits_of_global : global_reference -> Int.Set.t +val implicits_of_global : GlobRef.t -> Int.Set.t (*s Table for user-given custom ML extractions. *) (* UGLY HACK: registration of a function defined in [extraction.ml] *) val type_scheme_nb_args_hook : (Environ.env -> Constr.t -> int) Hook.t -val is_custom : global_reference -> bool -val is_inline_custom : global_reference -> bool -val find_custom : global_reference -> string -val find_type_custom : global_reference -> string list * string +val is_custom : GlobRef.t -> bool +val is_inline_custom : GlobRef.t -> bool +val find_custom : GlobRef.t -> string +val find_type_custom : GlobRef.t -> string list * string val is_custom_match : ml_branch array -> bool val find_custom_match : ml_branch array -> string -- cgit v1.2.3