module TextualPp =
 struct
  (* It also returns the pretty-printing context! *)
  let print_context ctx =
    let print_name =
     function
        Cic.Name n -> n
      | Cic.Anonimous -> "_"
    in
     List.fold_right
      (fun i (output,context) ->
        let (newoutput,context') =
         match i with
            Some (n,Cic.Decl t) ->
              print_name n ^ ":" ^ CicPp.pp t context ^ "\n", (Some n)::context
          | Some (n,Cic.Def t) ->
              print_name n ^ ":=" ^ CicPp.pp t context ^ "\n", (Some n)::context
          | None ->
              "_ ?= _\n", None::context
        in
         output^newoutput,context'
      ) ctx ("",[])
  ;;

  exception NotImplemented;;

  let print_sequent (metano,context,goal) =
   let module P = ProofEngine in
    "\n" ^
     let (output,pretty_printer_context_of_context) = print_context context in
      output ^
       "---------------------- ?" ^ string_of_int metano ^ "\n" ^
        CicPp.pp goal pretty_printer_context_of_context
  ;;
 end
;;

module XmlPp =
 struct
  let print_sequent metasenv (metano,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_context =
      Cic2acic.acic_of_cic_context' seed ids_to_terms ids_to_father_ids
       ids_to_inner_sorts ids_to_inner_types metasenv
     in
      let final_s,_ =
       (List.fold_right
         (fun binding (s,context) ->
           match binding with
              (Some (n,(Cic.Def t as b)) as entry)
            | (Some (n,(Cic.Decl t as b)) as entry) ->
               let acic = acic_of_cic_context context t in
                [< s ;
                   X.xml_nempty
                    (match b with Cic.Decl _ -> "Decl" | Cic.Def _ -> "Def")
                    ["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)
                >], (entry::context)
            | None ->
               [< s ; X.xml_empty "Hidden" [] >], (None::context)
         ) context ([<>],[])
       )
      in
       let acic = acic_of_cic_context context goal in
        X.xml_nempty "Sequent" ["no",string_of_int metano]
         [< 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
;;