{-# LANGUAGE Safe #-}
module DeBruijn.Lvl (
    Lvl,
    lvlToIdx,
    lvlZ,
    sinkLvl,
    Sinkable (..),
    sink,
    mapSink,
    sinkSize,
    mapSinkSize,
    sinkAdd,
    mapSinkAdd,
) where

import Data.Kind (Constraint, Type)

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

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

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

-- | de Bruijn levels.
--
--
type Lvl :: Ctx -> Type
type role Lvl nominal
data Lvl ctx = MkLvl !Int !(Idx ctx)
  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)

-- Note: we need an integer field for Show instance.

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

instance Show (Lvl ctx) where
    showsPrec :: Int -> Lvl ctx -> ShowS
showsPrec Int
d (MkLvl Int
i Idx ctx
_) = 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 Size ctx
_ (MkLvl Int
_ Idx ctx
x) = Idx ctx
x

-- | Last level.
--
-- >>> lvlZ S1
-- 1
--
-- >>> lvlZ S5
-- 5
--
lvlZ :: Size ctx -> Lvl (S ctx)
lvlZ :: forall (ctx :: Ctx). Size ctx -> Lvl (S ctx)
lvlZ Size ctx
s = Int -> Idx (S ctx) -> Lvl (S ctx)
forall (ctx :: Ctx). Int -> Idx ctx -> Lvl ctx
MkLvl (Size ctx -> Int
forall (ctx :: Ctx). Size ctx -> Int
sizeToInt Size ctx
s) Idx (S ctx)
forall (n1 :: Ctx). Idx ('S n1)
IZ

-- | Sink 'Lvl' into a larger context.
--
-- >>> sinkLvl (lvlZ S3)
-- 3
--
-- >>> sink (lvlZ S3)
-- 3
--
-- >>> mapLvl (LS LZ) (lvlZ S3)
-- 3
--
--
sinkLvl :: Lvl ctx -> Lvl (S ctx)
sinkLvl :: forall (ctx :: Ctx). Lvl ctx -> Lvl (S ctx)
sinkLvl (MkLvl Int
s Idx ctx
i) = Int -> Idx (S ctx) -> Lvl (S ctx)
forall (ctx :: Ctx). Int -> Idx ctx -> Lvl ctx
MkLvl Int
s (Idx ctx -> Idx (S ctx)
forall (n1 :: Ctx). Idx n1 -> Idx ('S n1)
IS Idx ctx
i)

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

-- | Sinkable terms can be weakened (sunk) cheaply.
-- (when 'Lvl' is implemented as newtype over 'Int').
type Sinkable :: (Ctx -> Type) -> Constraint
class Sinkable t where
    mapLvl :: Lte ctx ctx' -> t ctx -> t ctx'

lteLvl :: Lte ctx ctx' -> Lvl ctx -> Lvl ctx'
lteLvl :: forall (ctx :: Ctx) (ctx' :: Ctx).
Lte ctx ctx' -> Lvl ctx -> Lvl ctx'
lteLvl Lte ctx ctx'
LZ     Lvl ctx
t           = Lvl ctx
Lvl ctx'
t
lteLvl (LS Lte ctx ctx'1
l) (MkLvl Int
s Idx ctx
i) = Int -> Idx ctx' -> Lvl ctx'
forall (ctx :: Ctx). Int -> Idx ctx -> Lvl ctx
MkLvl Int
s (Lte ctx ctx' -> Idx ctx -> Idx ctx'
forall (ctx :: Ctx) (ctx' :: Ctx).
Lte ctx ctx' -> Idx ctx -> Idx ctx'
lteIdx (Lte ctx ctx'1 -> Lte ctx ('S ctx'1)
forall (ctx :: Ctx) (ctx'1 :: Ctx).
Lte ctx ctx'1 -> Lte ctx ('S ctx'1)
LS Lte ctx ctx'1
l) Idx ctx
i)

lteIdx :: Lte ctx ctx' -> Idx ctx -> Idx ctx'
lteIdx :: forall (ctx :: Ctx) (ctx' :: Ctx).
Lte ctx ctx' -> Idx ctx -> Idx ctx'
lteIdx Lte ctx ctx'
LZ     Idx ctx
i = Idx ctx
Idx ctx'
i
lteIdx (LS Lte ctx ctx'1
s) Idx ctx
i = Idx ctx'1 -> Idx ('S ctx'1)
forall (n1 :: Ctx). Idx n1 -> Idx ('S n1)
IS (Lte ctx ctx'1 -> Idx ctx -> Idx ctx'1
forall (ctx :: Ctx) (ctx' :: Ctx).
Lte ctx ctx' -> Idx ctx -> Idx ctx'
lteIdx Lte ctx ctx'1
s Idx ctx
i)

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 (ctx :: Ctx) (ctx' :: Ctx).
Lte ctx ctx' -> Lvl ctx -> Lvl ctx'
lteLvl

sink :: Sinkable t => t ctx -> t (S ctx)
sink :: forall (t :: Ctx -> *) (ctx :: Ctx).
Sinkable t =>
t ctx -> t (S ctx)
sink = Lte ctx (S ctx) -> t ctx -> t (S ctx)
forall (ctx :: Ctx) (ctx' :: Ctx). Lte ctx ctx' -> t ctx -> t ctx'
forall (t :: Ctx -> *) (ctx :: Ctx) (ctx' :: Ctx).
Sinkable t =>
Lte ctx ctx' -> t ctx -> t ctx'
mapLvl (Lte ctx ctx -> Lte ctx (S ctx)
forall (ctx :: Ctx) (ctx'1 :: Ctx).
Lte ctx ctx'1 -> Lte ctx ('S ctx'1)
LS Lte ctx ctx
forall (ctx :: Ctx). Lte ctx ctx
LZ)

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 = (t ctx -> t (S ctx)) -> f (t ctx) -> f (t (S ctx))
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap t ctx -> t (S ctx)
forall (t :: Ctx -> *) (ctx :: Ctx).
Sinkable t =>
t ctx -> t (S ctx)
sink

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
SZ     t EmptyCtx
t = t ctx
t EmptyCtx
t
sinkSize (SS Size ctx1
n) t EmptyCtx
t = t ctx1 -> t ('S ctx1)
forall (t :: Ctx -> *) (ctx :: Ctx).
Sinkable t =>
t ctx -> t (S ctx)
sink (Size ctx1 -> t EmptyCtx -> t ctx1
forall (t :: Ctx -> *) (ctx :: Ctx).
Sinkable t =>
Size ctx -> t EmptyCtx -> t ctx
sinkSize Size ctx1
n t EmptyCtx
t)

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 = (t EmptyCtx -> t ctx) -> f (t EmptyCtx) -> f (t ctx)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((t EmptyCtx -> t ctx) -> f (t EmptyCtx) -> f (t ctx))
-> (Size ctx -> t EmptyCtx -> t ctx)
-> Size ctx
-> f (t EmptyCtx)
-> f (t ctx)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Size ctx -> t EmptyCtx -> t ctx
forall (t :: Ctx -> *) (ctx :: Ctx).
Sinkable t =>
Size ctx -> t EmptyCtx -> t ctx
sinkSize

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'
AZ t ctx
t = t ctx
t ctx'
t
sinkAdd (AS Add n1 ctx ctx'
s) t ctx
t = t ctx' -> t ('S ctx')
forall (t :: Ctx -> *) (ctx :: Ctx).
Sinkable t =>
t ctx -> t (S ctx)
sink (Add n1 ctx ctx' -> t ctx -> t ctx'
forall (t :: Ctx -> *) (n :: Ctx) (ctx :: Ctx) (ctx' :: Ctx).
Sinkable t =>
Add n ctx ctx' -> t ctx -> t ctx'
sinkAdd Add n1 ctx ctx'
s t ctx
t)

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 = (t ctx -> t ctx') -> f (t ctx) -> f (t ctx')
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((t ctx -> t ctx') -> f (t ctx) -> f (t ctx'))
-> (Add n ctx ctx' -> t ctx -> t ctx')
-> Add n ctx ctx'
-> f (t ctx)
-> f (t ctx')
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Add n ctx ctx' -> t ctx -> t ctx'
forall (t :: Ctx -> *) (n :: Ctx) (ctx :: Ctx) (ctx' :: Ctx).
Sinkable t =>
Add n ctx ctx' -> t ctx -> t ctx'
sinkAdd