{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
module UntypedPlutusCore.DeBruijn
( Index (..)
, Level (..)
, LevelInfo (..)
, HasIndex (..)
, DeBruijn (..)
, NamedDeBruijn (..)
, FakeNamedDeBruijn (unFakeNamedDeBruijn)
, FreeVariableError (..)
, AsFreeVariableError (..)
, deBruijnTerm
, unDeBruijnTerm
, unNameDeBruijn
, fakeNameDeBruijn
, deBruijnTermWith
, unDeBruijnTermWith
, freeIndexAsConsistentLevel
, deBruijnInitIndex
) where
import PlutusCore.DeBruijn.Internal
import PlutusCore.Name.Unique
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 :: forall e (m :: * -> *) (uni :: * -> *) fun ann.
(AsFreeVariableError e, MonadError e m) =>
Term Name uni fun ann -> m (Term NamedDeBruijn uni fun ann)
deBruijnTerm = (Unique -> ReaderT LevelInfo m Index)
-> Term Name uni fun ann -> m (Term NamedDeBruijn uni fun ann)
forall (m :: * -> *) (uni :: * -> *) fun ann.
Monad m =>
(Unique -> ReaderT LevelInfo m Index)
-> Term Name uni fun ann -> m (Term NamedDeBruijn uni fun ann)
deBruijnTermWith Unique -> ReaderT LevelInfo 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 :: forall (m :: * -> *) e (uni :: * -> *) fun ann.
(MonadQuote m, AsFreeVariableError e, MonadError e m) =>
Term NamedDeBruijn uni fun ann -> m (Term Name uni fun ann)
unDeBruijnTerm = (Index -> ReaderT LevelInfo m Unique)
-> Term NamedDeBruijn uni fun ann -> m (Term Name uni fun ann)
forall (m :: * -> *) (uni :: * -> *) fun ann.
MonadQuote m =>
(Index -> ReaderT LevelInfo m Unique)
-> Term NamedDeBruijn uni fun ann -> m (Term Name uni fun ann)
unDeBruijnTermWith Index -> ReaderT LevelInfo m Unique
forall e (m :: * -> *).
(AsFreeVariableError e, MonadError e m) =>
Index -> m Unique
freeIndexThrow
deBruijnTermWith
:: Monad m
=> (Unique -> ReaderT LevelInfo m Index)
-> Term Name uni fun ann
-> m (Term NamedDeBruijn uni fun ann)
deBruijnTermWith :: forall (m :: * -> *) (uni :: * -> *) fun ann.
Monad m =>
(Unique -> ReaderT LevelInfo m Index)
-> Term Name uni fun ann -> m (Term NamedDeBruijn uni fun ann)
deBruijnTermWith = (ReaderT LevelInfo m (Term NamedDeBruijn uni fun ann)
-> m (Term NamedDeBruijn uni fun ann)
forall (m :: * -> *) a. ReaderT LevelInfo m a -> m a
runDeBruijnT (ReaderT LevelInfo m (Term NamedDeBruijn uni fun ann)
-> m (Term NamedDeBruijn uni fun ann))
-> (Term Name uni fun ann
-> ReaderT LevelInfo 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 LevelInfo m (Term NamedDeBruijn uni fun ann))
-> Term Name uni fun ann -> m (Term NamedDeBruijn uni fun ann))
-> ((Unique -> ReaderT LevelInfo m Index)
-> Term Name uni fun ann
-> ReaderT LevelInfo m (Term NamedDeBruijn uni fun ann))
-> (Unique -> ReaderT LevelInfo 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 LevelInfo m Index)
-> Term Name uni fun ann
-> ReaderT LevelInfo m (Term NamedDeBruijn uni fun ann)
forall (m :: * -> *) (uni :: * -> *) fun ann.
MonadReader LevelInfo m =>
(Unique -> m Index)
-> Term Name uni fun ann -> m (Term NamedDeBruijn uni fun ann)
deBruijnTermWithM
unDeBruijnTermWith
:: MonadQuote m
=> (Index -> ReaderT LevelInfo m Unique)
-> Term NamedDeBruijn uni fun ann
-> m (Term Name uni fun ann)
unDeBruijnTermWith :: forall (m :: * -> *) (uni :: * -> *) fun ann.
MonadQuote m =>
(Index -> ReaderT LevelInfo m Unique)
-> Term NamedDeBruijn uni fun ann -> m (Term Name uni fun ann)
unDeBruijnTermWith = (ReaderT LevelInfo m (Term Name uni fun ann)
-> m (Term Name uni fun ann)
forall (m :: * -> *) a. ReaderT LevelInfo m a -> m a
runDeBruijnT (ReaderT LevelInfo m (Term Name uni fun ann)
-> m (Term Name uni fun ann))
-> (Term NamedDeBruijn uni fun ann
-> ReaderT LevelInfo 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 LevelInfo m (Term Name uni fun ann))
-> Term NamedDeBruijn uni fun ann -> m (Term Name uni fun ann))
-> ((Index -> ReaderT LevelInfo m Unique)
-> Term NamedDeBruijn uni fun ann
-> ReaderT LevelInfo m (Term Name uni fun ann))
-> (Index -> ReaderT LevelInfo 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 LevelInfo m Unique)
-> Term NamedDeBruijn uni fun ann
-> ReaderT LevelInfo m (Term Name uni fun ann)
forall (m :: * -> *) (uni :: * -> *) fun ann.
(MonadReader LevelInfo m, MonadQuote m) =>
(Index -> m Unique)
-> Term NamedDeBruijn uni fun ann -> m (Term Name uni fun ann)
unDeBruijnTermWithM
deBruijnTermWithM
:: MonadReader LevelInfo m
=> (Unique -> m Index)
-> Term Name uni fun ann
-> m (Term NamedDeBruijn uni fun ann)
deBruijnTermWithM :: forall (m :: * -> *) (uni :: * -> *) fun ann.
MonadReader LevelInfo m =>
(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 LevelInfo 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 LevelInfo 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 LevelInfo 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 LevelInfo 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 a b. m (a -> b) -> m a -> m b
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
Constr ann
ann Word64
i [Term Name uni fun ann]
es -> ann
-> Word64
-> [Term NamedDeBruijn uni fun ann]
-> Term NamedDeBruijn uni fun ann
forall name (uni :: * -> *) fun ann.
ann -> Word64 -> [Term name uni fun ann] -> Term name uni fun ann
Constr ann
ann Word64
i ([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))
-> [Term Name uni fun ann] -> m [Term NamedDeBruijn uni fun ann]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Term Name uni fun ann -> m (Term NamedDeBruijn uni fun ann)
go [Term Name uni fun ann]
es
Case ann
ann Term Name uni fun ann
arg Vector (Term Name uni fun ann)
cs -> ann
-> Term NamedDeBruijn uni fun ann
-> Vector (Term NamedDeBruijn uni fun ann)
-> Term NamedDeBruijn uni fun ann
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Vector (Term name uni fun ann)
-> Term name uni fun ann
Case ann
ann (Term NamedDeBruijn uni fun ann
-> Vector (Term NamedDeBruijn uni fun ann)
-> Term NamedDeBruijn uni fun ann)
-> m (Term NamedDeBruijn uni fun ann)
-> m (Vector (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
arg m (Vector (Term NamedDeBruijn uni fun ann)
-> Term NamedDeBruijn uni fun ann)
-> m (Vector (Term NamedDeBruijn uni fun ann))
-> m (Term NamedDeBruijn uni fun ann)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Term Name uni fun ann -> m (Term NamedDeBruijn uni fun ann))
-> Vector (Term Name uni fun ann)
-> m (Vector (Term NamedDeBruijn uni fun ann))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Vector a -> f (Vector b)
traverse Term Name uni fun ann -> m (Term NamedDeBruijn uni fun ann)
go Vector (Term Name uni fun ann)
cs
Constant ann
ann Some (ValueOf uni)
con -> Term NamedDeBruijn uni fun ann
-> m (Term NamedDeBruijn uni fun ann)
forall a. a -> m a
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 a. a -> m a
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 a. a -> m a
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 LevelInfo m, MonadQuote m)
=> (Index -> m Unique)
-> Term NamedDeBruijn uni fun ann
-> m (Term Name uni fun ann)
unDeBruijnTermWithM :: forall (m :: * -> *) (uni :: * -> *) fun ann.
(MonadReader LevelInfo m, MonadQuote m) =>
(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 LevelInfo 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 LevelInfo 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 LevelInfo 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
Lens' NamedDeBruijn Index
index Index
deBruijnInitIndex NamedDeBruijn
n
m (Term Name uni fun ann) -> m (Term Name uni fun ann)
forall (m :: * -> *) a. MonadReader LevelInfo 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 a b. m (a -> b) -> m a -> m b
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
Constr ann
ann Word64
i [Term NamedDeBruijn uni fun ann]
es -> ann -> Word64 -> [Term Name uni fun ann] -> Term Name uni fun ann
forall name (uni :: * -> *) fun ann.
ann -> Word64 -> [Term name uni fun ann] -> Term name uni fun ann
Constr ann
ann Word64
i ([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))
-> [Term NamedDeBruijn uni fun ann] -> m [Term Name uni fun ann]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Term NamedDeBruijn uni fun ann -> m (Term Name uni fun ann)
go [Term NamedDeBruijn uni fun ann]
es
Case ann
ann Term NamedDeBruijn uni fun ann
arg Vector (Term NamedDeBruijn uni fun ann)
cs -> ann
-> Term Name uni fun ann
-> Vector (Term Name uni fun ann)
-> Term Name uni fun ann
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Vector (Term name uni fun ann)
-> Term name uni fun ann
Case ann
ann (Term Name uni fun ann
-> Vector (Term Name uni fun ann) -> Term Name uni fun ann)
-> m (Term Name uni fun ann)
-> m (Vector (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
arg m (Vector (Term Name uni fun ann) -> Term Name uni fun ann)
-> m (Vector (Term Name uni fun ann)) -> m (Term Name uni fun ann)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Term NamedDeBruijn uni fun ann -> m (Term Name uni fun ann))
-> Vector (Term NamedDeBruijn uni fun ann)
-> m (Vector (Term Name uni fun ann))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Vector a -> f (Vector b)
traverse Term NamedDeBruijn uni fun ann -> m (Term Name uni fun ann)
go Vector (Term NamedDeBruijn uni fun ann)
cs
Constant ann
ann Some (ValueOf uni)
con -> Term Name uni fun ann -> m (Term Name uni fun ann)
forall a. a -> m a
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 a. a -> m a
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 a. a -> m a
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