Removed several try .... with _ -> (which make thread killing impossible ;-((

[helm.git] / helm / ocaml / tactics / proofEngineHelpers.ml

diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index 74b6fcdaca1f344032da1afc7df9c393f30f9206..16be77edb443c84c3c7845182564dacfb1601cce 100644 (file)
--- a/helm/ocaml/tactics/proofEngineHelpers.ml
+++ b/helm/ocaml/tactics/proofEngineHelpers.ml
@@ -23,16 +23,42 @@
  * http://cs.unibo.it/helm/.
  *)
 
-(*CSC: generatore di nomi? Chiedere il nome? *)
-let fresh_name =
- let next_fresh_index = ref 0 in
-  function
-     Cic.Anonymous ->
-      incr next_fresh_index ;
-      "fresh_name" ^ string_of_int !next_fresh_index
-   | Cic.Name name ->
-      incr next_fresh_index ;
-      name ^ string_of_int !next_fresh_index
+(* mk_fresh_name context name typ                      *)
+(* returns an identifier which is fresh in the context *)
+(* and that resembles [name] as much as possible.      *)
+(* [typ] will be the type of the variable              *)
+let mk_fresh_name context name ~typ =
+ let module C = Cic in
+  let basename =
+   match name with
+      C.Anonymous ->
+       (*CSC: great space for improvements here *)
+       (try
+         (match CicTypeChecker.type_of_aux' [] context typ with
+             C.Sort C.Prop -> "H"
+           | C.Sort C.Set -> "x"
+           | _ -> "H"
+         )
+        with CicTypeChecker.TypeCheckerFailure _ -> "H"
+       )
+    | C.Name name ->
+       Str.global_replace (Str.regexp "[0-9]*$") "" name
+  in
+   let already_used name =
+    List.exists (function Some (C.Name n,_) -> n=name | _ -> false) context
+   in
+    if not (already_used basename) then
+     C.Name basename
+    else
+     let rec try_next n =
+      let name' = basename ^ string_of_int n in
+       if already_used name' then
+        try_next (n+1)
+       else
+        C.Name name'
+     in
+      try_next 1
+;;
 
 (* identity_relocation_list_for_metavariable i canonical_context         *)
 (* returns the identity relocation list, which is the list [1 ; ... ; n] *)