module Covenant.Internal.Rename
  ( RenameM,
    RenameError (..),
    runRenameM,
    renameValT,
    renameCompT,
    undoRename,
  )
where

import Control.Monad (unless)
import Control.Monad.Except
  ( ExceptT,
    runExceptT,
    throwError,
  )
import Control.Monad.Reader
  ( Reader,
    asks,
    local,
    runReader,
  )
import Control.Monad.State.Strict
  ( State,
    evalState,
    gets,
    modify,
  )
import Covenant.DeBruijn (DeBruijn (S, Z), asInt)
import Covenant.Index (Count, Index, intCount, intIndex)
import Covenant.Internal.Type
  ( AbstractTy (BoundAt),
    CompT (CompT),
    CompTBody (CompTBody),
    Renamed (Rigid, Unifiable, Wildcard),
    ValT (Abstraction, BuiltinFlat, ThunkT),
  )
import Data.Coerce (coerce)
import Data.Kind (Type)
import Data.Tuple.Optics (_1)
import Data.Vector (Vector)
import Data.Vector qualified as Vector
import Data.Vector.NonEmpty qualified as NonEmpty
import Data.Word (Word64)
import Optics.Core
  ( A_Lens,
    LabelOptic (labelOptic),
    ix,
    lens,
    over,
    review,
    set,
    to,
    view,
    (%),
  )

-- Used during renaming. Contains a source of fresh indices for wildcards, as
-- well as tracking:
--
-- 1. How many variables are bound by each scope;
-- 2. Which of these variables have been noted as used; and
-- 3. A unique identifier for each scope (for wildcards).
data RenameState = RenameState Word64 (Vector (Vector Bool, 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 Vector (Vector Bool, Word64)
_) -> a
Word64
x)
      (\(RenameState Word64
_ Vector (Vector Bool, Word64)
y) b
x' -> Word64 -> Vector (Vector Bool, Word64) -> RenameState
RenameState b
Word64
x' Vector (Vector Bool, Word64)
y)

-- The 'outer' vector represents a stack of scopes. Each entry is a combination
-- of a vector of used variables (length is equal to the number of variables
-- bound by that scope), together with a unique identifier not only for that
-- scope, but also the `step` into that scope, as required by wildcard renaming.
instance
  (k ~ A_Lens, a ~ Vector (Vector Bool, Word64), b ~ Vector (Vector Bool, 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
_ Vector (Vector Bool, Word64)
y) -> a
Vector (Vector Bool, Word64)
y)
      (\(RenameState Word64
x Vector (Vector Bool, Word64)
_) b
y' -> Word64 -> Vector (Vector Bool, Word64) -> RenameState
RenameState Word64
x b
Vector (Vector Bool, Word64)
y')

-- | Ways in which the renamer can fail.
--
-- @since 1.0.0
data RenameError
  = -- | An attempt to reference an abstraction in a scope where this
    -- abstraction doesn't exist. First field is the true level, second is
    -- the index that was requested.
    --
    -- @since 1.0.0
    InvalidAbstractionReference Int (Index "tyvar")
  | -- | A value type specifies an abstraction that never gets used
    -- anywhere. For example, the type @forall a b . [a]@ has @b@
    -- irrelevant.
    --
    -- @since 1.0.0
    IrrelevantAbstraction
  | -- | A computation type specifies an abstraction which is not used
    -- by any argument. For example, the type @forall a b . a -> !(b -> !a)@
    -- has @b@ undetermined.
    --
    -- @since 1.0.0
    UndeterminedAbstraction
  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)

-- | 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))

-- | Execute a renaming computation.
--
-- @since 1.0.0
runRenameM ::
  forall (a :: Type).
  RenameM a ->
  Either RenameError a
runRenameM :: forall a. RenameM a -> Either RenameError a
runRenameM (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 (Vector Bool, Word64) -> RenameState)
-> Vector (Vector Bool, Word64)
-> Either RenameError a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word64 -> Vector (Vector Bool, Word64) -> RenameState
RenameState Word64
0 (Vector (Vector Bool, Word64) -> Either RenameError a)
-> Vector (Vector Bool, Word64) -> Either RenameError a
forall a b. (a -> b) -> a -> b
$ Vector (Vector Bool, Word64)
forall a. Vector a
Vector.empty

-- | 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 that we don't overdetermine anything
  Vector Bool
ourAbstractions <- (RenameState -> Vector Bool)
-> ExceptT RenameError (State RenameState) (Vector Bool)
forall s (m :: Type -> Type) a. MonadState s m => (s -> a) -> m a
gets (Optic' A_Getter NoIx RenameState (Vector Bool)
-> RenameState -> Vector Bool
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 (Vector Bool, Word64))
  (Vector (Vector Bool, Word64))
#tracker Optic
  A_Lens
  NoIx
  RenameState
  RenameState
  (Vector (Vector Bool, Word64))
  (Vector (Vector Bool, Word64))
-> Optic
     A_Getter
     NoIx
     (Vector (Vector Bool, Word64))
     (Vector (Vector Bool, Word64))
     (Vector Bool, Word64)
     (Vector Bool, Word64)
-> Optic
     A_Getter
     NoIx
     RenameState
     RenameState
     (Vector Bool, Word64)
     (Vector Bool, Word64)
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 (Vector Bool, Word64) -> (Vector Bool, Word64))
-> Optic
     A_Getter
     NoIx
     (Vector (Vector Bool, Word64))
     (Vector (Vector Bool, Word64))
     (Vector Bool, Word64)
     (Vector Bool, Word64)
forall s a. (s -> a) -> Getter s a
to Vector (Vector Bool, Word64) -> (Vector Bool, Word64)
forall a. Vector a -> a
Vector.head Optic
  A_Getter
  NoIx
  RenameState
  RenameState
  (Vector Bool, Word64)
  (Vector Bool, Word64)
-> Optic
     A_Lens
     NoIx
     (Vector Bool, Word64)
     (Vector Bool, Word64)
     (Vector Bool)
     (Vector Bool)
-> Optic' A_Getter NoIx RenameState (Vector Bool)
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
% Optic
  A_Lens
  NoIx
  (Vector Bool, Word64)
  (Vector Bool, Word64)
  (Vector Bool)
  (Vector Bool)
forall s t a b. Field1 s t a b => Lens s t a b
_1))
  Bool
-> ExceptT RenameError (State RenameState) ()
-> ExceptT RenameError (State RenameState) ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless (Vector Bool -> Bool
Vector.and Vector Bool
ourAbstractions) (RenameError -> ExceptT RenameError (State RenameState) ()
forall a. RenameError -> ExceptT RenameError (State RenameState) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError RenameError
UndeterminedAbstraction)
  -- 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

-- 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.
undoRename :: ValT Renamed -> ValT AbstractTy
undoRename :: ValT Renamed -> ValT AbstractTy
undoRename ValT Renamed
t = Reader Int (ValT AbstractTy) -> Int -> ValT AbstractTy
forall r a. Reader r a -> r -> a
runReader (ValT Renamed -> Reader Int (ValT AbstractTy)
go ValT Renamed
t) Int
1
  where
    go :: ValT Renamed -> Reader Int (ValT AbstractTy)
    go :: ValT Renamed -> Reader Int (ValT AbstractTy)
go = \case
      Abstraction Renamed
t' ->
        AbstractTy -> ValT AbstractTy
forall a. a -> ValT a
Abstraction (AbstractTy -> ValT AbstractTy)
-> ReaderT Int Identity AbstractTy -> Reader Int (ValT AbstractTy)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> case Renamed
t' of
          Unifiable Index "tyvar"
index -> DeBruijn -> Index "tyvar" -> AbstractTy
BoundAt (DeBruijn -> Index "tyvar" -> AbstractTy)
-> ReaderT Int Identity DeBruijn
-> ReaderT Int Identity (Index "tyvar" -> AbstractTy)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> ReaderT Int Identity DeBruijn
trueLevelToDB Int
1 ReaderT Int Identity (Index "tyvar" -> AbstractTy)
-> ReaderT Int Identity (Index "tyvar")
-> ReaderT Int Identity AbstractTy
forall a b.
ReaderT Int Identity (a -> b)
-> ReaderT Int Identity a -> ReaderT Int Identity b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Index "tyvar" -> ReaderT Int Identity (Index "tyvar")
forall a. a -> ReaderT Int Identity a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Index "tyvar"
index
          Rigid Int
trueLevel Index "tyvar"
index -> DeBruijn -> Index "tyvar" -> AbstractTy
BoundAt (DeBruijn -> Index "tyvar" -> AbstractTy)
-> ReaderT Int Identity DeBruijn
-> ReaderT Int Identity (Index "tyvar" -> AbstractTy)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> ReaderT Int Identity DeBruijn
trueLevelToDB Int
trueLevel ReaderT Int Identity (Index "tyvar" -> AbstractTy)
-> ReaderT Int Identity (Index "tyvar")
-> ReaderT Int Identity AbstractTy
forall a b.
ReaderT Int Identity (a -> b)
-> ReaderT Int Identity a -> ReaderT Int Identity b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Index "tyvar" -> ReaderT Int Identity (Index "tyvar")
forall a. a -> ReaderT Int Identity a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Index "tyvar"
index
          Wildcard Word64
_ Int
trueLevel Index "tyvar"
index -> DeBruijn -> Index "tyvar" -> AbstractTy
BoundAt (DeBruijn -> Index "tyvar" -> AbstractTy)
-> ReaderT Int Identity DeBruijn
-> ReaderT Int Identity (Index "tyvar" -> AbstractTy)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> ReaderT Int Identity DeBruijn
trueLevelToDB Int
trueLevel ReaderT Int Identity (Index "tyvar" -> AbstractTy)
-> ReaderT Int Identity (Index "tyvar")
-> ReaderT Int Identity AbstractTy
forall a b.
ReaderT Int Identity (a -> b)
-> ReaderT Int Identity a -> ReaderT Int Identity b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Index "tyvar" -> ReaderT Int Identity (Index "tyvar")
forall a. a -> ReaderT Int Identity a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure 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)
-> ReaderT Int Identity (NonEmptyVector (ValT AbstractTy))
-> Reader Int (ValT AbstractTy)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int -> Int)
-> ReaderT Int Identity (NonEmptyVector (ValT AbstractTy))
-> ReaderT Int Identity (NonEmptyVector (ValT AbstractTy))
forall a.
(Int -> Int) -> ReaderT Int Identity a -> ReaderT Int Identity a
forall r (m :: Type -> Type) a.
MonadReader r m =>
(r -> r) -> m a -> m a
local (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) ((ValT Renamed -> Reader Int (ValT AbstractTy))
-> NonEmptyVector (ValT Renamed)
-> ReaderT Int Identity (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 -> Reader Int (ValT AbstractTy)
go NonEmptyVector (ValT Renamed)
xs)
      BuiltinFlat BuiltinFlatT
t' -> ValT AbstractTy -> Reader Int (ValT AbstractTy)
forall a. a -> ReaderT Int Identity a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (ValT AbstractTy -> Reader Int (ValT AbstractTy))
-> (BuiltinFlatT -> ValT AbstractTy)
-> BuiltinFlatT
-> Reader Int (ValT AbstractTy)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinFlatT -> ValT AbstractTy
forall a. BuiltinFlatT -> ValT a
BuiltinFlat (BuiltinFlatT -> Reader Int (ValT AbstractTy))
-> BuiltinFlatT -> Reader Int (ValT AbstractTy)
forall a b. (a -> b) -> a -> b
$ BuiltinFlatT
t'

-- Helpers

trueLevelToDB :: Int -> Reader Int DeBruijn
trueLevelToDB :: Int -> ReaderT Int Identity DeBruijn
trueLevelToDB Int
trueLevel = (Int -> DeBruijn) -> ReaderT Int Identity DeBruijn
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
asks (Int -> DeBruijn
go (Int -> DeBruijn) -> (Int -> Int) -> Int -> DeBruijn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> Int
forall a. Num a => a -> a -> a
subtract Int
trueLevel)
  where
    go :: Int -> DeBruijn
    go :: Int -> DeBruijn
go = \case
      Int
0 -> DeBruijn
Z
      Int
n -> DeBruijn -> DeBruijn
S (DeBruijn -> DeBruijn) -> (Int -> DeBruijn) -> Int -> DeBruijn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> DeBruijn
go (Int -> DeBruijn) -> Int -> DeBruijn
forall a b. (a -> b) -> a -> b
$ Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1

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
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 (Vector Bool, Word64))
  (Vector (Vector Bool, Word64))
#tracker Optic
  A_Lens
  NoIx
  RenameState
  RenameState
  (Vector (Vector Bool, Word64))
  (Vector (Vector Bool, Word64))
-> Optic
     A_Getter
     NoIx
     (Vector (Vector Bool, Word64))
     (Vector (Vector Bool, 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 (Vector Bool, Word64) -> Int)
-> Optic
     A_Getter
     NoIx
     (Vector (Vector Bool, Word64))
     (Vector (Vector Bool, Word64))
     Int
     Int
forall s a. (s -> a) -> Getter s a
to Vector (Vector Bool, Word64) -> Int
forall a. Vector a -> Int
Vector.length) RenameState
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- DeBruijn -> Int
asInt DeBruijn
scope)
  Maybe (Vector Bool, Word64)
scopeInfo <- (RenameState -> Maybe (Vector Bool, Word64))
-> ExceptT
     RenameError (State RenameState) (Maybe (Vector Bool, Word64))
forall s (m :: Type -> Type) a. MonadState s m => (s -> a) -> m a
gets (\RenameState
x -> Optic
  A_Lens
  NoIx
  RenameState
  RenameState
  (Vector (Vector Bool, Word64))
  (Vector (Vector Bool, Word64))
-> RenameState -> Vector (Vector Bool, 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 (Vector Bool, Word64))
  (Vector (Vector Bool, Word64))
#tracker RenameState
x Vector (Vector Bool, Word64) -> Int -> Maybe (Vector Bool, Word64)
forall a. Vector a -> Int -> Maybe a
Vector.!? DeBruijn -> Int
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 (Vector Bool, Word64)
scopeInfo of
    -- This variable is bound in a scope that encloses the renaming scope. Thus,
    -- the variable is rigid.
    Maybe (Vector Bool, Word64)
Nothing -> 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)
-> (Index "tyvar" -> Renamed)
-> Index "tyvar"
-> ExceptT RenameError (State RenameState) Renamed
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Index "tyvar" -> Renamed
Rigid 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 (Vector Bool
occursTracker, Word64
uniqueScopeId) -> case Vector Bool
occursTracker Vector Bool -> Int -> Maybe Bool
forall a. Vector a -> Int -> Maybe a
Vector.!? Int
asIntIx of
      Maybe Bool
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
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
      Just Bool
beenUsed -> do
        -- Note that this variable has occurred
        Bool
-> ExceptT RenameError (State RenameState) ()
-> ExceptT RenameError (State RenameState) ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless Bool
beenUsed ((RenameState -> RenameState)
-> ExceptT RenameError (State RenameState) ()
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
modify (DeBruijn -> Index "tyvar" -> RenameState -> RenameState
noteUsed DeBruijn
scope Index "tyvar"
index))
        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
$
          if Int
trueLevel Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1
            -- This is a unifiable variable
            then Index "tyvar" -> Renamed
Unifiable Index "tyvar"
index
            -- This is a wildcard variable
            else Word64 -> Int -> Index "tyvar" -> Renamed
Wildcard Word64
uniqueScopeId Int
trueLevel Index "tyvar"
index

-- 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
      absesI :: Int
absesI = Optic' A_Prism NoIx Int (Count "tyvar") -> Count "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 (Count "tyvar")
forall (ofWhat :: Symbol). Prism' Int (Count ofWhat)
intCount Count "tyvar"
abses
      -- Label (speculatively) the current scope 'step' with a unique value.
      entry :: (Vector Bool, Word64)
entry = (Int -> Bool -> Vector Bool
forall a. Int -> a -> Vector a
Vector.replicate Int
absesI Bool
False, Word64
fresh)
   in -- Ensure that our source of fresh identifiers is incremented
      Optic
  A_Lens
  NoIx
  RenameState
  RenameState
  (Vector (Vector Bool, Word64))
  (Vector (Vector Bool, Word64))
-> (Vector (Vector Bool, Word64) -> Vector (Vector Bool, 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 (Vector Bool, Word64))
  (Vector (Vector Bool, Word64))
#tracker ((Vector Bool, Word64)
-> Vector (Vector Bool, Word64) -> Vector (Vector Bool, Word64)
forall a. a -> Vector a -> Vector a
Vector.cons (Vector Bool, 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 (Vector Bool, Word64))
  (Vector (Vector Bool, Word64))
-> (Vector (Vector Bool, Word64) -> Vector (Vector Bool, 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 (Vector Bool, Word64))
  (Vector (Vector Bool, Word64))
#tracker Vector (Vector Bool, Word64) -> Vector (Vector Bool, Word64)
forall a. Vector a -> Vector a
Vector.tail

-- Given a pair of DeBruijn index and positional index for a variable, note that
-- we've seen this variable.
noteUsed :: DeBruijn -> Index "tyvar" -> RenameState -> RenameState
noteUsed :: DeBruijn -> Index "tyvar" -> RenameState -> RenameState
noteUsed DeBruijn
scope Index "tyvar"
index =
  Optic
  An_AffineTraversal
  NoIx
  RenameState
  RenameState
  (IxValue (Vector Bool))
  Bool
-> Bool -> 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
  RenameState
  (Vector (Vector Bool, Word64))
  (Vector (Vector Bool, Word64))
#tracker Optic
  A_Lens
  NoIx
  RenameState
  RenameState
  (Vector (Vector Bool, Word64))
  (Vector (Vector Bool, Word64))
-> Optic
     (IxKind (Vector (Vector Bool, Word64)))
     NoIx
     (Vector (Vector Bool, Word64))
     (Vector (Vector Bool, Word64))
     (IxValue (Vector (Vector Bool, Word64)))
     (IxValue (Vector (Vector Bool, Word64)))
-> Optic
     An_AffineTraversal
     NoIx
     RenameState
     RenameState
     (IxValue (Vector (Vector Bool, Word64)))
     (IxValue (Vector (Vector Bool, Word64)))
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
% Index (Vector (Vector Bool, Word64))
-> Optic
     (IxKind (Vector (Vector Bool, Word64)))
     NoIx
     (Vector (Vector Bool, Word64))
     (Vector (Vector Bool, Word64))
     (IxValue (Vector (Vector Bool, Word64)))
     (IxValue (Vector (Vector Bool, Word64)))
forall m. Ixed m => Index m -> Optic' (IxKind m) NoIx m (IxValue m)
ix (DeBruijn -> Int
asInt DeBruijn
scope) Optic
  An_AffineTraversal
  NoIx
  RenameState
  RenameState
  (IxValue (Vector (Vector Bool, Word64)))
  (IxValue (Vector (Vector Bool, Word64)))
-> Optic
     A_Lens
     NoIx
     (IxValue (Vector (Vector Bool, Word64)))
     (IxValue (Vector (Vector Bool, Word64)))
     (Vector Bool)
     (Vector Bool)
-> Optic
     An_AffineTraversal
     NoIx
     RenameState
     RenameState
     (Vector Bool)
     (Vector Bool)
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
% Optic
  A_Lens
  NoIx
  (IxValue (Vector (Vector Bool, Word64)))
  (IxValue (Vector (Vector Bool, Word64)))
  (Vector Bool)
  (Vector Bool)
forall s t a b. Field1 s t a b => Lens s t a b
_1 Optic
  An_AffineTraversal
  NoIx
  RenameState
  RenameState
  (Vector Bool)
  (Vector Bool)
-> Optic
     (IxKind (Vector Bool))
     NoIx
     (Vector Bool)
     (Vector Bool)
     (IxValue (Vector Bool))
     Bool
-> Optic
     An_AffineTraversal
     NoIx
     RenameState
     RenameState
     (IxValue (Vector Bool))
     Bool
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
% Index (Vector Bool)
-> Optic'
     (IxKind (Vector Bool)) NoIx (Vector Bool) (IxValue (Vector Bool))
forall m. Ixed m => Index m -> Optic' (IxKind m) NoIx m (IxValue m)
ix (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)) Bool
True