1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/libisabelle-protocol/libisabelle/protocol/codec.ML Tue Sep 04 14:50:30 2018 +0200
1.3 @@ -0,0 +1,248 @@
1.4 +signature CODEC = sig
1.5 + datatype 'a result = Success of 'a | Failure of string * XML.body
1.6 + datatype ('a, 'b) either = Left of 'a | Right of 'b
1.7 + type 'a codec
1.8 +
1.9 + val the_success: 'a result -> 'a
1.10 +
1.11 + val map_result: ('a -> 'b) -> 'a result -> 'b result
1.12 + val bind_result: ('a -> 'b result) -> 'a result -> 'b result
1.13 + val sequence_results: 'a result list -> 'a list result
1.14 + val traverse_results: ('a -> 'b result) -> 'a list -> 'b list result
1.15 +
1.16 + val transform: ('a -> 'b) -> ('b -> 'a) -> 'a codec -> 'b codec
1.17 + val encode: 'a codec -> 'a -> XML.tree
1.18 + val decode: 'a codec -> XML.tree -> 'a result
1.19 + val the_decode: 'a codec -> XML.tree -> 'a
1.20 +
1.21 + val basic: {encode: 'a -> XML.tree, decode: XML.tree -> 'a result} -> 'a codec
1.22 +
1.23 + val variant: ('a -> (int * XML.tree)) -> (int -> (XML.tree -> 'a result) option) -> string -> 'a codec
1.24 + val tagged: string -> 'a codec -> 'a codec
1.25 +
1.26 + val unit: unit codec
1.27 + val bool: bool codec
1.28 + val string: string codec
1.29 + val int: int codec
1.30 + val list: 'a codec -> 'a list codec
1.31 + val tuple: 'a codec -> 'b codec -> ('a * 'b) codec
1.32 + val triple: 'a codec -> 'b codec -> 'c codec -> ('a * 'b * 'c) codec
1.33 + val either: 'a codec -> 'b codec -> ('a, 'b) either codec
1.34 + val option: 'a codec -> 'a option codec
1.35 + val tree: XML.tree codec
1.36 +
1.37 + val sort: sort codec
1.38 + val typ: typ codec
1.39 + val term: term codec
1.40 +
1.41 + exception GENERIC of string
1.42 + val exn: exn codec
1.43 + val exn_result: 'a codec -> 'a Exn.result codec
1.44 +
1.45 + (* internal *)
1.46 + val id: XML.tree codec
1.47 +end
1.48 +
1.49 +structure Codec: CODEC = struct
1.50 +
1.51 +datatype 'a result = Success of 'a | Failure of string * XML.body
1.52 +datatype ('a, 'b) either = Left of 'a | Right of 'b
1.53 +
1.54 +fun map_result f (Success a) = Success (f a)
1.55 + | map_result _ (Failure (msg, body)) = Failure (msg, body)
1.56 +
1.57 +fun bind_result f (Success a) = f a
1.58 + | bind_result _ (Failure (msg, body)) = Failure (msg, body)
1.59 +
1.60 +fun traverse_results _ [] = Success []
1.61 + | traverse_results f (x :: xs) =
1.62 + case f x of
1.63 + Success y => map_result (fn ys => y :: ys) (traverse_results f xs)
1.64 + | Failure (msg, body) => Failure (msg, body)
1.65 +
1.66 +fun sequence_results xs = traverse_results I xs
1.67 +
1.68 +fun the_success (Success a) = a
1.69 + | the_success _ = raise Fail "unexpected failure"
1.70 +
1.71 +fun add_tag tag idx body =
1.72 + let
1.73 + val attrs = case idx of SOME i => [("idx", XML.Encode.int_atom i)] | _ => []
1.74 + in XML.Elem (("tag", ("type", tag) :: attrs), body) end
1.75 +
1.76 +fun expect_tag tag tree =
1.77 + case tree of
1.78 + XML.Elem (("tag", [("type", tag')]), body) =>
1.79 + if tag = tag' then
1.80 + Success body
1.81 + else
1.82 + Failure ("tag mismatch: expected " ^ tag ^ ", got " ^ tag', [tree])
1.83 + | _ =>
1.84 + Failure ("tag " ^ tag ^ " expected", [tree])
1.85 +
1.86 +fun expect_tag' tag tree =
1.87 + case tree of
1.88 + XML.Elem (("tag", [("type", tag'), ("idx", i)]), body) =>
1.89 + if tag = tag' then
1.90 + Success (XML.Decode.int_atom i, body)
1.91 + handle XML.XML_ATOM err => Failure (err, [tree])
1.92 + else
1.93 + Failure ("tag mismatch: expected " ^ tag ^ ", got " ^ tag', [tree])
1.94 + | _ =>
1.95 + Failure ("indexed tag " ^ tag ^ " expected", [tree])
1.96 +
1.97 +
1.98 +abstype 'a codec = Codec of {encode: 'a -> XML.tree, decode: XML.tree -> 'a result} with
1.99 +
1.100 +val basic = Codec
1.101 +
1.102 +fun encode (Codec {encode, ...}) = encode
1.103 +fun decode (Codec {decode, ...}) = decode
1.104 +
1.105 +fun transform f g (Codec {encode, decode}) = Codec
1.106 + {encode = g #> encode,
1.107 + decode = decode #> map_result f}
1.108 +
1.109 +fun list a = Codec
1.110 + {encode = map (encode a) #> add_tag "list" NONE,
1.111 + decode = expect_tag "list" #> bind_result (traverse_results (decode a))}
1.112 +
1.113 +fun tuple a b = Codec
1.114 + {encode = (fn (x, y) => add_tag "tuple" NONE [encode a x, encode b y]),
1.115 + decode = expect_tag "tuple" #> bind_result (fn body =>
1.116 + case body of
1.117 + [x, y] => decode a x |> bind_result (fn x' => decode b y |> map_result (pair x'))
1.118 + | _ => Failure ("invalid structure", body))}
1.119 +
1.120 +fun variant enc dec tag = Codec
1.121 + {encode = (fn a => let val (idx, tree) = enc a in add_tag tag (SOME idx) [tree] end),
1.122 + decode = (fn tree => expect_tag' tag tree |> bind_result (fn (idx, body) =>
1.123 + case (body, dec idx) of
1.124 + ([tree'], SOME res) => res tree'
1.125 + | (_, SOME _) => Failure ("invalid structure", [tree])
1.126 + | (_, NONE) => Failure ("invalid index " ^ print_int idx, [tree])))}
1.127 +
1.128 +fun tagged tag a = Codec
1.129 + {encode = encode a #> single #> add_tag tag NONE,
1.130 + decode = expect_tag tag #> bind_result (fn body =>
1.131 + case body of
1.132 + [tree] => decode a tree
1.133 + | _ => Failure ("invalid structure", body))}
1.134 +
1.135 +val unit = Codec
1.136 + {encode = K (add_tag "unit" NONE []),
1.137 + decode = expect_tag "unit" #> bind_result (fn body =>
1.138 + case body of
1.139 + [] => Success ()
1.140 + | _ => Failure ("expected nothing", body))}
1.141 +
1.142 +fun text to from = Codec
1.143 + {encode = fn s => XML.Elem (("text", [("content", encode_string (to s))]), []),
1.144 + decode =
1.145 + (fn tree as XML.Elem (("text", [("content", s)]), []) =>
1.146 + (case from (decode_string s) of
1.147 + NONE => Failure ("decoding failed", [tree]) |
1.148 + SOME a => Success a)
1.149 + | tree => Failure ("expected text tree", [tree]))}
1.150 +
1.151 +val id = Codec {encode = I, decode = Success}
1.152 +
1.153 +end
1.154 +
1.155 +fun the_decode c = the_success o decode c
1.156 +
1.157 +val int = tagged "int" (text print_int (Exn.get_res o Exn.capture parse_int))
1.158 +val bool = tagged "bool" (text print_bool (Exn.get_res o Exn.capture parse_bool))
1.159 +val string = tagged "string" (text I SOME)
1.160 +
1.161 +val tree = tagged "XML.tree" id
1.162 +
1.163 +fun option a =
1.164 + let
1.165 + fun enc (SOME x) = (0, encode a x)
1.166 + | enc NONE = (1, encode unit ())
1.167 + fun dec 0 = SOME (decode a #> map_result SOME)
1.168 + | dec 1 = SOME (decode unit #> map_result (K NONE))
1.169 + | dec _ = NONE
1.170 + in variant enc dec "option" end
1.171 +
1.172 +val content_of =
1.173 + XML.content_of o YXML.parse_body
1.174 +
1.175 +(* slightly fishy codec, doesn't preserve exception type *)
1.176 +exception GENERIC of string
1.177 +
1.178 +fun string_of_exn (ERROR msg) = "ERROR " ^ content_of msg
1.179 + | string_of_exn exn = content_of (@{make_string} exn)
1.180 +
1.181 +val exn = tagged "exn" (text string_of_exn (SOME o GENERIC))
1.182 +
1.183 +fun exn_result a =
1.184 + let
1.185 + fun enc (Exn.Res t) = (0, encode a t)
1.186 + | enc (Exn.Exn e) = (1, encode exn e)
1.187 + fun dec _ = NONE
1.188 + in variant enc dec "Exn.result" end
1.189 +
1.190 +fun triple a b c =
1.191 + tuple a (tuple b c)
1.192 + |> transform (fn (a, (b, c)) => (a, b, c)) (fn (a, b, c) => (a, (b, c)))
1.193 +
1.194 +fun either a b =
1.195 + let
1.196 + fun enc (Left l) = (0, encode a l)
1.197 + | enc (Right r) = (1, encode b r)
1.198 + fun dec 0 = SOME (decode a #> map_result Left)
1.199 + | dec 1 = SOME (decode b #> map_result Right)
1.200 + | dec _ = NONE
1.201 + in variant enc dec "either" end
1.202 +
1.203 +val sort: sort codec = list string
1.204 +val indexname: indexname codec = tuple string int
1.205 +
1.206 +fun typ () =
1.207 + let
1.208 + fun typ_type () = tuple string (list (typ ()))
1.209 + val typ_tfree = tuple string sort
1.210 + val typ_tvar = tuple indexname sort
1.211 +
1.212 + fun enc (Type arg) = (0, encode (typ_type ()) arg)
1.213 + | enc (TFree arg) = (1, encode typ_tfree arg)
1.214 + | enc (TVar arg) = (2, encode typ_tvar arg)
1.215 + fun dec 0 = SOME (decode (typ_type ()) #> map_result Type)
1.216 + | dec 1 = SOME (decode typ_tfree #> map_result TFree)
1.217 + | dec 2 = SOME (decode typ_tvar #> map_result TVar)
1.218 + | dec _ = NONE
1.219 + in variant enc dec "typ" end
1.220 +
1.221 +val typ = typ ()
1.222 +
1.223 +fun term () =
1.224 + let
1.225 + val term_const = tuple string typ
1.226 + val term_free = tuple string typ
1.227 + val term_var = tuple indexname typ
1.228 + val term_bound = int
1.229 + fun term_abs () = triple string typ (term ())
1.230 + fun term_app () = tuple (term ()) (term ())
1.231 +
1.232 + fun enc (Const arg) = (0, encode term_const arg)
1.233 + | enc (Free arg) = (1, encode term_free arg)
1.234 + | enc (Var arg) = (2, encode term_var arg)
1.235 + | enc (Bound arg) = (3, encode term_bound arg)
1.236 + | enc (Abs arg) = (4, encode (term_abs ()) arg)
1.237 + | enc (op $ arg) = (5, encode (term_app ()) arg)
1.238 + fun dec 0 = SOME (decode term_const #> map_result Const)
1.239 + | dec 1 = SOME (decode term_free #> map_result Free)
1.240 + | dec 2 = SOME (decode term_var #> map_result Var)
1.241 + | dec 3 = SOME (decode term_bound #> map_result Bound)
1.242 + | dec 4 = SOME (decode (term_abs ()) #> map_result Abs)
1.243 + | dec 5 = SOME (decode (term_app ()) #> map_result op $)
1.244 + | dec _ = NONE
1.245 + in variant enc dec "term" end
1.246 +
1.247 +val term = term ()
1.248 +
1.249 +end
1.250 +
1.251 +type 'a codec = 'a Codec.codec
1.252 \ No newline at end of file