helm/ocaml/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 type type_checked_obj =
  39    CheckedObj of Cic.obj     (* cooked obj *)
  40  | UncheckedObj of Cic.obj   (* uncooked obj to proof-check *)
  41 ;;
  42
  43 exception NoFunctionProvided;;
  44
  45 let cook_obj = ref (fun obj uri -> raise NoFunctionProvided);;
  46
  47 let set_cooking_function foo =
  48  cook_obj := foo
  49 ;;
  50
  51 exception AlreadyCooked of string;;
  52 exception CircularDependency of string;;
  53 exception CouldNotFreeze of string;;
  54 exception CouldNotUnfreeze of string;;
  55
  56 (* Cache that uses == instead of = for testing equality *)
  57 (* Invariant: an object is always in at most one of the *)
  58 (* following states: unchecked, frozen and cooked.      *)
  59 module Cache :
  60   sig
  61    val find_or_add_unchecked :
  62     UriManager.uri -> get_object_to_add:(unit -> Cic.obj) -> Cic.obj
  63    val unchecked_to_frozen : UriManager.uri -> unit
  64    val frozen_to_cooked :
  65     uri:UriManager.uri ->
  66     cooking_procedure:
  67      (object_to_cook:Cic.obj ->
  68       add_cooked:(UriManager.uri * int-> Cic.obj -> unit)
  69       -> unit
  70      )
  71     -> unit
  72    val find_cooked : key:(UriManager.uri * int) -> Cic.obj
  73   end
  74 =
  75   struct
  76    module CacheOfCookedObjects :
  77     sig
  78      val mem  : UriManager.uri -> int -> bool
  79      val find : UriManager.uri -> int -> Cic.obj
  80      val add  : UriManager.uri -> int -> Cic.obj -> unit
  81     end
  82    =
  83     struct
  84      module HashedType =
  85       struct
  86        type t = UriManager.uri
  87        let equal = UriManager.eq
  88        let hash = Hashtbl.hash
  89       end
  90      ;;
  91      module HT = Hashtbl.Make(HashedType);;
  92      let hashtable = HT.create 1009;;
  93      let mem uri cookingsno =
  94       try
  95        let cooked_list =
  96         HT.find hashtable uri
  97        in
  98         List.mem_assq cookingsno !cooked_list
  99       with
 100        Not_found -> false
 101      ;;
 102      let find uri cookingsno =
 103       List.assq cookingsno !(HT.find hashtable uri)
 104      ;;
 105      let add uri cookingsno obj =
 106       let cooked_list =
 107        try
 108         HT.find hashtable uri
 109        with
 110         Not_found ->
 111          let newl = ref [] in
 112           HT.add hashtable uri newl ;
 113           newl
 114       in
 115        cooked_list := (cookingsno,obj)::!cooked_list
 116      ;;
 117     end
 118    ;;
 119    let frozen_list = ref [];;
 120    let unchecked_list = ref [];;
 121
 122    let find_or_add_unchecked uri ~get_object_to_add =
 123     try
 124      List.assq uri !unchecked_list
 125     with
 126      Not_found ->
 127       if List.mem_assq uri !frozen_list then
 128        raise (CircularDependency (UriManager.string_of_uri uri))
 129       else
 130        if CacheOfCookedObjects.mem uri 0 then
 131         raise (AlreadyCooked (UriManager.string_of_uri uri))
 132        else
 133         (* OK, it is not already frozen nor cooked *)
 134         let obj = get_object_to_add () in
 135          unchecked_list := (uri,obj)::!unchecked_list ;
 136          obj
 137    ;;
 138    let unchecked_to_frozen uri =
 139     try
 140      let obj = List.assq uri !unchecked_list in
 141       unchecked_list := List.remove_assq uri !unchecked_list ;
 142       frozen_list := (uri,obj)::!frozen_list
 143     with
 144      Not_found -> raise (CouldNotFreeze (UriManager.string_of_uri uri))
 145    ;;
 146    let frozen_to_cooked ~uri ~cooking_procedure =
 147     try
 148      let obj = List.assq uri !frozen_list in
 149       frozen_list := List.remove_assq uri !frozen_list ;
 150       cooking_procedure
 151        ~object_to_cook:obj
 152        ~add_cooked:(fun (uri,cookno) -> CacheOfCookedObjects.add uri cookno)
 153     with
 154      Not_found -> raise (CouldNotUnfreeze (UriManager.string_of_uri uri))
 155    ;;
 156    let find_cooked ~key:(uri,cookingsno)= CacheOfCookedObjects.find uri cookingsno;;
 157   end
 158 ;;
 159
 160 (* get_cooked_obj uri                                                               *)
 161 (* returns the cooked cic object whose uri is uri. The term must be present  *)
 162 (* and cooked in cache                                                       *)
 163 let get_cooked_obj uri cookingsno =
 164  Cache.find_cooked (uri,cookingsno)
 165 ;;
 166
 167 let find_or_add_unchecked_to_cache uri =
 168  Cache.find_or_add_unchecked uri
 169   ~get_object_to_add:
 170    (function () ->
 171      let filename = Getter.getxml uri in
 172       let obj = CicParser.obj_of_xml filename uri in
 173        obj
 174    )
 175 ;;
 176
 177 (* get_obj uri                                                                *)
 178 (* returns the cic object whose uri is uri. If the term is not just in cache, *)
 179 (* then it is parsed via CicParser.term_of_xml from the file whose name is    *)
 180 (* the result of Getter.getxml uri                                            *)
 181 let get_obj uri =
 182  try
 183   get_cooked_obj uri 0
 184  with
 185   Not_found ->
 186    find_or_add_unchecked_to_cache uri
 187 ;;
 188
 189 (* is_type_checked uri                                                *)
 190 (* CSC: commento falso ed obsoleto *)
 191 (* returns a CheckedObj if the term has been type-checked             *)
 192 (* otherwise it freezes the term for type-checking and returns
 193  it *)
 194 (* set_type_checking_info must be called to unfreeze the term         *)
 195 let is_type_checked uri cookingsno =
 196  try
 197   CheckedObj (Cache.find_cooked (uri,cookingsno))
 198  with
 199   Not_found ->
 200    let obj = find_or_add_unchecked_to_cache uri in
 201     Cache.unchecked_to_frozen uri ;
 202     UncheckedObj obj
 203 ;;
 204
 205 (* set_type_checking_info uri                               *)
 206 (* must be called once the type-checking of uri is finished *)
 207 (* The object whose uri is uri is unfreezed                 *)
 208 let set_type_checking_info uri =
 209  Cache.frozen_to_cooked uri
 210   (fun ~object_to_cook:obj ~add_cooked ->
 211     (* let's cook the object at every level *)
 212     let obj' = CicSubstitution.undebrujin_inductive_def uri obj in
 213      add_cooked (uri,0) obj' ;
 214      let cooked_objs = !cook_obj obj' uri in
 215       let last_cooked_level = ref 0 in
 216       let last_cooked_obj = ref obj' in
 217        List.iter
 218         (fun (n,cobj) ->
 219           for i = !last_cooked_level + 1 to n do
 220            add_cooked (uri,i) !last_cooked_obj
 221           done ;
 222           add_cooked (uri,n + 1) cobj ;
 223           last_cooked_level := n + 1 ;
 224           last_cooked_obj := cobj
 225         ) cooked_objs ;
 226        for i = !last_cooked_level + 1 to UriManager.depth_of_uri uri + 1 do
 227         add_cooked (uri,i) !last_cooked_obj
 228        done
 229   )
 230 ;;