plunder

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

pq.sire (4321B)

      1 ; Copyright 2023 The Plunder Authors
      2 ; Use of this source code is governed by a BSD-style license that can be
      3 ; found in the LICENSE file.
      4 
      5 #### pq <- splitmix
      6 
      7 ;;;; Priority Queues
      8 ;;;; ===============
      9 ;;;;
     10 ;;;; This implementation is based on section 4.16 of the book 'ML for the
     11 ;;;; Working Programmer' by Larry C. Paulson (Cambridge University Press
     12 ;;;; [1996]).
     13 ;;;;
     14 ;;;; It is modified to support a customizeable comparator function (`cmp`,
     15 ;;;; below) which is passed as an argument to many `pq.*` functions. This
     16 ;;;; allows similar functionality to, for example, a Haskell `Ord`
     17 ;;;; instance. `cmp` takes 2 arguments and outputs a LT/EQ/GT value
     18 ;;;; (see 03_nat.sire) indicating their relation to each other.
     19 
     20 
     21 ;;; Imports ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
     22 
     23 :| sire_02_bit [if and TRUE FALSE]
     24 :| sire_03_nat [LT EQ GT div sub]
     25 :| sire_04_cmp [eql cmp neq]
     26 :| sire_07_dat [listLen listUnsafeHead listDrop NIL listRev listFoldr]
     27 :| sire_07_dat [SOME NONE maybeCase]
     28 :| prelude     ;
     29 :| stew        ;
     30 
     31 
     32 ;;; Types ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
     33 
     34 # data (Pq a)
     35 - LF
     36 - BR a Pq Pq
     37 
     38 = pqEmpty LF
     39 
     40 = (pqNull t)
     41 | (t == pqEmpty)
     42 
     43 =?= 1 | pqNull LF
     44 =?= 0 | pqNull (BR 7 LF LF)
     45 
     46 = (pqInsert cmp w t)
     47 ^ _ w t
     48 ? (go w t)
     49 # case t
     50 - LF
     51     | BR w LF LF
     52 - BR v t1 t2
     53     | if (cmp w v == GT) | (BR v (go w t2) t1)
     54     | else               | (BR w (go v t2) t1)
     55 
     56 = (leftRem cmp t)
     57 # case t
     58 - LF [NONE t]
     59 - BR w t1 t2
     60     | if (pqNull t1 && pqNull t2)
     61         | (SOME w, LF)
     62     | else
     63         @ [mbW t] (leftRem cmp t1)
     64         | (mbW, BR w t2 t)
     65 
     66 = test1 | pqInsert cmp 0 pqEmpty
     67 = test2 | pqInsert cmp 1 test1
     68 = test3 | leftRem cmp test2
     69 
     70 = (siftDown cmp w t1 t2)
     71 ^ _ w t1 t2
     72 ? (go w t1 t2)
     73 # case t1
     74 - LF
     75     # case t2
     76     - LF (BR w LF LF)
     77     - _  (go w t2 t1)
     78 - BR v1 t1L t1R
     79     # case t2
     80     - LF
     81         | if (and (pqNull t1L) (pqNull t1R))
     82             | if (cmp w v1 == GT)
     83                 | BR v1 (BR w LF LF) LF
     84             | else
     85                 | BR w t1 LF
     86         | die {siftDown: wat}
     87     - BR v2 t2L t2R
     88         | if ((GT /= cmp w v1) && (GT /= cmp w v2))
     89             | BR w t1 t2
     90         | if (GT == cmp v1 v2)
     91             | BR v2 t1 (go w t2L t2R)
     92         | else
     93             | BR v1 (go w t1L t1R) t2
     94 
     95 = (pqDelMin cmp t)
     96 # case t
     97 - LF [NONE LF]
     98 - BR v t1 t2
     99     @ [mbW t] (leftRem cmp t1)
    100     : w < maybeCase mbW (SOME v, LF)
    101     | (SOME v, siftDown cmp w t2 t)
    102 
    103 = (pqMin t)
    104 # case t
    105 - LF       | NONE
    106 - BR w _ _ | SOME w
    107 
    108 =?= (SOME 7) | pqMin (BR 7 LF LF)
    109 
    110 = (heapify cmp ls)
    111 ^ _ (listLen ls) ls
    112 ? (go n vs)
    113 | ifz n    | [LF vs]
    114 @ v        | listUnsafeHead vs
    115 @ vs       | listDrop 1 vs
    116 @ [t1 vs1] | go (div n 2) vs
    117 @ [t2 vs2] | go (div (sub n 1) 2) vs1
    118 | (siftDown cmp v t1 t2, vs2)
    119 
    120 = (pqFromList cmp vs)
    121 | idx 0 (heapify cmp vs)
    122 
    123 = (pqFromList0 cmp vs)
    124 | listFoldl (acc x & pqInsert cmp x acc) pqEmpty vs
    125 
    126 = (pqToList cmp t)
    127 ^ _ NIL t
    128 ? (go acc t)
    129 @ [mbW t1] (pqDelMin cmp t)
    130 : w < maybeCase mbW (listRev acc)
    131 | go (w::acc) t1
    132 
    133 = (pqSort cmp xs)
    134 | pqToList cmp
    135 | pqFromList cmp
    136 | xs
    137 
    138 = (pqSort0 cmp xs)
    139 | pqToList cmp
    140 | pqFromList0 cmp
    141 | xs
    142 
    143 =?= ~[0 1 2 3 5 7 9 9]
    144   | pqSort  cmp ~[1 9 7 5 2 0 9 3]
    145 
    146 =?= ~[0 1 2 3 5 7 9 9]
    147   | pqSort0 cmp ~[1 9 7 5 2 0 9 3]
    148 
    149 ;; more sophisticated tests, examining laziness of pq values.
    150 ;; we ensure that infinite values at position 1 of a tuple can pass in/out of
    151 ;; pqs, provided they are not touched.
    152 
    153 = (cmpPairNatKey p1 p2)
    154 | cmp idx-0-p1 idx-0-p2
    155 
    156 = (repeat n)
    157 @@ z=(n::z)
    158  z
    159 
    160 =?= 9
    161   # case
    162       | pqMin
    163       | pqInsert cmpPairNatKey (9, repeat 3) pqEmpty
    164   - NONE   | 7
    165   - SOME x | idx 0 x
    166 
    167 ; insert in ascending order of key
    168 =?= 110
    169   @ ls0 : x < listGen 11
    170         | (x, repeat x)
    171   @ pq (pqFromList0 cmpPairNatKey ls0)
    172   @ ls1 (pqToList cmpPairNatKey pq)
    173   | listSum : p < listForEach ls1
    174             | add idx-0-p (listUnsafeHead idx-1-p)
    175 
    176 ; insert in descending order of key
    177 
    178 =?= 110
    179   @ ls0 : x < listGen 11
    180         | (sub 10 x, repeat (sub 10 x))
    181   @ pq (pqFromList0 cmpPairNatKey ls0)
    182   @ ls1 (pqToList cmpPairNatKey pq)
    183   | listSum : p < listForEach ls1
    184             | add idx-0-p (listUnsafeHead idx-1-p)
    185 
    186 
    187 ;;; Exports ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
    188 
    189 ^-^
    190 ^-^ pqEmpty pqInsert pqDelMin pqMin pqNull
    191 ^-^ pqFromList pqToList pqSort
    192 ^-^