]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/library/librarySync.ml
fast and sound registry lists
[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 (fun _ _ -> ());;
29 let set_object_declaration_hook f =
30  object_declaration_hook := f
31
32 exception AlreadyDefined of UriManager.uri
33
34 let auxiliary_lemmas_hashtbl = UriManager.UriHashtbl.create 29
35
36 (* uri |-->  (derived_coercions_in_the_coercion_DB, derived_coercions_in_lib)
37  * 
38  * in case of remove_coercion uri, the first component is removed from the
39  * coercion DB, while the second is passed to remove_obj (and is not [] only if
40  * add_coercion is called with add_composites 
41  * *)
42 let coercion_hashtbl = UriManager.UriHashtbl.create 3
43
44 let uris_of_obj uri =
45  let innertypesuri = UriManager.innertypesuri_of_uri uri in
46  let bodyuri = UriManager.bodyuri_of_uri uri in
47  let univgraphuri = UriManager.univgraphuri_of_uri uri in
48   innertypesuri,bodyuri,univgraphuri
49
50 let paths_and_uris_of_obj uri =
51   let resolved = Http_getter.filename' ~local:true ~writable:true uri in
52   let basepath = Filename.dirname resolved in
53   let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in
54   let innertypesfilename=(UriManager.nameext_of_uri innertypesuri)^".xml.gz"in
55   let innertypespath = basepath ^ "/" ^ innertypesfilename in
56   let xmlfilename = (UriManager.nameext_of_uri uri) ^ ".xml.gz" in
57   let xmlpath = basepath ^ "/" ^ xmlfilename in
58   let xmlbodyfilename = (UriManager.nameext_of_uri uri) ^ ".body.xml.gz" in
59   let xmlbodypath = basepath ^ "/" ^  xmlbodyfilename in
60   let xmlunivgraphfilename=(UriManager.nameext_of_uri univgraphuri)^".xml.gz"in
61   let xmlunivgraphpath = basepath ^ "/" ^ xmlunivgraphfilename in
62   xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri, 
63   xmlunivgraphpath, univgraphuri
64
65 let save_object_to_disk uri obj ugraph univlist =
66   let write f x =
67     if not (Helm_registry.get_opt_default 
68               Helm_registry.bool "matita.nodisk" ~default:false) 
69     then      
70       f x
71   in
72   let ensure_path_exists path =
73     let dir = Filename.dirname path in
74     HExtlib.mkdir dir
75   in
76   (* generate annobj, ids_to_inner_sorts and ids_to_inner_types *)
77   let annobj, innertypes, ids_to_inner_sorts, generate_attributes =
78    if Helm_registry.get_bool "matita.system" &&
79       not (Helm_registry.get_bool "matita.noinnertypes")
80    then
81     let annobj, _, _, ids_to_inner_sorts, ids_to_inner_types, _, _ =
82      Cic2acic.acic_object_of_cic_object obj 
83     in
84     let innertypesxml = 
85      Cic2Xml.print_inner_types
86       uri ~ids_to_inner_sorts ~ids_to_inner_types ~ask_dtd_to_the_getter:false
87     in
88     annobj, Some innertypesxml, Some ids_to_inner_sorts, false
89    else 
90     let annobj = Cic2acic.plain_acic_object_of_cic_object obj in  
91     annobj, None, None, true 
92   in 
93   (* prepare XML *)
94   let xml, bodyxml =
95    Cic2Xml.print_object
96     uri ?ids_to_inner_sorts ~ask_dtd_to_the_getter:false 
97     ~generate_attributes annobj 
98   in    
99   let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri, 
100       xmlunivgraphpath, univgraphuri = 
101     paths_and_uris_of_obj uri 
102   in
103   write (List.iter HExtlib.mkdir) (List.map Filename.dirname [xmlpath]);
104   (* now write to disk *)
105   write ensure_path_exists xmlpath;
106   write (Xml.pp ~gzip:true xml) (Some xmlpath);
107   write (CicUniv.write_xml_of_ugraph xmlunivgraphpath ugraph) univlist;
108   (* we return a list of uri,path we registered/created *)
109   (uri,xmlpath) ::
110   (univgraphuri,xmlunivgraphpath) ::
111     (* now the optional inner types, both write and register *)
112     (match innertypes with 
113      | None -> []
114      | Some innertypesxml ->
115          write ensure_path_exists innertypespath;
116          write (Xml.pp ~gzip:true innertypesxml) (Some innertypespath);
117          [innertypesuri, innertypespath]
118     ) @
119     (* now the optional body, both write and register *)
120     (match bodyxml,bodyuri with
121        None,_ -> []
122      | Some bodyxml,Some bodyuri->
123          write ensure_path_exists xmlbodypath;
124          write (Xml.pp ~gzip:true bodyxml) (Some xmlbodypath);
125          [bodyuri, xmlbodypath]
126      | _-> assert false) 
127
128
129 let typecheck_obj =
130  let profiler = HExtlib.profile "add_obj.typecheck_obj" in
131   fun uri obj -> profiler.HExtlib.profile (CicTypeChecker.typecheck_obj uri) obj
132
133 let index_obj =
134  let profiler = HExtlib.profile "add_obj.index_obj" in
135   fun ~dbd ~uri ->
136    profiler.HExtlib.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri
137
138 let add_single_obj uri obj refinement_toolkit =
139   let module RT = RefinementTool in
140   let obj = 
141     if (*List.mem `Generated (CicUtil.attributes_of_obj obj) &&*)
142        not (CoercDb.is_a_coercion' (Cic.Const (uri, [])))
143     then
144       refinement_toolkit.RT.pack_coercion_obj obj
145     else
146       obj 
147   in
148   let dbd = LibraryDb.instance () in
149   if CicEnvironment.in_library uri then
150     raise (AlreadyDefined uri)
151   else begin
152     (*CicUniv.reset_spent_time ();
153     let before = Unix.gettimeofday () in*)
154     typecheck_obj uri obj; (* 1 *)
155     (*let after = Unix.gettimeofday () in
156     let univ_time = CicUniv.get_spent_time () in
157     let total_time = after -. before in
158     prerr_endline 
159       (Printf.sprintf "QED: %%univ = %2.5f, total = %2.5f, univ = %2.5f, %s\n" 
160       (univ_time *. 100. /. total_time) (total_time) (univ_time)
161       (UriManager.name_of_uri uri));*)
162     let _, ugraph, univlist = 
163       CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri in
164     try 
165       index_obj ~dbd ~uri; (* 2 must be in the env *)
166       try
167         (*3*)
168         let new_stuff = save_object_to_disk uri obj ugraph univlist in
169         (* EXPERIMENTAL: pretty print the object in natural language *)
170         (try !object_declaration_hook uri obj
171          with exc ->
172           prerr_endline "Error: object_declaration_hook failed");
173         try 
174          HLog.message
175           (Printf.sprintf "%s defined" (UriManager.string_of_uri uri))
176         with exc ->
177           List.iter HExtlib.safe_remove (List.map snd new_stuff); (* -3 *)
178           raise exc
179       with exc ->
180         ignore(LibraryDb.remove_uri uri); (* -2 *)
181         raise exc
182     with exc ->
183       CicEnvironment.remove_obj uri; (* -1 *)
184       raise exc
185   end
186
187 let remove_single_obj uri =
188   let derived_uris_of_uri uri =
189    let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in
190     innertypesuri::univgraphuri::(match bodyuri with None -> [] | Some u -> [u])
191   in
192   let uris_to_remove =
193    if UriManager.uri_is_ind uri then LibraryDb.xpointers_of_ind uri else [uri]
194   in
195   let files_to_remove = uri :: derived_uris_of_uri uri in   
196   List.iter 
197    (fun uri -> 
198      (try
199        let file = Http_getter.resolve' ~local:true ~writable:true uri in
200         HExtlib.safe_remove file;
201         HExtlib.rmdir_descend (Filename.dirname file)
202      with Http_getter_types.Key_not_found _ -> ());
203    ) files_to_remove ;
204   List.iter 
205    (fun uri -> 
206      ignore (LibraryDb.remove_uri uri);
207      (*CoercGraph.remove_coercion uri;*)
208    ) uris_to_remove ;
209   CicEnvironment.remove_obj uri
210
211 (*** GENERATION OF AUXILIARY LEMMAS ***)
212
213 let generate_elimination_principles uri refinement_toolkit =
214   let uris = ref [] in
215   let elim i =
216     let elim sort =
217       try
218         let uri,obj = CicElim.elim_of ~sort uri i in
219           add_single_obj uri obj refinement_toolkit;
220           uris := uri :: !uris
221       with CicElim.Can_t_eliminate -> ()
222     in
223       try
224         List.iter 
225           elim [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ];
226       with exn ->
227         List.iter remove_single_obj !uris;
228         raise exn 
229   in
230   let (obj, univ) = (CicEnvironment.get_obj CicUniv.empty_ugraph uri) in
231     match obj with
232       | Cic.InductiveDefinition (indTypes, _, _, _) ->
233           let counter = ref 0 in
234             List.iter (fun _ -> elim !counter; counter := !counter+1) indTypes;
235             !uris
236       | _  -> 
237           failwith (Printf.sprintf "not an inductive definition (%s)"
238                       (UriManager.string_of_uri uri))
239
240 (* COERCIONS ***********************************************************)
241   
242 let remove_all_coercions () =
243   UriManager.UriHashtbl.clear coercion_hashtbl;
244   CoercDb.remove_coercion (fun (_,_,_,_) -> true)
245
246 let add_coercion ~add_composites refinement_toolkit uri arity saturations
247  baseuri
248 =
249   let coer_ty,_ =
250     let coer = CicUtil.term_of_uri uri in
251     CicTypeChecker.type_of_aux' [] [] coer CicUniv.empty_ugraph 
252   in
253   (* we have to get the source and the tgt type uri
254    * in Coq syntax we have already their names, but
255    * since we don't support Funclass and similar I think
256    * all the coercion should be of the form
257    * (A:?)(B:?)T1->T2
258    * So we should be able to extract them from the coercion type
259    * 
260    * Currently only (_:T1)T2 is supported.
261    * should we saturate it with metas in case we insert it?
262    * 
263    *)
264   let spine2list ty =
265     let rec aux = function
266       | Cic.Prod( _, src, tgt) -> src::aux tgt
267       | t -> [t]
268     in
269     aux ty
270   in
271   let src_carr, tgt_carr = 
272     let get_classes arity saturations l = 
273       (* this is the ackerman's function revisited *)
274       let rec aux = function
275          0,0,None,tgt::src::_ -> src,Some (`Class tgt)
276        | 0,0,target,src::_ -> src,target
277        | 0,saturations,None,tgt::tl -> aux (0,saturations,Some (`Class tgt),tl)
278        | 0,saturations,target,_::tl -> aux (0,saturations - 1,target,tl)
279        | arity,saturations,None,_::tl -> 
280             aux (arity, saturations, Some `Funclass, tl)
281        | arity,saturations,target,_::tl -> 
282             aux (arity - 1, saturations, target, tl)
283        | _ -> assert false
284       in
285        aux (arity,saturations,None,List.rev l)
286     in
287     let types = spine2list coer_ty in
288     let src,tgt = get_classes arity saturations types in
289      CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src),
290      match tgt with
291         None -> assert false
292       | Some `Funclass -> CoercDb.Fun arity
293       | Some (`Class tgt) ->
294          CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt)
295   in
296   let already_in_obj src_carr tgt_carr uri obj = 
297      List.exists 
298       (fun (s,t,ul) -> 
299         List.exists 
300          (fun u,_ -> 
301            let bo = 
302             match obj with 
303             | Cic.Constant (_, Some bo, _, _, _) -> bo
304             | _ -> assert false
305            in
306            CoercDb.eq_carr s src_carr && 
307            CoercDb.eq_carr t tgt_carr &&
308            if fst (CicReduction.are_convertible [] (CicUtil.term_of_uri u) bo
309            CicUniv.oblivion_ugraph)
310            then true else
311             (HLog.warn
312               ("Coercions " ^ 
313                 UriManager.string_of_uri u ^ " and " ^ UriManager.string_of_uri
314                 uri^" are not convertible, but are between the same nodes.\n"^
315                 "From now on unification can fail randomly.");
316              false))
317          ul)
318       (CoercDb.to_list ())
319   in
320   if not add_composites then
321     (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);
322     UriManager.UriHashtbl.add coercion_hashtbl uri ([],[]);
323     [])
324   else
325     let new_coercions = 
326       CicCoercion.close_coercion_graph src_carr tgt_carr uri saturations
327        baseuri
328     in
329     let new_coercions = 
330       List.filter (fun (s,t,u,_,obj,_) -> not(already_in_obj s t u obj))
331       new_coercions 
332     in
333     let composite_uris = List.map (fun (_,_,uri,_,_,_) -> uri) new_coercions in
334     (* update the DB *)
335     List.iter 
336       (fun (src,tgt,uri,saturations,_,_) ->
337         CoercDb.add_coercion (src,tgt,uri,saturations)) 
338       new_coercions;
339     CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);
340     (* add the composites obj and they eventual lemmas *)
341     let lemmas = 
342         List.fold_left
343           (fun acc (_,tgt,uri,saturations,obj,arity) -> 
344             add_single_obj uri obj refinement_toolkit;
345              (uri,arity,saturations)::acc) 
346           [] new_coercions
347     in
348     (* store that composite_uris are related to uri. the first component is
349      * the stuff in the DB while the second is stuff for remove_obj *)
350     (* 
351        prerr_endline ("adding: " ^ 
352          string_of_bool add_composites ^ UriManager.string_of_uri uri);
353        List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
354         composite_uris; 
355     *)
356     UriManager.UriHashtbl.add 
357       coercion_hashtbl uri (composite_uris,composite_uris);
358     (*
359     prerr_endline ("lemmas:");
360       List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
361       lemmas;
362     prerr_endline ("lemmas END");*)
363     lemmas
364 ;;
365
366 let remove_coercion uri =
367   try
368     let (composites_in_db, composites_in_lib) = 
369       UriManager.UriHashtbl.find coercion_hashtbl uri 
370     in
371     (*prerr_endline ("removing: " ^UriManager.string_of_uri uri);
372     List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
373       composites_in_db;*)
374     UriManager.UriHashtbl.remove coercion_hashtbl uri;
375     CoercDb.remove_coercion 
376       (fun (_,_,u,_) -> UriManager.eq uri u);
377     (* remove from the DB *) 
378     List.iter 
379       (fun u -> CoercDb.remove_coercion (fun (_,_,u1,_) -> UriManager.eq u u1))
380       composites_in_db;
381     (* remove composites from the lib *)
382     List.iter remove_single_obj composites_in_lib
383   with
384     Not_found -> HLog.warn "Coercion removal raise Not_found" (* mhh..... *)
385     
386
387 let generate_projections refinement_toolkit uri fields =
388  let uris = ref [] in
389  let projections = 
390    CicRecord.projections_of uri 
391      (List.map (fun (x,_,_) -> x) fields) 
392  in
393   try
394    List.iter2 
395     (fun (uri, name, bo) (_name, coercion, arity) ->
396       let saturations = 0 in
397       try
398        let ty, ugraph =
399          CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in
400        let attrs = [`Class `Projection; `Generated] in
401        let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
402         add_single_obj uri obj refinement_toolkit;
403         let composites = 
404          if coercion then
405             begin
406 (*prerr_endline ("composite for " ^ UriManager.string_of_uri uri);*)
407               (*CSC: I think there is a bug here. The composite coercions
408                 are not remembered in the .moo file. Thus they are re-generated
409                 every time. Right? *)
410               let x = 
411                 add_coercion ~add_composites:true refinement_toolkit uri arity
412                  saturations (UriManager.buri_of_uri uri)
413               in
414 (*prerr_endline ("are: ");
415   List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) x;
416   prerr_endline "---";
417 *)
418               (*CSC: I throw the arity away. See comment above *)
419               List.map (fun u,_,_ -> u) x
420             end
421           else  
422             []
423         in
424         uris := uri :: composites @ !uris
425       with
426          CicTypeChecker.TypeCheckerFailure s ->
427           HLog.message
428            ("Unable to create projection " ^ name ^ " cause: " ^ Lazy.force s);
429        | CicEnvironment.Object_not_found uri ->
430           let depend = UriManager.name_of_uri uri in
431            HLog.message
432             ("Unable to create projection " ^ name ^ " because it requires " ^
433                depend)
434     ) projections fields;
435    !uris
436   with exn ->
437    List.iter remove_single_obj !uris;
438    raise exn
439
440 let build_inversion_principle = ref (fun a b -> assert false);;
441
442 let generate_inversion refinement_toolkit uri obj =
443   List.map 
444     (fun (ind_uri,ind_obj) -> 
445        add_single_obj ind_uri ind_obj refinement_toolkit;ind_uri)
446     (!build_inversion_principle uri obj)
447
448 let
449  generate_sibling_mutual_definitions refinement_toolkit uri attrs name_to_avoid
450 =
451  function
452     Cic.Fix (_,funs) ->
453      snd (
454       List.fold_right
455        (fun (name,idx,ty,bo) (n,uris) ->
456          if name = name_to_avoid then
457           (n+1,uris)
458          else
459           let uri =
460            UriManager.uri_of_string
461             (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in
462           let bo = Cic.Fix (n,funs) in 
463           let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
464            add_single_obj uri obj refinement_toolkit;
465            (n+1,uri::uris)
466        ) funs (1,[]))
467   | Cic.CoFix (_,funs) ->
468      snd (
469       List.fold_right
470        (fun (name,ty,bo) (n,uris) ->
471          if name = name_to_avoid then
472           (n+1,uris)
473          else
474           let uri =
475            UriManager.uri_of_string
476             (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in
477           let bo = Cic.CoFix (n,funs) in 
478           let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
479            add_single_obj uri obj refinement_toolkit;
480            (n+1,uri::uris)
481        ) funs (1,[]))
482   | _ -> assert false
483
484 let add_obj refinement_toolkit uri obj =
485  add_single_obj uri obj refinement_toolkit;
486  let uris = ref [] in
487  let not_debug = not (Helm_registry.get_bool "matita.debug") in
488  try
489   begin
490    match obj with
491     | Cic.Constant (name,Some bo,_,_,attrs) when
492        List.mem (`Flavour `MutualDefinition) attrs ->
493         uris :=
494          !uris @
495            generate_sibling_mutual_definitions refinement_toolkit uri attrs
496             name bo
497     | Cic.Constant _ -> ()
498     | Cic.InductiveDefinition (_,_,_,attrs) ->
499         uris := !uris @ 
500           generate_elimination_principles uri refinement_toolkit;
501         uris := !uris @ generate_inversion refinement_toolkit uri obj;
502         let rec get_record_attrs =
503           function
504           | [] -> None
505           | (`Class (`Record fields))::_ -> Some fields
506           | _::tl -> get_record_attrs tl
507         in
508          (match get_record_attrs attrs with
509          | None -> () (* not a record *)
510          | Some fields ->
511             uris := !uris @ 
512               (generate_projections refinement_toolkit uri fields))
513     | Cic.CurrentProof _
514     | Cic.Variable _ -> assert false
515   end;
516   UriManager.UriHashtbl.add auxiliary_lemmas_hashtbl uri !uris;
517   !uris
518  with 
519  | exn when not_debug ->
520     List.iter remove_single_obj !uris;
521     raise exn
522
523 let remove_obj uri =
524  let uris =
525   try
526    let res = UriManager.UriHashtbl.find auxiliary_lemmas_hashtbl uri in
527     UriManager.UriHashtbl.remove auxiliary_lemmas_hashtbl uri;
528     res
529   with
530     Not_found -> [] (*assert false*)
531  in
532   List.iter remove_single_obj (uri::uris)
533