+(*** Functions to apply a substitution ***)
+
+let apply_subst_gen ~appl_fun subst term =
+ let rec um_aux =
+ let module C = Cic in
+ let module S = CicSubstitution in
+ function
+ C.Rel _ as t -> t
+ | C.Var _ as t -> t
+ | C.Meta (i, l) ->
+ (try
+ let t = List.assoc i subst in
+ um_aux (S.lift_meta l t)
+ with Not_found -> (* not constrained variable, i.e. free in subst*)
+ let l' =
+ List.map (function None -> None | Some t -> Some (um_aux t)) l
+ in
+ C.Meta (i,l'))
+ | C.Sort _ as t -> t
+ | C.Implicit _ -> assert false
+ | C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty)
+ | C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t)
+ | C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t)
+ | C.LetIn (n,s,t) -> C.LetIn (n, um_aux s, um_aux t)
+ | C.Appl (hd :: tl) -> appl_fun um_aux hd tl
+ | C.Appl _ -> assert false
+ | C.Const (uri,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
+ in
+ C.Const (uri, exp_named_subst')
+ | C.MutInd (uri,typeno,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
+ in
+ C.MutInd (uri,typeno,exp_named_subst')
+ | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
+ in
+ C.MutConstruct (uri,typeno,consno,exp_named_subst')
+ | C.MutCase (sp,i,outty,t,pl) ->
+ let pl' = List.map um_aux pl in
+ C.MutCase (sp, i, um_aux outty, um_aux t, pl')
+ | C.Fix (i, fl) ->
+ let fl' =
+ List.map (fun (name, i, ty, bo) -> (name, i, um_aux ty, um_aux bo)) fl
+ in
+ C.Fix (i, fl')
+ | C.CoFix (i, fl) ->
+ let fl' =
+ List.map (fun (name, ty, bo) -> (name, um_aux ty, um_aux bo)) fl
+ in
+ C.CoFix (i, fl')
+ in
+ um_aux term
+;;
+
+let apply_subst =
+ let appl_fun um_aux he tl =
+ let tl' = List.map um_aux tl in
+ begin
+ match um_aux he with
+ Cic.Appl l -> Cic.Appl (l@tl')
+ | he' -> Cic.Appl (he'::tl')
+ end
+ in
+ apply_subst_gen ~appl_fun
+;;
+
+(* apply_subst_reducing subst (Some (mtr,reductions_no)) t *)
+(* performs as (apply_subst subst t) until it finds an application of *)
+(* (META [meta_to_reduce]) that, once unwinding is performed, creates *)
+(* a new beta-redex; in this case up to [reductions_no] consecutive *)
+(* beta-reductions are performed. *)
+(* Hint: this function is usually called when [reductions_no] *)
+(* eta-expansions have been performed and the head of the new *)
+(* application has been unified with (META [meta_to_reduce]): *)
+(* during the unwinding the eta-expansions are undone. *)
+
+let apply_subst_reducing meta_to_reduce =
+ let appl_fun um_aux he tl =
+ let tl' = List.map um_aux tl in
+ let t' =
+ match um_aux he with
+ Cic.Appl l -> Cic.Appl (l@tl')
+ | he' -> Cic.Appl (he'::tl')
+ in
+ begin
+ match meta_to_reduce, he with
+ Some (mtr,reductions_no), Cic.Meta (m,_) when m = mtr ->
+ let rec beta_reduce =
+ function
+ (n,(Cic.Appl (Cic.Lambda (_,_,t)::he'::tl'))) when n > 0 ->
+ let he'' = CicSubstitution.subst he' t in
+ if tl' = [] then
+ he''
+ else
+ beta_reduce (n-1,Cic.Appl(he''::tl'))
+ | (_,t) -> t
+ in
+ beta_reduce (reductions_no,t')
+ | _,_ -> t'
+ end
+ in
+ apply_subst_gen ~appl_fun
+
+let rec apply_subst_context subst context =
+ List.fold_right
+ (fun item context ->
+ match item with
+ | Some (n, Cic.Decl t) ->
+ let t' = apply_subst subst t in
+ Some (n, Cic.Decl t') :: context
+ | Some (n, Cic.Def (t, ty)) ->
+ let ty' =
+ match ty with
+ | None -> None
+ | Some ty -> Some (apply_subst subst ty)
+ in
+ let t' = apply_subst subst t in
+ Some (n, Cic.Def (t', ty')) :: context
+ | None -> None :: context)
+ context []
+
+let apply_subst_metasenv subst metasenv =
+ List.map
+ (fun (n, context, ty) ->
+ (n, apply_subst_context subst context, apply_subst subst ty))
+ (List.filter
+ (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) subst))
+ metasenv)
+
+(***** Pretty printing functions ******)
+