mk_fresh_name moved to FreshNamesGenerator.

[helm.git] / helm / ocaml / cic_unification / freshNamesGenerator.ml

diff --git a/helm/ocaml/cic_unification/freshNamesGenerator.ml b/helm/ocaml/cic_unification/freshNamesGenerator.ml
new file mode 100644 (file)
index 0000000..3f0006a
--- /dev/null
+++ b/helm/ocaml/cic_unification/freshNamesGenerator.ml
@@ -0,0 +1,62 @@
+(* Copyright (C) 2004, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* 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
+           | C.Sort C.CProp -> "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
+;;