diff -r fe45fbb111c5 -r abc7f90188af ProgTutorial/FirstSteps.thy --- a/ProgTutorial/FirstSteps.thy Fri Apr 03 07:55:07 2009 +0100 +++ b/ProgTutorial/FirstSteps.thy Tue Apr 07 17:04:39 2009 +0100 @@ -1554,6 +1554,68 @@ valid local theory. *} +ML{*signature UNIVERSAL_TYPE = +sig + type t + + val embed: unit -> ('a -> t) * (t -> 'a option) +end*} + +ML{*structure U:> UNIVERSAL_TYPE = + struct + type t = exn + + fun 'a embed () = + let + exception E of 'a + fun project (e: t): 'a option = + case e of + E a => SOME a + | _ => NONE + in + (E, project) + end + end*} + +text {* + The idea is that type t is the universal type and that each call to embed + returns a new pair of functions (inject, project), where inject embeds a + value into the universal type and project extracts the value from the + universal type. A pair (inject, project) returned by embed works together in + that project u will return SOME v if and only if u was created by inject + v. If u was created by a different function inject', then project returns + NONE. + + in library.ML +*} + +ML_val{*structure Object = struct type T = exn end; *} + +ML{*functor Test (U: UNIVERSAL_TYPE): sig end = + struct + val (intIn: int -> U.t, intOut) = U.embed () + val r: U.t ref = ref (intIn 13) + val s1 = + case intOut (!r) of + NONE => "NONE" + | SOME i => Int.toString i + val (realIn: real -> U.t, realOut) = U.embed () + val () = r := realIn 13.0 + val s2 = + case intOut (!r) of + NONE => "NONE" + | SOME i => Int.toString i + val s3 = + case realOut (!r) of + NONE => "NONE" + | SOME x => Real.toString x + val () = warning (concat [s1, " ", s2, " ", s3, "\n"]) + end*} + +ML_val{*structure t = Test(U) *} + +ML_val{*structure Datatab = TableFun(type key = int val ord = int_ord);*} + section {* Storing Theorems\label{sec:storing} (TBD) *} text {* @{ML PureThy.add_thms_dynamic} *}