1 (* Copyright (C) 2005, 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://helm.cs.unibo.it/
27 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
29 (* given the new coercion uri from src to tgt returns the list
30 * of new coercions to create. hte list elements are
31 * (source, list of coercions to follow, target)
33 let get_closure_coercions src tgt uri coercions =
38 | CoercDb.EqCarrNotImplemented _ | CoercDb.EqCarrOnNonMetaClosed -> false
41 | CoercDb.Uri _, CoercDb.Uri _ ->
43 List.filter (fun (f,_,_) -> eq_carr f tgt) coercions
46 List.filter (fun (_,t,_) -> eq_carr t src) coercions
48 (List.map (fun (_,t,u) -> src,[uri; u],t) c_from_tgt) @
49 (List.map (fun (s,_,u) -> s,[u; uri],tgt) c_to_src) @
52 ((List.map (fun (_,t,u2) ->
56 | _ -> [] (* do not close in case source or target is not an indty ?? *)
59 let obj_attrs = [`Class `Coercion; `Generated]
61 (* generate_composite_closure (c2 (c1 s)) in the universe graph univ *)
62 let generate_composite_closure c1 c2 univ =
63 let c1_ty,univ = CicTypeChecker.type_of_aux' [] [] c1 univ in
67 | _ -> (Cic.Rel n) :: (mk_rels (n-1))
71 | Cic.Prod (name,src,tgt) ->
74 | Cic.Anonymous -> Cic.Name "x"
77 Cic.Lambda (name,src,compose (k+1) tgt)
78 | Cic.Appl (he::tl) ->
79 Cic.Appl (c2 :: tl @ [Cic.Appl (c1 :: (mk_rels k)) ])
80 | _ -> Cic.Appl (c2 :: [Cic.Appl (c1 :: (mk_rels k)) ])
82 let c = compose 0 c1_ty in
85 CicTypeChecker.type_of_aux' [] [] c univ
86 with CicTypeChecker.TypeCheckerFailure s as exn ->
87 debug_print (lazy (Printf.sprintf "Generated composite coercion:\n%s\n%s"
88 (CicPp.ppterm c) (Lazy.force s)));
92 FreshNamesGenerator.clean_dummy_dependent_types c_ty
94 let obj = Cic.Constant ("xxxx",Some c,cleaned_ty,[],obj_attrs) in
98 (* removes from l the coercions that are in !coercions *)
99 let filter_duplicates l coercions =
102 not (List.exists (fun (s,t,u) ->
103 CoercDb.eq_carr s src &&
104 CoercDb.eq_carr t tgt)
108 (* given a new coercion uri from src to tgt returns
109 * a list of (new coercion uri, coercion obj, universe graph)
111 let close_coercion_graph src tgt uri =
112 (* check if the coercion already exists *)
113 let coercions = CoercDb.to_list () in
114 let todo_list = get_closure_coercions src tgt uri coercions in
115 let todo_list = filter_duplicates todo_list coercions in
118 fun (src, l , tgt) ->
124 Some (CoercDb.term_of_carr (CoercDb.Uri he)),
125 Cic.Sort Cic.Prop, [], obj_attrs)
128 List.fold_left (fun (o,univ) coer ->
130 | Cic.Constant (_,Some c,_,[],_) ->
131 generate_composite_closure c (CoercDb.term_of_carr (CoercDb.Uri
134 ) (first_step, CicUniv.empty_ugraph) tl
136 let name_src = CoercDb.name_of_carr src in
137 let name_tgt = CoercDb.name_of_carr tgt in
138 let name = name_tgt ^ "_of_" ^ name_src in
139 let buri = UriManager.buri_of_uri uri in
141 UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con")
145 | Cic.Constant (_,bo,ty,vl,attrs) ->
146 Cic.Constant (name,bo,ty,vl,attrs)
149 ((src,tgt,c_uri,named_obj))