<commit_before>(*  Title:      Pure/Syntax/lexicon.ML
    ID:         $Id$
    Author:     <NAME> and <NAME>, TU Muenchen

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

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

signature SCANNER =
sig
  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
  val max_of: ('a -> ('b * string) * 'a) -> ('a -> ('b * string) * 'a)
    -> 'a -> ('b * string) option * 'a
  val scan_id: string list -> string * string list
  val scan_tid: string list -> string * string list
  val scan_nat: string list -> string * string list
  type lexicon
  val dest_lexicon: lexicon -> string list
  val empty_lexicon: lexicon
  val extend_lexicon: lexicon -> string list -> lexicon
  val make_lexicon: string list -> lexicon
  val merge_lexicons: lexicon -> lexicon -> lexicon
  val scan_literal: lexicon -> string list -> string * string list
end;

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
  val const: string -> term
  val free: string -> term
  val var: indexname -> term
end;

signature LEXICON =
sig
  include SCANNER
  include LEXICON0
  val is_xid: string -> bool
  val is_tid: string -> bool
  datatype token =
    Token of string |
    IdentSy of string |
    VarSy of string |
    TFreeSy of string |
    TVarSy of string |
    NumSy of string |
    StrSy of string |
    EndToken
  val idT: typ
  val varT: typ
  val tidT: typ
  val tvarT: typ
  val terminals: string list
  val is_terminal: string -> bool
  val str_of_token: token -> string
  val display_token: token -> string
  val matching_tokens: token * token -> bool
  val token_assoc: (token option * 'a list) list * token -> 'a list
  val valued_token: token -> bool
  val predef_term: string -> token option
  val tokenize: lexicon -> bool -> string -> token list
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_tid 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 **)<commit_msg>Now string_of_vname checks for the empty variable name, catching the exception LIST.<commit_after>(*  Title:      Pure/Syntax/lexicon.ML
    ID:         $Id$
    Author:     <NAME> and <NAME>, TU Muenchen

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

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

signature SCANNER =
sig
  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
  val max_of: ('a -> ('b * string) * 'a) -> ('a -> ('b * string) * 'a)
    -> 'a -> ('b * string) option * 'a
  val scan_id: string list -> string * string list
  val scan_tid: string list -> string * string list
  val scan_nat: string list -> string * string list
  type lexicon
  val dest_lexicon: lexicon -> string list
  val empty_lexicon: lexicon
  val extend_lexicon: lexicon -> string list -> lexicon
  val make_lexicon: string list -> lexicon
  val merge_lexicons: lexicon -> lexicon -> lexicon
  val scan_literal: lexicon -> string list -> string * string list
end;

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
  val const: string -> term
  val free: string -> term
  val var: indexname -> term
end;

signature LEXICON =
sig
  include SCANNER
  include LEXICON0
  val is_xid: string -> bool
  val is_tid: string -> bool
  datatype token =
    Token of string |
    IdentSy of string |
    VarSy of string |
    TFreeSy of string |
    TVarSy of string |
    NumSy of string |
    StrSy of string |
    EndToken
  val idT: typ
  val varT: typ
  val tidT: typ
  val tvarT: typ
  val terminals: string list
  val is_terminal: string -> bool
  val str_of_token: token -> string
  val display_token: token -> string
  val matching_tokens: token * token -> bool
  val token_assoc: (token option * 'a list) list * token -> 'a list
  val valued_token: token -> bool
  val predef_term: string -> token option
  val tokenize: lexicon -> bool -> string -> token list
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_tid 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)
    handle LIST _ => "?NULL_VARIABLE." ^ si
  end;



(** datatype token **)
{'fraction_non_alphanumeric': 0.15432006010518406, 'fraction_numerical': 0.002404207362885049, 'mean_word_length': 2.595894111291194, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 170, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '487381', 'n_tokens_mistral': 2480, 'n_tokens_neox': 2418, 'n_words': 879}