module UVMHS.Core.Classes.Collections where

import UVMHS.Core.Init

infixl 7 ⋕?,⋕,⋕!

class All a where all ∷ 𝐼 a

-- aggregate size = sum of sizes of each element
class ASized a where asize ∷ a → ℕ64

-- count size = number of elements
class CSized a where csize ∷ a → ℕ64

class Single a t | t → a where single ∷ a → t
class Lookup k v t | t → k,t → v where (⋕?) ∷ t → k → 𝑂 v
class Access k v t | t → k,t → v where (⋕) ∷ t → k → v

class ToIter a t | t → a where iter ∷ t → 𝐼 a

lup ∷ (Lookup k v t) ⇒ k → t → 𝑂 v
lup :: forall k v t. Lookup k v t => k -> t -> 𝑂 v
lup = (t -> k -> 𝑂 v) -> k -> t -> 𝑂 v
forall a b c. (a -> b -> c) -> b -> a -> c
flip t -> k -> 𝑂 v
forall k v t. Lookup k v t => t -> k -> 𝑂 v
(⋕?)

(⋕!) ∷ (Lookup k v t,STACK) ⇒ t → k → v
t
kvs ⋕! :: forall k v t. (Lookup k v t, STACK) => t -> k -> v
⋕! k
k = case t
kvs t -> k -> 𝑂 v
forall k v t. Lookup k v t => t -> k -> 𝑂 v
⋕? k
k of
  Some v
v → v
v
  𝑂 v
None → 𝕊 -> v
forall a. STACK => 𝕊 -> a
error 𝕊
"failed ⋕! lookup"

lupΩ ∷ (Lookup k v t) ⇒ k → t → v
lupΩ :: forall k v t. Lookup k v t => k -> t -> v
lupΩ = (t -> k -> v) -> k -> t -> v
forall a b c. (a -> b -> c) -> b -> a -> c
flip t -> k -> v
forall k v t. (Lookup k v t, STACK) => t -> k -> v
(⋕!)