diff options
Diffstat (limited to 'pretyping/classops.ml')
| -rw-r--r-- | pretyping/classops.ml | 101 |
1 files changed, 50 insertions, 51 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 4f265e76..a0804b72 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -1,23 +1,23 @@ (************************************************************************) -(* 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 CErrors open Util open Pp -open Flags open Names +open Constr open Libnames open Globnames open Nametab open Environ open Libobject -open Term -open Termops open Mod_subst (* usage qque peu general: utilise aussi dans record *) @@ -29,9 +29,9 @@ type cl_typ = | CL_SORT | CL_FUN | CL_SECVAR of variable - | CL_CONST of constant + | CL_CONST of Constant.t | CL_IND of inductive - | CL_PROJ of constant + | CL_PROJ of Constant.t type cl_info_typ = { cl_param : int @@ -45,12 +45,13 @@ type coe_info_typ = { coe_value : constr; coe_type : types; coe_local : bool; - coe_context : Univ.universe_context_set; + coe_context : Univ.ContextSet.t; coe_is_identity : bool; coe_is_projection : bool; coe_param : int } let coe_info_typ_equal c1 c2 = + let eq_constr c1 c2 = Termops.eq_constr Evd.empty (EConstr.of_constr c1) (EConstr.of_constr c2) in eq_constr c1.coe_value c2.coe_value && eq_constr c1.coe_type c2.coe_type && c1.coe_local == c2.coe_local && @@ -60,8 +61,8 @@ let coe_info_typ_equal c1 c2 = let cl_typ_ord t1 t2 = match t1, t2 with | CL_SECVAR v1, CL_SECVAR v2 -> Id.compare v1 v2 - | CL_CONST c1, CL_CONST c2 -> con_ord c1 c2 - | CL_PROJ c1, CL_PROJ c2 -> con_ord c1 c2 + | CL_CONST c1, CL_CONST c2 -> Constant.CanOrd.compare c1 c2 + | CL_PROJ c1, CL_PROJ c2 -> Constant.CanOrd.compare c1 c2 | CL_IND i1, CL_IND i2 -> ind_ord i1 i2 | _ -> Pervasives.compare t1 t2 (** OK *) @@ -89,7 +90,7 @@ sig type t val compare : t -> t -> int val equal : t -> t -> bool - val print : t -> std_ppcmds + val print : t -> Pp.t end type 'a t val empty : 'a t @@ -192,15 +193,16 @@ let coercion_exists coe = CoeTypMap.mem coe !coercion_tab (* find_class_type : evar_map -> constr -> cl_typ * universe_list * constr list *) let find_class_type sigma t = + let open EConstr in let t', args = Reductionops.whd_betaiotazeta_stack sigma t in - match kind_of_term t' with - | Var id -> CL_SECVAR id, Univ.Instance.empty, args + match EConstr.kind sigma t' with + | Var id -> CL_SECVAR id, EInstance.empty, args | Const (sp,u) -> CL_CONST sp, u, args | Proj (p, c) when not (Projection.unfolded p) -> - CL_PROJ (Projection.constant p), Univ.Instance.empty, c :: args + CL_PROJ (Projection.constant p), EInstance.empty, (c :: args) | Ind (ind_sp,u) -> CL_IND ind_sp, u, args - | Prod (_,_,_) -> CL_FUN, Univ.Instance.empty, [] - | Sort _ -> CL_SORT, Univ.Instance.empty, [] + | Prod (_,_,_) -> CL_FUN, EInstance.empty, [] + | Sort _ -> CL_SORT, EInstance.empty, [] | _ -> raise Not_found @@ -214,7 +216,7 @@ let subst_cl_typ subst ct = match ct with | CL_CONST c -> let c',t = subst_con_kn subst c in if c' == c then ct else - pi1 (find_class_type Evd.empty t) + pi1 (find_class_type Evd.empty (EConstr.of_constr t)) | CL_IND i -> let i' = subst_ind subst i in if i' == i then ct else CL_IND i' @@ -297,9 +299,9 @@ let lookup_path_to_sort_from env sigma s = let get_coercion_constructor env coe = let c, _ = - Reductionops.whd_all_stack env Evd.empty coe.coe_value + Reductionops.whd_all_stack env Evd.empty (EConstr.of_constr coe.coe_value) in - match kind_of_term c with + match EConstr.kind Evd.empty (** FIXME *) c with | Construct (cstr,u) -> (cstr, Inductiveops.constructor_nrealargs cstr -1) | _ -> @@ -317,21 +319,21 @@ let coercion_value { coe_value = c; coe_type = t; coe_context = ctx; let subst, ctx = Universes.fresh_universe_context_set_instance ctx in let c' = Vars.subst_univs_level_constr subst c and t' = Vars.subst_univs_level_constr subst t in - (make_judge c' t', b, b'), ctx + (make_judge (EConstr.of_constr c') (EConstr.of_constr t'), b, b'), ctx (* pretty-print functions are now in Pretty *) (* rajouter une coercion dans le graphe *) -let path_printer = ref (fun _ -> str "<a class path>" - : (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> std_ppcmds) +let path_printer : (env -> Evd.evar_map -> (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t) ref = + ref (fun _ _ _ -> str "<a class path>") let install_path_printer f = path_printer := f -let print_path x = !path_printer x +let print_path env sigma x = !path_printer env sigma x -let message_ambig l = - (str"Ambiguous paths:" ++ spc () ++ - prlist_with_sep fnl (fun ijp -> print_path ijp) l) +let message_ambig env sigma l = + str"Ambiguous paths:" ++ spc () ++ + prlist_with_sep fnl (fun ijp -> print_path env sigma ijp) l (* add_coercion_in_graph : coe_index * cl_index * cl_index -> unit coercion,source,target *) @@ -344,8 +346,8 @@ let different_class_params i = | CL_IND i -> Global.is_polymorphic (IndRef i) | CL_CONST c -> Global.is_polymorphic (ConstRef c) | _ -> false - -let add_coercion_in_graph (ic,source,target) = + +let add_coercion_in_graph env sigma (ic,source,target) = let old_inheritance_graph = !inheritance_graph in let ambig_paths = (ref [] : ((cl_index * cl_index) * inheritance_path) list ref) in @@ -386,8 +388,8 @@ let add_coercion_in_graph (ic,source,target) = old_inheritance_graph end; let is_ambig = match !ambig_paths with [] -> false | _ -> true in - if is_ambig && is_verbose () then - Feedback.msg_info (message_ambig !ambig_paths) + if is_ambig && not !Flags.quiet then + Feedback.msg_info (message_ambig env sigma !ambig_paths) type coercion = { coercion_type : coe_typ; @@ -402,8 +404,8 @@ type coercion = { (* Computation of the class arity *) let reference_arity_length ref = - let t = Universes.unsafe_type_of_global ref in - List.length (fst (Reductionops.splay_arity (Global.env()) Evd.empty t)) + let t, _ = Global.type_of_global_in_context (Global.env ()) ref in + List.length (fst (Reductionops.splay_arity (Global.env()) Evd.empty (EConstr.of_constr t))) (** FIXME *) let projection_arity_length p = let len = reference_arity_length (ConstRef p) in @@ -427,20 +429,20 @@ let automatically_import_coercions = ref false open Goptions let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = true; (* remove in 8.8 *) optname = "automatic import of coercions"; optkey = ["Automatic";"Coercions";"Import"]; optread = (fun () -> !automatically_import_coercions); optwrite = (:=) automatically_import_coercions } -let cache_coercion (_, c) = +let cache_coercion env sigma (_, c) = let () = add_class c.coercion_source in let () = add_class c.coercion_target in let is, _ = class_info c.coercion_source in let it, _ = class_info c.coercion_target in - let value, ctx = Universes.fresh_global_instance (Global.env()) c.coercion_type in - let typ = Retyping.get_type_of (Global.env ()) Evd.empty value in + let value, ctx = Universes.fresh_global_instance env c.coercion_type in + let typ = Retyping.get_type_of env sigma (EConstr.of_constr value) in + let typ = EConstr.Unsafe.to_constr typ in let xf = { coe_value = value; coe_type = typ; @@ -450,19 +452,15 @@ let cache_coercion (_, c) = coe_is_projection = c.coercion_is_proj; coe_param = c.coercion_params } in let () = add_new_coercion c.coercion_type xf in - add_coercion_in_graph (xf,is,it) + add_coercion_in_graph env sigma (xf,is,it) let load_coercion _ o = - if - !automatically_import_coercions || Flags.version_less_or_equal Flags.V8_2 - then - cache_coercion o + if !automatically_import_coercions then + cache_coercion (Global.env ()) Evd.empty o let open_coercion i o = - if Int.equal i 1 && not - (!automatically_import_coercions || Flags.version_less_or_equal Flags.V8_2) - then - cache_coercion o + if Int.equal i 1 && not !automatically_import_coercions then + cache_coercion (Global.env ()) Evd.empty o let subst_coercion (subst, c) = let coe = subst_coe_typ subst c.coercion_type in @@ -501,7 +499,9 @@ let inCoercion : coercion -> obj = declare_object {(default_object "COERCION") with open_function = open_coercion; load_function = load_coercion; - cache_function = cache_coercion; + cache_function = (fun objn -> + let env = Global.env () in cache_coercion env Evd.empty objn + ); subst_function = subst_coercion; classify_function = classify_coercion; discharge_function = discharge_coercion } @@ -538,7 +538,7 @@ let inheritance_graph () = let coercion_of_reference r = let ref = Nametab.global r in if not (coercion_exists ref) then - errorlabstrm "try_add_coercion" + user_err ~hdr:"try_add_coercion" (Nametab.pr_global_env Id.Set.empty ref ++ str" is not a coercion."); ref @@ -554,7 +554,6 @@ module CoercionPrinting = let member_message x b = str "Explicit printing of coercion " ++ printer x ++ str (if b then " is set" else " is unset") - let synchronous = true end module PrintingCoercion = Goptions.MakeRefTable(CoercionPrinting) |