www

Unnamed repository; edit this file 'description' to name the repository.
Log | Files | Refs | Submodules | README | LICENSE

list-test.rkt (6697B)


      1 #lang typed/racket
      2 (require "../typed-untyped.rkt")
      3 (define-typed/untyped-test-module
      4   (require-typed/untyped phc-toolkit/list
      5                          phc-toolkit/typed-rackunit)
      6   
      7   (check-equal?: (indexof 'c '(c)) 0)
      8   (check-equal?: (indexof 'c '(c a b c d a b c d)) 0)
      9   (check-equal?: (indexof 'c '(a b c d a b c d)) 2)
     10   (check-equal?: (indexof 'x '()) #f)
     11   (check-equal?: (indexof 'x '(c)) #f)
     12   (check-equal?: (indexof 'x '(c a b c d a b c d)) #f)
     13   (check-equal?: (indexof 'x '(a b c d a b c d)) #f)
     14 
     15   (define-syntax (skip<=6.6 stx)
     16     (syntax-case stx ()
     17       [(_ . rest)
     18        (if (or (regexp-match #px"^6(\\.[012345](\\..*|)|)$" (version))
     19                (regexp-match #px"^6.6$" (version))
     20                (regexp-match #px"^[123245]\\..*$" (version)))
     21            #'(begin)
     22            #'(begin . rest))]))
     23   
     24   ;; replace-first
     25   (skip<=6.6
     26     (check-equal?: (replace-first 'c 'r '(c)) '(r))
     27     (check-equal?: (replace-first 'c 'r '(c a b c d a b c d))
     28                    '(r a b c d a b c d))
     29     (check-equal?: (replace-first 'c 'r '(a b c d a b c d)) '(a b r d a b c d))
     30     (check-equal?: (replace-first 'x 'r '()) '())
     31     (check-equal?: (replace-first 'x 'r '(c)) '(c))
     32     (check-equal?: (replace-first 'x 'r '(c a b c d a b c d))
     33                    '(c a b c d a b c d))
     34     (check-equal?: (replace-first 'x 'r '(a b c d a b c d)) '(a b c d a b c d))
     35     
     36     (struct s ([a : Number]) #:transparent)
     37     (check-equal?: (replace-first (s 2) 'r (list (s 3) (s 2) (s 1) (s 2)))
     38                    (list (s 3) (s 2) (s 1) (s 2)))
     39     (check-equal?: (replace-first (s 2)
     40                                   'r
     41                                   (list (s 3) (s 2) (s 1) (s 2))
     42                                   equal?)
     43                    (list (s 3) 'r (s 1) (s 2)))
     44     
     45     (define-type (Test-List3-Maybe Start Mid End)
     46       (U (Pairof Start (Test-List3-Maybe Start Mid End))
     47          Null
     48          (Pairof Mid (Listof End))))
     49     
     50     (check-equal?: (replace-first (s 3) 'r (list (s 4) (s 3) (s 2) (s 1) (s 3)))
     51                    : (Test-List3-Maybe s 'r s)
     52                    (list (s 4) (s 3) (s 2) (s 1) (s 3)))
     53     
     54     (check-equal?: (replace-first (s 3) 'r (list (s 4) (s 3) (s 2) (s 1) (s 3)))
     55                    : (Rec R (U (Pairof s R)
     56                                Null
     57                                (Pairof 'r (Listof s))))
     58                    (list (s 4) (s 3) (s 2) (s 1) (s 3)))
     59     
     60     (check-equal?: (replace-first (s 3) 'r (list (s 4) (s 3) (s 2) (s 1) (s 3)))
     61                    : (List3-Maybe s 'r s)
     62                    (list (s 4) (s 3) (s 2) (s 1) (s 3)))
     63     
     64     (check-equal?: (replace-first 'r (list 'a 'b 'c 'a 'b 'c)
     65                                   (λ (x) (eq? x 'c)))
     66                    : (List3-Maybe (U 'a 'b) 'r (U 'a 'b 'c))
     67                    (list 'a 'b 'r 'a 'b 'c))
     68     
     69     ;; TR is not strong enough yet to infer the type to use, but at least we can
     70     ;; prove the result has the desired type without using casts:
     71     (check-equal?: ((inst (ann replace-first
     72                                (∀ (A B1 B2 C D)
     73                                   (→ C
     74                                      (Listof* A (U Null (Pairof B2 D)))
     75                                      (→ (U A B2) Any :
     76                                         #:+ (! A) ;; ∴ (and (! A) B2)
     77                                         #:- (! B2))
     78                                      (Listof* A (U Null (Pairof C D))))))
     79                           (U 'a 'b) Nothing 'c 'r (Listof (U 'd 'e)))
     80                     'r
     81                     (ann (list 'a 'b 'c 'd 'e)
     82                          (List3-Maybe (U 'a 'b) 'c (U 'd 'e)))
     83                     (λ (x) (eq? x 'c)))
     84                    : (List3-Maybe (U 'a 'b) 'r (U 'd 'e))
     85                    (list 'a 'b 'r 'd 'e))
     86     
     87     ;; TR is not strong enough yet to infer the type to use, but at least we can
     88     ;; prove the result has the desired type without using casts:
     89     (check-equal?: ((inst (ann replace-first
     90                                (∀ (A B1 B2 C D)
     91                                   (→ C
     92                                      (Listof* A (Pairof B2 D))
     93                                      (→ (U A B2) Any :
     94                                         #:+ (! A) ;; ∴ (and (! A) B2)
     95                                         #:- (! B2))
     96                                      (Listof* A (Pairof C D)))))
     97                           (U 'a 'b) Nothing 'c 'r (Listof (U 'd 'e)))
     98                     'r
     99                     (ann (list 'a 'b 'c 'd 'e)
    100                          (List3 (U 'a 'b) 'c (U 'd 'e)))
    101                     (λ (x) (eq? x 'c)))
    102                    : (List3 (U 'a 'b) 'r (U 'd 'e))
    103                    (list 'a 'b 'r 'd 'e))
    104     
    105     ;; TR is not strong enough yet to infer the type to use, but at least we can
    106     ;; prove the result has the desired type without using casts:
    107     (check-equal?: ((inst (ann replace-first
    108                                (∀ (A B1 B2 C D)
    109                                   (→ C
    110                                      (Listof* A (Pairof B2 D))
    111                                      (→ (U A B2) Any :
    112                                         #:+ (! A) ;; ∴ (and (! A) B2)
    113                                         #:- (! B2))
    114                                      (Listof* A (Pairof C D)))))
    115                           (U 'a 'b) Nothing 'c 'r (List))
    116                     'r
    117                     (ann (list 'a 'b 'c)
    118                          (Listof* (U 'a 'b) (List 'c)))
    119                     (λ (x) (eq? x 'c)))
    120                    : (Listof* (U 'a 'b) (List 'r))
    121                    (list 'a 'b 'r)))
    122   
    123   ;; map+fold
    124   (begin
    125     (check-equal?: (let-values ([(l a) (map+fold (λ ([e : Number] [a : Number])
    126                                                    (values (add1 e)
    127                                                            (+ a e)))
    128                                                  0
    129                                                  '(1 2 3 4 5))])
    130                      (list l a))
    131                    '((2 3 4 5 6) 15))
    132     
    133     (check-equal?: (let-values ([(l a) (map+fold (λ ([e : Number] [a : Number])
    134                                                    (values 1 2))
    135                                                  7
    136                                                  '())])
    137                      (list l a))
    138                    '(() 7))
    139     
    140     (check-equal?: (let-values ([(l a) (map+fold (λ ([e : Number] [a : Number])
    141                                                    (values 1 2))
    142                                                  7
    143                                                  '(3))])
    144                      (list l a))
    145                    '((1) 2))))