(* auto2pl main loop.
   Copyright (C) 2003, 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 "xa_h";
open "gclause_h";
open "intersym_h";
open "gensym_h";
open "yyerror_h";
open "rel_h";

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

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

val negated = ref ({} : string set);
val purge = ref false;
val completion = ref 0;
val defsp = ref false;
val inline_defsp = ref true;

fun do_purge (all_preds, states, tables, negated) =
    let val useful0 = union {if neg inset all_preds
				 then {q
				      | q => preds in map states
					  such that not (neg inset preds)}
			     else {}
			    | neg in set negated}
	fun do_useful (olduseful, useful) =
	    if useful=olduseful
		then useful
	    else let val new = useful \ olduseful
		 in
		     do_useful (useful,
				useful U union {union {elems ql
						      | ql => q in map table
							  such that q inset new}
					       | f => (_, table) in map tables})
		 end
	val useful = do_useful ({}, useful0)
    in
	if useful = all_preds
	    then (states, tables)
	else (useful <| states,
	      {f => (k, table |> useful)
	      | f => (k, table) in map tables})
    end;

memofun states_power (states : states, 0) = {nil}
      | states_power (states, 1) = {[q]
				   | q in set states}
      | states_power (states, n) = {q :: ql
				   | q in set states and ql in set states_power (states, n-1)};

(*
 OK, normally a deterministic tree automaton is a set Q of states q1, ..., qn
 together with partial functions I_f : Q^k -> Q for each k-ary function f.
 (Almost a first-order model.  Completing the automaton yields a true model.)

 However a convention of h1 is that non unary predicates R (say binary)
 are encoded by a unary predicate R plus a binary function symbol #R.
 So we are actually in an order-sorted first-order model.
 #R goes from Q^k to |R|, where |R| is the subsort of Q consisting
 of all states satisfying R.
 *)

fun incomplete (states, tables) =
    some
      (f, undef)
    | f => (k, table) in map tables
    (*$V-*)
    val false = invisible_fun f (* only visible functions are to be made complete. *)
    (*$V+*)
    val space = states_power (states, k)
    val undef = (table <-| space)
	such that not (empty undef)
    end

(*
fun freshq states =
    let val q = gensym ("q")
    in
	if q inset states
	    then freshq states
	else q
    end;
*)

fun make_complete (states, tables) =
    case incomplete (states, tables) of
	SOME _ => let val qsink = "__bot"
		      val states' = states ++ {qsink => {}}
		      memofun spower 0 = {nil => qsink}
			    | spower 1 = {[q] => qsink
					 | q in set states'}
			    | spower n = {q :: ql => qsink
					 | q in set states'
					 and ql in set spower (n-1)};
		  in
		      (states',
		       tables ++
		       {f => (k, spower k ++ fmap)
		       | f => (k, fmap) in map tables
			 such that not (invisible_fun f)}
		       (* do nothing for invisible functions (n-ary relations) *)
		       )
		  end
      | _ => (states, tables);

fun gclauses_from_table (f, table) =
    [GCLAUSE (neg, pos)
    | ql => q in map table
	val ir = ref 0
	val neg = [qi $ [V (inc ir; !ir)]
		  | qi in list ql]
	val pos = [q $ [f $ [let val _ $ [xi, ...] = ti
			     in
				 xi
			     end
			    | ti in list neg]]]
	    ];

fun gclauses_from_tables tables =
    append [gclauses_from_table (f, table)
	   | f => (k, table) in map tables];

fun resolve_states (states, gclauses) =
    (* Merge states into tables.
     The idea is that if v => P is in states,
     and f => (k, [v1,...,vk] => v) is in tables,
     then we add f => (k, [v1,...,vk] => P).

     The idea is that we resolve between the clauses:
     P(X) :- v(X)
     v(f(X1,...,Xk)) :- v1(X1), ..., vk(Xk)
     giving
     P(f(X1,...,Xk)) :- v1(X1), ..., vk(Xk)

     To sum up, given any clause
     v(f(X1,...,Xk)) :- v1(X1), ..., vk(Xk)
     and any v => P in states, we add
     P(f(X1,...,Xk)) :- v1(X1), ..., vk(Xk)

     Finally, we only keep those clauses that
     serve to define at least one predicate in pred.
     *)
    let val gclauses' =
	    append [let val Ps = ?states v
		    in
			[GCLAUSE (neg, [P $ l])
			| P in set Ps]
		    end
		   | gc as GCLAUSE (neg, [v $ l]) in list gclauses
		     such that v inset states]
	    @ gclauses
	val reachr = ref {}
	val g = union_rel {{P => {Q | Q $ _ in list neg}}
			  | GCLAUSE (neg, [P $ _]) in list gclauses'}
	fun do_reach P =
	    if P inset !reachr
		then ()
	    else (reachr := !reachr U {P};
		  if P inset g
		      then iterate
			  do_reach Q
			   | Q in set ?g P
			   end
		  else ())
    in
	iterate
	  do_reach P
	| P in set states <-|
	  {P | GCLAUSE (_, [P $ _]) in list gclauses'}
	    (* start by saying we are only interested in predicates
	     that are not values; others will be added by do_reach
	     above. *)
	end;
	let val Ps = !reachr
	in
	    [gc
	    | gc as GCLAUSE (_, [P $ _]) in list gclauses'
		such that P inset Ps
		    ]
	end
    end;

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;

fun usage () =
    (#put stderr "Usage: auto2pl <flags>* filename.\n\
     \  Version ";
     #put stderr version;
     #put stderr ", Copyright (C) Jean Goubault-Larrecq;\n\
      \     see file COPYRIGHT.\n\
      \  auto2pl 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\
      \    -complete <n>: if <n>=0, only checks that input automaton is deterministic\n\
      \                             (default).\n\
      \                   if <n>=1, makes it complete if it is not already.\n\
      \                   if <n>=2, fails if input automaton is not complete.\n\
      \    -negate <name> adds clauses to define a predicate __not_<name>\n\
      \            recognizing the complement of <name>;\n\
      \            <name> should be the name of a predicate (not a state),\n\
      \            as found in the <definitions> section of the input file.\n\
      \       Several -negate <name> flags may be given, to define several\n\
      \       negated predicates at once\n\
      \    -defs includes clauses defining predicates, not just states.\n\
      \        -no-defs does not include them.\n\
      \        -inline-defs resolves them with the automaton clauses\n\
      \         (and produces an automaton that is in general non-deterministic).\n\
      \        Default: -inline-defs.\n\
      \    -purge (only useful with -negate) outputs only the part of\n\
      \          the input automaton that is useful to build the negations\n\
      \          of the predicates given in -negate flags.\n\
      \        Default: -no-purge (and obsolescent anyway).\n";
     #flush stderr ());

exception XmlAutoDummy;

fun do_args ("-negate" :: name :: l) =
    (negated := !negated U {name};
     do_args l)
  | do_args ("-purge" :: l) = (purge := true; do_args l)
  | do_args ("-no-purge" :: l) = (purge := false; do_args l)
  | do_args ("-defs" :: l) = (defsp := true; inline_defsp := false; do_args l)
  | do_args ("-no-defs" :: l) = (defsp := false; inline_defsp := false;
				 do_args l)
  | do_args ("-inline-defs" :: l) = (defsp := false; inline_defsp := true;
				     do_args l)
  | do_args ("-complete"::s::l) =
    (case match_dec s of
	 SOME n => (completion := n;
		    do_args l)
       | _ => (#put stderr "Expected number after -complete.\n";
	       #flush stderr ();
	       quit 2))
  | 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, xmlautolex, xanone (), xa_value, yyloc, yyerror yyloc)
	 in
	     case xmlautoparse hyd of
		 SOME (xamodel (defs, states0, tables0)) =>
		 let val all_preds = union (rng states0)
		     val all_states = union {rng trans
					    | _ => (_, trans) in map tables0}
		     val (states1, tables1) =
			 if !completion>=2 andalso
			     (case incomplete (states0, tables0) of
				  SOME (f, undef) =>
				  (#put stderr "Definition of ";
				   #put stderr f;
				   #put stderr " is incomplete, e.g. entry ";
				   print stderr (pack (choose undef));
				   #put stderr " is undefined.\n";
				   #flush stderr ();
				   quit 2)
				| _ => false)
			     then raise XmlAutoDummy
			 else if not (empty (!negated)) orelse !completion>=1
			     then make_complete (states0, tables0)
			 else (states0, tables0)
		     val (states, tables) =
			 if !purge
			     then do_purge (all_preds, states1, tables1, !negated)
			 else (states1, tables1)
		     fun varname n =
			 let val f = outstring "X"
			 in
			     print f (pack (n:int));
			     #convert f ()
			 end
		     val pgpl = print_gclause_pl (stdout, varname)
		     val clauses0 = gclauses_from_tables tables
		     val clauses = if !inline_defsp
				       then resolve_states (states, clauses0)
				   else clauses0
		 in
		     iterate
		       (pgpl gc; #put stdout "\n")
		     | gc in list clauses
		     end;
		     if !defsp
			 then
			     (#put stdout "% Definitions.\n";
			      iterate
				(if P inset defs
				     then let val |[arg, cond]| = ?defs P
					  in
					      #put stdout "%[def] ";
					      #put stdout P;
					      #put stdout "(";
					      #put stdout arg;
					      #put stdout ")";
					      if cond=""
						  then ()
					      else (#put stdout " :- ";
						    #put stdout cond);
						  #put stdout ".\n"
					  end
				 else ();
				     iterate
				       (#put stdout P;
					#put stdout "(X) :- ";
					#put stdout q;
					#put stdout "(X).\n")
				     | q => preds in map states
					 such that P inset preds
				     end
				     )
			      | P in set all_preds \ all_states
			      end
			      )
		     else ();
		     if empty (!negated)
			 then ()
		     else (#put stdout "% Negated predicates.\n";
			   iterate
			     if neg inset all_preds
				 then iterate
				     (#put stdout "__not_";
				      #put stdout (_stringify neg);
				      #put stdout "(X) :- ";
				      #put stdout q;
				      #put stdout "(X).\n")
				      | q => preds in map states
					  such that not (neg inset preds)
				      end
			     else (#put stdout "__not_";
				   #put stdout (_stringify neg);
				   #put stdout "(X).\n")
			   | neg in set !negated
			   end);
			 #flush stdout ();
			 quit 0
		 end
	       | _ =>
		 (#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)
		  | XmlUnterminatedCommentEvt => (#put stderr "Unterminated comment: stop.\n";
						  #flush stderr ();
						  quit 2)
		  | EOFEncounteredEvt => (#put stderr "End of file reached unexpectedly: stop.\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 ());
