]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/cic_proof_checking/freshNamesGenerator.ml
- code cleanup, especialli in Indexing where all the goal related functions have
[helm.git] / helm / software / components / cic_proof_checking / freshNamesGenerator.ml
1 (* Copyright (C) 2004, HELM Team.
2  * 
3  * This file is part of HELM, an Hypertextual, Electronic
4  * Library of Mathematics, developed at the Computer Science
5  * Department, University of Bologna, Italy.
6  * 
7  * HELM is free software; you can redistribute it and/or
8  * modify it under the terms of the GNU General Public License
9  * as published by the Free Software Foundation; either version 2
10  * of the License, or (at your option) any later version.
11  * 
12  * HELM is distributed in the hope that it will be useful,
13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
15  * GNU General Public License for more details.
16  *
17  * You should have received a copy of the GNU General Public License
18  * along with HELM; if not, write to the Free Software
19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  *)
25
26 (* $Id$ *)
27
28 let debug_print = fun _ -> ()
29
30 let rec higher_name arity =
31   function 
32       Cic.Sort Cic.Prop
33     | Cic.Sort Cic.CProp -> 
34         if arity = 0 then "A" (* propositions *)
35         else if arity = 1 then "P" (* predicates *)
36         else "R" (*relations *)
37     | Cic.Sort Cic.Set
38         -> if arity = 0 then "S" else "F"
39     | Cic.Sort (Cic.Type _ ) -> 
40         if arity = 0 then "T" else "F"
41     | Cic.Prod (_,_,t) -> higher_name (arity+1) t
42     | _ -> "f"
43
44 let get_initial s = 
45    if String.length s = 0 then "_"
46    else 
47      let head = String.sub s 0 1 in
48      String.lowercase head
49
50 (* only used when the sort is not Prop or CProp *)
51 let rec guess_a_name context ty =
52   match ty with
53     Cic.Rel n ->  
54       (match List.nth context (n-1) with
55         None -> assert false
56       | Some (Cic.Anonymous,_) -> "eccomi_qua"
57       | Some (Cic.Name s,_) -> get_initial s)
58   | Cic.Var (uri,_) -> get_initial (UriManager.name_of_uri uri)
59   | Cic.Sort _ -> higher_name 0 ty
60   | Cic.Implicit _ -> assert false
61   | Cic.Cast (t1,t2) -> guess_a_name context t1
62   | Cic.Prod (na_,_,t) -> higher_name 1 t
63   | Cic.Lambda _ -> assert false                   
64   | Cic.LetIn (_,s,t) -> guess_a_name context (CicSubstitution.subst ~avoid_beta_redexes:true s t)
65   | Cic.Appl [] -> assert false
66   | Cic.Appl (he::_) -> guess_a_name context he 
67   | Cic.Const (uri,_)
68   | Cic.MutInd (uri,_,_)
69   | Cic.MutConstruct (uri,_,_,_) -> get_initial (UriManager.name_of_uri uri)  
70   | _ -> "x"
71
72 (* mk_fresh_name context name typ                      *)
73 (* returns an identifier which is fresh in the context *)
74 (* and that resembles [name] as much as possible.      *)
75 (* [typ] will be the type of the variable              *)
76 let mk_fresh_name ~subst metasenv context name ~typ =
77  let module C = Cic in
78   let basename =
79    match name with
80       C.Anonymous ->
81        (try
82         let ty,_ = 
83           CicTypeChecker.type_of_aux' ~subst metasenv context typ 
84             CicUniv.empty_ugraph in 
85          (match ty with
86              C.Sort C.Prop
87            | C.Sort C.CProp -> "H"
88            | _ -> guess_a_name context typ
89          )
90         with CicTypeChecker.TypeCheckerFailure _ -> "H"
91        )
92     | C.Name name ->
93        Str.global_replace (Str.regexp "[0-9]*$") "" name
94   in
95    let already_used name =
96     List.exists (function Some (n,_) -> n=name | _ -> false) context
97    in
98     if name <> C.Anonymous && not (already_used name) then
99      name
100     else if not (already_used (C.Name basename)) then
101      C.Name basename
102     else
103      let rec try_next n =
104       let name' = C.Name (basename ^ string_of_int n) in
105        if already_used name' then
106         try_next (n+1)
107        else
108         name'
109      in
110       try_next 1
111 ;;
112
113 (* let mk_fresh_names ~subst metasenv context t *)
114 let rec mk_fresh_names ~subst metasenv context t =
115   match t with
116     Cic.Rel _ -> t
117   | Cic.Var (uri,exp_named_subst) ->
118       let ens = 
119         List.map 
120           (fun (uri,t) ->
121             (uri,mk_fresh_names ~subst metasenv context t)) exp_named_subst in
122       Cic.Var (uri,ens)
123   | Cic.Meta (i,l) ->
124        let l' = 
125         List.map 
126          (fun t ->
127            match t with
128              None -> None
129            | Some t -> Some (mk_fresh_names ~subst metasenv context t)) l in
130        Cic.Meta(i,l')
131     | Cic.Sort _ 
132     | Cic.Implicit _ -> t
133     | Cic.Cast (te,ty) ->
134        let te' = mk_fresh_names ~subst metasenv context te in
135        let ty' = mk_fresh_names ~subst metasenv context ty in
136        Cic.Cast (te', ty')
137     | Cic.Prod (n,s,t) ->
138         let s' = mk_fresh_names ~subst metasenv context s in
139         let n' =
140           match n with
141             Cic.Anonymous -> Cic.Anonymous
142           | Cic.Name "matita_dummy" -> 
143               mk_fresh_name ~subst metasenv context Cic.Anonymous ~typ:s'
144           | _ -> n in 
145         let t' = mk_fresh_names ~subst metasenv (Some(n',Cic.Decl s')::context) t in
146         Cic.Prod (n',s',t')
147     | Cic.Lambda (n,s,t) ->
148         let s' = mk_fresh_names ~subst metasenv context s in
149         let n' =
150           match n with
151             Cic.Anonymous -> Cic.Anonymous
152           | Cic.Name "matita_dummy" -> 
153               mk_fresh_name ~subst metasenv context Cic.Anonymous ~typ:s' 
154           | _ -> n in 
155         let t' = mk_fresh_names ~subst metasenv (Some(n',Cic.Decl s')::context) t in
156         Cic.Lambda (n',s',t')
157     | Cic.LetIn (n,s,t) ->
158         let s' = mk_fresh_names ~subst metasenv context s in
159         let n' =
160           match n with
161             Cic.Anonymous -> Cic.Anonymous
162           | Cic.Name "matita_dummy" -> 
163               mk_fresh_name ~subst metasenv context Cic.Anonymous ~typ:s' 
164           | _ -> n in 
165         let t' = mk_fresh_names ~subst metasenv (Some(n',Cic.Def (s',None))::context) t in
166         Cic.LetIn (n',s',t')    
167     | Cic.Appl l ->
168         Cic.Appl (List.map (mk_fresh_names ~subst metasenv context) l)
169     | Cic.Const (uri,exp_named_subst) ->
170         let ens = 
171           List.map 
172             (fun (uri,t) ->
173               (uri,mk_fresh_names ~subst metasenv context t)) exp_named_subst in
174         Cic.Const(uri,ens)
175     | Cic.MutInd (uri,tyno,exp_named_subst) ->
176         let ens = 
177           List.map 
178             (fun (uri,t) ->
179               (uri,mk_fresh_names ~subst metasenv context t)) exp_named_subst in
180         Cic.MutInd (uri,tyno,ens)
181     | Cic.MutConstruct (uri,tyno,consno,exp_named_subst) ->
182         let ens = 
183           List.map 
184             (fun (uri,t) ->
185               (uri,mk_fresh_names ~subst metasenv context t)) exp_named_subst in
186         Cic.MutConstruct (uri,tyno,consno, ens)
187     | Cic.MutCase (sp,i,outty,t,pl) ->
188        let outty' = mk_fresh_names ~subst metasenv context outty in
189        let t' = mk_fresh_names ~subst metasenv context t in
190        let pl' = List.map (mk_fresh_names ~subst metasenv context) pl in
191        Cic.MutCase (sp, i, outty', t', pl')
192     | Cic.Fix (i, fl) -> 
193         let tys = List.map 
194             (fun (n,_,ty,_) -> 
195               Some (Cic.Name n,(Cic.Decl ty))) fl in
196         let fl' = List.map 
197             (fun (n,i,ty,bo) -> 
198               let ty' = mk_fresh_names ~subst metasenv context ty in
199               let bo' = mk_fresh_names ~subst metasenv (tys@context) bo in
200               (n,i,ty',bo')) fl in
201         Cic.Fix (i, fl') 
202     | Cic.CoFix (i, fl) ->
203         let tys = List.map 
204             (fun (n,_,ty) -> 
205               Some (Cic.Name n,(Cic.Decl ty))) fl in
206         let fl' = List.map 
207             (fun (n,ty,bo) -> 
208               let ty' = mk_fresh_names ~subst metasenv context ty in
209               let bo' = mk_fresh_names ~subst metasenv (tys@context) bo in
210               (n,ty',bo')) fl in
211         Cic.CoFix (i, fl')      
212 ;;
213
214 (* clean_dummy_dependent_types term                             *)
215 (* returns a copy of [term] where every dummy dependent product *)
216 (* have been replaced with a non-dependent product and where    *)
217 (* dummy let-ins have been removed.                             *)
218 let clean_dummy_dependent_types t =
219  let module C = Cic in
220   let rec aux k =
221    function
222       C.Rel m as t -> t,[k - m]
223     | C.Var (uri,exp_named_subst) ->
224        let exp_named_subst',rels = 
225         List.fold_right
226          (fun (uri,t) (exp_named_subst,rels) ->
227            let t',rels' = aux k t in
228             (uri,t')::exp_named_subst, rels' @ rels
229          ) exp_named_subst ([],[])
230        in
231         C.Var (uri,exp_named_subst'),rels
232     | C.Meta (i,l) ->
233        let l',rels =
234         List.fold_right
235          (fun t (l,rels) ->
236            let t',rels' =
237             match t with
238                None -> None,[]
239              | Some t ->
240                 let t',rels' = aux k t in
241                  Some t', rels'
242            in
243             t'::l, rels' @ rels
244          ) l ([],[])
245        in
246         C.Meta(i,l'),rels
247     | C.Sort _ as t -> t,[]
248     | C.Implicit _ as t -> t,[]
249     | C.Cast (te,ty) ->
250        let te',rels1 = aux k te in
251        let ty',rels2 = aux k ty in
252         C.Cast (te', ty'), rels1@rels2
253     | C.Prod (n,s,t) ->
254        let s',rels1 = aux k s in
255        let t',rels2 = aux (k+1) t in
256         let n' =
257          match n with
258             C.Anonymous ->
259              if List.mem k rels2 then
260 (
261               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") ;
262               C.Anonymous
263 )
264              else
265               C.Anonymous
266           | C.Name _ as n ->
267              if List.mem k rels2 then n else C.Anonymous
268         in
269          C.Prod (n', s', t'), rels1@rels2
270     | C.Lambda (n,s,t) ->
271        let s',rels1 = aux k s in
272        let t',rels2 = aux (k+1) t in
273         C.Lambda (n, s', t'), rels1@rels2
274     | C.LetIn (n,s,t) ->
275        let s',rels1 = aux k s in
276        let t',rels2 = aux (k+1) t in
277        let rels = rels1 @ rels2 in
278         if List.mem k rels2 then
279          C.LetIn (n, s', t'), rels
280         else
281          (* (C.Rel 1) is just a dummy term; any term would fit *)
282          CicSubstitution.subst (C.Rel 1) t', rels
283     | C.Appl l ->
284        let l',rels =
285         List.fold_right
286          (fun t (exp_named_subst,rels) ->
287            let t',rels' = aux k t in
288             t'::exp_named_subst, rels' @ rels
289          ) l ([],[])
290        in
291         C.Appl l', rels
292     | C.Const (uri,exp_named_subst) ->
293        let exp_named_subst',rels = 
294         List.fold_right
295          (fun (uri,t) (exp_named_subst,rels) ->
296            let t',rels' = aux k t in
297             (uri,t')::exp_named_subst, rels' @ rels
298          ) exp_named_subst ([],[])
299        in
300         C.Const (uri,exp_named_subst'),rels
301     | C.MutInd (uri,tyno,exp_named_subst) ->
302        let exp_named_subst',rels = 
303         List.fold_right
304          (fun (uri,t) (exp_named_subst,rels) ->
305            let t',rels' = aux k t in
306             (uri,t')::exp_named_subst, rels' @ rels
307          ) exp_named_subst ([],[])
308        in
309         C.MutInd (uri,tyno,exp_named_subst'),rels
310     | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
311        let exp_named_subst',rels = 
312         List.fold_right
313          (fun (uri,t) (exp_named_subst,rels) ->
314            let t',rels' = aux k t in
315             (uri,t')::exp_named_subst, rels' @ rels
316          ) exp_named_subst ([],[])
317        in
318         C.MutConstruct (uri,tyno,consno,exp_named_subst'),rels
319     | C.MutCase (sp,i,outty,t,pl) ->
320        let outty',rels1 = aux k outty in
321        let t',rels2 = aux k t in
322        let pl',rels3 =
323         List.fold_right
324          (fun t (exp_named_subst,rels) ->
325            let t',rels' = aux k t in
326             t'::exp_named_subst, rels' @ rels
327          ) pl ([],[])
328        in
329         C.MutCase (sp, i, outty', t', pl'), rels1 @ rels2 @rels3
330     | C.Fix (i, fl) ->
331        let len = List.length fl in
332        let fl',rels =
333         List.fold_right
334          (fun (name,i,ty,bo) (fl,rels) ->
335            let ty',rels1 = aux k ty in
336            let bo',rels2 = aux (k + len) bo in
337             (name,i,ty',bo')::fl, rels1 @ rels2 @ rels
338          ) fl ([],[])
339        in
340         C.Fix (i, fl'),rels
341     | C.CoFix (i, fl) ->
342        let len = List.length fl in
343        let fl',rels =
344         List.fold_right
345          (fun (name,ty,bo) (fl,rels) ->
346            let ty',rels1 = aux k ty in
347            let bo',rels2 = aux (k + len) bo in
348             (name,ty',bo')::fl, rels1 @ rels2 @ rels
349          ) fl ([],[])
350        in
351         C.CoFix (i, fl'),rels
352   in
353    fst (aux 0 t)
354 ;;