The variables from the contract are bound only if they have
underscores in them (because ones without underscores are not
constrained to be the same when they appear in contract positions (or
in define-language)). I've pushed a small clarification of this in the
docs and below is a program that demonstrates an invariant in action.
hth,
Robby
#lang racket/base
(require redex)
(define-language L
[nat ::= Z (S nat)])
(define-judgment-form L
#:mode (sum I I O)
#:contract (sum nat_1 nat_2 nat_3)
#:inv (≤ nat_3 nat_1)
[---------------
(sum Z nat nat)]
[(sum nat_1 nat_2 nat_3)
-------------------------------
(sum (S nat_1) nat_2 (S nat_3))])
(define-judgment-form L
#:mode (≤ I I)
#:contract (≤ nat nat)
[------------
(≤ Z nat)]
[(≤ nat_1 nat_2)
------------------------
(≤ (S nat_1) (S nat_2))])
(judgment-holds (sum (S (S (S Z)))
(S (S (S (S Z))))
nat)
nat)
On Fri, Jan 18, 2019 at 7:03 PM Joey Eremondi <joey.eremo...@gmail.com> wrote:
>
> I'm wondering, are there any good examples out there of using #:inv with
> Redex-judgments? Particularly with asserting that some other judgment holds
> on the output.
>
> For example, I've got:
> #:contract (SomeJudgment Gamma tt gv gU)
> #:inv ,(judgment-holds (SomeOtherJudgment gv gU))
>
> The problem I'm having right now is that, if I unquote gv and gU in the
> invariant, it says they're unbound variables. But if I quote them, it uses
> the literal terms (term gv) and (term gU), that is, it's not properly
> binding/substituting gv and gU when it's evaluating the contract.
>
> If I add a (begin (println (term gv) ... ) to the contract, it prints 'gv,
> confirming that the substitution isn't happening.
>
> Am I using this wrong? Are there examples of its proper usage, or is this
> just a mostly-unused feature in Redex?
>
> Thanks for all the Redex 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.
> 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 racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
