racket / redex

Other
93 stars 36 forks source link

`generate-term` from reduction relation bypasses `#:domain`. #214

Open florence opened 4 years ago

florence commented 4 years ago

Concider:

#lang racket
(require redex/reduction-semantics)
(define-language L)
(define r
  (reduction-relation
   L
   #:domain 1
   (--> any any)))

(generate-term #:source r 5)

This will generate things like, say strings, which are not 1. I would expect this generation to, at least, fail when it attempts to generate a term outside of the domain of the relation.