# HG changeset patch # User Christian Urban # Date 1231454766 0 # Node ID 83cea5dc6bac4ca6b78e84fb61d6c2b5376f781b # Parent c3fe4749ef01ce0f74405673a074522181ad2adf tuned diff -r c3fe4749ef01 -r 83cea5dc6bac CookBook/Recipes/Config.thy --- a/CookBook/Recipes/Config.thy Wed Jan 07 16:36:31 2009 +0000 +++ b/CookBook/Recipes/Config.thy Thu Jan 08 22:46:06 2009 +0000 @@ -1,5 +1,5 @@ theory Config -imports Base +imports "../Base" begin section {* Configuration Options *} @@ -7,49 +7,80 @@ text {* {\bf Problem:} - You would like to enhance your tool with options which can be changed later on - by the user.\smallskip + You would like to enhance your tool with options that can be changed + by the user without having to resort to the ML-level.\smallskip {\bf Solution:} This can be achieved using configuration values.\smallskip - *} - -ML {* -val (bvalue, setup_bvalue) = Attrib.config_bool "bvalue" false -val (ivalue, setup_ivalue) = Attrib.config_int "ivalue" 0 -val (svalue, setup_svalue) = Attrib.config_string "svalue" "some string" -*} - -setup "setup_bvalue o setup_ivalue o setup_svalue" - -declare [[bvalue = true, ivalue = 3]] - -text {* - Note that this works without introducing a new command to modify the - configuration options. *} - -ML {* -Config.get @{context} bvalue + Assume you want to control three values, say @{ML_text bval} containing a + boolean, @{ML_text ival} containing an integer and @{ML_text sval} + containing a string. These values can be declared on the ML-level by *} ML {* -Config.get_thy @{theory} ivalue +val (bval, setup_bval) = Attrib.config_bool "bval" false +val (ival, setup_ival) = Attrib.config_int "ival" 0 +val (sval, setup_sval) = Attrib.config_string "sval" "some string" +*} + +text {* + where each value is given a default. To enable these values, they need to + be set up using +*} + +setup {* setup_bval *} +setup {* setup_ival *} + +text {* or on the ML-level *} + +ML {*setup_sval @{theory} +*} + +text {* + The user can now manipulate the values with the command *} -setup {* Config.put_thy svalue "foo" *} +declare [[bval = true, ival = 3]] + +text {* + On the ML-level these values can be retrieved using the function @{ML Config.get}: + + @{ML_response [display] "Config.get @{context} bval" "true"} -ML {* -Config.get @{context} svalue + @{ML_response [display] "Config.get @{context} ival" "3"} + + The function @{ML Config.put} manipulates the values. For example + + @{ML_response [display] "Config.put sval \"foo\" @{context}; Config.get @{context} sval" "foo"} + + The same can be achived using the command \isacommand{setup}. *} -ML {* -let val ctxt = Config.map ivalue (fn i => i + 1) @{context} -in Config.get ctxt ivalue end +setup {* Config.put_thy sval "bar" *} + +text {* + Then retrival of this value yields now + + @{ML_response [display] "Config.get @{context} sval" "\"bar\""} + + We can apply a function to a value using @{ML Config.map}. For example incrementing + @{ML ival} can be done by + + @{ML_response [display] +"let + val ctxt = Config.map ival (fn i => i + 1) @{context} +in + Config.get ctxt ival +end" "4"} + +\begin{readmore} + For more information see @{ML_file "Pure/Isar/attrib.ML"} and @{ML_file "Pure/config.ML"}. +\end{readmore} + *} text {* - Code: Pure/Isar/attrib.ML, Pure/config.ML Note: Avoid to use references for this purpose! *} diff -r c3fe4749ef01 -r 83cea5dc6bac CookBook/Recipes/NamedThms.thy --- a/CookBook/Recipes/NamedThms.thy Wed Jan 07 16:36:31 2009 +0000 +++ b/CookBook/Recipes/NamedThms.thy Thu Jan 08 22:46:06 2009 +0000 @@ -47,18 +47,21 @@ declare rule1[foo del] -text {* and query the remaining ones by: *} +text {* and query the remaining ones with: -thm foo +@{ML_response_fake_both [display] "thm foo" +"?C +?B"} -text {* On the ML-level the rules marked with @{text "foo"} an be retrieved using the function @{ML FooRules.get}: @{ML_response_fake [display] "FooRules.get @{context}" "[\"?C\",\"?B\"]"} \begin{readmore} - For more information see @{ML_file "Pure/Tools/named_thms.ML"}. + For more information see @{ML_file "Pure/Tools/named_thms.ML"} and also + the recipe in Section~\ref{recipe:storingdata} about storing arbitrary + data. \end{readmore} *} diff -r c3fe4749ef01 -r 83cea5dc6bac CookBook/Recipes/StoringData.thy --- a/CookBook/Recipes/StoringData.thy Wed Jan 07 16:36:31 2009 +0000 +++ b/CookBook/Recipes/StoringData.thy Thu Jan 08 22:46:06 2009 +0000 @@ -2,7 +2,7 @@ imports "../Base" begin -section {* Storing Data *} +section {* Storing Data\label{recipe:storingdata} *} text {* @@ -16,8 +16,7 @@ *} -ML {* -local +ML {* local structure Data = GenericDataFun ( @@ -33,8 +32,7 @@ fun update k v = Data.map (Symtab.update (k, v)) -end -*} +end *} setup {* Context.theory_map (update "foo" 1) *} diff -r c3fe4749ef01 -r 83cea5dc6bac CookBook/Recipes/TimeLimit.thy --- a/CookBook/Recipes/TimeLimit.thy Wed Jan 07 16:36:31 2009 +0000 +++ b/CookBook/Recipes/TimeLimit.thy Thu Jan 08 22:46:06 2009 +0000 @@ -1,41 +1,54 @@ theory TimeLimit -imports Base +imports "../Base" begin section {* Restricting the Runtime of a Function *} - text {* {\bf Problem:} - Your tool should run only a specified amount of seconds.\smallskip + Your tool should run only a specified amount of time.\smallskip - {\bf Solution:} This can be achieved using time limits.\smallskip + {\bf Solution:} This can be achieved using the function + @{ML timeLimit in TimeLimit}.\smallskip - Assume the following function should run only five seconds: + Assume the following well-known function: *} -ML {* +ML {* fun ackermann (0, n) = n + 1 | ackermann (m, 0) = ackermann (m - 1, 1) | ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1)) *} -ML {* ackermann (3, 12) *} +text {* + + Now the call + + @{ML_response_fake [display] "ackermann (4, 12)" "\"} -(* takes more than 10 seconds *) + takes a bit long. To avoid this, the call can be encapsulated + in a time limit of five seconds. For this you have to write: + +@{ML_response [display] +"TimeLimit.timeLimit (Time.fromSeconds 5) ackermann (4, 12) + handle TimeOut => ~1" +"~1"} -text {* - The call can be encapsulated in a time limit of five seconds as follows: - *} + where @{ML_text TimeOut} is the exception raised when the time limit + is reached. + + Note that @{ML "timeLimit" in TimeLimit} is only meaningful when you use PolyML, + because PolyML has a rich infrastructure for multithreading programming on + which @{ML "timeLimit" in TimeLimit} relies. -ML {* -TimeLimit.timeLimit (Time.fromSeconds 5) ackermann (3, 12) - handle TimeOut => ~1 +\begin{readmore} + The function @{ML "timeLimit" in TimeLimit} is defined in the structure + @{ML_struct TimeLimit} which can be found in the file + @{ML_file "Pure/ML-Systems/multithreading_polyml.ML"}. +\end{readmore} + + *} -text {* - The function "TimeLimit.timeLimit" has type "???" and is defined in - TODO: refer to code *} - end \ No newline at end of file