1247 (*

  1248 ML{*signature UNIVERSAL_TYPE =

  1249 sig

  1250   type t

  1251 

  1252   val embed: unit -> ('a -> t) * (t -> 'a option)

  1253 end*}

  1254 

  1255 ML{*structure U:> UNIVERSAL_TYPE =

  1256    struct

  1257       type t = exn

  1258 

  1259       fun 'a embed () =

  1260          let

  1261             exception E of 'a

  1262             fun project (e: t): 'a option =

  1263                case e of

  1264                   E a => SOME a

  1265                 | _ => NONE

  1266          in

  1267             (E, project)

  1268          end

  1269    end*}

  1270 

  1271 text {*

  1272   The idea is that type t is the universal type and that each call to embed

  1273   returns a new pair of functions (inject, project), where inject embeds a

  1274   value into the universal type and project extracts the value from the

  1275   universal type. A pair (inject, project) returned by embed works together in

  1276   that project u will return SOME v if and only if u was created by inject

  1277   v. If u was created by a different function inject', then project returns

  1278   NONE.

  1279 

  1280   in library.ML

  1281 *}

  1282 

  1283 ML_val{*structure Object = struct type T = exn end; *}

  1284 

  1285 ML{*functor Test (U: UNIVERSAL_TYPE): sig end =

  1286    struct

  1287       val (intIn: int -> U.t, intOut) = U.embed ()

  1288       val r: U.t ref = ref (intIn 13)

  1289       val s1 =

  1290          case intOut (!r) of

  1291             NONE => "NONE"

  1292           | SOME i => Int.toString i

  1293       val (realIn: real -> U.t, realOut) = U.embed ()

  1294       val () = r := realIn 13.0

  1295       val s2 =

  1296          case intOut (!r) of

  1297             NONE => "NONE"

  1298           | SOME i => Int.toString i

  1299       val s3 =

  1300          case realOut (!r) of

  1301             NONE => "NONE"

  1302           | SOME x => Real.toString x

  1303       val () = tracing (concat [s1, " ", s2, " ", s3, "\n"])

  1304    end*}

  1305 

  1306 ML_val{*structure t = Test(U) *} 

  1307 

  1308 ML_val{*structure Datatab = TableFun(type key = int val ord = int_ord);*}

  1309 

  1310 ML {* LocalTheory.restore *}

  1311 ML {* LocalTheory.set_group *}

  1312 *)

  1313