(* Alternating tree automata, headers.
   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.
*)


type block = string set;
(* a block is a set {P1, ..., Pk} of predicates (states).
 *)

datatype automaton = AUTO of
	 (string -m> string -m> block list set * int * int set)
	 * string set;

(* An alternating tree automaton:
 - First entry is a map from predicates (states) P and functions f to
 the set of all clauses of the form P(f(x1,...,xk)) <= body
 in the automaton.
 P and f are mapped to (blkls, k, {1, ..., k}),
 where k is the arity of f,
 and blkls is the set of all possible bodies.
 Each body is coded as a list of k blocks [B1, ..., Bk] and
 denotes B1(x1), ..., Bk(xk).
 - Second entry is a set of all universal states, i.e., of states P
 such that we have a clause P(x).
 *)

extern val auto_trim : automaton -> automaton;
	   (* removes empty states, and transitions leading to
	    universal states.  May not be exhaustive.
	    Should be exhaustive on non-alternating automata,
	    provided we understand universal states as those
	    that are in the univ [second] component of the automaton. *)

extern val auto_intersects : automaton -> string set -> bool;
(*
 Given an automaton, decides whether a given set of states
 has a non-empty intersection.
 *)

extern val auto_simple_inclusions : automaton ->
	   |[ pred_incl : string * string -> bool,
	      block_incl : block * block -> bool ]|;
	   (* auto_simple_inclusions a returns functions
	    testing inclusion of predicates, and of blocks.
	    pred_incl (P, Q):
	      if returns true then
		the language of P is a subset of that of Q in a;
              otherwise we don't know.
	    block_incl (blk1, blk2):
	      if returns true then
	        the intersection of languages of P, P in blk1,
	        is a subset of the intersection of languages of Q, Q in blk2;
	      otherwise we don't know.
	    Given a, auto_simple_inclusions a returns a memoizing function. *)

extern val auto_simplify : automaton * (block * block -> bool) -> automaton;
	   (* removes transitions subsumed by others.
	    Subsumption is decided here by calling second argument
	    on pairs of blocks, which is typically obtained as the
	    block_incl field of auto_simple_inclusions of the first
	    argument.
	    This should be called after auto_trim.
	    *)

extern val print_auto_clauses : 'a outstream * string * string
	   -> string * string * block list set * int -> unit;
(* print_auto (fd, xname, separ) (P, f, blkls, k)
 print all clauses P(f(X1,...,Xk)) :- blkl.
 where blkl in blks.
 Separates each clause with the string terminator.
*)

extern val print_auto : 'a outstream * string -> automaton -> unit;
(* print_auto (fd, xname) auto
 prints auto on file fd; variables are based on prefix xname.
 *)

extern val enrich_auto_eq : automaton -> automaton;
(* enrich_auto_eq auto
 adds all clauses of the form equal(X,Y) :- q(X), q(Y)
 to auto, where q ranges over the states of auto.
 The states are those predicates occurring in bodies of
 clauses of auto, but not in univ.
 This approximates equality, and should be exactly equality
 in the finite model M, when auto is the deterministic
 automaton representation of M. *)
