src/HOL/Import/seq.ML
author wenzelm
Fri Dec 17 17:43:54 2010 +0100 (2010-12-17)
changeset 41229 d797baa3d57c
parent 40627 becf5d5187cc
permissions -rw-r--r--
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
obua@19089
     1
signature SCANNER_SEQ =
obua@19089
     2
sig
obua@19089
     3
    type 'a seq
obua@19089
     4
    
obua@19089
     5
    val pull : 'a seq -> ('a * 'a seq) option 
obua@19089
     6
end
obua@19089
     7
obua@19089
     8
signature EXTENDED_SCANNER_SEQ =
obua@19089
     9
sig
obua@19089
    10
obua@19089
    11
  include SCANNER_SEQ
obua@19089
    12
obua@19089
    13
  val null : 'a seq -> bool
obua@19089
    14
  val length : 'a seq -> int
obua@19089
    15
  val take_at_most : 'a seq -> int -> 'a list
obua@19089
    16
obua@19089
    17
end
obua@19089
    18
obua@19089
    19
functor ExtendScannerSeq (structure Seq : SCANNER_SEQ) : EXTENDED_SCANNER_SEQ =
obua@19089
    20
struct
obua@19089
    21
  
obua@19089
    22
type 'a seq = 'a Seq.seq
obua@19089
    23
obua@19089
    24
val pull = Seq.pull
obua@19089
    25
obua@19089
    26
fun null s = is_none (pull s)
obua@19089
    27
obua@19089
    28
fun take_at_most s n = 
obua@19089
    29
    if n <= 0 then [] else
obua@19089
    30
    case pull s of 
wenzelm@32960
    31
        NONE => []
obua@19089
    32
      | SOME (x,s') => x::(take_at_most s' (n-1))
obua@19089
    33
obua@19089
    34
fun length' s n = 
obua@19089
    35
    case pull s of
wenzelm@32960
    36
        NONE => n
obua@19089
    37
      | SOME (_, s') => length' s' (n+1)
obua@19089
    38
obua@19089
    39
fun length s = length' s 0
wenzelm@32960
    40
                
obua@19089
    41
end  
obua@19089
    42
obua@19089
    43
signature VECTOR_SCANNER_SEQ = 
obua@19089
    44
sig
obua@19089
    45
    include EXTENDED_SCANNER_SEQ
obua@19089
    46
obua@19089
    47
    val fromString : string -> string seq
obua@19089
    48
    val fromVector : 'a Vector.vector -> 'a seq
obua@19089
    49
end
obua@19089
    50
obua@19089
    51
structure VectorScannerSeq :> VECTOR_SCANNER_SEQ =
obua@19089
    52
struct
obua@19089
    53
  
obua@19089
    54
structure Incubator : SCANNER_SEQ =
obua@19089
    55
struct
obua@19089
    56
obua@19089
    57
type 'a seq = 'a Vector.vector * int * int
obua@19089
    58
fun pull (v, len, i) = if i >= len then NONE else SOME (Vector.sub (v, i), (v, len, i+1))
obua@19089
    59
obua@19089
    60
end
obua@19089
    61
obua@19089
    62
structure Extended = ExtendScannerSeq (structure Seq = Incubator)
obua@19089
    63
obua@19089
    64
open Extended
obua@19089
    65
obua@19089
    66
fun fromVector v = (v, Vector.length v, 0)
obua@19089
    67
fun vector_from_string s = Vector.tabulate (String.size s, fn i => String.str (String.sub (s, i)))
obua@19089
    68
fun fromString s = fromVector (vector_from_string s)
obua@19089
    69
obua@19089
    70
end
obua@19089
    71
obua@19089
    72
signature LIST_SCANNER_SEQ =
obua@19089
    73
sig
obua@19089
    74
    include EXTENDED_SCANNER_SEQ
obua@19089
    75
    
obua@19089
    76
    val fromString : string -> string seq
obua@19089
    77
    val fromList : 'a list -> 'a seq
obua@19089
    78
end
obua@19089
    79
obua@19089
    80
structure ListScannerSeq :> LIST_SCANNER_SEQ =
obua@19089
    81
struct
obua@19089
    82
     
obua@19089
    83
structure Incubator : SCANNER_SEQ =
obua@19089
    84
struct
obua@19089
    85
obua@19089
    86
type 'a seq = 'a list
obua@19089
    87
fun pull [] = NONE
obua@19089
    88
  | pull (x::xs) = SOME (x, xs)
obua@19089
    89
obua@19089
    90
end
obua@19089
    91
obua@19089
    92
structure Extended = ExtendScannerSeq (structure Seq = Incubator)
obua@19089
    93
obua@19089
    94
open Extended
obua@19089
    95
obua@19089
    96
val fromList = I
wenzelm@40627
    97
val fromString = raw_explode
obua@19089
    98
obua@19089
    99
end