www

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

loop.mlish (2814B)

      1 #lang s-exp "../../mlish.rkt"
      2 (require "../rackunit-typechecking.rkt")
      3 
      4 ;; datatype with no self-reference
      5 (define-type (Test X)
      6   (A X) 
      7   (B X X))
      8 
      9 (typecheck-fail
     10     (define-type (Test2 X)
     11       (AA (Test2 X X)))
     12   #:with-msg "Improper use of constructor Test2; expected 1 args, got 2")
     13 
     14 (typecheck-fail
     15     (define-type (Test3 X)
     16       (AA (→)))
     17   #:with-msg "Improper usage of type constructor →")
     18 
     19 (typecheck-fail
     20     (define-type (Test4 X)
     21       (AA (+ 1 2)))
     22   #:with-msg "\\(\\+ 1 2\\) is not a valid type")
     23 
     24 (check-type (A 1) : (Test Int))
     25 (check-type (B 1 2) : (Test Int))
     26 
     27 (check-type
     28     (match (A 1) with
     29      [A x -> x]
     30      [B x y -> (+ x y)]) : Int -> 1)
     31 
     32 (check-type
     33     (match (B 1 2) with
     34      [A x -> x]
     35      [B x y -> (+ x y)]) : Int -> 3)
     36 
     37 ;; datatype with self-reference
     38 (define-type (Rec X)
     39   N
     40   (C X (Rec X)))
     41 
     42 ; check inferred and explicit instantiation versions
     43 (check-type N : (Rec Int) -> N)
     44 (check-type (N {Int}) : (Rec Int) -> (N {Int}))
     45 (check-type (C 1 N) : (Rec Int) -> (C 1 N))
     46 
     47 (check-type
     48     (match (N {Int}) with
     49      [N -> 0]
     50      [C x xs -> x]) : Int -> 0)
     51 
     52 (check-type
     53     (match (C 1 N) with
     54      [N -> 0]
     55      [C x xs -> x]) : Int -> 1)
     56 
     57 ;; mutually referential datatypes
     58 (define-type (Loop1 X)
     59   (L1 (Loop2 X)))
     60 (define-type (Loop2 X)
     61   (L2 (Loop1 X)))
     62 
     63 (define (looping-f [x : (Loop1 Y)] -> (Loop1 Y)) x)
     64 
     65 (define-type (ListA X)
     66   NA
     67   (CA X (ListB X)))
     68 (define-type (ListB X)
     69   NB
     70   (CB X (ListA X)))
     71 
     72 (typecheck-fail
     73     (define-type (ListC X)
     74       NC
     75       (CC X (ListA X X)))
     76   #:with-msg 
     77   "Improper usage of type constructor ListA: \\(ListA X X\\), expected = 1 arguments")
     78 
     79 (typecheck-fail (CA 1 NA))
     80 (check-type (CA 1 NB) : (ListA Int))
     81 (check-type (CA 1 (CB 2 NA)) : (ListA Int))
     82 (typecheck-fail (CA 1 (CB 2 NB)))
     83 (typecheck-fail (CB 1 NB))
     84 (check-type (CB 1 NA) : (ListB Int))
     85 (check-type (CB 1 (CA 2 NB)) : (ListB Int))
     86 (typecheck-fail (CB 1 (CA 2 NA)))
     87 
     88 (check-type
     89     (match (CA 1 NB) with
     90      [NA -> 0]
     91      [CA x xs -> x]) : Int -> 1)
     92 
     93 (check-type
     94     (match (CA 1 (CB 2 NA)) with
     95      [NA -> 0]
     96      [CA x xs ->
     97       (match xs with
     98        [NB -> 3]
     99        [CB x xs -> x])]) : Int -> 2)
    100 
    101 ;; "real world" mutually referential datatypes
    102 (define-type (BankersDeque A)
    103   [BD Int (List A) Int (List A)])
    104 
    105 (define-type (ImplicitCatDeque A)
    106   [Shallow (BankersDeque A)]
    107   [Deep (BankersDeque A)
    108         (ImplicitCatDeque (BankersDeque (CmpdElem (BankersDeque A))))
    109         (BankersDeque A)
    110         (ImplicitCatDeque (BankersDeque (CmpdElem (BankersDeque A))))
    111         (BankersDeque A)])
    112 
    113 (define-type (CmpdElem A)
    114   [Simple (BankersDeque A)]
    115   [Cmpd (BankersDeque A) 
    116         (ImplicitCatDeque 
    117           (BankersDeque (CmpdElem (BankersDeque A)))) (BankersDeque A)])
    118 
    119 (define (id (icd : (ImplicitCatDeque Int)) → (ImplicitCatDeque Int))
    120   icd)
    121