(* Automata determinization functions.
   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 "determinize_h";
open "sort_h";
(*open "gensym_h";*)
open "intersym_h";
open "verbose_h";

(*$P-*)

local
    val nfa = re_make_nfa [(re_parse "^#", fn _ => ())]
in
    fun invisible_fun P =
	case nfa_run (nfa, P) of
	    SOME _ => true
	  | _ => false
end;

fun pstate v =
    let val delimr = ref ""
    in
	if empty v
	    then #put stderr "<catchall>"
	else
	    iterate
	      (#put stderr (!delimr);
	       delimr := " & ";
	       #put stderr P)
	    | P in set v
	    end
    end;

fun determinize (AUTO (auto, univ), block_incl) =
    let val auto_nary = {P => fmap
			| P => fmap as {f => (_, _, {_, _, ...})} in map auto
			  such that invisible_fun f}
	val auto_unary = auto_nary <-| auto
	val values = ref ({} : block set)
	val semantics = ref ({} : string -m> (block list -m> block))
	    (* map f to table *)
	(* values (states of the determinized complete automaton defined by auto,
	 or rather auto_unary) are sets of predicates.
	 Semantics of f is given by:
	 f (v1, ..., vn) =
	 {P | exists P(f(x1,...,xn)) <= B1(x1), ..., Bn(xn) .
	      B1 subseteq v1 and ... and Bn subseteq vn}
	 *)
	val funs = overwrite [{f => k | f => (_, k, _) in map fmap
			       (*such that not (invisible_fun f)*)}
			     | _ => fmap in map auto_unary]
	    (*
	fun min_set {v} = v
	  | min_set vs = let val (vs1, vs2) = split vs
			     val v1 = min_set vs1
			     val v2 = min_set vs2
			 in
			     if card v1 < card v2
				 then v1
			     else v2
			 end
	memofun reduce_value {} = {}
	      | reduce_value v =
		(case {reduce_value v'
		      | P in set v
			val v' = v \ {P}
			  such that block_incl (v', {P})
			      }
		     of
		     {} => v
		   | vs => min_set vs)
	     *)
	memofun reduce_value {} = {}
	      | reduce_value v =
		case
		    some
		      P
		    | P in set v
		      such that block_incl (v \ {P}, {P})
		    end of
		    SOME P => reduce_value (v \ {P})
		  | _ => v
	val red_value = if !verbosity>=2
			    then memofn v =>
				let val v' = reduce_value v
				in
				    if v <> v'
					then (#put stderr "Reduce state ";
					      pstate v;
					      #put stderr " to ";
					      pstate v';
					      #put stderr "\n";
					      #flush stderr ())
				    else ();
					v'
				end
			else reduce_value
	fun new_value v =
	    if v inset !values
		then ()
	    else (do_verbose (1, fn () => (#put stderr "New state ";
					   pstate v;
					   #put stderr "\n";
					   #flush stderr ()));
		  values := !values U {v})
	fun init_semantics () =
	    let val oldsemantics = !semantics
	    in
		iterate
		  semantics := !semantics ++ {f => new_sem_f}
		| f => 0 in map funs
		val new_sem_f = let val v = {P
					    | P => fmap in map auto_unary
						such that f inset fmap andalso
						    not (empty (#1 (?fmap f)))}
				    val v' = red_value v
				in
				    if empty v'
					then (new_value v'; {})
				    (* do not include transition leading to empty set
				     as value.
				     This means we produce incomplete deterministic
				     automata. *)
				    else (new_value v';
					  {nil => v'})
				end
(*
val _ = (#put stderr "Initial entries for ";
	 #put stderr f;
	 #put stderr ":\n";
	 pretty stderr (pack new_sem_f);
	 #flush stderr ())
*)
		end
	    end
	fun inter_auto (a : string -m> block list set, a' : string -m> block list set) =
	    {P => blkls''
	    | P => blkls in map a' <| a
		val blkls' = ?a' P
		val blkls'' = blkls & blkls'
					such that not (empty blkls'')}

	fun new_semantics (oldvalues, allvalues) =
	    (* with oldvalues subset allvalues *)
	    let val oldsemantics = !semantics
	    in
(*
#put stderr "Number of values now: ";
print stderr (pack (card allvalues));
#put stderr "; oldvalues = ";
pretty stderr (pack oldvalues);
#put stderr "  newvalues = ";
pretty stderr (pack (allvalues \ oldvalues));
#flush stderr ();
*)
		case allvalues \ oldvalues of
		    {} => ()
		  | newvalues => 
		    iterate
		      semantics := !semantics ++ {f => sem_f ++ new_sem_f}
		    | f => k0 in map funs
(*
val _ = (#put stderr "New entries for ";
	 #put stderr f;
	 #put stderr ":\n";
	 #flush stderr ())
*)
		    val sem_f = if f inset oldsemantics
				    then ?oldsemantics f
				else {}
		    val a0 = {P => #1 (?fmap f)
			     | P => fmap in map auto_unary
				 such that f inset fmap}

		    memofun filter_auto (v, i) =
			    {P => blkls'
			    | P => blkls in map a0
				val blkls' = {blkl
					     | blkl in set blkls
						 such that block_incl (v, blkl nth i)}
				such that not (empty blkls')
				    }

		    fun do_iter (_, _, {}) = {}
		      (* do not include transition leading to empty set as value.
		       This means we produce incomplete deterministic automata. *)
		      | do_iter (0, vl, a) =
			(* normally rev vl is not in sem_f. *)
			let val v = dom a
			    val v' = red_value v
			in
			    new_value v';
			    {rev vl => v'}
			end
		      | do_iter (k, vl, a) =
			let val k' = k-1
			    val i = k0-k
			in
			    overwrite [
				       do_iter (k', v::vl, inter_auto (a, a'))
				      | v in set allvalues
					  val a' = filter_auto (v, i)
					      ]
			end
		    fun do_iter_not_all_old (0, ...) = {}
		      | do_iter_not_all_old (_, _, {}) = {}
		      (* do not include transition leading to empty set as value.
		       This means we produce incomplete deterministic automata. *)
		      | do_iter_not_all_old (1, vl, a) = (* not necessary,
							  still useful for speed. *)
			let val i = k0-1
			in
			    overwrite [
				       do_iter (0, v::vl, inter_auto (a, a'))
				      | v in set newvalues
					  val a' = filter_auto (v, i)
					  ]
			end
		      | do_iter_not_all_old (k, vl, a) =
			let val k' = k-1
			    val i = k0-k
			in
			    overwrite [
				       do_iter_not_all_old (k', v::vl, inter_auto (a, a'))
				      | v in set oldvalues
					  val a' = filter_auto (v, i)
					      ] ++
			    overwrite [
				       do_iter (k', v::vl, inter_auto (a, a'))
				      | v in set newvalues
					  val a' = filter_auto (v, i)
					      ]
			end
		    val new_sem_f = do_iter_not_all_old (k0, nil, a0)
(*
val _ = (pretty stderr (pack new_sem_f);
	 #flush stderr ())
*)
		    end
	    end
	fun saturate oldvalues =
	    let val allvalues = !values
	    in
		if oldvalues = allvalues
		    then ()
		else
		    (new_semantics (oldvalues, allvalues);
		     saturate allvalues)
	    end
    in
	init_semantics ();
	new_value {};
	saturate {};
	(!values, !semantics ++ {f => {blkl => {P}
				      | blkl in set blkls}
				| P => fmap as {f => (blkls, ...)} in map auto_nary})
    end;

(*
fun print_fmodel_dot (f as |[put, ...]|, (states, tables)) =
    let val p = print f
	val sortP = sort (op strless)
	memofun state_name {} = "."
	      | state_name blk =
		let val f as |[put, convert, ...]| = outstring ""
		    val delimr = ref ""
		in
		    iterate
		      (put (!delimr); delimr := ", "; put P)
		    | P in list sortP blk
		    end;
		    convert ()
		end
	fun pstate blk = p (pack (state_name blk))
    in
	(put "digraph G {\n  size = \"8.5,11\";\n  rankdir = TB;\n  node[shape=circle];\n";
	 iterate
	   iterate
	     let val trans = gensym "trans"
		 val ir = ref 0
	     in
		 put "  "; put trans;
		 put " [shape=record,height=0,width=0,label="; p (pack fname);
		 put "];\n";
		 iterate
		   (put "  "; pstate vi;
		    put " -> "; put trans;
		    (case vl of
			 [_, _, ...] => (put ":";
					 inc ir;
					 put "port";
					 p (pack (!ir)))
		       | _ => ());
		    (*put " [dir=none]";*)
		    put ";\n")
		 | vi in list vl
		 end;
		 put "  "; put trans;
		 (case vl of
		      [_, _, ...] => put ":out"
		    | _ => ());
		 put " -> "; pstate v;
		 put ";\n"
	     end
	   | vl => v in map table
	     such that v<>{}
	   end
	 | f => table in map tables
	 val fname = if empty table
			 then f
		     else case choose table of
			      nil => f
			    | [_] => f
			    | l => let val fd as |[put, convert, ...]| = outstring "<out>"
				       val delimr = ref ""
				       val ir = ref 0
				   in
				       put f;
				       iterate
					 (put (!delimr); delimr := ""; inc ir;
					  put "|<port"; print fd (pack (!ir)); put "> ")
				       | _ in list l
				       end;
				       convert ()
				   end
	 end;
	 put "}\n")
    end;
*)

fun print_fmodel_table (fd as |[put, ...]|, (states, tables) : fmodel,
			preds0 : string set, defs0 : string -m> string * string, block_incl) =
    let (*val nfd as |[convert, tell, seek, ...]| = outstring "q"*)
	(*val n = tell ()*)
	(*val qr = ref 0*)
	val defs = union states <| defs0
	val preds = defs0 <-| preds0
	    (*
	memofun qname blk =
		(inc qr;
		 seek n;
		 print nfd (pack (!qr));
		 convert ())
	     *)
    (*
	memofun not_P P = "__not_" ^ _stringify P
	memofun block_not blk = {not_P P | P in set blk}
	memofun qname blk = mk_inter (blk U block_not (preds0 \ blk))
     *)
	memofun qname blk = mk_detval blk
    in
	put "<?xml version=\"1.0\" encoding=\"UTF-8\"?>\n";
	put "<definitions>\n";
	iterate
	  (put "  <definition name=";
	   print fd (pack P);
	   put " arg=";
	   print fd (pack arg);
	   if def=""
	       then ()
	   else (put " cond=";
		 print fd (pack def));
	   put "/>\n")
	| P => (arg, def) in map defs
	end;
	put "</definitions>\n";
	put "<states>\n";
	iterate
	  (put "  <state name=";
	   print fd (pack (qname blk));
	   let val Pl = [P
			| P in set preds
			  such that block_incl (blk, {P})]
	       val blk' = defs <| blk
	   in
	       if null Pl andalso empty blk'
		   then put "/>\n"
	       else (put ">\n";
		     iterate
		       (put "    <satisfies name=";
			print fd (pack P);
			put "/>\n")
		     | P in list Pl
		     end;
		     iterate
		       (put "    <satisfies name=";
			print fd (pack P);
			put "/>\n")
		     | P => def in map blk'
		     end;
		     put "  </state>\n")
	   end)
	| blk in set states
	end;
	put "</states>\n";
	put "<tables>\n";
	iterate
	  (put "  <table name=";
	   print fd (pack f);
	   put " arity=\"";
	   print fd (pack (case table of
			       {} => 0
			     | {vl => _, ...} => len vl));
	   put "\">\n";
	   iterate
	     (put "    <entry result=";
	      print fd (pack (qname v));
	      put ">";
	      iterate
		(put "<arg name=";
		 print fd (pack (qname vi));
		 put "/>")
	      | vi in list vl
	      end;
	      put "</entry>\n")
	   | vl => v in map table
	   end;
	   put "  </table>\n")
	| f => table in map tables
	end;
	put "</tables>\n"
    end;
