From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- pretyping/classops.ml | 126 ++++++++++++++++++++++++++------------------------ 1 file changed, 66 insertions(+), 60 deletions(-) (limited to 'pretyping/classops.ml') diff --git a/pretyping/classops.ml b/pretyping/classops.ml index a0804b72..52e02c87 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -31,29 +31,26 @@ type cl_typ = | CL_SECVAR of variable | CL_CONST of Constant.t | CL_IND of inductive - | CL_PROJ of Constant.t + | CL_PROJ of Projection.Repr.t type cl_info_typ = { cl_param : int } -type coe_typ = global_reference +type coe_typ = GlobRef.t module CoeTypMap = Refmap_env type coe_info_typ = { - coe_value : constr; - coe_type : types; + coe_value : GlobRef.t; coe_local : bool; - coe_context : Univ.ContextSet.t; coe_is_identity : bool; - coe_is_projection : bool; - coe_param : int } + coe_is_projection : Projection.Repr.t option; + 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 && + GlobRef.equal c1.coe_value c2.coe_value && c1.coe_local == c2.coe_local && c1.coe_is_identity == c2.coe_is_identity && c1.coe_is_projection == c2.coe_is_projection && @@ -62,7 +59,7 @@ 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 -> Constant.CanOrd.compare c1 c2 - | CL_PROJ c1, CL_PROJ c2 -> Constant.CanOrd.compare c1 c2 + | CL_PROJ c1, CL_PROJ c2 -> Projection.Repr.CanOrd.compare c1 c2 | CL_IND i1, CL_IND i2 -> ind_ord i1 i2 | _ -> Pervasives.compare t1 t2 (** OK *) @@ -77,9 +74,7 @@ module IntMap = Map.Make(Int) let cl_typ_eq t1 t2 = Int.equal (cl_typ_ord t1 t2) 0 -type coe_index = coe_info_typ - -type inheritance_path = coe_index list +type inheritance_path = coe_info_typ list (* table des classes, des coercions et graphe d'heritage *) @@ -123,6 +118,9 @@ let class_tab = let coercion_tab = ref (CoeTypMap.empty : coe_info_typ CoeTypMap.t) +let coercions_in_scope = + ref Refset_env.empty + module ClPairOrd = struct type t = cl_index * cl_index @@ -136,12 +134,13 @@ module ClPairMap = Map.Make(ClPairOrd) let inheritance_graph = ref (ClPairMap.empty : inheritance_path ClPairMap.t) -let freeze _ = (!class_tab, !coercion_tab, !inheritance_graph) +let freeze _ = (!class_tab, !coercion_tab, !inheritance_graph, !coercions_in_scope) -let unfreeze (fcl,fco,fig) = +let unfreeze (fcl,fco,fig,in_scope) = class_tab:=fcl; coercion_tab:=fco; - inheritance_graph:=fig + inheritance_graph:=fig; + coercions_in_scope:=in_scope (* ajout de nouveaux "objets" *) @@ -199,7 +198,7 @@ let find_class_type sigma t = | 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), EInstance.empty, (c :: args) + CL_PROJ (Projection.repr p), EInstance.empty, (c :: args) | Ind (ind_sp,u) -> CL_IND ind_sp, u, args | Prod (_,_,_) -> CL_FUN, EInstance.empty, [] | Sort _ -> CL_SORT, EInstance.empty, [] @@ -211,7 +210,7 @@ let subst_cl_typ subst ct = match ct with | CL_FUN | CL_SECVAR _ -> ct | CL_PROJ c -> - let c',t = subst_con_kn subst c in + let c' = subst_proj_repr subst c in if c' == c then ct else CL_PROJ c' | CL_CONST c -> let c',t = subst_con_kn subst c in @@ -248,8 +247,11 @@ let class_args_of env sigma c = pi3 (find_class_type sigma c) let string_of_class = function | CL_FUN -> "Funclass" | CL_SORT -> "Sortclass" - | CL_CONST sp | CL_PROJ sp -> - string_of_qualid (shortest_qualid_of_global Id.Set.empty (ConstRef sp)) + | CL_CONST sp -> + string_of_qualid (shortest_qualid_of_global Id.Set.empty (ConstRef sp)) + | CL_PROJ sp -> + let sp = Projection.Repr.constant sp in + string_of_qualid (shortest_qualid_of_global Id.Set.empty (ConstRef sp)) | CL_IND sp -> string_of_qualid (shortest_qualid_of_global Id.Set.empty (IndRef sp)) | CL_SECVAR sp -> @@ -297,31 +299,25 @@ let lookup_path_to_fun_from env sigma s = let lookup_path_to_sort_from env sigma s = apply_on_class_of env sigma s lookup_path_to_sort_from_class +let mkNamed = function + | GlobRef.ConstRef c -> EConstr.mkConst c + | VarRef v -> EConstr.mkVar v + | ConstructRef c -> EConstr.mkConstruct c + | IndRef i -> EConstr.mkInd i + let get_coercion_constructor env coe = - let c, _ = - Reductionops.whd_all_stack env Evd.empty (EConstr.of_constr coe.coe_value) - in - match EConstr.kind Evd.empty (** FIXME *) c with - | Construct (cstr,u) -> - (cstr, Inductiveops.constructor_nrealargs cstr -1) - | _ -> - raise Not_found + let evd = Evd.from_env env in + let red x = fst (Reductionops.whd_all_stack env evd x) in + match EConstr.kind evd (red (mkNamed coe.coe_value)) with + | Constr.Construct (c, _) -> + c, Inductiveops.constructor_nrealargs c -1 + | _ -> raise Not_found let lookup_pattern_path_between env (s,t) = let i = inductive_class_of s in let j = inductive_class_of t in List.map (get_coercion_constructor env) (ClPairMap.find (i,j) !inheritance_graph) -(* coercion_value : coe_index -> unsafe_judgment * bool *) - -let coercion_value { coe_value = c; coe_type = t; coe_context = ctx; - coe_is_identity = b; coe_is_projection = b' } = - 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 (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 : (env -> Evd.evar_map -> (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t) ref = @@ -395,7 +391,7 @@ type coercion = { coercion_type : coe_typ; coercion_local : bool; coercion_is_id : bool; - coercion_is_proj : bool; + coercion_is_proj : Projection.Repr.t option; coercion_source : cl_typ; coercion_target : cl_typ; coercion_params : int; @@ -408,9 +404,8 @@ let reference_arity_length ref = 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 - let pb = Environ.lookup_projection (Projection.make p false) (Global.env ()) in - len - pb.Declarations.proj_npars + let len = reference_arity_length (ConstRef (Projection.Repr.constant p)) in + len - Projection.Repr.npars p let class_params = function | CL_FUN | CL_SORT -> 0 @@ -440,17 +435,13 @@ let cache_coercion env sigma (_, c) = 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 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; - coe_context = ctx; + { coe_value = c.coercion_type; coe_local = c.coercion_local; coe_is_identity = c.coercion_is_id; coe_is_projection = c.coercion_is_proj; - coe_param = c.coercion_params } in + coe_param = c.coercion_params; + } in let () = add_new_coercion c.coercion_type xf in add_coercion_in_graph env sigma (xf,is,it) @@ -458,21 +449,32 @@ let load_coercion _ o = if !automatically_import_coercions then cache_coercion (Global.env ()) Evd.empty o +let set_coercion_in_scope (_, c) = + let r = c.coercion_type in + coercions_in_scope := Refset_env.add r !coercions_in_scope + let open_coercion i o = - if Int.equal i 1 && not !automatically_import_coercions then - cache_coercion (Global.env ()) Evd.empty o + if Int.equal i 1 then begin + set_coercion_in_scope o; + if not !automatically_import_coercions then + cache_coercion (Global.env ()) Evd.empty o + end let subst_coercion (subst, c) = let coe = subst_coe_typ subst c.coercion_type in let cls = subst_cl_typ subst c.coercion_source in let clt = subst_cl_typ subst c.coercion_target in - if c.coercion_type == coe && c.coercion_source == cls && c.coercion_target == clt then c - else { c with coercion_type = coe; coercion_source = cls; coercion_target = clt } + let clp = Option.Smart.map (subst_proj_repr subst) c.coercion_is_proj in + if c.coercion_type == coe && c.coercion_source == cls && + c.coercion_target == clt && c.coercion_is_proj == clp + then c + else { c with coercion_type = coe; coercion_source = cls; + coercion_target = clt; coercion_is_proj = clp; } let discharge_cl = function | CL_CONST kn -> CL_CONST (Lib.discharge_con kn) | CL_IND ind -> CL_IND (Lib.discharge_inductive ind) - | CL_PROJ p -> CL_PROJ (Lib.discharge_con p) + | CL_PROJ p -> CL_PROJ (Lib.discharge_proj_repr p) | cl -> cl let discharge_coercion (_, c) = @@ -489,6 +491,7 @@ let discharge_coercion (_, c) = coercion_source = discharge_cl c.coercion_source; coercion_target = discharge_cl c.coercion_target; coercion_params = n + c.coercion_params; + coercion_is_proj = Option.map Lib.discharge_proj_repr c.coercion_is_proj; } in Some nc @@ -500,7 +503,9 @@ let inCoercion : coercion -> obj = open_function = open_coercion; load_function = load_coercion; cache_function = (fun objn -> - let env = Global.env () in cache_coercion env Evd.empty objn + let env = Global.env () in + set_coercion_in_scope objn; + cache_coercion env Evd.empty objn ); subst_function = subst_coercion; classify_function = classify_coercion; @@ -509,8 +514,8 @@ let inCoercion : coercion -> obj = let declare_coercion coef ?(local = false) ~isid ~src:cls ~target:clt ~params:ps = let isproj = match coef with - | ConstRef c -> Environ.is_projection c (Global.env ()) - | _ -> false + | ConstRef c -> Recordops.find_primitive_projection c + | _ -> None in let c = { coercion_type = coef; @@ -524,8 +529,6 @@ let declare_coercion coef ?(local = false) ~isid ~src:cls ~target:clt ~params:ps Lib.add_anonymous_leaf (inCoercion c) (* For printing purpose *) -let get_coercion_value v = v.coe_value - let pr_cl_index = Bijint.Index.print let classes () = Bijint.dom !class_tab @@ -563,3 +566,6 @@ let hide_coercion coe = let coe_info = coercion_info coe in Some coe_info.coe_param else None + +let is_coercion_in_scope r = + Refset_env.mem r !coercions_in_scope -- cgit v1.2.3