[guru-lang] r535 committed - Added a new proof construct called lemma. I plan to post a detailed de...
guru...@googlecode.com
Author: kevinclancy0
Date: Mon Aug 22 15:38:29 2011
Log: Added a new proof construct called lemma. I plan to post a
detailed description of this, as well as plans for a couple of other
features, to guru gang within the next few days. Until then, the comments
in Lemma.java should be sufficient. Please post any questions or comments
to guru gang, or send them to me.
http://code.google.com/p/guru-lang/source/detail?r=535
Added:
/branches/1.0/guru/Lemma.java
/branches/1.0/guru/LemmaMark.java
/branches/1.0/guru/LemmaSet.java
Modified:
/branches/1.0/guru/Abbrev.java
/branches/1.0/guru/App.java
/branches/1.0/guru/Context.java
/branches/1.0/guru/Expr.java
/branches/1.0/guru/Parser.java
=======================================
--- /dev/null
+++ /branches/1.0/guru/Lemma.java Mon Aug 22 15:38:29 2011
@@ -0,0 +1,125 @@
+package guru;
+
+import java.io.PrintStream;
+
+/*
+ * 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.
+ *
+ * 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 P. If p1 has type T under context
+ * C,F, then the lemma term has type 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 }".
+ * We could write a proof that "Forall(a: nat). { (le (div a two) a) = tt
}"
+ * using the following code:
+ *
+ * Define div2_le : Forall(a: nat). { (le (div2 a) a) = tt } :=
+ * foralli(a:nat).
+ * lemma
+ * clash two Z
+ * in
+ * [div_le a two ##].
+ *
+ * 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
+ * under. Such a formula does exist in the context due to our use of the
lemma
+ * construct; hence, our proof is well typed.
+*/
+public class Lemma extends Expr {
+
+ // Proof of an unnamed lemma, to be referenced via formula.
+ final private Expr lemmaProof;
+
+ // A proof which may include implicit references to the unnamed lemma.
+ final private Expr body;
+
+ public Lemma(Expr lemma, Expr body) {
+ super(LEMMA);
+
+ assert(lemma != null);
+ assert(body != null);
+
+ this.lemmaProof = lemma;
+ this.body = body;
+ }
+
+ //Override form Expr
+ public Expr classify(Context ctxt) {
+ assert(ctxt != null);
+
+ Expr formula = lemmaProof.classify(ctxt);
+
+ if (!formula.isFormula(ctxt))
+ {
+ handleError(ctxt,
+ "Classifier for lemma is not a formula." +
+ "Computed classifier: " + formula.toString(ctxt));
+
+ return null;
+ }
+
+ if (ctxt.lemmaSet.hasLemma(formula))
+ {
+ handleError(ctxt,
+ "Lemma formula already contained in context.");
+
+ return null;
+ }
+
+ ctxt.lemmaSet.addLemma(formula);
+
+ Expr bodyClassifier = body.classify(ctxt);
+
+ ctxt.lemmaSet.removeLemma(formula);
+
+ return bodyClassifier;
+ }
+
+ //Override form Expr
+ protected void do_print(PrintStream w, Context ctxt) {
+ w.print("lemma ");
+ lemmaProof.print(w, ctxt);
+ //body.print(w,ctxt.addTermCtor(c, d, type))
+ }
+
+ //Override from Expr
+ public int numOcc(Expr e) {
+ //Lemmas are specificational; hence, this will not get called.
+ assert(false);
+ return 0;
+ }
+
+ //Override from Expr
+ public Expr subst(Expr e, Expr x) {
+ //Lemmas are specificational; hence, this will not get called.
+ assert(false);
+ return null;
+ }
+
+ public Expr dropAnnos(Context ctxt) {
+ return body.dropAnnos(ctxt);
+ }
+
+ // overridden from Expr.
+ //
+ // A lemma construct is considered to terminate if the lemmaProof
+ // and the body both terminate.
+ //
+ // The lemmaProof is required to terminate because we assume that
+ // this lemma is referenced by at least one lemma mark inside
+ // the body--an unreferenced lemma is pointless. Rather than
+ // redundantly checking the termination of each lemmaMark, we
+ // handle that task only once in a call to this method.
+ public void checkTermination(Context ctxt, Expr IH, int arg, Var[] vars)
+ {
+ lemmaProof.checkTermination(ctxt, IH, arg, vars);
+ body.checkTermination(ctxt, IH, arg, vars);
+ }
+}
=======================================
--- /dev/null
+++ /branches/1.0/guru/LemmaMark.java Mon Aug 22 15:38:29 2011
@@ -0,0 +1,92 @@
+package guru;
+
+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).
+ *
+ * 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.
+ *
+ * Occurrences of ## outside of applications are illegal.
+*/
+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.
+ public Expr formula;
+
+ public LemmaMark()
+ {
+ super(LEMMA_MARK);
+ }
+
+ //Overridden from Expr
+ protected void do_print(PrintStream w, Context ctxt) {
+ w.print("lemma mark");
+ }
+
+ //Overridden from Expr
+ public Expr classify(Context ctxt) {
+ assert(ctxt != null);
+
+ if (formula == null)
+ {
+ handleError(pos,
+ "Lemma mark used in a position that is not a proof argument.");
+
+ return null;
+ }
+ else if (!formula.isFormula(ctxt))
+ {
+ handleError(pos,
+ "Lemma mark used in a position whose expected classifier is" +
+ " not a formula.\n");
+
+ return null;
+ }
+ else if (!ctxt.lemmaSet.hasLemma(formula))
+ {
+ handleError(pos,
+ "Lemma mark used without the expected lemma in context.\n"
+ +"Missing lemma: " + formula.toString(ctxt));
+
+ return null;
+ }
+ else
+ {
+ return formula;
+ }
+ }
+
+ //Overridden from Expr
+ public int numOcc(Expr e) {
+ return (this == e) ? 1 : 0;
+ }
+
+ //Overridden from Expr
+ public Expr subst(Expr e, Expr x) {
+ return (this == x) ? e : this;
+ }
+
+ public Expr dropAnnos(Context ctxt) {
+ //Lemma marks are specificational, so this shouldn't get called
+ //Specificational constructs shouldn't have to implement this,
+ //and they shouldn't have to implement the above two methods either.
+ assert(false);
+ return null;
+ }
+
+ // Overridden from Expr.
+ //
+ // It is assumed that the termination of the lemma proof has already been
+ // checked for in lemma.checkTermination; this means that we don't have
to
+ // do anything in this method.
+ public void checkTermination(Context ctxt, Expr IH, int arg, Var[] vars)
+ {
+ }
+}
=======================================
--- /dev/null
+++ /branches/1.0/guru/LemmaSet.java Mon Aug 22 15:38:29 2011
@@ -0,0 +1,70 @@
+package guru;
+
+import java.util.ArrayList;
+import java.util.ListIterator;
+
+/*
+ * A set of all unnamed formulas which have been established in the current
+ * context. Unnamed formulas can be used as premises for proof
instantiation
+ * by using the ## token. They are introduced to the context using the
lemma
+ * construct (see Lemma.java).
+ *
+ * NOTE: The java API's set classes are not suitable for defining a lemma
set
+ * due to their usage of the equals method to determine uniqueness. The
equals
+ * method is not parameterized by context whereas our notion of
definitional equality is.
+*/
+public class LemmaSet {
+
+ // The context used to decide definitional equality
+ final private Context ctxt;
+
+ // A set of definitionally unique formulas currently contained in this
lemma set.
+ final private ArrayList formulas;
+
+ public LemmaSet(Context ctxt)
+ {
+ assert(ctxt != null);
+
+ this.ctxt = ctxt;
+ this.formulas = new ArrayList();
+ }
+
+ // Adds a lemma to the set. This lemma must be definitionally unequal
+ // to each lemma currently in the set. (Use the HasLemma method to
+ // determine whether or not an equivalent lemma is already in the set.)
+ public void addLemma(Expr newLemma)
+ {
+ assert(newLemma != null);
+ assert(newLemma.isFormula(ctxt));
+ assert(!hasLemma(newLemma));
+
+ formulas.add(newLemma);
+ }
+
+ // Removes a lemma from the set.
+ public void removeLemma(Expr toRemove)
+ {
+ assert(toRemove != null);
+ assert(toRemove.isFormula(ctxt));
+ assert(hasLemma(toRemove));
+
+ formulas.remove(toRemove);
+ }
+
+ // Returns true iff the given lemma is contained in this set.
+ public boolean hasLemma(Expr lemma)
+ {
+ assert(lemma.isFormula(ctxt));
+ assert(lemma != null);
+
+ ListIterator i = formulas.listIterator();
+ while(i.hasNext())
+ {
+ Expr curr = (Expr)i.next();
+
+ if (curr.defEq(ctxt, lemma))
+ return true;
+ }
+ return false;
+ }
+}
=======================================
--- /branches/1.0/guru/Abbrev.java Wed May 4 13:38:32 2011
+++ /branches/1.0/guru/Abbrev.java Mon Aug 22 15:38:29 2011
@@ -9,10 +9,15 @@
static final int fAbbrevClassify = 0x2;
int flags;
+ // The name of the abbreviation.
public Var x;
+ // The expression that the abbreviation has been defined as.
public Expr U;
+ // The scope of the abbreviation i.e. the expression in which
+ // the abbreviation may be used.
public Expr G;
- protected Expr subst; // cache for substituted version of G
+ // cache for substituted version of G
+ protected Expr subst;
public Abbrev(int f, Var x, Expr U, Expr G) {
super(ABBREV);
=======================================
--- /branches/1.0/guru/App.java Fri Oct 29 19:48:32 2010
+++ /branches/1.0/guru/App.java Mon Aug 22 15:38:29 2011
@@ -130,7 +130,7 @@
}
cl = cl.defExpandTop(ctxt, false, spec);
- Expr err_tgt = ((X[arg].construct == VAR || X[arg].construct == CONST)
+ Expr err_tgt = ((X[arg].construct == VAR || X[arg].construct == CONST ||
X[arg].construct == LEMMA_MARK)
? this : X[arg]);
if (cl.construct != expected_construct)
err_tgt.handleError
@@ -145,7 +145,7 @@
// if we are doing approximate checking and the argument is a proof
// (including !, which could also be for a dropped type), then
// we do not type check that argument.
-
+
if (approx == NO_APPROX || (!isTypeOrKind(ctxt)
&& !X[arg].isProof(ctxt)
&& X[arg].construct != BANG)) {
@@ -164,6 +164,11 @@
ctxt.w.flush();
}
+ if (X[arg].construct == LEMMA_MARK)
+ {
+ LemmaMark lm = (LemmaMark)X[arg];
+ lm.formula = e.types[0];
+ }
Expr xc = apply_classifier_classify_arg(ctxt,arg,X[arg], approx,
spec);
if (ctxt.getFlag("debug_classify_apps")) {
@@ -172,7 +177,7 @@
+"\n2. "+xc.toString(ctxt));
ctxt.w.flush();
}
-
+
if (!apply_classifier_types_defeq(ctxt, arg, e.types[0], xc, approx,
spec))
err_tgt.handleError
(ctxt,
=======================================
--- /branches/1.0/guru/Context.java Wed May 4 13:38:32 2011
+++ /branches/1.0/guru/Context.java Mon Aug 22 15:38:29 2011
@@ -37,6 +37,10 @@
protected HashMap drop_func_defs;
protected HashMap deps_to_name;
+ // The set of all unnamed lemmas established
+ // in the current context using the lemma construct
+ final public LemmaSet lemmaSet;
+
public Vector initCmds;
public guru.carraway.Context carraway_ctxt;
@@ -83,6 +87,8 @@
drop_func_defs = new HashMap(256);
deps_to_name = new HashMap(1024);
+ lemmaSet = new LemmaSet(this);
+
star = new Star();
starstar = new StarStar();
type = new Type();
=======================================
--- /branches/1.0/guru/Expr.java Sun Aug 7 05:34:30 2011
+++ /branches/1.0/guru/Expr.java Mon Aug 22 15:38:29 2011
@@ -4,785 +4,788 @@
import java.io.*;
public abstract class Expr {
-
- public static final int INVALID = 0; // never a "construct" of an
expr
- public static final int VAR = 1;
- public static final int CONST = 2;
- public static final int METAVAR = 3; // not supported right now
- public static final int STAR = 4; // a hole for contexts
- public static final int STARSTAR = 5; // another hole for contexts
- public static final int ABSTRACTION = 6; /* when the type is
- actually Abstraction (not
- a subclass) */
- public static final int BANG = 7;
-
- // terms
- // public static final int INC = 9;
- // public static final int DEC = 10;
-
- public static final int FUN_TERM = 11;
-
- public static final int CAST = 12;
- public static final int TERM_APP = 13;
- public static final int ABORT = 14;
- public static final int LET = 15;
- public static final int MATCH = 16;
- public static final int CASE = 17; // only found in match-terms
- public static final int APP = 18; // for some intermediate App
instances
- public static final int CUTOFF = 19;
-
- // types, type families, kinds, and the sole superkind
- public static final int FUN_TYPE = 20;
- public static final int TYPE_APP = 21;
- public static final int TYPE = 22;
- public static final int FORMULA = 23;
- public static final int TKIND = 24; // for kinds of types and type
fams.
- public static final int FKIND = 25; // for kinds of formulas and
predicates
-
- // proofs
- public static final int FORALLI = 30;
- public static final int PROOF_APP = 31;
- public static final int EXISTSI = 32;
- public static final int EXISTSE = 33;
-
- public static final int JOIN = 35;
- public static final int REFL = 36;
- public static final int SYMM = 37;
- public static final int TRANS = 38;
- public static final int CONG = 39;
- public static final int NCONG = 40;
- public static final int INJ = 41;
- public static final int CLASH = 42;
- public static final int ACLASH = 43;
- public static final int INV = 44;
- public static final int SUBST = 45;
- public static final int CONTRA = 46;
- public static final int INDUCTION = 47;
- public static final int HYPJOIN = 48;
- public static final int CIND = 49;
-
- // formulas
- public static final int FORALL = 50;
- public static final int EXISTS = 51;
- public static final int ATOM = 52;
-
- public static final int ABBREV = 53;
- public static final int EABBREV = 54;
- public static final int CABBREV = 56; // Duckki: abbrev with
classification
-
- public static final int TRUE = 55;
-
- // some extra items:
-
-
- public static final int TRUEI = 57;
- public static final int CASE_PROOF = 58; //proof
- public static final int EVAL = 59;//proof
- public static final int SHOW = 60; // proof
- public static final int ANDI = 61; // proof, like existsi
- public static final int EVALTO = 62; // proof
- public static final int DISEQI = 63; // proof
-
- public static final int TERMINATES = 70;//term
- public static final int IMPOSSIBLE = 71; //term
- public static final int STRING_EXPR = 73; //term
- public static final int EXISTSE_TERM = 74; // term
- public static final int SIZE = 75; // term
-
- public static final int PRED_APP = 80; //formula
- public static final int FALSE = 81; // formula
-
- public static final int VOID = 82; // type
- public static final int VOIDI = 83; // term
- public static final int DO = 84; // term
- public static final int TRANSS = 85; //proof
- public static final int COMPRESS = 86; // term
-
- public static final int CHAR_EXPR = 87; // term
- public static final int WORD_EXPR = 88; // term
- public static final int TERM_CASE = 89; // proof
-
- public static final int COMPILE_AS = 90; // term
-
- public static final int LAST = 200;
-
- public int construct;
- boolean result; /* true iff we reached this Expr as the result
- of (partial) evaluation */
- public Position pos;
-
- public Expr(int construct) {
- this.construct = construct;
- this.result = false;
- this.pos = null;
- }
-
- // subclasses for each construct must override to define printing
- // for that construct.
- abstract protected void do_print(java.io.PrintStream w, Context ctxt);
-
- final public void print(java.io.PrintStream w, Context ctxt) {
- // we used to handle a special case here, but no longer.
- do_print(w,ctxt);
- }
-
- protected void print_pos_comment_short(java.io.PrintStream w) {
- if (pos != null) {
- w.print("(* ");
- w.print(new Integer(pos.linenum).toString());
- w.print(" *)");
- }
- }
-
- protected void print_pos_comment_long(java.io.PrintStream w) {
- if (pos != null) {
- w.print("(* ");
- pos.print(w);
- w.print(" *)");
- }
- }
-
- public String debug(Context ctxt) {
- java.io.ByteArrayOutputStream s = new java.io.ByteArrayOutputStream();
- java.io.PrintStream w = new java.io.PrintStream(s);
- defExpandTop(ctxt).do_print(w,ctxt);
- return s.toString();
- }
-
- public String toString(Context ctxt) {
- java.io.ByteArrayOutputStream s = new java.io.ByteArrayOutputStream();
- java.io.PrintStream w = new java.io.PrintStream(s);
- print(w,ctxt);
- return s.toString();
- }
-
- // intended only for unannotated terms -- others may fail.
- public final int hashCode(Context ctxt) {
- ctxt.next_var_hash_code = 0;
- return hashCode_h(ctxt);
- }
-
- public int hashCode_h(Context ctxt) {
- handleError(ctxt,"Internal error: hashCode() function not implemented for"
- +" construct "+(new Integer(construct)).toString()+".");
- return 0;
- }
-
- // count free occurrences of e.
- abstract public int numOcc(Expr e);
-
- public boolean isApp() { // overridden by App
- return false;
- }
-
- // substitute e for x in this Expr. We only support substituting
- // for Vars x and Holes x.
- abstract public Expr subst(Expr e, Expr x);
-
- // return the Const with name s in the ctxt, or return an error.
- protected Const _const(Context ctxt, String s) {
- Expr c = ctxt.lookup(s);
- if (c == null || c.construct != Expr.CONST)
- handleError(ctxt,"Cannot find special constant "+s+".");
- return (Const)c;
- }
-
- public boolean containsVars(Stack boundVars)
- {
- boolean returnValue = false;
-
- Enumeration varsEnum = boundVars.elements();
- while(varsEnum.hasMoreElements())
- {
- Var currentVar = (Var)varsEnum.nextElement();
- if(numOcc(currentVar) > 0 )
- {
- returnValue = true;
- }
- }
-
- return returnValue;
- }
-
- // substitute e for x in this Expr. x may be an arbitrary ground
- // term, and any sub term of this which is definitionally equal
- // to x will be replaced with e.
- final public Expr rewrite(Context ctxt, Expr e, Expr x, Stack
boundVars)
- {
- if(defEq(ctxt, x, NO_APPROX, true) &&
- !x.containsVars(boundVars) &&
- !e.containsVars(boundVars))
- {
- return e;
- }
- else
- {
- ctxt.resetNotDefEq();
- return do_rewrite(ctxt, e, x, boundVars);
- }
- }
-
- public Expr do_rewrite(Context ctxt, Expr e, Expr x, Stack boundVars)
- {
- handleError(ctxt, "Internal error: do_rewrite called on an
inappropriate expression in: "+this.getClass().toString());
- //throw new RuntimeException("Internal error: do_rewrite called on an
inappropriate expression in: "+this.getClass().toString());
- return this;
- }
-
- public Expr classify(Context ctxt, int approx, boolean spec) {
- if (approx > NO_APPROX) {
- System.out.println("Approximate classification for this construct "
- +"unimplemented: "
- +(new Integer(construct)));
- System.exit(5);
- }
- return classify(ctxt);
- }
-
- /* subclasses should override one or the other classify method, or
expect
- a stack overflow. We will treat this as specificational (use the
- other classify() method to specify non-specificational). */
- public Expr classify(Context ctxt) {
- return classify(ctxt,NO_APPROX,true);
- }
-
- // is e definitionally equal to this expr in the given ctxt.
- protected boolean defEqNoAnno(Context ctxt, Expr e, boolean spec) {
- System.out.println("Definitional equality for this construct"
- +" unimplemented: "+(new Integer(construct)));
- System.exit(5);
- return false;
- }
-
- protected boolean defEqNoAnnoApprox(Context ctxt, Expr e,
- boolean spec) {
- System.out.println("Approximate definitional equality for this"
- +" construct unimplemented: "
- +(new Integer(construct)));
- System.exit(5);
- return false;
- }
-
- final public boolean defEq(Context ctxt, Expr e, boolean spec) {
- return defEq(ctxt,e,NO_APPROX,spec);
- }
-
- // specificational by default
- final public boolean defEq(Context ctxt, Expr e) {
- return defEq(ctxt,e,NO_APPROX,true);
- }
-
- /* approx level 2 means all types are considered equal; 1 means we
- drop indices; 0 means drop annotations from terms (no
- approximation). */
- public static final int NO_APPROX = 0;
- public static final int APPROX_NO_INDICES = 1;
- public static final int APPROX_TRIVIAL = 2;
-
- final public boolean defEq(Context ctxt, Expr e, int approx,
- boolean spec) {
- if (approx == 2)
- return true;
-
- if (ctxt.getFlag("debug_def_eq")) {
- ctxt.w.println("--------------------------------------------------");
- ctxt.w.println("Testing definitional equality (spec = "
- +(spec ? "true":"false")+") of:");
- ctxt.w.print("1. ");
- print(ctxt.w,ctxt);
- ctxt.w.print("\n2. ");
- e.print(ctxt.w,ctxt);
- ctxt.w.println("");
- ctxt.w.flush();
+
+ public static final int INVALID = 0; // never a "construct" of an expr
+ public static final int VAR = 1;
+ public static final int CONST = 2;
+ public static final int METAVAR = 3; // not supported right now
+ public static final int STAR = 4; // a hole for contexts
+ public static final int STARSTAR = 5; // another hole for contexts
+ public static final int ABSTRACTION = 6; /*
+ * when the type is actually
+ * Abstraction (not a subclass)
+ */
+ public static final int BANG = 7;
+
+ // terms
+ // public static final int INC = 9;
+ // public static final int DEC = 10;
+
+ public static final int FUN_TERM = 11;
+
+ public static final int CAST = 12;
+ public static final int TERM_APP = 13;
+ public static final int ABORT = 14;
+ public static final int LET = 15;
+ public static final int MATCH = 16;
+ public static final int CASE = 17; // only found in match-terms
+ public static final int APP = 18; // for some intermediate App instances
+ public static final int CUTOFF = 19;
+
+ // types, type families, kinds, and the sole superkind
+ public static final int FUN_TYPE = 20;
+ public static final int TYPE_APP = 21;
+ public static final int TYPE = 22;
+ public static final int FORMULA = 23;
+ public static final int TKIND = 24; // for kinds of types and type fams.
+ public static final int FKIND = 25; // for kinds of formulas and
predicates
+
+ // proofs
+ public static final int FORALLI = 30;
+ public static final int PROOF_APP = 31;
+ public static final int EXISTSI = 32;
+ public static final int EXISTSE = 33;
+
+ public static final int JOIN = 35;
+ public static final int REFL = 36;
+ public static final int SYMM = 37;
+ public static final int TRANS = 38;
+ public static final int CONG = 39;
+ public static final int NCONG = 40;
+ public static final int INJ = 41;
+ public static final int CLASH = 42;
+ public static final int ACLASH = 43;
+ public static final int INV = 44;
+ public static final int SUBST = 45;
+ public static final int CONTRA = 46;
+ public static final int INDUCTION = 47;
+ public static final int HYPJOIN = 48;
+ public static final int CIND = 49;
+ public static final int LEMMA = 50;
+
+ // formulas
+ public static final int FORALL = 51;
+ public static final int EXISTS = 52;
+ public static final int ATOM = 53;
+
+ public static final int ABBREV = 54;
+ public static final int EABBREV = 55;
+ public static final int CABBREV = 56; // Duckki: abbrev with
classification
+
+ public static final int TRUE = 57;
+
+ // some extra items:
+
+ public static final int TRUEI = 58;
+ public static final int CASE_PROOF = 59; // proof
+ public static final int EVAL = 60;// proof
+ public static final int SHOW = 61; // proof
+ public static final int ANDI = 62; // proof, like existsi
+ public static final int EVALTO = 63; // proof
+ public static final int DISEQI = 64; // proof
+
+ public static final int TERMINATES = 70;// term
+ public static final int IMPOSSIBLE = 71; // term
+ public static final int STRING_EXPR = 73; // term
+ public static final int EXISTSE_TERM = 74; // term
+ public static final int SIZE = 75; // term
+
+ public static final int PRED_APP = 80; // formula
+ public static final int FALSE = 81; // formula
+
+ public static final int VOID = 82; // type
+ public static final int VOIDI = 83; // term
+ public static final int DO = 84; // term
+ public static final int TRANSS = 85; // proof
+ public static final int COMPRESS = 86; // term
+
+ public static final int CHAR_EXPR = 87; // term
+ public static final int WORD_EXPR = 88; // term
+ public static final int TERM_CASE = 89; // proof
+
+ public static final int COMPILE_AS = 90; // term
+
+ public static final int LEMMA_MARK = 91;
+
+ public static final int LAST = 200;
+
+ public int construct;
+ boolean result; /*
+ * true iff we reached this Expr as the result of (partial)
+ * evaluation
+ */
+ public Position pos;
+
+ public Expr(int construct) {
+ this.construct = construct;
+ this.result = false;
+ this.pos = null;
+ }
+
+ // subclasses for each construct must override to define printing
+ // for that construct.
+ abstract protected void do_print(java.io.PrintStream w, Context ctxt);
+
+ final public void print(java.io.PrintStream w, Context ctxt) {
+ // we used to handle a special case here, but no longer.
+ do_print(w, ctxt);
+ }
+
+ protected void print_pos_comment_short(java.io.PrintStream w) {
+ if (pos != null) {
+ w.print("(* ");
+ w.print(new Integer(pos.linenum).toString());
+ w.print(" *)");
+ }
+ }
+
+ protected void print_pos_comment_long(java.io.PrintStream w) {
+ if (pos != null) {
+ w.print("(* ");
+ pos.print(w);
+ w.print(" *)");
+ }
+ }
+
+ public String debug(Context ctxt) {
+ java.io.ByteArrayOutputStream s = new java.io.ByteArrayOutputStream();
+ java.io.PrintStream w = new java.io.PrintStream(s);
+ defExpandTop(ctxt).do_print(w, ctxt);
+ return s.toString();
+ }
+
+ public String toString(Context ctxt) {
+ java.io.ByteArrayOutputStream s = new java.io.ByteArrayOutputStream();
+ java.io.PrintStream w = new java.io.PrintStream(s);
+ print(w, ctxt);
+ return s.toString();
+ }
+
+ // intended only for unannotated terms -- others may fail.
+ public final int hashCode(Context ctxt) {
+ ctxt.next_var_hash_code = 0;
+ return hashCode_h(ctxt);
+ }
+
+ public int hashCode_h(Context ctxt) {
+ handleError(ctxt,
+ "Internal error: hashCode() function not implemented for"
+ + " construct " + (new Integer(construct)).toString()
+ + ".");
+ return 0;
+ }
+
+ // count free occurrences of e.
+ abstract public int numOcc(Expr e);
+
+ public boolean isApp() { // overridden by App
+ return false;
+ }
+
+ // substitute e for x in this Expr. We only support substituting
+ // for Vars x and Holes x.
+ abstract public Expr subst(Expr e, Expr x);
+
+ // return the Const with name s in the ctxt, or return an error.
+ protected Const _const(Context ctxt, String s) {
+ Expr c = ctxt.lookup(s);
+ if (c == null || c.construct != Expr.CONST)
+ handleError(ctxt, "Cannot find special constant " + s + ".");
+ return (Const) c;
+ }
+
+ public boolean containsVars(Stack boundVars) {
+ boolean returnValue = false;
+
+ Enumeration varsEnum = boundVars.elements();
+ while (varsEnum.hasMoreElements()) {
+ Var currentVar = (Var) varsEnum.nextElement();
+ if (numOcc(currentVar) > 0) {
+ returnValue = true;
+ }
+ }
+
+ return returnValue;
+ }
+
+ // substitute e for x in this Expr. x may be an arbitrary ground
+ // term, and any sub term of this which is definitionally equal
+ // to x will be replaced with e.
+ final public Expr rewrite(Context ctxt, Expr e, Expr x, Stack boundVars) {
+ if (defEq(ctxt, x, NO_APPROX, true) && !x.containsVars(boundVars)
+ && !e.containsVars(boundVars)) {
+ return e;
+ } else {
+ ctxt.resetNotDefEq();
+ return do_rewrite(ctxt, e, x, boundVars);
+ }
}
- Expr e1 = dropAnnos(ctxt);
- Expr e2 = e.dropAnnos(ctxt);
-
- if (ctxt.getFlag("debug_def_eq")) {
- ctxt.w.println("With annotations dropped:");
- ctxt.w.print("1. ");
- e1.print(ctxt.w,ctxt);
- ctxt.w.print("\n2. ");
- e2.print(ctxt.w,ctxt);
- ctxt.w.println("");
- ctxt.w.flush();
- }
- if (approx == APPROX_NO_INDICES)
- return e1.defEqNoAnnoApprox(ctxt,e2,spec);
- return e1.defEqNoAnno(ctxt,e2,spec);
- }
-
- // do not drop annotations, treat as specificational
- //
- // type family abbrev's are not expanded.
- public Expr defExpandTop(Context ctxt) {
- return defExpandTop(ctxt, false, true);
- }
-
- public Expr defExpandTop(Context ctxt, boolean drop_annos,
- boolean spec) {
- Expr ret = defExpandOne(ctxt,drop_annos,spec);
- if (ret != this)
- return ret.defExpandTop(ctxt,drop_annos,spec);
- return ret;
- }
-
- public Expr defExpandOne(Context ctxt, boolean drop_annos,
- boolean spec) {
- if (construct == VAR) {
- Var v = (Var)this;
- if (ctxt.isMacroDefined(v))
- return ctxt.getDefBody(v);
- }
- else if (construct == CONST) {
- Const c = (Const)this;
- if (ctxt.isDefined(c)
- && (spec || !ctxt.isOpaque(c))
- && !ctxt.isTypeFamilyAbbrev(c))
- /* if we are not in a spec expression, then we do not
- expand opaque definitions. Also, we do not expand
- type family abbreviations. That is done in
- TypeApp, so that we can do beta-reductions
- immediately with them. */
- return (drop_annos ? ctxt.getDefBodyNoAnnos(c)
- : ctxt.getDefBody(c));
- }
- else if (construct == ABBREV)
- return ((Abbrev)this).subst();
- else if (construct == CUTOFF) {
- return ((Cutoff)this).get_nat_t(ctxt,spec);
- }
- else if (construct == PRED_APP)
- return ((PredApp)this).doBeta(ctxt, drop_annos, spec,
- true /* expand defs */);
- return this;
- }
-
- public static void handleError(Position p, String msg) {
- if (p != null) {
- p.print(System.out);
- System.out.print(": ");
- }
- System.out.println("");
- System.out.println(msg);
- System.exit(2);
- }
-
- public void handleError(Context ctxt, String msg) {
- handleError(ctxt,pos,msg);
- }
-
- public void handleError(Context ctxt, Position p, String msg) {
- if (p != null) {
- p.print(System.out);
- System.out.print(": ");
- }
- System.out.println("classification error.\n\n"+msg);
- ctxt.printDefEqErrorIf();
- System.exit(2);
- }
-
- // is this Expr either d or <d Xs>?
- boolean isdtype(Context ctxt, Const d) {
- if (this == d)
- return true;
- if ((construct == TYPE_APP)
- && ((TypeApp)this).getHead(ctxt, false) == d)
- return true;
- if (construct == VAR && ctxt.isMacroDefined((Var)this))
- return ctxt.getDefBody((Var)this).isdtype(ctxt,d);
- return false;
- }
-
- // if this is a dtype, return its head (i.e., c if this is c or <c
Y1 ... Yn>);
- // otherwise return null.
- Const typeGetHead(Context ctxt, boolean spec) {
- if (construct == CONST) {
- Const c = (Const)this;
- boolean not_opaque_if = spec || !ctxt.isOpaque(c);
- if (ctxt.isDefined(c) && not_opaque_if) {
- if (ctxt.getFlag("debug_typeGetHead")) {
- ctxt.w.println("typeGetHead() called on: "+toString(ctxt)
- +", with spec="+(new Boolean(spec)).toString()
- +", opaque="+(new Boolean(ctxt.isOpaque(c))).toString());
- ctxt.w.flush();
- }
- /* if c is coming from a type of the form <d xs> where d is a
- type family abbrev and xs is an incomplete argument list,
- then we will get an infinite loop without the following check. */
- Expr cc = c.defExpandTop(ctxt,false,true);
- if (cc == c)
- return null;
- return cc.typeGetHead(ctxt, spec);
- }
- if (ctxt.isTypeCtor((Const)this) && not_opaque_if)
- return (Const)this;
- return null;
- }
- if (construct != TYPE_APP)
- return null;
- return ((TypeApp)this).getHead(ctxt,spec).typeGetHead(ctxt, spec);
- }
-
- // we assume this is a type, and return true iff it is an inductive
- // type that is not opaque.
- boolean isdtype(Context ctxt, boolean spec) {
- Const head = typeGetHead(ctxt,spec);
- return (head != null);
- }
-
- /* assuming this is a type, is it one corresponding to tracked
references?
- We assume this is not being called in a specificational position. */
- public boolean isTrackedType(Context ctxt) {
- if (construct == CONST) {
- Const d = (Const)this;
- if (ctxt.isUntracked(d))
+ public Expr do_rewrite(Context ctxt, Expr e, Expr x, Stack boundVars) {
+ handleError(ctxt,
+ "Internal error: do_rewrite called on an inappropriate expression in: "
+ + this.getClass().toString());
+ // throw new
+ // RuntimeException("Internal error: do_rewrite called on an
inappropriate expression in: "+this.getClass().toString());
+ return this;
+ }
+
+ public Expr classify(Context ctxt, int approx, boolean spec) {
+ if (approx > NO_APPROX) {
+ System.out.println("Approximate classification for this construct "
+ + "unimplemented: " + (new Integer(construct)));
+ System.exit(5);
+ }
+ return classify(ctxt);
+ }
+
+ /*
+ * subclasses should override one or the other classify method, or expect
a
+ * stack overflow. We will treat this as specificational (use the other
+ * classify() method to specify non-specificational).
+ */
+ public Expr classify(Context ctxt) {
+ return classify(ctxt, NO_APPROX, true);
+ }
+
+ // is e definitionally equal to this expr in the given ctxt.
+ protected boolean defEqNoAnno(Context ctxt, Expr e, boolean spec) {
+ System.out.println("Definitional equality for this construct"
+ + " unimplemented: " + (new Integer(construct)));
+ System.exit(5);
+ return false;
+ }
+
+ protected boolean defEqNoAnnoApprox(Context ctxt, Expr e, boolean spec) {
+ System.out.println("Approximate definitional equality for this"
+ + " construct unimplemented: " + (new Integer(construct)));
+ System.exit(5);
+ return false;
+ }
+
+ final public boolean defEq(Context ctxt, Expr e, boolean spec) {
+ return defEq(ctxt, e, NO_APPROX, spec);
+ }
+
+ // specificational by default
+ final public boolean defEq(Context ctxt, Expr e) {
+ return defEq(ctxt, e, NO_APPROX, true);
+ }
+
+ /*
+ * approx level 2 means all types are considered equal; 1 means we drop
+ * indices; 0 means drop annotations from terms (no approximation).
+ */
+ public static final int NO_APPROX = 0;
+ public static final int APPROX_NO_INDICES = 1;
+ public static final int APPROX_TRIVIAL = 2;
+
+ final public boolean defEq(Context ctxt, Expr e, int approx, boolean
spec) {
+ if (approx == 2)
+ return true;
+
+ if (ctxt.getFlag("debug_def_eq")) {
+ ctxt.w.println("--------------------------------------------------");
+ ctxt.w.println("Testing definitional equality (spec = "
+ + (spec ? "true" : "false") + ") of:");
+ ctxt.w.print("1. ");
+ print(ctxt.w, ctxt);
+ ctxt.w.print("\n2. ");
+ e.print(ctxt.w, ctxt);
+ ctxt.w.println("");
+ ctxt.w.flush();
+ }
+
+ Expr e1 = dropAnnos(ctxt);
+ Expr e2 = e.dropAnnos(ctxt);
+
+ if (ctxt.getFlag("debug_def_eq")) {
+ ctxt.w.println("With annotations dropped:");
+ ctxt.w.print("1. ");
+ e1.print(ctxt.w, ctxt);
+ ctxt.w.print("\n2. ");
+ e2.print(ctxt.w, ctxt);
+ ctxt.w.println("");
+ ctxt.w.flush();
+ }
+ if (approx == APPROX_NO_INDICES)
+ return e1.defEqNoAnnoApprox(ctxt, e2, spec);
+ return e1.defEqNoAnno(ctxt, e2, spec);
+ }
+
+ // do not drop annotations, treat as specificational
+ //
+ // type family abbrev's are not expanded.
+ public Expr defExpandTop(Context ctxt) {
+ return defExpandTop(ctxt, false, true);
+ }
+
+ public Expr defExpandTop(Context ctxt, boolean drop_annos, boolean spec) {
+ Expr ret = defExpandOne(ctxt, drop_annos, spec);
+ if (ret != this)
+ return ret.defExpandTop(ctxt, drop_annos, spec);
+ return ret;
+ }
+
+ public Expr defExpandOne(Context ctxt, boolean drop_annos, boolean spec) {
+ if (construct == VAR) {
+ Var v = (Var) this;
+ if (ctxt.isMacroDefined(v))
+ return ctxt.getDefBody(v);
+ } else if (construct == CONST) {
+ Const c = (Const) this;
+ if (ctxt.isDefined(c) && (spec || !ctxt.isOpaque(c))
+ && !ctxt.isTypeFamilyAbbrev(c))
+ /*
+ * if we are not in a spec expression, then we do not expand
+ * opaque definitions. Also, we do not expand type family
+ * abbreviations. That is done in TypeApp, so that we can do
+ * beta-reductions immediately with them.
+ */
+ return (drop_annos ? ctxt.getDefBodyNoAnnos(c) : ctxt
+ .getDefBody(c));
+ } else if (construct == ABBREV)
+ return ((Abbrev) this).subst();
+ else if (construct == CUTOFF) {
+ return ((Cutoff) this).get_nat_t(ctxt, spec);
+ } else if (construct == PRED_APP)
+ return ((PredApp) this).doBeta(ctxt, drop_annos, spec, true /*
+ * expand
+ * defs
+ */);
+ return this;
+ }
+
+ public static void handleError(Position p, String msg) {
+ if (p != null) {
+ p.print(System.out);
+ System.out.print(": ");
+ }
+ System.out.println("");
+ System.out.println(msg);
+ System.exit(2);
+ }
+
+ public void handleError(Context ctxt, String msg) {
+ handleError(ctxt, pos, msg);
+ }
+
+ public void handleError(Context ctxt, Position p, String msg) {
+ if (p != null) {
+ p.print(System.out);
+ System.out.print(": ");
+ }
+ System.out.println("classification error.\n\n" + msg);
+ ctxt.printDefEqErrorIf();
+ System.exit(2);
+ }
+
+ // is this Expr either d or <d Xs>?
+ boolean isdtype(Context ctxt, Const d) {
+ if (this == d)
+ return true;
+ if ((construct == TYPE_APP)
+ && ((TypeApp) this).getHead(ctxt, false) == d)
+ return true;
+ if (construct == VAR && ctxt.isMacroDefined((Var) this))
+ return ctxt.getDefBody((Var) this).isdtype(ctxt, d);
return false;
- if (ctxt.isOpaque(d))
- return true;
- }
-
- Expr T = defExpandTop(ctxt,false,false);
-
- if (T.construct == FUN_TYPE || T.construct == TYPE)
- return false;
- if (T.construct == CONST) {
- Const d = (Const)T;
- return !ctxt.isFlat(d) && !ctxt.isUntracked(d);
- }
- if ((T.construct == TYPE_APP)) {
- Expr h = ((TypeApp)T).getHead(ctxt, false);
- return !ctxt.isFlat((Const)h);
- }
- return !isFormula(T.construct);
- }
-
-
- public static Expr[] varArrayToExprArray(Var[] v) {
- int iend = v.length;
- Expr[] e = new Expr[iend];
- for (int i = 0; i < iend; i++)
- e[i] = v[i];
- return e;
- }
-
- public boolean isFormula(Context ctxt) {
- Expr tmp = defExpandTop(ctxt);
- return isFormula(tmp.construct);
- }
-
- public static boolean isFormula(int construct) {
- switch(construct) {
- case FORALL:
- case EXISTS:
- case EABBREV:
- case CABBREV:
- case ABBREV:
- case ATOM:
- case PRED_APP:
- case TRUE:
- case FALSE:
- return true;
- }
- return false;
- }
-
- public static boolean isProof(int construct) {
- switch(construct) {
- case VAR:
- case BANG:
- case CONST:
- case FORALLI:
- case PROOF_APP:
- case CASE_PROOF:
- case EXISTSI:
- case ANDI:
- case EXISTSE:
- case EABBREV:
- case CABBREV:
- case ABBREV:
- case JOIN:
- case EVAL:
- case EVALTO:
- case HYPJOIN:
- case SHOW:
- case REFL:
- case SYMM:
- case TRANS:
- case TRANSS:
- case CONG:
- case NCONG:
- case INJ:
- case CLASH:
- case ACLASH:
- case INV:
- case SUBST:
- case CONTRA:
- case INDUCTION:
- case TRUEI:
- case DISEQI:
- case CIND:
- case TERM_CASE:
- return true;
- }
- return false;
- }
-
- public static boolean isTerm(int construct) {
- switch(construct) {
- case VAR:
- case CONST:
- case VOIDI:
- case DO:
- case COMPRESS:
- case FUN_TERM:
- case CAST:
- case COMPILE_AS:
- case TERMINATES:
- case TERM_APP:
- case ABORT:
- case LET:
- case ABBREV:
- case EABBREV:
- case CABBREV:
- case MATCH:
- case CUTOFF:
- case IMPOSSIBLE:
- case SIZE:
- case EXISTSE_TERM:
- return true;
- }
- return false;
- }
-
-
-
- public static boolean isTypeOrKind(int construct) {
- switch(construct) {
- case VAR:
- case CONST:
- case VOID:
- case BANG:
- case ABBREV:
- case EABBREV:
- case CABBREV:
- case FUN_TYPE:
- case TYPE_APP:
- case TYPE:
- return true;
- }
- return false;
- }
-
- public boolean isTerm(Context ctxt) {
- Expr tmp = defExpandTop(ctxt);
- if (tmp.construct == VAR)
- return ctxt.getClassifier((Var)tmp).isTypeOrKind(ctxt);
- if (tmp.construct == CONST)
- return ctxt.isTermCtor((Const)tmp);
-
- return isTerm(tmp.construct);
- }
-
- public boolean isTypeOrKind(Context ctxt) {
- Expr tmp = defExpandTop(ctxt);
-
- if (tmp.construct == VAR) {
- Expr c = ctxt.getClassifier((Var)tmp);
- if (c == null)
- System.err.println("Internal error. Null classifier
for: "+tmp.toString(ctxt));
- return c.construct == TYPE;
- }
- if (tmp.construct == CONST)
- return ctxt.isTypeCtor((Const)tmp) ||
ctxt.isTypeFamilyAbbrev((Const)tmp);
-
- return isTypeOrKind(tmp.construct);
- }
-
- public boolean isProof(Context ctxt) {
- Expr tmp = defExpandTop(ctxt);
- if (tmp.construct == VAR)
- return ctxt.isAssumption((Var)tmp);
- if (tmp.construct == CONST)
- return false;
-
- return isProof(tmp.construct);
- }
-
- public boolean isY(Context ctxt) {
- return isTerm(ctxt) || isTypeOrKind(ctxt);
- }
-
- public boolean isB(Context ctxt) {
- return (construct == TYPE || isTypeOrKind(ctxt));
***The diff for this file has been truncated for email.***
=======================================
--- /branches/1.0/guru/Parser.java Thu Jun 9 07:28:55 2011
+++ /branches/1.0/guru/Parser.java Mon Aug 22 15:38:29 2011
@@ -173,6 +173,12 @@
case Expr.CABBREV:
e = readAbbrev( Abbrev.fAbbrevClassify);
break;
+ case Expr.LEMMA:
+ e = readLemma();
+ break;
+ case Expr.LEMMA_MARK:
+ e = readLemmaMark();
+ break;
case Expr.MATCH:
e = readMatch();
break;
@@ -866,15 +872,23 @@
{
int construct = eatKeyword();
if (!isX(construct))
- handleError("Expected a term, type, or proof.");
+ handleError("Expected a term, type, kind, or proof.");
return readAny(construct);
}
+
+ protected Expr readArg() throws IOException
+ {
+ int construct = eatKeyword();
+ if(!isX(construct) && construct != Expr.LEMMA_MARK)
+ handleError("Expected a term, type, kind, proof, or lemma mark.");
+ return readAny(construct);
+ }
protected Expr readY() throws IOException
{
int construct = eatKeyword();
if (!isY(construct))
- handleError("Expected a term, type, or proof.");
+ handleError("Expected a type, kind, or term.");
return readAny(construct);
}
@@ -1254,7 +1268,7 @@
while(!tryToEat("]"))
{
- theT.add(readX());
+ theT.add(readArg());
if (!eat_ws())
handleError("Unexpected end of input parsing a proof"
@@ -1857,6 +1871,32 @@
ret.pos = pos;
return ret;
}
+
+ protected Lemma readLemma() throws IOException
+ {
+ 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;
+ }
+
+ protected LemmaMark readLemmaMark()
+ {
+ Position pos = getPos();
+ LemmaMark ret = new LemmaMark();
+ ret.pos = pos;
+ return ret;
+ }
protected Const readBindingConst() throws IOException
{
@@ -2696,6 +2736,8 @@
keywordTree.add( "abbrev", Expr.ABBREV );
keywordTree.add( "eabbrev", Expr.EABBREV );
keywordTree.add( "cabbrev", Expr.CABBREV );
+ keywordTree.add( "lemma", Expr.LEMMA );
+ keywordTree.add( "##", Expr.LEMMA_MARK );
keywordTree.add( "match", Expr.MATCH );
keywordTree.add( "Fun", Expr.FUN_TYPE );
keywordTree.add( "type", Expr.TYPE );