(* h1fi finite model finder.
   Copyright (C) 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 "verbose_h";
open "tptp_h";
open "yyerror_h";
open "h1ficc_h";
(*open "gclauseutils_h";*)

val version = "1.0 - Oct 24, 2008";

val h1fi_policy = ref (make_pred_policy (fn _ => false)
		       : (string, unit) policy);

val q_prefix = ref "_q";

exception QuitEvt of int;

fun usage () =
    (#put stderr "Usage: h1fi <flags>* filename.\n\
     \  Version ";
     #put stderr version;
     #put stderr ", Copyright (C) Jean Goubault-Larrecq;\n\
      \     see file COPYRIGHT.\n\
      \  h1 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,\n\
      \    -v1 (or just -v) shows derived equations as soon as they are found.\n\
      \    -policy <policyname> defines how new states should be merged;\n\
      \      -policy herbrand never merges new states;\n\
      \      -policy pred <params> is the predicate-based merging policy, where\n\
      \        <params> is either '-' (default)\n\
      \        or list of initials of variables that should be taken into\n\
      \        account (e.g., -policy heam ABC will treat specially those\n\
      \        variables starting with A, B, or C).\n\
      \      -policy heam <params> is the Heam merging policy, where\n\
      \        <params> is as above.\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 varname (i:int) =
    let val f as |[put, convert, ...]| = outstring "X"
    in
	print f (pack i);
	convert ()
    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 ("-v" :: l) = (verbosity := 1; do_args l)
  | do_args ("-policy" :: l) =
    (case l of
	 "herbrand" :: rest =>
	 (h1fi_policy := herbrand_policy; do_args rest)
       | "pred" :: params :: rest =>
	 let val initials = case params of
				"-" => {}
			      | _ => elems (explode params)
	 in
	     h1fi_policy := make_pred_policy (fn x =>
						 x <> "" andalso
						 chr (ord x) inset initials);
	     do_args rest
	 end
       | "heam" :: params :: rest =>
	 let val initials = case params of
				"-" => {}
			      | _ => elems (explode params)
	 in
	     h1fi_policy := make_heam_policy (fn x =>
						 x <> "" andalso
						 chr (ord x) inset initials);
	     do_args rest
	 end
       | _ => (#put stderr "unknown policy, or bad arguments to policy;\n";
	       usage ();
	       raise QuitEvt 2))
  | 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 cl0) =>
		 let val cl = cl0
			 (*range_restrict (cl0, !q_prefix ^ "dom",
					      varname, "__dummy__")*)
		     val cclo as |[universe, ...]| = cc ()
		     val |[force_gclause, ...]| = forcers (cclo, !h1fi_policy,
							   identity)
		     fun force_gclauses cl =
			 iterate
			   (do_verbose (1,
					fn () =>
					   (#put stderr "Examining clause ";
					    #put stderr name;
					    #put stderr " : ";
					    print_gclause_pl (stderr, identity) c;
					    #put stderr ".\n";
					    #flush stderr ()));
			    force_gclause c)
			 | (name, _, c) in list cl
			 end
		     fun iter_force_gclauses (round, cl, old_universe) =
			 (do_verbose (1,
				      fn () =>
					 (#put stderr "*** Round ";
					  print stderr (pack round);
					  #put stderr " ***\n";
					  #flush stderr ()));
			  force_gclauses cl;
			  let val new_universe = universe ()
			  in
			      if new_universe=old_universe
				  then () (* finished *)
			      else iter_force_gclauses (round+1, cl,
							new_universe)
			  end)
		 in
		     iter_force_gclauses (1, cl, universe ());
		     print_auto (stdout, "X") (auto_from_cc (cclo, !q_prefix));
		     #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))
  | 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;
