EnhancedForStatement.xjl

package extensions;

public extension EnhancedForStatement {
    lexical syntax
      "for" -> Keyword

    context-free syntax
      "for" "(" Type ID ":" Expr ")" Statement -> Statement

    inductive definitions
      S-EnhancedFor:
        // "context"
        typevars(CT) = X*
        norm(CT, X*, T) = t
        norm(CT, X*, JLIterator<T>) = javalight.util.JLIterator t::[]
        CT.javalight.lang.JLIterable = {[], iterator:[]->javalight.util.JLIterator A::[] :: [], Object, A::[]}
        CT.javalight.util.JLIterator = {[], hasNext:[]->boolean :: next:[]->A :: [], Object, A::[]}

        // right-hand side
        CT; Ef; El |- e : s
        CT |- s <: javalight.lang.JLIterable t::[]

        // body
        x notin dom(El)
        CT; Ef; El,x:t |- stm ~ void

        // subsequent statements
        CT; Ef; El |- stm* ~ rt
        ------------------------------------------------------------------------------------------------------
        CT; Ef; El |- for(T x : e) stm stm* ~ rt

    desugarings
      {
        // "context"
        typevars(CT) = X*
        norm(CT, X*, T) = t
        norm(CT, X*, JLIterator<T>) = javalight.util.JLIterator t::[]
        CT.javalight.lang.JLIterable = {[], iterator:[]->javalight.util.JLIterator A::[] :: [], Object, A::[]}
        CT.javalight.util.JLIterator = {[], hasNext:[]->boolean :: next:[]->A :: [], Object, A::[]}

        // right-hand side
        CT; Ef; El |- e : s
        CT |- s <: javalight.lang.JLIterable t::[]

        // body
        x notin dom(El)
        CT; Ef; El,x:t |- stm ~ void

        // subsequent statements
        CT; Ef; El |- stm* ~ rt
        ------------------------------------------------------------------------------------------------------
        CT; Ef; El |- [ for(T x : e) stm stm* ] ~ rt
        ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~>
        {
            JLIterator<T> y = e.iterator();
            while(y.hasNext()) {
                T x = y.next();
                stm
            }   
        }
        stm*
        where y =ID fresh(Ef;El,x:t)
      }
}