{-# LANGUAGE DerivingStrategies    #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
-- | Support for using de Bruijn indices for term names.
module UntypedPlutusCore.DeBruijn
    ( Index (..)
    , Level (..)
    , LevelInfo (..)
    , HasIndex (..)
    , DeBruijn (..)
    , NamedDeBruijn (..)
    -- we follow the same approach as Renamed, expose the constructor from Internal module,
    -- but hide it in the parent module.
    , FakeNamedDeBruijn (unFakeNamedDeBruijn)
    , FreeVariableError (..)
    , AsFreeVariableError (..)
    , deBruijnTerm
    , unDeBruijnTerm
    , unNameDeBruijn
    , fakeNameDeBruijn
    -- * unsafe api, use with care
    , 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

{- 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 :: 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

-- | 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 :: 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

-- | Takes a "handler" function to execute when encountering free variables.
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

-- | Takes a "handler" function to execute when encountering free variables.
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
       -- 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 LevelInfo 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 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
       -- 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 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
       -- boring non-recursive cases
       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

-- | Takes a "handler" function to execute when encountering free variables.
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
        -- 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 LevelInfo 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 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
        -- 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 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
        -- boring non-recursive cases
        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