[guru-lang] r540 committed - -Changed the error messages related to ascriptions and lemmas so that ...
guru...@googlecode.com
Author: kevinclancy0
Date: Mon Sep 5 17:40:33 2011
Log: -Changed the error messages related to ascriptions and lemmas so
that they are more consistent with other guru errors.
-Terms can now be ascribed.
-Changed the lemma syntax into a derived form so that multiple lemma proofs
can be included in a single lemma syntax
(this way we don't have to deal with the obfuscating repetition of
the "lemma" and "in" keywords.
http://code.google.com/p/guru-lang/source/detail?r=540
Modified:
/branches/1.0/guru/Ascription.java
/branches/1.0/guru/Lemma.java
/branches/1.0/guru/LemmaMark.java
/branches/1.0/guru/Parser.java
=======================================
--- /branches/1.0/guru/Ascription.java Fri Aug 26 15:33:33 2011
+++ /branches/1.0/guru/Ascription.java Mon Sep 5 17:40:33 2011
@@ -61,7 +61,8 @@
handleError(ctxt,
"Ascription classifier does not match the computed classifer" +
" of the ascription target.\n" +
- "Computed Classifier: " + computed.toString(ctxt));
+ "1. ascription classifier: " + classifier.toString(ctxt) +
+ "\n2. computed classifier: " + computed.toString(ctxt));
return null;
}
@@ -94,8 +95,14 @@
return target.dropAnnos(ctxt);
}
+ // overridden from Expr
public void checkTermination(Context ctxt, Expr IH, int arg, Var[] vars)
{
target.checkTermination(ctxt, IH, arg, vars);
}
-}
+
+ // overridden from Expr
+ public void checkSpec(Context ctxt, boolean in_type, Position p){
+ target.checkSpec(ctxt, in_type, p);
+ }
+}
=======================================
--- /branches/1.0/guru/Lemma.java Fri Aug 26 15:30:54 2011
+++ /branches/1.0/guru/Lemma.java Mon Sep 5 17:40:33 2011
@@ -7,11 +7,10 @@
* and referenced later; such referencing is done by putting the lemma mark
* token, ##, in positions where proofs of the unnamed lemma are expected.
*
- * A lemma proof appears in source code as "lemma p0 in p1", where p0 and
- * p1 are proofs.
- *
- * Let F be the classifier of p0 under context C. If p1 has classifeir T
under
- * context C,F, then the lemma expression has classifier T under context C.
+ * A lemma abstract syntax node has the form "lemma p in b", where p and b
are
+ * proofs. Let F be the classifier of p under context C. If b has
classifeir T
+ * under context C,F, then the lemma expression has classifier T under
context
+ * C.
*
* As an example, suppose we have a proof div_le, which proves the
* formula "Forall(a b: nat)(u: { b != Z} ). { (le (div a b) a) = tt }".
@@ -31,6 +30,18 @@
* of formula { two != Z } is in the context that [div_le a two ##] is
classified
* under. Such a formula does exist in the context due to our use of the
lemma
* construct; hence, our proof is well classified.
+ *
+ * Lemma is implemented as a derived form. In source code, it appears as
+ * "lemma p+ in b", where p+ is a sequence of one or more proofs p1 ... pn
+ * and b is also a proof.
+ *
+ * An occurrence of "lemma p1 ... pn in b" elaborates to the following
syntax:
+ * lemma p1 in (lemma p2 in (... (lemma pn in b)...))
+ *
+ * This derived form allows us--with only one occurrence of the "lemma"
keyword
+ * and one occurrence of the "in" keyword--to establish a sequence of
unnamed
+ * lemmas, where the proof of each additional lemma can reference all of
the
+ * previously defined lemmas using lemma marks.
*/
public class Lemma extends Expr {
@@ -59,8 +70,8 @@
if (!formula.isFormula(ctxt))
{
handleError(ctxt,
- "Classifier for lemma is not a formula." +
- "Computed classifier: " + formula.toString(ctxt));
+ "Classifier for lemma is not a formula.\n" +
+ "1. computed classifier: " + formula.toString(ctxt));
return null;
}
@@ -68,7 +79,8 @@
if (ctxt.lemmaSet.hasLemma(formula))
{
handleError(ctxt,
- "Lemma formula already contained in context.");
+ "Lemma formula already contained in context.\n" +
+ "1. formula: " + formula.toString(ctxt));
return null;
}
=======================================
--- /branches/1.0/guru/LemmaMark.java Fri Aug 26 15:30:54 2011
+++ /branches/1.0/guru/LemmaMark.java Mon Sep 5 17:40:33 2011
@@ -39,7 +39,7 @@
//Overridden from Expr
protected void do_print(PrintStream w, Context ctxt) {
- w.print("lemma mark");
+ w.print("##");
}
//Overridden from Expr
@@ -49,7 +49,8 @@
if (formula == null)
{
handleError(pos,
- "Lemma mark used in a position that is not a proof argument.");
+ "Lemma mark used in an illegal position.\n" +
+ "Unascribed lemma marks can only be used as proof arguments.\n");
return null;
}
@@ -57,7 +58,8 @@
{
handleError(pos,
"Lemma mark used in a position whose expected classifier is" +
- " not a formula.\n");
+ " not a formula.\n" +
+ "1. expected classifier: " + formula.toString(ctxt));
return null;
}
@@ -65,7 +67,7 @@
{
handleError(pos,
"Lemma mark used without the expected lemma in context.\n"
- +"Missing lemma: " + formula.toString(ctxt));
+ +"1. expected lemma: " + formula.toString(ctxt));
return null;
}
=======================================
--- /branches/1.0/guru/Parser.java Fri Aug 26 15:30:54 2011
+++ /branches/1.0/guru/Parser.java Mon Sep 5 17:40:33 2011
@@ -1880,17 +1880,26 @@
Position pos = getPos();
if (!eat_ws())
- handleError("Unexpected end of input parsing a abbrev term.");
-
- Expr lemma = readProof();
-
- eat("in", "lemma term");
-
- Expr body = readProof();
-
- Lemma ret = new Lemma(lemma, body);
- ret.pos = pos;
- return ret;
+ handleError("Unexpected end of input parsing a lemma term.");
+
+ Expr lemmaProof = readProof();
+
+ eat_ws();
+
+ if (tryToEat("in", true))
+ {
+ Expr body = readProof();
+ Lemma ret = new Lemma(lemmaProof, body);
+ ret.pos = pos;
+ return ret;
+ }
+ else
+ {
+ Expr body = readLemma();
+ Lemma ret = new Lemma(lemmaProof, body);
+ ret.pos = pos;
+ return ret;
+ }
}
protected LemmaMark readLemmaMark()