(* Parser for systems of linear equations and inequations.
   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.
*)

%{

fun linearexpr_add ((row1, c1), (row2, c2)) =
    ((row1 delta row2) ++ {x => zadd (a1, ?row2 x)
			  | x => a1 in map row2 <| row1},
	 zadd (c1, c2));

fun linearexpr_sub ((row1, c1), (row2, c2)) =
    ((row2 <-| row1) ++ {x => zsub (if x inset row1
					then ?row1 x
				    else Int 0,
					a2)
			| x => a2 in map row2},
	 zsub (c1, c2));

exception LinearExprTimesEvt;

fun linearexpr_times (({}, c1), (row2, c2)) =
    if c1=Int 0
	then ({}, c1)
    else ({x => zmul (c1, a)
	  | x => a in map row2},
	    zmul (c1, c2))
  | linearexpr_times (e1, e2 as ({}, _)) =
    linearexpr_times (e2, e1)
  | linearexpr_times _ =
    raise LinearExprTimesEvt;

fun linearexpr_neg (row, c) =
    ({x => zneg a
     | x => a in map row},
       zneg c);

  %}

%header {
  open "lin_h";
  %}

%union {
  linearnone of unit
| linearint of Int
| linearstring of string
| linearexpr of string row * Int
| linear of string linear
| linearproblem of string linear set
}

%start problem

%type <linearproblem> problem
%type <linear> row
%type <linearexpr> expr

%token <linearint> integer_constant
%token kw_open_paren kw_close_paren kw_comma
%token <linearstring> VAR

%token kw_equal kw_ne kw_le kw_lt kw_ge kw_gt
%left kw_minus kw_plus
%left kw_times
%left NEG

%%

problem : { $$ {} }
| row { $$ {$1} }
| problem kw_comma row { $$ ($1 U {$3}) }
;

row : expr kw_equal expr { let val (row, c) = linearexpr_sub ($1, $3)
			   in
			       $$ (LIN (row, EQ_OP, zneg c))
			   end }
| expr kw_ne expr { let val (row, c) = linearexpr_sub ($1, $3)
		    in
			$$ (LIN (row, NE_OP, zneg c))
		    end }
| expr kw_le expr { let val (row, c) = linearexpr_sub ($1, $3)
		    in
			$$ (LIN (row, LE_OP, zneg c))
		    end }
| expr kw_lt expr { let val (row, c) = linearexpr_sub ($1, $3)
		    in
			$$ (LIN (row, LE_OP, zneg (zsadd (c, 1))))
		    end }
| expr kw_ge expr { let val (row, c) = linearexpr_sub ($3, $1)
		    in
			$$ (LIN (row, LE_OP, zneg c))
		    end }
| expr kw_gt expr { let val (row, c) = linearexpr_sub ($3, $1)
		    in
			$$ (LIN (row, LE_OP, zneg (zsadd (c, 1))))
		    end }
;

expr : integer_constant { $$ ({}, $1) }
| VAR { $$ ({$1 => Int 1}, Int 0) }
| expr kw_plus expr { $$ (linearexpr_add ($1, $3)) }
| expr kw_minus expr { $$ (linearexpr_sub ($1, $3)) }
| expr kw_times expr { $$ (linearexpr_times ($1, $3))
		       handle LinearExprTimesEvt =>
		       (#put stderr "Error: non-Presburger expression (one side of the multiplication\
			\ should be constant).\n";
		       gyacc_error) }
| kw_minus expr %prec NEG { $$ (linearexpr_neg $2) }
| kw_open_paren expr kw_close_paren { $$ $2 }
;
