(* h1 main loop.
   Copyright (C) 2003-2005 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 "plauto_h";
open "seidl_h";
open "print_seidl_h";
open "gensym_h";
open "verbose_h";
open "version_h";
open "yyerror_h";
open "sort_h";
open "rel_h";


local
    val nfa = re_make_nfa [(re_parse "^[0-9]+$", fn (s,a) => intofstring s)]
in
    fun match_dec s =
	nfa_run (nfa, s)
end;

val stop_on_first_botname = ref true;
val output_proof = ref 3;
val output_automaton = ref true;
val check_h1 = ref 0;
val seidl_flatten_body = ref false;
val seidl_monadic_proxy = ref false;
val maxpathlen = ref 3;
val maxneglit = ref max_int;
val output_trace = ref false;
fun modeloutp () = !output_automaton;
val resolvep = ref true;
val trimp = ref true;
val mknondetp = ref false;
val deepabbrvp = ref true;
val sortsimplp = ref true;

val the_automaton = ref (NONE : automaton option);

val bot_prefix = ref "reach_";
val rem_name = ref "rem_";
val term_type = ref "term";
val xname = ref "_x";
val state_prefix = ref "auto_";
val trans_name = ref "trans_";

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;

(*
val outproc_dummy = |[put = fn _ => (),
		      kill = fn _ => (),
		      flush = fn _ => ()
		      ]|;

fun condoutprocess (cond, arg as (s, _)) =
    if cond
	then outprocess arg
	    handle IO n => (#put stderr "Cannot execute '"; #put stderr s; #put stderr "': ";
			    #put stderr (iomsg n);
			    #put stderr "\n";
			    #flush stderr ();
			    raise QuitEvt 2)
    else outproc_dummy;
*)

val atexit = ref nil : (unit -> unit) list ref;

val magic = ref false;

fun usage () =
    (#put stderr "Usage: h1 <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) adds '%' comments to <filename>.log saying which clauses\n\
      \        are derived,\n\
      \    -v2 adds more detailed such comments.\n\
      \    -check-h1 <n>: if n=0, do not check whether input clauses\n\
      \                      are in class H1 (default);\n\
      \                   if n=1, emits warnings for non-H1 clauses;\n\
      \                   if n>=2, checks and fails on non-H1 clauses.\n\
      \    -all finds all contradictions,\n\
      \        -first stops on first contradiction (default).\n\
      \    -log outputs proof trace in file <filename>.log', \n\
      \        -log-out outputs proof trace on stdout, \n\
      \        -log-gz outputs proof in file <filename>.log.gz, compressed,\n\
      \        -no-log does not output any proof trace.\n\
      \        Default: -log.\n\
      \    -model outputs model (alternating automaton) as sets of Horn clauses,\n\
      \        in file '<filename>.model.pl',\n\
      \        -no-model does not.\n\
      \        Default: -model.\n\
      \    -progress outputs trace of proof search process that the h1mon utility\n\
      \        may use to display on-line statistics, in file 'h1.pgr'.\n\
      \        Default -no-progress.\n\
      \    -no-resolve disables the resolution engine.  That is, with the -no-resolve\n\
      \        option, h1 will just produce an approximated set of clauses into\n\
      \        file <filename>.log and exit.\n\
      \        Default -resolve.\n\
      \    -no-trim disables trimming.  Normally h1 removes from the input clauses\n\
      \        all clauses that cannot participate in any contradiction; this is\n\
      \        called trimming; -no-trim disables this.  This is useful e.g. to just\n\
      \        convert clauses to automata without looking for a contradiction.\n\
      \        (To be blunt, in case no input clause is a goal, trimming will just\n\
      \        remove every clause from the input set and h1 will conclude right away\n\
      \        that there is no contradiction, period.)\n\
      \        Default -trim.\n\
      \    -no-alternation activates reduction from alternating clauses to\n\
      \        non-deterministic automata clauses; useful to eliminate alternation in\n\
      \        '<filename>.model.pl'.\n\
      \        May also speed up, or slow down, proof search.\n\
      \        Default -alternation.\n\
      \    -no-deep-abbrv deactivates the generation of abbreviations for deep\n\
      \        terms in clause bodies during resolution.\n\
      \        Default -deep-abbrv.\n\
      \    -no-sort_simplify deactivates sort simplification.\n\
      \        Default -sort-simplify.\n\
      \    -monadic-proxy: changes the approximation process in a way that loses\n\
      \        more information than the standard one, -standard-approx;\n\
      \        may be faster sometimes.\n\
      \        Default: -standard-approx.\n\
      \    -path-refine <n>: h1 is guided by first computing an over-approximation\n\
      \        of the set of paths through all atoms in the least Herbrand model\n\
      \        of the definite clauses of the input; set the max length of these\n\
      \        paths to <n>.\n\
      \        Default: 3.\n\
      \    -body-chop <n>: chop every generated clause so that it has at most\n\
      \        <n> atoms of depth at least 1, i.e. of the form P (f (t1, ..., tn)),\n\
      \        in its body.  Proofs found may be false, but this may accelerate\n\
      \        the search for a model.\n\
      \        Default: max_int (i.e., no chop).\n\
      \    -magic: first transform input clause set using magic templates (experimental).\n";
     #flush stderr ());
(* disactivated:
      \    -auto <.pl filename> uses the automaton in the given Prolog file\n\
      \        as a guide in the proof search process.\n\
*)

fun var_name "" = "__dummy__"
  | var_name s =
    if ord s>=ord "A" andalso ord s<=ord "Z"
	then ("_big_" ^ chr (ord s+32) ^ substr (s, 1, size s))
    else s;

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

local
    val nfa = re_make_nfa [(re_parse "^(.*)\\.p$",
			    fn (s,a) => re_subst(s,a,1))]
in
    fun match_dot_p s =
	nfa_run (nfa, s)
end;

exception QuitResolveEvt;

fun do_args ("-model"::l) = (output_automaton := true; do_args l)
  | do_args ("-no-model"::l) = (output_automaton := false; do_args l)
  | do_args ("-log-out"::l) = (output_proof := 2; do_args l)
  | do_args ("-log-gz"::l) = (output_proof := 1; do_args l)
  | do_args ("-log"::l) = (output_proof := 3; do_args l)
  | do_args ("-no-log"::l) = (output_proof := 0; do_args l)
  | do_args ("-progress"::l) = (output_trace := true; do_args l)
  | do_args ("-no-progress"::l) = (output_trace := false; do_args l)
  | do_args ("-all"::l) = (stop_on_first_botname := false; do_args l)
  | do_args ("-first"::l) = (stop_on_first_botname := true; do_args l)
  | do_args ("-resolve"::l) = (resolvep := true; do_args l)
  | do_args ("-no-resolve"::l) = (resolvep := false; do_args l)
  | do_args ("-trim"::l) = (trimp := true; do_args l)
  | do_args ("-no-trim"::l) = (trimp := false; do_args l)
  | do_args ("-no-alternation"::l) = (mknondetp := true; do_args l)
  | do_args ("-alternation"::l) = (mknondetp := false; do_args l)
  | do_args ("-no-deep-abbrv"::l) = (deepabbrvp := false; do_args l)
  | do_args ("-deep-abbrv"::l) = (deepabbrvp := true; do_args l)
  | do_args ("-no-sort-simplify"::l) = (sortsimplp := false; do_args l)
  | do_args ("-sort-simplify"::l) = (sortsimplp := true; do_args l)
  | do_args ("-path-refine"::s::l) =
    (case match_dec s of
	 SOME n => (maxpathlen := n; do_args l)
       | _ => (#put stderr "Expected number after -path-refine.\n";
	       #flush stderr ();
	       raise QuitEvt 2))
  | do_args ("-body-chop"::s::l) =
    (case match_dec s of
	 SOME n => (maxneglit := n; do_args l)
       | _ => (#put stderr "Expected number after -body-chop.\n";
	       #flush stderr ();
	       raise QuitEvt 2))
  | do_args ("-monadic-proxy"::l) = (seidl_monadic_proxy := true; do_args l)
  | do_args ("-standard-approx"::l) = (seidl_monadic_proxy := false; do_args l)
    (* +-flat not documented: does not work so great. *)
    (*
  | do_args ("+flat"::l) = (seidl_flatten_body := true; do_args l)
  | do_args ("-flat"::l) = (seidl_flatten_body := false; do_args l)
     *)
  | do_args ("-check-h1"::s::l) =
    (case match_dec s of
	 SOME n => (check_h1 := n;
		    do_args l)
       | _ => (#put stderr "Expected number after -check-h1.\n";
	       #flush stderr ();
	       raise QuitEvt 2))
  | do_args ("-magic" :: l) =
    (magic := true; do_args l)
(* disactivated:
  | do_args ("-auto"::s::l) =
    (case !the_automaton of
	 SOME _ => (#put stderr "Duplicate -auto option.\n";
		    #flush stderr ();
		    raise QuitEvt 2)
       | _ => 
	 (let val f = infile s
	      val yyd = glex_data (f, fn _ => true)
	      val yyloc = glex_loc yyd
	      val hyd = gyacc_data (yyd, plautolex, aplnone (), plauto_value, yyloc, yyerror yyloc)
	  in
	      case plautoparse hyd of
		  SOME (aplauto a) => (the_automaton := SOME a;
				       do_args l)
		| _ => (#put stderr "Could not parse ";
			#put stderr s;
			#put stderr ": stop.\n";
			#flush stderr ();
			raise QuitEvt 2)
	  end handle IO n => (#put stderr s;
			      #put stderr ": ";
			      #put stderr (iomsg n);
			      #put stderr "\n";
			      #flush stderr ();
			      raise QuitEvt 2)
		   | PlautoUnterminatedCommentEvt =>
		     (#put stderr "Unterminated comment in file ";
		      #put stderr s;
		      #put stderr ": stop.\n";
		      #flush stderr ();
		      raise QuitEvt 2)))
*)
  | 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 ("-v2" :: l) = (verbosity := 2; 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 prefix = case filename of
			      "-" => "h1out"
			    | _ => (case match_dot_p filename of
					SOME base => base
				      | _ => 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 proof_out =
		 (case !output_proof of
		      1 => let val cmd = "gzip -c >" ^ prefix ^ ".log.gz"
			       val |[put, flush, ...]| =
				  outprocess ("sh", ["-c", cmd])
				  handle IO n => (#put stderr "Cannot execute '";
						  #put stderr cmd; #put stderr "': ";
						  #put stderr (iomsg n);
						  #put stderr "\n";
						  #flush stderr ();
						  raise QuitEvt 2)
			   in
			       SOME |[put=put, flush=flush]|
			   end
		    | 2 => SOME |[put = #put stdout, flush = #flush stdout]|
		    | 3 => (let val |[put, flush, ...]| =
				    outfile (prefix ^ ".log")
			    in
				SOME |[put=put, flush=flush]|
			    end handle IO n =>
				(#put stderr "Cannot open '";
				 #put stderr prefix;
				 #put stderr "' for writing: ";
				 #put stderr (iomsg n);
				 #put stderr "\n";
				 #flush stderr ();
				 raise QuitEvt 2))
		    | _ => NONE)
	     val flsh = fn () => case proof_out of
				     SOME |[flush, ...]| => flush ()
				   | _ => ()
	     val trace_out = if !output_trace
				 then SOME (condoutfile (true, "h1.pgr"))
			     else NONE
	     val flsh = fn () => ((case trace_out of
				       SOME |[flush, ...]| => flush ()
				     | _ => ());
				      flsh ())
	     val freshdefs = ref {}
	 in
	     case tptpparse hyd of
		 SOME (clauselist cl) =>
		 let val |[ new_clause, resolve, get_automaton, ...]| =
			 resolver (fn (c as CL (HBOT botname, ...)) =>
				      (#put stderr "*** Derived: ";
				       #put stderr botname;
				       #put stderr " ***\n";
				       #flush stderr ();
				       if !stop_on_first_botname
					   then raise QuitResolveEvt
				       else ()),
				      !maxpathlen, !maxneglit, !the_automaton,
				      !trimp, !mknondetp, !deepabbrvp,
				      !sortsimplp,
				      proof_out, trace_out)
		     val cl = if !magic
				  then magic_template cl
			      else cl
		     val preds = gclause_list_preds cl
		     fun freshP prefix =
			 let val P = gensym prefix
			 in
			     if P inset preds
				 then freshP prefix
			     else P
			 end
		     memofun newP_aux (body : int term list, t : int term) =
			     (case t of (* the distinction between __type_ and __def_
					 helps resolver (in clause.ml). *)
				  V _ => freshP "__type_"
				| _ => freshP "__def_")
		     val seidl_cvt = seidl_from_gclause (fn () => gensym "__X",
							    newP_aux, !seidl_flatten_body,
							    !seidl_monadic_proxy)
		     val non_h1 = ref false
		     val sjl = [(if !check_h1>=1
				     then (h1_exact c
					   handle H1NonHornEvt =>
					   (non_h1 := true;
					    #put stderr "Warning: clause ";
					    #put stderr name;
					    #put stderr " is not Horn.\n";
					    #flush stderr ())
						| H1NonLinearEvt x =>
						  (non_h1 := true;
						   #put stderr "Warning: clause ";
						   #put stderr name;
						   #put stderr " has non-linear head, variable ";
						   #put stderr x;
						   #put stderr " occurs repeatedly.\n";
						   #flush stderr ())
						| H1ConnectedNonSiblingEvt (x, y) =>
						  (non_h1 := true;
						   #put stderr "Warning: clause ";
						   #put stderr name;
						   #put stderr " has two non-sibling variables in\
						    \ the head\n\t\tthat are connected in the body, ";
						   #put stderr x;
						   #put stderr " and ";
						   #put stderr y;
						   #put stderr ".\n";
						   #flush stderr ()))
				 else ();
				     freshdefs := !freshdefs ++ newdefs;
				     (name, jc))
			       | name_c as (name, _, c) in list cl
				   val (jc, newdefs) = seidl_cvt name_c]
		     (*$V-*)
		     val _ = if !check_h1>=2 andalso !non_h1
				 then (#put stderr "Stop.\n"; #flush stderr (); raise QuitEvt 2)
			     else ()
		     (*$V+*)
		     val clauses = union {seidl_list_from_justif sj
					 | (_, sj) in list sjl}
		 in
		     case proof_out of
			 SOME (f as |[put, ...]|) =>
			 let val pgc = print_gclause_pl (f, identity)
			     val ps = print_seidl (f, identity)
			     val pc = print_clause (f, "X")
			 in
			     put "<source>\n";
			     iterate
			       (put "  <clause name=";
				print f (pack name);
				put "> ";
				pgc c;
				put " </clause>\n")
			     | (name, (_, c)) in list sjl
			     end;
			     put "</source>\n";
			     let fun shead (SEIDL (SHVAR (P, ...), ...)) = P
				   | shead (SEIDL (SHFUN (P, ...), ...)) = P
				   | shead _ = ""
				 val defs = {c => P
					    | c in set clauses
						val P = shead c
						such that P inset !freshdefs}
				 val invdefs = invrel defs
			     in
				 put "<definitions>\n";
				 iterate
				   iterate
				     (pc c; put "\n")
				   | sc in set ?invdefs P
				     val (c, ...) = clause_from_seidl sc
				   end
				 | P in list sort (op strless) (!freshdefs)
				   such that P inset invdefs
				 end;
				 put "</definitions>\n";
				 put "<approximation>\n";
				 iterate
				   (pc c; put "\n")
				 | sc in set defs <-| clauses
				 val (c, ...) = clause_from_seidl sc
				 end;
				 put "</approximation>\n"
			     end;
			     put "<justifications>\n";
			     iterate
			       ps sj
			     | (_, sj as (_, c)) in list sjl
			     end;
			     put "</justifications>\n"
			 end
		       | _ => ();
		     iterate
		       new_clause c
		     | seidlc in set clauses
		     val (c, rho, k) = clause_from_seidl seidlc
		     end;
		     if !resolvep
			 then (resolve () handle QuitResolveEvt => ())
		     else (flsh ();
			   raise QuitEvt 0);
		     let val trimauto = if modeloutp ()
					    then auto_trim (clean_automaton (get_automaton ()))
					else AUTO ({}, {})
			 val |[block_incl, ...]| = auto_simple_inclusions trimauto
			 val auto_out = condoutfile (!output_automaton, prefix ^ ".model.pl")
			 val pldefs = {P => let val f as |[put, convert, seek, truncate,
							   ...]| = outstring ""
						val arg =
						    (seek 0; truncate ();
						     print_term (f, identity) t;
						     convert ())
						val delimr = ref ""
						val def =
						    (seek 0; truncate ();
						     iterate
						       (put (!delimr); delimr:=",";
							print_atom (f, identity) a)
						     | a in list neg
						     end;
						     convert ())
					    in
						(arg, def)
					    end
				      | P => GCLAUSE (neg, [_ $ [t]]) in map !freshdefs}
		     in
			 if !output_automaton
			     then (iterate
				     (#put auto_out "%[def] ";
				      #put auto_out P;
				      #put auto_out " ";
				      #put auto_out arg;
				      if def=""
					  then ()
				      else (#put auto_out " :- ";
					    #put auto_out def);
				      #put auto_out ".\n")
				   | P => (arg, def) in map pldefs
				   end;
				     print_auto (auto_out, "X") trimauto;
				     #flush auto_out ())
			 else ();
			     flsh ()
		     end
		 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 =>
    (iterate
       xfun ()
     | xfun in list !atexit
     end;
       quit n);

