(* print natural deduction proof in tree format.
   Copyright (C) 2003 Jean Goubault-Larrecq and LSV, CNRS UMR 8643 & ENS Cachan.

   This file is part of h1.

   h1 is free software; you can redistribute it and/or modify
   it under the terms of the GNU General Public License as published by
   the Free Software Foundation; either version 2, or (at your option)
   any later version.

   h1 is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   GNU General Public License for more details.

   You should have received a copy of the GNU General Public License
   along with h1; see the file COPYING.  If not, write to
   the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.
*)

open "pfcprinttree_h";

fun print_case (fd as |[put, ...]|) =
    let val prt = print fd
    in
	fn i => (prt (pack (i:int));
		 put ".")
    end;

exception PfcPrintTree;

fun pfc_print_tree (f as |[put, ...]|, prompt, pdef, pass) =
    let val pt = print_term (f, identity)
	val pa = print_atom (f, identity)
	val pgc = print_gclause_pl (f, identity)
	fun pspaces 0 = ()
	  | pspaces n = (put " "; pspaces (n-1))
	(*
	fun pstars 0 = ()
	  | pstars n = (put "*"; pstars (n-1))
	 *)
	fun psigma (_, {}) = ()
	  | psigma (n, sigma) =
	    let val delimr = ref "{"
	    in
		put "\n";
		pspaces n;
		iterate
		  (put (!delimr); delimr := ",";
		   put X; put "="; pt t)
		| X => t in map sigma
		end;
		put "}"
	    end
	fun pfc_pr (PFC (PFC_AXIOM "inj", (Xs, c as GCLAUSE (_, pos)), ts, [pfc]),
		    dewey) =
	    let val sigma = {X => t
			    || X in list Xs and t in list ts
				 such that t<>V X}
		    handle ParSweep => raise PfcPrintTree
		val tsub = tsubst sigma
		val pos' = [tsub a | a in list pos]
	    in
		put dewey; put " "; pgc (GCLAUSE (nil, pos'));
		put " by weakening.\n";
		pfc_pr (pfc, dewey ^ "1.")
	    end
	  | pfc_pr (PFC (kind, (Xs, c as GCLAUSE (_, [a])), ts, pfs),
		    dewey) =
	    let val sigma = {X => t
			    || X in list Xs and t in list ts
				 such that t<>V X}
		    handle ParSweep => raise PfcPrintTree
		val fact = tsubst sigma a
	    in
		put dewey; put " "; pa fact;
		case pfs of
		    nil => (case kind of
				PFC_DEF => (put " by "; pdef c; put ".\n")
			      | PFC_INPUT => (put " by "; pass c; put ".\n")
			      | _ => raise PfcPrintTree)
		  | _ => (put ".\n";
			  pspaces (size dewey + 2);
			  (*put dewey; put "1. ";*)
			  put "using ";
			  (case kind of
			       PFC_DEF => pdef c
			     | PFC_INPUT => pass c
			     | _ => raise PfcPrintTree);
			  put " ";
			  pgc c; psigma (size dewey+3, sigma);
			  put "\n";
			  let val ir = ref 0
			      val f as |[put, convert, tell, seek, truncate,
					  ...]|
				  = outstring dewey
			      val n = tell ()
			  in
			      iterate
				(inc ir; seek n; truncate ();
				 print_case f (!ir);
				 pfc_pr (pf, convert ()))
			      | pf in list pfs
			      end
			  end)
	    end
	  | pfc_pr arg = raise PfcPrintTree
    in
	fn pfcl => iterate (put prompt; pfc_pr (pfc, ""))
		   | pfc in list pfcl end
    end;
