(* spi-calculus-like process parser.
   Copyright (C) 2004 Jean Goubault-Larrecq and LSV, CNRS UMR 8643 & ENS Cachan
   and INRIA Futurs projet SECSI.

   This file is part of ispi.

   ispi 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.

   ispi 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 ispi; see the file COPYING.  If not, write to
   the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.
*)

  %{
  open "yyerror_h";
  open "gensym_h";

  val constructors = ref ({"0", "s"
			      (*, "nil", "cons"*)
			      } : string set);
  val |[ matches = cons_matches, subst = cons_subst, ... ]| = regexp "^__c"; (*"^t([0-9]+)$";*)

  val private_funs = ref ({"__eq", "__nu"});

  val funs = ref ({"crypt" => 2,
		     "acrypt" => 2,
		     "__eq" => 1,
		     "pub" => 1,
		     "prv" => 1,
		     "0" => 0,
		     "s" => 1,
		      "__nu" => 2 (*,
				   "nil" => 0,
				   "cons" => 2 *)} : string -m> int);

  fun is_constructor f =
      f inset !constructors orelse cons_matches f;

  fun is_fun f =
      f inset !funs orelse cons_matches f;

  fun fun_arity f =
      if cons_matches f
	  then intofstring (cons_subst "\\1")
      else ?(!funs) f;

  val procs = ref ({"dy_synthesizer" => 2, "dy_analyzer" => 2} : string -m> int);
  val expected_procs = ref ({} : string -m> int);

  fun copy_loc loc =
      let val loc' = iarray (4, 0)
      in
	  iupdate (loc', 0, isub (loc,0));
	  iupdate (loc', 1, isub (loc,1));
	  iupdate (loc', 2, isub (loc,2));
	  iupdate (loc', 3, isub (loc,3));
	  loc'
      end;

  val ploc = print_yyloc stderr;
  fun ploc2 (loc1, loc2) =
      let val loc = iarray(4,0)
      in
	  iupdate (loc, 0, isub (loc1,0));
	  iupdate (loc, 1, isub (loc1,1));
	  iupdate (loc, 2, isub (loc2,2));
	  iupdate (loc, 3, isub (loc2,3));
	  ploc loc
      end
  val eput = #put stderr;
  val eflush = #flush stderr;

  fun loc_proc_2 (loc1, loc2, proc) =
    (proc, isub (loc1, 0), isub (loc1, 1), isub (loc2, 2), isub (loc2, 3));
  fun loc_proc (loc, proc) =
    loc_proc_2 (loc, loc, proc);
  fun loc_proc_end (loc, proc) =
    (proc, isub (loc, 2), isub (loc, 3), isub (loc, 2), isub (loc, 3));

  fun M_i i =
      let val f as |[convert, ...]| = outstring "M"
      in
	  print f (pack (i:int));
	  convert ()
      end;

  fun in_vars (i, k, loc, args, f) =
      if i=k
	  then f (rev args)
      else
	  let val Mi = M_i (i+1)
	  in
	      loc_proc (loc, SPI_IN (SPI_VAR "c_in", Mi,
				     in_vars (i+1, k, loc, Mi::args, f)))
	  end;

  val dummy_loc = iarray (4, 0);

  fun f_synthesizer (f, loc, k) =
      in_vars (0, k, loc, nil,
	       fn args => loc_proc (loc, SPI_OUT (SPI_VAR "c_out",
						  SPI_APPL (f,
							    [SPI_VAR x
							    | x in list args]),
						  loc_proc (loc, SPI_ZERO))));

  val synthesizer = ref ([f_synthesizer (f, dummy_loc, k)
			 | f => k in map !private_funs <-| !funs])

  fun vars_upto k =
      let val ir = ref 0
      in
	  [(inc ir; M_i (!ir))
	  |while !ir<k]
      end;

  fun spi_par (loc, nil) = loc_proc (loc, SPI_ZERO)
    | spi_par (_, [proc]) = proc
    | spi_par (loc, procs) = loc_proc (loc, SPI_PAR procs)

  fun f_analyzer (f, loc, k) =
      let val vars = vars_upto k
	  val stop = loc_proc (loc, SPI_ZERO)
      in
	  loc_proc (loc,
		    SPI_IN (SPI_VAR "c_in", "M",
			    loc_proc (loc,
				      SPI_DESTRUCT (SPI_VAR "M", f, vars,
						    spi_par (loc,
							     [loc_proc (loc,
									SPI_OUT (SPI_VAR "c_out", SPI_VAR Mi,
										 stop))
							     | Mi in list vars]),
						    stop))))
      end;

  val stop = loc_proc (dummy_loc, SPI_ZERO);

  val analyzer =
      ref (loc_proc (dummy_loc,
		     SPI_IN (SPI_VAR "c_in", "M",
			     loc_proc (dummy_loc,
				       SPI_IN (SPI_VAR "c_in", "M2",
					       loc_proc (dummy_loc,
							 SPI_DECRYPT_SYM (SPI_VAR "M",
									  "M1",
									  SPI_VAR "M2",
									  loc_proc (dummy_loc,
										    SPI_OUT (SPI_VAR "c_out",
											     SPI_VAR "M1",
											     stop)),
									  stop)))))) ::
	   loc_proc (dummy_loc,
		     SPI_IN (SPI_VAR "c_in", "M",
			     loc_proc (dummy_loc,
				       SPI_IN (SPI_VAR "c_in", "M2",
					       loc_proc (dummy_loc,
							 SPI_DECRYPT_ASYM (SPI_VAR "M",
									   "M1",
									   SPI_VAR "M2",
									   loc_proc (dummy_loc,
										     SPI_OUT (SPI_VAR "c_out",
											      SPI_VAR "M1",
											      stop)),
									   stop)))))) ::
	   [f_analyzer (f, dummy_loc, k)
	   | f => k in map !constructors <| !funs])
  fun newvar loc =
      let val f as |[put, convert, ...]| = outstring "__Z_"
      in
	  print f (pack (isub (loc, 0)));
	  put "_";
	  print f (pack (isub (loc, 1)));
	  put "_";
	  print f (pack (isub (loc, 2)));
	  put "_";
	  print f (pack (isub (loc, 3)));
	  convert ()
      end;

  fun var_of_term (SPI_VAR x) = x
    | var_of_term t = gensym "__Var_"
(*
      let val f = outstring "__Var_"
      in
	  print_spi_term (mangle f) t;
	  #convert f ()
      end
*)

    (*
  fun tuple l =
    let val f as |[convert, ...]| = outstring "t"
    in
      print f (pack (len l));
      SPI_APPL (convert (), l)
    end;
     *)

  fun tuple nil = SPI_APPL ("nil", nil)
    | tuple (t::l) = SPI_APPL ("cons", [t, tuple l]);

  fun fv (SPI_VAR x) = {x}
    | fv (SPI_APPL (_, l)) = union {fv t | t in list l};

  fun pat_bv (SPI_VAR x) = {x}
    | pat_bv (SPI_APPL ("__eq", [_])) = {}
    | pat_bv (SPI_APPL ("crypt", [pat, t])) = pat_bv pat
    | pat_bv (SPI_APPL ("acrypt", [pat, t])) = pat_bv pat
    | pat_bv (SPI_APPL (f, l)) = patl_bv l
  and patl_bv l = union {pat_bv pat | pat in list l};

  fun pat_fv (SPI_VAR _) = {}
    | pat_fv (SPI_APPL ("__eq", [t])) = fv t
    | pat_fv (SPI_APPL ("crypt", [pat, t])) = pat_fv pat U fv t
    | pat_fv (SPI_APPL ("acrypt", [pat, t])) = pat_fv pat U fv t
    | pat_fv (SPI_APPL (f, l)) = patl_fv l
  and patl_fv l = union {pat_fv pat | pat in list l};

  fun mk_vars args =
      let val alreadyseen = ref ({} : string set)
	  val vars = [let val var = ref (var_of_term t)
		      in
			  while !var inset !alreadyseen
			      do var := !var ^ "'";
			      !var
		      end
		     | t in list args]
      in
	  vars
      end;

  fun mk_let (loc, var :: othervars, arg :: otherargs, p) =
      if arg=SPI_VAR var
	  then mk_let (loc, othervars, otherargs, p)
      else loc_proc_end (loc, SPI_LET (var, arg,
				       mk_let (loc, othervars, otherargs, p)))
    | mk_let (_, _, _, p) = p

  exception MkIf;

  fun mk_if (SPI_DIFF (t, u), thenb, elseb) =
      mk_if (SPI_EQ (t, u), elseb, thenb)
    | mk_if (SPI_EQ (t, u), thenb, elseb) =
      SPI_IF (t, u, thenb, elseb)
    | mk_if arg = raise MkIf;

  exception MkPatsMatch;

  fun mk_pat_match (loc, pat as SPI_VAR x, u, thenb, elseb) =
      if pat=u
	  then thenb
      else loc_proc_end (loc, SPI_LET (x, u, thenb))
    | mk_pat_match (loc, SPI_APPL ("crypt", [pat, k]), u, thenb, elseb) =
      let val x = var_of_term pat
      in
	  loc_proc_end (loc, SPI_DECRYPT_SYM (u, x, k,
					      mk_pat_match (loc, pat,
							    SPI_VAR x, thenb, elseb),
					      elseb))
      end
    | mk_pat_match (loc, SPI_APPL ("acrypt", [pat, k]), u, thenb, elseb) =
      let val x = var_of_term pat
      in
	  loc_proc_end (loc, SPI_DECRYPT_ASYM (u, x, k,
					       mk_pat_match (loc, pat,
							     SPI_VAR x, thenb, elseb),
					       elseb))
      end
    | mk_pat_match (loc, SPI_APPL ("__eq", [t]), u, thenb, elseb) =
      loc_proc_end (loc, mk_if (SPI_EQ (t, u), thenb, elseb))
    | mk_pat_match (loc, SPI_APPL (f, pats), u, thenb, elseb) =
      let val vars = mk_vars pats
      in
	  loc_proc_end (loc, SPI_DESTRUCT (u, f, vars,
					   mk_pats_match (loc, pats,
							  [SPI_VAR x | x in list vars],
							  thenb, elseb),
					   elseb))
      end
  and mk_pats_match (_, nil, nil, thenb, _) = thenb
    | mk_pats_match (loc, pat::pats, u::us, thenb, elseb) =
      mk_pat_match (loc, pat, u,
		    mk_pats_match (loc, pats, us, thenb, elseb), elseb)
    | mk_pats_match arg = raise MkPatsMatch;

  %}

%union {
  spinone of unit
| st of spi_term
| stl of spi_term list
| sf of spi_fact
| sp of located_process
| spl of located_process list
| sd of spi_declaration
| sdl of spi_declaration list
| scase of (spi_term * located_process -> located_process)
| spi of spi_program
| string of string
| sb of bool
}

%start spi

%type <spi> spi

%type <st> term term_sequence pattern pattern_sequence
%type <stl> optional_args
%type <stl> term_list pattern_list
%type <sf> fact
%type <sp> process atomic_process continuation
%type <spl> process_list
%type <sd> single_proc_declaration
%type <sdl> declaration proc_declaration
%type <sdl> declaration_list
%type <scase> matches
%type <string> bang
%type <spinone> proc
%type <string> id_or_var
%type <sb> fun data

%token <string> identifier VAR kw_slash
%token kw_open_paren kw_close_paren kw_open_bracket kw_close_bracket
%token kw_open_curly kw_close_curly
%token kw_comma kw_semicolon kw_period kw_equal kw_different kw_bang kw_zero kw_new
%token kw_if kw_of kw_then kw_else kw_in kw_out kw_let kw_case kw_par kw_event kw_proc
%token kw_implies kw_any kw_data kw_fun kw_private kw_and kw_eof

%expect 3

%%

spi : declaration_list
{ let val procs = {f => (args, p)
		  | SPI_PROC (f, args, p) in list $1}
  in
      if "main" inset procs
	  then $$ |[funs = !funs,
		    constructors = !constructors,
		    processes = procs ++
		    {"dy_synthesizer" => (["c_in", "c_out"],
					    spi_par (dummy_loc, !synthesizer)),
		     "dy_analyzer" => (["c_in", "c_out"],
					 spi_par (dummy_loc, !analyzer))}
		    ]|
      else (eput "Line "; ploc @1;
	    eput ": identifier 'main' undefined. ";
	    hyacc_error)
  end
}
;

term : identifier
{ if is_fun $1
      then let val expected_n = fun_arity $1
	   in
	       if expected_n <> 0
		   then (eput "Line "; ploc @1;
			 eput ": identifier ";
			 eput $1;
			 eput " expects ";
			 print stderr (pack expected_n);
			 eput (if expected_n<=1 then " argument" else " arguments");
			 eput ", got none. ";
			 hyacc_error)
	       else $$ (SPI_APPL ($1, nil))
	   end
  else (eput "Line "; ploc @1;
	eput ": identifier ";
	eput $1;
	eput " undeclared. ";
	hyacc_error)
}
| identifier kw_open_paren term_list kw_close_paren
{ if is_fun $1
      then let val n = len $3
	       val expected_n = fun_arity $1
	   in
	       if expected_n <> n
		   then (eput "Line "; ploc @1;
			 eput ": identifier ";
			 eput $1;
			 eput " expects ";
			 print stderr (pack expected_n);
			 eput (if expected_n<=1 then " argument" else " arguments");
			 eput ", got ";
			 print stderr (pack n);
			 eput ". ";
			 hyacc_error)
	       else $$ (SPI_APPL ($1, rev $3))
	   end
  else (eput "Line "; ploc @1;
	eput ": identifier ";
	eput $1;
	eput " undeclared. ";
	hyacc_error)
}
| kw_open_paren term_sequence kw_close_paren { $$ $2 }
| kw_open_curly term_sequence kw_close_curly term
{ $$ (SPI_APPL ("crypt", [$2, $4])) }
(* crypt is symmetric encryption. *)
| kw_open_bracket term_sequence kw_close_bracket term
{ $$ (SPI_APPL ("acrypt", [$2, $4])) }
(* acrypt is asymmetric encryption; the notation used is reminiscent of signatures. *)
| VAR { $$ (SPI_VAR $1) }
;

term_sequence : term_list
{ $$ (case $1 of
      nil => tuple nil
    | [t] => t
      | l => tuple (rev l))
    }
;

(* term_list is a reversed list of terms *)
term_list : term { $$ [$1] }
| term_list kw_comma term { $$ ($3::$1) }
;

bang : kw_bang { $$ "Pid" } (* current pid *)
     | kw_bang kw_open_bracket VAR kw_close_bracket { $$ $3 }
;

optional_semicolon : optional_semicolon kw_semicolon
|
;

fact : term kw_equal term { $$ (SPI_EQ ($1, $3)) }
| term kw_different term { $$ (SPI_DIFF ($1, $3)) }
;

pattern : identifier
{ if is_constructor $1
      then let val expected_n = fun_arity $1
	   in
	       if expected_n <> 0
		   then (eput "Line "; ploc @1;
			 eput ": identifier ";
			 eput $1;
			 eput " expects ";
			 print stderr (pack expected_n);
			 eput (if expected_n<=1 then " argument" else " arguments");
			 eput ", got none. ";
			 hyacc_error)
	       else $$ (SPI_APPL ($1, nil))
	   end
  else (eput "Line "; ploc @1;
	eput ": identifier ";
	eput $1;
	eput " undeclared. ";
	hyacc_error)
}
| identifier kw_open_paren pattern_list kw_close_paren
{ if is_constructor $1
      then let val n = len $3
	       val expected_n = fun_arity $1
	   in
	       if expected_n <> n
		   then (eput "Line "; ploc @1;
			 eput ": identifier ";
			 eput $1;
			 eput " expects ";
			 print stderr (pack expected_n);
			 eput (if expected_n<=1 then " argument" else " arguments");
			 eput ", got ";
			 print stderr (pack n);
			 eput ". ";
			 hyacc_error)
	       else $$ (SPI_APPL ($1, rev $3))
	   end
  else (eput "Line "; ploc @1;
	eput ": identifier ";
	eput $1;
	eput " undeclared. ";
	hyacc_error)
}
| kw_equal term { $$ (SPI_APPL ("__eq", [$2])) }
| kw_any { $$ (SPI_VAR (newvar @1)) }
| kw_open_paren pattern_sequence kw_close_paren { $$ $2 }
| kw_open_curly pattern_sequence kw_close_curly term
  { case pat_bv $2 & fv $4 of
	{x, ...} => (eput "Line "; ploc2 (@1, @4);
		     eput ": ambiguous pattern, variable ";
		     eput x;
		     eput " occurs both bound by plaintext pattern and free in key. ";
		     hyacc_error)
      | _ => $$ (SPI_APPL ("crypt", [$2, $4])) }
| kw_open_bracket pattern_sequence kw_close_bracket term
  { case pat_bv $2 & fv $4 of
	{x, ...} => (eput "Line "; ploc2 (@1, @4);
		     eput ": ambiguous pattern, variable ";
		     eput x;
		     eput " occurs both bound by plaintext pattern and free in key. ";
		     hyacc_error)
      | _ => $$ (SPI_APPL ("acrypt", [$2, $4])) }
| VAR { $$ (SPI_VAR $1) }
;

pattern_sequence : pattern_list
{ $$ (case $1 of
      nil => tuple nil
    | [t] => t
      | l => tuple (rev l))
    }
;

(* pattern_list is a reversed list of patterns *)
pattern_list : pattern { $$ [$1] }
| pattern_list kw_comma pattern { case patl_bv $1 & pat_bv $3 of
				      {x, ...} => (eput "Line "; ploc @3;
						   eput ": non-linear pattern, variable ";
						   eput x;
						   eput " occurs already at line ";
						   ploc @1; eput ". ";
						   hyacc_error)
				    | _ =>
				      (case patl_bv $1 & pat_fv $3 of
					   {x, ...} => (eput "Line "; ploc @1;
							eput ": ambiguous pattern, variable ";
							eput x;
							eput " occurs both bound in pattern\
							 \ and free at line ";
							ploc @3; eput ". ";
							hyacc_error)
					 | _ => (case patl_fv $1 & pat_bv $3 of
						     {x, ...} => (eput "Line "; ploc @3;
								  eput ": ambiguous pattern, \
								  \variable ";
								  eput x;
								  eput " occurs both bound in\
								   \ pattern and free at line ";
								  ploc @1; eput ". ";
								  hyacc_error)
						   | _ => $$ ($3::$1))) }
;

continuation : { $$ (loc_proc_end (@0, SPI_ZERO)) }
| atomic_process { $$ $1 }
| kw_semicolon optional_semicolon atomic_process { $$ $3 }
| kw_semicolon optional_semicolon { $$ (loc_proc_end (@1, SPI_ZERO)) }
;

atomic_process : kw_open_paren process kw_close_paren optional_semicolon { $$ $2 }
| id_or_var optional_semicolon
  {
   let val n = if $1 inset !procs
		   then ?(!procs) $1
	       else if $1 inset !expected_procs
		   then ?(!expected_procs) $1
	       else (expected_procs := {$1 => 0};
		     0)
   in
       if n=0
	     then $$ (loc_proc (@1, SPI_CALL ($1, nil)))
       else (eput "Line "; ploc @2;
	     eput ": expected ";
	     print stderr (pack n);
	     eput (if n<=1 then " argument" else " arguments");
	     eput ", got none. ";
	     hyacc_error)
   end
   }
| id_or_var kw_open_paren term_list kw_close_paren optional_semicolon
  { let val args = rev $3
	val nargs = len args
	val n = if $1 inset !procs
		    then ?(!procs) $1
		else if $1 inset !expected_procs
		    then ?(!expected_procs) $1
		else (expected_procs := {$1 => nargs};
		      nargs)
    in
       if n=nargs
	     then $$ (loc_proc_2 (@1, @4, SPI_CALL ($1, args)))
       else (eput "Line "; ploc @2;
	     eput ": expected ";
	     print stderr (pack n);
	     eput (if n<=1 then " argument" else " arguments");
	     eput ", got ";
	     print stderr (pack nargs);
	     eput ". ";
	     hyacc_error)
    end }
| bang atomic_process { $$ (loc_proc_2 (@1, @1, SPI_BANG ($1, $2))) }
| kw_zero optional_semicolon { $$ (loc_proc (@1, SPI_ZERO)) }
| kw_new VAR continuation { $$ (loc_proc_2 (@1, @2, SPI_NEW ($2, $3))) }
| kw_if fact kw_then atomic_process
{ $$ (loc_proc_2 (@1, @2, mk_if ($2, $4, loc_proc_end (@4, SPI_ZERO)))) }
| kw_if fact kw_then atomic_process kw_else atomic_process
{ $$ (loc_proc_2 (@1, @2, mk_if ($2, $4, $6))) }
| kw_in kw_open_paren term kw_comma pattern_sequence kw_close_paren continuation
{ let val x = var_of_term $5
  in
    $$ (loc_proc_2 (@1, @6,
		    SPI_IN ($3, x, mk_pat_match (@6, $5, SPI_VAR x, $7,
						 loc_proc_end (@6, SPI_ZERO)))))
  end }
| kw_out kw_open_paren term kw_comma term_sequence kw_close_paren continuation
{ $$ (loc_proc_2 (@1, @6, SPI_OUT ($3, $5, $7))) }
| kw_let pattern_list kw_equal term_list kw_in atomic_process
{ let val patlen = len $2
      val tlen = len $4
  in
      if patlen<>tlen
	  then (eput "Line "; ploc @4;
		eput ": expecting ";
		print stderr (pack patlen);
		eput (if patlen<=1 then " term" else " terms");
		eput ", got ";
		print stderr (pack tlen);
		eput ". ";
		hyacc_error)
      else $$ (loc_proc_2 (@1, @4,
			   #1 (mk_pats_match (@5, $2, $4, $6,
					      loc_proc_end (@6, SPI_ZERO)))))
  end
 }
| kw_let pattern_list kw_equal term_list kw_in atomic_process kw_else atomic_process
{ let val patlen = len $2
      val tlen = len $4
  in
      if patlen<>tlen
	  then (eput "Line "; ploc @4;
		eput ": expecting ";
		print stderr (pack patlen);
		eput (if patlen<=1 then " term" else " terms");
		eput ", got ";
		print stderr (pack tlen);
		eput ". ";
		hyacc_error)
      else $$ (loc_proc_2 (@1, @4,
			   #1 (mk_pats_match (@5, $2, $4, $6, $8))))
  end
 }
| kw_case term_sequence kw_of matches
{ $$ ($4 ($2, loc_proc_end (@4, SPI_ZERO))) }
(*
| kw_event term continuation
{ $$ (loc_proc_2 (@1, @2, SPI_EVT ($2, $3))) }
*)
;

matches : pattern_sequence kw_implies atomic_process
{ let val loc1 = @1
      val loc2 = @2
  in
      $$ (fn (u, cont) => loc_proc_2 (loc1, loc2,
				      #1 (mk_pat_match (loc2, $1, u, $3, cont))))
  end }
| matches kw_else pattern_sequence kw_implies atomic_process
{ let val loc1 = @3
      val loc2 = @4
  in
      $$ (fn (u, cont) => $1 (u, loc_proc_2 (loc1, loc2,
					     #1 (mk_pat_match (loc2, $3, u, $5, cont)))))
  end }
;

process : process_list { case $1 of
			     [p] => $$ p
			   | _ => $$ (spi_par (@1, rev $1)) }
;

(* process_lists are reversed lists of processes. *)
process_list : atomic_process { $$ [$1] }
| process_list kw_par atomic_process { $$ ($3::$1) }
;

proc : kw_proc { expected_procs := {}; $$ () }
;

single_proc_declaration : id_or_var optional_args kw_equal process
{ if $1 inset !procs
      then (eput "Line "; ploc @1;
	    eput ": attempt to redefine process ";
	    eput $1;
	    eput ". ";
	    hyacc_error)
  else let val nargs = len $2
	   val vars = mk_vars $2
       in
	   if $1 inset !expected_procs
	       then let val n = ?(!expected_procs) $1
		    in
			if n=nargs
			    then (procs := !procs ++ {$1 => n};
				  expected_procs := {$1} <-| !expected_procs;
				  $$ (SPI_PROC ($1, vars,
						mk_pats_match (@3, $2,
							       [SPI_VAR x | x in list vars],
							       $4,
							       loc_proc_end (@4,
									     SPI_ZERO)))))
			else (eput "Line "; ploc @1;
			      eput ": was used previously on ";
			      print stderr (pack n);
			      eput (if n<=1 then " argument" else " arguments");
			      eput ", defined here as taking ";
			      print stderr (pack nargs);
			      eput ". ";
			      hyacc_error)
		    end
	   else (procs := !procs ++ {$1 => nargs};
		 $$ (SPI_PROC ($1, vars,
			       mk_pats_match (@3, $2,
					      [SPI_VAR x | x in list vars],
					      $4, loc_proc_end (@4, SPI_ZERO)))))
       end
}
;

proc_declaration : single_proc_declaration { $$ [$1] }
| proc_declaration kw_and single_proc_declaration { $$ ($3::$1) }
;

declaration : proc proc_declaration
{ (case !expected_procs of
       {} => $$ $2
     | {f => _, ...} => (eput "Line "; ploc2 (@1, @2);
			 eput ": process ";
			 eput f;
			 eput " called, not defined. ";
			 hyacc_error))
}
| data id_or_var kw_slash optional_semicolon
{ if is_fun $2
      then (eput "Line "; ploc @2;
	    eput ": identifier ";
	    eput $2;
	    eput " already declared, redeclaration ignored. ";
	    hyacc_error)
  else let val n = intofstring (substr ($3, 1, size $3))
       in
	   funs := !funs ++ {$2 => n};
	   constructors := !constructors ++ {$2};
	   if $1
	       then private_funs := !private_funs U {$2}
	   else (synthesizer := f_synthesizer ($2, @2, n) :: !synthesizer;
		 analyzer := f_analyzer ($2, @2, n) :: !analyzer);
	   $$ nil
       end
}
| fun id_or_var kw_slash optional_semicolon
{ if is_fun $2
      then (eput "Line "; ploc @2;
	    eput ": identifier ";
	    eput $2;
	    eput " already declared, redeclaration ignored. ";
	    hyacc_error)
  else let val n = intofstring (substr ($3, 1, size $3))
       in
	   funs := !funs ++ {$2 => n};
	   if $1
	       then private_funs := !private_funs U {$2}
	   else synthesizer := f_synthesizer ($2, @2, n) :: !synthesizer;
	   $$ nil
       end
}
;

fun : kw_fun { $$ false }
| kw_private kw_fun { $$ true }
;

data : kw_data { $$ false }
| kw_private kw_data { $$ true }
;

id_or_var : identifier { $$ $1 }
| VAR { $$ $1 }
;

(* declaration_lists are reversed lists of declarations *)
declaration_list : { $$ nil }
| declaration_list declaration { $$ ($2 @ $1) }
;

optional_args : { $$ nil }
| kw_open_paren pattern_list kw_close_paren { $$ (rev $2) }
;