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