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
40 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
42 let saturate_coercion ul metasenv subst context =
46 let t = CicUtil.term_of_uri u in
48 match CoercDb.is_a_coercion t with
49 | Some (_,CoercDb.Fun i,_,_,_) -> i
52 arity,t,saturations) ul
54 let freshmeta = CicMkImplicit.new_meta metasenv subst in
56 (fun (arity,c,saturations) ->
58 CicTypeChecker.type_of_aux' ~subst metasenv context c
59 CicUniv.oblivion_ugraph in
60 let _,metasenv,args,lastmeta =
61 TermUtil.saturate_term ~delta:false freshmeta metasenv context ty arity in
63 CicMkImplicit.identity_relocation_list_for_metavariable context
65 metasenv, Cic.Meta (lastmeta - saturations - 1,irl),
68 | _ -> Cic.Appl (c::args)
72 (* searches a coercion fron src to tgt in the !coercions list *)
73 let look_for_coercion_carr metasenv subst context src tgt =
74 let is_dead = function CoercDb.Dead -> true | _ -> false in
80 (sprintf ":-( coercion non trovata[%s] da %s a %s" s
81 (CoercDb.string_of_carr src)
82 (CoercDb.string_of_carr tgt)));
85 sprintf ":-) TROVATE[%s] %d coercion(s) da %s a %s" s
87 (CoercDb.string_of_carr src)
88 (CoercDb.string_of_carr tgt)));
90 if is_dead src || is_dead tgt then NotHandled
95 CoercDb.eq_carr s src &&
97 | CoercDb.Sort Cic.Prop, CoercDb.Sort Cic.Prop
98 | CoercDb.Sort Cic.Set, CoercDb.Sort Cic.Set
99 | CoercDb.Sort _, CoercDb.Sort (Cic.Type _|Cic.CProp _) -> true
100 | _ -> CoercDb.eq_carr t tgt)
106 CoercDb.find_coercion
107 (fun (_,t) -> CoercDb.eq_carr t tgt)
113 SomeCoercionToTgt (saturate_coercion ul metasenv subst context))
114 | ul -> SomeCoercion (saturate_coercion ul metasenv subst context))
117 let rec count_pi c s t =
118 match CicReduction.whd ~delta:false ~subst:s c t with
119 | Cic.Prod (_,_,t) -> 1 + count_pi c s t
123 let look_for_coercion metasenv subst context src tgt =
124 let src_arity = count_pi context subst src in
125 let tgt_arity = count_pi context subst tgt in
126 let src_carr = CoercDb.coerc_carr_of_term src src_arity in
127 let tgt_carr = CoercDb.coerc_carr_of_term tgt tgt_arity in
128 look_for_coercion_carr metasenv subst context src_carr tgt_carr
131 match CoercDb.is_a_coercion t with
132 | None -> assert false
133 | Some (CoercDb.Sort s,_,_,_,_) -> Cic.Sort s
134 | Some (CoercDb.Uri u,_,_,_,_) -> CicUtil.term_of_uri u
135 | Some _ -> assert false (* t must be a coercion not to funclass *)
138 let generate_dot_file () =
139 let l = CoercDb.to_list () in
140 let module Pp = GraphvizPp.Dot in
141 let buf = Buffer.create 10240 in
142 let fmt = Format.formatter_of_buffer buf in
143 Pp.header ~node_attrs:["fontsize", "9"; "width", ".4"; "height", ".4"]
144 ~edge_attrs:["fontsize", "10"] fmt;
146 Format.fprintf fmt "subgraph cluster_rest { style=\"filled\";
147 color=\"white\"; label=<%s>; labelloc=\"b\"; %s; }\n"
148 ("<FONT POINT-SIZE=\"10.0\"><TABLE BORDER=\"1\" CELLBORDER=\"1\" >
149 <TR><TD BGCOLOR=\"gray95\">Source</TD>
150 <TD BGCOLOR=\"gray95\">Target</TD>
151 <TD BGCOLOR=\"gray95\">Arrows</TD></TR>"^
152 String.concat "</TR>"
155 let src_name = CoercDb.string_of_carr src in
156 let tgt_name = CoercDb.string_of_carr tgt in
157 let names = List.map (fun (u,_,_) -> UriManager.name_of_uri u) ul in
158 "<TR><TD>" ^ src_name ^ "</TD><TD>" ^ tgt_name ^ "</TD><TD>" ^
159 String.concat "," names ^ "</TD>")
160 (List.sort (fun (x,y,_) (x1,y1,_) ->
161 let rc = compare x x1 in
162 if rc = 0 then compare y y1 else rc) l))
163 ^ "</TR></TABLE></FONT>")
165 (List.flatten (List.map (fun (s,t,_) ->
166 let src_name = CoercDb.string_of_carr s in
167 let tgt_name = CoercDb.string_of_carr t in
168 [ "\""^src_name^"\""; "\""^tgt_name^"\"" ]
170 let pp_description carr =
173 Pp.node (CoercDb.string_of_carr carr)
174 ~attrs:["href", UriManager.string_of_uri uri] fmt
178 (fun (src, tgt, ul) ->
179 let src_name = CoercDb.string_of_carr src in
180 let tgt_name = CoercDb.string_of_carr tgt in
184 (fun (u,saturations,_) ->
185 Pp.edge src_name tgt_name
187 (UriManager.name_of_uri u ^
188 if saturations = 0 then
191 "(" ^ string_of_int saturations ^ ")");
192 "href", UriManager.string_of_uri u ]
204 match CoercDb.is_a_coercion c with
206 | Some (_,_,_,_,cpos) ->
207 if List.length tl > cpos then Some (List.nth tl cpos, cpos) else None
210 (************************* meet calculation stuff ********************)
211 let eq_uri_opt u1 u2 =
213 | Some (u1,_), Some (u2,_) -> UriManager.eq u1 u2
214 | None,Some _ | Some _, None -> false
218 let eq_carr_uri (c1,u1) (c2,u2) = CoercDb.eq_carr c1 c2 && eq_uri_opt u1 u2;;
220 let eq_carr_uri_uri (c1,u1,u11) (c2,u2,u22) =
221 CoercDb.eq_carr c1 c2 && eq_uri_opt u1 u2 && eq_uri_opt u11 u22
224 let uniq = HExtlib.list_uniq ~eq:eq_carr_uri;;
226 let uniq2 = HExtlib.list_uniq ~eq:eq_carr_uri_uri;;
228 let splat e l = List.map (fun (x1,x2,_) -> e, Some (x1,x2)) l;;
230 (* : carr -> (carr * uri option) where the option is always Some *)
231 let get_coercions_to carr =
232 let l = CoercDb.to_list () in
233 let splat_coercion_to carr (src,tgt,cl) =
234 if CoercDb.eq_carr tgt carr then Some (splat src cl) else None
236 let l = List.flatten (HExtlib.filter_map (splat_coercion_to carr) l) in
240 (* : carr -> (carr * uri option) where the option is always Some *)
241 let get_coercions_from carr =
242 let l = CoercDb.to_list () in
243 let splat_coercion_from carr (src,tgt,cl) =
244 if CoercDb.eq_carr src carr then Some (splat tgt cl) else None
246 List.flatten (HExtlib.filter_map (splat_coercion_from carr) l)
249 (* intersect { (s1,u1) | u1:s1->t1 } { (s2,u2) | u2:s2->t2 }
250 * gives the set { (s,u1,u2) | u1:s->t1 /\ u2:s->t2 } *)
251 let intersect l1 l2 =
252 let is_in_l1 (x,u2) =
255 if CoercDb.eq_carr x src then Some (src,u1,u2) else None)
258 uniq2 (List.flatten (List.map is_in_l1 l2))
261 (* grow tgt gives all the (src,u) such that u:tgt->src *)
263 uniq ((tgt,None)::(get_coercions_to tgt))
267 let l = get_coercions_from c in
268 fun (x,_,_) -> List.exists (fun (y,_) -> CoercDb.eq_carr x y) l
271 (* given the set { (s,u1,u2) | u1:s->t1 /\ u2:s->t2 } removes the elements
272 * (s,_,_) such that (s',_,_) is in the set and there exists a coercion s->s' *)
273 let rec min acc = function
275 if List.exists (lb c) (tl@acc) then min acc tl else min (c::acc) tl
279 let meets metasenv subst context (grow_left,left) (grow_right,right) =
280 let saturate metasenv uo =
282 | None -> metasenv, None
284 match saturate_coercion [u] metasenv subst context with
285 | [metasenv, sat, last] -> metasenv, Some (sat, last)
291 if grow_left then saturate metasenv uo1 else metasenv, None in
293 if grow_right then saturate metasenv uo2 else metasenv, None in
294 c,metasenv, uo1, uo2)
295 (min [] (intersect (grow left) (grow right)))