889 val project_bool = Universal.tagProject fn_bool |
889 val project_bool = Universal.tagProject fn_bool |
890 end*} |
890 end*} |
891 |
891 |
892 text {* |
892 text {* |
893 Using the injection functions, we can inject the integer @{ML_text "13"} |
893 Using the injection functions, we can inject the integer @{ML_text "13"} |
894 and the boolean @{ML_text "true"} into @{ML_type Universal.universal}, and |
894 and the boolean value @{ML_text "true"} into @{ML_type Universal.universal}, and |
895 then store them in a @{ML_type "Universal.universal list"} as follows: |
895 then store them in a @{ML_type "Universal.universal list"} as follows: |
896 *} |
896 *} |
897 |
897 |
898 ML{*val foo_list = |
898 ML{*val foo_list = |
899 let |
899 let |
1001 "SOME \"True\""} |
1001 "SOME \"True\""} |
1002 |
1002 |
1003 there are no references involved. This is one of the most fundamental |
1003 there are no references involved. This is one of the most fundamental |
1004 coding conventions for programming in Isabelle. References would |
1004 coding conventions for programming in Isabelle. References would |
1005 interfere with the multithreaded execution model of Isabelle and also |
1005 interfere with the multithreaded execution model of Isabelle and also |
1006 defeat the undo-mechanism in proof scripts. For this consider the |
1006 defeat its undo-mechanism in proof scripts. For this consider the |
1007 following data container where we maintain a reference to a list of |
1007 following data container where we maintain a reference to a list of |
1008 integers. |
1008 integers. |
1009 *} |
1009 *} |
1010 |
1010 |
1011 ML{*structure WrongRefData = TheoryDataFun |
1011 ML{*structure WrongRefData = TheoryDataFun |
1085 context is derived). We choose to just return the empty list. Next |
1085 context is derived). We choose to just return the empty list. Next |
1086 we define two auxiliary functions for updating the list with a given |
1086 we define two auxiliary functions for updating the list with a given |
1087 term and printing the list. |
1087 term and printing the list. |
1088 *} |
1088 *} |
1089 |
1089 |
1090 ML{*fun update trm = Data.map (fn xs => trm::xs) |
1090 ML{*fun update trm = Data.map (fn trms => trm::trms) |
1091 |
1091 |
1092 fun print ctxt = |
1092 fun print ctxt = |
1093 case (Data.get ctxt) of |
1093 case (Data.get ctxt) of |
1094 [] => tracing "Empty!" |
1094 [] => tracing "Empty!" |
1095 | xs => tracing (string_of_terms ctxt xs)*} |
1095 | trms => tracing (string_of_terms ctxt trms)*} |
1096 |
1096 |
1097 text {* |
1097 text {* |
1098 Next we start with the context given by the antiquotation |
1098 Next we start with the context generated by the antiquotation |
1099 @{text "@{context}"} and update it in various ways. |
1099 @{text "@{context}"} and update it in various ways. |
1100 |
1100 |
1101 @{ML_response_fake [display,gray] |
1101 @{ML_response_fake [display,gray] |
1102 "let |
1102 "let |
1103 val ctxt = @{context} |
1103 val ctxt = @{context} |
1121 Isabelle code, although the ``context flow'' is usually only linear. |
1121 Isabelle code, although the ``context flow'' is usually only linear. |
1122 Note also that the calculation above has no effect on the underlying |
1122 Note also that the calculation above has no effect on the underlying |
1123 theory. Once we throw away the contexts, we have no access to their |
1123 theory. Once we throw away the contexts, we have no access to their |
1124 associated data. This is different to theories, where the command |
1124 associated data. This is different to theories, where the command |
1125 \isacommand{setup} registers the data with the current and future |
1125 \isacommand{setup} registers the data with the current and future |
1126 theories, and therefore can access the data potentially |
1126 theories, and therefore one can access the data potentially |
1127 indefinitely.\footnote{\bf FIXME: check this; it seems that is in |
1127 indefinitely.\footnote{\bf FIXME: check this; it seems that is in |
1128 conflict with the statements below.} |
1128 conflict with the statements below.} |
1129 |
1129 |
1130 \footnote{\bf FIXME: Say something about generic contexts.} |
1130 For convenience there is an abstract layer, the type @{ML_type Context.generic}, |
|
1131 for theories and proof contexts. This type is defined as follows |
|
1132 *} |
|
1133 |
|
1134 ML_val{*datatype generic = |
|
1135 Theory of theory |
|
1136 | Proof of proof*} |
|
1137 |
|
1138 text {* |
|
1139 For this type a number of operations are defined which allow the |
|
1140 uniform treatment of theories and proof contexts. |
1131 |
1141 |
1132 There are two special instances of the data storage mechanism described |
1142 There are two special instances of the data storage mechanism described |
1133 above. The first instance are named theorem lists. Since storing theorems in a list |
1143 above. The first instance are named theorem lists. Since storing theorems in a list |
1134 is such a common task, there is the special functor @{ML_funct_ind Named_Thms}. |
1144 is such a common task, there is the special functor @{ML_funct_ind Named_Thms}. |
1135 To obtain a named theorem list, you just declare |
1145 To obtain a named theorem list, you just declare |