A hierarchy of languages

lcs.rkt

#lang racket

(require redex/reduction-semantics)

(define-language lc/syntax
  (x variable-not-otherwise-mentioned)
  (v (lambda (x) e))
  (e v x (e e)))


(define-extended-language lc/cbn lc/syntax
  (E hole (E e)))

(define-extended-language lc/cbv lc/cbn
  (E .... (v E)))

(define-extended-language lc+/syntax lc/syntax
  (i 1 2)
  (v .... () (pair e e))
  (e .... (prj i e)))

(define-union-language lc+/cbn lc/cbn lc+/syntax)

;; Should have a macro to combine these two steps:
(define-union-language _lc+/cbv lc/cbv lc+/syntax)
(define-extended-language lc+/cbv _lc+/cbv
  (E .... (prj i E)))