open import CoverageCheck.Prelude
open import CoverageCheck.Name
open import CoverageCheck.GlobalScope using (Globals)
open import CoverageCheck.Syntax
open import CoverageCheck.Instance

module CoverageCheck.Subsumption
  ⦃ @0 globals : Globals ⦄
  ⦃ @0 sig : Signature ⦄
  where

private open module @0 G = Globals globals

infix  Subsumption Subsumptions _⊈_ _⊈*_

private
  variable
    α β : Ty
    αs βs : Tys
    d : NameData
    @0 α0 β0 : Ty
    @0 αs0 βs0 : Tys
    @0 d0 : NameData

--------------------------------------------------------------------------------
-- Subsumption

data Subsumption : (@0 p q : Pattern α0) → Type
Subsumptions : (@0 ps qs : Patterns αs0) → Type

syntax Subsumption  p  q  = p ⊆ q
syntax Subsumptions ps qs = ps ⊆* qs

-- p ⊆ q : q subsumes p
-- Not complete; for example, — ⊆ (true ∣ false) is not derivable
data Subsumption where
  SWild : {@0 p : Pattern α0} → p ⊆ —

  SCon : {c : NameCon d0}
    → (let @0 αs : Tys
           αs = argsTy (dataDefs sig d0) c)
    → {@0 ps qs : Patterns αs}
    → (subs : ps ⊆* qs)
    → con c ps ⊆ con c qs

  SOrL : {@0 p q r : Pattern α0}
    → (sub : p ⊆ q)
    → p ⊆ (q ∣ r)

  SOrR : {@0 p q r : Pattern α0}
    → (sub : p ⊆ r)
    → p ⊆ (q ∣ r)

  SOr : {@0 p q r : Pattern α0}
    → (sub₁ : p ⊆ r)
    → (sub₂ : q ⊆ r)
    → (p ∣ q) ⊆ r

{-# COMPILE AGDA2HS Subsumption deriving Show #-}

pattern —⊆           = SWild
pattern con⊆ subs    = SCon subs
pattern ⊆∣ˡ sub      = SOrL sub
pattern ⊆∣ʳ sub      = SOrR sub
pattern ∣⊆ sub₁ sub₂ = SOr sub₁ sub₂

Subsumptions = HPointwise (λ p q → p ⊆ q)

{-# COMPILE AGDA2HS Subsumptions #-}

_⊈_ : (@0 p q : Pattern α0) → Type
p ⊈ q = ¬ p ⊆ q

_⊈*_ : (@0 ps qs : Patterns αs0) → Type
qs ⊈* ps = ¬ ps ⊆* qs

--------------------------------------------------------------------------------
-- Properties of the subsumption relation

-- List of wildcards subsumes any list of patterns
sWilds : {@0 ps : Patterns αs} → ps ⊆* —*
sWilds {[]}     {[]}    = []
sWilds {α ∷ αs} {_ ∷ _} = —⊆ ∷ sWilds
{-# COMPILE AGDA2HS sWilds #-}
syntax sWilds = —⊆*

-- ⊆ is reflexive
⊆-refl  : (p : Pattern α0) → p ⊆ p
⊆*-refl : (ps : Patterns αs0) → ps ⊆* ps

⊆-refl —          = —⊆
⊆-refl (con c ps) = con⊆ (⊆*-refl ps)
⊆-refl (p ∣ q)    = ∣⊆ (⊆∣ˡ (⊆-refl p)) (⊆∣ʳ (⊆-refl q))

⊆*-refl []       = []
⊆*-refl (p ∷ ps) = ⊆-refl p ∷ ⊆*-refl ps

module _ {@0 c : NameCon d0}
  (let @0 αs : Tys
       αs = argsTy (dataDefs sig d0) c)
  {@0 ps qs : Patterns αs}
  where

  -- Inversion lemma for con⊆
  sConInv : (con c ps ⊆ con c qs) → ps ⊆* qs
  sConInv (con⊆ subs) = subs
  {-# COMPILE AGDA2HS sConInv #-}
  syntax sConInv = con⊆⁻

-- ⊆ implies the "semantic" version of subsumption relation
subsume : {p q : Pattern α0} {v : Value α0}
  → p ⊆ q
  → (v ≼ p → v ≼ q)
subsumes : {ps qs : Patterns αs0} {vs : Values αs0}
  → ps ⊆* qs
  → (vs ≼* ps → vs ≼* qs)

subsume —⊆ inst = —≼
subsume (con⊆ subs) (con≼ insts) = con≼ (subsumes subs insts)
subsume (⊆∣ˡ sub) inst = ∣≼ˡ (subsume sub inst)
subsume (⊆∣ʳ sub) inst = ∣≼ʳ (subsume sub inst)
subsume (∣⊆ sub _) (∣≼ˡ inst) = subsume sub inst
subsume (∣⊆ _ sub) (∣≼ʳ inst) = subsume sub inst

subsumes [] [] = []
subsumes (sub ∷ subs) (inst ∷ insts) = subsume sub inst ∷ subsumes subs insts

⊆only : {p : Pattern α0} {v : Value α0}
  → v ≼ p
  → only v ⊆ p
⊆onlys : {ps : Patterns αs0} {vs : Values αs0}
  → vs ≼* ps
  → onlys vs ⊆* ps

⊆only —≼ = —⊆
⊆only (con≼ insts) = con⊆ (⊆onlys insts)
⊆only (∣≼ˡ inst) = ⊆∣ˡ (⊆only inst)
⊆only (∣≼ʳ inst) = ⊆∣ʳ (⊆only inst)

⊆onlys [] = []
⊆onlys (inst ∷ insts) = ⊆only inst ∷ ⊆onlys insts