{-# OPTIONS --safe #-}

module CBPV.Axiom where

open import Data.List using (List; []; _∷_; [_]; map)
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Membership.Propositional.Properties using (∈-map⁺)
open import Data.List.Relation.Unary.Any using () renaming (here to ↓_; there to ↑_)
open import Data.List.Relation.Unary.All using (_∷_; tabulate) renaming ([] to •⟩)
open import Data.Product using () renaming (_,_ to _⊩_)
open import Level using (0ℓ)
open import Relation.Binary using (Rel)
open import Relation.Binary.PropositionalEquality using (refl)

open import CBPV.Family
open import CBPV.Term
open import CBPV.Type

pattern _∶_ a b = a ∷ b

pattern x₀ = var (↓ refl)
pattern x₁ = var (↑ ↓ refl)
pattern x₂ = var (↑ ↑ ↓ refl)
pattern x₃ = var (↑ ↑ ↑ ↓ refl)
pattern x₄ = var (↑ ↑ ↑ ↑ ↓ refl)
pattern x₅ = var (↑ ↑ ↑ ↑ ↑ ↓ refl)

pattern 𝔞⟨_ ε = mvar (↓ refl) ε
pattern 𝔟⟨_ ε = mvar (↑ ↓ refl) ε
pattern 𝔠⟨_ ε = mvar (↑ ↑ ↓ refl) ε
pattern 𝔡⟨_ ε = mvar (↑ ↑ ↑ ↓ refl) ε

pattern ◌ᵃ⟨_ ε = 𝔞⟨ ε
pattern ◌ᵇ⟨_ ε = 𝔟⟨ ε
pattern ◌ᶜ⟨_ ε = 𝔠⟨ ε
pattern ◌ᵈ⟨_ ε = 𝔡⟨ ε

infix 19 _⟩
infix 18 𝔞⟨_ 𝔟⟨_ 𝔠⟨_ 𝔡⟨_ ◌ᵃ⟨_ ◌ᵇ⟨_ ◌ᶜ⟨_ ◌ᵈ⟨_
infixr 18 ⟨_ _∶_

pattern 𝔞 = 𝔞⟨ •⟩
pattern 𝔟 = 𝔟⟨ •⟩
pattern 𝔠 = 𝔠⟨ •⟩
pattern 𝔡 = 𝔡⟨ •⟩
pattern ◌ᵃ = ◌ᵃ⟨ •⟩
pattern ◌ᵇ = ◌ᵇ⟨ •⟩
pattern ◌ᶜ = ◌ᶜ⟨ •⟩
pattern ◌ᵈ = ◌ᵈ⟨ •⟩

pattern _⟩ a = a ∶ •⟩
pattern ⟨_ as = as

pattern []⊩_ C = [] ⊩ C
pattern [_]⊩_ A C = (A ∷ []) ⊩ C
pattern [_•_]⊩_ A A′ C = (A ∷ A′ ∷ []) ⊩ C

private
  variable
    A A′ A′′ : ValType
    B B′ : CompType

infix 0 _⨾_▹⊢ᵛ_≋_ _⨾_▹⊢ᶜ_≋_

data _⨾_▹⊢ᵛ_≋_ : ∀ Vs Cs {A} → Rel (⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ [] ⊢ᵛ A) 0ℓ
data _⨾_▹⊢ᶜ_≋_ : ∀ Vs Cs {B} → Rel (⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ [] ⊢ᶜ B) 0ℓ

data _⨾_▹⊢ᵛ_≋_ where
  -- Structural
  have : ([]⊩ A) ∷ ([ A ]⊩ A′) ∷ [] ⨾ [] ▹⊢ᵛ have 𝔞 be 𝔟⟨ x₀ ⟩ ≋ 𝔟⟨ 𝔞 ⟩
  -- Beta
  𝟙β : [ []⊩ A ] ⨾ [] ▹⊢ᵛ unpoint tt 𝔞 ≋ 𝔞
  +β₁ :
    ([]⊩ A) ∷ ([ A ]⊩ A′′) ∷ ([ A′ ]⊩ A′′) ∷ [] ⨾ [] ▹⊢ᵛ
      untag (inl 𝔞) (𝔟⟨ x₀ ⟩) (𝔠⟨ x₀ ⟩)
    ≋
      𝔟⟨ 𝔞 ⟩
  +β₂ :
    ([]⊩ A′) ∷ ([ A ]⊩ A′′) ∷ ([ A′ ]⊩ A′′) ∷ [] ⨾ [] ▹⊢ᵛ
      untag (inr 𝔞) (𝔟⟨ x₀ ⟩) (𝔠⟨ x₀ ⟩)
    ≋
      𝔠⟨ 𝔞 ⟩
  ×β :
    ([]⊩ A) ∷ ([]⊩ A′) ∷ ([ A • A′ ]⊩ A′′) ∷ [] ⨾ [] ▹⊢ᵛ
      unpair (𝔞 , 𝔟) (𝔠⟨ x₀ ∶ x₁ ⟩)
    ≋
      𝔠⟨ 𝔞 ∶ 𝔟 ⟩
  ⟶β : ([]⊩ A) ∷ ([ A ]⊩ A′) ∷ [] ⨾ [] ▹⊢ᵛ 𝔞 ‵ ƛ 𝔟⟨ x₀ ⟩ ≋ 𝔟⟨ 𝔞 ⟩
  -- Eta
  Uη : [ []⊩ (U B) ] ⨾ [] ▹⊢ᵛ thunk (force 𝔞) ≋ 𝔞
  𝟘η : ([]⊩ 𝟘) ∷ ([ 𝟘 ]⊩ A) ∷ [] ⨾ [] ▹⊢ᵛ absurd 𝔞 ≋ 𝔟⟨ 𝔞 ⟩
  𝟙η : ([]⊩ 𝟙) ∷ ([ 𝟙 ]⊩ A) ∷ [] ⨾ [] ▹⊢ᵛ unpoint 𝔞 (𝔟⟨ tt ⟩) ≋ 𝔟⟨ 𝔞 ⟩
  +η :
    ([]⊩ (A + A′)) ∷ ([ A + A′ ]⊩ A′′) ∷ [] ⨾ [] ▹⊢ᵛ
      untag 𝔞 (𝔟⟨ inl x₀ ⟩) (𝔟⟨ inr x₀ ⟩)
    ≋
      𝔟⟨ 𝔞 ⟩
  ×η :
    ([]⊩ (A × A′)) ∷ ([ A × A′ ]⊩ A′′) ∷ [] ⨾ [] ▹⊢ᵛ
      unpair 𝔞 (𝔟⟨ (x₀ , x₁) ⟩)
    ≋
      𝔟⟨ 𝔞 ⟩
  ⟶η : [ []⊩ (A ⟶ A′) ] ⨾ [] ▹⊢ᵛ ƛ (x₀ ‵ 𝔞) ≋ 𝔞

data _⨾_▹⊢ᶜ_≋_ where
  -- Structural
  have : [ []⊩ A ] ⨾ [ [ A ]⊩ B ] ▹⊢ᶜ have 𝔞 be 𝔞⟨ x₀ ⟩ ≋ 𝔞⟨ 𝔞 ⟩
  -- Beta
  Uβ : [] ⨾ [ []⊩ B ] ▹⊢ᶜ force (thunk 𝔞) ≋ 𝔞
  𝟙β : [] ⨾ [ []⊩ B ] ▹⊢ᶜ unpoint tt 𝔞 ≋ 𝔞
  +β₁ :
    [ []⊩ A ] ⨾ ([ A ]⊩ B) ∷ ([ A′ ]⊩ B) ∷ [] ▹⊢ᶜ
      untag (inl 𝔞) (𝔞⟨ x₀ ⟩) (𝔟⟨ x₀ ⟩)
    ≋
      𝔞⟨ 𝔞 ⟩
  +β₂ :
    [ []⊩ A′ ] ⨾ ([ A ]⊩ B) ∷ ([ A′ ]⊩ B) ∷ [] ▹⊢ᶜ
      untag (inr 𝔞) (𝔞⟨ x₀ ⟩) (𝔟⟨ x₀ ⟩)
    ≋
      𝔟⟨ 𝔞 ⟩
  ×β :
    ([]⊩ A) ∷ ([]⊩ A′) ∷ [] ⨾ [ [ A • A′ ]⊩ B ] ▹⊢ᶜ
      unpair (𝔞 , 𝔟) (𝔞⟨ x₀ ∶ x₁ ⟩)
    ≋
      𝔞⟨ 𝔞 ∶ 𝔟 ⟩
  Fβ : [ []⊩ A ] ⨾ [ [ A ]⊩ B ] ▹⊢ᶜ return 𝔞 to 𝔞⟨ x₀ ⟩ ≋ 𝔞⟨ 𝔞 ⟩
  ×ᶜβ₁ : [] ⨾ ([]⊩ B) ∷ ([]⊩ B′) ∷ [] ▹⊢ᶜ π₁ (𝔞 , 𝔟) ≋ 𝔞
  ×ᶜβ₂ : [] ⨾ ([]⊩ B) ∷ ([]⊩ B′) ∷ [] ▹⊢ᶜ π₂ (𝔞 , 𝔟) ≋ 𝔟
  ⟶β : [ []⊩ A ] ⨾ [ [ A ]⊩ B ] ▹⊢ᶜ 𝔞 ‵ ƛ 𝔞⟨ x₀ ⟩ ≋ 𝔞⟨ 𝔞 ⟩
  -- Eta
  𝟘η : [ []⊩ 𝟘 ] ⨾ [ [ 𝟘 ]⊩ B ] ▹⊢ᶜ absurd 𝔞 ≋ 𝔞⟨ 𝔞 ⟩
  𝟙η : [ []⊩ 𝟙 ] ⨾ [ [ 𝟙 ]⊩ B ] ▹⊢ᶜ unpoint 𝔞 (𝔞⟨ tt ⟩) ≋ 𝔞⟨ 𝔞 ⟩
  +η :
    [ []⊩ (A + A′) ] ⨾ [ [ A + A′ ]⊩ B ] ▹⊢ᶜ
      untag 𝔞 (𝔞⟨ inl x₀ ⟩) (𝔞⟨ inr x₀ ⟩)
    ≋
      𝔞⟨ 𝔞 ⟩
  ×η :
    [ []⊩ (A × A′) ] ⨾ [ [ A × A′ ]⊩ B ] ▹⊢ᶜ
      unpair 𝔞 (𝔞⟨ (x₀ , x₁) ⟩)
    ≋
      𝔞⟨ 𝔞 ⟩
  Fη : [] ⨾ [ []⊩ (F A) ] ▹⊢ᶜ 𝔞 to return x₀ ≋ 𝔞
  𝟙ᶜη : [] ⨾ [ []⊩ 𝟙 ] ▹⊢ᶜ tt ≋ 𝔞
  ×ᶜη : [] ⨾ [ []⊩ (B × B′) ] ▹⊢ᶜ π₁ 𝔞 , π₂ 𝔞 ≋ 𝔞
  ⟶η : [] ⨾ [ []⊩ (A ⟶ B) ] ▹⊢ᶜ ƛ (x₀ ‵ 𝔞) ≋ 𝔞
  -- Sequencing
  to-to :
    [] ⨾ ([]⊩ (F A)) ∷ ([ A ]⊩ (F A′)) ∷ ([ A′ ]⊩ B) ∷ [] ▹⊢ᶜ
      (𝔞 to 𝔟⟨ x₀ ⟩) to 𝔠⟨ x₀ ⟩
    ≋
      𝔞 to (𝔟⟨ x₀ ⟩ to 𝔠⟨ x₀ ⟩)
  to-π₁ :
    [] ⨾ ([]⊩ (F A)) ∷ ([ A ]⊩ (B × B′)) ∷ [] ▹⊢ᶜ
      π₁ (𝔞 to 𝔟⟨ x₀ ⟩)
    ≋
      𝔞 to π₁ (𝔟⟨ x₀ ⟩)
  to-π₂ :
    [] ⨾ ([]⊩ (F A)) ∷ ([ A ]⊩ (B × B′)) ∷ [] ▹⊢ᶜ
      π₂ (𝔞 to 𝔟⟨ x₀ ⟩)
    ≋
      𝔞 to π₂ (𝔟⟨ x₀ ⟩)
  to-‵ :
    [ []⊩ A ] ⨾ ([]⊩ (F A′)) ∷ ([ A′ ]⊩ (A ⟶ B)) ∷ [] ▹⊢ᶜ
      𝔞 ‵ (𝔞 to 𝔟⟨ x₀ ⟩)
    ≋
      𝔞 to 𝔞 ‵ 𝔟⟨ x₀ ⟩