(* tptpmorph 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 "tptp_h";
open "morph_h";
open "gensym_h";
open "morphrewrite_h";
open "yyerror_h";

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

val tptp_version = ref ""; (* default: autodetect *)

fun zzerror equation tokens =
    (#put stderr "Parse error in -rewrite ";
     #put stderr equation;
     let val sep = ref ", expected: "
     in
        iterate
          (#put stderr (!sep);
           sep := " or ";
           #put stderr token)
        | token in list tokens
        end;
        #put stderr ".\n";
        #flush stderr ()
     end);

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

fun check_pattern_vars (equation, xl) =
    let val xs = ref {}
    in
	iterate
	  if x inset !xs
	      then (#put stderr "Duplicate variable ";
		    #put stderr x;
		    #put stderr " in -rewrite ";
		    #put stderr equation;
		    #put stderr "; stop.\n";
		    #flush stderr ();
		    quit 2)
	  else xs := !xs U {x}
	| x in list xl
	end;
	!xs
    end;

val rewrites = ref ({} : string -m> string list * string term);
val clause_status = ref "";

fun usage () =
    (#put stderr "Usage: tptpmorph <flags>* filename.\n\
     \  Version ";
     #put stderr version;
     #put stderr ", Copyright (C) Jean Goubault-Larrecq;\n\
      \     see file COPYRIGHT.\n\
      \  tptpmorph 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\
      \    -rewrite \"f(X1,...,Xn)=t\" where t is a term.\n\
      \       Several -rewrite flags may be given, with distinct f's.\n\
      \    -status <name>: uses <name> as second argument of 'input_clause'/'cnf'\n\
      \                    (default: do not override original second argument).\n\
      \    -tptp <version>: uses <version> as TPTP syntax version;\n\
      \                    may be 1.0 or 3.3.0 (default: autodetect)\n";
     #flush stderr ());

fun do_args ("-rewrite"::equation::l) =
    let val f = instring equation
	val yyd = glex_data (f, fn _ => true)
	val yyloc = glex_loc yyd
	val hyd = gyacc_data (yyd, morphlex, morphnone (), morph_value, yyloc, zzerror equation)
    in
	case morphparse hyd of
	    SOME (morphrewrite ((f, xl), t)) =>
	    let val xs = check_pattern_vars (equation, xl)
		val undef = tvars t \ xs
	    in
		if empty undef
		    then if f inset !rewrites
			     then (#put stderr "Function symbol ";
				   #put stderr f;
				   #put stderr " cannot be redefined in -rewrite ";
				   #put stderr equation;
				   #put stderr "; stop.\n";
				   #flush stderr ();
				   quit 2)
			 else (rewrites := !rewrites ++ {f => (xl, t)};
			       do_args l)
		else (#put stderr "Right-hand side variable ";
		      #put stderr (choose undef);
		      #put stderr " is not defined by left-hand side in -rewrite ";
		      #put stderr equation;
		      #put stderr "; stop.\n";
		      #flush stderr ();
		      quit 2)
	    end
	  | _ => quit 2
    end
  | 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, tptplex, yynone (), tptp_value, yyloc, yyerror yyloc)
	     val tptp_ver = if !tptp_version="" (* autodetect *)
				then tptp_default_version (!tptp_version_tally)
			    else !tptp_version
	     val kwds as |[input_clause, open_bracket, close_bracket,
			   ...]| = ?tptp_keywords tptp_ver
	     val pgclause = print_gclause (stdout, identity, kwds)
	     val apply = apply_morphism_gclause (!rewrites)
	 in
	     case tptpparse hyd of
		 SOME (clauselist cl) =>
		 (iterate
		    let val c' = apply c
			    handle MorphismBadArityEvt (f, pat_n, arity) =>
			    (#put stderr "Non-matching arity for function ";
			     #put stderr f;
			     #put stderr " of arity ";
			     print stderr (pack arity);
			     #put stderr " in clause ";
			     #put stderr name;
			     #put stderr ":\n    rewrite pattern expects ";
			     print stderr (pack pat_n);
			     #put stderr " arguments.\n";
			     #flush stderr ();
			     quit 2)
		    in
			#put stdout input_clause;
			#put stdout "(";
			#put stdout name;
			#put stdout ",";
			#put stdout (if !clause_status=""
					 then status
				     else !clause_status);
			#put stdout ",\n  ";
			#put stdout open_bracket;
			pgclause c';
			#put stdout close_bracket;
			#put stdout ").\n"
		    end
		  | (name, status, 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))
  | do_args nil = (#put stderr "Missing filename.\n"; usage (); quit 2)
  | do_args _ = (usage ();
		 quit 2)
    ;

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