From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- pretyping/classops.ml | 370 ++++++++++++++++++++++++++++++++------------------ 1 file changed, 238 insertions(+), 132 deletions(-) (limited to 'pretyping/classops.ml') diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 59f3c740..559f5fe6 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -1,24 +1,23 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Id.compare v1 v2 + | CL_CONST c1, CL_CONST c2 -> con_user_ord c1 c2 + | CL_PROJ c1, CL_PROJ c2 -> con_user_ord c1 c2 + | CL_IND i1, CL_IND i2 -> ind_user_ord i1 i2 + | _ -> Pervasives.compare t1 t2 (** OK *) + +module ClTyp = struct + type t = cl_typ + let compare = cl_typ_ord +end + +module ClTypMap = Map.Make(ClTyp) -type cl_index = int +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 @@ -61,31 +82,60 @@ type inheritance_path = coe_index list (* table des classes, des coercions et graphe d'heritage *) -module Bijint = struct - type ('a,'b) t = { v : ('a * 'b) array; s : int; inv : ('a,int) Gmap.t } - let empty = { v = [||]; s = 0; inv = Gmap.empty } - let mem y b = Gmap.mem y b.inv - let map x b = if 0 <= x & x < b.s then b.v.(x) else raise Not_found - let revmap y b = let n = Gmap.find y b.inv in (n, snd (b.v.(n))) +module Bijint : +sig + module Index : + sig + type t + val compare : t -> t -> int + val equal : t -> t -> bool + val print : t -> std_ppcmds + end + type 'a t + val empty : 'a t + val mem : cl_typ -> 'a t -> bool + val map : Index.t -> 'a t -> cl_typ * 'a + val revmap : cl_typ -> 'a t -> Index.t * 'a + val add : cl_typ -> 'a -> 'a t -> 'a t + val dom : 'a t -> cl_typ list +end += +struct + + module Index = struct include Int let print = Pp.int end + + type 'a t = { v : (cl_typ * 'a) IntMap.t; s : int; inv : int ClTypMap.t } + let empty = { v = IntMap.empty; s = 0; inv = ClTypMap.empty } + let mem y b = ClTypMap.mem y b.inv + let map x b = IntMap.find x b.v + let revmap y b = let n = ClTypMap.find y b.inv in (n, snd (IntMap.find n b.v)) let add x y b = - let v = - if b.s = Array.length b.v then - (let v = Array.make (b.s + 8) (x,y) in Array.blit b.v 0 v 0 b.s; v) - else b.v in - v.(b.s) <- (x,y); { v = v; s = b.s+1; inv = Gmap.add x b.s b.inv } - let dom b = Gmap.dom b.inv + { v = IntMap.add b.s (x,y) b.v; s = b.s+1; inv = ClTypMap.add x b.s b.inv } + let dom b = List.rev (ClTypMap.fold (fun x _ acc -> x::acc) b.inv []) end +type cl_index = Bijint.Index.t + let class_tab = - ref (Bijint.empty : (cl_typ, cl_info_typ) Bijint.t) + ref (Bijint.empty : cl_info_typ Bijint.t) let coercion_tab = - ref (Gmap.empty : (coe_typ, coe_info_typ) Gmap.t) + ref (CoeTypMap.empty : coe_info_typ CoeTypMap.t) + +module ClPairOrd = +struct + type t = cl_index * cl_index + let compare (i1, j1) (i2, j2) = + let c = Bijint.Index.compare i1 i2 in + if Int.equal c 0 then Bijint.Index.compare j1 j2 else c +end + +module ClPairMap = Map.Make(ClPairOrd) let inheritance_graph = - ref (Gmap.empty : (cl_index * cl_index, inheritance_path) Gmap.t) + ref (ClPairMap.empty : inheritance_path ClPairMap.t) -let freeze () = (!class_tab, !coercion_tab, !inheritance_graph) +let freeze _ = (!class_tab, !coercion_tab, !inheritance_graph) let unfreeze (fcl,fco,fig) = class_tab:=fcl; @@ -99,17 +149,17 @@ let add_new_class cl s = class_tab := Bijint.add cl s !class_tab let add_new_coercion coe s = - coercion_tab := Gmap.add coe s !coercion_tab + coercion_tab := CoeTypMap.add coe s !coercion_tab let add_new_path x y = - inheritance_graph := Gmap.add x y !inheritance_graph + inheritance_graph := ClPairMap.add x y !inheritance_graph let init () = class_tab:= Bijint.empty; add_new_class CL_FUN { cl_param = 0 }; add_new_class CL_SORT { cl_param = 0 }; - coercion_tab:= Gmap.empty; - inheritance_graph:= Gmap.empty + coercion_tab:= CoeTypMap.empty; + inheritance_graph:= ClPairMap.empty let _ = Summary.declare_summary "inh_graph" @@ -135,20 +185,22 @@ let cl_sort_index = fst(class_info CL_SORT) (* coercion_info : coe_typ -> coe_info_typ *) -let coercion_info coe = Gmap.find coe !coercion_tab +let coercion_info coe = CoeTypMap.find coe !coercion_tab -let coercion_exists coe = Gmap.mem coe !coercion_tab +let coercion_exists coe = CoeTypMap.mem coe !coercion_tab -(* find_class_type : evar_map -> constr -> cl_typ * constr list *) +(* find_class_type : evar_map -> constr -> cl_typ * universe_list * constr list *) let find_class_type sigma t = let t', args = Reductionops.whd_betaiotazeta_stack sigma t in match kind_of_term t' with - | Var id -> CL_SECVAR id, args - | Const sp -> CL_CONST sp, args - | Ind ind_sp -> CL_IND ind_sp, args - | Prod (_,_,_) -> CL_FUN, [] - | Sort _ -> CL_SORT, [] + | Var id -> CL_SECVAR id, Univ.Instance.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 + | Ind (ind_sp,u) -> CL_IND ind_sp, u, args + | Prod (_,_,_) -> CL_FUN, Univ.Instance.empty, [] + | Sort _ -> CL_SORT, Univ.Instance.empty, [] | _ -> raise Not_found @@ -156,55 +208,57 @@ let subst_cl_typ subst ct = match ct with CL_SORT | CL_FUN | CL_SECVAR _ -> ct - | CL_CONST kn -> - let kn',t = subst_con subst kn in - if kn' == kn then ct else - fst (find_class_type Evd.empty t) - | CL_IND (kn,i) -> - let kn' = subst_ind subst kn in - if kn' == kn then ct else - CL_IND (kn',i) + | CL_PROJ c -> + let c',t = subst_con_kn subst c in + if c' == c then ct else CL_PROJ c' + | 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) + | CL_IND i -> + let i' = subst_ind subst i in + if i' == i then ct else CL_IND i' (*CSC: here we should change the datatype for coercions: it should be possible to declare any term as a coercion *) -let subst_coe_typ subst t = fst (subst_global subst t) +let subst_coe_typ subst t = subst_global_reference subst t (* class_of : Term.constr -> int *) let class_of env sigma t = - let (t, n1, i, args) = + let (t, n1, i, u, args) = try - let (cl,args) = find_class_type sigma t in + let (cl, u, args) = find_class_type sigma t in let (i, { cl_param = n1 } ) = class_info cl in - (t, n1, i, args) + (t, n1, i, u, args) with Not_found -> let t = Tacred.hnf_constr env sigma t in - let (cl, args) = find_class_type sigma t in + let (cl, u, args) = find_class_type sigma t in let (i, { cl_param = n1 } ) = class_info cl in - (t, n1, i, args) + (t, n1, i, u, args) in - if List.length args = n1 then t, i else raise Not_found + if Int.equal (List.length args) n1 then t, i else raise Not_found let inductive_class_of ind = fst (class_info (CL_IND ind)) -let class_args_of env sigma c = snd (find_class_type sigma c) +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 -> - string_of_qualid (shortest_qualid_of_global Idset.empty (ConstRef sp)) + | CL_CONST sp | CL_PROJ sp -> + string_of_qualid (shortest_qualid_of_global Id.Set.empty (ConstRef sp)) | CL_IND sp -> - string_of_qualid (shortest_qualid_of_global Idset.empty (IndRef sp)) + string_of_qualid (shortest_qualid_of_global Id.Set.empty (IndRef sp)) | CL_SECVAR sp -> - string_of_qualid (shortest_qualid_of_global Idset.empty (VarRef sp)) + string_of_qualid (shortest_qualid_of_global Id.Set.empty (VarRef sp)) let pr_class x = str (string_of_class x) (* lookup paths *) let lookup_path_between_class (s,t) = - Gmap.find (s,t) !inheritance_graph + ClPairMap.find (s,t) !inheritance_graph let lookup_path_to_fun_from_class s = lookup_path_between_class (s,cl_fun_index) @@ -216,16 +270,16 @@ let lookup_path_to_sort_from_class s = let apply_on_class_of env sigma t cont = try - let (cl,args) = find_class_type sigma t in + let (cl,u,args) = find_class_type sigma t in let (i, { cl_param = n1 } ) = class_info cl in - if List.length args <> n1 then raise Not_found; + if not (Int.equal (List.length args) n1) then raise Not_found; t, cont i with Not_found -> (* Is it worth to be more incremental on the delta steps? *) let t = Tacred.hnf_constr env sigma t in - let (cl, args) = find_class_type sigma t in + let (cl, u, args) = find_class_type sigma t in let (i, { cl_param = n1 } ) = class_info cl in - if List.length args <> n1 then raise Not_found; + if not (Int.equal (List.length args) n1) then raise Not_found; t, cont i let lookup_path_between env sigma (s,t) = @@ -241,31 +295,35 @@ 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 get_coercion_constructor coe = +let get_coercion_constructor env coe = let c, _ = - Reductionops.whd_betadeltaiota_stack (Global.env()) Evd.empty coe.coe_value + Reductionops.whd_betadeltaiota_stack env Evd.empty coe.coe_value in match kind_of_term c with - | Construct cstr -> - (cstr, Inductiveops.constructor_nrealargs (Global.env()) cstr -1) + | Construct (cstr,u) -> + (cstr, Inductiveops.constructor_nrealargs cstr -1) | _ -> raise Not_found -let lookup_pattern_path_between (s,t) = +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 (Gmap.find (i,j) !inheritance_graph) + 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_is_identity = b } = - (make_judge c t, b) +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 c' t', b, b'), ctx (* pretty-print functions are now in Pretty *) (* rajouter une coercion dans le graphe *) let path_printer = ref (fun _ -> str "" - : (int * int) * inheritance_path -> std_ppcmds) + : (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> std_ppcmds) let install_path_printer f = path_printer := f @@ -273,27 +331,33 @@ let print_path x = !path_printer x let message_ambig l = (str"Ambiguous paths:" ++ spc () ++ - prlist_with_sep pr_fnl (fun ijp -> print_path ijp) l) + prlist_with_sep fnl (fun ijp -> print_path ijp) l) (* add_coercion_in_graph : coe_index * cl_index * cl_index -> unit coercion,source,target *) -let different_class_params i j = - (snd (class_info_from_index i)).cl_param > 0 - +let different_class_params 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) + | _ -> false + let add_coercion_in_graph (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 i=j then begin - if different_class_params i j then begin + 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 (i,j) in + let _ = lookup_path_between_class ij in ambig_paths := (ij,p)::!ambig_paths end; false @@ -306,35 +370,50 @@ let add_coercion_in_graph (ic,source,target) = let _ = try_add_new_path ij p in () in if try_add_new_path (source,target) [ic] then begin - Gmap.iter + ClPairMap.iter (fun (s,t) p -> - if s<>t then begin - if t = source then begin + if not (Bijint.Index.equal s t) then begin + if Bijint.Index.equal t source then begin try_add_new_path1 (s,target) (p@[ic]); - Gmap.iter + ClPairMap.iter (fun (u,v) q -> - if u<>v & u = target && not (list_equal coe_info_typ_equal p q) then + if not (Bijint.Index.equal u v) && Bijint.Index.equal u target && not (List.equal coe_info_typ_equal p q) then try_add_new_path1 (s,v) (p@[ic]@q)) old_inheritance_graph end; - if s = target then try_add_new_path1 (source,t) (ic::p) + if Bijint.Index.equal s target then try_add_new_path1 (source,t) (ic::p) end) old_inheritance_graph end; - if (!ambig_paths <> []) && is_verbose () then - ppnl (message_ambig !ambig_paths) - -type coercion = coe_typ * locality * bool * cl_typ * cl_typ * int + let is_ambig = match !ambig_paths with [] -> false | _ -> true in + if is_ambig && is_verbose () then + msg_warning (message_ambig !ambig_paths) + +type coercion = { + coercion_type : coe_typ; + coercion_local : bool; + coercion_is_id : bool; + coercion_is_proj : bool; + coercion_source : cl_typ; + coercion_target : cl_typ; + coercion_params : int; +} -(* Calcul de l'arit้ d'une classe *) +(* Computation of the class arity *) let reference_arity_length ref = - let t = Global.type_of_global ref in + let t = Universes.unsafe_type_of_global ref in List.length (fst (Reductionops.splay_arity (Global.env()) Evd.empty t)) +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 class_params = 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) @@ -355,18 +434,22 @@ let _ = optread = (fun () -> !automatically_import_coercions); optwrite = (:=) automatically_import_coercions } -let cache_coercion (_,(coe,stre,isid,cls,clt,ps)) = - add_class cls; - add_class clt; - let is,_ = class_info cls in - let it,_ = class_info clt in +let cache_coercion (_, 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 xf = - { coe_value = constr_of_global coe; - coe_type = Global.type_of_global coe; - coe_strength = stre; - coe_is_identity = isid; - coe_param = ps } in - add_new_coercion coe xf; + { coe_value = value; + coe_type = typ; + coe_context = ctx; + 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 + let () = add_new_coercion c.coercion_type xf in add_coercion_in_graph (xf,is,it) let load_coercion _ o = @@ -376,40 +459,45 @@ let load_coercion _ o = cache_coercion o let open_coercion i o = - if i = 1 && not + if Int.equal i 1 && not (!automatically_import_coercions || Flags.version_less_or_equal Flags.V8_2) then cache_coercion o -let subst_coercion (subst,(coe,stre,isid,cls,clt,ps as obj)) = - let coe' = subst_coe_typ subst coe in - let cls' = subst_cl_typ subst cls in - let clt' = subst_cl_typ subst clt in - if coe' == coe && cls' == cls & clt' == clt then obj else - (coe',stre,isid,cls',clt',ps) +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 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 -> cl -let discharge_coercion (_,(coe,stre,isid,cls,clt,ps)) = - if stre = Local then None else - let n = try Array.length (Lib.section_instance coe) with Not_found -> 0 in - Some (Lib.discharge_global coe, - stre, - isid, - discharge_cl cls, - discharge_cl clt, - n + ps) - -let classify_coercion (coe,stre,isid,cls,clt,ps as obj) = - if stre = Local then Dispose else Substitute obj - -type coercion_obj = - coe_typ * Decl_kinds.locality * bool * cl_typ * cl_typ * int - -let inCoercion : coercion_obj -> obj = +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_type = Lib.discharge_global c.coercion_type; + coercion_source = discharge_cl c.coercion_source; + coercion_target = discharge_cl c.coercion_target; + coercion_params = n + c.coercion_params; + } 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; load_function = load_coercion; @@ -418,31 +506,49 @@ let inCoercion : coercion_obj -> obj = classify_function = classify_coercion; discharge_function = discharge_coercion } -let declare_coercion coef stre ~isid ~src:cls ~target:clt ~params:ps = - Lib.add_anonymous_leaf (inCoercion (coef,stre,isid,cls,clt,ps)) +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 + 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) (* For printing purpose *) let get_coercion_value v = v.coe_value -let pr_cl_index n = int n +let pr_cl_index = Bijint.Index.print let classes () = Bijint.dom !class_tab -let coercions () = Gmap.rng !coercion_tab -let inheritance_graph () = Gmap.to_list !inheritance_graph +let coercions () = + List.rev (CoeTypMap.fold (fun _ y acc -> y::acc) !coercion_tab []) + +let inheritance_graph () = + ClPairMap.bindings !inheritance_graph let coercion_of_reference r = let ref = Nametab.global r in if not (coercion_exists ref) then errorlabstrm "try_add_coercion" - (Nametab.pr_global_env Idset.empty ref ++ str" is not a coercion."); + (Nametab.pr_global_env Id.Set.empty ref ++ str" is not a coercion."); ref module CoercionPrinting = struct type t = coe_typ + let compare = RefOrdered.compare let encode = coercion_of_reference let subst = subst_coe_typ - let printer x = pr_global_env Idset.empty x + let printer x = pr_global_env Id.Set.empty x let key = ["Printing";"Coercion"] let title = "Explicitly printed coercions: " let member_message x b = -- cgit v1.2.3