module TextualPp =
 struct
  (* It also returns the pretty-printing context! *)
  let print_context ctx =
   let module P = ProofEngine in
    let print_name =
     function
        Cic.Name n -> n
      | Cic.Anonimous -> "_"
    in
     List.fold_right
      (fun i env ->
        match i with
           (P.Declaration,n,t) ->
             print_endline (print_name n ^ ":" ^ CicPp.pp t env) ;
             flush stdout ;
             n::env
         | (P.Definition,n,t) ->
             print_endline (print_name n ^ ":=" ^ CicPp.pp t env) ;
             flush stdout ;
             n::env
      ) ctx []
  ;;

  exception NotImplemented;;

  let print_sequent (context,goal) =
   let module P = ProofEngine in
    print_newline () ;
    let pretty_printer_env_of_context =
     print_context context
    in
    print_endline "----------------------" ;
    print_endline (CicPp.pp goal pretty_printer_env_of_context) ; flush stdout
  ;;
 end
;;

module XmlPp =
 struct
  let print_sequent (context,goal) =
   let module X = Xml in
    X.xml_nempty "Sequent" []
     (let final_s,final_env =
       (List.fold_right
         (fun (b,n,t) (s,env) ->
           [< s ;
              X.xml_nempty
               (match b with
                   ProofEngine.Definition  -> "Definition"
                 | ProofEngine.Declaration -> "Declaration"
               ) ["name",(match n with Cic.Name n -> n | _ -> assert false)]
               (Cic2Xml.print_term
                 (UriManager.uri_of_string "cic:/dummy.con")
                 (let (acic,_,_) = Cic2acic.acic_of_cic_env env t in acic)) ;
           >],(n::env)
         ) context ([<>],[])
       )
      in
       [< final_s ;
          Xml.xml_nempty "Goal" []
           (Cic2Xml.print_term (UriManager.uri_of_string "cic:/dummy.con")
             (let (acic,_,_) = Cic2acic.acic_of_cic_env final_env goal in acic))
       >]
     )
  ;;
 end
;;