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

module Variants where

  open import Data.Bool
  open import Data.Empty
  open import Data.List
  open import Data.Nat hiding (_≟_)
  open import Data.Product hiding (map)
  open import Data.Sum hiding (map)
  open import Data.Unit hiding (_≟_)

  open import Function

  open import Level

  open import Relation.Nullary
  open import Relation.Binary.PropositionalEquality renaming ([_] to 〈_〉)

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

  data Expression : Set where
    ↑   : ℕ → Expression
    _⊕_ : Expression → Expression → Expression
    _⊗_ : Expression → Expression → Expression

  module MissingStandardLibrary where

    -- Lifting Bool into Set
    toSet : Bool → Set
    toSet true  = ⊤
    toSet false = ⊥

    -- Properties of Boolean negation
    not-not-elim : (b : Bool) → not (not b) ≡ b
    not-not-elim true  = refl
    not-not-elim false = refl

    not-self-adjoint₁ : (b c : Bool) → not b ≡ c → b ≡ not c
    not-self-adjoint₁ true  true  ()
    not-self-adjoint₁ true  false not-b≡c = refl
    not-self-adjoint₁ false true  not-b≡c = refl
    not-self-adjoint₁ false false ()

    not-self-adjoint₂ : (b c : Bool) → b ≡ not c → not b ≡ c
    not-self-adjoint₂ b c b≡not-c = sym $ not-self-adjoint₁ c b $ sym $ b≡not-c

    -- Properties of Boolean disjunction and conjunction
    ∨-elim₂ : (b : Bool) → b ∨ true ≡ true
    ∨-elim₂ true  = refl
    ∨-elim₂ false = refl

    ∨-cases-true₁ : (b c : Bool) → b ∨ c ≡ true → b ≡ true ⊎ c ≡ true
    ∨-cases-true₁ true  c b∨c-true = inj₁ refl
    ∨-cases-true₁ false c b∨c-true = inj₂ b∨c-true

    ∨-cases-true₂ : (b c : Bool) → b ≡ true ⊎ c ≡ true → b ∨ c ≡ true
    ∨-cases-true₂ true  c b⊎c≡true = refl
    ∨-cases-true₂ false c (inj₁ ())
    ∨-cases-true₂ false c (inj₂ y) = y

    ∧-cases-true₁ : (b c : Bool) → b ∧ c ≡ true → (b ≡ true) × (c ≡ true)
    ∧-cases-true₁ true  c     b∧c≡true = refl , b∧c≡true
    ∧-cases-true₁ false true  b∧c≡true = b∧c≡true , refl
    ∧-cases-true₁ false false b∧c≡true = b∧c≡true , b∧c≡true

    ∧-cases-true₂ : (b c : Bool) → (b ≡ true) × (c ≡ true) → (b ∧ c) ≡ true
    ∧-cases-true₂ true  c b≡true×c≡true = proj₂ b≡true×c≡true
    ∧-cases-true₂ false c b≡true×c≡true = proj₁ b≡true×c≡true

    -- Boolean equality
    _≈_ : Bool → Bool → Bool
    true  ≈ c = c
    false ≈ c = not c

    ≈-reflexive : (b : Bool) → b ≈ b ≡ true
    ≈-reflexive true  = refl
    ≈-reflexive false = refl

    ≈-true₁ : (b c : Bool) → b ≈ c ≡ true → b ≡ c
    ≈-true₁ true  true  b≈c-true = refl
    ≈-true₁ true  false ()
    ≈-true₁ false true  b≈c-true = b≈c-true
    ≈-true₁ false false b≈c-true = refl

    ≈-true₂ : (b c : Bool) → b ≡ c → b ≈ c ≡ true
    ≈-true₂ b c b≡c rewrite b≡c = ≈-reflexive c

  -- Tags, and their equality
  module Tag where

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

    toTag : Expression → Tag
    toTag (↑ _)   = literal
    toTag (_ ⊕ _) = plus
    toTag (_ ⊗ _) = times

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

    _≉_ : Tag → Tag → Bool
    l ≉ r = not $ l ≈ r

    ≈-≉-dual : (l r : Tag) → l ≈ r ≡ not (l ≉ r)
    ≈-≉-dual l r rewrite MissingStandardLibrary.not-not-elim (l ≈ r) = refl

    ≈-reflexive : (l : Tag) → l ≈ l ≡ true
    ≈-reflexive literal = refl
    ≈-reflexive plus    = refl
    ≈-reflexive times   = refl

    ≈-true₁ : (l r : Tag) → l ≈ r ≡ true → l ≡ r
    ≈-true₁ literal literal l≈r-true = refl
    ≈-true₁ literal plus    ()
    ≈-true₁ literal times   ()
    ≈-true₁ plus    literal ()
    ≈-true₁ plus    plus    l≈r-true = refl
    ≈-true₁ plus    times   ()
    ≈-true₁ times   literal ()
    ≈-true₁ times   plus    ()
    ≈-true₁ times   times   l≈r-true = refl

    ≈-true₂ : (l r : Tag) → l ≡ r → l ≈ r ≡ true
    ≈-true₂ l r l≡r rewrite l≡r = ≈-reflexive r

    ≉-true₁ : (l r : Tag) → l ≉ r ≡ true → l ≢ r
    ≉-true₁ literal literal ()
    ≉-true₁ literal plus    l≉r-true = λ ()
    ≉-true₁ literal times   l≉r-true = λ ()
    ≉-true₁ plus    literal l≉r-true = λ ()
    ≉-true₁ plus    plus    ()
    ≉-true₁ plus    times   l≉r-true = λ ()
    ≉-true₁ times   literal l≉r-true = λ ()
    ≉-true₁ times   plus    l≉r-true = λ ()
    ≉-true₁ times   times   ()

    ≉-true₂ : (l r : Tag) → l ≢ r → l ≉ r ≡ true
    ≉-true₂ literal literal l≢r = ⊥-elim $ l≢r refl
    ≉-true₂ literal plus    l≢r = refl
    ≉-true₂ literal times   l≢r = refl
    ≉-true₂ plus    literal l≢r = refl
    ≉-true₂ plus    plus    l≢r = ⊥-elim $ l≢r refl
    ≉-true₂ plus    times   l≢r = refl
    ≉-true₂ times   literal l≢r = refl
    ≉-true₂ times   plus    l≢r = refl
    ≉-true₂ times   times   l≢r = ⊥-elim $ l≢r refl

    ≈-≉-decidable : (l r : Tag) → l ≈ r ≡ true ⊎ l ≉ r ≡ true
    ≈-≉-decidable literal literal = inj₁ refl
    ≈-≉-decidable literal plus    = inj₂ refl
    ≈-≉-decidable literal times   = inj₂ refl
    ≈-≉-decidable plus    literal = inj₂ refl
    ≈-≉-decidable plus    plus    = inj₁ refl
    ≈-≉-decidable plus    times   = inj₂ refl
    ≈-≉-decidable times   literal = inj₂ refl
    ≈-≉-decidable times   plus    = inj₂ refl
    ≈-≉-decidable times   times   = inj₁ refl

  module DeqSet where

    record DeqSet (α : Set) : Set where
      constructor
        mkDeqSet
      field
        _≈_           : α → α → Bool
        _≉_           : α → α → Bool
        ≈-≉-dual      : (l r : α) → l ≈ r ≡ not (l ≉ r)
        ≈-true₁       : (l r : α) → l ≈ r ≡ true → l ≡ r
        ≈-true₂       : (l r : α) → l ≡ r → l ≈ r ≡ true
        ≉-true₁       : (l r : α) → l ≉ r ≡ true → l ≢ r
        ≉-true₂       : (l r : α) → l ≢ r → l ≉ r ≡ true
        ≈-≉-decidable : (l r : α) → l ≈ r ≡ true ⊎ l ≉ r ≡ true

    Tag-DeqSet : DeqSet Tag.Tag
    Tag-DeqSet = mkDeqSet Tag._≈_ Tag._≉_ Tag.≈-≉-dual Tag.≈-true₁ Tag.≈-true₂ Tag.≉-true₁ Tag.≉-true₂ Tag.≈-≉-decidable

    _∈_ : {α : Set} → ⦃ DS : DeqSet α ⦄ → α → List α → Bool
    _∈_ ⦃ DS ⦄ e []       = false
    _∈_ ⦃ DS ⦄ e (x ∷ xs) = DeqSet._≈_ DS e x ∨ (e ∈ xs)

    _⊆_ : {α : Set} → ⦃ DS : DeqSet α ⦄ → List α → List α → Bool
    _⊆_ ⦃ DS ⦄ sub sup = all (λ x → x ∈ sup) sub

    -- (DeqSet._≈_ DS x x ∨ x ∈ xs) ∧ foldr _∧_ true (map (λ x' → DeqSet._≈_ DS x' x ∨ x' ∈ xs) xs) ≡ true
    ⊆-reflexive : {α : Set} → ⦃ DS : DeqSet α ⦄ → (l : List α) → l ⊆ l ≡ true
    ⊆-reflexive ⦃ DS ⦄ []       = refl
    ⊆-reflexive ⦃ DS ⦄ (x ∷ xs)
      rewrite
        ⊆-reflexive xs = {!!} -- MissingStandardLibrary.∧-cases-true₂ (DeqSet._≈_ DS x x ∨ x ∈ xs) _ (x≈x-∨-x-∈-xs-≡-true , {!!})
      where
        x≈x-∨-x-∈-xs-≡-true : (DeqSet._≈_ DS x x) ∨ (x ∈ xs) ≡ true
        x≈x-∨-x-∈-xs-≡-true = MissingStandardLibrary.∨-cases-true₂ _ _ (inj₁ $ DeqSet.≈-true₂ DS x x refl)

        xs-⊆-xs-≡-true : xs ⊆ xs ≡ true
        xs-⊆-xs-≡-true = ⊆-reflexive xs

    x∷xs-⊆-ys-to-x-∈-ys : {α : Set} → ⦃ DS : DeqSet α ⦄ → (x : α) → (xs ys : List α) → (x ∷ xs) ⊆ ys ≡ true → x ∈ ys ≡ true
    x∷xs-⊆-ys-to-x-∈-ys ⦃ DS ⦄ x xs []         x∷xs⊆ys = x∷xs⊆ys
    x∷xs-⊆-ys-to-x-∈-ys ⦃ DS ⦄ x xs (x' ∷ xs') x∷xs⊆ys with x ∈ xs'
    ... | true  = MissingStandardLibrary.∨-elim₂ $ DeqSet._≈_ DS x x'
    ... | false = MissingStandardLibrary.∨-cases-true₂ (DeqSet._≈_ DS x x') false $ inj₁ x≈x'≡true
      where
        x≈x'∨false≡true∧foldr≡true : (DeqSet._≈_ DS x x' ∨ false) ≡ true × foldr _∧_ true (Data.List.map (λ x0 → DeqSet._≈_ DS x0 x' ∨ x0 ∈ xs') xs) ≡ true
        x≈x'∨false≡true∧foldr≡true = MissingStandardLibrary.∧-cases-true₁ (DeqSet._≈_ DS x x' ∨ false) (foldr _∧_ true (map (λ x → DeqSet._≈_ DS x x' ∨ x ∈ xs') xs)) x∷xs⊆ys

        x≈x'∨false≡true : DeqSet._≈_ DS x x' ∨ false ≡ true
        x≈x'∨false≡true = proj₁ $ x≈x'∨false≡true∧foldr≡true

        x≈x'≡true : DeqSet._≈_ DS x x' ≡ true
        x≈x'≡true with MissingStandardLibrary.∨-cases-true₁ (DeqSet._≈_ DS x x') false x≈x'∨false≡true
        ... | inj₁ p = p
        ... | inj₂ ()

    -- Oh `destruct' how I miss thee...
    false≡true-to-α : {α : Set} → false ≡ true → α
    false≡true-to-α ()

    x∷xs-⊆-ys-to-xs-⊆-ys : {α : Set} → ⦃ DS : DeqSet α ⦄ → (x : α) → (xs ys : List α) → (x ∷ xs) ⊆ ys ≡ true → xs ⊆ ys ≡ true
    x∷xs-⊆-ys-to-xs-⊆-ys ⦃ DS ⦄ x xs ys x∷xs⊆ys with x ∈ ys
    ... | true  = x∷xs⊆ys
    ... | false = false≡true-to-α x∷xs⊆ys

    x-∈-xs-to-xs-⊆-ys-to-x-∈-ys : {α : Set} → ⦃ DS : DeqSet α ⦄ → (x : α) → (xs ys : List α) → x ∈ xs ≡ true → xs ⊆ ys ≡ true → x ∈ ys ≡ true
    x-∈-xs-to-xs-⊆-ys-to-x-∈-ys ⦃ DS ⦄ x []        ys x∈xs≡true xs⊆ys≡true = false≡true-to-α x∈xs≡true
    x-∈-xs-to-xs-⊆-ys-to-x-∈-ys ⦃ DS ⦄ x (x' ∷ xs) ys x∈xs≡true xs⊆ys≡true with DeqSet._≈_ DS x x' | inspect (λ x'' → DeqSet._≈_ DS x'' x') $ x
    ... | true  | 〈 p 〉 = subst _ (sym $ DeqSet.≈-true₁ DS x x' p) (proj₁ $ MissingStandardLibrary.∧-cases-true₁ (x' ∈ ys) (foldr _∧_ true (map (λ x0 → x0 ∈ ys) xs)) xs⊆ys≡true)
    ... | false | 〈 p 〉 = x-∈-xs-to-xs-⊆-ys-to-x-∈-ys x xs ys x∈xs≡true foldr-∧-≡-true
      where
        foldr-∧-≡-true : foldr _∧_ true (map (λ x → x ∈ ys) xs) ≡ true
        foldr-∧-≡-true = proj₂ $ MissingStandardLibrary.∧-cases-true₁ (x' ∈ ys) _ xs⊆ys≡true
  
  module Random where

    _∈_ : Expression → List Tag.Tag → Set
    e ∈ [] = ⊥
    e ∈ (x ∷ xs) with Tag._≈_ x $ Tag.toTag e
    ... | true  = ⊤
    ... | false = e ∈ xs

    `_ : List Tag.Tag → Set
    ` xs = Σ Expression (λ x → x ∈ xs)

    -- XXX: No syntax for list literals?
    test₁ : ` (Tag.literal ∷ Tag.plus ∷ []) → ` [ Tag.literal ]
    test₁ (↑ y    , tt)     = ↑ y , tt
    test₁ (y ⊕ y' , tt)     = ↑ 5 , tt
    test₁ (y ⊗ y' , absurd) = ⊥-elim absurd

    ⟦_⟧↑ : ` [ Tag.literal ] → ℕ
    ⟦ ↑ y    , tt ⟧↑     = y
    ⟦ y ⊕ y' , absurd ⟧↑ = ⊥-elim absurd
    ⟦ y ⊗ y' , absurd ⟧↑ = ⊥-elim absurd

    ⟦_⟧⊕_ : ` [ Tag.plus ] → (Expression → ℕ) → ℕ
    ⟦ ↑ y    , absurd ⟧⊕ f = ⊥-elim absurd
    ⟦ y ⊕ y' , tt     ⟧⊕ f = f y + f y'
    ⟦ y ⊗ y' , absurd ⟧⊕ f = ⊥-elim absurd

    ⟦_⟧⊗_ : ` [ Tag.times ] → (Expression → ℕ) → ℕ
    ⟦ ↑ y    , absurd ⟧⊗ f = ⊥-elim absurd
    ⟦ y ⊕ y' , absurd ⟧⊗ f = ⊥-elim absurd
    ⟦ y ⊗ y' , tt     ⟧⊗ f = f y * f y'

    ⟦_⟧ : Expression → ℕ
    ⟦ ↑ y    ⟧ = ⟦ ↑ y ⟧
    ⟦ y ⊕ y' ⟧ = ⟦ y ⊕ y' , tt ⟧⊕ ⟦_⟧
    ⟦ y ⊗ y' ⟧ = ⟦ y ⊗ y' , tt ⟧⊗ ⟦_⟧