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

Generic scanners (for potentially infinite input).
*)

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

signature BASIC_SCAN =
sig
  (*error msg handler*)
  val !! : ('a * string option -> string) -> ('a -> 'b) -> 'a -> 'b
  (*apply function*)
  val >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
  (*alternative*)
  val || : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b
  (*sequential pairing*)
  val -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e
  (*dependent pairing*)
  val :-- : ('a -> 'b * 'c) * ('b -> 'c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e
  (*forget fst*)
  val |-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'd * 'e
  (*forget snd*)
  val --| : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'b * 'e
  (*concatenation*)
  val ^^ : ('a -> string * 'b) * ('b -> string * 'c) -> 'a -> string * 'c
  (*one element literal*)
  val $$ : ''a -> ''a list -> ''a * ''a list
end;

signature SCAN =
sig
  include BASIC_SCAN
  val fail: 'a -> 'b
  val fail_with: ('a -> string) -> 'a -> 'b
  val succeed: 'a -> 'b -> 'a * 'b
  val some: ('a -> 'b option) -> 'a list -> 'b * 'a list
  val one: ('a -> bool) -> 'a list -> 'a * 'a list
  val this: ''a list -> ''a list -> ''a list * ''a list
  val this_string: string -> string list -> string * string list
  val any: ('a -> bool) -> 'a list -> 'a list * 'a list
  val any1: ('a -> bool) -> 'a list -> 'a list * 'a list
  val optional: ('a -> 'b * 'a) -> 'b -> 'a -> 'b * 'a
  val option: ('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: ('a * 'a -> bool) -> ('b -> 'a * 'b) -> ('b -> 'a * 'b) -> 'b -> 'a * 'b
  val ahead: ('a -> 'b * 'c) -> 'a -> 'b * 'a
  val unless: ('a -> 'b * 'a) -> ('a -> 'c * 'd) -> 'a -> 'c * 'd
  val first: ('a -> 'b) list -> 'a -> 'b
  val state: 'a * 'b -> 'a * ('a * 'b)
  val depend: ('a -> 'b -> ('c * 'd) * 'e) -> 'a * 'b -> 'd * ('c * 'e)
  val peek: ('a -> 'b -> 'c * 'd) -> 'a * 'b -> 'c * ('a * 'd)
  val pass: 'a -> ('a * 'b -> 'c * ('d * 'e)) -> 'b -> 'c * 'e
  val lift: ('a -> 'b * 'c) -> 'd * 'a -> 'b * ('d * 'c)
  val trace': ('a * 'b list -> 'c * ('d * 'e list)) -> 'a * 'b list ->
    ('c * 'b list) * ('d * 'e list)
  val trace: ('a list -> 'b * 'c list) -> 'a list -> ('b * 'a list) * 'c list
  val try: ('a -> 'b) -> 'a -> 'b
  val force: ('a -> 'b) -> 'a -> 'b
  val prompt: string -> ('a -> 'b) -> 'a -> 'b
  val finite': 'a * ('a -> bool) -> ('b * 'a list -> 'c * ('d * 'a list))
    -> 'b * 'a list -> 'c * ('d * 'a list)
  val finite: 'a * ('a -> bool) -> ('a list -> 'b * 'a list) -> 'a list -> 'b * 'a list
  val read: 'a * ('a -> bool) -> ('a list -> 'b * 'a list) -> 'a list -> 'b option
  val catch: ('a -> 'b) -> 'a -> 'b
  val error: ('a -> 'b) -> 'a -> 'b
  val source': string -> (string -> 'a -> 'b list * 'a) -> ('b list * 'a -> 'c) ->
    'b * ('b -> bool) -> ('d * 'b list -> 'e list * ('d * 'b list)) ->
    ('d * 'b list -> 'e list * ('d * 'b list)) option -> 'd * 'a -> 'e list * ('d * 'c)
  val source: string -> (string -> 'a -> 'b list * 'a) -> ('b list * 'a -> 'c) ->
    'b * ('b -> bool) -> ('b list -> 'd list * 'b list) ->
    ('b list -> 'd list * 'b list) option -> 'a -> 'd list * 'c
  val single: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
  val bulk: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
  type lexicon
  val dest_lexicon: lexicon -> string list
  val make_lexicon: string list list -> lexicon
  val empty_lexicon: lexicon
  val extend_lexicon: lexicon -> string list list -> lexicon
  val merge_lexicons: lexicon -> lexicon -> lexicon
  val is_literal: lexicon -> string list -> bool
  val literal: lexicon -> string list -> string list * string list
end;

structure Scan: SCAN =
struct


(** scanners **)

exception MORE of string option;        (*need more input (prompt)*)
exception FAIL of string option;        (*try alternatives (reason of failure)*)
exception ABORT of string;              (*dead end*)


(* scanner combinators *)

(*dependent pairing*)
fun (scan1 :-- scan2) toks =
  let
    val (x, toks2) = scan1 toks;
    val (y, toks3) = scan2 x toks2;
  in ((x, y), toks3) end;

(*sequential pairing*)
fun (scan1 -- scan2) toks =
  let
    val (x, toks2) = scan1 toks;
    val (y, toks3) = scan2 toks2;
  in ((x, y), toks3) end;

(*application*)
fun (scan >> f) toks =
  let val (x, toks2) = scan toks;
  in (f x, toks2) end;

(*forget snd*)
fun (scan1 --| scan2) toks =
  let
    val (x, toks2) = scan1 toks;
    val (_, toks3) = scan2 toks2;
  in (x, toks3) end;

(*forget fst*)
fun (scan1 |-- scan2) toks =
  let val (_, toks2) = scan1 toks;
  in scan2 toks2 end;

(*concatenation*)
fun (scan1 ^^ scan2) toks =
  let
    val (x, toks2) = scan1 toks;
    val (y, toks3) = scan2 toks2;
  in (x ^ y, toks3) end;

(*alternative*)
fun (scan1 || scan2) toks = scan1 toks handle FAIL _ => scan2 toks;


(* generic scanners *)

fun fail _ = raise FAIL NONE;
fun fail_with msg_of xs = raise FAIL (SOME (msg_of xs));
fun succeed y xs = (y, xs);

fun some _ [] = raise MORE NONE
  | some f (x :: xs) =
      (case f x of SOME y => (y, xs) | _ => raise FAIL NONE);

fun one _ [] = raise MORE NONE
  | one pred (x :: xs) =
      if pred x then (x, xs) else raise FAIL NONE;

fun $$ _ [] = raise MORE NONE
  | $$ a (x :: xs) =
      if a = x then (x, xs) else raise FAIL NONE;

fun this ys xs =
  let
    fun drop_prefix [] xs = xs
      | drop_prefix (_ :: _) [] = raise MORE NONE
      | drop_prefix (y :: ys) (x :: xs) =
          if y = x then drop_prefix ys xs else raise FAIL NONE;
  in (ys, drop_prefix ys xs) end;
<commit_msg>made $$ and "this" monomorphic (string);<commit_after>(*  Title:      Pure/General/scan.ML
    ID:         $Id$
    Author:     <NAME> and <NAME>, TU Muenchen

Generic scanners (for potentially infinite input).
*)

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

signature BASIC_SCAN =
sig
  (*error msg handler*)
  val !! : ('a * string option -> string) -> ('a -> 'b) -> 'a -> 'b
  (*apply function*)
  val >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
  (*alternative*)
  val || : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b
  (*sequential pairing*)
  val -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e
  (*dependent pairing*)
  val :-- : ('a -> 'b * 'c) * ('b -> 'c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e
  (*forget fst*)
  val |-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'd * 'e
  (*forget snd*)
  val --| : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'b * 'e
  (*concatenation*)
  val ^^ : ('a -> string * 'b) * ('b -> string * 'c) -> 'a -> string * 'c
  (*one element literal*)
  val $$ : string -> string list -> string * string list
end;

signature SCAN =
sig
  include BASIC_SCAN
  val fail: 'a -> 'b
  val fail_with: ('a -> string) -> 'a -> 'b
  val succeed: 'a -> 'b -> 'a * 'b
  val some: ('a -> 'b option) -> 'a list -> 'b * 'a list
  val one: ('a -> bool) -> 'a list -> 'a * 'a list
  val this: string list -> string list -> string list * string list
  val this_string: string -> string list -> string * string list
  val any: ('a -> bool) -> 'a list -> 'a list * 'a list
  val any1: ('a -> bool) -> 'a list -> 'a list * 'a list
  val optional: ('a -> 'b * 'a) -> 'b -> 'a -> 'b * 'a
  val option: ('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: ('a * 'a -> bool) -> ('b -> 'a * 'b) -> ('b -> 'a * 'b) -> 'b -> 'a * 'b
  val ahead: ('a -> 'b * 'c) -> 'a -> 'b * 'a
  val unless: ('a -> 'b * 'a) -> ('a -> 'c * 'd) -> 'a -> 'c * 'd
  val first: ('a -> 'b) list -> 'a -> 'b
  val state: 'a * 'b -> 'a * ('a * 'b)
  val depend: ('a -> 'b -> ('c * 'd) * 'e) -> 'a * 'b -> 'd * ('c * 'e)
  val peek: ('a -> 'b -> 'c * 'd) -> 'a * 'b -> 'c * ('a * 'd)
  val pass: 'a -> ('a * 'b -> 'c * ('d * 'e)) -> 'b -> 'c * 'e
  val lift: ('a -> 'b * 'c) -> 'd * 'a -> 'b * ('d * 'c)
  val trace': ('a * 'b list -> 'c * ('d * 'e list)) -> 'a * 'b list ->
    ('c * 'b list) * ('d * 'e list)
  val trace: ('a list -> 'b * 'c list) -> 'a list -> ('b * 'a list) * 'c list
  val try: ('a -> 'b) -> 'a -> 'b
  val force: ('a -> 'b) -> 'a -> 'b
  val prompt: string -> ('a -> 'b) -> 'a -> 'b
  val finite': 'a * ('a -> bool) -> ('b * 'a list -> 'c * ('d * 'a list))
    -> 'b * 'a list -> 'c * ('d * 'a list)
  val finite: 'a * ('a -> bool) -> ('a list -> 'b * 'a list) -> 'a list -> 'b * 'a list
  val read: 'a * ('a -> bool) -> ('a list -> 'b * 'a list) -> 'a list -> 'b option
  val catch: ('a -> 'b) -> 'a -> 'b
  val error: ('a -> 'b) -> 'a -> 'b
  val source': string -> (string -> 'a -> 'b list * 'a) -> ('b list * 'a -> 'c) ->
    'b * ('b -> bool) -> ('d * 'b list -> 'e list * ('d * 'b list)) ->
    ('d * 'b list -> 'e list * ('d * 'b list)) option -> 'd * 'a -> 'e list * ('d * 'c)
  val source: string -> (string -> 'a -> 'b list * 'a) -> ('b list * 'a -> 'c) ->
    'b * ('b -> bool) -> ('b list -> 'd list * 'b list) ->
    ('b list -> 'd list * 'b list) option -> 'a -> 'd list * 'c
  val single: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
  val bulk: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
  type lexicon
  val dest_lexicon: lexicon -> string list
  val make_lexicon: string list list -> lexicon
  val empty_lexicon: lexicon
  val extend_lexicon: lexicon -> string list list -> lexicon
  val merge_lexicons: lexicon -> lexicon -> lexicon
  val is_literal: lexicon -> string list -> bool
  val literal: lexicon -> string list -> string list * string list
end;

structure Scan: SCAN =
struct


(** scanners **)

exception MORE of string option;        (*need more input (prompt)*)
exception FAIL of string option;        (*try alternatives (reason of failure)*)
exception ABORT of string;              (*dead end*)


(* scanner combinators *)

(*dependent pairing*)
fun (scan1 :-- scan2) toks =
  let
    val (x, toks2) = scan1 toks;
    val (y, toks3) = scan2 x toks2;
  in ((x, y), toks3) end;

(*sequential pairing*)
fun (scan1 -- scan2) toks =
  let
    val (x, toks2) = scan1 toks;
    val (y, toks3) = scan2 toks2;
  in ((x, y), toks3) end;

(*application*)
fun (scan >> f) toks =
  let val (x, toks2) = scan toks;
  in (f x, toks2) end;

(*forget snd*)
fun (scan1 --| scan2) toks =
  let
    val (x, toks2) = scan1 toks;
    val (_, toks3) = scan2 toks2;
  in (x, toks3) end;

(*forget fst*)
fun (scan1 |-- scan2) toks =
  let val (_, toks2) = scan1 toks;
  in scan2 toks2 end;

(*concatenation*)
fun (scan1 ^^ scan2) toks =
  let
    val (x, toks2) = scan1 toks;
    val (y, toks3) = scan2 toks2;
  in (x ^ y, toks3) end;

(*alternative*)
fun (scan1 || scan2) toks = scan1 toks handle FAIL _ => scan2 toks;


(* generic scanners *)

fun fail _ = raise FAIL NONE;
fun fail_with msg_of xs = raise FAIL (SOME (msg_of xs));
fun succeed y xs = (y, xs);

fun some _ [] = raise MORE NONE
  | some f (x :: xs) =
      (case f x of SOME y => (y, xs) | _ => raise FAIL NONE);

fun one _ [] = raise MORE NONE
  | one pred (x :: xs) =
      if pred x then (x, xs) else raise FAIL NONE;

fun $$ _ [] = raise MORE NONE
  | $$ a (x :: xs) =
      if (a: string) = x then (x, xs) else raise FAIL NONE;

fun this ys xs =
  let
    fun drop_prefix [] xs = xs
      | drop_prefix (_ :: _) [] = raise MORE NONE
      | drop_prefix (y :: ys) (x :: xs) =
          if (y: string) = x then drop_prefix ys xs else raise FAIL NONE;
  in (ys, drop_prefix ys xs) end;

{'fraction_non_alphanumeric': 0.2424427214914191, 'fraction_numerical': 0.008537329035630281, 'mean_word_length': 2.1677704194260485, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 393, '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': '6781355', 'n_tokens_mistral': 4807, 'n_tokens_neox': 4696, 'n_words': 1708}