From 7c4012bbd452ed2b37392c07abf16f2ca0b2a537 Mon Sep 17 00:00:00 2001 From: Jay McCarthy Date: Wed, 19 Mar 2014 16:32:09 -0600 Subject: [PATCH] delim cont 1 --- .../examples/benchmark/delim-cont/1.diff | 29 ++++++++++++++++++- .../benchmark/delim-cont/delim-cont-1.rkt | 26 +++++++++++++++++ 2 files changed, 54 insertions(+), 1 deletion(-) 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 6ce90cd4ef..7fbbe79f6a 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 @@ -11,5 +11,32 @@ > (monitor ctc (ccm mk t) k l j) 326a330 > -937a942 +938a943 > +948a954,979 +> (define small-counter-example +> (term +> ;; (List Num) +> (ccm +> ;; (Mark Num) +> (MG ;; (Con Num) +> (flat (λ (x : Num) (number? x))) +> ;; (Mark Num) +> (make-cm-key Num) +> "k" "l" "j") +> Num))) +> +> (local +> () +> (define ctc-fun (term (λ (x : Num) (number? x)))) +> (test-equal (judgment-holds (tc · · ,ctc-fun (→ Num Bool))) #t) +> (define ctc (term (flat ,ctc-fun))) +> (test-equal (judgment-holds (tcc · · ,ctc (Con Num))) #t) +> (define v (term (make-cm-key Num))) +> (test-equal (judgment-holds (tc · · ,v (Mark Num))) #t) +> (test-equal (redex-match? abort-lang l "k") #t) +> (test-equal (redex-match? abort-lang l "l") #t) +> (test-equal (redex-match? abort-lang l "j") #t) +> ;; XXX This makes no sense, given the definition on line 495 +> (test-equal (judgment-holds (tc · · (MG ,ctc ,v "k" "l" "j") (Mark Num))) #t)) +> (test-equal (check small-counter-example) #f) 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 c66b5942a9..454ac0fb1f 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 @@ -951,3 +951,29 @@ (set! index (add1 index)) (generate-term abort-lang e #:i-th index)))) +(define small-counter-example + (term + ;; (List Num) + (ccm + ;; (Mark Num) + (MG ;; (Con Num) + (flat (λ (x : Num) (number? x))) + ;; (Mark Num) + (make-cm-key Num) + "k" "l" "j") + Num))) + +(local + () + (define ctc-fun (term (λ (x : Num) (number? x)))) + (test-equal (judgment-holds (tc · · ,ctc-fun (→ Num Bool))) #t) + (define ctc (term (flat ,ctc-fun))) + (test-equal (judgment-holds (tcc · · ,ctc (Con Num))) #t) + (define v (term (make-cm-key Num))) + (test-equal (judgment-holds (tc · · ,v (Mark Num))) #t) + (test-equal (redex-match? abort-lang l "k") #t) + (test-equal (redex-match? abort-lang l "l") #t) + (test-equal (redex-match? abort-lang l "j") #t) + ;; XXX This makes no sense, given the definition on line 495 + (test-equal (judgment-holds (tc · · (MG ,ctc ,v "k" "l" "j") (Mark Num))) #t)) +(test-equal (check small-counter-example) #f)