module RecursiveTypes.Coinductive.Subtyping where

open import Data.Empty
  using ( ⊥-elim )

open import Data.Integer
  using ( +_ )

open import Data.Product
  using ( _,_ ; proj₁ ; proj₂ ; _×_ ; Σ-syntax )

open import Data.Sum
  using ( _⊎_ ; inj₁ ; inj₂ ; [_,_] )

open import Function
  using ( _∘_ )

open import Relation.Binary
  using ( Reflexive ; Transitive )

open import Relation.Binary.PropositionalEquality
  using ( _≡_ ; _≢_ ; refl ; cong₂ )

open import Relation.Nullary
  using ( ¬_ )

open import RecursiveTypes.Coinductive.Type

open import RecursiveTypes.Coinductive.Semantics
  hiding ( _×_ )

open import RecursiveTypes.Value

infix 8 _≤_ _∞≤_

-- Subtyping, with the rule for pairs defined coinductively.  The paper defines
-- all of these rules coinductively, but as all rules clearly deconstruct at
-- least one of the types into its components, only the one which operates on
-- the point of recursion needs to be coinductive to ensure infinite types are
-- able to subtype one another.
mutual
  data _≤_ : Type → Type → Set where
    int : Int ≤ Int
    pair : ∀ {A B C D}
           → A ∞≤ C → B ∞≤ D → A ⨯ B ≤ C ⨯ D
    left : ∀ {A B C} → A ≤ B → A ≤ B ∨ C
    right : ∀ {A B C} → A ≤ C → A ≤ B ∨ C
    union : ∀ {A B C} → A ≤ C → B ≤ C → A ∨ B ≤ C
    bottom : ∀ {A B} → ¬ ⟦ A ⟧ → A ≤ B

  -- As with the coinductive types, the point of recursion is defined using a
  -- coinductive record declaration.
  record _∞≤_ (A B : ∞Type) : Set where
    coinductive
    constructor delay
    field sub : type A ≤ type B

open _∞≤_ public

-- A lemma that the ordering of unions in the subtype does not affect the
-- subtype relation.
flip-union₁ : ∀ {A B C} → A ∨ B ≤ C → B ∨ A ≤ C
flip-union₁ (left p) = left (flip-union₁ p)
flip-union₁ (right p) = right (flip-union₁ p)
flip-union₁ (union p q) = union q p
flip-union₁ (bottom ¬x) = bottom (¬x ∘ [ inj₂ , inj₁ ])

-- A lemma that the ordering of unions in the supertype does not affect the
-- subtype relation.
flip-union₂ : ∀ {A B C} → A ≤ B ∨ C → A ≤ C ∨ B
flip-union₂ (left p) = right p
flip-union₂ (right p) = left p
flip-union₂ (union p q) = union (flip-union₂ p) (flip-union₂ q)
flip-union₂ (bottom ¬x) = bottom ¬x

-- Subtyping is naturally reflexive.
mutual
  reflexive : Reflexive _≤_
  reflexive {Int}   = int
  reflexive {A ⨯ B} = pair ∞reflexive ∞reflexive
  reflexive {A ∨ B} = union (left reflexive) (right reflexive)

  -- Again, we use a copattern to enforce productivity.
  ∞reflexive : Reflexive _∞≤_
  sub ∞reflexive = reflexive

-- Subsets between the semantic interpretation of the coinductive types A and B
-- is defined as a proof that, for every value x in A, there exists a
-- corresponding y in B such that the embedding of x and y into the Value type
-- are equivalent.  Every Value that can be generated by the embed function for
-- the type A can also be generated by embed for the type B.
⟦_⟧⊆⟦_⟧ : Type → Type → Set
⟦ A ⟧⊆⟦ B ⟧ = (x : ⟦ A ⟧) → Σ[ y ∈ ⟦ B ⟧ ] embed x ≡ embed y

⟦_⟧⊈⟦_⟧ : Type → Type → Set
⟦ A ⟧⊈⟦ B ⟧ = Σ[ x ∈ ⟦ A ⟧ ] ((y : ⟦ B ⟧) → embed x ≢ embed y)

-- Subtyping is a sound argument for this new subset relation: a proof of
-- subtyping between types A and B implies a proof that their meanings are
-- subsets.
{-# TERMINATING #-}
≤-sound : ∀ {A B} → A ≤ B → ⟦ A ⟧⊆⟦ B ⟧
≤-sound int         x        = x , refl
≤-sound (left p)    x        with ≤-sound p x
≤-sound (left p)    x        | y , q = inj₁ y , q
≤-sound (right p)   x        with ≤-sound p x
≤-sound (right p)   x        | y , q = inj₂ y , q
≤-sound (pair p q)  (w , x)  with ≤-sound (sub p) w | ≤-sound (sub q) x
≤-sound (pair p q)  (w , x)  | y , r | z , s = (y , z) , cong₂ _,_ r s
≤-sound (union p q) (inj₁ x) = ≤-sound p x
≤-sound (union p q) (inj₂ y) = ≤-sound q y
≤-sound (bottom ¬x) x        = ⊥-elim (¬x x)

-- Subtyping is naturally transitive.
mutual
  transitive : Transitive _≤_
  transitive p           int         = p
  transitive p           (left q)    = left (transitive p q)
  transitive p           (right q)   = right (transitive p q)
  transitive (left p)    (union q r) = transitive p q
  transitive (right p)   (union q r) = transitive p r
  transitive (pair p q)  (pair r s)  = pair (∞transitive p r)
                                            (∞transitive q s)
  transitive (union p q) r           = union (transitive p r)
                                             (transitive q r)
  transitive (bottom ¬x) q           = bottom ¬x
  transitive p           (bottom ¬x) = bottom (¬x ∘ proj₁ ∘ ≤-sound p)

  -- A copattern is also used here.
  ∞transitive : Transitive _∞≤_
  sub (∞transitive p q) = transitive (sub p) (sub q)
