If you want to stay inside redex-land, you have to do something like the code below, where you use typesetting to turn uses of length-ok (in other relations) into something like "#(l) = k".
hth, Robby #lang racket (require redex) (define-term k 3) (define-language L) (define-judgment-form L #:mode (length-ok I I) #:contract (length-ok (any ...) natural) [---------------- (length-ok () 0)] [(length-ok (any_2 ...) ,(- (term natural_k) 1)) --------------------------------------- (length-ok (any_1 any_2 ...) natural_k)]) (test-judgment-holds (length-ok (1 2 3) k)) (test-results) On Fri, Mar 16, 2018 at 7:44 AM, 'Leandro Facchinetti' via Racket Users < [email protected]> wrote: > > But I clearly don’t get what you really want so I will abandon this one. >> >> Good luck — Matthias >> > > Thanks for trying, talking to you is always instructive 😀 > > For people that hasn’t abandoned this one: I decided to bite the bullet > and thread the ‘metaparameter’ in my definitions. This will allow me to > re-enable the cache, and I’m interested in measuring how this impacts > performance. (I’m not benchmarking these models, I know that isn’t Redex > purpose, but there are some small programs that are beyond the reach of my > models because they take too long to complete.) In the process I found a > case that I can’t express: in my language definition I have a production > that means “a list of maximum size ‘k’”, which I express with a > side-condition. There is no way to *thread parameters* into ‘redex-match?’ > and pattern matching in general, so I have to turn off this verification. > > The problem below is a minimal working example to illustrate my use case. > Either I have to remove the ‘side-condition’ for ‘t’ or turn off the cache: > > #lang racket > (require redex) > > (define k (make-parameter 0)) > > (define-language L > [t ::= (side-condition (name t [_ ...]) (<= (length (term t)) (k)))]) > > (caching-enabled? #f) > > (displayln (redex-match? L t (term []))) ;; => #t > (displayln (redex-match? L t (term [a]))) ;; => #f > (displayln (redex-match? L t (term [a b]))) ;; => #f > > (parameterize ([k 1]) > (displayln (redex-match? L t (term []))) ;; => #t > (displayln (redex-match? L t (term [a]))) ;; => #t > (displayln (redex-match? L t (term [a b]))) ;; => #f > ) > > -- > 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]. > For more options, visit https://groups.google.com/d/optout. > -- 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]. For more options, visit https://groups.google.com/d/optout.
