Email Gateway (Apr 30 2021 at 01:35): Email Gateway (Apr 30 2021 at 01:35):From: Matthys Grobbelaar <m.grobbelaar@uq.net.au>
I'm currently attempting to do syntax translations which require data (a queue) from the current theory context.
I've been able to add the queue into the theory context using the Theory_Data functor, however I can't seem to access that data in my translation function (called via parse_translation). For reference, I've been using the "Isabelle/Isar Implementation" (implementation.pdf (tum.de)<https://isabelle.in.tum.de/dist/Isabelle2021/doc/implementation.pdf> Chapter 1.1 as a basis for adding data into the context.
Am I adding the data into the wrong place? What's the correct way of doing this?
Kind regards and thank you in advance,
Matthys Grobbelaar
Email Gateway (Apr 30 2021 at 10:22):From: Dominique Unruh <unruh@ut.ee>
Hi,
how are you accessing the theory inside your parse translation? If you
use the ML antiquotation \<^theory> (rendered /theory/), then you get
the theory that you had at compile time of the parse translation. (And
theories are immutable, so changing the theory data will not affect that
theory.) The correct way is to use the context that is given to the
parse translation as an argument, and then get the theory via
"Proof_Context.theory_of ctxt". (If this is already what you are doing,
sorry for pointing out the obvious.)
Best wishes,
Dominique.
Email Gateway (Apr 30 2021 at 23:52):From: Matthys Grobbelaar <m.grobbelaar@uq.net.au>
Hi Dominique,
Thank you for your quick response.
At the moment, I've been accessing the theory with the following: Context.theory_of (Context.proof ctxt) where ctxt is the context given to the parse translation.
I've since changed it to be Proof_Context.theory_of ctxt which looks cleaner and appears to yield identical results.
At the moment, I've been testing this as follows:
* Making a duplicate translation function in the file where I'm modifying the theory context (via setup and using the functor) and called it directly: val _ = parse_val (Context.the_local_context ()) [@{term "..."}]
* Making a direct call to my original translation function (which lives in another theory) with the same parameters: val _ = parse_val_orig (Context.the_local_context ()) [@{term "..."}]
* Using the syntax directly in the file where I'm modifying the theory context: <\lrel>...</rrel> where <\lrel> and <\rrel> is the new syntax (just a pair of parentheses essentially)
The dummy translation function is as follows (essentially just printing out the content of the queue):
fun parse_val ctxt [trm] =
let
val data = VarList.get (Proof_Context.theory_of ctxt) (* VarList is the structure using the functor which stores the data *)
val _ = VarList.print_vars data ctxt
in undefined end;
The duplicate function in the file where the I'm modifying the context prints out the values in the queue correctly. The direct call to the translation function in the other theory and the use of syntax (which also uses this other function) prints nothing (an empty queue). Note that the printing function does not modify the queue passed in for printing.
Why would the same argument, given to identical methods in different files, have different results? It seems a bit strange to me.
Kind regards and thank you in advance,
Matthys Grobbelaar
Email Gateway (May 01 2021 at 09:15):From: Makarius <makarius@sketis.net>
I find it hard to follow what you are actually doing. Can you show the formal
explanation written in Isabelle/ML?
A lot of details are non-standard in the small snipptes (e.g. use of
Context.the_local_context, undefined, trm as name for a term), so it is likely
that the overall approach is somehow wrong.
Further note that in functional programming, functions are called "functions",
not methods.
Makarius
Email Gateway (May 01 2021 at 09:41):From: Dominique Unruh <unruh@ut.ee>
Why would the same argument, given to identical methods in different
files, have different results? It seems a bit strange to me.
That does seem very strange to me, too. My best hypothesis is that they
are not, actually, identical methods. (They might have the exact same
code but, due to different namespaces, call different functions in their
code.)
What I would try:
* Write \<^context> instead of "Context.the_local_context ()" in your
experiments (shouldn't change much, but if you want to refer to the
current context at compile time of a given code snippet, that's the
right thing to use).
* Ctrl-click on both of VarList.get and VarList.print_vars to see
where jEdit jumps. If it jumps to different places, then you have
accidentally defined VarList twice. (Also check whether you might
include the same ML-file twice.)
* Try and print theory you got, to see if it's the right one (val _ =
Proof_Context.theory_of ctxt |> \<^print> or something like that).
\<^print> is useful generally for debugging because it can be
applied to anything, not just strings.
* Instead of "undefined", you can also as a hack return debug output
from a parse translation via: HOLogic.mk_literal string_to_return
(this will then give you a string literal inside your parsed
output). Not sure it helps specifically with your current problem,
but it might be useful in general.
Best wishes,
Dominique.
Email Gateway (May 02 2021 at 04:01):From: Matthys Grobbelaar <m.grobbelaar@uq.net.au>
Hi Makarius,
My overall approach is as follows:
In order to add my queue of data into the theory context I have the following structure defined in a file structures.ML:
--- BEGIN structures.ML ---
signature VAR_LIST =
sig
val get: theory -> term Queue.T
val add: term -> theory -> theory
val reset: theory -> theory
end;
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;
fun reset thy = Terms.put (Queue.empty) thy;
end;
--- END structures.ML ---
Then, in a separate theory file, I have my syntax definition and translation function:
--- BEGIN MyRelations.thy ---
theory MyRelations
imports Main (* I'm not sure if there's a more appropriate theory to import *)
begin
ML_file \<open> structures.ML \<close>
syntax
"_myrelation" :: "args => 'a set" ("\<lrel>_\<rrel>") (* lrel and rrel are new symbols I've defined *)
ML \<open>
fun translate_relation ctxt [trm] =
let
val data = VarList.get (Proof_Context.theory_of ctxt) (* Retrieve the data in the theory context *)
val _ = print_var_list data ctxt (* Just prints out the terms in the list with the given context *)
(* My actual translation uses the data stored to build a set of tuples satisfying a predicate *)
val translation = @{term "{((x, y),(x', y')). x > x'}"} (* Just a dummy value for demo purposes *)
in
translation
end
\<close>
parse_translation \<open>[(@{syntax_const "_myrelation"}, translate_relation)] \<close>
end
--- END MyRelations.thy ---
Finally, I have a theory file used for testing the translation:
--- BEGIN TestRelation.thy ---
theory TestRelation
imports "MyRelations"
begin
(* Update the theory context with the necessary data for translation *)
setup \<open>
VarList.add (@{term "x"}) #>
VarList.add (@{term "y"}) #>
VarList.add (@{term "z"})
\<close>
(* See if the syntax creates the correct result *)
(* Note that the variables added create the tuples in the set comprehension *)
(* Here, the queue data is not printed out *)
lemma test_relation: "\<lrel> x > x' \<rrel>" = "{((x,y,z), (x',y',z')). x > x'}"
(* We also create a duplicate of the translation function to see if it works differently *)
ML \<open>
fun translate_relation_dup ctxt [trm] =
let
val data = VarList.get (Proof_Context.theory_of ctxt)
val _ = print_var_list data ctxt
val translation = @{term "{((x, y),(x', y')). x > x'}"}
in
translation
end
(* We call the duplicate translation function directly - the data is printed *)
val res = translate_relation_dup (Context.the_local_context ()) [@{term "x > x'"}]
\<close>
end
--- END TestRelation.thy ---
So essentially, when the translation function is called via the syntax, the data stored
in the theory context is not passed into the function. However, when I call a duplicate
translation function with what I would think are identical arguments, the stored data
is present.
I'm not sure where I'm going wrong. Any help is much appreciated. I'm quite new
to Isabelle so I'm certain that there are better ways to go about this.
Kind regards and thank you in advance,
Matthys Grobbelaar
I find it hard to follow what you are actually doing. Can you show the formal explanation written in Isabelle/ML?
A lot of details are non-standard in the small snipptes (e.g. use of Context.the_local_context, undefined, trm as name for a term), so it is likely that the overall approach is somehow wrong.
Further note that in functional programming, functions are called "functions", not methods.
Makarius
Email Gateway (May 02 2021 at 04:09):From: Matthys Grobbelaar <m.grobbelaar@uq.net.au>
Hi Dominique,
Thank you for your advice.
Learning about \<^context>, <\^print> and mk_literal has been very useful and has made debugging a lot easier.
With regards to looking where JEdit jumps to, both jump to the same structure so the code is the same there. Also printing the theory appears to give the same output as well. It may well be that there is something happening with the namespaces.
Kind regards,
Matthys Grobbelaar
From: Dominique Unruh <d.unruh@gmail.com> On Behalf Of Dominique Unruh
Sent: Saturday, 1 May 2021 7:41 PM
To: Matthys Grobbelaar <m.grobbelaar@uq.net.au>
Cc: cl-isabelle-users@lists.cam.ac.uk
Subject: Re: [isabelle] parse_translation does not detect changes in theory data
Why would the same argument, given to identical methods in different files, have different results? It seems a bit strange to me.
That does seem very strange to me, too. My best hypothesis is that they are not, actually, identical methods. (They might have the exact same code but, due to different namespaces, call different functions in their code.)
What I would try:
* Write \<^context> instead of "Context.the_local_context ()" in your experiments (shouldn't change much, but if you want to refer to the current context at compile time of a given code snippet, that's the right thing to use).
* Ctrl-click on both of VarList.get and VarList.print_vars to see where jEdit jumps. If it jumps to different places, then you have accidentally defined VarList twice. (Also check whether you might include the same ML-file twice.)
* Try and print theory you got, to see if it's the right one (val _ = Proof_Context.theory_of ctxt |> \<^print> or something like that). \<^print> is useful generally for debugging because it can be applied to anything, not just strings.
* Instead of "undefined", you can also as a hack return debug output from a parse translation via: HOLogic.mk_literal string_to_return (this will then give you a string literal inside your parsed output). Not sure it helps specifically with your current problem, but it might be useful in general.
Best wishes,
Dominique.
Email Gateway (May 02 2021 at 10:03):From: Makarius <makarius@sketis.net>
These theory and ML sources are the main means of communication, both with the
system and between humans.
I've put everything into "canonical form", such it tells the story on its own
account, using standard "style and orthography": see the attached
My_Relation.thy. Doing this, it magically worked in the end, while your
original sources did not even type-check (maybe something was missing here and
there).
Of course, it requires some practice to do things in the proper way. It helps
to look around in documentation and existing implementations, and eventually
develop a taste for good and bad approaches.
Here are also some concrete hints for your attempt so far:
* There is no point to have many small files to obscure the structure of the
project. Instead, I've written just one "theory document" with various
sections. (As the project grows and matures, it will of course have more files
at some later stage, e.g. at a healthy size of 5-25 KByte each.)
* A theory name should consist of several words separated by underscore,
describing the main concept of your theory in singular. Plural is only used if
you have multiple concepts, or multiple examples. E.g. theory
"My_Great_Concept" vs. theory "My_Great_Concept_Examples". Moreover,
WeDontUseCamelCaseAnymore, because Underscore_has_been_discovered_decades_ago.
* For Isabelle/HOL the canonical import is indeed theory "Main"; you should
not import anything more primitive inside HOL, because that would mean to
depend on its rather complex bootstrap. Sometimes you need more base material,
e.g. types rat, real, complex: then you import "Complex_Main" or a different
library entry point (beyond Main).
* Theory data: Instead of the slightly odd Queue.T you can use a plain list
in "canonical reverse order" as shown in my version. To add means to "cons",
and to merge means to use the standard operation "Library.merge": with proper
equality on type term (aconv).
* Symbols \<lrel> and \<rrel>: it is OK to experiment with newly allocated
symbols in the infinite space of possibilities, but to get anything into the
official Isabelle release (e.g. for Isabelle/AFP entries with more than one
user), it needs to be really convincing. (I've done that with some Z guys
recently, and it required 2 weeks to get everything right: fonts, latex
macros, symbol names and groups.)
It is often better to use variants of pre-allocated symbols, e.g. together
with \<^bold> or other decoration to avoid conflicts. It is easy to define
specific input methods for Isabelle/jEdit in the theory header using
"abbrevs", e.g. see theory HOL-Library.Finite_Map.
Side-remark: the Isabelle Prover IDE is called Isabelle/jEdit, while "jEdit"
is a plain text editor used as a basis for that. Nobody would call an Emacs
mode for Isabelle just "Emacs", or a VSCode extension for Isabelle just "VSCode".
It is important to treat the jEdit project honestly as something separate (and
quite different). It deserves its original name for itself, and not confuse it
with our Prover IDE add-ons.
(An alternative is to call Isabelle/jEdit abstractly "PIDE".)
Makarius
My_Relation.thy
Email Gateway (May 02 2021 at 12:58):From: Matthys Grobbelaar <m.grobbelaar@uq.net.au>
Hi Makarius,
Thank you for the great advice, I appreciate it! It will really help improve my programming in Isabelle.
With regards to structuring theories, I am constructing a framework of syntax translations (as part of a larger project) and would like to have a single top-level entry point which the other theories in the project can include if they would like to use the framework.
At the moment I have the following entry point:
--- BEGIN Translations_Main.thy ---
theory Translations_Main
imports
"core/My_Relation"
"core/My_Predicate"
(* More imports are added here as the framework evolves *)
begin
end
--- END Translations_Main ---
Then any other theory can simply use the framework by importing Translations_Main.
Is this the correct way to go about structuring such a framework? Are there things I should watch out for?
Kind regards and thank you in advance,
Matthys Grobbelaar
These theory and ML sources are the main means of communication, both with the system and between humans.
I've put everything into "canonical form", such it tells the story on its own account, using standard "style and orthography": see the attached My_Relation.thy. Doing this, it magically worked in the end, while your original sources did not even type-check (maybe something was missing here and there).
Of course, it requires some practice to do things in the proper way. It helps to look around in documentation and existing implementations, and eventually develop a taste for good and bad approaches.
Here are also some concrete hints for your attempt so far:
* There is no point to have many small files to obscure the structure of the project. Instead, I've written just one "theory document" with various sections. (As the project grows and matures, it will of course have more files at some later stage, e.g. at a healthy size of 5-25 KByte each.)
* A theory name should consist of several words separated by underscore, describing the main concept of your theory in singular. Plural is only used if you have multiple concepts, or multiple examples. E.g. theory "My_Great_Concept" vs. theory "My_Great_Concept_Examples". Moreover, WeDontUseCamelCaseAnymore, because Underscore_has_been_discovered_decades_ago.
* For Isabelle/HOL the canonical import is indeed theory "Main"; you should not import anything more primitive inside HOL, because that would mean to depend on its rather complex bootstrap. Sometimes you need more base material, e.g. types rat, real, complex: then you import "Complex_Main" or a different library entry point (beyond Main).
* Theory data: Instead of the slightly odd Queue.T you can use a plain list in "canonical reverse order" as shown in my version. To add means to "cons", and to merge means to use the standard operation "Library.merge": with proper equality on type term (aconv).
* Symbols \<lrel> and \<rrel>: it is OK to experiment with newly allocated symbols in the infinite space of possibilities, but to get anything into the official Isabelle release (e.g. for Isabelle/AFP entries with more than one user), it needs to be really convincing. (I've done that with some Z guys recently, and it required 2 weeks to get everything right: fonts, latex macros, symbol names and groups.)
It is often better to use variants of pre-allocated symbols, e.g. together with \<^bold> or other decoration to avoid conflicts. It is easy to define specific input methods for Isabelle/jEdit in the theory header using "abbrevs", e.g. see theory HOL-Library.Finite_Map.
Side-remark: the Isabelle Prover IDE is called Isabelle/jEdit, while "jEdit"
is a plain text editor used as a basis for that. Nobody would call an Emacs mode for Isabelle just "Emacs", or a VSCode extension for Isabelle just "VSCode".
It is important to treat the jEdit project honestly as something separate (and quite different). It deserves its original name for itself, and not confuse it with our Prover IDE add-ons.
(An alternative is to call Isabelle/jEdit abstractly "PIDE".)
Makarius
Email Gateway (May 02 2021 at 13:29):From: Makarius <makarius@sketis.net>
It is correct, merely some possibilities for fine-tuning:
* No need for "_Main" in the name, just use a theory name that describes
your framework, and potentially let it coincide with the session name. For
example: session "My_Great_Framework" with main theory "My_Great_Framework"
(and "_Framework" does not have to be literally in the name).
* Sub-directories for sessions are possible, but somehow confusing: it
complicates the mapping of the per-session theory name space to files, both
for the system and the user.
* Did you actually have a proper ROOT file with session definition already?
If not, you can start with "isabelle mkroot" and then remove the generated
document setup; or you just look at example ROOT files (and strip the "HOL-"
name prefix).
Makarius
Last updated: Jul 15 2022 at 23:21 UTC