This commit (partially) removes a big source of inefficiency (at least for

[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 8ae28448387aee48141c3382d3dce78883fa62fc..fe5ae76502ba2703cbb70519186eb1d29872abfb 100644 (file)
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -25,9 +25,16 @@
 
 open Printf
 
-exception UnificationFailure of string;;
+type failure_msg =
+   Reason of string
+ | Enriched of string * Cic.substitution * Cic.context * Cic.metasenv *
+               Cic.term * Cic.term * CicUniv.universe_graph
+
+let failure_msg_of_string msg = Reason msg
+
+exception UnificationFailure of failure_msg;;
 exception Uncertain of string;;
-exception AssertFailure of string;;
+exception AssertFailure of failure_msg;;
 
 let debug_print = fun _ -> () 
 
@@ -45,7 +52,7 @@ let type_of_aux' metasenv subst context term ugraph =
              (CicMetaSubst.ppcontext subst context)
              (CicMetaSubst.ppmetasenv subst metasenv) 
              (CicMetaSubst.ppsubst subst) msg) in
-        raise (AssertFailure msg);;
+        raise (AssertFailure (Reason msg));;
 
 let exists_a_meta l = 
   List.exists (function Cic.Meta _ -> true | _ -> false) l
@@ -293,7 +300,7 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin
             with
                 Exit ->
                   raise 
-                    (UnificationFailure "1")
+                    (UnificationFailure (Reason "1"))
                     (*
                     (sprintf
                       "Error trying to unify %s with %s: the algorithm tried to check whether the two substitutions are convertible; if they are not, it tried to unify the two substitutions. No restriction was attempted."
@@ -301,7 +308,7 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin
                       (CicMetaSubst.ppterm subst t2))) *)
               | Invalid_argument _ ->
                   raise 
-                    (UnificationFailure "2"))
+                    (UnificationFailure (Reason "2")))
                     (*
                     (sprintf
                       "Error trying to unify %s with %s: the lengths of the two local contexts do not match." 
@@ -336,9 +343,8 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin
                   test_equality_only 
                   subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
             with 
-                UnificationFailure msg 
-              | Uncertain msg ->
-                  (* debug_print msg; *)raise (UnificationFailure msg) 
+                UnificationFailure msg ->raise (UnificationFailure msg)  
+              | Uncertain msg -> raise (UnificationFailure (Reason msg))
               | AssertFailure _ ->
                   debug_print "siamo allo huge hack";
                   (* TODO huge hack!!!!
@@ -354,7 +360,7 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin
              CicMetaSubst.delift n subst context metasenv l t
            with
                (CicMetaSubst.MetaSubstFailure msg)-> 
-                 raise (UnificationFailure msg)
+                 raise (UnificationFailure (Reason msg))
              | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
          in
          let t'',ugraph2 =
@@ -388,7 +394,7 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin
        fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
         exp_named_subst1 exp_named_subst2 ugraph
       else
-       raise (UnificationFailure "3")
+       raise (UnificationFailure (Reason "3"))
          (* (sprintf
             "Can't unify %s with %s due to different constants"
             (CicMetaSubst.ppterm subst t1) 
@@ -399,7 +405,7 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin
            test_equality_only 
            subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
        else
-         raise (UnificationFailure "4")
+         raise (UnificationFailure (Reason "4"))
            (* (sprintf
               "Can't unify %s with %s due to different inductive principles"
               (CicMetaSubst.ppterm subst t1) 
@@ -411,7 +417,7 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin
            test_equality_only 
            subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
        else
-         raise (UnificationFailure "5")
+         raise (UnificationFailure (Reason "5"))
            (* (sprintf
               "Can't unify %s with %s due to different inductive constructors"
               (CicMetaSubst.ppterm subst t1) 
@@ -449,7 +455,7 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin
                         test_equality_only subst context metasenv t1 t2 ugraph)
                    (subst,metasenv,ugraph) l1 l2 
                with (Invalid_argument msg) -> 
-                 raise (UnificationFailure msg)) 
+                 raise (UnificationFailure (Reason msg)))
           | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
               (* we verify that none of the args is a Meta, 
                 since beta expanding with respoect to a metavariable 
@@ -526,7 +532,7 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin
           ) (subst'',metasenv'',ugraph2) pl1 pl2 
         with
          Invalid_argument _ ->
-          raise (UnificationFailure "6"))
+          raise (UnificationFailure (Reason "6")))
            (* (sprintf
               "Error trying to unify %s with %s: the number of branches is not the same." 
               (CicMetaSubst.ppterm subst t1) 
@@ -535,7 +541,7 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin
        if t1 = t2 then
          subst, metasenv,ugraph
        else
-        raise (UnificationFailure "6")
+        raise (UnificationFailure (Reason "6"))
           (* (sprintf
              "Can't unify %s with %s because they are not convertible"
              (CicMetaSubst.ppterm subst t1) 
@@ -570,17 +576,17 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin
              subst, metasenv, ugraph1
            else
              raise (* (UnificationFailure "7") *)
-                (UnificationFailure (sprintf
+                (UnificationFailure (Reason (sprintf
                   "7: Can't unify %s with %s because they are not convertible"
                   (CicMetaSubst.ppterm subst t1) 
-                  (CicMetaSubst.ppterm subst t2)))
+                  (CicMetaSubst.ppterm subst t2))))
    | (C.Prod _, t2) ->
        let t2' = R.whd ~subst context t2 in
        (match t2' with
             C.Prod _ -> 
               fo_unif_subst test_equality_only 
                 subst context metasenv t1 t2' ugraph         
-          | _ -> raise (UnificationFailure "8"))
+          | _ -> raise (UnificationFailure (Reason "8")))
    | (t1, C.Prod _) ->
        let t1' = R.whd ~subst context t1 in
        (match t1' with
@@ -589,22 +595,16 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin
                 subst context metasenv t1' t2 ugraph         
           | _ -> (* raise (UnificationFailure "9")) *)
              raise 
-                (UnificationFailure (sprintf
+                (UnificationFailure (Reason (sprintf
                    "9: Can't unify %s with %s because they are not convertible"
                    (CicMetaSubst.ppterm subst t1) 
-                   (CicMetaSubst.ppterm subst t2))))
+                   (CicMetaSubst.ppterm subst t2)))))
    | (_,_) ->
-       let b,ugraph1 = 
-         R.are_convertible ~subst ~metasenv context t1 t2 ugraph 
-       in
-         if b then 
-           subst, metasenv, ugraph1
-         else
-           raise (UnificationFailure  "10") 
-             (* (sprintf
-                "Can't unify %s with %s because they are not convertible"
-                (CicMetaSubst.ppterm subst t1) 
-                (CicMetaSubst.ppterm subst t2))) *)
+       raise (UnificationFailure (Reason "10"))
+         (* (sprintf
+            "Can't unify %s with %s because they are not convertible"
+            (CicMetaSubst.ppterm subst t1) 
+            (CicMetaSubst.ppterm subst t2))) *)
 
 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
  exp_named_subst1 exp_named_subst2 ugraph
@@ -624,8 +624,8 @@ and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
          UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm subst t)
        ) ens) 
    in
-    raise (UnificationFailure (sprintf
-     "Error trying to unify the two explicit named substitutions (local contexts) %s and %s: their lengths is different." (print_ens exp_named_subst1) (print_ens exp_named_subst2)))
+    raise (UnificationFailure (Reason (sprintf
+     "Error trying to unify the two explicit named substitutions (local contexts) %s and %s: their lengths is different." (print_ens exp_named_subst1) (print_ens exp_named_subst2))))
 
 (* A substitution is a (int * Cic.term) list that associates a               *)
 (* metavariable i with its body.                                             *)
@@ -638,7 +638,21 @@ let fo_unif metasenv context t1 t2 ugraph =
  fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
 
 let fo_unif_subst subst context metasenv t1 t2 ugraph =
-  let enrich_msg msg = (* "bella roba" *)
+  try
+    fo_unif_subst false subst context metasenv t1 t2 ugraph
+  with
+  | AssertFailure (Enriched _ as msg) -> assert false
+  | AssertFailure (Reason msg) ->
+     raise (AssertFailure (Enriched (msg,subst,context,metasenv,t1,t2,ugraph)))
+  | UnificationFailure (Enriched _ as msg) -> assert false
+  | UnificationFailure (Reason msg) ->
+     raise (UnificationFailure (Enriched (msg,subst,context,metasenv,t1,t2,ugraph)))
+;;
+
+let explain_error =
+ function
+    Reason msg -> msg
+  | Enriched (msg,subst,context,metasenv,t1,t2,ugraph) ->
     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"
       (CicMetaSubst.ppterm subst t1)
       (try
@@ -653,11 +667,3 @@ let fo_unif_subst subst context metasenv t1 t2 ugraph =
       (CicMetaSubst.ppcontext subst context)
       (CicMetaSubst.ppmetasenv subst metasenv)
       (CicMetaSubst.ppsubst subst) msg 
-  in
-  try
-    fo_unif_subst false subst context metasenv t1 t2 ugraph
-  with
-  | AssertFailure msg -> raise (AssertFailure (enrich_msg msg))
-  | UnificationFailure msg -> raise (UnificationFailure (enrich_msg msg))
-;;
-