{-# OPTIONS --safe --sized-types #-}
module Motivation.Problem.WithLibrary where
open import Data.Var hiding (_<$>_)
open import Data.Var.Varlike
open import Data.Environment as E
open import Data.Relation
open import Generic.Syntax
open import Generic.Syntax.LetBinder
open import Generic.Semantics
open import Generic.Semantics.Syntactic
open import Generic.Semantics.Elaboration.LetBinder
open import Generic.Simulation as S
open import Generic.Fusion
open import Generic.Fusion.Syntactic as F
open import Generic.Fusion.Elaboration.LetBinder
open import Generic.Identity
open import Data.Bool hiding (T)
open import Data.Sum
open import Data.Product
open import Function
open import Relation.Binary.PropositionalEquality hiding ([_])
open ≡-Reasoning
open import Data.List hiding ([_] ; lookup)
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
infixr 5 _⇒_
data Type : Set where
♭ : Type
_⇒_ : Type → Type → Type
data `Target : Set where
Lam App : Type → Type → `Target
Target : Desc Type
Target = `σ `Target $ λ where
(Lam σ τ) → `X (σ ∷ []) τ (`∎ (σ ⇒ τ))
(App σ τ) → `X [] (σ ⇒ τ) (`X [] σ (`∎ τ))
Source : Desc Type
Source = Target `+ Let
S : Type ─Scoped
S = Tm Source _
T : Type ─Scoped
T = Tm Target _
pattern lam' b = (Lam _ _ , b , refl)
pattern lamS' b = (true , lam' b)
pattern lamS b = `con (lamS' b)
pattern lamT b = `con (lam' b)
pattern app' f t = (App _ _ , f , t , refl)
pattern appS' f t = (true , app' f t)
pattern appS f t = `con (appS' f t)
pattern appT f t = `con (app' f t)
pattern defS' e t = (false , _ , e , t , refl)
pattern defS e t = `con (defS' e t)
infix 1 _⊢_∋_↝S_
data _⊢_∋_↝S_ : ∀ Γ σ → S σ Γ → S σ Γ → Set where
`β : ∀ {Γ σ τ} (b : S τ (σ ∷ Γ)) u → Γ ⊢ τ ∋ appS (lamS b) u ↝S b [ u /0]
`ζ : ∀ {Γ σ τ} e (t : S τ (σ ∷ Γ)) → Γ ⊢ τ ∋ defS e t ↝S t [ e /0]
`lam : ∀ {Γ σ τ b c} → (σ ∷ Γ) ⊢ τ ∋ b ↝S c → Γ ⊢ σ ⇒ τ ∋ lamS b ↝S lamS c
`appl : ∀ {Γ σ τ f g} → Γ ⊢ σ ⇒ τ ∋ f ↝S g → ∀ t → Γ ⊢ τ ∋ appS f t ↝S appS g t
`appr : ∀ {Γ σ τ t u} f → Γ ⊢ σ ∋ t ↝S u → Γ ⊢ τ ∋ appS f t ↝S appS f u
infix 1 _⊢_∋_↝T_
data _⊢_∋_↝T_ : ∀ Γ σ → T σ Γ → T σ Γ → Set where
`β : ∀ {Γ σ τ} (b : T τ (σ ∷ Γ)) u → Γ ⊢ τ ∋ appT (lamT b) u ↝T b [ u /0]
`lam : ∀ {Γ σ τ b c} → (σ ∷ Γ) ⊢ τ ∋ b ↝T c → Γ ⊢ σ ⇒ τ ∋ lamT b ↝T lamT c
`appl : ∀ {Γ σ τ f g} → Γ ⊢ σ ⇒ τ ∋ f ↝T g → ∀ t → Γ ⊢ τ ∋ appT f t ↝T appT g t
`appr : ∀ {Γ σ τ t u} f → Γ ⊢ σ ∋ t ↝T u → Γ ⊢ τ ∋ appT f t ↝T appT f u
_⊢_∋_↝⋆T_ : ∀ Γ σ → T σ Γ → T σ Γ → Set
Γ ⊢ σ ∋ t ↝⋆T u = Star (Γ ⊢ σ ∋_↝T_) t u
↝⋆Tᴿ : Rel T T
rel ↝⋆Tᴿ σ = _ ⊢ σ ∋_↝⋆T_
th^↝T : ∀ {Γ Δ σ t u} (ρ : Thinning Γ Δ) →
Γ ⊢ σ ∋ t ↝T u → Δ ⊢ σ ∋ th^Tm t ρ ↝T th^Tm u ρ
th^↝T ρ (`lam r) = `lam (th^↝T _ r)
th^↝T ρ (`appl r t) = `appl (th^↝T ρ r) _
th^↝T ρ (`appr f r) = `appr _ (th^↝T ρ r)
th^↝T ρ (`β b u) = cast $ `β (th^Tm b _) (th^Tm u ρ)
where cast = subst (_ ⊢ _ ∋ th^Tm (appT (lamT b) u) ρ ↝T_) (renβ Target b (E.ε ∙ u) ρ)
th^↝⋆T : ∀ {Γ Δ σ t u} (ρ : Thinning Γ Δ) →
Γ ⊢ σ ∋ t ↝⋆T u → Δ ⊢ σ ∋ th^Tm t ρ ↝⋆T th^Tm u ρ
th^↝⋆T ρ Star.ε = Star.ε
th^↝⋆T ρ (r ◅ rs) = th^↝T ρ r ◅ th^↝⋆T ρ rs
UnLet^↝⋆T : Simulation Source UnLet UnLet ↝⋆Tᴿ ↝⋆Tᴿ
Simulation.thᴿ UnLet^↝⋆T = th^↝⋆T
Simulation.varᴿ UnLet^↝⋆T = id
Simulation.algᴿ UnLet^↝⋆T = λ where
(appS' f t) ρᴿ (refl , refl , f^r , t^r , _) →
gmap (λ f → appT f _) (λ r → `appl r _) f^r
◅◅ gmap (appT _) (`appr _) t^r
(lamS' b) ρᴿ (refl , refl , b^r , _) →
gmap lamT `lam (b^r _ (packᴿ (λ v → Star.ε)))
(defS' e t) ρᴿ (refl , refl , e^r , t^r , _) →
t^r _ (εᴿ ∙ᴿ e^r)
simulation : ∀ {Γ Δ σ t u ρ ρ′} → All ↝⋆Tᴿ Γ ρ ρ′ → Γ ⊢ σ ∋ t ↝S u →
Δ ⊢ σ ∋ unLet ρ t ↝⋆T unLet ρ′ u
simulation {Γ} {Δ} {ρ = ρ} {ρ′} ρᴿ (`β b u) =
subst (Δ ⊢ _ ∋ _ ↝⋆T_) (sym (Fusion.fusion SubUnLet reflᴿ b))
$ `β (unLet _ b) (unLet _ u)
◅_ $ subst (Δ ⊢ _ ∋_↝⋆T _) (sym (unLetSub b eqᴿ))
$ Simulation.sim UnLet^↝⋆T ρ∙uᴿ b where
eq′ᴿ : All Eqᴿ _ (select (th^Env th^Var (base vl^Var) weaken) (unLet ρ u /0])) (base vl^Tm)
lookupᴿ eq′ᴿ z = refl
lookupᴿ eq′ᴿ (s v) = cong (ren weaken ∘ lookup (base vl^Tm)) (lookup-base^Var v)
eqᴿ : All Eqᴿ _ (sub (unLet ρ u /0]) <$> (freshˡ vl^Tm Δ >> _))
(unLet ρ <$> (u /0]))
lookupᴿ eqᴿ z = refl
lookupᴿ eqᴿ (s v) = begin
sub (unLet ρ u /0]) (ren (th^Env th^Var (base vl^Var) weaken) (lookup ρ v))
≡⟨ Fusion.fusion (F.RenSub Target) eq′ᴿ (lookup ρ v) ⟩
sub (base vl^Tm) (lookup ρ v)
≡⟨ sub-id (lookup ρ v) ⟩
lookup ρ v
≡⟨ cong (unLet ρ) (sym $ lookup-base^Tm v) ⟩
unLet ρ (lookup (base vl^Tm) v)
∎
ρ∙uᴿ : All ↝⋆Tᴿ _ (unLet ρ <$> (u /0])) (unLet ρ′ <$> (u /0]))
lookupᴿ ρ∙uᴿ z = Simulation.sim UnLet^↝⋆T ρᴿ u
lookupᴿ ρ∙uᴿ (s v) = cast $ lookupᴿ ρᴿ v where
cast = subst (λ v → Δ ⊢ _ ∋ unLet ρ v ↝⋆T unLet ρ′ v) (sym (lookup-base^Tm v))
simulation {ρ = ρ} {ρ′} ρᴿ (`ζ e t) =
subst (_ ⊢ _ ∋ _ ↝⋆T_) (sym (Fusion.fusion SubUnLet reflᴿ t))
$ Simulation.sim UnLet^↝⋆T ρ′ᴿ t where
ρ′ᴿ : All ↝⋆Tᴿ _ ((E.ε ∙ unLet ρ e) >> th^Env th^Tm ρ (pack id)) (unLet ρ′ <$> (e /0]))
lookupᴿ ρ′ᴿ k with split (_ ∷ []) k
... | inj₁ z = Simulation.sim UnLet^↝⋆T ρᴿ e
... | inj₁ (s ())
... | inj₂ kʳ = cast $ lookupᴿ ρᴿ kʳ where
cast = subst₂ (λ v w → _ ⊢ _ ∋ v ↝⋆T unLet ρ′ w)
(sym (ren-id′ (lookup ρ kʳ)))
(sym (lookup-base^Tm kʳ))
simulation {Γ} {Δ} {ρ = ρ} {ρ′} ρᴿ (`lam r) = gmap lamT `lam (simulation ρ′ᴿ r) where
ρ′ᴿ : All ↝⋆Tᴿ _ (freshˡ vl^Tm Δ >> th^Env th^Tm ρ (freshʳ vl^Var (_ ∷ [])))
(freshˡ vl^Tm Δ >> th^Env th^Tm ρ′ (freshʳ vl^Var (_ ∷ [])))
lookupᴿ ρ′ᴿ k with split (_ ∷ []) k
... | inj₁ kˡ = Star.ε
... | inj₂ kʳ = th^↝⋆T (th^Env th^Var (base vl^Var) weaken) (lookupᴿ ρᴿ kʳ)
simulation ρᴿ (`appl r t) =
gmap (λ f → appT f _) (λ r → `appl r _) (simulation ρᴿ r)
◅◅ gmap (appT _) (`appr _) (Simulation.sim UnLet^↝⋆T ρᴿ t)
simulation ρᴿ (`appr f r) =
gmap (appT _) (`appr _) (simulation ρᴿ r)
◅◅ gmap (λ f → appT f _) (λ r → `appl r _) (Simulation.sim UnLet^↝⋆T ρᴿ f)