[racket-users] [Redex] Variable names must be different
Hello, When defining a language, is it possible to define that all instances of a pattern have to be different ? For example, I have f ::= variable-not-otherwise-mentioned, which represents a function name. How do I guarantee all fs are different? 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+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/40a4b1b2-a736-4499-9c21-6aec5eb3ada1n%40googlegroups.com.
[racket-users] Re: Judgement not holding
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”. A sexta-feira, 9 de abril de 2021 à(s) 01:20:32 UTC+1, philngu...@gmail.com escreveu: > 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”. > > On Wednesday, April 7, 2021 at 9:57:15 AM UTC-7 beatriz@gmail.com > wrote: > >> 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)] >> ) >> > -- 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/684893ee-9383-43bf-848a-dd217eb0b405n%40googlegroups.com.
[racket-users] Judgement not holding
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)] ) -- 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/db09a9df-807c-4fb9-8df3-2e3a1486195cn%40googlegroups.com.
Re: [racket-users] Smart contracts in Racket
Hi! Thank you for the Goblins idea, but that's not really what I have in mind. What I did in Racket was a formalisation of two smart contract core languages, to be able to see the execution step-by-step. What I had in mind was something like a git where I could publish my work for case study purposes. Thank you :D A terça-feira, 16 de março de 2021 à(s) 19:24:35 UTC, cwebber escreveu: > James Platt writes: > > > On Mar 15, 2021, at 7:01 PM, Beatriz Moreira wrote: > > > >> Hello! I recently used Racket as a tool to see the small step > >> execution of some smart contract languages and I was wondering if > >> there is anywhere i can submit my work or share it with the Racket > >> community. > > > > One place might be the Racket Artifacts site. I think it's mainly > > intended for short demonstrations of code but, if yours is not too > > long, that might be the place. > > > > https://github.com/racket/racket/wiki/Artifacts > > > > I am interested in smart contracts, as well, for a possible future > > addition to a project I am working on but it will be a while before I > > get to that point. > > Spritely Goblins is probably what you want to look at, or will after the > next release (v0.8) comes out: > > https://docs.racket-lang.org/goblins/index.html > > In the not too distant future, Spritely and Agoric's CapTP should > converge. Agoric's current work is all based around smart contracts: > > https://agoric.com/ > https://github.com/Agoric/agoric-sdk/issues/1827 > > There's a lot of confusion out there about what "smart contracts" mean; > most of the examples tend to assume it has to do with blockchains. In > fact, work on smart contracts precedes blockchains by several decades. > If you look at http://www.erights.org/ on which many of the ideas in > Spritely Goblins is based, you'll notice that it has the word "smart > contracts" prominently, yet this was well over a decade before > blockchains even existed. What the heck? > > Smart contracts as something implemented with distributed objects can be > best understood probably by reading Capability Based Financial Instruments: > > http://erights.org/elib/capability/ode/index.html > > The mint example from that paper is implemented in Goblins: > > > https://gitlab.com/spritely/goblins/-/blob/dev/goblins/actor-lib/simple-mint.rkt > > That's right, in about 25 lines of Goblins code you can have a > functioning bank of sorts, which preserves financial integrity and even > permits networked accounts. No blockchain required. > > Yet, you could add a blockchain, or even turn Goblins into a blockchain > if you wanted. (Since Goblins' actor state is transactional and > snapshottable, you can have a merkle tree of all inputs, and global > consensus on the set of messages accepted by the network, and all > participants can replay and simulate the same abstract machine. This is > fairly trivial to do in Goblins.) > > But more interestingly, Agoric has already done the work of abstracting > even remote blockchains as abstract machines on the network. Since > we'll be implementing the same CapTP, when the time comes you'll be able > to access all that for free, even though Agoric programs are written in > Javascript and Goblins programs in Racket. > > Anyway, the next release of Goblins, coming soon, should allow for > beginning to play with this kind of stuff on the network more easily > than in the present (v0.7) stuff, which currently takes a lot of work. > So maybe if you can wait a few weeks, it'll be easier to talk about. > > But "smart contracts" is a use case, a broad problem domain. What kind > of smart contracts are you wanting to write? > > - Chris > -- 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/6066d33f-f6e5-44ed-bed9-edda173b15c2n%40googlegroups.com.
Re: [racket-users] Smart contracts in Racket
Hello! My code is a bit long. I formalised two languages for smart contracts, with a typechecker, so this might not be for me :D but thank you! A terça-feira, 16 de março de 2021 à(s) 18:22:44 UTC, James Platt escreveu: > > On Mar 15, 2021, at 7:01 PM, Beatriz Moreira wrote: > > > Hello! I recently used Racket as a tool to see the small step execution > of some smart contract languages and I was wondering if there is anywhere i > can submit my work or share it with the Racket community. > > One place might be the Racket Artifacts site. I think it's mainly intended > for short demonstrations of code but, if yours is not too long, that might > be the place. > > https://github.com/racket/racket/wiki/Artifacts > > I am interested in smart contracts, as well, for a possible future > addition to a project I am working on but it will be a while before I get > to that point. -- 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/506a256c-c6da-41dc-8e3a-5eb0ffd8d4d2n%40googlegroups.com.
[racket-users] Smart contracts in Racket
Hello! I recently used Racket as a tool to see the small step execution of some smart contract languages and I was wondering if there is anywhere i can submit my work or share it with the Racket community. Thank you in advance! 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+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/c64f3dff-82ae-4479-85ea-2e4aec1b899fn%40googlegroups.com.
Re: [racket-users] [Redex] Side conditions in Reduction Relations
Yes a subset ! Sorry ! Yours didn't do exactly what i wanted but it helped a lot, as i didn't understand how i could also use judgments as guards in reduction relations. Thank you again :D Beatriz Moreira A quarta-feira, 3 de fevereiro de 2021 à(s) 22:17:50 UTC, Robby Findler escreveu: > You mean it should be a subset, not a subsequence? (And yes, the example I > sent was one where I was guessing that mine did not do what you want!) > > Robby > > > On Wed, Feb 3, 2021 at 4:14 PM Beatriz Moreira > wrote: > >> 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 >>> 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 < >>>>> beatriz@gmail.com> wrote: >>>>> >>>>>> Hi ! >>>>>> I have a reduction relation where I have to match a pattern *ts* to >>>>
Re: [racket-users] [Redex] Side conditions in Reduction Relations
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 > 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 >>> 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_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...@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 >> >> <https://groups.google.com/d/msgid/racket-users/0c6555d8-9c60-4371-9369-30bd93e3027fn%40googlegroups.com?utm_medium=email_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/a2db87c0-ccfa-4a2f-86ed-ce9aac0fe37en%40googlegroups.com.
Re: [racket-users] [Redex] Side conditions in Reduction Relations
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 > 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_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.
[racket-users] [Redex] Side conditions in Reduction Relations
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+unsubscr...@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.
Re: [racket-users] side-conditions
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: #* 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 :) A segunda-feira, 21 de dezembro de 2020 à(s) 15:05:37 UTC, Robby Findler escreveu: > I recommend you define a metafunction or judgment form that captures what > you want exactly and then use that. > > Robby > > > On Mon, Dec 21, 2020 at 8:32 AM Beatriz Moreira > wrote: > >> 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 :) >> >> -- >> 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 >> >> <https://groups.google.com/d/msgid/racket-users/c8632f31-98c2-46cb-8231-2ca272ae2b8an%40googlegroups.com?utm_medium=email_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/30754357-0563-4709-8d88-f0f8ef5d8b63n%40googlegroups.com.
[racket-users] side-conditions
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 :) -- 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/c8632f31-98c2-46cb-8231-2ca272ae2b8an%40googlegroups.com.
Re: [racket-users] Pattern Matching
Hello, Yes, my idea is to check the type of the parameters. I still have to add the types to my code, but I was trying to see if I could do it without them (just pattern matching), as the functions of type *f* are in the declaration of the contract. Can you access this link? https://bitbucket.org/beatrizmoreira/msc/src/master/fwsollast.rkt Thank you for your answer :D A terça-feira, 29 de setembro de 2020 à(s) 17:20:58 UTC+1, wesley@gmail.com escreveu: > Hello Beatriz, > > Is this something like contracts with parameters? That sounds neat, > actually. > > Anyway, this seems more like syntax analysis rather than string matching, > but I'm not entirely certain as to what your approach is. I can't access > the file you linked. > > If this _is_ syntax analysis, then maybe a macro using `syntax-case` or > `syntax-parse` would serve you better? Again, I'm not exactly sure what > your approach is, and I'm sorry for that. > On Monday, September 28, 2020 at 3:31:11 PM UTC-4 gneuner2 wrote: > >> >> On 9/28/2020 10:50 AM, Beatriz Moreira wrote: >> >> Hello, >> I would like to know how do I match multiple variables to a regular >> expression. >> My idea is to match every *f* variables (f...) to an *f* in ((contract C >> ((T x) ...) ((T f)) ...) ... ). >> I am trying to implement a core language for smart contracts in Racket, >> but I need to have as pre condition in my reduction rules that the *f* is >> a function in one of the contracts. >> Thank you! :) >> >> >> 'regexp-match*' outputs a list of matched strings, and match has an apply >> clause: '(app *expr* pats ...)' which evaluates *expr* and tries to >> match the output. My first thought would be to try something like: >> >> match ( inp ) >> : >> ((app (regexp-match* pattern inp) match1 match2 ... ) >>... ) >> : >> >> Caveat ... I've never tried to do this. If match doesn't like this >> approach (or something close to it), then I would separately perform the >> regexp-match* and the pattern match on its output list. >> >> Hope this helps, >> George >> >> https://docs.racket-lang.org/reference/regexp.html >> https://docs.racket-lang.org/reference/match.html >> > -- 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/76283498-990f-4c7c-b445-0d40f10108can%40googlegroups.com.
Re: [racket-users] Pattern Matching
Hello, I don't think this is what im looking for, but thank you very much :D A segunda-feira, 28 de setembro de 2020 à(s) 20:31:11 UTC+1, gneuner2 escreveu: > > On 9/28/2020 10:50 AM, Beatriz Moreira wrote: > > Hello, > I would like to know how do I match multiple variables to a regular > expression. > My idea is to match every *f* variables (f...) to an *f* in ((contract C > ((T x) ...) ((T f)) ...) ... ). > I am trying to implement a core language for smart contracts in Racket, > but I need to have as pre condition in my reduction rules that the *f* is > a function in one of the contracts. > Thank you! :) > > > 'regexp-match*' outputs a list of matched strings, and match has an apply > clause: '(app *expr* pats ...)' which evaluates *expr* and tries to match > the output. My first thought would be to try something like: > > match ( inp ) > : > ((app (regexp-match* pattern inp) match1 match2 ... ) >... ) > : > > Caveat ... I've never tried to do this. If match doesn't like this > approach (or something close to it), then I would separately perform the > regexp-match* and the pattern match on its output list. > > Hope this helps, > George > > https://docs.racket-lang.org/reference/regexp.html > https://docs.racket-lang.org/reference/match.html > -- 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/3d0e5945-a81e-4424-99c5-96f6d0b7b198n%40googlegroups.com.
[racket-users] Pattern Matching
Hello, I would like to know how do I match multiple variables to a regular expression. My idea is to match every *f* variables (f...) to an *f* in ((contract C ((T x) ...) ((T f)) ...) ... ). I am trying to implement a core language for smart contracts in Racket, but I need to have as pre condition in my reduction rules that the *f* is a function in one of the contracts. Thank you! :) https://bitbucket.org/beatrizmoreira/msc/src/master/fwsollast.rkt -- 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/e4bc2e79-c375-4dad-8d49-2f308ad53c19n%40googlegroups.com.
[racket-users] [Reduction Relation] where clause
Hello, I was reading your documentation for the Reduction Relations (4.4), and we can use side-conditions and other extras like where and bind. But I cannot implement them in my code. Can someone show me an example of how do I use the clause *where*? For example, how do I verify that a variable *f* is the same f as the one in the pattern-sequence *T f ( T x ).* Thank you! -- 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/83123805-8d83-486d-9680-05551aaced8bn%40googlegroups.com.
Re: [racket-users] [relation-rules] found the same binder
Thank you, the problem was that I was defining f_0 as multiple patterns of*
(c_0 -> f_0)...* and only comparing it to one instance of f_0.
A quinta-feira, 24 de setembro de 2020 à(s) 02:27:45 UTC+1, Robby Findler
escreveu:
> I'm not sure exactly what you're trying to accomplish so take this with a
> grain of salt, but that error message means that redex doesn't really know
> how to interpret your rules. Here's a simpler example that has the same
> error message.
>
> (reduction-relation
>L
>(--> (+ (+ n ...) n)
> 5))
>
> In this case you might be intending to say that all of the "n"s inside the
> inner plus should be the same and should also be the same as the one in
> outer plus.
>
> Redex's pattern matcher isn't smart enough to do that for you, so you'd
> need to write something explicitly that makes sure you get what you want,
> running example below.
>
> Maybe in your actual code you can use a similar idea. I would also say
> that your patterns look huge so it is probably in your interest to
> introduce something to break things down into simpler pieces somehow and
> judgment-forms are one tool to help with that.
>
> hth,
> Robby
>
>
> #lang racket
> (require redex)
>
> (define-language L
> (e ::= (+ e ...) n)
> (n ::= natural))
>
> (define red
> (reduction-relation
>L
>(--> (+ (+ n_2 ...) n_1)
> 5
> (judgment-holds (matching n_1 (n_2 ...)))
> )))
>
> (define-judgment-form L
> #:mode (matching I I)
> #:contract (matching n (n ...))
>
> [---
>(matching n ())]
>
> [(matching n_1 (n_2 ...))
>--------
>(matching n_1 (n_1 n_2 ...))])
>
>
> (test--> red
> (term (+ (+ 1 1 1 1) 1))
> 5)
>
>
> On Tue, Sep 22, 2020 at 12:18 PM Beatriz Moreira
> wrote:
>
>> Hello,
>> I have a bunch of relation rules, but in one of them i need to check if
>> f_0 is the same as i have in one of the environments, but the error
>> *reduction-relation:
>> found the same binder, f_0, at different depths, 0 and 1 ... F_01 ... (T
>> f_0 ((T_00 x_00) ...) (return e)) F_02 ...)) (contract C_2 ((T_2 x_21) ...
>> K_2 F_2... *appears and i would like to know if there's an alternative.
>>
>> The part of the code where the error is is below and the link for the
>> repository is this :
>> https://bitbucket.org/beatrizmoreira/msc/src/master/fwsollast.rkt
>>
>> Thank you!
>>
>>
>> (--> [(in-hole E (c -> f -> value (n) ((s : (c_0 -> f_0)) ...))) env-ß
>> env-σ ((contract C_1 {(T_1 x_11) ... K_1 F_1 ...}) ... (contract C {(T_0
>> x_01) ... K F_01 ... (T f_0 ((T_00 x_00) ... ) {return e}) F_02 ...})
>> (contract C_2 {(T_2 x_21) ... K_2 F_2 ...}) ...)]
>> [(in-hole E (return (call env-ß CT c
>> (top-σ env-σ) f n ((s : (c_0 -> f_0))
>> ... (decl (uptbal (uptbal env-ß (ref env-ß c) n) (top-σ env-σ) ,(-
>> (term 0)(term n))) ((s -> (c_0 -> f_0)) ...)) (call-σ env-σ (ref env-ß c))
>> ((contract C_1 {(T_1 x_11) ... K_1 F_1 ...}) ... (contract C {(T_0 x_01)
>> ... K F_01 ... (T f_0 ((T_00 x_00) ... ) {return e}) F_02 ...}) (contract
>> C_2 {(T_2 x_21) ... K_2 F_2 ...}) ...)]
>> (side-condition)
>> "CALL2")
>>
>> --
>> 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/6ab63e3a-72f8-4ae9-a43a-64dcb07a9320n%40googlegroups.com
>>
>> <https://groups.google.com/d/msgid/racket-users/6ab63e3a-72f8-4ae9-a43a-64dcb07a9320n%40googlegroups.com?utm_medium=email_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/d3d0ecb9-c6db-4b9f-88d0-61933d9f0f2an%40googlegroups.com.
[racket-users] [relation-rules] found the same binder
Hello,
I have a bunch of relation rules, but in one of them i need to check if f_0
is the same as i have in one of the environments, but the error
*reduction-relation:
found the same binder, f_0, at different depths, 0 and 1 ... F_01 ... (T
f_0 ((T_00 x_00) ...) (return e)) F_02 ...)) (contract C_2 ((T_2 x_21) ...
K_2 F_2... *appears and i would like to know if there's an alternative.
The part of the code where the error is is below and the link for the
repository is this :
https://bitbucket.org/beatrizmoreira/msc/src/master/fwsollast.rkt
Thank you!
(--> [(in-hole E (c -> f -> value (n) ((s : (c_0 -> f_0)) ...))) env-ß
env-σ ((contract C_1 {(T_1 x_11) ... K_1 F_1 ...}) ... (contract C {(T_0
x_01) ... K F_01 ... (T f_0 ((T_00 x_00) ... ) {return e}) F_02 ...})
(contract C_2 {(T_2 x_21) ... K_2 F_2 ...}) ...)]
[(in-hole E (return (call env-ß CT c
(top-σ env-σ) f n ((s : (c_0 -> f_0))
... (decl (uptbal (uptbal env-ß (ref env-ß c) n) (top-σ env-σ) ,(-
(term 0)(term n))) ((s -> (c_0 -> f_0)) ...)) (call-σ env-σ (ref env-ß c))
((contract C_1 {(T_1 x_11) ... K_1 F_1 ...}) ... (contract C {(T_0 x_01)
... K F_01 ... (T f_0 ((T_00 x_00) ... ) {return e}) F_02 ...}) (contract
C_2 {(T_2 x_21) ... K_2 F_2 ...}) ...)]
(side-condition)
"CALL2")
--
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/6ab63e3a-72f8-4ae9-a43a-64dcb07a9320n%40googlegroups.com.
[racket-users] "is not in my domain"
Hi, im a beginner with racket and im using it to implement a language in
order to test its operational semantic rules.
This is the function where i keep having the error:
(define-metafunction FS
call : env-ß classes address f ((x v)...) -> e
[(call (env-ß_1 ... ((address_1 C_1 n_1 vars_1 ...) ... (address C n vars
...) (address_2 C_2 n_2 vars_2 ...) ...) env-ß_2 ...)
((contract C_1 {x_11 ...} F_1) ... (contract C {x_1 ...} f (x ...) {return
e}) (contract C_2 {x_22 ...} F_2) ...) address f ((x v)...))
e])
And this is the error message :
../../../../../../../Applications/Racket
v7.6/share/pkgs/redex-lib/redex/private/reduction-semantics.rkt:1588:55:
call: (call (((2 C 4 (x 3) (r 9)) (9 A 24 (a 9) (b 5 ((contract C (x r)
(a (d y) (return (y + d (contract A (a b) (c (a b) (return (3) 2 a
(d 7) (y 3)) is not in my domain
I have tried changing the parenthesis but i can't seem to get it right.
Here's the code
.Thank
you guys for your help! :)
--
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/88c98b73-7ad4-4fd9-ab47-484ab0c686ae%40googlegroups.com.
