+let height_of_ref (NReference.Ref (uri, x)) =
+ match x with
+ | NReference.Decl
+ | NReference.Ind _
+ | NReference.Con _
+ | NReference.CoFix _ ->
+ let _,height,_,_,_ = NCicEnvironment.get_checked_obj uri in
+ height
+ | NReference.Def h -> h
+ | NReference.Fix (_,_,h) -> h
+;;
+
+let fast_height_of_term t =
+ let h = ref 0 in
+ let rec aux =
+ function
+ NCic.Meta (_,(_,NCic.Ctx l)) -> List.iter aux l
+ | NCic.Meta _ -> ()
+ | NCic.Rel _
+ | NCic.Sort _ -> ()
+ | NCic.Implicit _ -> assert false
+ | NCic.Const nref as t ->
+(*
+ prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[]
+ ~context:[] t ^ ":" ^ string_of_int (height_of_ref nref));
+*)
+ h := max !h (height_of_ref nref)
+ | NCic.Prod (_,t1,t2)
+ | NCic.Lambda (_,t1,t2) -> aux t1; aux t2
+ | NCic.LetIn (_,s,ty,t) -> aux s; aux ty; aux t
+ | NCic.Appl l -> List.iter aux l
+ | NCic.Match (_,outty,t,pl) -> aux outty; aux t; List.iter aux pl
+ in
+ aux t; !h
+;;
+
+let height_of_goals status =
+ let open_goals = head_goals status#stack in
+ assert (List.length open_goals > 0);
+ let h = ref 1 in
+ List.iter
+ (fun open_goal ->
+ let ty = get_goalty status open_goal in
+ let context = ctx_of ty in
+ let _, ty = term_of_cic_term status ty (ctx_of ty) in
+ h := max !h (fast_height_of_term ty);
+ List.iter
+ (function
+ | _, NCic.Decl ty -> h := max !h (fast_height_of_term ty)
+ | _, NCic.Def (bo,ty) ->
+ h := max !h (fast_height_of_term ty);
+ h := max !h (fast_height_of_term bo);
+ )
+ context)
+ open_goals;
+ prerr_endline ("altezza sequente: " ^ string_of_int !h);
+ !h
+;;
+