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

module Variants where

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

  open import Function

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

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

  data Expression (α : Set) : 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
    ∨-elim₂ : (b : Bool) → b ∨ true ≡ true
    ∨-elim₂ true  = refl
    ∨-elim₂ false = refl

    ∨-cases : (b c : Bool) → b ∨ c ≡ true → b ≡ true ⊎ c ≡ true
    ∨-cases true  c b∨c-true = inj₁ refl
    ∨-cases false c b∨c-true = inj₂ b∨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 : {α : Set} → 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

    x∷xs-⊂-to-∈ : {α : Set} → ⦃ DS : DeqSet α ⦄ → (x : α) → (xs ys : List α) → (x ∷ xs) ⊂ ys ≡ true → x ∈ ys ≡ true
    x∷xs-⊂-to-∈ ⦃ DS ⦄ x xs []         x∷xs⊂ys = x∷xs⊂ys
    x∷xs-⊂-to-∈ ⦃ DS ⦄ x xs (x' ∷ xs') x∷xs⊂ys with x ∈ xs' | inspect (λ x → x ∈ xs') $ x
    ... | true  | 〈 p 〉 = MissingStandardLibrary.∨-elim₂ $ DeqSet._≈_ DS x x'
    ... | false | 〈 p 〉 = {!? $ MissingStandardLibrary.∨-cases ? ? p !}
  
  module Random where
  -- Random stuff

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

    holds-for-tag-specialise : {α : Set} → (Q : Expression α → Set) → (x : Expression α) →
      [ Q holds-for (Tag.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'.

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

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

    -- The following two functions are coercions in Matita.
    subexpression : List Tag.Tag → Set → Set
    subexpression l = λ α → Subexpression α l

    mkSubexpression : {α : Set} → (l : List Tag.Tag) → (e : Expression α) →
      MissingStandardLibrary.toSet $ e ∈ l → Subexpression α l
    mkSubexpression l e p = record { element = e; ∈-element = p }

    -- Missing from the Agda standard library, seemingly.
    member : {α : Set} → (α → α → Bool) → α → List α → Bool
    member p e []       = false
    member p e (x ∷ xs) = (p e x) ∨ (member p e xs)