[guru-lang] r542 committed - added a very rough implementation for an upcoming proof construct call...
guru...@googlecode.com
Author: kevinclancy0
Date: Wed Oct 12 12:15:28 2011
Log: added a very rough implementation for an upcoming proof construct
called unjoin. Don't worry; I plan to clean this up. Fixed some bugs in
lemma and ascription.
http://code.google.com/p/guru-lang/source/detail?r=542
Added:
/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/UnjoinEmpty.java
/branches/1.0/guru/UnjoinIntro.java
/branches/1.0/guru/UnjoinOr.java
/branches/1.0/tests/unjoin.g
Modified:
/branches/1.0/guru/Ascription.java
/branches/1.0/guru/Const.java
/branches/1.0/guru/Expr.java
/branches/1.0/guru/FunTerm.java
/branches/1.0/guru/Lemma.java
/branches/1.0/guru/LemmaMark.java
/branches/1.0/guru/LemmaSet.java
/branches/1.0/guru/Let.java
/branches/1.0/guru/Match.java
/branches/1.0/guru/Parser.java
/branches/1.0/guru/TermApp.java
/branches/1.0/guru/Var.java
=======================================
--- /dev/null
+++ /branches/1.0/guru/Unjoin.java Wed Oct 12 12:15:28 2011
@@ -0,0 +1,197 @@
+package guru;
+
+import java.io.PrintStream;
+import java.util.*;
+
+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 Unjoin(Expr scrutineeProof, Vector paths)
+ {
+ super(UNJOIN);
+
+ this.scrutineeProof = scrutineeProof;
+ this.paths = paths;
+ }
+
+ // Expr override
+ protected void do_print(PrintStream w, Context ctxt) {
+ // TODO Auto-generated method stub
+
+ }
+
+// private boolean covers(VarListExpr parsedPath, Vector unjoinedPath)
+// {
+// int parsedPathInd = 0;
+//
+// while(parsedPathInd < parsedPath.vars.length)
+// {
+//
+// }
+// }
+
+ 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);
+ }
+
+ 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);
+ }
+
+ UnjoinDeduction deduction = scrutinee.Y1.Unjoin(
+ scrutinee.Y2,
+ new UnjoinContext(ctxt),
+ 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())
+ {
+ //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];
+ }
+
+ public void checkTermination(Context ctxt, Expr IH, int arg, Var[]
vars) {
+ for (int i = 0; i < paths.size(); ++i)
+ ((Foralli)paths.get(i)).checkTermination(ctxt,IH,arg,vars);
+ }
+
+ 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);
+ }
+ }
+
+ // Expr override
+ public int numOcc(Expr e) {
+ // TODO Auto-generated method stub
+ return 0;
+ }
+
+ // Expr override
+ public Expr subst(Expr e, Expr x) {
+ // TODO Auto-generated method stub
+ return null;
+ }
+
+ // Expr override
+ public Expr dropAnnos(Context ctxt) {
+ // TODO Auto-generated method stub
+ return null;
+ }
+
+}
=======================================
--- /dev/null
+++ /branches/1.0/guru/UnjoinContext.java Wed Oct 12 12:15:28 2011
@@ -0,0 +1,99 @@
+package guru;
+
+import java.util.HashSet;
+import java.util.HashMap;
+
+//TODO: comment all methods
+
+// When we unjoin a term, we need to have information about the execution
+// path that lead to the term. For example, we need to keep track of the
names
+// of variables introduced so that we don't have any duplicates. We also
need
+// 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);
+ alreadyUsed |= (baseContext.lookup(currentCandidate) != null);
+
+ while (alreadyUsed) {
+ currentCandidate += "'";
+ alreadyUsed = varNames.contains(currentCandidate);
+ alreadyUsed |= (baseContext.lookup(currentCandidate) != null);
+ }
+
+ varNames.add(currentCandidate);
+ return currentCandidate;
+ }
+
+ // Remove a name for the varNames set
+ public void removeName(String name) {
+ assert(varNames.contains(name));
+ varNames.remove(name);
+ }
+}
=======================================
--- /dev/null
+++ /branches/1.0/guru/UnjoinContradiction.java Wed Oct 12 12:15:28 2011
@@ -0,0 +1,20 @@
+package guru;
+
+import java.util.ArrayList;
+
+public class UnjoinContradiction extends UnjoinDeduction {
+
+ public static int count = 0;
+
+ public UnjoinContradiction()
+ {
+ count++;
+ assert(count <= 1);
+ }
+
+ public int GetDeductionType()
+ {
+ return CONTRADICTION;
+ }
+
+}
=======================================
--- /dev/null
+++ /branches/1.0/guru/UnjoinDeduction.java Wed Oct 12 12:15:28 2011
@@ -0,0 +1,79 @@
+package guru;
+
+import java.util.*;
+
+public abstract class UnjoinDeduction {
+
+ public static final int INTRO = 0;
+ public static final int OR = 1;
+ public static final int EMPTY = 2;
+ public static final int CONTRADICTION = 3;
+
+ public static final UnjoinDeduction contradiction = new
UnjoinContradiction();
+ public static final UnjoinDeduction empty = new UnjoinEmpty();
+
+ abstract public int GetDeductionType();
+
+ static public UnjoinDeduction Append(
+ UnjoinDeduction appendThis,
+ UnjoinDeduction ontoThis
+ )
+ {
+ switch (ontoThis.GetDeductionType())
+ {
+ case INTRO:
+ return 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(
+ UnjoinDeduction currDeduction,
+ Stack currPathDeduction,
+ List paths
+ )
+ {
+ switch (currDeduction.GetDeductionType())
+ {
+ case INTRO:
+ UnjoinIntro intro = (UnjoinIntro)currDeduction;
+ currPathDeduction.push(intro);
+ FlattenDfs(intro.rest, currPathDeduction, paths);
+ currPathDeduction.pop();
+ return;
+ case OR:
+ UnjoinOr or = (UnjoinOr)currDeduction;
+ FlattenDfs(or.d0, currPathDeduction, paths);
+ FlattenDfs(or.d1, currPathDeduction, paths);
+ return;
+ case CONTRADICTION:
+ return;
+ case EMPTY:
+ paths.add(currPathDeduction.clone());
+ return;
+ }
+ }
+
+ // 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)
+ {
+ Stack deductions = new Stack();
+ List paths = new Vector();
+
+ //Get a list existentially quantified variables for each eval path
+ FlattenDfs(deduction, deductions, paths);
+
+ return paths;
+ }
+}
=======================================
--- /dev/null
+++ /branches/1.0/guru/UnjoinEmpty.java Wed Oct 12 12:15:28 2011
@@ -0,0 +1,16 @@
+package guru;
+
+public class UnjoinEmpty extends UnjoinDeduction {
+
+ private static int count = 0;
+
+ public UnjoinEmpty() {
+ count++;
+ assert(count <= 1);
+ }
+
+ public int GetDeductionType()
+ {
+ return EMPTY;
+ }
+}
=======================================
--- /dev/null
+++ /branches/1.0/guru/UnjoinIntro.java Wed Oct 12 12:15:28 2011
@@ -0,0 +1,25 @@
+package guru;
+
+import java.util.ArrayList;
+
+public class UnjoinIntro extends UnjoinDeduction {
+
+ public final Var introVar;
+ public final Expr introVarType;
+ public final UnjoinDeduction rest;
+
+ public UnjoinIntro(Var introVar, Expr introVarType, UnjoinDeduction rest)
{
+ assert(introVar != null);
+ assert(introVarType != null);
+ assert(rest != null);
+
+ this.introVar = introVar;
+ this.introVarType = introVarType;
+ this.rest = rest;
+ }
+
+ public int GetDeductionType()
+ {
+ return INTRO;
+ }
+}
=======================================
--- /dev/null
+++ /branches/1.0/guru/UnjoinOr.java Wed Oct 12 12:15:28 2011
@@ -0,0 +1,29 @@
+package guru;
+
+import java.util.ArrayList;
+
+public class UnjoinOr extends UnjoinDeduction {
+
+ public final UnjoinDeduction d0;
+ public final UnjoinDeduction d1;
+
+ public UnjoinOr(UnjoinDeduction d0, UnjoinDeduction d1) {
+ assert(d0 != null);
+ assert(d1 != null);
+
+ this.d0 = d0;
+ this.d1 = d1;
+ }
+
+ public UnjoinDeduction Or(UnjoinDeduction deduction) {
+ if (deduction == contradiction)
+ return this;
+
+ return new UnjoinOr(deduction, this);
+ }
+
+ public int GetDeductionType()
+ {
+ return OR;
+ }
+}
=======================================
--- /dev/null
+++ /branches/1.0/tests/unjoin.g Wed Oct 12 12:15:28 2011
@@ -0,0 +1,194 @@
+
+Include "../lib/nat.g"
+Include "../lib/bool.g"
+Include "../lib/minus.g"
+
+%-
+Define myproof :=
+ foralli(a b : nat)(x:{ (lt a b) = tt } ).
+ unjoin x by with
+ | foralli(p2 : { a = Z })(b' : nat)(p1 : { b = (S b') }).
+ trans : { b = (S b') } p1
+ : { (S b') != Z } clash (S b') Z
+ | foralli(a' : nat)(p5 : { a = (S a') })(b' : nat)(p4 : { b = (S b') })
+ (u : { (lt a' b') = tt }).
+ trans : { b = (S b') } p4
+ : { (S b') != Z } clash (S b') Z
+ end.
+-%
+
+ %-
+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
+ -%
+Define eqnatEq2 : 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 by with
+ | foralli(p0 : { m = Z }).
+ trans : { n = Z } n_eq
+ : { Z = m } symm p0
+ end
+ | S z' =>
+ foralli(m: nat)(u : { (eqnat n m) = tt }).
+ lemma n_eq in
+ unjoin u by with
+ | foralli(n' : nat)(p4 : { z' = n' })(m' : nat)(p3 : { m = (S m') })
+ (u : { (eqnat n' m') = tt }).
+ lemma
+ : { (eqnat z' m') = tt }
+ trans : { (eqnat z' m') = (eqnat n' m') } cong (eqnat * m') p4
+ : { (eqnat n' m') = tt } u
+ in
+
+ hypjoin n m by
+ : { z' = m' } [n_IH z' m' ##]
+ : { m = (S m') } p3
+ : { n = (S z') } n_eq
+ end
+ end
+ end.
+
+%-
+Define minus_lt2 : Forall
+ (a b:nat)(u1:{ (le b a) = tt })(u2:{ (lt Z b) = tt }).{ (lt (minus a b)
a) = tt }
+ :=
+ foralli(a: nat).
+ induction (b:nat) return
+ Forall(u1:{ (le b a) = tt })(u2:{ (lt Z b) = tt }).{ (lt (minus a b)
a) = tt }
+ with
+ | default nat =>
+ foralli(u1:{ (le b a) = tt })(u2:{ (lt Z b) = tt }).
+ unjoin u2 by with
+ | foralli(b' : nat)(b_eq : { b = (S b') }).
+ lemma b_eq in
+ unjoin u1 by with
+ | foralli(n' : nat)(a' : nat)(a_eq : { a = (S a') })(u : { (eqnat
n' a') = tt }).
+ lemma
+ : { (minus a b) = (minus a' b') }
+ hypjoin (minus a b) (minus a' b') by a_eq b_eq end
+ in
+ case b' with
+ | Z =>
+ lemma
+ : { (minus a b) = a' }
+ trans : { (minus a b) = (minus a' b') } ##
+ trans : { (minus a' b') = (minus a' Z) } cong (minus a'
*) b'_eq
+ : { (minus a' Z) = a' } join (minus a' Z) a'
+ in
+ hypjoin (lt (minus a b) a) tt by
+ : { (minus a b) = a' } ##
+ : { a = (S a') } a_eq
+ : { (lt a' (S a')) = tt } [lt_S a']
+ end
+ | S b'' =>
+ abbrev x = (minus a (S b')) in
+ lemma
+ : { (lt Z b') = tt }
+ hypjoin (lt Z b') tt by b'_eq end
+
+ : { (lt b' b) = tt }
+ transs
+ : { (lt b' b) = (lt b' (S b')) } cong (lt b' *) b_eq
+ : { (lt b' (S b')) = tt } [lt_S b']
+ end
+
+ : { (lt b' a) = tt }
+ [ltle_trans b' b a ## u1]
+
+ : { (le b' a) = tt }
+ [lt_implies_le b' a ##]
+
+
+ : { (lt (S x) a) = tt }
+ hypjoin (lt (S x) a ) tt by
+ : { (minus a b') = (S x) } [minusS2 a b' ##]
+ : { (lt (minus a b') a) = tt } [b_IH b' ## ##]
+ end
+
+ : { (lt x a) = tt }
+ [lt_trans x (S x) a [lt_S x] ##]
+ in
+
+ hypjoin (lt (minus a b) a) tt by
+ : { (lt x a) = tt } ##
+ : { b = (S b') } b_eq
+ end
+ end
+ end
+ end
+ end.
+-%
+
+%-
+ | Z =>
+ foralli(u1:{ (le b a) = tt })(u2:{ (lt Z b) = tt }).
+ contra
+ trans symm b_eq
+ [lt_implies_not_zero Z b u2]
+
+ { (lt (minus a b) a) = tt }
+ | S b' =>
+ foralli(u1:{ (le b a) = tt })(u2:{ (lt Z b) = tt }).
+
+ case a with
+ | Z =>
+ contra
+ abbrev Z_lt_a = [ltle_trans Z b a u2 u1] in
+ trans [lt_implies_not_zero Z a Z_lt_a]
+ symm a_eq
+
+ { (lt (minus a b) a) = tt }
+ | S a' =>
+ abbrev stripped =
+ hypjoin (minus a b) (minus a' b') by a_eq b_eq end
+ in
+ case b' with
+ | Z =>
+ abbrev a_minus_b_eq_a' =
+ trans stripped
+ trans cong (minus a' *) b'_eq
+ join (minus a' Z) a'
+ in
+ trans cong (lt * a) a_minus_b_eq_a'
+ trans cong (lt a' *) a_eq
+ [lt_S a']
+ | S b'' =>
+ abbrev z_lt_b' = hypjoin (lt Z b') tt by b'_eq end in
+ abbrev b'_lt_b =
+ trans cong (lt b' *) b_eq
+ [lt_S b']
+ in
+ abbrev b'_lt_a = [ltle_trans b' b a b'_lt_b u1] in
+ abbrev b'_le_a = [lt_implies_le b' a b'_lt_a] in
+ abbrev x = (minus a (S b')) in
+ abbrev Sx_lt_a =
+ trans cong (lt * a)
+ symm [minusS2 a b' b'_lt_a]
+ [b_IH b' b'_le_a z_lt_b']
+ in
+ abbrev x_lt_a = [lt_trans x (S x) a [lt_S x] Sx_lt_a] in
+
+ trans cong (lt * a)
+ hypjoin (minus a b) x by b_eq end
+ x_lt_a
+ end % b'
+ end % a
+ end. %b
+-%
+
+Classify eqnatEq.
=======================================
--- /branches/1.0/guru/Ascription.java Mon Sep 5 17:40:33 2011
+++ /branches/1.0/guru/Ascription.java Wed Oct 12 12:15:28 2011
@@ -87,7 +87,7 @@
// overridden from Expr
public Expr subst(Expr e, Expr x) {
- return new Ascription(target.subst(e,x), classifier.subst(e,x));
+ return new Ascription(classifier.subst(e,x), target.subst(e,x));
}
// overridden from Expr
=======================================
--- /branches/1.0/guru/Const.java Tue Sep 8 09:44:56 2009
+++ /branches/1.0/guru/Const.java Wed Oct 12 12:15:28 2011
@@ -123,6 +123,24 @@
+ "\n1. the constant: " + toString(ctxt));
}
}
+
+ public UnjoinDeduction Unjoin(
+ Expr target,
+ UnjoinContext uCtxt,
+ Context baseCtxt,
+ boolean eq
+ )
+ {
+ if (target.construct != CONST)
+ return eq ? UnjoinDeduction.contradiction : UnjoinDeduction.empty;
+
+ Const c = (Const)target;
+
+ if (this.name == c.name)
+ return eq ? UnjoinDeduction.empty : UnjoinDeduction.contradiction;
+ else
+ return eq ? UnjoinDeduction.contradiction : UnjoinDeduction.empty;
+ }
public guru.carraway.Expr toCarrawayType(Context ctxt, boolean rttype)
{
if (rttype) {
=======================================
--- /branches/1.0/guru/Expr.java Fri Aug 26 15:30:54 2011
+++ /branches/1.0/guru/Expr.java Wed Oct 12 12:15:28 2011
@@ -107,6 +107,7 @@
public static final int LEMMA_MARK = 91;
public static final int ASCRIPTION = 92;
+ public static final int UNJOIN = 93;
public static final int LAST = 200;
@@ -508,6 +509,7 @@
case CABBREV:
case ABBREV:
case JOIN:
+ case UNJOIN:
case EVAL:
case EVALTO:
case HYPJOIN:
@@ -773,6 +775,25 @@
public java.util.Set getDependences() {
return new TreeSet();
}
+
+ // Given a target term, target, and a set of enclosing functions calls,
+ // funCalls, returns an unjoin deduction representing all possible
+ // evaluation paths for this term which could result in joining with
+ // the target term. (If eq is false, then we instead return the set of
+ // all possible evaluation paths which do not join this term with the
+ // target term.)
+ public UnjoinDeduction Unjoin(
+ Expr target,
+ UnjoinContext uCtxt,
+ Context baseCtxt,
+ boolean eq
+ )
+ {
+ //Unjoin has not been implemented for this construct.
+ assert(false);
+
+ return null;
+ }
/*
* get all the constants in this Expr or in any Expr reachable by a
=======================================
--- /branches/1.0/guru/FunTerm.java Sun Apr 4 22:14:59 2010
+++ /branches/1.0/guru/FunTerm.java Wed Oct 12 12:15:28 2011
@@ -193,6 +193,16 @@
}
+ // substitutes the given expr for the first var in this abstraction.
+ // unlike the instantiate method, this does not expand fixpoints.
+ public Expr substituteForParam(Expr e)
+ {
+ Expr ret = super.instantiate(e);
+ if (ret.construct == ABSTRACTION)
+ return new FunTerm(null, null, (FunAbstraction)ret);
+ return ret;
+ }
+
// return the result of substituting the given expr for
// the first var in this abstraction.
public Expr instantiate(Expr e) {
@@ -300,7 +310,20 @@
body.checkSpec(ctxt, in_type, pos);
}
-
+
+ public UnjoinDeduction Unjoin(
+ Expr target,
+ HashSet funCalls,
+ Context ctxt,
+ boolean eq
+ )
+ {
+ // TODO: Maybe not consistent with how other values unjoin,
+ // but I think it would be weird to unjoin an abstraction.
+ assert(target.construct != FUN_TERM);
+ return UnjoinDeduction.contradiction;
+ }
+
// we assume r is non-null (Compile sets it if it is null).
public guru.carraway.Expr toCarraway(Context ctxt) {
guru.carraway.FunTerm F = new guru.carraway.FunTerm();
=======================================
--- /branches/1.0/guru/Lemma.java Mon Sep 5 17:40:33 2011
+++ /branches/1.0/guru/Lemma.java Wed Oct 12 12:15:28 2011
@@ -115,8 +115,7 @@
//Override from Expr
public Expr subst(Expr e, Expr x) {
//Lemmas are specificational; hence, this will not get called.
- assert(false);
- return null;
+ return new Lemma(lemmaProof.subst(e,x), body.subst(e,x));
}
public Expr dropAnnos(Context ctxt) {
=======================================
--- /branches/1.0/guru/LemmaMark.java Mon Sep 5 17:40:33 2011
+++ /branches/1.0/guru/LemmaMark.java Wed Oct 12 12:15:28 2011
@@ -88,11 +88,7 @@
}
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;
+ return this;
}
// Overridden from Expr.
=======================================
--- /branches/1.0/guru/LemmaSet.java Mon Aug 22 15:38:29 2011
+++ /branches/1.0/guru/LemmaSet.java Wed Oct 12 12:15:28 2011
@@ -18,7 +18,7 @@
// The context used to decide definitional equality
final private Context ctxt;
- // A set of definitionally unique formulas currently contained in this
lemma set.
+ // The set of definitionally unique formulas currently contained in this
lemma set.
final private ArrayList formulas;
public LemmaSet(Context ctxt)
@@ -34,7 +34,6 @@
// 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));
@@ -44,7 +43,6 @@
// Removes a lemma from the set.
public void removeLemma(Expr toRemove)
{
- assert(toRemove != null);
assert(toRemove.isFormula(ctxt));
assert(hasLemma(toRemove));
@@ -55,7 +53,6 @@
public boolean hasLemma(Expr lemma)
{
assert(lemma.isFormula(ctxt));
- assert(lemma != null);
ListIterator i = formulas.listIterator();
while(i.hasNext())
@@ -67,4 +64,99 @@
}
return false;
}
-}
+
+ // Returns a new lemma set containing exactly the same set of formulas as
+ // this one.
+ public LemmaSet copy()
+ {
+ LemmaSet ret = new LemmaSet(ctxt);
+
+ ListIterator i = formulas.listIterator();
+ while(i.hasNext())
+ ret.addLemma((Expr)i.next());
+
+ return ret;
+ }
+
+ public Expr simplify(Expr e)
+ {
+ Expr e_ = null;
+
+ while (e_ != e)
+ {
+ e_ = e;
+
+ if (e.construct == Expr.MATCH)
+ {
+ Match m = (Match)e;
+ Expr mt_ = simplify(m.t);
+ if (mt_ != m.t) {
+ e = new Match(
+ simplify(m.t),
+ m.x1,
+ m.x2,
+ m.T,
+ m.C,
+ m.consume_scrut
+ );
+ }
+ }
+
+ e = e.evalStep(ctxt);
+ e = rewrite(e);
+ }
+
+ return e;
+ }
+
+ private Expr rewrite(Expr e)
+ {
+ if (e.construct != Expr.VAR)
+ return e;
+
+ Var v = (Var)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 == v) {
+ if (a.Y2.construct == Expr.TERM_APP)
+ {
+ TermApp ta = (TermApp)a.Y2;
+
+ if (ta.head.construct == Expr.CONST &&
ctxt.isTermCtor((Const)ta.head))
+ return ta;
+ }
+ else if(a.Y2.construct == Expr.CONST)
+ {
+ return a.Y2;
+ }
+ }
+
+ if (a.Y2 == v && a.Y1.construct == Expr.TERM_APP) {
+ if (a.Y1.construct == Expr.TERM_APP)
+ {
+ TermApp ta = (TermApp)a.Y1;
+
+ if (ta.head.construct == Expr.CONST &&
ctxt.isTermCtor((Const)ta.head))
+ return ta;
+ }
+ else if(a.Y1.construct == Expr.CONST)
+ {
+ return a.Y1;
+ }
+ }
+ }
+
+ return v;
+ }
+}
=======================================
--- /branches/1.0/guru/Let.java Sun May 2 12:13:20 2010
+++ /branches/1.0/guru/Let.java Wed Oct 12 12:15:28 2011
@@ -166,6 +166,22 @@
t2.checkSpec(ctxt, in_type, pos);
}
+ // Overloaded from Expr
+ public UnjoinDeduction Unjoin(
+ Expr target,
+ HashSet funCalls,
+ Context ctxt,
+ boolean eq
+ )
+ {
+ return Unjoin(
+ t2.subst(t1, x1),
+ funCalls,
+ ctxt,
+ eq
+ );
+ }
+
public guru.carraway.Expr toCarraway(Context ctxt) {
guru.carraway.Let l = new guru.carraway.Let();
l.pos = pos;
=======================================
--- /branches/1.0/guru/Match.java Sun May 2 12:13:20 2010
+++ /branches/1.0/guru/Match.java Wed Oct 12 12:15:28 2011
@@ -158,7 +158,146 @@
C[i].checkSpec(ctxt, in_type, pos);
}
}
-
+
+ //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,
+ 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
+ //each branch.
+ for(int i = 0; i < C.length; ++i)
+ {
+ Case c = C[i];
+
+ if (t_.construct == TERM_APP)
+ {
+ TermApp ta = (TermApp)t_;
+
+ if (ta.head != c.c)
+ continue;
+ }
+ else if (t_.construct == CONST)
+ {
+ if (t_ != c.c)
+ continue;
+ }
+
+ // Prepend immediate deductions onto case body deductions -----
+ if (c.x.length == 0)
+ {
+ // Make deductions from case body -----
+ branch = c.body.Unjoin(
+ target,
+ uCtxt,
+ 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);
+ }
+ }
+ else
+ {
+ FunType consType =
(FunType)c.c.classify(baseCtxt).defExpandTop(baseCtxt);
+
+ // Create contstructor argument variable -----
+ Var[] clones = new Var[c.x.length];
+ Expr[] types = new Expr[c.x.length];
+
+ // A version of body for which variables corresponding to
+ // match arguments are replaced with their corresponding
+ // unjoin introductions.
+ Expr body = c.body;
+
+ int last = c.x.length-1;
+ for(int j = 0; j <= last; ++j)
+ {
+
+ clones[j] = new Var(uCtxt.genName(c.x[j].name));
+ types[j] = consType.types[0];
+
+ //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
+ // return type, which may not be a function type.
+ if (j != last)
+ consType = (FunType)consType.instantiate(clones[j]);
+ }
+
+ // Make deductions from case body -----
+ branch = body.Unjoin(
+ target,
+ uCtxt,
+ baseCtxt,
+ eq
+ );
+
+ for(int j = 0; j < c.x.length; ++j)
+ uCtxt.removeName(clones[j].name);
+
+ //prepend immediate deductions to case body deductions
+ 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);
+ }
+ else if (t_.construct == TERM_APP)
+ {
+ TermApp ta = (TermApp)t_;
+
+ for (int j = 0; j < ta.X.length; ++j)
+ {
+ Atom varEq = new Atom(true, ta.X[j], clones[j]);
+ Var varEqProof = new Var("p" + Integer.toString(varNum++));
+ branch = new UnjoinIntro(varEqProof, varEq, branch);
+ }
+ }
+
+ for (int j = c.x.length-1; j >= 0; --j)
+ branch = new UnjoinIntro(clones[j], types[j], branch);
+ }
+
+ if (t_.construct == MATCH)
+ {
+ UnjoinDeduction tDeduction = t_.Unjoin(
+ new TermApp(c.c,c.x),
+ uCtxt,
+ baseCtxt,
+ true
+ );
+
+ branch = UnjoinDeduction.Append(branch, tDeduction);
+ }
+
+ //Or the current return value with the deduction for the
+ //current branch (if ret is null, we set it to the current branch)
+ ret = new UnjoinOr(ret, branch);
+ }
+
+ return ret;
+ }
+
public guru.carraway.Expr toCarraway(Context ctxt) {
guru.carraway.Match m = new guru.carraway.Match();
m.pos = pos;
=======================================
--- /branches/1.0/guru/Parser.java Mon Sep 5 17:40:33 2011
+++ /branches/1.0/guru/Parser.java Wed Oct 12 12:15:28 2011
@@ -326,6 +326,9 @@
case Expr.WORD_EXPR:
e = readWordExpr();
break;
+ case Expr.UNJOIN:
+ e = readUnjoin();
+ break;
case Expr.LAST+STRING:
e = readStringExpr();
break;
@@ -449,6 +452,43 @@
}
+ protected Unjoin readUnjoin() throws IOException
+ {
+ if (!eat_ws())
+ handleError("Unexpected end of input parsing an unjoin proof.");
+
+ Expr scrutinee = readProof();
+
+ if (!eat_ws())
+ handleError("Unexpected end of input parsing an unjoin proof.");
+
+ eat("by", "unjoin proof");
+
+ if (!eat_ws())
+ handleError("Unexpected end of input parsing an unjoin proof.");
+
+ //TODO: read some lemmas and add them into the lemma set using
+ //lemma AST nodes.
+
+ eat("with", "unjoin proof");
+
+ if (!eat_ws())
+ handleError("Unexpected end of input parsing an unjoin proof.");
+
+ Vector paths = new Vector();
+ while (tryToEat("|"))
+ {
+ paths.add(readProof());
+
+ if (!eat_ws())
+ handleError("Unexpected end of input parsing an unjoin
proof.");
+ }
+
+ eat("end", "unjoin proof");
+
+ return new Unjoin(scrutinee, paths);
+ }
+
protected Set readSet() throws IOException
{
Set s = new Set();
@@ -2797,6 +2837,7 @@
keywordTree.add( "show", Expr.SHOW );
keywordTree.add( "contra", Expr.CONTRA );
keywordTree.add( "induction", Expr.INDUCTION );
+ keywordTree.add( "unjoin", Expr.UNJOIN );
keywordTree.add( "Forall", Expr.FORALL );
keywordTree.add( "Exists", Expr.EXISTS );
keywordTree.add( "{", Expr.ATOM );
=======================================
--- /branches/1.0/guru/TermApp.java Fri May 6 13:14:28 2011
+++ /branches/1.0/guru/TermApp.java Wed Oct 12 12:15:28 2011
@@ -513,6 +513,133 @@
else
X[i].getFreeVarsComputational(ctxt,vars);
}
+
+ public UnjoinDeduction Unjoin(
+ Expr target,
+ UnjoinContext uCtxt,
+ 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
+ );
+ }
+ }
public guru.carraway.Expr toCarraway(Context ctxt) {
if (head.construct == MATCH)
=======================================
--- /branches/1.0/guru/Var.java Sat Feb 13 11:17:14 2010
+++ /branches/1.0/guru/Var.java Wed Oct 12 12:15:28 2011
@@ -155,6 +155,26 @@
+ "1. the variable: " + toString(ctxt));
}
}
+
+ public UnjoinDeduction Unjoin(
+ Expr target,
+ UnjoinContext uCtxt,
+ Context baseCtxt,
+ boolean eq
+ )
+ {
+ if (baseCtxt.isMacroDefined(this))
+ {
+ return evalStep(baseCtxt).Unjoin(target, uCtxt, baseCtxt, eq);
+ }
+ else
+ {
+ if (target == this)
+ return eq ? UnjoinDeduction.empty : UnjoinDeduction.contradiction;
+ else
+ return eq ? UnjoinDeduction.contradiction : UnjoinDeduction.empty;
+ }
+ }
public guru.carraway.Expr toCarrawayType(Context ctxt, boolean rttype)
{
guru.carraway.Sym s = ctxt.carraway_ctxt.lookup(name);