Bug fixed: the debrujinate function (hence the one to compute objects height)

did not take the substitution.

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 9817474cddbb50cadea0f5b143d333bb65fdc3ce..eb994854f49c6d0e648aa7c4fa916aad18a38b63 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -705,7 +705,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
         let obj_kind =
          NCicUntrusted.map_obj_kind 
           (NCicUntrusted.apply_subst subst []) obj_kind in
-        let height = NCicTypeChecker.height_of_obj_kind uri obj_kind in
+        let height = NCicTypeChecker.height_of_obj_kind uri [] obj_kind in
         (* fix the height inside the object *)
         let rec fix () = function 
           | NCic.Const (NReference.Ref (u,spec)) when NUri.eq u uri -> 

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index ce16af7d213dc5fbb33f315fdeef49b526689d50..c4c2af477d3a510e33846f2bec5f827635a16ef3 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -96,13 +96,22 @@ let fixed_args bos j n nn =
    (let rec f = function 0 -> [] | n -> true :: f (n-1) in f j) bos
 ;;
 
-let debruijn uri number_of_types context = 
+let debruijn uri number_of_types ~subst context = 
+(* manca la subst! *)
  let rec aux k t =
   match t with
-   | C.Meta (i,(s,C.Ctx l)) ->
-      let l1 = HExtlib.sharing_map (aux (k-s)) l in
-      if l1 == l then t else C.Meta (i,(s,C.Ctx l1))
-   | C.Meta _ -> t
+   | C.Meta (i,(s,l)) ->
+      (try
+        let _,_,term,_ = U.lookup_subst i subst in
+        let ts = S.subst_meta (0,l) term in
+        let ts' = aux (k-s) ts in
+         if ts == ts' then t else ts'
+       with U.Subst_not_found _ ->
+        match l with
+           C.Ctx l ->
+            let l1 = HExtlib.sharing_map (aux (k-s)) l in
+            if l1 == l then t else C.Meta (i,(s,C.Ctx l1))
+         | _ -> t)
    | C.Const (Ref.Ref (uri1,(Ref.Fix (no,_,_) | Ref.CoFix no))) 
    | C.Const (Ref.Ref (uri1,Ref.Ind (_,no,_))) when NUri.eq uri uri1 ->
       C.Rel (k + number_of_types - no)
@@ -166,7 +175,7 @@ let specialize_and_abstract_constrs ~subst r_uri r_len context ty_term =
     | _ -> assert false
   in
   context_dcl,
-  List.map (fun (_,id,ty) -> id, debruijn r_uri r_len context ty) cl,
+  List.map (fun (_,id,ty) -> id, debruijn r_uri r_len ~subst context ty) cl,
   len, len + r_len
 ;;
 
@@ -695,7 +704,7 @@ and eat_prods ~subst ~metasenv context he ty_he args_with_ty =
 
 and is_non_recursive_singleton ~subst (Ref.Ref (uri,_)) iname ity cty =
      let ctx = [iname, C.Decl ity] in
-     let cty = debruijn uri 1 [] cty in
+     let cty = debruijn uri 1 [] ~subst cty in
      let len = List.length ctx in
      let rec aux ctx n nn t =
        match R.whd ~subst ctx t with
@@ -733,7 +742,7 @@ and check_mutual_inductive_defs uri ~metasenv ~subst leftno tyl =
           let k_relev =
             try snd (HExtlib.split_nth leftno k_relev)
             with Failure _ -> k_relev in
-           let te = debruijn uri len [] te in
+           let te = debruijn uri len [] ~subst te in
            let context,te = NCicReduction.split_prods ~subst tys leftno te in
            let _,chopped_context_rev =
             HExtlib.split_nth (List.length tys) (List.rev context) in
@@ -864,7 +873,7 @@ and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t =
         List.split (List.map (fun (_,name,_,ty,bo) -> (name, C.Decl ty), bo) fl)
       in
       let fl_len = List.length fl in
-      let bos = List.map (debruijn uri fl_len context) bos in
+      let bos = List.map (debruijn uri fl_len context ~subst) bos in
       let j = List.fold_left min max_int (List.map (fun (_,_,i,_,_)->i) fl) in
       let ctx_len = List.length context in
         (* we may look for fixed params not only up to j ... *)
@@ -1204,7 +1213,7 @@ let height_of_term tl =
   1 + !h
 ;;
 
-let height_of_obj_kind uri =
+let height_of_obj_kind uri ~subst =
  function
     NCic.Inductive _
   | NCic.Constant (_,_,None,_,_)
@@ -1214,7 +1223,7 @@ let height_of_obj_kind uri =
       height_of_term
        (List.fold_left
         (fun l (_,_,_,ty,bo) ->
-          let bo = debruijn uri iflno [] bo in
+          let bo = debruijn uri iflno [] ~subst bo in
            ty::bo::l
        ) [] ifl)
   | NCic.Constant (_,_,Some bo,ty,_) -> height_of_term [bo;ty]
@@ -1222,7 +1231,7 @@ let height_of_obj_kind uri =
 
 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
+ let iheight = height_of_obj_kind uri ~subst kind in
  if height <> iheight then
   raise (TypeCheckerFailure (lazy (Printf.sprintf
    "the declared object height (%d) is not the inferred one (%d)"
@@ -1259,7 +1268,7 @@ let typecheck_obj (uri,height,metasenv,subst,kind) =
       let dfl, kl =   
         List.split (List.map2 
           (fun (_,_,_,_,bo) rno -> 
-             let dbo = debruijn uri len [] bo in
+             let dbo = debruijn uri len [] ~subst bo in
              dbo, Evil rno)
           fl kl)
       in

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.mli b/helm/software/components/ng_kernel/nCicTypeChecker.mli
index af0f2cadeffb8d7528f05df5250c6f9e7b7262ff..3cd11c0f8fa78744e1fc5eee50c4c6c1bdf081e5 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.mli
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.mli
@@ -30,7 +30,7 @@ val typeof:
   NCic.context -> NCic.term -> 
     NCic.term
 
-val height_of_obj_kind: NUri.uri -> NCic.obj_kind -> int
+val height_of_obj_kind: NUri.uri -> subst:NCic.substitution -> NCic.obj_kind -> int
 
 val get_relevance : 
   metasenv:NCic.metasenv -> subst:NCic.substitution ->
@@ -53,7 +53,9 @@ val check_allowed_sort_elimination :
     NCic.term -> NCic.term -> NCic.term -> unit
 
 (* Functions to be used by the refiner *)
-val debruijn: NUri.uri -> int -> NCic.context -> NCic.term -> NCic.term
+val debruijn:
+ NUri.uri -> int -> subst:NCic.substitution -> NCic.context -> NCic.term ->
+  NCic.term
 val are_all_occurrences_positive: 
  subst:NCic.substitution ->
   NCic.context -> NUri.uri -> int -> int -> int -> int -> NCic.term -> bool

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 6bcda0df86781d8abe3f61bc5334bed860a2b6e3..d279b840b18d0fcc8602bff628677e7d32967dc3 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -574,8 +574,7 @@ let typeof_obj
          match bo with
          | Some bo ->
              let metasenv, subst, bo, ty = 
-               typeof rdb ~localise metasenv subst [] bo (Some ty)
-             in
+               typeof rdb ~localise metasenv subst [] bo (Some ty) in
              let height = (* XXX recalculate *) height in
                metasenv, subst, Some bo, ty, height
          | None -> metasenv, subst, None, ty, 0
@@ -588,7 +587,7 @@ let typeof_obj
         List.fold_left
          (fun (types, metasenv, subst, fl) (relevance,name,k,ty,bo) ->
            let metasenv, subst, ty, _ = check_type metasenv subst [] ty in
-           let dbo = NCicTypeChecker.debruijn uri len [] bo in
+           let dbo = NCicTypeChecker.debruijn uri len [] ~subst bo in
            let localise = relocalise localise dbo bo in
             (name,C.Decl ty)::types,
               metasenv, subst, (relevance,name,k,ty,dbo,localise)::fl
@@ -637,7 +636,7 @@ let typeof_obj
             let k_relev =
               try snd (HExtlib.split_nth leftno k_relev)
               with Failure _ -> k_relev in
-             let te = NCicTypeChecker.debruijn uri len [] te in
+             let te = NCicTypeChecker.debruijn uri len [] ~subst te in
              let metasenv, subst, te, _ = check_type metasenv subst tys te in
              let context,te = NCicReduction.split_prods ~subst tys leftno te in
              let _,chopped_context_rev =