X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_refiner%2FnCicRefiner.ml;h=a59a6fd359109202b3c8aed7c39efcaf1c6e3339;hb=da71c09b8f4a42d3273fcbaea0cda3bceed1d949;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..a59a6fd35 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 
@@ -819,13 +845,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 +857,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 +909,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 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)