]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/library/librarySync.ml
select honors the substitution
[helm.git] / helm / software / components / library / librarySync.ml
1 (* Copyright (C) 2004-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 object_declaration_hook = ref []
29 let add_object_declaration_hook f =
30  object_declaration_hook := f :: !object_declaration_hook
31
32 exception AlreadyDefined of UriManager.uri
33
34 type coercion_decl = 
35   UriManager.uri -> int (* arity *) ->
36    int (* saturations *) -> string (* baseuri *) ->
37     UriManager.uri list (* lemmas (new objs) *)
38
39   
40 let stack = ref [];;
41
42 let push () =
43   stack := CoercDb.dump () :: !stack;
44   CoercDb.restore CoercDb.empty_coerc_db;
45 ;;
46
47 let pop () =
48   match !stack with
49   | [] -> raise (Failure "Unable to POP from librarySync.ml")
50   | db :: tl -> 
51       stack := tl;
52       CoercDb.restore db;
53 ;;
54
55 let uris_of_obj uri =
56  let innertypesuri = UriManager.innertypesuri_of_uri uri in
57  let bodyuri = UriManager.bodyuri_of_uri uri in
58  let univgraphuri = UriManager.univgraphuri_of_uri uri in
59   innertypesuri,bodyuri,univgraphuri
60
61 let paths_and_uris_of_obj uri =
62   let resolved = Http_getter.filename' ~local:true ~writable:true uri in
63   let basepath = Filename.dirname resolved in
64   let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in
65   let innertypesfilename=(UriManager.nameext_of_uri innertypesuri)^".xml.gz"in
66   let innertypespath = basepath ^ "/" ^ innertypesfilename in
67   let xmlfilename = (UriManager.nameext_of_uri uri) ^ ".xml.gz" in
68   let xmlpath = basepath ^ "/" ^ xmlfilename in
69   let xmlbodyfilename = (UriManager.nameext_of_uri uri) ^ ".body.xml.gz" in
70   let xmlbodypath = basepath ^ "/" ^  xmlbodyfilename in
71   let xmlunivgraphfilename=(UriManager.nameext_of_uri univgraphuri)^".xml.gz"in
72   let xmlunivgraphpath = basepath ^ "/" ^ xmlunivgraphfilename in
73   xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri, 
74   xmlunivgraphpath, univgraphuri
75
76 let save_object_to_disk uri obj ugraph univlist =
77   let write f x =
78     if not (Helm_registry.get_opt_default 
79               Helm_registry.bool "matita.nodisk" ~default:false) 
80     then      
81       f x
82   in
83   let ensure_path_exists path =
84     let dir = Filename.dirname path in
85     HExtlib.mkdir dir
86   in
87   (* generate annobj, ids_to_inner_sorts and ids_to_inner_types *)
88   let annobj, innertypes, ids_to_inner_sorts, generate_attributes =
89    if Helm_registry.get_bool "matita.system" &&
90       not (Helm_registry.get_bool "matita.noinnertypes")
91    then
92     let annobj, _, _, ids_to_inner_sorts, ids_to_inner_types, _, _ =
93      Cic2acic.acic_object_of_cic_object obj 
94     in
95     let innertypesxml = 
96      Cic2Xml.print_inner_types
97       uri ~ids_to_inner_sorts ~ids_to_inner_types ~ask_dtd_to_the_getter:false
98     in
99     annobj, Some innertypesxml, Some ids_to_inner_sorts, false
100    else 
101     let annobj = Cic2acic.plain_acic_object_of_cic_object obj in  
102     annobj, None, None, true 
103   in 
104   (* prepare XML *)
105   let xml, bodyxml =
106    Cic2Xml.print_object
107     uri ?ids_to_inner_sorts ~ask_dtd_to_the_getter:false 
108     ~generate_attributes annobj 
109   in    
110   let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri, 
111       xmlunivgraphpath, univgraphuri = 
112     paths_and_uris_of_obj uri 
113   in
114   write (List.iter HExtlib.mkdir) (List.map Filename.dirname [xmlpath]);
115   (* now write to disk *)
116   write ensure_path_exists xmlpath;
117   write (Xml.pp ~gzip:true xml) (Some xmlpath);
118   write (CicUniv.write_xml_of_ugraph xmlunivgraphpath ugraph) univlist;
119   (* we return a list of uri,path we registered/created *)
120   (uri,xmlpath) ::
121   (univgraphuri,xmlunivgraphpath) ::
122     (* now the optional inner types, both write and register *)
123     (match innertypes with 
124      | None -> []
125      | Some innertypesxml ->
126          write ensure_path_exists innertypespath;
127          write (Xml.pp ~gzip:true innertypesxml) (Some innertypespath);
128          [innertypesuri, innertypespath]
129     ) @
130     (* now the optional body, both write and register *)
131     (match bodyxml,bodyuri with
132        None,_ -> []
133      | Some bodyxml,Some bodyuri->
134          write ensure_path_exists xmlbodypath;
135          write (Xml.pp ~gzip:true bodyxml) (Some xmlbodypath);
136          [bodyuri, xmlbodypath]
137      | _-> assert false) 
138
139
140 let typecheck_obj =
141  let profiler = HExtlib.profile "add_obj.typecheck_obj" in
142   fun uri obj -> profiler.HExtlib.profile (CicTypeChecker.typecheck_obj uri) obj
143
144 let index_obj =
145  let profiler = HExtlib.profile "add_obj.index_obj" in
146   fun ~dbd ~uri ->
147    profiler.HExtlib.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri
148
149 let remove_obj uri =
150   let derived_uris_of_uri uri =
151    let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in
152     innertypesuri::univgraphuri::(match bodyuri with None -> [] | Some u -> [u])
153   in
154   let uris_to_remove =
155    if UriManager.uri_is_ind uri then LibraryDb.xpointers_of_ind uri else [uri]
156   in
157   let files_to_remove = uri :: derived_uris_of_uri uri in   
158   List.iter 
159    (fun uri -> 
160      (try
161        let file = Http_getter.resolve' ~local:true ~writable:true uri in
162         HExtlib.safe_remove file;
163         HExtlib.rmdir_descend (Filename.dirname file)
164      with Http_getter_types.Key_not_found _ -> ());
165    ) files_to_remove ;
166   List.iter (fun uri -> ignore (LibraryDb.remove_uri uri)) uris_to_remove ;
167   CicEnvironment.remove_obj uri
168 ;;
169
170 let rec add_obj uri obj ~pack_coercion_obj =
171   let obj = 
172     if CoercDb.is_a_coercion (Cic.Const (uri, [])) = None
173     then pack_coercion_obj obj
174     else obj 
175   in
176   let dbd = LibraryDb.instance () in
177   if CicEnvironment.in_library uri then raise (AlreadyDefined uri);
178   begin (* ATOMIC *)
179     typecheck_obj uri obj; (* 1 *)
180     let obj, ugraph, univlist = 
181       try CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri 
182       with CicEnvironment.Object_not_found _ -> assert false
183     in
184     try 
185       index_obj ~dbd ~uri; (* 2 must be in the env *)
186       try
187         (*3*)
188         let new_stuff = save_object_to_disk uri obj ugraph univlist in
189         try 
190          HLog.message
191           (Printf.sprintf "%s defined" (UriManager.string_of_uri uri))
192         with exc ->
193           List.iter HExtlib.safe_remove (List.map snd new_stuff); (* -3 *)
194           raise exc
195       with exc ->
196         ignore(LibraryDb.remove_uri uri); (* -2 *)
197         raise exc
198     with exc ->
199       CicEnvironment.remove_obj uri; (* -1 *)
200       raise exc
201   end; 
202   let added = ref [] in
203   let add_obj_with_parachute u o =
204     added := u :: !added;
205     add_obj u o ~pack_coercion_obj in
206   let old_db = CoercDb.dump () in
207   try
208     List.fold_left 
209       (fun lemmas f ->
210         f ~add_obj:add_obj_with_parachute 
211         ~add_coercion:(add_coercion ~add_composites:true ~pack_coercion_obj)
212         uri obj @ lemmas)
213       [] !object_declaration_hook
214   with exn -> 
215     List.iter remove_obj !added;
216     remove_obj uri;
217     CoercDb.restore old_db;
218     raise exn
219   (* /ATOMIC *)
220
221 and
222  add_coercion ~add_composites ~pack_coercion_obj uri arity saturations baseuri 
223 =
224   let coer_ty,_ =
225     let coer = CicUtil.term_of_uri uri in
226     CicTypeChecker.type_of_aux' [] [] coer CicUniv.oblivion_ugraph 
227   in
228   (* we have to get the source and the tgt type uri
229    * in Coq syntax we have already their names, but
230    * since we don't support Funclass and similar I think
231    * all the coercion should be of the form
232    * (A:?)(B:?)T1->T2
233    * So we should be able to extract them from the coercion type
234    * 
235    * Currently only (_:T1)T2 is supported.
236    * should we saturate it with metas in case we insert it?
237    * 
238    *)
239   let spine2list ty =
240     let rec aux = function
241       | Cic.Prod( _, src, tgt) -> src::aux tgt
242       | t -> [t]
243     in
244     aux ty
245   in
246   let src_carr, tgt_carr, no_args = 
247     let get_classes arity saturations l = 
248       (* this is the ackerman's function revisited *)
249       let rec aux = function
250          0,0,None,tgt::src::_ -> src,Some (`Class tgt)
251        | 0,0,target,src::_ -> src,target
252        | 0,saturations,None,tgt::tl -> aux (0,saturations,Some (`Class tgt),tl)
253        | 0,saturations,target,_::tl -> aux (0,saturations - 1,target,tl)
254        | arity,saturations,None,_::tl -> 
255             aux (arity, saturations, Some `Funclass, tl)
256        | arity,saturations,target,_::tl -> 
257             aux (arity - 1, saturations, target, tl)
258        | _ -> assert false
259       in
260        aux (arity,saturations,None,List.rev l)
261     in
262     let types = spine2list coer_ty in
263     let src,tgt = get_classes arity saturations types in
264      CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src) 0,
265      (match tgt with
266      | None -> assert false
267      | Some `Funclass -> CoercDb.coerc_carr_of_term (Cic.Implicit None) arity
268      | Some (`Class tgt) ->
269          CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt) 0),
270      List.length types - 1
271   in
272   let already_in_obj src_carr tgt_carr uri obj = 
273      List.exists 
274       (fun (s,t,ul) -> 
275         if not (CoercDb.eq_carr s src_carr && 
276                 CoercDb.eq_carr t tgt_carr)
277         then false 
278         else
279         List.exists 
280          (fun u,_,_ -> 
281            let bo, ty = 
282             match obj with 
283             | Cic.Constant (_, Some bo, ty, _, _) -> bo, ty
284             | _ -> 
285                (* this is not a composite coercion, thus the uri is valid *)
286               let bo = CicUtil.term_of_uri uri in
287               bo,
288               fst (CicTypeChecker.type_of_aux' [] [] bo
289               CicUniv.oblivion_ugraph)
290            in
291            let are_body_convertible =
292             fst (CicReduction.are_convertible [] (CicUtil.term_of_uri u) bo
293                   CicUniv.oblivion_ugraph)
294            in
295            if not are_body_convertible then
296              (HLog.warn
297               ("Coercions " ^ 
298                UriManager.string_of_uri u ^ " and " ^ UriManager.string_of_uri
299                uri^" are not convertible, but are between the same nodes.\n"^
300                "From now on unification can fail randomly.");
301              false)
302            else
303              match t, tgt_carr with
304              | CoercDb.Sort (Cic.Type i), CoercDb.Sort (Cic.Type j)
305              | CoercDb.Sort (Cic.CProp i), CoercDb.Sort (Cic.CProp j)
306               when not (CicUniv.eq i j) -> 
307               (HLog.warn 
308                ("Coercion " ^ UriManager.string_of_uri uri ^ " has the same " ^
309                "body of " ^ UriManager.string_of_uri u ^ " but lives in a " ^
310                "different universe : " ^ 
311                  CicUniv.string_of_universe j ^ " <> " ^
312                  CicUniv.string_of_universe i); false)
313              | CoercDb.Sort Cic.Prop , CoercDb.Sort Cic.Prop 
314              | CoercDb.Sort (Cic.Type _) , CoercDb.Sort (Cic.Type _)
315              | CoercDb.Sort (Cic.CProp _), CoercDb.Sort (Cic.CProp _) -> 
316                 (HLog.warn 
317                 ("Skipping coercion " ^ UriManager.name_of_uri uri ^ " since "^
318                  "it is a duplicate of " ^ UriManager.string_of_uri u);
319                 true) 
320              | CoercDb.Sort s1, CoercDb.Sort s2 -> 
321               (HLog.warn 
322                ("Coercion " ^ UriManager.string_of_uri uri ^ " has the same " ^
323                "body of " ^ UriManager.string_of_uri u ^ " but lives in a " ^
324                "different universe : " ^ 
325                  CicPp.ppterm (Cic.Sort s1) ^ " <> " ^ 
326                  CicPp.ppterm (Cic.Sort s2)); false)
327              | _ -> 
328                 let ty', _ = 
329                   CicTypeChecker.type_of_aux' [] [] (CicUtil.term_of_uri u) 
330                   CicUniv.oblivion_ugraph
331                 in
332                 if CicUtil.alpha_equivalence ty ty' then
333                 (HLog.warn 
334                 ("Skipping coercion " ^ UriManager.name_of_uri uri ^ " since "^
335                  "it is a duplicate of " ^ UriManager.string_of_uri u);
336                 true)
337                 else false
338                 
339                 )
340          ul)
341       (CoercDb.to_list ())
342   in
343   let cpos = no_args - arity - saturations - 1 in 
344   if not add_composites then
345     (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations, cpos); [])
346   else
347     let _ = 
348       if already_in_obj src_carr tgt_carr uri
349        (fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri)) then
350         raise (AlreadyDefined uri);
351     in
352     let new_coercions = 
353       CicCoercion.close_coercion_graph src_carr tgt_carr uri saturations
354        baseuri
355     in
356     let new_coercions = 
357       List.filter (fun (s,t,u,_,obj,_,_) -> not(already_in_obj s t u obj))
358       new_coercions 
359     in
360     (* update the DB *)
361     let lemmas = 
362       List.fold_left
363         (fun acc (src,tgt,uri,saturations,obj,arity,cpos) ->
364            CoercDb.add_coercion (src,tgt,uri,saturations,cpos);
365            let acc = add_obj uri obj pack_coercion_obj @ uri::acc in
366            acc)
367         [] new_coercions
368     in
369     CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations, cpos);
370 (*     CoercDb.prefer uri; *)
371     lemmas
372 ;;
373
374