(* Lexer for proof.log files.
   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 "proof_h";

val proof_value = ref (prnone ());

fun unstringify s =
    let val |[put, convert, ...]| = outstring ""
        fun unstringify1 ("\\"::l) =
	    (case l of
		 "\""::l' => (put "\""; unstringify1 l')
	       | "\\"::l' =>  (put "\\"; unstringify1 l')
	       | "n"::l' => (put "\n"; unstringify1 l')
	       | "t"::l' => (put "\t"; unstringify1 l')
	       | "v"::l' => (put "\v"; unstringify1 l')
	       | "f"::l' => (put "\f"; unstringify1 l')
	       | "^"::c::l' => (put (chr (ord c-ord "@")); unstringify1 l')
               | c::l' =>
		 if ord c >= ord "0" andalso ord c <= ord "9"
		     then let val c' :: c'' :: l'' = l'
			      val n = (ord c - ord "0") * 100
			      val n' = n + (ord c' - ord "0") * 10
			      val n'' = n' + (ord c'' - ord "0")
			  in
			      put (chr n'')
			  end
		 else skip l)
          | unstringify1 ("\"":: _) = ()
          | unstringify1 (c::l) = (put c; unstringify1 l)
          | unstringify1 nil = ()
        and skip ("\\"::l) = unstringify1 l
	  | skip (_ :: l) = skip l
    in
       unstringify1 (tl (explode s)); (* extremely inefficient, but so what? *)
       convert ()
    end;

%}

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

%x COMMENT

%%

{SPACE}	continue
"%".*\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 ProofUnterminatedCommentEvt }
}
\#ne\([^()]*\) { proof_value := prstring (glex_text yyd); return kw_ne }
\#false\([^()]*\) { proof_value := prstring (glex_text yyd); return kw_false }

"<source>" return kw_open_source
"</source>" return kw_close_source
"<clause"{SPACE}+"name"{SPACE}*"="{SPACE}* return kw_open_clause
"</clause>" return kw_close_clause
"<definitions>" return kw_open_definitions
"</definitions>" return kw_close_definitions
"<approximation>" return kw_open_approximation
"</approximation>" return kw_close_approximation
"<justifications>" return kw_open_justifications
"</justifications>" return kw_close_justifications

\[({ALPHA}|\-)+\] { proof_value := prstring (substr (glex_text yyd, 1, glex_length yyd-1)); return kw_axiom }
\[({ALPHA}|\-)+: { proof_value := prstring (substr (glex_text yyd, 1, glex_length yyd-1)); return kw_open_rule }
\] return kw_close_rule

\"([^\"\\]|(\\([\"\\ntvf]|(\^[\@A-Z\[\\\]\^\_])|({DIG}{DIG}{DIG})|({FMT}*\\))))*\"	{
  proof_value := prstring (unstringify (glex_text yyd)); return string_constant }
{DIG}:	{ proof_value := pri (intofstring (substr (glex_text yyd, 0, glex_length yyd-1)));
          return kw_clause_def }
{DIG};	{ proof_value := pri (intofstring (substr (glex_text yyd, 0, glex_length yyd-1)));
          return kw_clause_use }

\(	return kw_open_paren
\)	return kw_close_paren
\{	return kw_open_brace
\}	return kw_close_brace
:-	return kw_provided
\,	return kw_comma
\;	return kw_semicolon
\.	return kw_period
\?	return kw_question_mark
\=	return kw_equal
\>	return kw_end_tag
\_*{SMALL}{ALPHA}*	{ proof_value := prstring (glex_text yyd); return identifier }
\_*{DIG}		{ proof_value := prstring (glex_text yyd); return identifier }
\_*{CAPITAL}{ALPHA}*	{ proof_value := prstring (glex_text yyd); return VAR }
\*			{ proof_value := prstring (glex_text yyd); return identifier }
\#q{DIG}*		{ proof_value := prstring (glex_text yyd); return identifier }
.	{ #put stderr "Unrecognized character: ";
          #put stderr (glex_text yyd);
          #put stderr "\n"; continue }

%%
