190   (FIXME Mention how to work with @{ML_ind  debug in Toplevel} and 

   190   \footnote{\bf FIXME Mention how to work with @{ML_ind  debug in Toplevel} and 

   191   @{ML_ind  profiling in Toplevel}.)

   191   @{ML_ind  profiling in Toplevel}.}

   613   (FIXME: maybe give a ``real world'' example for this combinator)

   613   \footnote{\bf FIXME: maybe give a ``real world'' example for this combinator.}

   681   (FIXME: find a good exercise for combinators)

   681   \footnote{\bf FIXME: find a good exercise for combinators}

   682 

   682 

   683   (FIXME: say something about calling conventions) 

   683   \footnote{\bf FIXME: say something about calling conventions} 

   801   (FIXME give a better example why bindings are important; maybe

   801   \footnote{\bf FIXME give a better example why bindings are important; maybe

   803   why @{ML snd} is needed)

   803   why @{ML snd} is needed.}

   847 section {* Storing Data in Isabelle (TBD) *}

   847 section {* Storing Data in Isabelle *}

   848 

   848 

   849 text {*

   849 text {*

   850   Isabelle provides mechanisms to store (and retrieve) arbitrary data. Before we 

   850   Isabelle provides mechanisms for storing (and retrieving) arbitrary

   851   explain them, let us digress: Convenitional wisdom has it that 

   851   data. Before we delve into the details, let us digress a bit. Conventional

   852   ML's type-system ensures that for example an @{ML_type "'a list"} can only

   852   wisdom has it that the type-system of ML ensures that for example an

   853   hold elements of the same type, namely @{ML_type "'a"}. Still, by some arguably

   853   @{ML_type "'a list"} can only hold elements of the same type, namely

   854   accidental features of ML, one can implement a universal type. In Isabelle it

   854   @{ML_type "'a"}. Despite this wisdom, however, it is possible to implement a

   855   is implemented as @{ML_type Universal.universal}. This type allows one to

   855   universal type in ML, although by some arguably accidental features of ML.

   856   inject and project elements of different type into for example into a list.

   856   This universal type can be used to store data of different type into a single list.

   857   We will show this by storing an integer and boolean in a list. What is important

   857   It allows one to inject and to project data of \emph{arbitrary} type. This is

   858   that access to the data is done in a type-safe manner. 

   858   in contrast to datatypes, which only allow injection and projection of data for

   859 

   859   some fixed collection of types. In light of the conventional wisdom cited

   860   Let us first define projection and injection functions for booleans and integers.

   860   above it is important to keep in mind that the universal type does not

   861   destroy type-safety of ML: storing and accessing the data can only be done

   862   in a type-safe manner.

   863 

   864   \begin{readmore}

   865   In Isabelle the universal type is implemented as the type @{ML_type

   866   Universal.universal} in the file

   867   @{ML_file "Pure/ML-Systems/universal.ML"}.

   868   \end{readmore}

   869 

   870   We will show the usage of the universal type by storing an integer and

   871   a boolean into a single list. Let us first define injection and projection 

   872   functions for booleans and integers into and from @{ML_type Universal.universal}.

   874   We can now build a list injecting @{ML_text "13"} and @{ML_text "true"} as

   886   Using the injection functions, we can inject the integer @{ML_text "13"} 

   875   its two elements.

   887   and the boolean @{ML_text "true"} into @{ML_type Universal.universal}, and

   876 *}

   888   then store them in a @{ML_type "Universal.universal list"} as follows:

   877 

   889 *}

   878 ML{* val list = [inject_int 13, inject_bool true]*}

   890 

   879 

   891 ML{*val foo_list = 

   880 ML {*

   892 let

   881  project_int (nth list 0)

   893   val thirteen  = inject_int 13

   882 *}

   894   val truth_val = inject_bool true

   883 

   895 in

   884 ML {*

   896   [thirteen, truth_val]

   885  project_bool (nth list 1)

   897 end*}

   886 *}

   898 

   887 

   899 text {*

   888 ML {* 

   900   The data can be retrieved using the projection functions.

   889   Context.the_thread_data ();

   901   

   890   Context.display_names @{theory};

   902   @{ML_response [display, gray]

   891   Context.pretty_thy @{theory}

   903 "(project_int (nth foo_list 0), project_bool (nth foo_list 1))" 

   892     |> Pretty.string_of

   904 "(13, true)"}

   893     |> tracing

   905 

   894 *}

   906   Notice that we access the integer as an integer and the boolean as

   895 

   907   a boolean. If we attempt to access the integer as a boolean, then we get 

   896 text {*

   908   a runtime error. 

   909   

   910   @{ML_response_fake [display, gray]

   911 "project_bool (nth foo_list 0)"  

   912 "*** Exception- Match raised"}

   913 

   914   This runtime error is the reason why ML is still type-sound despite

   915   containing a universal type.

   916 

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

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

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

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

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

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

   923   therefore need to be maintained inside a proof 

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

   925 

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

   927   with the data storage. Below we show how to implement a table in which we

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

   929   intention is to be able to look up introduction rules for logical

   930   connectives. Such a table might be useful in an automatic proof procedure

   931   and therefore it makes sense to store this data inside a theory.  The code

   932   for the table is:

   933 *}

   934 

   935 ML %linenosgray{*structure Data = TheoryDataFun

   936   (type T = thm Symtab.table

   937    val empty = Symtab.empty

   938    val copy = I

   939    val extend = I

   940    fun merge _ = Symtab.merge (K true))*}

   941 

   942 text {*

   943   In order to store data in a theory, we have to specify the type of the data

   944   (Line 2). In this case we specify the type @{ML_type "thm Symtab.table"}, which 

   945   stands for tables in which @{ML_type string}s can be looked up producing an associated

   946   @{ML_type thm}. We also have to specify four functions: how to initialise

   947   the data storage (Line 3), how to copy it (Line 4), how to extend it (Line

   948   5) and how two tables should be merged (Line 6). These functions correspond

   949   roughly to the operations performed on theories.\footnote{\bf FIXME: Say more

   950   about the assumptions of these operations.} The result structure @{ML_text Data}

   951   contains functions for accessing the table (@{ML Data.get}) and for updating

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

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

   954   accessing the table.

   955 *}

   956 

   957 ML{*val lookup = Symtab.lookup o Data.get

   958 fun update k v = Data.map (Symtab.update (k, v))*}

   959 

   960 text {*

   961   Since we want to store introduction rules associated with their 

   962   logical connective, we can fill the table as follows.

   963 *}

   964 

   965 setup %gray {*

   966   update "op &"   @{thm conjI} #>

   967   update "op -->" @{thm impI}  #>

   968   update "All"    @{thm allI}

   969 *}

   970 

   971 text {*

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

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

   974 

   975   @{ML_response_fake [display, gray]

   976 "lookup @{theory} \"op &\""

   977 "SOME \"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\""}

   978 

   979   An important point to note is that these tables (and data in general)

   980   need to be treated in a purely functional fashion. Although

   981   we can update the table as follows

   982 *}

   983 

   984 setup %gray {* update "op &" @{thm TrueI} *}

   985 

   986 text {*

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

   988   

   989 @{ML_response_fake [display, gray]

   990 "lookup @{theory} \"op &\""

   991 "SOME \"True\""}

   992 

   993   there are no references involved. This is one of the most fundamental

   994   coding conventions for programming in Isabelle. References would interfere

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

   996   

   898   @{ML_file "Pure/ML-Systems/universal.ML"}

   998   Isabelle contains implementations of several container data structures,

   999   including association lists in @{ML_file "Pure/General/alist.ML"},

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

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

   900 *}

  1003 

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

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

  1006 *}

  1007 

  1008 ML{*structure Data = ProofDataFun

  1009   (type T = term list

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

  1011 

  1012 text {*

  1013   The function we have to specify has to produce a list once a context 

  1014   is initialised (taking the theory into account from which the 

  1015   context is derived). We choose to just return the empty list. Next 

  1016   we define two auxiliary functions for updating the list with a given

  1017   term and printing the list. 

  1018 *}

  1019 

  1020 ML{*fun update trm = Data.map (fn xs => trm::xs)

  1021 

  1022 fun print ctxt =

  1023   case (Data.get ctxt) of

  1024     [] => tracing "Empty!"

  1025   | xs => tracing (string_of_terms ctxt xs)*}

  1026 

  1027 text {*

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

  1029   update it in various ways. 

  1030 

  1031   @{ML_response_fake [display,gray]

  1032 "let

  1033   val ctxt    = @{context}

  1034   val ctxt'   = ctxt   |> update @{term \"False\"}

  1035                        |> update @{term \"True \<and> True\"} 

  1036   val ctxt''  = ctxt   |> update @{term \"1::nat\"}

  1037   val ctxt''' = ctxt'' |> update @{term \"2::nat\"}

  1038 in

  1039   print ctxt; 

  1040   print ctxt';

  1041   print ctxt'';

  1042   print ctxt'''

  1043 end"

  1044 "Empty!

  1045 True \<and> True, False

  1046 1

  1047 2, 1"}

  1048 

  1049   Many functions in Isabelle manage and update data in a similar

  1050   fashion. Consequently, such calculation with contexts occur frequently in

  1051   Isabelle code, although the ``context flow'' is usually only linear.

  1052 

  1053   A special instance of the mechanisms described above are configuration

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

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

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

  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}

  1092 *}

  1093 

  1094