1. More localization: interpretation errors are now loosely localized.

[helm.git] / components / cic_unification / cicUnification.ml

diff --git a/components/cic_unification/cicUnification.ml b/components/cic_unification/cicUnification.ml
index a7a3a16741e50889b1a60a823eb41cd6d6f7452f..fb6a66d4fc5c8cb6969353d90b49c1409635cf91 100644 (file)
--- a/components/cic_unification/cicUnification.ml
+++ b/components/cic_unification/cicUnification.ml
@@ -136,7 +136,7 @@ let eta_reduce after_beta_expansion after_beta_expansion_body
  with
   WrongShape -> after_beta_expansion
 
-let rec beta_expand test_equality_only metasenv subst context t arg ugraph =
+let rec beta_expand num test_equality_only metasenv subst context t arg ugraph =
  let module S = CicSubstitution in
  let module C = Cic in
 let foo () =
@@ -279,7 +279,7 @@ let foo () =
   let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
   let fresh_name =
    FreshNamesGenerator.mk_fresh_name ~subst
-    metasenv context (Cic.Name "Hbeta") ~typ:argty
+    metasenv context (Cic.Name ("Hbeta" ^ string_of_int num)) ~typ:argty
   in
    let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
    let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
@@ -288,15 +288,15 @@ in profiler_beta_expand.HExtlib.profile foo ()
 
 
 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
-  let subst,metasenv,hd,ugraph =
+  let _,subst,metasenv,hd,ugraph =
     List.fold_right
-      (fun arg (subst,metasenv,t,ugraph) ->
+      (fun arg (num,subst,metasenv,t,ugraph) ->
          let subst,metasenv,t,ugraph1 =
-           beta_expand test_equality_only 
+           beta_expand num test_equality_only 
              metasenv subst context t arg ugraph 
          in
-           subst,metasenv,t,ugraph1 
-      ) args (subst,metasenv,t,ugraph) 
+           num+1,subst,metasenv,t,ugraph1 
+      ) args (1,subst,metasenv,t,ugraph) 
   in
     subst,metasenv,hd,ugraph
 
@@ -628,51 +628,44 @@ let res =
                              metasenv (C.Appl l1) (C.Appl l2) ugraph
                          | _ -> raise exn)
                       else
-                       let meets = CoercGraph.meets car1 car2 in
+                       let meets = 
+                         CoercGraph.meets metasenv subst context car1 car2 
+                       in
                         (match meets with
                         | [] -> raise exn
-                        | _::_::_ ->
-prerr_endline ("1: NON DOVEVA SUCCEDERE!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!");
-let m1::m2::_ = meets in
-prerr_endline ("M1 = " ^ CoercDb.name_of_carr m1 ^ "\nM2 = " ^ CoercDb.name_of_carr m2);
-assert false
-                        | [m] -> 
+                        | (carr,metasenv,to1,to2)::xxx -> 
+                          (match xxx with
+                          [] -> ()
+                          | (m2,_,c2,c2')::_ ->
+                          let m1,_,c1,c1' = carr,metasenv,to1,to2 in
+                          let unopt = 
+                            function Some (_,t) -> CicPp.ppterm t 
+                            | None -> "id"
+                          in
+                          HLog.warn 
+                            ("There are two minimal joins of "^
+                            CoercDb.name_of_carr car1^" and "^
+                            CoercDb.name_of_carr car2^": " ^ 
+                            CoercDb.name_of_carr m1 ^ " via "^unopt c1^" + "^
+                            unopt c1'^" and " ^ CoercDb.name_of_carr m2^" via "^
+                            unopt c2^" + "^unopt c2'));
                           let last_tl1',(subst,metasenv,ugraph) =
-                           match last_tl1 with
-                            | Cic.Meta (i1,l1)
-                              when not (CoercDb.eq_carr m car1) ->
-                               (match
-                                 CoercGraph.look_for_coercion' metasenv subst
-                                  context m car1
-                                with
-                                 | CoercGraph.SomeCoercion ((metasenv,last,coerced)::_)
-                                   ->
-                                    last,
-                                    fo_unif_subst test_equality_only subst context
+                           match last_tl1,to1 with
+                            | Cic.Meta (i1,l1),Some (last,coerced) -> 
+                                last,
+                                  fo_unif_subst test_equality_only subst context
                                      metasenv coerced last_tl1 ugraph
-                                 | _ ->
-prerr_endline ("2: NON DOVEVA SUCCEDERE!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!");
-assert false)
-                            | _ -> last_tl1,(subst,metasenv,ugraph) in
+                            | _ -> last_tl1,(subst,metasenv,ugraph) 
+                          in
                           let last_tl2',(subst,metasenv,ugraph) =
-                           match last_tl2 with
-                              Cic.Meta (i2,l2) when not (CoercDb.eq_carr m car2) ->
-                               (match
-                                 CoercGraph.look_for_coercion' metasenv subst
-                                  context m car2
-                                with
-                                   (*CSC: bu here: I am considering only the first one*)
-                                 | CoercGraph.SomeCoercion ((metasenv,last,coerced)::_)
-                                   ->
-                                    last,
-                                    fo_unif_subst test_equality_only subst context
+                           match last_tl2,to2 with
+                            | Cic.Meta (i2,l2),Some (last,coerced) -> 
+                                last,
+                                  fo_unif_subst test_equality_only subst context
                                      metasenv coerced last_tl2 ugraph
-                                 | _ ->
-prerr_endline ("3: NON DOVEVA SUCCEDERE!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!");
-assert false)
-                            | _ -> last_tl2,(subst,metasenv,ugraph)
+                            | _ -> last_tl2,(subst,metasenv,ugraph) 
                           in
-(*DEBUGGING ONLY:
+                        (*DEBUGGING ONLY:
 prerr_endline ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context);
 *)
                            let subst,metasenv,ugraph =