[guru-lang] r545 committed - unjoin no longer recursively unjoins. simplified, commented, cleaned u...
guru...@googlecode.com
Author: kevinclancy0
Date: Thu Oct 27 08:11:15 2011
Log: unjoin no longer recursively unjoins. simplified, commented,
cleaned up. added a missing file, UnjoinContra
http://code.google.com/p/guru-lang/source/detail?r=545
Added:
/branches/1.0/guru/UnjoinContra.java
Modified:
/branches/1.0/guru/Const.java
/branches/1.0/guru/Expr.java
/branches/1.0/guru/Lemma.java
/branches/1.0/guru/LemmaSet.java
/branches/1.0/guru/Let.java
/branches/1.0/guru/Match.java
/branches/1.0/guru/TermApp.java
/branches/1.0/guru/Unjoin.java
/branches/1.0/guru/UnjoinContext.java
/branches/1.0/guru/UnjoinContradiction.java
/branches/1.0/guru/UnjoinDeduction.java
/branches/1.0/guru/Var.java
=======================================
--- /dev/null
+++ /branches/1.0/guru/UnjoinContra.java Thu Oct 27 08:11:15 2011
@@ -0,0 +1,237 @@
+package guru;
+
+import java.io.PrintStream;
+import java.util.List;
+import java.util.Stack;
+import java.util.Vector;
+
+import guru.Atom;
+import guru.Context;
+import guru.Exists;
+import guru.Existse;
+import guru.Expr;
+import guru.Foralli;
+import guru.UnjoinContext;
+import guru.UnjoinDeduction;
+import guru.UnjoinIntro;
+import guru.Var;
+
+
+/*
+ * A proof construct, taking a proof of a formula of the form { t = v },
+ * which allows us to automatically derive a contradiction by determining
+ * that no normalization path from t to v exists given that the formulas
+ * in the unnamed lemma set are true.
+ *
+ * UnjoinContra appears in source as "unjoin u contra F", where u is a
proof
+ * whose classifier has the form { t = v } and F is the formula we wish our
+ * unjoin construct to classify as.
+ *
+ * Here is an example of a usage of UnjoinContra.
+ *
+ * Define lt_Z2 : Forall(a:nat).{ (lt a Z) = ff } :=
+ * foralli(a : nat).
+ * case (lt a Z) by v ign with
+ * | ff =>
+ * v
+ * | tt =>
+ * unjoin v contra { (lt a Z) = ff }
+ * end.
+ *
+ * UnjoinContra's implementation is very similar to Unjoin's. See
+ * Unjoin.java for a more detailed explanation of how unjoining works.
+ */
+public class UnjoinContra extends Expr {
+
+ // An expression which proves the scrutinee atom.
+ public final Expr scrutineeProof;
+
+ // The formula, written by the programmer, which the contradiction
+ // is being used to prove.
+ public final Expr conclusion;
+
+ public UnjoinContra(Expr scrutineeProof, Expr conclusion)
+ {
+ super(UNJOIN_CONTRA);
+
+ assert(scrutineeProof != null);
+ assert(conclusion != null);
+
+ this.scrutineeProof = scrutineeProof;
+ this.conclusion = conclusion;
+ }
+
+ private void DumpUnjoinPaths(List unjoinPaths, Context ctxt) {
+ for(int i = 0; i < unjoinPaths.size(); ++i) {
+ String pathString = "";
+ Stack path = (Stack)unjoinPaths.get(i);
+ for(int j = 0; j < path.size(); ++j)
+ {
+ UnjoinIntro u = (UnjoinIntro)path.get(j);
+
+ pathString += "(" + u.introVar.toString(ctxt) + " : " +
+ u.introVarType.toString(ctxt) + ")";
+ }
+
+ System.out.println(pathString);
+ }
+ }
+
+ // Converts the left hand side of the scrutinee atom into an equivalent
term
+ // from which unjoin can derive useful information. This equivalent term
+ // will either be a match, a let, or an abbrev.
+ //
+ // The conversion process is as follows:
+ //
+ // - While t is a term app:
+ // - if the head is a const defined to be some recursive function,
+ // establish a correspondence between the constant and the
function's
+ // recursive variable in the unjoin context
+ // - evaluate the head if possible
+ // - if the resulting head is a function term, instantiate the function
+ // in a lazy manner, substituting each actual argument for its
corresponding
+ // formal argument without evaluating the actuals.
+ // otherwise, generate an error and halt.
+ // - assign t to the instantiated function.
+ // - return t
+ private Expr instantiate(Context ctxt, Expr lhs)
+ {
+ if (lhs.construct != TERM_APP)
+ return lhs;
+
+ TermApp ta = (TermApp)lhs;
+
+ while (true) {
+ //The head, normalized to a function term
+ Expr h = ta.head.evalStep(ctxt);
+ //The constant or variable initially used for the head.
+ Expr pre = ta.head;
+
+ //TODO: we really need to loop here, evaluating the head
+ //one step at a time until normalization, generating an
+ //error message if any intermediate form is not a constant.
+ //We only need to establish a correspondence between the
+ //initial const and the recursive variable of the normal form.
+
+ // If the head does not normalize to a function, we cannot
+ // instantiate it, so we cannot unjoin this term app.
+ if (h.construct != FUN_TERM) {
+ handleError(ctxt,
+ "The left hand side of an unjoin scrutinee " +
+ "simplifies to a term app whose head is not a function.\n" +
+ "1. lhs:" + lhs.toString(ctxt) + "\n" +
+ "2. simplified lhs: " + h.toString(ctxt) + "\n"
+ );
+ }
+
+ // The pre-instantiated value of the head.
+ FunTerm f = (FunTerm)h;
+ // A variable used to instantiate the head
+ FunTerm inst = f;
+
+ // Apply all arguments except last.
+ for (int i = 0; i < ta.X.length-1; ++i)
+ inst = (FunTerm)inst.substituteForParam(ta.X[i]);
+
+ // Apply last argument.
+ // Instantiating a function with one argument may result in an
+ // arbitrary term, so we need to use an Expr rather than
+ // a FunTerm to hold the result.
+ Expr fullInstantiation = inst.substituteForParam(ta.X[ta.X.length-1]);
+
+ // If we are unjoining an application of a recursive, top-level
+ // function, we substitute the function's constant for occurrences
+ // of the function's recursive variable in the body.
+ //
+ // This way, any facts deduced about recursive calls will mention
+ // the constant which, unlike the recursive variable, is accessible
+ // via the current context.
+ if (f.r != null && pre.construct == CONST)
+ fullInstantiation = (Expr)fullInstantiation.subst((Const)pre, f.r);
+
+ //TODO: substitute lets and abbrevs here?
+
+ if (fullInstantiation.construct != TERM_APP)
+ return fullInstantiation;
+
+ ta = (TermApp)fullInstantiation;
+ }
+ }
+
+ public Expr classify(Context ctxt) {
+ Expr cScrutProof = scrutineeProof.classify(ctxt);
+
+ if (cScrutProof.construct != ATOM) {
+ handleError(ctxt,
+ "Attempted to unjoin an expression not classified as an equation" +
+ " or disequation.\n" +
+ "1. classifier of expression: " + cScrutProof.toString(ctxt)
+ );
+
+ System.exit(0);
+ }
+
+ Atom scrutinee = (Atom)cScrutProof;
+
+ if (!scrutinee.Y2.isI(ctxt)) {
+ handleError(ctxt,
+ "Right hand side of unjoin scrutinee classifier is not" +
+ "a value.\n" +
+ "1. scrutinee classifier: " + cScrutProof.toString(ctxt)
+ );
+
+ System.exit(0);
+ }
+
+ Expr instantiated = instantiate(ctxt, scrutinee.Y1);
+ instantiated = ctxt.lemmaSet.instantiate(instantiated);
+
+ UnjoinDeduction deduction = instantiated.Unjoin(
+ scrutinee.Y2,
+ 0,
+ ctxt,
+ scrutinee.equality
+ );
+
+ List unjoinPaths = UnjoinDeduction.Flatten(deduction, ctxt);
+
+ if (unjoinPaths.size() != 0) {
+ DumpUnjoinPaths(unjoinPaths, ctxt);
+ handleError(ctxt,
+ "Unjoin did not derive a contradiction. Unjoin has deduced\n" +
+ "the execution paths listed above.");
+ }
+
+ return conclusion;
+ }
+
+ public void checkTermination(Context ctxt, Expr IH, int arg, Var[]
vars) {
+ conclusion.checkTermination(ctxt,IH,arg,vars);
+ }
+
+ protected void do_print(PrintStream w, Context ctxt) {
+ w.print("unjoin ");
+ scrutineeProof.print(w, ctxt);
+ w.print(" contra ");
+ conclusion.print(w, ctxt);
+ }
+
+ // Expr override
+ public int numOcc(Expr e) {
+ return scrutineeProof.numOcc(e) + conclusion.numOcc(e);
+ }
+
+ // Expr override
+ public Expr subst(Expr e, Expr x) {
+ return new UnjoinContra(
+ scrutineeProof.subst(e, x),
+ conclusion.subst(e, x)
+ );
+ }
+
+ // Expr override
+ public Expr dropAnnos(Context ctxt) {
+ return new Bang();
+ }
+
+}
=======================================
--- /branches/1.0/guru/Const.java Wed Oct 12 12:15:28 2011
+++ /branches/1.0/guru/Const.java Thu Oct 27 08:11:15 2011
@@ -126,7 +126,7 @@
public UnjoinDeduction Unjoin(
Expr target,
- UnjoinContext uCtxt,
+ int proofCount,
Context baseCtxt,
boolean eq
)
=======================================
--- /branches/1.0/guru/Expr.java Fri Oct 21 12:38:46 2011
+++ /branches/1.0/guru/Expr.java Thu Oct 27 08:11:15 2011
@@ -785,7 +785,7 @@
// target term.)
public UnjoinDeduction Unjoin(
Expr target,
- UnjoinContext uCtxt,
+ int proofCount,
Context baseCtxt,
boolean eq
)
=======================================
--- /branches/1.0/guru/Lemma.java Wed Oct 12 12:15:28 2011
+++ /branches/1.0/guru/Lemma.java Thu Oct 27 08:11:15 2011
@@ -26,7 +26,7 @@
*
* 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
+ * [div_le a two ##] will only be considered well classified if an unnamed
proof
* 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.
=======================================
--- /branches/1.0/guru/LemmaSet.java Wed Oct 12 12:15:28 2011
+++ /branches/1.0/guru/LemmaSet.java Thu Oct 27 08:11:15 2011
@@ -108,6 +108,49 @@
return e;
}
+
+
+ public Expr instantiate(Expr e)
+ {
+ Expr ret = e;
+
+ ListIterator i = formulas.listIterator();
+ while(i.hasNext()) {
+ Expr curr = (Expr)i.next();
+
+ if (curr.construct != Expr.ATOM)
+ continue;
+
+ Atom a = (Atom)curr;
+
+ if (a.equality == false)
+ continue;
+
+ if (a.Y1.construct == Expr.VAR) {
+ if (a.Y2.construct == Expr.TERM_APP) {
+ TermApp ta = (TermApp)a.Y2;
+
+ if (ta.head.construct == Expr.CONST &&
ctxt.isTermCtor((Const)ta.head))
+ ret = ret.subst(a.Y2, a.Y1);
+ }
+ else if(a.Y2.construct == Expr.CONST) {
+ ret = ret.subst(a.Y2, a.Y1);
+ }
+ }
+ else if (a.Y2.construct == Expr.VAR) {
+ if (a.Y1.construct == Expr.TERM_APP) {
+ TermApp ta = (TermApp)a.Y1;
+
+ if (ta.head.construct == Expr.CONST &&
ctxt.isTermCtor((Const)ta.head))
+ ret = ret.subst(a.Y1, a.Y2);
+ }
+ else if(a.Y1.construct == Expr.CONST)
+ ret = ret.subst(a.Y1, a.Y2);
+ }
+ }
+
+ return ret;
+ }
private Expr rewrite(Expr e)
{
=======================================
--- /branches/1.0/guru/Let.java Wed Oct 12 12:15:28 2011
+++ /branches/1.0/guru/Let.java Thu Oct 27 08:11:15 2011
@@ -169,14 +169,14 @@
// Overloaded from Expr
public UnjoinDeduction Unjoin(
Expr target,
- HashSet funCalls,
+ int proofCount,
Context ctxt,
boolean eq
)
{
return Unjoin(
t2.subst(t1, x1),
- funCalls,
+ proofCount,
ctxt,
eq
);
=======================================
--- /branches/1.0/guru/Match.java Fri Oct 21 12:38:46 2011
+++ /branches/1.0/guru/Match.java Thu Oct 27 08:11:15 2011
@@ -159,126 +159,84 @@
}
}
- //When we generate a new var name during unjoin, we append this integer
- //to it to make it unique.
- //TODO: This does not seem like an airtight method.
- private static int varNum = 0;
//Override from Expr
public UnjoinDeduction Unjoin(
Expr target,
- UnjoinContext uCtxt,
+ int proofCount,
Context baseCtxt,
boolean eq
)
{
UnjoinDeduction ret = UnjoinDeduction.contradiction;
- Expr t_ = uCtxt.lemmaSet.simplify(t);
-
- UnjoinDeduction branch;
-
- //Set ret to the conjunction of the deductions that can be made from
+ Expr t_ = t;
+ while (t_.construct != TERM_APP && t_ != t_.evalStep(baseCtxt))
+ t_ = t_.evalStep(baseCtxt);
+
+ //Set ret to the disjunction of the deductions that can be made from
//each branch.
for(int i = 0; i < C.length; ++i)
{
+ UnjoinDeduction branch;
+
Case c = C[i];
- UnjoinDeduction scrutDeduction = UnjoinDeduction.empty;
-
- if (t_.construct == TERM_APP)
- {
- TermApp ta = (TermApp)t_;
-
- if (ta.head != c.c)
+
+ //TODO: do we really have to do this to detect term constructors?
+ boolean isTermConstructor = t_.construct == TERM_APP &&
t_.evalStep(baseCtxt) == t_;
+ if (isTermConstructor) {
+ if (((TermApp)t_).head != c.c)
continue;
}
- else if (t_.construct == CONST)
- {
+ else if (t_.construct == CONST) {
if (t_ != c.c)
continue;
}
- else if (t_.construct == MATCH)
- {
- if(c.x.length == 0)
- {
- scrutDeduction = t_.Unjoin(
- c.c,
- uCtxt,
- baseCtxt,
- true
- );
- }
- else
- {
- scrutDeduction = t_.Unjoin(
- new TermApp(c.c,c.x),
- uCtxt,
- baseCtxt,
- true
- );
- }
- }
// Prepend immediate deductions onto case body deductions -----
- if (c.x.length == 0)
- {
+ if (c.x.length == 0) {
// Make deductions from case body -----
- branch = UnjoinDeduction.FancyAppend(
- UnjoinDeduction.Simplify(scrutDeduction),
- c.body,
+ branch = c.body.Unjoin(
target,
- uCtxt,
+ t_.construct == CONST ? proofCount : proofCount + 1,
baseCtxt,
eq
);
- if(t_.construct == VAR)
- {
- Atom matchEq = new Atom(true, t_, c.c);
- Var matchEqVar = new Var("p" + Integer.toString(varNum++));
- branch = new UnjoinIntro(matchEqVar, matchEq, branch);
+ if (t_.construct != CONST) {
+ Atom matchEq = new Atom(true, t_, c.c);
+ Var matchEqVar = new Var("p" + proofCount);
+ branch = new UnjoinIntro(matchEqVar, matchEq, branch);
}
}
- else
- {
+ else {
FunType consType =
(FunType)c.c.classify(baseCtxt).defExpandTop(baseCtxt);
- // A version of body for which variables corresponding to
- // match arguments are replaced with their corresponding
- // unjoin introductions.
Expr body = c.body;
- // Create contstructor argument variable -----
-
-
- if (t_.construct == TERM_APP)
- {
+
+ // Create argument variables -----
+ if (t_.construct == TERM_APP) {
TermApp ta = (TermApp)t_;
- Expr substitutedBody = body;
for (int j = 0; j < ta.X.length; ++j)
- substitutedBody = substitutedBody.subst(ta.X[j], c.x[j]);
-
- branch = substitutedBody.Unjoin(
- target,
- uCtxt,
- baseCtxt,
- eq
+ body = body.subst(ta.X[j], c.x[j]);
+
+ branch = body.Unjoin(
+ target,
+ proofCount,
+ baseCtxt,
+ eq
);
}
- else
- {
-
+ else {
Var[] clones = new Var[c.x.length];
Expr[] types = new Expr[c.x.length];
int last = c.x.length-1;
- String prefix = ((Var)t_).name;
-
for(int j = 0; j <= last; ++j)
{
- clones[j] = new Var(uCtxt.genName(prefix + String.valueOf(j)));
+ clones[j] = new Var(((Var)t_).name + j);
types[j] = consType.types[j];
- //TODO: This seems a bit inefficient. Could we optimize this?
body = body.subst(clones[j], c.x[j]);
// Instantiating the last argument would result in the
@@ -288,34 +246,21 @@
}
// Make deductions from case body -----
- branch = UnjoinDeduction.FancyAppend(
- UnjoinDeduction.Simplify(scrutDeduction),
- body,
+ branch = body.Unjoin(
target,
- uCtxt,
+ proofCount+1,
baseCtxt,
eq
);
-
//prepend immediate deductions to case body deductions
- //could this be anything other than a var?
- if(t_.construct == VAR)
- {
- // Create match proof (i.e. { scrutinee = match case } ) -----
- Atom matchEq = new Atom(true, t_, new TermApp(c.c,clones));
- Var matchEqVar = new Var("p" + Integer.toString(varNum++));
- branch = new UnjoinIntro(matchEqVar, matchEq, branch);
- }
+ Atom matchEq = new Atom(true, t_, new TermApp(c.c,clones));
+ Var matchEqVar = new Var("p" + proofCount);
+ branch = new UnjoinIntro(matchEqVar, matchEq, branch);
for (int j = c.x.length-1; j >= 0; --j)
branch = new UnjoinIntro(clones[j], types[j], branch);
-
-
- for(int j = 0; j < c.x.length; ++j)
- uCtxt.removeName(clones[j].name);
- }
-
+ }
}
//Or the current return value with the deduction for the
=======================================
--- /branches/1.0/guru/TermApp.java Wed Oct 12 12:15:28 2011
+++ /branches/1.0/guru/TermApp.java Thu Oct 27 08:11:15 2011
@@ -516,129 +516,22 @@
public UnjoinDeduction Unjoin(
Expr target,
- UnjoinContext uCtxt,
+ int proofCount,
Context baseCtxt,
boolean eq
)
- {
- //The head's normal form.
- Expr h = head;
- //The last form that the head takes on before normalization.
- Expr pre = head;
-
- do {
- if (h.construct == VAR && uCtxt.getFuncConst((Var)h) != null)// &&
uCtxt.hasRecFuncVar((Var)h_))
- {
- Const c = uCtxt.getFuncConst((Var)h);
- TermApp app = new TermApp(c, X);
- Atom introAtom = new Atom(eq, app, target);
-
- //since this is the final deduction, we can name it whatever we
- //want without introducing ambiguity.
- Var introVar = new Var("u");
-
- return new UnjoinIntro(
- introVar,
- introAtom,
- UnjoinDeduction.empty
- );
- }
-
- pre = h;
- h = h.evalStep(baseCtxt);
- } while (h != h.evalStep(baseCtxt));
-
- if (h.construct != FUN_TERM && h.construct != CONST && h.construct !=
VAR)
- {
- handleError(head.pos,
- "Unjoin can't handle term applications for which the head's " +
- "value cannot be determined."
- );
-
- System.exit(0);
- }
-
-
- //TODO: remove this...
- Expr[] evaluatedArgs = new Expr[X.length];
- for (int i = 0; i < X.length; i++)
- evaluatedArgs[i] = X[i];//X[i].eval(baseCtxt);
-
- //We either have a function app or a data constructor
- if (h.construct == FUN_TERM) {
- FunTerm f = (FunTerm)h;
- Var rec = f.r;
-
- for (int i = 0; i < evaluatedArgs.length-1; ++i)
- f = (FunTerm)f.substituteForParam(evaluatedArgs[i]);
-
- //We cast f to FunAbstraction in order to avoid fixpoint
- //expansion.
- Expr fullInstantiation =
f.substituteForParam(evaluatedArgs[evaluatedArgs.length-1]);
-
- if (rec != null)
- {
- if (pre.construct == CONST)
- uCtxt.setFuncConst(rec, (Const)pre);
-
- //TODO: this is not going to work unless we introduce the recursive
- //function.
- uCtxt.addRecFuncVar(rec);
- }
-// if (rec != null) {
-// if (pre.construct == CONST)
-//
-// else
-// // we do not handle this yet, but it should be a simple matter
-// // of introducting a function variable followed by a proof that
-// // the function variable is equal to its definition.
-// assert(false); // I was setting the entry to the function's full
instantiation... does that make sense?
-// }
-
- UnjoinDeduction ret = fullInstantiation.Unjoin(
- target,
- uCtxt,
- baseCtxt,
- eq
- );
-
- //TODO: I think it might be easier to store funcalls
- //in an immutable data structure, a list or rb tree for example.
- if (rec != null)
- {
- if (uCtxt.getFuncConst(rec) != null)
- uCtxt.removeFuncConst(rec);
-
- uCtxt.removeRecFuncVar(rec);
- }
-
- return ret;
- }
- else
- {
- Atom introAtom;
-
-// if (h.construct == VAR && ) {
-// Expr h_ = (Expr)uCtxt.hasRecFuncVar((Var)h);
-//
-// }
-// else {
- //introAtom = new Atom(eq, this, target);
- // }
-
- TermApp app = new TermApp(h, evaluatedArgs);
- introAtom = new Atom(eq, app, target);
-
- //since this is the final deduction, we can name it whatever we
- //want without introducing ambiguity.
- Var introVar = new Var("u");
-
- return new UnjoinIntro(
- introVar,
- introAtom,
- UnjoinDeduction.empty
- );
- }
+ {
+ Atom introAtom = new Atom(eq, this, target);
+
+ //since this is the final deduction, we can name it whatever we
+ //want without introducing ambiguity.
+ Var introVar = new Var("u");
+
+ return new UnjoinIntro(
+ introVar,
+ introAtom,
+ UnjoinDeduction.empty
+ );
}
public guru.carraway.Expr toCarraway(Context ctxt) {
=======================================
--- /branches/1.0/guru/Unjoin.java Fri Oct 21 12:38:46 2011
+++ /branches/1.0/guru/Unjoin.java Thu Oct 27 08:11:15 2011
@@ -3,43 +3,260 @@
import java.io.PrintStream;
import java.util.*;
+
+/*
+ * A proof construct, taking a proof of a formula of the form { t = v },
+ * which allows us to decompose the proof into cases for all normalization
+ * paths from t to v. Unjoin uses the unnamed lemma set (see Lemma,
LemmaSet)
+ * in order to constrain the list of paths which must be handled.
+ *
+ * Decomposing a proof using unjoin relieves us from the tedious task of
deriving
+ * contradictions for impossible cases.
+ *
+ * Unjoin appears in source as "unjoin u with | p1 | p2 ... | pn end",
+ * where u is a proof whose classifier has the form { t = v } and p1, ...
pn
+ * are forall proofs.
+ *
+ * To use unjoin, first add the following syntax at the position in which
+ * you want to use unjoin:
+ *
+ * unjoin u with
+ * end
+ *
+ * Then classify your proof. You should see a classification error listing
+ * all cases which must be handled inside the unjoin. Copy these cases
+ * into your unjoin (between with and end) and then handle them.
+ *
+ *
+ * As an example, consider the following proof.
+ *
+ * Define eqnatEq : Forall(n m:nat)(u:{(eqnat n m) = tt}). { n = m } :=
+ * induction(n:nat) return
+ * Forall(m:nat)(u:{(eqnat n m) = tt}). { n = m }
+ * with
+ * | Z =>
+ * foralli(m: nat)(u : { (eqnat n m) = tt }).
+ * lemma n_eq in
+ * unjoin u with
+ * | foralli(p0 : { m = Z }).
+ * trans : { n = Z } n_eq
+ * : { Z = m } symm p0
+ * end
+ * | S n' =>
+ * foralli(m: nat)(u : { (eqnat n m) = tt }).
+ * lemma n_eq in
+ * | foralli(m' : nat)(p3 : { m = (S m') })(u : { (eqnat n' m') = tt }).
+ * hypjoin n m by
+ * : { n' = m' } [n_IH n' m' u]
+ * : { m = (S m') } p3
+ * : { n = (S n') } n_eq
+ * end
+ * end
+ * end.
+ *
+ * The above proof uses unjoin twice. In both uses, it operates on a proof
+ * of the formula { (eqnat n m) = tt }. The first use deduces that, because
+ * { n = Z } and { (eqnat n m) = tt }, we must have { m = Z }. The second
+ * use deduces facts regarding the situation where { n = (S n') }. In both
+ * uses, unjoin removes the need for us to case split on m, which greatly
+ * simplifies our proof.
+ *
+ * It's important to know that unjoin deductions are made by processing
+ * the syntax for the term being normalized, (eqnat n m) in this case.
+ * Referring to the source code for eqnat should help us understand why
+ * unjoin made the deductions that it did.
+ *
+ * Define eqnat : Fun(^ #owned n m:nat).bool :=
+ * fun eqnat(^ #owned n m:nat):bool.
+ * match ! n with
+ * Z => match ! m with
+ * Z => tt
+ * | S m' => ff
+ * end
+ * | S n' => match ! m with
+ * Z => ff
+ * | S m' => (eqnat n' m')
+ * end
+ * end
+ *
+ * The first use of unjoin is classified with the formula { n = Z } in the
+ * lemma set. Hence, any normalization path for (eqnat n m) must evaluate
+ * to the first case of the match on n. Inside this case, m is scrutinized.
+ * Since we have no formulas regarding m in our lemma set, either case
+ * could be taken. However, the case where m = S m' evaluates to ff, which
+ * does not match our target value tt. This leads unjoin to deduce that
+ * the only possible value for m is Z.
+ *
+ * Unjoin cannot be used under contradictory contexts. A special construct
+ * is needed for this, which is implemented in UnjoinContra.java.
+ *
+ */
public class Unjoin extends Expr {
// An expression which proves the scrutinee atom.
public final Expr scrutineeProof;
- // An equation of the form t = v or a disequation of the form t != v,
- // where t is a terminating term and v is a value.
- public Atom scrutinee;
-
// A list containing forall proofs which quantify over the
// deductions made in each unjoin path.
- private final Vector paths;
+ public final Vector paths;
public Unjoin(Expr scrutineeProof, Vector paths)
{
super(UNJOIN);
+ assert(scrutineeProof != null);
+ assert(paths != null);
+
this.scrutineeProof = scrutineeProof;
this.paths = paths;
}
// Expr override
protected void do_print(PrintStream w, Context ctxt) {
- // TODO Auto-generated method stub
-
+ w.print("unjoin ");
+ scrutineeProof.print(w, ctxt);
+ w.print(" with\n");
+ for (int i = 0; i < paths.size(); ++i) {
+ Foralli path = (Foralli)paths.get(i);
+ path.do_print(w, ctxt);
+ }
+ w.print("end");
+ }
+
+ // TODO: we need a base class for Unjoin and UnjoinContra which implements
+ // this.
+ //
+ // Converts the left hand side of the scrutinee atom into an equivalent
term
+ // from which unjoin can derive useful information. This equivalent term
+ // will either be a match, a let, or an abbrev.
+ //
+ // The conversion process is as follows:
+ //
+ // - While t is a term app:
+ // - if the head is a const defined to be some recursive function,
+ // establish a correspondence between the constant and the
function's
+ // recursive variable in the unjoin context
+ // - evaluate the head if possible
+ // - if the resulting head is a function term, instantiate the function
+ // in a lazy manner, substituting each actual argument for its
corresponding
+ // formal argument without evaluating the actuals.
+ // otherwise, generate an error and halt.
+ // - assign t to the instantiated function.
+ // - return t
+ //
+ // TODO: We might have to prove an equivalence between the strict function
+ // call semantics used by guru and the lazy approach taken by unjoin.
Since
+ // guru is functional, this should work.
+ private Expr instantiate(Context ctxt, Expr lhs)
+ {
+ if (lhs.construct != TERM_APP)
+ return lhs;
+
+ TermApp ta = (TermApp)lhs;
+
+ while (true) {
+ //The head, normalized to a function term
+ Expr h = ta.head.evalStep(ctxt);
+ //The constant or variable initially used for the head.
+ Expr pre = ta.head;
+
+ //TODO: we really need to loop here, evaluating the head
+ //one step at a time until normalization, generating an
+ //error message if any intermediate form is not a constant.
+ //We only need to establish a correspondence between the
+ //initial const and the recursive variable of the normal form.
+
+ // If the head does not normalize to a function, we cannot
+ // instantiate it, so we cannot unjoin this term app.
+ if (h.construct != FUN_TERM) {
+ handleError(ctxt,
+ "The left hand side of an unjoin scrutinee " +
+ "evaluates to a term app whose head is not a function.\n" +
+ "1. lhs:" + lhs.toString(ctxt) + "\n" +
+ "2. evaluated lhs: " + h.toString(ctxt) + "\n"
+ );
+ }
+
+ // The pre-instantiated value of the head.
+ FunTerm f = (FunTerm)h;
+ // A variable used to instantiate the head
+ FunTerm inst = f;
+
+ // Apply all arguments except last.
+ for (int i = 0; i < ta.X.length-1; ++i)
+ inst = (FunTerm)inst.substituteForParam(ta.X[i]);
+
+ // Apply last argument.
+ // Instantiating a function with one argument may result in an
+ // arbitrary term, so we need to use an Expr rather than
+ // a FunTerm to hold the result.
+ Expr fullInstantiation = inst.substituteForParam(ta.X[ta.X.length-1]);
+
+ // If we are unjoining an application of a recursive, top-level
+ // function, we substitute the function's constant for occurrences
+ // of the function's recursive variable in the body.
+ //
+ // This way, any facts deduced about recursive calls will mention
+ // the constant which, unlike the recursive variable, is accessible
+ // via the current context.
+ if (f.r != null && pre.construct == CONST)
+ fullInstantiation = (Expr)fullInstantiation.subst((Const)pre, f.r);
+
+
+ //TODO: substitute lets and abbrevs here?
+
+ if (fullInstantiation.construct != TERM_APP)
+ return fullInstantiation;
+
+ ta = (TermApp)fullInstantiation;
+ }
}
-// private boolean covers(VarListExpr parsedPath, Vector unjoinedPath)
-// {
-// int parsedPathInd = 0;
-//
-// while(parsedPathInd < parsedPath.vars.length)
-// {
-//
-// }
-// }
-
+ // Checks that each parsed path (a forall proof) can eliminate the
+ // corresponding unjoined path (and exists proof), and that every such
+ // elimination proves the same formula. Guru terminates with an error
+ // if any of these checks fail.
+ //
+ // Returns the formula which the eliminations prove. This formula
+ // is the classifier for the unjoin construct.
+ private Expr classifyPaths(Vector unjoinedPaths, Context ctxt)
+ {
+ Expr [] pathClassifiers = new Expr[paths.size()];
+ for (int i = 0; i < paths.size(); ++i)
+ {
+ Foralli parsedPath = (Foralli)paths.get(i);
+ Stack unjoinedPath = (Stack)unjoinedPaths.get(i);
+
+ //convert unjoined path into a exists
+ Var[] unjoinVars = new Var[unjoinedPath.size()-1];
+ Expr[] unjoinTypes = new Expr[unjoinedPath.size()-1];
+ for(int j = 0; j < unjoinedPath.size()-1; ++j)
+ {
+ unjoinVars[j] = ((UnjoinIntro)unjoinedPath.get(j)).introVar;
+ unjoinTypes[j] = ((UnjoinIntro)unjoinedPath.get(j)).introVarType;
+ }
+
+ Expr body = ((UnjoinIntro)unjoinedPath.lastElement()).introVarType;
+ assert(body.isFormula(ctxt));
+ Exists unjoinedExists = new Exists(unjoinVars,unjoinTypes,body);
+ Var existsVar = new Var("path " + Integer.toString(i));
+ ctxt.setClassifier(existsVar, unjoinedExists);
+
+ Existse eliminator = new Existse(existsVar, parsedPath);
+ eliminator.pos = parsedPath.pos;
+ pathClassifiers[i] = eliminator.classify(ctxt);
+ }
+
+ for(int i = 1; i < pathClassifiers.length; ++i) {
+ if (!pathClassifiers[i].defEq(ctxt, pathClassifiers[0])) {
+ handleError(ctxt, "unjoin path classifiers do not match");
+ }
+ }
+
+ return pathClassifiers[0];
+ }
+
+ //Expr override
public Expr classify(Context ctxt) {
Expr cScrutProof = scrutineeProof.classify(ctxt);
@@ -53,10 +270,9 @@
System.exit(0);
}
- scrutinee = (Atom)cScrutProof;
-
- if (!scrutinee.Y2.isI(ctxt))
- {
+ Atom scrutinee = (Atom)cScrutProof;
+
+ if (!scrutinee.Y2.isI(ctxt)) {
handleError(ctxt,
"Right hand side of unjoin scrutinee classifier is not" +
"a value.\n" +
@@ -66,91 +282,28 @@
System.exit(0);
}
- UnjoinDeduction deduction = scrutinee.Y1.Unjoin(
- scrutinee.Y2,
- new UnjoinContext(ctxt),
+
+ Expr instantiated = instantiate(ctxt, scrutinee.Y1);
+ instantiated = ctxt.lemmaSet.instantiate(instantiated);
+
+ UnjoinDeduction deduction = instantiated.Unjoin(
+ scrutinee.Y2,
+ 0,
ctxt,
scrutinee.equality
);
-
- List unjoinPaths = UnjoinDeduction.Flatten(deduction, ctxt);
-
- Iterator it = unjoinPaths.iterator();
- while(it.hasNext())
- {
- if (((Stack)it.next()).size() == 0)
- it.remove();
- }
-
- if (unjoinPaths.size() != paths.size())
- {
+ Vector unjoinPaths = UnjoinDeduction.Flatten(deduction, ctxt);
+
+ if (unjoinPaths.size() != paths.size()) {
//TODO: spit out error message, remove assert
DumpUnjoinPaths(unjoinPaths, ctxt);
handleError(ctxt, "blaaarg!");
assert(false);
System.exit(0);
}
-
-// Expr [] pathClassifiers = new Expr[paths.size()];
-//
-// for (int i = 0; i < paths.size(); ++i)
-// {
-// Foralli parsedPath = (Foralli)paths.get(i);
-//
-// Iterator it = unjoinPaths.iterator();
-// while (it.hasNext())
-// {
-// Stack unjoinedPath = (Stack)it.next();
-//
-// // If the parsed path is a subsequence of the
-// // unjoined path, we consider the parsed path adequate
-// // and remove the unjoined path.
-//
-//
-//
-// }
-// }
-
- Expr [] pathClassifiers = new Expr[paths.size()];
- for (int i = 0; i < paths.size(); ++i)
- {
- Foralli parsedPath = (Foralli)paths.get(i);
- Stack unjoinedPath = (Stack)unjoinPaths.get(i);
-
- //convert unjoined path into a exists
- Var[] unjoinVars = new Var[unjoinedPath.size()-1];
- Expr[] unjoinTypes = new Expr[unjoinedPath.size()-1];
- for(int j = 0; j < unjoinedPath.size()-1; ++j)
- {
- unjoinVars[j] = ((UnjoinIntro)unjoinedPath.get(j)).introVar;
- unjoinTypes[j] = ((UnjoinIntro)unjoinedPath.get(j)).introVarType;
- }
-
- Expr body = ((UnjoinIntro)unjoinedPath.lastElement()).introVarType;
- assert(body.isFormula(ctxt));
- Exists unjoinedExists = new Exists(unjoinVars,unjoinTypes,body);
- Var existsVar = new Var("path " + Integer.toString(i));
- ctxt.setClassifier(existsVar, unjoinedExists);
-
- //TODO: Might be able to compare the paths here to get
- //better error message
-
- Existse eliminator = new Existse(existsVar, parsedPath);
- eliminator.pos = parsedPath.pos;
- pathClassifiers[i] = eliminator.classify(ctxt);
- }
-
- for(int i = 1; i < pathClassifiers.length; ++i)
- {
- if (!pathClassifiers[i].defEq(ctxt, pathClassifiers[0]))
- {
- handleError(ctxt, "unjoin path classifiers do not match");
- System.exit(0);
- }
- }
-
- return pathClassifiers[0];
+
+ return classifyPaths(unjoinPaths, ctxt);
}
public void checkTermination(Context ctxt, Expr IH, int arg, Var[]
vars) {
@@ -160,14 +313,11 @@
private void DumpUnjoinPaths(List unjoinPaths, Context ctxt)
{
- for(int i = 0; i < unjoinPaths.size(); ++i)
- {
+ for(int i = 0; i < unjoinPaths.size(); ++i) {
String pathString = "";
Stack path = (Stack)unjoinPaths.get(i);
- for(int j = 0; j < path.size(); ++j)
- {
- UnjoinIntro u = (UnjoinIntro)path.get(j);
-
+ for(int j = 0; j < path.size(); ++j) {
+ UnjoinIntro u = (UnjoinIntro)path.get(j);
pathString += "(" + u.introVar.toString(ctxt) + " : " +
u.introVarType.toString(ctxt) + ")";
}
@@ -178,20 +328,26 @@
// Expr override
public int numOcc(Expr e) {
- // TODO Auto-generated method stub
- return 0;
+ int ret = 0;
+ ret += scrutineeProof.numOcc(e);
+ for (int i = 0; i < paths.size(); ++i)
+ ret += ((Foralli)paths.get(i)).numOcc(e);
+ return ret;
}
// Expr override
public Expr subst(Expr e, Expr x) {
- // TODO Auto-generated method stub
- return null;
+ Vector retPaths = new Vector(paths.size());
+
+ for (int i = 0; i < paths.size(); ++i)
+ retPaths.set(i, ((Foralli)paths.get(i)).subst(e, x));
+
+ return new Unjoin(scrutineeProof.subst(e,x), retPaths);
}
// Expr override
public Expr dropAnnos(Context ctxt) {
- // TODO Auto-generated method stub
- return null;
+ return new Bang();
}
}
=======================================
--- /branches/1.0/guru/UnjoinContext.java Fri Oct 21 12:38:46 2011
+++ /branches/1.0/guru/UnjoinContext.java Thu Oct 27 08:11:15 2011
@@ -11,87 +11,18 @@
// to keep track of equational facts that we have discovered so that we
// can use them to prevent unnecessary nondeterminism and getting stuck.
public class UnjoinContext {
- //The context that the unjoin proof is being classified under.
- private final Context baseContext;
-
- // A set of lemmas that may be used for rewriting and simplification.
- public final LemmaSet lemmaSet;
-
- // A set of the names of all variables encountered so far.
- private final HashSet varNames;
-
- // Whenever we expand a constant that contains a recursive function as
- // an immediate subterm, we map (in funcVarToConst) the variable
representing
- // the recursive function to the constant. This allows us to refer to the
- // constant rather than the variable in our deduced formulas.
- private final HashMap funcVarToConst;
-
- // The set of all variables that correspond to recursive function calls.
- // We keep track of these so that we don't expand them while unjoining.
- // TODO: can we prove things about a function inside its own body?
- private final HashSet recFuncVars;
-
- public UnjoinContext(Context baseContext) {
- this.baseContext = baseContext;
- lemmaSet = baseContext.lemmaSet.copy();
- varNames = new HashSet();
- funcVarToConst = new HashMap();
- recFuncVars = new HashSet();
- }
-
- public void setFuncConst(Var v, Const c) {
- assert(!funcVarToConst.containsKey(v));
- assert(!funcVarToConst.containsValue(c));
- funcVarToConst.put(v, c);
- }
-
- public Const getFuncConst(Var v)
- {
- return (Const)funcVarToConst.get(v);
- }
-
- public void removeFuncConst(Var v) {
- assert(funcVarToConst.containsKey(v));
- funcVarToConst.remove(v);
- }
-
- public void addRecFuncVar(Var v) {
- assert(!recFuncVars.contains(v));
- recFuncVars.add(v);
- }
-
- public boolean hasRecFuncVar(Var v)
- {
- return recFuncVars.contains(v);
- }
-
- public void removeRecFuncVar(Var v) {
- assert(recFuncVars.contains(v));
- recFuncVars.remove(v);
- }
-
- // Generates a name for a variable introduction. If the suggested name
- // has not already been used on this execution path, we use it. Otherwise,
- // we add primes to the end of the suggestion until no
currently-introduced
- // variable has a matching name.
- public String genName(String suggestion) {
- assert(suggestion != null);
-
- String currentCandidate = suggestion;
- boolean alreadyUsed = varNames.contains(currentCandidate);
-
- while (alreadyUsed) {
- currentCandidate += "'";
- alreadyUsed = varNames.contains(currentCandidate);
- }
-
- varNames.add(currentCandidate);
- return currentCandidate;
- }
-
- // Remove a name for the varNames set
- public void removeName(String name) {
- assert(varNames.contains(name));
- varNames.remove(name);
- }
-}
+
+ // Counts the number of proof variables in the current unjoin path.
+ // Whenever we introduce a new proof variable, we append the current value
+ // of proofCounter onto the name of the new variable in order to make it
+ // unique.
+ public int proofCounter;
+
+ // The recursive variable of the function being unjoined.
+ // If this is null, then we are not unjoining an application of a
recursive,
+ // top-level function, or it hasn't been set yet.
+ public Var recVar;
+
+ // The constant representing the function being unjoined.
+ public Const recConst;
+}
=======================================
--- /branches/1.0/guru/UnjoinContradiction.java Wed Oct 12 12:15:28 2011
+++ /branches/1.0/guru/UnjoinContradiction.java Thu Oct 27 08:11:15 2011
@@ -2,6 +2,8 @@
import java.util.ArrayList;
+//
+//
public class UnjoinContradiction extends UnjoinDeduction {
public static int count = 0;
=======================================
--- /branches/1.0/guru/UnjoinDeduction.java Fri Oct 21 12:38:46 2011
+++ /branches/1.0/guru/UnjoinDeduction.java Thu Oct 27 08:11:15 2011
@@ -2,6 +2,18 @@
import java.util.*;
+/*
+ * A heterogenous tree containing nodes of the following types:
+ * - Introduction, which asserts the existence of a expression having a
specified classifier
+ * - Or, which introduces nondeterminism
+ * - Contradiction, which asserts false
+ * - Empty, which asserts true
+ *
+ * UnjoinDeductions are produced by Expr.Unjoin, and have the property that
+ * all of the assertions from some root-to-leaf path must hold if the some
+ * instantiation of the expression being unjoined can join with the target
under
+ * the given context.
+ */
public abstract class UnjoinDeduction {
public static final int INTRO = 0;
@@ -9,9 +21,14 @@
public static final int EMPTY = 2;
public static final int CONTRADICTION = 3;
+ // An UnjoinDeduction which asserts false
public static final UnjoinDeduction contradiction = new
UnjoinContradiction();
+
+ // An UnjoinDeduction which asserts true
public static final UnjoinDeduction empty = new UnjoinEmpty();
+ // Returns an int identifying the type of this deduction node:
+ // INTRO, OR, EMPTY, or CONTRADICTION
abstract public int GetDeductionType();
static public UnjoinDeduction Simplify(UnjoinDeduction target)
@@ -49,108 +66,12 @@
return null;
}
- static public UnjoinDeduction FancyAppend(
- UnjoinDeduction baseDeduction,
- Expr startTerm,
- Expr target,
- UnjoinContext uCtxt,
- Context baseCtxt,
- boolean eq
- )
- {
- switch (baseDeduction.GetDeductionType())
- {
- case INTRO:
- UnjoinIntro intro = (UnjoinIntro)baseDeduction;
-
- //okay... basically, I need to collapse contradictory
- //paths, as I was originally planning to do, so that
- //I can add everything to the context here.
- if (intro.introVarType.construct == Expr.ATOM)
- uCtxt.lemmaSet.addLemma(intro.introVarType);
- else if (intro.introVarType.isTypeOrKind(baseCtxt))
- baseCtxt.setClassifier(intro.introVar, intro.introVarType);
-
- UnjoinDeduction ret = new UnjoinIntro(
- intro.introVar,
- intro.introVarType,
- FancyAppend(
- intro.rest,
- startTerm,
- target,
- uCtxt,
- baseCtxt,
- eq
- )
- );
-
- if (intro.introVarType.construct == Expr.ATOM)
- uCtxt.lemmaSet.removeLemma(intro.introVarType);
-
- return ret;
- case OR:
- UnjoinOr or = (UnjoinOr)baseDeduction;
-
- UnjoinDeduction d0 = FancyAppend(
- or.d0,
- startTerm,
- target,
- uCtxt,
- baseCtxt,
- eq
- );
-
- UnjoinDeduction d1 = FancyAppend(
- or.d1,
- startTerm,
- target,
- uCtxt,
- baseCtxt,
- eq
- );
-
- return new UnjoinOr(d0, d1);
- case CONTRADICTION:
- return contradiction;
- case EMPTY:
- return startTerm.Unjoin(target, uCtxt, baseCtxt, eq);
- }
-
- assert(false);
- return null;
- }
-
- static public UnjoinDeduction Append(
- UnjoinDeduction appendThis,
- UnjoinDeduction ontoThis
- )
- {
- switch (ontoThis.GetDeductionType())
- {
- case INTRO:
- UnjoinIntro intro = (UnjoinIntro)ontoThis;
- return new UnjoinIntro(
- intro.introVar,
- intro.introVarType,
- Append(appendThis, ((UnjoinIntro)ontoThis).rest)
- );
- case OR:
- UnjoinOr or = (UnjoinOr)ontoThis;
- return new UnjoinOr(Append(appendThis, or.d0), Append(appendThis,
or.d1));
- case CONTRADICTION:
- return contradiction;
- case EMPTY:
- return appendThis;
- }
-
- assert(false);
- return null;
- }
-
- static private void FlattenDfs(
+ // Backtrack through the given deduction, inserting a copy of
+ // each root-to-leaf path into the paths vector.
+ static private void FlattenAux(
UnjoinDeduction currDeduction,
Stack currPathDeduction,
- List paths
+ Vector paths
)
{
switch (currDeduction.GetDeductionType())
@@ -158,13 +79,13 @@
case INTRO:
UnjoinIntro intro = (UnjoinIntro)currDeduction;
currPathDeduction.push(intro);
- FlattenDfs(intro.rest, currPathDeduction, paths);
+ FlattenAux(intro.rest, currPathDeduction, paths);
currPathDeduction.pop();
return;
case OR:
UnjoinOr or = (UnjoinOr)currDeduction;
- FlattenDfs(or.d0, currPathDeduction, paths);
- FlattenDfs(or.d1, currPathDeduction, paths);
+ FlattenAux(or.d0, currPathDeduction, paths);
+ FlattenAux(or.d1, currPathDeduction, paths);
return;
case CONTRADICTION:
return;
@@ -177,13 +98,12 @@
// Returns a vector containing, for each evaluation path, an array of
// UnjoinIntro values which describe variables deduced to exist in the
case
// of an execution of that path.
- static public List Flatten(UnjoinDeduction deduction, Context ctxt)
+ static public Vector Flatten(UnjoinDeduction deduction, Context ctxt)
{
Stack deductions = new Stack();
- List paths = new Vector();
-
- //Get a list existentially quantified variables for each eval path
- FlattenDfs(deduction, deductions, paths);
+ Vector paths = new Vector();
+
+ FlattenAux(deduction, deductions, paths);
return paths;
}
=======================================
--- /branches/1.0/guru/Var.java Wed Oct 12 12:15:28 2011
+++ /branches/1.0/guru/Var.java Thu Oct 27 08:11:15 2011
@@ -158,14 +158,16 @@
public UnjoinDeduction Unjoin(
Expr target,
- UnjoinContext uCtxt,
+ int proofCount,
Context baseCtxt,
boolean eq
)
{
if (baseCtxt.isMacroDefined(this))
{
- return evalStep(baseCtxt).Unjoin(target, uCtxt, baseCtxt, eq);
+ //TODO: this should be removed... abbrevs should be substituted
+ //before unjoining.
+ return evalStep(baseCtxt).Unjoin(target, proofCount, baseCtxt, eq);
}
else
{