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 metasenv (context,goal) =
   let module X = Xml in
    let ids_to_terms = Hashtbl.create 503 in
    let ids_to_father_ids = Hashtbl.create 503 in
    let ids_to_inner_sorts = Hashtbl.create 503 in
    let ids_to_inner_types = Hashtbl.create 503 in
    let seed = ref 0 in
     let acic_of_cic_env =
      Cic2acic.acic_of_cic_env' seed ids_to_terms ids_to_father_ids
       ids_to_inner_sorts ids_to_inner_types metasenv
     in
      let final_s,final_env =
       (List.fold_right
         (fun binding (s,env) ->
           let b,n,t,cicbinding =
            match binding with
               ProofEngine.Definition  (n,t) -> "Def", n, t,Cic.Def t
             | ProofEngine.Declaration (n,t) -> "Decl", n, t, Cic.Decl t
           in
            let acic = acic_of_cic_env env t in
             [< s ;
                X.xml_nempty b
                 ["name",(match n with Cic.Name n -> n | _ -> assert false)]
                 (Cic2Xml.print_term
                   (UriManager.uri_of_string "cic:/dummy.con")
                   ids_to_inner_sorts acic)
             >],((n,cicbinding)::env)
         ) context ([<>],[])
       )
      in
       let acic = acic_of_cic_env final_env goal in
        X.xml_nempty "Sequent" []
         [< final_s ;
            Xml.xml_nempty "Goal" []
             (Cic2Xml.print_term (UriManager.uri_of_string "cic:/dummy.con")
               ids_to_inner_sorts acic)
         >],
         ids_to_terms,ids_to_father_ids
  ;;
 end
;;