(* 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 "linproto_h";
open "gensym_h";
open "sort_h";
open "rel_h";

fun lin_vars (LIN (row, ...)) =
    dom row;

fun linsys_vars lsys = union {lin_vars lin | lin in set lsys};

exception LinSysModEvt;

val lsys_false = {LIN ({}, EQ_OP, Int 1)};
val state_false = (nil, lsys_false);
val state_true = (nil, {});

fun linsys_to_auto (env : ''_var -m> lintype, deftype,
		    less : ''_var * ''_var -> bool, base, lsys : ''_var linear set) =
    let val vars = {x => deftype
		   | x in set linsys_vars lsys} ++ env
	val varl = sort less vars
	val trans = ref ({} : ''_var linstate -m> ''_var linstate array)
	val final = ref ({} : ''_var linstate set)

	fun mktrans (nil, lsys) =
	    (* current state is the set of all tuples (x_1, ..., x_n) such that
	     base.sum_{i<=n} a_ij x_i  eqop_j  b_j.
	     If base divides b_j, then this is equivalent to sum_{i<=n} a_ij x_i  eqop_j  b_j/base.
	     Otherwise, this is false (eqop_j=EQ_OP), true (eqop_j=NE_OP),
	     or equivalent to sum_{i<=n} a_ij x_i  eqop_j  floor(b_j/base) (eqop_j=LE_OP).
	     *)
	    let val lsys' = {if eqop=EQ_OP andalso r<>0 (* then row is false. *)
				 then raise LinSysModEvt
			     else LIN (row, eqop, q)
			    | LIN (row, eqop, b) in set lsys
				val (q, r) = zsdivmod (b, base)
				such that (* eliminate true rows. *)
				    not (eqop=NE_OP) orelse r=0
				    } handle LinSysModEvt => lsys_false
	    in
		if all (* final iff the 0 vector is solution of lsys (eqv., lsys'). *)
		    (case eqop of
			 EQ_OP => zsign b=0
		       | NE_OP => zsign b<>0
		       | LE_OP => zsign b>=0)
		   | LIN (row, eqop, b) in set lsys'
		   end
		    then final := !final U {(varl, lsys')}
		else ();
		    mktrans (varl, lsys')
	    end
	  | mktrans state =
	    if state inset !trans
		then state
	    else let val next = array (base, state_false) (* state_false is dummy here. *)
		     val ir = ref 0
		     val (xi::xl, lsys) = state (* x_i may be 0, 1, ..., base-1 plus base * x'_i *)
		 in
		     trans := !trans ++ {state => next};
		     iterate
		       let val i = !ir
			   val lsys' = {if xi inset row
					    then LIN (row, eqop, zsub (b, zsmul (?row xi, i)))
					else l
				       | l as LIN (row, eqop, b) in set lsys}
		       in
			   update (next, i, mktrans (xl, lsys'));
			   inc ir
		       end
		     |while !ir<base
		     end;
		     state
		 end
	fun inv_trans {} = {}
	  | inv_trans {q => qa} =
	    let val ir = ref 0
	    in
		{(qa.(!ir) before inc ir) => {q}
		|while !ir<base}
	    end
	  | inv_trans trans =
	    let val (trans1, trans2) = split trans
	    in
		inv_trans trans1 Urel inv_trans trans2
	    end
    in
	if null varl
	    then if
		all
		  (case eqop of
		       EQ_OP => zsign b=0
		     | NE_OP => zsign b<>0
		     | LE_OP => zsign b>=0)
		| LIN (row, eqop, b) in set lsys
		end
		     then LINAUTO (state_true, {}, {state_true})
		 else LINAUTO (state_false, {}, {})
	else let val init = mktrans (varl, lsys)
		 val invtrans = inv_trans (!trans)
		 fun reach (old, r) =
		     if old=r
			 then r
		     else let val new = r \ old
			  in
			      reach (r, r U union {preds
						  | q => preds in map new <| invtrans})
			  end
		 val can_reach_final = reach ({}, !final)
		 val reach_trans = can_reach_final <| !trans
		 fun state_false_q (nil, _) = (varl, lsys_false)
		   | state_false_q (xl, _) = (xl, lsys_false)
		 fun add_false_states (trans, nil) = trans
		   | add_false_states (trans, xl) =
		     let val q = (xl, lsys_false)
			 val nextq = state_false_q (tl xl, lsys_false)
			 val trans' = trans ++ {q => array (base, nextq)}
		     in
			 add_false_states (trans', tl xl)
		     end
		 val trans' = (iterate
				 let val ir = ref 0
				 in
				     while !ir<base do
					 (if qa.(!ir) inset can_reach_final
					      then ()
					  else qa.(!ir) .:= state_false_q (tl xl, lsys);
					      inc ir)
				 end
			       | q as (xl, lsys) => qa in map reach_trans
			       end;
				 add_false_states (reach_trans, varl))
	     in
		 LINAUTO (init, trans', !final)
	     end
    end;

fun print_lin_table (fd as |[put, ...]|, prefix, start, finalpred, _cycle,
		     base, LINAUTO (init, trans, final)) =
    let memofun qname q = gensym prefix
	(*
		qname (q as (xl, _)) =
		let val f as |[put, convert, ...]| = outstring prefix
		in
		    print f (pack (len xl));
		    put "_";
		    gensym (convert ())
		end
	 *)
	memofun cycle i =
		let val f as |[put, convert, ...]| = outstring _cycle
		in
		    print f (pack (i : int));
		    convert ()
		end
	val p = print fd
	val ir = ref 0
	val xls = ref {}
    in
	put "<?xml version=\"1.0\" encoding=\"UTF-8\"?>\n\
	 \<definitions/>\n";
	put "<states>\n";
	iterate
	  (put "  <state name=";
	   p (pack (qname q));
	   put ">";
	   if q inset final
	       then (put "<satisfies name=";
		     p (pack (finalpred : string));
		     put "/>")
	   else ();
	       put "<satisfies name=";
	       p (pack (cycle (len xl)));
	       put "/></state>\n";
	       xls := !xls U {xl})
	| q as (xl, _) in set trans
	end;
	   put "</states>\n<tables>\n  <table name=";
	   p (pack (start : string));
	   put " arity=\"0\">\n    <entry result=";
	   p (pack (qname init)); put "/>\n  </table>\n";
	   iterate
	     let val i = !ir
	     in
		 iterate
		   (put "  <table name=\"d";
		    p (pack n); put "_";
		    p (pack i);
		    put "\" arity=\"1\">\n";
		    iterate
		      let val qn = qname q
		      in
			  put "    <entry result=";
			  p (pack (qname (qa.(i))));
			  put "><arg name=";
			  p (pack qn);
			  put "/></entry>\n"
		      end
		    | q => qa in map trans
		      such that #1 q = xl
		    end;
		    put "  </table>\n")
		 | xl in set !xls
		 val n = len xl
		 end;
		 inc ir
	     end
	   |while !ir<base
	   end;
	   put "</tables>\n"
    end;

