the refiner was not checking that the resulting type

[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 18540dcda060c1551341ebcd3ed403f9fc60213a..037c5c6e2ce6b80f23e4bbacfe2f0471162e1b8b 100644 (file)
--- a/helm/software/components/ng_refiner/nCicCoercion.ml
+++ b/helm/software/components/ng_refiner/nCicCoercion.ml
@@ -14,11 +14,12 @@
 let debug s = prerr_endline (Lazy.force s);;
 let debug _ = ();;
 
-module COT : Set.OrderedType with type t = NCic.term * int * int  * NCic.term *
+module COT : Set.OrderedType 
+with type t = string * NCic.term * int * int  * NCic.term *
 NCic.term = 
   struct
-        type t = NCic.term * int * int * NCic.term * NCic.term
-        let compare = Pervasives.compare
+     type t = string * NCic.term * int * int * NCic.term * NCic.term
+     let compare = Pervasives.compare
   end
 
 module CoercionSet = Set.Make(COT)
@@ -42,11 +43,10 @@ class status =
           = fun o -> {< db = o#coerc_db >}#set_unifhint_status o
  end
 
-let index_coercion status c src tgt arity arg =
+let index_coercion status name c src tgt arity arg =
   let db_src,db_tgt = status#coerc_db in
-  let data = (c,arity,arg,src,tgt) in
+  let data = (name,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 ^ "  :=  " ^
@@ -88,7 +88,7 @@ let index_old_db odb (status : #status) =
                     NCicPp.ppterm ~metasenv ~subst:[] ~context:[] t));
                   assert false
             in
-            index_coercion status c src tgt arity arg
+            index_coercion status "foo" c src tgt arity arg
            with 
            | NCicEnvironment.BadDependency _ 
            | NCicTypeChecker.TypeCheckerFailure _ -> status)
@@ -98,10 +98,13 @@ let index_old_db odb (status : #status) =
 
 let look_for_coercion status metasenv subst context infty expty =
  let db_src,db_tgt = status#coerc_db in
-  match infty, expty with
+  match 
+    NCicUntrusted.apply_subst subst context infty, 
+    NCicUntrusted.apply_subst subst context expty 
+  with
   | (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)), 
     (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)) -> [] 
-  | _ ->
+  | infty, expty ->
 
     debug (lazy ("LOOK FOR COERCIONS: " ^ 
       NCicPp.ppterm ~metasenv ~subst ~context infty ^ "  |===> " ^
@@ -122,15 +125,25 @@ let look_for_coercion status metasenv subst context infty expty =
           CoercionSet.union (DB.retrieve_unifiables db_tgt expty) set)
         CoercionSet.empty tgt_class
     in
+
+    debug (lazy ("CANDIDATES SRC: " ^ 
+      String.concat "," (List.map (fun (name,t,_,_,_,_) ->
+        name ^ " :: " ^ NCicPp.ppterm ~metasenv ~subst ~context t) 
+      (CoercionSet.elements set_src))));
+    debug (lazy ("CANDIDATES TGT: " ^ 
+      String.concat "," (List.map (fun (name,t,_,_,_,_) ->
+        name ^ " :: " ^ NCicPp.ppterm ~metasenv ~subst ~context t) 
+      (CoercionSet.elements set_tgt))));
+
     let candidates = CoercionSet.inter set_src set_tgt in
 
     debug (lazy ("CANDIDATES: " ^ 
-      String.concat "," (List.map (fun (t,_,_,_,_) ->
-        NCicPp.ppterm ~metasenv ~subst ~context t) 
+      String.concat "," (List.map (fun (name,t,_,_,_,_) ->
+        name ^ " :: " ^ NCicPp.ppterm ~metasenv ~subst ~context t) 
       (CoercionSet.elements candidates))));
 
     List.map
-      (fun (t,arity,arg,_,_) ->
+      (fun (name,t,arity,arg,_,_) ->
           let ty =
             try NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] t 
             with NCicTypeChecker.TypeCheckerFailure s ->
@@ -148,7 +161,7 @@ let look_for_coercion status metasenv subst context infty expty =
             (NCicUntrusted.mk_appl t args) ^ " --- " ^ 
               string_of_int (List.length args) ^ " == " ^ string_of_int arg)); 
              
-          metasenv, NCicUntrusted.mk_appl t args, ty, List.nth args arg)
+          name,metasenv, NCicUntrusted.mk_appl t args, ty, List.nth args arg)
       (CoercionSet.elements candidates)
 ;;
 
@@ -159,7 +172,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
@@ -183,23 +196,19 @@ let match_coercion status ~metasenv ~subst ~context t =
       ) db)
 ;;
 
-let generate_dot_file status =
+let generate_dot_file status fmt =
   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
+        (fun (name,t,a,g,sk,dk) -> 
+          debug(lazy (let p = NCicPp.ppterm ~metasenv:[] ~context:[]
+                ~subst:[] in p t ^ " ::: " ^ p sk ^ " |--> " ^ p dk));
+          let eq_s= sk::NCicUnifHint.eq_class_of status sk in
+          let eq_t= dk::NCicUnifHint.eq_class_of status dk in
+          (name,t,a,g),eq_s,eq_t
           )
         (CoercionSet.elements dataset);
     );
@@ -233,12 +242,8 @@ let generate_dot_file status =
       fmt)
     nodes;
   List.iter 
-    (fun ((t,a,b),src,tgt) ->
+    (fun ((name,_,_,_),src,tgt) ->
        Pp.edge (mangle src) (mangle tgt)
-         ~attrs:["label",
-           NCicPp.ppterm ~metasenv:[]
-           ~subst:[] ~context:[] t] fmt)
+       ~attrs:["label", name] fmt)
     !edges;
-  Pp.trailer fmt;
-  Buffer.contents buf
 ;;