X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicEnvironment.ml;h=823aa3a40880b8500f6723fad1a8bfc76361ecff;hb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;hp=9d93c443e44479248c793cac425ed9427801c332;hpb=2dc0733271cd251aaa3edaece8a883fe691775ab;p=helm.git diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml index 9d93c443e..823aa3a40 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml @@ -35,18 +35,15 @@ (* *) (******************************************************************************) +let cleanup_tmp = true;; + +let trust_obj = function uri -> true;; + type type_checked_obj = CheckedObj of Cic.obj (* cooked obj *) | UncheckedObj of Cic.obj (* uncooked obj to proof-check *) ;; -exception NoFunctionProvided;; - -let cook_obj = ref (fun obj uri -> raise NoFunctionProvided);; - -let set_cooking_function foo = - cook_obj := foo -;; exception AlreadyCooked of string;; exception CircularDependency of string;; @@ -62,22 +59,17 @@ module Cache : UriManager.uri -> get_object_to_add:(unit -> Cic.obj) -> Cic.obj val unchecked_to_frozen : UriManager.uri -> unit val frozen_to_cooked : - uri:UriManager.uri -> - cooking_procedure: - (object_to_cook:Cic.obj -> - add_cooked:(UriManager.uri * int-> Cic.obj -> unit) - -> unit - ) - -> unit - val find_cooked : key:(UriManager.uri * int) -> Cic.obj + uri:UriManager.uri -> unit + val find_cooked : key:UriManager.uri -> Cic.obj + val add_cooked : key:UriManager.uri -> Cic.obj -> unit end = struct module CacheOfCookedObjects : sig - val mem : UriManager.uri -> int -> bool - val find : UriManager.uri -> int -> Cic.obj - val add : UriManager.uri -> int -> Cic.obj -> unit + val mem : UriManager.uri -> bool + val find : UriManager.uri -> Cic.obj + val add : UriManager.uri -> Cic.obj -> unit end = struct @@ -90,29 +82,16 @@ module Cache : ;; module HT = Hashtbl.Make(HashedType);; let hashtable = HT.create 1009;; - let mem uri cookingsno = + let mem uri = try - let cooked_list = - HT.find hashtable uri - in - List.mem_assq cookingsno !cooked_list + HT.mem hashtable uri with Not_found -> false ;; - let find uri cookingsno = - List.assq cookingsno !(HT.find hashtable uri) + let find uri = HT.find hashtable uri ;; - let add uri cookingsno obj = - let cooked_list = - try - HT.find hashtable uri - with - Not_found -> - let newl = ref [] in - HT.add hashtable uri newl ; - newl - in - cooked_list := (cookingsno,obj)::!cooked_list + let add uri obj = + HT.add hashtable uri obj ;; end ;; @@ -127,7 +106,7 @@ module Cache : if List.mem_assq uri !frozen_list then raise (CircularDependency (UriManager.string_of_uri uri)) else - if CacheOfCookedObjects.mem uri 0 then + if CacheOfCookedObjects.mem uri then raise (AlreadyCooked (UriManager.string_of_uri uri)) else (* OK, it is not already frozen nor cooked *) @@ -143,48 +122,55 @@ module Cache : with Not_found -> raise (CouldNotFreeze (UriManager.string_of_uri uri)) ;; - let frozen_to_cooked ~uri ~cooking_procedure = + let frozen_to_cooked ~uri = try let obj = List.assq uri !frozen_list in frozen_list := List.remove_assq uri !frozen_list ; - cooking_procedure - ~object_to_cook:obj - ~add_cooked:(fun (uri,cookno) -> CacheOfCookedObjects.add uri cookno) + CacheOfCookedObjects.add uri obj with Not_found -> raise (CouldNotUnfreeze (UriManager.string_of_uri uri)) ;; - let find_cooked ~key:(uri,cookingsno)= CacheOfCookedObjects.find uri cookingsno;; + let find_cooked ~key:uri = CacheOfCookedObjects.find uri;; + let add_cooked ~key:uri obj = CacheOfCookedObjects.add uri obj;; end ;; -(* get_cooked_obj uri *) -(* returns the cooked cic object whose uri is uri. The term must be present *) -(* and cooked in cache *) -let get_cooked_obj uri cookingsno = - Cache.find_cooked (uri,cookingsno) -;; - let find_or_add_unchecked_to_cache uri = Cache.find_or_add_unchecked uri ~get_object_to_add: (function () -> let filename = Getter.getxml uri in - let obj = CicParser.obj_of_xml filename uri in + let bodyfilename = + match UriManager.bodyuri_of_uri uri with + None -> None + | Some bodyuri -> + try + ignore (Getter.resolve bodyuri) ; + (* The body exists ==> it is not an axiom *) + Some (Getter.getxml bodyuri) + with + Getter.Unresolved -> + (* The body does not exist ==> we consider it an axiom *) + None + in + let obj = CicParser.obj_of_xml filename bodyfilename in + if cleanup_tmp then + begin + Unix.unlink filename ; + match bodyfilename with + Some f -> Unix.unlink f + | None -> () + end ; obj ) ;; -(* get_obj uri *) -(* returns the cic object whose uri is uri. If the term is not just in cache, *) -(* then it is parsed via CicParser.term_of_xml from the file whose name is *) -(* the result of Getter.getxml uri *) -let get_obj uri = - try - get_cooked_obj uri 0 - with - Not_found -> - find_or_add_unchecked_to_cache uri -;; +(* set_type_checking_info uri *) +(* must be called once the type-checking of uri is finished *) +(* The object whose uri is uri is unfreezed *) +let set_type_checking_info uri = + Cache.frozen_to_cooked uri +;; (* is_type_checked uri *) (* CSC: commento falso ed obsoleto *) @@ -192,39 +178,60 @@ let get_obj uri = (* otherwise it freezes the term for type-checking and returns it *) (* set_type_checking_info must be called to unfreeze the term *) -let is_type_checked uri cookingsno = +let is_type_checked ?(trust=true) uri = try - CheckedObj (Cache.find_cooked (uri,cookingsno)) + CheckedObj (Cache.find_cooked uri) with Not_found -> let obj = find_or_add_unchecked_to_cache uri in Cache.unchecked_to_frozen uri ; - UncheckedObj obj + if trust && trust_obj uri then + begin + Logger.log (`Trusting uri) ; + set_type_checking_info uri ; + CheckedObj (Cache.find_cooked uri) + end + else + UncheckedObj obj ;; -(* set_type_checking_info uri *) -(* must be called once the type-checking of uri is finished *) -(* The object whose uri is uri is unfreezed *) -let set_type_checking_info uri = - Cache.frozen_to_cooked uri - (fun ~object_to_cook:obj ~add_cooked -> - (* let's cook the object at every level *) - let obj' = CicSubstitution.undebrujin_inductive_def uri obj in - add_cooked (uri,0) obj' ; - let cooked_objs = !cook_obj obj' uri in - let last_cooked_level = ref 0 in - let last_cooked_obj = ref obj' in - List.iter - (fun (n,cobj) -> - for i = !last_cooked_level + 1 to n do - add_cooked (uri,i) !last_cooked_obj - done ; - add_cooked (uri,n + 1) cobj ; - last_cooked_level := n + 1 ; - last_cooked_obj := cobj - ) cooked_objs ; - for i = !last_cooked_level + 1 to UriManager.depth_of_uri uri + 1 do - add_cooked (uri,i) !last_cooked_obj - done - ) +(* get_cooked_obj ~trust uri *) +(* returns the object if it is already type-checked or if it can be *) +(* trusted (if [trust] = true and the trusting function accepts it) *) +(* Otherwise it raises Not_found *) +let get_cooked_obj ?(trust=true) uri = + try + Cache.find_cooked uri + with Not_found -> + if trust && trust_obj uri then + begin + match is_type_checked uri with + CheckedObj obj -> obj + | _ -> assert false + end + else + begin + prerr_endline ("@@@ OOOOOOOPS: get_cooked_obj(" ^ UriManager.string_of_uri uri ^ ") raises Not_found since the object is not type-checked nor trusted.") ; + raise Not_found + end +;; + +(* get_obj uri *) +(* returns the cic object whose uri is uri. If the term is not just in cache, *) +(* then it is parsed via CicParser.term_of_xml from the file whose name is *) +(* the result of Getter.getxml uri *) +let get_obj uri = + try + get_cooked_obj uri + with + Not_found -> + find_or_add_unchecked_to_cache uri +;; + +exception OnlyPutOfInductiveDefinitionsIsAllowed + +let put_inductive_definition uri obj = + match obj with + Cic.InductiveDefinition _ -> Cache.add_cooked uri obj + | _ -> raise OnlyPutOfInductiveDefinitionsIsAllowed ;;