{-# LANGUAGE BangPatterns        #-}
{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE ScopedTypeVariables #-}
module UntypedPlutusCore.Check.Scope (checkScope) where

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

import Control.Monad.Error.Lens
import Control.Monad.Except

{- | 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.
-}
{-# INLINE checkScope #-}
checkScope :: forall e m name uni fun a.
             (HasIndex name, MonadError e m, AsFreeVariableError e)
           => UPLC.Term name uni fun a
           -> m ()
checkScope :: Term name uni fun a -> m ()
checkScope = 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
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
$
                AReview e FreeVariableError -> FreeVariableError -> m ()
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview e FreeVariableError
forall r. AsFreeVariableError r => Prism' r FreeVariableError
_FreeVariableError (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
bindername -> 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
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
$
                AReview e FreeVariableError -> FreeVariableError -> m ()
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview e FreeVariableError
forall r. AsFreeVariableError r => Prism' r FreeVariableError
_FreeVariableError (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
lvlWord -> 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 (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
        Term name uni fun a
_             -> () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()