# HG changeset patch # User Christian Urban # Date 1404815650 -3600 # Node ID 77ea2de0ca62522eb83f306194ab5cf31a8885ae # Parent 3c214b215f7efa2f90f86ef879d82e9e425f4028 updated for Isabelle 2014 diff -r 3c214b215f7e -r 77ea2de0ca62 ProgTutorial/Base.thy --- a/ProgTutorial/Base.thy Wed May 28 12:41:09 2014 +0100 +++ b/ProgTutorial/Base.thy Tue Jul 08 11:34:10 2014 +0100 @@ -1,10 +1,6 @@ theory Base imports Main "~~/src/HOL/Library/LaTeXsugar" -(*keywords "ML" "setup" "local_setup" :: thy_decl and - "ML_prf" :: prf_decl and - "ML_val" :: diag -*) begin notation (latex output) diff -r 3c214b215f7e -r 77ea2de0ca62 ProgTutorial/Essential.thy --- a/ProgTutorial/Essential.thy Wed May 28 12:41:09 2014 +0100 +++ b/ProgTutorial/Essential.thy Tue Jul 08 11:34:10 2014 +0100 @@ -175,12 +175,13 @@ Hint: The third term is already quite big, and the pretty printer may omit parts of it by default. If you want to see all of it, you - can use the following ML-function to set the printing depth to a higher - value: - - @{ML [display,gray] "default_print_depth 50"} + need to set the printing depth to a higher value by \end{exercise} - +*} + +declare [[ML_print_depth = 50]] + +text {* The antiquotation @{text "@{prop \}"} constructs terms by inserting the usually invisible @{text "Trueprop"}-coercions whenever necessary. Consider for example the pairs diff -r 3c214b215f7e -r 77ea2de0ca62 ProgTutorial/First_Steps.thy --- a/ProgTutorial/First_Steps.thy Wed May 28 12:41:09 2014 +0100 +++ b/ProgTutorial/First_Steps.thy Tue Jul 08 11:34:10 2014 +0100 @@ -1,8 +1,7 @@ theory First_Steps imports Base begin - - + chapter {* First Steps\label{chp:firststeps} *} text {* @@ -98,7 +97,7 @@ @{ML_response_fake [display,gray] "writeln \"any string\"" "\"any string\""} - will print out @{text [quotes] "any string"} inside the response buffer. + will print out @{text [quotes] "any string"}. This function expects a string as argument. If you develop under PolyML, then there is a convenient, though again ``quick-and-dirty'', method for converting values into strings, namely the antiquotation @@ -114,11 +113,12 @@ @{ML_response_fake [display,gray] "if 0 = 1 then true else (error \"foo\")" -"Exception- ERROR \"foo\" raised -At command \"ML\"."} +"*** foo +***"} This function raises the exception @{text ERROR}, which will then - be displayed by the infrastructure. Note that this exception is meant + be displayed by the infrastructure indicating that it is an error by + painting the output red. Note that this exception is meant for ``user-level'' error messages seen by the ``end-user''. For messages where you want to indicate a genuine program error, then use the exception @{text Fail}. @@ -152,7 +152,7 @@ text {* You can also print out terms together with their typing information. - For this you need to set the configuration value + For this you need to set the configuration value @{ML_ind show_types in Syntax} to @{ML true}. *} @@ -543,7 +543,7 @@ can be implemented more concisely as *} -ML %grayML{*fun separate i [] = ([], []) +ML %grayML{*fun separate _ [] = ([], []) | separate i (x::xs) = if i <= x then separate i xs ||> cons x @@ -772,15 +772,17 @@ difference between a theory and a context is will be described in Chapter \ref{chp:advanced}.) A context is for example needed in order to use the function @{ML print_abbrevs in Proof_Context} that list of all currently - defined abbreviations. + defined abbreviations. For example @{ML_response_fake [display, gray] "Proof_Context.print_abbrevs @{context}" -"Code_Evaluation.valtermify \ \x. (x, \u. Code_Evaluation.termify x) +"\ INTER \ INFI Inter \ Inf \"} + The precise output of course depends on the abbreviations that are + currently defined; this can change over time. You can also use antiquotations to refer to proved theorems: @{text "@{thm \}"} for a single theorem @@ -812,14 +814,14 @@ and the second is a proof. For example *} -ML %grayML{*val foo_thm = @{lemma "True" and "False \ P" by simp_all} *} +ML %grayML{*val foo_thms = @{lemma "True" and "False \ P" by simp_all} *} text {* The result can be printed out as follows. @{ML_response_fake [gray,display] -"foo_thm |> pretty_thms_no_vars @{context} - |> pwriteln" +"foo_thms |> pretty_thms_no_vars @{context} + |> pwriteln" "True, False \ P"} You can also refer to the current simpset via an antiquotation. To illustrate @@ -915,10 +917,9 @@ setup %gray {* type_pat_setup *} -text {* - However, a word of warning is in order: Introducing new antiquotations - should be done only after careful deliberations. They can make your - code harder to read, than making it easier. +text {* +However, a word of warning is in order: Introducing new antiquotations should be done only after +careful deliberations. They can potentially make your code harder to read, than making it easier. \begin{readmore} The files @{ML_file "Pure/ML/ml_antiquotation.ML"} and @{ML_file "Pure/ML/ml_antiquotations.ML"} @@ -992,10 +993,10 @@ 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"} +"*** exception Match raised"} This runtime error is the reason why ML is still type-sound despite containing a universal type. @@ -1216,7 +1217,7 @@ for treating theories and proof contexts more uniformly. This type is defined as follows *} -ML_val{*datatype generic = +ML_val %grayML{*datatype generic = Theory of theory | Proof of proof*} diff -r 3c214b215f7e -r 77ea2de0ca62 ProgTutorial/Intro.thy --- a/ProgTutorial/Intro.thy Wed May 28 12:41:09 2014 +0100 +++ b/ProgTutorial/Intro.thy Tue Jul 08 11:34:10 2014 +0100 @@ -4,6 +4,7 @@ chapter {* Introduction *} + text {* \begin{flushright} {\em @@ -22,7 +23,9 @@ and implement new ideas. The source code of Isabelle can look intimidating, but beginners can get by with knowledge of only a handful of concepts, a small number of functions and a few basic coding conventions. - + There is also a considerable amount of code written in Scala that allows + Isabelle interface with the Jedit GUI. Explanation of this part is beyond + this tutorial. The best way to get to know the ML-level of Isabelle is by experimenting with the many code examples included in the tutorial. The code is as far as diff -r 3c214b215f7e -r 77ea2de0ca62 ProgTutorial/Recipes/TimeLimit.thy --- a/ProgTutorial/Recipes/TimeLimit.thy Wed May 28 12:41:09 2014 +0100 +++ b/ProgTutorial/Recipes/TimeLimit.thy Tue Jul 08 11:34:10 2014 +0100 @@ -22,7 +22,7 @@ Now the call - @{ML_response_fake [display,gray] "ackermann (4, 12)" "\"} + @{ML_response_fake_both [display,gray] "ackermann (4, 12)" "\"} takes a bit of time before it finishes. To avoid this, the call can be encapsulated in a time limit of five seconds. For this you have to write diff -r 3c214b215f7e -r 77ea2de0ca62 ProgTutorial/antiquote_setup.ML --- a/ProgTutorial/antiquote_setup.ML Wed May 28 12:41:09 2014 +0100 +++ b/ProgTutorial/antiquote_setup.ML Tue Jul 08 11:34:10 2014 +0100 @@ -31,6 +31,9 @@ fun ml_type txt = implode ["val _ = NONE : (", txt, ") option"]; +fun ml_out txt = + implode ["val _ = Pretty.writeln ((Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation ((", txt, "), ML_Options.get_print_depth ()))))) handle _ => writeln \"exception\""] + (* eval function *) fun eval_fn ctxt exp = ML_Context.eval_source_in (SOME ctxt) ML_Compiler.flags @@ -82,18 +85,18 @@ (* checks and expression agains a result pattern *) fun output_response {context = ctxt, ...} (lhs, pat) = (eval_fn ctxt (ml_pat (lhs, pat)); - (*write_file_ml_blk lhs (Proof_Context.theory_of ctxt);*) + eval_fn ctxt (ml_out lhs); output ctxt ((prefix_lines "" lhs) @ (prefix_lines "> " pat))) (* checks the expressions, but does not check it against a result pattern *) fun output_response_fake {context = ctxt, ...} (lhs, pat) = (eval_fn ctxt (ml_val [] NONE lhs); - (*write_file_ml_blk lhs (Proof_Context.theory_of ctxt);*) + eval_fn ctxt (ml_out lhs); output ctxt ((split_lines lhs) @ (prefix_lines "> " pat))) (* checks the expressions, but does not check it against a result pattern *) fun ouput_response_fake_both {context = ctxt, ...} (lhs, pat) = - output ctxt ((split_lines lhs) @ (prefix_lines "> " pat)) + (output ctxt ((split_lines lhs) @ (prefix_lines "> " pat))) val single_arg = Scan.lift (Args.name) val two_args = Scan.lift (Args.name -- Args.name) diff -r 3c214b215f7e -r 77ea2de0ca62 progtutorial.pdf Binary file progtutorial.pdf has changed