incomplete irrelevance test commented out

[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 598ed2a67c5b857072506292391d9594f461a01f..de633357c9b1692a2964e74e824dba2b7efcc683 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -1082,13 +1082,15 @@ let typecheck_subst ~metasenv subst =
     ) [] subst)
 ;;
 
-let check_rel1_irrelevant ~metasenv ~subst context =
+let check_rel1_irrelevant ~metasenv ~subst context = fun _ -> ()
+(*
   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
+    | 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)))))
+           (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
@@ -1110,38 +1112,68 @@ let check_rel1_irrelevant ~metasenv ~subst context =
     | t -> U.fold shift k aux () t
   in 
     aux (1, context) ()
+*)
 
-let check_relevance ~metasenv ~subst ~in_type relevance = 
+let check_relevance ~metasenv ~subst ~in_type relevance = fun _ -> ()
+(*
   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"))
+  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
-     aux (in_type, [], relevance) ()
+    aux2 (in_type, [], relevance)
+*)
 ;;
 
 let typecheck_obj (uri,_height,metasenv,subst,kind) =