(* Compiling systems of linear equations and inequations to automata, headers.
   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.
*)

open "lin_h";

extern val lin_vars : ''var linear -> ''var set;
extern val linsys_vars : ''var linear set -> ''var set;

datatype lintype = LIN_NAT;

type ''var linstate = ''var list * ''var linear set;
(*
 The state ([x_{k+1}, ..., x_n], (sum_i a_ij x_i eqop_j b_j)_j)
 recognizes exactly those tuples (x_1, ..., x_n)
 such that base.sum_{i<=k} a_ij x_i + sum_{i>k}  a_ij x_i
   eqop_j b_j, for all j, where base is the current base (>=2).
 *)

datatype ''var linauto = LINAUTO of ''var linstate (* initial state *)
	 * (''var linstate -m> ''var linstate array)
	 (* transition function; each array contains n entries,
	  where n>=2 is the chosen base. *)
	 * ''var linstate set (* final states, i.e., those recognizing
			       the zero vector, with a null var list. *)
	 ;

extern val linsys_to_auto : (''_var -m> lintype) * lintype
	   * (''_var * ''_var -> bool) * int (* base *)
	   * ''_var linear set
	   -> ''_var linauto;

extern val print_lin_table : ('a outstream
			      * string (* prefix for state names *)
			      * string (* starting word (epsilon) *)
			      * string (* final predicate name *)
			      * string (* names of __cycle_<i> predicates *)
			      * int (* number base [the same as the one
				     given to linsys_to_auto above.
				     *)
			      * ''_var linauto) -> unit;
