www

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

test-constructor.rkt (4669B)

      1 #lang typed/racket
      2 
      3 (require phc-adt phc-toolkit type-expander typed/rackunit)
      4 (adt-init)
      5 
      6 ; (_ name:id *)
      7 (check-not-exn
      8  (λ ()
      9    (ann (constructor tag1 *)
     10         (∀ (A ...) (→ A ... A (tagged tag1 [values (List A ... A)]))))))
     11 
     12 (check-equal?: (constructor-values
     13                 (ann ((constructor tag1 *))
     14                      (constructor tag1)))
     15                '())
     16 (check-equal?: (constructor-values
     17                 (ann ((constructor tag1 *) 1)
     18                      (constructor tag1 One)))
     19                '(1))
     20 (check-equal?: (constructor-values
     21                 (ann ((constructor tag1 *) 1 "b")
     22                      (constructor tag1 Number String)))
     23                '(1 "b"))
     24 (check-equal?: (constructor-values
     25                 (ann ((constructor tag1 *) 1 "b" 'c)
     26                      (constructor tag1 Number String 'c)))
     27                '(1 "b" c))
     28 
     29 ; (_ name:id :colon)
     30 (check-not-exn (λ () (ann (constructor tag1 :)
     31                           (→ (constructor tag1)))))
     32 
     33 ; (_ name:id :colon T₀:expr)
     34 (check-not-exn (λ () (ann (constructor tag1 : Number)
     35                           (→ Number (constructor tag1 Number)))))
     36 
     37 ; (_ name:id :colon Tᵢ:expr …+)
     38 (check-not-exn
     39  (λ () (ann (constructor tag1 : Number String)
     40             (→ Number String (constructor tag1 Number String)))))
     41 (check-not-exn
     42  (λ () (ann (constructor tag1 : Number String 'c)
     43             (→ Number String 'c (constructor tag1 Number String 'c)))))
     44 
     45 ; Call (_ name:id :colon)
     46 (check-equal?: (constructor-values (ann ((constructor tag1 :))
     47                                         (constructor tag1)))
     48                '())
     49 
     50 ; Call (_ name:id :colon T₀:expr)
     51 (check-equal?: (constructor-values (ann ((constructor tag1 : Number) 1)
     52                                         (constructor tag1 Number)))
     53                '(1))
     54 
     55 ; Call (_ name:id :colon Tᵢ:expr …+)
     56 (check-equal?: (constructor-values
     57                 (ann ((constructor tag1 : Number String) 1 "b")
     58                      (constructor tag1 Number String)))
     59                '(1 "b"))
     60 (check-equal?: (constructor-values
     61                 (ann ((constructor tag1 : Number String 'c) 1 "b" 'c)
     62                      (constructor tag1 Number String 'c)))
     63                '(1 "b" c))
     64 
     65 ; (_ name:id [val₀:expr :colon T₀:expr])
     66 (check-equal?: (constructor-values
     67                 (ann (constructor tag1 [1 : One])
     68                      (constructor tag1 One)))
     69                '(1))
     70 
     71 ; (_ name:id [valᵢ:expr :colon Tᵢ:expr] …)
     72 (check-equal?: (constructor-values
     73                 (ann (constructor tag1 [1 : One] ["b" : (U "b" "B")])
     74                      (constructor tag1 One (U "b" "B"))))
     75                '(1 "b"))
     76 
     77 ; (_ name:id val₀:expr)
     78 (check-equal?: (constructor-values
     79                 (ann (constructor tag1 "a")
     80                      (constructor tag1 String)))
     81                '("a"))
     82 
     83 ; (_ name:id valᵢ:expr …)
     84 (check-equal?: (constructor-values
     85                 (ann (constructor tag1 "a" "b")
     86                      (constructor tag1 String String)))
     87                '("a" "b"))
     88 (check-equal?: (constructor-values
     89                 (ann (constructor tag1 "a" "b" 'c)
     90                      (constructor tag1 String String Symbol)))
     91                '("a" "b" c))
     92 
     93 (check-equal?: (constructor-values
     94                 (constructor tag1 "a" #(#\b 3) #t . "a"))
     95                : (List* "a" (Vector Char 3) #t "a")
     96                '("a" #(#\b 3) #t . "a"))
     97 
     98 (check-equal?: (constructor-values
     99                 (constructor tag1 "a" #(#\b 3) #t . #\b))
    100                : (List* "a" (Vector Char 3) #t Char)
    101                '("a" #(#\b 3) #t . #\b))
    102 
    103 (check-equal?: (constructor-values
    104                 (constructor tag1 "a" #(#\b 3) #t . 3))
    105                : (List* "a" (Vector Char 3) #t 3)
    106                '("a" #(#\b 3) #t . 3))
    107 
    108 (check-equal?: (constructor-values
    109                 (constructor tag1 "a" #(#\b 3) #t . #t))
    110                : (List* "a" (Vector Char 3) #t #t)
    111                '("a" #(#\b 3) #t . #t))
    112 
    113 (check-equal?: (constructor-values
    114                 (constructor tag1 "a" #(#\b 3) #t . #("x" #\y 26 #f)))
    115                : (List* "a" (Vector Char 3) #t (Vector "x" Char 26 #f))
    116                '("a" #(#\b 3) #t . #("x" #\y 26 #f)))
    117 
    118 (check-equal?: (constructor-values
    119                 (constructor tag1 "a" #(#\b 3) #t #("x" #\y 26 #f) . 123))
    120                : (List* "a" (Vector Char 3) #t (Vector "x" Char 26 #f) 123)
    121                '("a" #(#\b 3) #t #("x" #\y 26 #f) . 123))
    122 
    123 (check-equal?: (constructor-values
    124                 (constructor tag1 "a" #(#\b 3) #t #("x" #\y 26 #f)))
    125                : (List "a" (Vector Char 3) #t (Vector "x" Char 26 #f))
    126                '("a" #(#\b 3) #t #("x" #\y 26 #f)))