65 section {* Debugging and Printing *}

    65 section {* Debugging and Printing\label{sec:printing} *}

   121   Section~\ref{sec:printing} will give more information about printing 

   121   Most often you want to inspect data of type @{ML_type term}, @{ML_type cterm} 

   122   the main data structures of Isabelle, namely @{ML_type term}, @{ML_type cterm} 

   122   or @{ML_type thm}. Isabelle contains elaborate pretty-printing functions for printing them, 

   123   and @{ML_type thm}.

   123   but  for quick-and-dirty solutions they are far too unwieldy. A simple way to transform 

   124   a term into a string is to use the function @{ML Syntax.string_of_term}.

   125 

   126   @{ML_response_fake [display,gray]

   127   "Syntax.string_of_term @{context} @{term \"1::nat\"}"

   128   "\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""}

   129 

   130   This produces a string with some additional information encoded in it. The string

   131   can be properly printed by using the function @{ML warning}.

   132 

   133   @{ML_response_fake [display,gray]

   134   "warning (Syntax.string_of_term @{context} @{term \"1::nat\"})"

   135   "\"1\""}

   136 

   137   A @{ML_type cterm} can be transformed into a string by the following function.

   138 *}

   139 

   140 ML{*fun str_of_cterm ctxt t =  

   141    Syntax.string_of_term ctxt (term_of t)*}

   142 

   143 text {*

   144   If there are more than one @{ML_type cterm}s to be printed, you can use the 

   145   function @{ML commas} to separate them.

   146 *} 

   147 

   148 ML{*fun str_of_cterms ctxt ts =  

   149    commas (map (str_of_cterm ctxt) ts)*}

   150 

   151 text {*

   152   The easiest way to get the string of a theorem is to transform it

   153   into a @{ML_type cterm} using the function @{ML crep_thm}.

   154 *}

   155 

   156 ML{*fun str_of_thm ctxt thm =

   157   let

   158     val {prop, ...} = crep_thm thm

   159   in 

   160     str_of_cterm ctxt prop

   161   end*}

   162 

   163 text {* 

   164   Again the function @{ML commas} helps with printing more than one theorem. 

   165 *}

   166 

   167 ML{*fun str_of_thms ctxt thms =  

   168   commas (map (str_of_thm ctxt) thms)*}

   169 

   170 

   171 section {* Combinators\label{sec:combinators} *}

   172 

   173 text {*

   174   (FIXME: maybe move before antiquotation section)

   175 

   176   For beginners, perhaps the most puzzling parts in the existing code of Isabelle are

   177   the combinators. At first they seem to greatly obstruct the

   178   comprehension of the code, but after getting familiar with them, they

   179   actually ease the understanding and also the programming.

   180 

   181   \begin{readmore}

   182   The most frequently used combinator are defined in the files @{ML_file "Pure/library.ML"}

   183   and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans} 

   184   contains further information about combinators.

   185   \end{readmore}

   186 

   187   The simplest combinator is @{ML I}, which is just the identity function defined as

   188 *}

   189 

   190 ML{*fun I x = x*}

   191 

   192 text {* Another simple combinator is @{ML K}, defined as *}

   193 

   194 ML{*fun K x = fn _ => x*}

   195 

   196 text {*

   197   @{ML K} ``wraps'' a function around the argument @{text "x"}. However, this 

   198   function ignores its argument. As a result, @{ML K} defines a constant function 

   199   always returning @{text x}.

   200 

   201   The next combinator is reverse application, @{ML "|>"}, defined as: 

   202 *}

   203 

   204 ML{*fun x |> f = f x*}

   205 

   206 text {* While just syntactic sugar for the usual function application,

   207   the purpose of this combinator is to implement functions in a  

   208   ``waterfall fashion''. Consider for example the function *}

   209 

   210 ML %linenosgray{*fun inc_by_five x =

   211   x |> (fn x => x + 1)

   212     |> (fn x => (x, x))

   213     |> fst

   214     |> (fn x => x + 4)*}

   215 

   216 text {*

   217   which increments its argument @{text x} by 5. It does this by first incrementing 

   218   the argument by 1 (Line 2); then storing the result in a pair (Line 3); taking 

   219   the first component of the pair (Line 4) and finally incrementing the first 

   220   component by 4 (Line 5). This kind of cascading manipulations of values is quite

   221   common when dealing with theories (for example by adding a definition, followed by

   222   lemmas and so on). The reverse application allows you to read what happens in 

   223   a top-down manner. This kind of coding should also be familiar, 

   224   if you used Haskell's do-notation. Writing the function @{ML inc_by_five} using 

   225   the reverse application is much clearer than writing

   226 *}

   227 

   228 ML{*fun inc_by_five x = fst ((fn x => (x, x)) (x + 1)) + 4*}

   229 

   230 text {* or *}

   231 

   232 ML{*fun inc_by_five x = 

   233        ((fn x => x + 4) o fst o (fn x => (x, x)) o (fn x => x + 1)) x*}

   234 

   235 text {* and typographically more economical than *}

   236 

   237 ML{*fun inc_by_five x =

   238    let val y1 = x + 1

   239        val y2 = (y1, y1)

   240        val y3 = fst y2

   241        val y4 = y3 + 4

   242    in y4 end*}

   243 

   244 text {* 

   245   Another reason why the let-bindings in the code above are better to be

   246   avoided: it is more than easy to get the intermediate values wrong, not to 

   247   mention the nightmares the maintenance of this code causes!

   248 

   249 

   250   (FIXME: give a real world example involving theories)

   251 

   252   Similarly, the combinator @{ML "#>"} is the reverse function 

   253   composition. It can be used to define the following function

   254 *}

   255 

   256 ML{*val inc_by_six = 

   257       (fn x => x + 1)

   258    #> (fn x => x + 2)

   259    #> (fn x => x + 3)*}

   260 

   261 text {* 

   262   which is the function composed of first the increment-by-one function and then

   263   increment-by-two, followed by increment-by-three. Again, the reverse function 

   264   composition allows you to read the code top-down.

   265 

   266   The remaining combinators described in this section add convenience for the

   267   ``waterfall method'' of writing functions. The combinator @{ML tap} allows

   268   you to get hold of an intermediate result (to do some side-calculations for

   269   instance). The function

   270 

   271  *}

   272 

   273 ML %linenosgray{*fun inc_by_three x =

   274      x |> (fn x => x + 1)

   275        |> tap (fn x => tracing (makestring x))

   276        |> (fn x => x + 2)*}

   277 

   278 text {* 

   279   increments the argument first by @{text "1"} and then by @{text "2"}. In the

   280   middle (Line 3), however, it uses @{ML tap} for printing the ``plus-one''

   281   intermediate result inside the tracing buffer. The function @{ML tap} can

   282   only be used for side-calculations, because any value that is computed

   283   cannot be merged back into the ``main waterfall''. To do this, you can use

   284   the next combinator.

   285 

   286   The combinator @{ML "`"} is similar to @{ML tap}, but applies a function to the value

   287   and returns the result together with the value (as a pair). For example

   288   the function 

   289 *}

   290 

   291 ML{*fun inc_as_pair x =

   292      x |> `(fn x => x + 1)

   293        |> (fn (x, y) => (x, y + 1))*}

   294 

   295 text {*

   296   takes @{text x} as argument, and then increments @{text x}, but also keeps

   297   @{text x}. The intermediate result is therefore the pair @{ML "(x + 1, x)"

   298   for x}. After that, the function increments the right-hand component of the

   299   pair. So finally the result will be @{ML "(x + 1, x + 1)" for x}.

   300 

   301   The combinators @{ML "|>>"} and @{ML "||>"} are defined for 

   302   functions manipulating pairs. The first applies the function to

   303   the first component of the pair, defined as

   304 *}

   305 

   306 ML{*fun (x, y) |>> f = (f x, y)*}

   307 

   308 text {*

   309   and the second combinator to the second component, defined as

   310 *}

   311 

   312 ML{*fun (x, y) ||> f = (x, f y)*}

   313 

   314 text {*

   315   With the combinator @{ML "|->"} you can re-combine the elements from a pair.

   316   This combinator is defined as

   317 *}

   318 

   319 ML{*fun (x, y) |-> f = f x y*}

   320 

   321 text {* and can be used to write the following roundabout version 

   322   of the @{text double} function: 

   323 *}

   324 

   325 ML{*fun double x =

   326       x |>  (fn x => (x, x))

   327         |-> (fn x => fn y => x + y)*}

   328 

   329 text {*

   330   Recall that @{ML "|>"} is the reverse function applications. Recall also that the related 

   331   reverse function composition is @{ML "#>"}. In fact all the combinators @{ML "|->"},

   332   @{ML "|>>"} and @{ML "||>"} described above have related combinators for function

   333   composition, namely @{ML "#->"}, @{ML "#>>"} and @{ML "##>"}. Using @{ML "#->"}, 

   334   for example, the function @{text double} can also be written as:

   335 *}

   336 

   337 ML{*val double =

   338             (fn x => (x, x))

   339         #-> (fn x => fn y => x + y)*}

   340 

   341 text {*

   342   

   343   (FIXME: find a good exercise for combinators)

   344  

   215                  (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}

   436    (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}

   259   @{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})" "(Free (\"P\", \<dots>) $ Free (\"x\", \<dots>),

   480 @{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})" 

   260  Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"}

   481 "(Free (\"P\", \<dots>) $ Free (\"x\", \<dots>),

   482   Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"}

   448   "(Const (\"HOL.zero_class.zero\", \<dots>), 

   670  "(Const (\"HOL.zero_class.zero\", \<dots>), 

   474   the smallest name which is still unique, while @{ML base_name in Sign} always

   696   the smallest name that is still unique, whereas @{ML base_name in Sign} always

   570   val term = 

   792   val c = Const (@{const_name \"plus\"}, dummyT) 

   571    Const (@{const_name \"plus\"}, dummyT) $ @{term \"1::nat\"} $ Free (\"x\", dummyT)

   793   val o = @{term \"1::nat\"} 

   794   val v = Free (\"x\", dummyT)

   573   Syntax.check_term @{context} term

   796   Syntax.check_term @{context} (c $ o $ v)

   575   "Const (\"HOL.plus_class.plus\", \"nat \<Rightarrow> nat \<Rightarrow> nat\") $

   798 "Const (\"HOL.plus_class.plus\", \"nat \<Rightarrow> nat \<Rightarrow> nat\") $

   576        Const (\"HOL.one_class.one\", \"nat\") $ Free (\"x\", \"nat\")"}

   799   Const (\"HOL.one_class.one\", \"nat\") $ Free (\"x\", \"nat\")"}

   718 section {* Combinators\label{sec:combinators} *}

   908 

   719 

   909 (* FIXME: some code below *)

   720 text {*

   721   For beginners, perhaps the most puzzling parts in the existing code of Isabelle are

   722   the combinators. At first they seem to greatly obstruct the

   723   comprehension of the code, but after getting familiar with them, they

   724   actually ease the understanding and also the programming.

   725 

   726   \begin{readmore}

   727   The most frequently used combinator are defined in the files @{ML_file "Pure/library.ML"}

   728   and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans} 

   729   contains further information about combinators.

   730   \end{readmore}

   731 

   732   The simplest combinator is @{ML I}, which is just the identity function defined as

   733 *}

   734 

   735 ML{*fun I x = x*}

   736 

   737 text {* Another simple combinator is @{ML K}, defined as *}

   738 

   739 ML{*fun K x = fn _ => x*}

   740 

   741 text {*

   742   @{ML K} ``wraps'' a function around the argument @{text "x"}. However, this 

   743   function ignores its argument. As a result, @{ML K} defines a constant function 

   744   always returning @{text x}.

   745 

   746   The next combinator is reverse application, @{ML "|>"}, defined as: 

   747 *}

   748 

   749 ML{*fun x |> f = f x*}

   750 

   751 text {* While just syntactic sugar for the usual function application,

   752   the purpose of this combinator is to implement functions in a  

   753   ``waterfall fashion''. Consider for example the function *}

   754 

   755 ML %linenosgray{*fun inc_by_five x =

   756   x |> (fn x => x + 1)

   757     |> (fn x => (x, x))

   758     |> fst

   759     |> (fn x => x + 4)*}

   760 

   761 text {*

   762   which increments its argument @{text x} by 5. It does this by first incrementing 

   763   the argument by 1 (Line 2); then storing the result in a pair (Line 3); taking 

   764   the first component of the pair (Line 4) and finally incrementing the first 

   765   component by 4 (Line 5). This kind of cascading manipulations of values is quite

   766   common when dealing with theories (for example by adding a definition, followed by

   767   lemmas and so on). The reverse application allows you to read what happens in 

   768   a top-down manner. This kind of coding should also be familiar, 

   769   if you used Haskell's do-notation. Writing the function @{ML inc_by_five} using 

   770   the reverse application is much clearer than writing

   771 *}

   772 

   773 ML{*fun inc_by_five x = fst ((fn x => (x, x)) (x + 1)) + 4*}

   774 

   775 text {* or *}

   776 

   777 ML{*fun inc_by_five x = 

   778        ((fn x => x + 4) o fst o (fn x => (x, x)) o (fn x => x + 1)) x*}

   779 

   780 text {* and typographically more economical than *}

   781 

   782 ML{*fun inc_by_five x =

   783    let val y1 = x + 1

   784        val y2 = (y1, y1)

   785        val y3 = fst y2

   786        val y4 = y3 + 4

   787    in y4 end*}

   788 

   789 text {* 

   790   Another reason why the let-bindings in the code above are better to be

   791   avoided: it is more than easy to get the intermediate values wrong, not to 

   792   mention the nightmares the maintenance of this code causes!

   793 

   794 

   795   (FIXME: give a real world example involving theories)

   796 

   797   Similarly, the combinator @{ML "#>"} is the reverse function 

   798   composition. It can be used to define the following function

   799 *}

   800 

   801 ML{*val inc_by_six = 

   802       (fn x => x + 1)

   803    #> (fn x => x + 2)

   804    #> (fn x => x + 3)*}

   805 

   806 text {* 

   807   which is the function composed of first the increment-by-one function and then

   808   increment-by-two, followed by increment-by-three. Again, the reverse function 

   809   composition allows you to read the code top-down.

   810 

   811   The remaining combinators described in this section add convenience for the

   812   ``waterfall method'' of writing functions. The combinator @{ML tap} allows

   813   you to get hold of an intermediate result (to do some side-calculations for

   814   instance). The function

   815 

   816  *}

   817 

   818 ML %linenosgray{*fun inc_by_three x =

   819      x |> (fn x => x + 1)

   820        |> tap (fn x => tracing (makestring x))

   821        |> (fn x => x + 2)*}

   822 

   823 text {* 

   824   increments the argument first by @{text "1"} and then by @{text "2"}. In the

   825   middle (Line 3), however, it uses @{ML tap} for printing the ``plus-one''

   826   intermediate result inside the tracing buffer. The function @{ML tap} can

   827   only be used for side-calculations, because any value that is computed

   828   cannot be merged back into the ``main waterfall''. To do this, you can use

   829   the next combinator.

   830 

   831   The combinator @{ML "`"} is similar to @{ML tap}, but applies a function to the value

   832   and returns the result together with the value (as a pair). For example

   833   the function 

   834 *}

   835 

   836 ML{*fun inc_as_pair x =

   837      x |> `(fn x => x + 1)

   838        |> (fn (x, y) => (x, y + 1))*}

   839 

   840 text {*

   841   takes @{text x} as argument, and then increments @{text x}, but also keeps

   842   @{text x}. The intermediate result is therefore the pair @{ML "(x + 1, x)"

   843   for x}. After that, the function increments the right-hand component of the

   844   pair. So finally the result will be @{ML "(x + 1, x + 1)" for x}.

   845 

   846   The combinators @{ML "|>>"} and @{ML "||>"} are defined for 

   847   functions manipulating pairs. The first applies the function to

   848   the first component of the pair, defined as

   849 *}

   850 

   851 ML{*fun (x, y) |>> f = (f x, y)*}

   852 

   853 text {*

   854   and the second combinator to the second component, defined as

   855 *}

   856 

   857 ML{*fun (x, y) ||> f = (x, f y)*}

   858 

   859 text {*

   860   With the combinator @{ML "|->"} you can re-combine the elements from a pair.

   861   This combinator is defined as

   862 *}

   863 

   864 ML{*fun (x, y) |-> f = f x y*}

   865 

   866 text {* and can be used to write the following roundabout version 

   867   of the @{text double} function: 

   868 *}

   869 

   870 ML{*fun double x =

   871       x |>  (fn x => (x, x))

   872         |-> (fn x => fn y => x + y)*}

   873 

   874 text {*

   875   Recall that @{ML "|>"} is the reverse function applications. Recall also that the related 

   876   reverse function composition is @{ML "#>"}. In fact all the combinators @{ML "|->"},

   877   @{ML "|>>"} and @{ML "||>"} described above have related combinators for function

   878   composition, namely @{ML "#->"}, @{ML "#>>"} and @{ML "##>"}. Using @{ML "#->"}, 

   879   for example, the function @{text double} can also be written as:

   880 *}

   881 

   882 ML{*val double =

   883             (fn x => (x, x))

   884         #-> (fn x => fn y => x + y)*}

   885 

   886 text {*

   887   

   888   (FIXME: find a good exercise for combinators)

   889 *}

   890