Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 5 additions & 3 deletions typed-racket-lib/typed-racket/core.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -48,10 +48,12 @@
(and (attribute opt?) (syntax-e (attribute opt?))))]
[with-refinements? (and (or (attribute refinement-reasoning?)
(with-refinements?))
(when (not (eq? te-mode deep))
(unless (eq? te-mode deep)
(raise-arguments-error
(string->symbol (format "typed/racket/~a" (keyword->string (syntax-e te-attr))))
"#:with-refinements unsupported")))])
(string->symbol (format "typed/racket/~a"
(keyword->string
(syntax-e te-attr))))
"#:with-refinements unsupported")))])
(tc-module/full te-mode stx pmb-form
(λ (new-mod pre-before-code pre-after-code)
(define ctc-cache (make-hash))
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -61,10 +61,9 @@
(list invoke/scs ...)))
v)
(define (sig-spec->syntax sig-spec)
(match sig-spec
[(signature-spec name members scs)
(define member-stx (map (lambda (id sc) #`(#,id #,(f sc))) members scs))
#`(#,name #,@member-stx)]))
(match-define (signature-spec name members scs) sig-spec)
(define member-stx (map (lambda (id sc) #`(#,id #,(f sc))) members scs))
#`(#,name #,@member-stx))

(define (invokes->contract lst)
(cond
Expand Down
18 changes: 9 additions & 9 deletions typed-racket-lib/typed-racket/tc-setup.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -36,15 +36,15 @@
;; types are enforced (not no-check etc.),
;; PLT_TR_NO_OPTIMIZE is not set, and the
;; current code inspector has sufficient privileges
(if (and (optimize?)
(memq (current-type-enforcement-mode) (list deep shallow))
(not (getenv "PLT_TR_NO_OPTIMIZE"))
(authorized-code-inspector?))
(begin
(do-time "Starting optimizer")
(begin0 (stx-map optimize-top body)
(do-time "Optimized")))
body))
(cond
[(and (optimize?)
(memq (current-type-enforcement-mode) (list deep shallow))
(not (getenv "PLT_TR_NO_OPTIMIZE"))
(authorized-code-inspector?))
(do-time "Starting optimizer")
(begin0 (stx-map optimize-top body)
(do-time "Optimized"))]
[else body]))

(define (maybe-shallow-rewrite body-stx ctc-cache)
(case (current-type-enforcement-mode)
Expand Down
15 changes: 6 additions & 9 deletions typed-racket-lib/typed-racket/typecheck/check-below.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -129,19 +129,16 @@
[((tc-result1: t1 p1 o1) (tc-result1: t2 p2 o2))
(define (perform-check!)
(cond
[(not (subtype t1 t2 o1))
(expected-but-got t2 t1)]
[(and (not (prop-set-better? p1 p2))
(object-better? o1 o2))
[(not (subtype t1 t2 o1)) (expected-but-got t2 t1)]
[(and (not (prop-set-better? p1 p2)) (object-better? o1 o2))
(type-mismatch p2 p1 "mismatch in proposition")]
[(and (prop-set-better? p1 p2)
(not (object-better? o1 o2)))
[(and (prop-set-better? p1 p2) (not (object-better? o1 o2)))
(type-mismatch (print-object o2) (print-object o1) "mismatch in object")]
[(and (not (prop-set-better? p1 p2))
(not (object-better? o1 o2)))
[(and (not (prop-set-better? p1 p2)) (not (object-better? o1 o2)))
(type-mismatch (format "`~a' and `~a'" p2 (print-object o2))
(format "`~a' and `~a'" p1 (print-object o1))
"mismatch in proposition and object")])
"mismatch in proposition and object")]
[else (void)])
(ret (upgrade-trusted-rng t1 t2) (fix-props p2 p1) (fix-object o2 o1)))
(cond
[(with-refinements?)
Expand Down
224 changes: 104 additions & 120 deletions typed-racket-lib/typed-racket/typecheck/integer-refinements.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -71,143 +71,127 @@
#:attr obj (if (Object? o) o -empty-obj)))

;; < <= >= =
(define (numeric-comparison-function prop-constructor)
(λ (args-stx result)
(syntax-parse args-stx
[((~var e1 (w/obj+type -Int)) (~var e2 (w/obj+type -Int)))
(define p (prop-constructor (attribute e1.obj) (attribute e2.obj)))
(add-p/not-p result p)]
[((~var e1 (w/type -Int)) (~var e2 (w/type -Int)) (~var e3 (w/type -Int)))
#:when (or (and (Object? (attribute e1.obj)) (Object? (attribute e2.obj)))
(and (Object? (attribute e2.obj)) (Object? (attribute e3.obj))))
(define p (-and (prop-constructor (attribute e1.obj) (attribute e2.obj))
(prop-constructor (attribute e2.obj) (attribute e3.obj))))
(add-p/not-p result p)]
[_ result])))
(define ((numeric-comparison-function prop-constructor) args-stx result)
(syntax-parse args-stx
[((~var e1 (w/obj+type -Int)) (~var e2 (w/obj+type -Int)))
(define p (prop-constructor (attribute e1.obj) (attribute e2.obj)))
(add-p/not-p result p)]
[((~var e1 (w/type -Int)) (~var e2 (w/type -Int)) (~var e3 (w/type -Int)))
#:when (or (and (Object? (attribute e1.obj)) (Object? (attribute e2.obj)))
(and (Object? (attribute e2.obj)) (Object? (attribute e3.obj))))
(define p
(-and (prop-constructor (attribute e1.obj) (attribute e2.obj))
(prop-constructor (attribute e2.obj) (attribute e3.obj))))
(add-p/not-p result p)]
[_ result]))

;; +/-
(define (plus/minus plus?)
(λ (args-stx result)
(match result
[(tc-result1: ret-t ps orig-obj)
(syntax-parse args-stx
;; +/- (2 args)
[((~var e1 (w/obj+type -Int))
(~var e2 (w/obj+type -Int)))
(define (sign o) (if plus? o (scale-obj -1 o)))
(define l (-lexp (attribute e1.obj) (sign (attribute e2.obj))))
(ret (-refine/fresh x ret-t (-eq (-lexp x) l))
ps
l)]
;; +/- (3 args)
[((~var e1 (w/obj+type -Int))
(~var e2 (w/obj+type -Int))
(~var e3 (w/obj+type -Int)))
(define (sign o) (if plus? o (scale-obj -1 o)))
(define l (-lexp (attribute e1.obj) (sign (attribute e2.obj)) (sign (attribute e3.obj))))
(ret (-refine/fresh x ret-t (-eq (-lexp x) l))
ps
l)]
[_ result])]
[_ result])))
(define ((plus/minus plus?) args-stx result)
(match result
[(tc-result1: ret-t ps orig-obj)
(syntax-parse args-stx
;; +/- (2 args)
[((~var e1 (w/obj+type -Int)) (~var e2 (w/obj+type -Int)))
(define (sign o)
(if plus?
o
(scale-obj -1 o)))
(define l (-lexp (attribute e1.obj) (sign (attribute e2.obj))))
(ret (-refine/fresh x ret-t (-eq (-lexp x) l)) ps l)]
;; +/- (3 args)
[((~var e1 (w/obj+type -Int)) (~var e2 (w/obj+type -Int)) (~var e3 (w/obj+type -Int)))
(define (sign o)
(if plus?
o
(scale-obj -1 o)))
(define l (-lexp (attribute e1.obj) (sign (attribute e2.obj)) (sign (attribute e3.obj))))
(ret (-refine/fresh x ret-t (-eq (-lexp x) l)) ps l)]
[_ result])]
[_ result]))

;; equal?/eqv?/eq?
;; if only one side is a supported type, we can learn integer equality for
;; a result of `#t`, whereas if both sides are of the supported type,
;; we learn on both `#t` and `#f` answers
(define (equality-function supported-type)
(λ (args-stx result)
(syntax-parse args-stx
[((~var e1 (w/obj+type supported-type)) (~var e2 (w/obj+type supported-type)))
(define p (-eq (attribute e1.obj) (attribute e2.obj)))
(add-p/not-p result p)]
[((~var e1 (w/obj+type supported-type)) (~var e2 (w/obj+type Univ)))
(define p (-eq (attribute e1.obj) (attribute e2.obj)))
(add-to-pos-side result p)]
[((~var e1 (w/obj+type Univ)) (~var e2 (w/obj+type supported-type)))
(define p (-eq (attribute e1.obj) (attribute e2.obj)))
(add-to-pos-side result p)]
[_ result])))
(define ((equality-function supported-type) args-stx result)
(syntax-parse args-stx
[((~var e1 (w/obj+type supported-type)) (~var e2 (w/obj+type supported-type)))
(define p (-eq (attribute e1.obj) (attribute e2.obj)))
(add-p/not-p result p)]
[((~var e1 (w/obj+type supported-type)) (~var e2 (w/obj+type Univ)))
(define p (-eq (attribute e1.obj) (attribute e2.obj)))
(add-to-pos-side result p)]
[((~var e1 (w/obj+type Univ)) (~var e2 (w/obj+type supported-type)))
(define p (-eq (attribute e1.obj) (attribute e2.obj)))
(add-to-pos-side result p)]
[_ result]))

;; *
(define product-function
(λ (args-stx result)
(match result
[(tc-result1: ret-t ps orig-obj)
(syntax-parse args-stx
[((~var e1 (w/obj+type -Int)) (~var e2 (w/obj+type -Int)))
(define product-obj (-obj* (attribute e1.obj) (attribute e2.obj)))
(cond
[(Object? product-obj)
(ret (-refine/fresh x ret-t (-eq (-lexp x) product-obj))
ps
product-obj)]
[else result])]
[_ result])]
[_ result])))
(define (product-function args-stx result)
(match result
[(tc-result1: ret-t ps orig-obj)
(syntax-parse args-stx
[((~var e1 (w/obj+type -Int)) (~var e2 (w/obj+type -Int)))
(define product-obj (-obj* (attribute e1.obj) (attribute e2.obj)))
(cond
[(Object? product-obj)
(ret (-refine/fresh x ret-t (-eq (-lexp x) product-obj)) ps product-obj)]
[else result])]
[_ result])]
[_ result]))

;; make-vector
(define make-vector-function
(λ (args-stx result)
(match result
[(tc-result1: ret-t ps orig-obj)
(syntax-parse args-stx
[((~var size (w/obj+type -Int)) . _)
(ret (-refine/fresh v ret-t (-eq (-lexp (-vec-len-of (-id-path v)))
(attribute size.obj)))
ps
orig-obj)]
[_ result])]
[_ result])))
(define (make-vector-function args-stx result)
(match result
[(tc-result1: ret-t ps orig-obj)
(syntax-parse args-stx
[((~var size (w/obj+type -Int)) . _)
(ret (-refine/fresh v ret-t (-eq (-lexp (-vec-len-of (-id-path v))) (attribute size.obj)))
ps
orig-obj)]
[_ result])]
[_ result]))

;; modulo
(define modulo-function
(λ (args-stx result)
(match result
[(tc-result1: ret-t ps orig-obj)
(syntax-parse args-stx
[((~var e1 (w/type -Int)) (~var e2 (w/obj+type -Nat)))
(ret (-refine/fresh x ret-t (-lt (-lexp x) (attribute e2.obj)))
ps
orig-obj)]
[_ result])]
[_ result])))
(define (modulo-function args-stx result)
(match result
[(tc-result1: ret-t ps orig-obj)
(syntax-parse args-stx
[((~var e1 (w/type -Int)) (~var e2 (w/obj+type -Nat)))
(ret (-refine/fresh x ret-t (-lt (-lexp x) (attribute e2.obj))) ps orig-obj)]
[_ result])]
[_ result]))

;; random
(define random-function
(λ (args-stx result)
(match result
[(tc-result1: ret-t ps orig-obj)
(syntax-parse args-stx
;; random (1 arg)
[((~var e1 (w/obj+type -Nat)))
(ret (-refine/fresh x ret-t (-lt (-lexp x) (attribute e1.obj)))
ps
orig-obj)]
;; random (2 arg)
[((~var e1 (w/type -Int)) (~var e2 (w/type -Int)))
#:when (or (Object? (attribute e1.obj))
(Object? (attribute e2.obj)))
(ret (-refine/fresh x ret-t (-and (-leq (attribute e1.obj) (-lexp x))
(-lt (-lexp x) (attribute e2.obj))))
ps
orig-obj)]
[_ result])]
[_ result])))
(define (random-function args-stx result)
(match result
[(tc-result1: ret-t ps orig-obj)
(syntax-parse args-stx
;; random (1 arg)
[((~var e1 (w/obj+type -Nat)))
(ret (-refine/fresh x ret-t (-lt (-lexp x) (attribute e1.obj))) ps orig-obj)]
;; random (2 arg)
[((~var e1 (w/type -Int)) (~var e2 (w/type -Int)))
#:when (or (Object? (attribute e1.obj)) (Object? (attribute e2.obj)))
(ret (-refine/fresh x
ret-t
(-and (-leq (attribute e1.obj) (-lexp x))
(-lt (-lexp x) (attribute e2.obj))))
ps
orig-obj)]
[_ result])]
[_ result]))

;; add1 / sub1
(define (add/sub-1-function add?)
(λ (args-stx result)
(match result
[(tc-result1: ret-t ps orig-obj)
(syntax-parse args-stx
[((~var e1 (w/obj+type -Int)))
(define l ((if add? -lexp-add1 -lexp-sub1) (attribute e1.obj)))
(ret (-refine/fresh x ret-t (-eq (-lexp x) l))
ps
l)]
[_ result])]
[_ result])))
(define ((add/sub-1-function add?) args-stx result)
(match result
[(tc-result1: ret-t ps orig-obj)
(syntax-parse args-stx
[((~var e1 (w/obj+type -Int)))
(define l ((if add? -lexp-add1 -lexp-sub1) (attribute e1.obj)))
(ret (-refine/fresh x ret-t (-eq (-lexp x) l)) ps l)]
[_ result])]
[_ result]))

(define linear-integer-function-table
(make-immutable-free-id-table
Expand Down
Loading