Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Using the global context when performing synta...

view this post on Zulip Email Gateway (Apr 25 2021 at 09:17):

From: Matthys Grobbelaar <>
I'm currently creating new syntax translations for a project I'm working on however I'm having issues with incorrect contexts being passed into the parse_translation function.

For context, I've added the new syntax as follows:
syntax "_myrelation" :: "args => 'a set" ("<\lrel>_<\rrel>")
where <\lrel> and <\rrel> are new symbols which have been added.

The translation is then done via:
parse_translation <\open>[(@{syntax_const "_myrelation"}, translate_relation)]

Essentially what this translation will be doing is taking an expression like
<\lrel>x > x'</rrel>
and converting it into
{((x, y), (x', y')) | x > x'}
where the variables in the tuples (i.e. (x,y), (x', y')) are dynamic from the context wherein the translation takes place.

At the moment, I've been able to add these variables into a queue stored in the global context using the following:
structure VarList: VAR_LIST =

structure Terms = Theory_Data
type T = term Queue.T;
val empty = Queue.empty;
val extend = I;
fun merge (ts1, ts2) =
fold Queue.enqueue (Library.merge (op =) (Queue.content ts1, Queue.content ts2)) Queue.empty;

val get = Terms.get

fun add raw_t thy =
val t = Sign.cert_term thy raw_t
in (Queue.enqueue t) thy

With this structure, I have then been able to update the context using setup:
setup <\open>
VarList.add (@{term "x::int"}) #>
VarList.add (@{term "y::int"})

To test out whether the context is in fact being updated, I created a dummy translation function which prints out the values stored in the queue.

ML <\open>
fun translate_relation_test ctxt [trm] =
val varlist = VarList.get (Context.theory_of (Context.Proof ctxt))
val _ = VarList.print_vars varlist ctxt
in undefined

If I call this dummy function right below the setup, the variables are printed correctly:
<end of setup>
translate_relation_test (Context.the_local_context ()) [@{term "x > x'"}]; -- queue has the added variables

However, when I try to do a translation, the queue remains empty:
<lrel>x > x'</rrel> -- added variables are not printed

This leaves me with a lot of questions. Is there something I'm missing about contexts? Is a different context being used for syntax translations? Is this the correct way to go about doing a translation like this?

Any help would be greatly appreciated.
Also, this is the first time I'm sending something to this mailing list so please let me know if I'm asking in the correct place.

Kind regards and thank you in advance,
Matthys Grobbelaar

Last updated: Jul 15 2022 at 23:21 UTC