{-# LANGUAGE Unsafe #-}
-- | de Bruijn levels for well-scoped terms.
module DeBruijn.Internal.Lvl (
    -- * Levels
    Lvl (UnsafeLvl),
    lvlToIdx,
    idxToLvl,
    lvlZ,
    sinkLvl,
    Sinkable (..),
    sink,
    mapSink,
    sinkSize,
    mapSinkSize,
    sinkAdd,
    mapSinkAdd,
) where

import Data.Coerce   (coerce)
import Data.Kind     (Constraint, Type)
import Data.Proxy    (Proxy (..))
import Unsafe.Coerce (unsafeCoerce)

import DeBruijn.Add
import DeBruijn.Ctx
import DeBruijn.Internal.Idx
import DeBruijn.Internal.Size
import DeBruijn.Lte

-- $setup
-- >>> import DeBruijn
-- >>> import DeBruijn.Lte

-------------------------------------------------------------------------------
-- de Bruijn levels
-------------------------------------------------------------------------------

-- | de Bruijn levels.
type Lvl :: Ctx -> Type
type role Lvl nominal
newtype Lvl ctx = UnsafeLvl { forall (ctx :: Ctx). Lvl ctx -> Int
_unLvl :: Int }
  deriving (Lvl ctx -> Lvl ctx -> Bool
(Lvl ctx -> Lvl ctx -> Bool)
-> (Lvl ctx -> Lvl ctx -> Bool) -> Eq (Lvl ctx)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (ctx :: Ctx). Lvl ctx -> Lvl ctx -> Bool
$c== :: forall (ctx :: Ctx). Lvl ctx -> Lvl ctx -> Bool
== :: Lvl ctx -> Lvl ctx -> Bool
$c/= :: forall (ctx :: Ctx). Lvl ctx -> Lvl ctx -> Bool
/= :: Lvl ctx -> Lvl ctx -> Bool
Eq, Eq (Lvl ctx)
Eq (Lvl ctx) =>
(Lvl ctx -> Lvl ctx -> Ordering)
-> (Lvl ctx -> Lvl ctx -> Bool)
-> (Lvl ctx -> Lvl ctx -> Bool)
-> (Lvl ctx -> Lvl ctx -> Bool)
-> (Lvl ctx -> Lvl ctx -> Bool)
-> (Lvl ctx -> Lvl ctx -> Lvl ctx)
-> (Lvl ctx -> Lvl ctx -> Lvl ctx)
-> Ord (Lvl ctx)
Lvl ctx -> Lvl ctx -> Bool
Lvl ctx -> Lvl ctx -> Ordering
Lvl ctx -> Lvl ctx -> Lvl ctx
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall (ctx :: Ctx). Eq (Lvl ctx)
forall (ctx :: Ctx). Lvl ctx -> Lvl ctx -> Bool
forall (ctx :: Ctx). Lvl ctx -> Lvl ctx -> Ordering
forall (ctx :: Ctx). Lvl ctx -> Lvl ctx -> Lvl ctx
$ccompare :: forall (ctx :: Ctx). Lvl ctx -> Lvl ctx -> Ordering
compare :: Lvl ctx -> Lvl ctx -> Ordering
$c< :: forall (ctx :: Ctx). Lvl ctx -> Lvl ctx -> Bool
< :: Lvl ctx -> Lvl ctx -> Bool
$c<= :: forall (ctx :: Ctx). Lvl ctx -> Lvl ctx -> Bool
<= :: Lvl ctx -> Lvl ctx -> Bool
$c> :: forall (ctx :: Ctx). Lvl ctx -> Lvl ctx -> Bool
> :: Lvl ctx -> Lvl ctx -> Bool
$c>= :: forall (ctx :: Ctx). Lvl ctx -> Lvl ctx -> Bool
>= :: Lvl ctx -> Lvl ctx -> Bool
$cmax :: forall (ctx :: Ctx). Lvl ctx -> Lvl ctx -> Lvl ctx
max :: Lvl ctx -> Lvl ctx -> Lvl ctx
$cmin :: forall (ctx :: Ctx). Lvl ctx -> Lvl ctx -> Lvl ctx
min :: Lvl ctx -> Lvl ctx -> Lvl ctx
Ord)

-------------------------------------------------------------------------------
-- Instances
-------------------------------------------------------------------------------

instance Show (Lvl ctx) where
    showsPrec :: Int -> Lvl ctx -> ShowS
showsPrec Int
d (UnsafeLvl Int
i) = Int -> Int -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
d Int
i

-------------------------------------------------------------------------------
-- Helpers
-------------------------------------------------------------------------------

-- | Convert level to index.
--
-- >>> lvlToIdx S2 (lvlZ S1)
-- 0
--
lvlToIdx :: Size ctx -> Lvl ctx -> Idx ctx
lvlToIdx :: forall (ctx :: Ctx). Size ctx -> Lvl ctx -> Idx ctx
lvlToIdx (UnsafeSize Int
ctx) (UnsafeLvl Int
lvl) = Int -> Idx ctx
forall (j :: Ctx). Int -> Idx j
UnsafeIdx (Int
ctx Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
lvl Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)

idxToLvl :: Size ctx -> Idx ctx -> Lvl ctx
idxToLvl :: forall (ctx :: Ctx). Size ctx -> Idx ctx -> Lvl ctx
idxToLvl (UnsafeSize Int
ctx) (UnsafeIdx Int
idx) = Int -> Lvl ctx
forall (ctx :: Ctx). Int -> Lvl ctx
UnsafeLvl (Int
ctx Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
idx Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)

-- | Last level.
--
-- >>> lvlZ S1
-- 1
--
-- >>> lvlZ S5
-- 5
--
lvlZ :: Size ctx -> Lvl (S ctx)
lvlZ :: forall (ctx :: Ctx). Size ctx -> Lvl (S ctx)
lvlZ (UnsafeSize Int
s) = Int -> Lvl (S ctx)
forall (ctx :: Ctx). Int -> Lvl ctx
UnsafeLvl Int
s

-- | Sink 'Lvl' into a larger context.
--
-- >>> sinkLvl (lvlZ S3)
-- 3
--
-- >>> sink (lvlZ S3)
-- 3
--
-- >>> mapLvl (LS LZ) (lvlZ S3)
-- 3
--
sinkLvl :: Lvl n -> Lvl (S n)
sinkLvl :: forall (n :: Ctx). Lvl n -> Lvl (S n)
sinkLvl = Lvl n -> Lvl (S n)
forall a b. Coercible a b => a -> b
coerce

-------------------------------------------------------------------------------
-- Sinkable
-------------------------------------------------------------------------------

-- | Sinkable terms can be weakened (sunk) cheaply.
type Sinkable :: (Ctx -> Type) -> Constraint
class Sinkable t where
    mapLvl :: Lte ctx ctx' -> t ctx -> t ctx'

instance Sinkable Lvl where mapLvl :: forall (ctx :: Ctx) (ctx' :: Ctx).
Lte ctx ctx' -> Lvl ctx -> Lvl ctx'
mapLvl Lte ctx ctx'
_ = Lvl ctx -> Lvl ctx'
forall a b. Coercible a b => a -> b
coerce
instance Sinkable Proxy where mapLvl :: forall (ctx :: Ctx) (ctx' :: Ctx).
Lte ctx ctx' -> Proxy ctx -> Proxy ctx'
mapLvl Lte ctx ctx'
_ = Proxy ctx -> Proxy ctx'
forall a b. Coercible a b => a -> b
coerce

-- | Sink term.
sink :: Sinkable t => t ctx -> t (S ctx)
sink :: forall (t :: Ctx -> *) (ctx :: Ctx).
Sinkable t =>
t ctx -> t (S ctx)
sink = t ctx -> t (S ctx)
forall a b. a -> b
unsafeCoerce

-- | Sink term from empty context to a context of given size.
sinkSize :: Sinkable t => Size ctx -> t EmptyCtx -> t ctx
sinkSize :: forall (t :: Ctx -> *) (ctx :: Ctx).
Sinkable t =>
Size ctx -> t EmptyCtx -> t ctx
sinkSize Size ctx
_ = t EmptyCtx -> t ctx
forall a b. a -> b
unsafeCoerce

-- | Essentially @'fmap' 'sink'@
mapSink :: (Functor f, Sinkable t) => f (t ctx) -> f (t (S ctx))
mapSink :: forall (f :: * -> *) (t :: Ctx -> *) (ctx :: Ctx).
(Functor f, Sinkable t) =>
f (t ctx) -> f (t (S ctx))
mapSink = f (t ctx) -> f (t (S ctx))
forall a b. a -> b
unsafeCoerce

-- | Essentially @'fmap' . 'sinkSize'@
mapSinkSize :: (Functor f, Sinkable t) => Size ctx -> f (t EmptyCtx) -> f (t ctx)
mapSinkSize :: forall (f :: * -> *) (t :: Ctx -> *) (ctx :: Ctx).
(Functor f, Sinkable t) =>
Size ctx -> f (t EmptyCtx) -> f (t ctx)
mapSinkSize Size ctx
_ = f (t EmptyCtx) -> f (t ctx)
forall a b. a -> b
unsafeCoerce

sinkAdd :: Sinkable t => Add n ctx ctx' -> t ctx -> t ctx'
sinkAdd :: forall (t :: Ctx -> *) (n :: Ctx) (ctx :: Ctx) (ctx' :: Ctx).
Sinkable t =>
Add n ctx ctx' -> t ctx -> t ctx'
sinkAdd Add n ctx ctx'
_ = t ctx -> t ctx'
forall a b. a -> b
unsafeCoerce

mapSinkAdd :: (Functor f, Sinkable t) => Add n ctx ctx' -> f (t ctx) -> f (t ctx')
mapSinkAdd :: forall (f :: * -> *) (t :: Ctx -> *) (n :: Ctx) (ctx :: Ctx)
       (ctx' :: Ctx).
(Functor f, Sinkable t) =>
Add n ctx ctx' -> f (t ctx) -> f (t ctx')
mapSinkAdd Add n ctx ctx'
_ = f (t ctx) -> f (t ctx')
forall a b. a -> b
unsafeCoerce