]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic_proof_checking/cicEnvironment.ml
added generation of LaTeX documentation
[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 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 ;;