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

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index ce16af7d2..cd49f2cea 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
 ;;
 
@@ -188,9 +197,9 @@ let does_not_occur ~subst context n nn t =
                perform substitution only if DoesOccur is raised *)
             let _,_,term,_ = U.lookup_subst mno subst in
             aux (k-s) () (S.subst_meta (0,l) term)
-          with U.Subst_not_found _ -> match l with
+          with U.Subst_not_found _ -> () (*match l with
           | C.Irl len -> if not (n+k >= s+len || s > nn+k) then raise DoesOccur
-          | C.Ctx lc -> List.iter (aux (k-s) ()) lc)
+          | C.Ctx lc -> List.iter (aux (k-s) ()) lc*))
     | t -> U.fold (fun _ k -> k + 1) k aux () t
   in
    try aux 0 () t; true
@@ -247,6 +256,10 @@ let rec weakly_positive ~subst context n nn uri indparamsno posuri te =
   let dummy = C.Sort C.Prop in
   (*CSC: to be moved in cicSubstitution? *)
   let rec subst_inductive_type_with_dummy _ = function
+    | C.Meta (_,(_,C.Irl _)) as x -> x
+    | C.Meta (i,(lift,C.Ctx ls)) -> 
+        C.Meta (i,(lift,C.Ctx 
+          (List.map (subst_inductive_type_with_dummy ()) ls)))
     | C.Const (Ref.Ref (uri',Ref.Ind (true,0,_))) when NUri.eq uri' uri -> dummy
     | C.Appl ((C.Const (Ref.Ref (uri',Ref.Ind (true,0,lno))))::tl) 
         when NUri.eq uri' uri -> 
@@ -261,6 +274,12 @@ let rec weakly_positive ~subst context n nn uri indparamsno posuri te =
   let rec aux context n nn te =
     match R.whd ~subst context te with
      | t when t = dummy -> true
+     | C.Meta (i,lc) ->
+        (try
+          let _,_,term,_ = U.lookup_subst i subst in
+          let t = S.subst_meta lc term in
+           weakly_positive ~subst context n nn uri indparamsno posuri t
+         with U.Subst_not_found _ -> true)
      | C.Appl (te::rargs) when te = dummy ->
         List.for_all (does_not_occur ~subst context n nn) rargs
      | C.Prod (name,source,dest) when
@@ -279,6 +298,12 @@ let rec weakly_positive ~subst context n nn uri indparamsno posuri te =
 and strictly_positive ~subst context n nn indparamsno posuri te =
   match R.whd ~subst context te with
    | t when does_not_occur ~subst context n nn t -> true
+   | C.Meta (i,lc) ->
+      (try
+        let _,_,term,_ = U.lookup_subst i subst in
+        let t = S.subst_meta lc term in
+         strictly_positive ~subst context n nn indparamsno posuri t
+       with U.Subst_not_found _ -> true)
    | C.Rel _ when indparamsno = 0 -> true
    | C.Appl ((C.Rel m)::tl) as reduct when m > n && m <= nn ->
       check_homogeneous_call ~subst context indparamsno n posuri reduct tl;
@@ -370,11 +395,11 @@ let rec typeof ~subst ~metasenv context term =
         with Failure _ -> 
           raise (TypeCheckerFailure (lazy ("unbound variable " ^ string_of_int n
             ^" under: " ^ NCicPp.ppcontext ~metasenv ~subst context))))
-    | C.Sort (C.Type [false,u]) -> C.Sort (C.Type [true, u])
-    | C.Sort (C.Type _) -> 
-        raise (AssertFailure (lazy ("Cannot type an inferred type: "^
-          NCicPp.ppterm ~subst ~metasenv ~context t)))
-    | C.Sort _ -> C.Sort (C.Type NCicEnvironment.type0)
+    | C.Sort s -> 
+         (try C.Sort (NCicEnvironment.typeof_sort s) 
+         with 
+         | NCicEnvironment.UntypableSort msg -> raise (TypeCheckerFailure msg)
+         | NCicEnvironment.AssertFailure msg -> raise (AssertFailure msg))
     | C.Implicit _ -> raise (AssertFailure (lazy "Implicit found"))
     | C.Meta (n,l) as t -> 
        let canonical_ctx,ty =
@@ -634,9 +659,10 @@ and check_allowed_sort_elimination ~subst ~metasenv r =
            (PP.ppterm ~subst ~metasenv ~context so)
            )));
          (match arity1, R.whd ~subst ((name,C.Decl so)::context) ta with
-           | (C.Sort C.Type _, C.Sort _)
-           | (C.Sort C.Prop, C.Sort C.Prop) -> ()
-           | (C.Sort C.Prop, C.Sort C.Type _) ->
+           | C.Sort s1, C.Sort s2 ->
+               (match NCicEnvironment.allowed_sort_elimination s1 s2 with
+               | `Yes -> ()
+               | `UnitOnly ->
        (* TODO: we should pass all these parameters since we
         * have them already *)
                let _,leftno,itl,_,i = E.get_checked_indtys r in
@@ -654,8 +680,8 @@ and check_allowed_sort_elimination ~subst ~metasenv r =
                      is_non_informative ~metasenv ~subst leftno constrty))
                 then
                  raise (TypeCheckerFailure (lazy
-                  ("Sort elimination not allowed")));
-         | _,_ -> ())
+                  ("Sort elimination not allowed"))))
+           | _ -> ())
       | _,_ -> ()
   in
    aux 
@@ -695,7 +721,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
@@ -712,7 +738,9 @@ and is_non_informative ~metasenv ~subst paramsno c =
    match R.whd ~subst context c with
     | C.Prod (n,so,de) ->
        let s = typeof ~metasenv ~subst context so in
-       s = C.Sort C.Prop && aux ((n,(C.Decl so))::context) de
+       (s = C.Sort C.Prop || 
+        match s with C.Sort (C.Type ((`CProp,_)::_)) -> true | _ -> false) && 
+       aux ((n,(C.Decl so))::context) de
     | _ -> true in
  let context',dx = NCicReduction.split_prods ~subst [] paramsno c in
   aux context' dx
@@ -733,7 +761,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 +892,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 ... *)
@@ -1024,10 +1052,7 @@ and is_really_smaller
     is_really_smaller r_uri r_len ~subst ~metasenv (shift_k (name,C.Decl s) k) t
  | C.Appl (he::_) ->
     is_really_smaller r_uri r_len ~subst ~metasenv k he
- | C.Rel _ 
- | C.Const (Ref.Ref (_,Ref.Con _)) -> false
- | C.Appl [] 
- | C.Const (Ref.Ref (_,Ref.Fix _)) -> assert false
+ | C.Appl [] | C.Implicit _ -> assert false
  | C.Meta _ -> true 
  | C.Match (Ref.Ref (_,Ref.Ind (isinductive,_,_)),_,term,pl) ->
     (match term with
@@ -1045,7 +1070,7 @@ and is_really_smaller
              is_really_smaller r_uri r_len ~subst ~metasenv k e)
            pl dcl
     | _ -> List.for_all (is_really_smaller r_uri r_len ~subst ~metasenv k) pl)
- | _ -> assert false
+ | _ -> false
 
 and returns_a_coinductive ~subst context ty =
   match R.whd ~subst context ty with
@@ -1204,7 +1229,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 +1239,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 +1247,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 +1284,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