[relation-rules] found the same binder

[Beatriz Moreira]

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")

[Robby Findler]

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)

--
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...@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.

[Beatriz Moreira]

Thank you, the problem was that I was defining f_0 as multiple patterns of (c_0 -> f_0)... and only comparing it to one instance of f_0.