blazes.redex

#lang racket
(require redex)
(define-language Blazes
  (ex stream
      ('apply component ex)
      ('combine ex ex ex ...)
      )
  (stream 'Async 'Taint ('NDRead label))
  ;(component (order op label) (order op))
  (component (order op label))
  (order 'C 'O)
  (op 'R 'W)
  ;(label 'None string)
  (label 'None)
 
  (e-cxt ('apply component e-cxt)
         ('combine ex ... e-cxt ex ...)
         hole)
)


(define red
  (reduction-relation
  Blazes
  (==> ('apply ('O 'W _) 'Async)
       'Taint
       "Taint1")
  (==> ('apply _ 'Taint)
       'Taint
       "Taint2")
  (==> ('combine _ ... 'Taint _ ...)
       'Taint
       "Taint3")
  (==> ('apply ('O 'R label) 'Async)
       ('NDread label)
       "NDRead")
  (==> ('apply ('C _ _) 'Async)
       'Async
       "clean")
  (==> ('combine 'Async 'Async ...)
       'Async
       "reduce")
  with
  [(--> (in-hole e-cxt a) (in-hole e-cxt b))
   (==> a b)]))








;----------------------------------------------------------------




(define (reduces? e)
  (not (null? (apply-reduction-relation
               red
               (term (,e))))))

(define (doreduce e)
  ;(display "does it reduce?  ")
  ;(display e)
  ;(display "-----------\n")
  ;(display (apply-reduction-relation red (term (,e))))
  ;(display "==================\n")
  (apply-reduction-relation red (term (,e)))
  )

(define (matches-stream? e)
  (and (not (null? e))
   (not (null? (redex-match Blazes stream e)))))

(define (isastream? e)
   ;(write e)
   ;(display "\n---------->")
   ;(display (doreduce e))
   ;(display "\n")
  (or (matches-stream? e) 
      (matches-stream? (doreduce e)))
  )





(let ([c (make-coverage red)])
    (parameterize ([relation-coverage (list c)])
      (check-reduction-relation
       red
       (λ (p) (andmap isastream? p)))
      (covered-cases c)))