-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 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 height_of_obj_kind uri ~subst =
+ function
+ NCic.Inductive _
+ | NCic.Constant (_,_,None,_,_)
+ | NCic.Fixpoint (false,_,_) -> 0
+ | NCic.Fixpoint (true,ifl,_) ->
+ let iflno = List.length ifl in
+ height_of_term
+ (List.fold_left
+ (fun l (_,_,_,ty,bo) ->
+ let bo = debruijn uri iflno [] ~subst bo in
+ ty::bo::l
+ ) [] ifl)
+ | NCic.Constant (_,_,Some bo,ty,_) -> height_of_term [bo;ty]
+;;