More sophisticated lazy language with pattern matching & eval interleaved

glorious-haskill-redex.rkt

#lang racket/base
(require redex)

(define-language Haskill
  [x ::= variable-not-otherwise-mentioned]
  [ctor ::= cons null A B C #t #f]

  ; expressions
  [e ::=
     x
     ctor
     (e e ...)
     (fix (x) e)
     (λ (p ...) e)
     (case e [p e] ...)
     (match m e e)  ; note: used internally, not "surface syntax"
     undefined]
  [v ::=
     ctor
     (ctor e ...)
     (λ (p ...) e)]

  ; patterns
  [p ::= x ctor (ctor p ...)]
  [vp ::= ctor (ctor p ...)]

  ; matching terms
  [m ::=
     [p = e]
     (and m ...)
     (ok Σ)
     (fail)]
  [Σ ::= ([x e] ...)]

  ; expression reduction context
  [E ::=
     (match (in-hole M [vp = E]) e e)
     (E e ...)
     hole]

  ; match reduction context
  [M ::=
     (and (ok Σ) ... M m ...)
     hole]

  ; M inside E
  [EM ::= (in-hole E (match M e e))])

(define-metafunction Haskill
  app* : (Σ ...) -> Σ
  [(app* (([x_i e_i] ...) ...)) ([x_i e_i] ... ...)])

(define-metafunction Haskill
  subst* : Σ e -> e
  [(subst* () e) e]
  [(subst* ([x_1 e_1] [x_i e_i] ...) e)
   (subst* ([x_i e_i] ...) (substitute e x_1 e_1))])

(define-metafunction Haskill
  split : vp v -> ([p e] ...) or #f
  [(split ctor_1 ctor_1) ()]
  [(split (ctor_1 p_i ..._n) (ctor_1 e_i ..._n)) ([p_i e_i] ...)]
  [(split _ _) #f])

(define rr
  (reduction-relation Haskill
    #:domain e

    ;; evaluation

    (--> (in-hole E (fix (x) e))
         (in-hole E (substitute e x (fix (x) e)))
         "E-fix")

    (--> (in-hole E ((λ (p_i ..._n) e) e_i ..._n))
         (in-hole E (match (and [p_i = e_i] ...) e undefined))
         "E-beta")

    (--> (in-hole E (case e [p_1 e_1] [p_i e_i] ...))
         (in-hole E (match [p_1 = e] e_1 (case e [p_i e_i] ...)))
         "E-case")

    (--> (in-hole E (case e))
         (in-hole E undefined)
         "E-case-mt")

    (--> (in-hole E (match (ok Σ) e_1 e_2))
         (in-hole E (subst* Σ e_1))
         "E-ok")

    (--> (in-hole E (match (fail) e_1 e_2))
         (in-hole E e_2)
         "E-fail")


    ;; pattern matching

    (--> (in-hole EM [x = e])
         (in-hole EM (ok ([x e])))
         "M-bind")

    (--> (in-hole EM [vp = v])
         (in-hole EM (and [p_i = e_i] ...))
         "M-split"
         (where ([p_i e_i] ...) (split vp v)))

    (--> (in-hole EM [vp = v])
         (in-hole EM (fail))
         "M-fail"
         (where #f (split vp v)))

    (--> (in-hole EM (and (ok Σ_i) ...))
         (in-hole EM (ok (app* (Σ_i ...))))
         "M-ok*")

    (--> (in-hole EM (and (ok Σ_i) ... (fail) m ...))
         (in-hole EM (fail))
         "M-fail*")

    ))