Bugs fixed in merging of composite coercions. In particular the imperative

status was not handled properly and letins were handled inefficiently.

diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml
index 3d58e9acf8522950a911499122c1abb464ed5cd6..1f2a8a19ef771005df2135e2db894e046c7aca4a 100644 (file)
--- a/components/cic_unification/cicRefine.ml
+++ b/components/cic_unification/cicRefine.ml
@@ -141,7 +141,7 @@ let is_a_double_coercion t =
       | sib1,Cic.Appl (c2::tl2) when CoercGraph.is_a_coercion c2 ->
           let sib2,head = last_of tl2 in
           true, c1, c2, head,Cic.Appl (c1::sib1@[Cic.Appl
-            (c2::sib2@[Cic.Implicit None])]) 
+            (c2::sib2@[imp])]) 
       | _ -> dummyres)
   | _ -> dummyres
 
@@ -321,8 +321,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
      ugraph
 =
   let rec type_of_aux subst metasenv context t ugraph =
+    let module C = Cic in
+    let module S = CicSubstitution in
+    let module U = UriManager in
     let try_coercion t subst metasenv context ugraph coercion_tgt c =
-      let coerced = Cic.Appl[c;t] in
+      let coerced = C.Appl[c;t] in
       try
         let newt,_,subst,metasenv,ugraph = 
           type_of_aux subst metasenv context coerced ugraph 
@@ -334,9 +337,6 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
       with 
       | RefineFailure _ | Uncertain _ -> None
     in
-    let module C = Cic in
-    let module S = CicSubstitution in
-    let module U = UriManager in
      let (t',_,_,_,_) as res =
       match t with
           (*    function *)
@@ -1061,6 +1061,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                | Some t,Some (_,C.Def (ct,_)) ->
                    let subst',metasenv',ugraph' = 
                    (try
+prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");
                       fo_unif_subst subst context metasenv t ct ugraph
                     with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
                    in
@@ -1176,6 +1177,9 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                 (CicPp.ppterm t2''))))
 
   and avoid_double_coercion context subst metasenv ugraph t ty = 
+   if not !pack_coercions then
+    t,ty,subst,metasenv,ugraph
+   else
     let b, c1, c2, head, c1_c2_implicit = is_a_double_coercion t in
     if b then
       let source_carr = CoercGraph.source_of c2 in
@@ -1216,11 +1220,12 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                | RefineFailure s | Uncertain s -> 
                    debug_print s;debug_print (lazy "goon\n");
                    try 
+                     let old_pack_coercions = !pack_coercions in
                      pack_coercions := false; (* to avoid diverging *)
                      let refined_c1_c2_implicit,ty,subst,metasenv,ugraph =
                        type_of_aux subst metasenv context c1_c2_implicit ugraph 
                      in
-                     pack_coercions := true;
+                     pack_coercions := old_pack_coercions;
                      let b, _, _, _, _ = 
                        is_a_double_coercion refined_c1_c2_implicit 
                      in 
@@ -1732,7 +1737,9 @@ let pack_coercion metasenv ctx t =
        C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
    | C.LetIn (name,so,dest) -> 
        let _,ty,metasenv,ugraph =
+        pack_coercions := false;
         type_of_aux' metasenv ctx so CicUniv.empty_ugraph in
+        pack_coercions := true;
        let ctx' = Some (name,(C.Def (so,Some ty)))::ctx in
        C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
    | C.Appl l -> 
@@ -1748,7 +1755,6 @@ let pack_coercion metasenv ctx t =
            try 
              type_of_aux' metasenv ctx t ugraph 
            with RefineFailure _ | Uncertain _ -> 
-             prerr_endline (CicPp.ppterm t);
              t, t, [], ugraph 
          in
          insert_coercions := old_insert_coercions;