221 lines
8.1 KiB
Racket
221 lines
8.1 KiB
Racket
#lang racket/base
|
|
|
|
(require "test-utils.rkt"
|
|
rackunit racket/list racket/match racket/format
|
|
syntax/srcloc syntax/location
|
|
(types abbrev union tc-result)
|
|
(utils tc-utils)
|
|
(rep filter-rep object-rep type-rep)
|
|
(typecheck check-below)
|
|
(for-syntax racket/base syntax/parse))
|
|
|
|
(provide tests)
|
|
(gen-test-main)
|
|
|
|
;; Ensure that we never return a filter of NoFilter or an object of NoObject.
|
|
(define (check-filter f)
|
|
(match f
|
|
[(NoFilter:) (fail-check "Result has no filter (instead of a top filter).")]
|
|
[_ (void)]))
|
|
|
|
(define (check-object o)
|
|
(match o
|
|
[(NoObject:) (fail-check "Result has no object (instead of an empty object).")]
|
|
[_ (void)]))
|
|
|
|
(define (check-result result)
|
|
(match result
|
|
[(tc-results: ts fs os)
|
|
(for-each check-filter fs)
|
|
(for-each check-object os) ]
|
|
[(tc-results: ts fs os dty bound)
|
|
(for-each check-filter fs)
|
|
(for-each check-object os)]
|
|
[(tc-any-results: f)
|
|
(check-filter f)]
|
|
[(? Type/c?)
|
|
(void)]))
|
|
|
|
|
|
(define-syntax (test-below stx)
|
|
(syntax-parse stx
|
|
[(_ t1:expr t2:expr (~optional (~seq #:result expected-result:expr)
|
|
#:defaults [(expected-result #'t2)]))
|
|
#`(test-case (~a 't1 " <: " 't2)
|
|
(with-check-info (['location (build-source-location-list (quote-srcloc #,stx))]
|
|
['expected expected-result])
|
|
(define result (check-below t1 t2))
|
|
(with-check-info (['actual result])
|
|
(check-result result)
|
|
(unless (equal? expected-result result)
|
|
(fail-check "Check below did not return expected result.")))))]
|
|
[(_ #:fail (~optional message:expr #:defaults [(message #'#rx"type mismatch")])
|
|
t1:expr t2:expr
|
|
(~optional (~seq #:result expected-result:expr)
|
|
#:defaults [(expected-result #'t2)]))
|
|
#`(test-case (~a 't1 " !<: " 't2)
|
|
(with-check-info (['location (build-source-location-list (quote-srcloc #,stx))]
|
|
['expected expected-result])
|
|
(define result
|
|
(parameterize ([delay-errors? #t])
|
|
(check-below t1 t2)))
|
|
(with-check-info (['actual result])
|
|
(define exn
|
|
(let/ec exit
|
|
(with-handlers [(exn:fail? exit)]
|
|
(report-all-errors)
|
|
(fail-check "Check below did not fail."))))
|
|
(check-result result)
|
|
(unless (equal? expected-result result)
|
|
(fail-check "Check below did not return expected result."))
|
|
(check-regexp-match message (exn-message exn)))))]))
|
|
|
|
|
|
(define tests
|
|
(test-suite "Check Below"
|
|
(test-below -Bottom Univ)
|
|
(test-below #:fail -Symbol -String)
|
|
|
|
(test-below
|
|
(ret -Bottom)
|
|
(ret (list Univ Univ) (list -true-filter -no-filter) (list -no-obj -empty-obj))
|
|
#:result (ret (list Univ Univ) (list -true-filter -bot-filter) (list -empty-obj -empty-obj)))
|
|
|
|
(test-below
|
|
(ret -Bottom)
|
|
(ret (list Univ) (list -no-filter) (list -no-obj) Univ 'B)
|
|
#:result (ret (list Univ) (list -bot-filter) (list -empty-obj) Univ 'B))
|
|
|
|
;; Bottom is not below everything if the number of values doesn't match up.
|
|
(test-below #:fail
|
|
(ret (list -Bottom -Bottom))
|
|
(ret (list Univ) (list -true-filter) (list -no-obj))
|
|
#:result (ret (list Univ) (list -true-filter) (list -empty-obj)))
|
|
|
|
(test-below #:fail
|
|
(ret (list))
|
|
(ret (list Univ) (list -true-filter) (list -no-obj))
|
|
#:result (ret (list Univ) (list -true-filter) (list -empty-obj)))
|
|
|
|
(test-below
|
|
(ret (list -Symbol) (list -top-filter) (list -empty-obj))
|
|
(ret (list Univ) (list -no-filter) (list -no-obj))
|
|
#:result (ret (list Univ) (list -top-filter) (list -empty-obj)))
|
|
|
|
(test-below
|
|
(ret (list -Symbol) (list -true-filter) (list -empty-obj))
|
|
(ret (list Univ) (list -top-filter) (list -empty-obj)))
|
|
|
|
(test-below #:fail
|
|
(ret (list -Symbol) (list -top-filter) (list -empty-obj))
|
|
(ret (list Univ) (list -true-filter) (list -no-obj))
|
|
#:result (ret (list Univ) (list -true-filter) (list -empty-obj)))
|
|
|
|
(test-below #:fail #rx"no object"
|
|
(ret (list -Symbol) (list -top-filter) (list -empty-obj))
|
|
(ret (list Univ) (list -top-filter) (list (make-Path empty #'x))))
|
|
|
|
(test-below #:fail #rx"no object"
|
|
(ret (list -Symbol) (list -top-filter) (list -empty-obj))
|
|
(ret (list Univ) (list -true-filter) (list (make-Path empty #'x))))
|
|
|
|
(test-below (ret -Bottom) (tc-any-results -no-filter) #:result (tc-any-results -bot))
|
|
(test-below (ret Univ) (tc-any-results -top) #:result (tc-any-results -top))
|
|
(test-below (tc-any-results -bot) (tc-any-results -no-filter) #:result (tc-any-results -bot))
|
|
(test-below
|
|
(ret (list -Symbol -String) (list -true-filter -bot-filter))
|
|
(tc-any-results -no-filter)
|
|
#:result (tc-any-results -bot))
|
|
(test-below (ret -Symbol -bot-filter) (tc-any-results -no-filter) #:result (tc-any-results -bot))
|
|
|
|
(test-below (ret -Symbol -true-filter -empty-obj) (tc-any-results -no-filter)
|
|
#:result (tc-any-results -top))
|
|
(test-below (ret (list -Symbol -String)) (tc-any-results -no-filter)
|
|
#:result (tc-any-results -top))
|
|
(test-below
|
|
(ret (list -Symbol -String) (list -true-filter -false-filter) (list -empty-obj -empty-obj))
|
|
(tc-any-results -no-filter)
|
|
#:result (tc-any-results -top))
|
|
|
|
|
|
(test-below #:fail
|
|
(ret -Symbol)
|
|
(ret (list -Symbol -Symbol) (list -top-filter -no-filter) (list -no-obj -empty-obj))
|
|
#:result (ret (list -Symbol -Symbol) (list -top-filter -top-filter) (list -empty-obj -empty-obj)))
|
|
|
|
(test-below #:fail
|
|
(tc-any-results -top)
|
|
(ret -Symbol))
|
|
|
|
|
|
(test-below #:fail
|
|
(ret -Symbol -true-filter -empty-obj)
|
|
(ret -Symbol -true-filter -empty-obj Univ 'B))
|
|
|
|
(test-below #:fail
|
|
(ret -Symbol -true-filter -empty-obj Univ 'B)
|
|
(ret -Symbol -true-filter -empty-obj))
|
|
|
|
(test-below #:fail
|
|
(ret -Symbol)
|
|
(ret -Symbol -no-filter -empty-obj Univ 'B)
|
|
#:result (ret -Symbol -top-filter -empty-obj Univ 'B))
|
|
|
|
(test-below #:fail
|
|
(tc-any-results -top)
|
|
(ret -Symbol -no-filter -empty-obj Univ 'B)
|
|
#:result (ret (list -Symbol) (list -top-filter) (list -empty-obj) Univ 'B))
|
|
|
|
(test-below #:fail
|
|
(ret -Symbol -top-filter -empty-obj Univ 'B)
|
|
(ret (list -Symbol -Symbol) (list -top-filter -top-filter) (list -empty-obj -empty-obj) Univ 'B))
|
|
|
|
(test-below (ret -Symbol -true-filter -empty-obj Univ 'B)
|
|
(tc-any-results -no-filter)
|
|
#:result (tc-any-results -top))
|
|
|
|
(test-below
|
|
(ret -Symbol)
|
|
(ret -Symbol -no-filter -empty-obj)
|
|
#:result (ret -Symbol -top-filter -empty-obj))
|
|
|
|
(test-below
|
|
(ret -Symbol -true-filter)
|
|
(ret -Symbol -no-filter -empty-obj)
|
|
#:result (ret -Symbol -true-filter -empty-obj))
|
|
|
|
(test-below #:fail
|
|
(ret -Symbol -true-filter)
|
|
(ret (list Univ -Symbol) (list -no-filter -top-filter))
|
|
#:result (ret (list Univ -Symbol) (list -top-filter -top-filter)))
|
|
|
|
|
|
(test-below
|
|
(ret (list Univ) (list -true-filter) (list -empty-obj))
|
|
(ret Univ -no-filter)
|
|
#:result (ret (list Univ) (list -true-filter) (list -empty-obj)))
|
|
|
|
;; Enable these once check-below is fixed
|
|
;; Currently does not fail
|
|
#;
|
|
(test-below #:fail
|
|
(ret (list Univ) (list -top-filter) (list -empty-obj) Univ 'B)
|
|
(ret (list Univ) (list -false-filter) (list -no-obj) Univ 'B)
|
|
#:result (ret (list Univ) (list -false-filter) (list -empty-obj) Univ 'B))
|
|
|
|
;; Currently does not fail
|
|
#;
|
|
(test-below #:fail
|
|
(ret (list Univ) (list -top-filter) (list -empty-obj))
|
|
(ret (list Univ) (list -false-filter) (list -no-obj) Univ 'B)
|
|
#:result (ret (list Univ) (list -false-filter) (list -empty-obj) Univ 'B))
|
|
|
|
;; Currently does not fail
|
|
#;
|
|
(test-below #:fail
|
|
(ret (list Univ Univ) (list -top-filter -top-filter) (list -empty-obj -empty-obj))
|
|
(ret (list Univ Univ) (list -false-filter -false-filter) (list -no-obj -no-obj))
|
|
#:result (ret (list Univ Univ) (list -false-filter -false-filter) (list -empty-obj -empty-obj)))
|
|
|
|
))
|