c70910aaa0
Previously the restriction didn't account for traversing the object type with the given path. This also relies on the previous commit that adds subtyping on filters. (because this change seems to introduce filters which only differ by an unrolling of a recursive type, but the old subtyping only worked for identical types)
182 lines
7.8 KiB
Racket
182 lines
7.8 KiB
Racket
#lang racket/base
|
|
|
|
(require "test-utils.rkt"
|
|
rackunit racket/format
|
|
(typecheck tc-metafunctions tc-subst)
|
|
(rep filter-rep type-rep object-rep)
|
|
(types abbrev union filter-ops tc-result numeric-tower)
|
|
(for-syntax racket/base syntax/parse))
|
|
|
|
(provide tests)
|
|
(gen-test-main)
|
|
|
|
(define-syntax (test-combine-props stx)
|
|
(syntax-parse stx
|
|
[(_ new:expr existing:expr expected:expr box-v:expr)
|
|
(quasisyntax/loc stx
|
|
(test-case (~a '(new + existing = expected))
|
|
(define success
|
|
(let/ec exit
|
|
(define-values (res-formulas res-props) (combine-props new existing exit))
|
|
#,(syntax/loc stx (check-equal? (append res-formulas res-props) expected))
|
|
#t))
|
|
#,(syntax/loc stx (check-equal? success box-v))))]))
|
|
|
|
|
|
(define tests
|
|
(test-suite "Metafunctions"
|
|
|
|
(test-suite "combine-props"
|
|
|
|
(test-combine-props
|
|
(list (-or (-not-filter -String #'x) (-not-filter -String #'y)))
|
|
(list (-filter (Un -String -Symbol) #'x) (-filter (Un -String -Symbol) #'y))
|
|
(list (-or (-not-filter -String #'y) (-not-filter -String #'x))
|
|
(-filter (Un -String -Symbol) #'y) (-filter (Un -String -Symbol) #'x))
|
|
#t)
|
|
|
|
(test-combine-props
|
|
(list (-or (-filter -String #'x) (-filter -String #'y)))
|
|
(list (-filter (Un -String -Symbol) #'x) (-filter (Un -String -Symbol) #'y))
|
|
(list (-or (-filter -String #'y) (-filter -String #'x))
|
|
(-filter (Un -String -Symbol) #'y) (-filter (Un -String -Symbol) #'x))
|
|
#t)
|
|
)
|
|
|
|
(test-suite "merge-tc-results"
|
|
(check-equal?
|
|
(merge-tc-results (list))
|
|
(ret -Bottom))
|
|
(check-equal?
|
|
(merge-tc-results (list (ret Univ)))
|
|
(ret Univ))
|
|
(check-equal?
|
|
(merge-tc-results (list (ret Univ -top-filter (make-Path null #'x))))
|
|
(ret Univ -top-filter (make-Path null #'x)))
|
|
(check-equal?
|
|
(merge-tc-results (list (ret -Bottom) (ret -Symbol -top-filter (make-Path null #'x))))
|
|
(ret -Symbol -top-filter (make-Path null #'x)))
|
|
(check-equal?
|
|
(merge-tc-results (list (ret -String) (ret -Symbol)))
|
|
(ret (Un -Symbol -String)))
|
|
(check-equal?
|
|
(merge-tc-results (list (ret -String -true-filter) (ret -Symbol -true-filter)))
|
|
(ret (Un -Symbol -String) -true-filter))
|
|
(check-equal?
|
|
(merge-tc-results (list (ret (-val #f) -false-filter) (ret -Symbol -true-filter)))
|
|
(ret (Un -Symbol (-val #f)) -top-filter))
|
|
(check-equal?
|
|
(merge-tc-results (list (ret (list (-val 0) (-val 1))) (ret (list (-val 1) (-val 2)))))
|
|
(ret (list (Un (-val 0) (-val 1)) (Un (-val 1) (-val 2)))))
|
|
(check-equal?
|
|
(merge-tc-results (list (ret null null null -Symbol 'x) (ret null null null -String 'x)))
|
|
(ret null null null (Un -Symbol -String) 'x))
|
|
)
|
|
|
|
|
|
(test-suite "values->tc-results"
|
|
(check-equal?
|
|
(values->tc-results (make-Values (list (-result -Symbol))) (list -empty-obj) (list Univ))
|
|
(ret -Symbol))
|
|
|
|
(check-equal?
|
|
(values->tc-results (make-Values (list (-result -Symbol) (-result -String)))
|
|
(list -empty-obj -empty-obj) (list Univ Univ))
|
|
(ret (list -Symbol -String)))
|
|
|
|
(check-equal?
|
|
(values->tc-results (make-Values (list (-result -Symbol (-FS -top -bot)))) (list -empty-obj) (list Univ))
|
|
(ret -Symbol (-FS -top -bot)))
|
|
|
|
(check-equal?
|
|
(values->tc-results (make-Values (list (-result -Symbol (-FS -top -bot) (make-Path null '(0 0)))))
|
|
(list -empty-obj) (list Univ))
|
|
(ret -Symbol (-FS -top -bot)))
|
|
|
|
(check-equal?
|
|
(values->tc-results (make-Values (list (-result (-opt -Symbol) (-FS (-filter -String '(0 0)) -top))))
|
|
(list -empty-obj) (list Univ))
|
|
(ret (-opt -Symbol) -top-filter))
|
|
|
|
(check-equal?
|
|
(values->tc-results (make-Values (list (-result (-opt -Symbol) (-FS (-not-filter -String '(0 0)) -top))))
|
|
(list -empty-obj) (list Univ))
|
|
(ret (-opt -Symbol) -top-filter))
|
|
|
|
(check-equal?
|
|
(values->tc-results (make-Values (list (-result (-opt -Symbol) (-FS (-imp (-not-filter (-val #f) '(0 0))
|
|
(-not-filter -String #'x))
|
|
-top))))
|
|
(list -empty-obj) (list Univ))
|
|
(ret (-opt -Symbol) -top-filter))
|
|
|
|
(check-equal?
|
|
(values->tc-results (make-Values (list (-result (-opt -Symbol) (-FS (-not-filter -String '(0 0)) -top)
|
|
(make-Path null '(0 0)))))
|
|
(list (make-Path null #'x)) (list Univ))
|
|
(ret (-opt -Symbol) (-FS (-not-filter -String #'x) -top) (make-Path null #'x)))
|
|
|
|
;; Check additional filters
|
|
(check-equal?
|
|
(values->tc-results (make-Values (list (-result (-opt -Symbol) (-FS (-not-filter -String '(0 0)) -top)
|
|
(make-Path null '(0 0)))))
|
|
(list (make-Path null #'x)) (list -String))
|
|
(ret (-opt -Symbol) -false-filter (make-Path null #'x)))
|
|
|
|
;; Substitute into ranges correctly
|
|
(check-equal?
|
|
(values->tc-results (make-Values (list (-result (-opt (-> Univ -Boolean : (-FS (-filter -Symbol '(0 0)) -top))))))
|
|
(list (make-Path null #'x)) (list Univ))
|
|
(ret (-opt (-> Univ -Boolean : (-FS (-filter -Symbol '(0 0)) -top)))))
|
|
|
|
(check-equal?
|
|
(values->tc-results (make-Values (list (-result (-opt (-> Univ -Boolean : (-FS (-filter -Symbol '(1 0)) -top))))))
|
|
(list (make-Path null #'x)) (list Univ))
|
|
(ret (-opt (-> Univ -Boolean : (-FS (-filter -Symbol #'x) -top)))))
|
|
|
|
;; Substitute into filter of any values
|
|
(check-equal?
|
|
(values->tc-results (make-AnyValues (-filter -String '(0 0)))
|
|
(list (make-Path null #'x)) (list Univ))
|
|
(tc-any-results (-filter -String #'x)))
|
|
|
|
|
|
(check-equal?
|
|
(values->tc-results (-values-dots null (-> Univ -Boolean : (-FS (-filter -String '(1 0)) -top)) 'b)
|
|
(list (make-Path null #'x)) (list Univ))
|
|
(ret null null null (-> Univ -Boolean : (-FS (-filter -String #'x) -top)) 'b))
|
|
|
|
;; Filter is restricted by type of object
|
|
(check-equal?
|
|
(values->tc-results (make-Values (list (-result -Boolean (-FS (-filter -PosReal '(0 0)) (-filter -NonPosReal '(0 0))))))
|
|
(list (make-Path null #'x)) (list -Integer))
|
|
(ret -Boolean (-FS (-filter -PosInt #'x) (-filter -NonPosInt #'x))))
|
|
|
|
;; Filter restriction accounts for paths
|
|
(check-equal?
|
|
(values->tc-results
|
|
(make-Values
|
|
(list (-result -Boolean
|
|
(-FS (make-TypeFilter -PosReal
|
|
(make-Path (list -car) '(0 0)))
|
|
(make-TypeFilter -NonPosReal
|
|
(make-Path (list -car) '(0 0)))))))
|
|
(list (make-Path null #'x))
|
|
(list (-lst -Integer)))
|
|
(ret -Boolean
|
|
(-FS (make-TypeFilter -PosInt (make-Path (list -car) #'x))
|
|
(make-TypeFilter -NonPosInt (make-Path (list -car) #'x)))))
|
|
)
|
|
|
|
(test-suite "replace-names"
|
|
(check-equal?
|
|
(replace-names (list (list #'x (make-Path null (list 0 0))))
|
|
(ret Univ -top-filter (make-Path null #'x)))
|
|
(ret Univ -top-filter (make-Path null (list 0 0))))
|
|
(check-equal?
|
|
(replace-names (list (list #'x (make-Path null (list 0 0))))
|
|
(ret (-> Univ Univ : -top-filter : (make-Path null #'x))))
|
|
(ret (-> Univ Univ : -top-filter : (make-Path null (list 1 0)))))
|
|
)
|
|
))
|