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 metasenv context name ~typ =
35 (*CSC: great space for improvements here *)
37 (match CicTypeChecker.type_of_aux' metasenv context typ with
39 | C.Sort C.CProp -> "H"
43 with CicTypeChecker.TypeCheckerFailure _ -> "H"
46 Str.global_replace (Str.regexp "[0-9]*$") "" name
48 let already_used name =
49 List.exists (function Some (C.Name n,_) -> n=name | _ -> false) context
51 if not (already_used basename) then
55 let name' = basename ^ string_of_int n in
56 if already_used name' then
64 (* clean_dummy_dependent_types term *)
65 (* returns a copy of [term] where every dummy dependent product *)
66 (* have been replaced with a non-dependent product and where *)
67 (* dummy let-ins have been removed. *)
68 let clean_dummy_dependent_types t =
72 C.Rel m as t -> t,[m - k]
73 | C.Var (uri,exp_named_subst) ->
74 let exp_named_subst',rels =
76 (fun (uri,t) (exp_named_subst,rels) ->
77 let t',rels' = aux k t in
78 (uri,t')::exp_named_subst, rels' @ rels
79 ) exp_named_subst ([],[])
81 C.Var (uri,exp_named_subst'),rels
90 let t',rels' = aux k t in
97 | C.Sort _ as t -> t,[]
98 | C.Implicit as t -> t,[]
100 let te',rels1 = aux k te in
101 let ty',rels2 = aux k ty in
102 C.Cast (te', ty'), rels1@rels2
104 let s',rels1 = aux k s in
105 let t',rels2 = aux (k+1) t in
109 if List.mem k rels2 then assert false else C.Anonymous
111 if List.mem k rels2 then n else C.Anonymous
113 C.Prod (n', s', t'), rels1@rels2
114 | C.Lambda (n,s,t) ->
115 let s',rels1 = aux k s in
116 let t',rels2 = aux (k+1) t in
117 C.Lambda (n, s', t'), rels1@rels2
119 let s',rels1 = aux k s in
120 let t',rels2 = aux (k+1) t in
121 let rels = rels1 @ rels2 in
122 if List.mem k rels2 then
123 C.LetIn (n, s', t'), rels
125 (* (C.Rel 1) is just a dummy term; any term would fit *)
126 CicSubstitution.subst (C.Rel 1) t', rels
130 (fun t (exp_named_subst,rels) ->
131 let t',rels' = aux k t in
132 t'::exp_named_subst, rels' @ rels
136 | C.Const (uri,exp_named_subst) ->
137 let exp_named_subst',rels =
139 (fun (uri,t) (exp_named_subst,rels) ->
140 let t',rels' = aux k t in
141 (uri,t')::exp_named_subst, rels' @ rels
142 ) exp_named_subst ([],[])
144 C.Const (uri,exp_named_subst'),rels
145 | C.MutInd (uri,tyno,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.MutInd (uri,tyno,exp_named_subst'),rels
154 | C.MutConstruct (uri,tyno,consno,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.MutConstruct (uri,tyno,consno,exp_named_subst'),rels
163 | C.MutCase (sp,i,outty,t,pl) ->
164 let outty',rels1 = aux k outty in
165 let t',rels2 = aux k t in
168 (fun t (exp_named_subst,rels) ->
169 let t',rels' = aux k t in
170 t'::exp_named_subst, rels' @ rels
173 C.MutCase (sp, i, outty', t', pl'), rels1 @ rels2 @rels3
175 let len = List.length fl in
178 (fun (name,i,ty,bo) (fl,rels) ->
179 let ty',rels1 = aux k ty in
180 let bo',rels2 = aux (k + len) bo in
181 (name,i,ty',bo')::fl, rels1 @ rels2 @ rels
186 let len = List.length fl in
189 (fun (name,ty,bo) (fl,rels) ->
190 let ty',rels1 = aux k ty in
191 let bo',rels2 = aux (k + len) bo in
192 (name,ty',bo')::fl, rels1 @ rels2 @ rels
195 C.CoFix (i, fl'),rels