From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 5 Jun 2009 08:56:17 +0000 (+0000)
Subject: The kernel _must_ check the correctness of the height since the reduction
X-Git-Tag: make_still_working~3918
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=156b87c397a8b5cf9b7381def41e070e235941ee;p=helm.git

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 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