(* Lexer for spi-calculus-like processes.
   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 "spi_h";

val spi_value = ref (spinone ());

fun id_or_var yyd =
    let val s = hlex_text yyd
    in
	spi_value := string s;
	if is_fun s
	    then identifier
	else VAR
    end;

%}

SPACE [\ \t\f\n\r]+
DIG [0-9]+
CAPITAL [A-Z]
SMALL [a-z]
LETTER ({CAPITAL}|{SMALL})
ALPHA [A-Za-z0-9\'\_]
SYMB [\!\%\&\$\#\+\-\/\:\<\=\>\?\@\\\~\'\^\|\*\`]

%x COMMENT

%%

{SPACE}	continue
"(*"	{ hlex_begin (yyd, COMMENT); continue }
<COMMENT>{
  [^*]*	{ continue (* eat anything that's not a '*' *) }
  "*"+[^*)]*  { continue (* eat up '*'s not followed by ')'s *) }
  "*"+")"       { hlex_begin (yyd, INITIAL); continue }
  <<EOF>>	{ hlex_begin (yyd, 0); hlex_flush (yyd, hlex_current_buffer yyd);
                  raise SpiUnterminatedCommentEvt }
}
\(	return kw_open_paren
\)	return kw_close_paren
\[	return kw_open_bracket
\]	return kw_close_bracket
\{	return kw_open_curly
\}	return kw_close_curly
\,	return kw_comma
\;	return kw_semicolon
\.	return kw_period
\/{DIG}	{ spi_value := string (hlex_text yyd); return kw_slash }
=	return kw_equal
\<\>	return kw_different
=\>	return kw_implies
!	return kw_bang
stop	return kw_zero
new	return kw_new
if	return kw_if
of	return kw_of
then	return kw_then
else	return kw_else
in	return kw_in
out	return kw_out
let	return kw_let
case	return kw_case
\|	return kw_par
event	return kw_event
proc	return kw_proc
data	return kw_data
fun	return kw_fun
private	return kw_private
and	return kw_and
\_	return kw_any
\_*{SMALL}{ALPHA}*	{ return (id_or_var yyd) }
\_*{DIG}		{ return (id_or_var yyd) }
\_*{CAPITAL}{ALPHA}*	{ return (id_or_var yyd) }
.	{ #put stderr "Unrecognized character: ";
          #put stderr (hlex_text yyd);
          #put stderr "\n";
          #flush stderr (); continue }

%%