src/Pure/Syntax/lexicon.ML

lots of internal cleaning and tuning;
removed {parse,print}_{pre,post}_proc;
new lexer: now human readable due to scanner combinators;
new parser installed, but still inactive (due to grammar ambiguities);
added Syntax.test_read;
typ_of_term: sorts now made distinct and sorted;
mixfix: added forced line breaks (//);
PROP now printed before subterm of type prop with non-const head;

(*  Title:      Pure/Syntax/lexicon.ML
    ID:         $Id$
    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen

Scanner combinators and Isabelle's main lexer (used for terms and typs).
*)

infix 5 -- ^^;
infix 3 >>;
infix 0 ||;

signature LEXICON0 =
sig
  val is_identifier: string -> bool
  val string_of_vname: indexname -> string
  val scan_varname: string list -> indexname * string list
  val scan_var: string -> term
end;

signature LEXICON =
sig
  include LEXICON0
  val is_xid: string -> bool
  val is_tfree: string -> bool
  type lexicon
  datatype token =
    Token of string |
    IdentSy of string |
    VarSy of string |
    TFreeSy of string |
    TVarSy of string |
    EndToken;
  val id: string
  val var: string
  val tfree: string
  val tvar: string
  val str_of_token: token -> string
  val display_token: token -> string
  val matching_tokens: token * token -> bool
  val valued_token: token -> bool
  val predef_term: string -> token
  val is_terminal: string -> bool
  val empty_lexicon: lexicon
  val extend_lexicon: lexicon -> string list -> lexicon
  val mk_lexicon: string list -> lexicon
  val tokenize: lexicon -> bool -> string -> token list

  exception LEXICAL_ERROR
  val >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
  val || : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b
  val -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e
  val ^^ : ('a -> string * 'b) * ('b -> string * 'c) -> 'a -> string * 'c
  val $$ : ''a -> ''a list -> ''a * ''a list
  val scan_empty: 'a list -> 'b list * 'a list
  val scan_one: ('a -> bool) -> 'a list -> 'a * 'a list
  val scan_any: ('a -> bool) -> 'a list -> 'a list * 'a list
  val scan_any1: ('a -> bool) -> 'a list -> 'a list * 'a list
  val scan_end: 'a list -> 'b list * 'a list
  val optional: ('a -> 'b * 'a) -> 'a -> 'b option * 'a
  val repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
  val repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
end;

functor LexiconFun(): LEXICON =
struct


(** is_identifier etc. **)

fun is_ident [] = false
  | is_ident (c :: cs) = is_letter c andalso forall is_letdig cs;

val is_identifier = is_ident o explode;

fun is_xid s =
  (case explode s of
    "_" :: cs => is_ident cs
  | cs => is_ident cs);

fun is_tfree s =
  (case explode s of
    "'" :: cs => is_ident cs
  | _ => false);



(** string_of_vname **)

fun string_of_vname (x, i) =
  let
    val si = string_of_int i;
  in
    if is_digit (last_elem (explode x)) then "?" ^ x ^ "." ^ si
    else if i = 0 then "?" ^ x
    else "?" ^ x ^ si
  end;



(** datatype token **)

datatype token =
  Token of string |
  IdentSy of string |
  VarSy of string |
  TFreeSy of string |
  TVarSy of string |
  EndToken;


(* names of valued tokens *)

val id = "id";
val var = "var";
val tfree = "tfree";
val tvar = "tvar";


(* str_of_token *)

fun str_of_token (Token s) = s
  | str_of_token (IdentSy s) = s
  | str_of_token (VarSy s) = s
  | str_of_token (TFreeSy s) = s
  | str_of_token (TVarSy s) = s
  | str_of_token EndToken = "";


(* display_token *)

fun display_token (Token s) = quote s
  | display_token (IdentSy s) = "id(" ^ s ^ ")"
  | display_token (VarSy s) = "var(" ^ s ^ ")"
  | display_token (TFreeSy s) = "tfree(" ^ s ^ ")"
  | display_token (TVarSy s) = "tvar(" ^ s ^ ")"
  | display_token EndToken = "";


(* matching_tokens *)

fun matching_tokens (Token x, Token y) = (x = y)
  | matching_tokens (IdentSy _, IdentSy _) = true
  | matching_tokens (VarSy _, VarSy _) = true
  | matching_tokens (TFreeSy _, TFreeSy _) = true
  | matching_tokens (TVarSy _, TVarSy _) = true
  | matching_tokens (EndToken, EndToken) = true
  | matching_tokens _ = false;


(* valued_token *)

fun valued_token (Token _) = false
  | valued_token (IdentSy _) = true
  | valued_token (VarSy _) = true
  | valued_token (TFreeSy _) = true
  | valued_token (TVarSy _) = true
  | valued_token EndToken = false;


(* predef_term *)

fun predef_term name =
  if name = id then IdentSy name
  else if name = var then VarSy name
  else if name = tfree then TFreeSy name
  else if name = tvar then TVarSy name
  else EndToken;


(* is_terminal **)

fun is_terminal s = s mem [id, var, tfree, tvar];



(** datatype lexicon **)

datatype lexicon =
  Empty |
  Branch of string * string * lexicon * lexicon * lexicon;

val no_token = "";


(* empty_lexicon *)

val empty_lexicon = Empty;


(* extend_lexicon *)

fun extend_lexicon lexicon strs =
  let
    fun ext (lex, s) =
      let
        fun add (Branch (d, a, lt, eq, gt)) (chs as c :: cs) =
              if c < d then Branch (d, a, add lt chs, eq, gt)
              else if c > d then Branch (d, a, lt, eq, add gt chs)
              else Branch (d, if null cs then s else a, lt, add eq cs, gt)
          | add Empty [c] =
              Branch (c, s, Empty, Empty, Empty)
          | add Empty (c :: cs) =
              Branch (c, no_token, Empty, add Empty cs, Empty)
          | add lex [] = lex;

        val cs = explode s;
      in
        if exists is_blank cs then
          error ("extend_lexicon: blank in literal " ^ quote s)
        else add lex cs
      end;
  in
    foldl ext (lexicon, strs)
  end;


(* mk_lexicon *)

val mk_lexicon = extend_lexicon empty_lexicon;



(** scanners **)

exception LEXICAL_ERROR;


(* scanner combinators *)

fun (scan >> f) cs = apfst f (scan cs);

fun (scan1 || scan2) cs = scan1 cs handle LEXICAL_ERROR => scan2 cs;

fun (scan1 -- scan2) cs =
  let
    val (x, cs') = scan1 cs;
    val (y, cs'') = scan2 cs';
  in
    ((x, y), cs'')
  end;

fun (scan1 ^^ scan2) = scan1 -- scan2 >> op ^;


(* generic scanners *)

fun $$ _ [] = raise LEXICAL_ERROR
  | $$ a (c :: cs) =
      if a = c then (c, cs) else raise LEXICAL_ERROR;

fun scan_empty cs = ([], cs);

fun scan_one _ [] = raise LEXICAL_ERROR
  | scan_one pred (c :: cs) =
      if pred c then (c, cs) else raise LEXICAL_ERROR;

val scan_any = take_prefix;

fun scan_any1 pred = scan_one pred -- scan_any pred >> op ::;

fun scan_rest cs = (cs, []);

fun scan_end [] = ([], [])
  | scan_end _ = raise LEXICAL_ERROR;

fun optional scan = scan >> Some || scan_empty >> K None;

fun repeat scan cs = (scan -- repeat scan >> op :: || scan_empty) cs;

fun repeat1 scan = scan -- repeat scan >> op ::;


(* other scanners *)

val scan_letter_letdigs = scan_one is_letter -- scan_any is_letdig >> op ::;

val scan_digits1 = scan_any1 is_digit;

val scan_id = scan_letter_letdigs >> implode;

val scan_id_nat =
  scan_id ^^ ($$ "." ^^ (scan_digits1 >> implode) || scan_empty >> K "");


(* scan_literal *)

fun scan_literal lex chrs =
  let
    fun scan_lit _ s_cs [] = s_cs
      | scan_lit Empty s_cs _ = s_cs
      | scan_lit (Branch (d, a, lt, eq, gt)) s_cs (chs as c :: cs) =
          if c < d then scan_lit lt s_cs chs
          else if c > d then scan_lit gt s_cs chs
          else scan_lit eq (if a = no_token then s_cs else Some (a, cs)) cs;
  in
    (case scan_lit lex None chrs of
      None => raise LEXICAL_ERROR
    | Some s_cs => s_cs)
  end;



(** tokenize **)

fun tokenize lex xids str =
  let
    val scan_xid =
      if xids then $$ "_" ^^ scan_id || scan_id
      else scan_id;

    val scan_lit = scan_literal lex >> pair Token;

    val scan_ident =
      $$ "?" ^^ $$ "'" ^^ scan_id_nat >> pair TVarSy ||
      $$ "?" ^^ scan_id_nat >> pair VarSy ||
      $$ "'" ^^ scan_id >> pair TFreeSy ||
      scan_xid >> pair IdentSy;

    fun scan_max_token cs =
      (case (optional scan_lit cs, optional scan_ident cs) of
        (tok1, (None, _)) => tok1
      | ((None, _), tok2) => tok2
      | (tok1 as (Some (_, s1), _), tok2 as (Some (_, s2), _)) =>
          if size s1 >= size s2 then tok1 else tok2);

    fun scan_tokens [] rev_toks = rev (EndToken :: rev_toks)
      | scan_tokens (chs as c :: cs) rev_toks =
          if is_blank c then scan_tokens cs rev_toks
          else
            (case scan_max_token chs of
              (None, _) => error ("Lexical error at: " ^ quote (implode chs))
            | (Some (tk, s), chs') => scan_tokens chs' (tk s :: rev_toks));
  in
    scan_tokens (explode str) []
  end;



(** scan variables **)

(* scan_vname *)

fun scan_vname chrs =
  let
    fun nat_of_chs n [] = n
      | nat_of_chs n (c :: cs) = nat_of_chs (n * 10 + (ord c - ord "0")) cs;

    val nat_of = nat_of_chs 0;

    fun split_vname chs =
      let val (cs, ds) = take_suffix is_digit chs
      in (implode cs, nat_of ds) end

    val scan =
      scan_letter_letdigs --
        ($$ "." -- scan_digits1 >> (nat_of o #2) || scan_empty >> K ~1);
  in
    (case scan chrs of
      ((cs, ~1), cs') => (split_vname cs, cs')
    | ((cs, i), cs') => ((implode cs, i), cs'))
  end;


(* scan_varname *)

fun scan_varname chs =
  scan_vname chs handle LEXICAL_ERROR
    => error ("scan_varname: bad varname " ^ quote (implode chs));


(* scan_var *)

fun scan_var str =
  let
    fun tvar (x, i) = Var (("'" ^ x, i), dummyT);
    fun var x_i = Var (x_i, dummyT);
    fun free x = Free (x, dummyT);

    val scan =
      $$ "?" -- $$ "'" -- scan_vname -- scan_end >> (tvar o #2 o #1) ||
      $$ "?" -- scan_vname -- scan_end >> (var o #2 o #1) ||
      scan_rest >> (free o implode);
  in
    #1 (scan (explode str))
  end;


end;