(*  Title:      Pure/ML/ml_lex.ML

    Author:     Makarius

Lexical syntax for SML.

*)

signature ML_LEX =

sig

  datatype token_kind =

    Keyword | Ident | LongIdent | TypeVar | Word | Int | Real | Char | String |

    Space | Comment | Error of string | EOF

  eqtype token

  val stopper: token Scan.stopper

  val is_regular: token -> bool

  val is_improper: token -> bool

  val set_range: Position.range -> token -> token

  val pos_of: token -> Position.T

  val end_pos_of: token -> Position.T

  val kind_of: token -> token_kind

  val content_of: token -> string

  val check_content_of: token -> string

  val flatten: token list -> string

  val report_token: token -> unit

  val keywords: string list

  val source: (Symbol.symbol, 'a) Source.source ->

    (token, (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source)

      Source.source) Source.source

  val tokenize: string -> token list

  val read: Position.T -> Symbol_Pos.text -> token Antiquote.antiquote list

end;

structure ML_Lex: ML_LEX =

struct

(** tokens **)

(* datatype token *)

datatype token_kind =

  Keyword | Ident | LongIdent | TypeVar | Word | Int | Real | Char | String |

  Space | Comment | Error of string | EOF;

datatype token = Token of Position.range * (token_kind * string);

(* position *)

fun set_range range (Token (_, x)) = Token (range, x);

fun pos_of (Token ((pos, _), _)) = pos;

fun end_pos_of (Token ((_, pos), _)) = pos;

(* control tokens *)

fun mk_eof pos = Token ((pos, Position.none), (EOF, ""));

val eof = mk_eof Position.none;

fun is_eof (Token (_, (EOF, _))) = true

  | is_eof _ = false;

val stopper =

  Scan.stopper (fn [] => eof | toks => mk_eof (end_pos_of (List.last toks))) is_eof;

(* token content *)

fun kind_of (Token (_, (k, _))) = k;

fun content_of (Token (_, (_, x))) = x;

fun token_leq (tok, tok') = content_of tok <= content_of tok';

fun is_regular (Token (_, (Error _, _))) = false

  | is_regular (Token (_, (EOF, _))) = false

  | is_regular _ = true;

fun is_improper (Token (_, (Space, _))) = true

  | is_improper (Token (_, (Comment, _))) = true

  | is_improper _ = false;

fun warn tok =

  (case tok of

    Token (_, (Keyword, ":>")) =>

      warning ("Opaque signature matching (:>) fails to work with ML pretty printing --\n\

        \prefer non-opaque matching (:) possibly with abstype" ^

        Position.str_of (pos_of tok))

  | _ => ());

fun check_content_of tok =

  (case kind_of tok of

    Error msg => error msg

  | _ => content_of tok);

fun flatten_content (tok :: (toks as tok' :: _)) =

      Symbol.escape (check_content_of tok) ::

        (if is_improper tok orelse is_improper tok' then flatten_content toks

         else Symbol.space :: flatten_content toks)

  | flatten_content toks = map (Symbol.escape o check_content_of) toks;

val flatten = implode o flatten_content;

(* markup *)

local

val token_kind_markup =

 fn Keyword   => Markup.ML_keyword

  | Ident     => Markup.ML_ident

  | LongIdent => Markup.ML_ident

  | TypeVar   => Markup.ML_tvar

  | Word      => Markup.ML_numeral

  | Int       => Markup.ML_numeral

  | Real      => Markup.ML_numeral

  | Char      => Markup.ML_char

  | String    => Markup.ML_string

  | Space     => Markup.empty

  | Comment   => Markup.ML_comment

  | Error _   => Markup.ML_malformed

  | EOF       => Markup.empty;

fun token_markup kind x =

  if kind = Keyword andalso exists_string (not o Symbol.is_ascii_letter) x

  then Markup.ML_delimiter

  else token_kind_markup kind;

in

fun report_token (Token ((pos, _), (kind, x))) = Position.report pos (token_markup kind x);

end;

(** scanners **)

open Basic_Symbol_Pos;

fun !!! msg = Symbol_Pos.!!! (fn () => "SML lexical error: " ^ msg);

(* blanks *)

val scan_blank = Scan.one (Symbol.is_ascii_blank o Symbol_Pos.symbol);

val scan_blanks1 = Scan.repeat1 scan_blank;

(* keywords *)

val keywords = ["#", "(", ")", ",", "->", "...", ":", ":>", ";", "=",

  "=>", "[", "]", "_", "{", "|", "}", "abstype", "and", "andalso", "as",

  "case", "datatype", "do", "else", "end", "eqtype", "exception", "fn",

  "fun", "functor", "handle", "if", "in", "include", "infix", "infixr",

  "let", "local", "nonfix", "of", "op", "open", "orelse", "raise", "rec",

  "sharing", "sig", "signature", "struct", "structure", "then", "type",

  "val", "where", "while", "with", "withtype"];

val lex = Scan.make_lexicon (map raw_explode keywords);

fun scan_keyword x = Scan.literal lex x;

(* identifiers *)

local

val scan_letdigs =

  Scan.many

    ((Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf Symbol.is_ascii_quasi) o

      Symbol_Pos.symbol);

val scan_alphanumeric =

  Scan.one (Symbol.is_ascii_letter o Symbol_Pos.symbol) -- scan_letdigs >> op ::;

val scan_symbolic =

  Scan.many1 (member (op =) (raw_explode "!#$%&*+-/:<=>?@\\^`|~") o Symbol_Pos.symbol);

in

val scan_ident = scan_alphanumeric || scan_symbolic;

val scan_longident =

  (Scan.repeat1 (scan_alphanumeric @@@ $$$ ".") >> flat) @@@ (scan_ident || $$$ "=");

val scan_typevar = $$$ "'" @@@ scan_letdigs;

end;

(* numerals *)

local

val scan_dec = Scan.many1 (Symbol.is_ascii_digit o Symbol_Pos.symbol);

val scan_hex = Scan.many1 (Symbol.is_ascii_hex o Symbol_Pos.symbol);

val scan_sign = Scan.optional ($$$ "~") [];

val scan_decint = scan_sign @@@ scan_dec;

in

val scan_word =

  $$$ "0" @@@ $$$ "w" @@@ $$$ "x" @@@ scan_hex ||

  $$$ "0" @@@ $$$ "w" @@@ scan_dec;

val scan_int = scan_sign @@@ ($$$ "0" @@@ $$$ "x" @@@ scan_hex || scan_dec);

val scan_exp = ($$$ "E" || $$$ "e") @@@ scan_decint;

val scan_real =

  scan_decint @@@ $$$ "." @@@ scan_dec @@@ Scan.optional scan_exp [] ||

  scan_decint @@@ scan_exp;

end;

(* chars and strings *)

local

val scan_escape =

  Scan.one (member (op =) (raw_explode "\"\\abtnvfr") o Symbol_Pos.symbol) >> single ||

  $$$ "^" @@@ (Scan.one (fn (s, _) => ord "@" <= ord s andalso ord s <= ord "_") >> single) ||

  Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) --

    Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) --

    Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) >> (fn ((a, b), c) => [a, b, c]);

val scan_str =

  Scan.one (fn (s, _) => Symbol.is_regular s andalso s <> "\"" andalso s <> "\\" andalso

    (not (Symbol.is_char s) orelse Symbol.is_printable s)) >> single ||

  $$$ "\\" @@@ !!! "bad escape character in string" scan_escape;

val scan_gap = $$$ "\\" @@@ scan_blanks1 @@@ $$$ "\\";

val scan_gaps = Scan.repeat scan_gap >> flat;

in

val scan_char =

  $$$ "#" @@@ $$$ "\"" @@@ scan_gaps @@@ scan_str @@@ scan_gaps @@@ $$$ "\"";

val scan_string =

  $$$ "\"" @@@ !!! "missing quote at end of string"

    ((Scan.repeat (scan_gap || scan_str) >> flat) @@@ $$$ "\"");

end;

(* scan tokens *)

local

fun token k ss = Token (Symbol_Pos.range ss, (k, Symbol_Pos.content ss));

val scan_ml =

 (scan_char >> token Char ||

  scan_string >> token String ||

  scan_blanks1 >> token Space ||

  Symbol_Pos.scan_comment !!! >> token Comment ||

  Scan.max token_leq

   (scan_keyword >> token Keyword)

   (scan_word >> token Word ||

    scan_real >> token Real ||

    scan_int >> token Int ||

    scan_longident >> token LongIdent ||

    scan_ident >> token Ident ||

    scan_typevar >> token TypeVar));

val scan_antiq = Antiquote.scan || scan_ml >> Antiquote.Text;

fun recover msg =

  Scan.many (((not o Symbol.is_blank) andf Symbol.is_regular) o Symbol_Pos.symbol)

  >> (fn cs => [token (Error msg) cs]);

in

fun source src =

  Symbol_Pos.source (Position.line 1) src

  |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_ml)) (SOME (false, recover));

val tokenize = Source.of_string #> Symbol.source #> source #> Source.exhaust;

fun read pos txt =

  let

    val _ = Position.report pos Markup.ML_source;

    val syms = Symbol_Pos.explode (txt, pos);

    val termination =

      if null syms then []

      else

        let

          val pos1 = List.last syms |-> Position.advance;

          val pos2 = Position.advance Symbol.space pos1;

        in [Antiquote.Text (Token (Position.range pos1 pos2, (Space, Symbol.space)))] end;

    val input =

      (Source.of_list syms

        |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_antiq))

          (SOME (false, fn msg => recover msg >> map Antiquote.Text))

        |> Source.exhaust

        |> tap (List.app (Antiquote.report report_token))

        |> tap Antiquote.check_nesting

        |> tap (List.app (fn Antiquote.Text tok => (check_content_of tok; warn tok) | _ => ())))

      handle ERROR msg =>

        cat_error msg ("The error(s) above occurred in ML source" ^ Position.str_of pos);

  in input @ termination end;

end;

end;