diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/1.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/1.diff index e9ce5bb684..67f1a494b8 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/1.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/1.diff @@ -5,9 +5,11 @@ > > ;; note: this bug was found and fixed during the development of this model > ;; with commit: 4b848777d12a2e5b59b43c8e77f9f68b747d1151 -224c227 +223c226 < (monitor (list/c ctc) (ccm mk t) k l j) --- > (monitor ctc (ccm mk t) k l j) -1554d1556 -< +325a329 +> +936a941 +> diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/2.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/2.diff index bf7a79b4ce..86d6b69d20 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/2.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/2.diff @@ -2,7 +2,12 @@ < (define the-error "no-error") --- > (define the-error "list/c contracts aren't applied properly in the cons case") -206c206 +205c205 < (--> (monitor (list/c ctc) (cons v_1 v_2) k l j) --- > (--> (monitor ctc (cons v_1 v_2) k l j) +325a326 +> +936a938,939 +> +> diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/3.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/3.diff index d9c28f93c0..b93bda9abe 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/3.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/3.diff @@ -2,7 +2,12 @@ < (define the-error "no-error") --- > (define the-error "the function argument to call/comp has the wrong type") -470c470 +325a326 +> +463c464 < [(tc Γ Σ e_1 (→ (→ t_3 t_2) t_3)) --- > [(tc Γ Σ e_1 (→ t_2 t_3)) +936a938,939 +> +> diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-1.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-1.rkt index 2e45e05606..c70376ea7f 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-1.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-1.rkt @@ -5,8 +5,7 @@ ;; note: this bug was found and fixed during the development of this model ;; with commit: 4b848777d12a2e5b59b43c8e77f9f68b747d1151 -(require redex/reduction-semantics - (for-syntax syntax/parse)) +(require redex/reduction-semantics) (provide (all-defined-out)) @@ -327,11 +326,6 @@ [(not-wcm (in-hole E (wcm w hole))) #f] [(not-wcm E) #t]) -(module+ test - (check-false (term (not-wcm (wcm · hole)))) - (check-false (term (not-wcm (+ 5 (wcm · hole))))) - (check-true (term (not-wcm hole))) - (check-true (term (not-wcm (abort Num hole 5))))) ;; wcm merging, second takes precedence (define-metafunction abort-lang @@ -557,42 +551,6 @@ [(different any_1 any_1) #f] [(different any_1 any_2) #t]) -(module+ test - (judgment-holds - (tc · · (+ 1 2) t) - t) - (judgment-holds - (tc · · ((λ (x : Num) (+ x 5)) 3) t) - t) - (judgment-holds - (tc · · (if (zero? 0) #t #f) t) - t) - (judgment-holds - (tc · · - ((λ (pt : (Prompt Num Num)) - (* (% (+ 1 (abort Num pt 5)) - pt - (λ (x : Num) (+ x 5))) - 3)) - (make-prompt-tag Num Num)) - t) - t) - (judgment-holds - (tc · · (flat (λ (x : Num) (zero? x))) t) - t) - (judgment-holds - (tc · - (tag0 : (Prompt Num Num) ·) - (monitor (prompt-tag/c - (flat (λ (x : Num) (zero? x))) - (flat (λ (x : Num) (zero? x))) - Num Num) - tag0 - "pos" - "neg" - "con") - t) - t)) ;; encoding for the paper (define-metafunction abort-lang @@ -777,29 +735,6 @@ (same-prompt-tag? pt_1 pt_2)] [(same-prompt-tag? tag_1 tag_2) #f]) -(module+ test - (test-equal - (term (no-match (wcm ((key_0 0) ·) hole) tag_0)) - #t) - (test-equal - (term (no-match (wcm · hole) tag_0)) - #t) - (test-equal - (term (no-match (abort Bool #t hole) tag_0)) - #t) - (test-equal (term (no-match hole tag_0)) #t) - (test-equal - (term (no-match (% hole - tag_0 - (λ (x : Num) (+ x 2))) - tag_0)) - #f) - (test-equal - (term (no-match (% hole - tag_0 - (λ (x : Num) (+ x 2))) - tag_1)) - #t)) ;; for continuation marks (define-metafunction abort-lang @@ -890,557 +825,7 @@ (term (no-match E_pt pt))) e))) -;;(current-traced-metafunctions 'all) -;; evaluation tests -(module+ test - (require rackunit) - (check-equal? (abort-eval (term (+ 1 2))) - 3) - (check-equal? (abort-eval (term (λ (x : Num) #t))) - 'procedure) - (check-equal? (abort-eval (term (make-prompt-tag Num Bool))) - 'prompt-tag)) - -;; helper for tests -(define-syntax (do-test stx) - (syntax-parse stx - [(_ ?input ?expected) - #'(do-test ?input ?expected - #:init-store (term ·) - #:store-type ·)] - [(_ ?input ?expected #:init-store ?store #:store-type ?store-type) - #'(begin - (check-true (judgment-holds (tc · ?store-type ,?input t))) - (check-equal? (abort-eval ?input #:init-store ?store) - ?expected))])) - -;; eval and type checking tests -(module+ test - ;; recursion - (do-test - (term ((μ (f : (→ Num Num)) - (λ (n : Num) - (if (zero? n) - 1 - (* n (f (- n 1)))))) - 5)) - (term 120)) - - ;; list recursion - (do-test - (term ((μ (f : (→ (List Num) Num)) - (λ (lst : (List Num)) - (case lst - (null = 0) - ((cons x1 x2) = - (+ x1 (f x2)))))) - (cons 5 (cons 6 (null Num))))) - (term 11)) - - ;; list contract - (do-test - (term (monitor (list/c (flat (λ (x : Num) (zero? x)))) - (cons 0 (cons 6 (null Num))) - "pos" "neg" "con")) - (term (ctc-error "pos" "con"))) - - ;; no control effect - (do-test - (term (% 5 (make-prompt-tag Num Num) (λ (x : Num) x))) - (term 5)) - - ;; test basic abort & handle - (do-test - (term (let ([(pt : (Prompt Num Num)) - (make-prompt-tag Num Num)]) - (% (abort Num pt 5) - pt - (λ (x : Num) (+ x 1))))) - (term 6)) - - ;; abort past a prompt - (do-test - (term (let ([(pt : (Prompt Num Num)) - (make-prompt-tag Num Num)]) - (% (% (abort Num pt 5) - (make-prompt-tag Num Num) - (λ (x : Num) (+ x 2))) - pt - (λ (x : Num) (+ x 1))))) - (term 6)) - - ;; abort to innermost prompt - (do-test - (term (let ([(pt : (Prompt Num Num)) - (make-prompt-tag Num Num)]) - (% (% (abort Num pt 5) - pt - (λ (x : Num) (+ x 2))) - pt - (λ (x : Num) (+ x 1))))) - (term 7)) - - ;; composable continuations - (do-test - (term (let ([(pt : (Prompt Num Num)) - (make-prompt-tag Num Num)]) - (% (+ 1 (call/comp - (λ (kont : (→ Num Num)) - (+ (kont 3) (kont 5))) - pt)) - pt - (λ (x : Num) x)))) - (term 11)) - - (do-test - (term (let ([(pt : (Prompt (→ Unit Num) Num)) - (make-prompt-tag (→ Unit Num) Num)]) - (% (+ 1 (call/comp - (λ (kont : (→ Num Num)) - (abort Num pt - (λ (x : Unit) - (+ (kont 3) (kont 5))))) - pt)) - pt - (λ (kont : (→ Unit Num)) (kont unit))))) - (term 10)) - - ;; call/cc encoding - (do-test - (term (let ([(pt : (Prompt (→ Unit Num) Num)) - (make-prompt-tag (→ Unit Num) Num)]) - (% (+ 1 (call/cc - (λ (kont : (→ Num Num)) - (+ (kont 3) (kont 5))) - pt)) - pt - (λ (kont : (→ Unit Num)) (kont unit))))) - (term 4)) - - ;; handler destroys call/cc semantics - (do-test - (term (let ([(pt : (Prompt (→ Unit Num) Num)) - (make-prompt-tag (→ Unit Num) Num)]) - (% (+ 1 (call/cc - (λ (kont : (→ Num Num)) - (+ (kont 3) (kont 5))) - pt)) - pt - (λ (kont : (→ Unit Num)) 18)))) - (term 18)) - - ;; continuation marks - (do-test - (term (let ([(mk : (Mark Num)) - (make-cm-key Num)]) - (call/cm - mk 5 - (ccm mk Num)))) - (term (cons 5 (null Num)))) - - (do-test - (term (let ([(mk : (Mark Num)) - (make-cm-key Num)]) - (call/cm - mk 5 - (call/cm - mk 7 - (ccm mk Num))))) - (term (cons 7 (null Num)))) - - ;; make sure wcms merge in weird cases - (do-test - (term ((λ (f : (→ Unit (List Num))) - (wcm ((key0 5) ·) (f unit))) - (λ (x : Unit) - (wcm ((key0 3) ·) (ccm key0 Num))))) - (term (cons 3 (null Num))) - #:init-store (term (key0 : (Mark Num) ·)) - #:store-type (key0 : (Mark Num) ·)) - - ;; continuation mark contracts - (do-test - (term (let ([(mk : (Mark Num)) - (monitor (mark/c (flat (λ (x : Num) (zero? x))) Num) - (make-cm-key Num) - "pos" - "neg" - "con")]) - (call/cm - mk 5 - (ccm mk Num)))) - (term (ctc-error "neg" "con"))) - - (do-test - (term (let ([(mk : (Mark Num)) - (monitor (mark/c (flat (λ (x : Num) (zero? x))) Num) - (make-cm-key Num) - "pos" - "neg" - "con")]) - (call/cm - mk 0 - (ccm mk Num)))) - (term (cons 0 (null Num)))) - - ;; naive contract - (do-test - (term (let ([(pt : (Prompt Num Num)) - (make-prompt-tag Num Num)]) - (% (monitor (flat (λ (x : Num) (number? x))) - (abort Num pt 5) - "pos" - "neg" - "con") - pt - (λ (x : Num) (+ x 1))))) - (term 6)) - - ;; first-order checks - (do-test - (term (monitor (flat (λ (x : Num) (zero? x))) - 5 - "server" - "client" - "con")) - (term (ctc-error "server" "con"))) - - ;; prompt & abort in the same component, the tag elsewhere - (do-test - (term (let ([(pt : (Prompt Num Num)) - (monitor (prompt-tag/c (flat (λ (x : Num) (zero? x))) - (flat (λ (x : Num) (zero? x))) - Num Num) - (make-prompt-tag Num Num) - "server" - "client" - "con")]) - (% (abort Num pt 3) - pt - (λ (x : Num) (+ x 1))))) - (term (ctc-error "client" "con"))) - - ;; call/comp issue - (do-test - (term (let ([(pt : (Prompt Num Num)) - (monitor (prompt-tag/c (flat (λ (x : Num) (zero? x))) - (flat (λ (x : Num) (zero? x))) - Num Num) - (make-prompt-tag Num Num) - "server" - "client" - "con")]) - (% (+ 1 - (call/comp - (λ (k : (→ Num Num)) - (k 0)) - pt)) - pt - (λ (x : Num) (+ x 1))))) - (term (ctc-error "client" "con"))) - - ;; blame even on one side - (do-test - (term (let ([(pt1 : (Prompt Num Num)) - (make-prompt-tag Num Num)]) - (let ([(pt2 : (Prompt Num Num)) - (monitor (prompt-tag/c (flat (λ (x : Num) (zero? x))) - (flat (λ (x : Num) (zero? (- x 5)))) - Num Num) - pt1 - "client" - "server" - "con")]) - (% (+ 1 ; doesn't add to 5 - (call/comp - (λ (k : (→ Num Num)) - (k 3)) - pt1)) - pt2 - (λ (x : Num) (+ x 1)))))) - (term (ctc-error "server" "con"))) - - ;; blame even on other side - (do-test - (term (let ([(pt1 : (Prompt Num Num)) - (make-prompt-tag Num Num)]) - (let ([(pt2 : (Prompt Num Num)) - (monitor (prompt-tag/c (flat (λ (x : Num) (zero? x))) - (flat (λ (x : Num) (zero? (- x 5)))) - Num Num) - pt1 - "server" - "client" - "con")]) - (% (+ 1 ; doesn't add to 5 - (call/comp - (λ (k : (→ Num Num)) - (k 3)) - pt2)) - pt1 - (λ (x : Num) (+ x 1)))))) - (term (ctc-error "server" "con"))) - - ;; same with ho-contract - (do-test - (term (let ([(pt : (Prompt (→ Num Num) Num)) - (monitor (prompt-tag/c (-> (flat (λ (x : Num) (zero? x))) - (flat (λ (x : Num) (number? x)))) - (flat (λ (x : Num) (number? x))) - (→ Num Num) Num) - (make-prompt-tag (→ Num Num) Num) - "server" - "client" - "con")]) - (% (abort Num pt (λ (x : Num) 5)) - pt - (λ (x : (→ Num Num)) (x 8))))) - (term (ctc-error "client" "con"))) - - ;; again, but from other side - (do-test - (term (let ([(pt : (Prompt (→ Num Num) Num)) - (monitor (prompt-tag/c (-> (flat (λ (x : Num) (zero? x))) - (flat (λ (x : Num) (zero? x)))) - (flat (λ (x : Num) (zero? x))) - (→ Num Num) Num) - (make-prompt-tag (→ Num Num) Num) - "server" - "client" - "con")]) - (% (abort Num pt (λ (x : Num) 3)) - pt - (λ (f : (→ Num Num)) (f 0))))) - (term (ctc-error "client" "con"))) - - ;; abort across boundary w/ ho-value - (do-test - (term (let ([(do-prompt : (→ (→ (Prompt (→ Num Num) Num) Num) Num)) - (let ([(pt : (Prompt (→ Num Num) Num)) - (make-prompt-tag (→ Num Num) Num)]) - (monitor (-> (-> (prompt-tag/c (-> (flat (λ (x : Num) (zero? x))) - (flat (λ (x : Num) (zero? x)))) - (flat (λ (x : Num) (zero? x))) - (→ Num Num) Num) - (flat (λ (x : Num) (number? x)))) - (flat (λ (x : Num) (number? x)))) - (λ (f : (→ (Prompt (→ Num Num) Num) Num)) - (% (f pt) - pt - (λ (f : (→ Num Num)) (f 5)))) - "server" - "client" - "con"))]) - (do-prompt - (λ (pt : (Prompt (→ Num Num) Num)) - (abort Num pt (λ (v : Num) (+ v 1))))))) - (term (ctc-error "server" "con"))) ;; MF: nice example but in a paper presentation you need to simplify - - ;; where the prompt flows across multiple boundaries - (do-test - (term (let ([(do-prompt : (→ (→ (Prompt (→ Num Num) Num) Num) Num)) - (let ([(pt : (Prompt (→ Num Num) Num)) - (make-prompt-tag (→ Num Num) Num)]) - (monitor (-> (-> (prompt-tag/c (-> (flat (λ (x : Num) (number? x))) - (flat (λ (x : Num) (number? x)))) - (flat (λ (x : Num) (number? x))) - (→ Num Num) Num) - (flat (λ (x : Num) (number? x)))) - (flat (λ (x : Num) (number? x)))) - (λ (f : (→ (Prompt (→ Num Num) Num) Num)) - (% (f pt) - pt - (λ (f : (→ Num Num)) (f 1)))) - "A" - "B" - "con1"))]) - (let ([(do-prompt-2 : (→ (→ (Prompt (→ Num Num) Num) Num) Num)) - (monitor (-> (-> (prompt-tag/c (-> (flat (λ (x : Num) (zero? x))) - (flat (λ (x : Num) (number? x)))) - (flat (λ (x : Num) (number? x))) - (→ Num Num) Num) - (flat (λ (x : Num) (number? x)))) - (flat (λ (x : Num) (number? x)))) - (λ (f : (→ (Prompt (→ Num Num) Num) Num)) - (do-prompt f)) - "B" - "C" - "con2")]) - (do-prompt-2 - (λ (pt : (Prompt (→ Num Num) Num)) - (abort Num pt (λ (v : Num) (+ v 1)))))))) - (term (ctc-error "B" "con2"))) - - #| - ;; from random test generation - (do-test - (term (boolean? - (abort (monitor - (prompt-tag/c (-> (flat (λ (H) (error))) - (flat (λ (R) (error))))) - (prompt-tag v) - "pos" - "neg") - (make-prompt-tag)))) - (term (error))) - |# - ) - -;; tests for bugs found by random generation -(module+ test - - (test-equal - (term (subst (make-cm-key Bool) x 5)) - (term (make-cm-key Bool))) - - (test-equal - (term (subst (null Bool) x 5)) - (term (null Bool))) - - (test-equal - (abort-eval (term (ccm (make-cm-key Bool) Bool))) - 'null) - - (test-equal - (abort-eval (term (μ (B : Num) B))) - 'non-terminating) - - (test-equal - (abort-eval (term unit)) - 'unit) - - (test-equal - (abort-eval - (term (call/comp - (λ (Dp : (→ (Mark Bool) Num)) (make-cm-key Bool)) - (make-prompt-tag (Mark (Con Num)) Num)))) - 'missing-prompt) - - (test-equal - (term (no-match (call/comp - (λ (K : (→ (Prompt (Mark Num) Bool) - (List (Prompt Bool Unit)))) - (make-prompt-tag (Mark Num) Bool)) - (wcm · hole)) tag)) - #t) - - (test-equal - (abort-eval - (term (abort - Num - (make-prompt-tag Bool (List (Mark Bool))) - (boolean? 2)))) - 'missing-prompt) - - (test-equal - (term (marks (call/cm hole (+ 1 2) 1) key1 (null (→ (Mark Num) Num)))) - (term (null (→ (Mark Num) Num)))) - - (test-equal - (term - (marks (if (boolean? hole) 1 2) key (null (→ Num (Mark Unit))))) - (term (null (→ Num (Mark Unit))))) - - (test-equal - (term - (no-match (call/cm key (wcm · hole) - ((wcm · (λ (C : Bool) #f)) (unit? 3))) - tag)) - #t) - - (test-equal - (abort-eval - (term - (number? - (μ - (i : Num) - (- - (+ (case - (null (Con (Con Bool))) - (null = 1) - ((cons X u) = 2)) (if #t 0 0)) - i))))) - 'non-terminating) - - (test-equal - (judgment-holds - (tc - · - (tag2 - : - (Prompt (Mark (Prompt Unit Num)) (Prompt (→ Num Unit) (Con Bool))) - (tag1 - : - (Prompt Num (→ (→ Unit Unit) (Con Unit))) - (tag - : - (Prompt - (→ (Prompt Num Unit) (→ Bool Unit)) - (Prompt Num (→ (→ Unit Unit) (Con Unit)))) - ·))) - (abort - (→ Num (→ Num Num)) - tag1 - (wcm - · - (call/comp - (λ (Sa : (→ Num (Prompt (→ Num Unit) (Con Bool)))) 0) - tag2))) - t) - t) - '((→ Num (→ Num Num)))) - - (test-equal - (judgment-holds - (tc - · - (tag1 - : - (Prompt Bool (List Num)) - (key1 - : - (Mark Bool) - (tag - : - (Prompt Unit (Mark (List (Mark Unit)))) - (key : (Mark (Prompt Unit (Mark (List (Mark Unit))))) ·)))) - (wcm - ((key - (PG - (flat (λ (G : Unit) #t)) - (mark/c - (list/c (mark/c (flat (λ (b : Unit) #t)) Unit)) - (List (Mark Unit))) - tag - "B" - "iF" - "CgXohMerymUWF")) - ·) - (monitor - (flat (λ (Mk : Unit) #t)) - (abort Unit tag1 #t) - "fO" - "clRmiOfXGo" - "jxeinueLyNmLozqsKl")) - t) - t) - '(Unit)) - - (test-equal - (judgment-holds - (tc · (key : (Mark (Mark (Mark Num))) ·) - (MG - (mark/c (mark/c (flat (λ (r : Num) #f)) Num) (Mark Num)) - key - "EVYdYcpulOg" - "G" - "BjUOkycjoz") - t) - t) - '((Mark (Mark (Mark Num))))) - - ) (define (random-exp depth) (match diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-2.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-2.rkt index de00ac0527..a82c0b2e84 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-2.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-2.rkt @@ -2,8 +2,7 @@ (define the-error "list/c contracts aren't applied properly in the cons case") -(require redex/reduction-semantics - (for-syntax syntax/parse)) +(require redex/reduction-semantics) (provide (all-defined-out)) @@ -324,11 +323,6 @@ [(not-wcm (in-hole E (wcm w hole))) #f] [(not-wcm E) #t]) -(module+ test - (check-false (term (not-wcm (wcm · hole)))) - (check-false (term (not-wcm (+ 5 (wcm · hole))))) - (check-true (term (not-wcm hole))) - (check-true (term (not-wcm (abort Num hole 5))))) ;; wcm merging, second takes precedence (define-metafunction abort-lang @@ -554,42 +548,6 @@ [(different any_1 any_1) #f] [(different any_1 any_2) #t]) -(module+ test - (judgment-holds - (tc · · (+ 1 2) t) - t) - (judgment-holds - (tc · · ((λ (x : Num) (+ x 5)) 3) t) - t) - (judgment-holds - (tc · · (if (zero? 0) #t #f) t) - t) - (judgment-holds - (tc · · - ((λ (pt : (Prompt Num Num)) - (* (% (+ 1 (abort Num pt 5)) - pt - (λ (x : Num) (+ x 5))) - 3)) - (make-prompt-tag Num Num)) - t) - t) - (judgment-holds - (tc · · (flat (λ (x : Num) (zero? x))) t) - t) - (judgment-holds - (tc · - (tag0 : (Prompt Num Num) ·) - (monitor (prompt-tag/c - (flat (λ (x : Num) (zero? x))) - (flat (λ (x : Num) (zero? x))) - Num Num) - tag0 - "pos" - "neg" - "con") - t) - t)) ;; encoding for the paper (define-metafunction abort-lang @@ -774,29 +732,6 @@ (same-prompt-tag? pt_1 pt_2)] [(same-prompt-tag? tag_1 tag_2) #f]) -(module+ test - (test-equal - (term (no-match (wcm ((key_0 0) ·) hole) tag_0)) - #t) - (test-equal - (term (no-match (wcm · hole) tag_0)) - #t) - (test-equal - (term (no-match (abort Bool #t hole) tag_0)) - #t) - (test-equal (term (no-match hole tag_0)) #t) - (test-equal - (term (no-match (% hole - tag_0 - (λ (x : Num) (+ x 2))) - tag_0)) - #f) - (test-equal - (term (no-match (% hole - tag_0 - (λ (x : Num) (+ x 2))) - tag_1)) - #t)) ;; for continuation marks (define-metafunction abort-lang @@ -887,557 +822,7 @@ (term (no-match E_pt pt))) e))) -;;(current-traced-metafunctions 'all) -;; evaluation tests -(module+ test - (require rackunit) - (check-equal? (abort-eval (term (+ 1 2))) - 3) - (check-equal? (abort-eval (term (λ (x : Num) #t))) - 'procedure) - (check-equal? (abort-eval (term (make-prompt-tag Num Bool))) - 'prompt-tag)) - -;; helper for tests -(define-syntax (do-test stx) - (syntax-parse stx - [(_ ?input ?expected) - #'(do-test ?input ?expected - #:init-store (term ·) - #:store-type ·)] - [(_ ?input ?expected #:init-store ?store #:store-type ?store-type) - #'(begin - (check-true (judgment-holds (tc · ?store-type ,?input t))) - (check-equal? (abort-eval ?input #:init-store ?store) - ?expected))])) - -;; eval and type checking tests -(module+ test - ;; recursion - (do-test - (term ((μ (f : (→ Num Num)) - (λ (n : Num) - (if (zero? n) - 1 - (* n (f (- n 1)))))) - 5)) - (term 120)) - - ;; list recursion - (do-test - (term ((μ (f : (→ (List Num) Num)) - (λ (lst : (List Num)) - (case lst - (null = 0) - ((cons x1 x2) = - (+ x1 (f x2)))))) - (cons 5 (cons 6 (null Num))))) - (term 11)) - - ;; list contract - (do-test - (term (monitor (list/c (flat (λ (x : Num) (zero? x)))) - (cons 0 (cons 6 (null Num))) - "pos" "neg" "con")) - (term (ctc-error "pos" "con"))) - - ;; no control effect - (do-test - (term (% 5 (make-prompt-tag Num Num) (λ (x : Num) x))) - (term 5)) - - ;; test basic abort & handle - (do-test - (term (let ([(pt : (Prompt Num Num)) - (make-prompt-tag Num Num)]) - (% (abort Num pt 5) - pt - (λ (x : Num) (+ x 1))))) - (term 6)) - - ;; abort past a prompt - (do-test - (term (let ([(pt : (Prompt Num Num)) - (make-prompt-tag Num Num)]) - (% (% (abort Num pt 5) - (make-prompt-tag Num Num) - (λ (x : Num) (+ x 2))) - pt - (λ (x : Num) (+ x 1))))) - (term 6)) - - ;; abort to innermost prompt - (do-test - (term (let ([(pt : (Prompt Num Num)) - (make-prompt-tag Num Num)]) - (% (% (abort Num pt 5) - pt - (λ (x : Num) (+ x 2))) - pt - (λ (x : Num) (+ x 1))))) - (term 7)) - - ;; composable continuations - (do-test - (term (let ([(pt : (Prompt Num Num)) - (make-prompt-tag Num Num)]) - (% (+ 1 (call/comp - (λ (kont : (→ Num Num)) - (+ (kont 3) (kont 5))) - pt)) - pt - (λ (x : Num) x)))) - (term 11)) - - (do-test - (term (let ([(pt : (Prompt (→ Unit Num) Num)) - (make-prompt-tag (→ Unit Num) Num)]) - (% (+ 1 (call/comp - (λ (kont : (→ Num Num)) - (abort Num pt - (λ (x : Unit) - (+ (kont 3) (kont 5))))) - pt)) - pt - (λ (kont : (→ Unit Num)) (kont unit))))) - (term 10)) - - ;; call/cc encoding - (do-test - (term (let ([(pt : (Prompt (→ Unit Num) Num)) - (make-prompt-tag (→ Unit Num) Num)]) - (% (+ 1 (call/cc - (λ (kont : (→ Num Num)) - (+ (kont 3) (kont 5))) - pt)) - pt - (λ (kont : (→ Unit Num)) (kont unit))))) - (term 4)) - - ;; handler destroys call/cc semantics - (do-test - (term (let ([(pt : (Prompt (→ Unit Num) Num)) - (make-prompt-tag (→ Unit Num) Num)]) - (% (+ 1 (call/cc - (λ (kont : (→ Num Num)) - (+ (kont 3) (kont 5))) - pt)) - pt - (λ (kont : (→ Unit Num)) 18)))) - (term 18)) - - ;; continuation marks - (do-test - (term (let ([(mk : (Mark Num)) - (make-cm-key Num)]) - (call/cm - mk 5 - (ccm mk Num)))) - (term (cons 5 (null Num)))) - - (do-test - (term (let ([(mk : (Mark Num)) - (make-cm-key Num)]) - (call/cm - mk 5 - (call/cm - mk 7 - (ccm mk Num))))) - (term (cons 7 (null Num)))) - - ;; make sure wcms merge in weird cases - (do-test - (term ((λ (f : (→ Unit (List Num))) - (wcm ((key0 5) ·) (f unit))) - (λ (x : Unit) - (wcm ((key0 3) ·) (ccm key0 Num))))) - (term (cons 3 (null Num))) - #:init-store (term (key0 : (Mark Num) ·)) - #:store-type (key0 : (Mark Num) ·)) - - ;; continuation mark contracts - (do-test - (term (let ([(mk : (Mark Num)) - (monitor (mark/c (flat (λ (x : Num) (zero? x))) Num) - (make-cm-key Num) - "pos" - "neg" - "con")]) - (call/cm - mk 5 - (ccm mk Num)))) - (term (ctc-error "neg" "con"))) - - (do-test - (term (let ([(mk : (Mark Num)) - (monitor (mark/c (flat (λ (x : Num) (zero? x))) Num) - (make-cm-key Num) - "pos" - "neg" - "con")]) - (call/cm - mk 0 - (ccm mk Num)))) - (term (cons 0 (null Num)))) - - ;; naive contract - (do-test - (term (let ([(pt : (Prompt Num Num)) - (make-prompt-tag Num Num)]) - (% (monitor (flat (λ (x : Num) (number? x))) - (abort Num pt 5) - "pos" - "neg" - "con") - pt - (λ (x : Num) (+ x 1))))) - (term 6)) - - ;; first-order checks - (do-test - (term (monitor (flat (λ (x : Num) (zero? x))) - 5 - "server" - "client" - "con")) - (term (ctc-error "server" "con"))) - - ;; prompt & abort in the same component, the tag elsewhere - (do-test - (term (let ([(pt : (Prompt Num Num)) - (monitor (prompt-tag/c (flat (λ (x : Num) (zero? x))) - (flat (λ (x : Num) (zero? x))) - Num Num) - (make-prompt-tag Num Num) - "server" - "client" - "con")]) - (% (abort Num pt 3) - pt - (λ (x : Num) (+ x 1))))) - (term (ctc-error "client" "con"))) - - ;; call/comp issue - (do-test - (term (let ([(pt : (Prompt Num Num)) - (monitor (prompt-tag/c (flat (λ (x : Num) (zero? x))) - (flat (λ (x : Num) (zero? x))) - Num Num) - (make-prompt-tag Num Num) - "server" - "client" - "con")]) - (% (+ 1 - (call/comp - (λ (k : (→ Num Num)) - (k 0)) - pt)) - pt - (λ (x : Num) (+ x 1))))) - (term (ctc-error "client" "con"))) - - ;; blame even on one side - (do-test - (term (let ([(pt1 : (Prompt Num Num)) - (make-prompt-tag Num Num)]) - (let ([(pt2 : (Prompt Num Num)) - (monitor (prompt-tag/c (flat (λ (x : Num) (zero? x))) - (flat (λ (x : Num) (zero? (- x 5)))) - Num Num) - pt1 - "client" - "server" - "con")]) - (% (+ 1 ; doesn't add to 5 - (call/comp - (λ (k : (→ Num Num)) - (k 3)) - pt1)) - pt2 - (λ (x : Num) (+ x 1)))))) - (term (ctc-error "server" "con"))) - - ;; blame even on other side - (do-test - (term (let ([(pt1 : (Prompt Num Num)) - (make-prompt-tag Num Num)]) - (let ([(pt2 : (Prompt Num Num)) - (monitor (prompt-tag/c (flat (λ (x : Num) (zero? x))) - (flat (λ (x : Num) (zero? (- x 5)))) - Num Num) - pt1 - "server" - "client" - "con")]) - (% (+ 1 ; doesn't add to 5 - (call/comp - (λ (k : (→ Num Num)) - (k 3)) - pt2)) - pt1 - (λ (x : Num) (+ x 1)))))) - (term (ctc-error "server" "con"))) - - ;; same with ho-contract - (do-test - (term (let ([(pt : (Prompt (→ Num Num) Num)) - (monitor (prompt-tag/c (-> (flat (λ (x : Num) (zero? x))) - (flat (λ (x : Num) (number? x)))) - (flat (λ (x : Num) (number? x))) - (→ Num Num) Num) - (make-prompt-tag (→ Num Num) Num) - "server" - "client" - "con")]) - (% (abort Num pt (λ (x : Num) 5)) - pt - (λ (x : (→ Num Num)) (x 8))))) - (term (ctc-error "client" "con"))) - - ;; again, but from other side - (do-test - (term (let ([(pt : (Prompt (→ Num Num) Num)) - (monitor (prompt-tag/c (-> (flat (λ (x : Num) (zero? x))) - (flat (λ (x : Num) (zero? x)))) - (flat (λ (x : Num) (zero? x))) - (→ Num Num) Num) - (make-prompt-tag (→ Num Num) Num) - "server" - "client" - "con")]) - (% (abort Num pt (λ (x : Num) 3)) - pt - (λ (f : (→ Num Num)) (f 0))))) - (term (ctc-error "client" "con"))) - - ;; abort across boundary w/ ho-value - (do-test - (term (let ([(do-prompt : (→ (→ (Prompt (→ Num Num) Num) Num) Num)) - (let ([(pt : (Prompt (→ Num Num) Num)) - (make-prompt-tag (→ Num Num) Num)]) - (monitor (-> (-> (prompt-tag/c (-> (flat (λ (x : Num) (zero? x))) - (flat (λ (x : Num) (zero? x)))) - (flat (λ (x : Num) (zero? x))) - (→ Num Num) Num) - (flat (λ (x : Num) (number? x)))) - (flat (λ (x : Num) (number? x)))) - (λ (f : (→ (Prompt (→ Num Num) Num) Num)) - (% (f pt) - pt - (λ (f : (→ Num Num)) (f 5)))) - "server" - "client" - "con"))]) - (do-prompt - (λ (pt : (Prompt (→ Num Num) Num)) - (abort Num pt (λ (v : Num) (+ v 1))))))) - (term (ctc-error "server" "con"))) ;; MF: nice example but in a paper presentation you need to simplify - - ;; where the prompt flows across multiple boundaries - (do-test - (term (let ([(do-prompt : (→ (→ (Prompt (→ Num Num) Num) Num) Num)) - (let ([(pt : (Prompt (→ Num Num) Num)) - (make-prompt-tag (→ Num Num) Num)]) - (monitor (-> (-> (prompt-tag/c (-> (flat (λ (x : Num) (number? x))) - (flat (λ (x : Num) (number? x)))) - (flat (λ (x : Num) (number? x))) - (→ Num Num) Num) - (flat (λ (x : Num) (number? x)))) - (flat (λ (x : Num) (number? x)))) - (λ (f : (→ (Prompt (→ Num Num) Num) Num)) - (% (f pt) - pt - (λ (f : (→ Num Num)) (f 1)))) - "A" - "B" - "con1"))]) - (let ([(do-prompt-2 : (→ (→ (Prompt (→ Num Num) Num) Num) Num)) - (monitor (-> (-> (prompt-tag/c (-> (flat (λ (x : Num) (zero? x))) - (flat (λ (x : Num) (number? x)))) - (flat (λ (x : Num) (number? x))) - (→ Num Num) Num) - (flat (λ (x : Num) (number? x)))) - (flat (λ (x : Num) (number? x)))) - (λ (f : (→ (Prompt (→ Num Num) Num) Num)) - (do-prompt f)) - "B" - "C" - "con2")]) - (do-prompt-2 - (λ (pt : (Prompt (→ Num Num) Num)) - (abort Num pt (λ (v : Num) (+ v 1)))))))) - (term (ctc-error "B" "con2"))) - - #| - ;; from random test generation - (do-test - (term (boolean? - (abort (monitor - (prompt-tag/c (-> (flat (λ (H) (error))) - (flat (λ (R) (error))))) - (prompt-tag v) - "pos" - "neg") - (make-prompt-tag)))) - (term (error))) - |# - ) - -;; tests for bugs found by random generation -(module+ test - - (test-equal - (term (subst (make-cm-key Bool) x 5)) - (term (make-cm-key Bool))) - - (test-equal - (term (subst (null Bool) x 5)) - (term (null Bool))) - - (test-equal - (abort-eval (term (ccm (make-cm-key Bool) Bool))) - 'null) - - (test-equal - (abort-eval (term (μ (B : Num) B))) - 'non-terminating) - - (test-equal - (abort-eval (term unit)) - 'unit) - - (test-equal - (abort-eval - (term (call/comp - (λ (Dp : (→ (Mark Bool) Num)) (make-cm-key Bool)) - (make-prompt-tag (Mark (Con Num)) Num)))) - 'missing-prompt) - - (test-equal - (term (no-match (call/comp - (λ (K : (→ (Prompt (Mark Num) Bool) - (List (Prompt Bool Unit)))) - (make-prompt-tag (Mark Num) Bool)) - (wcm · hole)) tag)) - #t) - - (test-equal - (abort-eval - (term (abort - Num - (make-prompt-tag Bool (List (Mark Bool))) - (boolean? 2)))) - 'missing-prompt) - - (test-equal - (term (marks (call/cm hole (+ 1 2) 1) key1 (null (→ (Mark Num) Num)))) - (term (null (→ (Mark Num) Num)))) - - (test-equal - (term - (marks (if (boolean? hole) 1 2) key (null (→ Num (Mark Unit))))) - (term (null (→ Num (Mark Unit))))) - - (test-equal - (term - (no-match (call/cm key (wcm · hole) - ((wcm · (λ (C : Bool) #f)) (unit? 3))) - tag)) - #t) - - (test-equal - (abort-eval - (term - (number? - (μ - (i : Num) - (- - (+ (case - (null (Con (Con Bool))) - (null = 1) - ((cons X u) = 2)) (if #t 0 0)) - i))))) - 'non-terminating) - - (test-equal - (judgment-holds - (tc - · - (tag2 - : - (Prompt (Mark (Prompt Unit Num)) (Prompt (→ Num Unit) (Con Bool))) - (tag1 - : - (Prompt Num (→ (→ Unit Unit) (Con Unit))) - (tag - : - (Prompt - (→ (Prompt Num Unit) (→ Bool Unit)) - (Prompt Num (→ (→ Unit Unit) (Con Unit)))) - ·))) - (abort - (→ Num (→ Num Num)) - tag1 - (wcm - · - (call/comp - (λ (Sa : (→ Num (Prompt (→ Num Unit) (Con Bool)))) 0) - tag2))) - t) - t) - '((→ Num (→ Num Num)))) - - (test-equal - (judgment-holds - (tc - · - (tag1 - : - (Prompt Bool (List Num)) - (key1 - : - (Mark Bool) - (tag - : - (Prompt Unit (Mark (List (Mark Unit)))) - (key : (Mark (Prompt Unit (Mark (List (Mark Unit))))) ·)))) - (wcm - ((key - (PG - (flat (λ (G : Unit) #t)) - (mark/c - (list/c (mark/c (flat (λ (b : Unit) #t)) Unit)) - (List (Mark Unit))) - tag - "B" - "iF" - "CgXohMerymUWF")) - ·) - (monitor - (flat (λ (Mk : Unit) #t)) - (abort Unit tag1 #t) - "fO" - "clRmiOfXGo" - "jxeinueLyNmLozqsKl")) - t) - t) - '(Unit)) - - (test-equal - (judgment-holds - (tc · (key : (Mark (Mark (Mark Num))) ·) - (MG - (mark/c (mark/c (flat (λ (r : Num) #f)) Num) (Mark Num)) - key - "EVYdYcpulOg" - "G" - "BjUOkycjoz") - t) - t) - '((Mark (Mark (Mark Num))))) - - ) (define (random-exp depth) (match diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-3.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-3.rkt index 234b784deb..2524d0e34f 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-3.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-3.rkt @@ -2,8 +2,7 @@ (define the-error "the function argument to call/comp has the wrong type") -(require redex/reduction-semantics - (for-syntax syntax/parse)) +(require redex/reduction-semantics) (provide (all-defined-out)) @@ -324,11 +323,6 @@ [(not-wcm (in-hole E (wcm w hole))) #f] [(not-wcm E) #t]) -(module+ test - (check-false (term (not-wcm (wcm · hole)))) - (check-false (term (not-wcm (+ 5 (wcm · hole))))) - (check-true (term (not-wcm hole))) - (check-true (term (not-wcm (abort Num hole 5))))) ;; wcm merging, second takes precedence (define-metafunction abort-lang @@ -554,42 +548,6 @@ [(different any_1 any_1) #f] [(different any_1 any_2) #t]) -(module+ test - (judgment-holds - (tc · · (+ 1 2) t) - t) - (judgment-holds - (tc · · ((λ (x : Num) (+ x 5)) 3) t) - t) - (judgment-holds - (tc · · (if (zero? 0) #t #f) t) - t) - (judgment-holds - (tc · · - ((λ (pt : (Prompt Num Num)) - (* (% (+ 1 (abort Num pt 5)) - pt - (λ (x : Num) (+ x 5))) - 3)) - (make-prompt-tag Num Num)) - t) - t) - (judgment-holds - (tc · · (flat (λ (x : Num) (zero? x))) t) - t) - (judgment-holds - (tc · - (tag0 : (Prompt Num Num) ·) - (monitor (prompt-tag/c - (flat (λ (x : Num) (zero? x))) - (flat (λ (x : Num) (zero? x))) - Num Num) - tag0 - "pos" - "neg" - "con") - t) - t)) ;; encoding for the paper (define-metafunction abort-lang @@ -774,29 +732,6 @@ (same-prompt-tag? pt_1 pt_2)] [(same-prompt-tag? tag_1 tag_2) #f]) -(module+ test - (test-equal - (term (no-match (wcm ((key_0 0) ·) hole) tag_0)) - #t) - (test-equal - (term (no-match (wcm · hole) tag_0)) - #t) - (test-equal - (term (no-match (abort Bool #t hole) tag_0)) - #t) - (test-equal (term (no-match hole tag_0)) #t) - (test-equal - (term (no-match (% hole - tag_0 - (λ (x : Num) (+ x 2))) - tag_0)) - #f) - (test-equal - (term (no-match (% hole - tag_0 - (λ (x : Num) (+ x 2))) - tag_1)) - #t)) ;; for continuation marks (define-metafunction abort-lang @@ -887,557 +822,7 @@ (term (no-match E_pt pt))) e))) -;;(current-traced-metafunctions 'all) -;; evaluation tests -(module+ test - (require rackunit) - (check-equal? (abort-eval (term (+ 1 2))) - 3) - (check-equal? (abort-eval (term (λ (x : Num) #t))) - 'procedure) - (check-equal? (abort-eval (term (make-prompt-tag Num Bool))) - 'prompt-tag)) - -;; helper for tests -(define-syntax (do-test stx) - (syntax-parse stx - [(_ ?input ?expected) - #'(do-test ?input ?expected - #:init-store (term ·) - #:store-type ·)] - [(_ ?input ?expected #:init-store ?store #:store-type ?store-type) - #'(begin - (check-true (judgment-holds (tc · ?store-type ,?input t))) - (check-equal? (abort-eval ?input #:init-store ?store) - ?expected))])) - -;; eval and type checking tests -(module+ test - ;; recursion - (do-test - (term ((μ (f : (→ Num Num)) - (λ (n : Num) - (if (zero? n) - 1 - (* n (f (- n 1)))))) - 5)) - (term 120)) - - ;; list recursion - (do-test - (term ((μ (f : (→ (List Num) Num)) - (λ (lst : (List Num)) - (case lst - (null = 0) - ((cons x1 x2) = - (+ x1 (f x2)))))) - (cons 5 (cons 6 (null Num))))) - (term 11)) - - ;; list contract - (do-test - (term (monitor (list/c (flat (λ (x : Num) (zero? x)))) - (cons 0 (cons 6 (null Num))) - "pos" "neg" "con")) - (term (ctc-error "pos" "con"))) - - ;; no control effect - (do-test - (term (% 5 (make-prompt-tag Num Num) (λ (x : Num) x))) - (term 5)) - - ;; test basic abort & handle - (do-test - (term (let ([(pt : (Prompt Num Num)) - (make-prompt-tag Num Num)]) - (% (abort Num pt 5) - pt - (λ (x : Num) (+ x 1))))) - (term 6)) - - ;; abort past a prompt - (do-test - (term (let ([(pt : (Prompt Num Num)) - (make-prompt-tag Num Num)]) - (% (% (abort Num pt 5) - (make-prompt-tag Num Num) - (λ (x : Num) (+ x 2))) - pt - (λ (x : Num) (+ x 1))))) - (term 6)) - - ;; abort to innermost prompt - (do-test - (term (let ([(pt : (Prompt Num Num)) - (make-prompt-tag Num Num)]) - (% (% (abort Num pt 5) - pt - (λ (x : Num) (+ x 2))) - pt - (λ (x : Num) (+ x 1))))) - (term 7)) - - ;; composable continuations - (do-test - (term (let ([(pt : (Prompt Num Num)) - (make-prompt-tag Num Num)]) - (% (+ 1 (call/comp - (λ (kont : (→ Num Num)) - (+ (kont 3) (kont 5))) - pt)) - pt - (λ (x : Num) x)))) - (term 11)) - - (do-test - (term (let ([(pt : (Prompt (→ Unit Num) Num)) - (make-prompt-tag (→ Unit Num) Num)]) - (% (+ 1 (call/comp - (λ (kont : (→ Num Num)) - (abort Num pt - (λ (x : Unit) - (+ (kont 3) (kont 5))))) - pt)) - pt - (λ (kont : (→ Unit Num)) (kont unit))))) - (term 10)) - - ;; call/cc encoding - (do-test - (term (let ([(pt : (Prompt (→ Unit Num) Num)) - (make-prompt-tag (→ Unit Num) Num)]) - (% (+ 1 (call/cc - (λ (kont : (→ Num Num)) - (+ (kont 3) (kont 5))) - pt)) - pt - (λ (kont : (→ Unit Num)) (kont unit))))) - (term 4)) - - ;; handler destroys call/cc semantics - (do-test - (term (let ([(pt : (Prompt (→ Unit Num) Num)) - (make-prompt-tag (→ Unit Num) Num)]) - (% (+ 1 (call/cc - (λ (kont : (→ Num Num)) - (+ (kont 3) (kont 5))) - pt)) - pt - (λ (kont : (→ Unit Num)) 18)))) - (term 18)) - - ;; continuation marks - (do-test - (term (let ([(mk : (Mark Num)) - (make-cm-key Num)]) - (call/cm - mk 5 - (ccm mk Num)))) - (term (cons 5 (null Num)))) - - (do-test - (term (let ([(mk : (Mark Num)) - (make-cm-key Num)]) - (call/cm - mk 5 - (call/cm - mk 7 - (ccm mk Num))))) - (term (cons 7 (null Num)))) - - ;; make sure wcms merge in weird cases - (do-test - (term ((λ (f : (→ Unit (List Num))) - (wcm ((key0 5) ·) (f unit))) - (λ (x : Unit) - (wcm ((key0 3) ·) (ccm key0 Num))))) - (term (cons 3 (null Num))) - #:init-store (term (key0 : (Mark Num) ·)) - #:store-type (key0 : (Mark Num) ·)) - - ;; continuation mark contracts - (do-test - (term (let ([(mk : (Mark Num)) - (monitor (mark/c (flat (λ (x : Num) (zero? x))) Num) - (make-cm-key Num) - "pos" - "neg" - "con")]) - (call/cm - mk 5 - (ccm mk Num)))) - (term (ctc-error "neg" "con"))) - - (do-test - (term (let ([(mk : (Mark Num)) - (monitor (mark/c (flat (λ (x : Num) (zero? x))) Num) - (make-cm-key Num) - "pos" - "neg" - "con")]) - (call/cm - mk 0 - (ccm mk Num)))) - (term (cons 0 (null Num)))) - - ;; naive contract - (do-test - (term (let ([(pt : (Prompt Num Num)) - (make-prompt-tag Num Num)]) - (% (monitor (flat (λ (x : Num) (number? x))) - (abort Num pt 5) - "pos" - "neg" - "con") - pt - (λ (x : Num) (+ x 1))))) - (term 6)) - - ;; first-order checks - (do-test - (term (monitor (flat (λ (x : Num) (zero? x))) - 5 - "server" - "client" - "con")) - (term (ctc-error "server" "con"))) - - ;; prompt & abort in the same component, the tag elsewhere - (do-test - (term (let ([(pt : (Prompt Num Num)) - (monitor (prompt-tag/c (flat (λ (x : Num) (zero? x))) - (flat (λ (x : Num) (zero? x))) - Num Num) - (make-prompt-tag Num Num) - "server" - "client" - "con")]) - (% (abort Num pt 3) - pt - (λ (x : Num) (+ x 1))))) - (term (ctc-error "client" "con"))) - - ;; call/comp issue - (do-test - (term (let ([(pt : (Prompt Num Num)) - (monitor (prompt-tag/c (flat (λ (x : Num) (zero? x))) - (flat (λ (x : Num) (zero? x))) - Num Num) - (make-prompt-tag Num Num) - "server" - "client" - "con")]) - (% (+ 1 - (call/comp - (λ (k : (→ Num Num)) - (k 0)) - pt)) - pt - (λ (x : Num) (+ x 1))))) - (term (ctc-error "client" "con"))) - - ;; blame even on one side - (do-test - (term (let ([(pt1 : (Prompt Num Num)) - (make-prompt-tag Num Num)]) - (let ([(pt2 : (Prompt Num Num)) - (monitor (prompt-tag/c (flat (λ (x : Num) (zero? x))) - (flat (λ (x : Num) (zero? (- x 5)))) - Num Num) - pt1 - "client" - "server" - "con")]) - (% (+ 1 ; doesn't add to 5 - (call/comp - (λ (k : (→ Num Num)) - (k 3)) - pt1)) - pt2 - (λ (x : Num) (+ x 1)))))) - (term (ctc-error "server" "con"))) - - ;; blame even on other side - (do-test - (term (let ([(pt1 : (Prompt Num Num)) - (make-prompt-tag Num Num)]) - (let ([(pt2 : (Prompt Num Num)) - (monitor (prompt-tag/c (flat (λ (x : Num) (zero? x))) - (flat (λ (x : Num) (zero? (- x 5)))) - Num Num) - pt1 - "server" - "client" - "con")]) - (% (+ 1 ; doesn't add to 5 - (call/comp - (λ (k : (→ Num Num)) - (k 3)) - pt2)) - pt1 - (λ (x : Num) (+ x 1)))))) - (term (ctc-error "server" "con"))) - - ;; same with ho-contract - (do-test - (term (let ([(pt : (Prompt (→ Num Num) Num)) - (monitor (prompt-tag/c (-> (flat (λ (x : Num) (zero? x))) - (flat (λ (x : Num) (number? x)))) - (flat (λ (x : Num) (number? x))) - (→ Num Num) Num) - (make-prompt-tag (→ Num Num) Num) - "server" - "client" - "con")]) - (% (abort Num pt (λ (x : Num) 5)) - pt - (λ (x : (→ Num Num)) (x 8))))) - (term (ctc-error "client" "con"))) - - ;; again, but from other side - (do-test - (term (let ([(pt : (Prompt (→ Num Num) Num)) - (monitor (prompt-tag/c (-> (flat (λ (x : Num) (zero? x))) - (flat (λ (x : Num) (zero? x)))) - (flat (λ (x : Num) (zero? x))) - (→ Num Num) Num) - (make-prompt-tag (→ Num Num) Num) - "server" - "client" - "con")]) - (% (abort Num pt (λ (x : Num) 3)) - pt - (λ (f : (→ Num Num)) (f 0))))) - (term (ctc-error "client" "con"))) - - ;; abort across boundary w/ ho-value - (do-test - (term (let ([(do-prompt : (→ (→ (Prompt (→ Num Num) Num) Num) Num)) - (let ([(pt : (Prompt (→ Num Num) Num)) - (make-prompt-tag (→ Num Num) Num)]) - (monitor (-> (-> (prompt-tag/c (-> (flat (λ (x : Num) (zero? x))) - (flat (λ (x : Num) (zero? x)))) - (flat (λ (x : Num) (zero? x))) - (→ Num Num) Num) - (flat (λ (x : Num) (number? x)))) - (flat (λ (x : Num) (number? x)))) - (λ (f : (→ (Prompt (→ Num Num) Num) Num)) - (% (f pt) - pt - (λ (f : (→ Num Num)) (f 5)))) - "server" - "client" - "con"))]) - (do-prompt - (λ (pt : (Prompt (→ Num Num) Num)) - (abort Num pt (λ (v : Num) (+ v 1))))))) - (term (ctc-error "server" "con"))) ;; MF: nice example but in a paper presentation you need to simplify - - ;; where the prompt flows across multiple boundaries - (do-test - (term (let ([(do-prompt : (→ (→ (Prompt (→ Num Num) Num) Num) Num)) - (let ([(pt : (Prompt (→ Num Num) Num)) - (make-prompt-tag (→ Num Num) Num)]) - (monitor (-> (-> (prompt-tag/c (-> (flat (λ (x : Num) (number? x))) - (flat (λ (x : Num) (number? x)))) - (flat (λ (x : Num) (number? x))) - (→ Num Num) Num) - (flat (λ (x : Num) (number? x)))) - (flat (λ (x : Num) (number? x)))) - (λ (f : (→ (Prompt (→ Num Num) Num) Num)) - (% (f pt) - pt - (λ (f : (→ Num Num)) (f 1)))) - "A" - "B" - "con1"))]) - (let ([(do-prompt-2 : (→ (→ (Prompt (→ Num Num) Num) Num) Num)) - (monitor (-> (-> (prompt-tag/c (-> (flat (λ (x : Num) (zero? x))) - (flat (λ (x : Num) (number? x)))) - (flat (λ (x : Num) (number? x))) - (→ Num Num) Num) - (flat (λ (x : Num) (number? x)))) - (flat (λ (x : Num) (number? x)))) - (λ (f : (→ (Prompt (→ Num Num) Num) Num)) - (do-prompt f)) - "B" - "C" - "con2")]) - (do-prompt-2 - (λ (pt : (Prompt (→ Num Num) Num)) - (abort Num pt (λ (v : Num) (+ v 1)))))))) - (term (ctc-error "B" "con2"))) - - #| - ;; from random test generation - (do-test - (term (boolean? - (abort (monitor - (prompt-tag/c (-> (flat (λ (H) (error))) - (flat (λ (R) (error))))) - (prompt-tag v) - "pos" - "neg") - (make-prompt-tag)))) - (term (error))) - |# - ) - -;; tests for bugs found by random generation -(module+ test - - (test-equal - (term (subst (make-cm-key Bool) x 5)) - (term (make-cm-key Bool))) - - (test-equal - (term (subst (null Bool) x 5)) - (term (null Bool))) - - (test-equal - (abort-eval (term (ccm (make-cm-key Bool) Bool))) - 'null) - - (test-equal - (abort-eval (term (μ (B : Num) B))) - 'non-terminating) - - (test-equal - (abort-eval (term unit)) - 'unit) - - (test-equal - (abort-eval - (term (call/comp - (λ (Dp : (→ (Mark Bool) Num)) (make-cm-key Bool)) - (make-prompt-tag (Mark (Con Num)) Num)))) - 'missing-prompt) - - (test-equal - (term (no-match (call/comp - (λ (K : (→ (Prompt (Mark Num) Bool) - (List (Prompt Bool Unit)))) - (make-prompt-tag (Mark Num) Bool)) - (wcm · hole)) tag)) - #t) - - (test-equal - (abort-eval - (term (abort - Num - (make-prompt-tag Bool (List (Mark Bool))) - (boolean? 2)))) - 'missing-prompt) - - (test-equal - (term (marks (call/cm hole (+ 1 2) 1) key1 (null (→ (Mark Num) Num)))) - (term (null (→ (Mark Num) Num)))) - - (test-equal - (term - (marks (if (boolean? hole) 1 2) key (null (→ Num (Mark Unit))))) - (term (null (→ Num (Mark Unit))))) - - (test-equal - (term - (no-match (call/cm key (wcm · hole) - ((wcm · (λ (C : Bool) #f)) (unit? 3))) - tag)) - #t) - - (test-equal - (abort-eval - (term - (number? - (μ - (i : Num) - (- - (+ (case - (null (Con (Con Bool))) - (null = 1) - ((cons X u) = 2)) (if #t 0 0)) - i))))) - 'non-terminating) - - (test-equal - (judgment-holds - (tc - · - (tag2 - : - (Prompt (Mark (Prompt Unit Num)) (Prompt (→ Num Unit) (Con Bool))) - (tag1 - : - (Prompt Num (→ (→ Unit Unit) (Con Unit))) - (tag - : - (Prompt - (→ (Prompt Num Unit) (→ Bool Unit)) - (Prompt Num (→ (→ Unit Unit) (Con Unit)))) - ·))) - (abort - (→ Num (→ Num Num)) - tag1 - (wcm - · - (call/comp - (λ (Sa : (→ Num (Prompt (→ Num Unit) (Con Bool)))) 0) - tag2))) - t) - t) - '((→ Num (→ Num Num)))) - - (test-equal - (judgment-holds - (tc - · - (tag1 - : - (Prompt Bool (List Num)) - (key1 - : - (Mark Bool) - (tag - : - (Prompt Unit (Mark (List (Mark Unit)))) - (key : (Mark (Prompt Unit (Mark (List (Mark Unit))))) ·)))) - (wcm - ((key - (PG - (flat (λ (G : Unit) #t)) - (mark/c - (list/c (mark/c (flat (λ (b : Unit) #t)) Unit)) - (List (Mark Unit))) - tag - "B" - "iF" - "CgXohMerymUWF")) - ·) - (monitor - (flat (λ (Mk : Unit) #t)) - (abort Unit tag1 #t) - "fO" - "clRmiOfXGo" - "jxeinueLyNmLozqsKl")) - t) - t) - '(Unit)) - - (test-equal - (judgment-holds - (tc · (key : (Mark (Mark (Mark Num))) ·) - (MG - (mark/c (mark/c (flat (λ (r : Num) #f)) Num) (Mark Num)) - key - "EVYdYcpulOg" - "G" - "BjUOkycjoz") - t) - t) - '((Mark (Mark (Mark Num))))) - - ) (define (random-exp depth) (match diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-base.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-base.rkt index 6c548c9624..41d814bd90 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-base.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-base.rkt @@ -2,8 +2,7 @@ (define the-error "no-error") -(require redex/reduction-semantics - (for-syntax syntax/parse)) +(require redex/reduction-semantics) (provide (all-defined-out)) @@ -324,12 +323,6 @@ [(not-wcm (in-hole E (wcm w hole))) #f] [(not-wcm E) #t]) -(module+ test - (check-false (term (not-wcm (wcm · hole)))) - (check-false (term (not-wcm (+ 5 (wcm · hole))))) - (check-true (term (not-wcm hole))) - (check-true (term (not-wcm (abort Num hole 5))))) - ;; wcm merging, second takes precedence (define-metafunction abort-lang merge : w w -> w @@ -554,42 +547,6 @@ [(different any_1 any_1) #f] [(different any_1 any_2) #t]) -(module+ test - (judgment-holds - (tc · · (+ 1 2) t) - t) - (judgment-holds - (tc · · ((λ (x : Num) (+ x 5)) 3) t) - t) - (judgment-holds - (tc · · (if (zero? 0) #t #f) t) - t) - (judgment-holds - (tc · · - ((λ (pt : (Prompt Num Num)) - (* (% (+ 1 (abort Num pt 5)) - pt - (λ (x : Num) (+ x 5))) - 3)) - (make-prompt-tag Num Num)) - t) - t) - (judgment-holds - (tc · · (flat (λ (x : Num) (zero? x))) t) - t) - (judgment-holds - (tc · - (tag0 : (Prompt Num Num) ·) - (monitor (prompt-tag/c - (flat (λ (x : Num) (zero? x))) - (flat (λ (x : Num) (zero? x))) - Num Num) - tag0 - "pos" - "neg" - "con") - t) - t)) ;; encoding for the paper (define-metafunction abort-lang @@ -774,29 +731,6 @@ (same-prompt-tag? pt_1 pt_2)] [(same-prompt-tag? tag_1 tag_2) #f]) -(module+ test - (test-equal - (term (no-match (wcm ((key_0 0) ·) hole) tag_0)) - #t) - (test-equal - (term (no-match (wcm · hole) tag_0)) - #t) - (test-equal - (term (no-match (abort Bool #t hole) tag_0)) - #t) - (test-equal (term (no-match hole tag_0)) #t) - (test-equal - (term (no-match (% hole - tag_0 - (λ (x : Num) (+ x 2))) - tag_0)) - #f) - (test-equal - (term (no-match (% hole - tag_0 - (λ (x : Num) (+ x 2))) - tag_1)) - #t)) ;; for continuation marks (define-metafunction abort-lang @@ -887,557 +821,7 @@ (term (no-match E_pt pt))) e))) -;;(current-traced-metafunctions 'all) -;; evaluation tests -(module+ test - (require rackunit) - (check-equal? (abort-eval (term (+ 1 2))) - 3) - (check-equal? (abort-eval (term (λ (x : Num) #t))) - 'procedure) - (check-equal? (abort-eval (term (make-prompt-tag Num Bool))) - 'prompt-tag)) - -;; helper for tests -(define-syntax (do-test stx) - (syntax-parse stx - [(_ ?input ?expected) - #'(do-test ?input ?expected - #:init-store (term ·) - #:store-type ·)] - [(_ ?input ?expected #:init-store ?store #:store-type ?store-type) - #'(begin - (check-true (judgment-holds (tc · ?store-type ,?input t))) - (check-equal? (abort-eval ?input #:init-store ?store) - ?expected))])) - -;; eval and type checking tests -(module+ test - ;; recursion - (do-test - (term ((μ (f : (→ Num Num)) - (λ (n : Num) - (if (zero? n) - 1 - (* n (f (- n 1)))))) - 5)) - (term 120)) - - ;; list recursion - (do-test - (term ((μ (f : (→ (List Num) Num)) - (λ (lst : (List Num)) - (case lst - (null = 0) - ((cons x1 x2) = - (+ x1 (f x2)))))) - (cons 5 (cons 6 (null Num))))) - (term 11)) - - ;; list contract - (do-test - (term (monitor (list/c (flat (λ (x : Num) (zero? x)))) - (cons 0 (cons 6 (null Num))) - "pos" "neg" "con")) - (term (ctc-error "pos" "con"))) - - ;; no control effect - (do-test - (term (% 5 (make-prompt-tag Num Num) (λ (x : Num) x))) - (term 5)) - - ;; test basic abort & handle - (do-test - (term (let ([(pt : (Prompt Num Num)) - (make-prompt-tag Num Num)]) - (% (abort Num pt 5) - pt - (λ (x : Num) (+ x 1))))) - (term 6)) - - ;; abort past a prompt - (do-test - (term (let ([(pt : (Prompt Num Num)) - (make-prompt-tag Num Num)]) - (% (% (abort Num pt 5) - (make-prompt-tag Num Num) - (λ (x : Num) (+ x 2))) - pt - (λ (x : Num) (+ x 1))))) - (term 6)) - - ;; abort to innermost prompt - (do-test - (term (let ([(pt : (Prompt Num Num)) - (make-prompt-tag Num Num)]) - (% (% (abort Num pt 5) - pt - (λ (x : Num) (+ x 2))) - pt - (λ (x : Num) (+ x 1))))) - (term 7)) - - ;; composable continuations - (do-test - (term (let ([(pt : (Prompt Num Num)) - (make-prompt-tag Num Num)]) - (% (+ 1 (call/comp - (λ (kont : (→ Num Num)) - (+ (kont 3) (kont 5))) - pt)) - pt - (λ (x : Num) x)))) - (term 11)) - - (do-test - (term (let ([(pt : (Prompt (→ Unit Num) Num)) - (make-prompt-tag (→ Unit Num) Num)]) - (% (+ 1 (call/comp - (λ (kont : (→ Num Num)) - (abort Num pt - (λ (x : Unit) - (+ (kont 3) (kont 5))))) - pt)) - pt - (λ (kont : (→ Unit Num)) (kont unit))))) - (term 10)) - - ;; call/cc encoding - (do-test - (term (let ([(pt : (Prompt (→ Unit Num) Num)) - (make-prompt-tag (→ Unit Num) Num)]) - (% (+ 1 (call/cc - (λ (kont : (→ Num Num)) - (+ (kont 3) (kont 5))) - pt)) - pt - (λ (kont : (→ Unit Num)) (kont unit))))) - (term 4)) - - ;; handler destroys call/cc semantics - (do-test - (term (let ([(pt : (Prompt (→ Unit Num) Num)) - (make-prompt-tag (→ Unit Num) Num)]) - (% (+ 1 (call/cc - (λ (kont : (→ Num Num)) - (+ (kont 3) (kont 5))) - pt)) - pt - (λ (kont : (→ Unit Num)) 18)))) - (term 18)) - - ;; continuation marks - (do-test - (term (let ([(mk : (Mark Num)) - (make-cm-key Num)]) - (call/cm - mk 5 - (ccm mk Num)))) - (term (cons 5 (null Num)))) - - (do-test - (term (let ([(mk : (Mark Num)) - (make-cm-key Num)]) - (call/cm - mk 5 - (call/cm - mk 7 - (ccm mk Num))))) - (term (cons 7 (null Num)))) - - ;; make sure wcms merge in weird cases - (do-test - (term ((λ (f : (→ Unit (List Num))) - (wcm ((key0 5) ·) (f unit))) - (λ (x : Unit) - (wcm ((key0 3) ·) (ccm key0 Num))))) - (term (cons 3 (null Num))) - #:init-store (term (key0 : (Mark Num) ·)) - #:store-type (key0 : (Mark Num) ·)) - - ;; continuation mark contracts - (do-test - (term (let ([(mk : (Mark Num)) - (monitor (mark/c (flat (λ (x : Num) (zero? x))) Num) - (make-cm-key Num) - "pos" - "neg" - "con")]) - (call/cm - mk 5 - (ccm mk Num)))) - (term (ctc-error "neg" "con"))) - - (do-test - (term (let ([(mk : (Mark Num)) - (monitor (mark/c (flat (λ (x : Num) (zero? x))) Num) - (make-cm-key Num) - "pos" - "neg" - "con")]) - (call/cm - mk 0 - (ccm mk Num)))) - (term (cons 0 (null Num)))) - - ;; naive contract - (do-test - (term (let ([(pt : (Prompt Num Num)) - (make-prompt-tag Num Num)]) - (% (monitor (flat (λ (x : Num) (number? x))) - (abort Num pt 5) - "pos" - "neg" - "con") - pt - (λ (x : Num) (+ x 1))))) - (term 6)) - - ;; first-order checks - (do-test - (term (monitor (flat (λ (x : Num) (zero? x))) - 5 - "server" - "client" - "con")) - (term (ctc-error "server" "con"))) - - ;; prompt & abort in the same component, the tag elsewhere - (do-test - (term (let ([(pt : (Prompt Num Num)) - (monitor (prompt-tag/c (flat (λ (x : Num) (zero? x))) - (flat (λ (x : Num) (zero? x))) - Num Num) - (make-prompt-tag Num Num) - "server" - "client" - "con")]) - (% (abort Num pt 3) - pt - (λ (x : Num) (+ x 1))))) - (term (ctc-error "client" "con"))) - - ;; call/comp issue - (do-test - (term (let ([(pt : (Prompt Num Num)) - (monitor (prompt-tag/c (flat (λ (x : Num) (zero? x))) - (flat (λ (x : Num) (zero? x))) - Num Num) - (make-prompt-tag Num Num) - "server" - "client" - "con")]) - (% (+ 1 - (call/comp - (λ (k : (→ Num Num)) - (k 0)) - pt)) - pt - (λ (x : Num) (+ x 1))))) - (term (ctc-error "client" "con"))) - - ;; blame even on one side - (do-test - (term (let ([(pt1 : (Prompt Num Num)) - (make-prompt-tag Num Num)]) - (let ([(pt2 : (Prompt Num Num)) - (monitor (prompt-tag/c (flat (λ (x : Num) (zero? x))) - (flat (λ (x : Num) (zero? (- x 5)))) - Num Num) - pt1 - "client" - "server" - "con")]) - (% (+ 1 ; doesn't add to 5 - (call/comp - (λ (k : (→ Num Num)) - (k 3)) - pt1)) - pt2 - (λ (x : Num) (+ x 1)))))) - (term (ctc-error "server" "con"))) - - ;; blame even on other side - (do-test - (term (let ([(pt1 : (Prompt Num Num)) - (make-prompt-tag Num Num)]) - (let ([(pt2 : (Prompt Num Num)) - (monitor (prompt-tag/c (flat (λ (x : Num) (zero? x))) - (flat (λ (x : Num) (zero? (- x 5)))) - Num Num) - pt1 - "server" - "client" - "con")]) - (% (+ 1 ; doesn't add to 5 - (call/comp - (λ (k : (→ Num Num)) - (k 3)) - pt2)) - pt1 - (λ (x : Num) (+ x 1)))))) - (term (ctc-error "server" "con"))) - - ;; same with ho-contract - (do-test - (term (let ([(pt : (Prompt (→ Num Num) Num)) - (monitor (prompt-tag/c (-> (flat (λ (x : Num) (zero? x))) - (flat (λ (x : Num) (number? x)))) - (flat (λ (x : Num) (number? x))) - (→ Num Num) Num) - (make-prompt-tag (→ Num Num) Num) - "server" - "client" - "con")]) - (% (abort Num pt (λ (x : Num) 5)) - pt - (λ (x : (→ Num Num)) (x 8))))) - (term (ctc-error "client" "con"))) - - ;; again, but from other side - (do-test - (term (let ([(pt : (Prompt (→ Num Num) Num)) - (monitor (prompt-tag/c (-> (flat (λ (x : Num) (zero? x))) - (flat (λ (x : Num) (zero? x)))) - (flat (λ (x : Num) (zero? x))) - (→ Num Num) Num) - (make-prompt-tag (→ Num Num) Num) - "server" - "client" - "con")]) - (% (abort Num pt (λ (x : Num) 3)) - pt - (λ (f : (→ Num Num)) (f 0))))) - (term (ctc-error "client" "con"))) - - ;; abort across boundary w/ ho-value - (do-test - (term (let ([(do-prompt : (→ (→ (Prompt (→ Num Num) Num) Num) Num)) - (let ([(pt : (Prompt (→ Num Num) Num)) - (make-prompt-tag (→ Num Num) Num)]) - (monitor (-> (-> (prompt-tag/c (-> (flat (λ (x : Num) (zero? x))) - (flat (λ (x : Num) (zero? x)))) - (flat (λ (x : Num) (zero? x))) - (→ Num Num) Num) - (flat (λ (x : Num) (number? x)))) - (flat (λ (x : Num) (number? x)))) - (λ (f : (→ (Prompt (→ Num Num) Num) Num)) - (% (f pt) - pt - (λ (f : (→ Num Num)) (f 5)))) - "server" - "client" - "con"))]) - (do-prompt - (λ (pt : (Prompt (→ Num Num) Num)) - (abort Num pt (λ (v : Num) (+ v 1))))))) - (term (ctc-error "server" "con"))) ;; MF: nice example but in a paper presentation you need to simplify - - ;; where the prompt flows across multiple boundaries - (do-test - (term (let ([(do-prompt : (→ (→ (Prompt (→ Num Num) Num) Num) Num)) - (let ([(pt : (Prompt (→ Num Num) Num)) - (make-prompt-tag (→ Num Num) Num)]) - (monitor (-> (-> (prompt-tag/c (-> (flat (λ (x : Num) (number? x))) - (flat (λ (x : Num) (number? x)))) - (flat (λ (x : Num) (number? x))) - (→ Num Num) Num) - (flat (λ (x : Num) (number? x)))) - (flat (λ (x : Num) (number? x)))) - (λ (f : (→ (Prompt (→ Num Num) Num) Num)) - (% (f pt) - pt - (λ (f : (→ Num Num)) (f 1)))) - "A" - "B" - "con1"))]) - (let ([(do-prompt-2 : (→ (→ (Prompt (→ Num Num) Num) Num) Num)) - (monitor (-> (-> (prompt-tag/c (-> (flat (λ (x : Num) (zero? x))) - (flat (λ (x : Num) (number? x)))) - (flat (λ (x : Num) (number? x))) - (→ Num Num) Num) - (flat (λ (x : Num) (number? x)))) - (flat (λ (x : Num) (number? x)))) - (λ (f : (→ (Prompt (→ Num Num) Num) Num)) - (do-prompt f)) - "B" - "C" - "con2")]) - (do-prompt-2 - (λ (pt : (Prompt (→ Num Num) Num)) - (abort Num pt (λ (v : Num) (+ v 1)))))))) - (term (ctc-error "B" "con2"))) - - #| - ;; from random test generation - (do-test - (term (boolean? - (abort (monitor - (prompt-tag/c (-> (flat (λ (H) (error))) - (flat (λ (R) (error))))) - (prompt-tag v) - "pos" - "neg") - (make-prompt-tag)))) - (term (error))) - |# - ) - -;; tests for bugs found by random generation -(module+ test - - (test-equal - (term (subst (make-cm-key Bool) x 5)) - (term (make-cm-key Bool))) - - (test-equal - (term (subst (null Bool) x 5)) - (term (null Bool))) - - (test-equal - (abort-eval (term (ccm (make-cm-key Bool) Bool))) - 'null) - - (test-equal - (abort-eval (term (μ (B : Num) B))) - 'non-terminating) - - (test-equal - (abort-eval (term unit)) - 'unit) - - (test-equal - (abort-eval - (term (call/comp - (λ (Dp : (→ (Mark Bool) Num)) (make-cm-key Bool)) - (make-prompt-tag (Mark (Con Num)) Num)))) - 'missing-prompt) - - (test-equal - (term (no-match (call/comp - (λ (K : (→ (Prompt (Mark Num) Bool) - (List (Prompt Bool Unit)))) - (make-prompt-tag (Mark Num) Bool)) - (wcm · hole)) tag)) - #t) - - (test-equal - (abort-eval - (term (abort - Num - (make-prompt-tag Bool (List (Mark Bool))) - (boolean? 2)))) - 'missing-prompt) - - (test-equal - (term (marks (call/cm hole (+ 1 2) 1) key1 (null (→ (Mark Num) Num)))) - (term (null (→ (Mark Num) Num)))) - - (test-equal - (term - (marks (if (boolean? hole) 1 2) key (null (→ Num (Mark Unit))))) - (term (null (→ Num (Mark Unit))))) - - (test-equal - (term - (no-match (call/cm key (wcm · hole) - ((wcm · (λ (C : Bool) #f)) (unit? 3))) - tag)) - #t) - - (test-equal - (abort-eval - (term - (number? - (μ - (i : Num) - (- - (+ (case - (null (Con (Con Bool))) - (null = 1) - ((cons X u) = 2)) (if #t 0 0)) - i))))) - 'non-terminating) - - (test-equal - (judgment-holds - (tc - · - (tag2 - : - (Prompt (Mark (Prompt Unit Num)) (Prompt (→ Num Unit) (Con Bool))) - (tag1 - : - (Prompt Num (→ (→ Unit Unit) (Con Unit))) - (tag - : - (Prompt - (→ (Prompt Num Unit) (→ Bool Unit)) - (Prompt Num (→ (→ Unit Unit) (Con Unit)))) - ·))) - (abort - (→ Num (→ Num Num)) - tag1 - (wcm - · - (call/comp - (λ (Sa : (→ Num (Prompt (→ Num Unit) (Con Bool)))) 0) - tag2))) - t) - t) - '((→ Num (→ Num Num)))) - - (test-equal - (judgment-holds - (tc - · - (tag1 - : - (Prompt Bool (List Num)) - (key1 - : - (Mark Bool) - (tag - : - (Prompt Unit (Mark (List (Mark Unit)))) - (key : (Mark (Prompt Unit (Mark (List (Mark Unit))))) ·)))) - (wcm - ((key - (PG - (flat (λ (G : Unit) #t)) - (mark/c - (list/c (mark/c (flat (λ (b : Unit) #t)) Unit)) - (List (Mark Unit))) - tag - "B" - "iF" - "CgXohMerymUWF")) - ·) - (monitor - (flat (λ (Mk : Unit) #t)) - (abort Unit tag1 #t) - "fO" - "clRmiOfXGo" - "jxeinueLyNmLozqsKl")) - t) - t) - '(Unit)) - - (test-equal - (judgment-holds - (tc · (key : (Mark (Mark (Mark Num))) ·) - (MG - (mark/c (mark/c (flat (λ (r : Num) #f)) Num) (Mark Num)) - key - "EVYdYcpulOg" - "G" - "BjUOkycjoz") - t) - t) - '((Mark (Mark (Mark Num))))) - - ) (define (random-exp depth) (match @@ -1550,5 +934,3 @@ (define (type-check e) (judgment-holds (tc · · ,e t))) - - diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/test.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/test.rkt new file mode 100644 index 0000000000..d2ce689708 --- /dev/null +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/test.rkt @@ -0,0 +1,621 @@ +#lang racket + +(require redex/reduction-semantics + (for-syntax syntax/parse) + "delim-cont-base.rkt" + (only-in rackunit + check-equal? + check-false + check-true)) + +(judgment-holds + (tc · · (+ 1 2) t) + t) +(judgment-holds + (tc · · ((λ (x : Num) (+ x 5)) 3) t) + t) +(judgment-holds + (tc · · (if (zero? 0) #t #f) t) + t) +(judgment-holds + (tc · · + ((λ (pt : (Prompt Num Num)) + (* (% (+ 1 (abort Num pt 5)) + pt + (λ (x : Num) (+ x 5))) + 3)) + (make-prompt-tag Num Num)) + t) + t) +(judgment-holds + (tc · · (flat (λ (x : Num) (zero? x))) t) + t) +(judgment-holds + (tc · + (tag0 : (Prompt Num Num) ·) + (monitor (prompt-tag/c + (flat (λ (x : Num) (zero? x))) + (flat (λ (x : Num) (zero? x))) + Num Num) + tag0 + "pos" + "neg" + "con") + t) + t) + + +(test-equal + (term (no-match (wcm ((key_0 0) ·) hole) tag_0)) + #t) +(test-equal + (term (no-match (wcm · hole) tag_0)) + #t) +(test-equal + (term (no-match (abort Bool #t hole) tag_0)) + #t) +(test-equal (term (no-match hole tag_0)) #t) +(test-equal + (term (no-match (% hole + tag_0 + (λ (x : Num) (+ x 2))) + tag_0)) + #f) +(test-equal + (term (no-match (% hole + tag_0 + (λ (x : Num) (+ x 2))) + tag_1)) + #t) + +;; evaluation tests + +(check-equal? (abort-eval (term (+ 1 2))) + 3) +(check-equal? (abort-eval (term (λ (x : Num) #t))) + 'procedure) +(check-equal? (abort-eval (term (make-prompt-tag Num Bool))) + 'prompt-tag) + +;; helper for tests +(define-syntax (do-test stx) + (syntax-parse stx + [(_ ?input ?expected) + #'(do-test ?input ?expected + #:init-store (term ·) + #:store-type ·)] + [(_ ?input ?expected #:init-store ?store #:store-type ?store-type) + #'(begin + (check-true (judgment-holds (tc · ?store-type ,?input t))) + (check-equal? (abort-eval ?input #:init-store ?store) + ?expected))])) + +;; eval and type checking tests +;; recursion +(do-test + (term ((μ (f : (→ Num Num)) + (λ (n : Num) + (if (zero? n) + 1 + (* n (f (- n 1)))))) + 5)) + (term 120)) + +;; list recursion +(do-test + (term ((μ (f : (→ (List Num) Num)) + (λ (lst : (List Num)) + (case lst + (null = 0) + ((cons x1 x2) = + (+ x1 (f x2)))))) + (cons 5 (cons 6 (null Num))))) + (term 11)) + +;; list contract +(do-test + (term (monitor (list/c (flat (λ (x : Num) (zero? x)))) + (cons 0 (cons 6 (null Num))) + "pos" "neg" "con")) + (term (ctc-error "pos" "con"))) + +;; no control effect +(do-test + (term (% 5 (make-prompt-tag Num Num) (λ (x : Num) x))) + (term 5)) + +;; test basic abort & handle +(do-test + (term (let ([(pt : (Prompt Num Num)) + (make-prompt-tag Num Num)]) + (% (abort Num pt 5) + pt + (λ (x : Num) (+ x 1))))) + (term 6)) + +;; abort past a prompt +(do-test + (term (let ([(pt : (Prompt Num Num)) + (make-prompt-tag Num Num)]) + (% (% (abort Num pt 5) + (make-prompt-tag Num Num) + (λ (x : Num) (+ x 2))) + pt + (λ (x : Num) (+ x 1))))) + (term 6)) + +;; abort to innermost prompt +(do-test + (term (let ([(pt : (Prompt Num Num)) + (make-prompt-tag Num Num)]) + (% (% (abort Num pt 5) + pt + (λ (x : Num) (+ x 2))) + pt + (λ (x : Num) (+ x 1))))) + (term 7)) + +;; composable continuations +(do-test + (term (let ([(pt : (Prompt Num Num)) + (make-prompt-tag Num Num)]) + (% (+ 1 (call/comp + (λ (kont : (→ Num Num)) + (+ (kont 3) (kont 5))) + pt)) + pt + (λ (x : Num) x)))) + (term 11)) + +(do-test + (term (let ([(pt : (Prompt (→ Unit Num) Num)) + (make-prompt-tag (→ Unit Num) Num)]) + (% (+ 1 (call/comp + (λ (kont : (→ Num Num)) + (abort Num pt + (λ (x : Unit) + (+ (kont 3) (kont 5))))) + pt)) + pt + (λ (kont : (→ Unit Num)) (kont unit))))) + (term 10)) + +;; call/cc encoding +(do-test + (term (let ([(pt : (Prompt (→ Unit Num) Num)) + (make-prompt-tag (→ Unit Num) Num)]) + (% (+ 1 (call/cc + (λ (kont : (→ Num Num)) + (+ (kont 3) (kont 5))) + pt)) + pt + (λ (kont : (→ Unit Num)) (kont unit))))) + (term 4)) + +;; handler destroys call/cc semantics +(do-test + (term (let ([(pt : (Prompt (→ Unit Num) Num)) + (make-prompt-tag (→ Unit Num) Num)]) + (% (+ 1 (call/cc + (λ (kont : (→ Num Num)) + (+ (kont 3) (kont 5))) + pt)) + pt + (λ (kont : (→ Unit Num)) 18)))) + (term 18)) + +;; continuation marks +(do-test + (term (let ([(mk : (Mark Num)) + (make-cm-key Num)]) + (call/cm + mk 5 + (ccm mk Num)))) + (term (cons 5 (null Num)))) + +(do-test + (term (let ([(mk : (Mark Num)) + (make-cm-key Num)]) + (call/cm + mk 5 + (call/cm + mk 7 + (ccm mk Num))))) + (term (cons 7 (null Num)))) + +;; make sure wcms merge in weird cases +(do-test + (term ((λ (f : (→ Unit (List Num))) + (wcm ((key0 5) ·) (f unit))) + (λ (x : Unit) + (wcm ((key0 3) ·) (ccm key0 Num))))) + (term (cons 3 (null Num))) + #:init-store (term (key0 : (Mark Num) ·)) + #:store-type (key0 : (Mark Num) ·)) + +;; continuation mark contracts +(do-test + (term (let ([(mk : (Mark Num)) + (monitor (mark/c (flat (λ (x : Num) (zero? x))) Num) + (make-cm-key Num) + "pos" + "neg" + "con")]) + (call/cm + mk 5 + (ccm mk Num)))) + (term (ctc-error "neg" "con"))) + +(do-test + (term (let ([(mk : (Mark Num)) + (monitor (mark/c (flat (λ (x : Num) (zero? x))) Num) + (make-cm-key Num) + "pos" + "neg" + "con")]) + (call/cm + mk 0 + (ccm mk Num)))) + (term (cons 0 (null Num)))) + +;; naive contract +(do-test + (term (let ([(pt : (Prompt Num Num)) + (make-prompt-tag Num Num)]) + (% (monitor (flat (λ (x : Num) (number? x))) + (abort Num pt 5) + "pos" + "neg" + "con") + pt + (λ (x : Num) (+ x 1))))) + (term 6)) + +;; first-order checks +(do-test + (term (monitor (flat (λ (x : Num) (zero? x))) + 5 + "server" + "client" + "con")) + (term (ctc-error "server" "con"))) + +;; prompt & abort in the same component, the tag elsewhere +(do-test + (term (let ([(pt : (Prompt Num Num)) + (monitor (prompt-tag/c (flat (λ (x : Num) (zero? x))) + (flat (λ (x : Num) (zero? x))) + Num Num) + (make-prompt-tag Num Num) + "server" + "client" + "con")]) + (% (abort Num pt 3) + pt + (λ (x : Num) (+ x 1))))) + (term (ctc-error "client" "con"))) + +;; call/comp issue +(do-test + (term (let ([(pt : (Prompt Num Num)) + (monitor (prompt-tag/c (flat (λ (x : Num) (zero? x))) + (flat (λ (x : Num) (zero? x))) + Num Num) + (make-prompt-tag Num Num) + "server" + "client" + "con")]) + (% (+ 1 + (call/comp + (λ (k : (→ Num Num)) + (k 0)) + pt)) + pt + (λ (x : Num) (+ x 1))))) + (term (ctc-error "client" "con"))) + +;; blame even on one side +(do-test + (term (let ([(pt1 : (Prompt Num Num)) + (make-prompt-tag Num Num)]) + (let ([(pt2 : (Prompt Num Num)) + (monitor (prompt-tag/c (flat (λ (x : Num) (zero? x))) + (flat (λ (x : Num) (zero? (- x 5)))) + Num Num) + pt1 + "client" + "server" + "con")]) + (% (+ 1 ; doesn't add to 5 + (call/comp + (λ (k : (→ Num Num)) + (k 3)) + pt1)) + pt2 + (λ (x : Num) (+ x 1)))))) + (term (ctc-error "server" "con"))) + +;; blame even on other side +(do-test + (term (let ([(pt1 : (Prompt Num Num)) + (make-prompt-tag Num Num)]) + (let ([(pt2 : (Prompt Num Num)) + (monitor (prompt-tag/c (flat (λ (x : Num) (zero? x))) + (flat (λ (x : Num) (zero? (- x 5)))) + Num Num) + pt1 + "server" + "client" + "con")]) + (% (+ 1 ; doesn't add to 5 + (call/comp + (λ (k : (→ Num Num)) + (k 3)) + pt2)) + pt1 + (λ (x : Num) (+ x 1)))))) + (term (ctc-error "server" "con"))) + +;; same with ho-contract +(do-test + (term (let ([(pt : (Prompt (→ Num Num) Num)) + (monitor (prompt-tag/c (-> (flat (λ (x : Num) (zero? x))) + (flat (λ (x : Num) (number? x)))) + (flat (λ (x : Num) (number? x))) + (→ Num Num) Num) + (make-prompt-tag (→ Num Num) Num) + "server" + "client" + "con")]) + (% (abort Num pt (λ (x : Num) 5)) + pt + (λ (x : (→ Num Num)) (x 8))))) + (term (ctc-error "client" "con"))) + +;; again, but from other side +(do-test + (term (let ([(pt : (Prompt (→ Num Num) Num)) + (monitor (prompt-tag/c (-> (flat (λ (x : Num) (zero? x))) + (flat (λ (x : Num) (zero? x)))) + (flat (λ (x : Num) (zero? x))) + (→ Num Num) Num) + (make-prompt-tag (→ Num Num) Num) + "server" + "client" + "con")]) + (% (abort Num pt (λ (x : Num) 3)) + pt + (λ (f : (→ Num Num)) (f 0))))) + (term (ctc-error "client" "con"))) + +;; abort across boundary w/ ho-value +(do-test + (term (let ([(do-prompt : (→ (→ (Prompt (→ Num Num) Num) Num) Num)) + (let ([(pt : (Prompt (→ Num Num) Num)) + (make-prompt-tag (→ Num Num) Num)]) + (monitor (-> (-> (prompt-tag/c (-> (flat (λ (x : Num) (zero? x))) + (flat (λ (x : Num) (zero? x)))) + (flat (λ (x : Num) (zero? x))) + (→ Num Num) Num) + (flat (λ (x : Num) (number? x)))) + (flat (λ (x : Num) (number? x)))) + (λ (f : (→ (Prompt (→ Num Num) Num) Num)) + (% (f pt) + pt + (λ (f : (→ Num Num)) (f 5)))) + "server" + "client" + "con"))]) + (do-prompt + (λ (pt : (Prompt (→ Num Num) Num)) + (abort Num pt (λ (v : Num) (+ v 1))))))) + (term (ctc-error "server" "con"))) ;; MF: nice example but in a paper presentation you need to simplify + +;; where the prompt flows across multiple boundaries +(do-test + (term (let ([(do-prompt : (→ (→ (Prompt (→ Num Num) Num) Num) Num)) + (let ([(pt : (Prompt (→ Num Num) Num)) + (make-prompt-tag (→ Num Num) Num)]) + (monitor (-> (-> (prompt-tag/c (-> (flat (λ (x : Num) (number? x))) + (flat (λ (x : Num) (number? x)))) + (flat (λ (x : Num) (number? x))) + (→ Num Num) Num) + (flat (λ (x : Num) (number? x)))) + (flat (λ (x : Num) (number? x)))) + (λ (f : (→ (Prompt (→ Num Num) Num) Num)) + (% (f pt) + pt + (λ (f : (→ Num Num)) (f 1)))) + "A" + "B" + "con1"))]) + (let ([(do-prompt-2 : (→ (→ (Prompt (→ Num Num) Num) Num) Num)) + (monitor (-> (-> (prompt-tag/c (-> (flat (λ (x : Num) (zero? x))) + (flat (λ (x : Num) (number? x)))) + (flat (λ (x : Num) (number? x))) + (→ Num Num) Num) + (flat (λ (x : Num) (number? x)))) + (flat (λ (x : Num) (number? x)))) + (λ (f : (→ (Prompt (→ Num Num) Num) Num)) + (do-prompt f)) + "B" + "C" + "con2")]) + (do-prompt-2 + (λ (pt : (Prompt (→ Num Num) Num)) + (abort Num pt (λ (v : Num) (+ v 1)))))))) + (term (ctc-error "B" "con2"))) + +#| + ;; from random test generation + (do-test + (term (boolean? + (abort (monitor + (prompt-tag/c (-> (flat (λ (H) (error))) + (flat (λ (R) (error))))) + (prompt-tag v) + "pos" + "neg") + (make-prompt-tag)))) + (term (error))) + |# + + +;; tests for bugs found by random generation +(test-equal + (term (subst (make-cm-key Bool) x 5)) + (term (make-cm-key Bool))) + +(test-equal + (term (subst (null Bool) x 5)) + (term (null Bool))) + +(test-equal + (abort-eval (term (ccm (make-cm-key Bool) Bool))) + 'null) + +(test-equal + (abort-eval (term (μ (B : Num) B))) + 'non-terminating) + +(test-equal + (abort-eval (term unit)) + 'unit) + +(test-equal + (abort-eval + (term (call/comp + (λ (Dp : (→ (Mark Bool) Num)) (make-cm-key Bool)) + (make-prompt-tag (Mark (Con Num)) Num)))) + 'missing-prompt) + +(test-equal + (term (no-match (call/comp + (λ (K : (→ (Prompt (Mark Num) Bool) + (List (Prompt Bool Unit)))) + (make-prompt-tag (Mark Num) Bool)) + (wcm · hole)) tag)) + #t) + +(test-equal + (abort-eval + (term (abort + Num + (make-prompt-tag Bool (List (Mark Bool))) + (boolean? 2)))) + 'missing-prompt) + +(test-equal + (term (marks (call/cm hole (+ 1 2) 1) key1 (null (→ (Mark Num) Num)))) + (term (null (→ (Mark Num) Num)))) + +(test-equal + (term + (marks (if (boolean? hole) 1 2) key (null (→ Num (Mark Unit))))) + (term (null (→ Num (Mark Unit))))) + +(test-equal + (term + (no-match (call/cm key (wcm · hole) + ((wcm · (λ (C : Bool) #f)) (unit? 3))) + tag)) + #t) + +(test-equal + (abort-eval + (term + (number? + (μ + (i : Num) + (- + (+ (case + (null (Con (Con Bool))) + (null = 1) + ((cons X u) = 2)) (if #t 0 0)) + i))))) + 'non-terminating) + +(test-equal + (judgment-holds + (tc + · + (tag2 + : + (Prompt (Mark (Prompt Unit Num)) (Prompt (→ Num Unit) (Con Bool))) + (tag1 + : + (Prompt Num (→ (→ Unit Unit) (Con Unit))) + (tag + : + (Prompt + (→ (Prompt Num Unit) (→ Bool Unit)) + (Prompt Num (→ (→ Unit Unit) (Con Unit)))) + ·))) + (abort + (→ Num (→ Num Num)) + tag1 + (wcm + · + (call/comp + (λ (Sa : (→ Num (Prompt (→ Num Unit) (Con Bool)))) 0) + tag2))) + t) + t) + '((→ Num (→ Num Num)))) + +(test-equal + (judgment-holds + (tc + · + (tag1 + : + (Prompt Bool (List Num)) + (key1 + : + (Mark Bool) + (tag + : + (Prompt Unit (Mark (List (Mark Unit)))) + (key : (Mark (Prompt Unit (Mark (List (Mark Unit))))) ·)))) + (wcm + ((key + (PG + (flat (λ (G : Unit) #t)) + (mark/c + (list/c (mark/c (flat (λ (b : Unit) #t)) Unit)) + (List (Mark Unit))) + tag + "B" + "iF" + "CgXohMerymUWF")) + ·) + (monitor + (flat (λ (Mk : Unit) #t)) + (abort Unit tag1 #t) + "fO" + "clRmiOfXGo" + "jxeinueLyNmLozqsKl")) + t) + t) + '(Unit)) + +(test-equal + (judgment-holds + (tc · (key : (Mark (Mark (Mark Num))) ·) + (MG + (mark/c (mark/c (flat (λ (r : Num) #f)) Num) (Mark Num)) + key + "EVYdYcpulOg" + "G" + "BjUOkycjoz") + t) + t) + '((Mark (Mark (Mark Num))))) + + + + +(check-false (term (not-wcm (wcm · hole)))) +(check-false (term (not-wcm (+ 5 (wcm · hole))))) +(check-true (term (not-wcm hole))) +(check-true (term (not-wcm (abort Num hole 5)))) \ No newline at end of file diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/test-file.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/test-file.rkt index 140780ff4b..e0914edde2 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/test-file.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/test-file.rkt @@ -4,6 +4,7 @@ racket/cmdline racket/list racket/set + racket/match math/statistics) (define minutes 1) @@ -25,8 +26,14 @@ #:multi [("-t" "--type") t "Generation type to run, one of: search, grammar, search-gen, search-gen-ref, search-gen-enum, search-gen-enum-ref" (set! types (cons (string->symbol t) types))] - #:args (filename) - filename)) + #:args filenames + (match filenames + [`() + (exit)] + [(list name) + name] + [else + (error "Expected a single file as an argument")]))) (when (empty? types) (set! types all-types))