(* pldet main loop.
   Copyright (C) 2003, 2004 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 "plauto_h";
open "determinize_h";
open "yyerror_h";
open "verbose_h";

(*val version = "1.0 - Nov 19, 2003";*)
val version = "1.1 - Mar 24, 2004";

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

datatype method = POWERSET | SIMPLE | SIMPLE_DEBUG;

val methr = ref SIMPLE;

fun usage () =
    (#put stderr "Usage: pldet <flags>* filename.\n\
     \  Version ";
     #put stderr version;
     #put stderr ", Copyright (C) Jean Goubault-Larrecq;\n\
      \     see file COPYRIGHT.\n\
      \  pldet 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\
      \    -v0 runs silently, -v1 (aka., -v) prints new states as they are derived,\n\
      \        -v2 prints more detailed info.\n\
      \    -powerset uses the standard powerset algorithm.\n\
      \    -simple uses the more refined simulation-based algorithm.\n\
      \        Default: -simple.\n";
     #flush stderr ());


local
    val nfa = re_make_nfa [(re_parse "^#q", fn _ => ())]
in
    fun matches_abbrv P =
	case nfa_run (nfa, P) of
	    SOME _ => true
	  | _ => false
end;

fun do_args ["-h"] = usage ()
  | do_args ("-h"::l) = (usage (); do_args l)
  | do_args ("-v0" :: l) = (verbosity := 0; do_args l)
  | do_args ("-v1" :: l) = (verbosity := 1; do_args l)
  | do_args ("-v2" :: l) = (verbosity := 2; do_args l)
  | do_args ("-v" :: l) = (verbosity := 1; do_args l)
  | do_args ("-powerset" :: l) = (methr := POWERSET; do_args l)
  | do_args ("-simple" :: l) = (methr := SIMPLE; 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, plautolex, aplnone (), plauto_value, yyloc, yyerror yyloc)
	 in
	     case plautoparse hyd of
		 SOME (aplauto a0) =>
		 let val AUTO (auto0, univ0) = a0
		     val auto = {P => fmap
				| P => fmap in map auto0
				    such that not (matches_abbrv P)}
		     val univ = {P | P in set univ0
				 such that not (matches_abbrv P)}
		     val a = AUTO (auto, univ)
		     val |[block_incl, ...]| = auto_simple_inclusions a
		     val incl = case !methr of
				    POWERSET => (fn (blk1, blk2) =>
						    blk2 subset blk1)
				  | SIMPLE => block_incl
				  | SIMPLE_DEBUG => (fn (blk1, blk2) =>
							let val res = block_incl (blk1,blk2)
							in
							    #put stderr "Included (";
							    print stderr (pack blk1);
							    #put stderr ", ";
							    print stderr (pack blk2);
							    #put stderr ") : ";
							    print stderr (pack res);
							    #put stderr "\n";
							    #flush stderr ();
							    res
							end)
		     val preds = univ U dom auto
		     val fmodel = determinize (a, incl)
		 in
		     print_fmodel_table (stdout, fmodel, preds,
					 !plauto_defs, block_incl);
		     #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)
		  | PlautoUnterminatedCommentEvt => (#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 ());
