+let cache1 = UriManager.UriHashtbl.create 313;;
+let rec get_height =
+ function u ->
+ try
+ UriManager.UriHashtbl.find cache1 u
+ with
+ Not_found ->
+ let h = ref 0 in
+ let res =
+ match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph u) with
+ Cic.Constant (_,Some bo,ty,params,_)
+ | Cic.Variable (_,Some bo,ty,params,_) ->
+ ignore (height_of_term ~h bo);
+ ignore (height_of_term ~h ty);
+ List.iter (function uri -> h := max !h (get_height uri)) params;
+ 1 + !h
+ | _ -> 0
+ in
+ UriManager.UriHashtbl.add cache1 u res;
+ res
+and height_of_term ?(h=ref 0) t =
+ let rec aux =
+ function
+ Cic.Rel _
+ | Cic.Sort _ -> ()
+ | Cic.Implicit _ -> assert false
+ | Cic.Var (uri,exp_named_subst)
+ | Cic.Const (uri,exp_named_subst)
+ | Cic.MutInd (uri,_,exp_named_subst)
+ | Cic.MutConstruct (uri,_,_,exp_named_subst) ->
+ h := max !h (get_height uri);
+ List.iter (function (_,t) -> aux t) exp_named_subst
+ | Cic.Meta (_,l) -> List.iter (function None -> () | Some t -> aux t) l
+ | Cic.Cast (t1,t2)
+ | Cic.Prod (_,t1,t2)
+ | Cic.Lambda (_,t1,t2) -> aux t1; aux t2
+ | Cic.LetIn (_,s,ty,t) -> aux s; aux ty; aux t
+ | Cic.Appl l -> List.iter aux l
+ | Cic.MutCase (_,_,outty,t,pl) -> aux outty; aux t; List.iter aux pl
+ | Cic.Fix (_, fl) -> List.iter (fun (_, _, ty, bo) -> aux ty; aux bo) fl; incr h
+ | Cic.CoFix (_, fl) -> List.iter (fun (_, ty, bo) -> aux ty; aux bo) fl; incr h
+ in
+ aux t;
+ 1 + !h
+;;
+