Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Automated Resyntax fixes #1419

Open
wants to merge 12 commits into
base: master
Choose a base branch
from
Open
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
10 changes: 5 additions & 5 deletions typed-racket-lib/typed-racket/typecheck/possible-domains.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -55,11 +55,11 @@

;; currently does not take advantage of multi-valued or arbitrary-valued expected types,
(define expected-ty
(and expected
(match expected
[(tc-result1: t) t]
[(tc-any-results: (or #f (TrueProp:))) #t] ; anything is a subtype of expected
[_ #f]))) ; don't know what it is, don't do any pruning
(match expected
[#f #f]
[(tc-result1: t) t]
[(tc-any-results: (or #f (TrueProp:))) #t] ; anything is a subtype of expected
[_ #f])) ; don't know what it is, don't do any pruning
(define (returns-subtype-of-expected? fun-ty)
(or (not expected) ; no expected type, anything is fine
(eq? expected-ty #t) ; expected is tc-anyresults, anything is fine
Expand Down
10 changes: 5 additions & 5 deletions typed-racket-lib/typed-racket/typecheck/provide-handling.rkt
Original file line number Diff line number Diff line change
@@ -1,13 +1,13 @@
#lang racket/base

(require "../utils/utils.rkt"
(require (for-syntax racket/base)
(for-template racket/base)
racket/sequence
syntax/parse
"../private/syntax-properties.rkt"
"def-binding.rkt"
"../env/env-utils.rkt"
(for-syntax racket/base)
(for-template racket/base))
"../private/syntax-properties.rkt"
"../utils/utils.rkt"
"def-binding.rkt")

(provide remove-provides provide? generate-prov)

Expand Down
10 changes: 5 additions & 5 deletions typed-racket-lib/typed-racket/typecheck/tc-app-combined.rkt
Original file line number Diff line number Diff line change
@@ -1,17 +1,17 @@
#lang racket/base

(require "tc-app/tc-app-apply.rkt"
(require "signatures.rkt"
"tc-app/tc-app-apply.rkt"
"tc-app/tc-app-contracts.rkt"
"tc-app/tc-app-eq.rkt"
"tc-app/tc-app-hetero.rkt"
"tc-app/tc-app-keywords.rkt"
"tc-app/tc-app-lambda.rkt"
"tc-app/tc-app-list.rkt"
"tc-app/tc-app-main.rkt"
"tc-app/tc-app-objects.rkt"
"tc-app/tc-app-special.rkt"
"tc-app/tc-app-values.rkt"
"tc-app/tc-app-contracts.rkt"
"tc-app/tc-app-main.rkt"
"signatures.rkt")
"tc-app/tc-app-values.rkt")

(require racket/unit)
(provide tc-app-combined@)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -3,16 +3,16 @@
;; This module provides custom type-checking rules for the expansion
;; of contracted values

(require "../../utils/utils.rkt"
"signatures.rkt"
"utils.rkt"
(require (for-template racket/base
;; shift -1 because it's provided +1
racket/contract/private/provide)
syntax/parse
"../signatures.rkt"
(only-in typed-racket/types/type-table add-typeof-expr)
(only-in typed-racket/types/tc-result ret)
(for-template racket/base
;; shift -1 because it's provided +1
racket/contract/private/provide))
"../../utils/utils.rkt"
"../signatures.rkt"
"signatures.rkt"
"utils.rkt")

(import tc-expr^)
(export tc-app-contracts^)
Expand Down
24 changes: 14 additions & 10 deletions typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-eq.rkt
Original file line number Diff line number Diff line change
@@ -1,19 +1,23 @@
#lang racket/unit

(require "../../utils/utils.rkt"
"signatures.rkt"
"utils.rkt"
(require (for-label racket/base
racket/bool)
racket/match
racket/unsafe/undefined
syntax/parse
syntax/stx
(only-in "../../infer/infer.rkt" intersect)
syntax/parse syntax/stx racket/match racket/unsafe/undefined
"../signatures.rkt"
"../tc-funapp.rkt"
"../../rep/object-rep.rkt"
"../../rep/type-rep.rkt"
"../../types/abbrev.rkt"
"../../types/match-expanders.rkt"
"../../types/prop-ops.rkt"
"../../types/utils.rkt"
"../../types/match-expanders.rkt"
"../../rep/type-rep.rkt"
"../../rep/object-rep.rkt"
(for-label racket/base racket/bool))
"../../utils/utils.rkt"
"../signatures.rkt"
"../tc-funapp.rkt"
"signatures.rkt"
"utils.rkt")

(import tc-expr^)
(export tc-app-eq^)
Expand Down
Loading
Loading