src/HOL/Import/mono_seq.ML
author wenzelm
Thu May 27 18:10:37 2010 +0200 (2010-05-27)
changeset 37146 f652333bbf8e
parent 32960 69916a850301
child 41589 bbd861837ebc
permissions -rw-r--r--
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
     1 (*  Title:      HOL/Import/mono_seq.ML
     2     ID:         $Id$
     3     Author:     Steven Obua, TU Muenchen
     4 
     5     Monomorphic sequences.
     6 *)
     7 
     8 (* The trouble is that signature / structures cannot depend on type variable parameters ... *)
     9 
    10 signature MONO_SCANNER_SEQ =
    11 sig
    12     type seq
    13     type item
    14     
    15     val pull : seq -> (item * seq) option 
    16 end
    17 
    18 signature MONO_EXTENDED_SCANNER_SEQ =
    19 sig
    20 
    21   include MONO_SCANNER_SEQ
    22 
    23   val null : seq -> bool
    24   val length : seq -> int
    25   val take_at_most : seq -> int -> item list
    26 
    27 end
    28 
    29 functor MonoExtendScannerSeq (structure Seq : MONO_SCANNER_SEQ) : MONO_EXTENDED_SCANNER_SEQ =
    30 struct
    31   
    32 type seq = Seq.seq
    33 type item = Seq.item
    34 val pull = Seq.pull
    35 
    36 fun null s = is_none (pull s)
    37 
    38 fun take_at_most s n = 
    39     if n <= 0 then [] else
    40     case pull s of 
    41         NONE => []
    42       | SOME (x,s') => x::(take_at_most s' (n-1))
    43 
    44 fun length' s n = 
    45     case pull s of
    46         NONE => n
    47       | SOME (_, s') => length' s' (n+1)
    48 
    49 fun length s = length' s 0
    50                 
    51 end  
    52 
    53 
    54 structure StringScannerSeq : 
    55           sig 
    56               include MONO_EXTENDED_SCANNER_SEQ 
    57               val fromString : string -> seq
    58           end
    59   =
    60 struct
    61 
    62 structure Incubator : MONO_SCANNER_SEQ =
    63 struct
    64 
    65 type seq = string * int * int
    66 type item = string
    67 
    68 fun pull (s, len, i) = if i >= len then NONE else SOME (String.substring (s, i, 1), (s, len, i+1))
    69 end
    70 
    71 structure Extended = MonoExtendScannerSeq (structure Seq = Incubator)
    72 open Extended
    73 
    74 fun fromString s = (s, String.size s, 0)
    75 
    76 end
    77