Potential performance improvement + better disambiguation error messages:

[helm.git] / helm / software / components / cic_unification / cicMetaSubst.ml

diff --git a/helm/software/components/cic_unification/cicMetaSubst.ml b/helm/software/components/cic_unification/cicMetaSubst.ml
index 53efcf96edfad1adeb23704626206dbcaaa9feab..96efe2e3cb7ff5f72442593effbc70d461452680 100644 (file)
--- a/helm/software/components/cic_unification/cicMetaSubst.ml
+++ b/helm/software/components/cic_unification/cicMetaSubst.ml
@@ -253,6 +253,11 @@ let apply_subst =
     apply_subst_gen ~appl_fun s t
 ;;
 
+let profiler = HExtlib.profile "U/CicMetaSubst.apply_subst"
+let apply_subst s t = 
+  profiler.HExtlib.profile (apply_subst s) t
+
+
 let rec apply_subst_context subst context =
 (*
   incr apply_subst_context_counter;
@@ -620,15 +625,17 @@ let delift n subst context metasenv l t =
     function
        C.Rel m -> 
          if m <=k then
-          C.Rel m   (*CSC: che succede se c'e' un Def? Dovrebbe averlo gia' *)
-                    (*CSC: deliftato la regola per il LetIn                 *)
-                    (*CSC: FALSO! La regola per il LetIn non lo fa          *)
+          C.Rel m
          else
           (try
             match List.nth context (m-k-1) with
                Some (_,C.Def (t,_)) ->
                 (*CSC: Hmmm. This bit of reduction is not in the spirit of    *)
                 (*CSC: first order unification. Does it help or does it harm? *)
+                (*CSC: ANSWER: it hurts performances since it is possible to  *)
+                (*CSC: have an exponential explosion of the size of the proof.*)
+                (*CSC: However, without this bit of reduction some "apply" in *)
+                (*CSC: the library fail (e.g. nat/nth_prime.ma).              *)
                 deliftaux k (S.lift m t)
              | Some (_,C.Decl t) ->
                 C.Rel ((position (m-k) l) + k)
@@ -733,13 +740,24 @@ debug_print(lazy (sprintf
           (List.map
             (function Some t -> ppterm subst t | None -> "_") l
           )))); *)
-      raise (Uncertain (lazy (sprintf
+      let msg = (lazy (sprintf
         "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
         (ppterm subst t)
         (String.concat "; "
           (List.map
             (function Some t -> ppterm subst t | None -> "_")
-            l)))))
+            l))))
+      in
+       if
+        (*CSC: WARNING: if we are working up to reduction (I do not think so),
+          the following test should be replaced with "all the terms in l are
+          meta-closed" *)
+        not
+         (List.exists (function Some (Cic.Meta _) -> true | _ -> false ) l)
+       then
+        raise (MetaSubstFailure msg)
+       else
+        raise (Uncertain msg)
    in
    let (metasenv, subst) = restrict subst !to_be_restricted metasenv in
     res, metasenv, subst