-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 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)
-;;