Theorems with multiple results are desirable to avoid the need to create 
synthetic "and" judgments.

SImilarly when inverting a rule with multiple inputs, it would be great if we 
could get all at once,
AND that:
   (1) the context's current substitution would be updated and
   (2) new variables could be generated.

Furthermore, a rule with ZERO inputs (e.g. type equality) could be inverted 
into a side-effect on the contexts current substitution.

If one puts a binding in a lemma argument (see attached file):

        _: Gamma |- t2[t1] t3[t1] ~>* t2'[t1] t3[t1] by lemma anys-app-1 on e', (t3[t1])

SASyLF 1.0.2 original through (uwm 9) gets an exception.
The latest SVN stacktrace is:

Internal SASyLF error!
java.lang.ClassCastException: edu.cmu.cs.sasylf.ast.Binding cannot be cast to 
edu.cmu.cs.sasylf.ast.Clause
        at edu.cmu.cs.sasylf.ast.DerivationWithArgs.typecheck(DerivationWithArgs.java:59)
...

If there is an error, it shows up as a red X in the margin of the editor, but 
the message cannot be found.  Instead one has to manually find the correct 
error in the Problems view.

ctx.innermostGamma and related parts of the context are badly broken.
They are trying to handle Twelf style blocks but get in the way.
In particular, in a match of a "var" rule that changes Gamma into Gamma',x...,
the new binding is added to all judgments referenced, even if context makes
no sense for them.  In the attached file, this means that a natural number
equality judgment gets an attached context and then doesn't match any rules!

Fixing this properly will require fixing contexts (issue #8),
but perhaps I can come up with a temporary fix. 

This bug applies to SASyLF 0.22, and SASyLF 1.0.2 (uwm 14)
and everything in between.

The new "assumes" syntax for theorem parameters shouldn't be allowed when the 
nonterminal doesn't use the context:

forall n assumes Gamma
when n is a natural number.

It is related to Issue #9 because that caused "assumes" to be copied to all 
later nonterminals with bad effects.
This bug can cause SASyLF to be confused as to whether the nonterminal depends 
on not on the context, because it uses canAppearIn and also the context and 
these messages are contradictory.

See attached bug file.

If a lemma has a forall/premise
   * |- ...

then current (through uwm13) SASyLF permits it to be called
with a judgment of the form:
  Gamma |- ....

This means that the variable case may be lost.
(This would permit us to prove progress even in non-empty contexts!)

Old (Fall 2008) Homework #8 code

Code not attached, but exception is:
Internal SASyLF error!
java.lang.ClassCastException: edu.cmu.cs.sasylf.term.Application cannot be cast 
to edu.cmu.cs.sasylf.term.Abstraction
        at edu.cmu.cs.sasylf.ast.DerivationByAnalysis.adapt(DerivationByAnalysis.java:188)
        at edu.cmu.cs.sasylf.ast.Theorem.verifyLastDerivation(Theorem.java:173)
        at edu.cmu.cs.sasylf.ast.Case.typecheck(Case.java:32)
        at edu.cmu.cs.sasylf.ast.RuleCase.typecheck(RuleCase.java:303)
        at edu.cmu.cs.sasylf.ast.DerivationByAnalysis.typecheck(DerivationByAnalysis.java:113)
        at edu.cmu.cs.sasylf.ast.Case.typecheck(Case.java:29)
        at edu.cmu.cs.sasylf.ast.RuleCase.typecheck(RuleCase.java:303)
        at edu.cmu.cs.sasylf.ast.DerivationByAnalysis.typecheck(DerivationByAnalysis.java:113)
        at edu.cmu.cs.sasylf.ast.DerivationByInduction.typecheck(DerivationByInduction.java:38)
        at edu.cmu.cs.sasylf.ast.Theorem.typecheck(Theorem.java:125)
        at edu.cmu.cs.sasylf.ast.CompUnit.typecheck(CompUnit.java:140)
        at edu.cmu.cs.sasylf.ast.CompUnit.typecheck(CompUnit.java:95)
        at edu.cmu.cs.sasylf.Main.main(Main.java:60)

The context is (I have some local changes) 

            if (!varSet.isEmpty()) {
                //TODO: make this more principled (e.g. work for more than one adaptation -- see code below)
                debug("adaptation sub = " + ctx.adaptationSub + " applied inside " + ctx.adaptationMap.get(ctx.adaptationRoot).varTypes.size());
                debug("current sub = " + ctx.currentSub);
                term = ((Abstraction)term).subInside(ctx.adaptationSub, ctx.adaptationMap.get(ctx.adaptationRoot).varTypes.size());
                debug("term = " + term);
            }

SASyLF doesn't check that syntax is inhabited; it assumes it is.
So the existential syntax in a theorem never needs to be given explicitly.
This is very convenient but is unsound if a nonterminal is useless, e.g.,
in the attached file:
    u ::= u + u

There are no instances of u, so we can use it to prove a contradiction.
This error is long-standing.
See attached: a proof of false.

What steps will reproduce the problem?

1. Define an object language without explicit parentheses in the grammar
2. State a theorem where explicit parentheses are present

What is the expected output? What do you see instead?

The expected output is an error message, an IndexOutOfBoundsException is thrown 
instead.

What version of the product are you using? On what operating system?

Eclipse plug-in org.sasylf_1.2.4a1.v20140107.jar
Eclipse Kepler Service Release 1 (20130919-0819) x64
Windows 7 x64

If we have a derivation
    Γ, x:τ ⊢ t[x] : τ'
that we do case analysis on, and then handle the case:
    x':τ' ∈ (Γ', x':τ', x:τ)
then inside this case, if we mention Γ at all, SASyLF 1.2.1 through 1.2.5 (and 
1.3.0) get confused and get variables mixed up.  This bug seems to go far back, 
but wasn't noticed until the "proof" syntax was added, and even then not until 
the substitution lemma was rewritten to use it.  The "proof" syntax copies in 
the goal clause which (in substitution) mentions Γ.

There are two extremely different methods for adapting terms in 
DerivationByAnalysis.java.  Forcing the first one to use the second when 
possible seems to fix almost all the problems, while perhaps introducing some 
minor new problems.  So this section of the code needs a rewrite (and get moved 
to Derivation.java or even to Context.java).

The cut-elimination proof (1.3.1a4) includes duplication that will only get 
worse if we add more terms (or, false, exists) because of O(n^2) pattern 
matching.

I propose adding a "do case analysis on : ... end case analysis"
that can handle *some* cases ahead of time.  This is related to, but nicer to 
use than the "else" approach.  It lightens the cognitive load by avoiding a 
nesting level.

It would be implemented by remembering the case analysis for use later.

See attached file accepted by SASyLF.  Crucially

    d1: n1 = n1 by rule eq
    use inversion of eq on d1
    d2: n1 = n2 by d1

The inversion rule generates an internal "n42" that n1 is bound to,
but n42 is not marked as an input variable, so d2 is then free to bind n42 to 
n2.  

What steps will reproduce the problem?
1. Create a judgement with a symbol composed of multiple characters, e.g., ->*
2. Use Quick Fix to insert a missing case that uses that symbol

What is the expected output? What do you see instead?
The symbol is inserted with additional spaces between the individual 
characters, e.g., "- > *" instead of "->*".

What version of the product are you using? On what operating system?
SASyLF 1.2.4a7
Eclipse Kepler Service Release 1 (20130919-0819)
Win 7 x64

If one checks a SASyLF file (currently, by saving it),
then all problems for other files are cleared.

Using
    exists T'' == all X <: T11' => T12'[X] 
    and * |- T11'' <: T11' 
    and *, X <: T11'' |- T12'[X] <: T12[X].
as the result of a lemma (e.g. in POPLmark 2a)
gets an error about X being unbound.

But it would be impossible for the current "and" framework to handle this case 
anyway, so it should give a more reasonable error.

But even with "assumes", it should be possible to do something like this.

It would be very helpful, also for teaching purposes, to be able to fold blocks 
such as cases, sub-proofs or even whole theorems. This would often make it 
possible to fit all relevant information on the screen.

If you have induction on a term (not a judgment),
and that term is used in a judgment and then you
do case analysis on the judgment, the term is
indirectly case'd on.  But the subderivation check for
induction does not notice, and signals an error.

What steps will reproduce the problem?
1. Declare a rule with different premises but identical names
2. Try to apply the rule to a derivation

What is the expected output? What do you see instead?
I would prefer if SASyLF would report an error if it detects multiple rules 
with the same name. Currently, an "the rule cannot legally be applied to the 
arguments" error is reported when one of the rules is to be applied, but the 
error message is not really helpful because it distracts from the real error 
reason.

What version of the product are you using? On what operating system?
SASyLF Eclipse plugin 1.2.4a4 on Eclipse Kepler x64. Windows 7 x64

An "assumes Gamma" line on a judgment crashes if "Gamma" is not the correct 
name for the context.  The same crash does not happen for theorems.

For various reasons, it would be nice to have a way to declare values, e.g.

   1 :=: S 0

or

   null :=: ptr(0)

This would make for better clarity (like named constants) and
this sort of thing needed if/when we add modules.

equality rules often have no premises:

       ----- eq
       n = n

Inverting one of these rules has a side-effect of
unifying the variables on each side of the equality.
The syntax does not (but possibly the internal forms does) permit

      () by inversion of eq on e

but this way of writing it is confusing.  Perhaps better is to write:

       use inversion of eq on e

as syntactic sugar for the previous.

See the attached file.

A rule shouldn't be allowed to hide context from its premises.
Neither should it permit pattern matching on contexts:
the conclusion shouldn't have a non-trivial context.

So a rule cannot be:
            ...
            ----------------------
            Gamma, x |- ...

And if the conclusion has an empty context, then the
rules above cannot use a context variable:

            Gamma |- ...
            --------------
            * |- ...

Indeed, I'm not sure if it makes sense to have anything except "Gamma"
as the context of the conclusion.

I often define syntax with implicit parens, e.g.

  t ::= t,t
     | ...

and then use (t,t) as syntax for pairs everywhere.
But sasylf (uwm 14) and earlier don't permit 

case (t1,t2) is ...

See attached file.  The rule that gets handled wrong is:

CT; Gamma |- t : C
CT |- class C
--------------------------- T-Bang
CT; Gamma |- t ! : C

Notice that CT (the "class table") is used both in Gamma specific rules
and in a rule that does not use Gamma.  As it happens CT has the
potential to have variables in it.  (If it didn't, the bug doesn't surface).

Here's the case analysis that fails:

lemma test:
    forall dt: CT; Gamma, x:C |- t[x] : C1
    exists CT |- class C1 .
    _: CT |- class C1 by induction on dt:
        case rule
            dt: CT; Gamma, x:C |- t'[x] : C1
            fl: CT |- class C1
            ------------------------------------ T-Bang
            _:  CT; Gamma, x:C |- t'[x] ! : C1
        is
            _: CT |- class C1 by fl
        end case
    end induction
end lemma

% sasylf --LF bug.slf
bug.slf:63 The rule case given is invalid; it is most likely too specific in 
some way and should be generalized
SASyLF considered the LF term (T-BangTERM [fn x:t => fn INTERNAL_DERIV_x:(isvar 
[BoundVar1, C]) => (type [CT, (H_13 [BoundVar2]), C1]), (lookup [CT_6, C1]), fn 
x:t => fn INTERNAL_DERIV_x:(isvar [BoundVar1, C]) => (type [CT, (C_! [(H_13 
[BoundVar2])]), C1])])
bug.slf: 1 error found

If you read the LF error carefully, you will see that it uses different 
variables (CT versus CT_6) for the different occurrences of CT in the rule 
which means that unification fails.  If the rule case uses CT' for the 
occurrence on the middle line, then the pattern match succeeds, but the "by fl" 
justification fails because CT is not the same as CT'.

The pattern matcher should NOT come up with different fresh variables because 
"dt" obviously says that CT does not depend on variable x.  (The problem may be 
a simple one of not freshify'ing the variables inside the       
abstraction, but I would have expected a bug like that to be more obvious.)

I'm trying to model FJ in SASyLF and writing the substitution lemma gets broken 
here.
The attached file is a (very) dumbed down version of fj.slf

It is common to use numeric subscripts in variable names. Currently, SASyLF 
will accept eg:

judgment eq: n = n
------- eq-refl
n1 = n1

but not eg:

judgment eq: n = n
------- eq-refl
n₁ = n₁

The attached example file will pass the checker after this enhancement is 
implemented but does not now.

If one mixes pattern matching which causes variables to be unified
with variable matches from context, the "wrapping subs"  don't
correctly work with the pattern matching unification "current subs".

As a result, we often lose unification that was valid.

e.g. if t1 and t2 are unified by a pattern match and then we reveal
a variable x from the context, then t1 -> t1'[x] and t2 -> t2'[x]
but t1'[x] and t2'[x] aren't related.

The attached file bug.slf shows 3-4 different errors caused by this.
(the last two errors are identical in SASyLF 1.0.2, but are distinguished
in SASyLF 1.1.0 because DerivationByPrevious is smarter than previously).

If we have managed to prove something impossible,
this lets us prove anything using syntax such as

   proof by case analysis on x: end case analysis

This would be clearer written as

    proof by contradiction on x

Internally, of course, the complex form can be used.

"by inversion" allows you to bind existing bound variables to new unknown 
variables in the inversion.  Indeed, one is not allowed to use a new variable.

See attached file with the lemma:
lemma weird:
    forall p: S n1 + n2 = n3
    forall n4
    exists n1 + n2 = n4.
    proof by inversion of plus-s on p
end lemma

Inversion should not permit 'n4' to be used as a fresh variable.

This bug goes way back, presumably to the new definition of inversion in 1.1.0 
or in the uwm releases.

Run SASyLF on the attached file.
It gets no errors.

The crucial lines are:
    17    a: 0 == 0 by rule eq
    18    b: s 0 == s 0 by rule eq
    19    c: s 0 == n by weakening on b
    20    d: 0 == n by weakening on a

I expected to see an error on line 20 with the second instance of 
weakening which rebinds n to an incompatible value.  But it lets me go 
ahead and then with case analysis, I can uncover the old binding on line 
19 and eventually prove that 0 == s 0.

(Discovered by a CS732 student here at UWM when doing homework.  I 
generated the simple example.)

It'd be great to have auto-indent working in the plugin.
And "tab" to mean increase indentation level.

If the judgment for a missing case has an empty context, occasionally there is 
an NPE.  If the judgment involves a lambda term, it generates bad output.

A SASyLF menu should only show up in the SASyLF perspective.
Instead, "Check Proofs" should be available in the context menu of a SLF file.

What steps will reproduce the problem?
1. Run in Eclipse workbench

What is the expected output? What do you see instead?

It doesn't work:

!ENTRY org.eclipse.osgi 2 0 2013-08-12 14:03:20.320
!MESSAGE One or more bundles are not resolved because the following root 
constraints are not resolved:
!SUBENTRY 1 org.eclipse.osgi 2 0 2013-08-12 14:03:20.320
!MESSAGE Bundle 
reference:file:/Applications/eclipse/plugins/org.eclipse.platform_4.2.2.v2013020
41200/ was not resolved.
!SUBENTRY 2 org.eclipse.platform 2 0 2013-08-12 14:03:20.320
!MESSAGE Missing required capability Require-Capability: osgi.ee; 
filter="(|(&(osgi.ee=JavaSE)(version=1.4))(&(osgi.ee=CDC/Foundation)(version=1.0
))(&(osgi.ee=JavaSE)(version=1.3)))".
...

If you do a case analysis on a term with variables, sasylf
doesn't require that the variable case be handled
(and up through current SVN, 1.0.2 (uwm 6), it doesn't have any way to
match a variable even if someone tried).

This means that it is possible to prove a contradiction without using any 
previously known holes.
The attached file is accepted by SASyLF (uwm 6) even though it purports to prove
a contradiction.  The same contradiction can be proved in SASyLF 1.0.2 before 
uwm changes,
but the last lemma is not accepted:

lemma no-problem:
   exists *, X, x:X |- unit = unit .
   _: *, X, x:X |- unit = unit by rule equal-unit
end lemma

This last lemma SHOULD be OK, but before SASyLF (uwm 6), the binding "x:X" 
confuses the checker.
As a result, the proof of lemma "problem" (the one that proves a contradiction) 
is convoluted in order to hide this binding.

Diagnosis:
There are several problems which must ALL be fixed to remove this unsoundness
1. syntax case analysis should require a variable case if the term is in a 
context
   (or simply forbid case analysis.)
2. a theorem should not be able to call a lemma or build a rule using a term 
bound in a context
unless that lemma or rule "assumes" the context.

The current file uses problem (2): lemma "lam-type-not-var" calls lemma 
"type-never-var"
with a term T from a context Gamma even though "type-never-var" doesn't have a 
context.

If (2) were fixed, we could "inline" the case analysis to exploit bug (1).

I am currently working on generalizing syntax case analysis to handle variables.
If and when I get this done, I should be able to fix these problems at the same 
time.

SASyLF provides no way to perform case analysis of variables.
Such case analysis is needed to produce recursive judgments for terms
if we don't have a recursive judgment on the same term already.

See attached for suggested syntax.

In order to solve POPLmark 1a, we need to be able to
do induction on multiple items: first one position, 
but if this stays the same, then a second term etc.

POPLmark 1a will also require the new context semantics,
so the motivation is not urgent.

Sometimes, when a nonterminal isn't an explicit argument, and gets
substituted by pattern matching, then a recent change (AFTER SASyLF 1.0.2)
causes SASyLF to fail to notice that it is in scope.

What's surprising is that this doesn't happen if the nonterminal was an argument
to the lemma, even if it was substituted away.  It even works when the 
nonterminal was a result of pattern matching another nonterminal.

Here is the error:
bug.slf:55 No derivation found for n2

This bug showed up when checking student code from before the change
that broke this (SASyLF 1.0.2 (uwm 11))
            // should use rule eq-z, but using lemma should be OK
            // 0 gets a syntax error, so student chose n2 instead
            // ("correct" solution is to parenthesize 0)
            _: 0 = 0 by lemma eq-reflexive on n2
This bug file is a radical simplification of what the student was doing.

What steps will reproduce the problem?
1. Use any unicode character that does not appear in ASCII in the syntax for a 
proof
2. "proof by solve"

What is the expected output? What do you see instead?
The output contains invalid UTF-8 sequences or question marks instead of 
certain characters, depending on which characters were used.

¬ becomes the byte AC (which is how it would be encoded in ISO-8859-1)
✓ becomes a question mark (3F)

What version of the product are you using? On what operating system?
Windows 8.1, Java 7u45, SASyLF r114

Please provide any additional information below.

One solution is to add

System.setOut(new PrintStream(System.out, true, "UTF-8"));
System.setErr(new PrintStream(System.err, true, "UTF-8"));

at the start of edu.cmu.cs.sasylf.Main.main.

The "Check Proofs" menu item doesn't seem to do anything.

Workaround: make a minor change and save.
Proofs are checked on save.

I would like to see SASyLF not give up so quickly after either syntax or 
semantic errors.
The latter is especially important for the Eclipse plugin

To have it handle syntax errors, we need to add lots of error productions to 
the grammar
for common errors.

To have it handle semantic errors, we need to make sure the context is 
correctly restored after recovering from problems.

AN and judgment incorrectly treats contexts as syntax.
The attached file should be accepted but instead gets the error (with --LF)


bug.slf:54 The claimed fact is not justified by applying theorem and2 to the 
argument
incorrectly instantiated an output variable Gamma_12 with a term (C_,_: [Gamma, 
T])
        while unifying (and2TERM [fn x:t => fn INTERNAL_DERIV_x:(type [BoundVar1, T]) => (type [(t [BoundVar2]), T']), fn x:t => fn INTERNAL_DERIV_x:(type [BoundVar1, T]) => (and-type-type [(t [BoundVar2]), T', (C_,_: [Gamma, T]), (t [BoundVar2]), T'])]) with rule term (and2TERM [fn x:t => fn INTERNAL_DERIV_x:(type [BoundVar1, T]) => (type [(t_13 [BoundVar2]), T'_10]), fn x:t => fn INTERNAL_DERIV_x:(type [BoundVar1, T]) => (and-type-type [(t_13 [BoundVar2]), T'_10, Gamma_12, (t_13 [BoundVar2]), T'_10])])
Error(s) in theorem and2a

At the LF level, Gamma should not occur.

If an error message takes more than one line, the Eclipse plugin loses is:

e.g.

arith.slf:66 Claimed fact n2 "+" n1' "=" n3'
    is not a consequence of applying rule induction hypothesis to the arguments

will lose the second line, even in the error view.

What steps will reproduce the problem?
1. Open a long SASyLF file
2. Scroll down halfway
3. Exit the plugin
4. Start up again

What is the expected output? What do you see instead?

Expected: that the scrollbar matches where the file has been scrolled to.
Instead: the file is at the same point as before the exit, but the
scrollbar is at the top of the window. 

Commenting an incorrect theorem declaration with single-line comments, e.g.,

  // theorem test:
  // end theorem.

apparently doesn't hide the code from the parser. Instead, an unexpected 
"Lexical error" is reported.

If two theorems are mutually inductive and one uses names inconsistently from 
the way the other does, we get an error, even though the names are in different 
scopes.

This happens in 1.2.3, and 1.2.4.

This comes from a student.

I don't want to post the example yet until I have a small test case.
Something of type fn x : (fn x:T => T) => T is applied to two arguments.
Not sure what's going on here.  More later when I get a small test case.

If a theorem has:
   forall t assumes Gamma
   forall n
then the first "assumes Gamma" spreads to the second one leading to nonsense.

(Actually the system should check that a non-terminal does not assume an 
irrelevant Gamma).

Eg:
$ echo "/*." > comment-defect.slf
$ java -jar SASyLF-1.2.5/SASyLF.jar comment-defect.slf 
comment-defect.slf: No errors reported.
Exception in thread "main" edu.cmu.cs.sasylf.parser.TokenMgrError: Lexical 
error at line 2, column 0.  Encountered: <EOF> after : ""
    at edu.cmu.cs.sasylf.parser.DSLToolkitParserTokenManager.getNextToken(DSLToolkitParserTokenManager.java:1989)
    at edu.cmu.cs.sasylf.parser.DSLToolkitParser.jj_ntk(DSLToolkitParser.java:2232)
    at edu.cmu.cs.sasylf.parser.DSLToolkitParser.CompilationUnit(DSLToolkitParser.java:194)
    at edu.cmu.cs.sasylf.parser.DSLToolkitParser.read(DSLToolkitParser.java:22)
    at edu.cmu.cs.sasylf.Main.main(Main.java:57)

Placing a comment on the line previous to a rule premise causes SASyLF to
fail in parsing the corresponding judgment:

judgment gt: n > n

// this is the bug
n1 > n2
--------- gt-more
s n1 > n2

Inserting a line between the comment and the premise or alternatively
removing the comment entirely is sufficient to avert the error.  The
attached file reproduces the problem.

$ sasylf --version
SASyLF version 0.21

What steps will reproduce the problem?
1. Set up a theorem with a forall argument that is a judgement.
2. proof by solve

What is the expected output? What do you see instead?
Each of the three theorems have their (commented out) output when solved by the 
proof solver followed by expected output when solved by a human. Only the 
human-produced output is valid when passed back through SASyLF.

What version of the product are you using? On what operating system?
Windows 8.1, Java 7u45, SASyLF r114