1 (* Copyright (C) 2004, HELM Team.
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.
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.
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.
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,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
28 let debug_print = fun _ -> ()
30 let rec higher_name arity =
33 | Cic.Sort Cic.CProp ->
34 if arity = 0 then "A" (* propositions *)
35 else if arity = 1 then "P" (* predicates *)
36 else "R" (*relations *)
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
45 if String.length s = 0 then "_"
47 let head = String.sub s 0 1 in
50 (* only used when the sort is not Prop or CProp *)
51 let rec guess_a_name context ty =
54 (match List.nth context (n-1) with
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
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
70 | Cic.MutInd (uri,_,_)
71 | Cic.MutConstruct (uri,_,_,_) -> get_initial (UriManager.name_of_uri uri)
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 =
85 CicTypeChecker.type_of_aux' ~subst metasenv context typ
86 CicUniv.oblivion_ugraph
90 | C.Sort C.CProp -> "H"
91 | _ -> guess_a_name context typ
93 with CicTypeChecker.TypeCheckerFailure _ -> "H"
96 Str.global_replace (Str.regexp "[0-9]*$") "" name
98 let already_used name =
99 List.exists (function Some (n,_) -> n=name | _ -> false) context
101 if name <> C.Anonymous && not (already_used name) then
103 else if not (already_used (C.Name basename)) then
107 let name' = C.Name (basename ^ string_of_int n) in
108 if already_used name' then
116 (* let mk_fresh_names ~subst metasenv context t *)
117 let rec mk_fresh_names ~subst metasenv context t =
120 | Cic.Var (uri,exp_named_subst) ->
124 (uri,mk_fresh_names ~subst metasenv context t)) exp_named_subst in
132 | Some t -> Some (mk_fresh_names ~subst metasenv context t)) l in
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
140 | Cic.Prod (n,s,t) ->
141 let s' = mk_fresh_names ~subst metasenv context s in
144 Cic.Anonymous -> Cic.Anonymous
145 | Cic.Name "matita_dummy" ->
146 mk_fresh_name ~subst metasenv context Cic.Anonymous ~typ:s'
148 let t' = mk_fresh_names ~subst metasenv (Some(n',Cic.Decl s')::context) t in
150 | Cic.Lambda (n,s,t) ->
151 let s' = mk_fresh_names ~subst metasenv context s in
154 Cic.Anonymous -> Cic.Anonymous
155 | Cic.Name "matita_dummy" ->
156 mk_fresh_name ~subst metasenv context Cic.Anonymous ~typ:s'
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,t) ->
161 let s' = mk_fresh_names ~subst metasenv context s in
164 Cic.Anonymous -> Cic.Anonymous
165 | Cic.Name "matita_dummy" ->
166 mk_fresh_name ~subst metasenv context Cic.Anonymous ~typ:s'
168 let t' = mk_fresh_names ~subst metasenv (Some(n',Cic.Def (s',None))::context) t in
171 Cic.Appl (List.map (mk_fresh_names ~subst metasenv context) l)
172 | Cic.Const (uri,exp_named_subst) ->
176 (uri,mk_fresh_names ~subst metasenv context t)) exp_named_subst in
178 | Cic.MutInd (uri,tyno,exp_named_subst) ->
182 (uri,mk_fresh_names ~subst metasenv context t)) exp_named_subst in
183 Cic.MutInd (uri,tyno,ens)
184 | Cic.MutConstruct (uri,tyno,consno,exp_named_subst) ->
188 (uri,mk_fresh_names ~subst metasenv context t)) exp_named_subst in
189 Cic.MutConstruct (uri,tyno,consno, ens)
190 | Cic.MutCase (sp,i,outty,t,pl) ->
191 let outty' = mk_fresh_names ~subst metasenv context outty in
192 let t' = mk_fresh_names ~subst metasenv context t in
193 let pl' = List.map (mk_fresh_names ~subst metasenv context) pl in
194 Cic.MutCase (sp, i, outty', t', pl')
198 Some (Cic.Name n,(Cic.Decl ty))) fl in
201 let ty' = mk_fresh_names ~subst metasenv context ty in
202 let bo' = mk_fresh_names ~subst metasenv (tys@context) bo in
205 | Cic.CoFix (i, fl) ->
208 Some (Cic.Name n,(Cic.Decl ty))) fl in
211 let ty' = mk_fresh_names ~subst metasenv context ty in
212 let bo' = mk_fresh_names ~subst metasenv (tys@context) bo in
217 (* clean_dummy_dependent_types term *)
218 (* returns a copy of [term] where every dummy dependent product *)
219 (* have been replaced with a non-dependent product and where *)
220 (* dummy let-ins have been removed. *)
221 let clean_dummy_dependent_types t =
222 let module C = Cic in
225 C.Rel m as t -> t,[k - m]
226 | C.Var (uri,exp_named_subst) ->
227 let exp_named_subst',rels =
229 (fun (uri,t) (exp_named_subst,rels) ->
230 let t',rels' = aux k t in
231 (uri,t')::exp_named_subst, rels' @ rels
232 ) exp_named_subst ([],[])
234 C.Var (uri,exp_named_subst'),rels
243 let t',rels' = aux k t in
250 | C.Sort _ as t -> t,[]
251 | C.Implicit _ as t -> t,[]
253 let te',rels1 = aux k te in
254 let ty',rels2 = aux k ty in
255 C.Cast (te', ty'), rels1@rels2
257 let s',rels1 = aux k s in
258 let t',rels2 = aux (k+1) t in
262 if List.mem k rels2 then
264 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") ;
270 if List.mem k rels2 then n else C.Anonymous
272 C.Prod (n', s', t'), rels1@rels2
273 | C.Lambda (n,s,t) ->
274 let s',rels1 = aux k s in
275 let t',rels2 = aux (k+1) t in
276 C.Lambda (n, s', t'), rels1@rels2
278 let s',rels1 = aux k s in
279 let t',rels2 = aux (k+1) t in
280 let rels = rels1 @ rels2 in
281 if List.mem k rels2 then
282 C.LetIn (n, s', t'), rels
284 (* (C.Rel 1) is just a dummy term; any term would fit *)
285 CicSubstitution.subst (C.Rel 1) t', rels
289 (fun t (exp_named_subst,rels) ->
290 let t',rels' = aux k t in
291 t'::exp_named_subst, rels' @ rels
295 | C.Const (uri,exp_named_subst) ->
296 let exp_named_subst',rels =
298 (fun (uri,t) (exp_named_subst,rels) ->
299 let t',rels' = aux k t in
300 (uri,t')::exp_named_subst, rels' @ rels
301 ) exp_named_subst ([],[])
303 C.Const (uri,exp_named_subst'),rels
304 | C.MutInd (uri,tyno,exp_named_subst) ->
305 let exp_named_subst',rels =
307 (fun (uri,t) (exp_named_subst,rels) ->
308 let t',rels' = aux k t in
309 (uri,t')::exp_named_subst, rels' @ rels
310 ) exp_named_subst ([],[])
312 C.MutInd (uri,tyno,exp_named_subst'),rels
313 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
314 let exp_named_subst',rels =
316 (fun (uri,t) (exp_named_subst,rels) ->
317 let t',rels' = aux k t in
318 (uri,t')::exp_named_subst, rels' @ rels
319 ) exp_named_subst ([],[])
321 C.MutConstruct (uri,tyno,consno,exp_named_subst'),rels
322 | C.MutCase (sp,i,outty,t,pl) ->
323 let outty',rels1 = aux k outty in
324 let t',rels2 = aux k t in
327 (fun t (exp_named_subst,rels) ->
328 let t',rels' = aux k t in
329 t'::exp_named_subst, rels' @ rels
332 C.MutCase (sp, i, outty', t', pl'), rels1 @ rels2 @rels3
334 let len = List.length fl in
337 (fun (name,i,ty,bo) (fl,rels) ->
338 let ty',rels1 = aux k ty in
339 let bo',rels2 = aux (k + len) bo in
340 (name,i,ty',bo')::fl, rels1 @ rels2 @ rels
345 let len = List.length fl in
348 (fun (name,ty,bo) (fl,rels) ->
349 let ty',rels1 = aux k ty in
350 let bo',rels2 = aux (k + len) bo in
351 (name,ty',bo')::fl, rels1 @ rels2 @ rels
354 C.CoFix (i, fl'),rels