X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicTypeChecker.ml;h=c4c2af477d3a510e33846f2bec5f827635a16ef3;hb=c22f39a5d5afc0ef55beb221e00e2e6703b13d90;hp=ce16af7d213dc5fbb33f315fdeef49b526689d50;hpb=4ae18461e6dfbf0011c062ab56fe85be00f011ec;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index ce16af7d2..c4c2af477 100644
--- 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