Pattern matching a lazy language with Redex

pattern-matching-redex.rkt

#lang racket/base
(require redex)

(define-language L
  [x ::= variable-not-otherwise-mentioned]
  [c ::= number null] ; atoms

  [e ::= c (cons e e) x (roll [x] e) (+ e e)] ; expression
  [v ::= c (cons e e)] ; WHNF values
  [e\v ::= (roll [x] e) (+ e e)] ; non-value expressions (thunks?)

  [p ::= c (cons p p) x] ; pattern
  [vp ::= c (cons p p)] ; value pattern (e.g. non-variable)

  [Σ ::= ([x e] ...)] ; bindings
  [m ::= [p = e] (and m m) <ok> <fail>] ; matching
  [M ::= (and M m) (and <ok> M) hole] ; matching reduction context

  )

(define-metafunction L
  evaluate : e -> v
  [(evaluate v) v]
  [(evaluate (roll [x] e))
   (evaluate (substitute e x (roll [x] e)))]
  [(evaluate (+ e_1 e_2))
   ,(+ (term (evaluate e_1)) (term (evaluate e_2)))])

(define pattern-match
  (reduction-relation L
    #:domain (Σ m)

    (--> (Σ (in-hole M [vp = e\v]))
         (Σ (in-hole M [vp = (evaluate e\v)])))

    (--> (Σ           (in-hole M [x = e]))
         (([x e] . Σ) (in-hole M <ok>)))

    (--> (Σ (in-hole M [c_1 = c_1]))
         (Σ (in-hole M <ok>)))

    (--> (Σ (in-hole M [c_!_1 = c_!_1])) ; distinct atoms
         (Σ <fail>))

    (--> (Σ (in-hole M [(cons p_1 p_2) = (cons e_1 e_2)]))
         (Σ (in-hole M (and [p_1 = e_1] [p_2 = e_2]))))

    (--> (Σ (in-hole M [(cons p_1 p_2) = c]))
         (Σ <fail>))

    (--> (Σ (in-hole M (and <ok> <ok>)))
         (Σ (in-hole M <ok>)))

    ))