helm/interface/cicCache.ml

   1 (******************************************************************************)
   2 (*                                                                            *)
   3 (*                               PROJECT HELM                                 *)
   4 (*                                                                            *)
   5 (*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
   6 (*                                 24/01/2000                                 *)
   7 (*                                                                            *)
   8 (* This module implements a trival cache system (an hash-table) for cic       *)
   9 (* objects. Uses the getter (getter.ml) and the parser (cicParser.ml)         *)
  10 (*                                                                            *)
  11 (******************************************************************************)
  12
  13 let raise e = print_endline "***" ; flush stdout ; print_endline (Printexc.to_string e) ; flush stdout ; raise e;;
  14
  15 (*CSC: forse i due seguenti tipi sono da unificare? *)
  16 type cooked_obj =
  17    Cooked of Cic.obj
  18  | Frozen of Cic.obj
  19  | Unchecked of Cic.obj
  20 type type_checked_obj =
  21    CheckedObj of Cic.obj     (* cooked obj *)
  22  | UncheckedObj of Cic.obj   (* uncooked obj *)
  23 ;;
  24
  25 exception NoFunctionProvided;;
  26
  27 (* CSC: da sostituire con un (...) option ref *)
  28 let cook_obj = ref (fun obj uri -> raise NoFunctionProvided);;
  29
  30 exception CircularDependency of string;;
  31 exception CouldNotUnfreeze of string;;
  32 exception Impossible;;
  33 exception UncookedObj;;
  34
  35 module HashedType =
  36  struct
  37   type t = UriManager.uri * int    (* uri, livello di cottura *)
  38   let equal (u1,n1) (u2,n2) = UriManager.eq u1 u2 && n1 = n2
  39   let hash = Hashtbl.hash
  40  end
  41 ;;
  42
  43 (* Hashtable that uses == instead of = for testing equality *)
  44 module HashTable = Hashtbl.Make(HashedType);;
  45
  46 let hashtable = HashTable.create 271;;
  47
  48 (* n is the number of time that the object must be cooked *)
  49 let get_obj_and_type_checking_info uri n =
  50  try
  51    HashTable.find hashtable (uri,n)
  52  with
  53   Not_found ->
  54    try
  55     match HashTable.find hashtable (uri,0) with
  56         Cooked _
  57       | Frozen _ -> raise Impossible
  58       | Unchecked _ as t -> t
  59    with
  60     Not_found ->
  61      let filename = Getter.get uri in
  62       let (annobj,_) = CicParser.term_of_xml filename uri false in
  63        let obj = Deannotate.deannotate_obj annobj in
  64         let output = Unchecked obj in
  65          HashTable.add hashtable (uri,0) output ;
  66          output
  67 ;;
  68
  69 (* DANGEROUS!!!                                *)
  70 (* USEFUL ONLY DURING THE FIXING OF THE FILES  *)
  71 (* change_obj uri (Some newobj)                *)
  72 (*  maps uri to newobj in cache.               *)
  73 (* change_obj uri None                         *)
  74 (*  maps uri to a freeze dummy-object.         *)
  75 let change_obj uri newobj =
  76  let newobj =
  77   match newobj with
  78      Some newobj' -> Unchecked newobj'
  79    | None         -> Frozen (Cic.Variable ("frozen-dummy", None, Cic.Implicit))
  80  in
  81   HashTable.remove hashtable (uri,0) ;
  82   HashTable.add hashtable (uri,0) newobj
  83 ;;
  84
  85 let is_annotation_uri uri =
  86  Str.string_match (Str.regexp ".*\.ann$") (UriManager.string_of_uri uri) 0
  87 ;;
  88
  89 (* returns both the annotated and deannotated uncooked forms (plus the *)
  90 (* map from ids to annotation targets)                                 *)
  91 let get_annobj_and_type_checking_info uri =
  92  let filename = Getter.get uri in
  93   match CicParser.term_of_xml filename uri true with
  94      (_, None) -> raise Impossible
  95    | (annobj, Some ids_to_targets) ->
  96     (* If uri is the uri of an annotation, let's use the annotation file *)
  97     if is_annotation_uri uri  then
  98      AnnotationParser.annotate (Getter.get_ann uri) ids_to_targets ;
  99     try
 100       (annobj, ids_to_targets, HashTable.find hashtable (uri,0))
 101     with
 102      Not_found ->
 103       let obj = Deannotate.deannotate_obj annobj in
 104        let output = Unchecked obj in
 105         HashTable.add hashtable (uri,0) output ;
 106         (annobj, ids_to_targets, output)
 107 ;;
 108
 109
 110 (* get_obj uri                                                               *)
 111 (* returns the cic object whose uri is uri. If the term is not just in cache, *)
 112 (* then it is parsed via CicParser.term_of_xml from the file whose name is    *)
 113 (* the result of Getter.get uri                                               *)
 114 let get_obj uri =
 115  match get_obj_and_type_checking_info uri 0 with
 116     Unchecked obj -> obj
 117   | Frozen    obj -> obj
 118   | Cooked    obj -> obj
 119 ;;
 120
 121 (* get_annobj uri                                                             *)
 122 (* returns the cic object whose uri is uri either in annotated and            *)
 123 (* deannotated form. The term is put into the cache if it's not there yet.    *)
 124 let get_annobj uri =
 125  let (ann, ids_to_targets, deann) = get_annobj_and_type_checking_info uri in
 126   let deannobj =
 127    match deann with
 128       Unchecked obj -> obj
 129     | Frozen    _   -> raise (CircularDependency (UriManager.string_of_uri uri))
 130     | Cooked    obj -> obj
 131   in
 132    (ann, ids_to_targets, deannobj)
 133 ;;
 134
 135 (*CSC Commento falso *)
 136 (* get_obj uri                                                               *)
 137 (* returns the cooked cic object whose uri is uri. The term must be present  *)
 138 (* and cooked in cache                                                       *)
 139 let rec get_cooked_obj uri cookingsno =
 140  match get_obj_and_type_checking_info uri cookingsno with
 141     Unchecked _
 142   | Frozen    _ -> raise UncookedObj
 143   | Cooked obj -> obj
 144 ;;
 145
 146 (* is_type_checked uri                                              *)
 147 (* CSC: commento falso ed obsoleto *)
 148 (* returns true if the term has been type-checked                   *)
 149 (* otherwise it returns false and freeze the term for type-checking *)
 150 (* set_type_checking_info must be called to unfreeze the term       *)
 151 let is_type_checked uri cookingsno =
 152  match get_obj_and_type_checking_info uri cookingsno with
 153     Cooked obj -> CheckedObj obj
 154   | Unchecked obj ->
 155      HashTable.remove hashtable (uri,0) ;
 156      HashTable.add hashtable (uri,0) (Frozen obj) ;
 157      UncheckedObj obj
 158   | Frozen _ -> raise (CircularDependency (UriManager.string_of_uri uri))
 159 ;;
 160
 161 (* set_type_checking_info uri                               *)
 162 (* must be called once the type-checking of uri is finished *)
 163 (* The object whose uri is uri is unfreezed                 *)
 164 let set_type_checking_info uri =
 165  match HashTable.find hashtable (uri,0) with
 166     Frozen obj ->
 167      (* let's cook the object at every level *)
 168      HashTable.remove hashtable (uri,0) ;
 169      let obj' = CicSubstitution.undebrujin_inductive_def uri obj in
 170       HashTable.add hashtable (uri,0) (Cooked obj') ;
 171       let cooked_objs = !cook_obj obj' uri in
 172        let last_cooked_level = ref 0 in
 173        let last_cooked_obj = ref obj' in
 174         List.iter
 175          (fun (n,cobj) ->
 176            for i = !last_cooked_level + 1 to n do
 177             HashTable.add hashtable (uri,i) (Cooked !last_cooked_obj)
 178            done ;
 179            HashTable.add hashtable (uri,n + 1) (Cooked cobj) ;
 180            last_cooked_level := n + 1 ;
 181            last_cooked_obj := cobj
 182          ) cooked_objs ;
 183         for i = !last_cooked_level + 1 to UriManager.depth_of_uri uri + 1 do
 184          HashTable.add hashtable (uri,i) (Cooked !last_cooked_obj)
 185         done
 186   | _ -> raise (CouldNotUnfreeze (UriManager.string_of_uri uri))
 187 ;;