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/.
26 let debug_print = fun _ -> ()
28 let rec higher_name arity =
31 | Cic.Sort Cic.CProp ->
32 if arity = 0 then "A" (* propositions *)
33 else if arity = 1 then "P" (* predicates *)
34 else "R" (*relations *)
36 -> if arity = 0 then "S" else "F"
37 | Cic.Sort (Cic.Type _ ) ->
38 if arity = 0 then "T" else "F"
39 | Cic.Prod (_,_,t) -> higher_name (arity+1) t
43 if String.length s = 0 then "_"
45 let head = String.sub s 0 1 in
48 (* only used when the sort is not Prop or CProp *)
49 let rec guess_a_name context ty =
52 (match List.nth context (n-1) with
54 | Some (Cic.Anonymous,_) -> "eccomi_qua"
55 | Some (Cic.Name s,_) -> get_initial s)
56 | Cic.Var (uri,_) -> get_initial (UriManager.name_of_uri uri)
57 | Cic.Sort _ -> higher_name 0 ty
58 | Cic.Implicit _ -> assert false
59 | Cic.Cast (t1,t2) -> guess_a_name context t1
60 | Cic.Prod (na_,_,t) -> higher_name 1 t
61 | Cic.Lambda _ -> assert false
62 | Cic.LetIn (_,s,t) -> guess_a_name context (CicSubstitution.subst s t)
63 | Cic.Appl [] -> assert false
64 | Cic.Appl (he::_) -> guess_a_name context he
66 | Cic.MutInd (uri,_,_)
67 | Cic.MutConstruct (uri,_,_,_) -> get_initial (UriManager.name_of_uri uri)
70 (* mk_fresh_name context name typ *)
71 (* returns an identifier which is fresh in the context *)
72 (* and that resembles [name] as much as possible. *)
73 (* [typ] will be the type of the variable *)
74 let mk_fresh_name ~subst metasenv context name ~typ =
81 CicTypeChecker.type_of_aux' ~subst metasenv context typ
82 CicUniv.empty_ugraph in
85 | C.Sort C.CProp -> "H"
86 | _ -> guess_a_name context typ
88 with CicTypeChecker.TypeCheckerFailure _ -> "H"
91 Str.global_replace (Str.regexp "[0-9]*$") "" name
93 let already_used name =
94 List.exists (function Some (n,_) -> n=name | _ -> false) context
96 if name <> C.Anonymous && not (already_used name) then
98 else if not (already_used (C.Name basename)) then
102 let name' = C.Name (basename ^ string_of_int n) in
103 if already_used name' then
111 (* let mk_fresh_names ~subst metasenv context t *)
112 let rec mk_fresh_names ~subst metasenv context t =
115 | Cic.Var (uri,exp_named_subst) ->
119 (uri,mk_fresh_names ~subst metasenv context t)) exp_named_subst in
127 | Some t -> Some (mk_fresh_names ~subst metasenv context t)) l in
130 | Cic.Implicit _ -> t
131 | Cic.Cast (te,ty) ->
132 let te' = mk_fresh_names ~subst metasenv context te in
133 let ty' = mk_fresh_names ~subst metasenv context ty in
135 | Cic.Prod (n,s,t) ->
136 let s' = mk_fresh_names ~subst metasenv context s in
139 Cic.Anonymous -> Cic.Anonymous
140 | Cic.Name "matita_dummy" ->
141 mk_fresh_name ~subst metasenv context Cic.Anonymous ~typ:s'
143 let t' = mk_fresh_names ~subst metasenv (Some(n',Cic.Decl s')::context) t in
145 | Cic.Lambda (n,s,t) ->
146 let s' = mk_fresh_names ~subst metasenv context s in
149 Cic.Anonymous -> Cic.Anonymous
150 | Cic.Name "matita_dummy" ->
151 mk_fresh_name ~subst metasenv context Cic.Anonymous ~typ:s'
153 let t' = mk_fresh_names ~subst metasenv (Some(n',Cic.Decl s')::context) t in
154 Cic.Lambda (n',s',t')
155 | Cic.LetIn (n,s,t) ->
156 let s' = mk_fresh_names ~subst metasenv context s in
159 Cic.Anonymous -> Cic.Anonymous
160 | Cic.Name "matita_dummy" ->
161 mk_fresh_name ~subst metasenv context Cic.Anonymous ~typ:s'
163 let t' = mk_fresh_names ~subst metasenv (Some(n',Cic.Def (s',None))::context) t in
166 Cic.Appl (List.map (mk_fresh_names ~subst metasenv context) l)
167 | Cic.Const (uri,exp_named_subst) ->
171 (uri,mk_fresh_names ~subst metasenv context t)) exp_named_subst in
173 | Cic.MutInd (uri,tyno,exp_named_subst) ->
177 (uri,mk_fresh_names ~subst metasenv context t)) exp_named_subst in
178 Cic.MutInd (uri,tyno,ens)
179 | Cic.MutConstruct (uri,tyno,consno,exp_named_subst) ->
183 (uri,mk_fresh_names ~subst metasenv context t)) exp_named_subst in
184 Cic.MutConstruct (uri,tyno,consno, ens)
185 | Cic.MutCase (sp,i,outty,t,pl) ->
186 let outty' = mk_fresh_names ~subst metasenv context outty in
187 let t' = mk_fresh_names ~subst metasenv context t in
188 let pl' = List.map (mk_fresh_names ~subst metasenv context) pl in
189 Cic.MutCase (sp, i, outty', t', pl')
193 Some (Cic.Name n,(Cic.Decl ty))) fl in
196 let ty' = mk_fresh_names ~subst metasenv context ty in
197 let bo' = mk_fresh_names ~subst metasenv (tys@context) bo in
200 | Cic.CoFix (i, fl) ->
203 Some (Cic.Name n,(Cic.Decl ty))) fl in
206 let ty' = mk_fresh_names ~subst metasenv context ty in
207 let bo' = mk_fresh_names ~subst metasenv (tys@context) bo in
212 (* clean_dummy_dependent_types term *)
213 (* returns a copy of [term] where every dummy dependent product *)
214 (* have been replaced with a non-dependent product and where *)
215 (* dummy let-ins have been removed. *)
216 let clean_dummy_dependent_types t =
217 let module C = Cic in
220 C.Rel m as t -> t,[k - m]
221 | C.Var (uri,exp_named_subst) ->
222 let exp_named_subst',rels =
224 (fun (uri,t) (exp_named_subst,rels) ->
225 let t',rels' = aux k t in
226 (uri,t')::exp_named_subst, rels' @ rels
227 ) exp_named_subst ([],[])
229 C.Var (uri,exp_named_subst'),rels
238 let t',rels' = aux k t in
245 | C.Sort _ as t -> t,[]
246 | C.Implicit _ as t -> t,[]
248 let te',rels1 = aux k te in
249 let ty',rels2 = aux k ty in
250 C.Cast (te', ty'), rels1@rels2
252 let s',rels1 = aux k s in
253 let t',rels2 = aux (k+1) t in
257 if List.mem k rels2 then
259 debug_print "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" ;
265 if List.mem k rels2 then n else C.Anonymous
267 C.Prod (n', s', t'), rels1@rels2
268 | C.Lambda (n,s,t) ->
269 let s',rels1 = aux k s in
270 let t',rels2 = aux (k+1) t in
271 C.Lambda (n, s', t'), rels1@rels2
273 let s',rels1 = aux k s in
274 let t',rels2 = aux (k+1) t in
275 let rels = rels1 @ rels2 in
276 if List.mem k rels2 then
277 C.LetIn (n, s', t'), rels
279 (* (C.Rel 1) is just a dummy term; any term would fit *)
280 CicSubstitution.subst (C.Rel 1) t', rels
284 (fun t (exp_named_subst,rels) ->
285 let t',rels' = aux k t in
286 t'::exp_named_subst, rels' @ rels
290 | C.Const (uri,exp_named_subst) ->
291 let exp_named_subst',rels =
293 (fun (uri,t) (exp_named_subst,rels) ->
294 let t',rels' = aux k t in
295 (uri,t')::exp_named_subst, rels' @ rels
296 ) exp_named_subst ([],[])
298 C.Const (uri,exp_named_subst'),rels
299 | C.MutInd (uri,tyno,exp_named_subst) ->
300 let exp_named_subst',rels =
302 (fun (uri,t) (exp_named_subst,rels) ->
303 let t',rels' = aux k t in
304 (uri,t')::exp_named_subst, rels' @ rels
305 ) exp_named_subst ([],[])
307 C.MutInd (uri,tyno,exp_named_subst'),rels
308 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
309 let exp_named_subst',rels =
311 (fun (uri,t) (exp_named_subst,rels) ->
312 let t',rels' = aux k t in
313 (uri,t')::exp_named_subst, rels' @ rels
314 ) exp_named_subst ([],[])
316 C.MutConstruct (uri,tyno,consno,exp_named_subst'),rels
317 | C.MutCase (sp,i,outty,t,pl) ->
318 let outty',rels1 = aux k outty in
319 let t',rels2 = aux k t in
322 (fun t (exp_named_subst,rels) ->
323 let t',rels' = aux k t in
324 t'::exp_named_subst, rels' @ rels
327 C.MutCase (sp, i, outty', t', pl'), rels1 @ rels2 @rels3
329 let len = List.length fl in
332 (fun (name,i,ty,bo) (fl,rels) ->
333 let ty',rels1 = aux k ty in
334 let bo',rels2 = aux (k + len) bo in
335 (name,i,ty',bo')::fl, rels1 @ rels2 @ rels
340 let len = List.length fl in
343 (fun (name,ty,bo) (fl,rels) ->
344 let ty',rels1 = aux k ty in
345 let bo',rels2 = aux (k + len) bo in
346 (name,ty',bo')::fl, rels1 @ rels2 @ rels
349 C.CoFix (i, fl'),rels