(* Parser for models in Paradox format.
   Copyright (C) 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 "yyerror_h";

%}

%union {
  state of block
| statelist of block list
| term of term
| line of string * block_list * block
}

%start model

%type <fmodel> model
%type <state> state
%type <statelist> state_list
%type <term> term
%type <line> def

%token <string> identifier value

%%

model : def_list
;

(* def_list is reversed *)
def_list : { $$ {} }
| def_list def { let val (P, 
;

def : term kw_equal state { let val f $ l = $1
			    in
				(f, l, $3)
			    end
			    }
| term kw_iff kw_true
| term kw_iff kw_false
;

term : identifier { $$ ($1 $ nil) }
| identifier kw_open_paren state_list kw_close_paren { $$ ($1 $ (rev $3)) };

(* state_list is reversed *)
state_list : state { $$ [$1] }
| state_list kw_comma state { $$ ($3 :: $1) }
;

state : value { $$ {$1} }
;
