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