S ::= cond      <-- formula   (what it uses)
    | switch    <-- pattern
    | foreach   <-- formula
    | if        <-- formula

F ::= P == P
    | T x = P
    | cut(F)
    | F && F
    | F || F
    | forall(F) F
    | exists(F) F
    | expr.pr(P*)
    | boolexpr

P ::= expr
    | T x
    | T(P*) x
    | expr.mt(P*)
    | *

pr,mt in Identifier

predicate P(formals) ...
predicate T F(formals) ... mode(F,..->..) ...


F[[F]]uGM = <inner class, iterator class, statement, expr yields an enum(u)>
P[[P]]uGM = <inner class, statement, expr yielding function:value->enum(u)>
E[[e]]G   = <class, statement, expr>
S[[s]]G   = <class, stmts>

u = unknown variables to be solved for by the formula or pattern
G = type context of already solved variables

last two fairly straightforward
first two index into following table:

         |  single  |  multiple
---------+----------+------------
forward  |   bool   |   bool
backward |   value  |   enum


int plus( int x, int y )
  mode( x,y ->! ) { return x+y; }
  mode( x,plus ->! y ) { return plus-x; }
  mode( y,plus ->! x ) { return plus-y; }


predicate bool Pr( T1 x1, ... , Tn xn )
    mode( x1, ..., xn -> ) = T1 x ... x Tn -> bool
    mode( xi -> xj ) = Ti -> enum(Tj)
    mode( xi ->! xj ) = Ti -> Tj

predicate T Fn( Ti xi )
    mode( x1, ..., xn -> Fn ) = Ti -> T
    mode( Fn,... -> xj ) = T x ... -> enum(Tj)
    mode( Fn,... ->! xj ) = T x ... -> Tj


If you declare a variable on one side of a disjunct in a formula, you
must declare the same variable on the other side of the disjunct.

F[[F1 || F2]]uG* =
  let <c1,s1,e1> = F[[F1]]uG* in
    let <c2,s2,e2> = F[[F2]]uG* in
      // note that c1 and c2 are isomorphic
      // And here, we iterate through c1 followed by c2
      C_1tuple, C_1iter, C_2iter
      
      class Iter implements Iterator{
	    Iterator i1, i2;
	    Iter() {
		   i1 = new Iter1();
		   i2 = new Iter2();
	    }
	    
	    Object getNext() {
		   if (i1.hasMore()) {
		      return i1.getNext();
		   } else {
		      return i2.getNext();
		   }
            }

	    boolean hasMore() {
		    return (i1.hasMore() || i2.hasMore());
	    }

            // Delete is easy, just call delete on i1 or i2
       }

F[[F_1 || F_2]]uGamma1 = 
    F[[cut(F_1||F_2)]]uGamma1
   
*** Some clarifications of translation: 
We translate a formula to (tuple(F),enum(F),state(F)), where each is
defined below

tuple(F) => c

That is, the tuple of a formula gives out a class definition of a
tuple that contains the elements we are "solving for" - i.e. the free
variables of the formula

enum(F) => c

Translating a formula also includes an enumeration class, that
enumerates the tuple objects corresponding to tuple(F)

state(S) => statments

Translating a formula also includes the statements that initialize the
enumeration class and create a new Enumerator object which we can use
to spit out the tuples

*NOTE* - we're not exactly sure what statements a formula should
 translate to.  We think it has to do with the initialization of the
 enumeration that spits out the tuples

F[[cut(F)]]uGammaM = 
   let <c,s,e> = F[[F]]uGammaM in
       if (M = single) then
          <c,s,e>
       else
	  C_tup c_iter
	  Iterator i = new C_iter();
	  return (C_tup)i.getNext();
	end

F[[cut(F)]]uGamma1 = 
   let <c,s,e> = F[[cut(F)]]uGamma*
       <C_tup C_iter 
	      Iterator i = new C_iter();
	      return (C_tup)i.getNext();>

F[[cut(F)]]uGamma* = 
   let <c,s,e> = F[[F]]uGammaF1 in
       C_tup
       Class Iter implements iterator {
	     boolean flag = true;

	     boolean hasMore() {
		     return flag;
	    }

	     Object getNext() {
		    if (flag) {
		       flag = false;
		       return e;
		    } else  {
		       throw newException;
		    }
	     }
	}

---------------------------------------

<c1,I1,s1,e1> = F[[F1]]u1G*
u1,u2 = u
<c2,I2,s2,e2> = F[[F2]]u2(G,u1)*

F[[F1 && F2]]uG* =
  < c1
    c2
    class I implements Iterator {
      Iterator i1, i2;
      Object v1;
      I() {
        i1 = new I1();
        i2 = new I2();
      }

      boolean hasNext() {
      }

      Object next() {
      }

      private void advance() {
        // move i1,i2 forward until element in both
      }
    }
  >

We're basically generating a double for-loop using the most painful method
possible.....

---------------------------------------

Introduce F* and F1 as translations that generate for loops as opposed to
iterators.

F*[[F]]uGs = s'

executing s' causes s to be executed for each solution to variables in u

F*[[F1 && F2]](u1,u2)Gs =
  F[[F1]]u1G( F[[F2]]u2(G,u1)s )

F1[[cut F]]uGs = < F*[[F]]uG(u' = u; break), u' >

F*[[F1 || F2]]uGs =
  F*[[F1]]uGs; F*[[F2]]uGs  // involves code duplication

F*[[T x = E]]{x}Gs = {T x = E; s}

+===
| // example:  both sides have unknowns, but it's solvable
| int x;
| x == f(y,int z) mode: y->f,z
| 
| x unknown: iteration over x,z
| x known:  test -> if success, bind z
+===

F*[[P1 == P2]]uGs = ?
// if P1 and P2 are both unknown, fail; at least one side needs to be "known"
// require that at least one can be evaluated to a value
// need predicate in target language: solved(P, Gamma)
// assume WLOG P1 solved

F[[F1 && F2]]uGammaM

P*[[T x]]emptyGammasv = 
   T' v = x; if (v instanceOf T) {T x= (T)v; s}

// (what we had before) if (x instanceof T) { T x' = (T)x; s} //

[[switch e case P1:S1 ... ]] = 

// maybe P1 must only be ! (that is, only return one thing)

T' v = e; boolean match = false;
          P*[[P1]]u1Gamma{match = true; S1}
	  if (!match) {
	      P*[[P2]]u2Gamma{match .. S2]

P* = solve for
P! = returns one thing?
P_*^e = ?
P_!^e = ?

need a translation for solved patterns vs. unsolved patterns

patterns can be evaluatable or unevaluatable?
for example, in a switch statement, we have the following:
the patterns corresponding to each case can either be evaluatable or 
unevaluatable - meaning, either we need the value v to start off the 
pattern (unevaluatable) and then match with v, or we don't (can just evaluate
and then match with v)


+===
| switch (e)
| case List x:S
|             List x' = (List)v;
+===

P*[[P]]uGamma

P1[[P]]

modification to grammar: 

Productions to F
T x = p => T x; x == p
Decl; F

Productions to P
P; F