From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Wed, 28 Jul 2004 21:54:47 +0000 Subject: Imported Upstream version 8.0pl1 --- pretyping/classops.ml | 397 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 397 insertions(+) create mode 100755 pretyping/classops.ml (limited to 'pretyping/classops.ml') diff --git a/pretyping/classops.ml b/pretyping/classops.ml new file mode 100755 index 00000000..2d8fb951 --- /dev/null +++ b/pretyping/classops.ml @@ -0,0 +1,397 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Global then + class_tab := Bijint.replace n cl s !class_tab + with Not_found -> + class_tab := Bijint.add cl s !class_tab + +let add_new_coercion coe s = + coercion_tab := Gmap.add coe s !coercion_tab + +let add_new_path x y = + inheritance_graph := Gmap.add x y !inheritance_graph + +let init () = + class_tab:= Bijint.empty; + add_new_class CL_FUN { cl_param = 0; cl_strength = Global }; + add_new_class CL_SORT { cl_param = 0; cl_strength = Global }; + coercion_tab:= Gmap.empty; + inheritance_graph:= Gmap.empty + +let _ = init() + +(* class_info : cl_typ -> int * cl_info_typ *) + +let class_info cl = Bijint.revmap cl !class_tab + +let class_exists cl = Bijint.mem cl !class_tab + +(* class_info_from_index : int -> cl_typ * cl_info_typ *) + +let class_info_from_index i = Bijint.map i !class_tab + +(* coercion_info : coe_typ -> coe_info_typ *) + +let coercion_info coe = Gmap.find coe !coercion_tab + +let coercion_exists coe = Gmap.mem coe !coercion_tab + +let coercion_params coe_info = coe_info.coe_param + +let lookup_path_between (s,t) = + Gmap.find (s,t) !inheritance_graph + +let lookup_path_to_fun_from s = + lookup_path_between (s,fst(class_info CL_FUN)) + +let lookup_path_to_sort_from s = + lookup_path_between (s,fst(class_info CL_SORT)) + +let lookup_pattern_path_between (s,t) = + let l = Gmap.find (s,t) !inheritance_graph in + List.map + (fun coe -> + let c, _ = + Reductionops.whd_betadeltaiota_stack (Global.env()) Evd.empty + coe.coe_value.uj_val + in + match kind_of_term c with + | Construct sp -> (sp, coe.coe_param) + | _ -> raise Not_found) l + + +let subst_cl_typ subst ct = match ct with + CL_SORT + | CL_FUN + | CL_SECVAR _ -> ct + | CL_CONST kn -> + let kn' = subst_kn subst kn in + if kn' == kn then ct else + CL_CONST kn' + | CL_IND (kn,i) -> + let kn' = subst_kn subst kn in + if kn' == kn then ct else + CL_IND (kn',i) + +let subst_coe_typ = subst_global + +let subst_coe_info subst info = + let jud = info.coe_value in + let val' = subst_mps subst (j_val jud) in + let type' = subst_mps subst (j_type jud) in + if val' == j_val jud && type' == j_type jud then info else + {info with coe_value = make_judge val' type'} + +(* library, summary *) + +(*val inClass : (cl_typ * cl_info_typ) -> Libobject.object = + val outClass : Libobject.object -> (cl_typ * cl_info_typ) = *) + +let cache_class (_,(x,y)) = add_new_class x y + +let subst_class (_,subst,(ct,ci as obj)) = + let ct' = subst_cl_typ subst ct in + if ct' == ct then obj else + (ct',ci) + +let (inClass,outClass) = + declare_object {(default_object "CLASS") with + load_function = (fun _ o -> cache_class o); + cache_function = cache_class; + subst_function = subst_class; + classify_function = (fun (_,x) -> Substitute x); + export_function = (function x -> Some x) } + +let declare_class (cl,stre,p) = + Lib.add_anonymous_leaf (inClass ((cl,{ cl_strength = stre; cl_param = p }))) + +let _ = + Summary.declare_summary "inh_graph" + { Summary.freeze_function = freeze; + Summary.unfreeze_function = unfreeze; + Summary.init_function = init; + Summary.survive_module = false; + Summary.survive_section = false } + +(* classe d'un terme *) + +(* find_class_type : constr -> cl_typ * int *) + +let find_class_type t = + let t', args = decompose_app (Reductionops.whd_betaiotazeta 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, [] + | _ -> raise Not_found + +(* class_of : Term.constr -> int *) + +let class_of env sigma t = + let (t, n1, i, args) = + try + let (cl,args) = find_class_type t in + let (i, { cl_param = n1 } ) = class_info cl in + (t, n1, i, args) + with Not_found -> + let t = Tacred.hnf_constr env sigma t in + let (cl, args) = find_class_type t in + let (i, { cl_param = n1 } ) = class_info cl in + (t, n1, i, args) + in + if 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 c = snd (decompose_app c) + +let string_of_class = function + | CL_FUN -> if !Options.v7 then "FUNCLASS" else "Funclass" + | CL_SORT -> if !Options.v7 then "SORTCLASS" else "Sortclass" + | CL_CONST sp -> + string_of_qualid (shortest_qualid_of_global Idset.empty (ConstRef sp)) + | CL_IND sp -> + string_of_qualid (shortest_qualid_of_global Idset.empty (IndRef sp)) + | CL_SECVAR sp -> + string_of_qualid (shortest_qualid_of_global Idset.empty (VarRef sp)) + +let pr_class x = str (string_of_class x) + +(* coercion_value : coe_index -> unsafe_judgment * bool *) + +let coercion_value { coe_value = j; coe_is_identity = b } = (j,b) + +(* 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) + +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 pr_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 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 + let _ = lookup_path_between ij in + ambig_paths := (ij,p)::!ambig_paths + end + end else begin + let _ = lookup_path_between (i,j) in + ambig_paths := (ij,p)::!ambig_paths + end; + 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 () + in + if try_add_new_path (source,target) [ic] then begin + Gmap.iter + (fun (s,t) p -> + if s<>t then begin + if t = source then begin + try_add_new_path1 (s,target) (p@[ic]); + Gmap.iter + (fun (u,v) q -> + if u<>v & (u = target) & (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) + end) + old_inheritance_graph + end; + if (!ambig_paths <> []) && is_verbose () then + ppnl (message_ambig !ambig_paths) + +type coercion = coe_typ * coe_info_typ * cl_typ * cl_typ + +let cache_coercion (_,(coe,xf,cls,clt)) = + let is,_ = class_info cls in + let it,_ = class_info clt in + add_new_coercion coe xf; + add_coercion_in_graph (xf,is,it) + +let subst_coercion (_,subst,(coe,xf,cls,clt as obj)) = + let coe' = subst_coe_typ subst coe in + let xf' = subst_coe_info subst xf in + let cls' = subst_cl_typ subst cls in + let clt' = subst_cl_typ subst clt in + if coe' == coe && xf' == xf && cls' == cls & clt' == clt then obj else + (coe',xf',cls',clt') + + +(* val inCoercion : coercion -> Libobject.object + val outCoercion : Libobject.object -> coercion *) + +let (inCoercion,outCoercion) = + declare_object {(default_object "COERCION") with + load_function = (fun _ o -> cache_coercion o); + cache_function = cache_coercion; + subst_function = subst_coercion; + classify_function = (fun (_,x) -> Substitute x); + export_function = (function x -> Some x) } + +let declare_coercion coef v stre ~isid ~src:cls ~target:clt ~params:ps = + Lib.add_anonymous_leaf + (inCoercion + (coef, + { coe_value = v; + coe_strength = stre; + coe_is_identity = isid; + coe_param = ps }, + cls, clt)) + +let coercion_strength v = v.coe_strength +let coercion_identity v = v.coe_is_identity + +(* For printing purpose *) +let get_coercion_value v = v.coe_value.uj_val + +let classes () = Bijint.dom !class_tab +let coercions () = Gmap.rng !coercion_tab +let inheritance_graph () = Gmap.to_list !inheritance_graph + +let coercion_of_qualid qid = + let ref = Nametab.global qid in + if not (coercion_exists ref) then + errorlabstrm "try_add_coercion" + (Nametab.pr_global_env Idset.empty ref ++ str" is not a coercion"); + ref + +module CoercionPrinting = + struct + type t = coe_typ + let encode = coercion_of_qualid + let subst = subst_coe_typ + let printer x = pr_global_env Idset.empty x + let key = Goptions.SecondaryTable ("Printing","Coercion") + let title = "Explicitly printed coercions: " + 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) + +let hide_coercion coe = + if not (PrintingCoercion.active coe) then + let coe_info = coercion_info coe in + Some coe_info.coe_param + else None -- cgit v1.2.3