(* General clauses.
   Copyright (C) 2003-2004 Jean Goubault-Larrecq and LSV, CNRS UMR 8643 & ENS Cachan
   and INRIA Futurs projet SECSI.

   This file is part of ispi.

   ispi 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.

   ispi 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 ispi; see the file COPYING.  If not, write to
   the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.
*)

open "gclause_h";

fun print_gclause (f as |[put, ...]|, varname) =
    let val pa = print_atom (f, varname)
	fun pgclause (GCLAUSE (neg, pos)) =
	    let val delimr = ref ""
	    in
		iterate
		  (put (!delimr); delimr := ", "; put "--"; pa a)
		| a in list neg
		end;
		iterate
		  (put (!delimr); delimr := ", "; put "++"; pa a)
		| a in list pos
		end
	    end
    in
	pgclause
    end;

fun print_gclause_pl (f as |[put, ...]|, varname) =
    let val pa = print_atom (f, varname)
	fun p_pos [a] = pa a
	  | p_pos nil = put "%false()"
	  | p_pos pos =
	    let val delimr = ref ""
	    in
		iterate
		  (put (!delimr); delimr := "; ";
		   pa a)
		| a in list pos
		end
	    end
	fun pgclause (GCLAUSE (neg, pos)) =
	    (p_pos pos;
	     (case neg of
		  nil => ()
		| _ => let val delimr = ref " :- "
		       in
			   iterate
			     (put (!delimr); delimr := ", ";
			      pa b)
			   | b in list neg
			   end
		       end);
		  put ".")
    in
	pgclause
    end;