{-# OPTIONS --allow-unsolved-metas --sized-types #-}

module A201607.OldBasicILP.Syntax.Projection where

open import A201607.Common.UntypedContext public

import A201607.OldBasicILP.UntypedSyntax.ClosedHilbertSequential as CHS
import A201607.OldBasicILP.UntypedSyntax.ClosedHilbert as CH


-- Projection of types and derivations to a form parametrised by a closed, untyped representation of syntax.

module ClosedHilbertSequential where
  open import A201607.OldBasicILP.Syntax.ClosedHilbertSequential

  mutual
    ⌊_⌋ᵀ : Ty → CHS.Ty
    ⌊ α P ⌋ᵀ   = CHS.α P
    ⌊ A ▻ B ⌋ᵀ = ⌊ A ⌋ᵀ CHS.▻ ⌊ B ⌋ᵀ
    ⌊ p ⦂ A ⌋ᵀ = ⌊ p ⌋ᴾ CHS.⦂ ⌊ A ⌋ᵀ
    ⌊ A ∧ B ⌋ᵀ = ⌊ A ⌋ᵀ CHS.∧ ⌊ B ⌋ᵀ
    ⌊ ⊤ ⌋ᵀ    = CHS.⊤

    -- FIXME: WHat is going on here?
    postulate
      ⌊_⌋ᴾ : ∀ {Ξ A} → Proof Ξ A → CHS.Proof

    ⌊_⌋ᵀ⋆ : Cx Ty → Cx CHS.Ty
    ⌊ ∅ ⌋ᵀ⋆     = ∅
    ⌊ Γ , A ⌋ᵀ⋆ = ⌊ Γ ⌋ᵀ⋆ , ⌊ A ⌋ᵀ

    ⌊_⌋∈ : ∀ {Ξ A} → A ∈ Ξ → ⌊ A ⌋ᵀ ∈ ⌊ Ξ ⌋ᵀ⋆
    ⌊ top ⌋∈   = top
    ⌊ pop i ⌋∈ = pop ⌊ i ⌋∈

    ⌊_⌋ᴰ : ∀ {Ξ} → ⊢ᴰ Ξ → CHS.⊢ᴰ ⌊ Ξ ⌋ᵀ⋆
    ⌊ nil ⌋ᴰ      = CHS.nil
    ⌊ mp i j d ⌋ᴰ = CHS.mp ⌊ i ⌋∈ ⌊ j ⌋∈ ⌊ d ⌋ᴰ
    ⌊ ci d ⌋ᴰ     = CHS.ci ⌊ d ⌋ᴰ
    ⌊ ck d ⌋ᴰ     = CHS.ck ⌊ d ⌋ᴰ
    ⌊ cs d ⌋ᴰ     = CHS.cs ⌊ d ⌋ᴰ
    ⌊ nec `d d ⌋ᴰ = {!CHS.nec ⌊ `d ⌋ᴰ ⌊ d ⌋ᴰ!}
    ⌊ cdist d ⌋ᴰ  = {!CHS.cdist ⌊ d ⌋ᴰ!}
    ⌊ cup d ⌋ᴰ    = {!CHS.cup ⌊ d ⌋ᴰ!}
    ⌊ cdown d ⌋ᴰ  = CHS.cdown ⌊ d ⌋ᴰ
    ⌊ cpair d ⌋ᴰ  = CHS.cpair ⌊ d ⌋ᴰ
    ⌊ cfst d ⌋ᴰ   = CHS.cfst ⌊ d ⌋ᴰ
    ⌊ csnd d ⌋ᴰ   = CHS.csnd ⌊ d ⌋ᴰ
    ⌊ unit d ⌋ᴰ   = CHS.unit ⌊ d ⌋ᴰ

    ⌊_⌋ : ∀ {A} → ⊢ A → CHS.⊢ ⌊ A ⌋ᵀ
    ⌊ Ξ , d ⌋ = ⌊ Ξ ⌋ᵀ⋆ , ⌊ d ⌋ᴰ


-- Projection of types and derivations to a form parametrised by a closed, untyped representation of syntax.

module ClosedHilbert where
  open import A201607.OldBasicILP.Syntax.ClosedHilbert

  mutual
    ⌊_⌋ᵀ : Ty → CH.Ty
    ⌊ α P ⌋ᵀ   = CH.α P
    ⌊ A ▻ B ⌋ᵀ = ⌊ A ⌋ᵀ CH.▻ ⌊ B ⌋ᵀ
    ⌊ p ⦂ A ⌋ᵀ = ⌊ p ⌋ᴾ CH.⦂ ⌊ A ⌋ᵀ
    ⌊ A ∧ B ⌋ᵀ = ⌊ A ⌋ᵀ CH.∧ ⌊ B ⌋ᵀ
    ⌊ ⊤ ⌋ᵀ    = CH.⊤

    ⌊_⌋ᴾ : ∀ {A} → Proof A → CH.Proof
    ⌊ [ d ] ⌋ᴾ = CH.[ CH.ᴿ⌊ ⌊ d ⌋ ⌋ ]

    ⌊_⌋ : ∀ {A} → ⊢ A → CH.⊢ ⌊ A ⌋ᵀ
    ⌊ app d₁ d₂ ⌋ = CH.app ⌊ d₁ ⌋ ⌊ d₂ ⌋
    ⌊ ci ⌋        = CH.ci
    ⌊ ck ⌋        = CH.ck
    ⌊ cs ⌋        = CH.cs
    ⌊ box d ⌋     = CH.box ⌊ d ⌋
    ⌊ cdist ⌋     = CH.cdist
    ⌊ cup ⌋       = CH.cup
    ⌊ cdown ⌋     = CH.cdown
    ⌊ cpair ⌋     = CH.cpair
    ⌊ cfst ⌋      = CH.cfst
    ⌊ csnd ⌋      = CH.csnd
    ⌊ unit ⌋      = CH.unit