X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FfreshNamesGenerator.ml;fp=helm%2Focaml%2Fcic_proof_checking%2FfreshNamesGenerator.ml;h=99c9e4d76c9d93f51e070fce5aca31487c6099af;hp=0000000000000000000000000000000000000000;hb=792b5d29ebae8f917043d9dd226692919b5d6ca1;hpb=a14a8c7637fd0b95e9d4deccb20c6abc98e8f953

diff --git a/helm/ocaml/cic_proof_checking/freshNamesGenerator.ml b/helm/ocaml/cic_proof_checking/freshNamesGenerator.ml
new file mode 100755
index 000000000..99c9e4d76
--- /dev/null
+++ b/helm/ocaml/cic_proof_checking/freshNamesGenerator.ml
@@ -0,0 +1,354 @@
+(* 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/.
+ *)
+
+(* $Id$ *)
+
+let debug_print = fun _ -> ()
+
+let rec higher_name arity =
+  function 
+      Cic.Sort Cic.Prop
+    | Cic.Sort Cic.CProp -> 
+	if arity = 0 then "A" (* propositions *)
+	else if arity = 1 then "P" (* predicates *)
+	else "R" (*relations *)
+    | Cic.Sort Cic.Set
+	-> if arity = 0 then "S" else "F"
+    | Cic.Sort (Cic.Type _ ) -> 
+	if arity = 0 then "T" else "F"
+    | Cic.Prod (_,_,t) -> higher_name (arity+1) t
+    | _ -> "f"
+
+let get_initial s = 
+   if String.length s = 0 then "_"
+   else 
+     let head = String.sub s 0 1 in
+     String.lowercase head
+
+(* only used when the sort is not Prop or CProp *)
+let rec guess_a_name context ty =
+  match ty with
+    Cic.Rel n ->  
+      (match List.nth context (n-1) with
+	None -> assert false
+      | Some (Cic.Anonymous,_) -> "eccomi_qua"
+      | Some (Cic.Name s,_) -> get_initial s)
+  | Cic.Var (uri,_) -> get_initial (UriManager.name_of_uri uri)
+  | Cic.Sort _ -> higher_name 0 ty
+  | Cic.Implicit _ -> assert false
+  | Cic.Cast (t1,t2) -> guess_a_name context t1
+  | Cic.Prod (na_,_,t) -> higher_name 1 t
+  | Cic.Lambda _ -> assert false                   
+  | Cic.LetIn (_,s,t) -> guess_a_name context (CicSubstitution.subst s t)
+  | Cic.Appl [] -> assert false
+  | Cic.Appl (he::_) -> guess_a_name context he 
+  | Cic.Const (uri,_)
+  | Cic.MutInd (uri,_,_)
+  | Cic.MutConstruct (uri,_,_,_) -> get_initial (UriManager.name_of_uri uri)  
+  | _ -> "x"
+
+(* 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 ~subst metasenv context name ~typ =
+ let module C = Cic in
+  let basename =
+   match name with
+      C.Anonymous ->
+       (try
+        let ty,_ = 
+          CicTypeChecker.type_of_aux' ~subst metasenv context typ 
+            CicUniv.empty_ugraph in 
+         (match ty with
+             C.Sort C.Prop
+           | C.Sort C.CProp -> "H"
+           | _ -> guess_a_name context typ
+         )
+        with CicTypeChecker.TypeCheckerFailure _ -> "H"
+       )
+    | C.Name name ->
+       Str.global_replace (Str.regexp "[0-9]*$") "" name
+  in
+   let already_used name =
+    List.exists (function Some (n,_) -> n=name | _ -> false) context
+   in
+    if name <> C.Anonymous && not (already_used name) then
+     name
+    else if not (already_used (C.Name basename)) then
+     C.Name basename
+    else
+     let rec try_next n =
+      let name' = C.Name (basename ^ string_of_int n) in
+       if already_used name' then
+        try_next (n+1)
+       else
+        name'
+     in
+      try_next 1
+;;
+
+(* let mk_fresh_names ~subst metasenv context t *)
+let rec mk_fresh_names ~subst metasenv context t =
+  match t with
+    Cic.Rel _ -> t
+  | Cic.Var (uri,exp_named_subst) ->
+      let ens = 
+	List.map 
+	  (fun (uri,t) ->
+	    (uri,mk_fresh_names ~subst metasenv context t)) exp_named_subst in
+      Cic.Var (uri,ens)
+  | Cic.Meta (i,l) ->
+       let l' = 
+        List.map 
+         (fun t ->
+           match t with
+             None -> None
+           | Some t -> Some (mk_fresh_names ~subst metasenv context t)) l in
+       Cic.Meta(i,l')
+    | Cic.Sort _ 
+    | Cic.Implicit _ -> t
+    | Cic.Cast (te,ty) ->
+       let te' = mk_fresh_names ~subst metasenv context te in
+       let ty' = mk_fresh_names ~subst metasenv context ty in
+       Cic.Cast (te', ty')
+    | Cic.Prod (n,s,t) ->
+	let s' = mk_fresh_names ~subst metasenv context s in
+	let n' =
+	  match n with
+	    Cic.Anonymous -> Cic.Anonymous
+	  | Cic.Name "matita_dummy" -> 
+	      mk_fresh_name ~subst metasenv context Cic.Anonymous ~typ:s'
+	  | _ -> n in 
+	let t' = mk_fresh_names ~subst metasenv (Some(n',Cic.Decl s')::context) t in
+	Cic.Prod (n',s',t')
+    | Cic.Lambda (n,s,t) ->
+	let s' = mk_fresh_names ~subst metasenv context s in
+	let n' =
+	  match n with
+	    Cic.Anonymous -> Cic.Anonymous
+	  | Cic.Name "matita_dummy" -> 
+	      mk_fresh_name ~subst metasenv context Cic.Anonymous ~typ:s' 
+	  | _ -> n in 
+	let t' = mk_fresh_names ~subst metasenv (Some(n',Cic.Decl s')::context) t in
+	Cic.Lambda (n',s',t')
+    | Cic.LetIn (n,s,t) ->
+	let s' = mk_fresh_names ~subst metasenv context s in
+	let n' =
+	  match n with
+	    Cic.Anonymous -> Cic.Anonymous
+	  | Cic.Name "matita_dummy" -> 
+	      mk_fresh_name ~subst metasenv context Cic.Anonymous ~typ:s' 
+	  | _ -> n in 
+	let t' = mk_fresh_names ~subst metasenv (Some(n',Cic.Def (s',None))::context) t in
+	Cic.LetIn (n',s',t')	
+    | Cic.Appl l ->
+	Cic.Appl (List.map (mk_fresh_names ~subst metasenv context) l)
+    | Cic.Const (uri,exp_named_subst) ->
+        let ens = 
+	  List.map 
+	    (fun (uri,t) ->
+	      (uri,mk_fresh_names ~subst metasenv context t)) exp_named_subst in
+	Cic.Const(uri,ens)
+    | Cic.MutInd (uri,tyno,exp_named_subst) ->
+	let ens = 
+	  List.map 
+	    (fun (uri,t) ->
+	      (uri,mk_fresh_names ~subst metasenv context t)) exp_named_subst in
+        Cic.MutInd (uri,tyno,ens)
+    | Cic.MutConstruct (uri,tyno,consno,exp_named_subst) ->
+        let ens = 
+	  List.map 
+	    (fun (uri,t) ->
+	      (uri,mk_fresh_names ~subst metasenv context t)) exp_named_subst in
+        Cic.MutConstruct (uri,tyno,consno, ens)
+    | Cic.MutCase (sp,i,outty,t,pl) ->
+       let outty' = mk_fresh_names ~subst metasenv context outty in
+       let t' = mk_fresh_names ~subst metasenv context t in
+       let pl' = List.map (mk_fresh_names ~subst metasenv context) pl in
+       Cic.MutCase (sp, i, outty', t', pl')
+    | Cic.Fix (i, fl) -> 
+        let tys = List.map 
+	    (fun (n,_,ty,_) -> 
+	      Some (Cic.Name n,(Cic.Decl ty))) fl in
+	let fl' = List.map 
+	    (fun (n,i,ty,bo) -> 
+	      let ty' = mk_fresh_names ~subst metasenv context ty in
+	      let bo' = mk_fresh_names ~subst metasenv (tys@context) bo in
+	      (n,i,ty',bo')) fl in
+	Cic.Fix (i, fl') 
+    | Cic.CoFix (i, fl) ->
+	let tys = List.map 
+	    (fun (n,_,ty) -> 
+	      Some (Cic.Name n,(Cic.Decl ty))) fl in
+	let fl' = List.map 
+	    (fun (n,ty,bo) -> 
+	      let ty' = mk_fresh_names ~subst metasenv context ty in
+	      let bo' = mk_fresh_names ~subst metasenv (tys@context) bo in
+	      (n,ty',bo')) fl in
+	Cic.CoFix (i, fl') 	
+;;
+
+(* 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
+(
+              debug_print (lazy "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)
+;;