Email Gateway (Aug 18 2022 at 11:12): Email Gateway (Aug 18 2022 at 11:12):From: Michael Norrish <Michael.Norrish@nicta.com.au>
In the previous version of Isabelle, I used the function
read_cdef_terms, which has now disappeared. Is there an exact
re-implementation using the new Isabelle2007 facilities? (That would
make my life simplest, naturally.)
Failing that, I need to be able to parse a list of strings into terms,
with variables being assigned types consistently across that list, and
also being able to provide variant names and types for certains of the
strings corresponding to variable names.
My previous call to read_cdef_terms looked like
read_cdef_terms (thy, f state, K NONE) [] true stringlist
where f state was of type
(string * 'a) -> (string * typ) option
Thanks,
Michael.
Email Gateway (Aug 18 2022 at 11:12):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear Michael,
In the previous version of Isabelle, I used the function
read_cdef_terms, which has now disappeared. Is there an exact
re-implementation using the new Isabelle2007 facilities? (That would
make my life simplest, naturally.)
There are still some apparently similar functions, e. g.
Thm.read_def_cterms or Sign.read_def_terms which might serve as a subsitute.
Failing that, I need to be able to parse a list of strings into terms,
with variables being assigned types consistently across that list, and
also being able to provide variant names and types for certains of the
strings corresponding to variable names.My previous call to read_cdef_terms looked like
read_cdef_terms (thy, f state, K NONE) [] true stringlist
where f state was of type
(string * 'a) -> (string * typ) option
Indeed tinkering with raw variable names has been highly discouraged
since Isabelle2005 - proof contexts allow to track declared and fixed
variables and avoid name clashes implicitly. Chapter 4 of the emerging
Isabelle Implementation Manual gives some hints.
Anyway, an adaption to that style usually requires a re-working of the
whole code since everything has to be lifted from theories to local
theories. Perhaps the easiest quick-fix to your problem is to copy &
paste from Isabelle 2005 sources which are available from CVS, -r
Isabelle2005. Just mail me if this is not straight-forward.
Hope this helps
Florian
florian.haftmann.vcf
signature.asc
Email Gateway (Aug 18 2022 at 11:12):From: Michael Norrish <Michael.Norrish@nicta.com.au>
Florian Haftmann wrote:
In the previous version of Isabelle, I used the function
read_cdef_terms, which has now disappeared. Is there an exact
re-implementation using the new Isabelle2007 facilities? (That would
make my life simplest, naturally.)
There are still some apparently similar functions, e. g.
Thm.read_def_cterms or Sign.read_def_terms which might serve as a
subsitute.
I couldn't see the former; but I think the latter is just what I need.
Failing that, I need to be able to parse a list of strings into terms,
with variables being assigned types consistently across that list, and
also being able to provide variant names and types for certains of the
strings corresponding to variable names.
Indeed tinkering with raw variable names has been highly discouraged
since Isabelle2005 - proof contexts allow to track declared and
fixed variables and avoid name clashes implicitly. Chapter 4 of the
emerging Isabelle Implementation Manual gives some hints.
I was incorrect; I'm not modifying the names, just ascribing types to
free names. This sort of parsing in a context of known names is
critical to our application. It's not happening as part of a proof,
but rather at the top "definitional" level, so I'm not sure that there
is a proof context to hand. In any case, I think I'm happy with
Sign.read_def_terms.
Thanks,
Michael.
Email Gateway (Aug 18 2022 at 11:13):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
The former is in source file Pure/more_thm.ML which extends the Thm
structure.
Florian
florian.haftmann.vcf
signature.asc
Email Gateway (Aug 18 2022 at 11:18):From: Makarius <makarius@sketis.net>
The short answer is to use Syntax.read_terms with the proper context that
should have been passed to you in the particular situation (e.g. the proof
context of a method, or the local_theory context of a specification
element). Additional type information may be added to the context by
declaring previous terms properly, using Variable.declare_term.
The long answer is that with Isabelle2007 we have made some serious moves
towards a much simpler and more powerful way of processing input of formal
entities (types and terms). Instead of the traditional rather weakly
defined all-in-one operations of the read_def_cterm kind of thing we have
now separate layers for parsing and type-checking. In particular:
(1) Syntax.parse_term (or similar operations for sort, typ, prop)
turns a concrete string representation into a formal entity where all
names are properly internalised (name space lookups for consts,
potential internalization of ``brown'' variables, de-Bruijn
representation of bound variables etc.).
Here type information is still incomplete, more or less exactly as
given in the original input. This format could be called a pre-term,
but uses the existing datatype term with dummyT etc. as usual in
Isabelle.
Parsing works independently on individual terms; if you have a list of
strings just map Syntax.parse_term over them. This also facilitates
mixed situations, where some terms are already alvailable in internal
form, and further ones are parsed from user input.
(2) Syntax.check_terms (and friends) turn a list of pre-terms into fully
checked terms, by simulatenous type-inference, or any other term
checking facility installed in the present context. (The latter
concept is new, and part of what is occasionally called ``user-space
type system'' in internal Isabelle jargon.)
(3) Any additional information (type constraints etc.) is specified
implicitly via the provided context. Recall that
Variable.declare_term will add additional information from previously
checked terms.
In very rare situations, you can conjure up a context via
ProofContext.init applied to the global background theory, but usually
this holds too little information for proper parsing/checking. E.g.
it lacks the local declarations of a locale or class context, or even
just the syntactic constraints of a goal context.
When experimenting with any of this, the ML antiquotation @{context} will
give you the (compile-time) context; in production code you usually need a
runtime context passed from somewhere else. Here is an example to read a
term the fully explicit way within an Isar proof:
lemma
fixes m n :: nat
shows "m + n = n + m"
ML {* val pre_t = Syntax.parse_term @{context} "m + n" *}
ML {* val [t] = Syntax.check_terms @{context} [pre_t] *}
This results in
val pre_t =
Const ("HOL.plus_class.plus", "_") $ Free ("m", "_") $ Free ("n", "_")
val t =
Const ("HOL.plus_class.plus", "nat => nat => nat") $ Free ("m", "nat") $
Free ("n", "nat")
There are also some common compositions of parse/check operations, such as
Syntax.read_term for the above Syntax.parse_term followed by singleton
Syntax.check_terms.
Many internal Isabelle components have already been converted to the new
system, but some obsolete read operations still lure in the code. As a
rule of thumb, anything that just takes a theory instead of a proper
Proof.context will disappear soon, e.g. the obsolete Thm.read_def_cterm(s)
in src/Pure/more_thm.ML (the comments in the sources already say so).
Makarius
Last updated: May 03 2024 at 08:18 UTC