Versions initiales

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

1 files changed, 392 insertions, 0 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
new file mode 100755
index 0000000000..667adca1b1
--- /dev/null
+++ b/pretyping/classops.ml
@@ -0,0 +1,392 @@
+
+
+open Std;;
+open Names;;
+open Vectops;;
+open Pp;;
+open Vartab;;
+open Libobject;;
+open Constrtypes;;
+open Vectops;;
+open List;;
+open Library;;
+open Term;;
+open More_util;;
+open Generic;;
+open Initial;;
+open Printer;;
+
+
+(* usage qque peu general: utilise aussi dans record *)
+
+type cte_typ = NAM_Var of identifier | NAM_SP of section_path | NAM_Construct of section_path*int*int
+;;
+
+let cte_of_constr = function  
+    (DOPN(Const sp,l)) -> NAM_SP sp
+  | (DOPN(MutInd (sp,_),l)) -> NAM_SP sp
+  | (VAR(id)) -> NAM_Var id
+  | (DOPN(MutConstruct ((sp,i),j) ,l)) -> NAM_Construct (sp,i,j)
+  |  _ -> raise Not_found
+;;
+
+type cl_typ = CL_SORT | CL_FUN | CL_Var of identifier | CL_SP of section_path 
+            | CL_IND of section_path*int
+;;
+
+type cl_info_typ = {cL_STR : string;
+                    cL_STRE : strength;
+                    cL_PARAM : int}
+;;
+
+type coe_typ = cte_typ
+;;
+
+type coe_info_typ = {cOE_VALUE : judgement;
+                     cOE_STRE : strength;
+                     cOE_ISID : bool;
+                     cOE_PARAM : int}
+;;
+
+type inheritance_path = int list
+;;
+
+(* table des classes, des coercions et graphe d'heritage *)
+
+let cLASSES = (ref [] : (int * (cl_typ * cl_info_typ)) list ref);;
+
+let cOERCIONS = (ref [] : (int * (coe_typ * coe_info_typ)) list ref);;
+
+let iNHERITANCE_GRAPH = (ref [] : ((int * int) * inheritance_path) list ref);; 
+
+let freeze () = (!cLASSES,!cOERCIONS,
+                 !iNHERITANCE_GRAPH)
+;;
+
+let unfreeze (fcl,fco,fig) = (cLASSES:=fcl;
+                              cOERCIONS:=fco;
+                              iNHERITANCE_GRAPH:=fig)
+;;
+
+(* ajout de nouveaux "objets" *)
+
+let newNum_class = 
+ let num = ref 0 in
+ function () -> (num:=!num+1;!num)
+;;
+
+let newNum_coercion = 
+ let num = ref 0 in
+ function () -> (num:=!num+1;!num)
+;;
+
+let add_new_class_num (n,(cl,s)) = 
+cLASSES := (n,(cl,s))::(!cLASSES)
+;;
+
+let add_new_class1 (cl,s) = 
+add_new_class_num (newNum_class(),(cl,s))
+;;
+
+let add_new_coercion_num (n,(coe,s)) = 
+cOERCIONS := (n,(coe,s))::(!cOERCIONS)
+;;
+
+let add_new_coercion (coe,s) = 
+let n = newNum_coercion() in 
+add_new_coercion_num (n,(coe,s));n
+;;
+
+let add_new_path x =
+iNHERITANCE_GRAPH := x::(!iNHERITANCE_GRAPH)
+;;
+
+let init () = (cLASSES:= []; 
+               add_new_class1 (CL_FUN,{cL_STR="FUNCLASS";cL_PARAM=0;cL_STRE=NeverDischarge});
+               add_new_class1 (CL_SORT,{cL_STR="SORTCLASS";cL_PARAM=0;cL_STRE=NeverDischarge});
+               cOERCIONS:= [];
+               iNHERITANCE_GRAPH:= [])
+;;
+
+init();;
+
+(* fonction de recherche *)
+
+let search_info x l = 
+let rec aux = function [] -> raise Not_found
+                     | (n,(x1,r))::l -> if x=x1 then (n,r)
+                                        else aux l
+in aux l
+;;
+
+(* class_info : cl_typ -> int * cl_info_typ *)
+
+let class_info cl = search_info cl (!cLASSES)
+;;
+
+(* class_info_from_index : int -> cl_typ * cl_info_typ *)
+
+let class_info_from_index i = List.assoc i (!cLASSES)
+;;
+
+(* coercion_info : coe_typ -> int * coe_info_typ *)
+
+let coercion_info coe = search_info coe (!cOERCIONS)
+;;
+
+(* coercion_info_from_index : int -> coe_typ * coe_info_typ *)
+
+let coercion_info_from_index i = List.assoc i (!cOERCIONS)
+;;
+
+let lookup_path_between (s,t) = List.assoc (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))
+;;
+
+
+(* library, summary *)
+
+(*val inClass : (cl_typ * cl_info_typ) -> Libobject.object = <fun>
+ val outClass : Libobject.object -> (cl_typ * cl_info_typ) = <fun> *)
+
+let (inClass,outClass) =
+    declare_object ("CLASS",
+                    {load_function = (fun _ -> ());
+                     cache_function = (function  (_,x) -> add_new_class1 x);
+                     specification_function = (function x -> x)});;
+
+let add_new_class (cl,s,stre,p) = 
+add_anonymous_object (inClass ((cl,{cL_STR=s;cL_STRE=stre;cL_PARAM=p})))
+;;
+
+Library.declare_summary "inh_graph"
+{Summary.freeze_function = freeze;
+ Summary.unfreeze_function = unfreeze;
+ Summary.init_function = init}
+;;
+
+(* classe d'un terme *)
+
+(* constructor_at_head : constr -> cl_typ * int *)
+
+let constructor_at_head t = 
+let rec aux t' = match t' with
+    (DOPN(Const sp,_)) -> CL_SP sp,0
+  | (DOPN(MutInd (sp,i),_)) -> CL_IND (sp,i),0
+  | (VAR(id)) -> CL_Var id,0
+  | (DOP2(Cast,c,_)) -> aux (collapse_appl c)
+  | (DOPN(AppL,cl)) -> let c,_ = aux (hd_vect cl) 
+                        in c,Array.length(cl)-1
+  | DOP2(Prod,_,DLAM(_,c)) -> CL_FUN,0
+  | DOP0(Sort(_)) -> CL_SORT,0
+  |  _ -> raise Not_found
+in aux (collapse_appl t)
+;;
+
+(* class_of : Term.constr -> int *)
+
+
+let class_of sigma t = 
+let t,n,n1,i = (try let (cl,n) = constructor_at_head t in
+               let (i,{cL_PARAM=n1}) = class_info cl in
+               t,n,n1,i              
+              with _ -> let t = Reduction.hnf_constr sigma t in
+                        let (cl,n) = constructor_at_head t in
+                        let (i,{cL_PARAM=n1}) = class_info cl in
+                        t,n,n1,i) in
+if n = n1 then t,i 
+else raise Not_found
+;;
+
+(*
+
+let class_of t = 
+let (cl,n) = constructor_at_head t in
+let (i,{cL_PARAM=n1}) = class_info cl in
+if n = n1 then i 
+else raise Not_found
+;;
+*)
+
+let rec class_args_of c = 
+let aux = function (DOP2(Cast,c,_)) -> class_args_of c
+                 | (DOPN(AppL,cl)) -> Array.to_list(tl_vect(cl))
+                 | _ -> []
+in aux (collapse_appl c)
+;;
+
+(* verfications pour l'ajout d'une classe *)
+
+let fully_applied id p p1 =
+if p <> p1
+then  errorlabstrm "fully_applied" 
+          [< 'sTR"Wrong number of parameters for ";'sTR(string_of_id id) >]
+;;
+
+let rec arity_sort = function
+    DOP0(Sort(Prop(_))) -> 0
+  | DOP0(Sort(Type(_))) -> 0
+  | DOP2(Prod,_,DLAM(_,c)) -> (arity_sort c) +1
+  | DOP2(Cast,c,_) -> arity_sort c
+  | _ -> raise Not_found
+;;
+
+let stre_of_cl = 
+  function CL_SP sp ->
+                    (match Lib.leaf_object_tag (objsp_of sp) with
+                      "CONSTANT" ->
+                       let (_,stre,_) = Environ.outConstant(Lib.map_leaf (objsp_of sp)) in stre
+                      | _ -> NeverDischarge)
+          | CL_Var id -> stre_of_var id
+          | _ -> NeverDischarge
+;;
+
+(* coe_value : int -> Term.constr * bool *)
+
+let coe_value i = 
+let (_,{cOE_VALUE=v;cOE_ISID=b}) = coercion_info_from_index i in
+v,b
+;;
+
+(* fonction de print *)
+
+let string_of_strength = function NeverDischarge -> "(global)"
+                                | DischargeAt sp -> "(disch@"^(string_of_path sp)
+;;
+
+let print_coercion_value v = (prterm v.cOE_VALUE._VAL);;
+
+let print_index_coercion c = 
+ let _,v = coercion_info_from_index c in
+ print_coercion_value v;;
+
+(*
+let string_of_cl = function CL_Var id -> string_of_id id
+                          | CL_SP sp -> string_of_id (basename sp)
+                          | CL_IND (sp,i,s) -> s
+                          | CL_FUN -> "FUNCLASS"
+                          | CL_SORT -> "SORTCLASS";;
+*)
+
+let print_class i =
+ let cl,x = class_info_from_index i in
+ [< 'sTR x.cL_STR >];;
+
+let print_path ((i,j),p) = [< 'sTR"["; 
+                                   prlist_with_sep (fun () -> [< 'sTR"; " >])
+                                   (fun c ->  print_index_coercion c) p;
+                                   'sTR"] : "; print_class i; 'sTR" >-> ";
+                                   print_class j >];;
+
+let print_graph () = 
+  [< prlist_with_sep pr_fnl print_path (!iNHERITANCE_GRAPH) >];;
+
+let print_classes () = 
+  [< prlist_with_sep pr_spc
+     (fun (_,(cl,x)) -> 
+        [< 'sTR x.cL_STR  (*; 'sTR(string_of_strength x.cL_STRE) *) >]) 
+        (!cLASSES) >];;
+
+let print_coercions () = 
+  [< prlist_with_sep pr_spc
+     (fun (_,(_,v)) -> [< (print_coercion_value v)
+              (* ;'sTR(string_of_strength v.cOE_STRE)*) >]) (!cOERCIONS) >];;
+
+let cl_of_id id = 
+match (string_of_id id) with
+ "FUNCLASS" -> CL_FUN
+| "SORTCLASS" -> CL_SORT
+| _ -> let v = Machops.global (gLOB(initial_sign())) id in
+       let cl,_ = constructor_at_head v in cl
+;;
+
+let index_cl_of_id id =
+try let cl = cl_of_id id in
+    let i,_=class_info cl in i
+with _ -> errorlabstrm "index_cl_of_id"
+          [< 'sTR(string_of_id id); 'sTR" is not a defined class" >]
+;;
+
+let print_path_between ids idt = 
+let i = (index_cl_of_id ids) in
+let j = (index_cl_of_id idt) in
+let p = (try lookup_path_between (i,j) 
+         with _ -> errorlabstrm "index_cl_of_id"
+           [< 'sTR"No path between ";'sTR(string_of_id ids); 'sTR" and ";'sTR(string_of_id ids) >]) in
+print_path ((i,j),p);;
+
+(* rajouter une coercion dans le graphe *)
+ 
+let message_ambig l =
+    [< 'sTR"Ambiguous paths : ";
+       prlist_with_sep pr_fnl (fun ijp -> print_path ijp) l >];;
+
+(* add_coercion_in_graph : int * int * int -> unit 
+                         coercion,source,target *)
+
+let add_coercion_in_graph (ic,source,target) =
+let old_iNHERITANCE_GRAPH = (!iNHERITANCE_GRAPH) in
+let ambig_paths = (ref []:((int * int) * inheritance_path) list ref) in
+
+let try_add_new_path (p,i,j) =
+    try (if i=j 
+         then (if (snd (class_info_from_index i)).cL_PARAM > 0
+               then (lookup_path_between (i,j);
+                     ambig_paths := ((i,j),p)::!ambig_paths))
+         else
+          (lookup_path_between (i,j);
+          ambig_paths := ((i,j),p)::!ambig_paths);false)
+    with Not_found -> (add_new_path ((i,j),p);true)
+in
+let try_add_new_path1 (p,i,j) = (try_add_new_path (p,i,j);())
+in
+        (if try_add_new_path ([ic],source,target)
+           then 
+             (iter (fun ((s,t),p) ->
+                if s<>t 
+                then ((if (t = source)
+                       then begin
+                            try_add_new_path1 (p @ [ ic ],s,target);
+                            (iter (fun ((u,v),q) ->
+                                    if u<>v 
+                                    then if (u = target) & (p <> q)
+                                         then try_add_new_path1 (p @ [ ic ] @ q,s,v))
+                                              old_iNHERITANCE_GRAPH)
+                            end);
+                       if (s = target)
+                       then try_add_new_path1 (ic::p,source,t)))
+                 old_iNHERITANCE_GRAPH);
+
+if ((!ambig_paths) <> []) & is_mes_ambig()
+then pPNL (message_ambig (!ambig_paths)))
+;;
+
+
+let add_new_coercion_in_graph ((coef,xf),cls,clt) =
+let is,_ = class_info cls in
+let it,_ = class_info clt in
+let jf = add_new_coercion (coef,xf) in
+add_coercion_in_graph (jf,is,it)
+;;
+
+
+
+
+
+(* val inCoercion : (coe_typ * coe_info_typ) * cl_typ * cl_typ  ->
+                    -> Libobject.object 
+   val outCoercion : Libobject.object -> (coe_typ * coe_info_typ) 
+                         * cl_typ * cl_typ *)
+
+let (inCoercion,outCoercion) =
+    declare_object ("COERCION",
+                    {load_function = (fun _ -> ());
+                     cache_function =
+                       (function  (_,x) -> add_new_coercion_in_graph x);
+                     specification_function = (function x -> x)});;
+
+