-let apply_subst status ctx t =
- let status, (name,_,t) = relocate status ctx t in
- let _,_,_,subst,_ = status.pstatus in
- status, (name, ctx, apply_subst subst ctx t)
+let path_string_of (ctx,t) =
+ let len_ctx = List.length ctx in
+ let rec aux arity = function
+ | NCic.Appl ((NCic.Meta _|NCic.Implicit _)::_) -> [Variable]
+ | NCic.Appl (NCic.Lambda _ :: _) -> [Variable] (* maybe we should b-reduce *)
+ | NCic.Appl [] -> assert false
+ | NCic.Appl (hd::tl) ->
+ aux (List.length tl) hd @ List.flatten (List.map (aux 0) tl)
+ | NCic.Lambda _ | NCic.Prod _ -> [Variable]
+ (* I think we should CicSubstitution.subst Implicit t *)
+ | NCic.LetIn _ -> [Variable] (* z-reduce? *)
+ | NCic.Meta _ | NCic.Implicit _ -> assert (arity = 0); [Variable]
+ | NCic.Rel i -> [Bound (len_ctx - i, arity)]
+ | NCic.Sort (NCic.Prop) -> assert (arity=0); [Proposition]
+ | NCic.Sort _ -> assert (arity=0); [Datatype]
+ | NCic.Const (NReference.Ref (u,_)) -> [Constant (u, arity)]
+ | NCic.Match _ -> [Dead]
+ in
+ aux 0 t