www

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

test-flexible-with2.rkt (1699B)

      1 #lang type-expander
      2 
      3 (require "../flexible-with2.hl.rkt"
      4          phc-toolkit/typed-rackunit-extensions)
      5 
      6 (check-ann ((record-builder 4 1 2 4 7 14) 'a 'b 'c 'd 'e)
      7            (Pairof
      8             (Pairof
      9              (Pairof (Pairof empty1/τ 'a) (Pairof 'b empty1/τ))
     10              (Pairof (Pairof 'c empty1/τ) (Pairof empty1/τ 'd)))
     11             (Pairof empty4/τ (Pairof empty2/τ (Pairof 'e empty1/τ)))))
     12 
     13 (with-ρ (Row)
     14   (define-type test
     15     (∀ρ (A #:ρ Row)
     16         (→ (List A Row)
     17            (record a b . Row)
     18            (List A Row)
     19            (record a c . Row)))))
     20 
     21 ;; TODO: I'm pretty sure that the lift-ing will cause some unbound identifier
     22 ;; or out of context id errors, when τ' refers to a locally-declared type.
     23 
     24 (with-ρ (Row)
     25   (define-type testf-τ (∀ρ (A #:ρ Row)
     26                            (→ (→ (List A Row)
     27                                  (record x y . Row)
     28                                  (List A Row)
     29                                  (record y z . Row))
     30                               Void)))
     31   (: testf
     32      (∀ρ (A #:ρ Row)
     33          (→ (→ (List A Row)
     34                (record x y . Row)
     35                (List A Row)
     36                (record y z . Row))
     37             Void)))
     38   (define (testf f)
     39     (: tmp (→ (record w x . Row) Any))
     40     (define (tmp r) r)
     41     (void)))
     42 
     43 (let ()
     44   (with-ρ (Row)
     45     (define-type Naht Integer)
     46     (: testf
     47        (∀ρ (A #:ρ Row)
     48            (→ (→ (List Naht A Row)
     49                  (record x y . Row)
     50                  (List Naht A Row)
     51                  (record y z . Row))
     52               Void)))
     53     (define (testf f)
     54       (: tmp (→ (record w x . Row) Any))
     55       (define (tmp r) r)
     56       (void)))
     57   testf)