{-# LANGUAGE DeriveAnyClass        #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE TemplateHaskell       #-}
-- | Support for using de Bruijn indices for term and type names.
module PlutusCore.DeBruijn.Internal
    ( Index (..)
    , HasIndex (..)
    , DeBruijn (..)
    , NamedDeBruijn (..)
    , FakeNamedDeBruijn (..)
    , TyDeBruijn (..)
    , NamedTyDeBruijn (..)
    , FreeVariableError (..)
    , AsFreeVariableError (..)
    , Level (..)
    , Levels (..)
    , declareUnique
    , declareBinder
    , withScope
    , getIndex
    , getUnique
    , unNameDeBruijn
    , unNameTyDeBruijn
    , fakeNameDeBruijn
    , nameToDeBruijn
    , tyNameToDeBruijn
    , deBruijnToName
    , deBruijnToTyName
    , freeIndexThrow
    , freeIndexAsConsistentLevel
    , freeUniqueThrow
    , runDeBruijnT
    , deBruijnInitIndex
    , toFake
    , fromFake
    ) where

import PlutusCore.Name
import PlutusCore.Pretty
import PlutusCore.Quote

import Control.Exception
import Control.Lens hiding (Index, Level, index, ix)
import Control.Monad.Error.Lens
import Control.Monad.Except
import Control.Monad.Reader
import Control.Monad.State

import Data.Bimap qualified as BM
import Data.Map qualified as M
import Data.Text qualified as T
import Data.Word
import Prettyprinter

import Control.DeepSeq (NFData)
import Data.Coerce
import ErrorCode
import GHC.Generics

-- | A relative index used for de Bruijn identifiers.
newtype Index = Index Word64
    deriving stock ((forall x. Index -> Rep Index x)
-> (forall x. Rep Index x -> Index) -> Generic Index
forall x. Rep Index x -> Index
forall x. Index -> Rep Index x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Index x -> Index
$cfrom :: forall x. Index -> Rep Index x
Generic)
    deriving newtype (Int -> Index -> ShowS
[Index] -> ShowS
Index -> String
(Int -> Index -> ShowS)
-> (Index -> String) -> ([Index] -> ShowS) -> Show Index
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Index] -> ShowS
$cshowList :: [Index] -> ShowS
show :: Index -> String
$cshow :: Index -> String
showsPrec :: Int -> Index -> ShowS
$cshowsPrec :: Int -> Index -> ShowS
Show, Integer -> Index
Index -> Index
Index -> Index -> Index
(Index -> Index -> Index)
-> (Index -> Index -> Index)
-> (Index -> Index -> Index)
-> (Index -> Index)
-> (Index -> Index)
-> (Index -> Index)
-> (Integer -> Index)
-> Num Index
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
fromInteger :: Integer -> Index
$cfromInteger :: Integer -> Index
signum :: Index -> Index
$csignum :: Index -> Index
abs :: Index -> Index
$cabs :: Index -> Index
negate :: Index -> Index
$cnegate :: Index -> Index
* :: Index -> Index -> Index
$c* :: Index -> Index -> Index
- :: Index -> Index -> Index
$c- :: Index -> Index -> Index
+ :: Index -> Index -> Index
$c+ :: Index -> Index -> Index
Num, Int -> Index
Index -> Int
Index -> [Index]
Index -> Index
Index -> Index -> [Index]
Index -> Index -> Index -> [Index]
(Index -> Index)
-> (Index -> Index)
-> (Int -> Index)
-> (Index -> Int)
-> (Index -> [Index])
-> (Index -> Index -> [Index])
-> (Index -> Index -> [Index])
-> (Index -> Index -> Index -> [Index])
-> Enum Index
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: Index -> Index -> Index -> [Index]
$cenumFromThenTo :: Index -> Index -> Index -> [Index]
enumFromTo :: Index -> Index -> [Index]
$cenumFromTo :: Index -> Index -> [Index]
enumFromThen :: Index -> Index -> [Index]
$cenumFromThen :: Index -> Index -> [Index]
enumFrom :: Index -> [Index]
$cenumFrom :: Index -> [Index]
fromEnum :: Index -> Int
$cfromEnum :: Index -> Int
toEnum :: Int -> Index
$ctoEnum :: Int -> Index
pred :: Index -> Index
$cpred :: Index -> Index
succ :: Index -> Index
$csucc :: Index -> Index
Enum, Num Index
Ord Index
Num Index -> Ord Index -> (Index -> Rational) -> Real Index
Index -> Rational
forall a. Num a -> Ord a -> (a -> Rational) -> Real a
toRational :: Index -> Rational
$ctoRational :: Index -> Rational
$cp2Real :: Ord Index
$cp1Real :: Num Index
Real, Enum Index
Real Index
Real Index
-> Enum Index
-> (Index -> Index -> Index)
-> (Index -> Index -> Index)
-> (Index -> Index -> Index)
-> (Index -> Index -> Index)
-> (Index -> Index -> (Index, Index))
-> (Index -> Index -> (Index, Index))
-> (Index -> Integer)
-> Integral Index
Index -> Integer
Index -> Index -> (Index, Index)
Index -> Index -> Index
forall a.
Real a
-> Enum a
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> (a, a))
-> (a -> a -> (a, a))
-> (a -> Integer)
-> Integral a
toInteger :: Index -> Integer
$ctoInteger :: Index -> Integer
divMod :: Index -> Index -> (Index, Index)
$cdivMod :: Index -> Index -> (Index, Index)
quotRem :: Index -> Index -> (Index, Index)
$cquotRem :: Index -> Index -> (Index, Index)
mod :: Index -> Index -> Index
$cmod :: Index -> Index -> Index
div :: Index -> Index -> Index
$cdiv :: Index -> Index -> Index
rem :: Index -> Index -> Index
$crem :: Index -> Index -> Index
quot :: Index -> Index -> Index
$cquot :: Index -> Index -> Index
$cp2Integral :: Enum Index
$cp1Integral :: Real Index
Integral, Index -> Index -> Bool
(Index -> Index -> Bool) -> (Index -> Index -> Bool) -> Eq Index
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Index -> Index -> Bool
$c/= :: Index -> Index -> Bool
== :: Index -> Index -> Bool
$c== :: Index -> Index -> Bool
Eq, Eq Index
Eq Index
-> (Index -> Index -> Ordering)
-> (Index -> Index -> Bool)
-> (Index -> Index -> Bool)
-> (Index -> Index -> Bool)
-> (Index -> Index -> Bool)
-> (Index -> Index -> Index)
-> (Index -> Index -> Index)
-> Ord Index
Index -> Index -> Bool
Index -> Index -> Ordering
Index -> Index -> Index
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
min :: Index -> Index -> Index
$cmin :: Index -> Index -> Index
max :: Index -> Index -> Index
$cmax :: Index -> Index -> Index
>= :: Index -> Index -> Bool
$c>= :: Index -> Index -> Bool
> :: Index -> Index -> Bool
$c> :: Index -> Index -> Bool
<= :: Index -> Index -> Bool
$c<= :: Index -> Index -> Bool
< :: Index -> Index -> Bool
$c< :: Index -> Index -> Bool
compare :: Index -> Index -> Ordering
$ccompare :: Index -> Index -> Ordering
$cp1Ord :: Eq Index
Ord, [Index] -> Doc ann
Index -> Doc ann
(forall ann. Index -> Doc ann)
-> (forall ann. [Index] -> Doc ann) -> Pretty Index
forall ann. [Index] -> Doc ann
forall ann. Index -> Doc ann
forall a.
(forall ann. a -> Doc ann)
-> (forall ann. [a] -> Doc ann) -> Pretty a
prettyList :: [Index] -> Doc ann
$cprettyList :: forall ann. [Index] -> Doc ann
pretty :: Index -> Doc ann
$cpretty :: forall ann. Index -> Doc ann
Pretty, Index -> ()
(Index -> ()) -> NFData Index
forall a. (a -> ()) -> NFData a
rnf :: Index -> ()
$crnf :: Index -> ()
NFData)

-- | The LamAbs index (for debruijn indices) and the starting level of DeBruijn monad
deBruijnInitIndex :: Index
deBruijnInitIndex :: Index
deBruijnInitIndex = Index
0

-- | A term name as a de Bruijn index.
data NamedDeBruijn = NamedDeBruijn { NamedDeBruijn -> Text
ndbnString :: T.Text, NamedDeBruijn -> Index
ndbnIndex :: Index }
    deriving stock (Int -> NamedDeBruijn -> ShowS
[NamedDeBruijn] -> ShowS
NamedDeBruijn -> String
(Int -> NamedDeBruijn -> ShowS)
-> (NamedDeBruijn -> String)
-> ([NamedDeBruijn] -> ShowS)
-> Show NamedDeBruijn
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NamedDeBruijn] -> ShowS
$cshowList :: [NamedDeBruijn] -> ShowS
show :: NamedDeBruijn -> String
$cshow :: NamedDeBruijn -> String
showsPrec :: Int -> NamedDeBruijn -> ShowS
$cshowsPrec :: Int -> NamedDeBruijn -> ShowS
Show, (forall x. NamedDeBruijn -> Rep NamedDeBruijn x)
-> (forall x. Rep NamedDeBruijn x -> NamedDeBruijn)
-> Generic NamedDeBruijn
forall x. Rep NamedDeBruijn x -> NamedDeBruijn
forall x. NamedDeBruijn -> Rep NamedDeBruijn x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep NamedDeBruijn x -> NamedDeBruijn
$cfrom :: forall x. NamedDeBruijn -> Rep NamedDeBruijn x
Generic)
    deriving anyclass NamedDeBruijn -> ()
(NamedDeBruijn -> ()) -> NFData NamedDeBruijn
forall a. (a -> ()) -> NFData a
rnf :: NamedDeBruijn -> ()
$crnf :: NamedDeBruijn -> ()
NFData

-- | A wrapper around nameddebruijn that must hold the invariant of name=`fakeName`.
newtype FakeNamedDeBruijn = FakeNamedDeBruijn NamedDeBruijn
    deriving newtype (Int -> FakeNamedDeBruijn -> ShowS
[FakeNamedDeBruijn] -> ShowS
FakeNamedDeBruijn -> String
(Int -> FakeNamedDeBruijn -> ShowS)
-> (FakeNamedDeBruijn -> String)
-> ([FakeNamedDeBruijn] -> ShowS)
-> Show FakeNamedDeBruijn
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FakeNamedDeBruijn] -> ShowS
$cshowList :: [FakeNamedDeBruijn] -> ShowS
show :: FakeNamedDeBruijn -> String
$cshow :: FakeNamedDeBruijn -> String
showsPrec :: Int -> FakeNamedDeBruijn -> ShowS
$cshowsPrec :: Int -> FakeNamedDeBruijn -> ShowS
Show, FakeNamedDeBruijn -> FakeNamedDeBruijn -> Bool
(FakeNamedDeBruijn -> FakeNamedDeBruijn -> Bool)
-> (FakeNamedDeBruijn -> FakeNamedDeBruijn -> Bool)
-> Eq FakeNamedDeBruijn
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FakeNamedDeBruijn -> FakeNamedDeBruijn -> Bool
$c/= :: FakeNamedDeBruijn -> FakeNamedDeBruijn -> Bool
== :: FakeNamedDeBruijn -> FakeNamedDeBruijn -> Bool
$c== :: FakeNamedDeBruijn -> FakeNamedDeBruijn -> Bool
Eq, FakeNamedDeBruijn -> ()
(FakeNamedDeBruijn -> ()) -> NFData FakeNamedDeBruijn
forall a. (a -> ()) -> NFData a
rnf :: FakeNamedDeBruijn -> ()
$crnf :: FakeNamedDeBruijn -> ()
NFData, PrettyBy config)

toFake :: DeBruijn -> FakeNamedDeBruijn
toFake :: DeBruijn -> FakeNamedDeBruijn
toFake (DeBruijn Index
ix) = NamedDeBruijn -> FakeNamedDeBruijn
FakeNamedDeBruijn (NamedDeBruijn -> FakeNamedDeBruijn)
-> NamedDeBruijn -> FakeNamedDeBruijn
forall a b. (a -> b) -> a -> b
$ Text -> Index -> NamedDeBruijn
NamedDeBruijn Text
fakeName Index
ix

fromFake :: FakeNamedDeBruijn -> DeBruijn
fromFake :: FakeNamedDeBruijn -> DeBruijn
fromFake (FakeNamedDeBruijn (NamedDeBruijn Text
_ Index
ix)) = Index -> DeBruijn
DeBruijn Index
ix

-- | Arbitrarily-chosen text to represent a missing textual representation of a debruijn index
fakeName :: T.Text
fakeName :: Text
fakeName = Text
"i"

instance Eq NamedDeBruijn where
    -- ignoring actual names and only relying solely on debruijn indices
    (NamedDeBruijn Text
_ Index
ix1) == :: NamedDeBruijn -> NamedDeBruijn -> Bool
== (NamedDeBruijn Text
_ Index
ix2) = Index
ix1 Index -> Index -> Bool
forall a. Eq a => a -> a -> Bool
== Index
ix2

-- | A term name as a de Bruijn index, without the name string.
newtype DeBruijn = DeBruijn { DeBruijn -> Index
dbnIndex :: Index }
    deriving stock (Int -> DeBruijn -> ShowS
[DeBruijn] -> ShowS
DeBruijn -> String
(Int -> DeBruijn -> ShowS)
-> (DeBruijn -> String) -> ([DeBruijn] -> ShowS) -> Show DeBruijn
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DeBruijn] -> ShowS
$cshowList :: [DeBruijn] -> ShowS
show :: DeBruijn -> String
$cshow :: DeBruijn -> String
showsPrec :: Int -> DeBruijn -> ShowS
$cshowsPrec :: Int -> DeBruijn -> ShowS
Show, (forall x. DeBruijn -> Rep DeBruijn x)
-> (forall x. Rep DeBruijn x -> DeBruijn) -> Generic DeBruijn
forall x. Rep DeBruijn x -> DeBruijn
forall x. DeBruijn -> Rep DeBruijn x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep DeBruijn x -> DeBruijn
$cfrom :: forall x. DeBruijn -> Rep DeBruijn x
Generic, DeBruijn -> DeBruijn -> Bool
(DeBruijn -> DeBruijn -> Bool)
-> (DeBruijn -> DeBruijn -> Bool) -> Eq DeBruijn
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DeBruijn -> DeBruijn -> Bool
$c/= :: DeBruijn -> DeBruijn -> Bool
== :: DeBruijn -> DeBruijn -> Bool
$c== :: DeBruijn -> DeBruijn -> Bool
Eq)
    deriving newtype (DeBruijn -> ()
(DeBruijn -> ()) -> NFData DeBruijn
forall a. (a -> ()) -> NFData a
rnf :: DeBruijn -> ()
$crnf :: DeBruijn -> ()
NFData)

-- | A type name as a de Bruijn index.
newtype NamedTyDeBruijn = NamedTyDeBruijn NamedDeBruijn
    deriving stock (Int -> NamedTyDeBruijn -> ShowS
[NamedTyDeBruijn] -> ShowS
NamedTyDeBruijn -> String
(Int -> NamedTyDeBruijn -> ShowS)
-> (NamedTyDeBruijn -> String)
-> ([NamedTyDeBruijn] -> ShowS)
-> Show NamedTyDeBruijn
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NamedTyDeBruijn] -> ShowS
$cshowList :: [NamedTyDeBruijn] -> ShowS
show :: NamedTyDeBruijn -> String
$cshow :: NamedTyDeBruijn -> String
showsPrec :: Int -> NamedTyDeBruijn -> ShowS
$cshowsPrec :: Int -> NamedTyDeBruijn -> ShowS
Show, (forall x. NamedTyDeBruijn -> Rep NamedTyDeBruijn x)
-> (forall x. Rep NamedTyDeBruijn x -> NamedTyDeBruijn)
-> Generic NamedTyDeBruijn
forall x. Rep NamedTyDeBruijn x -> NamedTyDeBruijn
forall x. NamedTyDeBruijn -> Rep NamedTyDeBruijn x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep NamedTyDeBruijn x -> NamedTyDeBruijn
$cfrom :: forall x. NamedTyDeBruijn -> Rep NamedTyDeBruijn x
Generic)
    deriving newtype (PrettyBy config, NamedTyDeBruijn -> ()
(NamedTyDeBruijn -> ()) -> NFData NamedTyDeBruijn
forall a. (a -> ()) -> NFData a
rnf :: NamedTyDeBruijn -> ()
$crnf :: NamedTyDeBruijn -> ()
NFData)
    -- ignoring actual names and only relying solely on debruijn indices
    deriving NamedTyDeBruijn -> NamedTyDeBruijn -> Bool
(NamedTyDeBruijn -> NamedTyDeBruijn -> Bool)
-> (NamedTyDeBruijn -> NamedTyDeBruijn -> Bool)
-> Eq NamedTyDeBruijn
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: NamedTyDeBruijn -> NamedTyDeBruijn -> Bool
$c/= :: NamedTyDeBruijn -> NamedTyDeBruijn -> Bool
== :: NamedTyDeBruijn -> NamedTyDeBruijn -> Bool
$c== :: NamedTyDeBruijn -> NamedTyDeBruijn -> Bool
Eq via NamedDeBruijn
instance Wrapped NamedTyDeBruijn

-- | A type name as a de Bruijn index, without the name string.
newtype TyDeBruijn = TyDeBruijn DeBruijn
    deriving stock (Int -> TyDeBruijn -> ShowS
[TyDeBruijn] -> ShowS
TyDeBruijn -> String
(Int -> TyDeBruijn -> ShowS)
-> (TyDeBruijn -> String)
-> ([TyDeBruijn] -> ShowS)
-> Show TyDeBruijn
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TyDeBruijn] -> ShowS
$cshowList :: [TyDeBruijn] -> ShowS
show :: TyDeBruijn -> String
$cshow :: TyDeBruijn -> String
showsPrec :: Int -> TyDeBruijn -> ShowS
$cshowsPrec :: Int -> TyDeBruijn -> ShowS
Show, (forall x. TyDeBruijn -> Rep TyDeBruijn x)
-> (forall x. Rep TyDeBruijn x -> TyDeBruijn) -> Generic TyDeBruijn
forall x. Rep TyDeBruijn x -> TyDeBruijn
forall x. TyDeBruijn -> Rep TyDeBruijn x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TyDeBruijn x -> TyDeBruijn
$cfrom :: forall x. TyDeBruijn -> Rep TyDeBruijn x
Generic)
    deriving newtype (TyDeBruijn -> ()
(TyDeBruijn -> ()) -> NFData TyDeBruijn
forall a. (a -> ()) -> NFData a
rnf :: TyDeBruijn -> ()
$crnf :: TyDeBruijn -> ()
NFData, PrettyBy config)
    deriving TyDeBruijn -> TyDeBruijn -> Bool
(TyDeBruijn -> TyDeBruijn -> Bool)
-> (TyDeBruijn -> TyDeBruijn -> Bool) -> Eq TyDeBruijn
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TyDeBruijn -> TyDeBruijn -> Bool
$c/= :: TyDeBruijn -> TyDeBruijn -> Bool
== :: TyDeBruijn -> TyDeBruijn -> Bool
$c== :: TyDeBruijn -> TyDeBruijn -> Bool
Eq via DeBruijn
instance Wrapped TyDeBruijn

instance HasPrettyConfigName config => PrettyBy config NamedDeBruijn where
    prettyBy :: config -> NamedDeBruijn -> Doc ann
prettyBy config
config (NamedDeBruijn Text
txt (Index Word64
ix))
        | Bool
showsUnique = Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
txt Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"_i" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Word64 -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Word64
ix
        | Bool
otherwise   = Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
txt
        where PrettyConfigName Bool
showsUnique = config -> PrettyConfigName
forall config.
HasPrettyConfigName config =>
config -> PrettyConfigName
toPrettyConfigName config
config

instance HasPrettyConfigName config => PrettyBy config DeBruijn where
    prettyBy :: config -> DeBruijn -> Doc ann
prettyBy config
config (DeBruijn (Index Word64
ix))
        | Bool
showsUnique = Doc ann
"i" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Word64 -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Word64
ix
        | Bool
otherwise   = Doc ann
""
        where PrettyConfigName Bool
showsUnique = config -> PrettyConfigName
forall config.
HasPrettyConfigName config =>
config -> PrettyConfigName
toPrettyConfigName config
config

class HasIndex a where
    index :: Lens' a Index

instance HasIndex NamedDeBruijn where
    index :: (Index -> f Index) -> NamedDeBruijn -> f NamedDeBruijn
index = (NamedDeBruijn -> Index)
-> (NamedDeBruijn -> Index -> NamedDeBruijn)
-> Lens' NamedDeBruijn Index
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens NamedDeBruijn -> Index
g NamedDeBruijn -> Index -> NamedDeBruijn
s where
        g :: NamedDeBruijn -> Index
g = NamedDeBruijn -> Index
ndbnIndex
        s :: NamedDeBruijn -> Index -> NamedDeBruijn
s NamedDeBruijn
n Index
i = NamedDeBruijn
n{ndbnIndex :: Index
ndbnIndex=Index
i}

instance HasIndex DeBruijn where
    index :: (Index -> f Index) -> DeBruijn -> f DeBruijn
index = (DeBruijn -> Index)
-> (DeBruijn -> Index -> DeBruijn) -> Lens' DeBruijn Index
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens DeBruijn -> Index
g DeBruijn -> Index -> DeBruijn
s where
        g :: DeBruijn -> Index
g = DeBruijn -> Index
dbnIndex
        s :: DeBruijn -> Index -> DeBruijn
s DeBruijn
n Index
i = DeBruijn
n{dbnIndex :: Index
dbnIndex=Index
i}

instance HasIndex NamedTyDeBruijn where
    index :: (Index -> f Index) -> NamedTyDeBruijn -> f NamedTyDeBruijn
index = (NamedDeBruijn -> f NamedDeBruijn)
-> NamedTyDeBruijn -> f NamedTyDeBruijn
forall s. Wrapped s => Iso' s (Unwrapped s)
_Wrapped' ((NamedDeBruijn -> f NamedDeBruijn)
 -> NamedTyDeBruijn -> f NamedTyDeBruijn)
-> ((Index -> f Index) -> NamedDeBruijn -> f NamedDeBruijn)
-> (Index -> f Index)
-> NamedTyDeBruijn
-> f NamedTyDeBruijn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Index -> f Index) -> NamedDeBruijn -> f NamedDeBruijn
forall a. HasIndex a => Lens' a Index
index

instance HasIndex TyDeBruijn where
    index :: (Index -> f Index) -> TyDeBruijn -> f TyDeBruijn
index = (DeBruijn -> f DeBruijn) -> TyDeBruijn -> f TyDeBruijn
forall s. Wrapped s => Iso' s (Unwrapped s)
_Wrapped' ((DeBruijn -> f DeBruijn) -> TyDeBruijn -> f TyDeBruijn)
-> ((Index -> f Index) -> DeBruijn -> f DeBruijn)
-> (Index -> f Index)
-> TyDeBruijn
-> f TyDeBruijn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Index -> f Index) -> DeBruijn -> f DeBruijn
forall a. HasIndex a => Lens' a Index
index

-- Converting from normal names to DeBruijn indices, and vice versa

{- Note [Levels and indices]
The indices ('Index') that we actually store as our de Bruijn indices in the program
are *relative* - that is, they say how many levels above the *current* level to look for
the binder.

However, when doing conversions it is easier to record the  *absolute* level of a variable,
in our state, since that way we don't have to adjust our mapping when we go under a binder (whereas
for relative indices we would need to increment them all by one, as the current level has increased).

However, this means that we *do* need to do an adjustment when we store an index as a level or extract
a level to use it as an index. The adjustment is fairly straightforward:
- An index `i` points to a binder `i` levels above (smaller than) the current level, so the level
  of `i` is `current - i`.
- A level `l` which is `i` levels above (smaller than) the current level has an index of `i`, so it
  is also calculated as `current - l`.

We use a newtype to keep these separate, since getting it wrong will lead to annoying bugs.
-}

-- | An absolute level in the program.
newtype Level = Level Integer deriving newtype (Level -> Level -> Bool
(Level -> Level -> Bool) -> (Level -> Level -> Bool) -> Eq Level
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Level -> Level -> Bool
$c/= :: Level -> Level -> Bool
== :: Level -> Level -> Bool
$c== :: Level -> Level -> Bool
Eq, Eq Level
Eq Level
-> (Level -> Level -> Ordering)
-> (Level -> Level -> Bool)
-> (Level -> Level -> Bool)
-> (Level -> Level -> Bool)
-> (Level -> Level -> Bool)
-> (Level -> Level -> Level)
-> (Level -> Level -> Level)
-> Ord Level
Level -> Level -> Bool
Level -> Level -> Ordering
Level -> Level -> Level
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
min :: Level -> Level -> Level
$cmin :: Level -> Level -> Level
max :: Level -> Level -> Level
$cmax :: Level -> Level -> Level
>= :: Level -> Level -> Bool
$c>= :: Level -> Level -> Bool
> :: Level -> Level -> Bool
$c> :: Level -> Level -> Bool
<= :: Level -> Level -> Bool
$c<= :: Level -> Level -> Bool
< :: Level -> Level -> Bool
$c< :: Level -> Level -> Bool
compare :: Level -> Level -> Ordering
$ccompare :: Level -> Level -> Ordering
$cp1Ord :: Eq Level
Ord, Integer -> Level
Level -> Level
Level -> Level -> Level
(Level -> Level -> Level)
-> (Level -> Level -> Level)
-> (Level -> Level -> Level)
-> (Level -> Level)
-> (Level -> Level)
-> (Level -> Level)
-> (Integer -> Level)
-> Num Level
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
fromInteger :: Integer -> Level
$cfromInteger :: Integer -> Level
signum :: Level -> Level
$csignum :: Level -> Level
abs :: Level -> Level
$cabs :: Level -> Level
negate :: Level -> Level
$cnegate :: Level -> Level
* :: Level -> Level -> Level
$c* :: Level -> Level -> Level
- :: Level -> Level -> Level
$c- :: Level -> Level -> Level
+ :: Level -> Level -> Level
$c+ :: Level -> Level -> Level
Num, Num Level
Ord Level
Num Level -> Ord Level -> (Level -> Rational) -> Real Level
Level -> Rational
forall a. Num a -> Ord a -> (a -> Rational) -> Real a
toRational :: Level -> Rational
$ctoRational :: Level -> Rational
$cp2Real :: Ord Level
$cp1Real :: Num Level
Real, Int -> Level
Level -> Int
Level -> [Level]
Level -> Level
Level -> Level -> [Level]
Level -> Level -> Level -> [Level]
(Level -> Level)
-> (Level -> Level)
-> (Int -> Level)
-> (Level -> Int)
-> (Level -> [Level])
-> (Level -> Level -> [Level])
-> (Level -> Level -> [Level])
-> (Level -> Level -> Level -> [Level])
-> Enum Level
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: Level -> Level -> Level -> [Level]
$cenumFromThenTo :: Level -> Level -> Level -> [Level]
enumFromTo :: Level -> Level -> [Level]
$cenumFromTo :: Level -> Level -> [Level]
enumFromThen :: Level -> Level -> [Level]
$cenumFromThen :: Level -> Level -> [Level]
enumFrom :: Level -> [Level]
$cenumFrom :: Level -> [Level]
fromEnum :: Level -> Int
$cfromEnum :: Level -> Int
toEnum :: Int -> Level
$ctoEnum :: Int -> Level
pred :: Level -> Level
$cpred :: Level -> Level
succ :: Level -> Level
$csucc :: Level -> Level
Enum, Enum Level
Real Level
Real Level
-> Enum Level
-> (Level -> Level -> Level)
-> (Level -> Level -> Level)
-> (Level -> Level -> Level)
-> (Level -> Level -> Level)
-> (Level -> Level -> (Level, Level))
-> (Level -> Level -> (Level, Level))
-> (Level -> Integer)
-> Integral Level
Level -> Integer
Level -> Level -> (Level, Level)
Level -> Level -> Level
forall a.
Real a
-> Enum a
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> (a, a))
-> (a -> a -> (a, a))
-> (a -> Integer)
-> Integral a
toInteger :: Level -> Integer
$ctoInteger :: Level -> Integer
divMod :: Level -> Level -> (Level, Level)
$cdivMod :: Level -> Level -> (Level, Level)
quotRem :: Level -> Level -> (Level, Level)
$cquotRem :: Level -> Level -> (Level, Level)
mod :: Level -> Level -> Level
$cmod :: Level -> Level -> Level
div :: Level -> Level -> Level
$cdiv :: Level -> Level -> Level
rem :: Level -> Level -> Level
$crem :: Level -> Level -> Level
quot :: Level -> Level -> Level
$cquot :: Level -> Level -> Level
$cp2Integral :: Enum Level
$cp1Integral :: Real Level
Integral)

-- | During visiting the AST we hold a reader "state" of current level and a current scoping (levelMapping).
-- Invariant-A: the current level is positive and greater than all levels in the levelMapping.
-- Invariant-B: only positive levels are stored in the levelMapping.
data Levels = Levels
            { Levels -> Level
currentLevel :: Level
            , Levels -> Bimap Unique Level
levelMapping :: BM.Bimap Unique Level
            }

-- | Declare a name with a unique, recording the mapping to a 'Level'.
declareUnique :: (MonadReader Levels m, HasUnique name unique) => name -> m a -> m a
declareUnique :: name -> m a -> m a
declareUnique name
n =
    (Levels -> Levels) -> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((Levels -> Levels) -> m a -> m a)
-> (Levels -> Levels) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ \(Levels Level
current Bimap Unique Level
ls) -> Level -> Bimap Unique Level -> Levels
Levels Level
current (Bimap Unique Level -> Levels) -> Bimap Unique Level -> Levels
forall a b. (a -> b) -> a -> b
$ Unique -> Level -> Bimap Unique Level -> Bimap Unique Level
forall a b. (Ord a, Ord b) => a -> b -> Bimap a b -> Bimap a b
BM.insert (name
n name -> Getting Unique name Unique -> Unique
forall s a. s -> Getting a s a -> a
^. Getting Unique name Unique
forall name unique. HasUnique name unique => Lens' name Unique
theUnique) Level
current Bimap Unique Level
ls

{-| Declares a new binder by assigning a fresh unique to the *current level*.
Maintains invariant-B of 'Levels' (that only positive levels are stored),
since current level is always positive (invariant-A).
See NOTE: [DeBruijn indices of Binders]
-}
declareBinder :: (MonadReader Levels m, MonadQuote m) => m a -> m a
declareBinder :: m a -> m a
declareBinder m a
act = do
    Unique
newU <- m Unique
forall (m :: * -> *). MonadQuote m => m Unique
freshUnique
    (Levels -> Levels) -> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\(Levels Level
current Bimap Unique Level
ls) -> Level -> Bimap Unique Level -> Levels
Levels Level
current (Bimap Unique Level -> Levels) -> Bimap Unique Level -> Levels
forall a b. (a -> b) -> a -> b
$ Unique -> Level -> Bimap Unique Level -> Bimap Unique Level
forall a b. (Ord a, Ord b) => a -> b -> Bimap a b -> Bimap a b
BM.insert Unique
newU Level
current Bimap Unique Level
ls) m a
act

-- | Enter a scope, incrementing the current 'Level' by one
-- Maintains invariant-A (that the current level is positive).
withScope :: MonadReader Levels m => m a -> m a
withScope :: m a -> m a
withScope = (Levels -> Levels) -> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((Levels -> Levels) -> m a -> m a)
-> (Levels -> Levels) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ \(Levels Level
current Bimap Unique Level
ls) -> Level -> Bimap Unique Level -> Levels
Levels (Level
currentLevel -> Level -> Level
forall a. Num a => a -> a -> a
+Level
1) Bimap Unique Level
ls

-- | We cannot do a correct translation to or from de Bruijn indices if the program is not well-scoped.
-- So we throw an error in such a case.
data FreeVariableError
    = FreeUnique Unique
    | FreeIndex Index
    deriving stock (Int -> FreeVariableError -> ShowS
[FreeVariableError] -> ShowS
FreeVariableError -> String
(Int -> FreeVariableError -> ShowS)
-> (FreeVariableError -> String)
-> ([FreeVariableError] -> ShowS)
-> Show FreeVariableError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FreeVariableError] -> ShowS
$cshowList :: [FreeVariableError] -> ShowS
show :: FreeVariableError -> String
$cshow :: FreeVariableError -> String
showsPrec :: Int -> FreeVariableError -> ShowS
$cshowsPrec :: Int -> FreeVariableError -> ShowS
Show, FreeVariableError -> FreeVariableError -> Bool
(FreeVariableError -> FreeVariableError -> Bool)
-> (FreeVariableError -> FreeVariableError -> Bool)
-> Eq FreeVariableError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FreeVariableError -> FreeVariableError -> Bool
$c/= :: FreeVariableError -> FreeVariableError -> Bool
== :: FreeVariableError -> FreeVariableError -> Bool
$c== :: FreeVariableError -> FreeVariableError -> Bool
Eq, Eq FreeVariableError
Eq FreeVariableError
-> (FreeVariableError -> FreeVariableError -> Ordering)
-> (FreeVariableError -> FreeVariableError -> Bool)
-> (FreeVariableError -> FreeVariableError -> Bool)
-> (FreeVariableError -> FreeVariableError -> Bool)
-> (FreeVariableError -> FreeVariableError -> Bool)
-> (FreeVariableError -> FreeVariableError -> FreeVariableError)
-> (FreeVariableError -> FreeVariableError -> FreeVariableError)
-> Ord FreeVariableError
FreeVariableError -> FreeVariableError -> Bool
FreeVariableError -> FreeVariableError -> Ordering
FreeVariableError -> FreeVariableError -> FreeVariableError
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
min :: FreeVariableError -> FreeVariableError -> FreeVariableError
$cmin :: FreeVariableError -> FreeVariableError -> FreeVariableError
max :: FreeVariableError -> FreeVariableError -> FreeVariableError
$cmax :: FreeVariableError -> FreeVariableError -> FreeVariableError
>= :: FreeVariableError -> FreeVariableError -> Bool
$c>= :: FreeVariableError -> FreeVariableError -> Bool
> :: FreeVariableError -> FreeVariableError -> Bool
$c> :: FreeVariableError -> FreeVariableError -> Bool
<= :: FreeVariableError -> FreeVariableError -> Bool
$c<= :: FreeVariableError -> FreeVariableError -> Bool
< :: FreeVariableError -> FreeVariableError -> Bool
$c< :: FreeVariableError -> FreeVariableError -> Bool
compare :: FreeVariableError -> FreeVariableError -> Ordering
$ccompare :: FreeVariableError -> FreeVariableError -> Ordering
$cp1Ord :: Eq FreeVariableError
Ord, (forall x. FreeVariableError -> Rep FreeVariableError x)
-> (forall x. Rep FreeVariableError x -> FreeVariableError)
-> Generic FreeVariableError
forall x. Rep FreeVariableError x -> FreeVariableError
forall x. FreeVariableError -> Rep FreeVariableError x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep FreeVariableError x -> FreeVariableError
$cfrom :: forall x. FreeVariableError -> Rep FreeVariableError x
Generic)
    deriving anyclass (Show FreeVariableError
Typeable FreeVariableError
Typeable FreeVariableError
-> Show FreeVariableError
-> (FreeVariableError -> SomeException)
-> (SomeException -> Maybe FreeVariableError)
-> (FreeVariableError -> String)
-> Exception FreeVariableError
SomeException -> Maybe FreeVariableError
FreeVariableError -> String
FreeVariableError -> SomeException
forall e.
Typeable e
-> Show e
-> (e -> SomeException)
-> (SomeException -> Maybe e)
-> (e -> String)
-> Exception e
displayException :: FreeVariableError -> String
$cdisplayException :: FreeVariableError -> String
fromException :: SomeException -> Maybe FreeVariableError
$cfromException :: SomeException -> Maybe FreeVariableError
toException :: FreeVariableError -> SomeException
$ctoException :: FreeVariableError -> SomeException
$cp2Exception :: Show FreeVariableError
$cp1Exception :: Typeable FreeVariableError
Exception, FreeVariableError -> ()
(FreeVariableError -> ()) -> NFData FreeVariableError
forall a. (a -> ()) -> NFData a
rnf :: FreeVariableError -> ()
$crnf :: FreeVariableError -> ()
NFData)

instance Pretty FreeVariableError where
    pretty :: FreeVariableError -> Doc ann
pretty (FreeUnique Unique
u) = Doc ann
"Free unique:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Unique -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Unique
u
    pretty (FreeIndex Index
i)  = Doc ann
"Free index:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Index -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Index
i
makeClassyPrisms ''FreeVariableError

instance HasErrorCode FreeVariableError where
    errorCode :: FreeVariableError -> ErrorCode
errorCode  FreeIndex {}  = Natural -> ErrorCode
ErrorCode Natural
23
    errorCode  FreeUnique {} = Natural -> ErrorCode
ErrorCode Natural
22

-- | Get the 'Index' corresponding to a given 'Unique'.
-- Uses supplied handler for free names (uniques).
getIndex :: MonadReader Levels m => Unique -> (Unique -> m Index) -> m Index
getIndex :: Unique -> (Unique -> m Index) -> m Index
getIndex Unique
u Unique -> m Index
h = do
    Levels Level
current Bimap Unique Level
ls <- m Levels
forall r (m :: * -> *). MonadReader r m => m r
ask
    case Unique -> Bimap Unique Level -> Maybe Level
forall a b (m :: * -> *).
(Ord a, Ord b, MonadThrow m) =>
a -> Bimap a b -> m b
BM.lookup Unique
u Bimap Unique Level
ls of
        Just Level
foundlvl -> Index -> m Index
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Index -> m Index) -> Index -> m Index
forall a b. (a -> b) -> a -> b
$ Level -> Level -> Index
levelToIx Level
current Level
foundlvl
        -- This call should return an index greater than the current level,
        -- otherwise it will map unbound variables to bound variables.
        Maybe Level
Nothing       ->  Unique -> m Index
h Unique
u
  where
    -- Compute the relative 'Index' of a absolute 'Level' relative to the current 'Level'.
    levelToIx :: Level -> Level -> Index
    levelToIx :: Level -> Level -> Index
levelToIx (Level Integer
current) (Level Integer
foundLvl) =
        -- Thanks to invariant-A, we can be sure that 'level >= foundLvl ', since foundLvl is in the levelMapping
        -- and thus the computation 'current-foundLvl' is '>=0' and its conversion to Natural will not lead to arithmetic underflow.
        Integer -> Index
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Index) -> Integer -> Index
forall a b. (a -> b) -> a -> b
$ Integer
current Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
foundLvl

-- | Get the 'Unique' corresponding to a given 'Index'.
-- Uses supplied handler for free debruijn indices.
getUnique :: MonadReader Levels m => Index -> (Index -> m Unique) -> m Unique
getUnique :: Index -> (Index -> m Unique) -> m Unique
getUnique Index
ix Index -> m Unique
h = do
    Levels Level
current Bimap Unique Level
ls <- m Levels
forall r (m :: * -> *). MonadReader r m => m r
ask
    case Level -> Bimap Unique Level -> Maybe Unique
forall a b (m :: * -> *).
(Ord a, Ord b, MonadThrow m) =>
b -> Bimap a b -> m a
BM.lookupR (Level -> Index -> Level
ixToLevel Level
current Index
ix) Bimap Unique Level
ls of
        -- Because of invariant-B, the levelMapping contains only positive (absolute) levels.
        Just Unique
u  -> Unique -> m Unique
forall (f :: * -> *) a. Applicative f => a -> f a
pure Unique
u
        -- This call should return a free/unbound unique,
        -- otherwise it will map unbound variables to bound variables.
        Maybe Unique
Nothing ->
            -- the lookup failed, meaning the index corresponds to a strictly-negative (absolute) level.
            Index -> m Unique
h Index
ix

unNameDeBruijn
    :: NamedDeBruijn -> DeBruijn
unNameDeBruijn :: NamedDeBruijn -> DeBruijn
unNameDeBruijn (NamedDeBruijn Text
_ Index
ix) = Index -> DeBruijn
DeBruijn Index
ix

unNameTyDeBruijn
    :: NamedTyDeBruijn -> TyDeBruijn
unNameTyDeBruijn :: NamedTyDeBruijn -> TyDeBruijn
unNameTyDeBruijn (NamedTyDeBruijn NamedDeBruijn
db) = DeBruijn -> TyDeBruijn
TyDeBruijn (DeBruijn -> TyDeBruijn) -> DeBruijn -> TyDeBruijn
forall a b. (a -> b) -> a -> b
$ NamedDeBruijn -> DeBruijn
unNameDeBruijn NamedDeBruijn
db

fakeNameDeBruijn :: DeBruijn -> NamedDeBruijn
fakeNameDeBruijn :: DeBruijn -> NamedDeBruijn
fakeNameDeBruijn = FakeNamedDeBruijn -> NamedDeBruijn
coerce (FakeNamedDeBruijn -> NamedDeBruijn)
-> (DeBruijn -> FakeNamedDeBruijn) -> DeBruijn -> NamedDeBruijn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DeBruijn -> FakeNamedDeBruijn
toFake

nameToDeBruijn
    :: MonadReader Levels m
    => (Unique -> m Index)
    -> Name
    -> m NamedDeBruijn
nameToDeBruijn :: (Unique -> m Index) -> Name -> m NamedDeBruijn
nameToDeBruijn Unique -> m Index
h (Name Text
str Unique
u) = Text -> Index -> NamedDeBruijn
NamedDeBruijn Text
str (Index -> NamedDeBruijn) -> m Index -> m NamedDeBruijn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Unique -> (Unique -> m Index) -> m Index
forall (m :: * -> *).
MonadReader Levels m =>
Unique -> (Unique -> m Index) -> m Index
getIndex Unique
u Unique -> m Index
h

tyNameToDeBruijn
    :: MonadReader Levels m
    => (Unique -> m Index)
    -> TyName
    -> m NamedTyDeBruijn
tyNameToDeBruijn :: (Unique -> m Index) -> TyName -> m NamedTyDeBruijn
tyNameToDeBruijn Unique -> m Index
h (TyName Name
n) = NamedDeBruijn -> NamedTyDeBruijn
NamedTyDeBruijn (NamedDeBruijn -> NamedTyDeBruijn)
-> m NamedDeBruijn -> m NamedTyDeBruijn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Unique -> m Index) -> Name -> m NamedDeBruijn
forall (m :: * -> *).
MonadReader Levels m =>
(Unique -> m Index) -> Name -> m NamedDeBruijn
nameToDeBruijn Unique -> m Index
h Name
n

deBruijnToName
    :: MonadReader Levels m
    => (Index -> m Unique)
    -> NamedDeBruijn
    -> m Name
deBruijnToName :: (Index -> m Unique) -> NamedDeBruijn -> m Name
deBruijnToName Index -> m Unique
h (NamedDeBruijn Text
str Index
ix) = Text -> Unique -> Name
Name Text
str (Unique -> Name) -> m Unique -> m Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Index -> (Index -> m Unique) -> m Unique
forall (m :: * -> *).
MonadReader Levels m =>
Index -> (Index -> m Unique) -> m Unique
getUnique Index
ix Index -> m Unique
h

deBruijnToTyName
    :: MonadReader Levels m
    => (Index -> m Unique)
    -> NamedTyDeBruijn
    -> m TyName
deBruijnToTyName :: (Index -> m Unique) -> NamedTyDeBruijn -> m TyName
deBruijnToTyName Index -> m Unique
h (NamedTyDeBruijn NamedDeBruijn
n) = Name -> TyName
TyName (Name -> TyName) -> m Name -> m TyName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Index -> m Unique) -> NamedDeBruijn -> m Name
forall (m :: * -> *).
MonadReader Levels m =>
(Index -> m Unique) -> NamedDeBruijn -> m Name
deBruijnToName Index -> m Unique
h NamedDeBruijn
n

-- | The default handler of throwing an error upon encountering a free name (unique).
freeUniqueThrow :: (AsFreeVariableError e, MonadError e m) => Unique -> m Index
freeUniqueThrow :: Unique -> m Index
freeUniqueThrow =
    AReview e FreeVariableError -> FreeVariableError -> m Index
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview e FreeVariableError
forall r. AsFreeVariableError r => Prism' r FreeVariableError
_FreeVariableError (FreeVariableError -> m Index)
-> (Unique -> FreeVariableError) -> Unique -> m Index
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Unique -> FreeVariableError
FreeUnique

-- | The default handler of throwing an error upon encountering a free debruijn index.
freeIndexThrow :: (AsFreeVariableError e, MonadError e m) => Index -> m Unique
freeIndexThrow :: Index -> m Unique
freeIndexThrow =
    AReview e FreeVariableError -> FreeVariableError -> m Unique
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview e FreeVariableError
forall r. AsFreeVariableError r => Prism' r FreeVariableError
_FreeVariableError (FreeVariableError -> m Unique)
-> (Index -> FreeVariableError) -> Index -> m Unique
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index -> FreeVariableError
FreeIndex

{-| A different implementation of a handler,  where "free" debruijn indices do not throw an error
but are instead gracefully converted to fresh uniques.
These generated uniques remain free; i.e.  if the original term was open, it will remain open after applying this handler.
These generated free uniques are consistent across the open term (by using a state cache).
-}
freeIndexAsConsistentLevel :: (MonadReader Levels m, MonadState (M.Map Level Unique) m, MonadQuote m) => Index -> m Unique
freeIndexAsConsistentLevel :: Index -> m Unique
freeIndexAsConsistentLevel Index
ix = do
    Map Level Unique
cache <- m (Map Level Unique)
forall s (m :: * -> *). MonadState s m => m s
get
    Levels Level
current Bimap Unique Level
_ <- m Levels
forall r (m :: * -> *). MonadReader r m => m r
ask
    -- the absolute level is strictly-negative
    let absoluteLevel :: Level
absoluteLevel =  Level -> Index -> Level
ixToLevel Level
current Index
ix
    case Level -> Map Level Unique -> Maybe Unique
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Level
absoluteLevel Map Level Unique
cache of
        Maybe Unique
Nothing -> do
            Unique
u <- m Unique
forall (m :: * -> *). MonadQuote m => m Unique
freshUnique
            -- the cache contains only strictly-negative levels
            Map Level Unique -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Level -> Unique -> Map Level Unique -> Map Level Unique
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Level
absoluteLevel Unique
u Map Level Unique
cache)
            Unique -> m Unique
forall (f :: * -> *) a. Applicative f => a -> f a
pure Unique
u
        Just Unique
u -> Unique -> m Unique
forall (f :: * -> *) a. Applicative f => a -> f a
pure Unique
u

-- Compute the absolute 'Level' of a relative 'Index' relative to the current 'Level'.
-- The index `ixAST` may be malformed or point to a free variable because it comes straight from the AST;
-- in such a case, this function may return a negative level.
ixToLevel :: Level -> Index -> Level
ixToLevel :: Level -> Index -> Level
ixToLevel (Level Integer
current) Index
ixAST = Integer -> Level
Level (Integer -> Level) -> Integer -> Level
forall a b. (a -> b) -> a -> b
$ Integer
current Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Index -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Index
ixAST

runDeBruijnT :: ReaderT Levels m a -> m a
runDeBruijnT :: ReaderT Levels m a -> m a
runDeBruijnT = (ReaderT Levels m a -> Levels -> m a)
-> Levels -> ReaderT Levels m a -> m a
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT Levels m a -> Levels -> m a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (Level -> Bimap Unique Level -> Levels
Levels (Integer -> Level
Level (Integer -> Level) -> Integer -> Level
forall a b. (a -> b) -> a -> b
$ Index -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Index
deBruijnInitIndex) Bimap Unique Level
forall a b. Bimap a b
BM.empty)