[guru-lang] r548 committed - added plausibility testing
guru...@googlecode.com
Author: kevinclancy0
Date: Mon Nov 21 12:42:14 2011
Log: added plausibility testing
http://code.google.com/p/guru-lang/source/detail?r=548
Modified:
/branches/1.0/guru/Abort.java
/branches/1.0/guru/Match.java
/branches/1.0/guru/TermApp.java
/branches/1.0/guru/UnjoinBase.java
/branches/1.0/guru/UnjoinContext.java
/branches/1.0/tests/unjoin.g
=======================================
--- /branches/1.0/guru/Abort.java Sun May 2 09:11:33 2010
+++ /branches/1.0/guru/Abort.java Mon Nov 21 12:42:14 2011
@@ -104,5 +104,15 @@
e.pos = pos;
return e;
}
+
+ public UnjoinDeduction Unjoin(
+ Expr target,
+ UnjoinContext uctxt,
+ Context baseCtxt,
+ boolean eq
+ )
+ {
+ return UnjoinDeduction.contradiction;
+ }
}
=======================================
--- /branches/1.0/guru/Match.java Mon Nov 14 12:52:03 2011
+++ /branches/1.0/guru/Match.java Mon Nov 21 12:42:14 2011
@@ -203,6 +203,9 @@
// Prepend immediate deductions onto case body deductions -----
if (c.x.length == 0) {
+ if (!UnjoinBase.plausible(t_, c.c, uctxt, baseCtxt,true))
+ continue;
+
Atom matchEq = new Atom(true, t_, c.c);
Var matchEqVar = new Var("p" + uctxt.proofCounter);
=======================================
--- /branches/1.0/guru/TermApp.java Mon Nov 14 12:52:03 2011
+++ /branches/1.0/guru/TermApp.java Mon Nov 21 12:42:14 2011
@@ -521,44 +521,17 @@
boolean eq
)
{
- if (evalStep(baseCtxt) == this
&& !Unjoin.placeHolder(target,baseCtxt))
- {
- // A term constructor
-
- if (target.construct != TERM_APP)
- return eq ? UnjoinDeduction.contradiction :
UnjoinDeduction.empty;
- else
- {
- UnjoinDeduction ret = UnjoinDeduction.empty;
-
- for (int i = 0; i < X.length; ++i)
- {
- Atom introAtom = new Atom(eq, this, target);
- Var introVar = new Var("u");
-
- ret = new UnjoinIntro(
- introVar,
- introAtom,
- ret
- );
- }
-
- return ret;
- }
- }
- else
- {
- // A function call
- Atom introAtom = new Atom(eq, this, target);
- Var introVar = new Var("u");
-
- return new UnjoinIntro(
- introVar,
- introAtom,
- UnjoinDeduction.empty
- );
- }
-
+ if (!Unjoin.plausible(this,target,uctxt,baseCtxt,eq))
+ return UnjoinDeduction.contradiction;
+
+ Atom introAtom = new Atom(eq, this, target);
+ Var introVar = new Var("u");
+
+ return new UnjoinIntro(
+ introVar,
+ introAtom,
+ UnjoinDeduction.empty
+ );
}
public guru.carraway.Expr toCarraway(Context ctxt) {
=======================================
--- /branches/1.0/guru/UnjoinBase.java Mon Nov 14 12:52:03 2011
+++ /branches/1.0/guru/UnjoinBase.java Mon Nov 21 12:42:14 2011
@@ -30,6 +30,287 @@
return false;
}
+
+ class VarValue
+ {
+ public final Var var;
+ public final Expr classifier;
+
+ public VarValue(Var var, Expr classifier)
+ {
+ this.var = var;
+ this.classifier = classifier;
+ }
+ }
+
+ public static boolean plausible(
+ Expr term,
+ Expr target,
+ UnjoinContext uCtxt,
+ Context baseCtxt,
+ boolean eq
+ )
+ {
+ assert(eq == true);
+
+ target = uCtxt.lemmaSet.simplify(target);
+
+ if (target.construct == Expr.VAR)
+ return true;
+
+ switch (term.construct)
+ {
+ case Expr.TERM_APP:
+ TermApp taTerm = (TermApp)term;
+
+ if (taTerm.head.construct == CONST &&
baseCtxt.isCtor((Const)taTerm.head))
+ {
+ if (target.construct != TERM_APP)
+ return false;
+
+ TermApp taTarget = (TermApp)target;
+
+ if (taTarget.head != taTerm.head)
+ return false;
+
+
+ boolean ret = true;
+ for (int i = 0; i < taTerm.X.length; ++i)
+ {
+ ret = ret && plausible(
+ taTerm.X[i],
+ taTarget.X[i],
+ uCtxt,
+ baseCtxt,
+ eq
+ );
+ }
+
+ return ret;
+ }
+ else
+ {
+ if (taTerm.head.eval(baseCtxt).construct != Expr.FUN_TERM)
+ return true; // maybe it could be a variable
+
+ FunTerm inst = (FunTerm)taTerm.head.eval(baseCtxt);
+
+ Var oldRec = uCtxt.recVar;
+ uCtxt.recVar = inst.r;
+
+ // Apply all arguments except last.
+ for (int i = 0; i < taTerm.X.length-1; ++i)
+ inst = (FunTerm)inst.substituteForParam(taTerm.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 fullInst = inst.substituteForParam(taTerm.X[taTerm.X.length-1]);
+
+ boolean ret = plausible(
+ fullInst,
+ target,
+ uCtxt,
+ baseCtxt,
+ eq
+ );
+
+ uCtxt.recVar = oldRec;
+
+ return ret;
+ }
+ case Expr.FUN_TERM:
+ return target.construct == FUN_TERM;
+ case Expr.VAR:
+ return true;
+ case Expr.CONST:
+ if (term.evalStep(baseCtxt) != term) {
+ return plausible(
+ term.evalStep(baseCtxt),
+ target,
+ uCtxt,
+ baseCtxt,
+ eq
+ );
+ }
+
+ return target == term;
+ case Expr.MATCH:
+ Match m = (Match)term;
+ boolean ret = false;
+ Expr t_ = uCtxt.lemmaSet.simplify(m.t);
+ boolean branchPlausible;
+
+ Case[] C = m.C;
+
+ for(int i = 0; i < C.length; ++i)
+ {
+ Case c = C[i];
+
+ // We need to factor this out
+ boolean isScrutConstructor = t_.construct == TERM_APP;
+ if (isScrutConstructor)
+ isScrutConstructor &= ((TermApp)t_).head.construct == Expr.CONST;
+
+ if (isScrutConstructor)
+ isScrutConstructor &= baseCtxt.isTermCtor(
(Const)((TermApp)t_).head );
+
+ // If the case is for a constructor without any arguments,
+ // we have this simple case involving no substitutions.
+ if (c.x.length == 0)
+ {
+ boolean scrutPlausible = plausible(
+ t_,
+ c.c,
+ uCtxt,
+ baseCtxt,
+ true
+ );
+
+ if (!scrutPlausible)
+ continue;
+
+ Atom matchEq = new Atom(true, t_, c.c);
+ Var matchEqVar = new Var("p");
+
+ if (t_.construct != Expr.CONST)
+ uCtxt.lemmaSet.addLemma(matchEq);
+
+ // Make deductions from case body -----
+ branchPlausible = plausible(
+ c.body,
+ target,
+ uCtxt,
+ baseCtxt,
+ eq
+ );
+
+ if (t_.construct != CONST)
+ uCtxt.lemmaSet.removeLemma(matchEq);
+ }
+ // if the case is for a constructor with arguments,
+ // things are a bit more complicated.
+ else
+ {
+ boolean scrutPlausible = plausible(
+ t_,
+ new TermApp(c.c,c.x),
+ uCtxt,
+ baseCtxt,
+ true
+ );
+
+ if (!scrutPlausible)
+ continue;
+
+ if (isScrutConstructor)
+ {
+ TermApp ta = (TermApp)t_;
+ Expr substitutedBody = c.body;
+
+ for (int j = 0; j < ta.X.length; ++j)
+ substitutedBody = substitutedBody.subst(ta.X[j], c.x[j]);
+
+ branchPlausible = plausible(
+ substitutedBody,
+ target,
+ uCtxt,
+ baseCtxt,
+ eq
+ );
+ }
+ else
+ {
+ //
+ Expr substitutedBody = c.body;;
+
+ FunType consType =
(FunType)c.c.classify(baseCtxt).defExpandTop(baseCtxt);
+ Var[] clones = new Var[consType.vars.length];
+ Var[] nonSpecificationalClones = new Var[c.x.length];
+ Expr[] types = new Expr[consType.vars.length];
+
+ int last = consType.vars.length-1;
+
+ //index into non-specificational args
+ int uInd = 0;
+
+ for(int j = 0; j < clones.length; ++j)
+ {
+ clones[j] = new Var("z");
+ types[j] = consType.types[0];
+ baseCtxt.setClassifier(clones[j], types[j]);
+
+ int spec = (consType.owned[0].status & Ownership.SPEC);
+
+ if (!(clones[j].isTypeOrKind(baseCtxt) ||
+ clones[j].isProof(baseCtxt) ||
+ spec != 0) ) {
+
+ nonSpecificationalClones[uInd] = clones[j];
+ substitutedBody = substitutedBody.subst(clones[j],
c.x[uInd]);
+ uInd++;
+ }
+
+ // 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]);
+ }
+
+ Atom matchEq = new Atom(
+ true,
+ t_,
+ new TermApp(c.c,nonSpecificationalClones)
+ );
+
+ uCtxt.lemmaSet.addLemma(matchEq);
+
+ // Make deductions from case body -----
+ branchPlausible = plausible(
+ substitutedBody,
+ target,
+ uCtxt,
+ baseCtxt,
+ eq
+ );
+
+ uCtxt.lemmaSet.removeLemma(matchEq);
+ }
+ }
+
+ //Or the current return value with the deduction for the
+ //current branch (if ret is null, we set it to the current
branch)
+ ret = ret || branchPlausible;
+ }
+
+ return ret;
+ case Expr.BANG:
+ return target.construct == Expr.BANG;
+ case Expr.DO:
+ Do d = (Do)term;
+ return plausible(
+ d.t,
+ target,
+ uCtxt,
+ baseCtxt,
+ eq
+ );
+ case Expr.VOIDI:
+ return target.construct == VOIDI;
+ case Expr.LET:
+ return plausible(
+ term.evalStep(baseCtxt),
+ target,
+ uCtxt,
+ baseCtxt,
+ eq
+ );
+ default:
+ assert(false);
+ return false;
+ }
+ }
//Non-unfolding evaluation step
public Expr nustep(Expr e, Context ctxt)
@@ -130,7 +411,7 @@
while (e2 != nustep(e2,ctxt))
{
- System.out.println(e2.toString(ctxt));
+ //System.out.println(e2.toString(ctxt));
e2 = nustep(e2,ctxt);
}
@@ -298,6 +579,8 @@
);
}
+ return null;
+ case Expr.ABORT:
return null;
default:
assert(false);
@@ -335,6 +618,8 @@
case Expr.LET:
Let let = (Let)e;
return matchFree(let.t1) && matchFree(let.t2);
+ case Expr.ABORT:
+ return true;
default:
assert(false);
return false;
@@ -433,18 +718,18 @@
Expr lhs2 = lhs;
while (true) {
- System.out.println("a.");
- System.out.println(lhs2.toString(ctxt));
+ //System.out.println("a.");
+ //System.out.println(lhs2.toString(ctxt));
lhs2 = nueval(lhs2, ctxt);
- System.out.println("b.");
- System.out.println(lhs2.toString(ctxt));
+ //System.out.println("b.");
+ //System.out.println(lhs2.toString(ctxt));
lhs2 = liftMatches(lhs2);
- System.out.println("c.");
- System.out.println(lhs2.toString(ctxt));
+ //System.out.println("c.");
+ //System.out.println(lhs2.toString(ctxt));
if (lhs2.construct == TERM_APP)
{
=======================================
--- /branches/1.0/guru/UnjoinContext.java Mon Nov 14 12:52:03 2011
+++ /branches/1.0/guru/UnjoinContext.java Mon Nov 21 12:42:14 2011
@@ -20,9 +20,16 @@
public final LemmaSet lemmaSet;
+ //Whenever we enter recursively defined functions, testing for
plausibility,
+ //we need to make sure we don't traverse recusive function calls. recVars
+ //is equal to the current recursive variable, if any, so we can use
+ //it to check for this.
+ public Var recVar;
+
public UnjoinContext(LemmaSet baseLemmaSet)
{
this.proofCounter = 0;
this.lemmaSet = baseLemmaSet.copy();
+ this.recVar = null;
}
}
=======================================
--- /branches/1.0/tests/unjoin.g Mon Nov 14 12:52:03 2011
+++ /branches/1.0/tests/unjoin.g Mon Nov 21 12:42:14 2011
@@ -10,68 +10,173 @@
| nil2 : Fun(A:type).<list2 A>
| cons2 : Fun(A:type)(a:A)(l:<list2 A>). <list2 A>.
-Define foldr2
- : Fun(S A : type)(acc : Fun(s : S)(a : A). S)(init : S)(l : <list2 A>). S
+Define matchArgs :=
+ fun(x : nat)(y : nat).
+ let z =
+ match x with
+ | Z =>
+ one
+ | S x' =>
+ two
+ end
+ in
+ (max z y).
+
+Define matchArgsProof
:=
- fun foldr2(S A : type)(acc : Fun(s : S)(a : A). S)(s : S)(l : <list2
A>):S.
- match l with
- | nil2 _ =>
- s
- | cons2 _ a' l' =>
- let s' = (acc s a') in
- (foldr2 S A acc s' l')
+ foralli(x y : nat)(u : { (matchArgs x y) = two }).
+ unjoin u with
+ | foralli(p0 : { x = Z })(u : { (max one y) = two }).
+ lemma
+ : { (le y (max one y)) = tt }
+ [max_easy y one]
+ : { (le (max one y) two) = tt }
+ [eq_le (max one y) two u]
+ in
+ [le_trans y (max one y) two ## ##]
+ | foralli(x0 : nat)(p0 : { x = (S x0) })(u : { (max two y) = two }).
+ lemma
+ : { (le y (max two y)) = tt }
+ [max_easy y two]
+ : { (le (max two y) two) = tt }
+ [eq_le (max two y) two u]
+ in
+ [le_trans y (max two y) two ## ##]
end.
-Define ormap :=
- fun(l : <list2 bool>).
- (foldr2 bool bool or ff l).
-%-
Define list_setmember2
: Forall(A:type)(a:A)
(eqA:Fun(^#owned x y: A).bool)
(eqA_total:Forall(a b: A).Exists(z:bool).{ (eqA a b) = z })
- (u:{ (eqA a a) = tt })
+ (eqA_refl: Forall(a: A). { (eqA a a) = tt })
(l'' l':<list A>).
{ (member a (append l' (cons a l'')) eqA) = tt }
:=
foralli(A:type)(a:A)(eqA:Fun(^ #owned x y: A).bool)
(eqA_total:Forall(a b: A).Exists(z:bool).{ (eqA a b) = z })
- (u: {(eqA a a) = tt})(l'' l':<list A>).
- abbrev eqA = terminates eqA by eqA_total in
- case (member A a (append A l' (cons A a l'')) eqA) by v ign with
- | ff =>
- lemma u in
- unjoin v with
- | foralli(p0 : { (append l' (cons a l'')) = nil }).
- unjoin p0 with
-
- | (l'0 : type)(l'1 : l'0)(l'2 : <list l'0>)(p0 : { l' = (cons l'1
l'2) })
- (u : { (append_h (inspect mk_append_i) l'1 (foldr (clone_owned
(inspect mk_append_i)) append_h (cons a l'') l'2)) = nil }) =>
+ (eqA_refl: Forall(a: A). { (eqA a a) = tt })
+ (l'' l': <list A>).
+ [member_append_cons A a l' l'' eqA eqA_total eqA_refl].
- %-
- %%
- %% INTERESTING POINT - PARTIAL APPLICATION USED TO CREATE A FUNCTION
- %% DOES NOT HANDLE WELL. NUEVAL
- %%
- %%
- | foralli(l'0 : type)(l'1 : l'0)(l'2 : <list l'0>)
- (p0 : { l' = (cons l'1 l'2) })
- (u : { (fun(^ #owned cookie)(^ #owned x)(l) : !. match
cookie by cookie_eq cookie_Eq return <list A> with mk_append_i => (cons
(inc_owned x) l) end mk_append_i l'1 (fun foldr(^ #owned cookie)(fcn)(b)(^
#owned l) : !. match l by l_eq l_Eq return B with nil => b | cons a' l' =>
(fcn cookie a' (foldr (clone_owned cookie) fcn b l')) end (clone_owned
mk_append_i) fun(^ #owned cookie)(^ #owned x)(l) : !. match cookie by
cookie_eq cookie_Eq return <list A> with mk_append_i => (cons (inc_owned x)
l) end (cons a l'') l'2)) = nil })
- -%
-
+
+Define nth_append2 : Forall(A:type)(n:nat)(l:<list A>)(a:A)
+ (u:{(nth n l) = a}).
+ Exists(l1 l2:<list A>).
+ { l = (append l1 (cons a l2)) } :=
+ foralli(A:type)(n:nat)(l:<list A>)(a:A)
+ (u:{(nth n l) = a}).
+
+ unjoin u with
+ | foralli(p0 : { n = Z })(l0 : type)(l1 : l0)(l2 : <list l0>)
+ (p1 : { l = (cons l1 l2) })(u : { l1 = a }).
+
+ %% darnit... there is no way to prove l0 = A.
+ %% I need to lookup l0 from the type of l. even though u
+ %% is unannotated, we should be able to find the type in
+ %%
+
+ lemma
+ : { l0 = A }
+ l
+ in
+ existsi (nil A)
+ Exists(l'' : <list l0>)
+
+ | foralli(n0 : nat)(p0 : { n = (S n0) })(l0 : type)(l1 : l0)
+ (l2 : <list l0>)(p1 : { l = (cons l1 l2) })
+ (u : { (nth n0 l2) = a }).
+
+
+
+ end.
+
+
+Define set_nth_other : Forall(A:type)(l:<list A>)(n m:nat)(b:A)
+ (u:{ n != m }).
+ { (nth n (set_nth m l b)) = (nth n l) } :=
+ foralli(A:type).
+ induction(l:<list A>)
+ return Forall(n m:nat)(b:A)
+ (u:{ n != m }).
+ { (nth n (set_nth m l b)) = (nth n l) } with
+ | nil _ =>
+ foralli(n m:nat)(b:A)(u:{ n != m }).
+ hypjoin (nth n (set_nth m l b)) (nth n l) by l_eq end
+ | cons _ a l' =>
+ foralli(n m:nat)(b:A)(u:{ n != m }).
+ case m with
+ Z =>
+ case n with
+ Z => contra trans m_eq
+ trans symm n_eq u
+ { (nth n (set_nth m l b)) = (nth n l) }
+ | S n' =>
+ hypjoin (nth n (set_nth m l b)) (nth n l)
+ by l_eq m_eq n_eq end
+ end
+ | S m' =>
+ case n with
+ Z => hypjoin (nth n (set_nth m l b)) (nth n l)
+ by l_eq m_eq n_eq end
+ | S n' =>
+ hypjoin (nth n (set_nth m l b)) (nth n l)
+ by l_eq m_eq n_eq
+ [l_IH l' n' m' b
+ diseqi foralli(u1:{n' = m'}).
+ contra
+ transs cong (S *) u1
+ symm m_eq
+ symm trans symm n_eq u
+ end
+ False]
+ end
+ end
end
-
- | foralli(c0 : type)(c1 : c0)(c2 : <list c0>)
- (p0 : { (append l' (cons a l'')) = (cons c1 c2) })
- (u : { (or (eqA (clone_owned a) c1) (member a c2 eqA)) = ff
}).
- truei
+ end.
+
+
+Define foldr2
+ : Fun(S A : type)(acc : Fun(s : S)(a : A). S)(init : S)(l : <list2 A>). S
+:=
+ fun foldr2(S A : type)(acc : Fun(s : S)(a : A). S)(s : S)(l : <list2
A>):S.
+ match l with
+ | nil2 _ =>
+ s
+ | cons2 _ a' l' =>
+ let s' = (acc s a') in
+ (foldr2 S A acc s' l')
+ end.
+
+Define matchLet :=
+ fun(x : nat)(y : bool).
+ match x with
+ | Z =>
+ tt
+ | S n' =>
+ let z = (and y tt) in
+ z
+ end.
+
+Define matchLetProof
+ : Forall(x : nat)(y: bool)(u1 : { (matchLet x y) = tt })
+ (x' : nat)(u2 : { x = (S x')}). { y = tt }
+:=
+ foralli(x : nat)(y: bool)(u1 : { (matchLet x y) = tt })
+ (x' : nat)(u2 : { x = (S x')}).
+ lemma u2 in
+ unjoin u1 with
+ | foralli(p0 : { (and y tt) = tt }).
+ unjoin p0 with
+ | foralli(u : {y = tt}).
+ u
end
-
- | tt =>
- v
- end
--%
+ end.
+
+Define ormap :=
+ fun(l : <list2 bool>).
+ (foldr2 bool bool or ff l).
+
Define eqnatEq3 : Forall(n:nat)(u:{(eqnat n Z) = tt}). { n = Z } :=
@@ -105,31 +210,6 @@
| foralli(u : { x = tt }).
u
end.
-
-Define matchLet :=
- fun(x : nat)(y : bool).
- match x with
- | Z =>
- tt
- | S n' =>
- let z = (and y tt) in
- z
- end.
-
-Define matchLetProof
- : Forall(x : nat)(y: bool)(u1 : { (matchLet x y) = tt })
- (x' : nat)(u2 : { x = (S x')}). { y = tt }
-:=
- foralli(x : nat)(y: bool)(u1 : { (matchLet x y) = tt })
- (x' : nat)(u2 : { x = (S x')}).
- lemma u2 in
- unjoin u1 with
- | foralli(p0 : { (and y tt) = tt }).
- unjoin p0 with
- | foralli(u : {y = tt}).
- u
- end
- end.
Define matchAbbrev :=
fun(x : nat)(y : bool).
@@ -179,39 +259,7 @@
u
end.
-Define matchArgs :=
- fun(x : nat)(y : nat).
- let z =
- match x with
- | Z =>
- one
- | S x' =>
- two
- end
- in
- (max z y).
-
-Define matchArgsProof
-:=
- foralli(x y : nat)(u : { (matchArgs x y) = two }).
- unjoin u with
- | foralli(p0 : { x = Z })(u : { (max one y) = two }).
- lemma
- : { (le y (max one y)) = tt }
- [max_easy y one]
- : { (le (max one y) two) = tt }
- [eq_le (max one y) two u]
- in
- [le_trans y (max one y) two ## ##]
- | foralli(x0 : nat)(p0 : { x = (S x0) })(u : { (max two y) = two }).
- lemma
- : { (le y (max two y)) = tt }
- [max_easy y two]
- : { (le (max two y) two) = tt }
- [eq_le (max two y) two u]
- in
- [le_trans y (max two y) two ## ##]
- end.
+
Define badSub :=
@@ -245,14 +293,7 @@
: { (badSub x) = (S z) } u'
end
end
- end.
-
-
-
-%
-% MOAR PROOOFS
-%
-%
+ end.
Define eqnatNeq2 : Forall(n m:nat)(u:{(eqnat n m) = ff}). { n != m } :=
induction (n:nat) return