[Agda] Converting intrinsically typed terms

[rozowski w.k. (wkr1u18)]

Hello everyone!

I'm relatively new to Agda (recently just went through first two Parts of PLFA), so I'm sorry if my question is obvious or don't appropriate for this forum.
I am writing to ask for any advice how to formalise type correct transformations between intrinsically typed terms.

Currently, while doing my BSc thesis, I am working on formalizing a paper about framework for specifying abstract machines, as a series of transforms between STLC and intermediate languages including combinators (eg. pushₛ to push on stack, ƛₛ to pop from stack and bind to variable, _∘_ to perform sequencing). Each intermediate language adds a pair of push and lambda combinators to work with different parts of machine - eg. environments, continuations. Each of the intermediate languages is a subset of the following ones.

The type rules (and way of building terms - because intrinsic typing) for those combinators, are:
  pushₛ_ : ∀ {Γ A}
    → Γ ⊢ A
      -----
    → Γ ⊢ Rₛ A

  ƛₛ_  : ∀ {Γ A B}
    → Γ , A ⊢ B
      ---------
    → Γ ⊢ A ⇒ₛ B

  _∘_ : ∀ {Γ A B}
    → Γ ⊢ Rₛ A
    → Γ ⊢ A ⇒ₛ B
      ---------
    → Γ ⊢ B

(Rs A is just annotated type for something of type A being stored on stack)

I managed to use the PLFA formalism and add typing rules for lambda calculus extended with pair of combinators for the stack and sequencing operators. The extended semantics now include:

  ξ-∘ₛ₁ : ∀ {Γ A B} {L L′ : Γ ⊢ A ⇒ₛ B} {M : Γ ⊢ Rₛ A}
    → L —→ L′
      ---------------
    → M ∘ L —→ M ∘ L′

  ξ-∘ₛ₂ : ∀ {Γ A B} {V : Γ ⊢ A ⇒ₛ B} {M M′ : Γ ⊢ Rₛ A}
    → Value V
    → M —→ M′
      ---------------
    → M ∘ V —→ M′ ∘ V

  β-∘ₛ :  ∀ {Γ A B} {N : Γ , A ⊢ B} {W : Γ ⊢ A}
      -------------------
    →  (pushₛ W) ∘ (ƛₛ N) —→ N [ W ]

The part I am having trouble with is formalising a transform between terms from STLC to this intermediate language. One of the transforms introduced by this paper is:

Va : Λ→Λs

Va [[x]] = pushs x
Va [[λx.E]] = pushs (λsx.Va [[E]] )
Va [[E1 E2]] = Va [[E2]] o Va [[E1]] o app with app = λsf.f

 As the STLC is the subset of the first combinator language, I just defined transform from the language to itself: I defined map between types, contexts and variables lookup

Va-type : Type → Type
Va-type (x ⇒ x₁) = Rₛ ( (Va-type x) ⇒ₛ (Va-type x₁) )
Va-type `ℕ  = Rₛ `ℕ
Va-type (Rₛ x)  = Rₛ (Va-type x)
Va-type (x ⇒ₛ x₁)  = (Va-type x) ⇒ₛ (Va-type x₁)

Va-context : Context → Context
Va-context ∅ = ∅
Va-context (x , x₁) =  ( Va-context x , Va-type x₁ )

Va-var : ∀ {Γ A} → Γ ∋ A → ((Va-context Γ) ∋ (Va-type A))
Va-var Z = Z
Va-var (S x) = S Va-var x

And the problematic part is declaring the transform between terms:

Va : ∀ {Γ A} → Γ ⊢ A → (Va-context Γ) ⊢ (Va-type A)
Va (` x) = ` Va-var x
Va (ƛ x) =  pushₛ (ƛₛ Va x)

-- Here is the hole I cannot come up with filling it
Va {Γ} (x · x₁) = (pushₛ (Va x₁)) ∘ ((pushₛ (Va x)) ∘ (ƛₛ {!!} ))
Va `zero = pushₛ `zero
Va (`suc x) = pushₛ (`zero) -- paper doesn't provide any notion for dealing with sucessors of Nats - currently left like this to pass the typecheck

-- Combinators from intermediate language are mapped to itself
Va (pushₛ x) = pushₛ Va x
Va (ƛₛ x) = ƛₛ Va x
Va (x ∘ x₁) = Va x ∘ Va x₁

The only bit, I am not able to formalise is the "app" combinator, as standard lookup using #_ doesnt work when mapping between terms.
Do you happen to have any advice for me, how to tackle such transformations? Is there anything I am missing in my way of formalising? Did any of you worked with type correct transformations of terms in de Brujin typed terms and have any tips for me?

I would be most grateful if I could hear back from you!

Best,
Wojciech
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201102/212afd68/attachment.html>