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 coercions = (UriManager.uri * UriManager.uri * UriManager.uri) list
30 (* the list of known coercions (MUST be transitively closed) *)
32 (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)",
33 UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R.con",
34 UriManager.uri_of_string "cic:/Coq/Reals/Raxioms/INR.con") ;
37 UriManager.uri_of_string "cic:/CoRN/algebra/CFields/CField.ind#xpointer(1/1)",
38 UriManager.uri_of_string "cic:/CoRN/algebra/CRings/CRing.ind#xpointer(1/1)",
39 UriManager.uri_of_string "cic:/CoRN/algebra/CFields/cf_crr.con"
43 UriManager.uri_of_string "cic:/CoRN/algebra/CAbGroups/CAbGroup.ind#xpointer(1/1)",
44 UriManager.uri_of_string "cic:/CoRN/algebra/CGroups/CGroup.ind#xpointer(1/1)",
45 UriManager.uri_of_string "cic:/CoRN/algebra/CAbGroups/cag_crr.con"
52 (* searches a coercion fron src to tgt in the !coercions list *)
53 let look_for_coercion src tgt =
56 List.find (fun (s,t,_) ->
57 UriManager.eq s src &&
61 prerr_endline (sprintf ":) TROVATA la coercion %s %s"
62 (UriManager.name_of_uri src)
63 (UriManager.name_of_uri tgt));
64 Some (CicUtil.term_of_uri (UriManager.string_of_uri u))
67 prerr_endline (sprintf ":( NON TROVATA la coercion %s %s"
68 (UriManager.name_of_uri src) (UriManager.name_of_uri tgt));
72 (* given the new coercion uri from src to tgt returns the list
73 * of new coercions to create. hte list elements are
74 * (source, list of coercions to follow, target)
76 let get_closure_coercions src tgt uri =
78 List.filter (fun (f,_,_) ->
83 List.filter (fun (_,t,_) ->
87 (List.map (fun (_,t,u) -> src,[uri; u],t) c_from_tgt) @
88 (List.map (fun (s,_,u) -> s,[u; uri],tgt) c_to_src) @
91 ((List.map (fun (_,t,u2) ->
97 let obj_attrs = [`Class `Coercion; `Generated]
99 (* generate_composite_closure (c2 (c1 s)) in the universe graph univ *)
100 let generate_composite_closure c1 c2 univ =
101 let c1_ty,univ = CicTypeChecker.type_of_aux' [] [] c1 univ in
105 | _ -> (Cic.Rel n) :: (mk_rels (n-1))
109 | Cic.Prod (name,src,tgt) ->
112 | Cic.Anonymous -> Cic.Name "x"
115 Cic.Lambda (name,src,compose (k+1) tgt)
116 | Cic.Appl (he::tl) ->
117 Cic.Appl (c2 :: tl @ [Cic.Appl (c1 :: (mk_rels k)) ])
118 | _ -> Cic.Appl (c2 :: [Cic.Appl (c1 :: (mk_rels k)) ])
120 let c = compose 0 c1_ty in
123 CicTypeChecker.type_of_aux' [] [] c univ
124 with CicTypeChecker.TypeCheckerFailure s as exn ->
125 prerr_endline (sprintf "Generated composite coercion:\n%s\n%s"
130 FreshNamesGenerator.clean_dummy_dependent_types c_ty
132 let obj = Cic.Constant ("xxxx",Some c,cleaned_ty,[],obj_attrs) in
136 (* removes from l the coercions that are in !coercions *)
137 let filter_duplicates l =
140 not (List.exists (fun (s,t,u) ->
141 UriManager.eq s src &&
146 (* given a new coercion uri from src to tgt returns
147 * a list of (new coercion uri, coercion obj, universe graph)
149 let close_coercion_graph src tgt uri =
150 (* check if the coercion already exists *)
151 let todo_list = get_closure_coercions src tgt uri in
152 let todo_list = filter_duplicates todo_list in
153 let new_coercions, new_coercions_obj =
156 fun (src, l , tgt) ->
160 let term_of_uri' uri =
161 CicUtil.term_of_uri (UriManager.string_of_uri uri)
164 Cic.Constant ("", Some (term_of_uri' he), Cic.Sort Cic.Prop, [],
168 List.fold_left (fun (o,u) coer ->
170 | Cic.Constant (_,Some c,_,[],_) ->
171 generate_composite_closure c (term_of_uri' coer) u
173 ) (first_step, CicUniv.empty_ugraph) tl
175 let name_src = UriManager.name_of_uri src in
176 let name_tgt = UriManager.name_of_uri tgt in
177 let name = name_tgt ^ "_of_" ^ name_src in
178 let buri = UriManager.buri_of_uri uri in
180 UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con")
184 | Cic.Constant (_,bo,ty,vl,attrs) ->
185 Cic.Constant (name,bo,ty,vl,attrs)
188 ((src,tgt,c_uri),(c_uri,named_obj,u))
191 coercions := !coercions @ new_coercions @ [src,tgt,uri];
195 let get_coercions_list () =
201 let l = close_coercion_graph
202 (UriManager.uri_of_string
203 "cic:/CoRN/algebra/CRings/CRing.ind#xpointer(1/1)")
204 (UriManager.uri_of_string
205 "cic:/CoRN/algebra/CAbGroups/CAbGroup.ind#xpointer(1/1)")
206 (UriManager.uri_of_string
207 "cic:/CoRN/algebra/CRings/cr_crr.con")
209 List.iter (fun (u,o,g) ->
210 prerr_endline (CicPp.ppobj o);
211 prerr_endline (UriManager.string_of_uri u);