From f803f187bdcce3f0ab3de17c11e00d87b68ee726 Mon Sep 17 00:00:00 2001 From: Casey Klein Date: Tue, 9 Aug 2011 09:38:06 -0500 Subject: [PATCH] Adds bigger define-judgment-form examples --- collects/redex/examples/README | 2 + .../define-judgment-form/multi-val.rkt | 51 +++++++ .../examples/define-judgment-form/sos.rkt | 137 ++++++++++++++++++ .../define-judgment-form/typing-rules.rkt | 112 ++++++++++++++ collects/redex/redex.scrbl | 20 ++- 5 files changed, 320 insertions(+), 2 deletions(-) create mode 100644 collects/redex/examples/define-judgment-form/multi-val.rkt create mode 100644 collects/redex/examples/define-judgment-form/sos.rkt create mode 100644 collects/redex/examples/define-judgment-form/typing-rules.rkt diff --git a/collects/redex/examples/README b/collects/redex/examples/README index 2b2789e793..9f0bae8c5b 100644 --- a/collects/redex/examples/README +++ b/collects/redex/examples/README @@ -26,6 +26,8 @@ to demonstrate various different uses of PLT Redex: with function contracts, (eager) pair contracts, and a few numeric predicates + define-judgment-form: example uses of `define-judgment-form' + delim-cont: The model from Flatt, Yu, Findler, and Felleisen's ICFP '07 paper "Adding Delimited and Composable Control to a Production Programming Environment" diff --git a/collects/redex/examples/define-judgment-form/multi-val.rkt b/collects/redex/examples/define-judgment-form/multi-val.rkt new file mode 100644 index 0000000000..d1fb7536cd --- /dev/null +++ b/collects/redex/examples/define-judgment-form/multi-val.rkt @@ -0,0 +1,51 @@ +#lang racket + +(require redex) + +(define-language non-det-arith + (e (e e) + x + v) + (v (λ (x) e) + integer + add1) + (E hole + (E e) + (v E)) + (x variable-not-otherwise-mentioned)) + +(define reduction + (reduction-relation + non-det-arith + (--> (in-hole E ((λ (x) e) v)) + (in-hole E (subst e x v))) + (--> (in-hole E (add1 integer)) + (in-hole E v) + (judgment-holds (δ add1 integer v))))) + +(define-judgment-form non-det-arith + #:mode (δ I I O) + [(δ add1 integer 0)] + [(δ add1 integer v) + (where v (Σ 1 integer))]) + +(define-metafunction non-det-arith + Σ : integer ... -> integer + [(Σ integer ...) + ,(apply + (term (integer ...)))]) + +(define-metafunction non-det-arith + subst : e x v -> e + [(subst (e_1 e_2) x v) + ((subst e_1 x v) (subst e_2 x v))] + [(subst x x v) v] + [(subst x_1 x_2 v) x_1] + [(subst (λ (x) e) x v) + (λ (x) e)] + [(subst (λ (x_1) e) x_2 v) + ; capture shmapture... + (λ (x_1) (subst e x_2 v))] + [(subst integer x v) integer] + [(subst add1 x v) add1]) + +(traces reduction (term (((λ (x) (λ (x) (x (add1 7)))) (add1 0)) add1))) \ No newline at end of file diff --git a/collects/redex/examples/define-judgment-form/sos.rkt b/collects/redex/examples/define-judgment-form/sos.rkt new file mode 100644 index 0000000000..a23b9262ec --- /dev/null +++ b/collects/redex/examples/define-judgment-form/sos.rkt @@ -0,0 +1,137 @@ +#lang racket + +(require redex) + + +; +; +; ;;; ; ; ; +; ; ; ; ; +; ; ; ;;; ;;;;; ;;; ;; ;; ;;; ;;;;; ;;; ;;; ;; ;; +; ; ; ; ; ; ; ;; ; ; ; ; ; ; ;; ; +; ; ; ;;;;; ; ; ; ; ; ; ; ; ; ; ; +; ; ; ; ; ; ; ; ; ; ; ; ; ; ; +; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; +; ;;;; ;;;; ;;;;; ;;;;; ;;; ;;; ;;;;; ;;; ;;;;; ;;; ;;; ;;; +; +; +; +; + + +(define-language λv + (e (e e) + x + v) + (v (λ (x) e) + i + add1) + (i integer) + (x variable-not-otherwise-mentioned)) + +(define-judgment-form λv + #:mode (small-step I O) + #:contract (small-step e e) + [(small-step ((λ (x) e) v) (subst e x v))] + [(small-step (add1 i) (δ add1 i))] + [(small-step (e_1 e_2) (e_1′ e_2)) + (small-step e_1 e_1′)] + [(small-step (v e_2) (v e_2′)) + (small-step e_2 e_2′)]) + +(define-judgment-form λv + #:mode (small-step* I O) + #:contract (small-step* e e) + [(small-step* e e)] + [(small-step* e_1 e_3) + (small-step e_1 e_2) + (small-step* e_2 e_3)]) + +(define-judgment-form λv + #:mode (eval I O) + #:contract (eval e e) + [(eval e v) + (small-step* e v)]) + +(define-metafunction λv + [(δ add1 i) ,(add1 (term i))]) + +(define-metafunction λv + subst : e x v -> e + [(subst (e_1 e_2) x v) + ((subst e_1 x v) (subst e_2 x v))] + [(subst x x v) v] + [(subst x_1 x_2 v) x_1] + [(subst (λ (x) e) x v) + (λ (x) e)] + [(subst (λ (x_1) e) x_2 v) + ; capture shmapture... + (λ (x_1) (subst e x_2 v))] + [(subst i x v) i] + [(subst add1 x v) add1]) + +(test-equal (judgment-holds (eval (add1 (add1 (add1 0))) v) v) + (list (term 3))) +(test-equal (judgment-holds + (eval (((λ (x) (λ (x) (x (add1 7)))) 0) add1) + v) + v) + (list (term 9))) + + +; +; +; ; +; ; ; ; ; ; +; ; ;;; ;;;;; ;; ;;; ;;;; ;;; ;;;;; ;;;;; ;;; ;; ;; ;; ;; +; ; ; ; ;; ; ; ; ; ; ; ; ; ; ; ;; ; ; ;; +; ; ; ; ; ; ;;;;; ;;; ;;;;; ; ; ; ; ; ; ; +; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; +; ; ;; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; +; ;;; ; ;;;; ;;;; ;;;; ;;;; ;;; ;;; ;;;;; ;;; ;;; ;;;; +; ; ; ; +; ;;;; ;;; ;;; +; +; + + +(define rewrite-subst + (match-lambda + [(list _ _ e x v _) + (list "" e "{" x ":=" v "}")])) +(define rewrite-small-step + (match-lambda + [(list _ _ e1 e2 _) + (list "" e1 " → " e2)])) + +(with-compound-rewriters + (['small-step rewrite-small-step] + ['subst rewrite-subst]) + (render-judgment-form small-step)) + + +; +; +; ; +; ; ; ; +; ; ;; ;; ;;; ;;;; ;;; ;; ;; ;; ;; +; ; ;; ; ; ; ; ; ;; ; ; ;; +; ; ; ;;;; ; ; ; ; ; ; +; ; ; ; ; ; ; ; ; ; ; +; ; ; ; ; ; ; ; ; ; ; ; +; ;;; ;;;;; ;;;;; ;;; ;;;;; ;;; ;;; ;;;; +; ; +; ;;; +; +; + +;; Relations defined with `define-judgment-form' do +;; not work directly with `traces', but they can be +;; embedded within reduction relations. +(define small-step-rr + (reduction-relation + λv + (--> e_1 e_2 + (judgment-holds (small-step e_1 e_2))))) + +(traces small-step-rr (term ((λ (x) (add1 x)) 0))) \ No newline at end of file diff --git a/collects/redex/examples/define-judgment-form/typing-rules.rkt b/collects/redex/examples/define-judgment-form/typing-rules.rkt new file mode 100644 index 0000000000..aa88ce7389 --- /dev/null +++ b/collects/redex/examples/define-judgment-form/typing-rules.rkt @@ -0,0 +1,112 @@ +#lang racket + +(require redex/pict + redex/reduction-semantics) + + +; +; +; ;;; ; ; ; +; ; ; ; ; +; ; ; ;;; ;;;;; ;;; ;; ;; ;;; ;;;;; ;;; ;;; ;; ;; +; ; ; ; ; ; ; ;; ; ; ; ; ; ; ;; ; +; ; ; ;;;;; ; ; ; ; ; ; ; ; ; ; ; +; ; ; ; ; ; ; ; ; ; ; ; ; ; ; +; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; +; ;;;; ;;;; ;;;;; ;;;;; ;;; ;;; ;;;;; ;;; ;;;;; ;;; ;;; ;;; +; +; +; +; + + +(define-language STLC + (e (λ (x τ) e) + (e e) + x + i + add1) + (τ int + (τ → τ)) + (Γ ([x τ] ...)) + (i integer) + (x variable-not-otherwise-mentioned)) + +(define-judgment-form STLC + #:mode (typeof I I O) + #:contract (typeof Γ e τ) + [(typeof Γ (λ (x τ_1) e) (τ_1 → τ_2)) + (typeof (extend Γ x τ_1) e τ_2)] + [(typeof Γ (e_1 e_2) τ) + (typeof Γ e_1 (τ_2 → τ)) + (typeof Γ e_2 τ_2)] + [(typeof Γ x τ) + (where τ (lookup Γ x))] + [(typeof Γ i int)] + [(typeof Γ add1 (int → int))]) + +(define-metafunction STLC + extend : Γ x τ -> Γ + [(extend ([x_0 τ_0] ... [x_i τ_i] [x_i+1 τ_i+1] ...) x_i τ) + ([x_0 τ_0] ... [x_i τ] [x_i+1 τ_i+1] ...)] + [(extend ([x_1 τ_1] ...) x_0 τ_0) + ([x_0 τ_0] [x_1 τ_1] ...)]) + +(define-metafunction STLC + lookup : Γ x -> τ + [(lookup ([x_0 τ_0] ... [x_i τ_i] [x_i+1 τ_i+1] ...) x_i) + τ_i]) + +(test-equal + (judgment-holds + (typeof () + (λ (x int) + (λ (x (int → int)) + (x (add1 7)))) + τ) + τ) + (list (term (int → ((int → int) → int))))) +(test-equal + (judgment-holds + (typeof () + (λ (x int) + (λ (x (int → int)) + (add1 x))) + τ)) + #f) + + +; +; +; ; +; ; ; ; ; ; +; ; ;;; ;;;;; ;; ;;; ;;;; ;;; ;;;;; ;;;;; ;;; ;; ;; ;; ;; +; ; ; ; ;; ; ; ; ; ; ; ; ; ; ; ;; ; ; ;; +; ; ; ; ; ; ;;;;; ;;; ;;;;; ; ; ; ; ; ; ; +; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; +; ; ;; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; +; ;;; ; ;;;; ;;;; ;;;; ;;;; ;;; ;;; ;;;;; ;;; ;;; ;;;; +; ; ; ; +; ;;;; ;;; ;;; +; +; + + +(define rewrite-typeof + (match-lambda + [(list _ _ Γ e τ _) + (list "" Γ " ⊢ " e " : " τ)])) +(define rewrite-extend + (match-lambda + [(list _ _ Γ x τ _) + (list "" Γ ", " x ":" τ)])) +(define rewrite-lookup + (match-lambda + [(list _ _ Γ x _) + (list "" Γ "(" x ")")])) + +(with-compound-rewriters + (['typeof rewrite-typeof] + ['extend rewrite-extend] + ['lookup rewrite-lookup]) + (render-judgment-form typeof)) \ No newline at end of file diff --git a/collects/redex/redex.scrbl b/collects/redex/redex.scrbl index fd35a3293b..d78e710f6a 100644 --- a/collects/redex/redex.scrbl +++ b/collects/redex/redex.scrbl @@ -56,6 +56,11 @@ (list (racketidfont (make-element #f (list (symbol->string 'a0)))) (make-element #f (list " " (hspace 1) " " (racketidfont (symbol->string 'a)))) ...))))) +@(define (examples-link relative-path text) + (link (string-append "http://git.racket-lang.org/plt/tree/HEAD:/collects/redex/examples/" + relative-path) + (filepath text))) + @(define redex-eval (make-base-eval)) @(interaction-eval #:eval redex-eval (require redex/reduction-semantics)) @@ -787,7 +792,7 @@ variables in the @|ttpattern| are bound in that expression. A a @racket[side-condition] clause, except that the condition is not rendered when typesetting via @racketmodname[redex/pict]. -Each @as-index{@racket[where] clause} acts as a side condition requiring a +Each @deftech{@racket[where] clause} acts as a side condition requiring a successful pattern match, and it can bind pattern variables in the side-conditions (and @racket[where] clauses) that follow and in the metafunction result. The bindings are the same as bindings in a @@ -1193,7 +1198,18 @@ non-termination. For example, consider the following definitions: (path v_2 v_3)])] Due to the second @racket[path] rule, the follow query fails to terminate: @racketinput[(judgment-holds (path a c))] -} + +The @(examples-link "" "examples") directory demonstrates three use cases: +@itemlist[ +@item{@(examples-link "define-judgment-form/typing-rules.rkt" "typing-rules.rkt") --- + defines a type system in a way that supports mechanized typesetting. + When a typing judgment form can be given a mode, it can also be encoded as + a metafunction using @tech{@racket[where] clauses} as premises, but Redex + cannot typeset that encoding as inference rules.} +@item{@(examples-link "define-judgment-form/sos.rkt" "sos.rkt") --- + defines an SOS-style semantics in a way that supports mechanized typesetting.} +@item{@(examples-link "define-judgment-form/multi-val.rkt" "multi-val.rkt") --- + defines a judgment form that serves as a multi-valued metafunction.}]} @defform*/subs[((judgment-holds judgment) (judgment-holds judgment @#,tttterm))