I'm not sure exactly what you're trying to accomplish so take this with a
grain of salt, but that error message means that redex doesn't really know
how to interpret your rules. Here's a simpler example that has the same
error message.
(reduction-relation
L
(--> (+ (+ n ...) n)
5))
In this case you might be intending to say that all of the "n"s inside the
inner plus should be the same and should also be the same as the one in
outer plus.
Redex's pattern matcher isn't smart enough to do that for you, so you'd
need to write something explicitly that makes sure you get what you want,
running example below.
Maybe in your actual code you can use a similar idea. I would also say that
your patterns look huge so it is probably in your interest to introduce
something to break things down into simpler pieces somehow and
judgment-forms are one tool to help with that.
hth,
Robby
#lang racket
(require redex)
(define-language L
(e ::= (+ e ...) n)
(n ::= natural))
(define red
(reduction-relation
L
(--> (+ (+ n_2 ...) n_1)
5
(judgment-holds (matching n_1 (n_2 ...)))
)))
(define-judgment-form L
#:mode (matching I I)
#:contract (matching n (n ...))
[---------------
(matching n ())]
[(matching n_1 (n_2 ...))
----------------------------
(matching n_1 (n_1 n_2 ...))])
(test--> red
(term (+ (+ 1 1 1 1) 1))
5)
On Tue, Sep 22, 2020 at 12:18 PM Beatriz Moreira <beatriz.smore...@gmail.com>
wrote:
> Hello,
> I have a bunch of relation rules, but in one of them i need to check if
> f_0 is the same as i have in one of the environments, but the error
> *reduction-relation:
> found the same binder, f_0, at different depths, 0 and 1 ... F_01 ... (T
> f_0 ((T_00 x_00) ...) (return e)) F_02 ...)) (contract C_2 ((T_2 x_21) ...
> K_2 F_2... *appears and i would like to know if there's an alternative.
>
> The part of the code where the error is is below and the link for the
> repository is this :
> https://bitbucket.org/beatrizmoreira/msc/src/master/fwsollast.rkt
>
> Thank you!
>
>
> (--> [(in-hole E (c -> f -> value (n) ((s : (c_0 -> f_0)) ...))) env-ß
> env-σ ((contract C_1 {(T_1 x_11) ... K_1 F_1 ...}) ... (contract C {(T_0
> x_01) ... K F_01 ... (T f_0 ((T_00 x_00) ... ) {return e}) F_02 ...})
> (contract C_2 {(T_2 x_21) ... K_2 F_2 ...}) ...)]
> [(in-hole E (return (call env-ß CT c
> (top-σ env-σ) f n ((s : (c_0 -> f_0))
> ...)))) (decl (uptbal (uptbal env-ß (ref env-ß c) n) (top-σ env-σ) ,(-
> (term 0)(term n))) ((s -> (c_0 -> f_0)) ...)) (call-σ env-σ (ref env-ß c))
> ((contract C_1 {(T_1 x_11) ... K_1 F_1 ...}) ... (contract C {(T_0 x_01)
> ... K F_01 ... (T f_0 ((T_00 x_00) ... ) {return e}) F_02 ...}) (contract
> C_2 {(T_2 x_21) ... K_2 F_2 ...}) ...)]
> (side-condition)
> "CALL2")
>
> --
> You received this message because you are subscribed to the Google Groups
> "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to racket-users+unsubscr...@googlegroups.com.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/racket-users/6ab63e3a-72f8-4ae9-a43a-64dcb07a9320n%40googlegroups.com
> <https://groups.google.com/d/msgid/racket-users/6ab63e3a-72f8-4ae9-a43a-64dcb07a9320n%40googlegroups.com?utm_medium=email&utm_source=footer>
> .
>
--
You received this message because you are subscribed to the Google Groups
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to racket-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/racket-users/CAL3TdONnHzwwZm3NTT5swuF%2B7mD5MNSxXE4ybbGF6RcV-O_1Hg%40mail.gmail.com.
