type svalue = Tokens.svalue 
type pos = int
type ('a,'b) token = ('a,'b) Tokens.token
type lexresult = (svalue,pos) token
val line_num = ref 1;
val open_coms =  ref 0;
val prog_string = ref "";
val temp_string = ref "";
val begin_string_pos = ref 0;
val open_string = ref false;
val num_buffer = ref "";
val id_buffer = ref "";
val last_id_char = ref "";
local
fun is_reserved(str,position) = 
    let fun do_reserved "assume" = (true,Tokens.ASSUME(position,position+6)) |
            do_reserved "claim" = (true,Tokens.CLAIM(position,position+5)) |    
            do_reserved "fetch" = (true,Tokens.FETCH(position,position+5)) |    
            do_reserved "fetch-all" = (true,Tokens.FETCH_ALL(position,position+9)) |    
            do_reserved "switch" = (true,Tokens.IF_ELSE(position,position+4)) |    
            do_reserved "the" = (true,Tokens.THE(position,position+3)) |    
            do_reserved "assert" = (true,Tokens.ASSERT(position,position+6)) |            
            do_reserved "load-file" = (true,Tokens.LOAD_FILE(position,position+9)) |            
            do_reserved "define-symbol" = 
                        (true,Tokens.DEFINE_SYMBOL(position,position+13)) |            
            do_reserved "clear-assumption-base" = 
                    (true,Tokens.CLEAR(position,position+21)) |            
            do_reserved "assume-let" = (true,Tokens.ASSUME_LET(position,position+10)) |
            do_reserved "function" = (true,Tokens.FUNCTION(position,position+8)) |
            do_reserved "method" = (true,Tokens.METHOD(position,position+6)) |
            do_reserved "define" = (true,Tokens.DEFINE(position,position+6)) |
            do_reserved "structure" = (true,Tokens.STRUCTURE(position,position+9)) |
            do_reserved "structures" = (true,Tokens.STRUCTURES(position,position+10)) |
            do_reserved "datatype" = (true,Tokens.DATA_TYPE(position,position+8)) |
            do_reserved "domain" = (true,Tokens.DOMAIN(position,position+6)) |
            do_reserved "declare" = (true,Tokens.DECLARE(position,position+7)) |
            do_reserved "val-of" = (true,Tokens.VAL_OF(position,position+6)) |
            do_reserved "help" = (true,Tokens.HELP(position,position+4)) |
            do_reserved "suppose-absurd" = (true,Tokens.SUPPOSE_ABSURD(position,position+14)) |
            do_reserved "suppose-absurd-let" = 
                     (true,Tokens.SUPPOSE_ABSURD_LET(position,position+18)) |
            do_reserved "dmatch" = (true,Tokens.DMATCH(position,position+6)) |
            do_reserved "match" = (true,Tokens.MATCH(position,position+6)) |
            do_reserved "let" = (true,Tokens.LET(position,position+3)) |
            do_reserved "letrec" = (true,Tokens.LETREC(position,position+6)) |
            do_reserved "dlet" = (true,Tokens.DLET(position,position+4)) |
            do_reserved "dletrec" = (true,Tokens.DLETREC(position,position+7)) |
            do_reserved "apply-method" = (true,Tokens.APPLY_METHOD(position,position+12)) |
            do_reserved "mp" = (true,Tokens.MP(position,position+2)) |
            do_reserved "cd" = (true,Tokens.CD(position,position+2)) |
            do_reserved "dn" = (true,Tokens.DN(position,position+2)) |
            do_reserved "absurd" = (true,Tokens.ABSURD(position,position+6)) |
            do_reserved "begin" = (true,Tokens.BEGIN(position,position+5)) |
            do_reserved "dbegin" = (true,Tokens.DBEGIN(position,position+6)) |
            do_reserved "while" = (true,Tokens.WHILE(position,position+5)) |
            do_reserved "equiv" = (true,Tokens.EQUIV(position,position+5)) |
            do_reserved "left-iff" = (true,Tokens.LEFT_IFF(position,position+8)) |
            do_reserved "right-iff" = (true,Tokens.RIGHT_IFF(position,position+9)) |
            do_reserved "both" = (true,Tokens.BOTH(position,position+4)) |
            do_reserved "left-and" = (true,Tokens.LEFT_AND(position,position+8)) |
            do_reserved "right-and" = (true,Tokens.RIGHT_AND(position,position+9)) |
            do_reserved "either" = (true,Tokens.EITHER(position,position+6)) |
            do_reserved "uspec" = (true,Tokens.USPEC(position,position+5)) |
            do_reserved "leibniz" = (true,Tokens.LEIBNIZ(position,position+7)) |
            do_reserved "eq-reflex" = (true,Tokens.EQ_REFLEX(position,position+9)) |
            do_reserved "unequal-terms" = (true,Tokens.UNEQUAL_TERMS(position,position+13)) |
            do_reserved "egen" = (true,Tokens.EGEN(position,position+4)) |
            do_reserved "egen-unique" = (true,Tokens.EGEN_UNIQUE(position,position+11)) |
            do_reserved "variable" = (true,Tokens.VAR(position,position+8)) |
            do_reserved "try" = (true,Tokens.TRY(position,position+3)) |    
            do_reserved "forall" = (true,Tokens.FORALL(position,position+6)) |
            do_reserved "exists" = (true,Tokens.EXISTS(position,position+6)) |
            do_reserved "exists-unique" = (true,Tokens.EXISTS_UNIQUE(position,position+13)) |
            do_reserved "not" = (true,Tokens.NOT(position,position+3)) |
            do_reserved "and" = (true,Tokens.AND(position,position+3)) |
            do_reserved "or" = (true,Tokens.OR(position,position+2)) |           
            do_reserved "if" = (true,Tokens.IF(position,position+2)) |           
            do_reserved "iff" = (true,Tokens.IFF(position,position+3)) |     
            do_reserved "pick-any" = (true,Tokens.PICK_ANY(position,position+8)) |           
            do_reserved "pick-any-var" = (true,Tokens.PICK_ANY2(position,position+8)) |           
            do_reserved "pick-witness" = (true,Tokens.PICK_WITNESS(position,position+12)) |           
            do_reserved "any" = (true,Tokens.ANY_PATTERN(position,position+3)) |           
            do_reserved "set!" = (true,Tokens.SET(position,position+4)) |           
            do_reserved "some-var" = (true,Tokens.SOME_VAR(position,position+8)) |           
            do_reserved "some-quant" = (true,Tokens.SOME_QUANT(position,position+10)) |           
            do_reserved "some-prop-con" = (true,Tokens.SOME_PROP_CON(position,position+15)) |           
            do_reserved _ = (false,Tokens.ASSUME(0,0))
      in
          do_reserved(str) 
    end
in  
fun do_id(str,position) = let (* val lower_str = Basic.toLower(str) *)
                              val (flag,tok) = is_reserved(str,position) in
                              if flag then tok else Tokens.ID(str,position,position+size(str))
                          end;                        
end;

local
open Int;
fun int_exp(a:int,b:int) = if (b <= 0) then 1 else a*int_exp(a,b-1);
fun digit_val(c) = ord(c) - ord(#"0");
fun conv([],_,sum) = sum |
    conv(c::rest,pos,sum) = conv(rest,pos-1,sum+(digit_val(c)*int_exp(10,pos)));
in
   fun str_2_int(str) = 
       conv(explode(str),size(str)-1,0);
end;


fun str_2_real(str) = case Real.fromString str of SOME(r) => r | _ => 0.0;

fun convert_int(str) = case Int.fromString str of SOME(r) => r | _ => 0;

fun convert_real(str) = case Real.fromString str of SOME(r) => r | _ => 0.0;

fun getInt(str) = Option.getOpt(Int.fromString(str),0);

fun getReal(str) = Option.getOpt(Real.fromString(str),0.0);

fun error(str) = print("\n"^str);
fun inc(i) = i := !i + 1;
fun dec(i) = i := !i - 1;
fun eof() = (if ((!open_coms) > 0) then (open_coms := 0;
                                         print("\nError...unclosed comment..\n")) 
                                 else ();
             Tokens.EOF(0,0));

%%
%header (functor AthenaLexFun(structure Tokens:Athena_TOKENS));
%s EOL_COMMENT;
%s STRING;
%s INT_STATE;
%s REAL_STATE;
%s ID_STATE;
alpha = [A-Za-z];
digit = [0-9];
alpha_num = {alpha} | {digit}; 
printable_char = [\033-\127];
init_ide_char =  \038 | [\042-\058] | [\060-\062] | [\064-\090] | \092 | \094 | \095 | [\097-\126];
internal_ide_char = \033 | [\035-\040] | [\042-\058] | [\060-\092] | \094 | [\095-\126];
ide_char =  ' | _ | - | \094 | \035 | \038 | \063 | \042 | \126 | {alpha_num};
identifier = {init_ide_char}{internal_ide_char}*;
non_neg_integer = {digit}+;
non_neg_number = {non_neg_integer} | {non_neg_integer}.{non_neg_integer};
number = {non_neg_number} | -{non_neg_number};
object_type_var = #{identifier};
type_var = ##{identifier};
white_space = [\ \t\b];
printable_and_non_paren = [\033-\039] | [\042-\127];
%%
<INITIAL>\n => (inc(line_num);continue());
<INITIAL>{white_space}+ => (continue());
<INITIAL>"\"" => (begin_string_pos := yypos;open_string := true;temp_string := "";
                  YYBEGIN STRING; continue());
<INITIAL>"(" => (Tokens.LPAREN(yypos,yypos+1));
<INITIAL>")" => (Tokens.RPAREN(yypos,yypos+1));
<INITIAL>"[" => (Tokens.LEFT_BRACKET(yypos,yypos+1));
<INITIAL>"]" => (Tokens.RIGHT_BRACKET(yypos,yypos+1));
<INITIAL>"$" => (Tokens.DOLLAR(yypos,yypos+1));
<INITIAL>"%" => (Tokens.DIRECTIVE_PREFIX(yypos,yypos+1));
<INITIAL>"<<" => (Tokens.ORDERED_PAIR_LEFT(yypos,yypos+2));
<INITIAL>">>" => (Tokens.ORDERED_PAIR_RIGHT(yypos,yypos+2));
<INITIAL>"->" => (Tokens.FUN_ARROW(yypos,yypos+2));
<INITIAL>"?" => (Tokens.QMARK(yypos,yypos+1));
<INITIAL>"!" => (Tokens.EXCL_MARK(yypos,yypos+1));
<INITIAL>"'" => (Tokens.QUOTE_SYMBOL(yypos,yypos+1));
<INITIAL>"`" => (Tokens.BACK_QUOTE_SYMBOL(yypos,yypos+1));
<INITIAL>";" => (YYBEGIN EOL_COMMENT; continue());
<INITIAL>{identifier} => (do_id(yytext,yypos));
<INITIAL>{object_type_var} => (Tokens.OBJECT_TYPE_VAR(yytext,yypos,yypos+size(yytext)));
<INITIAL>{type_var} => (Tokens.TYPE_VAR(yytext,yypos,yypos+size(yytext)));
<INITIAL>. => (error("Illegal character found and ignored: "^yytext);continue());
<STRING>"\\\"" => (prog_string := !prog_string^yytext;continue());
<STRING>"\"" => (temp_string := !prog_string;prog_string := "";open_string := false;YYBEGIN INITIAL;
                 Tokens.STRING(!temp_string,!begin_string_pos,!begin_string_pos+size(!temp_string)));
<STRING>. => (prog_string := !prog_string^yytext;continue());
<EOL_COMMENT>\n => (YYBEGIN INITIAL;continue());
<EOL_COMMENT>. => (continue());
