(* Alternating tree automata.
   Copyright (C) 2003,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 "auto_h";
open "fixbool_h";

(*$P-*)

fun auto_trim (AUTO (auto, univ)) =
    let val auto' = univ <-| auto (* first remove all clauses P(f(x1, ..., xk)) <= ...
				   for all P in univ, i.e., such that there is a clause +P(x). *)
	val ne_horn = new_horn_set ()
    in
	(* P is estimated non empty as soon as
	 there exists a clause P(x) in univ [assumes there is at least one constant...]
	 or there is a clause P(f(x1,...,xk)) <= B1(x1), ..., Bk(xk) in auto
	 such that all predicates in B1, ..., Bk are non empty.
	 This estimates more predicates as non empty than there really are, unless
	 B1, ..., Bk contain at most one predicate.
	 But this runs in polynomial time.
	 *)
	iterate
	  add_horn_clause (ne_horn, SOME P, {})
	| P in set univ
	end;
	iterate
	  iterate
	    iterate
	      add_horn_clause (ne_horn, SOME P, union {blk | blk in list blkl})
	    | blkl in set blkls
	    end
	  | f => (blkls, ...) in map fmap
	  end
	| P => fmap in map auto
	end;
	let val non_empty = horn_solve ne_horn
		(* remove empty states, both in heads and bodies. *)
	    val auto'' = {P => fmap'
			 | P => fmap in map non_empty <| auto
			   val fmap' = {f => (blkls', k, vars)
				       | f => (blkls, k, vars) in map fmap
					   val blkls' = {blkl
							| blkl in set blkls
							    such that
								all
								  all
								    P inset non_empty
								  | P in set blk
								  end
								| blk in list blkl
								end}
					   such that not (empty blkls')}
							   such that not (empty fmap')}
	in
	    AUTO (auto'', univ)
	end
    end;

(* Given an automaton a, and states q1, ..., qn,
 try to decide quickly when q1 & ... & qn is definitely empty.
 We assume that a is trimmed, meaning that all obviously empty
 states have already been removed.
*)
fun auto_intersects (AUTO (auto, univ)) =
    let val non_empty_map = ref ({} : block -m> bool)
	fun is_non_empty qs =
		(case univ <-| qs of (* remove universal states, which do not count. *)
		     {} => true (* intersection of 0 state is the whole universe, so not empty. *)
		       (*
			| {_} => true (* assume that single states are (probably) not empty. *)
			  *)
		   | qs' as {q1} U otherqs =>
		     if qs' inset !non_empty_map
			 then ?(!non_empty_map) qs'
		     else (non_empty_map := !non_empty_map ++ {qs' => false};
			   (* By default, qs' is estimated empty. *)
			   let val fs = inter {if q inset auto
						   then ?auto q
					       else {}
					      | q in set qs'}
			       val res =
				   exists
				     let fun merge_blkl (blk::rest, blk' :: rest') =
					     (blk U blk') :: merge_blkl (rest, rest')
					   | merge_blkl _ = nil
					 fun ex_blkl ({}, blkl) =
					     all
					       is_non_empty blk
					     | blk in list blkl
					     end
					   | ex_blkl ({q} U rest, blkl1) =
					     let val (blkls, ...) = ?(?auto q) f
					     in
						 exists
						   ex_blkl (rest, merge_blkl (blkl, blkl1))
						 | blkl in set blkls
						 end
					     end
				     in
					 exists
					   ex_blkl (otherqs, blkl)
					 | blkl in set #1 (?(?auto q1) f)
					 end
				     end
				   | f in set fs
				   end
			   in
			       non_empty_map := !non_empty_map ++ {qs' => res};
			       res
			   end))
    in
	is_non_empty
    end;

(*
fun auto_match_term (AUTO (auto, univ)) =
    let memofun auto_match (B, V x) = {{x => B}}
	      | auto_match ({}, _) = {{}}
	      | auto_match ({P}, f $ l) =
		if P inset univ
		    then {{}}
		else if P inset auto
		    then let val fmap = ?auto P
			 in
			     if f inset fmap
				 then union {

					    | blkl in set #1 (?fmap f)}
			     else {}
			 end
		else {}
	      | auto_match (B, t) =
		let val (B1, B2) = split B
		    val sigmas1 = auto_match (B1, t)
		    val sigmas2 = auto_match (B2, t)
		in
		    
		end
    in
	auto_match
    end;
*)

fun auto_simple_inclusions (AUTO (auto, univ)) =
    let val mapr = ref ({} : string * string -m> bool)
	fun detect (pair as (P, Q)) =
	    Q inset univ orelse P=Q orelse
	    (not (P inset univ) andalso (* estimate that no universal language is included in
					 any auto language; this is true when signatures can be
					 extended. *)
	     let val savemap = !mapr
	     in
		 if pair inset savemap
		     then ?savemap pair
		 else (mapr := savemap ++ {pair => true};
		       let val Qfmap = if Q inset auto
					   then ?auto Q
				       else {}
			   val Pfmap = if P inset auto
					   then ?auto P
				       else {}
		       in
			   all
			     f inset Qfmap andalso
			     let val (Qblkls, ...) = ?Qfmap f
			     in
				 all
				   exists
				     all
				       block_incl (Pblk, Qblk)
				     || Pblk in list Pblkl and Qblk in list Qblkl
				     end
				   | Qblkl in set Qblkls
				   end
				 | Pblkl in set Pblkls
				 end
			     end
			   | f => (Pblkls, Pk, Pvars) in map Pfmap
			   end
		       end orelse (mapr := (savemap ++ {p => false
						       | p => false in map savemap <-| !mapr}
					    ++ {pair => false});
				   (* add the fact that pair is not an inclusion;
				    keep all found non-inclusions, but remove all inclusions
				    found since we assumed pair to be an inclusion.
				    This is not the most efficient algorithm...
				    *)
				   false))
	     end)
	and block_incl (Pblk, Qblk) =
	    (* simple test: Pblk included in Qblk if for every Q1 in Qblk, there is a P1 in Pblk
	     with P1 included in Q1 ("included in" meaning that the languages are included).
	     Optimisation: if Qblk is a subset (as a set of predicates) of Pblk, then this
	     criterion is always true.
	     This optimisation can be generalized as follows.  Assume that
	     Pblk = blk U Pblk' and Qblk = blk U Qblk', e.g., blk = Pblk & Qblk,
	     Pblk' = Pblk \ Qblk, Qblk' = Qblk \ Pblk.
	     Then Pblk included in Qblk if for every Q1 in Qblk', there is a P1 in Pblk
	     with P1 included in Q1.
	     *)
	    all
	      exists
		detect (P1, Q1)
	      | P1 in set Pblk
	      end
	    | Q1 in set Qblk \ Pblk
	    end
    in
	|[ pred_incl = detect,
	   block_incl = block_incl]|
    end;

(*
exception AutoFairlySimpleInclusions;

fun auto_fairly_simple_inclusions (AUTO (auto, univ)) =
    let val mapr = ref ({} : block * string -m> bool)
	memofun blk_fmap {} = raise AutoFairlySimpleInclusions
	      | blk_fmap {P} = if P inset auto
				   then ?auto P
			       else {}
	      | blk_fmap Pblk = let val (Pblk1, Pblk2) = split Pblk
				    val fmap1 = blk_fmap Pblk1
				    val fmap2 = blk_fmap Pblk2
				in
				    (fmap1 delta fmap2) ++
				    {f => !!!
				    | f => (blkls1, k, vars) in map fmap2 <| fmap1
					val (blkls2, ...) = ?fmap2 f}
				end
	fun detect (Pblk, Qblk) =
	    (* first, Pblk subseteq Qblk <=> Pblk subseteq (Qblk \ Pblk \ univ)
	     where subseteq is language inclusion. *)
	    let val Qblk' = (Qblk \ Pblk) \ univ
		val Pblk' = Pblk \ univ
	    in
		not (empty Pblk) andalso
		all
		  detect1 (Pblk, Q)
		| Q in set Qblk'
		end
	    end
	and detect1 (pair as (Pblk, Q)) =
	    if pair inset !mapr
		then ?(!mapr) pair
	    else (mapr := !mapr ++ {pair => true};
		  let val Qfmap = if Q inset auto
				      then ?auto Q
				  else {}
		  in
		      all
		      | P

		  end orelse (mapr := !mapr ++ {pair => false};
			      false))
    in
	|[ pred_incl = fn (P, Q) => detect1 ({P}, Q),
	   block_incl = detect ]|
    end;
*)

fun auto_simplify (a as AUTO (auto, univ), block_incl) =
    let fun blocks_incl (Pblkl, Qblkl) =
	    all
	      block_incl (Pblk, Qblk)
	    || Pblk in list Pblkl and Qblk in list Qblkl
	    end
	fun filter_in (blkl, {}, acc) = acc U {blkl}
	  | filter_in (blkl, blkls as ({blkl'} U rest), acc) =
	    if blocks_incl (blkl, blkl')
		then acc U blkls
	    else if blocks_incl (blkl', blkl)
		then filter_in (blkl, rest, acc)
	    else filter_in (blkl, rest, acc U {blkl'})
	fun filter ({}, acc) = acc
	  | filter ({blkl} U rest, acc) =
	    filter (rest, filter_in (blkl, acc, {}))
    in
	AUTO ({P => {f => (filter (blkls, {}), k, vars)
		    | f => (blkls, k, vars) in map fmap}
	      | P => fmap in map auto},
		univ)
    end;

fun print_auto_clauses (fd as |[put, ...]|, xname, separ) (P, f, blkls, k) =
    let val ir = ref 0
	val xl = case k of
		     0 => nil
		   | 1 => [xname]
		   | _ => [(inc ir;
			    let val f as |[put, convert, ...]| = outstring xname
			    in
				print f (pack (!ir));
				convert ()
			    end)
			  |while !ir<k]
	val head = let val |[put, convert, ...]| = outstring P
		       val invis = f<>"" andalso ord f=ord "#"
		   in
		       if invis
			   then ()
		       else (put "("; put f);
			   (case xl of
					   nil => ()
			      | [x1] => (put "("; put x1; put ")")
			      | _ => let val delimr = ref "("
				     in
					 iterate
					   (put (!delimr); delimr := ",";
					    put x)
					 | x in list xl
					 end;
					 put ")"
				     end);
				if invis
				    then ()
				else put ")";
				    convert ()
		   end
	val dr = ref ""
    in
	iterate
	  (put (!dr); dr := separ;
	   put head;
	   (case blkl of
		nil => ()
	      | _ => let val delimr = ref " :- "
		     in
			 iterate
			   iterate
			     (put (!delimr); delimr := ", ";
			      put P; put "("; put xi; put ")")
			   | P in set blk
			   end
			 || blk in list blkl and xi in list xl
			 end
		     end))
	| blkl in set blkls
	end
    end;
    
fun print_auto (fd as |[put, ...]|, xname) =
    let val pa_clauses = print_auto_clauses (fd, xname, ".\n")
	fun pauto (AUTO (auto, univ)) =
	    (iterate
	       (put P; put "("; put xname; put ").\n")
	     | P in set univ
	     end;
	       iterate
		 iterate
		   (pa_clauses (P, f, blkls, k);
		    if empty blkls
			then ()
		    else put ".\n")
		 | f => (blkls, k, _) in map fmap
		 end
	       | P => fmap in map auto
	       end
	       )
    in
	pauto
    end;

fun enrich_auto_eq (a as AUTO (auto, univ)) =
    let val states =
	    univ <-| (union {union {union {union {blk
						 | blk in list blkl}
					  | blkl in set blkls}
				   | f => (blkls, ...) in map fmap}
			    | P => fmap in map auto})
    in
	if "equal" inset states orelse
	    "equal" inset auto orelse
	    "equal" inset univ
	    then a (* "equal" already there: do not change anything. *)
		(* otherwise, add all clauses equal(X,Y) :- q(X), q(Y)
		 for all states q. *)
	else AUTO (auto ++ {"equal" => {"#equal" => ({[{q}, {q}]
						     | q in set states},
						       2, {1,2})
					}},
		   univ)
    end;

