# HG changeset patch # User Christian Urban # Date 1254490694 -7200 # Node ID ce754ad78bc9146d02496ab2d085e5e5b4f1597f # Parent f76135c6c52747e11c0bd97025427e2a1a45a18b more work on the storing section diff -r f76135c6c527 -r ce754ad78bc9 ProgTutorial/FirstSteps.thy --- a/ProgTutorial/FirstSteps.thy Thu Oct 01 10:19:21 2009 +0200 +++ b/ProgTutorial/FirstSteps.thy Fri Oct 02 15:38:14 2009 +0200 @@ -187,8 +187,8 @@ be displayed by the infrastructure. - (FIXME Mention how to work with @{ML_ind debug in Toplevel} and - @{ML_ind profiling in Toplevel}.) + \footnote{\bf FIXME Mention how to work with @{ML_ind debug in Toplevel} and + @{ML_ind profiling in Toplevel}.} *} (* FIXME @@ -610,7 +610,7 @@ "acc_incs 1 ||>> (fn x => (x, x + 2))" "(((((\"\", 1), 2), 3), 4), 6)"} - (FIXME: maybe give a ``real world'' example for this combinator) + \footnote{\bf FIXME: maybe give a ``real world'' example for this combinator.} *} text {* @@ -678,9 +678,9 @@ contains further information about combinators. \end{readmore} - (FIXME: find a good exercise for combinators) + \footnote{\bf FIXME: find a good exercise for combinators} - (FIXME: say something about calling conventions) + \footnote{\bf FIXME: say something about calling conventions} *} @@ -798,9 +798,9 @@ @{text "> "}~@{thm TrueConj_def} \end{isabelle} - (FIXME give a better example why bindings are important; maybe + \footnote{\bf FIXME give a better example why bindings are important; maybe give a pointer to \isacommand{local\_setup}; if not, then explain - why @{ML snd} is needed) + why @{ML snd} is needed.} It is also possible to define your own antiquotations. But you should exercise care when introducing new ones, as they can also make your code @@ -844,20 +844,32 @@ \end{readmore} *} -section {* Storing Data in Isabelle (TBD) *} +section {* Storing Data in Isabelle *} text {* - Isabelle provides mechanisms to store (and retrieve) arbitrary data. Before we - explain them, let us digress: Convenitional wisdom has it that - ML's type-system ensures that for example an @{ML_type "'a list"} can only - hold elements of the same type, namely @{ML_type "'a"}. Still, by some arguably - accidental features of ML, one can implement a universal type. In Isabelle it - is implemented as @{ML_type Universal.universal}. This type allows one to - inject and project elements of different type into for example into a list. - We will show this by storing an integer and boolean in a list. What is important - that access to the data is done in a type-safe manner. + Isabelle provides mechanisms for storing (and retrieving) arbitrary + data. Before we delve into the details, let us digress a bit. Conventional + wisdom has it that the type-system of ML ensures that for example an + @{ML_type "'a list"} can only hold elements of the same type, namely + @{ML_type "'a"}. Despite this wisdom, however, it is possible to implement a + universal type in ML, although by some arguably accidental features of ML. + This universal type can be used to store data of different type into a single list. + It allows one to inject and to project data of \emph{arbitrary} type. This is + in contrast to datatypes, which only allow injection and projection of data for + some fixed collection of types. In light of the conventional wisdom cited + above it is important to keep in mind that the universal type does not + destroy type-safety of ML: storing and accessing the data can only be done + in a type-safe manner. - Let us first define projection and injection functions for booleans and integers. + \begin{readmore} + In Isabelle the universal type is implemented as the type @{ML_type + Universal.universal} in the file + @{ML_file "Pure/ML-Systems/universal.ML"}. + \end{readmore} + + We will show the usage of the universal type by storing an integer and + a boolean into a single list. Let us first define injection and projection + functions for booleans and integers into and from @{ML_type Universal.universal}. *} ML{*local @@ -871,34 +883,216 @@ end*} text {* - We can now build a list injecting @{ML_text "13"} and @{ML_text "true"} as - its two elements. -*} - -ML{* val list = [inject_int 13, inject_bool true]*} - -ML {* - project_int (nth list 0) + Using the injection functions, we can inject the integer @{ML_text "13"} + and the boolean @{ML_text "true"} into @{ML_type Universal.universal}, and + then store them in a @{ML_type "Universal.universal list"} as follows: *} -ML {* - project_bool (nth list 1) +ML{*val foo_list = +let + val thirteen = inject_int 13 + val truth_val = inject_bool true +in + [thirteen, truth_val] +end*} + +text {* + The data can be retrieved using the projection functions. + + @{ML_response [display, gray] +"(project_int (nth foo_list 0), project_bool (nth foo_list 1))" +"(13, true)"} + + Notice that we access the integer as an integer and the boolean as + a boolean. If we attempt to access the integer as a boolean, then we get + a runtime error. + + @{ML_response_fake [display, gray] +"project_bool (nth foo_list 0)" +"*** Exception- Match raised"} + + This runtime error is the reason why ML is still type-sound despite + containing a universal type. + + Now, Isabelle heavily uses this mechanism to store all sorts of data: theorem lists, + simpsets, facts etc. Roughly speaking, there are two places where data can + be stored: in \emph{theories} and in \emph{proof contexts}. Again + roughly speaking, data such as simpsets need to be stored in a theory, + since they need to be maintained across proofs and even theories. + On the other hands, data such as facts change inside a proof and + therefore need to be maintained inside a proof + context.\footnote{\bf TODO: explain more bout this.} + + For both theories and proof contexts there are convenient functors that help + with the data storage. Below we show how to implement a table in which we + can store theorems that can be looked up according to a string key. The + intention is to be able to look up introduction rules for logical + connectives. Such a table might be useful in an automatic proof procedure + and therefore it makes sense to store this data inside a theory. The code + for the table is: *} -ML {* - Context.the_thread_data (); - Context.display_names @{theory}; - Context.pretty_thy @{theory} - |> Pretty.string_of - |> tracing +ML %linenosgray{*structure Data = TheoryDataFun + (type T = thm Symtab.table + val empty = Symtab.empty + val copy = I + val extend = I + fun merge _ = Symtab.merge (K true))*} + +text {* + In order to store data in a theory, we have to specify the type of the data + (Line 2). In this case we specify the type @{ML_type "thm Symtab.table"}, which + stands for tables in which @{ML_type string}s can be looked up producing an associated + @{ML_type thm}. We also have to specify four functions: how to initialise + the data storage (Line 3), how to copy it (Line 4), how to extend it (Line + 5) and how two tables should be merged (Line 6). These functions correspond + roughly to the operations performed on theories.\footnote{\bf FIXME: Say more + about the assumptions of these operations.} The result structure @{ML_text Data} + contains functions for accessing the table (@{ML Data.get}) and for updating + it (@{ML Data.map}). There are also two more functions, which however we + ignore here. Below we define two auxiliary functions, which help us with + accessing the table. +*} + +ML{*val lookup = Symtab.lookup o Data.get +fun update k v = Data.map (Symtab.update (k, v))*} + +text {* + Since we want to store introduction rules associated with their + logical connective, we can fill the table as follows. +*} + +setup %gray {* + update "op &" @{thm conjI} #> + update "op -->" @{thm impI} #> + update "All" @{thm allI} *} text {* + The use of \isacommand{setup} makes sure the table in the current theory + is updated. The lookup can now be performed as follows. + + @{ML_response_fake [display, gray] +"lookup @{theory} \"op &\"" +"SOME \"\?P; ?Q\ \ ?P \ ?Q\""} + + An important point to note is that these tables (and data in general) + need to be treated in a purely functional fashion. Although + we can update the table as follows +*} + +setup %gray {* update "op &" @{thm TrueI} *} + +text {* + and lookup now produces the introduction rule for @{term "True"} + +@{ML_response_fake [display, gray] +"lookup @{theory} \"op &\"" +"SOME \"True\""} + + there are no references involved. This is one of the most fundamental + coding conventions for programming in Isabelle. References would interfere + with the multithreaded execution model of Isabelle.\footnote{\bf FIXME: say more} + \begin{readmore} - @{ML_file "Pure/ML-Systems/universal.ML"} + Isabelle contains implementations of several container data structures, + including association lists in @{ML_file "Pure/General/alist.ML"}, + tables and symtables in @{ML_file "Pure/General/table.ML"}, and + directed graphs in @{ML_file "Pure/General/graph.ML"}. + \end{readmore} + + Storing data in a proof context is similar. With the following code we + can store a list of terms in a proof context. +*} + +ML{*structure Data = ProofDataFun + (type T = term list + val init = (K []))*} + +text {* + The function we have to specify has to produce a list once a context + is initialised (taking the theory into account from which the + context is derived). We choose to just return the empty list. Next + we define two auxiliary functions for updating the list with a given + term and printing the list. +*} + +ML{*fun update trm = Data.map (fn xs => trm::xs) + +fun print ctxt = + case (Data.get ctxt) of + [] => tracing "Empty!" + | xs => tracing (string_of_terms ctxt xs)*} + +text {* + Next we start with the context given by @{text "@{context}"} and + update it in various ways. + + @{ML_response_fake [display,gray] +"let + val ctxt = @{context} + val ctxt' = ctxt |> update @{term \"False\"} + |> update @{term \"True \ True\"} + val ctxt'' = ctxt |> update @{term \"1::nat\"} + val ctxt''' = ctxt'' |> update @{term \"2::nat\"} +in + print ctxt; + print ctxt'; + print ctxt''; + print ctxt''' +end" +"Empty! +True \ True, False +1 +2, 1"} + + Many functions in Isabelle manage and update data in a similar + fashion. Consequently, such calculation with contexts occur frequently in + Isabelle code, although the ``context flow'' is usually only linear. + + A special instance of the mechanisms described above are configuration + values. They are used to in order to configure tools by the user without + having to resort to the ML-level. Assume you want the user to control three + values, say @{text bval} containing a boolean, @{text ival} containing an + integer and @{text sval} containing a string. These values can be declared + by +*} + +ML{*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 needs to be given a default. To enable these values, they need to + be set up with +*} + +setup %gray {* + setup_bval #> + setup_ival +*} + +text {* + The user can now manipulate the values from the user-level of Isabelle + with the command +*} + +declare [[bval = true, ival = 3]] + +text {* + On the ML-level these values can be retrieved using the + function @{ML Config.get}: + + @{ML_response [display,gray] "Config.get @{context} bval" "true"} + + \begin{readmore} + For more information about configuration values see + @{ML_file "Pure/Isar/attrib.ML"} and @{ML_file "Pure/config.ML"}. \end{readmore} *} + + (**************************************************) (* bak *) (**************************************************) diff -r f76135c6c527 -r ce754ad78bc9 ProgTutorial/Parsing.thy --- a/ProgTutorial/Parsing.thy Thu Oct 01 10:19:21 2009 +0200 +++ b/ProgTutorial/Parsing.thy Fri Oct 02 15:38:14 2009 +0200 @@ -697,6 +697,7 @@ | evenS: "odd n \ even (Suc n)" | oddS: "even n \ odd (Suc n)" + text {* For this we are going to use the parser: *} @@ -980,10 +981,10 @@ text {* but you will not see any action as we chose to implement this command to do - nothing. The point of this command is to only show the procedure of how + nothing. The point of this command is only to show the procedure of how to interact with ProofGeneral. A similar procedure has to be done with any other new command, and also any new keyword that is introduced with - @{ML_ind OuterKeyword.keyword}. + the function @{ML_ind keyword in OuterKeyword}. For example: *} ML{*val _ = OuterKeyword.keyword "blink" *} @@ -1005,13 +1006,12 @@ ML{*let fun trace_prop str = - LocalTheory.theory (fn lthy => (tracing str; lthy)) + LocalTheory.theory (fn ctxt => (tracing str; ctxt)) - val trace_prop_parser = OuterParse.prop >> trace_prop val kind = OuterKeyword.thy_decl in OuterSyntax.local_theory "foobar_trace" "traces a proposition" - kind trace_prop_parser + kind (OuterParse.prop >> trace_prop) end *} text {* @@ -1036,28 +1036,28 @@ OuterKeyword} to @{ML thy_goal in OuterKeyword} then the keyword file needs to be re-created! - Below we change \isacommand{foobar\_trace} so that it takes a proposition as - argument and then starts a proof in order to prove it. Therefore in Line 13, - we set the kind indicator to @{ML thy_goal in OuterKeyword}. + Below we show the command \isacommand{foobar\_goal} which takes a + proposition as argument and then starts a proof in order to prove + it. Therefore in Line 9, we set the kind indicator to @{ML thy_goal in + OuterKeyword}. *} ML%linenosgray{*let - fun prove_prop str lthy = + fun goal_prop str lthy = let val prop = Syntax.read_prop lthy str in Proof.theorem_i NONE (K I) [[(prop,[])]] lthy - end; + end - val prove_prop_parser = OuterParse.prop >> prove_prop val kind = OuterKeyword.thy_goal in - OuterSyntax.local_theory_to_proof "foobar_goal" "proving a proposition" - kind prove_prop_parser + OuterSyntax.local_theory_to_proof "foobar_goal" "proves a proposition" + kind (OuterParse.prop >> goal_prop) end *} text {* - The function @{text prove_prop} in Lines 2 to 7 takes a string (the proposition to be + The function @{text goal_prop} in Lines 2 to 7 takes a string (the proposition to be proved) and a context as argument. The context is necessary in order to be able to use @{ML_ind read_prop in Syntax}, which converts a string into a proper proposition. In Line 6 the function @{ML_ind theorem_i in Proof} starts the proof for the @@ -1083,6 +1083,7 @@ done text {* + {\bf TBD below} (FIXME: read a name and show how to store theorems; see @{ML_ind note in LocalTheory}) diff -r f76135c6c527 -r ce754ad78bc9 ProgTutorial/ROOT.ML --- a/ProgTutorial/ROOT.ML Thu Oct 01 10:19:21 2009 +0200 +++ b/ProgTutorial/ROOT.ML Fri Oct 02 15:38:14 2009 +0200 @@ -20,8 +20,6 @@ use_thy "Recipes/Antiquotes"; use_thy "Recipes/TimeLimit"; use_thy "Recipes/Timing"; -use_thy "Recipes/Config"; -use_thy "Recipes/StoringData"; use_thy "Recipes/ExternalSolver"; use_thy "Recipes/Oracle"; use_thy "Recipes/Sat"; diff -r f76135c6c527 -r ce754ad78bc9 ProgTutorial/Recipes/Config.thy --- a/ProgTutorial/Recipes/Config.thy Thu Oct 01 10:19:21 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,82 +0,0 @@ -theory Config -imports "../Base" -begin - -section {* Configuration Options\label{rec:config} *} - -text {* - {\bf Problem:} - 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 - - Assume you want to control three values, say @{text bval} containing a - boolean, @{text ival} containing an integer and @{text sval} - containing a string. These values can be declared on the ML-level by -*} - -ML{*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 needs to be given a default. To enable these values, they need to - be set up with -*} - -setup {* setup_bval *} -setup {* setup_ival *} - -text {* or on the ML-level with *} - -ML{*setup_sval @{theory} *} - -text {* - The user can now manipulate the values from within Isabelle with the command -*} - -declare [[bval = true, ival = 3]] - -text {* - On the ML-level these values can be retrieved using the - function @{ML Config.get}: - - @{ML_response [display,gray] "Config.get @{context} bval" "true"} - - @{ML_response [display,gray] "Config.get @{context} ival" "3"} - - The function @{ML Config.put} manipulates the values. For example - - @{ML_response [display,gray] "Config.put sval \"foo\" @{context}; Config.get @{context} sval" "foo"} - - The same can be achieved using the command \isacommand{setup}. -*} - -setup {* Config.put_thy sval "bar" *} - -text {* - Now the retrieval of this value yields: - - @{ML_response [display,gray] "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,gray] -"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} - - There are many good reasons to control parameters in this way. One is - that no global reference is needed, which would cause many headaches - with the multithreaded execution of Isabelle. -*} - -end \ No newline at end of file diff -r f76135c6c527 -r ce754ad78bc9 ProgTutorial/Recipes/StoringData.thy --- a/ProgTutorial/Recipes/StoringData.thy Thu Oct 01 10:19:21 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,46 +0,0 @@ -theory StoringData -imports "../Base" -begin - -section {* Storing Data (TBD)\label{rec:storingdata} *} - - -text {* - {\bf Problem:} - Your tool needs to manage data.\smallskip - - {\bf Solution:} This can be achieved using a generic data slot.\smallskip - - Every generic data slot may keep data of any kind which is stored in the - context. - - *} - -ML{*local - -structure Data = GenericDataFun - ( type T = int Symtab.table - val empty = Symtab.empty - val extend = I - fun merge _ = Symtab.merge (K true) - ) - -in - val lookup = Symtab.lookup o Data.get - fun update k v = Data.map (Symtab.update (k, v)) -end *} - -setup {* Context.theory_map (update "foo" 1) *} - -text {* - - @{ML_response [display,gray] "lookup (Context.Proof @{context}) \"foo\"" "SOME 1"} - - -*} - -text {* - alternatives: TheoryDataFun, ProofDataFun - Code: Pure/context.ML *} - -end \ No newline at end of file diff -r f76135c6c527 -r ce754ad78bc9 progtutorial.pdf Binary file progtutorial.pdf has changed