60   val r = ref 0

    60   val r = Unsynchronized.ref 0

   277   instantiation of @{text "?P"} and @{text "?Q"} 

   277   instantiation of @{text "?P"} and @{text "?Q"}. 

   847 section {* Storing Data in Isabelle *}

   847 section {* Storing Data in Isabelle\label{sec:storing} *}

   917   Now, Isabelle heavily uses this mechanism to store all sorts of data: theorem lists,

   917   Now, Isabelle heavily uses this mechanism for storing all sorts of

   918   simpsets, facts etc.  Roughly speaking, there are two places where data can 

   918   data: theorem lists, simpsets, facts etc.  Roughly speaking, there are two

   919   be stored: in \emph{theories} and in \emph{proof contexts}. Again

   919   places where data can be stored: in \emph{theories} and in \emph{proof

   920   roughly speaking, data such as simpsets need to be stored in a theory,

   920   contexts}. Again roughly speaking, data such as simpsets need to be stored

   921   since they need to be maintained across proofs and even theories.

   921   in a theory, since they need to be maintained across proofs and even across

   922   On the other hands, data such as facts change inside a proof and

   922   theories.  On the other hand, data such as facts change inside a proof and

   923   therefore need to be maintained inside a proof 

   923   are only relevant to the proof at hand. Therefore such data needs to be 

   924   context.\footnote{\bf TODO: explain more bout this.} 

   924   maintained inside a proof context.\footnote{\bf TODO: explain more about 

   925 

   925   this in a separate section.}

   926   For both theories and proof contexts there are convenient functors that help

   926 

   927   For theories and proof contexts there are, respectively, the functors 

   928   @{ML_funct_ind TheoryDataFun} and @{ML_funct_ind ProofDataFun} that help

   928   can store theorems that can be looked up according to a string key. The

   930   can store theorems and look them up according to a string key. The

   952   it (@{ML Data.map}). There are also two more functions, which however we

   954   it (@{ML Data.map}). There are also two more functions (@{ML Data.init} and 

   953   ignore here. Below we define two auxiliary functions, which help us with

   955   @{ML Data.put}), which however we ignore here. Below we define two auxiliary 

   954   accessing the table.

   956   functions, which help us with accessing the table.

   972   The use of \isacommand{setup} makes sure the table in the current theory 

   974   The use of the command \isacommand{setup} makes sure the table in the 

   973   is updated. The lookup can now be performed as follows.

   975   \emph{current} theory is updated. The lookup can now be performed as 

   976   follows.

   987   and lookup now produces the introduction rule for @{term "True"}

   990   and @{ML lookup} now produces the introduction rule for @{term "True"}

   994   coding conventions for programming in Isabelle. References would interfere

   997   coding conventions for programming in Isabelle. References would 

   995   with the multithreaded execution model of Isabelle.\footnote{\bf FIXME: say more}

   998   interfere with the multithreaded execution model of Isabelle and also

   996   

   999   defeat the undo-mechanism in proof scripts. For this consider the 

  1000   following data container where we maintain a reference to a list of 

  1001   integers.

  1002 *}

  1003 

  1004 ML{*structure WrongRefData = TheoryDataFun

  1005   (type T = (int list) Unsynchronized.ref

  1006    val empty = Unsynchronized.ref []

  1007    val copy = I

  1008    val extend = I

  1009    fun merge _ = fst)*}

  1010 

  1011 text {*

  1012   We initialise the reference with the empty list. Consequently a first 

  1013   lookup produces @{ML "ref []" in Unsynchronized}.

  1014 

  1015   @{ML_response_fake [display,gray]

  1016   "WrongRefData.get @{theory}"

  1017   "ref []"}

  1018 

  1019   For updating the reference we use the following function.

  1020 *}

  1021 

  1022 ML{*fun ref_update n = WrongRefData.map 

  1023       (fn r => let val _ = r := n::(!r) in r end)*}

  1024 

  1025 text {*

  1026   As above we update the reference with the command 

  1027   \isacommand{setup}. 

  1028 *}

  1029 

  1030 setup %gray{* ref_update 1 *}

  1031 

  1032 text {*

  1033   A lookup in the current theory gives then the expected list 

  1034   @{ML "ref [1]" in Unsynchronized}.

  1035 

  1036   @{ML_response_fake [display,gray]

  1037   "WrongRefData.get @{theory}"

  1038   "ref [1]"}

  1039 

  1040   So far everything is as expected. But, the trouble starts if we attempt

  1041   to backtrack to ``before'' the \isacommand{setup}-command. There, we 

  1042   would expect that the list is empty again. But since it is stored in 

  1043   a reference, Isabelle has no control over it. So it is not

  1044   empty, but still @{ML "ref [1]" in Unsynchronized}. Adding to the trouble, 

  1045   if we execute the \isacommand{setup}-command again, we do not obtain 

  1046   @{ML "ref [1]" in Unsynchronized}, but

  1047 

  1048   @{ML_response_fake [display,gray]

  1049   "WrongRefData.get @{theory}"

  1050   "ref [1, 1]"}

  1051 

  1052   Now imagine how often you go backwards and forwards in your proof scripts. 

  1053   By using references in Isabelle code, you are bound to cause all

  1054   hell to break lose. Therefore observe the coding convention: 

  1055   Do not use references for storing data!

  1056 

  1000   tables and symtables in @{ML_file "Pure/General/table.ML"}, and

  1061   directed graphs in @{ML_file "Pure/General/graph.ML"}. and 

  1001   directed graphs in @{ML_file "Pure/General/graph.ML"}.

  1062   tables and symtables in @{ML_file "Pure/General/table.ML"}.

  1004   Storing data in a proof context is similar. With the following code we

  1065   A special instance of the data storage mechanism described above are

  1005   can store a list of terms in a proof context. 

  1066   configuration values. They are used to enable users to configure tools

  1067   without having to resort to the ML-level (and also to avoid

  1068   references). Assume you want the user to control three values, say @{text

  1069   bval} containing a boolean, @{text ival} containing an integer and @{text

  1070   sval} containing a string. These values can be declared by

  1071 *}

  1072 

  1073 ML{*val (bval, setup_bval) = Attrib.config_bool "bval" false

  1074 val (ival, setup_ival) = Attrib.config_int "ival" 0

  1075 val (sval, setup_sval) = Attrib.config_string "sval" "some string" *}

  1076 

  1077 text {* 

  1078   where each value needs to be given a default. To enable these values, they need to 

  1079   be set up with

  1080 *}

  1081 

  1082 setup %gray {* 

  1083   setup_bval #> 

  1084   setup_ival 

  1085 *}

  1086 

  1087 text {*

  1088   The user can now manipulate the values from the user-level of Isabelle 

  1089   with the command

  1090 *}

  1091 

  1092 declare [[bval = true, ival = 3]]

  1093 

  1094 text {*

  1095   On the ML-level these values can be retrieved using the 

  1096   function @{ML Config.get}.

  1097 

  1098   @{ML_response [display,gray] "Config.get @{context} bval" "true"}

  1099 

  1100   \begin{readmore}

  1101   For more information about configuration values see 

  1102   @{ML_file "Pure/Isar/attrib.ML"} and @{ML_file "Pure/config.ML"}.

  1103   \end{readmore}

  1104 

  1105   Storing data in a proof context is done in a similar fashion. The

  1106   corresponding functor is @{ML_funct_ind ProofDataFun}. With the 

  1107   following code we can store a list of terms in a proof context. 

  1010    val init = (K []))*}

  1112    fun init _ = [])*}

  1028   Next we start with the context given by @{text "@{context}"} and 

  1130   Next we start with the context given by the antiquotation 

  1029   update it in various ways. 

  1131   @{text "@{context}"} and update it in various ways. 

  1052 

  1154   Note also that the calculation above has no effect on the underlying

  1053   A special instance of the mechanisms described above are configuration

  1155   theory. Once we throw away the contexts, we have no access to their

  1054   values. They are used to in order to configure tools by the user without

  1156   associated data. This is different to theories, where the command 

  1055   having to resort to the ML-level. Assume you want the user to control three

  1157   \isacommand{setup} registers the data with the current and future 

  1056   values, say @{text bval} containing a boolean, @{text ival} containing an

  1158   theories, and therefore can access the data potentially indefinitely. 

  1057   integer and @{text sval} containing a string. These values can be declared

  1058   by

  1059 *}

  1060 

  1061 ML{*val (bval, setup_bval) = Attrib.config_bool "bval" false

  1062 val (ival, setup_ival) = Attrib.config_int "ival" 0

  1063 val (sval, setup_sval) = Attrib.config_string "sval" "some string" *}

  1064 

  1065 text {* 

  1066   where each value needs to be given a default. To enable these values, they need to 

  1067   be set up with

  1068 *}

  1069 

  1070 setup %gray {* 

  1071   setup_bval #> 

  1072   setup_ival 

  1073 *}

  1074 

  1075 text {*

  1076   The user can now manipulate the values from the user-level of Isabelle 

  1077   with the command

  1078 *}

  1079 

  1080 declare [[bval = true, ival = 3]]

  1081 

  1082 text {*

  1083   On the ML-level these values can be retrieved using the 

  1084   function @{ML Config.get}:

  1085 

  1086   @{ML_response [display,gray] "Config.get @{context} bval" "true"}

  1087 

  1088   \begin{readmore}

  1089   For more information about configuration values see 

  1090   @{ML_file "Pure/Isar/attrib.ML"} and @{ML_file "Pure/config.ML"}.

  1091   \end{readmore}