1 (* Copyright (C) 2000, 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 type coercion_search_result =
29 | SomeCoercion of Cic.term
32 | NotHandled of string Lazy.t
35 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
38 (* searches a coercion fron src to tgt in the !coercions list *)
39 let look_for_coercion src tgt =
43 (fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt)
49 (sprintf ":-( coercion non trovata da %s a %s"
50 (CoercDb.name_of_carr src)
51 (CoercDb.name_of_carr tgt)));
55 sprintf ":-) TROVATA 1 coercion da %s a %s: %s"
56 (CoercDb.name_of_carr src)
57 (CoercDb.name_of_carr tgt)
58 (UriManager.name_of_uri u)));
59 SomeCoercion (CicUtil.term_of_uri u)
62 sprintf ":-/ TROVATE %d coercion(s) da %s a %s, prendo la prima: %s"
64 (CoercDb.name_of_carr src)
65 (CoercDb.name_of_carr tgt)
66 (UriManager.name_of_uri u)));
67 SomeCoercion (CicUtil.term_of_uri u)
69 | CoercDb.EqCarrNotImplemented s -> NotHandled s
70 | CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed
73 let look_for_coercion src tgt =
74 let src_uri = CoercDb.coerc_carr_of_term src in
75 let tgt_uri = CoercDb.coerc_carr_of_term tgt in
76 look_for_coercion src_uri tgt_uri
78 (* given the new coercion uri from src to tgt returns the list
79 * of new coercions to create. hte list elements are
80 * (source, list of coercions to follow, target)
82 let get_closure_coercions src tgt uri coercions =
87 | CoercDb.EqCarrNotImplemented _ | CoercDb.EqCarrOnNonMetaClosed -> false
90 | CoercDb.Uri _, CoercDb.Uri _ ->
92 List.filter (fun (f,_,_) -> eq_carr f tgt) coercions
95 List.filter (fun (_,t,_) -> eq_carr t src) coercions
97 (List.map (fun (_,t,u) -> src,[uri; u],t) c_from_tgt) @
98 (List.map (fun (s,_,u) -> s,[u; uri],tgt) c_to_src) @
101 ((List.map (fun (_,t,u2) ->
105 | _ -> [] (* do not close in case source or target is not an indty ?? *)
108 let obj_attrs = [`Class `Coercion; `Generated]
110 (* generate_composite_closure (c2 (c1 s)) in the universe graph univ *)
111 let generate_composite_closure c1 c2 univ =
112 let c1_ty,univ = CicTypeChecker.type_of_aux' [] [] c1 univ in
116 | _ -> (Cic.Rel n) :: (mk_rels (n-1))
120 | Cic.Prod (name,src,tgt) ->
123 | Cic.Anonymous -> Cic.Name "x"
126 Cic.Lambda (name,src,compose (k+1) tgt)
127 | Cic.Appl (he::tl) ->
128 Cic.Appl (c2 :: tl @ [Cic.Appl (c1 :: (mk_rels k)) ])
129 | _ -> Cic.Appl (c2 :: [Cic.Appl (c1 :: (mk_rels k)) ])
131 let c = compose 0 c1_ty in
134 CicTypeChecker.type_of_aux' [] [] c univ
135 with CicTypeChecker.TypeCheckerFailure s as exn ->
136 debug_print (lazy (sprintf "Generated composite coercion:\n%s\n%s"
137 (CicPp.ppterm c) (Lazy.force s)));
141 FreshNamesGenerator.clean_dummy_dependent_types c_ty
143 let obj = Cic.Constant ("xxxx",Some c,cleaned_ty,[],obj_attrs) in
147 (* removes from l the coercions that are in !coercions *)
148 let filter_duplicates l coercions =
151 not (List.exists (fun (s,t,u) ->
152 CoercDb.eq_carr s src &&
153 CoercDb.eq_carr t tgt)
157 let term_of_carr = function
158 | CoercDb.Uri u -> CicUtil.term_of_uri u
159 | CoercDb.Sort s -> Cic.Sort s
160 | CoercDb.Term _ -> assert false
162 (* given a new coercion uri from src to tgt returns
163 * a list of (new coercion uri, coercion obj, universe graph)
165 let close_coercion_graph src tgt uri =
166 (* check if the coercion already exists *)
167 let coercions = CoercDb.to_list () in
168 let todo_list = get_closure_coercions src tgt uri coercions in
169 let todo_list = filter_duplicates todo_list coercions in
172 fun (src, l , tgt) ->
178 Some (term_of_carr (CoercDb.Uri he)),
179 Cic.Sort Cic.Prop, [], obj_attrs)
182 List.fold_left (fun (o,univ) coer ->
184 | Cic.Constant (_,Some c,_,[],_) ->
185 generate_composite_closure c (term_of_carr (CoercDb.Uri
188 ) (first_step, CicUniv.empty_ugraph) tl
190 let name_src = CoercDb.name_of_carr src in
191 let name_tgt = CoercDb.name_of_carr tgt in
192 let name = name_tgt ^ "_of_" ^ name_src in
193 let buri = UriManager.buri_of_uri uri in
195 UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con")
199 | Cic.Constant (_,bo,ty,vl,attrs) ->
200 Cic.Constant (name,bo,ty,vl,attrs)
203 ((src,tgt,c_uri,named_obj))
209 let coercion_hashtbl = UriManager.UriHashtbl.create 3
211 let add_coercion uri =
213 CicTypeChecker.type_of_aux' [] [] (CicUtil.term_of_uri uri)
216 (* we have to get the source and the tgt type uri
217 * in Coq syntax we have already their names, but
218 * since we don't support Funclass and similar I think
219 * all the coercion should be of the form
221 * So we should be able to extract them from the coercion type
223 let extract_last_two_p ty =
224 let rec aux = function
225 | Cic.Prod( _, src, Cic.Prod (n,t1,t2)) -> aux (Cic.Prod(n,t1,t2))
226 | Cic.Prod( _, src, tgt) -> src, tgt
231 let ty_src,ty_tgt = extract_last_two_p coer_ty in
232 let src_uri = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_src) in
233 let tgt_uri = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_tgt) in
234 let new_coercions = close_coercion_graph src_uri tgt_uri uri in
235 UriManager.UriHashtbl.add coercion_hashtbl uri
236 (List.map (fun (_,_,uri,_) -> uri) new_coercions);
237 CoercDb.add_coercion (src_uri,tgt_uri,uri);
239 (fun (src,tgt,uri,_) -> CoercDb.add_coercion (src,tgt,uri))
241 List.map (fun (_,_,uri,o) -> uri,o) new_coercions
244 let remove_coercion uri =
246 let res = UriManager.UriHashtbl.find coercion_hashtbl uri in
247 UriManager.UriHashtbl.remove coercion_hashtbl uri;
248 CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq uri u);
251 CoercDb.remove_coercion
252 (fun (_,_,u1) -> UriManager.eq u u1))
258 CoercDb.remove_coercion (fun (_,_,u1) -> true)
260 let is_a_coercion t =
262 let uri = CicUtil.uri_of_term t in
263 CoercDb.is_a_coercion uri
264 with Invalid_argument _ -> false
268 let uri = CicUtil.uri_of_term t in
269 term_of_carr (fst (CoercDb.get_carr uri))
270 with Invalid_argument _ -> assert false (* t must be a coercion *)
274 let uri = CicUtil.uri_of_term t in
275 term_of_carr (snd (CoercDb.get_carr uri))
276 with Invalid_argument _ -> assert false (* t must be a coercion *)