Moving centralised discharge into dispatched discharge_function; required to delay some computation from before to after caching time + various simplifications and uniformisations

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6748 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 217 insertions, 177 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 66ed81d02..6d49baf52 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -36,14 +36,14 @@ type cl_typ =
   | 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_value : constr;
+  coe_type : types;
   coe_strength : strength;
   coe_is_identity : bool;
   coe_param : int }
@@ -92,11 +92,7 @@ let unfreeze (fcl,fco,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 ->
+  if not (Bijint.mem cl !class_tab) then
     class_tab := Bijint.add cl s !class_tab
 
 let add_new_coercion coe s = 
@@ -107,11 +103,19 @@ let add_new_path x y =
 
 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 };
+  add_new_class CL_FUN  { cl_param = 0 };
+  add_new_class CL_SORT { cl_param = 0 };
   coercion_tab:= Gmap.empty;
   inheritance_graph:= Gmap.empty
 
+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 }
+
 let _ = init()
 
 (* class_info : cl_typ -> int * cl_info_typ *)
@@ -147,7 +151,7 @@ let lookup_pattern_path_between (s,t) =
     (fun coe ->
        let c, _ =
 	 Reductionops.whd_betadeltaiota_stack (Global.env()) Evd.empty 
-	   coe.coe_value.uj_val
+	   coe.coe_value
        in 
        match kind_of_term c with
 	 | Construct sp -> (sp, coe.coe_param)
@@ -183,44 +187,6 @@ let subst_cl_typ subst ct = match ct with
        to declare any term as a coercion *)
 let subst_coe_typ subst t = fst (subst_global subst t)
 
-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 *)
 
 (* class_of : Term.constr -> int *)
@@ -257,7 +223,8 @@ 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)
+let coercion_value { coe_value = c; coe_type = t; coe_is_identity = b } =
+  (make_judge c t, b)
 
 (* pretty-print functions are now in Pretty *)
 (* rajouter une coercion dans le graphe *)
@@ -322,49 +289,81 @@ let add_coercion_in_graph (ic,source,target) =
   if (!ambig_paths <> []) && is_verbose () then 
     ppnl (message_ambig !ambig_paths)
 
-type coercion = coe_typ * coe_info_typ * cl_typ * cl_typ
+type coercion = coe_typ * strength * bool * cl_typ * cl_typ * int
 
-let cache_coercion (_,(coe,xf,cls,clt)) =
+(* Calcul de l'arité d'une classe *)
+
+let reference_arity_length ref =
+  let t = Global.type_of_global ref in
+  List.length (fst (Reductionops.splay_arity (Global.env()) Evd.empty t))
+
+let class_params = function
+  | CL_FUN | CL_SORT -> 0
+  | CL_CONST sp -> reference_arity_length (ConstRef sp)
+  | CL_SECVAR sp -> reference_arity_length (VarRef sp)
+  | CL_IND sp  -> reference_arity_length (IndRef sp)
+
+(* add_class : cl_typ -> strength option -> bool -> unit *)
+
+let add_class cl =
+  add_new_class cl { cl_param = class_params cl }
+
+let load_coercion i (_,(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 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;
   add_coercion_in_graph (xf,is,it)
 
-let subst_coercion (_,subst,(coe,xf,cls,clt as obj)) =
+let cache_coercion o =
+  load_coercion 1 o
+
+let subst_coercion (_,subst,(coe,stre,isid,cls,clt,ps 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 *)
+    if coe' == coe && cls' == cls & clt' == clt then obj else
+      (coe',stre,isid,cls',clt',ps)
+
+let discharge_cl = function
+  | CL_CONST kn -> CL_CONST (Lib.discharge_con kn)
+  | CL_IND ind -> CL_IND (Lib.discharge_inductive ind)
+  | 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 (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))
+    load_function = load_coercion;
+    cache_function = cache_coercion;
+    subst_function = subst_coercion;
+    classify_function = (fun (_,x) -> Substitute x);
+    discharge_function = discharge_coercion;
+    export_function = (function x -> Some x)  }
+
+let declare_coercion coef stre ~isid ~src:cls ~target:clt ~params:ps =
+  Lib.add_anonymous_leaf (inCoercion (coef,stre,isid,cls,clt,ps))
 
 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 get_coercion_value v = v.coe_value
 
 let classes () = Bijint.dom !class_tab
 let coercions () = Gmap.rng !coercion_tab
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index c1590f6a8..dd51ee970 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -30,7 +30,6 @@ val subst_cl_typ : substitution -> cl_typ -> cl_typ
 
 (* This is the type of infos for declared classes *)
 type cl_info_typ = {
-  cl_strength : strength;
   cl_param : int }
 
 (* This is the type of coercion kinds *)
@@ -48,9 +47,6 @@ type coe_index
 (* This is the type of paths from a class to another *)
 type inheritance_path = coe_index list
 
-(*s [declare_class] adds a class to the set of declared classes *)
-val declare_class : cl_typ * strength * int -> unit
-
 (*s Access to classes infos *)
 val class_info : cl_typ -> (cl_index * cl_info_typ)
 val class_exists : cl_typ -> bool
@@ -70,7 +66,7 @@ val class_args_of : constr -> constr list
 
 (*s [declare_coercion] adds a coercion in the graph of coercion paths *)
 val declare_coercion : 
-  coe_typ -> unsafe_judgment -> strength -> isid:bool ->
+  coe_typ -> strength -> isid:bool ->
       src:cl_typ -> target:cl_typ -> params:int -> unit
 
 (*s Access to coercions infos *)
@@ -85,19 +81,6 @@ val lookup_path_to_sort_from : cl_index -> inheritance_path
 val lookup_pattern_path_between :
   cl_index * cl_index -> (constructor * int) list
 
-(*i Pour le discharge *)
-type coercion = coe_typ * coe_info_typ * cl_typ * cl_typ
-
-open Libobject
-val inClass : (cl_typ * cl_info_typ) -> Libobject.obj
-val outClass : Libobject.obj -> (cl_typ * cl_info_typ)
-val inCoercion : coercion -> Libobject.obj
-val outCoercion : Libobject.obj -> coercion
-val coercion_strength : coe_info_typ -> strength
-val coercion_identity : coe_info_typ -> bool
-val coercion_params : coe_info_typ -> int
-(*i*)
-
 (*i Crade *)
 open Pp
 val install_path_printer : 
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index cfccdb5e6..7f557d9b3 100755
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -21,17 +21,19 @@ open Library
 open Classops
 open Mod_subst
 
-(*s Une structure S est un type inductif non récursif à un seul
-   constructeur (de nom par défaut Build_S) *)
+(*s A structure S is a non recursive inductive type with a single
+   constructor (the name of which defaults to Build_S) *)
 
 (* Table des structures: le nom de la structure (un [inductive]) donne
    le nom du constructeur, le nombre de paramètres et pour chaque
-   argument réels du constructeur, le noms de la projection
-   correspondante, si valide *)
+   argument réel du constructeur, le nom de la projection
+   correspondante, si valide, et un booléen disant si c'est une vraie
+   projection ou bien une fonction constante (associée à un LetIn) *)
 
 type struc_typ = {
   s_CONST : identifier; 
   s_PARAM : int;
+  s_PROJKIND : bool list;
   s_PROJ : constant option list }
 
 let structure_table = ref (Indmap.empty : struc_typ Indmap.t)
@@ -39,121 +41,177 @@ let projection_table = ref Cmap.empty
 
 let option_fold_right f p e = match p with Some a -> f a e | None -> e
 
-let cache_structure (_,(ind,struc)) =
+let load_structure i (_,(ind,id,kl,projs)) =
+  let n = (snd (Global.lookup_inductive ind)).Declarations.mind_nparams in
+  let struc =
+    { s_CONST = id; s_PARAM = n; s_PROJ = projs; s_PROJKIND = kl } in
   structure_table := Indmap.add ind struc !structure_table;
   projection_table := 
     List.fold_right (option_fold_right (fun proj -> Cmap.add proj struc))
-      struc.s_PROJ !projection_table
+      projs !projection_table
 
-let subst_structure (_,subst,((kn,i),struc as obj)) = 
+let cache_structure o =
+  load_structure 1 o
+
+let subst_structure (_,subst,((kn,i),id,kl,projs as obj)) = 
   let kn' = subst_kn subst kn in
-  let proj' =
+  let projs' =
    (* invariant: struc.s_PROJ is an evaluable reference. Thus we can take *)
    (* the first component of subst_con.                                   *)
    list_smartmap 
-    (option_smartmap (fun kn -> fst (subst_con subst kn)))
-    struc.s_PROJ
+     (option_smartmap (fun kn -> fst (subst_con subst kn)))
+    projs
   in
-    if proj' == struc.s_PROJ && kn' == kn then obj else
-      (kn',i),{struc with s_PROJ = proj'}
+    if projs' == projs && kn' == kn then obj else
+      ((kn',i),id,kl,projs')
+
+let discharge_structure (_,(ind,id,kl,projs)) =
+  Some (Lib.discharge_inductive ind, id, kl,
+        List.map (option_app Lib.discharge_con) projs)
 
 let (inStruc,outStruc) =
   declare_object {(default_object "STRUCTURE") with 
-                    cache_function = cache_structure;
-		    load_function = (fun _ o -> cache_structure o);
-                    subst_function = subst_structure;
-		    classify_function = (fun (_,x) -> Substitute x);
-		    export_function = (function x -> Some x)  }
+    cache_function = cache_structure;
+    load_function = load_structure;
+    subst_function = subst_structure;
+    classify_function = (fun (_,x) -> Substitute x);
+    discharge_function = discharge_structure;
+    export_function = (function x -> Some x) }
 
-let add_new_struc (s,c,n,l) = 
-  Lib.add_anonymous_leaf (inStruc (s,{s_CONST=c;s_PARAM=n;s_PROJ=l}))
+let declare_structure (s,c,_,kl,pl) = 
+  Lib.add_anonymous_leaf (inStruc (s,c,kl,pl))
 
-let find_structure indsp = Indmap.find indsp !structure_table
+let lookup_structure indsp = Indmap.find indsp !structure_table
 
 let find_projection_nparams = function
   | ConstRef cst -> (Cmap.find cst !projection_table).s_PARAM
   | _ -> raise Not_found
 
-(*s Un "object" est une fonction construisant une instance d'une structure *)
+
+(************************************************************************)
+(*s A canonical structure declares "canonical" conversion hints between *)
+(*  the effective components of a structure and the projections of the  *)
+(*  structure *)
 
 (* Table des definitions "object" : pour chaque object c,
 
   c := [x1:B1]...[xk:Bk](Build_R a1...am t1...t_n)
 
-  avec ti = (ci ui1...uir)
+  If ti has the form (ci ui1...uir) where ci is a global reference and
+if the corresponding projection Li of the structure R is defined, one
+declare a "conversion" between ci and Li
+
+    x1:B1..xk:Bk |- (Li a1..am (c x1..xk)) =_conv (ci ui1...uir)
 
-  Pour tout ci, et Li, la ième projection de la structure R (si
-  définie), on déclare une "coercion"
+that maps the pair (Li,ci) to the following data
 
     o_DEF = c
     o_TABS = B1...Bk
     o_PARAMS = a1...am
     o_TCOMP = ui1...uir
+
 *)
 
 type obj_typ = {
   o_DEF : constr;
-  o_TABS : constr list;    (* dans l'ordre *)
-  o_TPARAMS : constr list; (* dans l'ordre *)
-  o_TCOMPS : constr list } (* dans l'ordre *)
-
-let subst_obj subst obj =
-  let o_DEF' = subst_mps subst obj.o_DEF in
-  let o_TABS' = list_smartmap (subst_mps subst) obj.o_TABS in    
-  let o_TPARAMS' = list_smartmap (subst_mps subst) obj.o_TPARAMS in 
-  let o_TCOMPS' = list_smartmap (subst_mps subst) obj.o_TCOMPS in 
-    if o_DEF' == obj.o_DEF
-      && o_TABS' == obj.o_TABS    
-      && o_TPARAMS' == obj.o_TPARAMS 
-      && o_TCOMPS' == obj.o_TCOMPS 
-    then 
-      obj
-    else
-      { o_DEF = o_DEF' ;
-	o_TABS = o_TABS' ;    
-	o_TPARAMS = o_TPARAMS' ; 
-	o_TCOMPS = o_TCOMPS' }
+  o_TABS : constr list;    (* ordered *)
+  o_TPARAMS : constr list; (* ordered *)
+  o_TCOMPS : constr list } (* ordered *)
 
 let object_table =
   (ref [] : ((global_reference * global_reference) * obj_typ) list ref)
 
-let canonical_structures () = !object_table
-
-let cache_canonical_structure (_,(cst,lo)) =
-  List.iter (fun (o,_ as x) ->
-    if not (List.mem_assoc o !object_table) then
-      object_table := x :: (!object_table)) lo
-
-let subst_object subst ((r1,r2),o as obj) = 
-  (* invariant: r1 and r2 are evaluable references. Thus subst_global   *)
-  (* cannot instantiate them. Hence we can use just the first component *)
-  (* of the answer.                                                     *)
-  let r1',_ = subst_global subst r1 in
-  let r2',_ = subst_global subst r2 in
-  let o' = subst_obj subst o in
-  if r1' == r1 && r2' == r2 && o' == o then obj
-  else (r1',r2'),o'
-
-let subst_canonical_structure (_,subst,(cst,lo as obj)) =
+let canonical_projections () = !object_table
+
+let keep_true_projections projs kinds =
+  map_succeed (function (p,true) -> p | _ -> failwith "")
+    (List.combine projs kinds)
+
+(* Intended to always success *)
+let compute_canonical_projections (con,ind) =
+  let v = mkConst con in
+  let c = Environ.constant_value (Global.env()) con in
+  let lt,t = Reductionops.splay_lambda (Global.env()) Evd.empty c in
+  let lt = List.rev (List.map snd lt) in
+  let args = snd (decompose_app t) in
+  let { s_PARAM = p; s_PROJ = lpj; s_PROJKIND = kl } = lookup_structure ind in
+  let params, projs = list_chop p args in
+  let lpj = keep_true_projections lpj kl in
+  let lps = List.combine lpj projs in
+  let comp =
+    List.fold_left
+      (fun l (spopt,t) -> (* comp=components *)
+	 match spopt with
+           | Some proji_sp ->
+	       let c, args = decompose_app t in
+	       (try (ConstRef proji_sp, reference_of_constr c, args) :: l
+                with Not_found -> l)
+	   | _ -> l)
+      [] lps in
+  List.map (fun (refi,c,argj) ->
+    (refi,c),{o_DEF=v; o_TABS=lt; o_TPARAMS=params; o_TCOMPS=argj})
+    comp
+
+let open_canonical_structure i (_,o) =
+  if i=1 then
+    let lo = compute_canonical_projections o in
+    List.iter (fun (o,_ as x) ->
+      if not (List.mem_assoc o !object_table) then
+	object_table := x :: (!object_table)) lo
+
+let cache_canonical_structure o =
+  open_canonical_structure 1 o
+
+let subst_canonical_structure (_,subst,(cst,ind as obj)) =
   (* invariant: cst is an evaluable reference. Thus we can take *)
   (* the first component of subst_con.                                   *)
   let cst' = fst (subst_con subst cst) in
-  let lo' = list_smartmap (subst_object subst) lo in
-  if cst' == cst & lo' == lo then obj else (cst',lo')
+  let ind' = Inductiveops.subst_inductive subst ind in
+  if cst' == cst & ind' == ind then obj else (cst',ind')
+
+let discharge_canonical_structure (_,(cst,ind)) =
+  Some (Lib.discharge_con cst,Lib.discharge_inductive ind)
 
 let (inCanonStruc,outCanonStruct) =
   declare_object {(default_object "CANONICAL-STRUCTURE") with 
-    open_function = (fun i o -> if i=1 then cache_canonical_structure o);
+    open_function = open_canonical_structure;
     cache_function = cache_canonical_structure;
     subst_function = subst_canonical_structure;
     classify_function = (fun (_,x) -> Substitute x);
+    discharge_function = discharge_canonical_structure;
     export_function = (function x -> Some x) }
 
 let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x)
 
+(*s High-level declaration of a canonical structure *)
+
+let error_not_structure ref =
+  errorlabstrm "object_declare"
+    (Nameops.pr_id (id_of_global ref) ++ str" is not a structure object")
+
+let check_and_decompose_canonical_structure ref =
+  let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref in
+  let env = Global.env () in
+  let vc = match Environ.constant_opt_value env sp with
+    | Some vc -> vc
+    | None -> error_not_structure ref in
+  let f,args = match kind_of_term (snd (decompose_lam vc)) with
+    | App (f,args) -> f,args
+    | _ -> error_not_structure ref in
+  let indsp = match kind_of_term f with
+    | Construct (indsp,1) -> indsp
+    | _ -> error_not_structure ref in
+  let s = try lookup_structure indsp with Not_found -> error_not_structure ref in
+  if s.s_PARAM + List.length s.s_PROJ > Array.length args then
+    error_not_structure ref;
+  (sp,indsp)
+
+let declare_canonical_structure ref =
+  add_canonical_structure (check_and_decompose_canonical_structure ref)
+
 let outCanonicalStructure x = fst (outCanonStruct x)
 
-let canonical_structure_info o = List.assoc o !object_table
+let lookup_canonical_conversion o = List.assoc o !object_table
 
 let freeze () =
   !structure_table, !projection_table, !object_table
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 7402f74c9..d6f90e11e 100755
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -18,36 +18,36 @@ open Libobject
 open Library
 (*i*)
 
+(*s A structure S is a non recursive inductive type with a single
+   constructor (the name of which defaults to Build_S) *)
+
 type struc_typ = {
   s_CONST : identifier; 
   s_PARAM : int;
+  s_PROJKIND : bool list;
   s_PROJ : constant option list }
 
-val add_new_struc : 
-  inductive * identifier * int * constant option list -> unit
+val declare_structure : 
+  inductive * identifier * int * bool list * constant option list -> unit
 
-(* [find_structure isp] returns the infos associated to inductive path
+(* [lookup_structure isp] returns the infos associated to inductive path
    [isp] if it corresponds to a structure, otherwise fails with [Not_found] *)
-val find_structure : inductive -> struc_typ
+val lookup_structure : inductive -> struc_typ
 
 (* raise [Not_found] if not a projection *)
 val find_projection_nparams : global_reference -> int
 
+(*s A canonical structure declares "canonical" conversion hints between *)
+(*  the effective components of a structure and the projections of the  *)
+(*  structure *)
+
 type obj_typ = {
   o_DEF : constr;
-  o_TABS : constr list; (* dans l'ordre *)
-  o_TPARAMS : constr list; (* dans l'ordre *)
-  o_TCOMPS : constr list } (* dans l'ordre *)
+  o_TABS : constr list;    (* ordered *)
+  o_TPARAMS : constr list; (* ordered *)
+  o_TCOMPS : constr list } (* ordered *)
                
-val canonical_structure_info : 
-  (global_reference * global_reference) -> obj_typ
-val add_canonical_structure : 
-  constant * ((global_reference * global_reference) * obj_typ) list -> unit
-
-val inStruc : inductive * struc_typ -> obj
-val outStruc : obj -> inductive * struc_typ
-
-val outCanonicalStructure : obj -> constant
-
-val canonical_structures : unit -> 
+val lookup_canonical_conversion : (global_reference * global_reference) -> obj_typ
+val declare_canonical_structure : global_reference -> unit
+val canonical_projections : unit -> 
   ((global_reference * global_reference) * obj_typ) list