{-# LANGUAGE MultiWayIf #-}

module Covenant.Internal.Rename
  ( RenameM,
    RenameError (..),
    runRenameM,
    renameValT,
    renameDataDecl,
    renameCompT,
    undoRename,
    renameDatatypeInfo,
    UnRenameM,
    UnRenameError (..),
    runUnRenameM,
  )
where

import Control.Monad.Except
  ( ExceptT,
    MonadError,
    runExceptT,
    throwError,
  )
import Control.Monad.Reader
  ( MonadReader,
    Reader,
    asks,
    local,
    runReader,
  )
import Control.Monad.State.Strict
  ( State,
    evalState,
    gets,
    modify,
  )
import Covenant.Data (DatatypeInfo (DatatypeInfo))
import Covenant.DeBruijn (DeBruijn (Z), asInt)
import Covenant.Index (Count, Index, intIndex, wordCount)
import Covenant.Internal.Type
  ( AbstractTy (BoundAt),
    CompT (CompT),
    CompTBody (CompTBody),
    Constructor (Constructor),
    DataDeclaration (DataDeclaration, OpaqueData),
    Renamed (Rigid, Unifiable, Wildcard),
    ValT (Abstraction, BuiltinFlat, Datatype, ThunkT),
  )
import Data.Bitraversable (Bitraversable (bitraverse))
import Data.Coerce (coerce)
import Data.Kind (Type)
import Data.Vector (Vector)
import Data.Vector qualified as Vector
import Data.Vector.NonEmpty qualified as NonEmpty
import Data.Word (Word32, Word64)
import Optics.Core
  ( A_Lens,
    LabelOptic (labelOptic),
    lens,
    over,
    preview,
    review,
    set,
    to,
    view,
    (%),
  )

-- Used during renaming. Contains a source of fresh indices for wildcards, as
-- well as:
--
-- 1. The first Word64 argument is the "source of freshness" for WildCards
-- 2. The second Word64 argument is the inherited scope size
-- 3. The *size* of the vector tracks the current scope size (the enclosing scope is inherited, but it may grow during renaming)
-- 4. The first element of the tuple in the vector is the *count* of TyVars bound in each scope. (Note: It is therefore 1 greater than the index)
-- 5. The second element of the tuple in the vector is the unique identifier for wildcards in each scope.
data RenameState = RenameState Word64 Word32 (Vector (Word32, Word64))
  deriving stock (RenameState -> RenameState -> Bool
(RenameState -> RenameState -> Bool)
-> (RenameState -> RenameState -> Bool) -> Eq RenameState
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: RenameState -> RenameState -> Bool
== :: RenameState -> RenameState -> Bool
$c/= :: RenameState -> RenameState -> Bool
/= :: RenameState -> RenameState -> Bool
Eq, Int -> RenameState -> ShowS
[RenameState] -> ShowS
RenameState -> String
(Int -> RenameState -> ShowS)
-> (RenameState -> String)
-> ([RenameState] -> ShowS)
-> Show RenameState
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> RenameState -> ShowS
showsPrec :: Int -> RenameState -> ShowS
$cshow :: RenameState -> String
show :: RenameState -> String
$cshowList :: [RenameState] -> ShowS
showList :: [RenameState] -> ShowS
Show)

-- Note (Koz, 11/04/2025): We need this field as a source of unique identifiers
-- when renaming wildcards. Wildcards are special in that they can unify with
-- anything (possibly _several_ anythings) except different wildcards in the
-- same scope as each other. For example, consider the computation type below:
--
-- (forall a b . a -> b -> !Int) -> (forall c . c -> !Int) -> String -> !Int
--
-- In particular, `a` and `c` would be defined the same way: `BoundAt Z ix0`.
-- However, while `c` and `b` could unify just fine, `a` and `b` could not.
-- Furthermore, they are identically scoped (in the sense that they're both
-- enclosed the same way), which means that, unlike rigid variables, we cannot
-- uniquely identify them just by their scoping.
--
-- Thus, we have to have to have a way to uniquely label any wildcard in such a
-- way that wildcards in the same scope, at the same level, are tagged
-- separately from wildcards in a _different_ scope at the same level. See the
-- functions `stepUpScope` and `dropDownScope` to see how we achieve this.
instance
  (k ~ A_Lens, a ~ Word64, b ~ Word64) =>
  LabelOptic "idSource" k RenameState RenameState a b
  where
  {-# INLINEABLE labelOptic #-}
  labelOptic :: Optic k NoIx RenameState RenameState a b
labelOptic =
    (RenameState -> a)
-> (RenameState -> b -> RenameState)
-> Lens RenameState RenameState a b
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens
      (\(RenameState Word64
x Word32
_ Vector (Word32, Word64)
_) -> a
Word64
x)
      (\(RenameState Word64
_ Word32
b Vector (Word32, Word64)
c) b
a' -> Word64 -> Word32 -> Vector (Word32, Word64) -> RenameState
RenameState b
Word64
a' Word32
b Vector (Word32, Word64)
c)

instance
  (k ~ A_Lens, a ~ Word32, b ~ Word32) =>
  LabelOptic "inheritedScope" k RenameState RenameState a b
  where
  {-# INLINEABLE labelOptic #-}
  labelOptic :: Optic k NoIx RenameState RenameState a b
labelOptic =
    (RenameState -> a)
-> (RenameState -> b -> RenameState)
-> Lens RenameState RenameState a b
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens
      (\(RenameState Word64
_ Word32
x Vector (Word32, Word64)
_) -> a
Word32
x)
      (\(RenameState Word64
a Word32
_ Vector (Word32, Word64)
c) b
b' -> Word64 -> Word32 -> Vector (Word32, Word64) -> RenameState
RenameState Word64
a b
Word32
b' Vector (Word32, Word64)
c)

instance
  (k ~ A_Lens, a ~ Vector (Word32, Word64), b ~ Vector (Word32, Word64)) =>
  LabelOptic "tracker" k RenameState RenameState a b
  where
  {-# INLINEABLE labelOptic #-}
  labelOptic :: Optic k NoIx RenameState RenameState a b
labelOptic =
    (RenameState -> a)
-> (RenameState -> b -> RenameState)
-> Lens RenameState RenameState a b
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens
      (\(RenameState Word64
_ Word32
_ Vector (Word32, Word64)
y) -> a
Vector (Word32, Word64)
y)
      (\(RenameState Word64
x Word32
y Vector (Word32, Word64)
_) b
z' -> Word64 -> Word32 -> Vector (Word32, Word64) -> RenameState
RenameState Word64
x Word32
y b
Vector (Word32, Word64)
z')

-- | Ways in which the renamer can fail.
--
-- @since 1.1.0
data RenameError
  = -- | An attempt to reference an abstraction in a scope where this
    -- abstraction doesn't exist, but where the scope itself /does/ exist.
    -- Put another way: This gets thrown when the argument index of an
    -- abstraction inconsistent with the `Count` of the scope its DB index refers to.
    -- First field is the true level, second is the index that was requested.
    --
    -- @since 1.2.0
    InvalidAbstractionReference Int (Index "tyvar")
  | -- | An abstraction refers to a scope which does not exist. That is: The abstraction's
    -- DeBruijn index points to a scope "higher than" the top-level scope.
    --
    -- @since 1.2.0
    InvalidScopeReference Int (Index "tyvar")
  deriving stock (RenameError -> RenameError -> Bool
(RenameError -> RenameError -> Bool)
-> (RenameError -> RenameError -> Bool) -> Eq RenameError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: RenameError -> RenameError -> Bool
== :: RenameError -> RenameError -> Bool
$c/= :: RenameError -> RenameError -> Bool
/= :: RenameError -> RenameError -> Bool
Eq, Int -> RenameError -> ShowS
[RenameError] -> ShowS
RenameError -> String
(Int -> RenameError -> ShowS)
-> (RenameError -> String)
-> ([RenameError] -> ShowS)
-> Show RenameError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> RenameError -> ShowS
showsPrec :: Int -> RenameError -> ShowS
$cshow :: RenameError -> String
show :: RenameError -> String
$cshowList :: [RenameError] -> ShowS
showList :: [RenameError] -> ShowS
Show)

-- | Ways in which the un-renamer can fail.
--
-- @since 1.2.0
data UnRenameError
  = -- | We tried to un-rename a wildcard. This means something has gone very wrong internally.
    -- @since 1.2.0
    UnRenameWildCard Renamed
  | -- | We received a negative DeBruijn in our true level calculation. This is impossible, and indicates another
    --   internal malfunction or bug
    NegativeDeBruijn Int
  deriving stock
    ( -- | @since 1.2.0
      UnRenameError -> UnRenameError -> Bool
(UnRenameError -> UnRenameError -> Bool)
-> (UnRenameError -> UnRenameError -> Bool) -> Eq UnRenameError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: UnRenameError -> UnRenameError -> Bool
== :: UnRenameError -> UnRenameError -> Bool
$c/= :: UnRenameError -> UnRenameError -> Bool
/= :: UnRenameError -> UnRenameError -> Bool
Eq,
      -- | @since 1.2.0
      Int -> UnRenameError -> ShowS
[UnRenameError] -> ShowS
UnRenameError -> String
(Int -> UnRenameError -> ShowS)
-> (UnRenameError -> String)
-> ([UnRenameError] -> ShowS)
-> Show UnRenameError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> UnRenameError -> ShowS
showsPrec :: Int -> UnRenameError -> ShowS
$cshow :: UnRenameError -> String
show :: UnRenameError -> String
$cshowList :: [UnRenameError] -> ShowS
showList :: [UnRenameError] -> ShowS
Show
    )

-- | A \'renaming monad\' which allows us to convert type representations from
-- ones that use /relative/ abstraction labelling to /absolute/ abstraction
-- labelling.
--
-- = Why this is necessary
--
-- Consider the following 'AbstractTy': @'BoundAtScope' 1 0@. The meaning of
-- this is relative to where in a type it is positioned: it could be bound by a
-- scope higher than our own, or something we can unify with. Because its
-- meaning (namely, what it refers to) is situational, type checking becomes
-- more difficult, although it has other advantages.
--
-- This monad allows us to convert this relative form into an absolute one. More
-- specifically, the renamer does two things:
--
-- * Ensures that any given abstraction refers to one, and /only/ one, thing;
-- and
-- * Indicates which abstractions are unifiable, and which are (effectively)
-- constant or fixed.
--
-- @since 1.0.0
newtype RenameM (a :: Type)
  = RenameM (ExceptT RenameError (State RenameState) a)
  deriving
    ( -- | @since 1.0.0
      (forall a b. (a -> b) -> RenameM a -> RenameM b)
-> (forall a b. a -> RenameM b -> RenameM a) -> Functor RenameM
forall a b. a -> RenameM b -> RenameM a
forall a b. (a -> b) -> RenameM a -> RenameM b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> RenameM a -> RenameM b
fmap :: forall a b. (a -> b) -> RenameM a -> RenameM b
$c<$ :: forall a b. a -> RenameM b -> RenameM a
<$ :: forall a b. a -> RenameM b -> RenameM a
Functor,
      -- | @since 1.0.0
      Functor RenameM
Functor RenameM =>
(forall a. a -> RenameM a)
-> (forall a b. RenameM (a -> b) -> RenameM a -> RenameM b)
-> (forall a b c.
    (a -> b -> c) -> RenameM a -> RenameM b -> RenameM c)
-> (forall a b. RenameM a -> RenameM b -> RenameM b)
-> (forall a b. RenameM a -> RenameM b -> RenameM a)
-> Applicative RenameM
forall a. a -> RenameM a
forall a b. RenameM a -> RenameM b -> RenameM a
forall a b. RenameM a -> RenameM b -> RenameM b
forall a b. RenameM (a -> b) -> RenameM a -> RenameM b
forall a b c. (a -> b -> c) -> RenameM a -> RenameM b -> RenameM c
forall (f :: Type -> Type).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall a. a -> RenameM a
pure :: forall a. a -> RenameM a
$c<*> :: forall a b. RenameM (a -> b) -> RenameM a -> RenameM b
<*> :: forall a b. RenameM (a -> b) -> RenameM a -> RenameM b
$cliftA2 :: forall a b c. (a -> b -> c) -> RenameM a -> RenameM b -> RenameM c
liftA2 :: forall a b c. (a -> b -> c) -> RenameM a -> RenameM b -> RenameM c
$c*> :: forall a b. RenameM a -> RenameM b -> RenameM b
*> :: forall a b. RenameM a -> RenameM b -> RenameM b
$c<* :: forall a b. RenameM a -> RenameM b -> RenameM a
<* :: forall a b. RenameM a -> RenameM b -> RenameM a
Applicative,
      -- | @since 1.0.0
      Applicative RenameM
Applicative RenameM =>
(forall a b. RenameM a -> (a -> RenameM b) -> RenameM b)
-> (forall a b. RenameM a -> RenameM b -> RenameM b)
-> (forall a. a -> RenameM a)
-> Monad RenameM
forall a. a -> RenameM a
forall a b. RenameM a -> RenameM b -> RenameM b
forall a b. RenameM a -> (a -> RenameM b) -> RenameM b
forall (m :: Type -> Type).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall a b. RenameM a -> (a -> RenameM b) -> RenameM b
>>= :: forall a b. RenameM a -> (a -> RenameM b) -> RenameM b
$c>> :: forall a b. RenameM a -> RenameM b -> RenameM b
>> :: forall a b. RenameM a -> RenameM b -> RenameM b
$creturn :: forall a. a -> RenameM a
return :: forall a. a -> RenameM a
Monad
    )
    via (ExceptT RenameError (State RenameState))

-- | The portions of the RenameState needed for unrenaming. Lacks the unique indicator for
-- wildcards, since trying to un-rename a wildcard is an error.
data UnRenameCxt = UnRenameCxt Word32 (Vector Word32)
  deriving stock
    ( -- @since 1.2.0
      Int -> UnRenameCxt -> ShowS
[UnRenameCxt] -> ShowS
UnRenameCxt -> String
(Int -> UnRenameCxt -> ShowS)
-> (UnRenameCxt -> String)
-> ([UnRenameCxt] -> ShowS)
-> Show UnRenameCxt
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> UnRenameCxt -> ShowS
showsPrec :: Int -> UnRenameCxt -> ShowS
$cshow :: UnRenameCxt -> String
show :: UnRenameCxt -> String
$cshowList :: [UnRenameCxt] -> ShowS
showList :: [UnRenameCxt] -> ShowS
Show,
      -- @since 1.2.0
      UnRenameCxt -> UnRenameCxt -> Bool
(UnRenameCxt -> UnRenameCxt -> Bool)
-> (UnRenameCxt -> UnRenameCxt -> Bool) -> Eq UnRenameCxt
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: UnRenameCxt -> UnRenameCxt -> Bool
== :: UnRenameCxt -> UnRenameCxt -> Bool
$c/= :: UnRenameCxt -> UnRenameCxt -> Bool
/= :: UnRenameCxt -> UnRenameCxt -> Bool
Eq,
      -- @since 1.2.0
      Eq UnRenameCxt
Eq UnRenameCxt =>
(UnRenameCxt -> UnRenameCxt -> Ordering)
-> (UnRenameCxt -> UnRenameCxt -> Bool)
-> (UnRenameCxt -> UnRenameCxt -> Bool)
-> (UnRenameCxt -> UnRenameCxt -> Bool)
-> (UnRenameCxt -> UnRenameCxt -> Bool)
-> (UnRenameCxt -> UnRenameCxt -> UnRenameCxt)
-> (UnRenameCxt -> UnRenameCxt -> UnRenameCxt)
-> Ord UnRenameCxt
UnRenameCxt -> UnRenameCxt -> Bool
UnRenameCxt -> UnRenameCxt -> Ordering
UnRenameCxt -> UnRenameCxt -> UnRenameCxt
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 :: UnRenameCxt -> UnRenameCxt -> Ordering
compare :: UnRenameCxt -> UnRenameCxt -> Ordering
$c< :: UnRenameCxt -> UnRenameCxt -> Bool
< :: UnRenameCxt -> UnRenameCxt -> Bool
$c<= :: UnRenameCxt -> UnRenameCxt -> Bool
<= :: UnRenameCxt -> UnRenameCxt -> Bool
$c> :: UnRenameCxt -> UnRenameCxt -> Bool
> :: UnRenameCxt -> UnRenameCxt -> Bool
$c>= :: UnRenameCxt -> UnRenameCxt -> Bool
>= :: UnRenameCxt -> UnRenameCxt -> Bool
$cmax :: UnRenameCxt -> UnRenameCxt -> UnRenameCxt
max :: UnRenameCxt -> UnRenameCxt -> UnRenameCxt
$cmin :: UnRenameCxt -> UnRenameCxt -> UnRenameCxt
min :: UnRenameCxt -> UnRenameCxt -> UnRenameCxt
Ord
    )

instance
  (k ~ A_Lens, a ~ Word32, b ~ Word32) =>
  LabelOptic "inheritedScopeSize" k UnRenameCxt UnRenameCxt a b
  where
  {-# INLINEABLE labelOptic #-}
  labelOptic :: Optic k NoIx UnRenameCxt UnRenameCxt a b
labelOptic =
    (UnRenameCxt -> a)
-> (UnRenameCxt -> b -> UnRenameCxt)
-> Lens UnRenameCxt UnRenameCxt a b
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens
      (\(UnRenameCxt Word32
x Vector Word32
_) -> a
Word32
x)
      (\(UnRenameCxt Word32
_ Vector Word32
y) b
x' -> Word32 -> Vector Word32 -> UnRenameCxt
UnRenameCxt b
Word32
x' Vector Word32
y)

instance
  (k ~ A_Lens, a ~ Vector Word32, b ~ Vector Word32) =>
  LabelOptic "scopeInfo" k UnRenameCxt UnRenameCxt a b
  where
  {-# INLINEABLE labelOptic #-}
  labelOptic :: Optic k NoIx UnRenameCxt UnRenameCxt a b
labelOptic =
    (UnRenameCxt -> a)
-> (UnRenameCxt -> b -> UnRenameCxt)
-> Lens UnRenameCxt UnRenameCxt a b
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens
      (\(UnRenameCxt Word32
_ Vector Word32
y) -> a
Vector Word32
y)
      (\(UnRenameCxt Word32
x Vector Word32
_) b
y' -> Word32 -> Vector Word32 -> UnRenameCxt
UnRenameCxt Word32
x b
Vector Word32
y')

-- | @since 1.2.0
newtype UnRenameM (a :: Type) = UnRenameM (ExceptT UnRenameError (Reader UnRenameCxt) a)
  deriving
    ( -- | @since 1.2.0
      (forall a b. (a -> b) -> UnRenameM a -> UnRenameM b)
-> (forall a b. a -> UnRenameM b -> UnRenameM a)
-> Functor UnRenameM
forall a b. a -> UnRenameM b -> UnRenameM a
forall a b. (a -> b) -> UnRenameM a -> UnRenameM b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> UnRenameM a -> UnRenameM b
fmap :: forall a b. (a -> b) -> UnRenameM a -> UnRenameM b
$c<$ :: forall a b. a -> UnRenameM b -> UnRenameM a
<$ :: forall a b. a -> UnRenameM b -> UnRenameM a
Functor,
      -- | @since 1.2.0
      Functor UnRenameM
Functor UnRenameM =>
(forall a. a -> UnRenameM a)
-> (forall a b. UnRenameM (a -> b) -> UnRenameM a -> UnRenameM b)
-> (forall a b c.
    (a -> b -> c) -> UnRenameM a -> UnRenameM b -> UnRenameM c)
-> (forall a b. UnRenameM a -> UnRenameM b -> UnRenameM b)
-> (forall a b. UnRenameM a -> UnRenameM b -> UnRenameM a)
-> Applicative UnRenameM
forall a. a -> UnRenameM a
forall a b. UnRenameM a -> UnRenameM b -> UnRenameM a
forall a b. UnRenameM a -> UnRenameM b -> UnRenameM b
forall a b. UnRenameM (a -> b) -> UnRenameM a -> UnRenameM b
forall a b c.
(a -> b -> c) -> UnRenameM a -> UnRenameM b -> UnRenameM c
forall (f :: Type -> Type).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall a. a -> UnRenameM a
pure :: forall a. a -> UnRenameM a
$c<*> :: forall a b. UnRenameM (a -> b) -> UnRenameM a -> UnRenameM b
<*> :: forall a b. UnRenameM (a -> b) -> UnRenameM a -> UnRenameM b
$cliftA2 :: forall a b c.
(a -> b -> c) -> UnRenameM a -> UnRenameM b -> UnRenameM c
liftA2 :: forall a b c.
(a -> b -> c) -> UnRenameM a -> UnRenameM b -> UnRenameM c
$c*> :: forall a b. UnRenameM a -> UnRenameM b -> UnRenameM b
*> :: forall a b. UnRenameM a -> UnRenameM b -> UnRenameM b
$c<* :: forall a b. UnRenameM a -> UnRenameM b -> UnRenameM a
<* :: forall a b. UnRenameM a -> UnRenameM b -> UnRenameM a
Applicative,
      -- | @since 1.2.0
      Applicative UnRenameM
Applicative UnRenameM =>
(forall a b. UnRenameM a -> (a -> UnRenameM b) -> UnRenameM b)
-> (forall a b. UnRenameM a -> UnRenameM b -> UnRenameM b)
-> (forall a. a -> UnRenameM a)
-> Monad UnRenameM
forall a. a -> UnRenameM a
forall a b. UnRenameM a -> UnRenameM b -> UnRenameM b
forall a b. UnRenameM a -> (a -> UnRenameM b) -> UnRenameM b
forall (m :: Type -> Type).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall a b. UnRenameM a -> (a -> UnRenameM b) -> UnRenameM b
>>= :: forall a b. UnRenameM a -> (a -> UnRenameM b) -> UnRenameM b
$c>> :: forall a b. UnRenameM a -> UnRenameM b -> UnRenameM b
>> :: forall a b. UnRenameM a -> UnRenameM b -> UnRenameM b
$creturn :: forall a. a -> UnRenameM a
return :: forall a. a -> UnRenameM a
Monad,
      -- | @since 1.2.0
      MonadReader UnRenameCxt,
      -- | @since 1.2.0
      MonadError UnRenameError
    )
    via (ExceptT UnRenameError (Reader UnRenameCxt))

-- | Execute a renaming computation.
--
-- @since 1.2.0
runRenameM ::
  forall (a :: Type).
  Vector Word32 ->
  RenameM a ->
  Either RenameError a
runRenameM :: forall a. Vector Word32 -> RenameM a -> Either RenameError a
runRenameM Vector Word32
scopeInfo (RenameM ExceptT RenameError (State RenameState) a
comp) =
  State RenameState (Either RenameError a)
-> RenameState -> Either RenameError a
forall s a. State s a -> s -> a
evalState (ExceptT RenameError (State RenameState) a
-> State RenameState (Either RenameError a)
forall e (m :: Type -> Type) a. ExceptT e m a -> m (Either e a)
runExceptT ExceptT RenameError (State RenameState) a
comp)
    (RenameState -> Either RenameError a)
-> (Vector (Word32, Word64) -> RenameState)
-> Vector (Word32, Word64)
-> Either RenameError a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word64 -> Word32 -> Vector (Word32, Word64) -> RenameState
RenameState Word64
0 (Int -> Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Word32) -> Int -> Word32
forall a b. (a -> b) -> a -> b
$ Vector Word32 -> Int
forall a. Vector a -> Int
Vector.length Vector Word32
scopeInfo)
    (Vector (Word32, Word64) -> Either RenameError a)
-> Vector (Word32, Word64) -> Either RenameError a
forall a b. (a -> b) -> a -> b
$ (Word32 -> (Word32, Word64))
-> Vector Word32 -> Vector (Word32, Word64)
forall a b. (a -> b) -> Vector a -> Vector b
Vector.map (,Word64
0) Vector Word32
scopeInfo

runUnRenameM ::
  forall (a :: Type).
  UnRenameM a ->
  Vector Word32 ->
  Either UnRenameError a
runUnRenameM :: forall a. UnRenameM a -> Vector Word32 -> Either UnRenameError a
runUnRenameM (UnRenameM ExceptT UnRenameError (Reader UnRenameCxt) a
comp) Vector Word32
inherited = Reader UnRenameCxt (Either UnRenameError a)
-> UnRenameCxt -> Either UnRenameError a
forall r a. Reader r a -> r -> a
runReader (ExceptT UnRenameError (Reader UnRenameCxt) a
-> Reader UnRenameCxt (Either UnRenameError a)
forall e (m :: Type -> Type) a. ExceptT e m a -> m (Either e a)
runExceptT ExceptT UnRenameError (Reader UnRenameCxt) a
comp) (UnRenameCxt -> Either UnRenameError a)
-> UnRenameCxt -> Either UnRenameError a
forall a b. (a -> b) -> a -> b
$ Word32 -> Vector Word32 -> UnRenameCxt
UnRenameCxt (Int -> Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Word32) -> Int -> Word32
forall a b. (a -> b) -> a -> b
$ Vector Word32 -> Int
forall a. Vector a -> Int
Vector.length Vector Word32
inherited) Vector Word32
inherited

-- | Rename a computation type.
--
-- @since 1.0.0
renameCompT :: CompT AbstractTy -> RenameM (CompT Renamed)
renameCompT :: CompT AbstractTy -> RenameM (CompT Renamed)
renameCompT (CompT Count "tyvar"
abses (CompTBody NonEmptyVector (ValT AbstractTy)
xs)) = ExceptT RenameError (State RenameState) (CompT Renamed)
-> RenameM (CompT Renamed)
forall a. ExceptT RenameError (State RenameState) a -> RenameM a
RenameM (ExceptT RenameError (State RenameState) (CompT Renamed)
 -> RenameM (CompT Renamed))
-> ExceptT RenameError (State RenameState) (CompT Renamed)
-> RenameM (CompT Renamed)
forall a b. (a -> b) -> a -> b
$ do
  -- Step up a scope
  (RenameState -> RenameState)
-> ExceptT RenameError (State RenameState) ()
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
modify (Count "tyvar" -> RenameState -> RenameState
stepUpScope Count "tyvar"
abses)
  -- Rename, but only the arguments
  Vector (ValT Renamed)
renamedArgs <-
    Int
-> (Int -> ExceptT RenameError (State RenameState) (ValT Renamed))
-> ExceptT RenameError (State RenameState) (Vector (ValT Renamed))
forall (m :: Type -> Type) a.
Monad m =>
Int -> (Int -> m a) -> m (Vector a)
Vector.generateM
      (NonEmptyVector (ValT AbstractTy) -> Int
forall a. NonEmptyVector a -> Int
NonEmpty.length NonEmptyVector (ValT AbstractTy)
xs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
      (\Int
i -> RenameM (ValT Renamed)
-> ExceptT RenameError (State RenameState) (ValT Renamed)
forall a b. Coercible a b => a -> b
coerce (RenameM (ValT Renamed)
 -> ExceptT RenameError (State RenameState) (ValT Renamed))
-> (ValT AbstractTy -> RenameM (ValT Renamed))
-> ValT AbstractTy
-> ExceptT RenameError (State RenameState) (ValT Renamed)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValT AbstractTy -> RenameM (ValT Renamed)
renameValT (ValT AbstractTy
 -> ExceptT RenameError (State RenameState) (ValT Renamed))
-> ValT AbstractTy
-> ExceptT RenameError (State RenameState) (ValT Renamed)
forall a b. (a -> b) -> a -> b
$ NonEmptyVector (ValT AbstractTy)
xs NonEmptyVector (ValT AbstractTy) -> Int -> ValT AbstractTy
forall a. NonEmptyVector a -> Int -> a
NonEmpty.! Int
i)
  -- Check result type
  ValT Renamed
renamedResult <- RenameM (ValT Renamed)
-> ExceptT RenameError (State RenameState) (ValT Renamed)
forall a b. Coercible a b => a -> b
coerce (RenameM (ValT Renamed)
 -> ExceptT RenameError (State RenameState) (ValT Renamed))
-> (NonEmptyVector (ValT AbstractTy) -> RenameM (ValT Renamed))
-> NonEmptyVector (ValT AbstractTy)
-> ExceptT RenameError (State RenameState) (ValT Renamed)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValT AbstractTy -> RenameM (ValT Renamed)
renameValT (ValT AbstractTy -> RenameM (ValT Renamed))
-> (NonEmptyVector (ValT AbstractTy) -> ValT AbstractTy)
-> NonEmptyVector (ValT AbstractTy)
-> RenameM (ValT Renamed)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmptyVector (ValT AbstractTy) -> ValT AbstractTy
forall a. NonEmptyVector a -> a
NonEmpty.last (NonEmptyVector (ValT AbstractTy)
 -> ExceptT RenameError (State RenameState) (ValT Renamed))
-> NonEmptyVector (ValT AbstractTy)
-> ExceptT RenameError (State RenameState) (ValT Renamed)
forall a b. (a -> b) -> a -> b
$ NonEmptyVector (ValT AbstractTy)
xs
  -- Roll back state
  (RenameState -> RenameState)
-> ExceptT RenameError (State RenameState) ()
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
modify RenameState -> RenameState
dropDownScope
  -- Rebuild and return
  CompT Renamed
-> ExceptT RenameError (State RenameState) (CompT Renamed)
forall a. a -> ExceptT RenameError (State RenameState) a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (CompT Renamed
 -> ExceptT RenameError (State RenameState) (CompT Renamed))
-> (ValT Renamed -> CompT Renamed)
-> ValT Renamed
-> ExceptT RenameError (State RenameState) (CompT Renamed)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Count "tyvar" -> CompTBody Renamed -> CompT Renamed
forall a. Count "tyvar" -> CompTBody a -> CompT a
CompT Count "tyvar"
abses (CompTBody Renamed -> CompT Renamed)
-> (ValT Renamed -> CompTBody Renamed)
-> ValT Renamed
-> CompT Renamed
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmptyVector (ValT Renamed) -> CompTBody Renamed
forall a. NonEmptyVector (ValT a) -> CompTBody a
CompTBody (NonEmptyVector (ValT Renamed) -> CompTBody Renamed)
-> (ValT Renamed -> NonEmptyVector (ValT Renamed))
-> ValT Renamed
-> CompTBody Renamed
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector (ValT Renamed)
-> ValT Renamed -> NonEmptyVector (ValT Renamed)
forall a. Vector a -> a -> NonEmptyVector a
NonEmpty.snocV Vector (ValT Renamed)
renamedArgs (ValT Renamed
 -> ExceptT RenameError (State RenameState) (CompT Renamed))
-> ValT Renamed
-> ExceptT RenameError (State RenameState) (CompT Renamed)
forall a b. (a -> b) -> a -> b
$ ValT Renamed
renamedResult

-- | Rename a value type.
--
-- @since 1.0.0
renameValT :: ValT AbstractTy -> RenameM (ValT Renamed)
renameValT :: ValT AbstractTy -> RenameM (ValT Renamed)
renameValT = \case
  Abstraction AbstractTy
t -> Renamed -> ValT Renamed
forall a. a -> ValT a
Abstraction (Renamed -> ValT Renamed)
-> RenameM Renamed -> RenameM (ValT Renamed)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> AbstractTy -> RenameM Renamed
renameAbstraction AbstractTy
t
  ThunkT CompT AbstractTy
t -> CompT Renamed -> ValT Renamed
forall a. CompT a -> ValT a
ThunkT (CompT Renamed -> ValT Renamed)
-> RenameM (CompT Renamed) -> RenameM (ValT Renamed)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> CompT AbstractTy -> RenameM (CompT Renamed)
renameCompT CompT AbstractTy
t
  BuiltinFlat BuiltinFlatT
t -> ValT Renamed -> RenameM (ValT Renamed)
forall a. a -> RenameM a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (ValT Renamed -> RenameM (ValT Renamed))
-> (BuiltinFlatT -> ValT Renamed)
-> BuiltinFlatT
-> RenameM (ValT Renamed)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinFlatT -> ValT Renamed
forall a. BuiltinFlatT -> ValT a
BuiltinFlat (BuiltinFlatT -> RenameM (ValT Renamed))
-> BuiltinFlatT -> RenameM (ValT Renamed)
forall a b. (a -> b) -> a -> b
$ BuiltinFlatT
t
  -- Assumes kind-checking has occurred
  Datatype TyName
tn Vector (ValT AbstractTy)
xs -> ExceptT RenameError (State RenameState) (ValT Renamed)
-> RenameM (ValT Renamed)
forall a. ExceptT RenameError (State RenameState) a -> RenameM a
RenameM (ExceptT RenameError (State RenameState) (ValT Renamed)
 -> RenameM (ValT Renamed))
-> ExceptT RenameError (State RenameState) (ValT Renamed)
-> RenameM (ValT Renamed)
forall a b. (a -> b) -> a -> b
$ do
    -- We don't step or un-step the scope here b/c a TyCon which appears as a ValT _cannot_ bind variables.
    -- This Vector here doesn't represent a function, but a product, so we there is no "return" type to treat specially (I think!)
    Vector (ValT Renamed)
renamedXS <- (ValT AbstractTy
 -> ExceptT RenameError (State RenameState) (ValT Renamed))
-> Vector (ValT AbstractTy)
-> ExceptT RenameError (State RenameState) (Vector (ValT Renamed))
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Vector a -> m (Vector b)
Vector.mapM (RenameM (ValT Renamed)
-> ExceptT RenameError (State RenameState) (ValT Renamed)
forall a b. Coercible a b => a -> b
coerce (RenameM (ValT Renamed)
 -> ExceptT RenameError (State RenameState) (ValT Renamed))
-> (ValT AbstractTy -> RenameM (ValT Renamed))
-> ValT AbstractTy
-> ExceptT RenameError (State RenameState) (ValT Renamed)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValT AbstractTy -> RenameM (ValT Renamed)
renameValT) Vector (ValT AbstractTy)
xs
    ValT Renamed
-> ExceptT RenameError (State RenameState) (ValT Renamed)
forall a. a -> ExceptT RenameError (State RenameState) a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (ValT Renamed
 -> ExceptT RenameError (State RenameState) (ValT Renamed))
-> ValT Renamed
-> ExceptT RenameError (State RenameState) (ValT Renamed)
forall a b. (a -> b) -> a -> b
$ TyName -> Vector (ValT Renamed) -> ValT Renamed
forall a. TyName -> Vector (ValT a) -> ValT a
Datatype TyName
tn Vector (ValT Renamed)
renamedXS

-- @since 1.1.0
renameDataDecl :: DataDeclaration AbstractTy -> RenameM (DataDeclaration Renamed)
renameDataDecl :: DataDeclaration AbstractTy -> RenameM (DataDeclaration Renamed)
renameDataDecl (OpaqueData TyName
tn Set PlutusDataConstructor
manual) = DataDeclaration Renamed -> RenameM (DataDeclaration Renamed)
forall a. a -> RenameM a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (DataDeclaration Renamed -> RenameM (DataDeclaration Renamed))
-> DataDeclaration Renamed -> RenameM (DataDeclaration Renamed)
forall a b. (a -> b) -> a -> b
$ TyName -> Set PlutusDataConstructor -> DataDeclaration Renamed
forall a. TyName -> Set PlutusDataConstructor -> DataDeclaration a
OpaqueData TyName
tn Set PlutusDataConstructor
manual
renameDataDecl (DataDeclaration TyName
tn Count "tyvar"
cnt Vector (Constructor AbstractTy)
ctors DataEncoding
strat) = ExceptT RenameError (State RenameState) (DataDeclaration Renamed)
-> RenameM (DataDeclaration Renamed)
forall a. ExceptT RenameError (State RenameState) a -> RenameM a
RenameM (ExceptT RenameError (State RenameState) (DataDeclaration Renamed)
 -> RenameM (DataDeclaration Renamed))
-> ExceptT
     RenameError (State RenameState) (DataDeclaration Renamed)
-> RenameM (DataDeclaration Renamed)
forall a b. (a -> b) -> a -> b
$ do
  (RenameState -> RenameState)
-> ExceptT RenameError (State RenameState) ()
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
modify (Count "tyvar" -> RenameState -> RenameState
stepUpScope Count "tyvar"
cnt)
  Vector (Constructor Renamed)
renamedCtors <- (Constructor AbstractTy
 -> ExceptT RenameError (State RenameState) (Constructor Renamed))
-> Vector (Constructor AbstractTy)
-> ExceptT
     RenameError (State RenameState) (Vector (Constructor Renamed))
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Vector a -> m (Vector b)
Vector.mapM (RenameM (Constructor Renamed)
-> ExceptT RenameError (State RenameState) (Constructor Renamed)
forall a b. Coercible a b => a -> b
coerce (RenameM (Constructor Renamed)
 -> ExceptT RenameError (State RenameState) (Constructor Renamed))
-> (Constructor AbstractTy -> RenameM (Constructor Renamed))
-> Constructor AbstractTy
-> ExceptT RenameError (State RenameState) (Constructor Renamed)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constructor AbstractTy -> RenameM (Constructor Renamed)
renameCtor) Vector (Constructor AbstractTy)
ctors
  (RenameState -> RenameState)
-> ExceptT RenameError (State RenameState) ()
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
modify RenameState -> RenameState
dropDownScope
  DataDeclaration Renamed
-> ExceptT
     RenameError (State RenameState) (DataDeclaration Renamed)
forall a. a -> ExceptT RenameError (State RenameState) a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (DataDeclaration Renamed
 -> ExceptT
      RenameError (State RenameState) (DataDeclaration Renamed))
-> DataDeclaration Renamed
-> ExceptT
     RenameError (State RenameState) (DataDeclaration Renamed)
forall a b. (a -> b) -> a -> b
$ TyName
-> Count "tyvar"
-> Vector (Constructor Renamed)
-> DataEncoding
-> DataDeclaration Renamed
forall a.
TyName
-> Count "tyvar"
-> Vector (Constructor a)
-> DataEncoding
-> DataDeclaration a
DataDeclaration TyName
tn Count "tyvar"
cnt Vector (Constructor Renamed)
renamedCtors DataEncoding
strat
  where
    renameCtor :: Constructor AbstractTy -> RenameM (Constructor Renamed)
    renameCtor :: Constructor AbstractTy -> RenameM (Constructor Renamed)
renameCtor (Constructor ConstructorName
cn Vector (ValT AbstractTy)
args) = ConstructorName -> Vector (ValT Renamed) -> Constructor Renamed
forall a. ConstructorName -> Vector (ValT a) -> Constructor a
Constructor ConstructorName
cn (Vector (ValT Renamed) -> Constructor Renamed)
-> RenameM (Vector (ValT Renamed)) -> RenameM (Constructor Renamed)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (ValT AbstractTy -> RenameM (ValT Renamed))
-> Vector (ValT AbstractTy) -> RenameM (Vector (ValT Renamed))
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Vector a -> f (Vector b)
traverse ValT AbstractTy -> RenameM (ValT Renamed)
renameValT Vector (ValT AbstractTy)
args

-- REVIEW: I am not sure if we really want the scope arg to runRenameM to be `mempty`.
--         If something breaks w/ BB forms or datatypes, look here.
renameDatatypeInfo :: DatatypeInfo AbstractTy -> Either RenameError (DatatypeInfo Renamed)
renameDatatypeInfo :: DatatypeInfo AbstractTy
-> Either RenameError (DatatypeInfo Renamed)
renameDatatypeInfo (DatatypeInfo DataDeclaration AbstractTy
ogDecl Maybe (DataDeclaration AbstractTy, ValT AbstractTy)
baseFStuff Maybe (ValT AbstractTy)
bb) = Vector Word32
-> RenameM (DatatypeInfo Renamed)
-> Either RenameError (DatatypeInfo Renamed)
forall a. Vector Word32 -> RenameM a -> Either RenameError a
runRenameM Vector Word32
forall a. Monoid a => a
mempty (RenameM (DatatypeInfo Renamed)
 -> Either RenameError (DatatypeInfo Renamed))
-> RenameM (DatatypeInfo Renamed)
-> Either RenameError (DatatypeInfo Renamed)
forall a b. (a -> b) -> a -> b
$ do
  DataDeclaration Renamed
ogDecl' <- DataDeclaration AbstractTy -> RenameM (DataDeclaration Renamed)
renameDataDecl DataDeclaration AbstractTy
ogDecl
  Maybe (DataDeclaration Renamed, ValT Renamed)
baseFStuff' <- ((DataDeclaration AbstractTy, ValT AbstractTy)
 -> RenameM (DataDeclaration Renamed, ValT Renamed))
-> Maybe (DataDeclaration AbstractTy, ValT AbstractTy)
-> RenameM (Maybe (DataDeclaration Renamed, ValT Renamed))
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe b)
traverse ((DataDeclaration AbstractTy -> RenameM (DataDeclaration Renamed))
-> (ValT AbstractTy -> RenameM (ValT Renamed))
-> (DataDeclaration AbstractTy, ValT AbstractTy)
-> RenameM (DataDeclaration Renamed, ValT Renamed)
forall (f :: Type -> Type) a c b d.
Applicative f =>
(a -> f c) -> (b -> f d) -> (a, b) -> f (c, d)
forall (t :: Type -> Type -> Type) (f :: Type -> Type) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bitraverse DataDeclaration AbstractTy -> RenameM (DataDeclaration Renamed)
renameDataDecl ValT AbstractTy -> RenameM (ValT Renamed)
renameValT) Maybe (DataDeclaration AbstractTy, ValT AbstractTy)
baseFStuff
  Maybe (ValT Renamed)
bb' <- (ValT AbstractTy -> RenameM (ValT Renamed))
-> Maybe (ValT AbstractTy) -> RenameM (Maybe (ValT Renamed))
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe b)
traverse ValT AbstractTy -> RenameM (ValT Renamed)
renameValT Maybe (ValT AbstractTy)
bb
  DatatypeInfo Renamed -> RenameM (DatatypeInfo Renamed)
forall a. a -> RenameM a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (DatatypeInfo Renamed -> RenameM (DatatypeInfo Renamed))
-> DatatypeInfo Renamed -> RenameM (DatatypeInfo Renamed)
forall a b. (a -> b) -> a -> b
$ DataDeclaration Renamed
-> Maybe (DataDeclaration Renamed, ValT Renamed)
-> Maybe (ValT Renamed)
-> DatatypeInfo Renamed
forall var.
DataDeclaration var
-> Maybe (DataDeclaration var, ValT var)
-> Maybe (ValT var)
-> DatatypeInfo var
DatatypeInfo DataDeclaration Renamed
ogDecl' Maybe (DataDeclaration Renamed, ValT Renamed)
baseFStuff' Maybe (ValT Renamed)
bb'

-- A way of 'undoing' the renaming process. This is meant to be used only after
-- applications, and assumes that what is being un-renamed is the result of a
-- computation.
--
-- @since 1.2.0
undoRename :: Vector Word32 -> ValT Renamed -> Either UnRenameError (ValT AbstractTy)
undoRename :: Vector Word32
-> ValT Renamed -> Either UnRenameError (ValT AbstractTy)
undoRename Vector Word32
scope ValT Renamed
t = UnRenameM (ValT AbstractTy)
-> Vector Word32 -> Either UnRenameError (ValT AbstractTy)
forall a. UnRenameM a -> Vector Word32 -> Either UnRenameError a
runUnRenameM (ValT Renamed -> UnRenameM (ValT AbstractTy)
go ValT Renamed
t) Vector Word32
scope
  where
    go :: ValT Renamed -> UnRenameM (ValT AbstractTy)
    go :: ValT Renamed -> UnRenameM (ValT AbstractTy)
go = \case
      Abstraction Renamed
t' ->
        AbstractTy -> ValT AbstractTy
forall a. a -> ValT a
Abstraction (AbstractTy -> ValT AbstractTy)
-> UnRenameM AbstractTy -> UnRenameM (ValT AbstractTy)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> case Renamed
t' of
          Rigid Int
trueLevel Index "tyvar"
index -> do
            DeBruijn
db <- Int -> UnRenameM DeBruijn
unTrueLevel Int
trueLevel
            AbstractTy -> UnRenameM AbstractTy
forall a. a -> UnRenameM a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (AbstractTy -> UnRenameM AbstractTy)
-> AbstractTy -> UnRenameM AbstractTy
forall a b. (a -> b) -> a -> b
$ DeBruijn -> Index "tyvar" -> AbstractTy
BoundAt DeBruijn
db Index "tyvar"
index
          w :: Renamed
w@(Wildcard {}) -> UnRenameError -> UnRenameM AbstractTy
forall a. UnRenameError -> UnRenameM a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (UnRenameError -> UnRenameM AbstractTy)
-> UnRenameError -> UnRenameM AbstractTy
forall a b. (a -> b) -> a -> b
$ Renamed -> UnRenameError
UnRenameWildCard Renamed
w
          Unifiable Index "tyvar"
index -> AbstractTy -> UnRenameM AbstractTy
forall a. a -> UnRenameM a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (AbstractTy -> UnRenameM AbstractTy)
-> AbstractTy -> UnRenameM AbstractTy
forall a b. (a -> b) -> a -> b
$ DeBruijn -> Index "tyvar" -> AbstractTy
BoundAt DeBruijn
Z Index "tyvar"
index
      ThunkT (CompT Count "tyvar"
abses (CompTBody NonEmptyVector (ValT Renamed)
xs)) ->
        CompT AbstractTy -> ValT AbstractTy
forall a. CompT a -> ValT a
ThunkT
          (CompT AbstractTy -> ValT AbstractTy)
-> (NonEmptyVector (ValT AbstractTy) -> CompT AbstractTy)
-> NonEmptyVector (ValT AbstractTy)
-> ValT AbstractTy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Count "tyvar" -> CompTBody AbstractTy -> CompT AbstractTy
forall a. Count "tyvar" -> CompTBody a -> CompT a
CompT Count "tyvar"
abses
          (CompTBody AbstractTy -> CompT AbstractTy)
-> (NonEmptyVector (ValT AbstractTy) -> CompTBody AbstractTy)
-> NonEmptyVector (ValT AbstractTy)
-> CompT AbstractTy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmptyVector (ValT AbstractTy) -> CompTBody AbstractTy
forall a. NonEmptyVector (ValT a) -> CompTBody a
CompTBody
          (NonEmptyVector (ValT AbstractTy) -> ValT AbstractTy)
-> UnRenameM (NonEmptyVector (ValT AbstractTy))
-> UnRenameM (ValT AbstractTy)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (UnRenameCxt -> UnRenameCxt)
-> UnRenameM (NonEmptyVector (ValT AbstractTy))
-> UnRenameM (NonEmptyVector (ValT AbstractTy))
forall a.
(UnRenameCxt -> UnRenameCxt) -> UnRenameM a -> UnRenameM a
forall r (m :: Type -> Type) a.
MonadReader r m =>
(r -> r) -> m a -> m a
local (Optic' A_Lens NoIx UnRenameCxt (Vector Word32)
-> (Vector Word32 -> Vector Word32) -> UnRenameCxt -> UnRenameCxt
forall k (is :: IxList) s t a b.
Is k A_Setter =>
Optic k is s t a b -> (a -> b) -> s -> t
over Optic' A_Lens NoIx UnRenameCxt (Vector Word32)
#scopeInfo (Word32 -> Vector Word32 -> Vector Word32
forall a. a -> Vector a -> Vector a
Vector.cons (Word32 -> Vector Word32 -> Vector Word32)
-> Word32 -> Vector Word32 -> Vector Word32
forall a b. (a -> b) -> a -> b
$ Optic' A_Lens NoIx (Count "tyvar") Word32
-> Count "tyvar" -> Word32
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view Optic' A_Lens NoIx (Count "tyvar") Word32
forall (ofWhat :: Symbol). Lens' (Count ofWhat) Word32
wordCount Count "tyvar"
abses)) ((ValT Renamed -> UnRenameM (ValT AbstractTy))
-> NonEmptyVector (ValT Renamed)
-> UnRenameM (NonEmptyVector (ValT AbstractTy))
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> NonEmptyVector a -> f (NonEmptyVector b)
traverse ValT Renamed -> UnRenameM (ValT AbstractTy)
go NonEmptyVector (ValT Renamed)
xs)
      BuiltinFlat BuiltinFlatT
t' -> ValT AbstractTy -> UnRenameM (ValT AbstractTy)
forall a. a -> UnRenameM a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (ValT AbstractTy -> UnRenameM (ValT AbstractTy))
-> (BuiltinFlatT -> ValT AbstractTy)
-> BuiltinFlatT
-> UnRenameM (ValT AbstractTy)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinFlatT -> ValT AbstractTy
forall a. BuiltinFlatT -> ValT a
BuiltinFlat (BuiltinFlatT -> UnRenameM (ValT AbstractTy))
-> BuiltinFlatT -> UnRenameM (ValT AbstractTy)
forall a b. (a -> b) -> a -> b
$ BuiltinFlatT
t'
      Datatype TyName
tn Vector (ValT Renamed)
args -> TyName -> Vector (ValT AbstractTy) -> ValT AbstractTy
forall a. TyName -> Vector (ValT a) -> ValT a
Datatype TyName
tn (Vector (ValT AbstractTy) -> ValT AbstractTy)
-> UnRenameM (Vector (ValT AbstractTy))
-> UnRenameM (ValT AbstractTy)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (ValT Renamed -> UnRenameM (ValT AbstractTy))
-> Vector (ValT Renamed) -> UnRenameM (Vector (ValT AbstractTy))
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Vector a -> f (Vector b)
traverse ValT Renamed -> UnRenameM (ValT AbstractTy)
go Vector (ValT Renamed)
args

    unTrueLevel :: Int -> UnRenameM DeBruijn
    unTrueLevel :: Int -> UnRenameM DeBruijn
unTrueLevel Int
tl = do
      Int
trackerLen <- (UnRenameCxt -> Int) -> UnRenameM Int
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
asks (Vector Word32 -> Int
forall a. Vector a -> Int
Vector.length (Vector Word32 -> Int)
-> (UnRenameCxt -> Vector Word32) -> UnRenameCxt -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Optic' A_Lens NoIx UnRenameCxt (Vector Word32)
-> UnRenameCxt -> Vector Word32
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view Optic' A_Lens NoIx UnRenameCxt (Vector Word32)
#scopeInfo)
      Int
inheritedSize <- (UnRenameCxt -> Int) -> UnRenameM Int
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
asks (Word32 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word32 -> Int) -> (UnRenameCxt -> Word32) -> UnRenameCxt -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Optic' A_Lens NoIx UnRenameCxt Word32 -> UnRenameCxt -> Word32
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view Optic' A_Lens NoIx UnRenameCxt Word32
#inheritedScopeSize)
      let db :: Int
db = Int
trackerLen Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
inheritedSize Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
tl
      case Optic' A_Prism NoIx Int DeBruijn -> Int -> Maybe DeBruijn
forall k (is :: IxList) s a.
Is k An_AffineFold =>
Optic' k is s a -> s -> Maybe a
preview Optic' A_Prism NoIx Int DeBruijn
asInt Int
db of
        Maybe DeBruijn
Nothing -> UnRenameError -> UnRenameM DeBruijn
forall a. UnRenameError -> UnRenameM a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (UnRenameError -> UnRenameM DeBruijn)
-> UnRenameError -> UnRenameM DeBruijn
forall a b. (a -> b) -> a -> b
$ Int -> UnRenameError
NegativeDeBruijn Int
db
        Just DeBruijn
res -> DeBruijn -> UnRenameM DeBruijn
forall a. a -> UnRenameM a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure DeBruijn
res

renameAbstraction :: AbstractTy -> RenameM Renamed
renameAbstraction :: AbstractTy -> RenameM Renamed
renameAbstraction (BoundAt DeBruijn
scope Index "tyvar"
index) = ExceptT RenameError (State RenameState) Renamed -> RenameM Renamed
forall a. ExceptT RenameError (State RenameState) a -> RenameM a
RenameM (ExceptT RenameError (State RenameState) Renamed
 -> RenameM Renamed)
-> ExceptT RenameError (State RenameState) Renamed
-> RenameM Renamed
forall a b. (a -> b) -> a -> b
$ do
  Int
inheritedScopeSize <- (RenameState -> Int) -> ExceptT RenameError (State RenameState) Int
forall s (m :: Type -> Type) a. MonadState s m => (s -> a) -> m a
gets (Word32 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word32 -> Int) -> (RenameState -> Word32) -> RenameState -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Optic' A_Lens NoIx RenameState Word32 -> RenameState -> Word32
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view Optic' A_Lens NoIx RenameState Word32
#inheritedScope)
  Int
trueLevel <- (RenameState -> Int) -> ExceptT RenameError (State RenameState) Int
forall s (m :: Type -> Type) a. MonadState s m => (s -> a) -> m a
gets (\RenameState
x -> Optic' A_Getter NoIx RenameState Int -> RenameState -> Int
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view (Optic
  A_Lens
  NoIx
  RenameState
  RenameState
  (Vector (Word32, Word64))
  (Vector (Word32, Word64))
#tracker Optic
  A_Lens
  NoIx
  RenameState
  RenameState
  (Vector (Word32, Word64))
  (Vector (Word32, Word64))
-> Optic
     A_Getter
     NoIx
     (Vector (Word32, Word64))
     (Vector (Word32, Word64))
     Int
     Int
-> Optic' A_Getter NoIx RenameState Int
forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% (Vector (Word32, Word64) -> Int)
-> Optic
     A_Getter
     NoIx
     (Vector (Word32, Word64))
     (Vector (Word32, Word64))
     Int
     Int
forall s a. (s -> a) -> Getter s a
to Vector (Word32, Word64) -> Int
forall a. Vector a -> Int
Vector.length) RenameState
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
inheritedScopeSize Int -> Int -> Int
forall a. Num a => a -> a -> a
- Optic' A_Prism NoIx Int DeBruijn -> DeBruijn -> Int
forall k (is :: IxList) t b.
Is k A_Review =>
Optic' k is t b -> b -> t
review Optic' A_Prism NoIx Int DeBruijn
asInt DeBruijn
scope)
  Maybe (Word32, Word64)
scopeInfo <- (RenameState -> Maybe (Word32, Word64))
-> ExceptT RenameError (State RenameState) (Maybe (Word32, Word64))
forall s (m :: Type -> Type) a. MonadState s m => (s -> a) -> m a
gets (\RenameState
x -> Optic
  A_Lens
  NoIx
  RenameState
  RenameState
  (Vector (Word32, Word64))
  (Vector (Word32, Word64))
-> RenameState -> Vector (Word32, Word64)
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view Optic
  A_Lens
  NoIx
  RenameState
  RenameState
  (Vector (Word32, Word64))
  (Vector (Word32, Word64))
#tracker RenameState
x Vector (Word32, Word64) -> Int -> Maybe (Word32, Word64)
forall a. Vector a -> Int -> Maybe a
Vector.!? Optic' A_Prism NoIx Int DeBruijn -> DeBruijn -> Int
forall k (is :: IxList) t b.
Is k A_Review =>
Optic' k is t b -> b -> t
review Optic' A_Prism NoIx Int DeBruijn
asInt DeBruijn
scope)
  let asIntIx :: Int
asIntIx = Optic' A_Prism NoIx Int (Index "tyvar") -> Index "tyvar" -> Int
forall k (is :: IxList) t b.
Is k A_Review =>
Optic' k is t b -> b -> t
review Optic' A_Prism NoIx Int (Index "tyvar")
forall (ofWhat :: Symbol). Prism' Int (Index ofWhat)
intIndex Index "tyvar"
index
  case Maybe (Word32, Word64)
scopeInfo of
    Maybe (Word32, Word64)
Nothing -> RenameError -> ExceptT RenameError (State RenameState) Renamed
forall a. RenameError -> ExceptT RenameError (State RenameState) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (RenameError -> ExceptT RenameError (State RenameState) Renamed)
-> (Index "tyvar" -> RenameError)
-> Index "tyvar"
-> ExceptT RenameError (State RenameState) Renamed
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Index "tyvar" -> RenameError
InvalidScopeReference Int
trueLevel (Index "tyvar" -> ExceptT RenameError (State RenameState) Renamed)
-> Index "tyvar" -> ExceptT RenameError (State RenameState) Renamed
forall a b. (a -> b) -> a -> b
$ Index "tyvar"
index
    Just (Word32
occursTracker, Word64
uniqueScopeId) ->
      if
        | Bool -> Bool
not (Int -> Word32 -> Bool
checkVarIxExists Int
asIntIx Word32
occursTracker) -> RenameError -> ExceptT RenameError (State RenameState) Renamed
forall a. RenameError -> ExceptT RenameError (State RenameState) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (RenameError -> ExceptT RenameError (State RenameState) Renamed)
-> (Index "tyvar" -> RenameError)
-> Index "tyvar"
-> ExceptT RenameError (State RenameState) Renamed
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Index "tyvar" -> RenameError
InvalidAbstractionReference Int
trueLevel (Index "tyvar" -> ExceptT RenameError (State RenameState) Renamed)
-> Index "tyvar" -> ExceptT RenameError (State RenameState) Renamed
forall a b. (a -> b) -> a -> b
$ Index "tyvar"
index
        | Int
trueLevel Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 -> Renamed -> ExceptT RenameError (State RenameState) Renamed
forall a. a -> ExceptT RenameError (State RenameState) a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Renamed -> ExceptT RenameError (State RenameState) Renamed)
-> Renamed -> ExceptT RenameError (State RenameState) Renamed
forall a b. (a -> b) -> a -> b
$ Index "tyvar" -> Renamed
Unifiable Index "tyvar"
index
        | Int
trueLevel Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 -> Renamed -> ExceptT RenameError (State RenameState) Renamed
forall a. a -> ExceptT RenameError (State RenameState) a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Renamed -> ExceptT RenameError (State RenameState) Renamed)
-> Renamed -> ExceptT RenameError (State RenameState) Renamed
forall a b. (a -> b) -> a -> b
$ Int -> Index "tyvar" -> Renamed
Rigid Int
trueLevel Index "tyvar"
index
        | Bool
otherwise -> Renamed -> ExceptT RenameError (State RenameState) Renamed
forall a. a -> ExceptT RenameError (State RenameState) a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Renamed -> ExceptT RenameError (State RenameState) Renamed)
-> Renamed -> ExceptT RenameError (State RenameState) Renamed
forall a b. (a -> b) -> a -> b
$ Word64 -> Int -> Index "tyvar" -> Renamed
Wildcard Word64
uniqueScopeId Int
trueLevel Index "tyvar"
index
  where
    checkVarIxExists :: Int -> Word32 -> Bool
    checkVarIxExists :: Int -> Word32 -> Bool
checkVarIxExists Int
i Word32
wCount = Int -> Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i Word32 -> Word32 -> Bool
forall a. Ord a => a -> a -> Bool
< Word32
wCount

-- Helpers

-- Given a number of abstractions bound by a scope, modify the state to track
-- that scope.
stepUpScope :: Count "tyvar" -> RenameState -> RenameState
stepUpScope :: Count "tyvar" -> RenameState -> RenameState
stepUpScope Count "tyvar"
abses RenameState
x =
  let fresh :: Word64
fresh = Optic' A_Lens NoIx RenameState Word64 -> RenameState -> Word64
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view Optic' A_Lens NoIx RenameState Word64
#idSource RenameState
x
      absesW :: Word32
absesW = Optic' A_Lens NoIx (Count "tyvar") Word32
-> Count "tyvar" -> Word32
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view Optic' A_Lens NoIx (Count "tyvar") Word32
forall (ofWhat :: Symbol). Lens' (Count ofWhat) Word32
wordCount Count "tyvar"
abses
      -- Label (speculatively) the current scope 'step' with a unique value.
      entry :: (Word32, Word64)
entry = (Word32
absesW, Word64
fresh)
   in -- Ensure that our source of fresh identifiers is incremented
      Optic
  A_Lens
  NoIx
  RenameState
  RenameState
  (Vector (Word32, Word64))
  (Vector (Word32, Word64))
-> (Vector (Word32, Word64) -> Vector (Word32, Word64))
-> RenameState
-> RenameState
forall k (is :: IxList) s t a b.
Is k A_Setter =>
Optic k is s t a b -> (a -> b) -> s -> t
over Optic
  A_Lens
  NoIx
  RenameState
  RenameState
  (Vector (Word32, Word64))
  (Vector (Word32, Word64))
#tracker ((Word32, Word64)
-> Vector (Word32, Word64) -> Vector (Word32, Word64)
forall a. a -> Vector a -> Vector a
Vector.cons (Word32, Word64)
entry) (RenameState -> RenameState)
-> (RenameState -> RenameState) -> RenameState -> RenameState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Optic' A_Lens NoIx RenameState Word64
-> Word64 -> RenameState -> RenameState
forall k (is :: IxList) s t a b.
Is k A_Setter =>
Optic k is s t a b -> b -> s -> t
set Optic' A_Lens NoIx RenameState Word64
#idSource (Word64
fresh Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
1) (RenameState -> RenameState) -> RenameState -> RenameState
forall a b. (a -> b) -> a -> b
$ RenameState
x

-- Stop tracking the last scope we added.
--
-- Note that, while we 'throw away' the information about (used) variables in
-- the scope, we do _not_ roll back the `idSource`. This is in fact why we have
-- to be in `State` rather than `Reader`: that change has to be persistent to
-- achieve our goal of renaming wildcards.
dropDownScope :: RenameState -> RenameState
dropDownScope :: RenameState -> RenameState
dropDownScope = Optic
  A_Lens
  NoIx
  RenameState
  RenameState
  (Vector (Word32, Word64))
  (Vector (Word32, Word64))
-> (Vector (Word32, Word64) -> Vector (Word32, Word64))
-> RenameState
-> RenameState
forall k (is :: IxList) s t a b.
Is k A_Setter =>
Optic k is s t a b -> (a -> b) -> s -> t
over Optic
  A_Lens
  NoIx
  RenameState
  RenameState
  (Vector (Word32, Word64))
  (Vector (Word32, Word64))
#tracker Vector (Word32, Word64) -> Vector (Word32, Word64)
forall a. Vector a -> Vector a
Vector.tail