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