www

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

okasaki.mlish (41459B)

      1 #lang s-exp "../../../mlish.rkt"
      2 (require "../../rackunit-typechecking.rkt")
      3 
      4 ;; TODO
      5 ;; - cannot inst polymorphic function `bq-empty`
      6 ;; - cannot inst `(BQ (Nil {A}) (Nil {A}))`
      7 ;; - cannot use bq-snoc directly in a foldl (need wrapper λ)
      8 
      9 ;; -----------------------------------------------------------------------------
     10 
     11 (define-type (Option A)
     12   [None]
     13   [Some A])
     14 
     15 ;; -----------------------------------------------------------------------------
     16 
     17 (define (div (n1 : Int) (n2 : Int) → Int)
     18   (if (< n1 n2)
     19     0
     20     (+ 1 (div (- n1 n2) n2))))
     21 
     22 (define (mod (n1 : Int) (n2 : Int) → Int)
     23   (if (< n1 n2)
     24     n1
     25     (mod (- n1 n2) n2)))
     26 
     27 ;; -----------------------------------------------------------------------------
     28 
     29 (define-type (List a)
     30   [Nil]
     31   [∷ a (List a)])
     32 
     33 (define (foldl [f : (→ A B A)] [acc : A] [x* : (List B)] → A)
     34   (match x* with
     35    [Nil -> acc]
     36    [∷ h t -> (foldl f (f acc h) t)]))
     37 
     38 (define (reverse [x* : (List A)] → (List A))
     39   (foldl (λ ([acc : (List A)] [x : A]) (∷ x acc)) Nil x*))
     40 
     41 (define (append [x* : (List A)] [y* : (List A)] → (List A))
     42   (match x* with
     43    [Nil -> y*]
     44    [∷ x x* ->
     45     (∷ x (append x* y*))]))
     46 
     47 (define (take [i : Int] [x* : (List A)] → (List A))
     48   (if (<= i 0)
     49     Nil
     50     (match x* with
     51      [Nil -> Nil]
     52      [∷ h t -> (∷ h (take (- i 1) t))])))
     53 
     54 (define (drop [i : Int] [x* : (List A)] → (List A))
     55   (if (<= i 0)
     56     x*
     57     (match x* with
     58      [Nil -> Nil]
     59      [∷ h t -> (drop (- i 1) t)])))
     60 
     61 ;; =============================================================================
     62 ;; === BatchedQueue
     63 
     64 (define-type (BatchedQueue A)
     65   [BQ (List A) (List A)])
     66 
     67 (define (bq-check [f : (List A)] [r : (List A)] → (BatchedQueue A))
     68   (match f with
     69    [Nil -> (BQ (reverse r) Nil)]
     70    [∷ h t -> (BQ f r)]))
     71 
     72 (define (bq-empty → (BatchedQueue A))
     73   (BQ Nil Nil))
     74 
     75 (define (bq-isEmpty [bq : (BatchedQueue A)] → Bool)
     76   (match bq with
     77    [BQ f r ->
     78     (match f with
     79      [Nil -> #t]
     80      [∷ h t -> #f])]))
     81 
     82 (define (bq-snoc [bq : (BatchedQueue A)] [x : A] → (BatchedQueue A))
     83   (match bq with
     84    [BQ f r -> (bq-check f (∷ x r))]))
     85 
     86 (define (bq-head [bq : (BatchedQueue A)] → (Option A))
     87   (match bq with
     88    [BQ f r ->
     89     (match f with
     90      [Nil -> None]
     91      [∷ h t -> (Some h)])]))
     92 
     93 (define (bq-tail [bq : (BatchedQueue A)] → (Option (BatchedQueue A)))
     94   (match bq with
     95    [BQ f* r* ->
     96     (match f* with
     97      [Nil -> None]
     98      [∷ x f* ->
     99       (Some (bq-check f* r*))])]))
    100 
    101 (define (list->bq [x* : (List A)] → (BatchedQueue A))
    102   (foldl
    103     ;bq-snoc ;; TODO
    104     (λ ([q : (BatchedQueue A)] [x : A]) (bq-snoc q x))
    105     (bq-empty) x*))
    106 
    107 ;; -----------------------------------------------------------------------------
    108 
    109 (define digit*
    110   (∷ 1 (∷ 2 (∷ 3 (∷ 4 (∷ 5 (∷ 6 (∷ 7 (∷ 8 (∷ 9 Nil))))))))))
    111 
    112 (define abc
    113   (∷ "A" (∷ "B" (∷ "C" Nil))))
    114 
    115 (define def
    116   (∷ "D" (∷ "E" (∷ "F" Nil))))
    117 
    118 (define sample-bq (list->bq digit*))
    119 
    120 (check-type
    121   (bq-isEmpty (BQ (Nil {Bool}) (Nil {Bool})))
    122   ;(bq-isEmpty (bq-empty {Bool}))
    123   ;(bq-isEmpty (BQ (Nil {Bool}) (Nil {Bool}))) ;; TODO
    124   : Bool
    125   ⇒ #t)
    126 
    127 (check-type
    128   (bq-isEmpty sample-bq)
    129   : Bool
    130   ⇒ #f)
    131 
    132 (check-type
    133   (bq-head sample-bq)
    134   : (Option Int)
    135   ⇒ (Some 1))
    136 
    137 (check-type
    138   (bq-head (bq-snoc sample-bq 10))
    139   : (Option Int)
    140   ⇒ (Some 1))
    141 
    142 (define (>> [f : (→ A (Option A))] [x : (Option A)] → (Option A))
    143   (match x with
    144    [None -> None]
    145    [Some y -> (f y)]))
    146 
    147 (check-type
    148   (match (bq-tail sample-bq) with
    149    [None -> None]
    150    [Some bq -> (bq-head bq)])
    151   : (Option Int)
    152   ⇒ (Some 2))
    153 
    154 ;; TODO
    155 ;(check-type
    156 ;  (>> bq-head (>> bq-tail (>> bq-tail (>> bq-tail (Some sample-bq)))))
    157 ;  : (Option Int)
    158 ;  ⇒ (Some 4))
    159 
    160 ;; =============================================================================
    161 ;; === Bankers Queue
    162 
    163 (define-type (BankersQueue A)
    164   (Bank Int (List A) Int (List A)))
    165 
    166 (define (bank-check [lenf : Int] [f : (List A)] [lenr : Int] [r : (List A)] → (BankersQueue A))
    167   (if (<= lenr lenf)
    168     (Bank lenf f lenr r)
    169     (Bank (+ lenf lenr) (append f (reverse r)) 0 Nil)))
    170 
    171 (define (bank-empty → (BankersQueue A))
    172   (Bank 0 Nil 0 Nil))
    173 
    174 (define (bank-isEmpty [bq : (BankersQueue A)] → Bool)
    175   (match bq with
    176    [Bank lenf f lenr r -> (= 0 lenf)]))
    177 
    178 (define (bank-snoc [bq : (BankersQueue A)] [x : A] → (BankersQueue A))
    179   (match bq with
    180    [Bank lenf f lenr r -> (bank-check lenf f (+ 1 lenr) (∷ x r))]))
    181 
    182 (define (bank-head [bq : (BankersQueue A)] → (Option A))
    183   (match bq with
    184    [Bank lenf f lenr r ->
    185     (match f with
    186      [Nil -> None]
    187      [∷ h t -> (Some h)])]))
    188 
    189 (define (bank-tail [bq : (BankersQueue A)] → (Option (BankersQueue A)))
    190   (match bq with
    191    [Bank lenf f lenr r ->
    192     (match f with
    193      [Nil -> None]
    194      [∷ h t -> (Some (bank-check (- lenf 1) t lenr r))])]))
    195 
    196 ;; -----------------------------------------------------------------------------
    197 
    198 (define sample-bank
    199   (foldl (λ ([acc : (BankersQueue Int)] [x : Int]) (bank-snoc acc x)) (bank-empty) digit*))
    200 
    201 (check-type
    202   (bank-isEmpty (Bank 0 (Nil {Int}) 0 (Nil {Int})))
    203   : Bool
    204   ⇒ #t)
    205 
    206 (check-type
    207   (bank-isEmpty sample-bank)
    208   : Bool
    209   ⇒ #f)
    210 
    211 (check-type
    212   (bank-head sample-bank)
    213   : (Option Int)
    214   ⇒ (Some 1))
    215 
    216 (check-type
    217   (bank-head (bank-snoc sample-bank 10))
    218   : (Option Int)
    219   ⇒ (Some 1))
    220 
    221 (check-type
    222   (match (bank-tail sample-bank) with
    223    [None -> None]
    224    [Some bank -> (bank-head bank)])
    225   : (Option Int)
    226   ⇒ (Some 2))
    227 
    228 ;; =============================================================================
    229 ;; === Physicists Queue
    230 
    231 (define-type (PhysicistsQueue A)
    232   (PQ (List A) Int (List A) Int (List A)))
    233 
    234 (define (pq-check [w : (List A)] [lenf : Int] [f : (List A)] [lenr : Int] [r : (List A)] → (PhysicistsQueue A))
    235   (if (<= lenr lenf)
    236     (pq-checkw w lenf f lenr r)
    237     (pq-checkw f (+ lenf lenr) (append f (reverse r)) 0 Nil)))
    238 
    239 (define (pq-checkw [w : (List A)] [lenf : Int] [f : (List A)] [lenr : Int] [r : (List A)] → (PhysicistsQueue A))
    240   (match w with
    241    [Nil -> (PQ f lenf f lenr r)]
    242    [∷ h t -> (PQ w lenf f lenr r)]))
    243 
    244 (define (pq-empty → (PhysicistsQueue A))
    245   (PQ Nil 0 Nil 0 Nil))
    246 
    247 (define (pq-isEmpty [pq : (PhysicistsQueue A)] → Bool)
    248   (match pq with
    249    [PQ w lenf f lenr r ->
    250     (= lenf 0)]))
    251 
    252 (define (pq-snoc [pq : (PhysicistsQueue A)] [x : A] → (PhysicistsQueue A))
    253   (match pq with
    254    [PQ w lenf f lenr r -> (pq-check w lenf f (+ 1 lenr) (∷ x r))]))
    255 
    256 (define (pq-head [pq : (PhysicistsQueue A)] → (Option A))
    257   (match pq with
    258    [PQ w lenf f lenr r ->
    259     (match w with
    260      [Nil -> None]
    261      [∷ w w* -> (Some w)])]))
    262 
    263 (define (pq-tail [pq : (PhysicistsQueue A)] → (Option (PhysicistsQueue A)))
    264   (match pq with
    265    [PQ w lenf f lenr r ->
    266     (match w with
    267      [Nil -> None]
    268      [∷ x w* ->
    269       (match f with
    270        [Nil -> None] ;; Never happens
    271        [∷ f f* -> (Some (pq-check w* (- lenf 1) f* lenr r))])])]))
    272 
    273 ;; -----------------------------------------------------------------------------
    274 
    275 (define sample-pq
    276   (foldl (λ ([acc : (PhysicistsQueue Int)] [x : Int]) (pq-snoc acc x)) (pq-empty) digit*))
    277 
    278 (check-type
    279   (pq-isEmpty (PQ (Nil {Int}) 0 (Nil {Int}) 0 (Nil {Int})))
    280   : Bool
    281   ⇒ #t)
    282 
    283 (check-type
    284   (pq-isEmpty sample-pq)
    285   : Bool
    286   ⇒ #f)
    287 
    288 (check-type
    289   (pq-head sample-pq)
    290   : (Option Int)
    291   ⇒ (Some 1))
    292 
    293 (check-type
    294   (pq-head (pq-snoc sample-pq 10))
    295   : (Option Int)
    296   ⇒ (Some 1))
    297 
    298 (check-type
    299   (match (pq-tail sample-pq) with
    300    [None -> None]
    301    [Some pq -> (pq-head pq)])
    302   : (Option Int)
    303   ⇒ (Some 2))
    304 
    305 ;; =============================================================================
    306 ;; === Hood-Melville Queue
    307 
    308 (define-type (RotationState A)
    309   [Idle]
    310   [Reversing Int (List A) (List A) (List A) (List A)]
    311   [Appending Int (List A) (List A)]
    312   [Done (List A)])
    313 
    314 (define-type (HoodMelvilleQueue A)
    315   [HM Int (List A) (RotationState A) Int (List A)])
    316 
    317 (define (hm-exec [rs : (RotationState A)] → (RotationState A))
    318   (match rs with
    319    [Idle -> rs]
    320    [Done x -> rs]
    321    [Appending ok f* r* ->
    322     (if (= ok 0)
    323       (Done r*)
    324       (match f* with
    325        [Nil -> rs]
    326        [∷ x f* ->
    327         (Appending (- ok 1) f* (∷ x r*))]))]
    328    [Reversing ok f1* f2* r1* r2* ->
    329     (match f1* with
    330      [Nil ->
    331       (match r1* with
    332        [Nil -> rs]
    333        [∷ y r1* ->
    334         (match r1* with
    335          [Nil -> (Appending ok f2* (∷ y r2*))]
    336          [∷ a b -> rs])])]
    337      [∷ x f1* ->
    338       (match r1* with
    339        [Nil -> rs]
    340        [∷ y r1* ->
    341         (Reversing (+ ok 1) f1* (∷ x f2*) r1* (∷ y r2*))])])]))
    342 
    343 (define (hm-invalidate [rs : (RotationState A)] → (RotationState A))
    344   (match rs with
    345    [Reversing ok f1* f2* r1* r2* ->
    346     (Reversing (- ok 1) f1* f2* r1* r2*)]
    347    [Appending ok f* r* ->
    348      (if (= 0 ok)
    349        (match r* with
    350         [Nil -> rs]
    351         [∷ x r* -> (Done r*)])
    352        (Appending (- ok 1) f* r*))]
    353    [Done x -> rs]
    354    [Idle -> rs]))
    355 
    356 (define (hm-exec2 [lenf : Int] [f* : (List A)] [state : (RotationState A)] [lenr : Int] [r : (List A)] → (HoodMelvilleQueue A))
    357   ((λ ([newstate : (RotationState A)])
    358      (match newstate with
    359       [Done newf -> (HM lenf newf Idle lenr r)]
    360       [Idle                -> (HM lenf f* newstate lenr r)]
    361       [Appending a b c     -> (HM lenf f* newstate lenr r)]
    362       [Reversing a b c d e -> (HM lenf f* newstate lenr r)]))
    363   (hm-exec (hm-exec state))))
    364 
    365 (define (hm-check [lenf : Int] [f* : (List A)] [state : (RotationState A)] [lenr : Int] [r* : (List A)] → (HoodMelvilleQueue A))
    366   (if (<= lenr lenf)
    367     (hm-exec2 lenf f* state lenr r*)
    368     (hm-exec2 (+ lenf lenr) f* (Reversing 0 f* Nil r* Nil) 0 Nil)))
    369 
    370 (define (hm-empty → (HoodMelvilleQueue A))
    371   (HM 0 Nil Idle 0 Nil))
    372 
    373 (define (hm-isEmpty [hm : (HoodMelvilleQueue A)] → Bool)
    374   (match hm with
    375    [HM lenf b c d e ->
    376     (= lenf 0)]))
    377 
    378 (define (hm-snoc [hm : (HoodMelvilleQueue A)] [x : A] → (HoodMelvilleQueue A))
    379   (match hm with
    380    [HM lenf f state lenr r -> (hm-check lenf f state (+ lenr 1) (∷ x r))]))
    381 
    382 (define (hm-head [hm : (HoodMelvilleQueue A)] → (Option A))
    383   (match hm with
    384    [HM a f b c d ->
    385     (match f with
    386      [Nil -> None]
    387      [∷ x f* -> (Some x)])]))
    388 
    389 (define (hm-tail [hm : (HoodMelvilleQueue A)] → (Option (HoodMelvilleQueue A)))
    390   (match hm with
    391    [HM lenf f state lenr r ->
    392     (match f with
    393      [Nil -> None]
    394      [∷ x f* -> (Some (hm-check (- lenf 1) f* (hm-invalidate state) lenr r))])]))
    395 
    396 ;; -----------------------------------------------------------------------------
    397 
    398 (define sample-hm
    399   (foldl (λ ([acc : (HoodMelvilleQueue Int)] [x : Int]) (hm-snoc acc x)) (hm-empty) digit*))
    400 
    401 (check-type
    402   (hm-isEmpty (HM 0 (Nil {Int}) Idle 0 (Nil {Int})))
    403   : Bool
    404   ⇒ #t)
    405 
    406 (check-type
    407   (hm-isEmpty sample-hm)
    408   : Bool
    409   ⇒ #f)
    410 
    411 (check-type
    412   (hm-head sample-hm)
    413   : (Option Int)
    414   ⇒ (Some 1))
    415 
    416 (check-type
    417   (hm-head (hm-snoc sample-hm 10))
    418   : (Option Int)
    419   ⇒ (Some 1))
    420 
    421 (check-type
    422   (match (hm-tail sample-hm) with
    423    [None -> None]
    424    [Some hm -> (hm-head hm)])
    425   : (Option Int)
    426   ⇒ (Some 2))
    427 
    428 ;; =============================================================================
    429 ;; === Bootstrapped Queue
    430 
    431 (define-type (BootstrappedQueue a)
    432   [E]
    433   [Q Int (List a) (BootstrappedQueue (List a)) Int (List a)])
    434 
    435 (define (bs-checkQ [lenfm : Int] [f : (List A)] [m : (BootstrappedQueue (List A))] [lenr : Int] [r : (List A)] → (BootstrappedQueue A))
    436   (if (<= lenr lenfm)
    437     (bs-checkF lenfm f m lenr r)
    438     (bs-checkF (+ lenfm lenr) f (bs-snoc m (reverse r)) 0 Nil)))
    439 
    440 (define (bs-checkF [lenfm : Int] [f : (List A)] [m : (BootstrappedQueue (List A))] [lenr : Int] [r : (List A)] → (BootstrappedQueue A))
    441   (match f with
    442    [Nil ->
    443     (match m with
    444      [E -> E]
    445      [Q _a _b _c _d _e ->
    446       (match (bs-head m) with
    447        [None -> E]
    448        [Some hd ->
    449         (match (bs-tail m) with
    450          [None -> E]
    451          [Some tl ->
    452           (Q lenfm hd tl lenr r)])])])]
    453    [∷ _f _f* ->
    454     (Q lenfm f m lenr r)]))
    455 
    456 (define (bs-empty → (BootstrappedQueue A))
    457   (Q 0 Nil E 0 Nil))
    458 
    459 (define (bs-isEmpty [m : (BootstrappedQueue A)] → Bool)
    460   (match m with
    461    [E -> #t]
    462    [Q a b c d e -> #f]))
    463 
    464 (define (bs-snoc [m : (BootstrappedQueue A)] [x : A] → (BootstrappedQueue A))
    465   (match m with
    466    [E -> (Q 1 (∷ x Nil) E 0 Nil)]
    467    [Q lenfm f m lenr r -> (bs-checkQ lenfm f m (+ 1 lenr) (∷ x r))]))
    468 
    469 (define (bs-head [m : (BootstrappedQueue A)] → (Option A))
    470   (match m with
    471    [E -> None]
    472    [Q lenfm f m lenr r ->
    473     (match f with
    474      [Nil -> None]
    475      [∷ x f* -> (Some x)])]))
    476 
    477 (define (bs-tail [m : (BootstrappedQueue A)] → (Option (BootstrappedQueue A)))
    478   (match m with
    479    [E -> None]
    480    [Q lenfm f m lenr r ->
    481     (match f with
    482      [Nil -> None]
    483      [∷ _x f* -> (Some (bs-checkQ (- lenfm 1) f* m lenr r))])]))
    484 
    485 ;; -----------------------------------------------------------------------------
    486 
    487 (define sample-bs
    488   (foldl (λ ([acc : (BootstrappedQueue Int)] [x : Int]) (bs-snoc acc x)) (bs-empty) digit*))
    489 
    490 (check-type
    491   (bs-isEmpty (E {Int}))
    492   : Bool
    493   ⇒ #t)
    494 
    495 (check-type
    496   (bs-isEmpty sample-bs)
    497   : Bool
    498   ⇒ #f)
    499 
    500 (check-type
    501   (bs-head sample-bs)
    502   : (Option Int)
    503   ⇒ (Some 1))
    504 
    505 (check-type
    506   (bs-head (bs-snoc sample-bs 10))
    507   : (Option Int)
    508   ⇒ (Some 1))
    509 
    510 (check-type
    511   (match (bs-tail sample-bs) with
    512    [None -> None]
    513    [Some bs -> (bs-head bs)])
    514   : (Option Int)
    515   ⇒ (Some 2))
    516 
    517 ;; =============================================================================
    518 ;; === Implicit Queue
    519 
    520 (define-type (Digit A)
    521   [Zero]
    522   [One A]
    523   [Two A A])
    524 
    525 (define-type (ImplicitQueue A)
    526   [Shallow (Digit A)]
    527   [Deep (Digit A) (ImplicitQueue (× A A)) (Digit A)])
    528 
    529 (define (iq-empty → (ImplicitQueue A))
    530   (Shallow Zero))
    531 
    532 (define (iq-isEmpty [iq : (ImplicitQueue A)] → Bool)
    533   (match iq with
    534    [Shallow d ->
    535     (match d with
    536      [Zero -> #t]
    537      [One x -> #f]
    538      [Two x y -> #f])]
    539    [Deep a b c -> #f]))
    540 
    541 (define (iq-snoc [iq : (ImplicitQueue A)] [y : A] → (ImplicitQueue A))
    542   (match iq with
    543    [Shallow d ->
    544     (match d with
    545      [Zero -> (Shallow (One y))]
    546      [One x -> (Deep (Two x y) (Shallow Zero) Zero)]
    547      [Two x y -> ;; Error
    548       (Shallow Zero)])]
    549    [Deep f m d ->
    550     (match d with
    551      [Zero -> (Deep f m (One y))]
    552      [One x -> (Deep f (iq-snoc m (tup x y)) Zero)]
    553      [Two x y -> (Shallow Zero)])])) ;; Error
    554 
    555 (define (iq-head [iq : (ImplicitQueue A)] → (Option A))
    556   (match iq with
    557    [Shallow d ->
    558     (match d with
    559      [Zero -> None]
    560      [One x -> (Some x)]
    561      [Two x y -> (Some x)])] ;; Error
    562    [Deep d m r ->
    563     (match d with
    564      [Zero -> None] ;; Error
    565      [One x -> (Some x)]
    566      [Two x y -> (Some x)])]))
    567 
    568 (define (iq-tail [iq : (ImplicitQueue A)] → (Option (ImplicitQueue A)))
    569   (match iq with
    570    [Shallow d ->
    571     (match d with
    572      [Zero -> None]
    573      [One x -> (Some (Shallow Zero))]
    574      [Two x y -> None])] ;; Error
    575    [Deep d m r ->
    576     (match d with
    577      [Zero -> None] ;; Error
    578      [One x ->
    579       (match (iq-head m) with
    580        [None -> (Some (Shallow r))]
    581        [Some yz ->
    582         (match yz with
    583          [y z ->
    584           (match (iq-tail m) with
    585            [None -> None]
    586            [Some tl ->
    587             (Some (Deep (Two y z) tl r))])])])]
    588      [Two x y -> (Some (Deep (One y) m r))])]))
    589 
    590 ;; -----------------------------------------------------------------------------
    591 
    592 (define sample-iq
    593   (foldl (λ ([acc : (ImplicitQueue Int)] [x : Int]) (iq-snoc acc x)) (iq-empty) digit*))
    594 
    595 (check-type
    596   (iq-isEmpty (Shallow (Zero {Int})))
    597   : Bool
    598   ⇒ #t)
    599 
    600 (check-type
    601   (iq-isEmpty sample-iq)
    602   : Bool
    603   ⇒ #f)
    604 
    605 (check-type
    606   (iq-head sample-iq)
    607   : (Option Int)
    608   ⇒ (Some 1))
    609 
    610 (check-type
    611   (iq-head (iq-snoc sample-iq 10))
    612   : (Option Int)
    613   ⇒ (Some 1))
    614 
    615 (check-type
    616   (match (iq-tail sample-iq) with
    617    [None -> None]
    618    [Some iq -> (iq-head iq)])
    619   : (Option Int)
    620   ⇒ (Some 2))
    621 
    622 ;; =============================================================================
    623 ;; === Bankers Deque
    624 
    625 (define-type (BankersDeque A)
    626   [BD Int (List A) Int (List A)])
    627 
    628 (define c 3)
    629 
    630 (define (bd-check [lenf : Int] [f : (List A)] [lenr : Int] [r : (List A)] → (BankersDeque A))
    631   (if (> lenf (+ c (+ lenr 1)))
    632     (let* ([i (div (+ lenf lenr) 2)]
    633            [j (- (+ lenf lenr) i)]
    634            [r2 (take j r)]
    635            [f2 (append f (reverse (drop j r)))])
    636       (BD i f2 j r2))
    637     (if (> lenr (+ 1 (* c lenf)))
    638       (let* ([j (div (+ lenf lenr) 2)]
    639              [i (- (+ lenr lenf) j)]
    640              [r2 (take j r)]
    641              [f2 (append f (reverse (drop j r)))])
    642         (BD i f2 j r2))
    643       (BD lenf f lenr r))))
    644 
    645 (define (bd-empty → (BankersDeque A))
    646   (BD 0 Nil 0 Nil))
    647 
    648 (define (bd-isEmpty [bd : (BankersDeque A)] → Bool)
    649   (match bd with
    650    [BD lenf f lenr r -> (= 0 (+ lenf lenr))]))
    651 
    652 (define (bd-cons [x : A] [bd : (BankersDeque A)] → (BankersDeque A))
    653   (match bd with
    654    [BD lenf f lenr r -> (bd-check (+ lenf 1) (∷ x f) lenr r)]))
    655 
    656 (define (bd-head [bd : (BankersDeque A)] → (Option A))
    657   (match bd with
    658    [BD lenf f lenr r ->
    659     (match f with
    660      [Nil -> None]
    661      [∷ x f2 -> (Some x)])]))
    662 
    663 (define (bd-tail [bd : (BankersDeque A)] → (Option (BankersDeque A)))
    664   (match bd with
    665    [BD lenf f lenr r ->
    666     (match f with
    667      [Nil -> None]
    668      [∷ x f2 -> (Some (bd-check (- lenf 1) f2 lenr r))])]))
    669 
    670 (define (bd-snoc [bd : (BankersDeque A)] [x : A] → (BankersDeque A))
    671   (match bd with
    672    [BD lenf f lenr r -> (bd-check lenf f (+ lenr 1) (∷ x r))]))
    673 
    674 (define (bd-last [bd : (BankersDeque A)] → (Option A))
    675   (match bd with
    676    [BD lenf f lenr r ->
    677     (match r with
    678      [Nil -> None]
    679      [∷ x r2 -> (Some x)])]))
    680 
    681 (define (bd-init [bd : (BankersDeque A)] → (Option (BankersDeque A)))
    682   (match bd with
    683    [BD lenf f lenr r ->
    684     (match r with
    685      [Nil -> None]
    686      [∷ x r -> (Some (bd-check lenf f (- lenr 1) r))])]))
    687 
    688 ;; -----------------------------------------------------------------------------
    689 
    690 (define sample-bd
    691   (foldl (λ ([acc : (BankersDeque Int)] [x : Int]) (bd-snoc acc x)) (bd-empty) digit*))
    692 
    693 (check-type
    694   (bd-isEmpty (BD 0 (Nil {Int}) 0 (Nil {Int})))
    695   : Bool
    696   ⇒ #t)
    697 
    698 (check-type
    699   (bd-isEmpty sample-bd)
    700   : Bool
    701   ⇒ #f)
    702 
    703 (check-type
    704   (bd-head sample-bd)
    705   : (Option Int)
    706   ⇒ (Some 1))
    707 
    708 (check-type
    709   (bd-last sample-bd)
    710   : (Option Int)
    711   ⇒ (Some 9))
    712 
    713 (check-type
    714   (bd-head (bd-snoc sample-bd 10))
    715   : (Option Int)
    716   ⇒ (Some 1))
    717 
    718 (check-type
    719   (bd-head (bd-cons 10 sample-bd))
    720   : (Option Int)
    721   ⇒ (Some 10))
    722 
    723 (check-type
    724   (match (bd-tail sample-bd) with
    725    [None -> None]
    726    [Some bd -> (bd-head bd)])
    727   : (Option Int)
    728   ⇒ (Some 2))
    729 
    730 (check-type
    731   (match (bd-init sample-bd) with
    732    [None -> None]
    733    [Some bd -> (bd-last bd)])
    734   : (Option Int)
    735   ⇒ (Some 8))
    736 
    737 ;; =============================================================================
    738 ;; === Simple Catenable Deque
    739 
    740 (define-type (SimpleCatDeque a)
    741   [SShallow (BankersDeque a)]
    742   [SDeep (BankersDeque a) (SimpleCatDeque (BankersDeque a)) (BankersDeque a)])
    743 
    744 (define (bd-tooSmall [d : (BankersDeque A)] → Bool)
    745   (if (bd-isEmpty d)
    746     #t
    747     (match (bd-tail d) with
    748      [None -> #t]
    749      [Some d -> (bd-isEmpty d)])))
    750 
    751 (define (bd-dappendL [d1 : (BankersDeque A)] [d2 : (BankersDeque A)] → (BankersDeque A))
    752   (match (bd-head d1) with
    753    [None -> d2]
    754    [Some h -> (bd-cons h d2)]))
    755 
    756 (define (bd-dappendR [d1 : (BankersDeque A)] [d2 : (BankersDeque A)] → (BankersDeque A))
    757   (match (bd-head d2) with
    758    [None -> d1]
    759    [Some h -> (bd-snoc d1 h)]))
    760 
    761 (define (scd-empty → (SimpleCatDeque A))
    762   (SShallow (bd-empty)))
    763 
    764 (define (scd-isEmpty [scd : (SimpleCatDeque A)] → Bool)
    765   (match scd with
    766    [SShallow d -> (bd-isEmpty d)]
    767    [SDeep a b c -> #f]))
    768 
    769 (define (scd-cons [x : A] [scd : (SimpleCatDeque A)] → (SimpleCatDeque A))
    770   (match scd with
    771    [SShallow d -> (SShallow (bd-cons x d))]
    772    [SDeep f m r -> (SDeep (bd-cons x f) m r)]))
    773 
    774 (define (scd-snoc [scd : (SimpleCatDeque A)] [x : A] → (SimpleCatDeque A))
    775   (match scd with
    776    [SShallow d -> (SShallow (bd-snoc d x))]
    777    [SDeep f m r -> (SDeep f m (bd-snoc f x))]))
    778 
    779 (define (scd-head [scd : (SimpleCatDeque A)] → (Option A))
    780   (match scd with
    781    [SShallow d -> (bd-head d)]
    782    [SDeep f m r -> (bd-head f)]))
    783 
    784 (define (scd-last [scd : (SimpleCatDeque A)] → (Option A))
    785   (match scd with
    786    [SShallow d -> (bd-last d)]
    787    [SDeep f m r -> (bd-last r)]))
    788 
    789 (define (scd-tail [scd : (SimpleCatDeque A)] → (Option (SimpleCatDeque A)))
    790   (match scd with
    791    [SShallow d ->
    792     (match (bd-tail d) with
    793      [None -> None]
    794      [Some t -> (Some (SShallow t))])]
    795    [SDeep f m r ->
    796     (match (bd-tail f) with
    797      [None -> None]
    798      [Some f2 ->
    799       (if (not (bd-tooSmall f2))
    800         (Some (SDeep f2 m r))
    801         (if (scd-isEmpty m)
    802           (Some (SShallow (bd-dappendL f2 r)))
    803           (match (scd-head m) with
    804            [None -> None]
    805            [Some hm ->
    806             (match (scd-tail m) with
    807              [None -> None]
    808              [Some tm ->
    809               (Some (SDeep (bd-dappendL f2 hm) tm r))])])))])]))
    810 
    811 (define (scd-init [scd : (SimpleCatDeque A)] → (Option (SimpleCatDeque A)))
    812   (match scd with
    813    [SShallow d ->
    814     (match (bd-init d) with
    815      [None -> None]
    816      [Some t -> (Some (SShallow t))])]
    817    [SDeep f m r ->
    818     (match (bd-init r) with
    819      [None -> None]
    820      [Some r2 ->
    821       (if (not (bd-tooSmall r2))
    822         (Some (SDeep f m r2))
    823         (if (scd-isEmpty m)
    824           (Some (SShallow (bd-dappendR r r2)))
    825           (match (scd-last m) with
    826            [None -> None]
    827            [Some lm ->
    828             (match (scd-init m) with
    829              [None -> None]
    830              [Some im ->
    831               (Some (SDeep f im (bd-dappendR lm r2)))])])))])]))
    832 
    833 (define (scd-++ [scd1 : (SimpleCatDeque A)] [scd2 : (SimpleCatDeque A)] → (SimpleCatDeque A))
    834   (match scd1 with
    835    [SShallow d1 ->
    836     (match scd2 with
    837      [SShallow d2 ->
    838       (if (bd-tooSmall d1)
    839         (SShallow (bd-dappendL d1 d2))
    840         (if (bd-tooSmall d2)
    841           (SShallow (bd-dappendR d1 d2))
    842           (SDeep d1 (scd-empty) d2)))]
    843      [SDeep f m r ->
    844       (if (bd-tooSmall d1)
    845         (SDeep (bd-dappendL d1 f) m r)
    846         (SDeep d1 (scd-cons f m) r))])]
    847    [SDeep f1 m1 r1 ->
    848     (match scd2 with
    849      [SShallow d2 ->
    850       (if (bd-tooSmall d2)
    851         (SDeep f1 m1 (bd-dappendR r1 d2))
    852         (SDeep f1 (scd-snoc m1 r1) d2))]
    853      [SDeep f2 m2 r2 ->
    854       (SDeep f1 (scd-++ (scd-snoc m1 f1) (scd-cons r1 m2)) r2)])]))
    855 
    856 (define (scd->list [scd : (SimpleCatDeque A)] → (List A))
    857   (match (scd-head scd) with
    858    [None -> Nil]
    859    [Some hd ->
    860     (match (scd-tail scd) with
    861      [None -> (∷ hd Nil)]
    862      [Some tl -> (∷ hd (scd->list tl))])]))
    863 
    864 ;; -----------------------------------------------------------------------------
    865 
    866 (define sample-scd
    867   (foldl (λ ([acc : (SimpleCatDeque Int)] [x : Int]) (scd-snoc acc x)) (scd-empty) digit*))
    868 
    869 (define (empty-sample → (SimpleCatDeque Int))
    870   (scd-empty))
    871 
    872 (check-type
    873   (scd-isEmpty (SShallow (BD 0 (Nil {Int}) 0 (Nil {Int}))))
    874   : Bool
    875   ⇒ #t)
    876 
    877 (check-type
    878   (scd-isEmpty sample-scd)
    879   : Bool
    880   ⇒ #f)
    881 
    882 (check-type
    883   (scd-head sample-scd)
    884   : (Option Int)
    885   ⇒ (Some 1))
    886 
    887 (check-type
    888   (scd-head (empty-sample))
    889   : (Option Int)
    890   ⇒ None)
    891 
    892 (check-type
    893   (scd-last sample-scd)
    894   : (Option Int)
    895   ⇒ (Some 9))
    896 
    897 (check-type
    898   (scd-last (empty-sample))
    899   : (Option Int)
    900   ⇒ None)
    901 
    902 (check-type
    903   (scd-head (scd-snoc sample-scd 10))
    904   : (Option Int)
    905   ⇒ (Some 1))
    906 
    907 (check-type
    908   (scd-head (scd-cons 10 sample-scd))
    909   : (Option Int)
    910   ⇒ (Some 10))
    911 
    912 (check-type
    913   (match (scd-tail sample-scd) with
    914    [None -> None]
    915    [Some scd -> (scd-head scd)])
    916   : (Option Int)
    917   ⇒ (Some 2))
    918 
    919 (check-type
    920   (scd-tail (empty-sample))
    921   : (Option (SimpleCatDeque Int))
    922   ⇒ None)
    923 
    924 (check-type
    925   (match (scd-init sample-scd) with
    926    [None -> None]
    927    [Some scd -> (scd-last scd)])
    928   : (Option Int)
    929   ⇒ (Some 8))
    930 
    931 (check-type
    932   (scd-init (empty-sample))
    933   : (Option (SimpleCatDeque Int))
    934   ⇒ None)
    935 
    936 (check-type
    937   (match (scd-head (scd-++ (scd-cons 1 (scd-empty)) (empty-sample))) with
    938    [None -> None]
    939    [Some i -> (Some i)])
    940   : (Option Int)
    941   ⇒ (Some 1))
    942 
    943 (check-type
    944   (match (scd-head (scd-++ (empty-sample) (scd-cons 2 (scd-empty)))) with
    945    [None -> None]
    946    [Some scd -> (Some scd)])
    947   : (Option Int)
    948   ⇒ (Some 2))
    949 
    950 (check-type
    951   (match (scd-tail (scd-++ (scd-cons 1 (scd-empty)) (scd-cons 2 (scd-empty)))) with
    952    [None -> None]
    953    [Some scd -> (scd-head scd)])
    954   : (Option Int)
    955   ⇒ (Some 2))
    956 
    957 (define (scd-ref [n : Int] [scd : (SimpleCatDeque A)] → (Option A))
    958   (if (< n 1)
    959     (scd-head scd)
    960     (match (scd-tail scd) with
    961      [None -> None]
    962      [Some tl -> (scd-ref (- n 1) tl)])))
    963 
    964 (check-type
    965   (scd-ref 2
    966     (scd-++
    967       (scd-++ (scd-cons 1 (scd-empty)) (scd-cons 2 (scd-empty)))
    968       (scd-++ (scd-cons 3 (scd-empty)) (scd-cons 4 (scd-empty)))))
    969   : (Option Int)
    970   ⇒ (Some 3))
    971 
    972 (check-type
    973   (scd-ref 0
    974     (scd-++
    975       (scd-++ (scd-cons 1 (scd-empty)) (scd-cons 2 (scd-empty)))
    976       (scd-++ (scd-cons 3 (scd-empty)) (scd-cons 4 (scd-empty)))))
    977   : (Option Int)
    978   ⇒ (Some 1))
    979 
    980 (check-type
    981   (scd->list
    982     (scd-++
    983       (scd-++ (scd-cons 1 (scd-empty)) (scd-cons 2 (scd-empty)))
    984       (scd-++ (scd-cons 3 (scd-empty)) (scd-cons 4 (scd-empty)))))
    985   : (List Int)
    986   ⇒ (∷ 1 (∷ 2 (∷ 3 (∷ 4 Nil)))))
    987 
    988 (check-type
    989   (scd-ref 1
    990     (scd-++
    991       (scd-++
    992         (scd-++ (scd-cons 1 (scd-empty)) (scd-cons 2 (scd-empty)))
    993         (scd-++ (scd-cons 3 (scd-empty)) (scd-cons 4 (scd-empty))))
    994       (scd-++
    995         (scd-++ (scd-cons 5 (scd-empty)) (scd-cons 6 (scd-empty)))
    996         (scd-++ (scd-cons 7 (scd-empty)) (scd-cons 8 (scd-empty))))))
    997   : (Option Int)
    998   ⇒ (Some 2))
    999 
   1000 (check-type
   1001   (scd-ref 3
   1002     (scd-++
   1003       (scd-++
   1004         (scd-++ (scd-cons 1 (scd-empty)) (scd-cons 2 (scd-empty)))
   1005         (scd-++ (scd-cons 3 (scd-empty)) (scd-cons 4 (scd-empty))))
   1006       (scd-++
   1007         (scd-++ (scd-cons 5 (scd-empty)) (scd-cons 6 (scd-empty)))
   1008         (scd-++ (scd-cons 7 (scd-empty)) (scd-cons 8 (scd-empty))))))
   1009   : (Option Int)
   1010   ⇒ (Some 4))
   1011 
   1012 ;; TODO this is a bug, but at least we have the right types in MLish
   1013 ;(check-type
   1014 ;  (scd->list
   1015 ;    (scd-++
   1016 ;      (scd-++
   1017 ;        (scd-++ (scd-cons 1 (scd-empty)) (scd-cons 2 (scd-empty)))
   1018 ;        (scd-++ (scd-cons 3 (scd-empty)) (scd-cons 4 (scd-empty))))
   1019 ;      (scd-++
   1020 ;        (scd-++ (scd-cons 5 (scd-empty)) (scd-cons 6 (scd-empty)))
   1021 ;        (scd-++ (scd-cons 7 (scd-empty)) (scd-cons 8 (scd-empty))))))
   1022 ;  : (List Int)
   1023 ;  ⇒ (∷ 1 (∷ 2 (∷ 3 (∷ 4 (∷ 5 (∷ 6 (∷ 7 (∷ 8 Nil)))))))))
   1024 
   1025 ;; =============================================================================
   1026 ;; === Binary Random Access List
   1027 
   1028 (define-type (Tree A)
   1029   (Leaf A)
   1030   (Node Int (Tree A) (Tree A)))
   1031 
   1032 (define-type (BLDigit A)
   1033   (BLZero)
   1034   (BLOne (Tree A)))
   1035 
   1036 (define-type (BinaryList A)
   1037   (BL (List (BLDigit A))))
   1038 
   1039 (define (size (t : (Tree A)) → Int)
   1040   (match t with
   1041    (Leaf x -> 1)
   1042    (Node w t1 t2 -> w)))
   1043 
   1044 (define (link (t1 : (Tree A)) (t2 : (Tree A)) → (Tree A))
   1045   (Node (+ (size t1) (size t2)) t1 t2))
   1046 
   1047 (define (consTree (t : (Tree A)) (x* : (List (BLDigit A))) → (List (BLDigit A)))
   1048   (match x* with
   1049    (Nil -> (∷ (BLOne t) Nil))
   1050    (∷ h ts ->
   1051     (match h with
   1052      (BLZero -> (∷ (BLOne t) ts))
   1053      (BLOne t2 -> (∷ BLZero (consTree (link t t2) ts)))))))
   1054 
   1055 
   1056 ;; TODO τ_e bad syntax when using `match2`
   1057 (define (unconsTree (d* : (List (BLDigit A))) → (Option (× (Tree A) (List (BLDigit A)))))
   1058   (match d* with
   1059    (Nil -> None)
   1060    (∷ d*-hd d*-tl ->
   1061     (match d*-hd with
   1062      (BLOne t ->
   1063       (match d*-tl with
   1064        (Nil -> (Some (tup t Nil)))
   1065        (∷ a b -> (Some (tup t (∷ BLZero d*-tl))))))
   1066      (BLZero ->
   1067       (match (unconsTree d*-tl) with
   1068        (None -> None)
   1069        (Some udt ->
   1070         (match udt with
   1071          (a ts ->
   1072           (match a with
   1073            (Leaf x -> None)
   1074            (Node x t1 t2 ->
   1075             (Some (tup t1 (∷ (BLOne t2) ts))))))))))))))
   1076 
   1077 (define (bl-empty → (BinaryList A))
   1078   (BL Nil))
   1079 
   1080 (define (bl-isEmpty (b : (BinaryList A)) → Bool)
   1081   (match b with
   1082    (BL x* ->
   1083     (match x* with
   1084      (Nil -> #t)
   1085      (∷ a b -> #f)))))
   1086 
   1087 (define (bl-cons (x : A) (b : (BinaryList A)) → (BinaryList A))
   1088   (match b with
   1089    (BL ts -> (BL (consTree (Leaf x) ts)))))
   1090 
   1091 (define (bl-head (b : (BinaryList A)) → (Option A))
   1092   (match b with
   1093    (BL ts ->
   1094     (match (unconsTree ts) with
   1095      (None -> None)
   1096      (Some xy ->
   1097       (match xy with
   1098        (x y ->
   1099         (match x with
   1100          (Leaf x -> (Some x))
   1101          (Node a b c -> None)))))))))
   1102 
   1103 (define (bl-tail (b : (BinaryList A)) → (Option (BinaryList A)))
   1104   (match b with
   1105    (BL ts ->
   1106     (match (unconsTree ts) with
   1107      (None -> None)
   1108      (Some xy ->
   1109       (match xy with
   1110        (x ts2 -> (Some (BL ts2)))))))))
   1111 
   1112 (define (bl-lookup (i : Int) (b : (BinaryList A)) → (Option A))
   1113   (match b with
   1114    [BL ts ->
   1115     (look i ts)]))
   1116 
   1117 (define (look [i : Int] [ts : (List (BLDigit A))] → (Option A))
   1118   (match ts with
   1119    [Nil -> None]
   1120    [∷ h ts ->
   1121     (match h with
   1122      [BLZero ->
   1123       (look i ts)]
   1124      [BLOne t ->
   1125       (let ((size-t (size t)))
   1126         (if (< i size-t)
   1127           (lookTree i t)
   1128           (look (- i size-t) ts)))])]))
   1129 
   1130 (define (lookTree (i : Int) (t : (Tree A)) → (Option A))
   1131   (match t with
   1132    [Leaf x ->
   1133     (if (= 0 i)
   1134       (Some x)
   1135       None)]
   1136    [Node w t1 t2 ->
   1137     (let ((w/2 (div w 2)))
   1138       (if (< i w/2)
   1139         (lookTree i t1)
   1140         (lookTree (- i w/2) t2)))]))
   1141 
   1142 (define (bl-update (i : Int) (y : A) (b : (BinaryList A)) → (Option (BinaryList A)))
   1143   (match b with
   1144    [BL ts ->
   1145     (match (upd i y ts) with
   1146      (None -> None)
   1147      (Some x -> (Some (BL x))))]))
   1148 
   1149 (define (upd (i : Int) (y : A) (b : (List (BLDigit A))) → (Option (List (BLDigit A))))
   1150   (match b with
   1151    [Nil -> None]
   1152    [∷ h ts ->
   1153     (match h with
   1154      [BLZero ->
   1155       (match (upd i y ts) with
   1156        (None -> None)
   1157        (Some x -> (Some (∷ BLZero x))))]
   1158      [BLOne t ->
   1159       (let ((size-t (size t)))
   1160         (if (< i size-t)
   1161           (match (updTree i y t) with
   1162            (None -> None)
   1163            (Some x -> (Some (∷ (BLOne x) ts))))
   1164           (match (upd (- i size-t) y ts) with
   1165            (None -> None)
   1166            (Some x -> (Some (∷ (BLOne t) x))))))])]))
   1167 
   1168 (define (updTree (i : Int) (y : A) (t : (Tree A)) → (Option (Tree A)))
   1169   (match t with
   1170    (Leaf x ->
   1171     (if (= 0 i)
   1172       (Some (Leaf y))
   1173       None))
   1174    (Node w t1 t2 ->
   1175     (let ((w/2 (div w 2)))
   1176       (if (< i w/2)
   1177         (match (updTree i y t1) with
   1178          (None -> None)
   1179          (Some x -> (Some (Node w x t2))))
   1180         (match (updTree (- i w/2) y t2) with
   1181          (None -> None)
   1182          (Some x -> (Some (Node w t1 x)))))))))
   1183 
   1184 (define (list->bl-list (x* : (List A)) → (BinaryList A))
   1185   (match x* with
   1186    (Nil -> (bl-empty))
   1187    (∷ x x* -> (bl-cons x (list->bl-list x*)))))
   1188 
   1189 ;; =============================================================================
   1190 
   1191 (define bl-digit*
   1192   (list->bl-list (∷ 1 (∷ 2 (∷ 3 (∷ 4 (∷ 5 (∷ 6 (∷ 7 (∷ 8 (∷ 9 Nil)))))))))))
   1193 
   1194 (define (bl-nil → (BinaryList Int))
   1195   (list->bl-list Nil))
   1196 
   1197 (check-type
   1198   (bl-isEmpty (bl-nil))
   1199   : Bool
   1200   ⇒ #t)
   1201 
   1202 (check-type
   1203   (bl-isEmpty bl-digit*)
   1204   : Bool
   1205   ⇒ #f)
   1206 
   1207 (check-type
   1208   (match (bl-head bl-digit*) with
   1209    (None -> 0)
   1210    (Some x -> x))
   1211   : Int
   1212   ⇒ 1)
   1213 
   1214 (check-type
   1215   (match (bl-tail bl-digit*) with
   1216    (None -> 0)
   1217    (Some x ->
   1218     (match (bl-head x) with
   1219      (None -> 0)
   1220      (Some y -> y))))
   1221   : Int
   1222   ⇒ 2)
   1223 
   1224 (check-type
   1225   (match (bl-lookup 7 bl-digit*) with
   1226    (None -> 0)
   1227    (Some x -> x))
   1228   : Int
   1229   ⇒ 8)
   1230 
   1231 (check-type
   1232   (match (bl-lookup 8 bl-digit*) with
   1233    (None -> 0)
   1234    (Some x -> x))
   1235   : Int
   1236   ⇒ 9)
   1237 
   1238 (check-type
   1239   (bl-lookup -111 bl-digit*)
   1240   : (Option Int)
   1241   ⇒ None)
   1242 
   1243 (check-type
   1244   (match (bl-update 3 99 bl-digit*) with
   1245    (None -> None)
   1246    (Some x -> (bl-lookup 3 x)))
   1247   : (Option Int)
   1248   ⇒ (Some 99))
   1249 
   1250 (check-type
   1251   (match (bl-update 0 222 bl-digit*) with
   1252    (None -> None)
   1253    (Some x -> (bl-head x)))
   1254   : (Option Int)
   1255   ⇒ (Some 222))
   1256 
   1257 (check-type
   1258   (bl-update 83 1 bl-digit*)
   1259   : (Option (BinaryList Int))
   1260   ⇒ None)
   1261 
   1262 ;; =============================================================================
   1263 ;; === Skew Binary Random Access Lists
   1264 
   1265 (define-type (ATree A)
   1266   (ALeaf A)
   1267   (ANode A (ATree A) (ATree A)))
   1268 
   1269 (define-type (SkewList A)
   1270   (SL (List (× Int (ATree A)))))
   1271 
   1272 (define (sb-empty → (SkewList A))
   1273   (SL Nil))
   1274 
   1275 (define (sb-isEmpty (sl : (SkewList A)) → Bool)
   1276   (match sl with
   1277    (SL xs ->
   1278     (match xs with
   1279      (Nil -> #t)
   1280      (∷ a b -> #f)))))
   1281 
   1282 (define (sb-cons (x : A) (sl : (SkewList A)) → (SkewList A))
   1283   (match sl with
   1284    (SL ts ->
   1285     (let ((base-case (SL (∷ (tup 1 (ALeaf x)) ts))))
   1286       (match ts with
   1287        (Nil -> base-case)
   1288        (∷ w1t1 ts ->
   1289         (match ts with
   1290          (Nil -> base-case)
   1291          (∷ w2t2 ts ->
   1292           (match w1t1 with
   1293            (w1 t1 ->
   1294             (match w2t2 with
   1295              (w2 t2 ->
   1296               (if (= w1 w2)
   1297                 (SL (∷ (tup (+ 1 (+ w1 w2)) (ANode x t1 t2)) ts))
   1298                 base-case)))))))))))))
   1299 
   1300 (define (sb-head (sl : (SkewList A)) → (Option A))
   1301   (match sl with
   1302    (SL ts ->
   1303     (match ts with
   1304      (Nil -> None)
   1305      (∷ w1t1 ts ->
   1306       (match w1t1 with
   1307        (w1 t1 ->
   1308         (match t1 with
   1309          (ALeaf x ->
   1310           (if (= w1 1)
   1311             (Some x)
   1312             None)) ;; Invariant error
   1313          (ANode x t1 t2 ->
   1314           (Some x))))))))))
   1315 
   1316 (define (sb-tail (sl : (SkewList A)) → (Option (SkewList A)))
   1317   (match sl with
   1318    (SL ts ->
   1319     (match ts with
   1320      (Nil -> None)
   1321      (∷ w1t1 ts ->
   1322       (match w1t1 with
   1323        (w1 t1 ->
   1324         (match t1 with
   1325          (ALeaf x ->
   1326           (if (= 1 w1)
   1327             (Some (SL ts))
   1328             None)) ;; Invariant
   1329          (ANode x t1 t2 ->
   1330            (let ((w1/2 (div w1 2)))
   1331              (Some (SL (∷ (tup w1/2 t1) (∷ (tup w1/2 t2) ts))))))))))))))
   1332 
   1333 (define (sb-lookup (i : Int) (sl : (SkewList A)) → (Option A))
   1334   (match sl with
   1335    (SL ts ->
   1336     (sb-look i ts))))
   1337 
   1338 (define (sb-look (i : Int) (ts : (List (× Int (ATree A)))) → (Option A))
   1339   (match ts with
   1340    (Nil -> None) ;; Bad subscript
   1341    (∷ wt ts ->
   1342     (match wt with
   1343      (w t ->
   1344       (if (< i w)
   1345         (sb-lookTree w i t)
   1346         (sb-look (- i w) ts)))))))
   1347 
   1348 (define (sb-lookTree (w : Int) (i : Int) (t : (ATree A)) → (Option A))
   1349   (match t with
   1350    (ALeaf x ->
   1351     (if (and (= w 1) (= i 0))
   1352       (Some x)
   1353       None))
   1354    (ANode x t1 t2 ->
   1355     (if (= 0 i)
   1356       (Some x)
   1357       (let ((w/2 (div w 2)))
   1358         (if (<= i w/2)
   1359           (sb-lookTree w/2 (- i 1) t1)
   1360           (sb-lookTree w/2 (- (- i 1) w/2) t2)))))))
   1361 
   1362 (define (sb-update (i : Int) (y : A) (sl : (SkewList A)) → (Option (SkewList A)))
   1363   (match sl with
   1364    (SL ts ->
   1365     (match (sb-upd i y ts) with
   1366      (None -> None)
   1367      (Some ts -> (Some (SL ts)))))))
   1368 
   1369 (define (sb-upd (i : Int) (y : A) (ts : (List (× Int (ATree A)))) → (Option (List (× Int (ATree A)))))
   1370   (match ts with
   1371    (Nil -> None)
   1372    (∷ wt ts ->
   1373     (match wt with
   1374      (w t ->
   1375       (if (< i w)
   1376         (match (sb-updTree w i y t) with
   1377          (None -> None)
   1378          (Some x -> (Some (∷ (tup w x) ts))))
   1379         (match (sb-upd (- i w) y ts) with
   1380          (None -> None)
   1381          (Some x -> (Some (∷ (tup w t) x))))))))))
   1382 
   1383 (define (sb-updTree (w : Int) (i : Int) (y : A) (t : (ATree A)) → (Option (ATree A)))
   1384   (match t with
   1385    (ALeaf x ->
   1386     (if (and (= 1 w) (= 0 i))
   1387       (Some (ALeaf y))
   1388       None)) ;; Invariant error
   1389    (ANode x t1 t2 ->
   1390     (if (= 0 i)
   1391       (Some (ANode y t1 t2))
   1392       (let ((w/2 (div w 2)))
   1393         (if (<= i w/2)
   1394           (match (sb-updTree w/2 (- i 1) y t1) with
   1395            (None -> None)
   1396            (Some z -> (Some (ANode x z t2))))
   1397           (match (sb-updTree w/2 (- (- i 1) w/2) y t2) with
   1398            (None -> None)
   1399            (Some z -> (Some (ANode x t1 z))))))))))
   1400 
   1401 (define (list->sb-list (x* : (List A)) → (SkewList A))
   1402   (match x* with
   1403    (Nil -> (sb-empty))
   1404    (∷ h t -> (sb-cons h (list->sb-list t)))))
   1405 
   1406 ;; =============================================================================
   1407 
   1408 (define sb-digit*
   1409   (list->sb-list (∷ 1 (∷ 2 (∷ 3 (∷ 4 (∷ 5 (∷ 6 (∷ 7 (∷ 8 (∷ 9 Nil)))))))))))
   1410 
   1411 (define (sb-nil → (SkewList Int))
   1412   (list->sb-list Nil))
   1413 
   1414 (check-type
   1415   (sb-isEmpty (sb-nil))
   1416   : Bool
   1417   ⇒ #t)
   1418 
   1419 (check-type
   1420   (sb-isEmpty sb-digit*)
   1421   : Bool
   1422   ⇒ #f)
   1423 
   1424 (check-type
   1425   (match (sb-head sb-digit*) with
   1426    (None -> 0)
   1427    (Some x -> x))
   1428   : Int
   1429   ⇒ 1)
   1430 
   1431 (check-type
   1432   (match (sb-tail sb-digit*) with
   1433    (None -> 0)
   1434    (Some x ->
   1435     (match (sb-head x) with
   1436      (None -> 0)
   1437      (Some y -> y))))
   1438   : Int
   1439   ⇒ 2)
   1440 
   1441 (check-type
   1442   (match (sb-lookup 7 sb-digit*) with
   1443    (None -> 0)
   1444    (Some x -> x))
   1445   : Int
   1446   ⇒ 8)
   1447 
   1448 (check-type
   1449   (match (sb-lookup 8 sb-digit*) with
   1450    (None -> 0)
   1451    (Some x -> x))
   1452   : Int
   1453   ⇒ 9)
   1454 
   1455 (check-type
   1456   (sb-lookup -111 sb-digit*)
   1457   : (Option Int)
   1458   ⇒ None)
   1459 
   1460 (check-type
   1461   (match (sb-update 3 99 sb-digit*) with
   1462    (None -> None)
   1463    (Some x -> (sb-lookup 3 x)))
   1464   : (Option Int)
   1465   ⇒ (Some 99))
   1466 
   1467 (check-type
   1468   (match (sb-update 0 222 sb-digit*) with
   1469    (None -> None)
   1470    (Some x -> (sb-head x)))
   1471   : (Option Int)
   1472   ⇒ (Some 222))
   1473 
   1474 (check-type
   1475   (sb-update 83 1 sb-digit*)
   1476   : (Option (SkewList Int))
   1477   ⇒ None)
   1478 
   1479 ;; =============================================================================
   1480 ;; === Alt Binary Random Access List
   1481 
   1482 (define-type (BinaryRAList A)
   1483   (ABLNil)
   1484   (ABLZero (BinaryRAList (× A A)))
   1485   (ABLOne A (BinaryRAList (× A A))))
   1486 
   1487 (define (abl-uncons (bl : (BinaryRAList A)) → (Option (× A (BinaryRAList A))))
   1488   (match bl with
   1489    (ABLNil -> None)
   1490    (ABLOne x ps ->
   1491     (Some (match ps with
   1492      (ABLNil -> (tup x ABLNil))
   1493      (ABLOne y ps2 -> (tup x (ABLZero ps)))
   1494      (ABLZero ps2 -> (tup x (ABLZero ps))))))
   1495    (ABLZero ps ->
   1496     (match (abl-uncons ps) with
   1497      (None -> None)
   1498      (Some xyps2 ->
   1499       (match xyps2 with
   1500        (xy ps2 ->
   1501         (match xy with
   1502          (x y -> (Some (tup x (ABLOne y ps2))))))))))))
   1503 
   1504 (define (abl-fupdate (f : (→ A A)) (i : Int) (bl : (BinaryRAList A)) → (Option (BinaryRAList A)))
   1505   (match bl with
   1506    (ABLNil -> None)
   1507    (ABLOne x ps ->
   1508     (if (= 0 i)
   1509       (Some (ABLOne (f x) ps))
   1510       (match (abl-fupdate f (- i 1) (ABLZero ps)) with
   1511        (None -> None)
   1512        (Some z -> (Some (abl-cons x z))))))
   1513    (ABLZero ps ->
   1514      (let ((f2 (if (= 0 (mod i 2))
   1515                  (λ ([xy : (× A A)])
   1516                    (match xy with (x y -> (tup (f x) y))))
   1517                  (λ ([xy : (× A A)])
   1518                    (match xy with (x y -> (tup x (f y))))))))
   1519       (match (abl-fupdate f2 (div i 2) ps) with
   1520         (None -> None)
   1521         (Some z -> (Some (ABLZero z))))))))
   1522 
   1523 (define (aabl-empty → (BinaryRAList A))
   1524   ABLNil)
   1525 
   1526 (define (abl-isEmpty (bl : (BinaryRAList A)) → Bool)
   1527   (match bl with
   1528    (ABLNil -> #t)
   1529    (ABLOne a b -> #f)
   1530    (ABLZero a -> #f)))
   1531 
   1532 (define (abl-cons (x : A) (bl : (BinaryRAList A)) → (BinaryRAList A))
   1533   (match bl with
   1534    (ABLNil -> (ABLOne x ABLNil))
   1535    (ABLZero ps -> (ABLOne x ps))
   1536    (ABLOne y ps -> (ABLZero (abl-cons (tup x y) ps)))))
   1537 
   1538 (define (abl-head (bl : (BinaryRAList A)) → (Option A))
   1539   (match (abl-uncons bl) with
   1540    (None -> None)
   1541    (Some xy ->
   1542     (match xy with
   1543      (x y -> (Some x))))))
   1544 
   1545 (define (abl-tail (bl : (BinaryRAList A)) → (Option (BinaryRAList A)))
   1546   (match (abl-uncons bl) with
   1547    (None -> None)
   1548    (Some xy ->
   1549     (match xy with
   1550      (x y -> (Some y))))))
   1551 
   1552 (define (abl-lookup (i : Int) (bl : (BinaryRAList A)) → (Option A))
   1553   (if (< i 0)
   1554     None
   1555     (abl-lookup/natural i bl)))
   1556 
   1557 (define (abl-lookup/natural (i : Int) (bl : (BinaryRAList A)) → (Option A))
   1558   (match bl with
   1559    (ABLNil -> None)
   1560    (ABLOne x ps ->
   1561     (if (= 0 i)
   1562       (Some x)
   1563       (abl-lookup/natural (- i 1) (ABLZero ps))))
   1564    (ABLZero ps ->
   1565     (match (abl-lookup/natural (div i 2) ps) with
   1566      (None -> None)
   1567      (Some xy ->
   1568       (match xy with
   1569        (x y ->
   1570         (if (= 0 (mod i 2))
   1571           (Some x)
   1572           (Some y)))))))))
   1573 
   1574 (define (abl-update (i : Int) (y : A) (bl : (BinaryRAList A)) → (Option (BinaryRAList A)))
   1575   (abl-fupdate (λ ([x : A]) y) i bl))
   1576 
   1577 (define (list->abl-list (xs : (List A)) → (BinaryRAList A))
   1578   (match xs with
   1579    (Nil -> (aabl-empty))
   1580    (∷ a b -> (abl-cons a (list->abl-list b)))))
   1581 
   1582 ;; =============================================================================
   1583 
   1584 (define abl-digit*
   1585   (list->abl-list (∷ 1 (∷ 2 (∷ 3 (∷ 4 (∷ 5 (∷ 6 (∷ 7 (∷ 8 (∷ 9 Nil)))))))))))
   1586 
   1587 (define (abl-nil → (BinaryRAList Int))
   1588   (list->abl-list Nil))
   1589 
   1590 (check-type
   1591   (abl-isEmpty (abl-nil))
   1592   : Bool
   1593   ⇒ #t)
   1594 
   1595 (check-type
   1596   (abl-isEmpty abl-digit*)
   1597   : Bool
   1598   ⇒ #f)
   1599 
   1600 (check-type
   1601   (match (abl-head abl-digit*) with
   1602    (None -> 0)
   1603    (Some x -> x))
   1604   : Int
   1605   ⇒ 1)
   1606 
   1607 (check-type
   1608   (match (abl-tail abl-digit*) with
   1609    (None -> 0)
   1610    (Some x ->
   1611     (match (abl-head x) with
   1612      (None -> 0)
   1613      (Some y -> y))))
   1614   : Int
   1615   ⇒ 2)
   1616 
   1617 (check-type
   1618   (match (abl-lookup 7 abl-digit*) with
   1619    (None -> 0)
   1620    (Some x -> x))
   1621   : Int
   1622   ⇒ 8)
   1623 
   1624 (check-type
   1625   (match (abl-lookup 8 abl-digit*) with
   1626    (None -> 0)
   1627    (Some x -> x))
   1628   : Int
   1629   ⇒ 9)
   1630 
   1631 (check-type
   1632   (abl-lookup -111 abl-digit*)
   1633   : (Option Int)
   1634   ⇒ None)
   1635 
   1636 (check-type
   1637   (match (abl-update 3 99 abl-digit*) with
   1638    (None -> None)
   1639    (Some x -> (abl-lookup 3 x)))
   1640   : (Option Int)
   1641   ⇒ (Some 99))
   1642 
   1643 (check-type
   1644   (match (abl-update 0 222 abl-digit*) with
   1645    (None -> None)
   1646    (Some x -> (abl-head x)))
   1647   : (Option Int)
   1648   ⇒ (Some 222))
   1649 
   1650 (check-type
   1651   (abl-update 83 1 abl-digit*)
   1652   : (Option (BinaryRAList Int))
   1653   ⇒ None)
   1654