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 (* mk_fresh_name context name typ *)
27 (* returns an identifier which is fresh in the context *)
28 (* and that resembles [name] as much as possible. *)
29 (* [typ] will be the type of the variable *)
30 let mk_fresh_name ~subst metasenv context name ~typ =
35 (*CSC: great space for improvements here *)
38 CicTypeChecker.type_of_aux' ~subst metasenv context typ
39 CicUniv.empty_ugraph in
42 | C.Sort C.CProp -> "H"
46 with CicTypeChecker.TypeCheckerFailure _ -> "H"
49 Str.global_replace (Str.regexp "[0-9]*$") "" name
51 let already_used name =
52 List.exists (function Some (C.Name n,_) -> n=name | _ -> false) context
54 if not (already_used basename) then
58 let name' = basename ^ string_of_int n in
59 if already_used name' then
67 (* clean_dummy_dependent_types term *)
68 (* returns a copy of [term] where every dummy dependent product *)
69 (* have been replaced with a non-dependent product and where *)
70 (* dummy let-ins have been removed. *)
71 let clean_dummy_dependent_types t =
75 C.Rel m as t -> t,[k - m]
76 | C.Var (uri,exp_named_subst) ->
77 let exp_named_subst',rels =
79 (fun (uri,t) (exp_named_subst,rels) ->
80 let t',rels' = aux k t in
81 (uri,t')::exp_named_subst, rels' @ rels
82 ) exp_named_subst ([],[])
84 C.Var (uri,exp_named_subst'),rels
93 let t',rels' = aux k t in
100 | C.Sort _ as t -> t,[]
101 | C.Implicit _ as t -> t,[]
103 let te',rels1 = aux k te in
104 let ty',rels2 = aux k ty in
105 C.Cast (te', ty'), rels1@rels2
107 let s',rels1 = aux k s in
108 let t',rels2 = aux (k+1) t in
112 if List.mem k rels2 then
114 prerr_endline "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" ;
120 if List.mem k rels2 then n else C.Anonymous
122 C.Prod (n', s', t'), rels1@rels2
123 | C.Lambda (n,s,t) ->
124 let s',rels1 = aux k s in
125 let t',rels2 = aux (k+1) t in
126 C.Lambda (n, s', t'), rels1@rels2
128 let s',rels1 = aux k s in
129 let t',rels2 = aux (k+1) t in
130 let rels = rels1 @ rels2 in
131 if List.mem k rels2 then
132 C.LetIn (n, s', t'), rels
134 (* (C.Rel 1) is just a dummy term; any term would fit *)
135 CicSubstitution.subst (C.Rel 1) t', rels
139 (fun t (exp_named_subst,rels) ->
140 let t',rels' = aux k t in
141 t'::exp_named_subst, rels' @ rels
145 | C.Const (uri,exp_named_subst) ->
146 let exp_named_subst',rels =
148 (fun (uri,t) (exp_named_subst,rels) ->
149 let t',rels' = aux k t in
150 (uri,t')::exp_named_subst, rels' @ rels
151 ) exp_named_subst ([],[])
153 C.Const (uri,exp_named_subst'),rels
154 | C.MutInd (uri,tyno,exp_named_subst) ->
155 let exp_named_subst',rels =
157 (fun (uri,t) (exp_named_subst,rels) ->
158 let t',rels' = aux k t in
159 (uri,t')::exp_named_subst, rels' @ rels
160 ) exp_named_subst ([],[])
162 C.MutInd (uri,tyno,exp_named_subst'),rels
163 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
164 let exp_named_subst',rels =
166 (fun (uri,t) (exp_named_subst,rels) ->
167 let t',rels' = aux k t in
168 (uri,t')::exp_named_subst, rels' @ rels
169 ) exp_named_subst ([],[])
171 C.MutConstruct (uri,tyno,consno,exp_named_subst'),rels
172 | C.MutCase (sp,i,outty,t,pl) ->
173 let outty',rels1 = aux k outty in
174 let t',rels2 = aux k t in
177 (fun t (exp_named_subst,rels) ->
178 let t',rels' = aux k t in
179 t'::exp_named_subst, rels' @ rels
182 C.MutCase (sp, i, outty', t', pl'), rels1 @ rels2 @rels3
184 let len = List.length fl in
187 (fun (name,i,ty,bo) (fl,rels) ->
188 let ty',rels1 = aux k ty in
189 let bo',rels2 = aux (k + len) bo in
190 (name,i,ty',bo')::fl, rels1 @ rels2 @ rels
195 let len = List.length fl in
198 (fun (name,ty,bo) (fl,rels) ->
199 let ty',rels1 = aux k ty in
200 let bo',rels2 = aux (k + len) bo in
201 (name,ty',bo')::fl, rels1 @ rels2 @ rels
204 C.CoFix (i, fl'),rels