Permalink
Browse files

* suppress errors on partial primitive ops (e.g. (sqrt -1))

* redex-check
  • Loading branch information...
1 parent b59c9ef commit 05c22057b42c898cd96179090e37078781f28abd Phil Nguyen committed Jun 2, 2012
Showing with 12 additions and 4 deletions.
  1. +1 −1 cpcf/cpcf.rkt
  2. +2 −1 cpcf/in-racket/scpcf-lang.rkt
  3. +9 −2 cpcf/scpcf.rkt
View
@@ -150,7 +150,7 @@
[(δ odd? n) (to-bool ,(odd? (term n)))]
[(δ true? b) (to-bool ,(equal? (term b) (term #t)))]
[(δ false? b) (to-bool ,(equal? (term b) (term #f)))]
- [(δ sqrt n) ,(inexact->exact (floor (sqrt (term n))))] ; whatever
+ [(δ sqrt n) ,(inexact->exact (floor (sqrt (abs (term n)))))] ; whatever
[(δ + m n) ,(+ (term m) (term n))]
[(δ - m n) ,(- (term m) (term n))]
[(δ ∨ b ...) ,(ormap (curry equal? (term #t)) (term (b ...)))]
@@ -288,7 +288,8 @@
['prime? (λ (n) (if (member n '(2 3 5 7 11 13)) #t #f))] ; force #t
['true? (compose not false?)]
['false? false?]
- ['sqrt (compose inexact->exact floor sqrt)]
+ ; 'abs' here to suppress cases like (sqrt -1)
+ ['sqrt (compose inexact->exact floor sqrt abs)]
['+ +]
['- -]
['∨ (λ (x y) (or x y))]
View
@@ -379,6 +379,8 @@
(require "in-racket/scpcf-eval.rkt")
(require (only-in "in-racket/scpcf-lang.rkt"
read-exp [type-check tc] show-type))
+(define count 0)
+
(redex-check
SCPCF-src
M-closed
@@ -387,5 +389,10 @@
[tc2 (show-type (tc readM))])
(and (equal? tc1 tc2)
(or (equal? tc1 'TypeError)
- (equal? (eval-red (term M-closed))
- (eval-cek (term M-closed)))))))
+ (begin
+ (set! count (add1 count))
+ (equal? (eval-red (term M-closed))
+ (eval-cek (term M-closed)))))))
+ #:attempts 5000)
+
+`(,count programs were well-typed)

1 comment on commit 05c2205

Owner
samth commented on 05c2205 Jun 2, 2012

I think that sqrt should produce a contract error in the model when applied to negative arguments, or we should support complex numbers.

Please sign in to comment.