source: Papers/polymorphic-variants-2012/Variants.agda @ 2542

module Variants where

  open import Data.Bool
  open import Data.Empty
  open import Data.List
  open import Data.Nat
  open import Data.Unit

  open import Function

  open import Relation.Binary.PropositionalEquality

  -- The following is ported from `test.ma'.

  data Expression (α : Set) : Set where
    ↑   : ℕ → Expression α
    _⊕_ : Expression α → Expression α → Expression α
    _⊗_ : Expression α → Expression α → Expression α

  data Tag : Set where
    literal : Tag
    plus    : Tag
    times   : Tag

  _≈_ : Tag → Tag → Bool
  literal ≈ literal = true
  plus    ≈ plus    = true
  times   ≈ times   = true
  _       ≈ _       = false

  toTag : {α : Set} → Expression α → Tag
  toTag (↑ _)   = literal
  toTag (_ ⊕ _) = plus
  toTag (_ ⊗ _) = times

  [_holds-for_] : {α : Set} → (Expression α → Set) → Tag → Set
  [ Q holds-for literal ] = (n : ℕ) → Q $ ↑ n
  [ Q holds-for plus ]    = (x y : _) → Q $ x ⊕ y
  [ Q holds-for times ]   = (x y : _) → Q $ x ⊗ y

  holds-for-tag-specialise : {α : Set} → (Q : Expression α → Set) → (x : Expression α) →
    [ Q holds-for (toTag x) ] → Q x
  holds-for-tag-specialise Q (↑ n)   Q-holds-for-toTag = Q-holds-for-toTag n
  holds-for-tag-specialise Q (x ⊕ y) Q-holds-for-toTag = Q-holds-for-toTag x y
  holds-for-tag-specialise Q (x ⊗ y) Q-holds-for-toTag = Q-holds-for-toTag x y

  -- The following is ported from `variants.ma'.

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

  _∈_ : {α : Set} → Expression α → List Tag → Bool
  tag ∈ []        = false
  tag ∈ (x ∷ xs) = (toTag tag ≈ x) ∨ (tag ∈ xs)

  record Subexpression (α : Set) (l : List Tag) : Set where
    field
      element   : Expression α
      ∈-element : toSet $ element ∈ l

  -- Ack!  We have no coercions in Agda.
  ofQ : {α : Set} → (l : List Tag) → (Q : Subexpression α l → Set) → Expression α → Set
  ofQ l s e = ?