(* Printing functions for justifications of h1 clauses in Seidl form.
   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 "print_seidl_h";

exception PrintSeidl;

fun print_seidl (f as |[put, ...]|, varname) =
    let val pgc = print_gclause_pl (f, varname)
	val pt = print_term (f, varname)
	val pc = print_clause (f, "X")
	memofun pj (AJ_START sc, c) =
		let val (cl, rho, k) = clause_from_seidl sc
		in
		    if empty rho
			then ()
		    else (pgc c; put " [rename-resolve:\n  ";
			  pc cl;
			  let val delimr = ref " {X"
			  in
			      iterate
				(put (!delimr); delimr := ",X";
				 print f (pack k);
				 put "=";
				 put (varname Z))
			      | Z => k in map rho
			      end;
			      put "}"
			  end;
			  put "\n  ]\n")
		end
	      | pj (AJ_NON_HORN jcl, c) =
		(iterate
		   pj jc
		 | jc in list jcl
		 end;
		   pgc c; put " [weaken-pos:\n";
		   iterate
		     (put "  "; pgc c'; put "\n")
		   | (_, c') in list jcl
		   end;
		   put "  ]\n")
	      | pj (AJ_RESOLVE (sc, jcl), c as GCLAUSE (_, [_ $ [_ $ l]])) =
		(iterate
		   pj jc
		 | jc in list jcl
		 end;
		   pgc c; put " [def-resolve-1:\n";
		   let val (c, ...) = clause_from_seidl sc
		   in
		       put "  ";
		       pc c;
		       if null l
			   then ()
		       else let val delimr = ref "{X"
				val ir = ref 0
			    in
				iterate
				  (put (!delimr); delimr := ",X";
				   inc ir;
				   print f (pack (!ir));
				   put "=";
				   pt ti)
				| ti in list l
				end;
				put "}"
			    end;
			    put "\n"
		   end;
		   iterate
		     (put "  "; pgc c'; put "\n")
		   | (_, c') in list jcl
		   end;
		   put "  ]\n")
	      | pj (AJ_CUT (jc1 as (_, c1), jc2 as (_, c2)), c) =
		(pj jc1; pj jc2;
		 pgc c; put " [def-resolve-2:\n  ";
		 pgc c1; put "\n  "; pgc c2;
		 put "  ]\n")
	      | pj (AJ_CUT_2 (jc as (_, c0 as GCLAUSE (neg0, _)), jcl), c) =
		(pj jc;
		 iterate
		   pj jc'
		 | jc' in list jcl
		 end;
		 pgc c; put " [def-resolve-3:\n  ";
		 pgc c0; put "\n";
		 iterate
		   (let val GCLAUSE (_, [Qi $ [V xi]]) = ci
		    in
			pgc ci; put "{"; put (varname xi);
			put "=";
			let val SOME u =
				some
				  u
				| Q $ [u] in list neg0
				  such that Q=Qi
				end
			in
			    pt u; put "}\n"
			end
		    end handle Bind => raise PrintSeidl)
		 | (_, ci) in list jcl
		 end;
		 put "  ]\n")
	      | pj (AJ_FACTOR (x, x', jc as (_, c0)), c) =
		(pj jc;
		 pgc c; put " [factor:\n  ";
		 pgc c0; put "{"; put (varname x'); put "=";
		 put (varname x); put "}\n  ]\n")
	      | pj jc = raise PrintSeidl
    in
	pj
    end;
