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 * int   (* uri, livello di cottura *)
  87        let equal (u1,n1) (u2,n2) = UriManager.eq u1 u2 && n1 = n2
  88        let hash = Hashtbl.hash
  89       end
  90      ;;
  91      module HT = Hashtbl.Make(HashedType);;
  92      let hashtable = HT.create 1009;;
  93      let mem = HT.mem hashtable;;
  94      let find = HT.find hashtable;;
  95      let add = HT.add hashtable;;
  96     end
  97    ;;
  98    let frozen_list = ref [];;
  99    let unchecked_list = ref [];;
 100
 101    let find_or_add_unchecked uri ~get_object_to_add =
 102     try
 103      List.assq uri !unchecked_list
 104     with
 105      Not_found ->
 106       if List.mem_assq uri !frozen_list then
 107        raise (CircularDependency (UriManager.string_of_uri uri))
 108       else
 109        if CacheOfCookedObjects.mem (uri,0) then
 110         raise (AlreadyCooked (UriManager.string_of_uri uri))
 111        else
 112         (* OK, it is not already frozen nor cooked *)
 113         let obj = get_object_to_add () in
 114          unchecked_list := (uri,obj)::!unchecked_list ;
 115          obj
 116    ;;
 117    let unchecked_to_frozen uri =
 118     try
 119      let obj = List.assq uri !unchecked_list in
 120       unchecked_list := List.remove_assq uri !unchecked_list ;
 121       frozen_list := (uri,obj)::!frozen_list
 122     with
 123      Not_found -> raise (CouldNotFreeze (UriManager.string_of_uri uri))
 124    ;;
 125    let frozen_to_cooked ~uri ~cooking_procedure =
 126     try
 127      let obj = List.assq uri !frozen_list in
 128       frozen_list := List.remove_assq uri !frozen_list ;
 129       cooking_procedure ~object_to_cook:obj ~add_cooked:CacheOfCookedObjects.add
 130     with
 131      Not_found -> raise (CouldNotUnfreeze (UriManager.string_of_uri uri))
 132    ;;
 133    let find_cooked = CacheOfCookedObjects.find;;
 134   end
 135 ;;
 136
 137 (* get_cooked_obj uri                                                               *)
 138 (* returns the cooked cic object whose uri is uri. The term must be present  *)
 139 (* and cooked in cache                                                       *)
 140 let get_cooked_obj uri cookingsno =
 141  Cache.find_cooked (uri,cookingsno)
 142 ;;
 143
 144 let find_or_add_unchecked_to_cache uri =
 145  Cache.find_or_add_unchecked uri
 146   ~get_object_to_add:
 147    (function () ->
 148      let filename = Getter.getxml uri in
 149       let obj = CicParser.obj_of_xml filename uri in
 150        obj
 151    )
 152 ;;
 153
 154 (* get_obj uri                                                                *)
 155 (* returns the cic object whose uri is uri. If the term is not just in cache, *)
 156 (* then it is parsed via CicParser.term_of_xml from the file whose name is    *)
 157 (* the result of Getter.getxml uri                                            *)
 158 let get_obj uri =
 159  try
 160   get_cooked_obj uri 0
 161  with
 162   Not_found ->
 163    find_or_add_unchecked_to_cache uri
 164 ;;
 165
 166 (* is_type_checked uri                                                *)
 167 (* CSC: commento falso ed obsoleto *)
 168 (* returns a CheckedObj if the term has been type-checked             *)
 169 (* otherwise it freezes the term for type-checking and returns
 170  it *)
 171 (* set_type_checking_info must be called to unfreeze the term         *)
 172 let is_type_checked uri cookingsno =
 173  try
 174   CheckedObj (Cache.find_cooked (uri,cookingsno))
 175  with
 176   Not_found ->
 177    let obj = find_or_add_unchecked_to_cache uri in
 178     Cache.unchecked_to_frozen uri ;
 179     UncheckedObj obj
 180 ;;
 181
 182 (* set_type_checking_info uri                               *)
 183 (* must be called once the type-checking of uri is finished *)
 184 (* The object whose uri is uri is unfreezed                 *)
 185 let set_type_checking_info uri =
 186  Cache.frozen_to_cooked uri
 187   (fun ~object_to_cook:obj ~add_cooked ->
 188     (* let's cook the object at every level *)
 189     let obj' = CicSubstitution.undebrujin_inductive_def uri obj in
 190      add_cooked (uri,0) obj' ;
 191      let cooked_objs = !cook_obj obj' uri in
 192       let last_cooked_level = ref 0 in
 193       let last_cooked_obj = ref obj' in
 194        List.iter
 195         (fun (n,cobj) ->
 196           for i = !last_cooked_level + 1 to n do
 197            add_cooked (uri,i) !last_cooked_obj
 198           done ;
 199           add_cooked (uri,n + 1) cobj ;
 200           last_cooked_level := n + 1 ;
 201           last_cooked_obj := cobj
 202         ) cooked_objs ;
 203        for i = !last_cooked_level + 1 to UriManager.depth_of_uri uri + 1 do
 204         add_cooked (uri,i) !last_cooked_obj
 205        done
 206   )
 207 ;;