# HG changeset patch # User Christian Urban <christian dot urban at kcl dot ac dot uk> # Date 1375281868 -3600 # Node ID 95d6853dec4a5ea9d0a8d4e2379ab8bd8dedcce1 # Parent 4d7543f4847634e023aeb2f06ea123ea20381dd6 deleted comment about Theory.copy which is not used anymore in Isabelle diff -r 4d7543f48476 -r 95d6853dec4a ProgTutorial/Advanced.thy --- a/ProgTutorial/Advanced.thy Fri Jul 26 16:30:33 2013 +0200 +++ b/ProgTutorial/Advanced.thy Wed Jul 31 15:44:28 2013 +0100 @@ -148,49 +148,6 @@ the modified one @{text thy'}. Such buggy code will always result into a runtime error message about stale theories. - However, sometimes it does make sense to work with two theories at the same - time, especially in the context of parsing and typing. In the code below we - use in Line 3 the function @{ML_ind copy in Theory} from the structure - @{ML_struct Theory} for obtaining a new theory that contains the same - data, but is unrelated to the existing theory. -*} - -setup %graylinenos {* fn thy => -let - val tmp_thy = Theory.copy thy - val foo_const = ((@{binding "FOO"}, @{typ "nat \<Rightarrow> nat"}), NoSyn) - val (_, tmp_thy') = Sign.declare_const @{context} foo_const tmp_thy - val trm1 = Syntax.read_term_global tmp_thy' "FOO baz" - val trm2 = Syntax.read_term_global thy "FOO baz" - val _ = pwriteln - (Pretty.str (@{make_string} trm1 ^ "\n" ^ @{make_string} trm2)) -in - thy -end *} - -text {* - That means we can make changes to the theory @{text tmp_thy} without - affecting the current theory @{text thy}. In this case we declare in @{text - "tmp_thy"} the constant @{text FOO} (Lines 4 and 5). The point of this code - is that we next, in Lines 6 and 7, parse a string to become a term (both - times the string is @{text [quotes] "FOO baz"}). But since we parse the string - once in the context of the theory @{text tmp_thy'} in which @{text FOO} is - declared to be a constant of type @{typ "nat \<Rightarrow>nat"} and once in the context - of @{text thy} where it is not, we obtain two different terms, namely - - \begin{isabelle} - \begin{graybox} - @{text "> Const (\"Advanced.FOO\", \"nat \<Rightarrow> nat\") $ Free (\"baz\", \"nat\")"}\isanewline - @{text "> Free (\"FOO\", \"'a \<Rightarrow> 'b\") $ Free (\"baz\", \"'a\")"} - \end{graybox} - \end{isabelle} - - There are two reasons for parsing a term in a temporary theory. One is to - obtain fully qualified names for constants and the other is appropriate type - inference. This is relevant in situations where definitions are made later, - but parsing and type inference has to take already proceed as if the definitions - were already made. - \begin{readmore} Most of the functions about theories are implemented in @{ML_file "Pure/theory.ML"} and @{ML_file "Pure/global_theory.ML"}. diff -r 4d7543f48476 -r 95d6853dec4a progtutorial.pdf Binary file progtutorial.pdf has changed