Email Gateway (Aug 18 2022 at 14:04): Email Gateway (Aug 18 2022 at 14:04):From: Lucas Dixon <ldixon@inf.ed.ac.uk>
Hello,
I have questions about using isabelle quickcheck/code generation.
I used to quite happily use it for various things but it seems that the
input is now stricter than it used to be (in 2008) - extra dependencies
between the input term and context - and I've not yet been able to
figure it out.
(Using Isabelle 32575:bf6c78d9f94c)
I'm trying to use
"Codegen.test_term : Proof.context -> term -> int -> term list option"
(is this the best ML function to be using? do tell me of a better higher
level one)
Trying to do what I used to do in ML...
ML{*
val _ = (Codegen.test_term
@{context}
@{term "(b :: int) + a = b"});
*}
;
Produces the error:
*** Error (line 19):
*** Value or constructor (b) has not been declared
*** Error (line 19):
*** Value or constructor (a) has not been declared
*** Error (line 19):
*** Value or constructor (b) has not been declared
*** Exception- ERROR of "Static Errors" raised
*** val ctxt2 = <context> : Context.proof
*** Exception- TOPLEVEL_ERROR raised
*** At command "ML" (line 11 of
"/afs/inf.ed.ac.uk/user/l/ldixon/Scratch.thy").
My first guess was that all terms are now implicitly dependent on the
context they live in, so perhaps I need to add the free variables to the
context, - the types should already be there. The quick undisciplined
way, I think, is:
ML{*
val (_,ctxt2) = @{context} |> Variable.add_fixes ["b", "a"];
val _ = (Codegen.test_term ctxt2 @{term "(b :: int) + a = b"});
*}
;
I can do some term manipulation and properly pull out the names of the
frees from the term - but I would expect the above to work... but it
also gives the same error.
This gives rise to further questions:
how to I inspect the context? (I remember this from the Isabelle dev
workshop, but couldn't find it in the online example theories)
what's the right way to quickly make the context that would get from a
statement like "lemma ..."? i.e. the context of a term, automatically
putting in the types and frees? (my first guess was to use
Variable.focus - but that seems to ignore free vars and types)
how can I use quickcheck (or nitpick) from the ML level? and I would
love this to be in the Isabelle cookbook (shall I write an entry, once I
find out how to use it?)
What is the hidden implicit dependency between the term given to
Codegen.text_term, and the context?
thanks,
lucas
Email Gateway (Aug 18 2022 at 14:04):From: Makarius <makarius@sketis.net>
On Wed, 16 Sep 2009, Lucas Dixon wrote:
This gives rise to further questions:
- how to I inspect the context? (I remember this from the Isabelle dev
workshop, but couldn't find it in the online example theories)
The context merely maintains arbitrary data of certain modules. You can
only print certain aspects of whatever might be there, using operations
that the corresponding modules offer. E.g. you can print the important
data provided by Variable/Assumption using print facitlities of
ProofContext, say like this:
ML_command "set ProofContext.debug"
potentially also this:
ML_command "set ProofContext.verbose"
Then the ML pretty printer for type Proof.context (in stable Poly/ML
5.2.1) should show you fixes/assumes and some more. E.g.
ML_val {* @{context} *}
- what's the right way to quickly make the context that would get from a
statement like "lemma ..."? i.e. the context of a term, automatically
putting in the types and frees?
For testing it is most convenient to have Isar do it for you, e.g. like
this:
lemma fixes x y :: nat assumes "x = y" shows "y = x"
ML_prf {* val my_ctxt = @{context} *}
my first guess was to use Variable.focus - but that seems to ignore free
vars and types
Focus is very special, to look under !! binders of rules and goals. To
get the outermost entities (free variables) into the context, you merely
need Variable.declare_term, or the slightly stronger version
Variable.auto_fixes.
Explicit Variable.add_fixes is also quite common, although the type
constraints need to be introduced separately, either via
Variable.declare_term or the weaker version Variable.declare_constraints.
Chapter 4 of the "implementation" manual provides some further clues how
things work, and which are the main operations.
Makarius
Email Gateway (Aug 18 2022 at 14:04):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Lucas,
note that the convention on the Codegen.test_term interface has changed:
ML {* Codegen.test_term @{context} @{term "%n. n = Suc n"} 2 *}
The proposition is now given as an abstraction containing no free
variables.
Hope this helps
Florian
Lucas Dixon schrieb:
Email Gateway (Aug 18 2022 at 14:04):From: Lucas Dixon <ldixon@inf.ed.ac.uk>
Lucas Dixon wrote:
Thanks to Omar for pointing this out to me, there is a high level
interface for Quickcheck in src/Tools/quickcheck.ML, it has signature:
signature QUICKCHECK =
sig
val auto: bool ref
val auto_time_limit: int ref
val test_term: Proof.context -> bool -> string option -> int -> int
-> term ->
(string * term) list option
val add_generator: string * (Proof.context -> term -> int -> term
list option) -> theory -> theory
val quickcheck: (string * string) list -> int -> Proof.state ->
(string * term) list option
end;
So this does much of what I'm after.
However, I'd like to also have access to:
fun test_goal quiet generator_name size iterations default_T insts i
assms state = ...
which seems to be a useful function - I think I'd otherwise need to
copy/rewrite chunks of it. Can this be added to the signature?
cheers,
lucas
Last updated: Apr 26 2024 at 08:19 UTC