]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/library/librarySync.ml
fixed recursiveness check
[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 CoercDb.is_a_coercion (Cic.Const (uri, [])) = None
142     then refinement_toolkit.RT.pack_coercion_obj obj
143     else obj 
144   in
145   let dbd = LibraryDb.instance () in
146   if CicEnvironment.in_library uri then
147     raise (AlreadyDefined uri)
148   else begin
149     (*CicUniv.reset_spent_time ();
150     let before = Unix.gettimeofday () in*)
151     typecheck_obj uri obj; (* 1 *)
152     (*let after = Unix.gettimeofday () in
153     let univ_time = CicUniv.get_spent_time () in
154     let total_time = after -. before in
155     prerr_endline 
156       (Printf.sprintf "QED: %%univ = %2.5f, total = %2.5f, univ = %2.5f, %s\n" 
157       (univ_time *. 100. /. total_time) (total_time) (univ_time)
158       (UriManager.name_of_uri uri));*)
159     let obj, ugraph, univlist = 
160       try CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri 
161       with CicEnvironment.Object_not_found _ -> assert false
162     in
163     try 
164       index_obj ~dbd ~uri; (* 2 must be in the env *)
165       try
166         (*3*)
167         let new_stuff = save_object_to_disk uri obj ugraph univlist in
168         (* EXPERIMENTAL: pretty print the object in natural language *)
169         (try !object_declaration_hook uri obj
170          with exc ->
171           prerr_endline ("Error: object_declaration_hook failed"^
172           Printexc.to_string exc));
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, _ = (CicEnvironment.get_obj CicUniv.oblivion_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 stack = ref [];;
247
248 let h2l h =
249   UriManager.UriHashtbl.fold 
250   (fun k v acc -> (k,v) :: acc) h []
251 ;;
252
253 let push () =
254   stack := (CoercDb.dump (), h2l coercion_hashtbl) :: !stack;
255   remove_all_coercions ()
256 ;;
257
258 let pop () =
259   match !stack with
260   | [] -> raise (Failure "Unable to POP from librarySync.ml")
261   | (db,h) :: tl -> 
262       stack := tl;
263       remove_all_coercions ();
264       CoercDb.restore db;
265       List.iter (fun (k,v) -> UriManager.UriHashtbl.add coercion_hashtbl k v)
266       h
267 ;;
268
269 let add_coercion ~add_composites refinement_toolkit uri arity saturations
270  baseuri
271 =
272   let coer_ty,_ =
273     let coer = CicUtil.term_of_uri uri in
274     CicTypeChecker.type_of_aux' [] [] coer CicUniv.oblivion_ugraph 
275   in
276   (* we have to get the source and the tgt type uri
277    * in Coq syntax we have already their names, but
278    * since we don't support Funclass and similar I think
279    * all the coercion should be of the form
280    * (A:?)(B:?)T1->T2
281    * So we should be able to extract them from the coercion type
282    * 
283    * Currently only (_:T1)T2 is supported.
284    * should we saturate it with metas in case we insert it?
285    * 
286    *)
287   let spine2list ty =
288     let rec aux = function
289       | Cic.Prod( _, src, tgt) -> src::aux tgt
290       | t -> [t]
291     in
292     aux ty
293   in
294   let src_carr, tgt_carr, no_args = 
295     let get_classes arity saturations l = 
296       (* this is the ackerman's function revisited *)
297       let rec aux = function
298          0,0,None,tgt::src::_ -> src,Some (`Class tgt)
299        | 0,0,target,src::_ -> src,target
300        | 0,saturations,None,tgt::tl -> aux (0,saturations,Some (`Class tgt),tl)
301        | 0,saturations,target,_::tl -> aux (0,saturations - 1,target,tl)
302        | arity,saturations,None,_::tl -> 
303             aux (arity, saturations, Some `Funclass, tl)
304        | arity,saturations,target,_::tl -> 
305             aux (arity - 1, saturations, target, tl)
306        | _ -> assert false
307       in
308        aux (arity,saturations,None,List.rev l)
309     in
310     let types = spine2list coer_ty in
311     let src,tgt = get_classes arity saturations types in
312      CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src) 0,
313      (match tgt with
314      | None -> assert false
315      | Some `Funclass -> CoercDb.coerc_carr_of_term (Cic.Implicit None) arity
316      | Some (`Class tgt) ->
317          CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt) 0),
318      List.length types - 1
319   in
320   let already_in_obj src_carr tgt_carr uri obj = 
321      List.exists 
322       (fun (s,t,ul) -> 
323         List.exists 
324          (fun u,_,_ -> 
325            let bo = 
326             match obj with 
327             | Cic.Constant (_, Some bo, _, _, _) -> bo
328             | _ -> assert false
329            in
330            CoercDb.eq_carr s src_carr && 
331            CoercDb.eq_carr t tgt_carr &&
332            if fst (CicReduction.are_convertible [] (CicUtil.term_of_uri u) bo
333            CicUniv.oblivion_ugraph)
334            then true else
335             (HLog.warn
336               ("Coercions " ^ 
337                 UriManager.string_of_uri u ^ " and " ^ UriManager.string_of_uri
338                 uri^" are not convertible, but are between the same nodes.\n"^
339                 "From now on unification can fail randomly.");
340              false))
341          ul)
342       (CoercDb.to_list ())
343   in
344   let cpos = no_args - arity - saturations - 1 in 
345   if not add_composites then
346     (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations, cpos);
347     UriManager.UriHashtbl.add coercion_hashtbl uri ([],[]);
348     [])
349   else
350     let new_coercions = 
351       CicCoercion.close_coercion_graph src_carr tgt_carr uri saturations
352        baseuri
353     in
354     let new_coercions = 
355       List.filter (fun (s,t,u,_,obj,_,_) -> not(already_in_obj s t u obj))
356       new_coercions 
357     in
358     let composite_uris = 
359       List.map (fun (_,_,uri,_,_,_,_) -> uri) new_coercions 
360     in
361     (* update the DB *)
362     List.iter 
363       (fun (src,tgt,uri,saturations,_,_,cpos) ->
364         CoercDb.add_coercion (src,tgt,uri,saturations,cpos)) 
365       new_coercions;
366     CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations, cpos);
367     (* add the composites obj and they eventual lemmas *)
368     let lemmas = 
369         List.fold_left
370           (fun acc (_,tgt,uri,saturations,obj,arity,cpos) -> 
371             add_single_obj uri obj refinement_toolkit;
372              (uri,arity,saturations,cpos)::acc) 
373           [] new_coercions
374     in
375     (* store that composite_uris are related to uri. the first component is
376      * the stuff in the DB while the second is stuff for remove_obj *)
377     (* 
378        prerr_endline ("adding: " ^ 
379          string_of_bool add_composites ^ UriManager.string_of_uri uri);
380        List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
381         composite_uris; 
382     *)
383     UriManager.UriHashtbl.add 
384       coercion_hashtbl uri (composite_uris,composite_uris);
385     (*
386     prerr_endline ("lemmas:");
387       List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
388       lemmas;
389     prerr_endline ("lemmas END");*)
390     lemmas
391 ;;
392
393 let remove_coercion uri =
394   try
395     let (composites_in_db, composites_in_lib) = 
396       UriManager.UriHashtbl.find coercion_hashtbl uri 
397     in
398     (*prerr_endline ("removing: " ^UriManager.string_of_uri uri);
399     List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
400       composites_in_db;*)
401     UriManager.UriHashtbl.remove coercion_hashtbl uri;
402     CoercDb.remove_coercion 
403       (fun (_,_,u,_,_) -> UriManager.eq uri u);
404     (* remove from the DB *) 
405     List.iter 
406       (fun u -> 
407          CoercDb.remove_coercion (fun (_,_,u1,_,_) -> UriManager.eq u u1))
408       composites_in_db;
409     (* remove composites from the lib *)
410     List.iter remove_single_obj composites_in_lib
411   with
412     Not_found -> HLog.warn "Coercion removal raise Not_found" (* mhh..... *)
413     
414
415 let generate_projections refinement_toolkit uri fields =
416  let uris = ref [] in
417  let projections = 
418    CicRecord.projections_of uri 
419      (List.map (fun (x,_,_) -> x) fields) 
420  in
421   try
422    List.iter2 
423     (fun (uri, name, bo) (_name, coercion, arity) ->
424       let saturations = 0 in
425       try
426        let ty, _ =
427          CicTypeChecker.type_of_aux' [] [] bo CicUniv.oblivion_ugraph in
428        let attrs = [`Class `Projection; `Generated] in
429        let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
430         add_single_obj uri obj refinement_toolkit;
431         let composites = 
432          if coercion then
433             begin
434 (*prerr_endline ("composite for " ^ UriManager.string_of_uri uri);*)
435               (*CSC: I think there is a bug here. The composite coercions
436                 are not remembered in the .moo file. Thus they are re-generated
437                 every time. Right? *)
438               let x = 
439                 add_coercion ~add_composites:true refinement_toolkit uri arity
440                  saturations (UriManager.buri_of_uri uri)
441               in
442 (*prerr_endline ("are: ");
443   List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) x;
444   prerr_endline "---";
445 *)
446               (*CSC: I throw the arity away. See comment above *)
447               List.map (fun u,_,_,_ -> u) x
448             end
449           else  
450             []
451         in
452         uris := uri :: composites @ !uris
453       with
454          CicTypeChecker.TypeCheckerFailure s ->
455           HLog.message
456            ("Unable to create projection " ^ name ^ " cause: " ^ Lazy.force s);
457        | CicEnvironment.Object_not_found uri ->
458           let depend = UriManager.name_of_uri uri in
459            HLog.message
460             ("Unable to create projection " ^ name ^ " because it requires " ^
461                depend)
462     ) projections fields;
463    !uris
464   with exn ->
465    List.iter remove_single_obj !uris;
466    raise exn
467
468 let build_inversion_principle = ref (fun a b -> assert false);;
469
470 let generate_inversion refinement_toolkit uri obj =
471   List.map 
472     (fun (ind_uri,ind_obj) -> 
473        add_single_obj ind_uri ind_obj refinement_toolkit;ind_uri)
474     (!build_inversion_principle uri obj)
475
476 let
477  generate_sibling_mutual_definitions refinement_toolkit uri attrs name_to_avoid
478 =
479  function
480     Cic.Fix (_,funs) ->
481      snd (
482       List.fold_right
483        (fun (name,idx,ty,bo) (n,uris) ->
484          if name = name_to_avoid then
485           (n-1,uris)
486          else
487           let uri =
488            UriManager.uri_of_string
489             (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in
490           let bo = Cic.Fix (n-1,funs) in 
491           let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
492            (add_single_obj uri obj refinement_toolkit;
493            (n-1,uri::uris)))
494        funs (List.length funs,[]))
495   | Cic.CoFix (_,funs) ->
496      snd (
497       List.fold_right
498        (fun (name,ty,bo) (n,uris) ->
499          if name = name_to_avoid then
500           (n-1,uris)
501          else
502           let uri =
503            UriManager.uri_of_string
504             (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in
505           let bo = Cic.CoFix (n-1,funs) in 
506           let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
507            add_single_obj uri obj refinement_toolkit;
508            (n-1,uri::uris)
509        ) funs (List.length funs,[]))
510   | _ -> assert false
511
512 let add_obj refinement_toolkit uri obj =
513  add_single_obj uri obj refinement_toolkit;
514  let uris = ref [] in
515  let not_debug = not (Helm_registry.get_bool "matita.debug") in
516  try
517   begin
518    match obj with
519     | Cic.Constant (name,Some bo,_,_,attrs) when
520        List.mem (`Flavour `MutualDefinition) attrs ->
521         uris :=
522          !uris @
523            generate_sibling_mutual_definitions refinement_toolkit uri attrs
524             name bo
525     | Cic.Constant _ -> ()
526     | Cic.InductiveDefinition (inductivefuns,_,_,attrs) ->
527        let _,inductive,_,_ = List.hd inductivefuns in
528        if inductive then
529         begin
530          uris := !uris @ 
531            generate_elimination_principles uri refinement_toolkit;
532          uris := !uris @ generate_inversion refinement_toolkit uri obj;
533         end ;
534        let rec get_record_attrs =
535          function
536          | [] -> None
537          | (`Class (`Record fields))::_ -> Some fields
538          | _::tl -> get_record_attrs tl
539        in
540         (match get_record_attrs attrs with
541         | None -> () (* not a record *)
542         | Some fields ->
543            uris := !uris @ 
544              (generate_projections refinement_toolkit uri fields))
545     | Cic.CurrentProof _
546     | Cic.Variable _ -> assert false
547   end;
548   UriManager.UriHashtbl.add auxiliary_lemmas_hashtbl uri !uris;
549   !uris
550  with 
551  | exn when not_debug ->
552     List.iter remove_single_obj !uris;
553     raise exn
554
555 let remove_obj uri =
556  let uris =
557   try
558    let res = UriManager.UriHashtbl.find auxiliary_lemmas_hashtbl uri in
559     UriManager.UriHashtbl.remove auxiliary_lemmas_hashtbl uri;
560     res
561   with
562     Not_found -> [] (*assert false*)
563  in
564   List.iter remove_single_obj (uri::uris)
565