Meta case not handled, the iterator was complaining.

[helm.git] / helm / software / components / ng_kernel / nCicTypeChecker.ml

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index c4c2af477d3a510e33846f2bec5f827635a16ef3..6dbaf3e5d05a702c45ac967d581e60a578955466 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -197,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
@@ -256,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 -> 
@@ -270,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
@@ -288,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;
@@ -379,7 +395,12 @@ 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 ([false,u] as univ)) ->
+       if NCicEnvironment.is_declared univ then
+        C.Sort (C.Type [true, u])
+       else
+        raise (TypeCheckerFailure (lazy ("undeclared universe " ^
+         NUri.string_of_uri u)))
     | C.Sort (C.Type _) -> 
         raise (AssertFailure (lazy ("Cannot type an inferred type: "^
           NCicPp.ppterm ~subst ~metasenv ~context t)))