]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic_proof_checking/cicEnvironment.ml
select and click signal added
[helm.git] / 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 let cleanup_tmp = true;;
39
40 let trust_obj = function uri -> true;;
41
42 type type_checked_obj =
43    CheckedObj of Cic.obj     (* cooked obj *)
44  | UncheckedObj of Cic.obj   (* uncooked obj to proof-check *)
45 ;;
46
47
48 exception AlreadyCooked of string;;
49 exception CircularDependency of string;;
50 exception CouldNotFreeze of string;;
51 exception CouldNotUnfreeze of string;;
52
53 (* Cache that uses == instead of = for testing equality *)
54 (* Invariant: an object is always in at most one of the *)
55 (* following states: unchecked, frozen and cooked.      *)
56 module Cache :
57   sig
58    val find_or_add_unchecked :
59     UriManager.uri -> get_object_to_add:(unit -> Cic.obj) -> Cic.obj
60    val unchecked_to_frozen : UriManager.uri -> unit
61    val frozen_to_cooked :
62     uri:UriManager.uri -> unit
63    val find_cooked : key:UriManager.uri -> Cic.obj
64    val add_cooked : key:UriManager.uri -> Cic.obj -> unit
65   end 
66 =
67   struct
68    module CacheOfCookedObjects :
69     sig
70      val mem  : UriManager.uri -> bool
71      val find : UriManager.uri -> Cic.obj
72      val add  : UriManager.uri -> Cic.obj -> unit
73     end
74    =
75     struct
76      module HashedType =
77       struct
78        type t = UriManager.uri
79        let equal = UriManager.eq
80        let hash = Hashtbl.hash
81       end
82      ;;
83      module HT = Hashtbl.Make(HashedType);;
84      let hashtable = HT.create 1009;;
85      let mem uri =
86       try
87        HT.mem hashtable uri
88       with
89        Not_found -> false
90      ;;
91      let find uri = HT.find hashtable uri
92      ;;
93      let add uri obj =
94       HT.add hashtable uri obj
95      ;;
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 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 =
126     try
127      let obj = List.assq uri !frozen_list in
128       frozen_list := List.remove_assq uri !frozen_list ;
129        CacheOfCookedObjects.add uri obj
130     with
131      Not_found -> raise (CouldNotUnfreeze (UriManager.string_of_uri uri))
132    ;;
133    let find_cooked ~key:uri = CacheOfCookedObjects.find uri;;
134    let add_cooked ~key:uri obj = CacheOfCookedObjects.add uri obj;;
135   end
136 ;;
137
138 let find_or_add_unchecked_to_cache uri =
139  Cache.find_or_add_unchecked uri
140   ~get_object_to_add:
141    (function () ->
142      let filename = Getter.getxml uri in
143      let bodyfilename =
144       match UriManager.bodyuri_of_uri uri with
145          None -> None
146        | Some bodyuri ->
147           try
148            ignore (Getter.resolve bodyuri) ;
149            (* The body exists ==> it is not an axiom *)
150            Some (Getter.getxml bodyuri)
151           with
152            Getter.Unresolved ->
153             (* The body does not exist ==> we consider it an axiom *)
154             None
155      in
156       let obj = CicParser.obj_of_xml filename bodyfilename in
157        if cleanup_tmp then
158         begin
159          Unix.unlink filename ;
160          match bodyfilename with
161             Some f -> Unix.unlink f
162           | None -> ()
163         end ;
164        obj
165    )
166 ;;
167
168 (* set_type_checking_info uri                               *)
169 (* must be called once the type-checking of uri is finished *)
170 (* The object whose uri is uri is unfreezed                 *)
171 let set_type_checking_info uri =
172  Cache.frozen_to_cooked uri
173 ;;
174
175 (* is_type_checked uri                                                *)
176 (* CSC: commento falso ed obsoleto *)
177 (* returns a CheckedObj if the term has been type-checked             *)
178 (* otherwise it freezes the term for type-checking and returns
179  it *)
180 (* set_type_checking_info must be called to unfreeze the term         *)
181 let is_type_checked ?(trust=true) uri =
182  try
183   CheckedObj (Cache.find_cooked uri)
184  with
185   Not_found ->
186    let obj = find_or_add_unchecked_to_cache uri in
187     Cache.unchecked_to_frozen uri ;
188     if trust && trust_obj uri then
189      begin
190       Logger.log (`Trusting uri) ;
191       set_type_checking_info uri ;
192       CheckedObj (Cache.find_cooked uri)
193      end
194     else
195      UncheckedObj obj
196 ;;
197
198 (* get_cooked_obj ~trust uri *)
199 (* returns the object if it is already type-checked or if it can be *)
200 (* trusted (if [trust] = true and the trusting function accepts it) *)
201 (* Otherwise it raises Not_found                                    *)
202 let get_cooked_obj ?(trust=true) uri =
203  try
204   Cache.find_cooked uri
205  with Not_found ->
206   if trust && trust_obj uri then
207    begin
208     match is_type_checked uri with
209        CheckedObj obj -> obj
210      | _ -> assert false
211    end
212   else
213    begin
214     prerr_endline ("@@@ OOOOOOOPS: get_cooked_obj(" ^ UriManager.string_of_uri uri ^ ") raises Not_found since the object is not type-checked nor trusted.") ;
215     raise Not_found
216    end
217 ;;
218
219 (* get_obj uri                                                                *)
220 (* returns the cic object whose uri is uri. If the term is not just in cache, *)
221 (* then it is parsed via CicParser.term_of_xml from the file whose name is    *)
222 (* the result of Getter.getxml uri                                            *)
223 let get_obj uri =
224  try
225   get_cooked_obj uri
226  with
227   Not_found ->
228    find_or_add_unchecked_to_cache uri
229 ;; 
230
231 exception OnlyPutOfInductiveDefinitionsIsAllowed
232
233 let put_inductive_definition uri obj =
234  match obj with
235     Cic.InductiveDefinition _ -> Cache.add_cooked uri obj
236   | _ -> raise OnlyPutOfInductiveDefinitionsIsAllowed
237 ;;