~plan/plunder

7c86da5624d2fd15497b9c96dfeba0e212155e72 — Sol a month ago 00e1149
viceroy: comment pq_vice to avoid breaking CI
1 files changed, 208 insertions(+), 208 deletions(-)

M sire/pq_vice.sire
M sire/pq_vice.sire => sire/pq_vice.sire +208 -208
@@ 4,211 4,211 @@

#### pq_vice <- viceroy

;;;; Priority Queues
;;;; ===============
;;;;
;;;; This implementation is based on section 4.16 of the book 'ML for the
;;;; Working Programmer' by Larry C. Paulson (Cambridge University Press
;;;; [1996]).
;;;;
;;;; It is modified to support a customizeable comparator function (`cmp`,
;;;; below) which is passed as an argument to many `pq.*` functions. This
;;;; allows similar functionality to, for example, a Haskell `Ord`
;;;; instance. `cmp` takes 2 arguments and outputs a LT/EQ/GT value
;;;; (see 03_nat.sire) indicating their relation to each other.


;;; Imports ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

:| sire_02_bit [if and TRUE FALSE]
:| sire_03_nat [LT EQ GT div sub]
:| sire_04_cmp [eql cmp neq]
:| sire_07_dat [listUnsafeHead listDrop NIL listRev listFoldr]
:| sire_07_dat [SOME NONE maybeCase]
:| viceroy


;;; Types ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

# data Pq
- LF
- BR Nat Pq Pq

= pqEmpty LF

= pqNull
? (pqNull t/Pq >Bit)
| (t == pqEmpty)

#* =?= TRUE  | pqNull LF
#* =?= FALSE | pqNull (BR 7 LF LF)

= pqInsert
? (pqInsert cmp/NatCmp w/Nat t/Pq >Pq)
^       >(Nat -> Pq -> Pq)
    | _ w t
? (go w/Nat t/Pq >Pq)
# case t
- LF
    | BR w LF LF
- BR v t1 t2
    | if (cmp w v == GT) | (BR v (go w t2) t1)
    | else               | (BR w (go v t2) t1)

= leftRem
? (leftRem cmp/NatCmp t/Pq >(MaybeNat, Pq))
# case t
- LF [NONE t]
- BR w t1 t2
    | if (pqNull t1 && pqNull t2)
        | (SOME w, LF)
    | else
        ; [mbW t] (leftRem cmp t1)
        @ pair/(MaybeNat, Pq) (leftRem cmp t1)
        @ mbW/MaybeNat        (fst pair)
        @ t/Pq                (snd pair)
        | (mbW, BR w t2 t)

* = test1 | pqInsert cmp 0 pqEmpty
* = test2 | pqInsert cmp 1 test1
* = test3 | leftRem cmp test2

= siftDown
? (siftDown cmp/NatCmp w/Nat t1/Pq t2/Pq >Pq)
^       > (Nat -> Pq -> Pq -> Pq)
    | _ w t1 t2
? (go w/Nat t1/Pq t2/Pq >Pq)
# case t1
- LF
    # case t2
    - LF | BR w LF LF
    - _  | go w t2 t1
- BR v1 t1L t1R
    # case t2
    - LF
        | if (and (pqNull t1L) (pqNull t1R))
            | if (cmp w v1 == GT)
                | BR v1 (BR w LF LF) LF
            | else
                | BR w t1 LF
        | die {siftDown: wat}
    - BR v2 t2L t2R
        | if ((GT /= cmp w v1) && (GT /= cmp w v2))
            | BR w t1 t2
        | if (GT == cmp v1 v2)
            | BR v2 t1 (go w t2L t2R)
        | else
            | BR v1 (go w t1L t1R) t2

= pqDelMin
? (pqDelMin cmp/NatCmp t/Pq >(MaybeNat, Pq))
# case t
- LF [NONE LF]
- BR v t1 t2
    @ pair/(MaybeNat, Pq) | leftRem cmp t1
    @ mbW/MaybeNat        | fst pair
    @ t/Pq                | snd pair
    | maybeCase mbW (SOME v, LF)
    & (w/Nat >(MaybeNat, Pq))
    | (SOME v, siftDown cmp w t2 t)

= pqMin
? (pqMin t/Pq >MaybeNat)
# case t
- LF       | NONE
- BR w _ _ | SOME w

=?= (SOME 7) | pqMin (BR 7 LF LF)

= heapify
? (heapify cmp/NatCmp ls/ListNat >(Pq, ListNat))
^       >(Nat -> ListNat -> (Pq, ListNat))
    | _ (listLen ls) ls
? (go n/Nat vs/ListNat >(Pq, ListNat))
# case vs
- LN_NIL
    | [LF vs]
- LN_CONS v vs
    @ p1/(Pq, ListNat) | go (div n 2) vs
    @ t1/Pq            | fst p1
    @ vs1/ListNat      | snd p1
    @ p2/(Pq, ListNat) | go (div (sub n 1) 2) vs1
    @ t2/Pq            | fst p2
    @ vs2/ListNat      | snd p2
    | (siftDown cmp v t1 t2, vs2)

= pqFromList
? (pqFromList cmp/NatCmp vs/ListNat >Pq)
| fst (heapify cmp vs)

= pqFromList0
? (pqFromList0 cmp/NatCmp vs/ListNat >Pq)
| listFoldl (acc x & pqInsert cmp x acc) pqEmpty vs

= (pqToList cmp/NatCmp t/Pq >ListNat)
^ _ NIL t
? (go acc t)
@ [mbW t1] (pqDelMin cmp t)
: w < maybeCase mbW (listRev acc)
| go (w::acc) t1

= (pqSort cmp/NatCmp xs/Pq >ListNat)
| pqToList cmp
| pqFromList cmp
| xs

= (pqSort0 cmp/NatCmp xs)
| pqToList cmp
| pqFromList0 cmp
| xs

=?= ~[0 1 2 3 5 7 9 9]
  | pqSort  cmp ~[1 9 7 5 2 0 9 3]

=?= ~[0 1 2 3 5 7 9 9]
  | pqSort0 cmp ~[1 9 7 5 2 0 9 3]

;; more sophisticated tests, examining laziness of pq values.
;; we ensure that infinite values at position 1 of a tuple can pass in/out of
;; pqs, provided they are not touched.

= (cmpPairNatKey p1 p2)
| cmp idx-0-p1 idx-0-p2

= (repeat n)
@@ z=(n::z)
 z

=?= 9
  # case
      | pqMin
      | pqInsert cmpPairNatKey (9, repeat 3) pqEmpty
  - NONE   | 7
  - SOME x | idx 0 x

; insert in ascending order of key
=?= 110
  @ ls0 : x < listGen 11
        | (x, repeat x)
  @ pq (pqFromList0 cmpPairNatKey ls0)
  @ ls1 (pqToList cmpPairNatKey pq)
  | listSum : p < listForEach ls1
            | add idx-0-p (listUnsafeHead idx-1-p)

; insert in descending order of key

=?= 110
  @ ls0 : x < listGen 11
        | (sub 10 x, repeat (sub 10 x))
  @ pq (pqFromList0 cmpPairNatKey ls0)
  @ ls1 (pqToList cmpPairNatKey pq)
  | listSum : p < listForEach ls1
            | add idx-0-p (listUnsafeHead idx-1-p)


;;; Exports ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

^-^
^-^ pqEmpty pqInsert pqDelMin pqMin pqNull
^-^ pqFromList pqToList pqSort
^-^
; ;;;; Priority Queues
; ;;;; ===============
; ;;;;
; ;;;; This implementation is based on section 4.16 of the book 'ML for the
; ;;;; Working Programmer' by Larry C. Paulson (Cambridge University Press
; ;;;; [1996]).
; ;;;;
; ;;;; It is modified to support a customizeable comparator function (`cmp`,
; ;;;; below) which is passed as an argument to many `pq.*` functions. This
; ;;;; allows similar functionality to, for example, a Haskell `Ord`
; ;;;; instance. `cmp` takes 2 arguments and outputs a LT/EQ/GT value
; ;;;; (see 03_nat.sire) indicating their relation to each other.
;
;
; ;;; Imports ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
; :| sire_02_bit [if and TRUE FALSE]
; :| sire_03_nat [LT EQ GT div sub]
; :| sire_04_cmp [eql cmp neq]
; :| sire_07_dat [listUnsafeHead listDrop NIL listRev listFoldr]
; :| sire_07_dat [SOME NONE maybeCase]
; :| viceroy
;
;
; ;;; Types ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
; # data Pq
; - LF
; - BR Nat Pq Pq
;
; = pqEmpty LF
;
; = pqNull
; ? (pqNull t/Pq >Bit)
; | (t == pqEmpty)
;
; #* =?= TRUE  | pqNull LF
; #* =?= FALSE | pqNull (BR 7 LF LF)
;
; = pqInsert
; ? (pqInsert cmp/NatCmp w/Nat t/Pq >Pq)
; ^       >(Nat -> Pq -> Pq)
;     | _ w t
; ? (go w/Nat t/Pq >Pq)
; # case t
; - LF
;     | BR w LF LF
; - BR v t1 t2
;     | if (cmp w v == GT) | (BR v (go w t2) t1)
;     | else               | (BR w (go v t2) t1)
;
; = leftRem
; ? (leftRem cmp/NatCmp t/Pq >(MaybeNat, Pq))
; # case t
; - LF [NONE t]
; - BR w t1 t2
;     | if (pqNull t1 && pqNull t2)
;         | (SOME w, LF)
;     | else
;         ; [mbW t] (leftRem cmp t1)
;         @ pair/(MaybeNat, Pq) (leftRem cmp t1)
;         @ mbW/MaybeNat        (fst pair)
;         @ t/Pq                (snd pair)
;         | (mbW, BR w t2 t)
;
; * = test1 | pqInsert cmp 0 pqEmpty
; * = test2 | pqInsert cmp 1 test1
; * = test3 | leftRem cmp test2
;
; = siftDown
; ? (siftDown cmp/NatCmp w/Nat t1/Pq t2/Pq >Pq)
; ^       > (Nat -> Pq -> Pq -> Pq)
;     | _ w t1 t2
; ? (go w/Nat t1/Pq t2/Pq >Pq)
; # case t1
; - LF
;     # case t2
;     - LF | BR w LF LF
;     - _  | go w t2 t1
; - BR v1 t1L t1R
;     # case t2
;     - LF
;         | if (and (pqNull t1L) (pqNull t1R))
;             | if (cmp w v1 == GT)
;                 | BR v1 (BR w LF LF) LF
;             | else
;                 | BR w t1 LF
;         | die {siftDown: wat}
;     - BR v2 t2L t2R
;         | if ((GT /= cmp w v1) && (GT /= cmp w v2))
;             | BR w t1 t2
;         | if (GT == cmp v1 v2)
;             | BR v2 t1 (go w t2L t2R)
;         | else
;             | BR v1 (go w t1L t1R) t2
;
; = pqDelMin
; ? (pqDelMin cmp/NatCmp t/Pq >(MaybeNat, Pq))
; # case t
; - LF [NONE LF]
; - BR v t1 t2
;     @ pair/(MaybeNat, Pq) | leftRem cmp t1
;     @ mbW/MaybeNat        | fst pair
;     @ t/Pq                | snd pair
;     | maybeCase mbW (SOME v, LF)
;     & (w/Nat >(MaybeNat, Pq))
;     | (SOME v, siftDown cmp w t2 t)
;
; = pqMin
; ? (pqMin t/Pq >MaybeNat)
; # case t
; - LF       | NONE
; - BR w _ _ | SOME w
;
; =?= (SOME 7) | pqMin (BR 7 LF LF)
;
; = heapify
; ? (heapify cmp/NatCmp ls/ListNat >(Pq, ListNat))
; ^       >(Nat -> ListNat -> (Pq, ListNat))
;     | _ (listLen ls) ls
; ? (go n/Nat vs/ListNat >(Pq, ListNat))
; # case vs
; - LN_NIL
;     | [LF vs]
; - LN_CONS v vs
;     @ p1/(Pq, ListNat) | go (div n 2) vs
;     @ t1/Pq            | fst p1
;     @ vs1/ListNat      | snd p1
;     @ p2/(Pq, ListNat) | go (div (sub n 1) 2) vs1
;     @ t2/Pq            | fst p2
;     @ vs2/ListNat      | snd p2
;     | (siftDown cmp v t1 t2, vs2)
;
; = pqFromList
; ? (pqFromList cmp/NatCmp vs/ListNat >Pq)
; | fst (heapify cmp vs)
;
; = pqFromList0
; ? (pqFromList0 cmp/NatCmp vs/ListNat >Pq)
; | listFoldl (acc x & pqInsert cmp x acc) pqEmpty vs
;
; = (pqToList cmp/NatCmp t/Pq >ListNat)
; ^ _ NIL t
; ? (go acc t)
; @ [mbW t1] (pqDelMin cmp t)
; : w < maybeCase mbW (listRev acc)
; | go (w::acc) t1
;
; = (pqSort cmp/NatCmp xs/Pq >ListNat)
; | pqToList cmp
; | pqFromList cmp
; | xs
;
; = (pqSort0 cmp/NatCmp xs)
; | pqToList cmp
; | pqFromList0 cmp
; | xs
;
; =?= ~[0 1 2 3 5 7 9 9]
;   | pqSort  cmp ~[1 9 7 5 2 0 9 3]
;
; =?= ~[0 1 2 3 5 7 9 9]
;   | pqSort0 cmp ~[1 9 7 5 2 0 9 3]
;
; ;; more sophisticated tests, examining laziness of pq values.
; ;; we ensure that infinite values at position 1 of a tuple can pass in/out of
; ;; pqs, provided they are not touched.
;
; = (cmpPairNatKey p1 p2)
; | cmp idx-0-p1 idx-0-p2
;
; = (repeat n)
; @@ z=(n::z)
;  z
;
; =?= 9
;   # case
;       | pqMin
;       | pqInsert cmpPairNatKey (9, repeat 3) pqEmpty
;   - NONE   | 7
;   - SOME x | idx 0 x
;
; ; insert in ascending order of key
; =?= 110
;   @ ls0 : x < listGen 11
;         | (x, repeat x)
;   @ pq (pqFromList0 cmpPairNatKey ls0)
;   @ ls1 (pqToList cmpPairNatKey pq)
;   | listSum : p < listForEach ls1
;             | add idx-0-p (listUnsafeHead idx-1-p)
;
; ; insert in descending order of key
;
; =?= 110
;   @ ls0 : x < listGen 11
;         | (sub 10 x, repeat (sub 10 x))
;   @ pq (pqFromList0 cmpPairNatKey ls0)
;   @ ls1 (pqToList cmpPairNatKey pq)
;   | listSum : p < listForEach ls1
;             | add idx-0-p (listUnsafeHead idx-1-p)
;
;
; ;;; Exports ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
; ^-^
; ^-^ pqEmpty pqInsert pqDelMin pqMin pqNull
; ^-^ pqFromList pqToList pqSort
; ^-^