My definition allows it to go backwards because for what im trying to do the order does not matter. So I evaluate the head of the sequence, and then recursively the tail. I tested your example you gave me just now and it passed :D Beatriz
A quarta-feira, 3 de fevereiro de 2021 à(s) 18:41:53 UTC, Robby Findler escreveu: > 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/a2db87c0-ccfa-4a2f-86ed-ce9aac0fe37en%40googlegroups.com.
