racket / redex Goto Github PK
View Code? Open in Web Editor NEWLicense: Other
License: Other
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))))
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))
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?
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)
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))
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)))
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))
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])
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.
#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.
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.
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
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?
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.
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
).
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)))
EDIT: I figured my mistake. See post below.
#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)
The typeset version of the grammar should include the double pipes in ||
and |||
.
The typeset version of the grammar omits double pipes.
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!
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:
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
#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''
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"
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))
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.
#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
#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
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)))))
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
#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)))))
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.
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
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.
#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)
unsaved editor:21:14: define-judgment-form: found the same binder, τ, at different depths, 1 and 0 at: τ
#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
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 ...) ...)
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.
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 "".
Would it be possible to accept symbols for these rendering parameters to match the contract for language and reduction relation parameters?
#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`
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]
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))
#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
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
#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
DrRacket's indentation of judgment forms matches the documentation.
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.
Thank you for Redex and DrRacket. They are amazing tools.
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).
It should be check-redundancy
#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)
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.
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.
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)
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.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.