Yes, I had to make some adjustments to the judgement you sent me but this 
helped me a lot!
This was what I ended up using:

(define-judgment-form L
  #:mode (subsequence I I)
  #:contract (subsequence (ts ...) (ts ...))

  [----------------------------------------------
   (subsequence (ts_1 )
                (ts_2 ... ts_1  ts_3 ...))]
  
  [(subsequence (ts_1 ...)
                (ts_2 ... ts_3 ...))
   ----------------------------------------------
   (subsequence (ts_0 ts_1 ...)
                (ts_2 ... ts_0 ts_3 ...))])

Thank you so much! :D

A sábado, 30 de janeiro de 2021 à(s) 20:08:17 UTC, Robby Findler escreveu:

> Is this what you have in mind? 
>
> #lang racket
> (require redex/reduction-semantics)
>
> (define-language L
>   (ts ::= variable number))
>
> (define-judgment-form L
>   #:mode (subsequence I I)
>   #:contract (subsequence (ts ...) (ts ...))
>
>   [----------------------------------------------
>    (subsequence (ts_1 ...)
>                 (ts_2 ... ts_1 ... ts_3 ...))])
>
> (test-judgment-holds
>  (subsequence () (1 2 3 4)))
>
> (test-judgment-holds
>  (subsequence (1) (1 2 3 4)))
>
> (test-judgment-holds
>  (subsequence (2) (1 2 3 4)))
>
> (test-judgment-holds
>  (subsequence (1 2) (1 2 3 4)))
>
> (test-judgment-holds
>  (subsequence (2 3) (1 2 3 4)))
>
> (test-judgment-holds
>  (subsequence (3 4) (1 2 3 4)))
>
> (test-judgment-holds
>  (subsequence (2 3 4) (1 2 3 4)))
>
> (test-judgment-holds
>  (subsequence (1 2 3) (1 2 3 4)))
>
> (test-judgment-holds
>  (subsequence (1 2 3 4) (1 2 3 4)))
>
> (test-equal
>  (judgment-holds (subsequence (5) (1 2 3 4))) #f)
>
> (test-equal
>  (judgment-holds (subsequence (3 2) (1 2 3 4))) #f)
>
> (test-equal
>  (judgment-holds (subsequence (4 1) (1 2 3 4))) #f)
>
> (test-results)
>
>
>
> On Sat, Jan 30, 2021 at 11:46 AM Beatriz Moreira <beatriz....@gmail.com> 
> wrote:
>
>> Hi !
>> I have a reduction relation where I have to match a pattern *ts* to two 
>> sequences, where the first one contains the other one. What I tried to do 
>> was something like this: 
>> 1st seq:  (*ts_all1 ... ts ts_all2 ...*)     2nd seq:   (*ts_x1 ... ts 
>> ts_x2 ...*),  where *ts_x* *⊆ **ts_all*.
>> But the problem is that with the pattern matching is that *ts_x1* 
>> doesn't match all elements of *ts_all1* .
>> I'm trying to use side conditions but i can't seem to get it right :c .
>> Any advice?
>>
>> Thank you , Beatriz :) 
>>
>> -- 
>> 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/1f9a3f57-787b-43b9-9fb4-560e425c1cdan%40googlegroups.com
>>  
>> <https://groups.google.com/d/msgid/racket-users/1f9a3f57-787b-43b9-9fb4-560e425c1cdan%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/0c6555d8-9c60-4371-9369-30bd93e3027fn%40googlegroups.com.

Reply via email to