-- editorconfig-checker-disable-file
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE ScopedTypeVariables #-}

module UntypedPlutusCore.Check.Scope (checkScope, ScopeCheckMode (..)) where

import Control.Lens hiding (index)
import UntypedPlutusCore.Core.Type as UPLC
import UntypedPlutusCore.DeBruijn as UPLC

import Control.Monad (unless)
import Control.Monad.Except (MonadError, throwError)

{- The scope check used to have a bug where it didn't traverse the subterms of
 - case and constr -}
data ScopeCheckMode
  = NoCaseConstr
  | Full

{-| A pass to check that the input term:
1) does not contain free variables and
2) that all binders are set to debruijn index 0.

Feeding the result of the debruijnification to this function is expected to pass.

On the other hand, because of (2), this pass is
stricter than the undebruijnification's (indirect)
scope-checking, see Note [DeBruijn indices of Binders].

Inlining this function makes a big difference,
since it will usually be called in a context where all the type variables are known.
That then means that GHC can optimize go locally in a completely monomorphic setting, which helps a lot. -}
checkScope
  :: forall m name uni fun a
   . (HasIndex name, MonadError FreeVariableError m)
  => ScopeCheckMode
  -> UPLC.Term name uni fun a
  -> m ()
checkScope :: forall (m :: * -> *) name (uni :: * -> *) fun a.
(HasIndex name, MonadError FreeVariableError m) =>
ScopeCheckMode -> Term name uni fun a -> m ()
checkScope ScopeCheckMode
mode = Word -> Term name uni fun a -> m ()
go Word
0
  where
    -- the current level as a reader value
    go :: Word -> UPLC.Term name uni fun a -> m ()
    go :: Word -> Term name uni fun a -> m ()
go !Word
lvl = \case
      Var a
_ name
n -> do
        let i :: Index
i = name
n name -> Getting Index name Index -> Index
forall s a. s -> Getting a s a -> a
^. Getting Index name Index
forall a. HasIndex a => Lens' a Index
Lens' name Index
index
        -- var index must be larger than 0
        -- var index must be LEQ to the current level
        Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Index
i Index -> Index -> Bool
forall a. Ord a => a -> a -> Bool
> Index
0 Bool -> Bool -> Bool
&& Index -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral Index
i Word -> Word -> Bool
forall a. Ord a => a -> a -> Bool
<= Word
lvl) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
          FreeVariableError -> m ()
forall a. FreeVariableError -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (FreeVariableError -> m ()) -> FreeVariableError -> m ()
forall a b. (a -> b) -> a -> b
$
            Index -> FreeVariableError
FreeIndex Index
i
      LamAbs a
_ name
binder Term name uni fun a
t -> do
        let bIx :: Index
bIx = name
binder name -> Getting Index name Index -> Index
forall s a. s -> Getting a s a -> a
^. Getting Index name Index
forall a. HasIndex a => Lens' a Index
Lens' name Index
index
        -- binder index must be equal to 0
        Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Index
bIx Index -> Index -> Bool
forall a. Eq a => a -> a -> Bool
== Index
0) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
          FreeVariableError -> m ()
forall a. FreeVariableError -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (FreeVariableError -> m ()) -> FreeVariableError -> m ()
forall a b. (a -> b) -> a -> b
$
            Index -> FreeVariableError
FreeIndex Index
bIx
        Word -> Term name uni fun a -> m ()
go (Word
lvl Word -> Word -> Word
forall a. Num a => a -> a -> a
+ Word
1) Term name uni fun a
t
      Apply a
_ Term name uni fun a
t1 Term name uni fun a
t2 -> Word -> Term name uni fun a -> m ()
go Word
lvl Term name uni fun a
t1 m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Word -> Term name uni fun a -> m ()
go Word
lvl Term name uni fun a
t2
      Force a
_ Term name uni fun a
t -> Word -> Term name uni fun a -> m ()
go Word
lvl Term name uni fun a
t
      Delay a
_ Term name uni fun a
t -> Word -> Term name uni fun a -> m ()
go Word
lvl Term name uni fun a
t
      Constr a
_ Word64
_ [Term name uni fun a]
ts ->
        case ScopeCheckMode
mode of
          ScopeCheckMode
Full -> (Term name uni fun a -> m ()) -> [Term name uni fun a] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Word -> Term name uni fun a -> m ()
go Word
lvl) [Term name uni fun a]
ts
          ScopeCheckMode
NoCaseConstr -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      Case a
_ Term name uni fun a
t Vector (Term name uni fun a)
ts ->
        case ScopeCheckMode
mode of
          ScopeCheckMode
Full -> Word -> Term name uni fun a -> m ()
go Word
lvl Term name uni fun a
t m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Term name uni fun a -> m ())
-> Vector (Term name uni fun a) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Word -> Term name uni fun a -> m ()
go Word
lvl) Vector (Term name uni fun a)
ts
          ScopeCheckMode
NoCaseConstr -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      Constant a
_ Some (ValueOf uni)
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      Error a
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      Builtin a
_ fun
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
{-# INLINE checkScope #-}