let t = NCicSubstitution.subst_meta lc t in
apply_subst subst () t
with
- Not_found ->
+ NCicUtils.Subst_not_found j when j = i ->
match lc with
_,NCic.Irl _ -> NCic.Meta (i,lc)
| n,NCic.Ctx l ->
(i,(name,apply_subst_context subst ctx,apply_subst subst ctx ty)) ::
apply_subst_metasenv subst tl
;;
-
-let height_of_term tl =
- let h = ref 0 in
- let get_height (NReference.Ref (uri,_)) =
- let _,height,_,_,_ = NCicEnvironment.get_checked_obj uri in
- height 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 -> h := max !h (get_height 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
- List.iter aux tl;
- 1 + !h
-;;
-
-let height_of_obj_kind uri =
- 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 = NCicTypeChecker.debruijn uri iflno [] bo in
- ty::bo::l
- ) [] ifl)
- | NCic.Constant (_,_,Some bo,ty,_) -> height_of_term [bo;ty]
-;;