{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TemplateHaskell #-}
{-# OPTIONS_GHC -Wno-identities #-}
module PlutusCore.DeBruijn.Internal
( Index (..)
, HasIndex (..)
, DeBruijn (..)
, NamedDeBruijn (..)
, 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
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)
deBruijnInitIndex :: Index
deBruijnInitIndex :: Index
deBruijnInitIndex = Index
0
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)
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
fakeName :: T.Text
fakeName :: Text
fakeName = Text
"i"
instance Eq NamedDeBruijn where
(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
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)
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)
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
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
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)
data LevelInfo = LevelInfo
{ LevelInfo -> Level
currentLevel :: Level
, LevelInfo -> Bimap Unique Level
levelMapping :: BM.Bimap Unique 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
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
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
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
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
Maybe Level
Nothing -> Unique -> m Index
h Unique
u
where
levelToIx :: Level -> Level -> Index
levelToIx :: Level -> Level -> Index
levelToIx (Level Integer
current) (Level Integer
foundLvl) =
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
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
Just Unique
u -> Unique -> m Unique
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Unique
u
Maybe Unique
Nothing ->
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
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
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
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
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
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
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)