source: Papers/polymorphic-variants-2012/Variants2.agda @ 3435

module Variants2 where

  open import Data.Bool
  open import Data.Empty
  open import Data.List hiding ([_])
  open import Data.Nat
  open import Data.Product
  open import Data.Sum
  open import Data.Unit

  open import Function

  open import Relation.Binary.PropositionalEquality

  module StdLib where

    toSet : Bool → Set
    toSet true  = ⊤
    toSet false = ⊥

  module VariantMachinery (α : Set) (τ : Set) (↑_ : α → τ) (_≈_ : τ → τ → Bool) where

    infixr 5 _▸_

    data Variants : Set where
      [_] : τ → Variants
      _▸_ : τ → Variants → Variants

    _∈_ : τ → Variants → Bool
    e ∈ [ y ]    = e ≈ y
    e ∈ (x ▸ xs) with e ≈ x
    ... | true  = true
    ... | false = e ∈ xs

    -- Intuition: valid pattern matches must match at most these tags.
    [<_] : Variants → Set
    [< n ] = Σ α (λ x → StdLib.toSet $ (↑ x) ∈ n)

    -- Intuition: valid pattern matches must match at least these tags.
    [>_] : Variants → Set
    [> [ y ]  ] = Σ α (λ x → StdLib.toSet $ (↑ x) ≈ y)
    [> y ▸ ys ] = Σ α (λ x → StdLib.toSet $ (↑ x) ≈ y) ⊎ [> ys ]

  module Test where

    data Size : Set where
      four    : Size
      seven   : Size
      eight   : Size
      eleven  : Size
      sixteen : Size

    data Tag : Set where
      `four    : Tag
      `seven   : Tag
      `eight   : Tag
      `eleven  : Tag
      `sixteen : Tag

    _≈_ : Tag → Tag → Bool
    `four    ≈ `four    = true
    `four    ≈ _        = false
    `seven   ≈ `seven   = true
    `seven   ≈ _        = false
    `eight   ≈ `eight   = true
    `eight   ≈ _        = false
    `eleven  ≈ `eleven  = true
    `eleven  ≈ _        = false
    `sixteen ≈ `sixteen = true
    `sixteen ≈ _        = false

    ↑ : Size → Tag
    ↑ four    = `four
    ↑ seven   = `seven
    ↑ eight   = `eight
    ↑ eleven  = `eleven
    ↑ sixteen = `sixteen

    open VariantMachinery Size Tag ↑ _≈_

    Bit : Set
    Bit = Bool

    private

      postulate
        assertFalse : {α : Set} → α

      Vect : Set → Set
      Vect α = List Bit

    Sizes : Set
    Sizes = [< `four ▸ `seven ▸ `eight ▸ `eleven ▸ [ `sixteen ] ]

    Nibble : Set
    Nibble = Vect [< [ `four ] ] 

    toNibble : Bool → Bool → Bool → Bool → Nibble
    toNibble b1 b2 b3 b4 = b1 ∷ b2 ∷ b3 ∷ b4 ∷ []

    fromNibble : Nibble → (Bool × Bool × Bool × Bool)
    fromNibble (b1 ∷ b2 ∷ b3 ∷ b4 ∷ []) = (b1 , b2 , b3 , b4)
    fromNibble _                        = assertFalse