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 final_s,final_env =
     (List.fold_right
       (fun (b,n,t) (s,env) ->
         let (acic,_,_,ids_to_inner_sorts,_) =
          Cic2acic.acic_of_cic_env metasenv env t
         in
          [< s ;
             X.xml_nempty
              (match b with
                  ProofEngine.Definition  -> "Def"
                | ProofEngine.Declaration -> "Decl"
              ) ["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,t)::env) (* CSC: sbagliato!!! Giusto solo se Declaration! *)
       ) context ([<>],[])
     )
    in
     let (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,_) =
      Cic2acic.acic_of_cic_env metasenv 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
;;