{-# LANGUAGE DerivingStrategies    #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings     #-}
-- | Support for using de Bruijn indices for term names.
module UntypedPlutusCore.DeBruijn
    ( Index (..)
    , HasIndex (..)
    , DeBruijn (..)
    , NamedDeBruijn (..)
    , FakeNamedDeBruijn (..)
    , FreeVariableError (..)
    , AsFreeVariableError (..)
    , deBruijnTerm
    , unDeBruijnTerm
    , unNameDeBruijn
    , fakeNameDeBruijn
    -- * unsafe api, use with care
    , deBruijnTermWith
    , unDeBruijnTermWith
    , freeIndexAsConsistentLevel
    , deBruijnInitIndex
    ) where

import PlutusCore.DeBruijn.Internal

import PlutusCore.Name
import PlutusCore.Quote
import UntypedPlutusCore.Core

import Control.Lens hiding (Index, Level, index)
import Control.Monad.Except
import Control.Monad.Reader

{- Note [Comparison with typed deBruijn conversion]
This module is just a boring port of the typed version.
-}

-- | Convert a 'Term' with 'Name's into a 'Term' with 'DeBruijn's.
-- Will throw an error if a free variable is encountered.
deBruijnTerm
    :: (AsFreeVariableError e, MonadError e m)
    => Term Name uni fun ann -> m (Term NamedDeBruijn uni fun ann)
deBruijnTerm :: Term Name uni fun ann -> m (Term NamedDeBruijn uni fun ann)
deBruijnTerm = (Unique -> ReaderT Levels m Index)
-> Term Name uni fun ann -> m (Term NamedDeBruijn uni fun ann)
forall (m :: * -> *) (uni :: * -> *) fun ann.
Monad m =>
(Unique -> ReaderT Levels m Index)
-> Term Name uni fun ann -> m (Term NamedDeBruijn uni fun ann)
deBruijnTermWith Unique -> ReaderT Levels m Index
forall e (m :: * -> *).
(AsFreeVariableError e, MonadError e m) =>
Unique -> m Index
freeUniqueThrow

-- | Convert a 'Term' with 'DeBruijn's into a 'Term' with 'Name's.
-- Will throw an error if a free variable is encountered.
unDeBruijnTerm
    :: (MonadQuote m, AsFreeVariableError e, MonadError e m)
    => Term NamedDeBruijn uni fun ann -> m (Term Name uni fun ann)
unDeBruijnTerm :: Term NamedDeBruijn uni fun ann -> m (Term Name uni fun ann)
unDeBruijnTerm = (Index -> ReaderT Levels m Unique)
-> Term NamedDeBruijn uni fun ann -> m (Term Name uni fun ann)
forall (m :: * -> *) (uni :: * -> *) fun ann.
MonadQuote m =>
(Index -> ReaderT Levels m Unique)
-> Term NamedDeBruijn uni fun ann -> m (Term Name uni fun ann)
unDeBruijnTermWith Index -> ReaderT Levels m Unique
forall e (m :: * -> *).
(AsFreeVariableError e, MonadError e m) =>
Index -> m Unique
freeIndexThrow

-- | Takes a "handler" function to execute when encountering free variables.
deBruijnTermWith
    :: Monad m
    => (Unique -> ReaderT Levels m Index)
    -> Term Name uni fun ann
    -> m (Term NamedDeBruijn uni fun ann)
deBruijnTermWith :: (Unique -> ReaderT Levels m Index)
-> Term Name uni fun ann -> m (Term NamedDeBruijn uni fun ann)
deBruijnTermWith = (ReaderT Levels m (Term NamedDeBruijn uni fun ann)
-> m (Term NamedDeBruijn uni fun ann)
forall (m :: * -> *) a. ReaderT Levels m a -> m a
runDeBruijnT (ReaderT Levels m (Term NamedDeBruijn uni fun ann)
 -> m (Term NamedDeBruijn uni fun ann))
-> (Term Name uni fun ann
    -> ReaderT Levels m (Term NamedDeBruijn uni fun ann))
-> Term Name uni fun ann
-> m (Term NamedDeBruijn uni fun ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((Term Name uni fun ann
  -> ReaderT Levels m (Term NamedDeBruijn uni fun ann))
 -> Term Name uni fun ann -> m (Term NamedDeBruijn uni fun ann))
-> ((Unique -> ReaderT Levels m Index)
    -> Term Name uni fun ann
    -> ReaderT Levels m (Term NamedDeBruijn uni fun ann))
-> (Unique -> ReaderT Levels m Index)
-> Term Name uni fun ann
-> m (Term NamedDeBruijn uni fun ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Unique -> ReaderT Levels m Index)
-> Term Name uni fun ann
-> ReaderT Levels m (Term NamedDeBruijn uni fun ann)
forall (m :: * -> *) (uni :: * -> *) fun ann.
MonadReader Levels m =>
(Unique -> m Index)
-> Term Name uni fun ann -> m (Term NamedDeBruijn uni fun ann)
deBruijnTermWithM

-- | Takes a "handler" function to execute when encountering free variables.
unDeBruijnTermWith
    :: MonadQuote m
    => (Index -> ReaderT Levels m Unique)
    -> Term NamedDeBruijn uni fun ann
    -> m (Term Name uni fun ann)
unDeBruijnTermWith :: (Index -> ReaderT Levels m Unique)
-> Term NamedDeBruijn uni fun ann -> m (Term Name uni fun ann)
unDeBruijnTermWith = (ReaderT Levels m (Term Name uni fun ann)
-> m (Term Name uni fun ann)
forall (m :: * -> *) a. ReaderT Levels m a -> m a
runDeBruijnT (ReaderT Levels m (Term Name uni fun ann)
 -> m (Term Name uni fun ann))
-> (Term NamedDeBruijn uni fun ann
    -> ReaderT Levels m (Term Name uni fun ann))
-> Term NamedDeBruijn uni fun ann
-> m (Term Name uni fun ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((Term NamedDeBruijn uni fun ann
  -> ReaderT Levels m (Term Name uni fun ann))
 -> Term NamedDeBruijn uni fun ann -> m (Term Name uni fun ann))
-> ((Index -> ReaderT Levels m Unique)
    -> Term NamedDeBruijn uni fun ann
    -> ReaderT Levels m (Term Name uni fun ann))
-> (Index -> ReaderT Levels m Unique)
-> Term NamedDeBruijn uni fun ann
-> m (Term Name uni fun ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Index -> ReaderT Levels m Unique)
-> Term NamedDeBruijn uni fun ann
-> ReaderT Levels m (Term Name uni fun ann)
forall (m :: * -> *) (uni :: * -> *) fun ann.
(MonadReader Levels m, MonadQuote m) =>
(Index -> m Unique)
-> Term NamedDeBruijn uni fun ann -> m (Term Name uni fun ann)
unDeBruijnTermWithM

deBruijnTermWithM
    :: MonadReader Levels m
    => (Unique -> m Index)
    -> Term Name uni fun ann
    -> m (Term NamedDeBruijn uni fun ann)
deBruijnTermWithM :: (Unique -> m Index)
-> Term Name uni fun ann -> m (Term NamedDeBruijn uni fun ann)
deBruijnTermWithM Unique -> m Index
h = Term Name uni fun ann -> m (Term NamedDeBruijn uni fun ann)
forall (uni :: * -> *) fun ann.
Term Name uni fun ann -> m (Term NamedDeBruijn uni fun ann)
go
 where
   go :: Term Name uni fun ann -> m (Term NamedDeBruijn uni fun ann)
go = \case
       -- variable case
       Var ann
ann Name
n -> ann -> NamedDeBruijn -> Term NamedDeBruijn uni fun ann
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var ann
ann (NamedDeBruijn -> Term NamedDeBruijn uni fun ann)
-> m NamedDeBruijn -> m (Term NamedDeBruijn uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Unique -> m Index) -> Name -> m NamedDeBruijn
forall (m :: * -> *).
MonadReader Levels m =>
(Unique -> m Index) -> Name -> m NamedDeBruijn
nameToDeBruijn Unique -> m Index
h Name
n
       -- binder cases
       LamAbs ann
ann Name
n Term Name uni fun ann
t -> Name
-> m (Term NamedDeBruijn uni fun ann)
-> m (Term NamedDeBruijn uni fun ann)
forall (m :: * -> *) name unique a.
(MonadReader Levels m, HasUnique name unique) =>
name -> m a -> m a
declareUnique Name
n (m (Term NamedDeBruijn uni fun ann)
 -> m (Term NamedDeBruijn uni fun ann))
-> m (Term NamedDeBruijn uni fun ann)
-> m (Term NamedDeBruijn uni fun ann)
forall a b. (a -> b) -> a -> b
$ do
           NamedDeBruijn
n' <- (Unique -> m Index) -> Name -> m NamedDeBruijn
forall (m :: * -> *).
MonadReader Levels m =>
(Unique -> m Index) -> Name -> m NamedDeBruijn
nameToDeBruijn Unique -> m Index
h Name
n
           m (Term NamedDeBruijn uni fun ann)
-> m (Term NamedDeBruijn uni fun ann)
forall (m :: * -> *) a. MonadReader Levels m => m a -> m a
withScope (m (Term NamedDeBruijn uni fun ann)
 -> m (Term NamedDeBruijn uni fun ann))
-> m (Term NamedDeBruijn uni fun ann)
-> m (Term NamedDeBruijn uni fun ann)
forall a b. (a -> b) -> a -> b
$ ann
-> NamedDeBruijn
-> Term NamedDeBruijn uni fun ann
-> Term NamedDeBruijn uni fun ann
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs ann
ann NamedDeBruijn
n' (Term NamedDeBruijn uni fun ann -> Term NamedDeBruijn uni fun ann)
-> m (Term NamedDeBruijn uni fun ann)
-> m (Term NamedDeBruijn uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term Name uni fun ann -> m (Term NamedDeBruijn uni fun ann)
go Term Name uni fun ann
t
       -- boring recursive cases
       Apply ann
ann Term Name uni fun ann
t1 Term Name uni fun ann
t2 -> ann
-> Term NamedDeBruijn uni fun ann
-> Term NamedDeBruijn uni fun ann
-> Term NamedDeBruijn uni fun ann
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply ann
ann (Term NamedDeBruijn uni fun ann
 -> Term NamedDeBruijn uni fun ann
 -> Term NamedDeBruijn uni fun ann)
-> m (Term NamedDeBruijn uni fun ann)
-> m (Term NamedDeBruijn uni fun ann
      -> Term NamedDeBruijn uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term Name uni fun ann -> m (Term NamedDeBruijn uni fun ann)
go Term Name uni fun ann
t1 m (Term NamedDeBruijn uni fun ann
   -> Term NamedDeBruijn uni fun ann)
-> m (Term NamedDeBruijn uni fun ann)
-> m (Term NamedDeBruijn uni fun ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term Name uni fun ann -> m (Term NamedDeBruijn uni fun ann)
go Term Name uni fun ann
t2
       Delay ann
ann Term Name uni fun ann
t -> ann
-> Term NamedDeBruijn uni fun ann -> Term NamedDeBruijn uni fun ann
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay ann
ann (Term NamedDeBruijn uni fun ann -> Term NamedDeBruijn uni fun ann)
-> m (Term NamedDeBruijn uni fun ann)
-> m (Term NamedDeBruijn uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term Name uni fun ann -> m (Term NamedDeBruijn uni fun ann)
go Term Name uni fun ann
t
       Force ann
ann Term Name uni fun ann
t -> ann
-> Term NamedDeBruijn uni fun ann -> Term NamedDeBruijn uni fun ann
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force ann
ann (Term NamedDeBruijn uni fun ann -> Term NamedDeBruijn uni fun ann)
-> m (Term NamedDeBruijn uni fun ann)
-> m (Term NamedDeBruijn uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term Name uni fun ann -> m (Term NamedDeBruijn uni fun ann)
go Term Name uni fun ann
t
       -- boring non-recursive cases
       Constant ann
ann Some (ValueOf uni)
con -> Term NamedDeBruijn uni fun ann
-> m (Term NamedDeBruijn uni fun ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term NamedDeBruijn uni fun ann
 -> m (Term NamedDeBruijn uni fun ann))
-> Term NamedDeBruijn uni fun ann
-> m (Term NamedDeBruijn uni fun ann)
forall a b. (a -> b) -> a -> b
$ ann -> Some (ValueOf uni) -> Term NamedDeBruijn uni fun ann
forall name (uni :: * -> *) fun ann.
ann -> Some (ValueOf uni) -> Term name uni fun ann
Constant ann
ann Some (ValueOf uni)
con
       Builtin ann
ann fun
bn -> Term NamedDeBruijn uni fun ann
-> m (Term NamedDeBruijn uni fun ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term NamedDeBruijn uni fun ann
 -> m (Term NamedDeBruijn uni fun ann))
-> Term NamedDeBruijn uni fun ann
-> m (Term NamedDeBruijn uni fun ann)
forall a b. (a -> b) -> a -> b
$ ann -> fun -> Term NamedDeBruijn uni fun ann
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin ann
ann fun
bn
       Error ann
ann -> Term NamedDeBruijn uni fun ann
-> m (Term NamedDeBruijn uni fun ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term NamedDeBruijn uni fun ann
 -> m (Term NamedDeBruijn uni fun ann))
-> Term NamedDeBruijn uni fun ann
-> m (Term NamedDeBruijn uni fun ann)
forall a b. (a -> b) -> a -> b
$ ann -> Term NamedDeBruijn uni fun ann
forall name (uni :: * -> *) fun ann. ann -> Term name uni fun ann
Error ann
ann

-- | Takes a "handler" function to execute when encountering free variables.
unDeBruijnTermWithM
    :: (MonadReader Levels m, MonadQuote m)
    => (Index -> m Unique)
    -> Term NamedDeBruijn uni fun ann
    -> m (Term Name uni fun ann)
unDeBruijnTermWithM :: (Index -> m Unique)
-> Term NamedDeBruijn uni fun ann -> m (Term Name uni fun ann)
unDeBruijnTermWithM Index -> m Unique
h = Term NamedDeBruijn uni fun ann -> m (Term Name uni fun ann)
forall (uni :: * -> *) fun ann.
Term NamedDeBruijn uni fun ann -> m (Term Name uni fun ann)
go
  where
    go :: Term NamedDeBruijn uni fun ann -> m (Term Name uni fun ann)
go = \case
        -- variable case
        Var ann
ann NamedDeBruijn
n -> ann -> Name -> Term Name uni fun ann
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var ann
ann (Name -> Term Name uni fun ann)
-> m Name -> m (Term Name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Index -> m Unique) -> NamedDeBruijn -> m Name
forall (m :: * -> *).
MonadReader Levels m =>
(Index -> m Unique) -> NamedDeBruijn -> m Name
deBruijnToName Index -> m Unique
h NamedDeBruijn
n
        -- binder cases
        LamAbs ann
ann NamedDeBruijn
n Term NamedDeBruijn uni fun ann
t ->
            -- See NOTE: [DeBruijn indices of Binders]
            m (Term Name uni fun ann) -> m (Term Name uni fun ann)
forall (m :: * -> *) a.
(MonadReader Levels m, MonadQuote m) =>
m a -> m a
declareBinder (m (Term Name uni fun ann) -> m (Term Name uni fun ann))
-> m (Term Name uni fun ann) -> m (Term Name uni fun ann)
forall a b. (a -> b) -> a -> b
$ do
              Name
n' <- (Index -> m Unique) -> NamedDeBruijn -> m Name
forall (m :: * -> *).
MonadReader Levels m =>
(Index -> m Unique) -> NamedDeBruijn -> m Name
deBruijnToName Index -> m Unique
h (NamedDeBruijn -> m Name) -> NamedDeBruijn -> m Name
forall a b. (a -> b) -> a -> b
$ ASetter NamedDeBruijn NamedDeBruijn Index Index
-> Index -> NamedDeBruijn -> NamedDeBruijn
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter NamedDeBruijn NamedDeBruijn Index Index
forall a. HasIndex a => Lens' a Index
index Index
deBruijnInitIndex NamedDeBruijn
n
              m (Term Name uni fun ann) -> m (Term Name uni fun ann)
forall (m :: * -> *) a. MonadReader Levels m => m a -> m a
withScope (m (Term Name uni fun ann) -> m (Term Name uni fun ann))
-> m (Term Name uni fun ann) -> m (Term Name uni fun ann)
forall a b. (a -> b) -> a -> b
$ ann -> Name -> Term Name uni fun ann -> Term Name uni fun ann
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs ann
ann Name
n' (Term Name uni fun ann -> Term Name uni fun ann)
-> m (Term Name uni fun ann) -> m (Term Name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term NamedDeBruijn uni fun ann -> m (Term Name uni fun ann)
go Term NamedDeBruijn uni fun ann
t
        -- boring recursive cases
        Apply ann
ann Term NamedDeBruijn uni fun ann
t1 Term NamedDeBruijn uni fun ann
t2 -> ann
-> Term Name uni fun ann
-> Term Name uni fun ann
-> Term Name uni fun ann
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply ann
ann (Term Name uni fun ann
 -> Term Name uni fun ann -> Term Name uni fun ann)
-> m (Term Name uni fun ann)
-> m (Term Name uni fun ann -> Term Name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term NamedDeBruijn uni fun ann -> m (Term Name uni fun ann)
go Term NamedDeBruijn uni fun ann
t1 m (Term Name uni fun ann -> Term Name uni fun ann)
-> m (Term Name uni fun ann) -> m (Term Name uni fun ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term NamedDeBruijn uni fun ann -> m (Term Name uni fun ann)
go Term NamedDeBruijn uni fun ann
t2
        Delay ann
ann Term NamedDeBruijn uni fun ann
t -> ann -> Term Name uni fun ann -> Term Name uni fun ann
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay ann
ann (Term Name uni fun ann -> Term Name uni fun ann)
-> m (Term Name uni fun ann) -> m (Term Name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term NamedDeBruijn uni fun ann -> m (Term Name uni fun ann)
go Term NamedDeBruijn uni fun ann
t
        Force ann
ann Term NamedDeBruijn uni fun ann
t -> ann -> Term Name uni fun ann -> Term Name uni fun ann
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force ann
ann (Term Name uni fun ann -> Term Name uni fun ann)
-> m (Term Name uni fun ann) -> m (Term Name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term NamedDeBruijn uni fun ann -> m (Term Name uni fun ann)
go Term NamedDeBruijn uni fun ann
t
        -- boring non-recursive cases
        Constant ann
ann Some (ValueOf uni)
con -> Term Name uni fun ann -> m (Term Name uni fun ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term Name uni fun ann -> m (Term Name uni fun ann))
-> Term Name uni fun ann -> m (Term Name uni fun ann)
forall a b. (a -> b) -> a -> b
$ ann -> Some (ValueOf uni) -> Term Name uni fun ann
forall name (uni :: * -> *) fun ann.
ann -> Some (ValueOf uni) -> Term name uni fun ann
Constant ann
ann Some (ValueOf uni)
con
        Builtin ann
ann fun
bn -> Term Name uni fun ann -> m (Term Name uni fun ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term Name uni fun ann -> m (Term Name uni fun ann))
-> Term Name uni fun ann -> m (Term Name uni fun ann)
forall a b. (a -> b) -> a -> b
$ ann -> fun -> Term Name uni fun ann
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin ann
ann fun
bn
        Error ann
ann -> Term Name uni fun ann -> m (Term Name uni fun ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term Name uni fun ann -> m (Term Name uni fun ann))
-> Term Name uni fun ann -> m (Term Name uni fun ann)
forall a b. (a -> b) -> a -> b
$ ann -> Term Name uni fun ann
forall name (uni :: * -> *) fun ann. ann -> Term name uni fun ann
Error ann
ann