s, t
;;
+let ppterm status t =
+ let uri,height,metasenv,subst,obj = status.pstatus in
+ let _,context,t = t in
+ NCicPp.ppterm ~metasenv ~subst ~context t
+;;
+
let disambiguate status t ty context =
let status, expty =
match ty with
let mk_cic_term c t = None,c,t ;;
+(* CSC: next two functions to be moved elsewhere *)
+let rec apply_subst subst ctx =
+ function
+ NCic.Meta (i,lc) ->
+ (try
+ let _,_,t,_ = NCicUtils.lookup_subst i subst in
+ let t = NCicSubstitution.subst_meta lc t in
+ apply_subst subst ctx t
+ with
+ Not_found ->
+ match lc with
+ _,NCic.Irl _ -> NCic.Meta (i,lc)
+ | n,NCic.Ctx l ->
+ NCic.Meta
+ (i,(0,NCic.Ctx
+ (List.map (fun t ->
+ apply_subst subst ctx (NCicSubstitution.lift n t)) l))))
+ | t -> NCicUtils.map (fun item ctx -> item::ctx) ctx (apply_subst subst) t
+;;
+
+let apply_subst_obj subst =
+ function
+ NCic.Constant (relev,name,bo,ty,attrs) ->
+ NCic.Constant
+ (relev,name,HExtlib.map_option (apply_subst subst []) bo,
+ apply_subst subst [] ty,attrs)
+ | NCic.Fixpoint (ind,fl,attrs) ->
+ let fl =
+ List.map
+ (function (relevance,name,recno,ty,bo) ->
+ relevance,name,recno,apply_subst subst [] ty,apply_subst subst [] bo
+ ) fl
+ in
+ NCic.Fixpoint (ind,fl,attrs)
+ | _ -> assert false (* not implemented yet *)
+;;
+
let apply_subst status ctx t =
let status, (name,_,t) = relocate status ctx t in
let _,_,_,subst,_ = status.pstatus in
- let rec aux ctx =
- function
- NCic.Meta (i,lc) ->
- (try
- let _,_,t,_ = NCicUtils.lookup_subst i subst in
- let t = NCicSubstitution.subst_meta lc t in
- aux ctx t
- with
- Not_found ->
- match lc with
- _,NCic.Irl _ -> NCic.Meta (i,lc)
- | n,NCic.Ctx l ->
- NCic.Meta
- (i,(0,NCic.Ctx
- (List.map (fun t -> aux ctx (NCicSubstitution.lift n t)) l))))
- | t -> NCicUtils.map (fun item ctx -> item::ctx) ctx aux t
- in
- status, (name, ctx, aux ctx t)
+ status, (name, ctx, apply_subst subst ctx t)
;;