(* ISpi translator from programs to clause sets.
   Copyright (C) 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 "lean_h";
open "spi_h";
open "yyerror_h";

val version = "1.0 - Apr 04, 2004";

exception QuitEvt of int;

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: ispi <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";
     #flush stderr ());

fun 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 = hlex_data (f, fn _ => true)
	     val yyloc = hlex_loc yyd
	     val hyd = hyacc_data (yyd, spilex, spinone (), spi_value, yyloc, yyerror yyloc)
	 in
	     (*hyacc_set_debug (hyd, true);*)
	     case spiparse hyd of
		 SOME (spi prog) =>
		 let val (subprocs, cs) = lean_semantics prog
		     val pgclause = print_gclause (stdout, identity)
		 in
		     #put stdout "% Clauses ";
		     if filename="-"
			 then ()
		     else (#put stdout "for the ISpi program ";
			   #put stdout filename;
			   #put stdout ", ");
		     #put stdout "automatically generated by ispi.\n\n";
		     iterate
		       (#put stdout "input_clause(";
			#put stdout name;
			#put stdout ",axiom,\n  [";
			pgclause c;
			#put stdout "]).\n")
		     | (name, c) in list cs
		     end;
		     #flush stdout ()
		 end
	       | _ =>
		 (#put stderr "Parsing failed: stop.\n"; #flush stderr ();
		  raise QuitEvt 2)
	 end handle IO n => (#put stderr filename;
			     #put stderr ": ";
			     #put stderr (iomsg n);
			     #put stderr "\n";
			     #flush stderr ();
			     raise QuitEvt 2)
		  | SpiUnterminatedCommentEvt => (#put stderr "Unterminated comment: stop.\n";
						  #flush stderr ();
						  raise QuitEvt 2))
  | do_args nil = (#put stderr "Missing filename.\n"; usage (); raise QuitEvt 2)
  | do_args _ = (usage ();
		 raise QuitEvt 2)
    ;

fun main () =
    do_args (args ()) handle QuitEvt n => quit n;