X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FfreshNamesGenerator.ml;fp=helm%2Focaml%2Fcic_unification%2FfreshNamesGenerator.ml;h=0000000000000000000000000000000000000000;hp=1a94c318599e2678e0898618d1fe40c254653d4b;hb=1696761e4b8576e8ed81caa905fd108717019226;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1

diff --git a/helm/ocaml/cic_unification/freshNamesGenerator.ml b/helm/ocaml/cic_unification/freshNamesGenerator.ml
deleted file mode 100644
index 1a94c3185..000000000
--- a/helm/ocaml/cic_unification/freshNamesGenerator.ml
+++ /dev/null
@@ -1,204 +0,0 @@
-(* 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 metasenv 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' metasenv 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
-;;
-
-(* clean_dummy_dependent_types term                             *)
-(* returns a copy of [term] where every dummy dependent product *)
-(* have been replaced with a non-dependent product and where    *)
-(* dummy let-ins have been removed.                             *)
-let clean_dummy_dependent_types t =
- let module C = Cic in
-  let rec aux k =
-   function
-      C.Rel m as t -> t,[k - m]
-    | C.Var (uri,exp_named_subst) ->
-       let exp_named_subst',rels = 
-        List.fold_right
-         (fun (uri,t) (exp_named_subst,rels) ->
-           let t',rels' = aux k t in
-            (uri,t')::exp_named_subst, rels' @ rels
-         ) exp_named_subst ([],[])
-       in
-        C.Var (uri,exp_named_subst'),rels
-    | C.Meta (i,l) ->
-       let l',rels =
-        List.fold_right
-         (fun t (l,rels) ->
-           let t',rels' =
-            match t with
-               None -> None,[]
-             | Some t ->
-                let t',rels' = aux k t in
-                 Some t', rels'
-           in
-            t'::l, rels' @ rels
-         ) l ([],[])
-       in
-        C.Meta(i,l'),rels
-    | C.Sort _ as t -> t,[]
-    | C.Implicit _ as t -> t,[]
-    | C.Cast (te,ty) ->
-       let te',rels1 = aux k te in
-       let ty',rels2 = aux k ty in
-        C.Cast (te', ty'), rels1@rels2
-    | C.Prod (n,s,t) ->
-       let s',rels1 = aux k s in
-       let t',rels2 = aux (k+1) t in
-        let n' =
-         match n with
-            C.Anonymous ->
-             if List.mem k rels2 then
-(
-              prerr_endline "If this happens often, we can do something about it (i.e. we can generate a new fresh name; problem: we need the metasenv and context ;-(. Alternative solution: mk_implicit does not generate entries for the elements in the context that have no name" ;
-              C.Anonymous
-)
-             else
-              C.Anonymous
-          | C.Name _ as n ->
-             if List.mem k rels2 then n else C.Anonymous
-        in
-         C.Prod (n', s', t'), rels1@rels2
-    | C.Lambda (n,s,t) ->
-       let s',rels1 = aux k s in
-       let t',rels2 = aux (k+1) t in
-        C.Lambda (n, s', t'), rels1@rels2
-    | C.LetIn (n,s,t) ->
-       let s',rels1 = aux k s in
-       let t',rels2 = aux (k+1) t in
-       let rels = rels1 @ rels2 in
-        if List.mem k rels2 then
-         C.LetIn (n, s', t'), rels
-        else
-         (* (C.Rel 1) is just a dummy term; any term would fit *)
-         CicSubstitution.subst (C.Rel 1) t', rels
-    | C.Appl l ->
-       let l',rels =
-        List.fold_right
-         (fun t (exp_named_subst,rels) ->
-           let t',rels' = aux k t in
-            t'::exp_named_subst, rels' @ rels
-         ) l ([],[])
-       in
-        C.Appl l', rels
-    | C.Const (uri,exp_named_subst) ->
-       let exp_named_subst',rels = 
-        List.fold_right
-         (fun (uri,t) (exp_named_subst,rels) ->
-           let t',rels' = aux k t in
-            (uri,t')::exp_named_subst, rels' @ rels
-         ) exp_named_subst ([],[])
-       in
-        C.Const (uri,exp_named_subst'),rels
-    | C.MutInd (uri,tyno,exp_named_subst) ->
-       let exp_named_subst',rels = 
-        List.fold_right
-         (fun (uri,t) (exp_named_subst,rels) ->
-           let t',rels' = aux k t in
-            (uri,t')::exp_named_subst, rels' @ rels
-         ) exp_named_subst ([],[])
-       in
-        C.MutInd (uri,tyno,exp_named_subst'),rels
-    | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
-       let exp_named_subst',rels = 
-        List.fold_right
-         (fun (uri,t) (exp_named_subst,rels) ->
-           let t',rels' = aux k t in
-            (uri,t')::exp_named_subst, rels' @ rels
-         ) exp_named_subst ([],[])
-       in
-        C.MutConstruct (uri,tyno,consno,exp_named_subst'),rels
-    | C.MutCase (sp,i,outty,t,pl) ->
-       let outty',rels1 = aux k outty in
-       let t',rels2 = aux k t in
-       let pl',rels3 =
-        List.fold_right
-         (fun t (exp_named_subst,rels) ->
-           let t',rels' = aux k t in
-            t'::exp_named_subst, rels' @ rels
-         ) pl ([],[])
-       in
-        C.MutCase (sp, i, outty', t', pl'), rels1 @ rels2 @rels3
-    | C.Fix (i, fl) ->
-       let len = List.length fl in
-       let fl',rels =
-        List.fold_right
-         (fun (name,i,ty,bo) (fl,rels) ->
-           let ty',rels1 = aux k ty in
-           let bo',rels2 = aux (k + len) bo in
-            (name,i,ty',bo')::fl, rels1 @ rels2 @ rels
-         ) fl ([],[])
-       in
-        C.Fix (i, fl'),rels
-    | C.CoFix (i, fl) ->
-       let len = List.length fl in
-       let fl',rels =
-        List.fold_right
-         (fun (name,ty,bo) (fl,rels) ->
-           let ty',rels1 = aux k ty in
-           let bo',rels2 = aux (k + len) bo in
-            (name,ty',bo')::fl, rels1 @ rels2 @ rels
-         ) fl ([],[])
-       in
-        C.CoFix (i, fl'),rels
-  in
-   fst (aux 0 t)
-;;