racket / redex Goto Github PK

License: Other

Racket 100.00%

redex's Introduction

redex

This the source for the Racket packages: "redex", "redex-benchmark", "redex-doc", "redex-examples", "redex-gui-lib", "redex-lib", "redex-pict-lib", "redex-test".

Contributing

Contribute to Racket by submitting a pull request, reporting an issue, joining the development mailing list, or visiting the IRC or Slack channels.

License

Racket, including these packages, is free software, see LICENSE for more details.

By making a contribution, you are agreeing that your contribution is licensed under the Apache 2.0 license and the MIT license.

redex's People

Contributors

Stargazers

Watchers

redex's Issues

`render-language` skips aliases in extended language

#lang racket
(require redex)
(define-language a
  (p q ::= natural))
(define-extended-language b a
  (P Q ::= natural))

(render-language b)

renders as P ::= natural

Running some ellipsis patterns in define-judgment-form causes syntax error.

There is a small issue with the parsing of ellipsis patterns in define-judgment-form. The following file gets the error in racket 6.2. There are some observations about the pattern in the use and test cases.

#lang racket

(require redex)

(define-language L
  (t ::= () (t ... -> t)))

(define-judgment-form L
  #:mode (≈ I I)
  #:contract (≈ t t)
  [-------------------- "≈Refl"
   (≈ () ())]
  [(≈ t_1 t_2)
   ;; I have the intuition that this should be the same as
   ;; (≈* (τ_1 ...) (γ_1 ...))
   (≈ t_n t_m) ... 
   ------------------------------------------ "≈->"
   (≈ (t_n ... -> t_1) (t_m ... -> t_2))
   ;; The following conclusion gets rid of this error.
   #;(≈ (t_n ..._n -> t_1) (t_m ..._n -> t_2))])

(define-judgment-form L
  #:mode (≈* I I)
  #:contract (≈* (t ...) (t ...))
  [--------- "≈*base"
   (≈* () ())]
  [(≈ t_1 t_2) (≈* (t_n ...) (t_m ...))
   ---------------------- "≈->"
   (≈* (t_1 t_n ...) (t_2 t_m ...))])

(module+ test
  (test-true  (judgment-holds (≈ () ())))
  (test-true  (judgment-holds (≈ (-> ()) (-> ()))))
  (test-true  (judgment-holds (≈ (() -> ()) (() -> ()))))
  (test-true  (judgment-holds (≈ (() () -> ()) (() () -> ()))))
  (test-false (judgment-holds (≈ () (-> ()))))
  ;; This test causes this pattern mentioned above to report
  ;; the following error.
  ;;syntax: incompatible ellipsis match counts for template in: ...
  (test-false (judgment-holds (≈ (-> ()) (() -> ()))))
  )

(module+ test (test-results))

;; Helpers to consider abstracting

(define-syntax-rule (test-true e)
  (test-equal e #t))

(define-syntax-rule (test-false e)
  (test-equal e #f))

Caching causes incorrect behavior in substitute

#lang racket

(require redex/reduction-semantics)

(define-language lc
  (e ::= x
     (λ (x) e)
     (e e))
  (x ::= variable-not-otherwise-mentioned))
(parameterize ([default-language lc])
  (term (substitute (x (λ (x) x)) x y)))


(define-language lc2
  (e ::= x
     (λ (x) e)
     (e e))
  (x ::= variable-not-otherwise-mentioned)
  #:binding-forms
  (λ (x) e #:refers-to x))
(parameterize ([default-language lc2])
  (term (substitute (x (λ (x) x)) x y)))

This program produces:

'(y (λ (y) y))
'(y (λ (y) y))

Even though default-language is parameterized differently in each example. It seems like the caching should take the language into account as well when the metafunction relies on the value of default-language

side-condition/hidden not supported in define-language

using side-condition in a language definition works great, but using side-condition/hidden does not (it just treats it like a literal s-expression, I believe)

#lang racket
(require redex)

(define (unique? l)
  (equal? l (remove-duplicates l)))

(define-language DTR
  [e  ::= x
      (side-condition (λ (x_ ...) e)
                      (unique? (term (x_ ...))))
      ;; (side-condition/hidden (λ (x_ ...) e) ; doesn't work =(
      ;;                        (unique? (term (x_ ...))))
      (e e ...)]
  [x  ::= variable-not-otherwise-mentioned])

(module+ test
  (test-equal (redex-match? DTR e (term (λ (x x) x))) #f)
  (test-equal (redex-match? DTR e (term (λ (x y) (x y)))) #t))

`judgment-holds` and `test-judgment-holds` fail when pattern matching alpha-equiv terms

Example:

#lang racket
(require redex)
(define-language λ
  (e ::=
     (lambda (x) e)
     (e e)
     x)
  (x ::= variable-not-otherwise-mentioned)
  #:binding-forms
  (lambda (x) e #:refers-to x))


(define-judgment-form λ
  #:mode (traverse I O)
  [(traverse e e_*)
   ---------- "lambda"
   (traverse (lambda (x) e) (lambda (x) e_*))]
  [---------- "x"
   (traverse x x)]
  [(traverse e_1 e_1*)
   ---------- "left"
   (traverse (e_1 e_2) (e_1* e_2))]
  [(traverse e_2 e_2*)
   ---------- "right"
   (traverse (e_1 e_2) (e_1 e_2*))])
(judgment-holds (traverse ((lambda (x) (x x)) (lambda (x) (x x)))
                          any)
                any)
;; returns '(((lambda (x«2») (x«2» x«2»)) (lambda (x) (x x))))
(judgment-holds (traverse ((lambda (x) (x x)) (lambda (x) (x x)))
                          ((lambda (x) (x x)) (lambda (x) (x x)))))
;; returns #f, I would expect it to return #t

Internal error on pattern match

The following program produces an internal error for me:

#lang racket/base

(require redex)

(define-language lang
  [m (variable-prefix m)]
  [h f m])

(redex-match lang (term foo))

The error looks like this:

format: format string requires 0 arguments, given 1; arguments were: "^" "m"
  context...:
   /home/asumu/plt/racket-git/racket/share/pkgs/redex-lib/redex/private/ambiguous.rkt:259:8: for-loop
   /home/asumu/plt/racket-git/racket/share/pkgs/redex-lib/redex/private/ambiguous.rkt:274:15: for-loop
   /home/asumu/plt/racket-git/racket/share/pkgs/redex-lib/redex/private/ambiguous.rkt:267:2: for-loop
   /home/asumu/plt/racket-git/racket/share/pkgs/redex-lib/redex/private/ambiguous.rkt:264:0: build-overlapping-productions-table
   /home/asumu/plt/racket-git/racket/share/pkgs/redex-lib/redex/private/ambiguous.rkt:27:0: build-ambiguity-cache
   /home/asumu/plt/racket-git/racket/collects/racket/contract/private/arrow-val-first.rkt:265:18
   /home/asumu/plt/racket-git/racket/share/pkgs/redex-lib/redex/private/matcher.rkt:124:0: compile-language
   /home/asumu/plt/racket-git/racket/collects/racket/contract/private/arrow-val-first.rkt:265:18
   /home/asumu/tmp/redex/model.rkt: [running body]

I'm running Redex on commit 13bb16c so I think I'm up-to-date.

internal `redex-check` error on `_!_` patterns

Example program:

#lang racket
(require redex/reduction-semantics)

(define-language lang
  (S ::= variable))

(redex-check lang (S_!_g S_!_g ...) #t)

The error:

t-env-misname-ref: contract violation
  expected: Integer
  given: '(nt S)
  in: the 3rd argument of
      (-> t-env? Symbol Integer Any)
  contract from:
      <pkgs>/redex-lib/redex/private/env.rkt
  blaming: <pkgs>/redex-lib/redex/private/enum.rkt
   (assuming the contract is correct)
  at: <pkgs>/redex-lib/redex/private/env.rkt:15.9
  context...:
   /Applications/Racket/racket/collects/racket/contract/private/blame.rkt:159:0: raise-blame-error16
   /Applications/Racket/racket/collects/racket/contract/private/arrow-higher-order.rkt:340:33
   /Users/florence/playground/redex/redex-lib/redex/private/enum.rkt:253:5
   /Users/florence/playground/redex/redex-lib/redex/private/enum.rkt:295:5: for-loop
   /Users/florence/playground/redex/redex-lib/redex/private/enum.rkt:294:2
   /Users/florence/playground/redex/redex-lib/redex/private/enum.rkt:294:2
   /Applications/Racket/racket/collects/racket/private/list.rkt:321:16: composed
   to-term
   /Applications/Racket/racket/collects/racket/contract/private/arrow-val-first.rkt:357:18
   /Users/florence/playground/redex/redex-lib/redex/private/generate-term.rkt:324:5
   /Users/florence/playground/redex/redex-lib/redex/private/generate-term.rkt:445:2: loop
   /Users/florence/playground/redex/redex-lib/redex/private/generate-term.rkt:419:0: check-one
   /Users/florence/tmp/rederr.rkt: [running body]

`judgment-holds` does not collapse alpha equivalent terms

If I have a judgment-holds that outputs two alpha equivalent terms then judgment-holds should collapse them.

Example:

(define-language λ
  (e ::=
     (lambda (x) e)
     (e e)
     x)
  (x ::= variable-not-otherwise-mentioned)
  #:binding-forms
  (lambda (x) e #:refers-to x))


(define-judgment-form λ
  #:mode (traverse I O)
  [(traverse e e_*)
   ---------- "lambda"
   (traverse (lambda (x) e) (lambda (x) e_*))]
  [---------- "x"
   (traverse x x)]
  [(traverse e_1 e_1*)
   ---------- "left"
   (traverse (e_1 e_2) (e_1* e_2))]
  [(traverse e_2 e_2*)
   ---------- "right"
   (traverse (e_1 e_2) (e_1 e_2*))])
(judgment-holds (traverse ((lambda (x) (x x)) (lambda (x) (x x)))
                      any)
                any)
;; outputs a list of two expressions:
;; '(((lambda (x) (x x)) (lambda (x«2») (x«2» x«2»))) ((lambda (x«2») (x«2» x«2»)) (lambda (x) (x x))))
;; but should output something alpha equivalent to '(((lambda (x) (x x)) (lambda (x«2») (x«2» x«2»)))
(alpha-equivalent? λ
                   (term ((lambda (x) (x x)) (lambda (x«2») (x«2» x«2»))))
                   (term ((lambda (x«2») (x«2» x«2»)) (lambda (x) (x x)))))
;; outputs #t

Problem with apply-reduction-relation and nested ... binding

Apparently, an empty list of binders nested under another possibly empty list of binders will cause problems when used with apply-reduction-relation (maybe other things, e.g., compiled-pattern?)

The below file crashes with this error:

 match-define: no matching clause for '()                                                                                                                                                                                                      
 ....redex/redex-lib/redex/private/binding-forms.rkt:495:7                                                                                                                                                                                     
 Context:                                                                                                                                                                                                                                      
  ....racket/racket/collects/racket/match/runtime.rkt:23:0 match:error                                                                                                                                                                         
  ....redex/redex-lib/redex/private/binding-forms.rkt:479:2 loop                                                                                                                                                                               
  ....redex/redex-lib/redex/private/binding-forms.rkt:479:2 loop                                                                                                                                                                               
  ....redex/redex-lib/redex/private/binding-forms.rkt:634:4 loop                                                                                                                                                                               
  ....redex/redex-lib/redex/private/binding-forms.rkt:634:4 loop                                                                                                                                                                               
  ....redex/redex-lib/redex/private/binding-forms.rkt:634:4 loop                                                                                                                                                                               
  ....redex/redex-lib/redex/private/binding-forms.rkt:630:0 rec-freshen-spec                                                                                                                                                                   
  ....redex/redex-lib/redex/private/binding-forms.rkt:116:0 freshen                                                                                                                                                                            
  ....redex/redex-lib/redex/private/matcher.rkt:766:13 compiled-pattern                                                                                                                                                                        
  ....redex/redex-lib/redex/private/matcher.rkt:592:0 match-pattern                                                                                                                                                                            
  ....redex/redex-lib/redex/private/reduction-semantics.rkt:979:9                                                                                                                                                                              
  ....redex/redex-lib/redex/private/reduction-semantics.rkt:257:0 apply-reduction-relation/tagged                                                                                                                                              
  ....redex/redex-lib/redex/private/reduction-semantics.rkt:2538:2                                                                                                                                                                             
  ....redex/redex-lib/redex/private/reduction-semantics.rkt:2706:0 test-->>/procs                                                                                                                                                              
  (submod /tmp/meow.rkt test):1:1 [running body]

#lang racket/base
(require redex/reduction-semantics)

(define-language lc
  (x ::= variable-not-otherwise-mentioned)
  (e ::= (λ x ... e) () (e e ...))
  #:binding-forms
  (λ x #:...bind (clauses x (shadow clauses x)) any_body #:refers-to clauses))

(define-metafunction lc
  subst-all : e (x ...) (e ...) -> e
  [(subst-all e () ()) e]
  [(subst-all e (x x_r ...) (e_x e_r ...))
   (subst-all (substitute e x e_x) (x_r ...) (e_r ...))])

(define lc-->
  (reduction-relation lc
   (--> ((λ x ..._0 e) e_a ..._0)
        (subst-all e (x ...) (e_a ...)))))

(module+ test
  (test-->> lc--> (term (λ ())) (term (λ ())))
  (test-->> lc--> (term (λ x (λ x ()))) (term (λ x (λ x ()))))
  (test-results)
  (test-->> lc--> (term (λ (λ ()))) (term (λ (λ ())))) ;; crashes here
  (test-->> lc--> (term (λ x (λ ()))) (term (λ x (λ ())))) ;; and here
  (test-results))

build-derivations doesn't save names at leaves

The leaves in a derivation returned by build-derivations don't seem to have names, even when the rules used have names in the judgment-form.

For example, see the example given in the documentation:

> (build-derivations (even (s (s z))))
(list
 (derivation '(even (s (s z))) "even2" (list (derivation '(even z) "" '()))))

The leaf of the derivation uses "evenz", but the name given is "".

"Unbound pattern variable" for pattern variable used as output of judgment form

Here is a small example. While I probably shouldn't actually be doing this, I think it should work.

#lang racket/base

(require redex/reduction-semantics)

(define-language nats
  (n ::= z (s n)))

(define-judgment-form nats    
  #:mode (plus I I O)
  #:contract (plus n n n)

  [-------- "plusz"
   (plus z n n)]

  [(plus n n_0 n_1)
   ---------------- "pluss"
   (plus (s n) n_0 (s n_1))])

(define-judgment-form nats    
  #:mode (not-plus I I O)
  #:contract (not-plus n n n)

  [(side-condition ,(not (judgment-holds (plus n_0 n_1 n))))
   -------- "not-plus"     
   (not-plus n_0 n_1 z)])

(judgment-holds (not-plus z (s z) z))

compatible-closure fails for non-terminals with multiple non-terminal names

If a non-terminal has multiple names, i.e. multiple meta-variables by which it can be referred to, then compatible-closure can fail to produce the correct reduction relation depending on which name it is given.

Here is a small test: https://gist.github.com/wilbowma/8ee2e47c9d0f443ddd81
I expect both test cases to pass, but the second one fails. The non-terminal definition only uses the name e, and the first test calls the non-terminal by that name. The second test appears to fail because, while the non-terminal is also named m, it is not defined using that name.

Binding spec fails to detect ellipsis depth issue

Here is an example program that demonstrates the problem:

#lang racket

(require redex)

(define-language lang
  (e (thing e* ([x e] ...))
     integer)
  (e* integer)
  (x variable-not-otherwise-mentioned)
  #:binding-forms
  (thing e* #:refers-to x ([x e] ...)))

(parameterize ([default-language lang])
  (term (substitute (thing 0 ([x 0])) x 1)))

When I run this, I get the following error:

second: list contains too few elements
  list: '((x«0» ((x x«0»))))
  context...:
   /home/asumu/plt/racket-git/racket/share/pkgs/redex-lib/redex/private/binding-forms.rkt:624:4: loop
   /home/asumu/plt/racket-git/racket/share/pkgs/redex-lib/redex/private/binding-forms.rkt:624:4: loop
   /home/asumu/plt/racket-git/racket/share/pkgs/redex-lib/redex/private/binding-forms.rkt:624:4: loop
   /home/asumu/plt/racket-git/racket/share/pkgs/redex-lib/redex/private/binding-forms.rkt:620:0: rec-freshen-spec
   /home/asumu/plt/racket-git/racket/share/pkgs/redex-lib/redex/private/binding-forms.rkt:146:0: safe-subst
   /home/asumu/plt/racket-git/racket/share/pkgs/redex-lib/redex/private/reduction-semantics.rkt:1424:42
   /home/asumu/plt/racket-git/racket/collects/racket/private/map.rkt:21:13: map
   /home/asumu/plt/racket-git/racket/share/pkgs/redex-lib/redex/private/reduction-semantics.rkt:1724:24: loop
   /tmp/redex.rkt: [running body]

The binding spec I wrote should probably be rejected. If the non-terminal e* is replaced with e in thing, it's actually rejected.

links in long tutorial broken

links to *.rkt files in the long tutorial do not work.

For example, the link to common.rkt leads to http://docs.racket-lang.org/redex/common.rkt for which I get a 403 forbidden response.

Feature Request: Add an expected pattern to `test-judgment-holds`

Something like:

(test-judgment-holds (traverse ((lambda (x) (x x)) (lambda (x) (x x))) any) ;; judgment
                     any ;; output
                     ((lambda (x) (x x)) (lambda (x) (x x)))) ;; expected pattern

This would fail in the same cases as

(test-judgment-holds (traverse ((lambda (x) (x x)) (lambda (x) (x x)))
                               ((lambda (x) (x x)) (lambda (x) (x x)))))

But would give a better error message than "judgment of traverse didn't hold". (Ie it would say "Expected pattern but found .

This would make debugging test failures a little easier when the judgement "held" for some pattern that wasn't the one you expected.

Language nonterminals and (side-conditions (in-hole ...) ...)

I'm getting an unexpected error when using side-conditions over in-hole patterns in language nonterminal definitions. The pattern variables don't seem to get bound in the guard expression unless I add an _ to each pattern name.

E.g. Here is a small example that I think should work:

#lang racket/base

(require
  redex/reduction-semantics)

(define-language testL
  (e ::= natural x (e e))
  (x ::= variable-not-otherwise-mentioned)
  (Θ ::= hole (Θ e)))

(define-metafunction testL
  arity : x -> natural
  [(arity add1) 1]
  [(arity +) 2])

(define-metafunction testL
  Θ-length : Θ -> natural
  [(Θ-length hole) 0]
  [(Θ-length (Θ e)) ,(add1 (term (Θ-length Θ)))])

(define-extended-language test-redL testL
  (Θv ::= hole (Θv v))
  (v ::= natural
         (side-condition
           (in-hole Θv x)
           (not (equal? (term (Θ-length Θv))
                        (term (arity x)))))))

(module+ test
  (require rackunit)
  (check-true (redex-match? test-redL Θv (term (hole 1))))
  (check-equal?
    (term (Θ-length (hole 1)))
    1)
  (check-true (redex-match? test-redL v (term (+ 1))))
  (check-false (redex-match? test-redL v (term ((+ 1) 1)))))

However, this doesn't work unless I change the side-condition pattern to the following (or similar).

(side-condition
  (in-hole Θv_0 x_0)
  (not (equal? (term (Θ-length Θv_0))
               (term (arity x_0)))))

If this is intended, it seems to be poorly documented.

`check-redudancy` is Misspelled

It should be check-redundancy

Dobule pipes in language not rendered

EDIT: I figured my mistake. See post below.

Minimal working example

#lang racket
(require redex)

(define-language pipe
  [operator ::= \| || \|||])

(module+ test
  (test-equal (redex-match? pipe operator (term \|)) #t)
  (test-equal (redex-match? pipe operator (term ||)) #t)
  (test-equal (redex-match? pipe operator (term \|||)) #t))

(render-language pipe)

Expected behavior

The typeset version of the grammar should include the double pipes in || and |||.

Current behavior

The typeset version of the grammar omits double pipes.

Caveat

Granted, having pipes on the grammar confuses things, since pipes are already used as or in BNF notation. But I'm fine with the font alone distinguishing between BNF operator and language terminal—this lets me stay closer to the language I'm modeling, in which || is an operator.

Can you please confirm that my proposal is indeed expected behavior? If so, can you please help me fix it?

Thanks a lot!

`redex-check` doesn't warn about ellipsis in judgment-forms more than one level deep

#lang racket
(require redex/reduction-semantics)

(define-language simple-plus
  (M (e e))
  (e natural))

(define-judgment-form simple-plus
  #:mode (okay1 I I)
  [
   --------
   (okay1 M (e ...))])

(define-judgment-form simple-plus
  #:mode (okay I)
  [(okay1 M ())
   --------
   (okay M)])

(redex-check simple-plus
 #:satisfying (okay e)
 (term e))

simply fails to generate terms. Note that if the okay in the redex-check is replaced with okay1 or if e is changes to have an ellipsis (ie changing e to (e ::= natural (+ e ...))) one gets the error (#:satisfying keyword does not support ellipses, contexts, side-conditions, or unquote)

Bad Macro Error Messages

The following all give generic $macro: bad syntax in $expression errors:

(define-language)
(redex-match)
(redex-match lang)
(define-judgment-form)
(reduction-relation)

Here's one that's even worse

> (define-metafunction)
?: bad syntax in: ()

What can we do to improve this? Are there racket guidelines for good macro error messages?

Improve treatment of ellipsis in `define-judgment-form`

Original text by @rfindler.

In general, this aspect of the handling of ellipses is implemented by the racket/datum library (the same library that syntax-case uses). It can cope with writing things like this:

((a b) ...)

where a is bound in some pattern like this (a ...) but b is just b with no ellipsis around it. It handles this by duplicating b, once for each a. That's what we'd like to happen here too. But the ellipses that are "between" premises in a define-judgment-form are not handled by just giving them to the racket/datum library. Instead, Redex is doing some of its own work before it can hand them off. And that work is what is raising the syntax error in this case.

So: best case, we figure out a more relaxed well-formedness check to implement in define-judgment-form and this example just starts working. Worse case, we need to change how the "inter premise" ellipses handling is implemented. I'm not sure which case we are in.

Test case

#lang racket
(require redex/reduction-semantics)

(define-language L
  (τ ::= n b)
  (e ::= (amb τ e ...) natural #t #f))

(define-judgment-form L
  #:mode (type I O)
  [----------------
   (type natural n)]

  [-----------
   (type #t b)]

  [-----------
   (type #f b)]

  [(type e τ) ...
   ----------------------
   (type (amb τ e ...) τ)])

(test-judgment-holds (type (amb b #f #t) b))
(test-judgment-holds (type (amb n 0 1) n))
(test-equal (judgment-holds (type (amb n 0 #f) any)) #f)
(test-equal (judgment-holds (type (amb n #t #t 11 #f) any)) #f)

Error

unsaved editor:21:14: define-judgment-form: found the same binder, τ, at different depths, 1 and 0 at: τ

References

Initial discussion.

`redex-check` sometimes generates variables bound by a metafunction

#lang racket
(require redex rackunit)
(define-language vars
  (x variable-not-otherwise-mentioned))

(define-metafunction vars
  [(U x) x])

;; eventually generates (term U), which is not a valid term
(redex-check vars x (not (equal? (term x) 'U)))
;(term U) ; errors with ``metafunction must be in an application in: U''

This happens both with this variant of redex-check and with the #:satisfies variant.

Accept symbols for metafunction-cases/judgment-form-cases?

Would it be possible to accept symbols for these rendering parameters to match the contract for language and reduction relation parameters?

Terms with #:...bind are alpha-equivalent?, but don't redex-match?

#lang racket/base
(require redex/reduction-semantics)

(define-language lc
  (x ::= variable-not-otherwise-mentioned)
  (e ::= x (λ x ... e) (e e ...))
  #:binding-forms
  (λ x #:...bind (clauses x (shadow clauses x)) any_body #:refers-to clauses))

(define-judgment-form lc
  #:mode (translate I O)
  #:contract (translate e e)

  [(translate x x)]

  [(translate e_f1 e_f2)
   (translate e_a1 e_a2) ...
   ----------------------------------------
   (translate (e_f1 e_a1 ...) (e_f2 e_a2 ...))]

  [(translate e_1 e_2)
   --------------------------------------------
   (translate (λ x ... e_1) (λ x ... e_2))])

(module+ test
  (require rackunit racket/function)
  ;; single binder; passes
  (check-true
   (redex-match? lc (λ x x) (term (λ x x))))
  (check-true
   (judgment-holds (translate (λ x x) (λ x x))))
  ;; many binders; fails
  (check
   (curry alpha-equivalent? lc)
   (term (λ x y z x))
   (car (judgment-holds (translate (λ x y z x) e) e)))
  (check-true
   (redex-match? lc (λ x y z x) (term (λ x y z x))))
  (check-true
   (judgment-holds (translate (λ x y z x) (λ x y z x)))))

non-deterministic metafunction

I'd like to write a metafunction that non-deterministically generates a term out of thin air. For a while I thought I could make this work with the following:

(define-language l
  (v integer)
  (t int))

(define-metafunction l
  gen : t -> v
  [(gen int) ,(generate-term l integer 5)])

But I just realized that the unquote is of course being evaluated at compile-time, so (gen int) will always return the same integer. It's been a while since I've written scheme.. :)

Is there a way to make use of redex's term generators as part of a metafunction?

The redex-check form does not correctly respect _!_

The redex-check form does not correctly respect _!_ for variables in sufficiently large examples. A gist containing code that produces this error may be found here: https://gist.github.com/cgswords/8f6ddb6174dc7db64603 (Warning: that is a full redex mode, not a boiled-down counter-example.)

Upon further investigation, the following was discovered:

< ianjneu> cswords: redex-lib/redex/private/enum.rkt:176 _!_ is unimplemented. It just doesn't warn you.
< ianjneu> it should raise an error. "unimplemented" raises an error. It doesn't.

For a temporary solution, we can define:

(define-judgment-form ccon #:mode (Good-e I) [--- (Good-e e)])

The generator can then use

#:satisfying (Good-e e)

Unfortunately, this disable retries.

too few args to judgment causes internal error

The 'assemble' function in redex/private/judgment-form.rkt will throw an internal error

car: contract violation
  expected: pair?
  got: '()

if a 'judgment-holds' clause in a metafunction passes too few arguments to the judgment:

#lang racket/base

(require redex/reduction-semantics)

(define-language L
  [x ::= variable-not-otherwise-mentioned]
  [e :: x (λ x e) (e e)])

(define-judgment-form L
  #:mode (lambda? I)
  #:contract (lambda? e)
  [----------------
   (lambda? (λ x e))])

(define-metafunction L
  not-lambda? : e -> boolean
  [(not-lambda? e)
   #f
   (judgment-holds (lambda?))] ;; <---- causes error
  [(not-lambda? e) #t])

http://imgur.com/MTwbZAS

redex-doc undelcared dependency on scribble or scribble-docs

I just updated redex-lib and installed redex-doc on a minimal install, but got some errors during installation of redex-doc about scribble/examples not existing. After installing scribble and scribble docs, these errors disappeared.

A quick look suggests this might have been introduced by 15fb87f and be the result of an undeclared dependency.

reduction-relation with shortcut not the same as without

Racket 6.2

While creating a silly relation to test reduction-relation syntax, I found a case where using a shortcut results in different behavior; it seems using any within the first pattern of in-hole is at least partially to blame.

#lang racket

(require redex)

(define-language L
  (e ::= n (e e))
  (n ::= natural)
  (C ::= hole (C n) (n C)))

(define in-term (term (42 (1 2))))
(define out-term (term (2 1)))

(module+ test
  (test-equal (apply-reduction-relation swapC in-term) (list out-term))
  (test-equal (apply-reduction-relation swapC-with-shortcut in-term) (list out-term))
  (test-equal (apply-reduction-relation swapC-with-shortcut-and-any in-term) (list out-term)))

(define swapC (reduction-relation
           L
           (--> (in-hole (any C) (n_1 n_2)) (in-hole C (n_2 n_1)))))

;; doesn't match using "(in-hole (any C) a)"
(define swapC-with-shortcut-and-any (reduction-relation
           L
           [==> (n_1 n_2) (n_2 n_1)]
           with
           [(--> (in-hole (any C) a) (in-hole C b))
            (==> a b)]))

;; does match using "(in-hole (n C) a)"
(define swapC-with-shortcut (reduction-relation
           L
           [==> (n_1 n_2) (n_2 n_1)]
           with
           [(--> (in-hole (n C) a) (in-hole C b))
            (==> a b)]))

(module+ test
  (test-results))

metafunction pre-conditions require using non-terminal-with-underscore names in contracts

Normally, non-terminal names without an underscore bind as names in patterns. However, when using a pre-condition on a metafunction, if the contract on the metafunction uses non-terminal-only names instead of non-terminal-with-underscore names, the precondition fails in an unexpected way.

Here is a small example: https://gist.github.com/wilbowma/4bc0ed97a60fa03dc07e

It is unclear if this is a bug or not. If not, that is unexpected given the way non-terminal names behave elsewhere and it should be documented or changed to match the normal behavior (IMHO).

`define-term`ed terms are not bound in judgment forms if there is an non-terminal of the same name

#lang racket
(require redex)
(define-language nats
  (nat Z (S Z))
  (one (S Z));; comment this out and the error goes away
  (two (S (S Z))))

(define-term one (S Z))
(define-term two (S (S Z)))

(term one);; produces '(S Z)

(define-metafunction nats
  [(test1 nat) (S one)])

(term (test1 one));; produces '(S (S Z))

(define-judgment-form nats
  #:mode (test I O)
  [---------
   (test nat one)]);; errors with `` unbound pattern variable in: one''

Metafunctions in O position of Judgment Not Working

Small repro:

#lang racket/base

(require redex)

(define-language Simple
  (e unit)
  (t top))

(define-judgment-form Simple
  #:mode (types I O)
  [------------
   (types unit top)])
(define-metafunction Simple
  [(unit2) unit])

(define-metafunction Simple
  [(top2) top])

Everything works fine if there's no metafunction or if a metafunction is used in an I position:

> (judgment-holds (types unit top))
#t
> (judgment-holds (types (unit2) top))
#t

But it fails if you use the metafunction in the O position:

> (judgment-holds (types unit (top2)))
#f

Even though

> (equal? (term (top2)) (car (judgment-holds (types unit t) t)))
#t

`test-judgment-holds` signals arity errors in terms of internal syntax locations

#lang racket
(require redex rackunit)
(define-language nats
  (nat Z (S Z)))

(define-judgment-form nats
  #:mode (test I O)
  [---------
   (test nat one)])

#;
(judgment-holds
 (test Z));; signals error here

(test-judgment-holds
 (test Z)) ;; signals an error at `redex/redex-lib/redex/private/reduction-semantics.rkt:2706:55`

Confusing behavior: literals interpreted as variables for binding purposes

I don't quite understand what's going on here but a the cyclic binding form in this language seems to break pattern matching.

#lang racket
(require redex/reduction-semantics)

(define-language esterel
  ;; If there was only p (ie this rule and pdot were deleted) the test would pass
  (pdotdot ::= pdot p)

  (p ::= nothing)

  (pdot ::= (· p))

  (M (machine pdotdot bindings))
  (bindings (s ...))

  #:binding-forms
  ;; without the following rule the test passes
  (machine pdotdot #:refers-to bindings
           bindings #:refers-to pdotdot))

;; these tests pass
(test-equal (redex-match? esterel M (term (machine nothing ())))
            #t)
(test-equal (redex-match? esterel (machine nothing ()) (term (machine nothing ())))
            #t)

;; this test fails, would expect it to pass
(test-equal (redex-match? esterel (machine pdotdot bindings) (term (machine nothing ())))
            #t)

test--> and test-->> don't set default-language

It doesn't look like default-language is set for the various reduction relation test forms, making the equality check not consider binding. The test-cases pass if you uncomment the language setter.

#lang racket
(require redex)
(define-language drop
  (x variable-not-otherwise-mentioned)
  #:binding-forms
  (x number #:refers-to x ...))
(define ->drop
  (reduction-relation
   drop
   (--> (x number_hd number_tl ...)
        (x))))
;(default-language drop)
(test--> ->drop (term (x 4 5 6)) (term (x)))
(test-->> ->drop (term (x 2 3 4)) (term (x)))

Expected a Parenthesized Binding Form Error

#lang racket
(require redex)

(define-language Core
  (G ::= (graph (v (v ...)) ...))
  (v ::= variable-not-otherwise-mentioned)
  #:binding-forms
  (graph (v_vertex (v ...)) ...) #:refers-to (shadow v_vertex ...))

This gives the following error:

/redex/redex-lib/redex/private/binding-forms-compiler.rkt:32:23: define-language: expected a parenthesized binding form. in: (#:refers-to (shadow v_vertex ...))

If I change the language slightly to

(define-language Core
  (G ::= (graph ((v (v ...)) ...)))
  (v ::= variable-not-otherwise-mentioned)
  #:binding-forms
  (graph ((v_vertex (v ...)) ...) #:refers-to (shadow v_vertex ...)))

Then the error goes away.

I'm not sure if this behavior is intended, but the error message seems incorrect since the form I'm trying to specify as a binding form is parenthesized

alpha-equivalent? requires language name

The prose in the docs imply that Redex's alpha-equivalent? should get the language from default-language, but in reality it requires a separate lang parameter. Either the docs or the code should be fixed (preferably the code - using default-language would match substitute).

Keywords in grammar confuse substitution

Example:

#lang racket/base

(require redex)

(define-language lang
  [e (Λ (x #:kw x) e)
     x
     number]
  [x variable-not-otherwise-mentioned]
  #:binding-forms
  (Λ (x_1 #:kw x_2) e #:refers-to x_1))

(parameterize ([default-language lang])
  (term (substitute (Λ (x_1 #:kw x_2) 0) x_1 1)))

The error message that results:

symbol=?: contract violation
  expected: symbol?
  given: '#:kw
  argument position: 2nd
  other arguments...:
   'x_1
  context...:
   /home/asumu/plt/racket-git/racket/collects/racket/bool.rkt:19:0: symbol=?
   /home/asumu/plt/racket-git/extra-pkgs/redex/redex-lib/redex/private/binding-forms.rkt:659:10: loop
   /home/asumu/plt/racket-git/extra-pkgs/redex/redex-lib/redex/private/binding-forms.rkt:620:4: loop
   /home/asumu/plt/racket-git/extra-pkgs/redex/redex-lib/redex/private/binding-forms.rkt:620:4: loop
   /home/asumu/plt/racket-git/extra-pkgs/redex/redex-lib/redex/private/binding-forms.rkt:620:4: loop
   /home/asumu/plt/racket-git/extra-pkgs/redex/redex-lib/redex/private/binding-forms.rkt:620:4: loop
   /home/asumu/plt/racket-git/extra-pkgs/redex/redex-lib/redex/private/binding-forms.rkt:620:4: loop
   /home/asumu/plt/racket-git/extra-pkgs/redex/redex-lib/redex/private/binding-forms.rkt:616:0: rec-freshen-spec
   /home/asumu/plt/racket-git/extra-pkgs/redex/redex-lib/redex/private/binding-forms.rkt:146:0: safe-subst
   /home/asumu/plt/racket-git/extra-pkgs/redex/redex-lib/redex/private/reduction-semantics.rkt:1424:42
   /home/asumu/plt/racket-git/racket/collects/racket/private/map.rkt:21:13: map
   /home/asumu/plt/racket-git/extra-pkgs/redex/redex-lib/redex/private/reduction-semantics.rkt:1724:24: loop
   /home/asumu/docs/dissertation/model/ex.rkt: [running body]

I'm not entirely sure if keyword literals in Redex patterns are actually considered valid, but they are accepted by define-language. So I'm not sure if this is a bug in substitution due to not handling keywords or a bug in define-language due to not ruling keywords out.

Binding forms parsing error

This language definition:

(define-language lc
    (e ::= (list e ...) x)
    (x ::= variable-not-otherwise-mentioned)
    #:binding-forms
    (list (list x ...) ...) #:exports nothing)

Produces the error:
redex/redex-lib/redex/private/binding-forms-compiler.rkt:36:39: define-language: Same name used at two different ... depths: list (depth 1) vs. list (depth 0) in: (list (list p ...) ...)

compile-pattern: unknown cross reference id-id

When I try to use cross in a language definition, or use cross with a non-terminal alias, I get this error.
I'm running redex-lib built from ce1360b.

Here is a test file: https://gist.github.com/wilbowma/4e8dae31a08b7c8eb693d38affa6ee4c

One weird non-terminal that will crash your computer

I accidently wrote a language with the following nf non-terminal, and tried to use it. I spent a week trying to figure out why running my tests caused Racket to eat all of my computer's memory in a few seconds.

Is there anything to be done to detect/warn the user of this sort of problem?

WARNING: Do not run this code outside of some kind of sandbox.

#lang racket/base
(require redex/reduction-semantics)

(check-redundancy #t)

(define-language lc-crash
  (e ::= () (λ (x) e) (e e))
  (E ::= hole (E e) (v E))
  (nf ::= x (in-hole E nf))
  ; oops should have been
  #;(nf ::= (in-hole E x)))

(module+ test
  (require rackunit)
  (check-true
   (redex-match? lc-crash nf (term x))))

internal # of values error leaking

A judgement in a term w/ the wrong number of arguments exposes an unsafe call-with-values bug (~line 880 in judgment-form.rkt):

This reproduces the error:

#lang racket/base

(require redex/reduction-semantics)

(define-language lc
  [x ::= variable-not-otherwise-mentioned]
  [e ::=
     x
     (e e)
     (λ x e)])

(define-judgment-form lc
  #:mode (foo I I)
  #:contract (foo any any)
  [------------------
   (foo any any)])

(term (foo (λ x x)))

Bad indentation of judgment forms in DrRacket

Expected behavior

DrRacket's indentation of judgment forms matches the documentation.

Current behavior

The documentation for judgment forms contains the following example:

#lang racket
(require redex)

(define-language nats
  (n ::= z (s n)))

(define-judgment-form nats
  #:mode (sum I I O)
  #:contract (sum n n n)
  [----------- "zero"
   (sum z n n)]

  [(sum n_1 n_2 n_3)
   ------------------------- "add1"
   (sum (s n_1) n_2 (s n_3))])

DrRacket indents this as (hit Cmd+i to reproduce):

#lang racket
(require redex)

(define-language nats
  (n ::= z (s n)))

(define-judgment-form nats
  #:mode (sum I I O)
  #:contract (sum n n n)
  [----------- "zero"
               (sum z n n)]

  [(sum n_1 n_2 n_3)
   ------------------------- "add1"
   (sum (s n_1) n_2 (s n_3))])

Notice how (sum z n n) is misaligned in relation to the -------- bar above it.

Do you agree this is an issue?
Is there a configuration/workaround that I'm unaware of?
If you agree this is an issue, how can I help fixing it? I'd love to collaborate, but would need a hint on where to start.

Thank you for Redex and DrRacket. They are amazing tools.

`test-judgment-holds` always fails on judgment forms with outputs

A test case for tl-test.rkt:

(let ()
  (define-judgment-form empty-language
    #:mode (J I O)

    [-----------
     (J natural 1)]

    [(J any_1 any_3)
     --------------
     (J (any_1 any_2) any_3)])

  (test
   (capture-output
    (test-judgment-holds (J (0 x) any)))
   "");fails


  (test
   (capture-output
    (test-judgment-holds (J (x 0) any)))
   #rx"judgment of J does not hold")

  (test (capture-output (test-results))
        "1 test failed (out of 2 total).\n")); fails with "2 tests failed (out of 2 total).\n"

where clauses mess up metafunction error reporting

Racket Snapshot: 20150728-75e19c9

Having a 'where clause' on a metafunction seems to cause it to be highlighted as the erroneous clause when in fact a later clause is at fault.

Consider the following small redex model:

#lang racket
(require redex)

(define-language Piano
  (n ::= O (S n)))

(define-metafunction Piano
  sub1 : n -> n
  [(sub1 (S n)) n]
  [(sub1 O) ]) ;; <-- error highlighting here, correct! =D

This error correctly reports ' [(sub1 O) ]' is bad since it has no rhs.

However, if we had a where clause to the previous clause:

#lang racket
(require redex)

(define-language Piano
  (n ::= O (S n)))

(define-metafunction Piano
  sub1 : n -> n
  [(sub1 (S n)) n (where #t #t)]  ;; <-- error highlighting here, wrong =(
  [(sub1 O) ])

Now the incorrect clause is highlighted and reported as erroneous in the error message:

Feature request: tool tips for languages and non-terminals

It would be nice if, when one moused over a language name or a non-terminal in a pattern, a tool tip popped up showing what was in that language/NT.

(nanopass does this and I've found it useful)

Doc links to examples broken

On this page: http://plt.eecs.northwestern.edu/snapshots/current/doc/redex/The_Redex_Reference.html?q=define-judgment#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._define-judgment-form%29%29

This link is broken (and a few others): http://git.racket-lang.org/plt/blob/HEAD:/collects/redex/examples/define-judgment-form/typing-rules.rkt

`redex-check` ellipsis error gives internal source location

#lang racket
(require redex/reduction-semantics)

(define-language simple-plus
  (M (e e))
  (e natural))

(define-judgment-form simple-plus
  #:mode (okay1 I I)
  [
   --------
   (okay1 M (e ...))])

(redex-check simple-plus
 #:satisfying (okay1 e)
 (term e))

Gives the error:

redex/redex-lib/redex/private/judgment-form.rkt:1698:9: redex-check: generation failed at unsupported pattern;
 (#:satisfying keyword does not support ellipses, contexts, side-conditions, or unquote)
  pattern: (repeat (name e (nt e)) #f #f)

Instead of reporting a source location in the given file

`test-judgment-holds` reverses order of `O` in error output

#lang racket
(require redex/reduction-semantics)
(define-language empty-language)
(define-judgment-form empty-language
  #:mode (broken-swap I I O O)
  [-------
   (broken-swap any_1 any_2 any_1 any_2)])
(test-judgment-holds
 (broken-swap first second second first))

Errors with

FAILED :8.0
  judgment of broken-swap does not match expected output patterns, got:
  second first

But the correct error is

FAILED :8.0
  judgment of broken-swap does not match expected output patterns, got:
  first second

Reusing meta-functions and judgment-forms after extending languages

Reusing metafunctions and judgment forms is hard or impossible after extending languages.

Metafunctions can't reliably be reused in an extended language. Trying to use a metafunction defined for the original language can result in contract errors if the metafunction has a contract and the extended language extends the definition of a nonterminal used in that contract.

This can be solved by using define-metafunction/extension to give a new contract, but no new clauses. It seems like this could be automated, maybe by making metafunction definitions depend on the current language...

#lang racket

(require
redex/reduction-semantics)
(module+ test
(require rackunit))

(provide (all-defined-out))

(define-language S
(t   ::= Nat (-> t t))
(e   ::= x (λ (x : t) e) (e e) natural)
(x   ::= variable-not-otherwise-mentioned)
(Γ   ::= ∅ (Γ x : t))
#:binding-forms
(λ (x : t) e #:refers-to x))

(define-metafunction S
Γ-ref : Γ x -> t or #f
[(Γ-ref ∅ x) #f]
[(Γ-ref (Γ x : t) x) t]
[(Γ-ref (Γ x_0 : t_0) x) (Γ-ref Γ x)])

(define-extended-language T S
(t   ::= .... Bool)
(e   ::= .... true false))

(define-metafunction/extension Γ-ref T
t.Γ-ref : Γ x -> t or #f)

(module+ test
(check-true
  (redex-match? T t (term Bool)))
;; I wish this wouldn't fail, but alas...
(check-exn exn:fail?
  (thunk (term (Γ-ref (∅ x : Bool) x))))
(check-equal?
  (term (t.Γ-ref (∅ x : Bool) x))
  (term Bool)))

judgment-forms should pretty much never be extended. Instead, use copy/paste as an abstraction. This is very annoying, but I'm not sure how to addressed.

If extending a judgment-form resulted in the same behavior as define-metafunction/extension--i.e., the clauses seem to be copied into the extended definition but use the new language's meta-variables--the first examples would work.

If metafunction and judgment-form definitions depended on the current language, all of these might work.

....

(define-judgment-form S
#:mode (s.wf I)
#:contract (s.wf t)

[----------
(s.wf nat)]

[(s.wf t_0)
(s.wf t_1)
--------------------
(s.wf (-> t_0 t_1))])

(define-judgment-form S
#:mode (s.valid I)
#:contract (s.valid Γ)

[(s.wf t)
(s.valid Γ)
-------------------
(s.valid (Γ x : t))])

(define-judgment-form S
#:mode (s.type-check I I O)

[(s.valid Γ)
-------------------------- "ℕ"
(s.type-check Γ natural Nat)]

[(where t (Γ-ref Γ x))
-------------------- "var"
(s.type-check Γ x t)]

[(s.type-check (Γ x : t_p) e t)
---------------------------- "λ"
(s.type-check Γ (λ (x : t_p) e) (-> t_p t))]

[(s.type-check Γ e_0 (-> t_1 t))
(s.type-check Γ e_1 t_1)
--------------------------- "app"
(s.type-check Γ (e_0 e_1) t)])

(define-extended-judgment-form T s.wf
#:mode (wf I)
#:contract (wf t)

[----------
(wf bool)])

(define-extended-judgment-form T s.type-check
#:mode (type-check I I O)
#:contract (type-check Γ e t)

[(s.valid Γ)
---------------------------
(type-check Γ true Bool)])

(module+ test
;; Fails because we extend wf, which uses the origianl definition of s.wf to check (-> bool bool),
;; which is defined for S, in which Bool is not a t.
(check-exn exn:fail?
  (thunk (judgment-holds (wf (-> bool bool)))))

;; Fails because we extended type-check, which used Γ-ref, which is defined for S, in which Bool is
;; not a t
(check-exn exn:fail?
  (thunk (judgment-holds (type-check (∅ x : Bool) x Bool))))

;; Fails because we extended type-check, which uses s.valid, which is defined for S, in which Bool
;; is not a t
(check-exn exn:fail?
  (thunk (judgment-holds (type-check (∅ x : Bool) true Bool)))))

racket / redex Goto Github PK

redex's Introduction

redex

Contributing

License

redex's People

Contributors

Stargazers

Watchers

Forkers

redex's Issues

Minimal working example

Expected behavior

Current behavior

Caveat

Test case

Error

References

Expected behavior

Current behavior

Recommend Projects

Recommend Topics

Recommend Org