+let rec ppcontext ~formatter ?(sep="\n") ~subst ~metasenv = function
+ | [] -> ()
+ | (name, NCic.Decl t) :: tl ->
+ ppcontext ~formatter ~sep ~subst ~metasenv tl;
+ F.fprintf formatter "%s: " name;
+ ppterm ~formatter ~subst ~metasenv ~context:tl t;
+ F.fprintf formatter "%s" sep
+ | (name, NCic.Def (bo,ty)) :: tl->
+ ppcontext ~formatter ~sep ~subst ~metasenv tl;
+ F.fprintf formatter "%s: " name;
+ ppterm ~formatter ~subst ~metasenv ~context:tl ty;
+ F.fprintf formatter " := ";
+ ppterm ~formatter ~subst ~metasenv ~context:tl bo;
+ F.fprintf formatter "%s" sep
+;;
+
+let rec ppmetasenv ~formatter ~subst metasenv = function
+ | [] -> ()
+ | (i,(name, ctx, ty)) :: tl ->
+ F.fprintf formatter "@[<hov 2>";
+ let name = match name with Some n -> "("^n^")" | _ -> "" in
+ ppcontext ~formatter ~sep:"; " ~subst ~metasenv ctx;
+ F.fprintf formatter "@;⊢@;?%d%s :@;" i name;
+ ppterm ~formatter ~metasenv ~subst ~context:ctx ty;
+ F.fprintf formatter "@]@\n";
+ ppmetasenv ~formatter ~subst metasenv tl
+;;
+
+let ppmetasenv ~formatter ~subst metasenv =
+ ppmetasenv ~formatter ~subst metasenv metasenv
+;;
+
+let rec ppsubst ~formatter ~subst ~metasenv = function
+ | [] -> ()
+ | (i,(name, ctx, t, ty)) :: tl ->
+ let name = match name with Some n -> "("^n^")" | _ -> "" in
+ ppcontext ~formatter ~sep:"; " ~subst ~metasenv ctx;
+ F.fprintf formatter " ⊢ ?%d%s := " i name;
+ ppterm ~formatter ~metasenv ~subst ~context:ctx t;
+ F.fprintf formatter " : ";
+ ppterm ~formatter ~metasenv ~subst ~context:ctx ty;
+ F.fprintf formatter "\n";
+ ppsubst ~formatter ~subst ~metasenv tl
+;;
+
+let ppsubst ~formatter ~metasenv subst =
+ ppsubst ~formatter ~metasenv ~subst subst
+;;
+
+let ppobj ~formatter (u,_,metasenv, subst, o) =
+ F.fprintf formatter "metasenv:\n";
+ ppmetasenv ~formatter ~subst metasenv;
+ F.fprintf formatter "\n";
+ F.fprintf formatter "subst:\n";
+ (*ppsubst subst ~formatter ~metasenv;*) F.fprintf formatter "...";
+ F.fprintf formatter "\n";
+ match o with
+ | NCic.Fixpoint (b, fl, _) ->
+ F.fprintf formatter "{%s}@\n@[<hov 0>" (NUri.string_of_uri u);
+ F.fprintf formatter "@[<hov 2>%s"(if b then "let rec " else "let corec ");
+ HExtlib.list_iter_sep
+ ~sep:(fun () -> F.fprintf formatter "@\n@[<hov 2>and ")
+ (fun (_,name,n,ty,bo) ->
+ F.fprintf formatter "%s on %d :@;" name n;
+ ppterm ~formatter ~metasenv ~subst ~context:[] ty;
+ F.fprintf formatter "@]@;@[<hov 2>:=@;";
+ ppterm ~formatter ~metasenv ~subst ~context:[] ~inside_fix:true bo;
+ F.fprintf formatter "@]") fl;
+ F.fprintf formatter "@]"
+ | NCic.Inductive (b, leftno,tyl, _) ->
+ F.fprintf formatter "{%s} with %d fixed params@\n@[<hov 0>@[<hov 2>%s"
+ (NUri.string_of_uri u) leftno
+ (if b then "inductive " else "coinductive ");
+ HExtlib.list_iter_sep
+ ~sep:(fun () -> F.fprintf formatter "@\n@[<hov 2>and ")
+ (fun (_,name,ty,cl) ->
+ F.fprintf formatter "%s:@;" name;
+ ppterm ~formatter ~metasenv ~subst ~context:[] ty;
+ F.fprintf formatter "@]@;@[<hov 3>:=@;";
+ HExtlib.list_iter_sep ~sep:(fun () -> F.fprintf formatter "@;")
+ (fun (_,name,ty) ->
+ F.fprintf formatter "| %s: " name;
+ ppterm ~formatter ~metasenv ~subst ~context:[] ty;)
+ cl;
+ F.fprintf formatter "@]"
+ ) tyl ;
+ F.fprintf formatter "@]"
+ | NCic.Constant (_,name,None,ty, _) ->
+ F.fprintf formatter "{%s}@\n@[<hov 2>axiom %s :@;" (NUri.string_of_uri u) name;
+ ppterm ~formatter ~metasenv ~subst ~context:[] ty;
+ F.fprintf formatter "@]@\n"
+ | NCic.Constant (_,name,Some bo,ty, _) ->
+ F.fprintf formatter "{%s}@\n@[<hov 0>@[<hov 2>definition %s :@;" (NUri.string_of_uri u) name;
+ ppterm ~formatter ~metasenv ~subst ~context:[] ty;
+ F.fprintf formatter "@]@;@[<hov 2>:=@;";
+ ppterm ~formatter ~metasenv ~subst ~context:[] bo;
+ F.fprintf formatter "@]@\n@]"
+;;
+
+let ppterm ~context ~subst ~metasenv ?margin ?inside_fix t =
+ on_buffer (ppterm ~context ~subst ~metasenv ?margin ?inside_fix) t
+;;
+
+let ppcontext ?sep ~subst ~metasenv ctx =
+ on_buffer (ppcontext ?sep ~subst ~metasenv) ctx
+;;
+
+let ppmetasenv ~subst metasenv = on_buffer (ppmetasenv ~subst) metasenv;;
+
+let ppsubst ~metasenv subst = on_buffer (ppsubst ~metasenv) subst;;