[isabelle] counter example checking from ML



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

-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.