(* Parser for alternating tree automata in Prolog format.
   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 "yyerror_h";

  val ploc = print_yyloc stderr;
  val head_free_vars = ref ({} : string set);
  exception BadArityEvt of int;
  %}

%header{
open "auto_h";
  %}

%union {
  aplnone of unit
| aplstring of string
| aplauto of automaton
| aplautoclause of string * string * block list
| apl0atom of string * string
| apl0atoms of string -m> string set
| apl1atom of string * (string * string list)
| aplflat of string * string list
| aplvars of string list
}

%start clause_list

%type <aplauto> clause_list
%type <aplstring> univ_clause
%type <aplautoclause> auto_clause
%type <apl0atoms> clause_body non_empty_clause_body
%type <apl0atom> depth_zero_atom body_atom
%type <apl1atom> depth_one_atom
%type <aplflat> flat_term
%type <aplvars> distinct_var_list var_list

%token <aplstring> identifier abbrv
%token kw_open_paren kw_close_paren kw_provided kw_comma kw_period kw_question_mark
%token <aplstring> VAR
%%

clause_list : { $$ (AUTO ({}, {})) }
| clause_list univ_clause { let val AUTO (auto, univ) = $1
			    in
				$$ (AUTO (auto, univ U {$2}))
			    end }
| clause_list auto_clause
{
  let val AUTO (auto, univ) = $1
      val (P, f, blkl) = $2
      val k = len blkl
  in
      let val auto' =
	      if P inset auto
		  then let val fmap = ?auto P
		       in
			   if f inset fmap
			       then let val (blkls, k1, vars) = ?fmap f
				    in
					if k1<>k
					    then raise BadArityEvt k1
					else auto ++ {P => fmap ++ {f => (blkls U {blkl}, k, vars)}}
				    end
			   else auto ++ {P => fmap ++ {f => ({blkl}, k, 1 to k)}}
		       end
	      else auto ++ {P => {f => ({blkl}, k, 1 to k)}}
      in
	  $$ (AUTO (auto', univ))
      end handle BadArityEvt k1 => (#put stderr "Line "; ploc @2;
				    #put stderr ": function ";
				    #put stderr f;
				    #put stderr " used to be of arity ";
				    print stderr (pack k1);
				    #put stderr " is applied to ";
				    print stderr (pack k);
				    #put stderr " arguments. ";
				    gyacc_error)
  end
}
;

univ_clause : depth_zero_atom kw_period { let val (P, x) = $1 in $$ P end }
;

auto_clause :
  depth_one_atom kw_period { let val (P, (f, xl)) = $1
			     in
				 $$ (P, f, [{} | _ in list xl])
			     end }
| depth_one_atom kw_provided clause_body kw_period
  { let val (P, (f, xl)) = $1
	val k = len xl
    in
	$$ (P, f, [if x inset $3
		       then ?$3 x
		   else {}
		  | x in list xl])
    end }
;

clause_body : { $$ {} }
| non_empty_clause_body { $$ $1 }
;

non_empty_clause_body : body_atom { let val (P, x) = $1
				    in
					$$ {x => {P}}
				    end }
| non_empty_clause_body kw_comma body_atom { let val (P, x) = $3
					     in
						 if x inset $1
						     then $$ ($1 ++ {x => ?$1 x U {P}})
						 else $$ ($1 ++ {x => {P}})
					     end }
;

body_atom : depth_zero_atom { let val (P, x) = $1
			      in
				  if x inset !head_free_vars
				      then $$ $1
				  else (#put stderr "Line "; ploc @1;
					#put stderr ": variable ";
					#put stderr x;
					#put stderr " is free in the body but not in the head. ";
					gyacc_error)
			      end }
;

depth_zero_atom : identifier kw_open_paren VAR kw_close_paren { $$ ($1, $3) }
| identifier VAR { $$ ($1, $2) }
;

depth_one_atom : identifier kw_open_paren flat_term kw_close_paren
{  head_free_vars := elems (#2 $3);
  $$ ($1, $3) }
| identifier flat_term { head_free_vars := elems (#2 $2);
			 $$ ($1, $2) }
| identifier { head_free_vars := {}; $$ ($1, ("#" ^ $1, nil)) }
| identifier kw_open_paren VAR kw_comma distinct_var_list kw_close_paren
{ if $3 inset elems $5
      then (#put stderr "Line "; ploc @3;
	    #put stderr ": duplicate variable ";
	    #put stderr $3;
	    #put stderr " in head. ";
	    gyacc_error)
  else let val args = $3 :: $5
       in
	   head_free_vars := elems args;
	   $$ ($1, ("#" ^ $1, args))
       end }
| abbrv { head_free_vars := {}; $$ ($1, ($1 ^ "_fun", nil)) }
| abbrv kw_open_paren distinct_var_list kw_close_paren
{ head_free_vars := elems $3; $$ ($1, ($1 ^ "_fun", $3)) }
;

flat_term : identifier { $$ ($1, nil) }
| identifier kw_open_paren distinct_var_list kw_close_paren { $$ ($1, $3) }
;

distinct_var_list : var_list
{
  let exception RevDistinctEvt of string
      fun rev_distinct (nil, acc, _) = acc
	| rev_distinct (x::xl, acc, vars) =
	  if x inset vars
	      then raise RevDistinctEvt x
	  else rev_distinct (xl, x::acc, vars U {x})
  in
      $$ (rev_distinct ($1, nil, {}))
      handle RevDistinctEvt x =>
      (#put stderr "Line "; ploc @1;
       #put stderr ": duplicate variable ";
       #put stderr x;
       #put stderr " in head. ";
       gyacc_error)
  end
}
;

var_list : VAR { $$ [$1] }
| var_list kw_comma VAR { $$ ($3::$1) }
;
