OO-machine: A heady mixture of TNG-R4, Jay&Kesner's Pure Pattern Calculus, and Cardelli&Abadi's ς calculus. Dec 2010 - Feb 2011.

oomachine.rkt

#lang racket
;; OO-machine
;; A heady mixture of TNG-R4,
;;                    Jay&Kesner's Pure Pattern Calculus, and
;;                    Cardelli&Abadi's ς calculus.

(require redex)
(require rackunit)

(define-language oc
  ;;
  ;; The language itself
  ;;
  (x variable-not-otherwise-mentioned)
  (selector variable-not-otherwise-mentioned)
  (e x
     n
     (e <- e via e)
     (selector e ...)
     (x p -> e orelse e) ;; is this too restrictive? (e orelse e) instead?
			 ;; Yes, it probably is too restrictive.
			 ;; Without (e orelse e), we can't express multiple
			 ;; trait combination.
     (x x -> e))
  (p (selector x ...))
  ;;
  ;; Values and reduction contexts
  ;;
  (n number)
  (v n
     (selector v ...)
     (x p -> e orelse v)
     (x x -> e))
  (E hole
     (e <- e via E)
     (E <- e via v)
     (v <- E via v)
     (x p -> e orelse E)))

(define oc-red
  (reduction-relation oc
    (--> (in-hole E (v_receiver <- v_message via v_behaviour))
         (in-hole E (beta v_receiver v_message v_behaviour))
         beta)))

(define does-not-understand-term
  (term (self any -> (does-not-understand self any))))

(define message-behaviour-term does-not-understand-term)
(define number-behaviour-term does-not-understand-term)

(define-metafunction oc
  beta : v v v -> e ;; receiver, message, behaviour
  ;; Method's selector matches message's selector.
  [(beta v_receiver
         (selector v_actual ...)
         (x_self (selector x_formal ...) -> e_body orelse v_alt))
   (subst-n (x_self v_receiver) (x_formal v_actual) ... e_body)
   (side-condition (= (length (term (x_formal ...)))
		      (length (term (v_actual ...)))))]
  ;; Message does not match method.
  [(beta v_receiver
         v_message
         (x_self (selector x_formal ...) -> e_body orelse v_alt))
   (beta v_receiver
         v_message
         v_alt)]
  ;; Catch-all method.
  [(beta v_receiver
         v_message
         (x_self x_formal -> e_body))
   (subst-n (x_self v_receiver) (x_formal v_message) e_body)]
  ;; Reflective protocol on numbers. (!)
  [(beta v_receiver
         v_message
	 n)
   (beta v_receiver
         v_message
         ,number-behaviour-term)]
  ;; Reflective protocol on messages. (!)
  [(beta v_receiver
         v_message
         (selector v_actual ...))
   (beta v_receiver
         v_message
         ,message-behaviour-term)])

;; From 5provided
(define-metafunction oc
  subst-n : (x any) ... any -> any
  [(subst-n (x_1 any_1) (x_2 any_2) ... any_3)
   (subst x_1 any_1 (subst-n (x_2 any_2) ... any_3))]
  [(subst-n any_3) any_3])

;; Specific implementation for this language
(define-metafunction oc
  subst : x any any -> any
  [(subst x_1 any x_1) any]
  [(subst x_1 any x_2) x_2]
  [(subst x_1 any (e_receiver <- e_message via e_behaviour))
   ((subst x_1 any e_receiver) <- (subst x_1 any e_message) via (subst x_1 any e_behaviour))]
  [(subst x_1 any (selector e ...)) (selector (subst x_1 any e) ...)]

  [(subst x_1 any (name v (x_1 x_other -> e))) v]
  [(subst x_1 any (name v (x_other x_1 -> e))) v]
  [(subst x_1 any (name v (x_other (selector x_2 ... x_1 x_3 ...)))) v]

  [(subst x_1 any (x_self x_message -> e))
   (x_selfnew x_messagenew -> (subst x_1 any (subst-n (x_self x_selfnew)
						      (x_message x_messagenew)
						      e)))
   (where (x_selfnew x_messagenew)
	  ,(variables-not-in (term (x_self x_message any e))
			     (term (x_self x_message))))]
  [(subst x_1 any (x_self (selector x_formal ...) -> e orelse e_alt))
   (x_selfnew (selector x_formalnew ...) ->
	      (subst x_1 any (subst-n (x_self x_selfnew)
				      (x_formal x_formalnew) ...
				      e))
	      orelse (subst x_1 any e_alt))
   (where (x_selfnew x_formalnew ...)
	  ,(variables-not-in (term (x_self (x_formal ...) any e))
			     (term (x_self x_formal ...))))])

(define-metafunction oc
  =alpha : e e -> any ;; would be boolean but redex doesn't support that
  [(=alpha e_1 e_2) (=alpha/env e_1 e_2 ())])

(define-metafunction oc
  =alpha/env : e e ((x x) ...) -> any ;; would be boolean
  [(=alpha/env x_1 x_2 ((x_1 x_2) any ...)) #t]
  [(=alpha/env x_1 x_2 ((x_1 x_3) any ...)) #f]
  [(=alpha/env x_1 x_2 ((x_3 x_2) any ...)) #f]
  [(=alpha/env x_1 x_2 ((x_3 x_4) any ...)) (=alpha/env x_1 x_2 (any ...))]
  [(=alpha/env x_1 x_1 ()) #t] ;; for non-closed terms

  [(=alpha/env (e_r1 <- e_m1 via e_b1)
	       (e_r2 <- e_m2 via e_b2) (any ...))
   ,(and (term (=alpha/env e_r1 e_r2 (any ...)))
	 (term (=alpha/env e_m1 e_m2 (any ...)))
	 (term (=alpha/env e_b1 e_b2 (any ...))))]

  [(=alpha/env (selector e_1 ...) (selector e_2 ...) (any ...))
   ,(andmap values (term ((=alpha/env e_1 e_2 (any ...)) ...)))]

  [(=alpha/env (x_1 (selector x_f1 ...) -> e_b1 orelse e_a1)
	       (x_2 (selector x_f2 ...) -> e_b2 orelse e_a2) (any ...))
   ,(and (term (=alpha/env e_b1 e_b2 ((x_1 x_2) (x_f1 x_f2) ... any ...)))
	 (term (=alpha/env e_a1 e_a2 (any ...))))]

  [(=alpha/env (x_1 x_m1 -> e_b1)
	       (x_2 x_m2 -> e_b2) (any ...))
   (=alpha/env e_b1 e_b2 ((x_1 x_2) (x_m1 x_m2) any ...))]

  ;; Catch-all false case. Relies on order of clauses.
  [(=alpha/env e_1 e_2 (any ...)) #f])

(define-metafunction oc
  parse : any -> e
  [(parse x) x]
  [(parse (any_r <- any_m)) ((parse any_r) <- (parse any_m) via (parse any_r))]
  [(parse (any_r <- any_m via any_b)) ((parse any_r) <- (parse any_m) via (parse any_b))]
  [(parse (x p -> any orelse any_a)) (x p -> (parse any) orelse (parse any_a))]
  [(parse (x p -> any)) (x p -> (parse any) orelse ,does-not-understand-term)]
  [(parse (x x_m -> any)) (x x_m -> (parse any))]
  [(parse (any -> any_1)) (parse (x any -> any_1))
   (where x ,(variable-not-in (term (any any_1)) (term dummyself)))]
  [(parse (selector any ...)) (selector (parse any) ...)]
  [(parse any) any])

(define (reduce-oc e)
  (let ((results (apply-reduction-relation* oc-red e)))
    (cond
     ((null? results) #f)
     (else (first results)))))

(define (reduces-to? e v)
  (let ((result (reduce-oc e)))
    (if (not result)
	(eq? v 'DIVERGENT)
	(term (=alpha ,result ,v)))))

(check-true (term (=alpha (parse (x -> x))
			  (self y -> y))))

(check-equal? (term (beta (d x -> (x <- x via x)) (d y -> y) (d x -> (x <- x via x))))
	      (term ((d y -> y) <- (d y -> y) via (d y -> y))))

(check reduces-to?
       (term (parse ((x -> x) <- (y -> y))))
       (term (self z -> z)))

(check reduces-to?
       (term (parse ((self (a) -> (a) orelse (self (b) -> (b))) <- (a))))
       (term (a)))
(check reduces-to?
       (term (parse ((self (a) -> (a) orelse (self (b) -> (b))) <- (b))))
       (term (b)))
(check reduces-to?
       (term (parse ((self (a) -> (a) orelse (self (b) -> (b))) <- (c))))
       (term (parse (does-not-understand (self (a) -> (a) orelse (self (b) -> (b)))
					 (c)))))

(check reduces-to?
       (term (parse (((a b c) -> (d b c)) <- (a (x -> x) (y -> y)))))
       (term (parse (d (x -> x) (y -> y)))))

(check reduces-to?
       (term (parse (((a b c) -> (d b c)) <- (a))))
       (term (parse (does-not-understand ((a b c) -> (d b c))
					 (a)))))