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

delim cont 1

Browse Source
This commit is contained in:
Jay McCarthy 2014-03-19 16:32:09 -06:00
parent ed840e90fa
commit 7c4012bbd4
2 changed files with 54 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

29
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/1.diff
View File

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

26
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-1.rkt
View File

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