Re: [isabelle] antiquotations



Dear Jeremy,

In addition to the references, let me try to comment more specifically
on some of your problems / complaints:

My complaint is that the _same_ ML expression bool_axioms RL
[fun_cong] behaves differently between (a) where I put it in the
theory file, where it doesn't work, and (b) when I use it later, in
trying to debug the problem.

If your radio doesn't work in the cellar, but does work in the living
room, then you cannot debug the problem in the living room. You have to
go to the cellar.

I want the same expression to have the same meaning when I am trying
to debug it as the meaning it has when it fails to work!

You should debug it in the same context: Open the offending theory in
PG, step to the point until it breaks, and debug it there. Then you
should be able to see what the problem is.

If I understand correctly the_context () returns the current theory
as at the point where it is executed.  Is that correct?
[...]
So far as I understood the previous emails, ML {* XXX the_context  ()
*} and ML {* XXX at {theory} *} would only return a different result if
the code represented by XXX actually changed the current theory.  Is
that correct?

No. Strictly speaking, the behaviour of the_context () is completely
unspecified: Since theories can be loaded in parallel, you could get
almost anything, including a theory that is currently developing in a
different thread. The "current context" is not defined in terms of the
point in time when something is executed. It must be given statically,
by the location in the theory source. The @{theory} antiquotation does that.

Let me repeat: If you use "the_context ()" in production code, it will
break with obscure errors sooner or later.

A further question from a previous email (the answer given then was
to use a different function) : bind_thm(s) seems to sometimes work
(in the sense of storing a theorem in the database so that it can be
effectively retrieved later).  Why is this?  What is the difference
between bind_thm and the function I was told to use (ie,
PureThy.add_thmss)?

You can read the answer from its type:

bind_thms         : string * Thm.thm list -> unit
PureThy.add_thmss : ((bstring * Thm.thm list) * Thm.attribute list) list
                -> Context.theory -> Thm.thm list list * Context.theory

Since bind_thms is impure, it can only update some global reference
hanging around. This is incompatible with paralellism. At the moment it
may work sometimes, but it is guaranteed to break sooner or later.

These changes are necessary, since the ability to process theories in
paralell decides whether you can use the 15 extra cores in your next CPU :-)

You can usually tell these "dont-use" functions from the type: If you
feel they should depend on or change the theory or context, and this is
not explicit in the type, then this is calling for trouble.

Since my comments above are a little non-constructive ("don't do this"),
I had another look at the theory you sent recently. You just need to
change a few things to avoid all the trouble.

1. Instead of the (evil, imperative) bind_thms, use a proper
declaration. On the theory level, the "setup" command will do what you
need. It takes an ML snippet of type "theory -> theory". In your example:

setup {*
  let
    val boolexp = @{thm "boolexp"} ;

    val bool_axioms = Seq.list_of (EVERY'
      [REPEAT o dresolve_tac [conjunct1, conjunct2], REPEAT o etac allE,
atac] 1
        (boolexp RS revcut_rl)) ;
  in
    snd o PureThy.add_thmss [(("bool_axioms", bool_axioms), [])]
  end
*}

will do the right thing. If you find the syntax of PureThy.add_thmss too
complicated, just define yourself a shortcut:

ML {*
  fun save_thms (name, thms) =
    snd o PureThy.add_thmss [((name, thms), [])]
*}

2. Use antiquotations to refer to things from the context. Don't use the
imperative "thm" or "thms". They have no context, so they are bad :-).


I recognise that it is hard to "unlearn" these things when they have
worked for you all the years. But it is really necessary to change them (and thus break backwards compatibility) in order to bring Isabelle forward. But in the end, it should not be so difficult to solve your concrete problems.

I hope this helps... Please don't hesitate to ask if you run into more problems, and include theory files whenever you can.

All the best,
Alex






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