{-# 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 (unless)
import Control.Monad.Error.Lens
import Control.Monad.Except (MonadError)
{-# 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 :: forall e (m :: * -> *) name (uni :: * -> *) fun a.
(HasIndex name, MonadError e m, AsFreeVariableError e) =>
Term name uni fun a -> m ()
checkScope = Word -> Term name uni fun a -> m ()
go Word
0
where
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
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
Prism' e 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
Lens' name Index
index
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
Prism' e 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 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
Term name uni fun a
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()