Strange construction in Redex, the generated examples produce a funny error.

ccon.rkt

#lang racket

(require redex)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; LANGUAGE

(define-language ccon
  (x y f ::= variable-not-otherwise-mentioned)
  (n     ::= integer)
  (b     ::= boolean)
  (unop  ::= not)
  (binop ::= + and or - > <)
  (c     ::= (channel n))
  (v     ::= b n (inl tv) (inr tv)
             unit
             (pair tv tv)
             (lambda (x_!_ ...) e) ;; _!_ means they must be unique
             s
             c) 
  (tv    ::= (thunk e) v)
  (ans   ::= tv (raise tv))
  (s     ::= eager semi future async)
  (e     ::= x ans (e e ...) (if e e e) 
             (pair e e) (unop e) (binop e e) 
             (case e x e x e) (injl e) (injr e)
             (delay e) (force e) 
             (raise e) (catch e e)
             (begin e e)
             (spawn T e) (chan e) (read e) (write e e)
             (check e e e)
             (predc e)
             (mraise e))
  (D     ::= hole
             (tv ... D e ...) (if D e e) 
             (pair D e) (pair tv D)
             (unop D)   (binop D e) (binop v D)
             (case D x e x e) (injl D) (injr D)
             (force D) (raise D) (catch D e)
             (begin D e)
             (chan D) (read D) (write D e) (write c D)
             (check D e e) (check v D e)
             (predc D)
             (mraise D))
  (E     ::= hole
             (tv ... E e ...) (if E e e) 
             (pair E e) (pair tv E)
             (unop E)   (binop E e) (binop v E)
             (case E x e x e) (injl E) (injr E)
             (force E) (raise E) (catch E e) (catch v E)
             (begin E e)
             (chan E) (read E) (write E e) (write c E)
             (check E e e) (check v E e)
             (predc E)
             (mraise E))
  (Th    ::= (Thread integer T e) (done ans))
  (T     ::= A U M)
  (P     ::= (para Th ... Th_1)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; REDUCTION RELATIONS

(define thread-number  0)
(define channel-number 0)

(define pstep
  (reduction-relation
   ccon
   (--> (para Th ... (Thread n T_0 (in-hole E (spawn T_1 e_0))) Th_2 ...)
        (para Th ... (Thread n T_0 (in-hole E unit)) (Thread n_1 T_1 e_0)   Th_2 ...)
        (where/hidden n_1 ,(begin (set! thread-number (add1 thread-number)) thread-number))
        "thread-spawn")
   (--> (para Th ... (Thread n T (in-hole E (chan tv))) Th_2 ...)
        (para Th ... (Thread n T (in-hole E (tv (channel n_1))))  Th_2 ...)
        (where n_1 ,(begin (set! channel-number (add1 channel-number)) channel-number))
        "chan-create")
   (--> (para Th ... (Thread n_1 T_1 (in-hole E_1 (read c))) Th_2 ... (Thread n_2 T_2 (in-hole E_2 (write c tv))) Th_3 ...)
        (para Th ... (Thread n_1 T_1 (in-hole E_1 tv))       Th_2 ... (Thread n_2 T_2 (in-hole E_2 unit))         Th_3 ...)
        "read-left")
   (--> (para Th ... (Thread n_1 T_1 (in-hole E_1 (write c tv))) Th_2 ... (Thread n_2 T_2 (in-hole E_2 (read c))) Th_3 ...)
        (para Th ... (Thread n_1 T_1 (in-hole E_1 unit))         Th_2 ... (Thread n_2 T_2 (in-hole E_2 tv))      Th_3 ...)
        "read-right")
   (--> (para Th ... (Thread n T e_0)   Th_2 ...)
        (para Th ... (Thread n T any_1) Th_2 ...)
        (where (any_1) ,(apply-reduction-relation step (term e_0)))
        "thread-step")
   (--> (para Th ... (Thread n U ans) Th_2 ...)
        (para Th ... (done ans)       Th_2 ...)
        "thread-done-user")
   (--> (para Th ... (Thread n M tv) Th_2 ...)
        (para Th ...                 Th_2 ...)
        "thread-done-mon")
   (--> (para Th ... (Thread n A tv) Th_2 ...)
        (para Th ...                 Th_2 ...)
        "thread-done-async")))

(define lambda?   (redex-match ccon (lambda (x_!_ ...) e)))
(define strat?    (redex-match ccon s))
(define thunk?    (redex-match ccon (thunk e)))
(define var?      (redex-match ccon x))


(define (non-usage-ctxt? E)
  (define app-ctxt?     (redex-match ccon (in-hole E_1 (tv ... E_0 e ...))))
  (define pair-l-ctxt?  (redex-match ccon (in-hole E_1 (pair E_0 e))))
  (define pair-r-ctxt?  (redex-match ccon (in-hole E_1 (pair E_0 e))))
  (define injl-ctxt?    (redex-match ccon (in-hole E_1 (injl E_0))))
  (define injr-ctxt?    (redex-match ccon (in-hole E_1 (injr E_0))))
  (define force-ctxt?   (redex-match ccon (in-hole E_1 (force E_0))))
  (define delay-ctxt?   (redex-match ccon (in-hole E_1 (delay E_0))))
  (define raise-ctxt?   (redex-match ccon (in-hole E_1 (raise E_0))))
  (define catch-r-ctxt? (redex-match ccon (in-hole E_1 (catch v E_0))))
  (define begin-ctxt?   (redex-match ccon (in-hole E_1 (begin E_0 e))))
  (define write-ctxt?   (redex-match ccon (in-hole E_1 (write c E_0))))
  (define mt-ctxt?      (redex-match ccon hole))
  (define predc-ctxt?   (redex-match ccon (in-hole E_1 (predc E_0))))  ;; Wrong, but it's a library fn so who cares
  (define mraise-ctxt?  (redex-match ccon (in-hole E_1 (mraise E_0)))) ;; Wrong, but it's a library fn so who cares
  (or (mt-ctxt? E) (app-ctxt? E) (begin-ctxt? E)
      (pair-l-ctxt? E) (pair-r-ctxt? E)
      (injl-ctxt? E)   (injr-ctxt? E)
      (force-ctxt? E)  (delay-ctxt? E)
      (raise-ctxt? E)  (catch-r-ctxt? E)
      (predc-ctxt? E) (mraise-ctxt? E)
      (write-ctxt? E)))
      
(define step
  (reduction-relation
   ccon
   (--> (in-hole E (binop tv_1 tv_2))
        (in-hole E (delta binop tv_1 tv_2))
        "binop")
   (--> (in-hole E (unop tv))
        (in-hole E (delta unop tv))
        "unop")
   (--> (in-hole E (if #t e_1 e_2))
        (in-hole E e_1)
        "ift")
   (--> (in-hole E (if #f e_1 e_2))
        (in-hole E e_2)
        "iff")
   (--> (in-hole E ((lambda (x ..._1) e) tv ..._1)) ;; _1 means 'must be the same length'
        (in-hole E e_1)
        (where e_1 (subst-n (x tv) ... e))
        "βv")
   (--> (in-hole E (begin tv_1 e_2))
        (in-hole E e_2)
        "begin")
   ;; Cases
   (--> (in-hole E (case (inl tv) x_1 e_1 x_2 e_2))
        (in-hole E (subst x_1 tv e_1))
        "casel")
   (--> (in-hole E (case (inr tv) x_1 e_1 x_2 e_2))
        (in-hole E (subst x_2 tv e_2))
        "caser")
   (--> (in-hole E (injl tv))
        (in-hole E (inl tv))
        "injl")
   (--> (in-hole E (injr tv))
        (in-hole E (inr tv))
        "injr")
   ;; Raise and Catch
   (--> (in-hole E (delay e)) 
        (in-hole E (thunk e))
        "thunk")
   (--> (in-hole E (force (thunk e)))
        (in-hole E e)
        "force-thunk")
   (--> (in-hole E (force v))
        (in-hole E v)
        "force-value")
   (--> (in-hole E (force c))
        (in-hole E c)
        "force-channel")
   ;; Exceptions
   (--> (in-hole D (raise tv))
        (raise tv)
        (side-condition (not (equal? (term hole) (term D))))
        "escape-raise")
   (--> (in-hole E (catch v (in-hole D (raise tv))))
        (in-hole E (v tv))
        "catch")
   (--> (in-hole E (catch v tv))
        (in-hole E tv)
        "no-raise")
   ;; Contracts
   (--> (in-hole E (check v eager e))
        (in-hole E (chan (lambda (x)
                           (begin
                             (spawn M (write x (catch (lambda (x) (injr x)) (injl (v e)))))
                             (mraise (read x))))))
        "check-eager")
   (--> (in-hole E (check v semi e))
        (in-hole E (chan (lambda (x)
                           (begin
                             (spawn M (write x (catch (lambda (x) (injr x)) (injl (delay (v e))))))
                             (mraise (read x))))))
        "check-semi")
   (--> (in-hole E (check v future e))
        (in-hole E (chan (lambda (x)
                           (begin
                             (spawn M (write x (catch (lambda (x) (injr x)) (injl (v e)))))
                             (delay (mraise (read x)))))))
        "check-future")
   (--> (in-hole E (check v async e))
        (in-hole E (begin
                     (spawn A (v e))
                     e))
        "check-async")
   (--> (in-hole E (predc tv))
        (in-hole E ((lambda (f) (lambda (x) (if (f x) x (raise x)))) tv))
        "predc")
   (--> (in-hole E (mraise tv))
        (in-hole E ((lambda (y) (case y x x x (raise x))) tv))
        "maybe-raise")
   ;; Invalid Cases
   (--> (in-hole E (thunk e))
        (error "Thunk used in invalid position")
        (side-condition (not (non-usage-ctxt? (term E))))
        "invalid-thunk")
   (--> (in-hole E (check tv_1 tv_2 e))
         (error "Invalid use of check")
         (side-condition (or (not (lambda? (term tv_1))) (not (strat? (term tv_2)))))
         "invalid-check")
   (--> (in-hole E (case tv x_1 e_1 x_2 e_2))
        (error "Invalid case value")
        (side-condition
          (and (not ((redex-match ccon (inl tv)) (term tv)))
               (not ((redex-match ccon (inr tv)) (term tv)))))
        "invalid-case")
   (--> (in-hole E (if tv e_1 e_2))
        (error "Invalid if value")
        (side-condition (not ((redex-match ccon boolean) (term tv))))
        "invalid-if")
   (--> (in-hole E (tv_1 tv ...))
        (error "Invalid operator")
        (side-condition (not (lambda? (term tv_1))))
        "invalid-op")
   (--> (in-hole E x) 
        (error "free var")
        "free-var")))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; METAFUNCTIONS

(define-metafunction ccon
  delta : any ... -> any
  [(delta + number_1 number_2)     ,(+ (term number_1) (term number_2))]
  [(delta - number_1 number_2)     ,(- (term number_1) (term number_2))]  
  [(delta > number_1 number_2)     ,(> (term number_1) (term number_2))]
  [(delta < number_1 number_2)     ,(< (term number_1) (term number_2))]
  [(delta and boolean_1 boolean_2) ,(and (term boolean_1) (term boolean_2))]
  [(delta or boolean_1 boolean_2)  ,(or (term boolean_1) (term boolean_2))]
  [(delta not boolean)             ,(not (term boolean))]
  [(delta _   _)                   (error "Invalid unary operation")]
  [(delta _ _ _)                   (error "Invalid binary operation")])

;; Subst e1 for x in e2 as (subst-n x e1 e2)
(define-metafunction ccon
  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])

(define-metafunction ccon
  subst : x any any -> any 
  [(subst x any x) any]
  [(subst x_1 any_1 (lambda (x_2 ... x_1 x_3 ...) any_2))
   (lambda (x_2 ... x_1 x_3 ...) any_2)]
  ;; capture avoiding case
  [(subst x_1 any_1 (lambda (x_2 ...) any_2))
   (lambda (x_new ...) 
     (subst x_1 any_1 (subst-vars (x_2 x_new) ...  any_2)))
   (where 
     (x_new ...) 
     ,(variables-not-in (term (x_1 any_1 any_2)) (term (x_2 ...))))]
  [(subst x_1 any_1 (case e_1 x_2 e_2 x_3 e_3))
   (case (subst x_1 any_1 e_1) x_2 e_4 x_3 e_5)
   (where e_4
      ,(if (equal? (term x_1) (term x_2)) (term e_2) (term (subst x_1 any_1 e_2))))
   (where e_5
      ,(if (equal? (term x_1) (term x_3)) (term e_3) (term (subst x_1 any_1 e_3))))]
  [(subst x_1 any_1 (thunk e)) (thunk e)]
  [(subst x_1 any_1 (any_2 ...))
   ((subst x_1 any_1 any_2) ...)]
  [(subst x_1 any_1 any_2) any_2])

(define-metafunction ccon
  subst-vars : (x any) ... any -> any
  [(subst-vars (x_1 any_1) x_1) any_1]
  [(subst-vars (x_1 any_1) (any_2 ...)) 
   ((subst-vars (x_1 any_1) any_2) ...)]
  [(subst-vars (x_1 any_1) any_2) any_2]
  [(subst-vars (x_1 any_1) (x_2 any_2) ... any_3) 
   (subst-vars (x_1 any_1) (subst-vars (x_2 any_2) ... any_3))]
  [(subst-vars any) any])

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; TESTING

(test-->> step (term (injl 5)) (term (inl 5)))
(test-->> step
          (term (case (injl 5) x x x x)) 5)
(test-->> step (term (lambda (x) x)) (term (lambda (x) x)))
(test-->> step (term ((lambda (x) x) 5)) 5)

;; Raise and Catch
(test-->> step (term ((lambda (x) (raise x)) 5)) (term (raise 5)))
(test-->> step (term (catch (lambda (x) x) (raise 5))) 5)
(test-->> step (term (catch (lambda (x) x) (+ 2 (raise 5)))) 5)
(test-->> step (term (catch (lambda (x) x) (+ 2 5))) 7)
(test-->> step (term (catch (lambda (x) x) ((lambda (x) x) (+ 2 (raise 5))))) 5)
(test-->> step (term (catch (lambda (x) (injr x)) (injl ((lambda (x) x) 5)))) (term (inl 5)))


;; Delay and Force
(test-->> step (term (delay (+ 2 3))) (term (thunk (+ 2 3))))
(test-->> step (term ((lambda (x) (force x)) (delay (+ 2 3)))) 5)

;; Parallelism
(test-->> pstep
          (term (para (Thread 0 U (begin (spawn U (+ 3 4)) (+ 2 3)))))
          (term (para (done 5) (done 7))))

(test-->> pstep
          (term (para (Thread 0 U (write (channel 0) 5)) (Thread 1 U (read (channel 0)))))
          (term (para (done unit) (done 5))))

(test-->> pstep
          (term (para (Thread 0 U (chan (lambda (x) (begin (spawn U (write x 5)) (read x)))))))
          (term (para (done 5) (done unit))))

(test-->> pstep
          (term (para (Thread 0 U (chan (lambda (x) (begin (spawn U (write x (+ 2 5))) (read x)))))))
          (term (para (done 7) (done unit))))

(test-->> pstep
          (term (para (Thread 0 U (chan (lambda (x) (begin (spawn U (write x 5)) (+ (read x) 3)))))))
          (term (para (done 8) (done unit))))

;; Contracts
(test-->> pstep
          (term (para (Thread 0 U (check (lambda (x) x) eager 5))))
          (term (para (done 5))))

(test-->> pstep
          (term (para (Thread 0 U (check (lambda (x) (raise x)) eager 5))))
          (term (para (done (raise 5)))))

(test-->> pstep
          (term (para (Thread 0 U (check (lambda (x) (raise x)) semi 5))))
          (term (para (done (thunk ((lambda (x) (raise x)) 5))))))

(test-->> pstep
          (term (para (Thread 0 U (check (lambda (x) (raise x)) future 5))))
          (term (para (done (thunk (mraise (read (channel 7))))) (Thread 8 M (write (channel 7) (inr 5))))))

(test-->> pstep
          (term (para (Thread 0 U (check (lambda (x) (raise x)) async 5))))
          (term (para (done 5) (Thread 9 A (raise 5)))))

(test-->> pstep
          (term (para (Thread 0 U (check (predc (lambda (x) (> x -1))) eager 5))))
          (term (para (done 5))))

(test-->> pstep
          (term (para (Thread 0 U (check (predc (lambda (x) (> x -1))) eager -2))))
          (term (para (done (raise -2)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; AUTOTESTING

;; Processes, Round One
;; Of course this doesn't work. We can't always step with the small step,
;; and the process stepp is nondeterministic. Neat that it works, though!
(define (single-step? p)
  (= (length (apply-reduction-relation pstep p)) 1))

(define value? (redex-match ccon (para (done tv))))

(redex-check ccon P
             (or (value? (term P)) (single-step? (term P))))

;; Term Language
;; Since we can't check for processes, but we still want to ask abou terms,
;; let's do that. Either:
;; - it's an answer
;; - it can step
;; - it produces an error
;; - it's trying to eval a process instruction.
;;
;; We must check for all of these.

(define (answer-e? e)
  (define value? (redex-match ccon tv))
  (define raise? (redex-match ccon (raise tv)))
  (or (value? e) (raise? e)))

(define (single-step-e? e)
  (= 1 (length (apply-reduction-relation step e))))

(define (contains-proc-step? e)
  (define chan?  (redex-match ccon (in-hole E (chan e))))
  (define spawn? (redex-match ccon (in-hole E (spawn T e))))
  (define write? (redex-match ccon (in-hole E (write e_1 e_2))))
  (define read?  (redex-match ccon (in-hole E (read e))))
  (or (chan? e) (spawn? e) (write? e) (read? e)))

(define (error-e? e)
  (let ([red (apply-reduction-relation step e)])
    (and (< 0 (length red))
         (andmap (lambda (x) (equal? (car x) (term error))) red))))

(define (display-term e)
  (print e)
  (newline)
  (flush-output))

;; Sanity Check, but it doesn't sane
(redex-check
 ccon e
 (begin
   ;; (display-term (term e))
   ((redex-match ccon e) (term e)))
 #:attempts 15000
 #:retries   1000)

(redex-check
 ccon e
 (begin
   ;; (display-term (term e))
   (or (answer-e?           (term e))
       (single-step-e?      (term e))
       (contains-proc-step? (term e))
       (error-e?            (term e))))
 #:attempts 15000
 #:retries   1000)

;; Processes, Round Two
;; Let's try processes again, but this time we'll look at a
;; many-step arrangement instead.

(define (many-step? p)
  (< 0 (length (apply-reduction-relation pstep p))))

(define values? (redex-match ccon (para (done ans) ...)))

(redex-check
 ccon P
 (or (values? (term P)) (many-step? (term P)))
 #:attempts 1500)

;; Slick, and it works!