author | wenzelm |
Thu, 27 May 2010 18:10:37 +0200 | |
changeset 37146 | f652333bbf8e |
parent 32960 | 69916a850301 |
child 41589 | bbd861837ebc |
permissions | -rw-r--r-- |
19093 | 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 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
41 |
NONE => [] |
19093 | 42 |
| SOME (x,s') => x::(take_at_most s' (n-1)) |
43 |
||
44 |
fun length' s n = |
|
45 |
case pull s of |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
46 |
NONE => n |
19093 | 47 |
| SOME (_, s') => length' s' (n+1) |
48 |
||
49 |
fun length s = length' s 0 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
50 |
|
19093 | 51 |
end |
52 |
||
53 |
||
54 |
structure StringScannerSeq : |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
55 |
sig |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
56 |
include MONO_EXTENDED_SCANNER_SEQ |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
57 |
val fromString : string -> seq |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
58 |
end |
19093 | 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 |