suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Adds bigger define-judgment-form examples

Browse Source
This commit is contained in:
Casey Klein 2011-08-09 09:38:06 -05:00
parent 31ec46170d
commit f803f187bd
5 changed files with 320 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
collects/redex/examples/README
View File

@ -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"

51
collects/redex/examples/define-judgment-form/multi-val.rkt Normal file
View File

@ -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)))

137
collects/redex/examples/define-judgment-form/sos.rkt Normal file
View File

@ -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)))

112
collects/redex/examples/define-judgment-form/typing-rules.rkt Normal file
View File

@ -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))

20
collects/redex/redex.scrbl
View File

@ -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))