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!

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 8101dd667b96572d2581108e806004b28ad8f007..d4738a5515d73cb9cabc3b9a948869d1ef6dd4a8 100644 (file)
--- 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 0d3fc07d12458267ef78b7addf98d4a393502047..ce16af7d213dc5fbb33f315fdeef49b526689d50 100644 (file)
--- 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 6ad40b8bb555c91f1f339fcb97861918b40eb724..df76faab71255607b1763621d755232a79565fe2 100644 (file)
--- 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 dc26794a1a096cb4f9575e93cf9e826cbe83989a..baae7f9c2f7486e1561b3ad6a47eddaeb7522c5b 100644 (file)
--- 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 9cde401b04542c5b0dd04eb4d4bfe8bbdcf66c43..1df92163d845c4d55f689978c05cfed6d1e00748 100644 (file)
--- 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