1 files changed, 397 insertions, 0 deletions
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     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: classops.ml,v 1.48.2.1 2004/07/16 19:30:44 herbelin Exp $ *)
+
+open Util
+open Pp
+open Options
+open Names
+open Libnames
+open Nametab
+open Environ
+open Libobject
+open Library
+open Term
+open Termops
+open Rawterm
+open Decl_kinds
+
+(* usage qque peu general: utilise aussi dans record *)
+
+(* A class is a type constructor, its type is an arity whose number of
+   arguments is cl_param (0 for CL_SORT and CL_FUN) *)
+
+type cl_typ = 
+  | CL_SORT 
+  | CL_FUN
+  | CL_SECVAR of variable
+  | CL_CONST of constant
+  | CL_IND of inductive
+
+type cl_info_typ = {
+  cl_strength : strength;
+  cl_param : int
+}
+
+type coe_typ = global_reference
+
+type coe_info_typ = {
+  coe_value : unsafe_judgment;
+  coe_strength : strength;
+  coe_is_identity : bool;
+  coe_param : int }
+
+type cl_index = int
+
+type coe_index = coe_info_typ
+
+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)))
+  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 replace n x y b =
+    let v = Array.copy b.v in v.(n) <- (x,y); { b with v = v }
+  let dom b = Gmap.dom b.inv
+end
+
+let class_tab =
+  ref (Bijint.empty : (cl_typ, cl_info_typ) Bijint.t)
+
+let coercion_tab =
+  ref (Gmap.empty : (coe_typ, coe_info_typ) Gmap.t)
+
+let inheritance_graph =
+  ref (Gmap.empty : (cl_index * cl_index, inheritance_path) Gmap.t)
+
+let freeze () = (!class_tab, !coercion_tab, !inheritance_graph)
+
+let unfreeze (fcl,fco,fig) = 
+  class_tab:=fcl;
+  coercion_tab:=fco;
+  inheritance_graph:=fig
+
+(* ajout de nouveaux "objets" *)
+
+let add_new_class cl s =
+  try
+    let n,s' = Bijint.revmap cl !class_tab in
+    if s.cl_strength = Global & s'.cl_strength <> 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 = <fun>
+ val outClass : Libobject.object -> (cl_typ * cl_info_typ) = <fun> *)
+
+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 "<a class path>"
+                        : (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