Speed-up in match.ma.

[helm.git] / matita / components / ng_refiner / nCicRefiner.ml

diff --git a/matita/components/ng_refiner/nCicRefiner.ml b/matita/components/ng_refiner/nCicRefiner.ml
index d26edf6d9d3bd40783963909cc84bd9dcaaa1d13..550c75e9382c4ec9173f76d1da3d9428f28644d0 100644 (file)
--- a/matita/components/ng_refiner/nCicRefiner.ml
+++ b/matita/components/ng_refiner/nCicRefiner.ml
@@ -70,7 +70,7 @@ let exp_implicit status ~localise metasenv subst context with_type t =
               ~unify:(fun m s c t1 t2 ->
                 try Some (NCicUnification.unify status m s c t1 t2)
                 with NCicUnification.UnificationFailure _ | NCicUnification.Uncertain _ -> None)
-              metasenv subst context 0 (0,NCic.Irl 0) typ
+              metasenv subst context (-1) (0,NCic.Irl 0) typ
             with
               NCicMetaSubst.MetaSubstFailure _
             | NCicMetaSubst.Uncertain _ ->
@@ -143,11 +143,14 @@ let check_allowed_sort_elimination status localise r orig =
 let mk_fresh_name context name =
 try
  let rex = Str.regexp "[0-9']*$" in
+ let rex2 = Str.regexp "'*$" in
  let basename = Str.global_replace rex "" in
  let suffix name =
   ignore (Str.search_forward rex name 0);
   let n = Str.matched_string name in
-   if n = "" then 0 else int_of_string n in
+  let n = Str.global_replace rex2 "" n in
+   if n = "" then 0 else int_of_string n
+in
  let name' = basename name in
  let name' = if name' = "_" then "H" else name' in
  let last =
@@ -502,13 +505,14 @@ and try_coercions status
   (* we try with a coercion *)
   let rec first exc = function
   | [] ->   
-     let expty =
-      match expty with
-         `Type expty -> status#ppterm ~metasenv ~subst ~context expty
-       | `Sort -> "[[sort]]"
-       | `Prod -> "[[prod]]" in
       pp (lazy "WWW: no more coercions!");      
-      raise (wrap_exc (lazy (localise orig_t, Printf.sprintf
+      raise (wrap_exc (lazy
+       let expty =
+        match expty with
+           `Type expty -> status#ppterm ~metasenv ~subst ~context expty
+         | `Sort -> "[[sort]]"
+         | `Prod -> "[[prod]]" in
+         (localise orig_t, Printf.sprintf
         "The term\n%s\nhas type\n%s\nbut is here used with type\n%s"
         (status#ppterm ~metasenv ~subst ~context t)
         (status#ppterm ~metasenv ~subst ~context infty)
@@ -906,12 +910,19 @@ and force_to_sort status metasenv subst context t orig_t localise ty =
       metasenv, subst, t, ty
   with
       Failure _ -> 
+        let msg =
+         (lazy (localise orig_t, 
+           "The type of " ^ status#ppterm ~metasenv ~subst ~context t ^
+           " is not a sort: " ^ status#ppterm ~metasenv ~subst ~context ty)) in
         let ty = NCicReduction.whd status ~subst context ty in
+        let exn =
+         if NCicUnification.could_reduce status ~subst context ty then
+          Uncertain msg
+         else
+          RefineFailure msg
+        in
           try_coercions status ~localise metasenv subst context
-            t orig_t ty `Sort 
-             (Uncertain (lazy (localise orig_t, 
-             "The type of " ^ status#ppterm ~metasenv ~subst ~context t ^
-             " is not a sort: " ^ status#ppterm ~metasenv ~subst ~context ty)))
+            t orig_t ty `Sort exn
 
 and sort_of_prod status localise metasenv subst context orig_s orig_t (name,s)
  t (t1, t2)