(* plpurge main loop.
   Copyright (C) 2005 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 "pl_h";
open "rel_h";
open "yyerror_h";

val version = "1.1 - Jan 22, 2008";
    (* "1.0 - Jan 03, 2005"; *)

val final = ref ({} : string set);

fun infile_or_stdin "-" = stdin
  | infile_or_stdin name =
    let val |[get, getline, ...]| = infile name
    in
	|[get=get, getline=getline]|
    end;

fun usage () =
    (#put stderr "Usage: plpurge <flags>* filename.\n\
     \  Version ";
     #put stderr version;
     #put stderr ", Copyright (C) Jean Goubault-Larrecq;\n\
      \     see file COPYRIGHT.\n\
      \  plpurge comes with ABSOLUTELY NO WARRANTY; see file COPYING, sections 11, 12.\n\
      \  This is free software, and you are welcome to redistribute it\n\
      \  under certain conditions; see TERMS AND CONDITIONS in file COPYING.\n\
      \    Use '-' instead of filename to read from stdin.\n\
      \  Flags are:\n\
      \    -h prints this help.\n\
      \    -final <name>: declare <name> as final state.\n\
      \      Several can be declared.\n";
     #flush stderr ());

fun do_args ("-final"::name::l) =
    (final := !final U {name};
     do_args l)
  | do_args ["-h"] = usage ()
  | do_args ("-h"::l) = (usage (); do_args l)
  | do_args (filename :: l) =
    (if not (null l)
	 then (#put stderr "ignored junk after filename (";
	       #put stderr filename;
	       #put stderr ")\n";
	       #flush stderr ())
     else ();
	 let val f = infile_or_stdin filename
	     val yyd = glex_data (f, fn _ => true)
	     val yyloc = glex_loc yyd
	     val hyd = gyacc_data (yyd, pllex, plnone (), pl_value, yyloc, yyerror yyloc)
	     (*val pgclause = print_gclause (stdout, identity)*)
	 in
	     case plparse hyd of
		 SOME (plclauselist cl) =>
		 let val preds = dom (gclause_list_pred_sig cl)
		     val deps = union_rel {union_rel {{P => {Q}}
						     | P $ _ in list pos and
							Q $ _ in list neg}
					  | GCLAUSE (neg, pos) in list cl}
		     fun invreach acc =
			 let val acc' = union {if P inset deps
						   then ?deps P
					       else {}
					      | P in set acc} U acc
			 in
			     if acc'=acc
				 then acc
			     else invreach acc'
			 end
		     val bots = union {{P
				       | P $ _ in list neg}
				      | GCLAUSE (neg, nil) in list cl}
		     val needed = invreach (!final U bots)
		     val cl' = [c
			       | c as GCLAUSE (neg, pos) in list cl
				   such that
				       all
					 P inset needed
				       | P $ _ in list pos
				       end]
		     val pgpl = print_gclause_pl (stdout, identity)
		 in
		     iterate
		       (pgpl c;
			#put stdout "\n")
		     | c in list cl'
		     end;
		     #flush stdout ();
		     quit 0
		 end
	       | _ =>
		 (#put stderr "Parsing failed: stop.\n"; #flush stderr ();
		  quit 2)
	 end handle IO n => (#put stderr filename;
			     #put stderr ": ";
			     #put stderr (iomsg n);
			     #put stderr "\n";
			     #flush stderr ();
			     quit 2)
		  | PlUnterminatedCommentEvt => (#put stderr "Unterminated comment: stop.\n";
						 #flush stderr ();
						 quit 2))
  | do_args nil = (#put stderr "Missing filename.\n"; usage (); quit 2)
  | do_args _ = (usage ();
		 quit 2)
    ;

fun main () =
    do_args (args ());
