src/Pure/General/source.ML
author wenzelm
Fri Dec 14 11:52:54 2001 +0100 (2001-12-14)
changeset 12498 3b0091bf06e8
parent 10746 01e2d857fb78
child 14727 ab06e87e5c83
permissions -rw-r--r--
changed Thm.varifyT';
wenzelm@6118
     1
(*  Title:      Pure/General/source.ML
wenzelm@6116
     2
    ID:         $Id$
wenzelm@6116
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@8806
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@6116
     5
wenzelm@8806
     6
Coalgebraic data sources -- efficient purely functional input streams.
wenzelm@6116
     7
*)
wenzelm@6116
     8
wenzelm@6116
     9
signature SOURCE =
wenzelm@6116
    10
sig
wenzelm@6116
    11
  type ('a, 'b) source
wenzelm@6681
    12
  val default_prompt: string
wenzelm@6116
    13
  val set_prompt: string -> ('a, 'b) source -> ('a, 'b) source
wenzelm@6116
    14
  val get: ('a, 'b) source -> 'a list * ('a, 'b) source
wenzelm@6116
    15
  val unget: 'a list * ('a, 'b) source -> ('a, 'b) source
wenzelm@6116
    16
  val get_single: ('a, 'b) source -> ('a * ('a, 'b) source) option
wenzelm@6116
    17
  val exhaust: ('a, 'b) source -> 'a list
wenzelm@6116
    18
  val mapfilter: ('a -> 'b option) -> ('a, 'c) source -> ('b, ('a, 'c) source) source
wenzelm@6116
    19
  val filter: ('a -> bool) -> ('a, 'b) source -> ('a, ('a, 'b) source) source
wenzelm@6116
    20
  val of_list: 'a list -> ('a, 'a list) source
wenzelm@6116
    21
  val of_string: string -> (string, string list) source
wenzelm@9123
    22
  val exhausted: ('a, 'b) source -> ('a, 'a list) source
wenzelm@6116
    23
  val of_stream: TextIO.instream -> TextIO.outstream -> (string, unit) source
wenzelm@6116
    24
  val tty: (string, unit) source
wenzelm@6116
    25
  val source': 'a -> 'b * ('b -> bool) -> ('a * 'b list -> 'c list * ('a * 'b list)) ->
wenzelm@10746
    26
    ('a * 'b list -> 'c list * ('a * 'b list)) option ->
wenzelm@6116
    27
    ('b, 'e) source -> ('c, 'a * ('b, 'e) source) source
wenzelm@6116
    28
  val source: 'a * ('a -> bool) -> ('a list -> 'b list * 'a list) ->
wenzelm@10746
    29
    ('a list -> 'b list * 'a list) option ->
wenzelm@6116
    30
    ('a, 'd) source -> ('b, ('a, 'd) source) source
wenzelm@6116
    31
end;
wenzelm@6116
    32
wenzelm@6116
    33
structure Source: SOURCE =
wenzelm@6116
    34
struct
wenzelm@6116
    35
wenzelm@6116
    36
wenzelm@6116
    37
(** datatype source **)
wenzelm@6116
    38
wenzelm@6116
    39
datatype ('a, 'b) source =
wenzelm@6116
    40
  Source of
wenzelm@6116
    41
   {buffer: 'a list,
wenzelm@6116
    42
    info: 'b,
wenzelm@6116
    43
    prompt: string,
wenzelm@6116
    44
    drain: string -> 'b -> 'a list * 'b};
wenzelm@6116
    45
wenzelm@6116
    46
fun make_source buffer info prompt drain =
wenzelm@6116
    47
  Source {buffer = buffer, info = info, prompt = prompt, drain = drain};
wenzelm@6116
    48
wenzelm@6116
    49
wenzelm@6116
    50
(* prompt *)
wenzelm@6116
    51
wenzelm@6116
    52
val default_prompt = "> ";
wenzelm@6116
    53
wenzelm@6116
    54
fun set_prompt prompt (Source {buffer, info, prompt = _, drain}) =
wenzelm@6116
    55
  make_source buffer info prompt drain;
wenzelm@6116
    56
wenzelm@6116
    57
wenzelm@6116
    58
(* get / unget *)
wenzelm@6116
    59
wenzelm@6116
    60
fun get (Source {buffer = [], info, prompt, drain}) =
wenzelm@6116
    61
      let val (xs, info') = drain prompt info
wenzelm@6116
    62
      in (xs, make_source [] info' prompt drain) end
wenzelm@6116
    63
  | get (Source {buffer, info, prompt, drain}) =
wenzelm@6116
    64
      (buffer, make_source [] info prompt drain);
wenzelm@6116
    65
wenzelm@6116
    66
fun unget (xs, Source {buffer, info, prompt, drain}) =
wenzelm@6116
    67
  make_source (xs @ buffer) info prompt drain;
wenzelm@6116
    68
wenzelm@6116
    69
wenzelm@6116
    70
(* variations on get *)
wenzelm@6116
    71
wenzelm@6116
    72
fun get_prompt prompt src = get (set_prompt prompt src);
wenzelm@6116
    73
wenzelm@6116
    74
fun get_single src =
wenzelm@6116
    75
  (case get src of
wenzelm@6116
    76
    ([], _) => None
wenzelm@6116
    77
  | (x :: xs, src') => Some (x, unget (xs, src')));
wenzelm@6116
    78
wenzelm@6116
    79
fun exhaust src =
wenzelm@6116
    80
  (case get src of
wenzelm@6116
    81
    ([], _) => []
wenzelm@6116
    82
  | (xs, src') => xs @ exhaust src');
wenzelm@6116
    83
wenzelm@6116
    84
wenzelm@6116
    85
(* (map)filter *)
wenzelm@6116
    86
wenzelm@6116
    87
fun drain_mapfilter f prompt src =
wenzelm@6116
    88
  let
wenzelm@6116
    89
    val (xs, src') = get_prompt prompt src;
wenzelm@6116
    90
    val xs' = Library.mapfilter f xs;
wenzelm@6116
    91
  in
wenzelm@6116
    92
    if null xs orelse not (null xs') then (xs', src')
wenzelm@6116
    93
    else drain_mapfilter f prompt src'
wenzelm@6116
    94
  end;
wenzelm@6116
    95
wenzelm@6116
    96
fun mapfilter f src = make_source [] src default_prompt (drain_mapfilter f);
wenzelm@6116
    97
fun filter pred = mapfilter (fn x => if pred x then Some x else None);
wenzelm@6116
    98
wenzelm@6116
    99
wenzelm@6116
   100
wenzelm@6116
   101
(** build sources **)
wenzelm@6116
   102
wenzelm@6116
   103
(* list source *)
wenzelm@6116
   104
wenzelm@6116
   105
(*limiting the input buffer considerably improves performance*)
wenzelm@6116
   106
val limit = 4000;
wenzelm@6116
   107
wenzelm@6116
   108
fun drain_list _ xs = (take (limit, xs), drop (limit, xs));
wenzelm@6116
   109
wenzelm@6116
   110
fun of_list xs = make_source [] xs default_prompt drain_list;
wenzelm@6116
   111
val of_string = of_list o explode;
wenzelm@6181
   112
wenzelm@9123
   113
fun exhausted src = of_list (exhaust src);
wenzelm@9123
   114
wenzelm@6116
   115
wenzelm@6116
   116
(* stream source *)
wenzelm@6116
   117
wenzelm@6116
   118
fun drain_stream instream outstream prompt () =
wenzelm@6681
   119
  (TextIO.output (outstream, prompt);
wenzelm@6116
   120
    TextIO.flushOut outstream;
wenzelm@6116
   121
    (explode (TextIO.inputLine instream), ()));
wenzelm@6116
   122
wenzelm@6116
   123
fun of_stream instream outstream =
wenzelm@6116
   124
  make_source [] () default_prompt (drain_stream instream outstream);
wenzelm@6116
   125
wenzelm@6116
   126
val tty = of_stream TextIO.stdIn TextIO.stdOut;
wenzelm@6116
   127
wenzelm@6116
   128
wenzelm@6116
   129
wenzelm@6116
   130
(** compose sources **)
wenzelm@6116
   131
wenzelm@6116
   132
fun drain_source source stopper scan recover prompt src =
wenzelm@6116
   133
  source prompt get_prompt unget stopper scan recover src;
wenzelm@6116
   134
wenzelm@6116
   135
wenzelm@6116
   136
(* state-based *)
wenzelm@6116
   137
wenzelm@6116
   138
fun source' init_state stopper scan recover src =
wenzelm@6116
   139
  make_source [] (init_state, src) default_prompt
wenzelm@6116
   140
    (drain_source Scan.source' stopper scan recover);
wenzelm@6116
   141
wenzelm@6116
   142
wenzelm@6116
   143
(* non state-based *)
wenzelm@6116
   144
wenzelm@6116
   145
fun source stopper scan recover src =
wenzelm@6116
   146
  make_source [] src default_prompt
wenzelm@6116
   147
    (drain_source Scan.source stopper scan recover);
wenzelm@6116
   148
wenzelm@6116
   149
wenzelm@6116
   150
end;