X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicEnvironment.ml;h=b491d4c8403f1d9d7daf25c8186335696b7ea57e;hb=cf4da27b865107f9b89f3d2726f14d6e2694c548;hp=10d3c198dea12d1e4a47c7188cb6f9dbbbe6fd0e;hpb=f75d2cc521bfa9941efb91f3a23cf554220de8e4;p=helm.git diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml index 10d3c198d..b491d4c84 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.ml +++ b/helm/software/components/ng_kernel/nCicEnvironment.ml @@ -1,8 +1,157 @@ +(* + ||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 nuri = - let ouri = NUriManager.ouri_of_nuri nuri in - let o,_ = - CicEnvironment.get_cooked_obj ~trust:false CicUniv.oblivion_ugraph - ouri +(* $Id$ *) + +exception CircularDependency of string Lazy.t;; +exception ObjectNotFound of string Lazy.t;; +exception BadDependency of string Lazy.t;; + +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 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 - OCic2NCic.convert_obj o + match obj with + `WellTyped o -> o + | `Exn e -> raise e +;; + +let get_checked_decl = function + | NReference.Ref (uri, NReference.Decl) -> + (match get_checked_obj uri with + | _,height,_,_, NCic.Constant (rlv,name,None,ty,att) -> + rlv,name,ty,att,height + | _,_,_,_, NCic.Constant (_,_,Some _,_,_) -> + prerr_endline "get_checked_decl on a definition"; assert false + | _ -> prerr_endline "get_checked_decl on a non decl 2"; assert false) + | _ -> prerr_endline "get_checked_decl on a non decl"; assert false +;; + +let get_checked_def = function + | NReference.Ref (uri, NReference.Def _) -> + (match get_checked_obj uri with + | _,height,_,_, NCic.Constant (rlv,name,Some bo,ty,att) -> + rlv,name,bo,ty,att,height + | _,_,_,_, NCic.Constant (_,_,None,_,_) -> + prerr_endline "get_checked_def on an axiom"; assert false + | _ -> prerr_endline "get_checked_def on a non def 2"; assert false) + | _ -> prerr_endline "get_checked_def on a non def"; assert false +;; + +let get_checked_indtys = function + | 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 + | _ -> prerr_endline "get_checked_indtys on a non ind 2"; assert false) + | _ -> prerr_endline "get_checked_indtys on a non ind"; assert false +;; + +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 (_,funcs,att) -> + funcs, att, height + | _ ->prerr_endline "get_checked_(co)fix on a non (co)fix 2";assert false) + | r -> prerr_endline ("get_checked_(co)fix on " ^ NReference.string_of_reference r); assert false +;; + +let get_indty_leftno = function + | NReference.Ref (uri, NReference.Ind _) + | NReference.Ref (uri, NReference.Con _) -> + (match get_checked_obj uri with + | _,_,_,_, NCic.Inductive (_,left,_,_) -> left + | _ ->prerr_endline "get_indty_leftno called on a non ind 2";assert false) + | _ -> prerr_endline "get_indty_leftno called on a non indty";assert false +;; + +let get_relevance (NReference.Ref (_, infos) as r) = + match infos with + NReference.Def _ -> let res,_,_,_,_,_ = get_checked_def r in res + | NReference.Decl -> let res,_,_,_,_ = get_checked_decl r in res + | NReference.Ind _ -> + let _,_,tl,_,n = get_checked_indtys r in + let res,_,_,_ = List.nth tl n in + res + | NReference.Con (_,i) -> + let _,_,tl,_,n = get_checked_indtys r in + let _,_,_,cl = List.nth tl n in + let res,_,_ = List.nth cl (i - 1) in + res + | NReference.Fix (fixno,_,_) + | NReference.CoFix fixno -> + let fl,_,_ = get_checked_fixes_or_cofixes r in + let res,_,_,_,_ = List.nth fl fixno in + res +;; + + +let invalidate _ = + assert (!frozen_list = []); + NUri.UriHash.clear cache +;;