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=8d0ae1a4f9e7e1a86225a23f2e5866fee1b8e3c0;hpb=b7535cd20248c564e942cc4e9058d34fbb062c6f;p=helm.git diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml index 8d0ae1a4f..b491d4c84 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.ml +++ b/helm/software/components/ng_kernel/nCicEnvironment.ml @@ -1,19 +1,99 @@ +(* + ||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_______________________________________________________________ *) + +(* $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 = - try NUri.UriHash.find cache u - with Not_found -> - let ouri = NUri.ouri_of_nuri u in - let o,_ = - CicEnvironment.get_cooked_obj ~trust:false CicUniv.oblivion_ugraph - ouri in - let no,_ = OCic2NCic.convert_obj ouri o in - NUri.UriHash.add cache u no; - no + 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_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) -> + | 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 @@ -23,22 +103,55 @@ let get_checked_def = function | _ -> prerr_endline "get_checked_def on a non def"; assert false ;; -let get_checked_fix_or_cofix b = function - | NReference.Ref (_, uri, NReference.Fix (fixno,_)) -> +let get_checked_indtys = function + | NReference.Ref (uri, (NReference.Ind (_,n)|NReference.Con (n,_))) -> (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 + | _,_,_,_, 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) - | _ -> 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 _) - | NReference.Ref (_, uri, NReference.Con _) -> + | 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 +;;