(*
    ||M||  This file is part of HELM, an Hypertextual, Electronic        
    ||A||  Library of Mathematics, developed at the Computer Science     
    ||T||  Department, University of Bologna, Italy.                     
    ||I||                                                                
    ||T||  HELM is free software; you can redistribute it and/or         
    ||A||  modify it under the terms of the GNU General Public License   
    \   /  version 2 or (at your option) any later version.      
     \ /   This software is distributed as is, NO WARRANTY.     
      V_______________________________________________________________ *)

(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)

module Pp (B : Terms.Blob) = struct

(* Main pretty printing functions *)

let pp_foterm ~formatter:f t =
  let rec aux ?(toplevel=false) = function
    | Terms.Leaf x ->
	Format.fprintf f "%s" (B.pp x)
    | Terms.Var i ->
	Format.fprintf f "?%d" i
    | Terms.Node (hd::tl) ->
	Format.fprintf f "@[<hov 2>";
	if not toplevel then Format.fprintf f "(";
	aux hd;
	List.iter (fun x -> Format.fprintf f "@;";
		     aux x) tl;
	if not toplevel then Format.fprintf f ")";
	Format.fprintf f "@]"
    | _ ->
	assert false
  in
    aux ~toplevel:true t
;;

let string_of_rule = function
  | Terms.SuperpositionRight -> "SupR"
  | Terms.SuperpositionLeft -> "SupL"
  | Terms.Demodulation -> "Demod"
;;

let string_of_direction = function
    | Terms.Left2Right -> "Left to right"
    | Terms.Right2Left -> "Right to left"
    | Terms.Nodir -> "No direction"
;;

let pp_substitution ~formatter:f subst =
     (List.iter
       (fun (i, t) ->
          (Format.fprintf f "?%d -> " i;
	   pp_foterm f t)
       )
       subst)
;;

let pp_proof bag ~formatter:f p =
  let rec aux eq = function
    | Terms.Exact t -> 
        Format.fprintf f "%d: Exact (" eq;
        pp_foterm f t;
        Format.fprintf f ")@;";
    | Terms.Step (rule,eq1,eq2,dir,pos,subst) ->
        Format.fprintf f "%d: %s("
          eq (string_of_rule rule);
	Format.fprintf f "|%d with %d dir %s))" eq1 eq2
	  (string_of_direction dir);
	let (_, _, _, proof1) = Terms.M.find eq1 bag in
	let (_, _, _, proof2) = Terms.M.find eq2 bag in
	  Format.fprintf f "@[<v 2>";
          aux eq1 proof1;	    
          aux eq2 proof2;
	  Format.fprintf f "@]";
  in
    Format.fprintf f "@[<v>";
    aux 0 p;
    Format.fprintf f "@]"
;;

let string_of_comparison = function
  | Terms.Lt -> "<"
  | Terms.Gt -> ">"
  | Terms.Eq -> "="
  | Terms.Incomparable -> "I"

let pp_unit_clause ~formatter:f c =
  let (id, l, vars, proof) = c in
    Format.fprintf f "Id : %d, " id ;
    match l with
      | Terms.Predicate t ->
	  pp_foterm f t
      | Terms.Equation (lhs, rhs, ty, comp) ->
	  Format.fprintf f "{";
	  pp_foterm f ty;
	  Format.fprintf f "}: ";
	  pp_foterm f lhs;
	  Format.fprintf f " =(%s) " (string_of_comparison comp);
	  pp_foterm f rhs;
	  Format.fprintf f " [%s] by %s"
            (String.concat ", " (List.map string_of_int vars))
            (match proof with
            | Terms.Exact _ -> "axiom"
            | Terms.Step (Terms.SuperpositionRight, id1, id2, _, p, _) -> 
                 Printf.sprintf "supR %d with %d at %s" id1 id2 (String.concat
                 "," (List.map string_of_int p))
            | _ -> assert false)

;;

(* String buffer implementation *)
let on_buffer f t = 
  let buff = Buffer.create 100 in
  let formatter = Format.formatter_of_buffer buff in
  f ~formatter:formatter t;
  Format.fprintf formatter "@?";
  Buffer.contents buff
;;

let pp_foterm =
 on_buffer pp_foterm
;;

let pp_substitution =
  on_buffer pp_substitution
;;

let pp_proof bag =
  on_buffer (pp_proof bag)
;;

let pp_unit_clause =
  on_buffer pp_unit_clause
;;

end