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

module extract where

-- Extraction to types and contexts from the Mixed-Context Type Theory MCTT.

open import Level

open import Data.Product
open import Data.Unit

open import mctt
open import context

------------------------------
-- Extraction to Types
------------------------------

ecxt : Cxt → Set₁

ekind : {cxt : Cxt} → (Kind cxt) → (ecxt cxt) → Set₁

etm : {cxt : Cxt} → {k : Kind cxt} → Tm cxt k → (x : ecxt cxt) → (ekind k x)

ety : {cxt : Cxt} → (Ty cxt) → (ecxt cxt) → Set

esub : {cxt1 cxt2 : Cxt} → Sub cxt1 cxt2 → ecxt cxt1 → ecxt cxt2

e≣→ : {cxt : Cxt} → {k1 k2 : Kind cxt} → (k1 ≣ k2) → (x : ecxt cxt) → (ekind k1 x → ekind k2 x)
e≣← : {cxt : Cxt} → {k1 k2 : Kind cxt} → (k1 ≣ k2) → (x : ecxt cxt) → (ekind k2 x → ekind k1 x)

e≡→ : {cxt : Cxt} → {t1 t2 : Ty cxt} → (t1 ≡ t2) → (x : ecxt cxt) → (ety t1 x → ety t2 x)
e≡← : {cxt : Cxt} → {t1 t2 : Ty cxt} → (t1 ≡ t2) → (x : ecxt cxt) → (ety t2 x → ety t1 x)

ecxt ε = Lift ⊤
ecxt (cxt ,, k) =  Σ[ x ∈ ecxt cxt ] ekind k x
ecxt (cxt , t) = Σ[ x ∈ ecxt cxt ] ety t x

ekind {cxt} U = λ x → Set
ekind (Π {cxt} t k) = λ x → ((z : ety t x) → ekind k (x , z))
ekind (_[_] {cxt1} {cxt2} k f) = λ x → ekind k (esub f x)

ety (el u) = λ x → (etm u x)
ety (t [ f ]) =  λ x → ety t (esub f x)

esub {cxt} id x = x
esub (kpop h) (x₁ , x₂) =  x₁
esub (tpop {cxt} t) (x₁ , x₂)  =  x₁
esub (_<id_ {cxt1} {cxt2} f t) (x₁ , x₂) =  (esub f x₁ , x₂)
esub (_id≪≣_ cxt {k1} {k2} eq) (x₁ , x₂) =  (x₁ , e≣→ eq x₁ x₂)
esub (_id<≡_ cxt {k1} {k2} eq) (x₁ , x₂) =  (x₁ , e≡→ eq x₁ x₂)
esub (_≪_ {cxt1} {cxt2} {k} f e) x = (esub f x , etm e x)
esub (f₂ ∘ f₁) x =  esub f₂ (esub f₁ x)

etm ktop =  λ x → proj₂ x
etm (e [ f ]) =  λ x → etm e (esub f x)
etm (ap e) =  λ x → etm e (proj₁ x) (proj₂ x)
etm (coe eq e) = λ x → e≣→ eq x (etm e x)

e≣→ (refl≣ k) =  λ x →  λ z → z
e≣→ (e2 • e1) = λ x →  λ z → e≣→ e2 x (e≣→ e1 x z)
e≣→ (e ⁻¹) = e≣← e
e≣→ (k[id] k) = λ x →  λ z → z
e≣→ (k[∘] k f2 f1) = λ x →  λ z → z
e≣→ (Π≣ t eq) = λ x →  λ w z →  e≣→ eq (x , z) (w z)  
e≣→ (U[] f) =  λ x → λ z → z
e≣→ (Π[] t k f) =  λ x w z →  w z
e≣→ (ktpop≣ h k t) = λ x → λ z → z
e≣→ (eq [ f ]) = λ x → λ z → e≣→ eq (esub f x) z
e≣→ (kpop∘≪ f t) = λ x y → y

e≣← (refl≣ k) =  λ x →  λ z → z
e≣← (e2 • e1) = λ x →  λ z → e≣← e1 x (e≣← e2 x z)
e≣← (e ⁻¹) = e≣→ e
e≣← (k[id] k) = λ x →  λ z → z
e≣← (k[∘] k f2 f1) = λ x →  λ z → z
e≣← (Π≣ t eq) = λ x →  λ w z →  e≣← eq (x , z) (w z)
e≣← (U[] f) =  λ x → λ z → z
e≣← (Π[] t k f) =  λ x w z →  w z
e≣← (ktpop≣ h k t) = λ x → λ z → z
e≣← (eq [ f ]) = λ x → λ z → e≣← eq (esub f x) z
e≣← (kpop∘≪ f t) = λ x y → y

e≡→ (refl≡ t) =  λ x →  λ z → z
e≡→ (e2 • e1) =  λ x →  λ z → e≡→ e2 x (e≡→ e1 x z)
e≡→ (e ⁻¹) = e≡← e
e≡→ (t[id] t) = λ x → λ z → z
e≡→ (t[∘] t f2 f1) = λ x →  λ z → z
e≡→ (ktpop≡ s h t) = λ x → λ z → z
e≡→ (el[] k f) = λ x → λ z →  z 
e≡→ (eq [ f ]) = λ x → λ z → e≡→ eq (esub f x) z

e≡← (refl≡ t) =  λ x →  λ z → z
e≡← (e2 • e1) =  λ x →  λ z → e≡← e1 x (e≡← e2 x z)
e≡← (e ⁻¹) = e≡→ e
e≡← (t[id] t) = λ x → λ z → z
e≡← (t[∘] t f2 f1) = λ x →  λ z → z
e≡← (ktpop≡ s h t) = λ x → λ z → z
e≡← (el[] k f) = λ x → λ z →  z 
e≡← (eq [ f ]) = λ x → λ z → e≡← eq (esub f x) z

------------------------------
-- From Types to Contexts
------------------------------

ecxt' : Cxt → Context

-- This is actually an equivalence, but we don't need the other direction
ecxt'is : (cxt : Cxt) → sum (ecxt' cxt) → ecxt cxt

ekind' : {cxt : Cxt} → (Kind cxt) → ((ecxt' cxt) ⇨ Set₁)

ety' : {cxt : Cxt} → (Ty cxt) → ((ecxt' cxt) ⇨ Set₁)

ecxt' ε = ε
ecxt' (cxt ,, k) = extend (ecxt' cxt) (ekind' k)
ecxt' (cxt , t) = extend (ecxt' cxt) (ety' t)

ekind' {cxt} k = sumto⇨ (ecxt' cxt) Set₁ (λ s → ekind k (ecxt'is cxt s))

ety' {cxt} t = sumto⇨ (ecxt' cxt) Set₁ (λ s → Lift (ety t (ecxt'is cxt s)))

ecxt'is ε s =   s
ecxt'is (cxt ,, x) s = (ecxt'is cxt (proj₁ (sumextend (ecxt' cxt) (λ s₁ → ekind x (ecxt'is cxt s₁)) s)) ,
                         (proj₂ (sumextend (ecxt' cxt) (λ s₁ → ekind x (ecxt'is cxt s₁)) s)))
ecxt'is (cxt , x) s  = (ecxt'is cxt (proj₁ (sumextend (ecxt' cxt) (λ s₁ → Lift (ety x (ecxt'is cxt s₁))) s)) ,
                         (lower (proj₂ (sumextend (ecxt' cxt) (λ s₁ → Lift (ety x (ecxt'is cxt s₁))) s))))

-- The nicest output

extract : Cxt → Set₁
extract cxt = sum (ecxt' cxt)