1structure Coding :> Coding =
2struct
3
4open optmonad
5infix >- >> ++ >->
6
7val || = op++
8
9type 'a reader = (string*int,'a) optmonad
10
11fun getc (s,i) = if i >= size s then NONE
12                 else SOME ((s, i + 1), String.sub(s,i))
13
14fun present_at (s,i) s2 =
15  if size s2 + i > size s then false
16  else
17    let
18      fun recurse d =
19        d < 0 orelse
20        String.sub(s, i + d) = String.sub(s2, d) andalso
21        recurse (d - 1)
22    in
23      recurse (size s2 - 1)
24    end
25
26fun literal s (si as (s0,i)) =
27  if present_at si s then SOME ((s0, i + size s), s)
28  else NONE
29
30fun takeP P (s,i) = let
31  fun recurse i = if i >= size s then i
32                  else if P (String.sub(s,i)) then recurse (i + 1)
33                  else i
34  val p = recurse i
35in
36  SOME ((s,p), String.substring(s,i,p-i))
37end
38
39fun eof (si as (s,i)) = if i >= size s then SOME (si, ()) else NONE
40fun chop j (si as (s,i)) =
41  if i + j <= size s then
42    SOME ((s, i + j), String.substring(s,i,j))
43  else NONE
44
45fun lift df s =
46  case df (s,0) of
47      SOME ((s',i), r) => if i = size s' then SOME r else NONE
48    | _ => NONE
49
50infix >*
51fun (f >* g) = f >- (fn x => g >- (fn y => return (x,y)))
52fun map f m = m >- (return o f)
53
54structure IntData =
55struct
56
57
58fun encode i = Int.toString i ^ "."
59val reader =
60   (((literal "~" >> return ~1) ++ (literal "-" >> return ~1) ++
61     return 1) >- (fn sign =>
62    takeP Char.isDigit >- (fn digits =>
63    if digits = "" then fail
64    else literal "." >> let
65      val n = (sign * valOf (Int.fromString digits))
66    in return n end handle Option => fail))) ++
67  fail
68
69val decode = lift reader
70
71
72end;
73
74fun length_encoded df = let
75  open IntData
76in
77  reader >- (fn len =>
78  chop len >- (fn pfx =>
79    case df pfx of
80      NONE => fail
81    | SOME r => return r))
82end
83
84
85structure CharData =
86struct
87  fun encode c = IntData.encode (ord c)
88  fun i2c i = return (chr i) handle Chr => fail
89  val reader = IntData.reader >- i2c
90  val decode = lift reader
91end
92
93structure StringData =
94struct
95
96fun encode s = let
97  val s' = String.toString s
98  val sz = size s'
99in
100  IntData.encode sz ^ s'
101end
102
103val reader = length_encoded String.fromString
104
105val decode = lift reader
106
107fun encodel slist = let
108  val dlist = List.map encode slist
109in
110  String.concat dlist
111end
112
113val decodel = lift (many reader)
114
115end (* string struct *)
116
117structure BoolData =
118struct
119
120  fun encode true = "T"
121    | encode false = "F"
122  val reader = (literal "T" >> return true) ++ (literal "F" >> return false)
123  val decode = lift reader
124end
125
126structure OptionData =
127struct
128
129  fun encode f NONE = "N"
130    | encode f (SOME x) = "S" ^ f x
131  fun reader f = (literal "N" >> return NONE) ++ (literal "S" >> f >- (return o SOME))
132  fun decode f = lift (reader f)
133end
134
135structure PairData =
136struct
137   fun encode (af, bf) (a,b) = af a ^ "," ^ bf b
138   fun reader (af, bf) = af >* (literal "," >> bf)
139   fun decode (af, bf) = lift (reader (af, bf))
140end
141
142structure KernelNameData =
143struct
144   fun encode {Name,Thy} =
145       PairData.encode (StringData.encode, StringData.encode) (Thy,Name)
146   val reader = PairData.reader (StringData.reader, StringData.reader) >-
147                (fn (Thy,Name) => return {Thy = Thy, Name = Name})
148   val decode = lift reader
149end
150
151end (* struct *)
152