removed no longer used METAs

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

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index a3bc1f39a02a6fb76213c7caf54de0bc798c3a3d..d1e010ca696558aefe36f8b2ec95f334634aea16 100644 (file)
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -23,12 +23,15 @@
  * http://cs.unibo.it/helm/.
  *)
 
+(* $Id$ *)
+
 open Printf
 
 exception UnificationFailure of string Lazy.t;;
 exception Uncertain of string Lazy.t;;
 exception AssertFailure of string Lazy.t;;
 
+let verbose = false;;
 let debug_print = fun _ -> () 
 
 let profiler_toa = HExtlib.profile "fo_unif_subst.type_of_aux'"
@@ -568,8 +571,58 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
                         fo_unif_l 
                           test_equality_only subst' metasenv' (l1,l2) ugraph1
               in
+              (try 
                 fo_unif_l 
-                  test_equality_only subst metasenv (lr1, lr2)  ugraph)
+                  test_equality_only subst metasenv (lr1, lr2)  ugraph
+              with 
+              | UnificationFailure _
+              | Uncertain _ as exn -> 
+                  (match l1, l2 with
+                  | (((Cic.Const (uri1, ens1)) as c1) :: tl1), 
+                     (((Cic.Const (uri2, ens2)) as c2) :: tl2) when
+                    CoercGraph.is_a_coercion c1 && 
+                    CoercGraph.is_a_coercion c2 ->
+                      let body1, attrs1, ugraph = 
+                        match CicEnvironment.get_obj ugraph uri1 with
+                        | Cic.Constant (_,Some bo, _, _, attrs),u  -> bo,attrs,u
+                        | _ -> assert false
+                      in
+                      let body2, attrs2, ugraph = 
+                        match CicEnvironment.get_obj ugraph uri2 with
+                        | Cic.Constant (_,Some bo, _, _, attrs),u -> bo, attrs,u
+                        | _ -> assert false
+                      in
+                      let is_composite1 = 
+                        List.exists ((=) (`Class `Coercion)) attrs1 in
+                      let is_composite2 = 
+                        List.exists ((=) (`Class `Coercion)) attrs2 in
+                      (match is_composite1, is_composite2 with
+                      | false, false -> raise exn
+                      | true, false ->
+                          let body1 = CicSubstitution.subst_vars ens1 body1 in
+                          let appl = Cic.Appl (body1::tl1) in
+                          let redappl = CicReduction.head_beta_reduce appl in
+                          fo_unif_subst 
+                            test_equality_only subst context metasenv 
+                              redappl t2 ugraph
+                      | false, true -> 
+                          let body2 = CicSubstitution.subst_vars ens2 body2 in
+                          let appl = Cic.Appl (body2::tl2) in
+                          let redappl = CicReduction.head_beta_reduce appl in
+                          fo_unif_subst 
+                            test_equality_only subst context metasenv 
+                             t1 redappl ugraph
+                      | true, true ->
+                          let body1 = CicSubstitution.subst_vars ens1 body1 in
+                          let appl1 = Cic.Appl (body1::tl1) in
+                          let redappl1 = CicReduction.head_beta_reduce appl1 in
+                          let body2 = CicSubstitution.subst_vars ens2 body2 in
+                          let appl2 = Cic.Appl (body2::tl2) in
+                          let redappl2 = CicReduction.head_beta_reduce appl2 in
+                          fo_unif_subst 
+                            test_equality_only subst context metasenv 
+                             redappl1 redappl2 ugraph)
+                  | _ -> raise exn)))
    | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
        let subst', metasenv',ugraph1 = 
         fo_unif_subst test_equality_only subst context metasenv outt1 outt2
@@ -691,8 +744,9 @@ let fo_unif metasenv context t1 t2 ugraph =
  fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
 
 let enrich_msg msg subst context metasenv t1 t2 ugraph =
- lazy
-  (sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nand substitution\n%s\nbecause %s"
+ lazy (
+  if verbose then
+   sprintf "[Verbose] Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nand substitution\n%s\nbecause %s"
     (CicMetaSubst.ppterm subst t1)
     (try
       let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
@@ -711,7 +765,29 @@ let enrich_msg msg subst context metasenv t1 t2 ugraph =
     | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
     (CicMetaSubst.ppcontext subst context)
     (CicMetaSubst.ppmetasenv subst metasenv)
-    (CicMetaSubst.ppsubst subst) (Lazy.force msg))
+    (CicMetaSubst.ppsubst subst) (Lazy.force msg)
+ else
+   sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
+    (CicMetaSubst.ppterm_in_context subst t1 context)
+    (try
+      let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
+      CicMetaSubst.ppterm_in_context subst ty_t1 context
+    with 
+    | UnificationFailure s
+    | Uncertain s
+    | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
+    (CicMetaSubst.ppterm_in_context subst t2 context)
+    (try
+      let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
+      CicMetaSubst.ppterm_in_context subst ty_t2 context
+    with
+    | UnificationFailure s
+    | Uncertain s
+    | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
+    (CicMetaSubst.ppcontext subst context)
+    (CicMetaSubst.ppmetasenv subst metasenv)
+    (Lazy.force msg)
+ )
 
 let fo_unif_subst subst context metasenv t1 t2 ugraph =
   try