src/HOL/Import/mono_seq.ML

fixed proof

(*  Title:      HOL/Import/mono_seq.ML
    ID:         $Id$
    Author:     Steven Obua, TU Muenchen

    Monomorphic sequences.
*)

(* The trouble is that signature / structures cannot depend on type variable parameters ... *)

signature MONO_SCANNER_SEQ =
sig
    type seq
    type item
    
    val pull : seq -> (item * seq) option 
end

signature MONO_EXTENDED_SCANNER_SEQ =
sig

  include MONO_SCANNER_SEQ

  val null : seq -> bool
  val length : seq -> int
  val take_at_most : seq -> int -> item list

end

functor MonoExtendScannerSeq (structure Seq : MONO_SCANNER_SEQ) : MONO_EXTENDED_SCANNER_SEQ =
struct
  
type seq = Seq.seq
type item = Seq.item
val pull = Seq.pull

fun null s = is_none (pull s)

fun take_at_most s n = 
    if n <= 0 then [] else
    case pull s of 
	NONE => []
      | SOME (x,s') => x::(take_at_most s' (n-1))

fun length' s n = 
    case pull s of
	NONE => n
      | SOME (_, s') => length' s' (n+1)

fun length s = length' s 0
		
end  


structure StringScannerSeq : 
	  sig 
	      include MONO_EXTENDED_SCANNER_SEQ 
	      val fromString : string -> seq
	  end
  =
struct

structure Incubator : MONO_SCANNER_SEQ =
struct

type seq = string * int * int
type item = string

fun pull (s, len, i) = if i >= len then NONE else SOME (String.substring (s, i, 1), (s, len, i+1))
end

structure Extended = MonoExtendScannerSeq (structure Seq = Incubator)
open Extended

fun fromString s = (s, String.size s, 0)

end