module Prelude where

open import Agda.Primitive public
  using (_⊔_ ; lsuc)


-- Truth.

open import Agda.Builtin.Unit public
  using (⊤)
  renaming (tt to ∅)


-- Strong existence.

record Σ {ℓ ℓ′} (X : Set ℓ) (Y : X → Set ℓ′) : Set (ℓ ⊔ ℓ′) where
  instance constructor _,_
  field
    π₁ : X
    π₂ : Y π₁
open Σ public

∃ : ∀ {ℓ ℓ′} {X : Set ℓ} → (X → Set ℓ′) → Set (ℓ ⊔ ℓ′)
∃ = Σ _

mapΣ : ∀ {ℓ ℓ′} {X : Set ℓ} {Y : X → Set ℓ′}
         {ℓₘ ℓₘ′} {Xₘ : Set ℓₘ} {Yₘ : Xₘ → Set ℓₘ′}
         (f : X → Xₘ) (g : ∀ {x} → Y x → Yₘ (f x)) →
         Σ X Y → Σ Xₘ Yₘ
mapΣ f g (x , y) = f x , g y

mapΣ₂ : ∀ {ℓ ℓ′} {X : Set ℓ} {Y : X → Set ℓ′}
          {ℓ₂ ℓ₂′} {X₂ : Set ℓ₂} {Y₂ : X₂ → Set ℓ₂′}
          {ℓₘ ℓₘ′} {Xₘ : Set ℓₘ} {Yₘ : Xₘ → Set ℓₘ′}
          (f : X → X₂ → Xₘ) (g : ∀ {x x₂} → Y x → Y₂ x₂ → Yₘ (f x x₂)) →
          Σ X Y → Σ X₂ Y₂ → Σ Xₘ Yₘ
mapΣ₂ f g (x , y) (x₂ , y₂) = f x x₂ , g y y₂


-- Conjunction.

infixr 2 _∧_
_∧_ : ∀ {ℓ ℓ′} → Set ℓ → Set ℓ′ → Set (ℓ ⊔ ℓ′)
X ∧ Y = Σ X (λ x → Y)


-- Built-in implication.

id : ∀ {ℓ} {X : Set ℓ} → X → X
id x = x

const : ∀ {ℓ ℓ′} {X : Set ℓ} {Y : Set ℓ′} → X → Y → X
const x y = x

flip : ∀ {ℓ ℓ′ ℓ″} {X : Set ℓ} {Y : Set ℓ′} {Z : Set ℓ″} →
       (X → Y → Z) → Y → X → Z
flip P y x = P x y

ap : ∀ {ℓ ℓ′ ℓ″} {X : Set ℓ} {Y : Set ℓ′} {Z : Set ℓ″} →
     (X → Y → Z) → (X → Y) → X → Z
ap f g x = f x (g x)

infixr 9 _∘_
_∘_ : ∀ {ℓ ℓ′ ℓ″} {X : Set ℓ} {Y : Set ℓ′} {Z : Set ℓ″} →
      (Y → Z) → (X → Y) → X → Z
f ∘ g = λ x → f (g x)

refl→ : ∀ {ℓ} {X : Set ℓ} → X → X
refl→ = id

trans→ : ∀ {ℓ ℓ′ ℓ″} {X : Set ℓ} {Y : Set ℓ′} {Z : Set ℓ″} →
          (X → Y) → (Y → Z) → X → Z
trans→ = flip _∘_


-- Disjunction.

infixr 1 _∨_
data _∨_ {ℓ ℓ′} (X : Set ℓ) (Y : Set ℓ′) : Set (ℓ ⊔ ℓ′) where
  ι₁ : X → X ∨ Y
  ι₂ : Y → X ∨ Y

elim∨ : ∀ {ℓ ℓ′ ℓ″} {X : Set ℓ} {Y : Set ℓ′} {Z : Set ℓ″} →
        X ∨ Y → (X → Z) → (Y → Z) → Z
elim∨ (ι₁ x) f g = f x
elim∨ (ι₂ y) f g = g y


-- Falsehood.

data ⊥ : Set where

elim⊥ : ∀ {ℓ} {X : Set ℓ} → ⊥ → X
elim⊥ ()


-- Negation.

infix 3 ¬_
¬_ : ∀ {ℓ} → Set ℓ → Set ℓ
¬ X = X → ⊥

_↯_ : ∀ {ℓ ℓ′} {X : Set ℓ} {Y : Set ℓ′} → X → ¬ X → Y
p ↯ ¬p = elim⊥ (¬p p)


-- Built-in equality.

open import Agda.Builtin.Equality public
  using (_≡_ ; refl)

infix 4 _≢_
_≢_ : ∀ {ℓ} {X : Set ℓ} → X → X → Set ℓ
x ≢ x′ = ¬ (x ≡ x′)

trans : ∀ {ℓ} {X : Set ℓ} {x x′ x″ : X} → x ≡ x′ → x′ ≡ x″ → x ≡ x″
trans refl refl = refl

sym : ∀ {ℓ} {X : Set ℓ} {x x′ : X} → x ≡ x′ → x′ ≡ x
sym refl = refl

subst : ∀ {ℓ ℓ′} {X : Set ℓ} → (P : X → Set ℓ′) →
        ∀ {x x′} → x ≡ x′ → P x → P x′
subst P refl p = p

cong : ∀ {ℓ ℓ′} {X : Set ℓ} {Y : Set ℓ′} → (f : X → Y) →
       ∀ {x x′} → x ≡ x′ → f x ≡ f x′
cong f refl = refl

cong₂ : ∀ {ℓ ℓ′ ℓ″} {X : Set ℓ} {Y : Set ℓ′} {Z : Set ℓ″} → (f : X → Y → Z) →
        ∀ {x x′ y y′} → x ≡ x′ → y ≡ y′ → f x y ≡ f x′ y′
cong₂ f refl refl = refl

cong₃ : ∀ {ℓ ℓ′ ℓ″ ℓ‴} {X : Set ℓ} {Y : Set ℓ′} {Z : Set ℓ″} {A : Set ℓ‴} →
        (f : X → Y → Z → A) →
        ∀ {x x′ y y′ z z′} → x ≡ x′ → y ≡ y′ → z ≡ z′ → f x y z ≡ f x′ y′ z′
cong₃ f refl refl refl = refl


-- Equational reasoning with built-in equality.

module ≡-Reasoning {ℓ} {X : Set ℓ} where
  infix 1 begin_
  begin_ : ∀ {x x′ : X} → x ≡ x′ → x ≡ x′
  begin p = p

  infixr 2 _≡⟨⟩_
  _≡⟨⟩_ : ∀ (x {x′} : X) → x ≡ x′ → x ≡ x′
  x ≡⟨⟩ p = p

  infixr 2 _≡⟨_⟩_
  _≡⟨_⟩_ : ∀ (x {x′ x″} : X) → x ≡ x′ → x′ ≡ x″ → x ≡ x″
  x ≡⟨ p ⟩ q = trans p q

  infix 3 _∎
  _∎ : ∀ (x : X) → x ≡ x
  x ∎ = refl

open ≡-Reasoning public


-- Booleans.

open import Agda.Builtin.Bool public
  using (Bool ; false ; true)

elimBool : ∀ {ℓ} {X : Set ℓ} → Bool → X → X → X
elimBool false z s = z
elimBool true  z s = s


-- Conditionals.

data Maybe {ℓ} (X : Set ℓ) : Set ℓ where
  nothing : Maybe X
  just    : X → Maybe X

{-# HASKELL type AgdaMaybe _ x = Maybe x #-}
{-# COMPILED_DATA Maybe MAlonzo.Code.Data.Maybe.Base.AgdaMaybe Just Nothing #-}

elimMaybe : ∀ {ℓ ℓ′} {X : Set ℓ} {Y : Set ℓ′} → Maybe X → Y → (X → Y) → Y
elimMaybe nothing  z f = z
elimMaybe (just x) z f = f x


-- Naturals.

open import Agda.Builtin.Nat public
  using (Nat ; zero ; suc)

elimNat : ∀ {ℓ} {X : Set ℓ} → Nat → X → (Nat → X → X) → X
elimNat zero    z f = z
elimNat (suc n) z f = f n (elimNat n z f)


-- Finite sets.

data Fin : Nat → Set where
  zero : ∀ {n} → Fin (suc n)
  suc  : ∀ {n} → Fin n → Fin (suc n)


-- Overloaded literals.

record Number {ℓ} (X : Set ℓ) : Set (lsuc ℓ) where
  field
    Constraint : Nat → Set ℓ
    fromNat    : (n : Nat) {{_ : Constraint n}} → X
open Number {{...}} public
  using (fromNat)
{-# BUILTIN FROMNAT fromNat #-}

data IsTrue : Bool → Set where
  isTrue : IsTrue true

instance
  trueIsTrue : IsTrue true
  trueIsTrue = isTrue

infix 5 _<?_
_<?_ : Nat → Nat → Bool
zero  <? zero  = false
zero  <? suc m = true
suc n <? zero  = false
suc n <? suc m = n <? m

infixl 3 _&&_
_&&_ : Bool → Bool → Bool
true && true = true
_    && _    = false

natToFin : ∀ {n} (m : Nat) {{_ : IsTrue (m <? n)}} → Fin n
natToFin {zero}  zero    {{()}}
natToFin {zero}  (suc m) {{()}}
natToFin {suc n} zero    {{isTrue}} = zero
natToFin {suc n} (suc m) {{p}}      = suc (natToFin m)

instance
  NatIsNumber : Number Nat
  Number.Constraint NatIsNumber n = ⊤
  Number.fromNat    NatIsNumber n = n

instance
  FinIsNumber : ∀ {n} → Number (Fin n)
  Number.Constraint (FinIsNumber {n}) m = IsTrue (m <? n)
  Number.fromNat    FinIsNumber       m = natToFin m


-- Stacks.

data Stack (X : Set) : Set where
  ∅   : Stack X
  _,_ : Stack X → X → Stack X

module StackThings {X : Set} where
  size : Stack X → Nat
  size ∅       = zero
  size (Γ , A) = suc (size Γ)

  get : (Γ : Stack X) (n : Nat) {{_ : IsTrue (n <? size Γ)}} → X
  get ∅       zero    {{()}}
  get ∅       (suc n) {{()}}
  get (Γ , A) zero    {{isTrue}} = A
  get (Γ , B) (suc n) {{p}}      = get Γ n

  infix 3 _∈_
  data _∈_ (A : X) : Stack X → Set where
    zero : ∀ {Γ}   → A ∈ Γ , A
    suc  : ∀ {B Γ} → A ∈ Γ → A ∈ Γ , B

  natTo∈ : ∀ {Γ : Stack X} (n : Nat) {{_ : IsTrue (n <? size Γ)}} → get Γ n ∈ Γ
  natTo∈ {∅}     zero    {{()}}
  natTo∈ {∅}     (suc n) {{()}}
  natTo∈ {Γ , A} zero    {{isTrue}} = zero
  natTo∈ {Γ , B} (suc n) {{p}}      = suc (natTo∈ n)

  instance
    ∈IsNumber : ∀ {A : X} {Γ} → Number (A ∈ Γ)
    Number.Constraint (∈IsNumber {A} {Γ}) n    = Σ (IsTrue (n <? size Γ)) (λ p → A ≡ get Γ n {{p}})
    Number.fromNat    ∈IsNumber n {{p , refl}} = natTo∈ n {{p}}

  infix 3 _∈⟨_⟩_
  data _∈⟨_⟩_ (A : X) : Nat → Stack X → Set where
    zero : ∀ {Γ}     → A ∈⟨ zero ⟩ Γ , A
    suc  : ∀ {B n Γ} → A ∈⟨ n ⟩ Γ → A ∈⟨ suc n ⟩ Γ , B

  natTo∈′ : ∀ {Γ : Stack X} (n : Nat) {{_ : IsTrue (n <? size Γ)}} → get Γ n ∈⟨ n ⟩ Γ
  natTo∈′ {∅}     zero    {{()}}
  natTo∈′ {∅}     (suc n) {{()}}
  natTo∈′ {Γ , A} zero    {{isTrue}} = zero
  natTo∈′ {Γ , B} (suc n) {{p}}      = suc (natTo∈′ n)

  instance
    ∈′IsNumber : ∀ {A : X} {n Γ} → Number (A ∈⟨ n ⟩ Γ)
    Number.Constraint (∈′IsNumber {A} {n} {Γ}) m         = Σ (IsTrue (n <? size Γ)) (λ p → A ≡ get Γ n {{p}} ∧ m ≡ n)
    Number.fromNat    ∈′IsNumber m {{p , (refl , refl)}} = natTo∈′ m {{p}}

  infix 3 _⊆_
  data _⊆_ : Stack X → Stack X → Set where
    done : ∅ ⊆ ∅
    skip : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → Γ ⊆ Γ′ , A
    keep : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → Γ , A ⊆ Γ′ , A

  refl⊆ : ∀ {Γ} → Γ ⊆ Γ
  refl⊆ {∅}     = done
  refl⊆ {Γ , A} = keep refl⊆

  trans⊆ : ∀ {Γ Γ′ Γ″} → Γ ⊆ Γ′ → Γ′ ⊆ Γ″ → Γ ⊆ Γ″
  trans⊆ done     η′        = η′
  trans⊆ η        (skip η′) = skip (trans⊆ η η′)
  trans⊆ (skip η) (keep η′) = skip (trans⊆ η η′)
  trans⊆ (keep η) (keep η′) = keep (trans⊆ η η′)

  inf⊆ : ∀ {Γ} → ∅ ⊆ Γ
  inf⊆ {∅}     = done
  inf⊆ {Γ , A} = skip inf⊆

  weak⊆ : ∀ {A Γ} → Γ ⊆ Γ , A
  weak⊆ = skip refl⊆

  move∈ : ∀ {A : X} {Γ Γ′} → Γ ⊆ Γ′ → A ∈ Γ → A ∈ Γ′
  move∈ done     ()
  move∈ (skip η) i       = suc (move∈ η i)
  move∈ (keep η) zero    = zero
  move∈ (keep η) (suc i) = suc (move∈ η i)

  move∈′ : ∀ {A : X} {n Γ Γ′} → Γ ⊆ Γ′ → A ∈⟨ n ⟩ Γ → Σ Nat (λ n′ → A ∈⟨ n′ ⟩ Γ′)
  move∈′ done     ()
  move∈′ (skip η) i       = mapΣ suc suc (move∈′ η i)
  move∈′ (keep η) zero    = zero , zero
  move∈′ (keep η) (suc i) = mapΣ suc suc (move∈′ η i)

record StackPair (X Y : Set) : Set where
  constructor _⁏_
  field
    π₁ : Stack X
    π₂ : Stack Y
open StackPair public

module StackPairThings {X Y : Set} where
  open StackThings

  infix 3 _⊆²_
  _⊆²_ : StackPair X Y → StackPair X Y → Set
  Γ ⁏ Δ ⊆² Γ′ ⁏ Δ′ = Γ ⊆ Γ′ ∧ Δ ⊆ Δ′

  refl⊆² : ∀ {Γ Δ} → Γ ⁏ Δ ⊆² Γ ⁏ Δ
  refl⊆² = refl⊆ , refl⊆

  trans⊆² : ∀ {Γ Γ′ Γ″ Δ Δ′ Δ″} → Γ ⁏ Δ ⊆² Γ′ ⁏ Δ′ → Γ′ ⁏ Δ′ ⊆² Γ″ ⁏ Δ″ → Γ ⁏ Δ ⊆² Γ″ ⁏ Δ″
  trans⊆² (η , μ) (η′ , μ′) = trans⊆ η η′ , trans⊆ μ μ′


-- Sized stacks.

data SStack (X : Set) : Nat → Set where
  ∅   : SStack X zero
  _,_ : ∀ {n} → SStack X n → X → SStack X (suc n)

module SStackThings {X : Set} where
  get : ∀ {n} → (Γ : SStack X n) (m : Nat) {{_ : IsTrue (m <? n)}} → X
  get ∅       zero    {{()}}
  get ∅       (suc n) {{()}}
  get (Γ , A) zero    {{isTrue}} = A
  get (Γ , B) (suc n) {{p}}      = get Γ n

  get′ : ∀ {n} → (Γ : SStack X n) (k : Fin n) → X
  get′ ∅       ()
  get′ (Γ , A) zero    = A
  get′ (Γ , B) (suc k) = get′ Γ k

  infix 3 _∈_
  data _∈_ (A : X) : ∀ {n} → SStack X n → Set where
    zero : ∀ {n}   {Γ : SStack X n} → A ∈ Γ , A
    suc  : ∀ {B n} {Γ : SStack X n} → A ∈ Γ → A ∈ Γ , B

  natTo∈ : ∀ {n} {Γ : SStack X n} (m : Nat) {{_ : IsTrue (m <? n)}} → get Γ m ∈ Γ
  natTo∈ {Γ = ∅}     zero    {{()}}
  natTo∈ {Γ = ∅}     (suc m) {{()}}
  natTo∈ {Γ = Γ , A} zero    {{isTrue}} = zero
  natTo∈ {Γ = Γ , B} (suc m) {{p}}      = suc (natTo∈ m)

  instance
    ∈IsNumber : ∀ {n} {Γ : SStack X n} {A} → Number (A ∈ Γ)
    Number.Constraint (∈IsNumber {n} {Γ} {A}) m = Σ (IsTrue (m <? n)) (λ p → A ≡ get Γ m {{p}})
    Number.fromNat    ∈IsNumber n {{p , refl}}  = natTo∈ n {{p}}

  infix 3 _∈⟨_⟩_
  data _∈⟨_⟩_ (A : X) : ∀ {n} → Fin n → SStack X n → Set where
    zero : ∀ {n}     {Γ : SStack X n} → A ∈⟨ zero ⟩ Γ , A
    suc  : ∀ {B n k} {Γ : SStack X n} → A ∈⟨ k ⟩ Γ → A ∈⟨ suc k ⟩ Γ , B

  natTo∈′ : ∀ {n} {Γ : SStack X n} (k : Fin n) → get′ Γ k ∈⟨ k ⟩ Γ
  natTo∈′ {Γ = ∅}     ()
  natTo∈′ {Γ = Γ , A} zero    = zero
  natTo∈′ {Γ = Γ , B} (suc m) = suc (natTo∈′ m)

  instance
    ∈′IsNumber : ∀ {n} {Γ : SStack X n} {A k} → Number (A ∈⟨ k ⟩ Γ)
    Number.Constraint (∈′IsNumber {n} {Γ} {A} {k}) m     = Σ (IsTrue (m <? n)) (λ p → A ≡ get′ Γ k ∧ natToFin m {{p}} ≡ k)
    Number.fromNat    ∈′IsNumber m {{p , (refl , refl)}} = natTo∈′ (natToFin m {{p}})

  infix 3 _⊆_
  data _⊆_ : ∀ {n n′} → SStack X n → SStack X n′ → Set where
    done : ∅ ⊆ ∅
    skip : ∀ {A n n′} {Γ : SStack X n} {Γ′ : SStack X n′} → Γ ⊆ Γ′ → Γ ⊆ Γ′ , A
    keep : ∀ {A n n′} {Γ : SStack X n} {Γ′ : SStack X n′} → Γ ⊆ Γ′ → Γ , A ⊆ Γ′ , A

  refl⊆ : ∀ {n} {Γ : SStack X n} → Γ ⊆ Γ
  refl⊆ {Γ = ∅}     = done
  refl⊆ {Γ = Γ , A} = keep refl⊆

  trans⊆ : ∀ {n n′ n″} {Γ : SStack X n} {Γ′ : SStack X n′} {Γ″ : SStack X n″} →
           Γ ⊆ Γ′ → Γ′ ⊆ Γ″ → Γ ⊆ Γ″
  trans⊆ done     η′        = η′
  trans⊆ η        (skip η′) = skip (trans⊆ η η′)
  trans⊆ (skip η) (keep η′) = skip (trans⊆ η η′)
  trans⊆ (keep η) (keep η′) = keep (trans⊆ η η′)

  inf⊆ : ∀ {n} {Γ : SStack X n} → ∅ ⊆ Γ
  inf⊆ {Γ = ∅}     = done
  inf⊆ {Γ = Γ , A} = skip inf⊆

  weak⊆ : ∀ {n} {Γ : SStack X n} {A} → Γ ⊆ Γ , A
  weak⊆ = skip refl⊆

  move∈ : ∀ {n n′} {Γ : SStack X n} {Γ′ : SStack X n′} {A} →
          Γ ⊆ Γ′ → A ∈ Γ → A ∈ Γ′
  move∈ done     ()
  move∈ (skip η) i       = suc (move∈ η i)
  move∈ (keep η) zero    = zero
  move∈ (keep η) (suc i) = suc (move∈ η i)

  move∈′ : ∀ {n n′} {Γ : SStack X n} {Γ′ : SStack X n′} {A k} →
           Γ ⊆ Γ′ → A ∈⟨ k ⟩ Γ → Σ (Fin n′) (λ k′ → A ∈⟨ k′ ⟩ Γ′)
  move∈′ done     ()
  move∈′ (skip η) i       = mapΣ suc suc (move∈′ η i)
  move∈′ (keep η) zero    = zero , zero
  move∈′ (keep η) (suc i) = mapΣ suc suc (move∈′ η i)

infixl 4 _⁏_
record SStackPair (X Y : Set) (n m : Nat) : Set where
  constructor _⁏_
  field
    π₁ : SStack X n
    π₂ : SStack Y m
open SStackPair public

module SStackPairThings {X Y : Set} where
  open SStackThings

  infix 3 _⊆²_
  _⊆²_ : ∀ {n n′ m m′} → SStackPair X Y n m → SStackPair X Y n′ m′ → Set
  Γ ⁏ Δ ⊆² Γ′ ⁏ Δ′ = Γ ⊆ Γ′ ∧ Δ ⊆ Δ′

  refl⊆² : ∀ {n m} {Γ : SStack X n} {Δ : SStack Y m} →
           Γ ⁏ Δ ⊆² Γ ⁏ Δ
  refl⊆² = refl⊆ , refl⊆

  trans⊆² : ∀ {n n′ n″} {Γ : SStack X n} {Γ′ : SStack X n′} {Γ″ : SStack X n″}
              {m m′ m″} {Δ : SStack Y m} {Δ′ : SStack Y m′} {Δ″ : SStack Y m″} →
            Γ ⁏ Δ ⊆² Γ′ ⁏ Δ′ → Γ′ ⁏ Δ′ ⊆² Γ″ ⁏ Δ″ → Γ ⁏ Δ ⊆² Γ″ ⁏ Δ″
  trans⊆² (η , μ) (η′ , μ′) = trans⊆ η η′ , trans⊆ μ μ′


-- Predicates.

Pred : ∀ {ℓ} → Set ℓ → Set (lsuc ℓ)
Pred {ℓ} X = X → Set ℓ

module _ {X : Set} where
  open StackThings

  data All (P : Pred X) : Pred (Stack X) where
    ∅   : All P ∅
    _,_ : ∀ {A Γ} → All P Γ → P A → All P (Γ , A)

  mapAll : ∀ {P Q Γ} → (∀ {A} → P A → Q A) → All P Γ → All Q Γ
  mapAll η ∅       = ∅
  mapAll η (γ , a) = mapAll η γ , η a

  lookupAll : ∀ {A : X} {Γ P} → A ∈ Γ → All P Γ → P A
  lookupAll zero    (γ , a) = a
  lookupAll (suc i) (γ , b) = lookupAll i γ

  lookupAll′ : ∀ {A : X} {n Γ P} → A ∈⟨ n ⟩ Γ → All P Γ → P A
  lookupAll′ zero    (γ , a) = a
  lookupAll′ (suc i) (γ , b) = lookupAll′ i γ

module _ {X : Set} where
  open SStackThings

  data SAll (P : Pred X) : ∀ {n} → Pred (SStack X n) where
    ∅   : SAll P ∅
    _,_ : ∀ {A n} {Γ : SStack X n} → SAll P Γ → P A → SAll P (Γ , A)

  mapSAll : ∀ {n} {Γ : SStack X n} {P Q} → (∀ {A} → P A → Q A) → SAll P Γ → SAll Q Γ
  mapSAll η ∅       = ∅
  mapSAll η (γ , a) = mapSAll η γ , η a

  lookupSAll : ∀ {n} {Γ : SStack X n} {P A} → A ∈ Γ → SAll P Γ → P A
  lookupSAll zero    (γ , a) = a
  lookupSAll (suc i) (γ , b) = lookupSAll i γ

  lookupSAll′ : ∀ {n} {Γ : SStack X n} {P A k} → A ∈⟨ k ⟩ Γ → SAll P Γ → P A
  lookupSAll′ zero    (γ , a) = a
  lookupSAll′ (suc i) (γ , b) = lookupSAll′ i γ