{-# OPTIONS --sized-types #-}
module A201607.OldBasicILP.Syntax.Translation where
open import A201607.Common.Context public
import A201607.OldBasicILP.Syntax.ClosedHilbertSequential as CHS
import A201607.OldBasicILP.Syntax.ClosedHilbert as CH
mutual
chsᵀ→chᵀ : CHS.Ty → CH.Ty
chsᵀ→chᵀ (CHS.α P) = CH.α P
chsᵀ→chᵀ (A CHS.▻ B) = chsᵀ→chᵀ A CH.▻ chsᵀ→chᵀ B
chsᵀ→chᵀ (p CHS.⦂ A) = chsᴾ→chᴾ p CH.⦂ chsᵀ→chᵀ A
chsᵀ→chᵀ (A CHS.∧ B) = chsᵀ→chᵀ A CH.∧ chsᵀ→chᵀ B
chsᵀ→chᵀ CHS.⊤ = CH.⊤
chsᴾ→chᴾ : ∀ {Ξ A} → CHS.Proof Ξ A → CH.Proof (chsᵀ→chᵀ A)
chsᴾ→chᴾ CHS.[ d ] = CH.[ chsᴰ→ch d top ]
chsᴰ→ch : ∀ {Ξ A} → CHS.⊢ᴰ Ξ → A ∈ Ξ → CH.⊢ (chsᵀ→chᵀ A)
chsᴰ→ch (CHS.mp i j d) top = CH.app (chsᴰ→ch d i) (chsᴰ→ch d j)
chsᴰ→ch (CHS.ci d) top = CH.ci
chsᴰ→ch (CHS.ck d) top = CH.ck
chsᴰ→ch (CHS.cs d) top = CH.cs
chsᴰ→ch (CHS.nec `d d) top = CH.box (chsᴰ→ch `d top)
chsᴰ→ch (CHS.cdist {Ξ} {A} {B} {`Ξ₁} {`Ξ₂} {`d₁} {`d₂} d) top = oops {A} {B} {`Ξ₁} {`Ξ₂} {`d₁} {`d₂}
chsᴰ→ch (CHS.cup d) top = CH.cup
chsᴰ→ch (CHS.cdown d) top = CH.cdown
chsᴰ→ch (CHS.cpair d) top = CH.cpair
chsᴰ→ch (CHS.cfst d) top = CH.cfst
chsᴰ→ch (CHS.csnd d) top = CH.csnd
chsᴰ→ch (CHS.unit d) top = CH.unit
chsᴰ→ch (CHS.mp i j d) (pop k) = chsᴰ→ch d k
chsᴰ→ch (CHS.ci d) (pop k) = chsᴰ→ch d k
chsᴰ→ch (CHS.ck d) (pop k) = chsᴰ→ch d k
chsᴰ→ch (CHS.cs d) (pop k) = chsᴰ→ch d k
chsᴰ→ch (CHS.nec `d d) (pop k) = chsᴰ→ch d k
chsᴰ→ch (CHS.cdist d) (pop k) = chsᴰ→ch d k
chsᴰ→ch (CHS.cup d) (pop k) = chsᴰ→ch d k
chsᴰ→ch (CHS.cdown d) (pop k) = chsᴰ→ch d k
chsᴰ→ch (CHS.cpair d) (pop k) = chsᴰ→ch d k
chsᴰ→ch (CHS.cfst d) (pop k) = chsᴰ→ch d k
chsᴰ→ch (CHS.csnd d) (pop k) = chsᴰ→ch d k
chsᴰ→ch (CHS.unit d) (pop k) = chsᴰ→ch d k
postulate
oops : ∀ {A B Ξ₁ Ξ₂} {d₁ : CHS.⊢ᴰ Ξ₁ , A CHS.▻ B} {d₂ : CHS.⊢ᴰ Ξ₂ , A}
→ CH.⊢ chsᴾ→chᴾ CHS.[ d₁ ] CH.⦂ (chsᵀ→chᵀ A CH.▻ chsᵀ→chᵀ B) CH.▻
chsᴾ→chᴾ CHS.[ d₂ ] CH.⦂ chsᵀ→chᵀ A CH.▻
chsᴾ→chᴾ CHS.[ CHS.appᴰ d₁ d₂ ] CH.⦂ chsᵀ→chᵀ B
chs→ch : ∀ {A} → CHS.⊢ A → CH.⊢ (chsᵀ→chᵀ A)
chs→ch (Ξ , d) = chsᴰ→ch d top
mutual
chᵀ→chsᵀ : CH.Ty → CHS.Ty
chᵀ→chsᵀ (CH.α P) = CHS.α P
chᵀ→chsᵀ (A CH.▻ B) = chᵀ→chsᵀ A CHS.▻ chᵀ→chsᵀ B
chᵀ→chsᵀ (p CH.⦂ A) with chᴾ→chsᴾ p
chᵀ→chsᵀ (p CH.⦂ A) | (Ξ , p′) = p′ CHS.⦂ chᵀ→chsᵀ A
chᵀ→chsᵀ (A CH.∧ B) = chᵀ→chsᵀ A CHS.∧ chᵀ→chsᵀ B
chᵀ→chsᵀ CH.⊤ = CHS.⊤
chᴾ→chsᴾ : ∀ {A} → CH.Proof A → ∃ (λ Ξ → CHS.Proof Ξ (chᵀ→chsᵀ A))
chᴾ→chsᴾ CH.[ d ] with ch→chs d
chᴾ→chsᴾ CH.[ d ] | (Ξ , d′) = Ξ , CHS.[ d′ ]
ch→chs : ∀ {A} → CH.⊢ A → CHS.⊢ (chᵀ→chsᵀ A)
ch→chs (CH.app d₁ d₂) = CHS.app (ch→chs d₁) (ch→chs d₂)
ch→chs CH.ci = ∅ , CHS.ci CHS.nil
ch→chs CH.ck = ∅ , CHS.ck CHS.nil
ch→chs CH.cs = ∅ , CHS.cs CHS.nil
ch→chs (CH.box d) = CHS.box (ch→chs d)
ch→chs CH.cdist = ∅ , CHS.cdist CHS.nil
ch→chs CH.cup = ∅ , CHS.cup CHS.nil
ch→chs CH.cdown = ∅ , CHS.cdown CHS.nil
ch→chs CH.cpair = ∅ , CHS.cpair CHS.nil
ch→chs CH.cfst = ∅ , CHS.cfst CHS.nil
ch→chs CH.csnd = ∅ , CHS.csnd CHS.nil
ch→chs CH.unit = ∅ , CHS.unit CHS.nil