Oh, I see -- you want (1 2 3) to be a subsequence of (1 4 2 4 3 4), for example.
But does your definition allow you to go "backwards"? Maybe you need a helper judgment that captures "a subsequence that starts here" and then subsequence can try that one at each position? Robby On Wed, Feb 3, 2021 at 10:33 AM Beatriz Moreira <[email protected]> wrote: > 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 <[email protected]> >> 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 [email protected]. >>> 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 [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/racket-users/0c6555d8-9c60-4371-9369-30bd93e3027fn%40googlegroups.com > <https://groups.google.com/d/msgid/racket-users/0c6555d8-9c60-4371-9369-30bd93e3027fn%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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/CAL3TdOOB-KE3OnF3rHUnYHyGnavSpYR_4QjBhgSFbmDyRGQ4mg%40mail.gmail.com.
