relevance check partially implemented but bugged since cic:/matita/nat/compare/eqb...

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index efb8386d1e1b787237abc00747b48446ad193108..598ed2a67c5b857072506292391d9594f461a01f 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -627,16 +627,6 @@ let rec typeof ~subst ~metasenv context term =
            "Local and canonical context %s have different lengths"
            (PP.ppterm ~subst ~metasenv ~context term))))
 
-  and is_non_informative context paramsno c =
-   let rec aux context c =
-     match R.whd context c with
-      | C.Prod (n,so,de) ->
-         let s = typeof_aux context so in
-         s = C.Sort C.Prop && aux ((n,(C.Decl so))::context) de
-      | _ -> true in
-   let context',dx = split_prods ~subst:[] context paramsno c in
-    aux context' dx
-
   and check_allowed_sort_elimination ~subst ~metasenv r =
    let mkapp he arg =
      match he with
@@ -670,15 +660,15 @@ let rec typeof ~subst ~metasenv context term =
          * have them already *)
                 let _,leftno,itl,_,i = E.get_checked_indtys r in
                 let itl_len = List.length itl in
-                let _,name,ty,cl = List.nth itl i in
+                let _,_,_,cl = List.nth itl i in
                 let cl_len = List.length cl in
                  (* is it a singleton or empty non recursive and non informative
                     definition? *)
                  if not
                   (cl_len = 0 ||
                    (itl_len = 1 && cl_len = 1 &&
-                    is_non_informative [name,C.Decl ty] leftno
-                     (let _,_,x = List.nth cl 0 in x)))
+                    is_non_informative leftno
+                     (let _,_,x = List.hd cl in x)))
                  then
                   raise (TypeCheckerFailure (lazy
                    ("Sort elimination not allowed")));
@@ -690,6 +680,17 @@ let rec typeof ~subst ~metasenv context term =
  in 
    typeof_aux context term
 
+and is_non_informative paramsno c =
+ let rec aux context c =
+   match R.whd 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
+    | _ -> true in
+ 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;
@@ -1081,6 +1082,68 @@ let typecheck_subst ~metasenv subst =
     ) [] subst)
 ;;
 
+let check_rel1_irrelevant ~metasenv ~subst context =
+  let shift e (k, context) = k+1,e::context in
+  let rec aux (evil, context as k) () t =
+    match R.whd ~subst context t with
+    | C.Rel i when i = evil -> raise (TypeCheckerFailure (lazy (Printf.sprintf
+         "Argument %s declared as irrelevante is used in a relevant position" 
+           (PP.ppterm ~subst ~metasenv ~context (C.Rel i)))))
+    | C.Meta _ -> ()
+    | C.Lambda (name,so,tgt) -> 
+        (* checking so is not needed since the implicit version of CC
+         * has untyped lambdas (curry style), see Barras and Bernardo  *)
+        aux (shift (name,C.Decl so) k) () tgt 
+    | C.Appl (C.Const ref::args) -> 
+         let relevance = NCicEnvironment.get_relevance ref in
+         HExtlib.list_iter_default2 
+           (fun t -> function false -> () | _ -> aux k () t)
+           args true relevance
+    | C.Match (_, _, _, []) -> ()
+    | C.Match (ref, _, t, [p]) -> 
+        aux k () p;
+        let _,lno,itl,_,_ = E.get_checked_indtys ref in
+        let _,_,_,cl = List.hd itl in
+        let _,_,c = List.hd cl in
+        if not (is_non_informative lno c) then aux k () t
+    | C.Match (_, _, t, pl) -> List.iter (aux k ()) (t::pl)
+    | t -> U.fold shift k aux () t
+  in 
+    aux (1, context) ()
+
+let check_relevance ~metasenv ~subst ~in_type relevance = 
+  let shift e (in_type, context, relevance) = 
+    assert (relevance = []); in_type, e::context, relevance
+  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 = HExtlib.split_nth lno rel in
+        aux (false, context, rel) () oty;
+        List.iter2 
+          (fun p (rel,_,_) -> 
+             let _,rel = HExtlib.split_nth lno rel in
+             aux (false, context, rel) () p)
+          pl cl
+    | [],t,_ -> U.fold shift k aux () t
+    | _,_,_ -> 
+        raise (TypeCheckerFailure (lazy "Wrong relevance declaration"))
+  in
+     aux (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;
@@ -1094,9 +1157,12 @@ let typecheck_obj (uri,_height,metasenv,subst,kind) =
         "the type of the body is not convertible with the declared one.\n"^^
         "inferred type:\n%s\nexpected type:\n%s")
         (PP.ppterm ~subst ~metasenv ~context:[] ty_te) 
-        (PP.ppterm ~subst ~metasenv ~context:[] ty))))
+        (PP.ppterm ~subst ~metasenv ~context:[] ty))));
+      check_relevance ~in_type:true ~subst ~metasenv relevance ty;
+      check_relevance ~in_type:false ~subst ~metasenv relevance te
    | C.Constant (relevance,_,None,ty,_) ->
-      ignore (typeof ~subst ~metasenv [] ty)
+      ignore (typeof ~subst ~metasenv [] ty);
+      check_relevance ~in_type:true ~subst ~metasenv relevance ty
    | C.Inductive (_, leftno, tyl, _) -> 
        check_mutual_inductive_defs uri ~metasenv ~subst leftno tyl
    | C.Fixpoint (inductive,fl,_) ->