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/.
30 type coercion_search_result =
31 (* metasenv, last coercion argument, fully saturated coercion *)
32 (* to apply the coercion it is sufficient to unify the last coercion
33 argument (that is a Meta) with the term to be coerced *)
34 | SomeCoercion of (Cic.metasenv * Cic.term * Cic.term) list
35 | SomeCoercionToTgt of (Cic.metasenv * Cic.term * Cic.term) list
38 | NotHandled of string Lazy.t
41 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
43 let saturate_coercion ul metasenv subst context =
44 let cl = List.map CicUtil.term_of_uri ul in
46 let _,tgtcarl = List.split (List.map CoercDb.get_carr ul) in
47 List.map (function CoercDb.Fun i -> i | _ -> 0) tgtcarl
49 let freshmeta = CicMkImplicit.new_meta metasenv subst in
53 CicTypeChecker.type_of_aux' ~subst metasenv context c
54 CicUniv.empty_ugraph in
55 let _,metasenv,args,lastmeta =
56 TermUtil.saturate_term freshmeta metasenv context ty arity in
58 CicMkImplicit.identity_relocation_list_for_metavariable context
60 metasenv, Cic.Meta (lastmeta-1,irl),
63 | _ -> Cic.Appl (c::args)
67 (* searches a coercion fron src to tgt in the !coercions list *)
68 let look_for_coercion' metasenv subst context src tgt =
74 (sprintf ":-( coercion non trovata[%s] da %s a %s" s
75 (CoercDb.name_of_carr src)
76 (CoercDb.name_of_carr tgt)));
79 sprintf ":-) TROVATE[%s] %d coercion(s) da %s a %s" s
81 (CoercDb.name_of_carr src)
82 (CoercDb.name_of_carr tgt)));
87 (fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt)
94 (fun (_,t) -> CoercDb.eq_carr t tgt)
99 | ul -> SomeCoercionToTgt (saturate_coercion ul metasenv subst context))
100 | ul -> SomeCoercion (saturate_coercion ul metasenv subst context))
102 | CoercDb.EqCarrNotImplemented s -> NotHandled s
103 | CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed
106 let look_for_coercion metasenv subst context src tgt =
107 let src_uri = CoercDb.coerc_carr_of_term src in
108 let tgt_uri = CoercDb.coerc_carr_of_term tgt in
109 look_for_coercion' metasenv subst context src_uri tgt_uri
113 let uri = CicUtil.uri_of_term t in
114 CoercDb.term_of_carr (fst (CoercDb.get_carr uri))
115 with Invalid_argument _ -> assert false (* t must be a coercion *)
117 let generate_dot_file () =
118 let module Pp = GraphvizPp.Dot in
119 let buf = Buffer.create 10240 in
120 let fmt = Format.formatter_of_buffer buf in
121 Pp.header ~node_attrs:["fontsize", "9"; "width", ".4"; "height", ".4"]
122 ~edge_attrs:["fontsize", "10"] fmt;
123 let l = CoercDb.to_list () in
124 let pp_description carr =
125 match CoercDb.uri_of_carr carr with
128 Pp.node (CoercDb.name_of_carr carr)
129 ~attrs:["href", UriManager.string_of_uri uri] fmt in
131 (fun (src, tgt, cl) ->
132 let src_name = CoercDb.name_of_carr src in
133 let tgt_name = CoercDb.name_of_carr tgt in
138 Pp.edge src_name tgt_name
139 ~attrs:[ "label", UriManager.name_of_uri c;
140 "href", UriManager.string_of_uri c ]
152 | Cic.Appl (he::_) -> CicUtil.uri_of_term he
153 | _ -> CicUtil.uri_of_term t
155 match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
156 | Cic.Constant (_,_, _, _, attrs),_ ->
157 List.exists (function `Class (`Coercion _) -> true | _ -> false) attrs
159 with Invalid_argument _ -> false
164 | [] | [_] -> assert false
165 | c::_ when not (CoercDb.is_a_coercion' c) -> assert false
168 match CoercDb.is_a_coercion_to_funclass c with None -> 0 | Some a -> a
170 (* decide a decent structure for coercion carriers so that all this stuff is
173 (* this calculation is not complete, since we have strange carriers *)
174 let rec count_pi = function
175 | Cic.Prod(_,_,t) -> 1+ (count_pi t)
178 let uri = CicUtil.uri_of_term c in
179 match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
180 | Cic.Constant (_, _, ty, _, _) -> count_pi ty
183 try Some (List.nth tl (pi - arity)) with Invalid_argument _ -> None
186 (************************* meet calculation stuff ********************)
187 let eq_uri_opt u1 u2 =
189 | Some u1, Some u2 -> UriManager.eq u1 u2
190 | None,Some _ | Some _, None -> false
194 let eq_carr_uri (c1,u1) (c2,u2) = CoercDb.eq_carr c1 c2 && eq_uri_opt u1 u2;;
196 let eq_carr_uri_uri (c1,u1,u11) (c2,u2,u22) =
197 CoercDb.eq_carr c1 c2 && eq_uri_opt u1 u2 && eq_uri_opt u11 u22
200 let uniq = HExtlib.list_uniq ~eq:eq_carr_uri;;
202 let uniq2 = HExtlib.list_uniq ~eq:eq_carr_uri_uri;;
204 let splat e l = List.map (fun x -> e, Some x) l;;
206 (* : carr -> (carr * uri option) where the option is always Some *)
207 let get_coercions_to carr =
208 let l = CoercDb.to_list () in
209 let splat_coercion_to carr (src,tgt,cl) =
210 if CoercDb.eq_carr tgt carr then Some (splat src cl) else None
212 let l = List.flatten (HExtlib.filter_map (splat_coercion_to carr) l) in
216 (* : carr -> (carr * uri option) where the option is always Some *)
217 let get_coercions_from carr =
218 let l = CoercDb.to_list () in
219 let splat_coercion_from carr (src,tgt,cl) =
220 if CoercDb.eq_carr src carr then Some (splat tgt cl) else None
222 List.flatten (HExtlib.filter_map (splat_coercion_from carr) l)
225 (* intersect { (s1,u1) | u1:s1->t1 } { (s2,u2) | u2:s2->t2 }
226 * gives the set { (s,u1,u2) | u1:s->t1 /\ u2:s->t2 } *)
227 let intersect l1 l2 =
228 let is_in_l1 (x,u2) =
231 if CoercDb.eq_carr x src then Some (src,u1,u2) else None)
234 uniq2 (List.flatten (List.map is_in_l1 l2))
237 (* grow tgt gives all the (src,u) such that u:tgt->src *)
239 uniq ((tgt,None)::(get_coercions_to tgt))
243 let l = get_coercions_from c in
244 fun (x,_,_) -> List.exists (fun (y,_) -> CoercDb.eq_carr x y) l
247 (* given the set { (s,u1,u2) | u1:s->t1 /\ u2:s->t2 } removes the elements
248 * (s,_,_) such that (s',_,_) is in the set and there exists a coercion s->s' *)
249 let rec min acc = function
251 if List.exists (lb c) (tl@acc) then min acc tl else min (c::acc) tl
255 let meets metasenv subst context left right =
256 let saturate metasenv uo =
258 | None -> metasenv, None
260 match saturate_coercion [u] metasenv subst context with
261 | [metasenv, sat, last] -> metasenv, Some (sat, last)
266 let metasenv, uo1 = saturate metasenv uo1 in
267 let metasenv, uo2 = saturate metasenv uo2 in
268 c,metasenv, uo1, uo2)
269 (min [] (intersect (grow left) (grow right)))