diff options
Diffstat (limited to 'pretyping/classops.ml')
| -rw-r--r-- | pretyping/classops.ml | 148 |
1 files changed, 51 insertions, 97 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 5560e5e5f5..57dbfb2580 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -15,7 +15,6 @@ open Names open Constr open Libnames open Globnames -open Libobject open Mod_subst (* usage qque peu general: utilise aussi dans record *) @@ -59,7 +58,7 @@ let cl_typ_ord t1 t2 = match t1, t2 with | CL_CONST c1, CL_CONST 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 *) + | _ -> pervasives_compare t1 t2 (** OK *) module ClTyp = struct type t = cl_typ @@ -226,14 +225,14 @@ let string_of_class = function | CL_FUN -> "Funclass" | CL_SORT -> "Sortclass" | CL_CONST sp -> - string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (ConstRef sp)) + string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (GlobRef.ConstRef sp)) | CL_PROJ sp -> let sp = Projection.Repr.constant sp in - string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (ConstRef sp)) + string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (GlobRef.ConstRef sp)) | CL_IND sp -> - string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (IndRef sp)) + string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (GlobRef.IndRef sp)) | CL_SECVAR sp -> - string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (VarRef sp)) + string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (GlobRef.VarRef sp)) let pr_class x = str (string_of_class x) @@ -277,8 +276,8 @@ 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 +let mkNamed = let open GlobRef in function + | ConstRef c -> EConstr.mkConst c | VarRef v -> EConstr.mkVar v | ConstructRef c -> EConstr.mkConstruct c | IndRef i -> EConstr.mkInd i @@ -288,7 +287,7 @@ let get_coercion_constructor env coe = 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 + c, Inductiveops.constructor_nrealargs env c -1 | _ -> raise Not_found let lookup_pattern_path_between env (s,t) = @@ -305,8 +304,8 @@ let install_path_printer f = path_printer := f let print_path x = !path_printer x -let path_comparator : (inheritance_path -> inheritance_path -> bool) ref = - ref (fun _ _ -> false) +let path_comparator : (Environ.env -> Evd.evar_map -> inheritance_path -> inheritance_path -> bool) ref = + ref (fun _ _ _ _ -> false) let install_path_comparator f = path_comparator := f @@ -314,30 +313,32 @@ let compare_path p q = !path_comparator p q let warn_ambiguous_path = CWarnings.create ~name:"ambiguous-paths" ~category:"typechecker" - (fun l -> strbrk"Ambiguous paths: " ++ prlist_with_sep fnl print_path l) + (fun l -> prlist_with_sep fnl (fun (c,p,q) -> + str"New coercion path " ++ print_path (c,p) ++ + str" is ambiguous with existing " ++ print_path (c, q) ++ str".") l) (* add_coercion_in_graph : coe_index * cl_index * cl_index -> unit coercion,source,target *) -let different_class_params i = +let different_class_params env i = let ci = class_info_from_index i in if (snd ci).cl_param > 0 then true else match fst ci with - | CL_IND i -> Global.is_polymorphic (IndRef i) - | CL_CONST c -> Global.is_polymorphic (ConstRef c) + | CL_IND i -> Environ.is_polymorphic env (GlobRef.IndRef i) + | CL_CONST c -> Environ.is_polymorphic env (GlobRef.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 + (ref [] : ((cl_index * cl_index) * inheritance_path * inheritance_path) list ref) in let try_add_new_path (i,j as ij) p = - if not (Bijint.Index.equal i j) || different_class_params i then + if not (Bijint.Index.equal i j) || different_class_params env i then match lookup_path_between_class ij with | q -> - if not (compare_path p q) then - ambig_paths := (ij,p)::!ambig_paths; + if not (compare_path env sigma p q) then + ambig_paths := (ij,p,q)::!ambig_paths; false | exception Not_found -> (add_new_path ij p; true) else @@ -374,31 +375,42 @@ type coercion = { coercion_params : int; } +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 + 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; } + (* Computation of the class arity *) -let reference_arity_length ref = - let t, _ = Typeops.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 reference_arity_length env sigma ref = + let t, _ = Typeops.type_of_global_in_context env ref in + List.length (fst (Reductionops.splay_arity env sigma (EConstr.of_constr t))) -let projection_arity_length p = - let len = reference_arity_length (ConstRef (Projection.Repr.constant p)) in +let projection_arity_length env sigma p = + let len = reference_arity_length env sigma (GlobRef.ConstRef (Projection.Repr.constant p)) in len - Projection.Repr.npars p -let class_params = function +let class_params env sigma = function | CL_FUN | CL_SORT -> 0 - | CL_CONST sp -> reference_arity_length (ConstRef sp) - | CL_PROJ sp -> projection_arity_length sp - | CL_SECVAR sp -> reference_arity_length (VarRef sp) - | CL_IND sp -> reference_arity_length (IndRef sp) + | CL_CONST sp -> reference_arity_length env sigma (GlobRef.ConstRef sp) + | CL_PROJ sp -> projection_arity_length env sigma sp + | CL_SECVAR sp -> reference_arity_length env sigma (GlobRef.VarRef sp) + | CL_IND sp -> reference_arity_length env sigma (GlobRef.IndRef sp) (* add_class : cl_typ -> locality_flag option -> bool -> unit *) -let add_class cl = - add_new_class cl { cl_param = class_params cl } +let add_class env sigma cl = + add_new_class cl { cl_param = class_params env sigma cl } -let cache_coercion (_, c) = - let () = add_class c.coercion_source in - let () = add_class c.coercion_target in +let declare_coercion env sigma c = + let () = add_class env sigma c.coercion_source in + let () = add_class env sigma c.coercion_target in let is, _ = class_info c.coercion_source in let it, _ = class_info c.coercion_target in let xf = @@ -409,65 +421,7 @@ let cache_coercion (_, c) = coe_param = c.coercion_params; } in let () = add_new_coercion c.coercion_type xf in - add_coercion_in_graph (xf,is,it) - -let open_coercion i o = - if Int.equal i 1 then - cache_coercion o - -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 - 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_coercion (_, c) = - if c.coercion_local then None - else - let n = - try - let ins = Lib.section_instance c.coercion_type in - Array.length (snd ins) - with Not_found -> 0 - in - let nc = { c with - coercion_params = n + c.coercion_params; - coercion_is_proj = Option.map Lib.discharge_proj_repr c.coercion_is_proj; - } in - Some nc - -let classify_coercion obj = - if obj.coercion_local then Dispose else Substitute obj - -let inCoercion : coercion -> obj = - declare_object {(default_object "COERCION") with - open_function = open_coercion; - cache_function = cache_coercion; - subst_function = subst_coercion; - classify_function = classify_coercion; - discharge_function = discharge_coercion } - -let declare_coercion coef ?(local = false) ~isid ~src:cls ~target:clt ~params:ps = - let isproj = - match coef with - | ConstRef c -> Recordops.find_primitive_projection c - | _ -> None - in - let c = { - coercion_type = coef; - coercion_local = local; - coercion_is_id = isid; - coercion_is_proj = isproj; - coercion_source = cls; - coercion_target = clt; - coercion_params = ps; - } in - Lib.add_anonymous_leaf (inCoercion c) + add_coercion_in_graph env sigma (xf,is,it) (* For printing purpose *) let pr_cl_index = Bijint.Index.print @@ -489,8 +443,8 @@ let coercion_of_reference r = module CoercionPrinting = struct type t = coe_typ - let compare = GlobRef.Ordered.compare - let encode = coercion_of_reference + module Set = GlobRef.Set + let encode _env = coercion_of_reference let subst = subst_coe_typ let printer x = Nametab.pr_global_env Id.Set.empty x let key = ["Printing";"Coercion"] |