From 156b87c397a8b5cf9b7381def41e070e235941ee Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 5 Jun 2009 08:56:17 +0000 Subject: [PATCH] The kernel _must_ check the correctness of the height since the reduction machine never tries to reduce terms whose height is 0. Thus, if the declared height is 0, the height is no longer an optimization! --- .../grafite_engine/grafiteEngine.ml | 2 +- .../components/ng_kernel/nCicTypeChecker.ml | 47 ++++++++++++++++++- .../components/ng_kernel/nCicTypeChecker.mli | 2 + .../components/ng_kernel/nCicUntrusted.ml | 39 --------------- .../components/ng_kernel/nCicUntrusted.mli | 2 - 5 files changed, 48 insertions(+), 44 deletions(-) diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 8101dd667..d4738a551 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -776,7 +776,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status let obj_kind = NCicUntrusted.map_obj_kind (NCicUntrusted.apply_subst subst []) obj_kind in - let height = NCicUntrusted.height_of_obj_kind uri obj_kind in + let height = NCicTypeChecker.height_of_obj_kind uri obj_kind in let obj = uri,height,[],[],obj_kind in NCicTypeChecker.typecheck_obj obj; NCicLibrary.add_obj uri obj; diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index 0d3fc07d1..ce16af7d2 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -1181,9 +1181,52 @@ let typecheck_subst ~metasenv subst = ) [] subst) ;; +let height_of_term tl = + let h = ref 0 in + let get_height (NReference.Ref (uri,_)) = + let _,height,_,_,_ = NCicEnvironment.get_checked_obj uri in + height in + let rec aux = + function + NCic.Meta (_,(_,NCic.Ctx l)) -> List.iter aux l + | NCic.Meta _ -> () + | NCic.Rel _ + | NCic.Sort _ -> () + | NCic.Implicit _ -> assert false + | NCic.Const nref -> h := max !h (get_height nref) + | NCic.Prod (_,t1,t2) + | NCic.Lambda (_,t1,t2) -> aux t1; aux t2 + | NCic.LetIn (_,s,ty,t) -> aux s; aux ty; aux t + | NCic.Appl l -> List.iter aux l + | NCic.Match (_,outty,t,pl) -> aux outty; aux t; List.iter aux pl + in + List.iter aux tl; + 1 + !h +;; + +let height_of_obj_kind uri = + function + NCic.Inductive _ + | NCic.Constant (_,_,None,_,_) + | NCic.Fixpoint (false,_,_) -> 0 + | NCic.Fixpoint (true,ifl,_) -> + let iflno = List.length ifl in + height_of_term + (List.fold_left + (fun l (_,_,_,ty,bo) -> + let bo = debruijn uri iflno [] bo in + ty::bo::l + ) [] ifl) + | NCic.Constant (_,_,Some bo,ty,_) -> height_of_term [bo;ty] +;; -let typecheck_obj (uri,_height,metasenv,subst,kind) = - (* height is not checked since it is only used to implement an optimization *) +let typecheck_obj (uri,height,metasenv,subst,kind) = +(*height must be checked since it is not only an optimization during reduction*) + let iheight = height_of_obj_kind uri kind in + if height <> iheight then + raise (TypeCheckerFailure (lazy (Printf.sprintf + "the declared object height (%d) is not the inferred one (%d)" + height iheight))); typecheck_metasenv metasenv; typecheck_subst ~metasenv subst; match kind with diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.mli b/helm/software/components/ng_kernel/nCicTypeChecker.mli index 6ad40b8bb..df76faab7 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.mli +++ b/helm/software/components/ng_kernel/nCicTypeChecker.mli @@ -33,6 +33,8 @@ val typeof: NCic.context -> NCic.term -> NCic.term +val height_of_obj_kind: NUri.uri -> NCic.obj_kind -> int + val get_relevance : metasenv:NCic.metasenv -> subst:NCic.substitution -> NCic.context -> NCic.term -> NCic.term list -> bool list diff --git a/helm/software/components/ng_kernel/nCicUntrusted.ml b/helm/software/components/ng_kernel/nCicUntrusted.ml index dc26794a1..baae7f9c2 100644 --- a/helm/software/components/ng_kernel/nCicUntrusted.ml +++ b/helm/software/components/ng_kernel/nCicUntrusted.ml @@ -209,42 +209,3 @@ let rec apply_subst_metasenv subst = function (i,(name,apply_subst_context subst ctx,apply_subst subst ctx ty)) :: apply_subst_metasenv subst tl ;; - -let height_of_term tl = - let h = ref 0 in - let get_height (NReference.Ref (uri,_)) = - let _,height,_,_,_ = NCicEnvironment.get_checked_obj uri in - height in - let rec aux = - function - NCic.Meta (_,(_,NCic.Ctx l)) -> List.iter aux l - | NCic.Meta _ -> () - | NCic.Rel _ - | NCic.Sort _ -> () - | NCic.Implicit _ -> assert false - | NCic.Const nref -> h := max !h (get_height nref) - | NCic.Prod (_,t1,t2) - | NCic.Lambda (_,t1,t2) -> aux t1; aux t2 - | NCic.LetIn (_,s,ty,t) -> aux s; aux ty; aux t - | NCic.Appl l -> List.iter aux l - | NCic.Match (_,outty,t,pl) -> aux outty; aux t; List.iter aux pl - in - List.iter aux tl; - 1 + !h -;; - -let height_of_obj_kind uri = - function - NCic.Inductive _ - | NCic.Constant (_,_,None,_,_) - | NCic.Fixpoint (false,_,_) -> 0 - | NCic.Fixpoint (true,ifl,_) -> - let iflno = List.length ifl in - height_of_term - (List.fold_left - (fun l (_,_,_,ty,bo) -> - let bo = NCicTypeChecker.debruijn uri iflno [] bo in - ty::bo::l - ) [] ifl) - | NCic.Constant (_,_,Some bo,ty,_) -> height_of_term [bo;ty] -;; diff --git a/helm/software/components/ng_kernel/nCicUntrusted.mli b/helm/software/components/ng_kernel/nCicUntrusted.mli index 9cde401b0..1df92163d 100644 --- a/helm/software/components/ng_kernel/nCicUntrusted.mli +++ b/helm/software/components/ng_kernel/nCicUntrusted.mli @@ -27,5 +27,3 @@ val mk_appl : NCic.term -> NCic.term list -> NCic.term (* the context is needed only to honour Barendregt's naming convention *) val apply_subst : NCic.substitution -> NCic.context -> NCic.term -> NCic.term val apply_subst_metasenv : NCic.substitution -> NCic.metasenv -> NCic.metasenv - -val height_of_obj_kind: NUri.uri -> NCic.obj_kind -> int -- 2.39.2