]> matita.cs.unibo.it Git - helm.git/blob - components/cic_proof_checking/cicEnvironment.ml
branch for universe
[helm.git] / components / cic_proof_checking / cicEnvironment.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 (*****************************************************************************)
27 (*                                                                           *)
28 (*                              PROJECT HELM                                 *)
29 (*                                                                           *)
30 (*               Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
31 (*                                24/01/2000                                 *)
32 (*                                                                           *)
33 (* This module implements a trival cache system (an hash-table) for cic      *)
34 (* objects. Uses the getter (getter.ml) and the parser (cicParser.ml)        *)
35 (*                                                                           *)
36 (*****************************************************************************)
37
38 (* $Id$ *)
39
40 (* ************************************************************************** *
41                  CicEnvironment SETTINGS (trust and clean_tmp)
42  * ************************************************************************** *)
43
44 let debug = false;;
45 let cleanup_tmp = true;;
46 let trust = ref  (fun _ -> true);;
47 let set_trust f = trust := f
48 let trust_obj uri = !trust uri
49 let debug_print = if debug then fun x -> prerr_endline (Lazy.force x) else ignore
50
51 (* ************************************************************************** *
52                                    TYPES 
53  * ************************************************************************** *)
54
55 type type_checked_obj =
56  | CheckedObj of (Cic.obj * CicUniv.universe_graph)    
57  | UncheckedObj of Cic.obj * (CicUniv.universe_graph * CicUniv.universe list) option
58
59 exception AlreadyCooked of string;;
60 exception CircularDependency of string Lazy.t;;
61 exception CouldNotFreeze of string;;
62 exception CouldNotUnfreeze of string;;
63 exception Object_not_found of UriManager.uri;;
64
65
66 (* ************************************************************************** *
67                          HERE STARTS THE CACHE MODULE 
68  * ************************************************************************** *)
69
70 (* I think this should be the right place to implement mecanisms and 
71  * invasriants 
72  *)
73
74 (* Cache that uses == instead of = for testing equality *)
75 (* Invariant: an object is always in at most one of the *)
76 (* following states: unchecked, frozen and cooked.      *)
77 module Cache :
78   sig
79    val find_or_add_to_unchecked :
80      UriManager.uri -> 
81      get_object_to_add:
82        (UriManager.uri -> 
83          Cic.obj * (CicUniv.universe_graph * CicUniv.universe list) option) -> 
84      Cic.obj * (CicUniv.universe_graph * CicUniv.universe list) option
85    val can_be_cooked:
86      UriManager.uri -> bool
87    val unchecked_to_frozen : 
88      UriManager.uri -> unit
89    val frozen_to_cooked :
90      uri:UriManager.uri -> 
91      Cic.obj -> CicUniv.universe_graph -> CicUniv.universe list -> unit
92    val find_cooked : 
93      key:UriManager.uri -> 
94        Cic.obj * CicUniv.universe_graph * CicUniv.universe list
95    val add_cooked : 
96      key:UriManager.uri -> 
97      (Cic.obj * CicUniv.universe_graph * CicUniv.universe list) -> unit
98    val remove: UriManager.uri -> unit
99    val dump_to_channel : ?callback:(string -> unit) -> out_channel -> unit
100    val restore_from_channel : ?callback:(string -> unit) -> in_channel -> unit
101    val empty : unit -> unit
102    val is_in_frozen: UriManager.uri -> bool
103    val is_in_unchecked: UriManager.uri -> bool
104    val is_in_cooked: UriManager.uri -> bool
105    val list_all_cooked_uris: unit -> UriManager.uri list
106    val invalidate: unit -> unit
107   end 
108 =
109   struct
110    (*************************************************************************
111      TASSI: invariant
112      The cacheOfCookedObjects will contain only objects with a valid universe
113      graph. valid means that not None (used if there is no universe file
114      in the universe generation phase).
115    **************************************************************************)
116
117     (* DATA: the data structure that implements the CACHE *)
118     module HashedType =
119     struct
120      type t = UriManager.uri
121      let equal = UriManager.eq
122      let hash = Hashtbl.hash
123     end
124     ;;
125
126     module HT = Hashtbl.Make(HashedType);;
127
128     let cacheOfCookedObjects = HT.create 1009;;
129
130     (* DATA: The parking lists 
131      * the lists elements are (uri * (obj * universe_graph option))
132      * ( u, ( o, None )) means that the object has no universes file, this
133      *  should happen only in the universe generation phase. 
134      *  FIXME: if the universe generation is integrated in the library
135      *  exportation phase, the 'option' MUST be removed.
136      * ( u, ( o, Some g)) means that the object has a universes file,
137      *  the usual case.
138      *)
139
140     (* frozen is used to detect circular dependency. *)
141     let frozen_list = ref [];;
142     (* unchecked is used to store objects just fetched, nothing more. *)    
143     let unchecked_list = ref [];;
144
145     let invalidate _ =
146       let l = HT.fold (fun k (o,g,gl) acc -> (k,(o,Some (g,gl)))::acc) cacheOfCookedObjects [] in
147       unchecked_list := 
148         HExtlib.list_uniq ~eq:(fun (x,_) (y,_) -> UriManager.eq x y)
149         (List.sort (fun (x,_) (y,_) -> UriManager.compare x y) (l @ !unchecked_list));
150       frozen_list := [];
151       HT.clear cacheOfCookedObjects;
152     ;;
153
154     let empty () = 
155       HT.clear cacheOfCookedObjects;
156       unchecked_list := [] ;
157       frozen_list := []
158     ;;
159
160     (* FIX: universe stuff?? *)
161     let dump_to_channel ?(callback = ignore) oc =
162      HT.iter (fun uri _ -> callback (UriManager.string_of_uri uri)) 
163        cacheOfCookedObjects;
164      Marshal.to_channel oc cacheOfCookedObjects [] 
165     ;;
166
167     (* FIX: universes stuff?? *)
168     let restore_from_channel ?(callback = ignore) ic =
169       let restored = Marshal.from_channel ic in
170       (* FIXME: should this empty clean the frozen and unchecked?
171        * if not, the only-one-empty-end-not-3 patch is wrong 
172        *)
173       empty (); 
174       HT.iter
175        (fun k (v,u,l) ->
176          callback (UriManager.string_of_uri k);
177          let reconsed_entry = 
178            CicUtil.rehash_obj v,
179            CicUniv.recons_graph u,
180            List.map CicUniv.recons_univ l
181          in
182          HT.add cacheOfCookedObjects 
183            (UriManager.uri_of_string (UriManager.string_of_uri k)) 
184            reconsed_entry)
185        restored
186     ;;
187
188          
189     let is_in_frozen uri =
190       List.mem_assoc uri !frozen_list
191     ;;
192     
193     let is_in_unchecked uri =
194       List.mem_assoc uri !unchecked_list
195     ;;
196     
197     let is_in_cooked uri =
198       HT.mem cacheOfCookedObjects uri
199     ;;
200
201        
202     (*******************************************************************
203       TASSI: invariant
204       we need, in the universe generation phase, to traverse objects
205       that are not yet committed, so we search them in the frozen list.
206       Only uncommitted objects without a universe file (see the assertion) 
207       can be searched with method
208     *******************************************************************)
209
210     let find_or_add_to_unchecked uri ~get_object_to_add =
211      try
212        List.assq uri !unchecked_list
213      with
214          Not_found ->
215            if List.mem_assq uri !frozen_list then
216              (* CIRCULAR DEPENDENCY DETECTED, print the error and raise *)
217              begin
218 (*
219                prerr_endline "\nCircularDependency!\nfrozen list: \n";
220                List.iter (
221                  fun (u,(_,o)) ->
222                    let su = UriManager.string_of_uri u in
223                    let univ = if o = None then "NO_UNIV" else "" in
224                    prerr_endline (su^" "^univ)) 
225                  !frozen_list;
226 *)
227                raise (CircularDependency (lazy (UriManager.string_of_uri uri)))
228              end
229            else
230              if HT.mem cacheOfCookedObjects uri then
231                (* DOUBLE COOK DETECTED, raise the exception *)
232                raise (AlreadyCooked (UriManager.string_of_uri uri))
233              else
234                (* OK, it is not already frozen nor cooked *)
235                let obj,ugraph_and_univlist = get_object_to_add uri in
236                unchecked_list := (uri,(obj,ugraph_and_univlist))::!unchecked_list;
237                obj, ugraph_and_univlist
238     ;;
239
240     let unchecked_to_frozen uri =
241       try
242         let obj,ugraph_and_univlist = List.assq uri !unchecked_list in
243         unchecked_list := List.remove_assq uri !unchecked_list ;
244         frozen_list := (uri,(obj,ugraph_and_univlist))::!frozen_list
245       with
246         Not_found -> raise (CouldNotFreeze (UriManager.string_of_uri uri))
247     ;;
248
249    let frozen_to_cooked ~uri o ug ul =
250      CicUniv.assert_univs_have_uri ug ul;
251      frozen_list := List.remove_assq uri !frozen_list ;
252      HT.add cacheOfCookedObjects uri (o,ug,ul) 
253    ;;
254
255    let can_be_cooked uri = List.mem_assq uri !frozen_list;;
256    
257    let find_cooked ~key:uri = HT.find cacheOfCookedObjects uri ;;
258  
259    let add_cooked ~key:uri (obj,ugraph,univlist) = 
260      HT.add cacheOfCookedObjects uri (obj,ugraph,univlist) 
261    ;;
262
263    (* invariant
264     *
265     * an object can be romeved from the cache only if we are not typechecking 
266     * something. this means check and frozen must be empty.
267     *)
268    let remove uri =
269      if !frozen_list <> [] then
270        failwith "CicEnvironment.remove while type checking"
271      else
272       begin
273        HT.remove cacheOfCookedObjects uri;
274        unchecked_list :=
275         List.filter (fun (uri',_) -> not (UriManager.eq uri uri')) !unchecked_list
276       end
277    ;;
278    
279    let  list_all_cooked_uris () =
280      HT.fold (fun u _ l -> u::l) cacheOfCookedObjects []
281    ;;
282    
283   end
284 ;;
285
286 (* ************************************************************************
287                         HERE ENDS THE CACHE MODULE
288  * ************************************************************************ *)
289
290 (* exported cache functions *)
291 let dump_to_channel = Cache.dump_to_channel;;
292 let restore_from_channel = Cache.restore_from_channel;;
293 let empty = Cache.empty;;
294
295 let total_parsing_time = ref 0.0
296
297 let get_object_to_add uri =
298  try
299   let filename = Http_getter.getxml' uri in
300   let bodyfilename =
301     match UriManager.bodyuri_of_uri uri with
302        None -> None
303     |  Some bodyuri ->
304         if Http_getter.exists' ~local:false bodyuri then
305           Some (Http_getter.getxml' bodyuri)
306         else
307           None
308   in
309   let obj = 
310     try 
311       let time = Unix.gettimeofday() in
312       let rc = CicParser.obj_of_xml uri filename bodyfilename in
313       total_parsing_time := 
314         !total_parsing_time +. ((Unix.gettimeofday()) -. time );
315       rc
316     with exn -> 
317       (match exn with
318       | CicParser.Getter_failure ("key_not_found", uri) ->
319           raise (Object_not_found (UriManager.uri_of_string uri))
320       | _ -> raise exn)
321   in
322   let ugraph_and_univlist,filename_univ = 
323     try 
324       let filename_univ = 
325         let univ_uri = UriManager.univgraphuri_of_uri uri in
326         Http_getter.getxml' univ_uri
327       in
328         Some (CicUniv.ugraph_and_univlist_of_xml filename_univ),
329         Some filename_univ
330     with 
331     | Http_getter_types.Key_not_found _ 
332     | Http_getter_types.Unresolvable_URI _ ->
333       debug_print (lazy (
334         "WE HAVE NO UNIVERSE FILE FOR " ^ (UriManager.string_of_uri uri)));
335       None, None
336   in
337   obj, ugraph_and_univlist
338  with Http_getter_types.Key_not_found _ -> raise (Object_not_found uri)
339 ;;
340  
341 (* this is the function to fetch the object in the unchecked list and 
342  * nothing more (except returning it)
343  *)
344 let find_or_add_to_unchecked uri =
345  Cache.find_or_add_to_unchecked uri ~get_object_to_add
346
347 (* set_type_checking_info uri                                   *)
348 (* must be called once the type-checking of uri is finished     *)
349 (* The object whose uri is uri is unfreezed                     *)
350 (*                                                              *)
351 (* the replacement ugraph must be the one returned by the       *)
352 (* typechecker, restricted with the CicUnivUtils.clean_and_fill *)
353 let set_type_checking_info uri (o,ug,ul) =
354   if not (Cache.can_be_cooked uri) then assert false
355   else 
356     Cache.frozen_to_cooked ~uri o ug ul
357 ;;
358
359 (* fetch, unfreeze and commit an uri to the cacheOfCookedObjects and
360  * return the object,ugraph
361  *)
362 let add_trusted_uri_to_cache uri = 
363   let o,u_and_ul = find_or_add_to_unchecked uri in
364   Cache.unchecked_to_frozen uri;
365   let u,ul = 
366     match u_and_ul with
367     (* for backward compat with Coq *)
368     | None -> CicUniv.empty_ugraph, []
369     | Some (ug,ul) -> ug, ul
370   in
371   set_type_checking_info uri (o,u,ul);
372   try Cache.find_cooked uri
373   with Not_found -> assert false 
374 ;;
375
376 (* get the uri, if we trust it will be added to the cacheOfCookedObjects *)
377 let get_cooked_obj_with_univlist ?(trust=true) base_ugraph uri =
378   try
379     (* the object should be in the cacheOfCookedObjects *)
380     let o,u,l = Cache.find_cooked uri in
381       o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri(*,l*))),l
382   with Not_found ->
383     (* this should be an error case, but if we trust the uri... *)
384     if trust && trust_obj uri then
385       (* trusting means that we will fetch cook it on the fly *)
386       let o,u,l = add_trusted_uri_to_cache uri in
387         o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri(*,l*))),l
388     else
389       (* we don't trust the uri, so we fail *)
390       begin
391         debug_print (lazy ("CACHE MISS: " ^ (UriManager.string_of_uri uri)));
392         raise Not_found
393       end
394
395 let get_cooked_obj ?trust base_ugraph uri = 
396   let o,g,_ = get_cooked_obj_with_univlist ?trust base_ugraph uri in
397   o,g
398       
399 let is_type_checked ?(trust=true) base_ugraph uri =
400   try 
401     let o,u,l = Cache.find_cooked uri in
402       CheckedObj (o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri(*,l*))))
403   with Not_found ->
404     (* this should return UncheckedObj *)
405     if trust && trust_obj uri then
406       (* trusting means that we will fetch cook it on the fly *)
407       let o,u,l = add_trusted_uri_to_cache uri in
408         CheckedObj ( o, CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri(*,l*)))
409     else
410       let o,u_and_ul = find_or_add_to_unchecked uri in
411       Cache.unchecked_to_frozen uri;
412       UncheckedObj (o,u_and_ul)
413 ;;
414
415 (* as the get cooked, but if not present the object is only fetched,
416  * not unfreezed and committed 
417  *)
418 let get_obj base_ugraph uri =
419   try
420     (* the object should be in the cacheOfCookedObjects *)
421     let o,u,_ = Cache.find_cooked uri in
422     o,CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri)
423   with Not_found ->
424     (* this should be an error case, but if we trust the uri... *)
425       let o,u_and_l = find_or_add_to_unchecked uri in
426       match u_and_l with
427       | None -> o, base_ugraph
428       | Some (ug,_) -> o,CicUniv.merge_ugraphs ~base_ugraph ~increment:(ug,uri)
429 ;; 
430
431 let in_cache uri =
432   Cache.is_in_cooked uri || Cache.is_in_frozen uri || Cache.is_in_unchecked uri
433
434 let add_type_checked_obj uri (obj,ugraph,univlist) =
435  Cache.add_cooked ~key:uri (obj,ugraph,univlist)
436
437 let in_library uri = in_cache uri || Http_getter.exists' ~local:false uri
438
439 let remove_obj = Cache.remove
440   
441 let list_uri () = 
442   Cache.list_all_cooked_uris ()
443 ;;
444
445 let list_obj () =
446   try 
447     List.map (fun u -> 
448       let o,ug = get_obj CicUniv.empty_ugraph u in
449         (u,o,ug)) 
450     (list_uri ())
451   with
452     Not_found -> 
453       debug_print (lazy "Who has removed the uri in the meanwhile?");
454       raise Not_found
455 ;;
456
457 let invalidate _ = 
458    Cache.invalidate ()
459 ;;