X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_refiner%2FnCicRefiner.ml;h=550c75e9382c4ec9173f76d1da3d9428f28644d0;hb=46990564407e2402686022884767fc749a97d734;hp=909f7519f2be828a44b9647e1a32d39ee18e5693;hpb=44ef57f5e371159a7900fe8d50db1c84a66151cd;p=helm.git

diff --git a/matita/components/ng_refiner/nCicRefiner.ml b/matita/components/ng_refiner/nCicRefiner.ml
index 909f7519f..550c75e93 100644
--- 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 _ ->
@@ -139,6 +139,32 @@ let check_allowed_sort_elimination status localise r orig =
     aux
 ;;
 
+(* CSC: temporary thing, waiting for better times *)
+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
+  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 =
+  List.fold_left
+   (fun last (name,_) ->
+     if basename name = name' then
+      max last (suffix name)
+     else
+      last
+   ) (-1) context
+ in
+  name' ^ (if last = -1 then "" else string_of_int (last + 1))
+with exn -> prerr_endline ("XXX" ^ Printexc.to_string exn); assert false
+
 let rec typeof (status:#NCicCoercion.status)
   ?(localise=fun _ -> Stdpp.dummy_loc) 
   metasenv subst context term expty 
@@ -479,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)
@@ -819,13 +846,8 @@ and try_coercions status
         in
         metasenv, subst, t, expty (*}}}*)
     | _,`Type expty,NCic.LetIn(name,ty,t,bo) -> 
-        let rec mk_fresh_name ctx firstch n =
-          let candidate = (String.make 1 firstch) ^ (string_of_int n) in
-          if (List.for_all (fun (s,_) -> s <> candidate) ctx) then candidate
-          else mk_fresh_name ctx firstch (n+1)
-        in
         pp (lazy "LETIN");
-        let name' = mk_fresh_name context 'l' 0 in
+        let name' = mk_fresh_name context name in
         let context_bo = (name', NCic.Def (t,ty)) :: context in
         let metasenv, subst, bo2, _ = 
           try_coercions status ~localise metasenv subst context_bo
@@ -836,17 +858,10 @@ and try_coercions status
         pp (lazy ("LETIN: coerced = " ^ status#ppterm ~metasenv ~subst ~context coerced));
         metasenv, subst, coerced, expty
     | NCic.Prod (nameprod, src, ty),`Type (NCic.Prod (_, src2, ty2) as expty), _ -> 
-        let rec mk_fresh_name ctx firstch n =
-          let candidate = (String.make 1 firstch) ^ (string_of_int n) in
-          if (List.for_all (fun (s,_) -> s <> candidate) ctx) then candidate
-          else mk_fresh_name ctx firstch (n+1)
-        in
         (*{{{*) pp (lazy "LAM");
         pp (lazy ("LAM: t = " ^ status#ppterm ~metasenv ~subst ~context t));
-        let name_con = mk_fresh_name context 'c' 0
-          (*FreshNamesGenerator.mk_fresh_name 
-            ~subst metasenv context ~typ:src2 Cic.Anonymous*)
-        in
+        let namename = match t with NCic.Lambda (n,_,_) -> n | _ -> nameprod in
+        let name_con = mk_fresh_name context namename in
         let context_src2 = ((name_con, NCic.Decl src2) :: context) in
         (* contravariant part: the argument of f:src->ty *)
         let metasenv, subst, rel1, _ = 
@@ -895,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)