X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicEnvironment.ml;h=38982d799768183d7353f1d205cfe2236000a699;hb=7f5d0adf3d44aa3e52e882dbe5f42358b8ee96cf;hp=599e1691f6bd37fd2eb0a18c52ffa9ec88d046ad;hpb=d9037e385e4cb12eccd8a734f4a9fc1a5a0f8b62;p=helm.git diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml index 599e1691f..38982d799 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.ml +++ b/helm/software/components/ng_kernel/nCicEnvironment.ml @@ -1,40 +1,82 @@ -let cache = NUri.UriHash.create 313;; +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) -let get_checked_obj u = - try let b, o = NUri.UriHash.find cache u in - if not b then assert false else o - with Not_found -> - let ouri = NUri.ouri_of_nuri u in - let o,_ = - try - CicEnvironment.get_obj CicUniv.oblivion_ugraph ouri - with exn -> prerr_endline (UriManager.string_of_uri ouri); raise exn - in - (* FIX: add all objects to the environment and give back the last one *) - let l = OCic2NCic.convert_obj ouri o in - List.iter (fun (u,_,_,_,_ as o) -> -(* prerr_endline ("+"^NUri.string_of_uri u); *) - NUri.UriHash.add cache u (false,o)) l; - HExtlib.list_last l -;; +exception CircularDependency of string Lazy.t;; +exception ObjectNotFound of string Lazy.t;; +exception BadDependency of string Lazy.t;; -let get_obj u = - try NUri.UriHash.find cache u - with Not_found -> - (* in th final implementation should get it from disk *) - let ouri = NUri.ouri_of_nuri u in - let o,_ = - CicEnvironment.get_obj CicUniv.oblivion_ugraph ouri - in - let l = OCic2NCic.convert_obj ouri o in - List.iter (fun (u,_,_,_,_ as o) -> -(* prerr_endline ("+"^NUri.string_of_uri u); *) - NUri.UriHash.add cache u (false,o)) l; - false, HExtlib.list_last l +let typecheck_obj,already_set = ref (fun _ -> assert false), ref false;; +let set_typecheck_obj f = + if !already_set then + assert false + else + begin + typecheck_obj := f; + already_set := true + end ;; -let add_obj (u,_,_,_,_ as o) = - NUri.UriHash.replace cache u (true, o) +let cache = NUri.UriHash.create 313;; +let frozen_list = ref [];; + +exception Propagate of NUri.uri * exn;; + +let get_checked_obj u = + if List.exists (fun (k,_) -> NUri.eq u k) !frozen_list + then + raise (CircularDependency (lazy (NUri.string_of_uri u))) + else + let obj = + try NUri.UriHash.find cache u + with + Not_found -> + let saved_frozen_list = !frozen_list in + try + let obj = + try NCicLibrary.get_obj u + with + NCicLibrary.ObjectNotFound m -> raise (ObjectNotFound m) + in + frozen_list := (u,obj)::saved_frozen_list; + !typecheck_obj obj; + frozen_list := saved_frozen_list; + let obj = `WellTyped obj in + NUri.UriHash.add cache u obj; + obj + with + Sys.Break as e -> + frozen_list := saved_frozen_list; + raise e + | Propagate (u',_) as e' -> + frozen_list := saved_frozen_list; + let exn = `Exn (BadDependency (lazy (NUri.string_of_uri u' ^ + " depends (recursively) on " ^ NUri.string_of_uri u ^ + " which is not well-typed"))) in + NUri.UriHash.add cache u exn; + if saved_frozen_list = [] then + exn + else + raise e' + | e -> + frozen_list := saved_frozen_list; + let exn = `Exn e in + NUri.UriHash.add cache u exn; + if saved_frozen_list = [] then + exn + else + raise (Propagate (u,e)) + in + match obj with + `WellTyped o -> o + | `Exn e -> raise e ;; let get_checked_def = function @@ -49,7 +91,7 @@ let get_checked_def = function ;; let get_checked_indtys = function - | NReference.Ref (_, uri, NReference.Ind n) -> + | NReference.Ref (_, uri, (NReference.Ind (_,n)|NReference.Con (n,_))) -> (match get_checked_obj uri with | _,_,_,_, NCic.Inductive (inductive,leftno,tys,att) -> inductive,leftno,tys,att,n @@ -57,17 +99,14 @@ let get_checked_indtys = function | _ -> prerr_endline "get_checked_indtys on a non ind"; assert false ;; -let get_checked_fix_or_cofix b = function - | NReference.Ref (_, uri, NReference.Fix (fixno,_)) -> +let get_checked_fixes_or_cofixes = function + | NReference.Ref (_, uri, (NReference.Fix (fixno,_)|NReference.CoFix fixno))-> (match get_checked_obj uri with - | _,height,_,_, NCic.Fixpoint (is_fix,funcs,att) when is_fix = b -> - let rlv, name, _, ty, bo = List.nth funcs fixno in - rlv, name, bo, ty, att, height + | _,height,_,_, NCic.Fixpoint (_,funcs,att) -> + funcs, att, height | _ ->prerr_endline "get_checked_(co)fix on a non (co)fix 2";assert false) - | _ -> prerr_endline "get_checked_(co)fix on a non (co)fix"; assert false + | r -> prerr_endline ("get_checked_(co)fix on " ^ NReference.string_of_reference r); assert false ;; -let get_checked_fix r = get_checked_fix_or_cofix true r;; -let get_checked_cofix r = get_checked_fix_or_cofix false r;; let get_indty_leftno = function | NReference.Ref (_, uri, NReference.Ind _) @@ -79,9 +118,6 @@ let get_indty_leftno = function ;; let invalidate _ = - List.iter - (fun (k,v) -> - NUri.UriHash.replace cache k (false,v)) - (NUri.UriHash.fold (fun k v -> (@) [k,snd v]) cache []) + assert (!frozen_list = []); + NUri.UriHash.clear cache ;; -