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