(* print natural deduction proof in log 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 "pfcprint_h";

exception PfcPrint;

fun pfc_print (f as |[put, ...]|) =
    let val pt = print_term (f, identity)
	val pa = print_atom (f, identity)
	val pgc = print_gclause_pl (f, identity)
	fun psigma {} = ()
	  | psigma sigma =
	    let val delimr = ref "{"
	    in
		iterate
		  (put (!delimr); delimr := ",";
		   put X; put "="; pt t)
		| X => t in map sigma
		end;
		put "}"
	    end
	memofun pfc_pr (PFC (PFC_AXIOM "inj", (Xs, c as GCLAUSE (_, pos)), ts, [pf])) =
		let val premise = pfc_pr pf
		    val sigma = {X => t
				|| X in list Xs and t in list ts
				   such that t<>V X}
			handle ParSweep => raise PfcPrint
		    val tsub = tsubst sigma
		    val pos' = [tsub a | a in list pos]
		in
		    pgc (GCLAUSE (nil, pos'));
		    put " [factor:\n  ";
		    pa premise;
		    put ". ]\n";
		    "or" $ pos' (* dummy term *)
		end
	      | pfc_pr (PFC (kind, (Xs, c as GCLAUSE (_, [a])), ts, pfs)) =
		let val premises = [pfc_pr pf
				   | pf in list pfs]
		    val sigma = {X => t
				|| X in list Xs and t in list ts
				   such that t<>V X}
			handle ParSweep => raise PfcPrint
		    val fact = tsubst sigma a
		in
		    if null pfs
			then fact
		    else (pa fact;
			  put ". [unit-resolve:\n    ";
			  pgc c; psigma sigma; put "\n    ";
			  iterate
			    (put " "; pa prem; put ".")
			  | prem in list premises
			  end;
			  put " ]\n";
			  fact)
		end
	  | pfc_pr arg = raise PfcPrint
    in
	fn pfcl => iterate pfc_pr pfc | pfc in list pfcl end
    end;
