]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/cic_unification/coercGraph.ml
added config.ac to the tarball for debian packages
[helm.git] / helm / software / components / cic_unification / coercGraph.ml
1 (* Copyright (C) 2000, HELM Team.
2  * 
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.
6  * 
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.
11  * 
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  *)
25
26 (* $Id$ *)
27
28 open Printf;;
29
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
36   | NoCoercion
37   | NotHandled
38
39 let debug = false
40 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
41
42 let saturate_coercion ul metasenv subst context =
43   let cl =
44    List.map 
45      (fun u,saturations -> 
46         let t = CicUtil.term_of_uri u in 
47         let arity = 
48           match CoercDb.is_a_coercion t with
49           | Some (_,CoercDb.Fun i,_,_,_) -> i
50           | _ -> 0
51         in
52         arity,t,saturations) ul
53   in
54   let freshmeta = CicMkImplicit.new_meta metasenv subst in
55    List.map
56     (fun (arity,c,saturations) -> 
57       let ty,_ =
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
62       let irl =
63        CicMkImplicit.identity_relocation_list_for_metavariable context
64       in
65        metasenv, Cic.Meta (lastmeta - saturations - 1,irl),
66         match args with
67            [] -> c
68          | _ -> Cic.Appl (c::args)
69     ) cl
70 ;;
71           
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
75   let pp_l s l =
76    match l with
77    | [] -> 
78        debug_print 
79          (lazy 
80          (sprintf ":-( coercion non trovata[%s] da %s a %s" s
81              (CoercDb.string_of_carr src) 
82              (CoercDb.string_of_carr tgt)));
83    | _::_ -> 
84        debug_print (lazy (
85                sprintf ":-) TROVATE[%s] %d coercion(s) da %s a %s" s
86            (List.length l)
87            (CoercDb.string_of_carr src) 
88            (CoercDb.string_of_carr tgt)));
89   in
90   if is_dead src || is_dead tgt then NotHandled
91   else
92     let l = 
93       CoercDb.find_coercion 
94         (fun (s,t) -> 
95           CoercDb.eq_carr s src && 
96           match t, tgt with
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) 
101     in
102     pp_l "precise" l;
103      (match l with
104      | [] -> 
105          let l = 
106            CoercDb.find_coercion 
107              (fun (_,t) -> CoercDb.eq_carr t tgt) 
108          in
109          pp_l "approx" l;
110          (match l with
111          | [] -> NoCoercion
112          | ul -> 
113             SomeCoercionToTgt (saturate_coercion ul metasenv subst context))
114      | ul -> SomeCoercion (saturate_coercion ul metasenv subst context))
115 ;;
116
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
120   | _ -> 0
121 ;;
122
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
129
130 let source_of t = 
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 *)
136 ;;
137
138 let generate_dot_file fmt =
139   let l = CoercDb.to_list (CoercDb.dump ()) in
140   let module Pp = GraphvizPp.Dot in
141   if List.exists (fun (_,t,_) -> CoercDb.string_of_carr t = "Type") l then
142     Format.fprintf fmt "subgraph cluster_rest { style=\"filled\";
143     color=\"white\"; label=<%s>; labelloc=\"b\"; %s; }\n" 
144        ("<FONT POINT-SIZE=\"10.0\"><TABLE BORDER=\"1\" CELLBORDER=\"1\" >
145          <TR><TD BGCOLOR=\"gray95\">Source</TD>
146          <TD BGCOLOR=\"gray95\">Target</TD>
147          <TD BGCOLOR=\"gray95\">Arrows</TD></TR>"^
148        String.concat "</TR>"   
149          (List.map 
150            (fun (src,tgt,ul) -> 
151             let src_name = CoercDb.string_of_carr src in
152             let tgt_name = CoercDb.string_of_carr tgt in
153             let names = 
154               List.map (fun (u,_,_) -> 
155                 UriManager.name_of_uri u ^ 
156                   (match CicEnvironment.get_obj CicUniv.empty_ugraph u with
157                   | Cic.Constant (_,Some (Cic.Const (u',_)),_,_,attrs), _
158                     when List.exists ((=) (`Flavour `Variant)) attrs -> "*"
159                   | _ -> "")
160               ) ul 
161             in
162             "<TR><TD>"  ^ src_name ^ "</TD><TD>" ^ tgt_name ^ "</TD><TD>" ^
163             String.concat ",&nbsp;" names ^ "</TD>")
164          (List.sort (fun (x,y,_) (x1,y1,_) -> 
165              let rc = compare x x1 in
166              if rc = 0 then compare y y1 else rc) l))
167        ^ "</TR></TABLE></FONT>")
168        (String.concat ";" ["Type"]);
169   let type_uri u = 
170     let ty, _ = 
171       CicTypeChecker.type_of_aux' [] [] (CicUtil.term_of_uri u)
172       CicUniv.oblivion_ugraph
173     in
174       ty
175   in
176   let deref_coercion u =
177    match CicEnvironment.get_obj CicUniv.empty_ugraph u with
178    | Cic.Constant (_,Some (Cic.Const (u',_)),_,_,attrs), _
179      when List.exists ((=) (`Flavour `Variant)) attrs ->
180        UriManager.name_of_uri u'
181    | Cic.Constant (_,Some t,_,_,_), _ when
182        let rec is_id = function 
183          | Cic.Lambda (_,_,t) -> is_id t
184          | Cic.Rel _ -> true
185          | _ -> false
186          in is_id t -> "ID"
187    | _ -> UriManager.name_of_uri u
188   in
189   List.iter
190     (fun (src, tgt, ul) ->
191       List.iter
192         (fun (u,saturations,cpos) ->
193           let ty = type_uri u in
194           let src_name, tgt_name = 
195             let rec aux ctx cpos t =
196               match cpos, t with
197               | 0,Cic.Prod (_,src,tgt) ->
198                   CicPp.pp src ctx, tgt, (Some (Cic.Name "_")::ctx)
199               | 0,t -> CicPp.pp t ctx, Cic.Implicit None, []
200               | n,Cic.Prod (_,_,tgt) -> aux (Some (Cic.Name "_")::ctx) (n-1) tgt
201               | _ -> assert false
202             in
203             let ssrc, rest, ctx = aux [] cpos ty in
204             let stgt, rest, _ = aux ctx saturations rest in
205             let stgt = 
206               if rest <> Cic.Implicit None then
207                 match tgt with 
208                 | CoercDb.Fun _ -> CoercDb.string_of_carr tgt
209                 | _ -> assert false
210               else
211                 stgt
212             in
213             ssrc, stgt
214           in
215           Pp.node src_name fmt;
216           Pp.node tgt_name fmt;
217           Pp.edge src_name tgt_name
218             ~attrs:[ "label",
219                  (deref_coercion u ^
220                   if saturations = 0 then ""
221                   else "(" ^ string_of_int saturations ^ ")");
222               "href", UriManager.string_of_uri u ]
223             fmt)
224         ul)
225     l;
226 ;;
227     
228 let coerced_arg l =
229   match l with
230   | [] | [_] -> None
231   | c::tl -> 
232      match CoercDb.is_a_coercion c with 
233      | None -> None
234      | Some (_,_,_,_,cpos) -> 
235         if List.length tl > cpos then Some (List.nth tl cpos, cpos) else None
236 ;;
237
238 (************************* meet calculation stuff ********************)
239 let eq_uri_opt u1 u2 = 
240   match u1,u2 with
241   | Some (u1,_), Some (u2,_) -> UriManager.eq u1 u2
242   | None,Some _ | Some _, None -> false
243   | None, None -> true
244 ;;
245
246 let eq_carr_uri (c1,u1) (c2,u2) = CoercDb.eq_carr c1 c2 && eq_uri_opt u1 u2;;
247
248 let eq_carr_uri_uri (c1,u1,u11) (c2,u2,u22) = 
249   CoercDb.eq_carr c1 c2 && eq_uri_opt u1 u2 && eq_uri_opt u11 u22
250 ;;
251
252 let uniq = HExtlib.list_uniq ~eq:eq_carr_uri;;
253
254 let uniq2 = HExtlib.list_uniq ~eq:eq_carr_uri_uri;;
255
256 let splat e l = List.map (fun (x1,x2,_) -> e, Some (x1,x2)) l;;
257
258 (* : carr -> (carr * uri option) where the option is always Some *)
259 let get_coercions_to carr = 
260   let l = CoercDb.to_list (CoercDb.dump ()) in
261   let splat_coercion_to carr (src,tgt,cl) =
262     if CoercDb.eq_carr tgt carr then Some (splat src cl) else None
263   in
264   let l = List.flatten (HExtlib.filter_map (splat_coercion_to carr) l) in
265   l
266 ;;
267
268 (* : carr -> (carr * uri option) where the option is always Some *)
269 let get_coercions_from carr = 
270   let l = CoercDb.to_list (CoercDb.dump ()) in
271   let splat_coercion_from carr (src,tgt,cl) =
272     if CoercDb.eq_carr src carr then Some (splat tgt cl) else None
273   in
274   List.flatten (HExtlib.filter_map (splat_coercion_from carr) l)
275 ;;
276
277 (* intersect { (s1,u1) | u1:s1->t1 } { (s2,u2) | u2:s2->t2 } 
278  * gives the set { (s,u1,u2) | u1:s->t1 /\ u2:s->t2 } *)
279 let intersect l1 l2 = 
280   let is_in_l1 (x,u2) = 
281     HExtlib.filter_map 
282       (fun (src,u1) -> 
283          if CoercDb.eq_carr x src then Some (src,u1,u2) else None)
284     l1
285   in
286   uniq2 (List.flatten (List.map is_in_l1 l2))
287 ;;
288
289 (* grow tgt gives all the (src,u) such that u:tgt->src *)
290 let grow tgt = 
291   uniq ((tgt,None)::(get_coercions_to tgt))
292 ;;
293
294 let lb (c,_,_) = 
295   let l = get_coercions_from c in
296   fun (x,_,_) -> List.exists (fun (y,_) -> CoercDb.eq_carr x y) l
297 ;;
298
299 (* given the set { (s,u1,u2) | u1:s->t1 /\ u2:s->t2 } removes the elements 
300  * (s,_,_) such that (s',_,_) is in the set and there exists a coercion s->s' *)
301 let rec min acc skipped = function
302   | c::tl -> 
303     if List.exists (lb c) (tl@acc) 
304     then min acc (c::skipped) tl else min (c::acc) skipped tl
305   | [] -> acc, skipped
306 ;;
307
308
309 let sort l = 
310   let low, high = min [] [] l in low @ high
311 ;;
312
313 let meets metasenv subst context (grow_left,left) (grow_right,right) =
314   let saturate metasenv uo =
315     match uo with 
316     | None -> metasenv, None
317     | Some u -> 
318         match saturate_coercion [u] metasenv subst context with
319         | [metasenv, sat, last] -> metasenv, Some (sat, last)
320         | _ -> assert false
321   in
322   List.map 
323     (fun (c,uo1,uo2) -> 
324       let metasenv, uo1 = saturate metasenv uo1 in
325       let metasenv, uo2 = saturate metasenv uo2 in
326       c,metasenv, uo1, uo2)
327     (sort (intersect 
328       (if grow_left then grow left else [left,None]) 
329       (if grow_right then grow right else [right,None])))
330 ;;
331
332 (* EOF *)