side-conditions

[Beatriz Moreira]

Hi,

I have been using side-condition to check if a sequence of variables exist is in an environment , like this : 

(side-condition (not (member (term ((s : _) ...)) (term (env-ß_1 ...)))))

being s a state variable and _ a value that i don't know. But it doesn't seem to work as expected, as it returns #t even when it shouldn't. 

Is it there a better way of doing it?

Thank you :) 

[Robby Findler]

I recommend you define a metafunction or judgment form that captures what you want exactly and then use that.

Robby

--
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/c8632f31-98c2-46cb-8231-2ca272ae2b8an%40googlegroups.com.

[Beatriz Moreira]

I have tried to use a metafunction to represent s∉dom(env-ß) in a side condition, (side-condition (notinenv ((ß_1 ...) env-ß ...) x)),  but the error message notinenv: illegal use of syntax in: (notinenv ((ß_1 ...) env-ß ...) x) value at phase 1: #<term-fn> appears and i don't understand why. 

I defined notinenv as a simple metafunction just for testing: 

(define-metafunction FS

  notinenv : env-ß x -> any

  [(notinenv (((x -> _) ß_1 ...) env-ß ...) x) #f]

  [(notinenv ((ß_1 ...) env-ß ...) x) #t])

Thank you :)

[Robby Findler]

I'm not sure without seeing more of your code (one annoying thing about Redex is that it is not always clear when you "in redex" and when you are "in racket" and your code might be mixing those up) but here is an example along the lines I think you're working towards. Note that it might be better to define in-dom as a judgment form (this would require you to define a metafunction that checks if two names are different) but I did it as a metafunction to show how that would work.

Robby

#lang racket
(require redex/reduction-semantics)

(define-language L
  (e ::= (+ e e) x)
  (x y ::= variable-not-otherwise-mentioned)
  (Γ ::= · (x Γ)))

(define-judgment-form L
  #:mode (closed-by I I)
  #:contract (closed-by Γ e)

  [(closed-by Γ e_1) (closed-by Γ e_2)
   -----------------------------------
   (closed-by Γ (+ e_1 e_2))]

  [(side-condition (in-dom x Γ))
   -----------------------------
   (closed-by Γ x)])

(define-metafunction L
  in-dom : x Γ -> boolean
  [(in-dom x ·) #false]
  [(in-dom x (x Γ)) #true]
  [(in-dom x (y Γ)) (in-dom x Γ)])

(test-judgment-holds (closed-by (c ·) c))
(test-judgment-holds (closed-by (b (c ·)) b))
(test-judgment-holds (closed-by (b (c ·)) c))
(test-judgment-holds (closed-by (a (b (c ·))) (+ a (+ b c))))
(test-equal (judgment-holds (closed-by · a)) #false)
(test-equal (judgment-holds (closed-by · (+ a (+ b c)))) #false)

(test-results)

To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/30754357-0563-4709-8d88-f0f8ef5d8b63n%40googlegroups.com.