{-# OPTIONS --copatterns --sized-types #-}

-- {-# OPTIONS -v tc.size:60 #-}
-- {-# OPTIONS -v term:20 -vterm.matrices:40 #-}


module SizedTypesMutual where

open import Common.Size

-- Syntax: Types, terms and contexts.

infixr 6 _⇒_
infixl 1 _,_

-- Types and contexts.

data Ty : Set where
  _⇒_ : (a b : Ty) → Ty

data Cxt : Set where
  _,_ : (Γ : Cxt) (a : Ty) → Cxt

-- Generic reversed Spines (last application available first).

data RSpine (V : Ty → Set) (a : Ty) : (c : Ty) → Set where
  _,_ : ∀ {b c} → RSpine V a (b ⇒ c) → V b → RSpine V a c

-- Functoriality for RSpine

mapRSp : ∀ {V W : Ty → Set} → (∀ {d} → V d → W d) → ∀ {a c} → RSpine V a c → RSpine W a c
mapRSp f (rs , r) = mapRSp f rs , f r

-- Values and environments

mutual
  data Env {i : Size} (Δ : Cxt) : Set where
    _,_ : ∀ {a} (ρ : Env {i = i} Δ) (v : Val {i = i} Δ a) → Env Δ

  data Val {i : Size} (Δ : Cxt) : (a : Ty) → Set where
    ne  : ∀ {j : Size< i}{a c} (vs : ValSpine {i = j} Δ a c) → Val Δ c
    lam : ∀ {a b}              (ρ : Env {i = i} Δ)           → Val Δ (a ⇒ b)

  ValSpine : {i : Size} (Δ : Cxt) (a c : Ty) → Set
  ValSpine {i = i} Δ = RSpine (Val {i = i} Δ)

-- Weakening

mutual
  weakEnv : ∀ {i Δ a} → Env {i = i} Δ → Env {i = i} (Δ , a)
  weakEnv {i = i} (ρ , v)  = weakEnv ρ , weakVal v

  weakVal : ∀ {i Δ a c} → Val {i = i} Δ c → Val {i = i} (Δ , a) c
  weakVal (ne {j = j} vs)  = ne (mapRSp (weakVal {i = j}) vs)
  weakVal (lam ρ)          = lam (weakEnv ρ)

-- This mutual block produces garbage size solutions
-- if solving is not done on a per-definition basis.

-- The reason is that the current solver assumes
-- that all size constraints live in (an extension of)
-- the same context (which is not true here).
