Email Gateway (Apr 25 2021 at 09:17): Email Gateway (Apr 25 2021 at 09:17):From: Matthys Grobbelaar <m.grobbelaar@uq.net.au>
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 =
struct
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 =
let
val t = Sign.cert_term thy raw_t
in
Terms.map (Queue.enqueue t) thy
end;
end;
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"})
</close>
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] =
let
val varlist = VarList.get (Context.theory_of (Context.Proof ctxt))
val _ = VarList.print_vars varlist ctxt
in undefined
</close>
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