{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
module UntypedPlutusCore.DeBruijn
( Index (..)
, HasIndex (..)
, DeBruijn (..)
, NamedDeBruijn (..)
, FakeNamedDeBruijn (..)
, FreeVariableError (..)
, AsFreeVariableError (..)
, deBruijnTerm
, unDeBruijnTerm
, unNameDeBruijn
, fakeNameDeBruijn
, 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
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
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
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
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
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
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
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
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
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
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
LamAbs ann
ann NamedDeBruijn
n Term NamedDeBruijn uni fun ann
t ->
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
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
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