]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/library/cicCoercion.ml
More exceptions pretty-printed.
[helm.git] / helm / software / components / library / cicCoercion.ml
1 (* Copyright (C) 2005, 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://helm.cs.unibo.it/
24  *)
25
26 (* $Id$ *)
27
28 let debug = false
29 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
30
31 (* given the new coercion uri from src to tgt returns the list 
32  * of new coercions to create. hte list elements are
33  * (source, list of coercions to follow, target)
34  *)
35 let get_closure_coercions src tgt uri coercions =
36   let eq_carr s t = 
37     try
38       CoercDb.eq_carr s t
39     with
40     | CoercDb.EqCarrNotImplemented _ | CoercDb.EqCarrOnNonMetaClosed -> false
41   in
42   match src,tgt with
43   | CoercDb.Uri _, CoercDb.Uri _ ->
44       let c_from_tgt = 
45         List.filter 
46           (fun (f,t,_) -> eq_carr f tgt (*&& not (eq_carr t src)*)) 
47           coercions 
48       in
49       let c_to_src = 
50         List.filter 
51           (fun (f,t,_) -> eq_carr t src (*&& not (eq_carr f tgt)*)) 
52           coercions 
53       in
54         (HExtlib.flatten_map 
55           (fun (_,t,ul) -> List.map (fun u -> src,[uri; u],t) ul) c_from_tgt) @
56         (HExtlib.flatten_map 
57           (fun (s,_,ul) -> List.map (fun u -> s,[u; uri],tgt) ul) c_to_src) @
58         (HExtlib.flatten_map 
59           (fun (s,_,u1l) ->
60             HExtlib.flatten_map 
61               (fun (_,t,u2l) ->
62                 HExtlib.flatten_map
63                   (fun u1 ->
64                     List.map 
65                       (fun u2 -> (s,[u1;uri;u2],t)) 
66                       u2l)
67                   u1l) 
68               c_from_tgt) 
69           c_to_src)
70   | _ -> [] (* do not close in case source or target is not an indty ?? *)
71 ;;
72
73 let obj_attrs n = [`Class (`Coercion n); `Generated]
74
75 exception UnableToCompose
76
77 (* generate_composite_closure (c2 (c1 s)) in the universe graph univ *)
78 let generate_composite_closure rt c1 c2 univ arity =
79   let module RT = RefinementTool in
80   let c1_ty,univ = CicTypeChecker.type_of_aux' [] [] c1 univ in
81   let c2_ty,univ = CicTypeChecker.type_of_aux' [] [] c2 univ in
82   let rec mk_implicits = function
83     | 0 -> [] | n -> (Cic.Implicit None) :: mk_implicits (n-1)
84   in
85   let rec mk_lambda_spline c namer = function
86     | 0 -> c
87     | n -> 
88         Cic.Lambda 
89           (namer n,
90            (Cic.Implicit None), 
91            mk_lambda_spline c namer (n-1))
92   in 
93   let count_saturations_needed t arity = 
94     let rec aux acc n = function
95       | Cic.Prod (name,src, ((Cic.Prod _) as t)) -> 
96           aux (acc@[name]) (n+1) t
97       | _ -> n,acc
98     in
99     let len,names = aux [] 0 t in
100     let len = len - arity in
101     List.fold_left 
102       (fun (n,l) x -> if n < len then n+1,l@[x] else n,l) (0,[]) 
103       names
104   in
105   let compose c1 nc1 c2 nc2 =
106     Cic.Lambda 
107       (Cic.Name "x",
108       (Cic.Implicit None),
109       Cic.Appl ( c2 :: mk_implicits nc2 @ 
110         [ Cic.Appl ( c1 :: mk_implicits nc1 @ [Cic.Rel 1]) ]))
111   in
112 (*
113   let order_metasenv metasenv = 
114     let module OT = struct type t = int let compare = Pervasives.compare end in
115     let module S = HTopoSort.Make (OT) in
116     let dep i = 
117       let _,_,ty = List.find (fun (j,_,_) -> j=i) metasenv in
118       let metas = List.map fst (CicUtil.metas_of_term ty) in
119       HExtlib.list_uniq (List.sort Pervasives.compare metas)
120     in
121     let om =  
122       S.topological_sort (List.map (fun (i,_,_) -> i) metasenv) dep 
123     in
124     List.map (fun i -> List.find (fun (j,_,_) -> i=j) metasenv) om
125   in 
126 *)
127   let rec create_subst_from_metas_to_rels n = function 
128     | [] -> []
129     | (metano, ctx, ty)::tl -> 
130         (metano,(ctx,Cic.Rel (n+1),ty)) ::
131           create_subst_from_metas_to_rels (n-1) tl
132   in
133   let split_metasenv metasenv n =
134     List.partition (fun (_,ctx,_) -> List.length ctx > n) metasenv
135   in
136   let purge_unused_lambdas metasenv t =
137     let rec aux = function
138         | Cic.Lambda (_, Cic.Meta (i,_), t) when  
139           List.exists (fun (j,_,_) -> j = i) metasenv ->
140             aux (CicSubstitution.subst (Cic.Rel ~-100) t)
141         | Cic.Lambda (name, s, t) -> 
142             Cic.Lambda (name, s, aux t)
143         | t -> t
144     in
145     aux t
146   in
147   let order_body_menv term body_metasenv =
148     let rec purge_lambdas = function
149       | Cic.Lambda (_,_,t) -> purge_lambdas t
150       | t -> t
151     in
152     let skip_appl = function | Cic.Appl l -> List.tl l | _ -> assert false in
153     let metas_that_saturate l =
154       List.fold_left 
155         (fun (acc,n) t ->
156           let metas = CicUtil.metas_of_term t in
157           let metas = List.map fst metas in
158           let metas = 
159             List.filter 
160               (fun i -> List.for_all (fun (j,_) -> j<>i) acc) 
161               metas 
162           in
163           let metas = List.map (fun i -> i,n) metas in
164           metas @ acc, n+1)
165         ([],0) l
166     in
167     let l_c2 = skip_appl (purge_lambdas term) in
168     let l_c1 = 
169       match HExtlib.list_last l_c2 with
170       | Cic.Appl l -> List.tl l
171       | _ -> assert false
172     in
173     (* i should cut off the laet elem of l_c2 *)
174     let meta2no = fst (metas_that_saturate (l_c1 @ l_c2)) in
175     List.sort 
176       (fun (i,ctx1,ty1) (j,ctx1,ty1) -> 
177           try List.assoc i meta2no -  List.assoc j meta2no 
178           with Not_found -> assert false) 
179       body_metasenv
180   in
181   let namer l n = 
182     let l = List.map (function Cic.Name s -> s | _ -> "A") l in
183     let l = List.fold_left
184       (fun acc s -> 
185         let rec add' s =
186           if List.exists ((=) s) acc then add' (s^"'") else s
187         in
188         acc@[add' s])
189       [] l
190     in
191     let l = List.rev l in 
192     Cic.Name (List.nth l (n-1))
193   in 
194   debug_print (lazy ("\nCOMPOSING"));
195   debug_print (lazy (" c1= "^CicPp.ppterm c1 ^"  :  "^ CicPp.ppterm c1_ty));
196   debug_print (lazy (" c2= "^CicPp.ppterm c2 ^"  :  "^ CicPp.ppterm c2_ty));
197   let saturations_for_c1, names_c1 = count_saturations_needed c1_ty 0 in 
198   let saturations_for_c2, names_c2 = count_saturations_needed c2_ty arity in
199   let c = compose c1 saturations_for_c1 c2 saturations_for_c2 in
200   let spline_len = saturations_for_c1 + saturations_for_c2 in
201   let c = mk_lambda_spline c (namer (names_c1 @ names_c2)) spline_len in
202   debug_print (lazy ("COMPOSTA: " ^ CicPp.ppterm c));
203   let c, univ = 
204     match rt.RT.type_of_aux' [] [] c univ with
205     | RT.Success (term, ty, metasenv, ugraph) -> 
206         debug_print(lazy("COMPOSED REFINED: "^CicPp.ppterm term));
207 (*         let metasenv = order_metasenv metasenv in *)
208 (*         debug_print(lazy("ORDERED MENV: "^rt.RT.ppmetasenv [] metasenv)); *)
209         let body_metasenv, lambdas_metasenv = 
210           split_metasenv metasenv spline_len 
211         in
212 (*
213         debug_print(lazy("B_MENV: "^rt.RT.ppmetasenv [] body_metasenv));
214         debug_print(lazy("L_MENV: "^rt.RT.ppmetasenv [] lambdas_metasenv));
215 *)
216         let body_metasenv = order_body_menv term body_metasenv in
217         debug_print(lazy("ORDERED_B_MENV: "^rt.RT.ppmetasenv [] body_metasenv));
218         let subst = create_subst_from_metas_to_rels spline_len body_metasenv in
219         debug_print (lazy("SUBST: "^rt.RT.ppsubst body_metasenv subst));
220         let term = rt.RT.apply_subst subst term in
221         debug_print (lazy ("COMPOSED SUBSTITUTED: " ^ CicPp.ppterm term));
222         (match rt.RT.type_of_aux' metasenv [] term ugraph with
223         | RT.Success (term, ty, metasenv, ugraph) -> 
224             let body_metasenv, lambdas_metasenv = 
225               split_metasenv metasenv spline_len 
226             in
227             let term = purge_unused_lambdas lambdas_metasenv term in
228             debug_print (lazy ("COMPOSED: " ^ CicPp.ppterm term));
229             term, ugraph
230         | RT.Exception s -> debug_print s; raise UnableToCompose)
231     | RT.Exception s -> debug_print s; raise UnableToCompose
232   in  
233   let c_ty,univ = 
234     try 
235       CicTypeChecker.type_of_aux' [] [] c univ
236     with CicTypeChecker.TypeCheckerFailure s ->
237       debug_print (lazy (Printf.sprintf "Generated composite coercion:\n%s\n%s" 
238         (CicPp.ppterm c) (Lazy.force s)));
239       raise UnableToCompose
240   in
241   let cleaned_ty =
242     FreshNamesGenerator.clean_dummy_dependent_types c_ty 
243   in
244   let obj = Cic.Constant ("xxxx",Some c,cleaned_ty,[],obj_attrs arity) in 
245     obj,univ
246 ;;
247
248 (* removes from l the coercions that are in !coercions *)
249 let filter_duplicates l coercions =
250   List.filter (
251       fun (src,l1,tgt) ->
252         not (List.exists (fun (s,t,l2) -> 
253           CoercDb.eq_carr s src && 
254           CoercDb.eq_carr t tgt &&
255           try 
256             List.for_all2 (fun u1 u2 -> UriManager.eq u1 u2) l1 l2
257           with
258           | Invalid_argument "List.for_all2" -> false)
259         coercions))
260   l
261
262 let mangle s t l = 
263   (*List.fold_left
264     (fun s x -> s ^ "_" ^ x)
265     (s ^ "_OF_" ^ t ^ "_BY" ^ string_of_int (List.length l)) l*)
266   s ^ "_OF_" ^ t
267 ;;
268
269 exception ManglingFailed of string 
270
271 let number_if_already_defined buri name l =
272   let err () =
273     raise 
274       (ManglingFailed 
275         ("Unable to give an altenative name to " ^ buri ^ "/" ^ name ^ ".con"))
276   in
277   let rec aux n =
278     let suffix = if n > 0 then string_of_int n else "" in
279     let suri = buri ^ "/" ^ name ^ suffix ^ ".con" in
280     let uri = UriManager.uri_of_string suri in
281     let retry () = 
282       if n < 100 then 
283         begin
284           HLog.warn ("Uri " ^ suri ^ " already exists.");
285           aux (n+1)
286         end
287       else
288         err ()
289     in
290     if List.exists (UriManager.eq uri) l then retry ()
291     else
292       try
293         let _  = Http_getter.resolve' ~writable:true uri in
294         if Http_getter.exists' uri then retry () else uri
295       with 
296       | Http_getter_types.Key_not_found _ -> uri
297       | Http_getter_types.Unresolvable_URI _ -> assert false
298   in
299   aux 0
300 ;;
301   
302 (* given a new coercion uri from src to tgt returns 
303  * a list of (new coercion uri, coercion obj, universe graph) 
304  *)
305 let close_coercion_graph rt src tgt uri baseuri =
306   (* check if the coercion already exists *)
307   let coercions = CoercDb.to_list () in
308   let todo_list = get_closure_coercions src tgt uri coercions in
309   let todo_list = filter_duplicates todo_list coercions in
310   try
311     let new_coercions = 
312       List.fold_left (
313         fun acc (src, l , tgt) ->
314           try 
315             (match l with
316             | [] -> assert false 
317             | he :: tl ->
318                 let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in
319                 let first_step = 
320                   Cic.Constant ("", 
321                     Some (CoercDb.term_of_carr (CoercDb.Uri he)),
322                     Cic.Sort Cic.Prop, [], obj_attrs arity)
323                 in
324                 let o,_ = 
325                   List.fold_left (fun (o,univ) coer ->
326                     match o with 
327                     | Cic.Constant (_,Some c,_,[],_) ->
328                         generate_composite_closure rt c 
329                           (CoercDb.term_of_carr (CoercDb.Uri coer)) univ arity
330                     | _ -> assert false 
331                   ) (first_step, CicUniv.empty_ugraph) tl
332                 in
333                 let name_src = CoercDb.name_of_carr src in
334                 let name_tgt = CoercDb.name_of_carr tgt in
335                 let by = List.map UriManager.name_of_uri l in
336                 let name = mangle name_tgt name_src by in
337                 let c_uri = 
338                   number_if_already_defined baseuri name 
339                     (List.map (fun (_,_,u,_) -> u) acc) 
340                 in
341                 let named_obj = 
342                   match o with
343                   | Cic.Constant (_,bo,ty,vl,attrs) ->
344                       Cic.Constant (name,bo,ty,vl,attrs)
345                   | _ -> assert false 
346                 in
347                   (src,tgt,c_uri,named_obj))::acc
348           with UnableToCompose -> acc
349       ) [] todo_list
350     in
351     new_coercions
352   with ManglingFailed s -> HLog.error s; []
353 ;;
354