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