# HG changeset patch # User Christian Urban # Date 1249300917 -7200 # Node ID 2728e8daebc05e50d58ee9600fd7c3337a7bc7a9 # Parent f286dfa9f173898622eec01dad6d5da2818b8c41 replaced "writeln" with "tracing" diff -r f286dfa9f173 -r 2728e8daebc0 ProgTutorial/Base.thy --- a/ProgTutorial/Base.thy Mon Aug 03 13:53:04 2009 +0200 +++ b/ProgTutorial/Base.thy Mon Aug 03 14:01:57 2009 +0200 @@ -7,6 +7,7 @@ begin (* to have a special tag for text enclosed in ML *) + ML {* fun propagate_env (context as Context.Proof lthy) = @@ -37,5 +38,4 @@ *} - end \ No newline at end of file diff -r f286dfa9f173 -r 2728e8daebc0 ProgTutorial/FirstSteps.thy --- a/ProgTutorial/FirstSteps.thy Mon Aug 03 13:53:04 2009 +0200 +++ b/ProgTutorial/FirstSteps.thy Mon Aug 03 14:01:57 2009 +0200 @@ -4,7 +4,6 @@ chapter {* First Steps *} - text {* Isabelle programming is done in ML. Just like lemmas and proofs, ML-code in Isabelle is part of a theory. If you want to follow the code given in @@ -230,7 +229,7 @@ @{text "?Q"} and so on. @{ML_response_fake [display, gray] - "writeln (string_of_thm @{context} @{thm conjI})" + "tracing (string_of_thm @{context} @{thm conjI})" "\?P; ?Q\ \ ?P \ ?Q"} In order to improve the readability of theorems we convert @@ -252,7 +251,7 @@ Theorem @{thm [source] conjI} is now printed as follows: @{ML_response_fake [display, gray] - "writeln (string_of_thm_no_vars @{context} @{thm conjI})" + "tracing (string_of_thm_no_vars @{context} @{thm conjI})" "\P; Q\ \ P \ Q"} Again the function @{ML commas} helps with printing more than one theorem. @@ -359,7 +358,7 @@ in apply_fresh_args t ctxt |> Syntax.string_of_term ctxt - |> writeln + |> tracing end" "P z za zb"} @@ -384,7 +383,7 @@ in apply_fresh_args t ctxt |> Syntax.string_of_term ctxt - |> writeln + |> tracing end" "za z zb"} @@ -743,9 +742,9 @@ val v2 = Var ((\"x1\", 3), @{typ bool}) val v3 = Free (\"x\", @{typ bool}) in - writeln (Syntax.string_of_term @{context} v1); - writeln (Syntax.string_of_term @{context} v2); - writeln (Syntax.string_of_term @{context} v3) + tracing (Syntax.string_of_term @{context} v1); + tracing (Syntax.string_of_term @{context} v2); + tracing (Syntax.string_of_term @{context} v3) end" "?x3 ?x1.3 @@ -776,7 +775,7 @@ "let val omega = Free (\"x\", @{typ nat}) $ Free (\"x\", @{typ nat}) in - writeln (Syntax.string_of_term @{context} omega) + tracing (Syntax.string_of_term @{context} omega) end" "x x"} @@ -980,7 +979,7 @@ "let val eq = HOLogic.mk_eq (@{term \"True\"}, @{term \"False\"}) in - writeln (Syntax.string_of_term @{context} eq) + tracing (Syntax.string_of_term @{context} eq) end" "True = False"} *} @@ -1908,7 +1907,7 @@ case realOut (!r) of NONE => "NONE" | SOME x => Real.toString x - val () = writeln (concat [s1, " ", s2, " ", s3, "\n"]) + val () = tracing (concat [s1, " ", s2, " ", s3, "\n"]) end*} ML_val{*structure t = Test(U) *} @@ -1985,7 +1984,7 @@ type: *} -ML{*fun pprint prt = writeln (Pretty.string_of prt)*} +ML{*fun pprint prt = tracing (Pretty.string_of prt)*} text {* The point of the pretty-printing infrastructure is to give hints about how to @@ -2008,7 +2007,7 @@ we obtain the ugly output: @{ML_response_fake [display,gray] -"writeln test_str" +"tracing test_str" "fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar foooooooooo ooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaa aaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fo @@ -2212,12 +2211,12 @@ text {* the infrastructure of Syntax-pretty-term makes sure it is printed nicely *} -ML {* Pretty.mark Markup.hilite (Pretty.str "foo") |> Pretty.string_of |> writeln *} -ML {* (Pretty.str "bar") |> Pretty.string_of |> writeln *} - - -ML {* Pretty.mark Markup.subgoal (Pretty.str "foo") |> Pretty.string_of |> writeln *} -ML {* (Pretty.str "bar") |> Pretty.string_of |> writeln *} +ML {* Pretty.mark Markup.hilite (Pretty.str "foo") |> Pretty.string_of |> tracing *} +ML {* (Pretty.str "bar") |> Pretty.string_of |> tracing *} + + +ML {* Pretty.mark Markup.subgoal (Pretty.str "foo") |> Pretty.string_of |> tracing *} +ML {* (Pretty.str "bar") |> Pretty.string_of |> tracing *} text {* Still to be done: @@ -2238,8 +2237,8 @@ *} -ML {* Pretty.mark Markup.hilite (Pretty.str "foo") |> Pretty.string_of |> writeln *} -ML {* (Pretty.str "bar") |> Pretty.string_of |> writeln *} +ML {* Pretty.mark Markup.hilite (Pretty.str "foo") |> Pretty.string_of |> tracing *} +ML {* (Pretty.str "bar") |> Pretty.string_of |> tracing *} text {* writing into the goal buffer *} @@ -2260,4 +2259,5 @@ section {* Name Space(TBD) *} + end diff -r f286dfa9f173 -r 2728e8daebc0 ProgTutorial/Package/Ind_Code.thy --- a/ProgTutorial/Package/Ind_Code.thy Mon Aug 03 13:53:04 2009 +0200 +++ b/ProgTutorial/Package/Ind_Code.thy Mon Aug 03 14:01:57 2009 +0200 @@ -50,7 +50,7 @@ val arg = ((@{binding "My_True"}, NoSyn), @{term True}) val (def, lthy') = make_defn arg lthy in - writeln (string_of_thm_no_vars lthy' def); lthy' + tracing (string_of_thm_no_vars lthy' def); lthy' end *} text {* @@ -117,7 +117,7 @@ let val def = defn_aux lthy eo_orules eo_preds (e_pred, e_arg_tys) in - writeln (Syntax.string_of_term lthy def); lthy + tracing (Syntax.string_of_term lthy def); lthy end *} text {* @@ -137,7 +137,7 @@ val def = defn_aux lthy fresh_orules [fresh_pred] (fresh_pred, fresh_arg_tys) in - writeln (Syntax.string_of_term lthy def); lthy + tracing (Syntax.string_of_term lthy def); lthy end *} @@ -187,7 +187,7 @@ val (defs, lthy') = defns eo_rules eo_preds eo_prednames eo_mxs eo_arg_tyss lthy in - writeln (string_of_thms_no_vars lthy' defs); lthy + tracing (string_of_thms_no_vars lthy' defs); lthy end *} text {* @@ -401,7 +401,7 @@ val intro = prove_ind lthy eo_defs srules cnewpreds ((e_pred, newpred), e_arg_tys) in - writeln (string_of_thm lthy intro); lthy + tracing (string_of_thm lthy intro); lthy end *} text {* @@ -460,7 +460,7 @@ let val ind_thms = inds eo_rules eo_defs eo_preds eo_arg_tyss lthy in - writeln (string_of_thms lthy ind_thms); lthy + tracing (string_of_thms lthy ind_thms); lthy end *} @@ -526,7 +526,7 @@ val ctrms = [@{cterm \"a::nat\"}, @{cterm \"b::nat\"}, @{cterm \"c::nat\"}] val new_thm = all_elims ctrms @{thm all_elims_test} in - writeln (string_of_thm_no_vars @{context} new_thm) + tracing (string_of_thm_no_vars @{context} new_thm) end" "P a b c"} @@ -542,7 +542,7 @@ "let val res = imp_elims @{thms imp_elims_test'} @{thm imp_elims_test} in - writeln (string_of_thm_no_vars @{context} res) + tracing (string_of_thm_no_vars @{context} res) end" "C"} diff -r f286dfa9f173 -r 2728e8daebc0 ProgTutorial/Tactical.thy --- a/ProgTutorial/Tactical.thy Mon Aug 03 13:53:04 2009 +0200 +++ b/ProgTutorial/Tactical.thy Mon Aug 03 14:01:57 2009 +0200 @@ -145,7 +145,7 @@ @{text "*** At command \"apply\"."} \end{isabelle} - This means they failed.\footnote{To be precise tactics do not produce this error + This means they failed.\footnote{To be precise, tactics do not produce this error message, it originates from the \isacommand{apply} wrapper.} The reason for this error message is that tactics are functions mapping a goal state to a (lazy) sequence of successor states. @@ -212,7 +212,7 @@ ML{*fun my_print_tac ctxt thm = let - val _ = writeln (string_of_thm_no_vars ctxt thm) + val _ = tracing (string_of_thm_no_vars ctxt thm) in Seq.single thm end*} @@ -528,9 +528,8 @@ safety is provided by the functions @{ML [index] FOCUS in Subgoal} and @{ML [index] SUBPROOF}. These tactics fix the parameters and bind the various components of a goal state to a record. - To see what happens, assume the function defined in Figure~\ref{fig:sptac}, which - takes a record and just prints out the content of this record (using the - string transformation functions from in Section~\ref{sec:printing}). Consider + To see what happens, use the function defined in Figure~\ref{fig:sptac}, which + takes a record and just prints out the contents of this record. Consider now the proof: *} @@ -549,11 +548,11 @@ val string_of_prems = string_of_thms_no_vars context prems val string_of_schms = string_of_cterms context (map fst (snd schematics)) - val _ = (writeln ("params: " ^ string_of_params); - writeln ("schematics: " ^ string_of_schms); - writeln ("assumptions: " ^ string_of_asms); - writeln ("conclusion: " ^ string_of_concl); - writeln ("premises: " ^ string_of_prems)) + val _ = (tracing ("params: " ^ string_of_params); + tracing ("schematics: " ^ string_of_schms); + tracing ("assumptions: " ^ string_of_asms); + tracing ("conclusion: " ^ string_of_concl); + tracing ("premises: " ^ string_of_prems)) in all_tac end*} @@ -577,19 +576,19 @@ \begin{quote}\small \begin{tabular}{ll} params: & @{term x}, @{term y}\\ - schematics: & @{term z}\\ + schematics: & @{text ?z}\\ assumptions: & @{term "A x y"}\\ conclusion: & @{term "B y x \ C (z y) x"}\\ premises: & @{term "A x y"} \end{tabular} \end{quote} - (FIXME: find out how nowadays the schmetics are handled) + (FIXME: Find out how nowadays the schematics are handled) - Notice in the actual output the brown colour of the variables @{term x} and - @{term y}. Although they are parameters in the original goal, they are fixed inside - the subproof. By convention these fixed variables are printed in brown colour. - Similarly the schematic variable @{term z}. The assumption, or premise, + Notice in the actual output the brown colour of the variables @{term x}, + and @{term y}. Although they are parameters in the original goal, they are fixed inside + the tactic. By convention these fixed variables are printed in brown colour. + Similarly the schematic variable @{text ?z}. The assumption, or premise, @{prop "A x y"} is bound as @{ML_type cterm} to the record-variable @{text asms}, but also as @{ML_type thm} to @{text prems}. @@ -605,7 +604,7 @@ \begin{quote}\small \begin{tabular}{ll} params: & @{term x}, @{term y}\\ - schematics: & @{term z}\\ + schematics: & @{text ?z}\\ assumptions: & @{term "A x y"}, @{term "B y x"}\\ conclusion: & @{term "C (z y) x"}\\ premises: & @{term "A x y"}, @{term "B y x"} @@ -617,15 +616,18 @@ text {* Now also @{term "B y x"} is an assumption bound to @{text asms} and @{text prems}. - The difference between @{ML SUBPROOF} and @{ML FOCUS in Subgoal} is that the former - expects that the goal is solved completely, which the latter does not. One - convenience of both @{ML FOCUS in Subgoal} and @{ML SUBPROOF} is that we can apply the - assumptions using the usual tactics, because the parameter @{text prems} - contains them as theorems. With this you can easily implement a tactic that - behaves almost like @{ML atac}: + The difference between the tactics @{ML SUBPROOF} and @{ML FOCUS in Subgoal} + is that the former expects that the goal is solved completely, which the + latter does not. @{ML SUBPROOF} can also not instantiate an schematic + variables. + + One convenience of both @{ML FOCUS in Subgoal} and @{ML SUBPROOF} is that we + can apply the assumptions using the usual tactics, because the parameter + @{text prems} contains them as theorems. With this you can easily implement + a tactic that behaves almost like @{ML atac}: *} -ML{*val atac' = SUBPROOF (fn {prems, ...} => resolve_tac prems 1)*} +ML{*val atac' = Subgoal.FOCUS (fn {prems, ...} => resolve_tac prems 1)*} text {* If you apply @{ML atac'} to the next lemma @@ -638,19 +640,14 @@ (*<*)oops(*>*) text {* - The restriction in this tactic which is not present in @{ML atac} is that it - cannot instantiate any schematic variables. This might be seen as a defect, - but it is actually an advantage in the situations for which @{ML SUBPROOF} - was designed: the reason is that, as mentioned before, instantiation of - schematic variables can affect several goals and can render them - unprovable. @{ML SUBPROOF} is meant to avoid this. + Notice that @{ML atac'} inside @{ML FOCUS in Subgoal} calls @{ML + resolve_tac} with the subgoal number @{text "1"} and also the outer call to + @{ML FOCUS in Subgoal} in the \isacommand{apply}-step uses @{text "1"}. This + is another advantage of @{ML FOCUS in Subgoal} and @{ML SUBPROOF}: the + addressing inside it is completely local to the tactic inside the + subproof. It is therefore possible to also apply @{ML atac'} to the second + goal by just writing: - Notice that @{ML atac'} inside @{ML SUBPROOF} calls @{ML resolve_tac} with - the subgoal number @{text "1"} and also the outer call to @{ML SUBPROOF} in - the \isacommand{apply}-step uses @{text "1"}. This is another advantage of - @{ML SUBPROOF}: the addressing inside it is completely local to the tactic - inside the subproof. It is therefore possible to also apply @{ML atac'} to - the second goal by just writing: *} lemma shows "True" and "\B x y; A x y; C x y\ \ A x y" @@ -666,7 +663,8 @@ \isccite{sec:results}. \end{readmore} - Similar but less powerful functions than @{ML FOCUS in Subgoal} are + Similar but less powerful functions than @{ML FOCUS in Subgoal}, respectively + @{ML SUBPROOF}, are @{ML [index] SUBGOAL} and @{ML [index] CSUBGOAL}. They allow you to inspect a given subgoal (the former presents the subgoal as a @{ML_type term}, while the latter as a @{ML_type @@ -1196,7 +1194,7 @@ ["Simproc patterns:"] @ map name_ctrm procs in s |> cat_lines - |> writeln + |> tracing end*} text_raw {* \end{isabelle} @@ -1523,7 +1521,7 @@ ML %linenosgray{*fun fail_simproc simpset redex = let val ctxt = Simplifier.the_context simpset - val _ = writeln ("The redex: " ^ (string_of_cterm ctxt redex)) + val _ = tracing ("The redex: " ^ (string_of_cterm ctxt redex)) in NONE end*} @@ -1594,7 +1592,7 @@ ML{*fun fail_simproc' simpset redex = let val ctxt = Simplifier.the_context simpset - val _ = writeln ("The redex: " ^ (Syntax.string_of_term ctxt redex)) + val _ = tracing ("The redex: " ^ (Syntax.string_of_term ctxt redex)) in NONE end*} diff -r f286dfa9f173 -r 2728e8daebc0 progtutorial.pdf Binary file progtutorial.pdf has changed