-- A weak HOAS interface to de Bruijn terms.
------------------------------------------------------------------------

-- Remembering one of Conor McBride's tricks.

-- Andreas, 14th March 2019,
-- AIM XXIX, 29th Agda Implementor's meeting,
-- Ochanomizu University, Tokyo, Japan

-- We need a more powerful version of instance search: overlapping instances.

{-# OPTIONS --overlapping-instances #-}
{-# OPTIONS --instance-search-depth=3 #-}


-- Imports.
------------------------------------------------------------------------

-- Contexts

open import Data.List using (List; []; _∷_)

-- Variables

open import Data.List.Membership.Propositional    using (_∈_)
open import Data.List.Any                         using (here; there)
open import Relation.Binary.PropositionalEquality using (refl)

pattern here! = here refl

-- Context extension

open import Data.List.Relation.Binary.Sublist.Propositional
  using    (_⊆_)
  renaming (skip to weak; keep to lift; base to [])
  renaming (lookup to renVar)

open import Data.List.Relation.Binary.Sublist.Propositional.Properties
  using    (⊆-refl; ⊆-trans)


-- Simply typed terms in de Bruijn representation.
------------------------------------------------------------------------

-- Types

infixr 15 _⇒_

data Ty : Set where
  _⇒_ : (A B : Ty) → Ty

-- Contexts, variables

Cxt = List Ty
Var = _∈_

-- We use the following default typings.

variable
  A B C : Ty
  Γ Δ Φ : Cxt
  x y   : Var A Γ

-- De Bruijn terms.

module DB where

  data Tm : (A : Ty) (Γ : Cxt) → Set where
    var : (x : Var A Γ)                   → Tm A Γ
    app : (t : Tm (A ⇒ B) Γ) (u : Tm A Γ) → Tm B Γ
    abs : (t : Tm B (A ∷ Γ))              → Tm (A ⇒ B) Γ

open DB using (Tm)


-- Context-indexed sets.
------------------------------------------------------------------------

CSet = Cxt → Set

-- Context extension.

_•_ : (P : CSet) (A : Ty) → CSet
(P • A) Γ = P (A ∷ Γ)

-- Pointwise function space.

_→̇_ : (P Q : CSet) → CSet
(P →̇ Q) Γ = P Γ → Q Γ

-- "Kripke"; monotonization.

□ : CSet → CSet
□ P Δ = ∀{Γ} {{τ : Δ ⊆ Γ}} → P Γ

-- Kripke function space.

_→̂_ : (P Q : CSet) → CSet
P →̂ Q = □ (P →̇ Q)

  -- (P →̂ Q) Δ = ∀{Γ} {{τ : Δ ⊆ Γ}} → P Γ → Q Γ

-- Global elements.

[_] : CSet → Set
[ P ] = ∀{Γ} → P Γ

infixl 15 _•_
infixr 10 _→̇_ _→̂_


-- Sublist chains Δ ⊆⁺ Γ:
------------------------------------------------------------------------

-- instance version of Relation.Binary.Construct.Closure.ReflexiveTransitive.Star
-- formerly known as Data.Star.Star
--
-- We use them to make instance search work, rather than using ⊆-refl and ⊆-trans as instances.

data _⊆⁺_ : (Γ Δ : Cxt) → Set where
  instance
    ε   :                                Γ ⊆⁺ Γ
    _◅_ : ⦃ τ : Δ ⊆ Γ ⦄ ⦃ τs : Φ ⊆⁺ Δ ⦄ → Φ ⊆⁺ Γ

-- Renaming a variable along a chain.

rensVar : (τs : Δ ⊆⁺ Γ) → Var A Δ → Var A Γ
rensVar ε                 x = x
rensVar (_◅_ ⦃ τ ⦄ ⦃ τs ⦄) x = renVar τ (rensVar τs x)


-- Weak HOAS smart constructors.
------------------------------------------------------------------------

-- Application (infix).

infixl 4 _∙_

_∙_ : [ Tm (A ⇒ B) →̇ Tm A →̇ Tm B ]
t ∙ u = DB.app t u

-- Abstraction.

abs : [ (Var A →̂ Tm B) →̇ Tm (A ⇒ B) ]
abs {A = A} {Γ = Γ} f = DB.abs (f {A ∷ Γ} ⦃ τ = weak ⊆-refl ⦄ here!)

-- Variable.

var : ⦃ τs : Δ ⊆⁺ Γ ⦄ → Var A Δ → Tm A Γ
var ⦃ τs ⦄ x = DB.var (rensVar τs x)


-- Examples.
------------------------------------------------------------------------

-- K  = λ x y. x
-- K* = λ x y. y

K : [ Tm (A ⇒ (B ⇒ A)) ]
K = abs λ x → abs λ y → var x

K* : [ Tm (A ⇒ (B ⇒ B)) ]
K* = abs λ x → abs λ y → var y

-- S = λ x y z. x z (y z)

S : [ Tm ((A ⇒ (B ⇒ C)) ⇒ (A ⇒ B) ⇒ A ⇒ C) ]
S = abs λ x → abs λ y → abs λ z →
      var x ∙ var z ∙ (var y ∙ var z)

-- Bind for the continuation monad:  λ ma mb k. ma (λ a. mb a k)

Bind : [ Tm (       ((A ⇒ C) ⇒ C)
             ⇒ (A ⇒ ((B ⇒ C) ⇒ C))
                   ⇒ (B ⇒ C) ⇒ C) ]
Bind = abs λ ma →
       abs λ mb →
       abs λ k  →
          var ma ∙ abs λ a →
           var mb ∙ var a ∙ var k


-- Iso.

toDB : [ (Var A →̂ Tm B) →̇ Tm B • A ]
toDB f = f {{ weak ⊆-refl }} here!

toHOAS : [ Tm B • A →̇ (Var A →̂ Tm B) ]
toHOAS t (here {A} {Γ} refl) = {!!}
toHOAS t (there x) = {!!}