- changed license to lgpl

[helm.git] / helm / ocaml / cic_proof_checking / cicEnvironment.ml

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
index b7dda108592449434fccc60d601b572acf49e806..5c1daa1373be26c35df429e23e6789847db69f5d 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
@@ -59,7 +59,7 @@ exception AlreadyCooked of string;;
 exception CircularDependency of string;;
 exception CouldNotFreeze of string;;
 exception CouldNotUnfreeze of string;;
-exception Term_not_found of UriManager.uri;;
+exception Object_not_found of UriManager.uri;;
 
 
 (* ************************************************************************** *
@@ -99,6 +99,7 @@ module Cache :
    val is_in_frozen: UriManager.uri -> bool
    val is_in_unchecked: UriManager.uri -> bool
    val is_in_cooked: UriManager.uri -> bool
+   val list_all_cooked_uris: unit -> UriManager.uri list
   end 
 =
   struct
@@ -214,7 +215,7 @@ module Cache :
              C.CoFix (i, liftedfl)
       in
       function
-         C.Constant (name,bo,ty,params) ->
+         C.Constant (name,bo,ty,params,attrs) ->
            let bo' =
              match bo with
                None -> None
@@ -222,8 +223,8 @@ module Cache :
            in
            let ty' = restore_in_term ty in
            let params' = List.map recons params in
-           C.Constant (name, bo', ty', params')
-       | C.CurrentProof (name,conjs,bo,ty,params) ->
+           C.Constant (name, bo', ty', params',attrs)
+       | C.CurrentProof (name,conjs,bo,ty,params,attrs) ->
            let conjs' =
              List.map
                (function (i,hyps,ty) ->
@@ -245,8 +246,8 @@ module Cache :
            let bo' = restore_in_term bo in
            let ty' = restore_in_term ty in
            let params' = List.map recons params in
-           C.CurrentProof (name, conjs', bo', ty', params')
-       | C.Variable (name,bo,ty,params) ->
+           C.CurrentProof (name, conjs', bo', ty', params',attrs)
+       | C.Variable (name,bo,ty,params,attrs) ->
            let bo' =
              match bo with
                None -> None
@@ -254,8 +255,8 @@ module Cache :
            in
            let ty' = restore_in_term ty in
            let params' = List.map recons params in
-           C.Variable (name, bo', ty', params')
-       | C.InductiveDefinition (tl,params,paramsno) ->
+           C.Variable (name, bo', ty', params',attrs)
+       | C.InductiveDefinition (tl,params,paramsno,attrs) ->
            let params' = List.map recons params in
            let tl' =
              List.map (function (name, inductive, ty, constructors) ->
@@ -267,7 +268,7 @@ module Cache :
                  constructors))
                tl
            in
-           C.InductiveDefinition (tl', params', paramsno)
+           C.InductiveDefinition (tl', params', paramsno, attrs)
     ;;
 
     let empty () = 
@@ -458,6 +459,10 @@ module Cache :
        HT.remove cacheOfCookedObjects uri 
    ;;
    
+   let  list_all_cooked_uris () =
+     HT.fold (fun u _ l -> u::l) cacheOfCookedObjects []
+   ;;
+   
   end
 ;;
 
@@ -508,7 +513,10 @@ let get_object_to_add uri =
      CicParser.obj_of_xml filename bodyfilename 
    with exn -> 
      cleanup ();
-     raise exn
+     (match exn with
+     | CicParser.Getter_failure ("key_not_found", uri) ->
+         raise (Object_not_found (UriManager.uri_of_string uri))
+     | _ -> raise exn)
  in
  let ugraph,filename_univ = 
    (* FIXME: decomment this when the universes will be part of the library
@@ -653,26 +661,38 @@ let put_inductive_definition uri (obj,ugraph) =
   | _ -> raise OnlyPutOfInductiveDefinitionsIsAllowed
 ;;
 
-let in_cache uri = 
- if Cache.is_in_cooked uri then
-   (prerr_endline "TROVATO NELLA CHECKED";true)
- else  
-   if Cache.is_in_frozen uri then
-     (prerr_endline "TROVATO NELLA FROZEN";true)
-   else
-     if Cache.is_in_unchecked uri then
-       (prerr_endline "TROVATO NELLA UNCHECKED";true)
-     else
-       (prerr_endline ("NON TROVATO:" ^ (UriManager.string_of_uri uri) );false)
-;;
+let in_cache uri =
+  Cache.is_in_cooked uri || Cache.is_in_frozen uri || Cache.is_in_unchecked uri
 
 let add_type_checked_term uri (obj,ugraph) =
   match obj with 
-      Cic.Constant (s,(Some bo),ty,ul) ->
+      Cic.Constant (s,(Some bo),ty,ul,_) ->
        Cache.add_cooked ~key:uri (obj,ugraph)
     | _ -> 
        assert false 
 ;;
 
+let in_library uri =
+  in_cache uri ||
+  (try
+    ignore (Http_getter.resolve' uri);
+    true
+  with Http_getter_types.Key_not_found _ -> false)
+
 let remove_term = Cache.remove
+  
+let list_uri () = 
+  Cache.list_all_cooked_uris ()
+;;
 
+let list_obj () =
+  try 
+    List.map (fun u -> 
+      let o,ug = get_obj CicUniv.empty_ugraph u in
+        (u,o,ug)) 
+    (list_uri ())
+  with
+    Not_found -> 
+      prerr_endline "Who has removed the uri in the meanwhile?";
+      raise Not_found
+;;