case PATTERN; FORMULA

switch ( l ) {
  case List;l.tail(IntList t) : ...
}

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

predicate range( int x, int l, int h )
    modes(l,h->x)

range(int x, -10, 10) && x*x == 1

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

forall( formula1 ) formula2

exists( formula1 ) formula2

pred maxelem( int[]a, int i )
    modes(a,i->;a->i) {
  // a[i] is the LUB of all elements in a
  forall( int v==a[int j] ) 
}

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

form ::= cut(form)
       | form && form
       | form || form
       | pat == pat
       | T x = pat
       | forall ( form1 ) form2
       | exists ( form1 ) form2

s ::= ...
    | switch expr {
        case PAT[;FORMULA] : s
        ...
      }
    | foreach( FORMULA ) s
    | if ( FORMULA ) s1 else s2
    | cond
        FORMULA : s
        ...
      }

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

f in Formula
m in mode = Var -> Unknown + Iterable + Known
GAMMA in Var -> Type
M in {Single, multiple} (->! vs ->)

V--------------------------F_1 vs. F_M, P_1 vs. P_M
F[[form]]mgM = ?
P[[pat]]mGM = ?   <-- what kind of syntactic form are we generating?
E[[expr]]mG = ?   <-- actual syntax-directed translations
S[[s]]mG = ?
[[t(formal)* (modes(...){F})*]]
               A------ views & methods