{-# OPTIONS --without-K --safe #-}

-- This file defines the syntax of Mints
module Mints.Statics.Syntax where

open import Level renaming (suc to succ)

open import Lib
open import LibNonEmpty public

-- O computes the truncation offset of A when truncated by a length
record HasO {i} (A : Set i) : Set i where
  field
    O : A → ℕ → ℕ

open HasO {{...}} public

-- _∥_ computes the truncation of A by a length
record HasTr {i} (A : Set i) : Set i where
  infixl  _∥_
  field
    _∥_ : A → ℕ → A

open HasTr {{...}} public

-- A is monotonic relative to B
record Monotone {i j} (A : Set i) (B : Set j) : Set (i ⊔ j) where
  infixl 4.5 _[_]
  field
    _[_] : A → B → A

open Monotone {{...}} public

infixl 4.2 _$_
infixl 4.5 _[|_]

mutual
  -- Type is also an expression.
  Typ = Exp

  -- Definition of terms in Mints
  data Exp : Set where
    -- type constructors
    N     : Typ
    Π     : Typ → Typ → Typ
    Se    : (i : ℕ) → Typ
    □     : Typ → Typ
    v     : (x : ℕ) → Exp
    -- natural numebrs
    ze    : Exp
    su    : Exp → Exp
    rec   : (T : Typ) (s r t : Exp) → Exp
    -- functions
    Λ     : Exp → Exp
    _$_   : Exp → Exp → Exp
    -- modal terms
    box   : Exp → Exp
    unbox : ℕ → Exp → Exp
    -- explicit substitutions
    sub   : Exp → Substs → Exp

  -- Definition of (unified) substitutions in Mints
  infixl  _∘_
  infixl  _；_
  data Substs : Set where
    -- identity
    I    : Substs
    -- one step weakening
    wk   : Substs
    -- composition
    _∘_  : Substs → Substs → Substs
    -- extension
    _,_  : Substs → Exp → Substs
    -- modal transformation (MoT)
    _；_ : Substs → ℕ → Substs

-- Individual contexts
Ctx : Set
Ctx = List Typ

-- Context stacks are an nonempty list of contexts.
Ctxs : Set
Ctxs = List⁺ Ctx

-- Cons the topmost context
infixr  _∺_
_∺_ : Typ → Ctxs → Ctxs
T ∺ (Ψ ∷ Ψs) = (T ∷ Ψ) ∷ Ψs


-- Concatenate the topmost context
infixr 4.5 _++⁻_

_++⁻_ : List Typ → Ctxs → Ctxs
_++⁻_ Ψ (Ψ′ ∷ Γ) = (Ψ ++ Ψ′) ∷ Γ

-- Exp is monotonic and transformed by substitutions
instance
  ExpMonotone : Monotone Exp Substs
  ExpMonotone = record { _[_] = sub }

-- quick helpers
----------------

-- Projection of substitutions
p : Substs → Substs
p σ = wk ∘ σ

-- Nondependent functions
infixr  _⟶_
_⟶_ : Typ → Typ → Typ
S ⟶ T = Π S (T [ wk ])

-- Substitute the first open variable of t with s
_[|_] : Exp → Exp → Exp
t [| s ] = t [ I , s ]

-- Weakening of substitutions by one variable
q : Substs → Substs
q σ = (σ ∘ wk) , v 

-- O (truncation offset) and truncation for syntactic substitutions
S-O : Substs → ℕ → ℕ
S-O σ               = 
S-O I (suc n)        = suc n
S-O wk (suc n)       = suc n
S-O (σ , t) (suc n)  = S-O σ (suc n)
S-O (σ ； m) (suc n) = m + S-O σ n
S-O (σ ∘ δ) (suc n)  = S-O δ (S-O σ (suc n))

instance
  SubstsHasO : HasO Substs
  SubstsHasO = record { O = S-O }

S-Tr : Substs → ℕ → Substs
S-Tr σ               = σ
S-Tr I (suc n)        = I
S-Tr wk (suc n)       = I
S-Tr (σ , t) (suc n)  = S-Tr σ (suc n)
S-Tr (σ ； m) (suc n) = S-Tr σ n
S-Tr (σ ∘ δ) (suc n)  = S-Tr σ (suc n) ∘ S-Tr δ (O σ (suc n))

instance
  SubstsHasTr : HasTr Substs
  SubstsHasTr = record { _∥_ = S-Tr }

-- Neutral and normal forms
--
-- Here we define β-η normal form
mutual
  data Ne : Set where
    v     : (x : ℕ) → Ne
    rec   : (T : Nf) (z s : Nf) → Ne → Ne
    _$_   : Ne → (n : Nf) → Ne
    unbox : ℕ → Ne → Ne

  data Nf : Set where
    ne  : (u : Ne) → Nf
    N   : Nf
    Π   : Nf → Nf → Nf
    Se  : (i : ℕ) → Nf
    □   : Nf → Nf
    ze  : Nf
    su  : Nf → Nf
    Λ   : Nf → Nf
    box : Nf → Nf

variable
  S S′ S″ : Typ
  T T′ T″ : Typ
  Ψ Ψ′ Ψ″ : Ctx
  Ψs Ψs′  : List Ctx
  Γ Γ′ Γ″ : Ctxs
  Δ Δ′ Δ″ : Ctxs
  t t′ t″ : Exp
  r r′ r″ : Exp
  s s′ s″ : Exp
  σ σ′ σ″ : Substs
  τ τ′ τ″ : Substs
  u u′ u″ : Ne
  V V′ V″ : Ne
  w w′ w″ : Nf
  W W′ W″ : Nf

-- Conversion from neutrals/normals to terms
mutual
  Ne⇒Exp : Ne → Exp
  Ne⇒Exp (v x)         = v x
  Ne⇒Exp (rec T z s u) = rec (Nf⇒Exp T) (Nf⇒Exp z) (Nf⇒Exp s) (Ne⇒Exp u)
  Ne⇒Exp (u $ n)       = Ne⇒Exp u $ Nf⇒Exp n
  Ne⇒Exp (unbox n u)   = unbox n (Ne⇒Exp u)

  Nf⇒Exp : Nf → Exp
  Nf⇒Exp (ne u)  = Ne⇒Exp u
  Nf⇒Exp ze      = ze
  Nf⇒Exp (su w)  = su (Nf⇒Exp w)
  Nf⇒Exp (Λ w)   = Λ (Nf⇒Exp w)
  Nf⇒Exp N       = N
  Nf⇒Exp (Π S T) = Π (Nf⇒Exp S) (Nf⇒Exp T)
  Nf⇒Exp (Se i)  = Se i
  Nf⇒Exp (□ w)   = □ (Nf⇒Exp w)
  Nf⇒Exp (box w) = box (Nf⇒Exp w)

-- Dependent context lookup
infix  _∶_∈!_
data _∶_∈!_ : ℕ → Typ → Ctxs → Set where
  here  :  ∶ T [ wk ] ∈! T ∺ Γ
  there : ∀ {n T S} → n ∶ T ∈! Γ → suc n ∶ T [ wk ] ∈! S ∺ Γ