Exported apply_subst_context

[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 6dbaf3e5d05a702c45ac967d581e60a578955466..cd49f2cea93332c7de1eb428292240225d4df6b2 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -395,16 +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] 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)))
-    | 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 =
@@ -664,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
@@ -684,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 
@@ -742,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
@@ -1054,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
@@ -1075,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