X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcoercGraph.ml;h=e54b3a847dde2d9489cf142baaa09f7b8b79cb11;hb=9dee1479d1d4ee35e9768612b35741e2ecde8fc0;hp=ac7441a4cdad4ee5f40fda81d3c0cf213cf7fb3e;hpb=2e2648a9ed26d9b813de8e6a10e2776162565f09;p=helm.git

diff --git a/helm/software/components/cic_unification/coercGraph.ml b/helm/software/components/cic_unification/coercGraph.ml
index ac7441a4c..e54b3a847 100644
--- a/helm/software/components/cic_unification/coercGraph.ml
+++ b/helm/software/components/cic_unification/coercGraph.ml
@@ -34,22 +34,26 @@ type coercion_search_result =
   | 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
+  | NotHandled
 
 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
+   List.map 
+     (fun u,saturations -> 
+        let t = CicUtil.term_of_uri u in 
+        let arity = 
+          match CoercDb.is_a_coercion t with
+          | Some (_,CoercDb.Fun i,_,_,_) -> i
+          | _ -> 0
+        in
+        arity,t,saturations) ul
   in
   let freshmeta = CicMkImplicit.new_meta metasenv subst in
-   List.map2
-    (fun arity (c,saturations) -> 
+   List.map
+    (fun (arity,c,saturations) -> 
       let ty,_ =
        CicTypeChecker.type_of_aux' ~subst metasenv context c
         CicUniv.oblivion_ugraph in
@@ -62,27 +66,29 @@ let saturate_coercion ul metasenv subst context =
         match args with
            [] -> c
          | _ -> Cic.Appl (c::args)
-    ) funclass_arityl cl
+    ) cl
 ;;
           
 (* searches a coercion fron src to tgt in the !coercions list *)
-let look_for_coercion' metasenv subst context src tgt =
+let look_for_coercion_carr metasenv subst context src tgt =
+  let is_dead = function CoercDb.Dead -> true | _ -> false in
   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)));
+             (CoercDb.string_of_carr src) 
+             (CoercDb.string_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)));
+           (CoercDb.string_of_carr src) 
+           (CoercDb.string_of_carr tgt)));
   in
-  try 
+  if is_dead src || is_dead tgt then NotHandled
+  else
     let l = 
       CoercDb.find_coercion 
         (fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt) 
@@ -97,23 +103,31 @@ let look_for_coercion' metasenv subst context src tgt =
          pp_l "approx" l;
          (match l with
          | [] -> NoCoercion
-         | ul -> SomeCoercionToTgt (saturate_coercion ul metasenv subst context))
+         | 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
+;;
+
+let rec count_pi c s t =
+  match CicReduction.whd ~delta:false ~subst:s c t with
+  | Cic.Prod (_,_,t) -> 1 + count_pi c s t
+  | _ -> 0
 ;;
 
 let look_for_coercion metasenv subst context src tgt = 
-  let src_uri = CoercDb.coerc_carr_of_term src in
-  let tgt_uri = CoercDb.coerc_carr_of_term tgt in
-  look_for_coercion' metasenv subst context src_uri tgt_uri
+  let src_arity = count_pi context subst src in
+  let tgt_arity = count_pi context subst tgt in
+  let src_carr = CoercDb.coerc_carr_of_term src src_arity in
+  let tgt_carr = CoercDb.coerc_carr_of_term tgt tgt_arity in
+  look_for_coercion_carr metasenv subst context src_carr tgt_carr
 
 let source_of t = 
-  try
-    let uri = CicUtil.uri_of_term t in
-    CoercDb.term_of_carr (fst (CoercDb.get_carr uri))
-  with Invalid_argument _ -> assert false (* t must be a coercion *)
+  match CoercDb.is_a_coercion t with
+  | None -> assert false
+  | Some (CoercDb.Sort s,_,_,_,_) -> Cic.Sort s
+  | Some (CoercDb.Uri u,_,_,_,_) -> CicUtil.term_of_uri u
+  | Some _ -> assert false (* t must be a coercion not to funclass *)
+;;
 
 let generate_dot_file () =
   let module Pp = GraphvizPp.Dot in
@@ -123,19 +137,20 @@ let generate_dot_file () =
     ~edge_attrs:["fontsize", "10"] fmt;
   let l = CoercDb.to_list () in
   let pp_description carr =
-    match CoercDb.uri_of_carr carr with
-    | None -> ()
-    | Some uri ->
-        Pp.node (CoercDb.name_of_carr carr)
-          ~attrs:["href", UriManager.string_of_uri uri] fmt in
+    match carr with
+    | CoercDb.Uri uri ->
+        Pp.node (CoercDb.string_of_carr carr)
+          ~attrs:["href", UriManager.string_of_uri uri] fmt 
+    | _ -> ()
+  in
   List.iter
     (fun (src, tgt, ul) ->
-      let src_name = CoercDb.name_of_carr src in
-      let tgt_name = CoercDb.name_of_carr tgt in
+      let src_name = CoercDb.string_of_carr src in
+      let tgt_name = CoercDb.string_of_carr tgt in
       pp_description src;
       pp_description tgt;
       List.iter
-        (fun (u,saturations) ->
+        (fun (u,saturations,_) ->
           Pp.edge src_name tgt_name
             ~attrs:[ "label",
                      (UriManager.name_of_uri u ^
@@ -167,26 +182,12 @@ let is_composite t =
 
 let coerced_arg l =
   match l with
-  | [] | [_] -> assert false
-  | c::_ when not (CoercDb.is_a_coercion' c) -> assert false
+  | [] | [_] -> None
   | 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
+     match CoercDb.is_a_coercion c with 
+     | None -> None
+     | Some (_,_,_,_,cpos) -> 
+        if List.length tl > cpos then Some (List.nth tl cpos, cpos) else None
 ;;
 
 (************************* meet calculation stuff ********************)
@@ -207,7 +208,7 @@ 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, Some x) l;;
+let splat e l = List.map (fun (x1,x2,_) -> e, Some (x1,x2)) l;;
 
 (* : carr -> (carr * uri option) where the option is always Some *)
 let get_coercions_to carr = 
@@ -258,7 +259,7 @@ let rec min acc = function
   | [] -> acc
 ;;
 
-let meets metasenv subst context left right =
+let meets metasenv subst context (grow_left,left) (grow_right,right) =
   let saturate metasenv uo =
     match uo with 
     | None -> metasenv, None
@@ -269,8 +270,10 @@ let meets metasenv subst context left right =
   in
   List.map 
     (fun (c,uo1,uo2) -> 
-      let metasenv, uo1 = saturate metasenv uo1 in
-      let metasenv, uo2 = saturate metasenv uo2 in
+      let metasenv, uo1 = 
+        if grow_left then saturate metasenv uo1 else metasenv, None in
+      let metasenv, uo2 = 
+        if grow_right then saturate metasenv uo2 else metasenv, None in
       c,metasenv, uo1, uo2)
     (min [] (intersect (grow left) (grow right)))
 ;;