X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcoercGraph.ml;h=ac7441a4cdad4ee5f40fda81d3c0cf213cf7fb3e;hb=790eccfa6b94dc82826d919691f8d4bfadb04573;hp=70e90af52f2c4fb0333441b872873c6e5fbfec0e;hpb=5d010a40c726d9a7eceeb35e70e41a158eb63c70;p=helm.git

diff --git a/helm/software/components/cic_unification/coercGraph.ml b/helm/software/components/cic_unification/coercGraph.ml
index 70e90af52..ac7441a4c 100644
--- a/helm/software/components/cic_unification/coercGraph.ml
+++ b/helm/software/components/cic_unification/coercGraph.ml
@@ -32,6 +32,7 @@ type coercion_search_result =
      (* to apply the coercion it is sufficient to unify the last coercion
         argument (that is a Meta) with the term to be coerced *)
   | SomeCoercion of (Cic.metasenv * Cic.term * Cic.term) list
+  | SomeCoercionToTgt of (Cic.metasenv * Cic.term * Cic.term) list
   | NoCoercion
   | NotMetaClosed
   | NotHandled of string Lazy.t
@@ -39,56 +40,65 @@ type coercion_search_result =
 let debug = false
 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
 
+let saturate_coercion ul metasenv subst context =
+  let cl =
+   List.map (fun u,saturations -> CicUtil.term_of_uri u,saturations) ul in
+  let funclass_arityl = 
+    let _,tgtcarl = List.split (List.map (fun u,_ -> CoercDb.get_carr u) ul) in
+    List.map (function CoercDb.Fun i -> i | _ -> 0) tgtcarl
+  in
+  let freshmeta = CicMkImplicit.new_meta metasenv subst in
+   List.map2
+    (fun arity (c,saturations) -> 
+      let ty,_ =
+       CicTypeChecker.type_of_aux' ~subst metasenv context c
+        CicUniv.oblivion_ugraph in
+      let _,metasenv,args,lastmeta =
+       TermUtil.saturate_term ~delta:false freshmeta metasenv context ty arity in
+      let irl =
+       CicMkImplicit.identity_relocation_list_for_metavariable context
+      in
+       metasenv, Cic.Meta (lastmeta - saturations - 1,irl),
+        match args with
+           [] -> c
+         | _ -> Cic.Appl (c::args)
+    ) funclass_arityl cl
+;;
+          
 (* searches a coercion fron src to tgt in the !coercions list *)
 let look_for_coercion' metasenv subst context src tgt =
+  let pp_l s l =
+   match l with
+   | [] -> 
+       debug_print 
+         (lazy 
+         (sprintf ":-( coercion non trovata[%s] da %s a %s" s
+             (CoercDb.name_of_carr src) 
+             (CoercDb.name_of_carr tgt)));
+   | _::_ -> 
+       debug_print (lazy (
+               sprintf ":-) TROVATE[%s] %d coercion(s) da %s a %s" s
+           (List.length l)
+           (CoercDb.name_of_carr src) 
+           (CoercDb.name_of_carr tgt)));
+  in
   try 
     let l = 
       CoercDb.find_coercion 
-        (fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt) in
-    let uri =
-     match l with
-     | [] -> 
-         debug_print 
-           (lazy 
-             (sprintf ":-( coercion non trovata da %s a %s" 
-               (CoercDb.name_of_carr src) 
-               (CoercDb.name_of_carr tgt)));
-         None
-     | _::_ -> 
-         debug_print (lazy (
-           sprintf ":-) TROVATE %d coercion(s) da %s a %s" 
-             (List.length l)
-             (CoercDb.name_of_carr src) 
-             (CoercDb.name_of_carr tgt)));
-         Some l
+        (fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt) 
     in
-     (match uri with
-         None -> NoCoercion
-       | Some ul ->
-          let cl = List.map CicUtil.term_of_uri ul in
-          let funclass_arityl = 
-            let _,tgtcarl = List.split (List.map CoercDb.get_carr ul) in
-            List.map (function CoercDb.Fun i -> i | _ -> 0) tgtcarl
-          in
-          let freshmeta = CicMkImplicit.new_meta metasenv subst in
-          let newtl =
-           List.map2
-            (fun arity c -> 
-              let ty,_ =
-               CicTypeChecker.type_of_aux' ~subst metasenv context c
-                CicUniv.empty_ugraph in
-              let _,metasenv,args,lastmeta =
-               TermUtil.saturate_term freshmeta metasenv context ty arity in
-              let irl =
-               CicMkImplicit.identity_relocation_list_for_metavariable context
-              in
-               metasenv, Cic.Meta (lastmeta-1,irl),
-                match args with
-                   [] -> c
-                 | _ -> Cic.Appl (c::args)
-            ) funclass_arityl cl
-          in
-           SomeCoercion newtl)
+    pp_l "precise" l;
+     (match l with
+     | [] -> 
+         let l = 
+           CoercDb.find_coercion 
+             (fun (_,t) -> CoercDb.eq_carr t tgt) 
+         in
+         pp_l "approx" l;
+         (match l with
+         | [] -> NoCoercion
+         | ul -> SomeCoercionToTgt (saturate_coercion ul metasenv subst context))
+     | ul -> SomeCoercion (saturate_coercion ul metasenv subst context))
   with
     | CoercDb.EqCarrNotImplemented s -> NotHandled s
     | CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed
@@ -119,18 +129,23 @@ let generate_dot_file () =
         Pp.node (CoercDb.name_of_carr carr)
           ~attrs:["href", UriManager.string_of_uri uri] fmt in
   List.iter
-    (fun (src, tgt, cl) ->
+    (fun (src, tgt, ul) ->
       let src_name = CoercDb.name_of_carr src in
       let tgt_name = CoercDb.name_of_carr tgt in
       pp_description src;
       pp_description tgt;
       List.iter
-        (fun c ->
+        (fun (u,saturations) ->
           Pp.edge src_name tgt_name
-            ~attrs:[ "label", UriManager.name_of_uri c;
-              "href", UriManager.string_of_uri c ]
+            ~attrs:[ "label",
+                     (UriManager.name_of_uri u ^
+                      if saturations = 0 then
+                       ""
+                      else
+                       "(" ^ string_of_int saturations ^ ")");
+              "href", UriManager.string_of_uri u ]
             fmt)
-        cl)
+        ul)
     l;
   Pp.trailer fmt;
   Buffer.contents buf
@@ -143,58 +158,121 @@ let is_composite t =
       | Cic.Appl (he::_) -> CicUtil.uri_of_term he
       | _ -> CicUtil.uri_of_term t
     in
-    match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
+    match CicEnvironment.get_obj CicUniv.oblivion_ugraph uri with
     | Cic.Constant (_,_, _, _, attrs),_  ->
         List.exists (function `Class (`Coercion _) -> true | _ -> false) attrs
     | _ -> false
   with Invalid_argument _ -> false
 ;;
 
-let uniq = HExtlib.list_uniq ~eq:(fun (a,_) (b,_) -> CoercDb.eq_carr a b);;
+let coerced_arg l =
+  match l with
+  | [] | [_] -> assert false
+  | c::_ when not (CoercDb.is_a_coercion' c) -> assert false
+  | c::tl -> 
+     let arity = 
+       match CoercDb.is_a_coercion_to_funclass c with None -> 0 | Some a -> a 
+    in
+    (* decide a decent structure for coercion carriers so that all this stuff is
+     * useless *)
+    let pi = 
+      (* this calculation is not complete, since we have strange carriers *)
+      let rec count_pi = function
+        | Cic.Prod(_,_,t) -> 1+ (count_pi t)
+        | _ -> 0
+      in
+      let uri = CicUtil.uri_of_term c in
+      match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
+      | Cic.Constant (_, _, ty, _, _) -> count_pi ty
+      | _ -> assert false
+    in
+    try Some (List.nth tl (pi - arity)) with Invalid_argument _ -> None
+;;
+
+(************************* meet calculation stuff ********************)
+let eq_uri_opt u1 u2 = 
+  match u1,u2 with
+  | Some (u1,_), Some (u2,_) -> UriManager.eq u1 u2
+  | None,Some _ | Some _, None -> false
+  | None, None -> true
+;;
+
+let eq_carr_uri (c1,u1) (c2,u2) = CoercDb.eq_carr c1 c2 && eq_uri_opt u1 u2;;
+
+let eq_carr_uri_uri (c1,u1,u11) (c2,u2,u22) = 
+  CoercDb.eq_carr c1 c2 && eq_uri_opt u1 u2 && eq_uri_opt u11 u22
+;;
+
+let uniq = HExtlib.list_uniq ~eq:eq_carr_uri;;
+
+let uniq2 = HExtlib.list_uniq ~eq:eq_carr_uri_uri;;
 
-let splat e l = List.map (fun x -> e, x) l;;
+let splat e l = List.map (fun x -> e, Some x) l;;
 
+(* : carr -> (carr * uri option) where the option is always Some *)
 let get_coercions_to carr = 
   let l = CoercDb.to_list () in
-  List.flatten 
-    (HExtlib.filter_map 
-      (fun (src,tgt,cl) -> 
-        if CoercDb.eq_carr tgt carr then Some (splat src cl) else None) 
-      l)
+  let splat_coercion_to carr (src,tgt,cl) =
+    if CoercDb.eq_carr tgt carr then Some (splat src cl) else None
+  in
+  let l = List.flatten (HExtlib.filter_map (splat_coercion_to carr) l) in
+  l
 ;;
 
+(* : carr -> (carr * uri option) where the option is always Some *)
 let get_coercions_from carr = 
   let l = CoercDb.to_list () in
-  List.flatten 
-    (HExtlib.filter_map 
-      (fun (src,tgt,cl) -> 
-        if CoercDb.eq_carr src carr then Some (splat tgt cl) else None) 
-      l)
+  let splat_coercion_from carr (src,tgt,cl) =
+    if CoercDb.eq_carr src carr then Some (splat tgt cl) else None
+  in
+  List.flatten (HExtlib.filter_map (splat_coercion_from carr) l)
 ;;
 
+(* intersect { (s1,u1) | u1:s1->t1 } { (s2,u2) | u2:s2->t2 } 
+ * gives the set { (s,u1,u2) | u1:s->t1 /\ u2:s->t2 } *)
 let intersect l1 l2 = 
-  let is_in_l1 (x,_) = List.exists (fun (src,_) -> CoercDb.eq_carr x src) l1 in
-  uniq (List.filter is_in_l1 l2)
+  let is_in_l1 (x,u2) = 
+    HExtlib.filter_map 
+      (fun (src,u1) -> 
+         if CoercDb.eq_carr x src then Some (src,u1,u2) else None)
+    l1
+  in
+  uniq2 (List.flatten (List.map is_in_l1 l2))
 ;;
 
-let grow s = 
-  uniq (List.flatten (List.map (fun (x,_) -> get_coercions_to x) s) @ s)
+(* grow tgt gives all the (src,u) such that u:tgt->src *)
+let grow tgt = 
+  uniq ((tgt,None)::(get_coercions_to tgt))
 ;;
 
-let lb c = 
+let lb (c,_,_) = 
   let l = get_coercions_from c in
-  function x -> List.exists (fun (y,_) -> CoercDb.eq_carr x y) l
+  fun (x,_,_) -> List.exists (fun (y,_) -> CoercDb.eq_carr x y) l
 ;;
 
+(* given the set { (s,u1,u2) | u1:s->t1 /\ u2:s->t2 } removes the elements 
+ * (s,_,_) such that (s',_,_) is in the set and there exists a coercion s->s' *)
 let rec min acc = function
   | c::tl -> 
     if List.exists (lb c) (tl@acc) then min acc tl else min (c::acc) tl
   | [] -> acc
 ;;
 
-let meets left right =
-  let u = UriManager.uri_of_string "cic:/foo.con" in
-  min [] (List.map fst (intersect (grow [left,u]) (grow [right,u])))
+let meets metasenv subst context left right =
+  let saturate metasenv uo =
+    match uo with 
+    | None -> metasenv, None
+    | Some u -> 
+        match saturate_coercion [u] metasenv subst context with
+        | [metasenv, sat, last] -> metasenv, Some (sat, last)
+        | _ -> assert false
+  in
+  List.map 
+    (fun (c,uo1,uo2) -> 
+      let metasenv, uo1 = saturate metasenv uo1 in
+      let metasenv, uo2 = saturate metasenv uo2 in
+      c,metasenv, uo1, uo2)
+    (min [] (intersect (grow left) (grow right)))
 ;;
 
 (* EOF *)