SASyLF Mode for jEdit
7 views
Skip to first unread message
Daniel Spiewak
Oct 15, 2008, 11:56:51 AM10/15/08
to sasylf-users
SASyLF may make writing proofs a lot easier, but that still doesn't
mean that it's exactly *easy* to use SASyLF correctly. Even basic
support in a sufficiently powerful text editor can be extremely
helpful. To that end, I have created a SASyLF mode for jEdit (http://
jedit.org). To date, Dr. Boyland has been storing this on the AFS
volume for his type theory course, but it occurred to me that it just
might benefit other people who are using the language. The current
version of the mode has been uploaded to the group "Files" section.
Features
=======
This mode supports both auto-indentation (tabs not spaces) as well as
contextual syntax highlighting. Note that this is *not* semantic
highlighting alla some mainstream IDEs; jEdit has no meaningful
understanding of SASyLF or the source file you are working on.
Features include:
* Top-level keywords like `theorem` and `lemma` are highlighted
differently from secondary ones such as `forall` and `rule`
* Statement labels are highlighted specially, but this highlighting is
*not* applied to type rules (conventionally declared using a colon)
given in the rules. Note that this only works so long as all rules
come previous to any theorems or lemmas
* Judgment, theorem and lemma names are given distinct highlighting
* Justifications are highlighted according to the syntactic element to
which they correspond. For example:
s1: ... by d1
s2: ... by rule absolutely-true on d1, s1
s3: ... by induction hypothesis on s2
In statement s1, "by" is highlighted as an operator, while "d1" is
recognized and properly highlighted as a statement label. Likewise,
in s2, "absolutely-true" is known to be a rule, thus is given the
appropriate highlighting; "on" is an operator and both "d1" and "s1"
are highlighted as statement labels.
* Multi-token keywords are handled appropriately (and in some cases,
contextually). For example, "induction" is a keyword, but
"hypothesis" is not. Only when they appear together in a
justification are they both highlighted.
* Rule separators are highlighted (seems like a minor thing, but I'm
proud of it) :-)
* Token "x" (and likewise, " x' ", "x1", etc) is recognized as magic
and highlighted specially in all contexts
* Special justification "unproved" gets its own highlighting in an
attempt to make it more noticeable
Known Quirks
==========
* Justification must remain on the same line as the statement,
otherwise the auto-indentation cannot handle it. Thus:
s1: ...
by theorem my-test on d2
SASyLF is fine with this, but jEdit's auto-indenter is not powerful
enough to properly add extra indentation to a dangling "by". Thus,
these lines will actually be auto-indented as follows:
s1: ....
by theorem my-test on d2
Not a huge deal, but worth remembering. Nothing really *bad*
happens if you manually override the auto-indenter, it's just extra
work.
* Rules must come before any theorems
* Since there is no official spec for SASyLF (or even a language
README), I had to guess on syntact elements. Thus, it's possible that
I missed some keywords (I added "weakening" for the first time a week
ago).
* No support (yet) for 0.20's mutual induction syntax.
* If you *ever* dare to use ASCII character 222, all hell will break
loose and I wouldn't be surprised if the editor itself crashed.
Fortunately, I don't think that SASyLF's lexer would be too happy
either...
This is an incredibly contextual highlighting schema. Due to the way
I had to write this in jEdit's mode definition syntax, you should
expect a fair number of strange problems whenever you stray off of the
syntactic beaten path. I think I've ironed out most of the issues (at
least, it seems to highlight all of the samples correctly), but don't
be surprised if things don't color nicely when you arrange things in
an unexpected way.
Please let me know if you run across any issues. So long as I have a
sample file to reproduce, I should be able to fix (or at least hack
around) any serious inconsistencies which may (read: almost certainly)
still exist.
mean that it's exactly *easy* to use SASyLF correctly. Even basic
support in a sufficiently powerful text editor can be extremely
helpful. To that end, I have created a SASyLF mode for jEdit (http://
jedit.org). To date, Dr. Boyland has been storing this on the AFS
volume for his type theory course, but it occurred to me that it just
might benefit other people who are using the language. The current
version of the mode has been uploaded to the group "Files" section.
Features
=======
This mode supports both auto-indentation (tabs not spaces) as well as
contextual syntax highlighting. Note that this is *not* semantic
highlighting alla some mainstream IDEs; jEdit has no meaningful
understanding of SASyLF or the source file you are working on.
Features include:
* Top-level keywords like `theorem` and `lemma` are highlighted
differently from secondary ones such as `forall` and `rule`
* Statement labels are highlighted specially, but this highlighting is
*not* applied to type rules (conventionally declared using a colon)
given in the rules. Note that this only works so long as all rules
come previous to any theorems or lemmas
* Judgment, theorem and lemma names are given distinct highlighting
* Justifications are highlighted according to the syntactic element to
which they correspond. For example:
s1: ... by d1
s2: ... by rule absolutely-true on d1, s1
s3: ... by induction hypothesis on s2
In statement s1, "by" is highlighted as an operator, while "d1" is
recognized and properly highlighted as a statement label. Likewise,
in s2, "absolutely-true" is known to be a rule, thus is given the
appropriate highlighting; "on" is an operator and both "d1" and "s1"
are highlighted as statement labels.
* Multi-token keywords are handled appropriately (and in some cases,
contextually). For example, "induction" is a keyword, but
"hypothesis" is not. Only when they appear together in a
justification are they both highlighted.
* Rule separators are highlighted (seems like a minor thing, but I'm
proud of it) :-)
* Token "x" (and likewise, " x' ", "x1", etc) is recognized as magic
and highlighted specially in all contexts
* Special justification "unproved" gets its own highlighting in an
attempt to make it more noticeable
Known Quirks
==========
* Justification must remain on the same line as the statement,
otherwise the auto-indentation cannot handle it. Thus:
s1: ...
by theorem my-test on d2
SASyLF is fine with this, but jEdit's auto-indenter is not powerful
enough to properly add extra indentation to a dangling "by". Thus,
these lines will actually be auto-indented as follows:
s1: ....
by theorem my-test on d2
Not a huge deal, but worth remembering. Nothing really *bad*
happens if you manually override the auto-indenter, it's just extra
work.
* Rules must come before any theorems
* Since there is no official spec for SASyLF (or even a language
README), I had to guess on syntact elements. Thus, it's possible that
I missed some keywords (I added "weakening" for the first time a week
ago).
* No support (yet) for 0.20's mutual induction syntax.
* If you *ever* dare to use ASCII character 222, all hell will break
loose and I wouldn't be surprised if the editor itself crashed.
Fortunately, I don't think that SASyLF's lexer would be too happy
either...
This is an incredibly contextual highlighting schema. Due to the way
I had to write this in jEdit's mode definition syntax, you should
expect a fair number of strange problems whenever you stray off of the
syntactic beaten path. I think I've ironed out most of the issues (at
least, it seems to highlight all of the samples correctly), but don't
be surprised if things don't color nicely when you arrange things in
an unexpected way.
Please let me know if you run across any issues. So long as I have a
sample file to reproduce, I should be able to fix (or at least hack
around) any serious inconsistencies which may (read: almost certainly)
still exist.
Daniel Spiewak
Oct 27, 2008, 6:28:38 PM10/27/08
to sasylf-users
In response to some new things I've learned about sasylf (such as =>
is *not* magic), I am now updating the jEdit mode slightly. After my
previous announcement, Dr Aldrich correctly pointed out that a Google
Group file space isn't exactly the best place to store something like
this, particularly with an eye for future releases. In an attempt to
correct this issue without taking the obvious solution of just storing
the file on UWM's servers, I have made the Git repository containing
this mode available on GitHub. The parent project can be found here
(http://github.com/djspiewak/jedit-modes/tree/master) along with some
other useful modes (including a very buggy mode for Cool). If you
wish to directly access the actual mode, the full URL is as follows:
http://github.com/djspiewak/jedit-modes/tree/master%2Fsasylf.xml?raw=true
I will keep the Git repository up to date with changes to the mode as
I make them (including the still-coming support for mutual
induction). Whenever anything significant is implemented (or fixed)
to the point where it doesn't break existing highlighting, I'll post a
brief announcement on this thread. Enjoy!
Daniel
is *not* magic), I am now updating the jEdit mode slightly. After my
previous announcement, Dr Aldrich correctly pointed out that a Google
Group file space isn't exactly the best place to store something like
this, particularly with an eye for future releases. In an attempt to
correct this issue without taking the obvious solution of just storing
the file on UWM's servers, I have made the Git repository containing
this mode available on GitHub. The parent project can be found here
(http://github.com/djspiewak/jedit-modes/tree/master) along with some
other useful modes (including a very buggy mode for Cool). If you
wish to directly access the actual mode, the full URL is as follows:
http://github.com/djspiewak/jedit-modes/tree/master%2Fsasylf.xml?raw=true
I will keep the Git repository up to date with changes to the mode as
I make them (including the still-coming support for mutual
induction). Whenever anything significant is implemented (or fixed)
to the point where it doesn't break existing highlighting, I'll post a
brief announcement on this thread. Enjoy!
Daniel
Jonathan Aldrich
Oct 27, 2008, 10:21:15 PM10/27/08
to sasylf...@googlegroups.com
Thanks, Daniel, for your great work on this! Good editor support is
essential for any programming language. We're working on an Eclipse
plugin for SASyLF as well (to be released very soon); the two should
compliment each other.
essential for any programming language. We're working on an Eclipse
plugin for SASyLF as well (to be released very soon); the two should
compliment each other.
Jonathan
Daniel Spiewak
Oct 30, 2008, 8:09:06 PM10/30/08
to sasylf-users
It's update time! I have added the long-promised support for mutual
induction within the jEdit SASyLF mode. I had entertained some hopes
that I could make the highlighting for `and` somewhat "smart" in not
allowing standalone "ands" at the top level, but I found that I could
not do this reliably due to the way that jEdit's parser consumes
tokens.
Anyway, the way I have done it should work just fine. The only
problem is that `and` will now be a reserved word *everywhere*. I
think this is how SASyLF's parser handles `and`, so I'm not too
worried, but it does preclude future "and judgments" as requested by
Dr Boyland. If and when that case arises, I do have an idea which
should make everything work quite nicely (different `and` highlighting
in different contexts), but I'm too lazy to implement this right now.
The URL for the mode itself remains the same. In case your scroll-
wheel is broken: http://github.com/djspiewak/jedit-modes/tree/master%2Fsasylf.xml?raw=true
Enjoy!
Daniel
On Oct 27, 5:28 pm, Daniel Spiewak <djspie...@gmail.com> wrote:
> In response to some new things I've learned about sasylf (such as =>
> is *not* magic), I am now updating the jEdit mode slightly. After my
> previous announcement, Dr Aldrich correctly pointed out that a Google
> Group file space isn't exactly the best place to store something like
> this, particularly with an eye for future releases. In an attempt to
> correct this issue without taking the obvious solution of just storing
> the file on UWM's servers, I have made the Git repository containing
> this mode available on GitHub. The parent project can be found here
> (http://github.com/djspiewak/jedit-modes/tree/master) along with some
> other useful modes (including a very buggy mode for Cool). If you
> wish to directly access the actual mode, the full URL is as follows:http://github.com/djspiewak/jedit-modes/tree/master%2Fsasylf.xml?raw=...
induction within the jEdit SASyLF mode. I had entertained some hopes
that I could make the highlighting for `and` somewhat "smart" in not
allowing standalone "ands" at the top level, but I found that I could
not do this reliably due to the way that jEdit's parser consumes
tokens.
Anyway, the way I have done it should work just fine. The only
problem is that `and` will now be a reserved word *everywhere*. I
think this is how SASyLF's parser handles `and`, so I'm not too
worried, but it does preclude future "and judgments" as requested by
Dr Boyland. If and when that case arises, I do have an idea which
should make everything work quite nicely (different `and` highlighting
in different contexts), but I'm too lazy to implement this right now.
The URL for the mode itself remains the same. In case your scroll-
wheel is broken: http://github.com/djspiewak/jedit-modes/tree/master%2Fsasylf.xml?raw=true
Enjoy!
Daniel
On Oct 27, 5:28 pm, Daniel Spiewak <djspie...@gmail.com> wrote:
> In response to some new things I've learned about sasylf (such as =>
> is *not* magic), I am now updating the jEdit mode slightly. After my
> previous announcement, Dr Aldrich correctly pointed out that a Google
> Group file space isn't exactly the best place to store something like
> this, particularly with an eye for future releases. In an attempt to
> correct this issue without taking the obvious solution of just storing
> the file on UWM's servers, I have made the Git repository containing
> this mode available on GitHub. The parent project can be found here
> (http://github.com/djspiewak/jedit-modes/tree/master) along with some
> other useful modes (including a very buggy mode for Cool). If you
Jonathan Aldrich
Jul 31, 2009, 5:14:47 PM7/31/09
to sasylf...@googlegroups.com
One of my students is using SASyLF for real research, and found that the
hardest aspect of using SASyLF is coming up with exactly the right cases
in case analysis. I'm sure many SASyLF users feel the same.
hardest aspect of using SASyLF is coming up with exactly the right cases
in case analysis. I'm sure many SASyLF users feel the same.
It turns out that in order to check that all cases are present, the tool
has to generate them. So if you are missing one, the tool can
(conceptually) tell you *exactly* what the missing cases are. Should it?
For a "real" user like my student, the answer is clearly yes. But would
this take away too much of a "learning opportunity" in an educational
context?
I actually have a kludgey version of this implemented already, but have
not distributed it (beyond the one student) because of this concern.
Let me know what you think.
Jonathan
Daniel Spiewak
Jul 31, 2009, 5:22:26 PM7/31/09
to sasylf...@googlegroups.com
I would be in favor of comprehensive error messages on missing cases. Scala does something like this when it can definitively say that a match is non-exhaustive:
scala> val t: Option[String] = Some("test")
t: Option[String] = Some(test)
scala> t match {
| case None => 42
| }
<console>:6: warning: match is not exhaustive!
missing combination Some
t match {
^
Speaking as a student, I don't think I learned all that much from trying to root through which cases I was missing. When I'm thinking about a proof, such activities are "operational boilerplate", something which is necessary for the proof, but doesn't require any real thought. It would be nice to simply rely on the engine for this task.
Daniel
scala> val t: Option[String] = Some("test")
t: Option[String] = Some(test)
scala> t match {
| case None => 42
| }
<console>:6: warning: match is not exhaustive!
missing combination Some
t match {
^
Speaking as a student, I don't think I learned all that much from trying to root through which cases I was missing. When I'm thinking about a proof, such activities are "operational boilerplate", something which is necessary for the proof, but doesn't require any real thought. It would be nice to simply rely on the engine for this task.
Daniel
Reply all
Reply to author
Forward
0 new messages