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 -String) (-FS -top (-not-filter -String '(0 0)))
|
|
(make-Path null '(0 0)))))
|
|
(list (make-Path null #'x)) (list -String))
|
|
(ret -String -true-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)))))
|
|
)
|
|
))
|