module HOAS where

{-
This module demonstrates how to layer a HOAS-based representation
on top of a de Bruijn representation, to make it easier to generate well scoped
lambda terms.

It is based on Conor McBride's "Classy Hack"
https://mazzo.li/epilogue/index.html%3Fp=773.html

-}

import LC qualified
import Data.Fin
import Rebound.Bind.Single
import Rebound

-- Here are some HOAS lambda calculus terms

tru :: Tm Z
tru = Lam $ \x -> Lam $ \y -> Var x

fls :: Tm Z
fls = Lam $ \x -> Lam $ \y -> Var y

app :: Tm Z
app = Lam $ \f -> Lam $ \x -> App (Var f) (Var x)

omega :: Tm Z
omega = App delta delta where
    delta = Lam $ \x -> App (Var x) (Var x)

-- We can convert them to a de Bruijn-indexed
-- representation easily

-- >>> cvt tru
-- (λ. (λ. 1))

-- >>> cvt fls
-- (λ. (λ. 0))

-- >>> cvt app
-- (λ. (λ. (1 0)))

-- >>> cvt omega
-- ((λ. (0 0)) (λ. (0 0)))


-- These terms are elements of the following datatype
-- that uses a form of "weak higher-order abstract syntax"
-- for variable binding. A type class constraint in the variable
-- constructor constructs the appropriate de Bruijn index.
data Tm (a :: Nat) where
  Var :: (b ⊆ a) => Proxy b -> Tm a
  App :: Tm a -> Tm a -> Tm a
  Lam :: (Proxy (S a) -> Tm (S a)) -> Tm a

instance Cvt Tm LC.Exp where
  cvt :: Tm m -> LC.Exp m
  cvt (Var x)   = LC.Var (cvtVar x)
  cvt (App a b) = LC.App (cvt a) (cvt b)
  cvt (Lam f)   = LC.Lam (cvtBind f)

------------------------------------------------------------
-- The rest of this file is independent of the language that we are using
-- and can be called reusable "library" code
-- It depends on overlapping instances

-- Conversion type class
class Cvt t u | t -> u where
  cvt :: t m -> u m

class (b :: Nat) ⊆ (a :: Nat) where
    inj :: Fin b -> Fin a
instance {-# OVERLAPPING #-} n ⊆ n where inj = id
instance {-# OVERLAPPING #-} (o ~ S n, m ⊆ n) => m ⊆ o where inj = FS . inj

-- Note: you don't actually need overlapping instances for this example:
--- instance n ⊆ n where inj = id
--- instance n ⊆ S n where inj = FS
-- would work just as well

newtype Proxy b = P (Fin b)

zeroVar :: Proxy (S b)
zeroVar = P FZ

cvtVar :: (b ⊆ a) => Proxy b -> Fin a
cvtVar (P x) = inj x

cvtBind :: (Subst v u, Cvt t u) => (Proxy (S a) -> t (S a)) -> Bind v u a
cvtBind f = bind (cvt (f zeroVar))