Added check of relevance lists for inductive types/constructors and

fixpoint definitions.

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 5daea200c976f366fa55cc0e366adcb23bcd160b..56d06a71b673f7edee75136c29204a3d43dd2041 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -691,7 +691,6 @@ and is_non_informative paramsno c =
  let context',dx = split_prods ~subst:[] [] paramsno c in
   aux context' dx
 
-
 and check_mutual_inductive_defs uri ~metasenv ~subst leftno tyl = 
   (* let's check if the arity of the inductive types are well formed *)
   List.iter (fun (_,_,x,_) -> ignore (typeof ~subst ~metasenv [] x)) tyl;
@@ -700,11 +699,12 @@ and check_mutual_inductive_defs uri ~metasenv ~subst leftno tyl =
   let tys = List.rev_map (fun (_,n,ty,_) -> (n,(C.Decl ty))) tyl in
   ignore
    (List.fold_right
-    (fun (_,_,ty,cl) i ->
+    (fun (it_relev,_,ty,cl) i ->
        let context,ty_sort = split_prods ~subst [] ~-1 ty in
        let sx_context_ty_rev,_ = HExtlib.split_nth leftno (List.rev context) in
        List.iter
-         (fun (_,_,te) -> 
+         (fun (k_relev,_,te) ->
+          let _,k_relev = HExtlib.split_nth leftno k_relev in
            let te = debruijn uri len [] te in
            let context,te = split_prods ~subst tys leftno te in
            let _,chopped_context_rev =
@@ -755,11 +755,42 @@ and check_mutual_inductive_defs uri ~metasenv ~subst leftno tyl =
            then
              raise
                (TypeCheckerFailure
-                 (lazy ("Non positive occurence in "^NUri.string_of_uri uri))))
+                 (lazy ("Non positive occurence in "^NUri.string_of_uri
+                uri)))
+           else check_relevance ~subst ~metasenv context k_relev te) 
          cl;
-        i + 1)
+        check_relevance ~subst ~metasenv [] it_relev ty;
+       i+1)
     tyl 1)
 
+and check_relevance ~subst ~metasenv context relevance ty =
+  let error context ty =
+    raise (TypeCheckerFailure 
+     (lazy ("Wrong relevance declaration: " ^ 
+     String.concat "," (List.map string_of_bool relevance)^ 
+     "\nfor type: "^PP.ppterm ~metasenv ~subst ~context ty)))
+  in
+  let rec aux context relevance ty =
+    match R.whd ~subst context ty with
+    | C.Prod (name,so,de) ->
+        let sort = typeof ~subst ~metasenv context so in
+        (match (relevance,R.whd ~subst context sort) with
+         | [],_ -> ()
+          | false::tl,C.Sort C.Prop -> aux ((name,(C.Decl so))::context) tl de
+         | true::_,C.Sort C.Prop
+         | false::_,C.Sort _
+          | false::_,C.Meta _ -> error context ty
+          | true::tl,C.Sort _
+          | true::tl,C.Meta _ -> aux ((name,(C.Decl so))::context) tl de
+          | _ -> raise (AssertFailure (lazy (Printf.sprintf
+                 "Prod: the type %s of the source of %s is not a sort"
+                  (PP.ppterm ~subst ~metasenv ~context sort)
+                  (PP.ppterm ~subst ~metasenv ~context so)))))
+    | _ -> (match relevance with
+      | [] -> ()
+      | _::_ -> error context ty)
+  in aux context relevance ty
+
 and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t = 
  let recursor f k t = U.fold shift_k k (fun k () -> f k) () t in
  let rec aux (context, recfuns, x as k) t = 
@@ -1152,95 +1183,6 @@ let check_rel1_irrelevant ~metasenv ~subst context = fun _ -> ();;
   in 
     aux (1, context) () *)
 
-let check_relevance ~subst ~metasenv relevance ty =
-  let error () =
-    raise (TypeCheckerFailure 
-     (lazy ("Wrong relevance declaration: " ^ 
-     String.concat "," (List.map string_of_bool relevance)^ 
-     "\nfor type: "^PP.ppterm ~metasenv ~subst ~context:[] ty)))
-  in
-  let rec aux context relevance ty =
-    match R.whd ~subst context ty with
-    | C.Prod (name,so,de) ->
-        let sort = typeof ~subst ~metasenv context so in
-        (match (relevance,R.whd ~subst context sort) with
-         | [],_ -> ()
-          | false::tl,C.Sort C.Prop -> aux ((name,(C.Decl so))::context) tl de
-         | true::_,C.Sort C.Prop
-         | false::_,C.Sort _
-          | false::_,C.Meta _ -> error ()
-          | true::tl,C.Sort _
-          | true::tl,C.Meta _ -> aux ((name,(C.Decl so))::context) tl de
-          | _ -> raise (TypeCheckerFailure (lazy (Printf.sprintf
-                 "Prod: the type %s of the source of %s is not a sort"
-                  (PP.ppterm ~subst ~metasenv ~context sort)
-                  (PP.ppterm ~subst ~metasenv ~context so)))))
-    | _ -> (match relevance with
-      | [] -> ()
-      | _::_ -> error ())
-  in aux [] relevance ty
-;;
-(* old check_relevance
-
-let shift e (in_type, context, relevance) = 
-    assert (relevance = []); in_type, e::context, relevance
-  in
-  let rec aux2 (_,context,relevance as k) t = 
-    let error () = () (*
-      raise (TypeCheckerFailure 
-       (lazy ("Wrong relevance declaration: " ^ 
-       String.concat "," (List.map string_of_bool relevance)^ 
-       "\nfor: "^PP.ppterm ~metasenv ~subst ~context t))) *)
-    in
-    let rec aux (in_type, context, relevance as k) () t = 
-      match relevance, R.whd ~subst context t, in_type with
-      | _,C.Meta _,_ -> ()
-      | true::tl,C.Lambda (name,so,t), false 
-      | true::tl,C.Prod (name,so,t), true -> 
-          aux (in_type, (name, C.Decl so)::context, tl) () t
-      | false::tl,C.Lambda (name,so,t), false 
-      | false::tl,C.Prod (name,so,t), true -> 
-          let context = (name, C.Decl so)::context in
-          check_rel1_irrelevant ~metasenv ~subst context t;
-          aux (in_type, context, tl) () t
-      | [], C.Match (ref,oty,t,pl), _ ->
-          aux k () t;
-          let _,lno,itl,_,i = E.get_checked_indtys ref in
-          let rel,_,_,cl = List.nth itl i in
-          let _, rel = 
-            try HExtlib.split_nth lno rel 
-            with Failure _ -> [],[]
-          in
-          aux2 (false, context, rel) oty;
-          List.iter2 
-            (fun p (rel,_,_) -> 
-               let _,rel = 
-                 try HExtlib.split_nth lno rel 
-                 with Failure _ -> [],[]
-               in
-               aux2 (false, context, rel) p)
-            pl cl
-      | [],t,_ -> U.fold shift k aux () t
-      | rel1,C.Appl (C.Const ref :: args),_ ->
-          let relevance = E.get_relevance ref in
-          let _, relevance = 
-            try HExtlib.split_nth (List.length args) relevance 
-            with Failure _ -> [],[] 
-          in
-          prerr_endline ("rimane: "^String.concat "," (List.map string_of_bool relevance)^ " contro "^ String.concat "," (List.map string_of_bool rel1) );
-          HExtlib.list_iter_default2 (fun r1 r2 -> if not r1 && r2 then error ())
-            rel1 true relevance
-      | rel1,C.Const ref,_ ->
-          let relevance = E.get_relevance ref in
-          HExtlib.list_iter_default2 (fun r1 r2 -> if not r1 && r2 then error ())
-            rel1 true relevance
-      | _,_,_ -> error ()
-    in
-       aux k () t
-  in
-    aux2 (in_type, [], relevance)
-;;*)
-
 let typecheck_obj (uri,_height,metasenv,subst,kind) =
  (* height is not checked since it is only used to implement an optimization *)
  typecheck_metasenv metasenv;
@@ -1255,11 +1197,11 @@ let typecheck_obj (uri,_height,metasenv,subst,kind) =
         "inferred type:\n%s\nexpected type:\n%s")
         (PP.ppterm ~subst ~metasenv ~context:[] ty_te) 
         (PP.ppterm ~subst ~metasenv ~context:[] ty))));
-      check_relevance ~subst ~metasenv relevance ty
+      check_relevance ~subst ~metasenv [] relevance ty
       (*check_relevance ~in_type:false ~subst ~metasenv relevance te*)
    | C.Constant (relevance,_,None,ty,_) ->
       ignore (typeof ~subst ~metasenv [] ty);
-      check_relevance ~subst ~metasenv relevance ty
+      check_relevance ~subst ~metasenv [] relevance ty
    | C.Inductive (_, leftno, tyl, _) -> 
        check_mutual_inductive_defs uri ~metasenv ~subst leftno tyl
    | C.Fixpoint (inductive,fl,_) ->
@@ -1267,6 +1209,7 @@ let typecheck_obj (uri,_height,metasenv,subst,kind) =
         List.fold_left
          (fun (types,kl) (relevance,name,k,ty,_) ->
            let _ = typeof ~subst ~metasenv [] ty in
+           check_relevance ~subst ~metasenv [] relevance ty;
             ((name,C.Decl ty)::types, k::kl)
          ) ([],[]) fl
       in