[guru-lang] r538 committed - Rewrote some comments to use guru terminology properly. Added ascripti...
guru...@googlecode.com
Author: kevinclancy0
Date: Fri Aug 26 15:30:54 2011
Log: Rewrote some comments to use guru terminology properly. Added
ascriptions to guru. Lemma marks can now appear anywhere as long as they're
ascribed.
http://code.google.com/p/guru-lang/source/detail?r=538
Added:
/branches/1.0/guru/Ascription.java
Modified:
/branches/1.0/guru/Expr.java
/branches/1.0/guru/Lemma.java
/branches/1.0/guru/LemmaMark.java
/branches/1.0/guru/Parser.java
=======================================
--- /dev/null
+++ /branches/1.0/guru/Ascription.java Fri Aug 26 15:30:54 2011
@@ -0,0 +1,101 @@
+package guru;
+
+import java.io.PrintStream;
+
+/*
+ * Ascriptions appear in source as ": C e", where C is a classifier and
+ * e is an expression. ": C e" is classified as C under context G iff
+ * e is classified as C under G. If e is not classified as C under
+ * context G, then ": C e" is not well classified under G.
+ *
+ * An ascription allows the writer of guru code to display the classifier
of
+ * a certain expression in source code; this provides the reader of said
code
+ * a convenient summary of the ascribed expression.
+ *
+ * For example, in a transitivity proof, you could ascribe each of the
atoms
+ * involved. This allows the reader (or writer) of the proof to consider
+ * (or state) the chain of transitivity before examining why each atom
+ * in the chain holds. In general, ascriptions allow guru programmers to
+ * write proofs in a more top-down manner, separating the basic outline
+ * of the proof from the details.
+ *
+ * An ascription can also be used to refer to a subproof by formula rather
than
+ * a programmer-given name. Instead of creating an abbreviation for a
subproof,
+ * one could insert the subproof into the context using the lemma
construct.
+ * The subproof could then be referred to inside the lemma body using an
+ * ascripted lemma mark.
+ */
+public class Ascription extends Expr {
+
+ // The classifier being ascribed to the target.
+ final Expr classifier;
+
+ // The target of the ascription.
+ final Expr target;
+
+ public Ascription(Expr classifier, Expr target)
+ {
+ super(ASCRIPTION);
+
+ assert(target != null);
+ assert(classifier != null);
+ assert(isFormula(classifier.construct) ||
isTypeOrKind(classifier.construct));
+
+ this.target = target;
+ this.classifier = classifier;
+ }
+
+ // overridden from Expr
+ public Expr classify(Context ctxt)
+ {
+ if (target.construct == LEMMA_MARK)
+ {
+ LemmaMark lm = (LemmaMark)target;
+ lm.formula = classifier;
+ }
+
+ Expr computed = target.classify(ctxt);
+
+ if (!computed.defEq(ctxt,classifier))
+ {
+ handleError(ctxt,
+ "Ascription classifier does not match the computed classifer" +
+ " of the ascription target.\n" +
+ "Computed Classifier: " + computed.toString(ctxt));
+
+ return null;
+ }
+
+ return classifier;
+ }
+
+ // overridden from Expr
+ protected void do_print(PrintStream w, Context ctxt) {
+ w.print(": ");
+ classifier.do_print(w,ctxt);
+ w.print(" ");
+ target.do_print(w,ctxt);
+ }
+
+ // overridden from Expr
+ public int numOcc(Expr e) {
+
+ return target.numOcc(e) + classifier.numOcc(e);
+ }
+
+ // overridden from Expr
+ public Expr subst(Expr e, Expr x) {
+
+ return new Ascription(target.subst(e,x), classifier.subst(e,x));
+ }
+
+ // overridden from Expr
+ public Expr dropAnnos(Context ctxt) {
+ return target.dropAnnos(ctxt);
+ }
+
+ public void checkTermination(Context ctxt, Expr IH, int arg, Var[] vars)
+ {
+ target.checkTermination(ctxt, IH, arg, vars);
+ }
+}
=======================================
--- /branches/1.0/guru/Expr.java Mon Aug 22 15:38:29 2011
+++ /branches/1.0/guru/Expr.java Fri Aug 26 15:30:54 2011
@@ -106,6 +106,7 @@
public static final int COMPILE_AS = 90; // term
public static final int LEMMA_MARK = 91;
+ public static final int ASCRIPTION = 92;
public static final int LAST = 200;
@@ -493,6 +494,7 @@
public static boolean isProof(int construct) {
switch (construct) {
+ case ASCRIPTION:
case VAR:
case BANG:
case CONST:
@@ -535,6 +537,7 @@
public static boolean isTerm(int construct) {
switch (construct) {
+ case ASCRIPTION:
case VAR:
case CONST:
case VOIDI:
@@ -581,6 +584,8 @@
Expr tmp = defExpandTop(ctxt);
if (tmp.construct == VAR)
return ctxt.getClassifier((Var) tmp).isTypeOrKind(ctxt);
+ if (tmp.construct == ASCRIPTION)
+ return ((Ascription)tmp).target.isTerm(ctxt);
if (tmp.construct == CONST)
return ctxt.isTermCtor((Const) tmp);
@@ -608,6 +613,8 @@
Expr tmp = defExpandTop(ctxt);
if (tmp.construct == VAR)
return ctxt.isAssumption((Var) tmp);
+ if (tmp.construct == ASCRIPTION)
+ return ((Ascription)tmp).target.isProof(ctxt);
if (tmp.construct == CONST)
return false;
=======================================
--- /branches/1.0/guru/Lemma.java Mon Aug 22 16:01:56 2011
+++ /branches/1.0/guru/Lemma.java Fri Aug 26 15:30:54 2011
@@ -5,13 +5,13 @@
/*
* A proof construct which allows allows an unnamed lemma to be proven
* and referenced later; such referencing is done by putting the lemma mark
- * token, ##, in positions where proofs of the unnamed lemma is expected.
+ * 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 type of p0 under context C. If p1 has type T under context
- * C,F, then the lemma term has type T under context C.
+ * 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.
*
* 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 }".
@@ -28,9 +28,9 @@
* In the above code, div_le is instantiated using ## as its third
argument.
* Since div_le expects a proof of the formula "{ two != Z }" in that
position,
* [div_le a two ##] will only be considered well typed if an unnamed proof
- * of formula { two != Z } is in the context that [div_le a two ##] is
typechecked
+ * 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 typed.
+ * construct; hence, our proof is well classified.
*/
public class Lemma extends Expr {
=======================================
--- /branches/1.0/guru/LemmaMark.java Mon Aug 22 15:38:29 2011
+++ /branches/1.0/guru/LemmaMark.java Fri Aug 26 15:30:54 2011
@@ -2,22 +2,34 @@
import java.io.PrintStream;
-/* A syntactic construct which can be used in proof argument positions in
order
- * to reference proofs of formulas which have been established earlier
using
- * the lemma construct (see Lemma.java).
+/* A construct, appearing in source as "##", which can be used to reference
+ * proofs of unnamed formulas that are contained in the current context's
+ * lemma set. (See LemmaSet.java.)
*
- * When an application is typechecked, an occurrence of ## in an argument
- * position will be considered well-typed iff the formal parameter for that
- * position is a proof of some formula that is currently in the context as
- * an unnamed lemma.
+ * Before ## is classified, it inherits an expected formula from its parent
+ * in the syntax tree. This is only possible if the lemma mark's parent
+ * determines the classifier of the expression which must appear in the
position
+ * that the lemma mark occupies; this is the case when the mark's parent
expression
+ * is either an ascription or an application.
*
- * Occurrences of ## outside of applications are illegal.
+ * For example, in the expression
+ * ": { (S (S n')) != Z } ##"
+ * the lemma mark inherits the classifer { (S (S n')) != Z } from its
+ * parent node, which is an ascription.
+ *
+ * In the expression
+ * "[lt_implies_le b' a' ##]"
+ * the lemma mark inherits a classifier from the application.
+ *
+ * If the lemma mark's inherited classifer is a formula contained in the
classifying
+ * context's lemma set, the lemma mark's classifier is its inherited
classifier.
+ * Otherwise, the lemma mark is not considered well typed.
*/
public class LemmaMark extends Expr {
- // The formula type that this lemma mark must have in order to typecheck,
- // inherited from the application that this lemma mark occurs as an
argument
- // in.
+ // The formula type that this lemma mark must have in order to classify,
+ // inherited from the expression that this lemma mark is a direct
subexpression
+ // of.
public Expr formula;
public LemmaMark()
=======================================
--- /branches/1.0/guru/Parser.java Mon Aug 22 15:38:29 2011
+++ /branches/1.0/guru/Parser.java Fri Aug 26 15:30:54 2011
@@ -128,6 +128,9 @@
Position pos = getPos();
switch(construct)
{
+ case Expr.ASCRIPTION:
+ e = readAscription();
+ break;
case Expr.VAR:
e = readIdentifier(false);
break;
@@ -1936,6 +1939,13 @@
return (Var)readIdentifier(true);
}
+ protected Expr readAscription() throws IOException
+ {
+ Expr classifier = readA();
+ Expr target = readArg();
+ return new Ascription(classifier, target);
+ }
+
protected Expr readIdentifier(boolean binding_occurrence)
throws IOException
{
@@ -2723,6 +2733,7 @@
static {
keywordTree = new DiscriminationTree();
+ keywordTree.add( ":", Expr.ASCRIPTION);
keywordTree.add( "**", Expr.STARSTAR );
keywordTree.add( "*", Expr.STAR );
keywordTree.add( "do", Expr.DO );