]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/cic_proof_checking/freshNamesGenerator.ml
short names
[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 (* warning: on appl we should beta reduce before the recursive call
64   | Cic.Lambda _ -> assert false   
65 *)
66   | Cic.LetIn (_,s,_,t) -> guess_a_name context (CicSubstitution.subst ~avoid_beta_redexes:true s t)
67   | Cic.Appl [] -> assert false
68   | Cic.Appl (he::_) -> guess_a_name context he 
69   | Cic.Const (uri,_)
70   | Cic.MutInd (uri,_,_)
71   | Cic.MutConstruct (uri,_,_,_) -> get_initial (UriManager.name_of_uri uri)  
72   | _ -> "x"
73
74 (* mk_fresh_name context name typ                      *)
75 (* returns an identifier which is fresh in the context *)
76 (* and that resembles [name] as much as possible.      *)
77 (* [typ] will be the type of the variable              *)
78 let mk_fresh_name ~subst metasenv context name ~typ =
79  let module C = Cic in
80   let basename =
81    match name with
82       C.Anonymous ->
83        (try
84         let ty,_ = 
85           CicTypeChecker.type_of_aux' ~subst metasenv context typ 
86             CicUniv.oblivion_ugraph 
87         in 
88          (match ty with
89              C.Sort C.Prop
90            | C.Sort (C.CProp _) -> "H"
91            | _ -> guess_a_name context typ
92          )
93         with CicTypeChecker.TypeCheckerFailure _ -> "H"
94        )
95     | C.Name name ->
96        Str.global_replace (Str.regexp "[0-9']*$") "" name
97   in
98    let already_used name =
99     List.exists (function Some (n,_) -> n=name | _ -> false) context
100    in
101     if name <> C.Anonymous && not (already_used name) then
102      name
103     else if not (already_used (C.Name basename)) then
104      C.Name basename
105     else
106      let rec try_next n =
107       let name' = C.Name (basename ^ string_of_int n) in
108        if already_used name' then
109         try_next (n+1)
110        else
111         name'
112      in
113       try_next 1
114 ;;
115
116 (* let mk_fresh_names ~subst metasenv context t *)
117 let rec mk_fresh_names ~subst metasenv context t =
118   match t with
119     Cic.Rel _ -> t
120   | Cic.Var (uri,exp_named_subst) ->
121       let ens = 
122         List.map 
123           (fun (uri,t) ->
124             (uri,mk_fresh_names ~subst metasenv context t)) exp_named_subst in
125       Cic.Var (uri,ens)
126   | Cic.Meta (i,l) ->
127        let l' = 
128         List.map 
129          (fun t ->
130            match t with
131              None -> None
132            | Some t -> Some (mk_fresh_names ~subst metasenv context t)) l in
133        Cic.Meta(i,l')
134     | Cic.Sort _ 
135     | Cic.Implicit _ -> t
136     | Cic.Cast (te,ty) ->
137        let te' = mk_fresh_names ~subst metasenv context te in
138        let ty' = mk_fresh_names ~subst metasenv context ty in
139        Cic.Cast (te', ty')
140     | Cic.Prod (n,s,t) ->
141         let s' = mk_fresh_names ~subst metasenv context s in
142         let n' =
143           match n with
144             Cic.Anonymous -> Cic.Anonymous
145           | Cic.Name "matita_dummy" -> 
146               mk_fresh_name ~subst metasenv context Cic.Anonymous ~typ:s'
147           | _ -> n in 
148         let t' = mk_fresh_names ~subst metasenv (Some(n',Cic.Decl s')::context) t in
149         Cic.Prod (n',s',t')
150     | Cic.Lambda (n,s,t) ->
151         let s' = mk_fresh_names ~subst metasenv context s in
152         let n' =
153           match n with
154             Cic.Anonymous -> Cic.Anonymous
155           | Cic.Name "matita_dummy" -> 
156               mk_fresh_name ~subst metasenv context Cic.Anonymous ~typ:s' 
157           | _ -> n in 
158         let t' = mk_fresh_names ~subst metasenv (Some(n',Cic.Decl s')::context) t in
159         Cic.Lambda (n',s',t')
160     | Cic.LetIn (n,s,ty,t) ->
161         let s' = mk_fresh_names ~subst metasenv context s in
162         let ty' = mk_fresh_names ~subst metasenv context ty in
163         let n' =
164           match n with
165             Cic.Anonymous -> Cic.Anonymous
166           | Cic.Name "matita_dummy" -> 
167               mk_fresh_name ~subst metasenv context Cic.Anonymous ~typ:s' 
168           | _ -> n in 
169         let t' = mk_fresh_names ~subst metasenv (Some(n',Cic.Def (s',ty'))::context) t in
170         Cic.LetIn (n',s',ty',t')        
171     | Cic.Appl l ->
172         Cic.Appl (List.map (mk_fresh_names ~subst metasenv context) l)
173     | Cic.Const (uri,exp_named_subst) ->
174         let ens = 
175           List.map 
176             (fun (uri,t) ->
177               (uri,mk_fresh_names ~subst metasenv context t)) exp_named_subst in
178         Cic.Const(uri,ens)
179     | Cic.MutInd (uri,tyno,exp_named_subst) ->
180         let ens = 
181           List.map 
182             (fun (uri,t) ->
183               (uri,mk_fresh_names ~subst metasenv context t)) exp_named_subst in
184         Cic.MutInd (uri,tyno,ens)
185     | Cic.MutConstruct (uri,tyno,consno,exp_named_subst) ->
186         let ens = 
187           List.map 
188             (fun (uri,t) ->
189               (uri,mk_fresh_names ~subst metasenv context t)) exp_named_subst in
190         Cic.MutConstruct (uri,tyno,consno, ens)
191     | Cic.MutCase (sp,i,outty,t,pl) ->
192        let outty' = mk_fresh_names ~subst metasenv context outty in
193        let t' = mk_fresh_names ~subst metasenv context t in
194        let pl' = List.map (mk_fresh_names ~subst metasenv context) pl in
195        Cic.MutCase (sp, i, outty', t', pl')
196     | Cic.Fix (i, fl) -> 
197         let tys,_ =
198           List.fold_left
199             (fun (types,len) (n,_,ty,_) ->
200                (Some (Cic.Name n,(Cic.Decl (CicSubstitution.lift len ty)))::types,
201                 len+1)
202             ) ([],0) fl
203         in
204         let fl' = List.map 
205             (fun (n,i,ty,bo) -> 
206               let ty' = mk_fresh_names ~subst metasenv context ty in
207               let bo' = mk_fresh_names ~subst metasenv (tys@context) bo in
208               (n,i,ty',bo')) fl in
209         Cic.Fix (i, fl') 
210     | Cic.CoFix (i, fl) ->
211         let tys,_ =
212           List.fold_left
213             (fun (types,len) (n,ty,_) ->
214                (Some (Cic.Name n,(Cic.Decl (CicSubstitution.lift len ty)))::types,
215                 len+1)
216             ) ([],0) fl
217         in
218         let fl' = List.map 
219             (fun (n,ty,bo) -> 
220               let ty' = mk_fresh_names ~subst metasenv context ty in
221               let bo' = mk_fresh_names ~subst metasenv (tys@context) bo in
222               (n,ty',bo')) fl in
223         Cic.CoFix (i, fl')      
224 ;;
225
226 (* clean_dummy_dependent_types term                             *)
227 (* returns a copy of [term] where every dummy dependent product *)
228 (* have been replaced with a non-dependent product and where    *)
229 (* dummy let-ins have been removed.                             *)
230 let clean_dummy_dependent_types t =
231  let module C = Cic in
232   let rec aux k =
233    function
234       C.Rel m as t -> t,[k - m]
235     | C.Var (uri,exp_named_subst) ->
236        let exp_named_subst',rels = 
237         List.fold_right
238          (fun (uri,t) (exp_named_subst,rels) ->
239            let t',rels' = aux k t in
240             (uri,t')::exp_named_subst, rels' @ rels
241          ) exp_named_subst ([],[])
242        in
243         C.Var (uri,exp_named_subst'),rels
244     | C.Meta (i,l) ->
245        let l',rels =
246         List.fold_right
247          (fun t (l,rels) ->
248            let t',rels' =
249             match t with
250                None -> None,[]
251              | Some t ->
252                 let t',rels' = aux k t in
253                  Some t', rels'
254            in
255             t'::l, rels' @ rels
256          ) l ([],[])
257        in
258         C.Meta(i,l'),rels
259     | C.Sort _ as t -> t,[]
260     | C.Implicit _ as t -> t,[]
261     | C.Cast (te,ty) ->
262        let te',rels1 = aux k te in
263        let ty',rels2 = aux k ty in
264         C.Cast (te', ty'), rels1@rels2
265     | C.Prod (n,s,t) ->
266        let s',rels1 = aux k s in
267        let t',rels2 = aux (k+1) t in
268         let n' =
269          match n with
270             C.Anonymous ->
271              if List.mem k rels2 then
272 (
273               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") ;
274               C.Anonymous
275 )
276              else
277               C.Anonymous
278           | C.Name _ as n ->
279              if List.mem k rels2 then n else C.Anonymous
280         in
281          C.Prod (n', s', t'), rels1@rels2
282     | C.Lambda (n,s,t) ->
283        let s',rels1 = aux k s in
284        let t',rels2 = aux (k+1) t in
285         C.Lambda (n, s', t'), rels1@rels2
286     | C.LetIn (n,s,ty,t) ->
287        let s',rels1 = aux k s in
288        let ty',rels2 = aux k ty in
289        let t',rels3 = aux (k+1) t in
290        let rels = rels1 @ rels2 @ rels3 in
291         if List.mem k rels3 then
292          C.LetIn (n, s', ty', t'), rels
293         else
294          (* (C.Rel 1) is just a dummy term; any term would fit *)
295          CicSubstitution.subst (C.Rel 1) t', rels
296     | C.Appl l ->
297        let l',rels =
298         List.fold_right
299          (fun t (exp_named_subst,rels) ->
300            let t',rels' = aux k t in
301             t'::exp_named_subst, rels' @ rels
302          ) l ([],[])
303        in
304         C.Appl l', rels
305     | C.Const (uri,exp_named_subst) ->
306        let exp_named_subst',rels = 
307         List.fold_right
308          (fun (uri,t) (exp_named_subst,rels) ->
309            let t',rels' = aux k t in
310             (uri,t')::exp_named_subst, rels' @ rels
311          ) exp_named_subst ([],[])
312        in
313         C.Const (uri,exp_named_subst'),rels
314     | C.MutInd (uri,tyno,exp_named_subst) ->
315        let exp_named_subst',rels = 
316         List.fold_right
317          (fun (uri,t) (exp_named_subst,rels) ->
318            let t',rels' = aux k t in
319             (uri,t')::exp_named_subst, rels' @ rels
320          ) exp_named_subst ([],[])
321        in
322         C.MutInd (uri,tyno,exp_named_subst'),rels
323     | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
324        let exp_named_subst',rels = 
325         List.fold_right
326          (fun (uri,t) (exp_named_subst,rels) ->
327            let t',rels' = aux k t in
328             (uri,t')::exp_named_subst, rels' @ rels
329          ) exp_named_subst ([],[])
330        in
331         C.MutConstruct (uri,tyno,consno,exp_named_subst'),rels
332     | C.MutCase (sp,i,outty,t,pl) ->
333        let outty',rels1 = aux k outty in
334        let t',rels2 = aux k t in
335        let pl',rels3 =
336         List.fold_right
337          (fun t (exp_named_subst,rels) ->
338            let t',rels' = aux k t in
339             t'::exp_named_subst, rels' @ rels
340          ) pl ([],[])
341        in
342         C.MutCase (sp, i, outty', t', pl'), rels1 @ rels2 @rels3
343     | C.Fix (i, fl) ->
344        let len = List.length fl in
345        let fl',rels =
346         List.fold_right
347          (fun (name,i,ty,bo) (fl,rels) ->
348            let ty',rels1 = aux k ty in
349            let bo',rels2 = aux (k + len) bo in
350             (name,i,ty',bo')::fl, rels1 @ rels2 @ rels
351          ) fl ([],[])
352        in
353         C.Fix (i, fl'),rels
354     | C.CoFix (i, fl) ->
355        let len = List.length fl in
356        let fl',rels =
357         List.fold_right
358          (fun (name,ty,bo) (fl,rels) ->
359            let ty',rels1 = aux k ty in
360            let bo',rels2 = aux (k + len) bo in
361             (name,ty',bo')::fl, rels1 @ rels2 @ rels
362          ) fl ([],[])
363        in
364         C.CoFix (i, fl'),rels
365   in
366    fst (aux 0 t)
367 ;;