fej.rkt

#lang racket

#|

Thise file contains a simple implementation of Featherweight EpsilonJ as presented in the paper
Kamina T, Tamai T.
"A Smooth Combination of Role-based Language and Context Activation" FOAL 2010 Proceedings, 2010.

|#

(require redex)

;; ============================================
;; FEJ Syntax
;; ============================================

(define-language FEJ

  ; class declarations
  (L (class C (T f) ... M ... A ... ))

  ; role declarations
  (A (role R requires Mi ... (T f) ... M ... ))

  ; type declarations
  (T
   (C R)
   ((C R) ... C))

  ; method signatures
  (Mi (T m ((T x) ...)))

  ; types and interfaces
  (Ts
   T
   (Mi ...))

  ; method declarations
  (M (Mi e))

  ; terms / expressions
  (e
   x
   (lkp e f)
   (call e m e ...)
   (new C e ... with r ...)
   (bind x ... with r ... from y ... e))

  ; values
  (v (new C v ... with r ...))

  ; role instance
  (r (v R v ...))

  ; class table
  (CT (L ...))

  ; evaluation contexts
  (E
   hole
   (lkp E f) ; CR-FIELD
   (call E m e ...) ; CR-INVK
   (call v m v ... E e ...) ; CR-INVK-ARG ;; Fig. 16 is not clear here - take definition of FJ
   (new C v ... E e ...) ; CR-NEW
   )

  ; typing environment
  (Γ ((x C) ...))

  (Bool #t #f)

  ; class names
  (C variable-not-otherwise-mentioned)
  (D variable-not-otherwise-mentioned)
  ; role names
  (R variable-not-otherwise-mentioned)
  ; field names
  (f variable-not-otherwise-mentioned)
  (g variable-not-otherwise-mentioned)
  ; method names
  (m variable-not-otherwise-mentioned)
  (n variable-not-otherwise-mentioned)
  ; variable names
  (x variable-not-otherwise-mentioned)
  (y variable-not-otherwise-mentioned)
  
  )

;; ============================================
;; FEJ subtyping
;; ============================================

(define-judgment-form FEJ
  ; all constituents are inputs
  #:mode (<: I I I)
  #:contract (<: CT Ts Ts)
  ; Ts ::= C.R | (C.R)*::C | Mi*

  ; S-REFL
  [-------------
   (<: CT Ts Ts)]

  #|
  This is a combination of
  S-TRANS and S-STRUCT
  |#
  ;[(where () ())
  ; -------------
  ; ]
  )

;; ============================================
;; FEJ auxilery metafunctions
;; ============================================

; Fig. 11: method type lookup
(define-metafunction FEJ
  mtype : CT m Ts -> any

  [ ; m is defined in C
   (mtype CT m C)
   (where)
   ]
  )

; auxilery metafunction - method signature in method list?
(module+ test
  (test-equal (term (method-in m (T n (T x) e))) #f)
  (test-equal (term (method-in m ())) #f)
  (test-equal (term (method-in m (((T m (T x) e)) ((T n (T x) e))))) (term(((T m (T x) e))))))


(define-metafunction FEJ
  method-in : m M ... -> any
  [(method-in m M_0 ... ((T m (any ...) e)) M_1 ...) ((T m (any ...) e))]
  [(method-in m ((T m (any ...) e))) ((T m (any ...) e))]
  [(method-in m any) #f])

;; ============================================
;; test metafunctions
;; ============================================

(define class-table-mf
  (term
   (
    (class A
      () ; T f
      () ; M
      () ; A
      )

    (class B
      (
       (A a)
       ) ; T f
      (
       (A m () (
              (lkp a)    
                  )
          )
       ) ; M
      () ; A
      )
    )
  ))


(module+ test
  (test-results))