Email Gateway (Aug 18 2022 at 16:47): Email Gateway (Aug 18 2022 at 16:47):From: Alexander Krauss <krauss@in.tum.de>
Hi Brian,
I don't think this is so easy. Abbreviations are unfolded only after
type inference (being typed is one of their main advantage over old
translations). Translating case expressions later would mean that the
representation that exists before that is typable in some way. This is
probably not impossible, but requires some non-trivial rethinking of how
the translation works.
In your particular example, could you just use "notation"?
Alex
Email Gateway (Aug 18 2022 at 16:53):From: Brian Huffman <brianh@cs.pdx.edu>
On Wed, Jan 5, 2011 at 12:17 AM, Alexander Krauss <krauss@in.tum.de> wrote:
Hi Brian,
theory Scratch imports Main begin
abbreviation (input) emptystring :: string ("ε")
where "ε ≡ []"term "case s of ε ⇒ True | c # cs ⇒ False"
*** Error in case expression:
*** Not a datatype constructor: Scratch.emptystring
*** In clause
*** emptystring ⇒ True
*** Failed to parse term
*** At command "term"Apparently the parse translation for case expressions happens after
processing notation (e.g. "[]" -> "List.Nil" or "c # cs" -> "List.Cons
c cs") but before processing abbreviations (e.g. "emptystring" ->
"List.Nil :: string"). Could this be changed so that abbreviations are
expanded earlier?I don't think this is so easy. Abbreviations are unfolded only after type
inference (being typed is one of their main advantage over old
translations). Translating case expressions later would mean that the
representation that exists before that is typable in some way. This is
probably not impossible, but requires some non-trivial rethinking of how the
translation works.
Ok, I had a feeling that this would be tricky to implement. I don't
have any critical need for this feature or anything, I just tried it
on a whim and was a bit surprised by the error message I got.
In your particular example, could you just use "notation"?
No, notation won't work in this particular example, because the
abbreviation "emptystring" has a more specific type than the constant
"Nil" that it stands for.
It seems that "syntax" + "translations" is the right way to go for
this kind of thing.
Using those commands seems a bit weird though, simply because they use
old-style input syntax (similar to "consts" or "defs") instead of the
new-style (like "notation"). Modernizing the input syntax of the
"syntax" and "translations" commands would make me feel more confident
that these will continue to be fully supported as user-level commands
in the future.
Email Gateway (Aug 18 2022 at 17:01):From: Brian Huffman <brianh@cs.pdx.edu>
Is it unreasonable to expect this to work?
theory Scratch imports Main begin
abbreviation (input) emptystring :: string ("ε")
where "ε ≡ []"
term "case s of ε ⇒ True | c # cs ⇒ False"
*** Error in case expression:
*** Not a datatype constructor: Scratch.emptystring
*** In clause
*** emptystring ⇒ True
*** Failed to parse term
*** At command "term"
Apparently the parse translation for case expressions happens after
processing notation (e.g. "[]" -> "List.Nil" or "c # cs" -> "List.Cons
c cs") but before processing abbreviations (e.g. "emptystring" ->
"List.Nil :: string"). Could this be changed so that abbreviations are
expanded earlier?
I suppose I could work around this problem by using something like this:
syntax emptystring :: logic ("ε")
translations "emptystring" == "CONST Nil :: string"
but the "syntax" and "translations" commands seem to be considered a
bit "old-style" nowadays, or at least a bit too low-level to be
considered best practice.
Last updated: Apr 25 2024 at 08:20 UTC