Judgement not holding

[Beatriz Moreira]

Hello,

I'm trying to write a side condition to a function, where it checks if a is in an environment ß. I tried this judgement by adding (judgment-holds (anotin (ß-v ...) a #f)) at the end of the function but it is not working :(

Thank you!

--Beatriz

(define-judgment-form Flint

  #:mode (anotin I I O)

  #:contract (anotin env-ß a boolean)

  [-------------------------

   (anotin () a #f)]

  [-------------------------

   (anotin ((a -> b ...)) a #t)]

  [-------------------------

   (anotin ((a_0 -> b ...)) a #f)]

  [-------------------------

   (anotin (ß-v_0 ... (a -> b ...)) a #t)]

  [(anotin (ß-v ...) a boolean)

   -------------------------

   (anotin (ß-v ... (a_0 -> b ...) ) a boolean)]

  )

[philngu...@gmail.com]

It’s difficult without seeing the definitions, but here are a few general comments:

1. Cases in judgment forms are not run in order. If multiple cases match, they’ll all hold. For example, in this case, if (anotin ((a -> b ...)) a #t) holds, (anotin ((a_0 -> b ...)) a #f) will also hold.

2. If your environment looks something like ((a_1 -> b_1) (a_2 -> b_2) (a_3 -> b_3)), the pattern for the second case should be (_ ... (a -> b) _ ...). The ellipses after b as it currently is means a sequence of zero or more b’s.

3. The relation is being named “not in”, but it seems like it’s computing both “in” and “not in” cases, which is confusing.

4. Checking for membership in an environment sounds like a (very) decidable problem. It maybe simpler to just write a judgment form for the positive case, and simply defining the negative case as “when the judgment doesn’t hold”.

[Beatriz Moreira]

Thank you, I did just that! :D

4. Checking for membership in an environment sounds like a (very) decidable problem. It maybe simpler to just write a judgment form for the positive case, and simply defining the negative case as “when the judgment doesn’t hold”.