(* Small utility to convert tptp files as used by h1, to dfg files as used by SPASS.
   Copyright (C) 2005, 2008 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 "tptp_h";
open "yyerror_h";

val out_dummy = |[ put = fn _ => (),
		   seek = fn _ => (),
		   tell = fn _ => 0,
		   close = fn _ => (),
		   flush = fn _ => (),
		   advance = fn _ => (),
		   seekend = fn _ => (),
		   truncate = fn _ => ()
		   ]|;

exception QuitEvt of int;

fun condoutfile (cond, s) =
    if cond
	then outfile s
	    handle IO n => (#put stderr "Cannot open file '"; #put stderr s; #put stderr "' for writing: ";
			    #put stderr (iomsg n);
			    #put stderr "\n";
			    #flush stderr ();
			    raise QuitEvt 2)
    else out_dummy;

fun usage () =
    (#put stderr "Usage: tptp2dfg <flags>* filename.\n\
     \  Version 1.0, Copyright (C) Jean Goubault-Larrecq;\n\
      \     see file COPYRIGHT.\n\
      \  tptp2dfg 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 infile_or_stdin "-" = stdin
  | infile_or_stdin name =
    let val |[get, getline, ...]| = infile name
    in
	|[get=get, getline=getline]|
    end;

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 = glex_data (f, fn _ => true)
	     val yyloc = glex_loc yyd
	     val hyd = gyacc_data (yyd, tptplex, yynone (), tptp_value, yyloc, yyerror yyloc)
	 in
	     case tptpparse hyd of
		 SOME (clauselist cl) =>
		     let val unnamed_cl = [c | (_, _, c) in list cl]
			 val preds = gclause_list_pred_sig unnamed_cl
			 val funs = gclause_list_sig unnamed_cl
			 val delimr = ref ""
			 val |[put, flush, ...]| = stdout
			 val pa = print_atom (stdout, identity)
		     in
			 put "% File generated by tptp2dfg 1.0 (a quick hack by Jean Goubault-Larrecq)\n";
			 put "% You don't need this hack if 'tptp2X -f dfg' works where you are.\n";
			 put "% Where I am, it barfs when the input contains too many clauses.\n";
			 put "begin_problem(TPTP_Problem).\n\n";
			 put "list_of_descriptions.\n";
			 put "name({*[ File: ";
			 put filename;
			 put "],[ Names:]*}).\n";
			 put "author({*[ Source: not recorded.]*}).\n";
			 put "status(unknown).\n";
			 put "description({*[ Refs: not recorded.]*}).\n";
			 put "end_of_list.\n\n";
			 put "list_of_symbols.\n";
			 if empty funs
			     then ()
			 else (
			       put "functions[";
			       iterate
				 (put (!delimr);
				  delimr := ", ";
				  put "(";
				  put f;
				  put ",";
				  print stdout (pack k);
				  put ")")
			       | f => k in map funs
			       end;
			       put "].\n"
			       );
			 if empty preds
			     then ()
			 else (
			       put "predicates[";
			       delimr := "";
			       iterate
				 (put (!delimr);
				  delimr := ", ";
				  put "(";
				  put P;
				  put ",";
				  print stdout (pack k);
				  put ")")
			       | P => k in map {"equal"} <-| preds
				 (* do not list "equal", which is
				  built in equality in SPASS. *)
			       end;
			       put "].\n"
			       );
			 put "end_of_list.\n\n";
			 put "list_of_clauses(axioms,cnf).\n\
			  \end_of_list.\n\n";
			 put "list_of_clauses(conjectures,cnf).\n";
			 iterate
			   let val vars = gclause_vars c
			       val spaces = ref "  "
			       val nl = ref ",\n     ";
			   in
			       put "clause(\n";
			       if empty vars
				   then ()
			       else (put "  forall([";
				     delimr := "";
				     iterate
				       (put (!delimr); delimr := ","; put x)
				     | x in set vars
				     end;
				     spaces := "    ";
				     nl := !nl ^ "  ";
				     put "],\n");
				   put (!spaces);
				   put "or(";
				   delimr := "";
				   iterate
				     (put (!delimr);
				      delimr := !nl;
				      put "not(";
				      pa t;
				      put ")")
				   | t in list neg
				   end;
				   iterate
				     (put (!delimr);
				      delimr := !nl;
				      pa t)
				   | t in list pos
				   end;
				   put ")"; (* closing "or" *)
				   if empty vars
				       then ()
				   else put ")"; (* closing "forall" *)
				       put ",\n  ";
				       put name;
				       put ").\n"
			   end
			 | (name, _, c as GCLAUSE (neg, pos)) in list cl
			 end;
			 put "end_of_list.\n";
			 put "end_problem.\n";
			 flush ()
		     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))
  | 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;

