-- 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