(* pl2tptp main loop.
   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 "pl_h";
open "gensym_h";
open "yyerror_h";

val version = "1.1 - Jan 22, 2008";
    (* "1.0 - Jul 10, 2003"; *)

val clause_name_prefix = ref "clause";
val clause_status = ref "conjecture";

val tptp_version = ref "3.3.0"; (* default *)

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: pl2tptp <flags>* filename.\n\
     \  Version ";
     #put stderr version;
     #put stderr ", Copyright (C) Jean Goubault-Larrecq;\n\
      \     see file COPYRIGHT.\n\
      \  pl2tptp 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\
      \    -prefix <name>: uses <name> as prefix to generate names of clauses\n\
      \                    (default: 'clause').\n\
      \    -status <name>: uses <name> as second argument of 'input_clause'/'cnf'\n\
      \                    (default: 'conjecture').\n\
      \    -tptp <version>: uses <version> as TPTP syntax version;\n\
      \                    may be 1.0 or 3.3.0 (default: 3.3.0)\n";
     #flush stderr ());

fun do_args ("-prefix"::name::l) =
    (clause_name_prefix := name;
     do_args l)
  | do_args ("-status"::name::l) =
    (clause_status := name;
     do_args l)
  | do_args ("-tptp"::ver::l) =
    (tptp_version := ver;
     if ver inset dom tptp_keywords
	 then do_args l
     else usage ())
  | 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 kwds as |[input_clause, open_bracket, close_bracket,
			   ...]| = ?tptp_keywords (!tptp_version)
	     val pgclause = print_gclause (stdout, identity, kwds)
	 in
	     case plparse hyd of
		 SOME (plclauselist cl) =>
		 (iterate
		    (#put stdout input_clause;
		     #put stdout "(";
		     #put stdout (gensym (!clause_name_prefix));
		     #put stdout ",";
		     #put stdout (!clause_status);
		     #put stdout ",\n  ";
		     #put stdout open_bracket;
		     pgclause c;
		     #put stdout close_bracket;
		     #put stdout ").\n")
		  | c in list cl
		  end;
		    #flush stdout ();
		    quit 0)
	       | _ =>
		 (#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 ());
