(* Lexer 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 "plauto_h";

val plauto_value = ref (aplnone ());

local
    val nfa = re_make_nfa [(re_parse "^[ \t\f]*([^:]*[^ :\t\f])[ \t\f]*(:-[ \t\f]*([^:]*[^ :\t\f])[ \t\f]*)?\\.\n$",
			    fn (s, a) => (re_subst (s,a,1), re_subst (s,a,3) handle Subscript => ""))]
in
    fun match_def s =
	nfa_run (nfa, s)
end;

val plauto_def_P = ref "";
val plauto_defs = ref ({} : string -m> string * string);
%}

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

%x COMMENT DEF DEF2

%%

{SPACE}	continue
"%[def]"{ONESPACE}* { glex_begin(yyd, DEF); continue }
<DEF>{
  \_*{SMALL}{ALPHA}* { plauto_def_P := glex_text yyd; glex_begin (yyd, DEF2); continue }
  \_*{DIG} { plauto_def_P := glex_text yyd; glex_begin (yyd, DEF2); continue }
  . continue
  \n { glex_begin (yyd, INITIAL); continue }
}
<DEF2>{
  {SPACE} continue
  .*\n? { let val s = glex_text yyd
          in
            (case match_def s of
                 SOME (head, body) =>
                 plauto_defs := !plauto_defs ++ {!plauto_def_P => (head, body)}
               | _ => ());
            glex_begin (yyd, INITIAL); continue
         end }
}

"%"\n continue
"%"[^[].*\n continue
"%["[^d].*\n continue
"%["d[^e].*\n continue
"%["de[^f].*\n continue
"%["def[^]].*\n continue
"/*"	{ glex_begin(yyd, COMMENT); continue }
<COMMENT>{
  [^*]*	{ continue (* eat anything that's not a '*' *) }
  "*"+[^*/]*  { continue (* eat up '*'s not followed by '/'s *) }
  "*"+"/"       { glex_begin (yyd, INITIAL); continue }
  <<EOF>>	{ glex_begin (yyd, 0); glex_flush (yyd, glex_current_buffer yyd);
                  raise PlautoUnterminatedCommentEvt }
}

\(	return kw_open_paren
\)	return kw_close_paren
:-	return kw_provided
\,	return kw_comma
\.	return kw_period
\?	return kw_question_mark
\_*{SMALL}{ALPHA}*	{ plauto_value := aplstring (glex_text yyd); return identifier }
\_*{DIG}		{ plauto_value := aplstring (glex_text yyd); return identifier }
\_*{CAPITAL}{ALPHA}*	{ plauto_value := aplstring (glex_text yyd); return VAR }
\#q{DIG}*		{ plauto_value := aplstring (glex_text yyd); return abbrv }
.	{ #put stderr "Unrecognized character: ";
          #put stderr (glex_text yyd);
          #put stderr "\n"; continue }

%%
