-let ppcontext ?(sep = "\n") subst context =
- String.concat sep
- (List.rev_map (function
- | Some (n, Cic.Decl t) ->
- sprintf "%s : %s" (CicPp.ppname n) (ppterm subst t)
- | Some (n, Cic.Def (t, ty)) ->
- sprintf "%s : %s := %s"
- (CicPp.ppname n)
- (match ty with None -> "_" | Some ty -> ppterm subst ty)
- (ppterm subst t)
- | None -> "_")
- context)
+let ppterm_in_context subst term name_context =
+ CicPp.pp (apply_subst subst term) name_context
+
+let ppcontext' ?(sep = "\n") subst context =
+ let separate s = if s = "" then "" else s ^ sep in
+ List.fold_right
+ (fun context_entry (i,name_context) ->
+ match context_entry with
+ Some (n,Cic.Decl t) ->
+ sprintf "%s%s : %s" (separate i) (CicPp.ppname n)
+ (ppterm_in_context subst t name_context), (Some n)::name_context
+ | Some (n,Cic.Def (bo,ty)) ->
+ sprintf "%s%s : %s := %s" (separate i) (CicPp.ppname n)
+ (match ty with
+ None -> "_"
+ | Some ty -> ppterm_in_context subst ty name_context)
+ (ppterm_in_context subst bo name_context), (Some n)::name_context
+ | None ->
+ sprintf "%s_ :? _" (separate i), None::name_context
+ ) context ("",[])
+
+let ppcontext ?sep subst context = fst (ppcontext' ?sep subst context)