Email Gateway (Aug 17 2022 at 13:46): Email Gateway (Aug 17 2022 at 13:46):From: Michael Norrish <Michael.Norrish@nicta.com.au>
I have a definitional term, of the form
Const ("==", ty) $ Free(name, ty') $ tm
such that it certifies with respect to a given theory, thy.
Thus,
cterm_of thy eqt;
val it =
"foo_body ==
TRY \<acute>j :== the (h_val \<acute>the_heap \<acute>i) CATCH SKIP END"
: Thm.cterm
But, if I try to use this as the basis for a definition, I get an
error from the constant certification part of the code:
thy |> Constdefs.add_constdefs_i ([], [(NONE, (("", []), eqt))]);
Exception-
TYPE
("Illegal type for constant \"mytest.globals.the_heap\" :: globals => addr => word8",
[],
[]) raised
What am I likely to be doing wrong in my invocation of
add_constdefs_i?
Thanks,
Michael.
Email Gateway (Aug 17 2022 at 13:46):From: Makarius <makarius@sketis.net>
This is hard to guess from a distance.
Generally speaking, add_constdefs_i is just the internal version of a
user-level command -- it is common practice to provide both external and
internal version just to make sure that ML packages can always invoke each
other. For basic definitions the primitive add_consts/add_defs are
usually easier to use in ML. Even more, constdefs is about to become a
legacy feature pretty soon, being superceded by a more general
'definition' element.
Anyway, add_constdefs_i actually does work for me as follows:
val eq = Logic.mk_equals (Free ("x", HOLogic.boolT), Const ("True", HOLogic.boolT));
val thy =
Theory.begin_theory "Test" [Main.thy]
|> Constdefs.add_constdefs_i ([], [(NONE, (("", []), eq))]);
print_theory thy;
Note that Constdefs.add_constdefs_i produces extra noise on the message
channel -- this is a toplevel command after all.
Makarius
Email Gateway (Aug 17 2022 at 13:46):From: Michael Norrish <Michael.Norrish@nicta.com.au>
Makarius writes:
On Tue, 28 Feb 2006, Michael Norrish wrote:
What am I likely to be doing wrong in my invocation of add_constdefs_i?
This is hard to guess from a distance.
Trying to step through the code, inasmuch as this is possible without
hitting hidden functions, I get to the point where
ProofContext.cert_term (ProofContext.init thy) tm
fails, but
cterm_of thy tm
succeeds.
Having looked at the code, I'm now pretty sure the reason for this is
that
Sign.certify_term
calls certify_typ on the types of its argument (using map_term_types),
but
ProofContext.cert_term
does not. It would be nice if the two behaved a little more
consistently, but I can now deal with the issue. In particular, if
you pass Consts.certify a term that doesn't have its type
abbreviations expanded, then it will complain. The action of
certifying a type does this expansion (among other things, I'm sure).
Generally speaking, add_constdefs_i is just the internal version of
a user-level command -- it is common practice to provide both
external and internal version just to make sure that ML packages can
always invoke each other. For basic definitions the primitive
add_consts/add_defs are usually easier to use in ML. Even more,
constdefs is about to become a legacy feature pretty soon, being
superceded by a more general 'definition' element.
When implemented, please document the ML API for this new entry-point!
Note that Constdefs.add_constdefs_i produces extra noise on the message
channel -- this is a toplevel command after all.
Yes, this is what I want because I'm implementing a top-level command
myself.
Michael.
Last updated: May 03 2024 at 04:19 UTC