{-# LANGUAGE DeriveAnyClass        #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE TemplateHaskell       #-}
-- This fires on GHC-9.2.4 for some reason, not entirely sure
-- what's going on
{-# OPTIONS_GHC -Wno-identities #-}

-- | Support for using de Bruijn indices for term and type names.
module PlutusCore.DeBruijn.Internal
  ( Index (..)
  , HasIndex (..)
  , DeBruijn (..)
  , NamedDeBruijn (..)
  -- we follow the same approach as Renamed: expose the constructor from Internal module,
  -- but hide it in the parent module.
  , FakeNamedDeBruijn (..)
  , TyDeBruijn (..)
  , NamedTyDeBruijn (..)
  , FreeVariableError (..)
  , AsFreeVariableError (..)
  , Level (..)
  , LevelInfo (..)
  , declareUnique
  , declareBinder
  , withScope
  , getIndex
  , getUnique
  , unNameDeBruijn
  , unNameTyDeBruijn
  , fakeNameDeBruijn
  , fakeTyNameDeBruijn
  , nameToDeBruijn
  , tyNameToDeBruijn
  , deBruijnToName
  , deBruijnToTyName
  , freeIndexThrow
  , freeIndexAsConsistentLevel
  , freeUniqueThrow
  , runDeBruijnT
  , deBruijnInitIndex
  , toFake
  , fromFake
  ) where

import PlutusCore.Name.Unique
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.Hashable
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 GHC.Generics

{- Note [Why newtype FakeNamedDeBruijn]
We use a newtype wrapper to optimize away the expensive re-traversing of the deserialized Term
for adding fake names everywhere --- the CEK works on names, but the scripts on ledger
don't have names for size reduction.

Specifically the expensive pipeline:

```
decode @(Term DeBruijn)
>>> term-Map-Names(FakeNamedDeBruijn)
>>> cekExecute
```

is optimized to to the faster:

```
decode @(Term FakeNamedDeBruijn)
>>> coerce @(Term FakeNamedDeBruijn) @(Term NamedDeBruijn)
>>> cekExecute
```

To achieve this we make sure:
- to use `coerce` since its 0-cost
- not to GeneralizeNewtypeDeriving the`Flat FakeNamedDeBruijn` instance, but "derive via"
the optimized `Flat DeBruijn` instance. This is ok, because `FND<->D` are
isomorphic.
-}

{- | A relative index used for de Bruijn identifiers.

FIXME: downside of using newtype+Num instead of type-synonym is that `-Woverflowed-literals`
does not work, e.g.: `DeBruijn (-1)` has no warning. To trigger the warning you have to bypass
the Num and write `DeBruijn (Index -1)`. This can be revisited when we implement PLT-1053.
-}
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
$cfrom :: forall x. Index -> Rep Index x
from :: forall x. Index -> Rep Index x
$cto :: forall x. Rep Index x -> Index
to :: forall x. Rep Index x -> Index
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
$cshowsPrec :: Int -> Index -> ShowS
showsPrec :: Int -> Index -> ShowS
$cshow :: Index -> String
show :: Index -> String
$cshowList :: [Index] -> ShowS
showList :: [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
$c+ :: Index -> Index -> Index
+ :: Index -> Index -> Index
$c- :: Index -> Index -> Index
- :: Index -> Index -> Index
$c* :: Index -> Index -> Index
* :: Index -> Index -> Index
$cnegate :: Index -> Index
negate :: Index -> Index
$cabs :: Index -> Index
abs :: Index -> Index
$csignum :: Index -> Index
signum :: Index -> Index
$cfromInteger :: Integer -> Index
fromInteger :: Integer -> 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
$csucc :: Index -> Index
succ :: Index -> Index
$cpred :: Index -> Index
pred :: Index -> Index
$ctoEnum :: Int -> Index
toEnum :: Int -> Index
$cfromEnum :: Index -> Int
fromEnum :: Index -> Int
$cenumFrom :: Index -> [Index]
enumFrom :: Index -> [Index]
$cenumFromThen :: Index -> Index -> [Index]
enumFromThen :: Index -> Index -> [Index]
$cenumFromTo :: Index -> Index -> [Index]
enumFromTo :: Index -> Index -> [Index]
$cenumFromThenTo :: Index -> Index -> Index -> [Index]
enumFromThenTo :: Index -> Index -> 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
$ctoRational :: Index -> Rational
toRational :: Index -> Rational
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
$cquot :: Index -> Index -> Index
quot :: Index -> Index -> Index
$crem :: Index -> Index -> Index
rem :: Index -> Index -> Index
$cdiv :: Index -> Index -> Index
div :: Index -> Index -> Index
$cmod :: Index -> Index -> Index
mod :: Index -> Index -> Index
$cquotRem :: Index -> Index -> (Index, Index)
quotRem :: Index -> Index -> (Index, Index)
$cdivMod :: Index -> Index -> (Index, Index)
divMod :: Index -> Index -> (Index, Index)
$ctoInteger :: Index -> Integer
toInteger :: Index -> Integer
Integral, Index -> Index -> Bool
(Index -> Index -> Bool) -> (Index -> Index -> Bool) -> Eq Index
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Index -> Index -> Bool
== :: Index -> Index -> Bool
$c/= :: Index -> Index -> Bool
/= :: 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
$ccompare :: Index -> Index -> Ordering
compare :: Index -> Index -> Ordering
$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
>= :: Index -> Index -> Bool
$cmax :: Index -> Index -> Index
max :: Index -> Index -> Index
$cmin :: Index -> Index -> Index
min :: Index -> Index -> Index
Ord, Eq Index
Eq Index =>
(Int -> Index -> Int) -> (Index -> Int) -> Hashable Index
Int -> Index -> Int
Index -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: Int -> Index -> Int
hashWithSalt :: Int -> Index -> Int
$chash :: Index -> Int
hash :: Index -> Int
Hashable, (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
$cpretty :: forall ann. Index -> Doc ann
pretty :: forall ann. Index -> Doc ann
$cprettyList :: forall ann. [Index] -> Doc ann
prettyList :: forall ann. [Index] -> Doc ann
Pretty, Index -> ()
(Index -> ()) -> NFData Index
forall a. (a -> ()) -> NFData a
$crnf :: Index -> ()
rnf :: Index -> ()
NFData, ReadPrec [Index]
ReadPrec Index
Int -> ReadS Index
ReadS [Index]
(Int -> ReadS Index)
-> ReadS [Index]
-> ReadPrec Index
-> ReadPrec [Index]
-> Read Index
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS Index
readsPrec :: Int -> ReadS Index
$creadList :: ReadS [Index]
readList :: ReadS [Index]
$creadPrec :: ReadPrec Index
readPrec :: ReadPrec Index
$creadListPrec :: ReadPrec [Index]
readListPrec :: ReadPrec [Index]
Read)

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

-- The bangs gave us a speedup of 6%.

-- | 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
$cshowsPrec :: Int -> NamedDeBruijn -> ShowS
showsPrec :: Int -> NamedDeBruijn -> ShowS
$cshow :: NamedDeBruijn -> String
show :: NamedDeBruijn -> String
$cshowList :: [NamedDeBruijn] -> ShowS
showList :: [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
$cfrom :: forall x. NamedDeBruijn -> Rep NamedDeBruijn x
from :: forall x. NamedDeBruijn -> Rep NamedDeBruijn x
$cto :: forall x. Rep NamedDeBruijn x -> NamedDeBruijn
to :: forall x. Rep NamedDeBruijn x -> NamedDeBruijn
Generic, ReadPrec [NamedDeBruijn]
ReadPrec NamedDeBruijn
Int -> ReadS NamedDeBruijn
ReadS [NamedDeBruijn]
(Int -> ReadS NamedDeBruijn)
-> ReadS [NamedDeBruijn]
-> ReadPrec NamedDeBruijn
-> ReadPrec [NamedDeBruijn]
-> Read NamedDeBruijn
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS NamedDeBruijn
readsPrec :: Int -> ReadS NamedDeBruijn
$creadList :: ReadS [NamedDeBruijn]
readList :: ReadS [NamedDeBruijn]
$creadPrec :: ReadPrec NamedDeBruijn
readPrec :: ReadPrec NamedDeBruijn
$creadListPrec :: ReadPrec [NamedDeBruijn]
readListPrec :: ReadPrec [NamedDeBruijn]
Read)
  deriving anyclass (Eq NamedDeBruijn
Eq NamedDeBruijn =>
(Int -> NamedDeBruijn -> Int)
-> (NamedDeBruijn -> Int) -> Hashable NamedDeBruijn
Int -> NamedDeBruijn -> Int
NamedDeBruijn -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: Int -> NamedDeBruijn -> Int
hashWithSalt :: Int -> NamedDeBruijn -> Int
$chash :: NamedDeBruijn -> Int
hash :: NamedDeBruijn -> Int
Hashable, NamedDeBruijn -> ()
(NamedDeBruijn -> ()) -> NFData NamedDeBruijn
forall a. (a -> ()) -> NFData a
$crnf :: NamedDeBruijn -> ()
rnf :: NamedDeBruijn -> ()
NFData)

{- | A wrapper around `NamedDeBruijn` that *must* hold the invariant of name=`fakeName`.

We do not export the `FakeNamedDeBruijn` constructor: the projection `FND->ND` is safe
but injection `ND->FND` is unsafe, thus they are not isomorphic.

See Note [Why newtype FakeNamedDeBruijn]
-}
newtype FakeNamedDeBruijn = FakeNamedDeBruijn {FakeNamedDeBruijn -> NamedDeBruijn
unFakeNamedDeBruijn :: 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
$cshowsPrec :: Int -> FakeNamedDeBruijn -> ShowS
showsPrec :: Int -> FakeNamedDeBruijn -> ShowS
$cshow :: FakeNamedDeBruijn -> String
show :: FakeNamedDeBruijn -> String
$cshowList :: [FakeNamedDeBruijn] -> ShowS
showList :: [FakeNamedDeBruijn] -> ShowS
Show, FakeNamedDeBruijn -> FakeNamedDeBruijn -> Bool
(FakeNamedDeBruijn -> FakeNamedDeBruijn -> Bool)
-> (FakeNamedDeBruijn -> FakeNamedDeBruijn -> Bool)
-> Eq FakeNamedDeBruijn
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FakeNamedDeBruijn -> FakeNamedDeBruijn -> Bool
== :: FakeNamedDeBruijn -> FakeNamedDeBruijn -> Bool
$c/= :: FakeNamedDeBruijn -> FakeNamedDeBruijn -> Bool
/= :: FakeNamedDeBruijn -> FakeNamedDeBruijn -> Bool
Eq, Eq FakeNamedDeBruijn
Eq FakeNamedDeBruijn =>
(Int -> FakeNamedDeBruijn -> Int)
-> (FakeNamedDeBruijn -> Int) -> Hashable FakeNamedDeBruijn
Int -> FakeNamedDeBruijn -> Int
FakeNamedDeBruijn -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: Int -> FakeNamedDeBruijn -> Int
hashWithSalt :: Int -> FakeNamedDeBruijn -> Int
$chash :: FakeNamedDeBruijn -> Int
hash :: FakeNamedDeBruijn -> Int
Hashable, FakeNamedDeBruijn -> ()
(FakeNamedDeBruijn -> ()) -> NFData FakeNamedDeBruijn
forall a. (a -> ()) -> NFData a
$crnf :: FakeNamedDeBruijn -> ()
rnf :: 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
$cshowsPrec :: Int -> DeBruijn -> ShowS
showsPrec :: Int -> DeBruijn -> ShowS
$cshow :: DeBruijn -> String
show :: DeBruijn -> String
$cshowList :: [DeBruijn] -> ShowS
showList :: [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
$cfrom :: forall x. DeBruijn -> Rep DeBruijn x
from :: forall x. DeBruijn -> Rep DeBruijn x
$cto :: forall x. Rep DeBruijn x -> DeBruijn
to :: forall x. Rep DeBruijn x -> DeBruijn
Generic, DeBruijn -> DeBruijn -> Bool
(DeBruijn -> DeBruijn -> Bool)
-> (DeBruijn -> DeBruijn -> Bool) -> Eq DeBruijn
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DeBruijn -> DeBruijn -> Bool
== :: DeBruijn -> DeBruijn -> Bool
$c/= :: DeBruijn -> DeBruijn -> Bool
/= :: DeBruijn -> DeBruijn -> Bool
Eq)
  deriving newtype (Eq DeBruijn
Eq DeBruijn =>
(Int -> DeBruijn -> Int) -> (DeBruijn -> Int) -> Hashable DeBruijn
Int -> DeBruijn -> Int
DeBruijn -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: Int -> DeBruijn -> Int
hashWithSalt :: Int -> DeBruijn -> Int
$chash :: DeBruijn -> Int
hash :: DeBruijn -> Int
Hashable, DeBruijn -> ()
(DeBruijn -> ()) -> NFData DeBruijn
forall a. (a -> ()) -> NFData a
$crnf :: DeBruijn -> ()
rnf :: 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
$cshowsPrec :: Int -> NamedTyDeBruijn -> ShowS
showsPrec :: Int -> NamedTyDeBruijn -> ShowS
$cshow :: NamedTyDeBruijn -> String
show :: NamedTyDeBruijn -> String
$cshowList :: [NamedTyDeBruijn] -> ShowS
showList :: [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
$cfrom :: forall x. NamedTyDeBruijn -> Rep NamedTyDeBruijn x
from :: forall x. NamedTyDeBruijn -> Rep NamedTyDeBruijn x
$cto :: forall x. Rep NamedTyDeBruijn x -> NamedTyDeBruijn
to :: forall x. Rep NamedTyDeBruijn x -> NamedTyDeBruijn
Generic)
  deriving newtype (PrettyBy config, NamedTyDeBruijn -> ()
(NamedTyDeBruijn -> ()) -> NFData NamedTyDeBruijn
forall a. (a -> ()) -> NFData a
$crnf :: NamedTyDeBruijn -> ()
rnf :: 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
$c== :: NamedTyDeBruijn -> NamedTyDeBruijn -> Bool
== :: NamedTyDeBruijn -> NamedTyDeBruijn -> Bool
$c/= :: NamedTyDeBruijn -> NamedTyDeBruijn -> Bool
/= :: 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
$cshowsPrec :: Int -> TyDeBruijn -> ShowS
showsPrec :: Int -> TyDeBruijn -> ShowS
$cshow :: TyDeBruijn -> String
show :: TyDeBruijn -> String
$cshowList :: [TyDeBruijn] -> ShowS
showList :: [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
$cfrom :: forall x. TyDeBruijn -> Rep TyDeBruijn x
from :: forall x. TyDeBruijn -> Rep TyDeBruijn x
$cto :: forall x. Rep TyDeBruijn x -> TyDeBruijn
to :: forall x. Rep TyDeBruijn x -> TyDeBruijn
Generic)
  deriving newtype (TyDeBruijn -> ()
(TyDeBruijn -> ()) -> NFData TyDeBruijn
forall a. (a -> ()) -> NFData a
$crnf :: TyDeBruijn -> ()
rnf :: 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
$c== :: TyDeBruijn -> TyDeBruijn -> Bool
== :: TyDeBruijn -> TyDeBruijn -> Bool
$c/= :: TyDeBruijn -> TyDeBruijn -> Bool
/= :: TyDeBruijn -> TyDeBruijn -> Bool
Eq) via DeBruijn

instance Wrapped TyDeBruijn

instance (HasPrettyConfigName config) => PrettyBy config NamedDeBruijn where
  prettyBy :: forall ann. config -> NamedDeBruijn -> Doc ann
prettyBy config
config (NamedDeBruijn Text
txt (Index Word64
ix))
    | Bool
showsUnique = Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Text -> Doc ann) -> Text -> Doc ann
forall a b. (a -> b) -> a -> b
$ Text -> Text
toPrintedName Text
txt Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"!" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Doc Any -> Text
forall ann. Doc ann -> Text
forall str ann. Render str => Doc ann -> str
render (Word64 -> Doc Any
forall ann. Word64 -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Word64
ix)
    | Bool
otherwise = Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Text -> Doc ann) -> Text -> Doc ann
forall a b. (a -> b) -> a -> b
$ Text -> Text
toPrintedName 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 :: forall ann. config -> DeBruijn -> Doc ann
prettyBy config
config (DeBruijn (Index Word64
ix))
    | Bool
showsUnique = Doc ann
"!" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Word64 -> Doc ann
forall ann. 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 :: Lens' NamedDeBruijn Index
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 = i}

instance HasIndex DeBruijn where
  index :: Lens' DeBruijn Index
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 = i}

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

instance HasIndex TyDeBruijn where
  index :: Lens' TyDeBruijn Index
index = (Unwrapped TyDeBruijn -> f (Unwrapped TyDeBruijn))
-> TyDeBruijn -> f TyDeBruijn
forall s. Wrapped s => Iso' s (Unwrapped s)
Iso' TyDeBruijn (Unwrapped TyDeBruijn)
_Wrapped' ((Unwrapped TyDeBruijn -> f (Unwrapped TyDeBruijn))
 -> TyDeBruijn -> f TyDeBruijn)
-> ((Index -> f Index)
    -> Unwrapped TyDeBruijn -> f (Unwrapped TyDeBruijn))
-> (Index -> f Index)
-> TyDeBruijn
-> f TyDeBruijn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Index -> f Index)
-> Unwrapped TyDeBruijn -> f (Unwrapped TyDeBruijn)
forall a. HasIndex a => Lens' a Index
Lens' (Unwrapped TyDeBruijn) 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
$c== :: Level -> Level -> Bool
== :: Level -> Level -> Bool
$c/= :: Level -> Level -> Bool
/= :: 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
$ccompare :: Level -> Level -> Ordering
compare :: Level -> Level -> Ordering
$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
>= :: Level -> Level -> Bool
$cmax :: Level -> Level -> Level
max :: Level -> Level -> Level
$cmin :: Level -> Level -> Level
min :: Level -> Level -> 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
$c+ :: Level -> Level -> Level
+ :: Level -> Level -> Level
$c- :: Level -> Level -> Level
- :: Level -> Level -> Level
$c* :: Level -> Level -> Level
* :: Level -> Level -> Level
$cnegate :: Level -> Level
negate :: Level -> Level
$cabs :: Level -> Level
abs :: Level -> Level
$csignum :: Level -> Level
signum :: Level -> Level
$cfromInteger :: Integer -> Level
fromInteger :: Integer -> 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
$ctoRational :: Level -> Rational
toRational :: Level -> Rational
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
$csucc :: Level -> Level
succ :: Level -> Level
$cpred :: Level -> Level
pred :: Level -> Level
$ctoEnum :: Int -> Level
toEnum :: Int -> Level
$cfromEnum :: Level -> Int
fromEnum :: Level -> Int
$cenumFrom :: Level -> [Level]
enumFrom :: Level -> [Level]
$cenumFromThen :: Level -> Level -> [Level]
enumFromThen :: Level -> Level -> [Level]
$cenumFromTo :: Level -> Level -> [Level]
enumFromTo :: Level -> Level -> [Level]
$cenumFromThenTo :: Level -> Level -> Level -> [Level]
enumFromThenTo :: Level -> Level -> 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
$cquot :: Level -> Level -> Level
quot :: Level -> Level -> Level
$crem :: Level -> Level -> Level
rem :: Level -> Level -> Level
$cdiv :: Level -> Level -> Level
div :: Level -> Level -> Level
$cmod :: Level -> Level -> Level
mod :: Level -> Level -> Level
$cquotRem :: Level -> Level -> (Level, Level)
quotRem :: Level -> Level -> (Level, Level)
$cdivMod :: Level -> Level -> (Level, Level)
divMod :: Level -> Level -> (Level, Level)
$ctoInteger :: Level -> Integer
toInteger :: Level -> Integer
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 LevelInfo = LevelInfo
  { LevelInfo -> Level
currentLevel :: Level
  , LevelInfo -> Bimap Unique Level
levelMapping :: BM.Bimap Unique Level
  }

-- | Declare a name with a unique, recording the mapping to a 'Level'.
declareUnique :: (MonadReader LevelInfo m, HasUnique name unique) => name -> m a -> m a
declareUnique :: forall (m :: * -> *) name unique a.
(MonadReader LevelInfo m, HasUnique name unique) =>
name -> m a -> m a
declareUnique name
n =
  (LevelInfo -> LevelInfo) -> m a -> m a
forall a. (LevelInfo -> LevelInfo) -> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((LevelInfo -> LevelInfo) -> m a -> m a)
-> (LevelInfo -> LevelInfo) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ \(LevelInfo Level
current Bimap Unique Level
ls) -> Level -> Bimap Unique Level -> LevelInfo
LevelInfo Level
current (Bimap Unique Level -> LevelInfo)
-> Bimap Unique Level -> LevelInfo
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
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 'LevelInfo' (that only positive levels are stored),
since current level is always positive (invariant-A).
See Note [DeBruijn indices of Binders]
-}
declareBinder :: (MonadReader LevelInfo m, MonadQuote m) => m a -> m a
declareBinder :: forall (m :: * -> *) a.
(MonadReader LevelInfo m, MonadQuote m) =>
m a -> m a
declareBinder m a
act = do
  Unique
newU <- m Unique
forall (m :: * -> *). MonadQuote m => m Unique
freshUnique
  (LevelInfo -> LevelInfo) -> m a -> m a
forall a. (LevelInfo -> LevelInfo) -> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\(LevelInfo Level
current Bimap Unique Level
ls) -> Level -> Bimap Unique Level -> LevelInfo
LevelInfo Level
current (Bimap Unique Level -> LevelInfo)
-> Bimap Unique Level -> LevelInfo
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 LevelInfo m) => m a -> m a
withScope :: forall (m :: * -> *) a. MonadReader LevelInfo m => m a -> m a
withScope = (LevelInfo -> LevelInfo) -> m a -> m a
forall a. (LevelInfo -> LevelInfo) -> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((LevelInfo -> LevelInfo) -> m a -> m a)
-> (LevelInfo -> LevelInfo) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ \(LevelInfo Level
current Bimap Unique Level
ls) -> Level -> Bimap Unique Level -> LevelInfo
LevelInfo (Level
current Level -> 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
$cshowsPrec :: Int -> FreeVariableError -> ShowS
showsPrec :: Int -> FreeVariableError -> ShowS
$cshow :: FreeVariableError -> String
show :: FreeVariableError -> String
$cshowList :: [FreeVariableError] -> ShowS
showList :: [FreeVariableError] -> ShowS
Show, FreeVariableError -> FreeVariableError -> Bool
(FreeVariableError -> FreeVariableError -> Bool)
-> (FreeVariableError -> FreeVariableError -> Bool)
-> Eq FreeVariableError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FreeVariableError -> FreeVariableError -> Bool
== :: FreeVariableError -> FreeVariableError -> Bool
$c/= :: FreeVariableError -> FreeVariableError -> Bool
/= :: 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
$ccompare :: FreeVariableError -> FreeVariableError -> Ordering
compare :: FreeVariableError -> FreeVariableError -> Ordering
$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
>= :: FreeVariableError -> FreeVariableError -> Bool
$cmax :: FreeVariableError -> FreeVariableError -> FreeVariableError
max :: FreeVariableError -> FreeVariableError -> FreeVariableError
$cmin :: FreeVariableError -> FreeVariableError -> FreeVariableError
min :: FreeVariableError -> FreeVariableError -> 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
$cfrom :: forall x. FreeVariableError -> Rep FreeVariableError x
from :: forall x. FreeVariableError -> Rep FreeVariableError x
$cto :: forall x. Rep FreeVariableError x -> FreeVariableError
to :: forall x. Rep FreeVariableError x -> FreeVariableError
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
$ctoException :: FreeVariableError -> SomeException
toException :: FreeVariableError -> SomeException
$cfromException :: SomeException -> Maybe FreeVariableError
fromException :: SomeException -> Maybe FreeVariableError
$cdisplayException :: FreeVariableError -> String
displayException :: FreeVariableError -> String
Exception, FreeVariableError -> ()
(FreeVariableError -> ()) -> NFData FreeVariableError
forall a. (a -> ()) -> NFData a
$crnf :: FreeVariableError -> ()
rnf :: FreeVariableError -> ()
NFData)

instance Pretty FreeVariableError where
  pretty :: forall ann. 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
forall ann. Unique -> 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
forall ann. Index -> Doc ann
pretty Index
i
makeClassyPrisms ''FreeVariableError

{- | Get the 'Index' corresponding to a given 'Unique'.
Uses supplied handler for free names (uniques).
-}
getIndex :: (MonadReader LevelInfo m) => Unique -> (Unique -> m Index) -> m Index
getIndex :: forall (m :: * -> *).
MonadReader LevelInfo m =>
Unique -> (Unique -> m Index) -> m Index
getIndex Unique
u Unique -> m Index
h = do
  LevelInfo Level
current Bimap Unique Level
ls <- m LevelInfo
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 a. a -> m a
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 LevelInfo m) => Index -> (Index -> m Unique) -> m Unique
getUnique :: forall (m :: * -> *).
MonadReader LevelInfo m =>
Index -> (Index -> m Unique) -> m Unique
getUnique Index
ix Index -> m Unique
h = do
  LevelInfo Level
current Bimap Unique Level
ls <- m LevelInfo
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 a. a -> m a
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
forall a b. Coercible a b => a -> b
coerce (FakeNamedDeBruijn -> NamedDeBruijn)
-> (DeBruijn -> FakeNamedDeBruijn) -> DeBruijn -> NamedDeBruijn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DeBruijn -> FakeNamedDeBruijn
toFake

fakeTyNameDeBruijn :: TyDeBruijn -> NamedTyDeBruijn
fakeTyNameDeBruijn :: TyDeBruijn -> NamedTyDeBruijn
fakeTyNameDeBruijn (TyDeBruijn DeBruijn
n) = NamedDeBruijn -> NamedTyDeBruijn
NamedTyDeBruijn (NamedDeBruijn -> NamedTyDeBruijn)
-> NamedDeBruijn -> NamedTyDeBruijn
forall a b. (a -> b) -> a -> b
$ DeBruijn -> NamedDeBruijn
fakeNameDeBruijn DeBruijn
n

nameToDeBruijn
  :: (MonadReader LevelInfo m)
  => (Unique -> m Index)
  -> Name
  -> m NamedDeBruijn
nameToDeBruijn :: forall (m :: * -> *).
MonadReader LevelInfo m =>
(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 LevelInfo m =>
Unique -> (Unique -> m Index) -> m Index
getIndex Unique
u Unique -> m Index
h

tyNameToDeBruijn
  :: (MonadReader LevelInfo m)
  => (Unique -> m Index)
  -> TyName
  -> m NamedTyDeBruijn
tyNameToDeBruijn :: forall (m :: * -> *).
MonadReader LevelInfo m =>
(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 LevelInfo m =>
(Unique -> m Index) -> Name -> m NamedDeBruijn
nameToDeBruijn Unique -> m Index
h Name
n

deBruijnToName
  :: (MonadReader LevelInfo m)
  => (Index -> m Unique)
  -> NamedDeBruijn
  -> m Name
deBruijnToName :: forall (m :: * -> *).
MonadReader LevelInfo m =>
(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 LevelInfo m =>
Index -> (Index -> m Unique) -> m Unique
getUnique Index
ix Index -> m Unique
h

deBruijnToTyName
  :: (MonadReader LevelInfo m)
  => (Index -> m Unique)
  -> NamedTyDeBruijn
  -> m TyName
deBruijnToTyName :: forall (m :: * -> *).
MonadReader LevelInfo m =>
(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 LevelInfo 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 :: forall e (m :: * -> *).
(AsFreeVariableError e, MonadError e m) =>
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
Prism' e 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 :: forall e (m :: * -> *).
(AsFreeVariableError e, MonadError e m) =>
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
Prism' e 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 LevelInfo m, MonadState (M.Map Level Unique) m, MonadQuote m)
  => Index
  -> m Unique
freeIndexAsConsistentLevel :: forall (m :: * -> *).
(MonadReader LevelInfo m, MonadState (Map Level Unique) m,
 MonadQuote m) =>
Index -> m Unique
freeIndexAsConsistentLevel Index
ix = do
  Map Level Unique
cache <- m (Map Level Unique)
forall s (m :: * -> *). MonadState s m => m s
get
  LevelInfo Level
current Bimap Unique Level
_ <- m LevelInfo
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 a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Unique
u
    Just Unique
u -> Unique -> m Unique
forall a. a -> m a
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 LevelInfo m a -> m a
runDeBruijnT :: forall (m :: * -> *) a. ReaderT LevelInfo m a -> m a
runDeBruijnT = (ReaderT LevelInfo m a -> LevelInfo -> m a)
-> LevelInfo -> ReaderT LevelInfo m a -> m a
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT LevelInfo m a -> LevelInfo -> m a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (Level -> Bimap Unique Level -> LevelInfo
LevelInfo (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)