-- Andreas Abel, 2019-10-30,
-- Parallel hereditary substitutions.
-- A riddle posed to me by Conor McBride during TYPES 2018.

-- This solution uses Agda's sized types to type substitutions
-- whose non-variable entries are bounded in the order of their type.
-- This bound is the main component of the termination measure
-- of parallel herediary substitutions.

-- Agda standard library imports

open import Size
open import Data.Product using (; _,_)

-- Lists (for typing contexts)
open import Data.List using (List; []; _∷_)

-- List membership _∈_ (for variables)
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Relation.Unary.Any using (here; there)
open import Relation.Binary.PropositionalEquality using (refl)

pattern here! = here refl

-- Sublists _⊆_ (for weakening)
import Data.List.Relation.Binary.Sublist.Propositional as Sublist
open Sublist using (_⊆_; _∷_; _∷ʳ_; ⊆-refl)

wk1 :  {a} {A : Set a} {x : A} {xs}  xs  x  xs
wk1 = _ ∷ʳ ⊆-refl

-- Types are indexed by an upper bound on their order.

data Ty : (i : Size)  Set where
  o   : ∀{i}  Ty i
  _⇒_ : ∀{i} (a : Ty i) (b : Ty ( i))  Ty ( i)

-- Agda's subtyping ensures the size index is just an upper bound.

test-Ty↑ : ∀{i}  Ty i  Ty ( i)
test-Ty↑ a = a

-- We do not expose the order of types in the type of the context.

TY =  Ty

-- Typing contexts

Cxt = List TY

-- Normal forms


  -- Introductions and neutrals

  data Nf (Γ : Cxt) :  i  Ty i  Set where

    ƛ   : ∀{i} {a : Ty i} {b : Ty ( i)}
         (t : Nf ((i , a)  Γ) ( i) b)
         Nf Γ ( i) (a  b)

    app : ∀{i} {a : Ty i} {j} {b : Ty j}
         (x : (i , a)  Γ)
         (s : Spine Γ i a j b)
         Nf Γ j b

  -- Eliminations

  data Spine (Γ : Cxt) :  i (a : Ty i) k (c : Ty k)  Set where
    []  : ∀{i} {c : Ty i}  Spine Γ i c i c
    _∷_ : ∀{i} {a : Ty i} {b : Ty ( i)} {k} {c : Ty k}
         (t : Nf Γ i a)
         (s : Spine Γ ( i) b k c)
         Spine Γ ( i) (a  b) k c

-- Spine concatenation

_++_ : ∀{Γ i a j b k c}  Spine Γ i a j b  Spine Γ j b k c  Spine Γ i a k c
[]      ++ s' = s'
(t  s) ++ s' = t  (s ++ s')

-- Substitution entries

data Entry (i : Size) (Γ : Cxt) :  j  Ty j  Set where
  var : ∀{j} {a : Ty j} (x : (j , a)  Γ)  Entry i Γ j a
  nf  :     {a : Ty i} (t : Nf Γ i a)     Entry i Γ i a

-- Weakening of syntax


  weakNf : ∀{Γ Δ} (τ : Γ  Δ) {i} {a : Ty i}
          Nf Γ i a
          Nf Δ i a
  weakNf τ (ƛ t) = ƛ (weakNf (refl  τ) t)
  weakNf τ (app x s) = app (Sublist.lookup τ x) (weakSp τ s)

  weakSp : ∀{Γ Δ} (τ : Γ  Δ) {i} {a : Ty i} {k} {c : Ty k}
          Spine Γ i a k c
          Spine Δ i a k c
  weakSp τ []      = []
  weakSp τ (t  s) = weakNf τ t  weakSp τ s

weakEntry : ∀{Γ Δ} (τ : Γ  Δ) {i j a }
         Entry i Γ j a
         Entry i Δ j a
weakEntry τ (var x) = var (Sublist.lookup τ x)
weakEntry τ (nf t)  = nf  (weakNf τ t)

-- Substitutions bounded by an order

data Subst i :  (Γ Δ : Cxt)  Set where
  []   : ∀{Γ}  Subst i Γ []
  id   : ∀{Γ : Cxt}  Subst i Γ Γ

  lift : ∀{Γ Δ}
        {a : TY}
        (σ : Subst i Γ Δ)
        Subst i (a  Γ) (a  Δ)

  _∷_  : ∀{Γ Δ} {a : Ty i}
        (u : Nf Γ i a)
        (σ : Subst i Γ Δ)
        Subst i Γ ((i , a)  Δ)

-- Substitutions (Subst i Γ Δ) are morally lists of entries
-- (All (uncurry (Entry i Γ)) Δ).

lookup : ∀{i Γ Δ} (σ : Subst i Γ Δ) {j} {a : Ty j} (x : (j , a)  Δ)  Entry i Γ j a
lookup id       x         = var x
lookup (lift σ) here!     = var here!
lookup (lift σ) (there x) = weakEntry wk1 (lookup σ x)
lookup (u  σ)  here!     = nf u
lookup (u  σ)  (there x) = lookup σ x

-- Parallel hereditary substitutions and accumulating application of Nfs


  -- Substitution into a normal form

  subst : ∀{i Γ j a Δ} (t : Nf Γ j a) (σ : Subst i Δ Γ)  Nf Δ j a
  subst (ƛ t)     σ = ƛ (subst t (lift σ))
  subst (app x s) σ = applyEntry (lookup σ x) (substSp s σ)

  -- Substitution into a spine (pointwise)

  substSp : ∀{i Γ Δ j a k c} (s : Spine Γ j a k c) (σ : Subst i Δ Γ)  Spine Δ j a k c
  substSp []      σ = []
  substSp (u  s) σ = subst u σ  substSp s σ

  -- Applying a substitution entry to a spine

  applyEntry :  {i Γ j a k c} (r : Entry i Γ j a) (s : Spine Γ j a k c)  Nf Γ k c
  applyEntry (var x) s = app x s
  applyEntry (nf t)  s = apply t s

  -- Application of a normal form to a spine

  apply :  {Γ i a j b} (t : Nf Γ i a) (s : Spine Γ i a j b)  Nf Γ j b
  apply (app x s) s'      = app x (s ++ s')
  apply (ƛ t)     []      = ƛ t
  apply (ƛ t)     (u  s) = applyClos t (u  id) s

  -- Accumulating application

  applyClos :  {i} {Γ} {Δ} {b} {k} {c}
             (t : Nf Δ ( i) b)
             (σ : Subst i Γ Δ)
             (s : Spine Γ ( i) b k c)
             Nf Γ k c
  applyClos (app x s) σ s'      = applyEntry (lookup σ x) (substSp s σ ++ s')
  applyClos (ƛ t)     σ []      = ƛ (subst t (lift σ))
  applyClos (ƛ t)     σ (u  s) = applyClos t (u  σ) s