{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UnicodeSyntax #-}

module Abt.Concrete.LocallyNameless
( Tm(..)
, Var(..)
, varName
, varIndex
) where

import Abt.Types.Nat
import Abt.Types.HList
import Abt.Types.View
import Abt.Class.HEq1
import Abt.Class.Show1
import Abt.Class.Abt
import Abt.Class.Monad

import Control.Applicative

-- | A variable is a De Bruijn index, optionally decorated with a display name.
data Var
  = Var
  { _varName  !(Maybe String)
  , _varIndex  !Int
  }

instance Show Var where
  show (Var (Just v) _) = v
  show (Var Nothing i) = "@" ++ show i

instance Eq Var where
  (Var _ i) == (Var _ j) = i == j

instance Ord Var where
  compare (Var _ i) (Var _ j) = compare i j

-- | A lens for '_varName'.
--
-- @
-- varName ∷ Lens' 'Var' ('Maybe' 'String')
-- @
--
varName
   Functor f
   (Maybe String  f (Maybe String))
   Var
   f Var
varName i (Var n j) =
  (\n'  Var n' j)
    <$> i n

-- | A lens for '_varIndex'.
--
-- @
-- varIndex ∷ Lens' 'Var' 'Int'
-- @
--
varIndex
   Functor f
   (Int  f Int)
   Var
   f Var
varIndex i (Var n j) =
  (\j'  Var n j')
    <$> i j

-- | Locally nameless terms with operators in @o@ at arity @n@.
--
data Tm (o  [Nat]  *) (n  Nat) where
  Free  Var  Tm o Z
  Bound  Int  Tm o Z
  Abs  Tm o n  Tm o (S n)
  App  o ns  HList (Tm o) ns  Tm o Z

instance HEq1 o  HEq1 (Tm o) where
  Free v1 === Free v2 = v1 == v2
  Bound m === Bound n = m == n
  Abs e1 === Abs e2 = e1 === e2
  App o1 es1 === App o2 es2 = o1 === o2 && es1 === es2
  _ === _ = False

shiftVar
   Var
   Int
   Tm o n
   Tm o n
shiftVar v n = \case
  Free v'  if v == v' then Bound n else Free v'
  Bound m  Bound m
  Abs e  Abs (shiftVar v (n + 1) e)
  App p es  App p $ hmap (shiftVar v n) es

addVar
   Var
   Int
   Tm o n
   Tm o n
addVar v n = \case
  Free v'  Free v'
  Bound m  if m == n then Free v else Bound m
  Abs e  Abs (addVar v (n + 1) e)
  App p es  App p $ hmap (addVar v n) es

instance Show1 o  Abt Var o (Tm o) where
  into = \case
    V v  Free v
    v :\ e  Abs (shiftVar v 0 e)
    v :$ es  App v es

  out = \case
    Free v  return $ V v
    Bound n  fail "bound variable occured in out"
    Abs e  do
      v  fresh
      return $ v :\ addVar v 0 e
    App p es  return $ p :$ es