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