(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
(*              Rocquencourt         Orsay          Lyon                    *)
(*                                                                          *)
(*                                 Coq V6.2                                 *)
(*                               May 1st 1998                               *)
(*                                                                          *)
(****************************************************************************)
(*                             top_printers.ml                              *)
(****************************************************************************)

open Std;;
open System;;
open More_util;;
open Pp;;

open CoqAst;;
open Ast;;
open Clexer;;
open Egrammar;;
open Initial;;
open Names;;
open Impuniv;;
open Generic;;
open Term;;
open Sosub;;
open Constrtypes;;
open Proof_trees;;
open Summary;;
open Libobject;;
open Library;;
open Environ;;
open Termenv;;
open Termast;;
open Printer;;
open Closure;;
open Reduction;;
open Typing;;
open Multcase;;
open Multcase_astterm;;
open Astterm;;
open Extraction;;
open Mach;;
open States;;
open Dischcore;;
open Variables;;
open Constants;;
open Indtypes;;
open Discharge;;
open Trad;;
open Command;;
open Pretty;;
open Refiner;;
open Tacmach;;
open Pfedit;;
open Clenv;;
open Tactics;;
open Tacticals;;
open Elim;;
open Auto;;
open Tacinterp;;
open Tacentries;;
open Vernacinterp;;
open Vernacentries;;
open Vernac;;
open Coqtoplevel;;
open Mltop;;

open Esyntax;;
open Metasyntax;;


let pP s = pP (hOV 0 s);;

let prast c = pP(print_ast c);;

let prastpat c = pP(print_astpat c);;
let prastpatl c = pP(print_astlpat c);;
let ppterm0 = (fun x -> pP(term0 (gLOB nil_sign) x));;

let prid id = pP [< 'sTR"#" ; 'sTR(string_of_id id) >];;

let prconst (sp,j) =
    pP [< 'sTR"#" ; 'sTR(string_of_path sp) ; 'sTR"=" ; term0 (gLOB nil_sign) j.vAL >];;

let prvar ((id,a)) =
    pP [< 'sTR"#" ; 'sTR(string_of_id id) ; 'sTR":" ; term0 (gLOB nil_sign) a >];;

let genprj f j = [< (f (gLOB nil_sign)j.vAL); 
                 'sTR " : ";
               (f (gLOB nil_sign)j.tYP);
                  'sTR " : ";
               (f  (gLOB nil_sign)j.kIND)>];;

let prj j = pP (genprj term0 j);;

let prinfo i =pP  (match i with
                        Logic  -> [<>]
                    |  (Inf j) -> (genprj fterm0 j))
;;

let prsp sp = pP[< 'sTR(string_of_path sp) >];;

let prgoal g = pP(prgl g);;

let prsigmagoal g = pP(prgl (sig_it g));;

let prgls gls = pP(pr_gls gls);;

let prglls glls = pP(pr_glls glls);;

let prctxt ctxt = pP(pr_ctxt ctxt);;

let pproof p = pP(print_proof (Evd.mt_evd()) nil_sign p);;

let prevd evd = pP(pr_decls evd);;

let prevc evc = pP(pr_evc evc);;

let prwc wc = pP(pr_evc wc);;

let prclenv clenv = pP(pr_clenv clenv);;

let pr_constobj cobj = pP(print_constant_object 0 cobj);;

let p_uni u = 
    [< 'sTR(string_of_path u.u_sp) ;
       'sTR "." ;
      'iNT u.u_num >]
;;
let print_uni u = (pP (p_uni u));;

let p_arc = function
    Undef -> [< 'sTR"<undef>">]
  | Arc(u,r) ->
    let rec collrec (ge,gt,equiv) = function
        Terminal -> (ge,gt,equiv)
      | Impuniv.Equiv v -> (ge,gt,v::equiv)
      | Impuniv.Greater(true,v,r) -> collrec (ge,v::gt,equiv) r
      | Impuniv.Greater(false,v,r) -> collrec (v::ge,gt,equiv) r in
    let (ge,gt,equiv) = collrec ([],[],[]) r
    in [< p_uni u ; 'sPC ;
        'sTR"GE: "; 'sTR"["; prlist_with_sep pr_spc p_uni ge; 'sTR"]"; 'sPC ;
        'sTR"GT: "; 'sTR"["; prlist_with_sep pr_spc p_uni gt; 'sTR"]"; 'sPC ;
        'sTR"EQ: "; 'sTR"["; prlist_with_sep pr_spc p_uni equiv; 'sTR"]" >]
;;

let print_arc a = pP [< p_arc a ; 'fNL >];;

let print_universes u =
let am = Avm.create uni_ord in
let am' = Avm.unfreeze u am in
let graph = Avm.toList am'
in prlist_with_sep pr_fnl (function (_,Arc(u,r)) -> p_arc(Arc(u,r))
                             | (_,Undef) -> anomaly "UNI")
     graph
;;

let pp_universes u = pP [< 'sTR"[" ; print_universes u ; 'sTR"]" >];;

let pp_libobj obj =
    try let cobj = outConstant obj
        in pP(print_constant_object 0 cobj)
    with Failure _ -> pP [< 'sTR"#<libobj: " ; 'sTR(object_tag obj) ; 'sTR">" >];;

(* $Id: top_printers.ml,v 1.8 1998/06/30 22:36:14 herbelin Exp $ *)
