diff options
Diffstat (limited to 'pretyping/classops.ml')
| -rw-r--r-- | pretyping/classops.ml | 153 |
1 files changed, 52 insertions, 101 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml index ef918a614e..90ce1cc594 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -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 *) @@ -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,42 +304,43 @@ let install_path_printer f = path_printer := f let print_path x = !path_printer x -let message_ambig l = - str"Ambiguous paths:" ++ spc () ++ - prlist_with_sep fnl print_path l +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 + +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) (* 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 (IndRef i) + | CL_CONST c -> Environ.is_polymorphic env (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 let try_add_new_path (i,j as ij) p = - try - if Bijint.Index.equal i j then begin - if different_class_params i then begin - let _ = lookup_path_between_class ij in - ambig_paths := (ij,p)::!ambig_paths - end - end else begin - let _ = lookup_path_between_class ij in - ambig_paths := (ij,p)::!ambig_paths - end; + 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 env sigma p q) then + ambig_paths := (ij,p)::!ambig_paths; + false + | exception Not_found -> (add_new_path ij p; true) + else false - with Not_found -> begin - add_new_path ij p; - true - end in let try_add_new_path1 ij p = let _ = try_add_new_path ij p in () @@ -361,9 +361,7 @@ let add_coercion_in_graph (ic,source,target) = end) old_inheritance_graph end; - let is_ambig = match !ambig_paths with [] -> false | _ -> true in - if is_ambig && not !Flags.quiet then - Feedback.msg_info (message_ambig !ambig_paths) + match !ambig_paths with [] -> () | _ -> warn_ambiguous_path !ambig_paths type coercion = { coercion_type : coe_typ; @@ -375,31 +373,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 (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 (ConstRef sp) + | CL_PROJ sp -> projection_arity_length env sigma sp + | CL_SECVAR sp -> reference_arity_length env sigma (VarRef sp) + | CL_IND sp -> reference_arity_length env sigma (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 = @@ -410,65 +419,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 @@ -491,7 +442,7 @@ module CoercionPrinting = struct type t = coe_typ let compare = GlobRef.Ordered.compare - let encode = coercion_of_reference + 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"] |