diff -r ed797395fab6 -r 007922777ff1 ProgTutorial/FirstSteps.thy --- a/ProgTutorial/FirstSteps.thy Sun Aug 16 22:14:36 2009 +0200 +++ b/ProgTutorial/FirstSteps.thy Mon Aug 17 20:57:32 2009 +0200 @@ -1,7 +1,10 @@ theory FirstSteps imports Base +uses "FirstSteps.ML" begin + + chapter {* First Steps *} text {* @@ -165,7 +168,7 @@ will cause that all tracing information is printed into the file @{text "foo.bar"}. You can print out error messages with the function @{ML [index] error}; for - example:\footnote{FIXME: unwanted pagebreak} + example: @{ML_response_fake [display,gray] "if 0=1 then true else (error \"foo\")" "Exception- ERROR \"foo\" raised @@ -194,46 +197,60 @@ *) text {* - Most often you want to inspect data of Isabelle's most basic datastructures, - namely @{ML_type term}, @{ML_type cterm} or @{ML_type thm}. Isabelle - contains elaborate pretty-printing functions for printing them (see Section - \ref{sec:pretty}), but for quick-and-dirty solutions they are far too - unwieldy. One way to transform a term into a string is to use the function - @{ML [index] string_of_term in Syntax}. - + Most often you want to inspect data of Isabelle's most basic data + structures, namely @{ML_type term}, @{ML_type cterm} or @{ML_type + thm}. Isabelle contains elaborate pretty-printing functions for printing + them (see Section \ref{sec:pretty}), but for quick-and-dirty solutions they + are a bit unwieldy. One way to transform a term into a string is to use the + function @{ML [index] string_of_term in Syntax} in structure @{ML_struct + Syntax}, which we bind for more convenience to the toplevel. +*} + +ML{*val string_of_term = Syntax.string_of_term*} + +text {* + It can now be used as follows @{ML_response_fake [display,gray] - "Syntax.string_of_term @{context} @{term \"1::nat\"}" + "string_of_term @{context} @{term \"1::nat\"}" "\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""} - This produces a string with some additional information encoded in it. The string - can be properly printed by using either the function @{ML [index] writeln} or - @{ML [index] tracing}: + This produces a string corrsponding to the term @{term [show_types] "1::nat"} with some + additional information encoded in it. The string can be properly printed by + using either the function @{ML [index] writeln} or @{ML [index] tracing}: @{ML_response_fake [display,gray] - "writeln (Syntax.string_of_term @{context} @{term \"1::nat\"})" + "writeln (string_of_term @{context} @{term \"1::nat\"})" "\"1\""} or @{ML_response_fake [display,gray] - "tracing (Syntax.string_of_term @{context} @{term \"1::nat\"})" + "tracing (string_of_term @{context} @{term \"1::nat\"})" "\"1\""} + If there are more than one @{ML_type term}s to be printed, you can use the + function @{ML [index] commas} to separate them. +*} + +ML{*fun string_of_terms ctxt ts = + commas (map (string_of_term ctxt) ts)*} + +text {* A @{ML_type cterm} can be transformed into a string by the following function. *} ML{*fun string_of_cterm ctxt t = - Syntax.string_of_term ctxt (term_of t)*} + string_of_term ctxt (term_of t)*} text {* In this example the function @{ML [index] term_of} extracts the @{ML_type term} from - a @{ML_type cterm}. If there are more than one @{ML_type cterm}s to be - printed, you can use the function @{ML [index] commas} to separate them. + a @{ML_type cterm}. More than one @{ML_type cterm}s can again be printed + with @{ML [index] commas}. *} -ML{*fun string_of_cterms ctxt ts = - commas (map (string_of_cterm ctxt) ts)*} +ML{*fun string_of_cterms ctxt cts = + commas (map (string_of_cterm ctxt) cts)*} text {* The easiest way to get the string of a theorem is to transform it @@ -251,10 +268,10 @@ "tracing (string_of_thm @{context} @{thm conjI})" "\?P; ?Q\ \ ?P \ ?Q"} - In order to improve the readability of theorems we convert - these schematic variables into free variables using the - function @{ML [index] import in Variable}. This is similar - to the attribute @{text "[no_vars]"} from Isabelle's user-level. + In order to improve the readability of theorems we convert these schematic + variables into free variables using the function @{ML [index] import in + Variable}. This is similar to the theorem attribute @{text "[no_vars]"} from + Isabelle's user-level. *} ML{*fun no_vars ctxt thm = @@ -409,7 +426,7 @@ val ctxt = @{context} in apply_fresh_args t ctxt - |> Syntax.string_of_term ctxt + |> string_of_term ctxt |> tracing end" "P z za zb"} @@ -434,7 +451,7 @@ val ctxt = @{context} in apply_fresh_args t ctxt - |> Syntax.string_of_term ctxt + |> string_of_term ctxt |> tracing end" "za z zb"} @@ -599,20 +616,59 @@ (fn x => (x, x)) #-> (fn x => fn y => x + y)*} + +text {* + When using combinators for writing function in waterfall fashion, it is + sometimes necessary to do some ``plumbing'' for fitting functions + together. We have already seen such plumbing in the function @{ML + apply_fresh_args}, where @{ML curry} is needed for making the function @{ML + list_comb} that works over pairs to fit with the combinator @{ML "|>"}. Such + plumbing is also needed in situations where a functions operate over lists, + but one calculates only with a single entity. An example is the function + @{ML [index] check_terms in Syntax}, whose purpose is to type-check a list + of terms. + + @{ML_response_fake [display, gray] + "let + val ctxt = @{context} +in + map (Syntax.parse_term ctxt) [\"m + n\", \"m - (n::nat)\"] + |> Syntax.check_terms ctxt + |> string_of_terms ctxt + |> tracing +end" + "m + n, m - n"} +*} + text {* - - (FIXME: find a good exercise for combinators) - + In this example we obtain two terms with appropriate typing. However, if you + have only a single term, then @{ML check_terms in Syntax} needs to be + adapted. This can be done with the ``plumbing'' function @{ML + singleton}.\footnote{There is in fact alread a function @{ML check_term in Syntax}, + which however is defined in terms of @{ML singleton} and @{ML check_terms in + Syntax}.} For example + + @{ML_response_fake [display, gray] + "let + val ctxt = @{context} +in + Syntax.parse_term ctxt \"m - (n::nat)\" + |> singleton (Syntax.check_terms ctxt) + |> string_of_term ctxt + |> tracing +end" + "m - n"} + \begin{readmore} The most frequently used combinators are defined in the files @{ML_file "Pure/library.ML"} and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans} contains further information about combinators. \end{readmore} - - (FIXME: say something about calling conventions) - - (FIXME: say something about singleton) + + (FIXME: find a good exercise for combinators) + + (FIXME: say something about calling conventions) *} @@ -831,13 +887,10 @@ val v2 = Var ((\"x1\", 3), @{typ bool}) val v3 = Free (\"x\", @{typ bool}) in - map (Syntax.string_of_term @{context}) [v1, v2, v3] - |> cat_lines + string_of_terms @{context} [v1, v2, v3] |> tracing end" -"?x3 -?x1.3 -x"} +"?x3, ?x1.3, x"} When constructing terms, you are usually concerned with free variables (as mentioned earlier, you cannot construct schematic variables using the antiquotation @{text "@{term \}"}). @@ -864,7 +917,7 @@ "let val omega = Free (\"x\", @{typ nat}) $ Free (\"x\", @{typ nat}) in - tracing (Syntax.string_of_term @{context} omega) + tracing (string_of_term @{context} omega) end" "x x"} @@ -1085,7 +1138,7 @@ val (vrs, trm) = strip_alls @{term \"\x y. x = (y::bool)\"} in subst_bounds (rev vrs, trm) - |> Syntax.string_of_term @{context} + |> string_of_term @{context} |> tracing end" "x = y"} @@ -1104,7 +1157,7 @@ "let val eq = HOLogic.mk_eq (@{term \"True\"}, @{term \"False\"}) in - tracing (Syntax.string_of_term @{context} eq) + tracing (string_of_term @{context} eq) end" "True = False"} *} @@ -1516,7 +1569,7 @@ then let val (params,t) = strip_assums_all([], nth prems (i - 1)) in subst_bounds(map Free params, t) end else error ("Not enough premises for prem" ^ string_of_int i ^ - " in propositon: " ^ Syntax.string_of_term ctxt t) + " in propositon: " ^ string_of_term ctxt t) end; *}