# HG changeset patch # User Christian Urban # Date 1394731009 0 # Node ID c53d74b34123779dcfb05f8071bdbf4b5a6b8c6e # Parent 82c482467d75dd529ec65367ad3be722233e2a97 updated to changes in Isabelle diff -r 82c482467d75 -r c53d74b34123 ProgTutorial/Essential.thy --- a/ProgTutorial/Essential.thy Sun Dec 15 23:49:05 2013 +0000 +++ b/ProgTutorial/Essential.thy Thu Mar 13 17:16:49 2014 +0000 @@ -609,9 +609,9 @@ term constructor is defined (@{text "List"}) and also in which datatype (@{text "list"}). Even worse, some constants have a name involving type-classes. Consider for example the constants for @{term "zero"} and - \mbox{@{text "(op *)"}}: - - @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"(op *)\"})" + \mbox{@{term "times"}}: + + @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"times\"})" "(Const (\"Groups.zero_class.zero\", \), Const (\"Groups.times_class.times\", \))"} @@ -2133,7 +2133,7 @@ *} setup %gray{* - Term_Style.setup "my_strip_allq" (Scan.succeed (K strip_allq)) + Term_Style.setup @{binding "my_strip_allq"} (Scan.succeed (K strip_allq)) *} text {* @@ -2185,7 +2185,7 @@ val parser = Scan.repeat Args.name fun action xs = K (rename_allq xs #> strip_allq) in - Term_Style.setup "my_strip_allq2" (parser >> action) + Term_Style.setup @{binding "my_strip_allq2"} (parser >> action) end *} text {* diff -r 82c482467d75 -r c53d74b34123 ProgTutorial/First_Steps.thy --- a/ProgTutorial/First_Steps.thy Sun Dec 15 23:49:05 2013 +0000 +++ b/ProgTutorial/First_Steps.thy Thu Mar 13 17:16:49 2014 +0000 @@ -862,7 +862,7 @@ ML %linenosgray{*val term_pat_setup = let - val parser = Args.context -- Scan.lift Args.name_source + val parser = Args.context -- Scan.lift Args.name_inner_syntax fun term_pat (ctxt, str) = str |> Proof_Context.read_term_pattern ctxt @@ -895,7 +895,7 @@ ML %grayML{*val type_pat_setup = let - val parser = Args.context -- Scan.lift Args.name_source + val parser = Args.context -- Scan.lift Args.name_inner_syntax fun typ_pat (ctxt, str) = let diff -r 82c482467d75 -r c53d74b34123 ProgTutorial/Helper/Command/Command.thy --- a/ProgTutorial/Helper/Command/Command.thy Sun Dec 15 23:49:05 2013 +0000 +++ b/ProgTutorial/Helper/Command/Command.thy Thu Mar 13 17:16:49 2014 +0000 @@ -7,7 +7,6 @@ ML {* let val do_nothing = Scan.succeed (Local_Theory.background_theory I) - val kind = Keyword.thy_decl in Outer_Syntax.local_theory @{command_spec "foobar"} "description of foobar" @@ -20,7 +19,6 @@ fun trace_prop str = Local_Theory.background_theory (fn lthy => (tracing str; lthy)) val trace_prop_parser = Parse.prop >> trace_prop - val kind = Keyword.thy_decl in Outer_Syntax.local_theory @{command_spec "foobar_trace"} "traces a proposition" @@ -37,7 +35,6 @@ Proof.theorem NONE (K I) [[(prop,[])]] lthy end; val prove_prop_parser = Parse.prop >> prove_prop - val kind = Keyword.thy_goal in Outer_Syntax.local_theory_to_proof @{command_spec "foobar_goal"} "proving a proposition" @@ -58,9 +55,9 @@ fun after_qed thm_name thms lthy = Local_Theory.note (thm_name, (flat thms)) lthy |> snd - fun setup_proof (thm_name, (txt, pos)) lthy = + fun setup_proof (thm_name, {text, ...}) lthy = let - val trm = Code_Runtime.value lthy result_cookie ("", txt) + val trm = Code_Runtime.value lthy result_cookie ("", text) in Proof.theorem NONE (after_qed thm_name) [[(trm,[])]] lthy end diff -r 82c482467d75 -r c53d74b34123 ProgTutorial/Intro.thy --- a/ProgTutorial/Intro.thy Sun Dec 15 23:49:05 2013 +0000 +++ b/ProgTutorial/Intro.thy Thu Mar 13 17:16:49 2014 +0000 @@ -296,7 +296,7 @@ \item {\bf Jeremy Dawson} wrote the first version of chapter \ref{chp:parsing} about parsing. - \item {\bf Florian Haftmann} helped with maintaining recipe \ref{rec:callml}. + %%\item {\bf Florian Haftmann} helped with maintaining recipe \ref{rec:callml}. \item {\bf Armin Heller} helped with recipe \ref{rec:sat}. @@ -306,7 +306,7 @@ \item {\bf Alexander Krauss} wrote a very early version of the ``first-steps'' chapter and also contributed the material on @{ML_funct Named_Thms}. - \item {\bf Tobias Nipkow} contributed recipe \ref{rec:callml}. + %%\item {\bf Tobias Nipkow} contributed recipe \ref{rec:callml}. \item {\bf Michael Norrish} proofread parts of the text. diff -r 82c482467d75 -r c53d74b34123 ProgTutorial/Package/Ind_Interface.thy --- a/ProgTutorial/Package/Ind_Interface.thy Sun Dec 15 23:49:05 2013 +0000 +++ b/ProgTutorial/Package/Ind_Interface.thy Thu Mar 13 17:16:49 2014 +0000 @@ -119,9 +119,9 @@ parse spec_parser input end" "(([(even, NONE, NoSyn), (odd, NONE, NoSyn)], - [((even0,\), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"), - ((evenS,\), \"\\^E\\^Ftoken\\^Eodd n \ even (Suc n)\\^E\\^F\\^E\"), - ((oddS,\), \"\\^E\\^Ftoken\\^Eeven n \ odd (Suc n)\\^E\\^F\\^E\")]), [])"} + [((even0,\), \), + ((evenS,\), \), + ((oddS,\), \)]), [])"} then we get back the specifications of the predicates (with type and syntax annotations), and specifications of the introduction rules. This is all the information we diff -r 82c482467d75 -r c53d74b34123 ProgTutorial/Parsing.thy --- a/ProgTutorial/Parsing.thy Sun Dec 15 23:49:05 2013 +0000 +++ b/ProgTutorial/Parsing.thy Thu Mar 13 17:16:49 2014 +0000 @@ -726,7 +726,7 @@ (* ML {* let - val parser = Args.context -- Scan.lift Args.name_source + val parser = Args.context -- Scan.lift Args.name_inner_syntax fun term_pat (ctxt, str) = str |> Syntax.read_prop ctxt @@ -752,23 +752,19 @@ for terms and types: you can just call the predefined parsers. Terms can be parsed using the function @{ML_ind term in Parse}. For example: -@{ML_response [display,gray] +@{ML_response_fake [display,gray] "let val input = Outer_Syntax.scan Position.none \"foo\" in Parse.term input end" -"(\"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\", [])"} +"(\"\", [])"} + The function @{ML_ind prop in Parse} is similar, except that it gives a different error message, when parsing fails. As you can see, the parser not just returns - the parsed string, but also some encoded information. You can decode the - information with the function @{ML_ind parse in YXML} in @{ML_struct YXML}. For example - - @{ML_response_fake [display,gray] - "YXML.parse \"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\"" - "Text \"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\""} - + the parsed string, but also some markup information. You can decode the + information with the function @{ML_ind parse in YXML} in @{ML_struct YXML}. The result of the decoding is an XML-tree. You can see better what is going on if you replace @{ML Position.none} by @{ML "Position.line 42"}, say: @@ -847,9 +843,9 @@ parse spec_parser input end" "(([(even, NONE, NoSyn), (odd, NONE, NoSyn)], - [((even0,\), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"), - ((evenS,\), \"\\^E\\^Ftoken\\^Eodd n \ even (Suc n)\\^E\\^F\\^E\"), - ((oddS,\), \"\\^E\\^Ftoken\\^Eeven n \ odd (Suc n)\\^E\\^F\\^E\")]), [])"} + [((even0,\),\), + ((evenS,\),\), + ((oddS,\),\)]), [])"} As you see, the result is a pair consisting of a list of variables with optional type-annotation and syntax-annotation, and a list of @@ -869,8 +865,8 @@ in parse Parse.fixes input end" -"([(foo, SOME \"\\^E\\^Ftoken\\^Eint \ bool\\^E\\^F\\^E\", NoSyn), - (bar, SOME \"\\^E\\^Ftoken\\^Enat\\^E\\^F\\^E\", Mixfix (\"BAR\", [], 100)), +"([(foo, SOME \, NoSyn), + (bar, SOME \, Mixfix (\"BAR\", [], 100)), (blonk, NONE, NoSyn)],[])"} *} @@ -897,8 +893,8 @@ val input = filtered_input \"foo_lemma[intro,dest!]:\" val ((name, attrib), _) = parse (Parse_Spec.thm_name \":\") input in - (name, map Args.dest_src attrib) -end" "(foo_lemma, [((\"intro\", []), \), ((\"dest\", [\]), \)])"} + (name, map Args.name_of_src attrib) +end" "(foo_lemma, [(\"intro\", \), (\"dest\", \)])"} The function @{ML_ind opt_thm_name in Parse_Spec} is the ``optional'' variant of @{ML_ind thm_name in Parse_Spec}. Theorem names can contain attributes. The name @@ -1133,9 +1129,9 @@ fun after_qed thm_name thms lthy = Local_Theory.note (thm_name, (flat thms)) lthy |> snd - fun setup_proof (thm_name, (txt, pos)) lthy = + fun setup_proof (thm_name, {text, ...}) lthy = let - val trm = Code_Runtime.value lthy result_cookie ("", txt) + val trm = Code_Runtime.value lthy result_cookie ("", text) in Proof.theorem NONE (after_qed thm_name) [[(trm, [])]] lthy end diff -r 82c482467d75 -r c53d74b34123 ProgTutorial/Recipes/Antiquotes.thy --- a/ProgTutorial/Recipes/Antiquotes.thy Sun Dec 15 23:49:05 2013 +0000 +++ b/ProgTutorial/Recipes/Antiquotes.thy Thu Mar 13 17:16:49 2014 +0000 @@ -35,7 +35,7 @@ The code is checked by sending the ML-expression @{text [quotes] "val _ = a_piece_of_code"} to the ML-compiler (i.e.~the function @{ML - "ML_Context.eval_text_in"} in Line 4 below). The complete code of the + "ML_Context.eval_source_in"} in Line 7 below). The complete code of the document antiquotation is as follows: *} @@ -43,8 +43,12 @@ ML%linenosgray{*fun ml_val code_txt = "val _ = " ^ code_txt fun output_ml {context = ctxt, ...} code_txt = - (ML_Context.eval_text_in (SOME ctxt) false Position.none (ml_val code_txt); +let + val srcpos = {delimited = false, text = (ml_val code_txt), pos = Position.none} +in + (ML_Context.eval_source_in (SOME ctxt) false srcpos; Thy_Output.output ctxt (map Pretty.str (space_explode "\n" code_txt))) +end val ml_checked_setup = Thy_Output.antiquotation @{binding "ML_checked"} (Scan.lift Args.name) output_ml*} @@ -76,8 +80,12 @@ *} ML%linenosgray{*fun output_ml {context = ctxt, ...} (code_txt, pos) = - (ML_Context.eval_text_in (SOME ctxt) false pos (ml_val code_txt); +let + val srcpos = {delimited = false, pos = pos, text = ml_val code_txt} +in + (ML_Context.eval_source_in (SOME ctxt) false srcpos; Thy_Output.output ctxt (map Pretty.str (space_explode "\n" code_txt))) +end val ml_checked_setup2 = Thy_Output.antiquotation @{binding "ML_checked2"} (Scan.lift (Parse.position Args.name)) output_ml *} @@ -132,7 +140,11 @@ *} ML %linenosgray{*fun output_ml_resp {context = ctxt, ...} ((code_txt, pat), pos) = - (ML_Context.eval_text_in (SOME ctxt) false pos (ml_pat (code_txt, pat)); + (let + val srcpos = {delimited = false, text = ml_pat (code_txt, pat), pos = pos} + in + ML_Context.eval_source_in (SOME ctxt) false srcpos + end; let val code_output = space_explode "\n" code_txt val resp_output = add_resp (space_explode "\n" pat) @@ -140,6 +152,7 @@ Thy_Output.output ctxt (map Pretty.str (code_output @ resp_output)) end) + val ml_resp_setup = Thy_Output.antiquotation @{binding "ML_resp"} (Scan.lift (Parse.position (Args.name -- Args.name))) output_ml_resp*} diff -r 82c482467d75 -r c53d74b34123 ProgTutorial/Recipes/CallML.thy --- a/ProgTutorial/Recipes/CallML.thy Sun Dec 15 23:49:05 2013 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,145 +0,0 @@ -(*<*) -theory CallML -imports "~~/src/HOL/Number_Theory/Primes" - "~~/src/HOL/Library/Code_Target_Numeral" -begin -(*>*) - -section {* Calling ML Functions from within HOL \label{rec:callml} *} - -text{* - {\bf Problem:} - How to call ML functions from within HOL?\smallskip - - {\bf Solution:} This can be achieved with \isacommand{code\_const} - and \isacommand{code\_reflect}.\smallskip - - - To make it clear we mean here calling unverified ML functions from within - HOL! The motivation is the paradigm of \emph{result checking}: rather than - verifying some complicated algorithm, have the algorithm produce an easily - checkable certificate. For example, instead of verifying an algorithm for - testing non-primality, have an algorithm that produces a factor as a witness to - non-primality. - - The algorithm is an ML function finding a factor of a number. We first - declare its type: -*} - -consts factor :: "nat \ nat" - -text{* - Its definition will be given below in ML. But the whole point is that - we can prove non-primality via @{const factor}, no matter what its - actual definition is: -*} - -lemma factor_non_prime: - "let k = factor n in k \ 1 \ k \ n \ k dvd n \ \ prime n" - by (auto simp: prime_nat_def Let_def) - -text{* - Note that the premise is executable once we have defined - @{const factor}. Here is a trivial definition in ML: -*} - -ML %grayML{*fun factor n = if n = 4 then 2 else 1*} - -text{* - Of course this trivial definition of @{const factor} could have been given - directly in HOL rather than ML. But by going to the ML level, all of ML is - at our disposal, including arrays and references, features that are less - easily emulated in HOL. In fact, we could even call some external software - from ML, e.g.\ a computer algebra system. - - It should be noted, however, that in this example you need to import the - theory @{theory Code_Target_Numeral} in order to force the HOL-type @{typ nat} to - be implemented by the ML-type @{text "int"}. - - \begin{graybox}\small - \isacommand{theory}~@{text CallML}\\ - \isacommand{imports}~@{text Main} @{text [quotes] "~~/src/HOL/Library/Code_Target_Numeral"}\\ - ... - \end{graybox} - - - Thus the ML implementation of - @{const factor} must be and is of type @{text "int -> int"}. Now it is time - to connect the two levels: -*} - -definition factor_integer :: "integer \ integer" -where - [code del]: "factor_integer = integer_of_nat \ factor \ nat_of_integer" - -lemma [code]: - "factor = nat_of_integer \ factor_integer \ integer_of_nat" - by (simp add: factor_integer_def fun_eq_iff) - -code_const factor_integer (SML "factor") -code_reserved SML factor - -text{* - The result of this declaration is that the HOL-function @{const factor} - is executable and command -*} - -value "factor 4" - -text{* - yields the expected result @{text 2}. Similarly we can prove that - @{text 4} is not prime: -*} - -lemma "\ prime (4::nat)" - apply(rule factor_non_prime) - apply eval - done - -text{* - Note, however, the command \isacommand{code\_const} cannot check that the ML function - has the required type. Therefore in the worst case a type mismatch will be detected by - the ML-compiler when we try to evaluate an expression involving @{const - factor}. It could also happen that @{const factor} is (accidentally) - redefined on the ML level later on. But remember that we do not assume - anything about @{const factor} on the HOL-level. Hence no definition of - @{const factor} can ever lead to an incorrect proof. Of course ``wrong'' - definitions can lead to compile time or run time exceptions, or to failed - proofs. - - The above example was easy because we forced Isabelle (via the inclusion of the - theory @{theory - Code_Target_Numeral}) to implement @{typ nat} by @{text int}, a predefined - ML-type. By default, Isabelle implements, for example, the HOL-type - @{text list} by the corresponding ML-type. Thus the following variation - on @{const factor} also works: -*} - -consts factor2 :: "nat \ nat list" (*<*)(*>*) -ML %grayML{*fun factor2 n = if n = 4 then [2] else []*}(*<*)(*>*) - -definition factor2_integer :: "integer \ integer list" -where - [code del]: "factor2_integer = map integer_of_nat \ factor2 \ nat_of_integer" - -lemma [code]: - "factor2 = map nat_of_integer \ factor2_integer \ integer_of_nat" - by (simp add: factor2_integer_def fun_eq_iff comp_def) - -code_const factor2_integer (SML "factor2") -code_reserved SML factor2 - -text{* - The first line declares the type of @{const factor2}; the second - gives its implementation in ML; the third makes it executable - in HOL, and the last is just a test. In this way, you can easily - interface with ML-functions whose types involve - @{text bool}, @{text int}, @{text list}, @{text option} and pairs, - only. If you have arbitrary tuples, for example, then you have to code - them as nested pairs. -*} - -value "factor2 4" - -end -(*>*) diff -r 82c482467d75 -r c53d74b34123 ProgTutorial/Recipes/Sat.thy --- a/ProgTutorial/Recipes/Sat.thy Sun Dec 15 23:49:05 2013 +0000 +++ b/ProgTutorial/Recipes/Sat.thy Thu Mar 13 17:16:49 2014 +0000 @@ -97,15 +97,15 @@ @{text [quotes] "dpll"}. There are also two tactics that make use of SAT solvers. One - is the tactic @{ML sat_tac in sat}. For example + is the tactic @{ML sat_tac in SAT}. For example *} lemma "True" -apply(tactic {* sat.sat_tac @{context} 1 *}) +apply(tactic {* SAT.sat_tac @{context} 1 *}) done text {* - However, for proving anything more exciting using @{ML "sat_tac" in sat} you + However, for proving anything more exciting using @{ML "sat_tac" in SAT} you have to use a SAT solver that can produce a proof. The internal one is not usuable for this. @@ -113,7 +113,7 @@ The interface for the external SAT solvers is implemented in @{ML_file "HOL/Tools/sat_solver.ML"}. This file contains also a simple SAT solver based on the DPLL algorithm. The tactics for SAT solvers are - implemented in @{ML_file "HOL/Tools/sat_funcs.ML"}. Functions concerning + implemented in @{ML_file "HOL/Tools/sat.ML"}. Functions concerning propositional formulas are implemented in @{ML_file "HOL/Tools/prop_logic.ML"}. The tables used in the translation function are implemented in @{ML_file "Pure/General/table.ML"}. diff -r 82c482467d75 -r c53d74b34123 ProgTutorial/antiquote_setup.ML --- a/ProgTutorial/antiquote_setup.ML Sun Dec 15 23:49:05 2013 +0000 +++ b/ProgTutorial/antiquote_setup.ML Thu Mar 13 17:16:49 2014 +0000 @@ -33,7 +33,8 @@ (* eval function *) fun eval_fn ctxt exp = - ML_Context.eval_text_in (SOME ctxt) false Position.none exp + ML_Context.eval_source_in (SOME ctxt) false + {delimited = false, text = exp, pos = Position.none} (* checks and prints a possibly open expressions, no index *) fun output_ml {context = ctxt, ...} (txt, (vs, stru)) = diff -r 82c482467d75 -r c53d74b34123 ROOT --- a/ROOT Sun Dec 15 23:49:05 2013 +0000 +++ b/ROOT Thu Mar 13 17:16:49 2014 +0000 @@ -23,7 +23,6 @@ "Recipes/Antiquotes" "Recipes/TimeLimit" "Recipes/Timing" - "Recipes/CallML" "Recipes/ExternalSolver" "Recipes/Oracle" "Recipes/Sat" @@ -56,7 +55,6 @@ "Recipes/Antiquotes" "Recipes/TimeLimit" "Recipes/Timing" - "Recipes/CallML" "Recipes/ExternalSolver" "Recipes/Oracle" "Recipes/Sat" diff -r 82c482467d75 -r c53d74b34123 progtutorial.pdf Binary file progtutorial.pdf has changed