snapshot for CSC

[helm.git] / helm / software / components / ng_refiner / nCicCoercion.ml

diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml
index e48e772079b86ef6d0d0eb8fafc9fca6706b3852..18540dcda060c1551341ebcd3ed403f9fc60213a 100644 (file)
--- a/helm/software/components/ng_refiner/nCicCoercion.ml
+++ b/helm/software/components/ng_refiner/nCicCoercion.ml
@@ -14,9 +14,10 @@
 let debug s = prerr_endline (Lazy.force s);;
 let debug _ = ();;
 
-module COT : Set.OrderedType with type t = NCic.term * int * int = 
+module COT : Set.OrderedType with type t = NCic.term * int * int  * NCic.term *
+NCic.term = 
   struct
-        type t = NCic.term * int * int
+        type t = NCic.term * int * int * NCic.term * NCic.term
         let compare = Pervasives.compare
   end
 
@@ -31,18 +32,21 @@ let empty_db = DB.empty,DB.empty
 
 class status =
  object
+  inherit NCicUnifHint.status
   val db = empty_db
   method coerc_db = db
   method set_coerc_db v = {< db = v >}
   method set_coercion_status
-   : 'status. < coerc_db : db; .. > as 'status -> 'self
-   = fun o -> {< db = o#coerc_db >}
+  : 'status. < coerc_db : db; uhint_db: NCicUnifHint.db; .. > as 'status -> 
+          'self
+          = fun o -> {< db = o#coerc_db >}#set_unifhint_status o
  end
 
 let index_coercion status c src tgt arity arg =
   let db_src,db_tgt = status#coerc_db in
-  let data = (c,arity,arg) in
+  let data = (c,arity,arg,src,tgt) in
 
+  let debug s = prerr_endline (Lazy.force s) in
   debug (lazy ("INDEX:" ^ 
     NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^
     NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^ "  :=  " ^
@@ -103,17 +107,30 @@ let look_for_coercion status metasenv subst context infty expty =
       NCicPp.ppterm ~metasenv ~subst ~context infty ^ "  |===> " ^
       NCicPp.ppterm ~metasenv ~subst ~context expty));
 
-    let set_src = DB.retrieve_unifiables db_src infty in
-    let set_tgt = DB.retrieve_unifiables db_tgt expty in
+    let src_class = infty :: NCicUnifHint.eq_class_of status infty in
+    let tgt_class = expty :: NCicUnifHint.eq_class_of status expty in
+
+    let set_src = 
+      List.fold_left 
+        (fun set infty -> 
+          CoercionSet.union (DB.retrieve_unifiables db_src infty) set)
+        CoercionSet.empty src_class
+    in
+    let set_tgt = 
+      List.fold_left 
+        (fun set expty -> 
+          CoercionSet.union (DB.retrieve_unifiables db_tgt expty) set)
+        CoercionSet.empty tgt_class
+    in
     let candidates = CoercionSet.inter set_src set_tgt in
 
     debug (lazy ("CANDIDATES: " ^ 
-      String.concat "," (List.map (fun (t,_,_) ->
+      String.concat "," (List.map (fun (t,_,_,_,_) ->
         NCicPp.ppterm ~metasenv ~subst ~context t) 
       (CoercionSet.elements candidates))));
 
     List.map
-      (fun (t,arity,arg) ->
+      (fun (t,arity,arg,_,_) ->
           let ty =
             try NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] t 
             with NCicTypeChecker.TypeCheckerFailure s ->
@@ -142,7 +159,7 @@ let match_coercion status ~metasenv ~subst ~context t =
   DB.fold (fst (status#coerc_db)) (fun _ v l -> (CoercionSet.elements v)@l) []
  in
     (HExtlib.list_findopt
-      (fun (p,arity,cpos) _ ->
+      (fun (p,arity,cpos,_,_) _ ->
         try
          let t =
           match p,t with
@@ -165,3 +182,63 @@ let match_coercion status ~metasenv ~subst ~context t =
          Failure _ -> None (* raised by split_nth *)
       ) db)
 ;;
+
+let generate_dot_file status =
+  let module Pp = GraphvizPp.Dot in
+  let buf = Buffer.create 10240 in
+  let fmt = Format.formatter_of_buffer buf in
+  Pp.header ~node_attrs:["fontsize", "9"; "width", ".4"; "height", ".4"]
+    ~edge_attrs:["fontsize", "10"] fmt;
+  let src_db, _ = status#coerc_db in
+  let edges = ref [] in
+  DB.iter src_db (fun _ dataset -> 
+     edges := !edges @ 
+      List.map
+        (fun (t,a,g,sk,dk) -> 
+                prerr_endline (let p = NCicPp.ppterm ~metasenv:[] ~context:[]
+                ~subst:[] in p t ^ " ::: " ^ p sk ^ " |--> " ^ p dk);
+          let eq_s=List.sort compare (sk::NCicUnifHint.eq_class_of status sk) in
+          let eq_t=List.sort compare (dk::NCicUnifHint.eq_class_of status dk) in
+          (t,a,g),eq_s,eq_t
+          )
+        (CoercionSet.elements dataset);
+    );
+  let nodes = 
+    HExtlib.list_uniq
+     (List.sort compare 
+       (List.flatten
+         (List.map
+           (fun (_,a,b) ->
+             [a;b]
+            )
+           !edges)))
+  in
+  let names = ref [] in
+  let id = ref 0 in
+  let mangle l =
+    try List.assoc l !names
+    with Not_found ->
+      incr id;
+      names := (l,"node"^string_of_int!id) :: !names;
+      List.assoc l !names
+  in
+  List.iter 
+    (fun cl -> 
+      Pp.node (mangle cl) 
+      ~attrs:["label",String.concat "\\n"
+        (List.map (fun t->
+          NCicPp.ppterm ~metasenv:[] ~subst:[]
+           ~context:[] t ~margin:max_int
+        ) cl)]
+      fmt)
+    nodes;
+  List.iter 
+    (fun ((t,a,b),src,tgt) ->
+       Pp.edge (mangle src) (mangle tgt)
+         ~attrs:["label",
+           NCicPp.ppterm ~metasenv:[]
+           ~subst:[] ~context:[] t] fmt)
+    !edges;
+  Pp.trailer fmt;
+  Buffer.contents buf
+;;