(* Monitoring script for h1.
   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.
*)

val derived_n = ref 0;
val forward_n = ref 0;
val funheads_n = iarray (4, 0);
val auto_n = ref 0;
val picked_n = ref 0;

local
    val nfa = re_make_nfa [ (re_parse "\\|-",
			     fn _ => inc derived_n),
			   (re_parse "forward",
			    fn _ => inc forward_n),
			   (re_parse "\\(([1-4])\\)",
			    fn (s,a) => let val i = ord (re_subst(s,a,1))
						- ord "1"
					in
					    iupdate (funheads_n, i,
						     isub (funheads_n, i)+1);
					end),
			   (re_parse "automaton",
			    fn _ => inc auto_n),
			   (re_parse "Picking",
			    fn _ => inc picked_n)]
in
    fun grep f =
	let val line = #getline f ()
	in
	    if line=""
		then ()
	    else (nfa_run (nfa, line); grep f)
	end;

fun main () =
    (grep stdin;
     #put stdout "Derived clauses: "; print stdout (pack (!derived_n));
     #put stdout "\nSubsumed clauses [forward]: "; print stdout (pack (!forward_n));
     (*#put stdout "\nSubsumed clauses [backward]: "; print stdout (pack (!backward_n));*)
     #put stdout "\nFunheads optimization: "; print stdout (pack (isub (funheads_n, 0)));
     #put stdout " / "; print stdout (pack (isub (funheads_n, 1)));
     #put stdout " / "; print stdout (pack (isub (funheads_n, 2)));
     #put stdout " / "; print stdout (pack (isub (funheads_n, 3)));
     #put stdout "\nAutomata clauses: "; print stdout (pack (!auto_n));
     #put stdout "\nDealt with: "; print stdout (pack (!picked_n));
     #put stdout "\n";
     #flush stdout ()
     );
