{-# LANGUAGE DerivingStrategies    #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}

-- | Support for using de Bruijn indices for term and type names.
module PlutusCore.DeBruijn
    ( Index (..)
    , Level (..)
    , LevelInfo (..)
    , HasIndex (..)
    , DeBruijn (..)
    , NamedDeBruijn (..)
    -- we follow the same approach as Renamed, expose the constructor from Internal module,
    -- but hide it in this parent module.
    , FakeNamedDeBruijn (unFakeNamedDeBruijn)
    , TyDeBruijn (..)
    , NamedTyDeBruijn (..)
    , FreeVariableError (..)
    , AsFreeVariableError (..)
    , unNameDeBruijn
    , unNameTyDeBruijn
    , fakeNameDeBruijn
    , fakeTyNameDeBruijn
    , deBruijnTy
    , deBruijnTerm
    , unDeBruijnTy
    , unDeBruijnTerm
    -- * unsafe api, use with care
    , deBruijnTyWith
    , deBruijnTermWith
    , unDeBruijnTyWith
    , unDeBruijnTermWith
    , freeIndexAsConsistentLevel
    , deBruijnInitIndex
    , fromFake
    , toFake
    ) where

import PlutusCore.DeBruijn.Internal

import PlutusCore.Core.Type
import PlutusCore.Name.Unique
import PlutusCore.Quote

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

{- Note [DeBruijn indices of Binders]
In a debruijnijfied Term AST, the Binders have a debruijn index
at their the specific AST location.
During *undebruijnification* we ignore such binders' indices because they are meaningless,
and instead use the convention that such introduced binders have
a fixed debruijn index '0' at their introduction.
-}

-- | Takes a "handler" function to execute when encountering free variables.
unDeBruijnTyWith
    :: MonadQuote m
    => (Index -> ReaderT LevelInfo m Unique)
    -> Type NamedTyDeBruijn uni ann
    -> m (Type TyName uni ann)
unDeBruijnTyWith :: forall (m :: * -> *) (uni :: * -> *) ann.
MonadQuote m =>
(Index -> ReaderT LevelInfo m Unique)
-> Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann)
unDeBruijnTyWith = (ReaderT LevelInfo m (Type TyName uni ann)
-> m (Type TyName uni ann)
forall (m :: * -> *) a. ReaderT LevelInfo m a -> m a
runDeBruijnT (ReaderT LevelInfo m (Type TyName uni ann)
 -> m (Type TyName uni ann))
-> (Type NamedTyDeBruijn uni ann
    -> ReaderT LevelInfo m (Type TyName uni ann))
-> Type NamedTyDeBruijn uni ann
-> m (Type TyName uni ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((Type NamedTyDeBruijn uni ann
  -> ReaderT LevelInfo m (Type TyName uni ann))
 -> Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann))
-> ((Index -> ReaderT LevelInfo m Unique)
    -> Type NamedTyDeBruijn uni ann
    -> ReaderT LevelInfo m (Type TyName uni ann))
-> (Index -> ReaderT LevelInfo m Unique)
-> Type NamedTyDeBruijn uni ann
-> m (Type TyName uni ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Index -> ReaderT LevelInfo m Unique)
-> Type NamedTyDeBruijn uni ann
-> ReaderT LevelInfo m (Type TyName uni ann)
forall (m :: * -> *) (uni :: * -> *) ann.
(MonadReader LevelInfo m, MonadQuote m) =>
(Index -> m Unique)
-> Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann)
unDeBruijnTyWithM

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

-- | Convert a 'Type' with 'NamedTyDeBruijn's into a 'Type' with 'TyName's.
-- Will throw an error if a free variable is encountered.
unDeBruijnTy
    :: (MonadQuote m, AsFreeVariableError e, MonadError e m)
    => Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann)
unDeBruijnTy :: forall (m :: * -> *) e (uni :: * -> *) ann.
(MonadQuote m, AsFreeVariableError e, MonadError e m) =>
Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann)
unDeBruijnTy = (Index -> ReaderT LevelInfo m Unique)
-> Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann)
forall (m :: * -> *) (uni :: * -> *) ann.
MonadQuote m =>
(Index -> ReaderT LevelInfo m Unique)
-> Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann)
unDeBruijnTyWith Index -> ReaderT LevelInfo m Unique
forall e (m :: * -> *).
(AsFreeVariableError e, MonadError e m) =>
Index -> m Unique
freeIndexThrow

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

-- | Convert a 'Type' with 'TyName's into a 'Type' with 'NamedTyDeBruijn's.
-- Will throw an error if a free variable is encountered.
deBruijnTy
    :: (AsFreeVariableError e, MonadError e m)
    => Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann)
deBruijnTy :: forall e (m :: * -> *) (uni :: * -> *) ann.
(AsFreeVariableError e, MonadError e m) =>
Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann)
deBruijnTy = (Unique -> ReaderT LevelInfo m Index)
-> Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann)
forall (m :: * -> *) (uni :: * -> *) ann.
Monad m =>
(Unique -> ReaderT LevelInfo m Index)
-> Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann)
deBruijnTyWith Unique -> ReaderT LevelInfo m Index
forall e (m :: * -> *).
(AsFreeVariableError e, MonadError e m) =>
Unique -> m Index
freeUniqueThrow

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

deBruijnTermWith
    :: Monad m
    => (Unique -> ReaderT LevelInfo m Index)
    -> Term TyName Name uni fun ann
    -> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
deBruijnTermWith :: forall (m :: * -> *) (uni :: * -> *) fun ann.
Monad m =>
(Unique -> ReaderT LevelInfo m Index)
-> Term TyName Name uni fun ann
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
deBruijnTermWith = (ReaderT
  LevelInfo m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
forall (m :: * -> *) a. ReaderT LevelInfo m a -> m a
runDeBruijnT (ReaderT
   LevelInfo m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
 -> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann))
-> (Term TyName Name uni fun ann
    -> ReaderT
         LevelInfo m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann))
-> Term TyName Name uni fun ann
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((Term TyName Name uni fun ann
  -> ReaderT
       LevelInfo m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann))
 -> Term TyName Name uni fun ann
 -> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann))
-> ((Unique -> ReaderT LevelInfo m Index)
    -> Term TyName Name uni fun ann
    -> ReaderT
         LevelInfo m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann))
-> (Unique -> ReaderT LevelInfo m Index)
-> Term TyName Name uni fun ann
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Unique -> ReaderT LevelInfo m Index)
-> Term TyName Name uni fun ann
-> ReaderT
     LevelInfo m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
forall (m :: * -> *) (uni :: * -> *) fun ann.
MonadReader LevelInfo m =>
(Unique -> m Index)
-> Term TyName Name uni fun ann
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
deBruijnTermWithM

deBruijnTyWith
    :: Monad m
    => (Unique -> ReaderT LevelInfo m Index)
    -> Type TyName uni ann
    -> m (Type NamedTyDeBruijn uni ann)
deBruijnTyWith :: forall (m :: * -> *) (uni :: * -> *) ann.
Monad m =>
(Unique -> ReaderT LevelInfo m Index)
-> Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann)
deBruijnTyWith = (ReaderT LevelInfo m (Type NamedTyDeBruijn uni ann)
-> m (Type NamedTyDeBruijn uni ann)
forall (m :: * -> *) a. ReaderT LevelInfo m a -> m a
runDeBruijnT (ReaderT LevelInfo m (Type NamedTyDeBruijn uni ann)
 -> m (Type NamedTyDeBruijn uni ann))
-> (Type TyName uni ann
    -> ReaderT LevelInfo m (Type NamedTyDeBruijn uni ann))
-> Type TyName uni ann
-> m (Type NamedTyDeBruijn uni ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((Type TyName uni ann
  -> ReaderT LevelInfo m (Type NamedTyDeBruijn uni ann))
 -> Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann))
-> ((Unique -> ReaderT LevelInfo m Index)
    -> Type TyName uni ann
    -> ReaderT LevelInfo m (Type NamedTyDeBruijn uni ann))
-> (Unique -> ReaderT LevelInfo m Index)
-> Type TyName uni ann
-> m (Type NamedTyDeBruijn uni ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Unique -> ReaderT LevelInfo m Index)
-> Type TyName uni ann
-> ReaderT LevelInfo m (Type NamedTyDeBruijn uni ann)
forall (m :: * -> *) (uni :: * -> *) ann.
MonadReader LevelInfo m =>
(Unique -> m Index)
-> Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann)
deBruijnTyWithM

{- Note [De Bruijn conversion and recursion schemes]
These are quite repetitive, but we can't use a catamorphism for this, because
we are not only altering the recursive type, but also the name type parameters.
These are normally constant in a catamorphic application.
-}

deBruijnTyWithM
    :: forall m uni ann. MonadReader LevelInfo m
    => (Unique -> m Index)
    -> Type TyName uni ann
    -> m (Type NamedTyDeBruijn uni ann)
deBruijnTyWithM :: forall (m :: * -> *) (uni :: * -> *) ann.
MonadReader LevelInfo m =>
(Unique -> m Index)
-> Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann)
deBruijnTyWithM Unique -> m Index
h = Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann)
go
  where
    go :: Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann)
    go :: Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann)
go = \case
        -- variable case
        TyVar ann
ann TyName
n -> ann -> NamedTyDeBruijn -> Type NamedTyDeBruijn uni ann
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar ann
ann (NamedTyDeBruijn -> Type NamedTyDeBruijn uni ann)
-> m NamedTyDeBruijn -> m (Type NamedTyDeBruijn uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Unique -> m Index) -> TyName -> m NamedTyDeBruijn
forall (m :: * -> *).
MonadReader LevelInfo m =>
(Unique -> m Index) -> TyName -> m NamedTyDeBruijn
tyNameToDeBruijn Unique -> m Index
h TyName
n
        -- binder cases
        TyForall ann
ann TyName
tn Kind ann
k Type TyName uni ann
ty -> TyName
-> m (Type NamedTyDeBruijn uni ann)
-> m (Type NamedTyDeBruijn uni ann)
forall (m :: * -> *) name unique a.
(MonadReader LevelInfo m, HasUnique name unique) =>
name -> m a -> m a
declareUnique TyName
tn (m (Type NamedTyDeBruijn uni ann)
 -> m (Type NamedTyDeBruijn uni ann))
-> m (Type NamedTyDeBruijn uni ann)
-> m (Type NamedTyDeBruijn uni ann)
forall a b. (a -> b) -> a -> b
$ do
            NamedTyDeBruijn
tn' <- (Unique -> m Index) -> TyName -> m NamedTyDeBruijn
forall (m :: * -> *).
MonadReader LevelInfo m =>
(Unique -> m Index) -> TyName -> m NamedTyDeBruijn
tyNameToDeBruijn Unique -> m Index
h TyName
tn
            m (Type NamedTyDeBruijn uni ann)
-> m (Type NamedTyDeBruijn uni ann)
forall (m :: * -> *) a. MonadReader LevelInfo m => m a -> m a
withScope (m (Type NamedTyDeBruijn uni ann)
 -> m (Type NamedTyDeBruijn uni ann))
-> m (Type NamedTyDeBruijn uni ann)
-> m (Type NamedTyDeBruijn uni ann)
forall a b. (a -> b) -> a -> b
$ ann
-> NamedTyDeBruijn
-> Kind ann
-> Type NamedTyDeBruijn uni ann
-> Type NamedTyDeBruijn uni ann
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall ann
ann NamedTyDeBruijn
tn' Kind ann
k (Type NamedTyDeBruijn uni ann -> Type NamedTyDeBruijn uni ann)
-> m (Type NamedTyDeBruijn uni ann)
-> m (Type NamedTyDeBruijn uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann)
go Type TyName uni ann
ty
        TyLam ann
ann TyName
tn Kind ann
k Type TyName uni ann
ty -> TyName
-> m (Type NamedTyDeBruijn uni ann)
-> m (Type NamedTyDeBruijn uni ann)
forall (m :: * -> *) name unique a.
(MonadReader LevelInfo m, HasUnique name unique) =>
name -> m a -> m a
declareUnique TyName
tn (m (Type NamedTyDeBruijn uni ann)
 -> m (Type NamedTyDeBruijn uni ann))
-> m (Type NamedTyDeBruijn uni ann)
-> m (Type NamedTyDeBruijn uni ann)
forall a b. (a -> b) -> a -> b
$ do
            NamedTyDeBruijn
tn' <- (Unique -> m Index) -> TyName -> m NamedTyDeBruijn
forall (m :: * -> *).
MonadReader LevelInfo m =>
(Unique -> m Index) -> TyName -> m NamedTyDeBruijn
tyNameToDeBruijn Unique -> m Index
h TyName
tn
            m (Type NamedTyDeBruijn uni ann)
-> m (Type NamedTyDeBruijn uni ann)
forall (m :: * -> *) a. MonadReader LevelInfo m => m a -> m a
withScope (m (Type NamedTyDeBruijn uni ann)
 -> m (Type NamedTyDeBruijn uni ann))
-> m (Type NamedTyDeBruijn uni ann)
-> m (Type NamedTyDeBruijn uni ann)
forall a b. (a -> b) -> a -> b
$ ann
-> NamedTyDeBruijn
-> Kind ann
-> Type NamedTyDeBruijn uni ann
-> Type NamedTyDeBruijn uni ann
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam ann
ann NamedTyDeBruijn
tn' Kind ann
k (Type NamedTyDeBruijn uni ann -> Type NamedTyDeBruijn uni ann)
-> m (Type NamedTyDeBruijn uni ann)
-> m (Type NamedTyDeBruijn uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann)
go Type TyName uni ann
ty
        -- boring recursive cases
        TyFun ann
ann Type TyName uni ann
i Type TyName uni ann
o -> ann
-> Type NamedTyDeBruijn uni ann
-> Type NamedTyDeBruijn uni ann
-> Type NamedTyDeBruijn uni ann
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun ann
ann (Type NamedTyDeBruijn uni ann
 -> Type NamedTyDeBruijn uni ann -> Type NamedTyDeBruijn uni ann)
-> m (Type NamedTyDeBruijn uni ann)
-> m (Type NamedTyDeBruijn uni ann -> Type NamedTyDeBruijn uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann)
go Type TyName uni ann
i m (Type NamedTyDeBruijn uni ann -> Type NamedTyDeBruijn uni ann)
-> m (Type NamedTyDeBruijn uni ann)
-> m (Type NamedTyDeBruijn uni ann)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann)
go Type TyName uni ann
o
        TyApp ann
ann Type TyName uni ann
fun Type TyName uni ann
arg -> ann
-> Type NamedTyDeBruijn uni ann
-> Type NamedTyDeBruijn uni ann
-> Type NamedTyDeBruijn uni ann
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp ann
ann (Type NamedTyDeBruijn uni ann
 -> Type NamedTyDeBruijn uni ann -> Type NamedTyDeBruijn uni ann)
-> m (Type NamedTyDeBruijn uni ann)
-> m (Type NamedTyDeBruijn uni ann -> Type NamedTyDeBruijn uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann)
go Type TyName uni ann
fun m (Type NamedTyDeBruijn uni ann -> Type NamedTyDeBruijn uni ann)
-> m (Type NamedTyDeBruijn uni ann)
-> m (Type NamedTyDeBruijn uni ann)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann)
go Type TyName uni ann
arg
        TyIFix ann
ann Type TyName uni ann
pat Type TyName uni ann
arg -> ann
-> Type NamedTyDeBruijn uni ann
-> Type NamedTyDeBruijn uni ann
-> Type NamedTyDeBruijn uni ann
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyIFix ann
ann (Type NamedTyDeBruijn uni ann
 -> Type NamedTyDeBruijn uni ann -> Type NamedTyDeBruijn uni ann)
-> m (Type NamedTyDeBruijn uni ann)
-> m (Type NamedTyDeBruijn uni ann -> Type NamedTyDeBruijn uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann)
go Type TyName uni ann
pat m (Type NamedTyDeBruijn uni ann -> Type NamedTyDeBruijn uni ann)
-> m (Type NamedTyDeBruijn uni ann)
-> m (Type NamedTyDeBruijn uni ann)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann)
go Type TyName uni ann
arg
        TySOP ann
ann [[Type TyName uni ann]]
tyls -> ann
-> [[Type NamedTyDeBruijn uni ann]] -> Type NamedTyDeBruijn uni ann
forall tyname (uni :: * -> *) ann.
ann -> [[Type tyname uni ann]] -> Type tyname uni ann
TySOP ann
ann ([[Type NamedTyDeBruijn uni ann]] -> Type NamedTyDeBruijn uni ann)
-> m [[Type NamedTyDeBruijn uni ann]]
-> m (Type NamedTyDeBruijn uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (([Type TyName uni ann] -> m [Type NamedTyDeBruijn uni ann])
-> [[Type TyName uni ann]] -> m [[Type NamedTyDeBruijn uni 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 (([Type TyName uni ann] -> m [Type NamedTyDeBruijn uni ann])
 -> [[Type TyName uni ann]] -> m [[Type NamedTyDeBruijn uni ann]])
-> ((Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann))
    -> [Type TyName uni ann] -> m [Type NamedTyDeBruijn uni ann])
-> (Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann))
-> [[Type TyName uni ann]]
-> m [[Type NamedTyDeBruijn uni ann]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann))
-> [Type TyName uni ann] -> m [Type NamedTyDeBruijn uni 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) Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann)
go [[Type TyName uni ann]]
tyls
        -- boring non-recursive cases
        TyBuiltin ann
ann SomeTypeIn uni
someUni -> Type NamedTyDeBruijn uni ann -> m (Type NamedTyDeBruijn uni ann)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type NamedTyDeBruijn uni ann -> m (Type NamedTyDeBruijn uni ann))
-> Type NamedTyDeBruijn uni ann -> m (Type NamedTyDeBruijn uni ann)
forall a b. (a -> b) -> a -> b
$ ann -> SomeTypeIn uni -> Type NamedTyDeBruijn uni ann
forall tyname (uni :: * -> *) ann.
ann -> SomeTypeIn uni -> Type tyname uni ann
TyBuiltin ann
ann SomeTypeIn uni
someUni

deBruijnTermWithM
    :: forall m uni fun ann. (MonadReader LevelInfo m)
    => (Unique -> m Index)
    -> Term TyName Name uni fun ann
    -> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
deBruijnTermWithM :: forall (m :: * -> *) (uni :: * -> *) fun ann.
MonadReader LevelInfo m =>
(Unique -> m Index)
-> Term TyName Name uni fun ann
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
deBruijnTermWithM Unique -> m Index
h = Term TyName Name uni fun ann
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
go
  where
    goT :: Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann)
    goT :: Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann)
goT = (Unique -> m Index)
-> Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann)
forall (m :: * -> *) (uni :: * -> *) ann.
MonadReader LevelInfo m =>
(Unique -> m Index)
-> Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann)
deBruijnTyWithM Unique -> m Index
h

    go :: Term TyName Name uni fun ann -> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
    go :: Term TyName Name uni fun ann
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
go = \case
        -- variable case
        Var ann
ann Name
n -> ann
-> NamedDeBruijn -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var ann
ann (NamedDeBruijn -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
-> m NamedDeBruijn
-> m (Term NamedTyDeBruijn 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
        TyAbs ann
ann TyName
tn Kind ann
k Term TyName Name uni fun ann
t -> TyName
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
forall (m :: * -> *) name unique a.
(MonadReader LevelInfo m, HasUnique name unique) =>
name -> m a -> m a
declareUnique TyName
tn (m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
 -> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann))
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
forall a b. (a -> b) -> a -> b
$ do
            NamedTyDeBruijn
tn' <- (Unique -> m Index) -> TyName -> m NamedTyDeBruijn
forall (m :: * -> *).
MonadReader LevelInfo m =>
(Unique -> m Index) -> TyName -> m NamedTyDeBruijn
tyNameToDeBruijn Unique -> m Index
h TyName
tn
            m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
forall (m :: * -> *) a. MonadReader LevelInfo m => m a -> m a
withScope (m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
 -> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann))
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
forall a b. (a -> b) -> a -> b
$ ann
-> NamedTyDeBruijn
-> Kind ann
-> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
-> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
TyAbs ann
ann NamedTyDeBruijn
tn' Kind ann
k (Term NamedTyDeBruijn NamedDeBruijn uni fun ann
 -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term TyName Name uni fun ann
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
go Term TyName Name uni fun ann
t
        LamAbs ann
ann Name
n Type TyName uni ann
ty Term TyName Name uni fun ann
t -> Name
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
-> m (Term NamedTyDeBruijn 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 NamedTyDeBruijn NamedDeBruijn uni fun ann)
 -> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann))
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
-> m (Term NamedTyDeBruijn 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 NamedTyDeBruijn NamedDeBruijn uni fun ann)
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
forall (m :: * -> *) a. MonadReader LevelInfo m => m a -> m a
withScope (m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
 -> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann))
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
forall a b. (a -> b) -> a -> b
$ ann
-> NamedDeBruijn
-> Type NamedTyDeBruijn uni ann
-> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
-> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs ann
ann NamedDeBruijn
n' (Type NamedTyDeBruijn uni ann
 -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
 -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
-> m (Type NamedTyDeBruijn uni ann)
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann
      -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann)
goT Type TyName uni ann
ty m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann
   -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
-> m (Term NamedTyDeBruijn 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 TyName Name uni fun ann
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
go Term TyName Name uni fun ann
t
        -- boring recursive cases
        Apply ann
ann Term TyName Name uni fun ann
t1 Term TyName Name uni fun ann
t2 -> ann
-> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
-> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
-> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply ann
ann (Term NamedTyDeBruijn NamedDeBruijn uni fun ann
 -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
 -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann
      -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term TyName Name uni fun ann
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
go Term TyName Name uni fun ann
t1 m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann
   -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
-> m (Term NamedTyDeBruijn 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 TyName Name uni fun ann
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
go Term TyName Name uni fun ann
t2
        TyInst ann
ann Term TyName Name uni fun ann
t Type TyName uni ann
ty -> ann
-> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
-> Type NamedTyDeBruijn uni ann
-> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
TyInst ann
ann (Term NamedTyDeBruijn NamedDeBruijn uni fun ann
 -> Type NamedTyDeBruijn uni ann
 -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
-> m (Type NamedTyDeBruijn uni ann
      -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term TyName Name uni fun ann
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
go Term TyName Name uni fun ann
t m (Type NamedTyDeBruijn uni ann
   -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
-> m (Type NamedTyDeBruijn uni ann)
-> m (Term NamedTyDeBruijn 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
<*> Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann)
goT Type TyName uni ann
ty
        Unwrap ann
ann Term TyName Name uni fun ann
t -> ann
-> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
-> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann
Unwrap ann
ann (Term NamedTyDeBruijn NamedDeBruijn uni fun ann
 -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term TyName Name uni fun ann
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
go Term TyName Name uni fun ann
t
        IWrap ann
ann Type TyName uni ann
pat Type TyName uni ann
arg Term TyName Name uni fun ann
t -> ann
-> Type NamedTyDeBruijn uni ann
-> Type NamedTyDeBruijn uni ann
-> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
-> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
IWrap ann
ann (Type NamedTyDeBruijn uni ann
 -> Type NamedTyDeBruijn uni ann
 -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
 -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
-> m (Type NamedTyDeBruijn uni ann)
-> m (Type NamedTyDeBruijn uni ann
      -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
      -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann)
goT Type TyName uni ann
pat m (Type NamedTyDeBruijn uni ann
   -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
   -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
-> m (Type NamedTyDeBruijn uni ann)
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann
      -> Term NamedTyDeBruijn 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
<*> Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann)
goT Type TyName uni ann
arg m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann
   -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
-> m (Term NamedTyDeBruijn 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 TyName Name uni fun ann
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
go Term TyName Name uni fun ann
t
        Error ann
ann Type TyName uni ann
ty -> ann
-> Type NamedTyDeBruijn uni ann
-> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann -> Type tyname uni ann -> Term tyname name uni fun ann
Error ann
ann (Type NamedTyDeBruijn uni ann
 -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
-> m (Type NamedTyDeBruijn uni ann)
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann)
goT Type TyName uni ann
ty
        Constr ann
ann Type TyName uni ann
ty Word64
i [Term TyName Name uni fun ann]
es -> ann
-> Type NamedTyDeBruijn uni ann
-> Word64
-> [Term NamedTyDeBruijn NamedDeBruijn uni fun ann]
-> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Word64
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
Constr ann
ann (Type NamedTyDeBruijn uni ann
 -> Word64
 -> [Term NamedTyDeBruijn NamedDeBruijn uni fun ann]
 -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
-> m (Type NamedTyDeBruijn uni ann)
-> m (Word64
      -> [Term NamedTyDeBruijn NamedDeBruijn uni fun ann]
      -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann)
goT Type TyName uni ann
ty m (Word64
   -> [Term NamedTyDeBruijn NamedDeBruijn uni fun ann]
   -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
-> m Word64
-> m ([Term NamedTyDeBruijn NamedDeBruijn uni fun ann]
      -> Term NamedTyDeBruijn 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
<*> Word64 -> m Word64
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word64
i m ([Term NamedTyDeBruijn NamedDeBruijn uni fun ann]
   -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
-> m [Term NamedTyDeBruijn NamedDeBruijn uni fun ann]
-> m (Term NamedTyDeBruijn 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 TyName Name uni fun ann
 -> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann))
-> [Term TyName Name uni fun ann]
-> m [Term NamedTyDeBruijn 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 TyName Name uni fun ann
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
go [Term TyName Name uni fun ann]
es
        Case ann
ann Type TyName uni ann
ty Term TyName Name uni fun ann
arg [Term TyName Name uni fun ann]
cs -> ann
-> Type NamedTyDeBruijn uni ann
-> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
-> [Term NamedTyDeBruijn NamedDeBruijn uni fun ann]
-> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
Case ann
ann (Type NamedTyDeBruijn uni ann
 -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
 -> [Term NamedTyDeBruijn NamedDeBruijn uni fun ann]
 -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
-> m (Type NamedTyDeBruijn uni ann)
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann
      -> [Term NamedTyDeBruijn NamedDeBruijn uni fun ann]
      -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann)
goT Type TyName uni ann
ty m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann
   -> [Term NamedTyDeBruijn NamedDeBruijn uni fun ann]
   -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
-> m ([Term NamedTyDeBruijn NamedDeBruijn uni fun ann]
      -> Term NamedTyDeBruijn 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 TyName Name uni fun ann
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
go Term TyName Name uni fun ann
arg m ([Term NamedTyDeBruijn NamedDeBruijn uni fun ann]
   -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
-> m [Term NamedTyDeBruijn NamedDeBruijn uni fun ann]
-> m (Term NamedTyDeBruijn 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 TyName Name uni fun ann
 -> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann))
-> [Term TyName Name uni fun ann]
-> m [Term NamedTyDeBruijn 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 TyName Name uni fun ann
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
go [Term TyName Name uni fun ann]
cs
        -- boring non-recursive cases
        Constant ann
ann Some (ValueOf uni)
con -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term NamedTyDeBruijn NamedDeBruijn uni fun ann
 -> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann))
-> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
forall a b. (a -> b) -> a -> b
$ ann
-> Some (ValueOf uni)
-> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann -> Some (ValueOf uni) -> Term tyname name uni fun ann
Constant ann
ann Some (ValueOf uni)
con
        Builtin ann
ann fun
bn -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term NamedTyDeBruijn NamedDeBruijn uni fun ann
 -> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann))
-> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
forall a b. (a -> b) -> a -> b
$ ann -> fun -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann -> fun -> Term tyname name uni fun ann
Builtin ann
ann fun
bn

-- | Takes a "handler" function to execute when encountering free variables.
unDeBruijnTyWithM
    :: forall m uni ann. (MonadReader LevelInfo m, MonadQuote m)
    => (Index -> m Unique)
    -> Type NamedTyDeBruijn uni ann
    -> m (Type TyName uni ann)
unDeBruijnTyWithM :: forall (m :: * -> *) (uni :: * -> *) ann.
(MonadReader LevelInfo m, MonadQuote m) =>
(Index -> m Unique)
-> Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann)
unDeBruijnTyWithM Index -> m Unique
h = Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann)
go
  where
    go :: Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann)
    go :: Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann)
go = \case
      -- variable case
      TyVar ann
ann NamedTyDeBruijn
n -> ann -> TyName -> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar ann
ann (TyName -> Type TyName uni ann)
-> m TyName -> m (Type TyName uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Index -> m Unique) -> NamedTyDeBruijn -> m TyName
forall (m :: * -> *).
MonadReader LevelInfo m =>
(Index -> m Unique) -> NamedTyDeBruijn -> m TyName
deBruijnToTyName Index -> m Unique
h NamedTyDeBruijn
n
      -- binder cases
      TyForall ann
ann NamedTyDeBruijn
tn Kind ann
k Type NamedTyDeBruijn uni ann
ty ->
          -- See Note [DeBruijn indices of Binders]
          m (Type TyName uni ann) -> m (Type TyName uni ann)
forall (m :: * -> *) a.
(MonadReader LevelInfo m, MonadQuote m) =>
m a -> m a
declareBinder (m (Type TyName uni ann) -> m (Type TyName uni ann))
-> m (Type TyName uni ann) -> m (Type TyName uni ann)
forall a b. (a -> b) -> a -> b
$ do
            TyName
tn' <- (Index -> m Unique) -> NamedTyDeBruijn -> m TyName
forall (m :: * -> *).
MonadReader LevelInfo m =>
(Index -> m Unique) -> NamedTyDeBruijn -> m TyName
deBruijnToTyName Index -> m Unique
h (NamedTyDeBruijn -> m TyName) -> NamedTyDeBruijn -> m TyName
forall a b. (a -> b) -> a -> b
$ ASetter NamedTyDeBruijn NamedTyDeBruijn Index Index
-> Index -> NamedTyDeBruijn -> NamedTyDeBruijn
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter NamedTyDeBruijn NamedTyDeBruijn Index Index
forall a. HasIndex a => Lens' a Index
Lens' NamedTyDeBruijn Index
index Index
deBruijnInitIndex NamedTyDeBruijn
tn
            m (Type TyName uni ann) -> m (Type TyName uni ann)
forall (m :: * -> *) a. MonadReader LevelInfo m => m a -> m a
withScope (m (Type TyName uni ann) -> m (Type TyName uni ann))
-> m (Type TyName uni ann) -> m (Type TyName uni ann)
forall a b. (a -> b) -> a -> b
$ ann
-> TyName -> Kind ann -> Type TyName uni ann -> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall ann
ann TyName
tn' Kind ann
k (Type TyName uni ann -> Type TyName uni ann)
-> m (Type TyName uni ann) -> m (Type TyName uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann)
go Type NamedTyDeBruijn uni ann
ty
      TyLam ann
ann NamedTyDeBruijn
tn Kind ann
k Type NamedTyDeBruijn uni ann
ty ->
          -- See Note [DeBruijn indices of Binders]
          m (Type TyName uni ann) -> m (Type TyName uni ann)
forall (m :: * -> *) a.
(MonadReader LevelInfo m, MonadQuote m) =>
m a -> m a
declareBinder (m (Type TyName uni ann) -> m (Type TyName uni ann))
-> m (Type TyName uni ann) -> m (Type TyName uni ann)
forall a b. (a -> b) -> a -> b
$ do
            TyName
tn' <- (Index -> m Unique) -> NamedTyDeBruijn -> m TyName
forall (m :: * -> *).
MonadReader LevelInfo m =>
(Index -> m Unique) -> NamedTyDeBruijn -> m TyName
deBruijnToTyName Index -> m Unique
h (NamedTyDeBruijn -> m TyName) -> NamedTyDeBruijn -> m TyName
forall a b. (a -> b) -> a -> b
$ ASetter NamedTyDeBruijn NamedTyDeBruijn Index Index
-> Index -> NamedTyDeBruijn -> NamedTyDeBruijn
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter NamedTyDeBruijn NamedTyDeBruijn Index Index
forall a. HasIndex a => Lens' a Index
Lens' NamedTyDeBruijn Index
index Index
deBruijnInitIndex NamedTyDeBruijn
tn
            m (Type TyName uni ann) -> m (Type TyName uni ann)
forall (m :: * -> *) a. MonadReader LevelInfo m => m a -> m a
withScope (m (Type TyName uni ann) -> m (Type TyName uni ann))
-> m (Type TyName uni ann) -> m (Type TyName uni ann)
forall a b. (a -> b) -> a -> b
$ ann
-> TyName -> Kind ann -> Type TyName uni ann -> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam ann
ann TyName
tn' Kind ann
k (Type TyName uni ann -> Type TyName uni ann)
-> m (Type TyName uni ann) -> m (Type TyName uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann)
go Type NamedTyDeBruijn uni ann
ty
      -- boring recursive cases
      TyFun ann
ann Type NamedTyDeBruijn uni ann
i Type NamedTyDeBruijn uni ann
o -> ann
-> Type TyName uni ann
-> Type TyName uni ann
-> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun ann
ann (Type TyName uni ann -> Type TyName uni ann -> Type TyName uni ann)
-> m (Type TyName uni ann)
-> m (Type TyName uni ann -> Type TyName uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann)
go Type NamedTyDeBruijn uni ann
i m (Type TyName uni ann -> Type TyName uni ann)
-> m (Type TyName uni ann) -> m (Type TyName uni ann)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann)
go Type NamedTyDeBruijn uni ann
o
      TyApp ann
ann Type NamedTyDeBruijn uni ann
fun Type NamedTyDeBruijn uni ann
arg -> ann
-> Type TyName uni ann
-> Type TyName uni ann
-> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp ann
ann (Type TyName uni ann -> Type TyName uni ann -> Type TyName uni ann)
-> m (Type TyName uni ann)
-> m (Type TyName uni ann -> Type TyName uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann)
go Type NamedTyDeBruijn uni ann
fun m (Type TyName uni ann -> Type TyName uni ann)
-> m (Type TyName uni ann) -> m (Type TyName uni ann)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann)
go Type NamedTyDeBruijn uni ann
arg
      TyIFix ann
ann Type NamedTyDeBruijn uni ann
pat Type NamedTyDeBruijn uni ann
arg -> ann
-> Type TyName uni ann
-> Type TyName uni ann
-> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyIFix ann
ann (Type TyName uni ann -> Type TyName uni ann -> Type TyName uni ann)
-> m (Type TyName uni ann)
-> m (Type TyName uni ann -> Type TyName uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann)
go Type NamedTyDeBruijn uni ann
pat m (Type TyName uni ann -> Type TyName uni ann)
-> m (Type TyName uni ann) -> m (Type TyName uni ann)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann)
go Type NamedTyDeBruijn uni ann
arg
      TySOP ann
ann [[Type NamedTyDeBruijn uni ann]]
tyls -> ann -> [[Type TyName uni ann]] -> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann -> [[Type tyname uni ann]] -> Type tyname uni ann
TySOP ann
ann ([[Type TyName uni ann]] -> Type TyName uni ann)
-> m [[Type TyName uni ann]] -> m (Type TyName uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (([Type NamedTyDeBruijn uni ann] -> m [Type TyName uni ann])
-> [[Type NamedTyDeBruijn uni ann]] -> m [[Type TyName uni 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 (([Type NamedTyDeBruijn uni ann] -> m [Type TyName uni ann])
 -> [[Type NamedTyDeBruijn uni ann]] -> m [[Type TyName uni ann]])
-> ((Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann))
    -> [Type NamedTyDeBruijn uni ann] -> m [Type TyName uni ann])
-> (Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann))
-> [[Type NamedTyDeBruijn uni ann]]
-> m [[Type TyName uni ann]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann))
-> [Type NamedTyDeBruijn uni ann] -> m [Type TyName uni 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) Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann)
go [[Type NamedTyDeBruijn uni ann]]
tyls
      -- boring non-recursive cases
      TyBuiltin ann
ann SomeTypeIn uni
someUni -> Type TyName uni ann -> m (Type TyName uni ann)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type TyName uni ann -> m (Type TyName uni ann))
-> Type TyName uni ann -> m (Type TyName uni ann)
forall a b. (a -> b) -> a -> b
$ ann -> SomeTypeIn uni -> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann -> SomeTypeIn uni -> Type tyname uni ann
TyBuiltin ann
ann SomeTypeIn uni
someUni

-- | Takes a "handler" function to execute when encountering free variables.
unDeBruijnTermWithM
    :: forall m uni fun ann. (MonadReader LevelInfo m, MonadQuote m)
    => (Index -> m Unique)
    -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
    -> m (Term TyName Name uni fun ann)
unDeBruijnTermWithM :: forall (m :: * -> *) (uni :: * -> *) fun ann.
(MonadReader LevelInfo m, MonadQuote m) =>
(Index -> m Unique)
-> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
-> m (Term TyName Name uni fun ann)
unDeBruijnTermWithM Index -> m Unique
h = Term NamedTyDeBruijn NamedDeBruijn uni fun ann
-> m (Term TyName Name uni fun ann)
go
  where
    goT :: Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann)
    goT :: Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann)
goT = (Index -> m Unique)
-> Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann)
forall (m :: * -> *) (uni :: * -> *) ann.
(MonadReader LevelInfo m, MonadQuote m) =>
(Index -> m Unique)
-> Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann)
unDeBruijnTyWithM Index -> m Unique
h

    go :: Term NamedTyDeBruijn NamedDeBruijn uni fun ann -> m (Term TyName Name uni fun ann)
    go :: Term NamedTyDeBruijn NamedDeBruijn uni fun ann
-> m (Term TyName Name uni fun ann)
go = \case
        -- variable case
        Var ann
ann NamedDeBruijn
n -> ann -> Name -> Term TyName Name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var ann
ann (Name -> Term TyName Name uni fun ann)
-> m Name -> m (Term TyName 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
        TyAbs ann
ann NamedTyDeBruijn
tn Kind ann
k Term NamedTyDeBruijn NamedDeBruijn uni fun ann
t ->
            -- See Note [DeBruijn indices of Binders]
            m (Term TyName Name uni fun ann)
-> m (Term TyName Name uni fun ann)
forall (m :: * -> *) a.
(MonadReader LevelInfo m, MonadQuote m) =>
m a -> m a
declareBinder (m (Term TyName Name uni fun ann)
 -> m (Term TyName Name uni fun ann))
-> m (Term TyName Name uni fun ann)
-> m (Term TyName Name uni fun ann)
forall a b. (a -> b) -> a -> b
$ do
              TyName
tn' <- (Index -> m Unique) -> NamedTyDeBruijn -> m TyName
forall (m :: * -> *).
MonadReader LevelInfo m =>
(Index -> m Unique) -> NamedTyDeBruijn -> m TyName
deBruijnToTyName Index -> m Unique
h (NamedTyDeBruijn -> m TyName) -> NamedTyDeBruijn -> m TyName
forall a b. (a -> b) -> a -> b
$ ASetter NamedTyDeBruijn NamedTyDeBruijn Index Index
-> Index -> NamedTyDeBruijn -> NamedTyDeBruijn
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter NamedTyDeBruijn NamedTyDeBruijn Index Index
forall a. HasIndex a => Lens' a Index
Lens' NamedTyDeBruijn Index
index Index
deBruijnInitIndex NamedTyDeBruijn
tn
              m (Term TyName Name uni fun ann)
-> m (Term TyName Name uni fun ann)
forall (m :: * -> *) a. MonadReader LevelInfo m => m a -> m a
withScope (m (Term TyName Name uni fun ann)
 -> m (Term TyName Name uni fun ann))
-> m (Term TyName Name uni fun ann)
-> m (Term TyName Name uni fun ann)
forall a b. (a -> b) -> a -> b
$ ann
-> TyName
-> Kind ann
-> Term TyName Name uni fun ann
-> Term TyName Name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
TyAbs ann
ann TyName
tn' Kind ann
k (Term TyName Name uni fun ann -> Term TyName Name uni fun ann)
-> m (Term TyName Name uni fun ann)
-> m (Term TyName Name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
-> m (Term TyName Name uni fun ann)
go Term NamedTyDeBruijn NamedDeBruijn uni fun ann
t
        LamAbs ann
ann NamedDeBruijn
n Type NamedTyDeBruijn uni ann
ty Term NamedTyDeBruijn NamedDeBruijn uni fun ann
t ->
            -- See Note [DeBruijn indices of Binders]
            m (Term TyName Name uni fun ann)
-> m (Term TyName Name uni fun ann)
forall (m :: * -> *) a.
(MonadReader LevelInfo m, MonadQuote m) =>
m a -> m a
declareBinder (m (Term TyName Name uni fun ann)
 -> m (Term TyName Name uni fun ann))
-> m (Term TyName Name uni fun ann)
-> m (Term TyName 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 TyName Name uni fun ann)
-> m (Term TyName Name uni fun ann)
forall (m :: * -> *) a. MonadReader LevelInfo m => m a -> m a
withScope (m (Term TyName Name uni fun ann)
 -> m (Term TyName Name uni fun ann))
-> m (Term TyName Name uni fun ann)
-> m (Term TyName Name uni fun ann)
forall a b. (a -> b) -> a -> b
$ ann
-> Name
-> Type TyName uni ann
-> Term TyName Name uni fun ann
-> Term TyName Name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs ann
ann Name
n' (Type TyName uni ann
 -> Term TyName Name uni fun ann -> Term TyName Name uni fun ann)
-> m (Type TyName uni ann)
-> m (Term TyName Name uni fun ann -> Term TyName Name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann)
goT Type NamedTyDeBruijn uni ann
ty m (Term TyName Name uni fun ann -> Term TyName Name uni fun ann)
-> m (Term TyName Name uni fun ann)
-> m (Term TyName 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 NamedTyDeBruijn NamedDeBruijn uni fun ann
-> m (Term TyName Name uni fun ann)
go Term NamedTyDeBruijn NamedDeBruijn uni fun ann
t
        -- boring recursive cases
        Apply ann
ann Term NamedTyDeBruijn NamedDeBruijn uni fun ann
t1 Term NamedTyDeBruijn NamedDeBruijn uni fun ann
t2 -> ann
-> Term TyName Name uni fun ann
-> Term TyName Name uni fun ann
-> Term TyName Name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply ann
ann (Term TyName Name uni fun ann
 -> Term TyName Name uni fun ann -> Term TyName Name uni fun ann)
-> m (Term TyName Name uni fun ann)
-> m (Term TyName Name uni fun ann -> Term TyName Name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
-> m (Term TyName Name uni fun ann)
go Term NamedTyDeBruijn NamedDeBruijn uni fun ann
t1 m (Term TyName Name uni fun ann -> Term TyName Name uni fun ann)
-> m (Term TyName Name uni fun ann)
-> m (Term TyName 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 NamedTyDeBruijn NamedDeBruijn uni fun ann
-> m (Term TyName Name uni fun ann)
go Term NamedTyDeBruijn NamedDeBruijn uni fun ann
t2
        TyInst ann
ann Term NamedTyDeBruijn NamedDeBruijn uni fun ann
t Type NamedTyDeBruijn uni ann
ty -> ann
-> Term TyName Name uni fun ann
-> Type TyName uni ann
-> Term TyName Name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
TyInst ann
ann (Term TyName Name uni fun ann
 -> Type TyName uni ann -> Term TyName Name uni fun ann)
-> m (Term TyName Name uni fun ann)
-> m (Type TyName uni ann -> Term TyName Name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
-> m (Term TyName Name uni fun ann)
go Term NamedTyDeBruijn NamedDeBruijn uni fun ann
t m (Type TyName uni ann -> Term TyName Name uni fun ann)
-> m (Type TyName uni ann) -> m (Term TyName 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
<*> Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann)
goT Type NamedTyDeBruijn uni ann
ty
        Unwrap ann
ann Term NamedTyDeBruijn NamedDeBruijn uni fun ann
t -> ann -> Term TyName Name uni fun ann -> Term TyName Name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann
Unwrap ann
ann (Term TyName Name uni fun ann -> Term TyName Name uni fun ann)
-> m (Term TyName Name uni fun ann)
-> m (Term TyName Name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
-> m (Term TyName Name uni fun ann)
go Term NamedTyDeBruijn NamedDeBruijn uni fun ann
t
        IWrap ann
ann Type NamedTyDeBruijn uni ann
pat Type NamedTyDeBruijn uni ann
arg Term NamedTyDeBruijn NamedDeBruijn uni fun ann
t -> ann
-> Type TyName uni ann
-> Type TyName uni ann
-> Term TyName Name uni fun ann
-> Term TyName Name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
IWrap ann
ann (Type TyName uni ann
 -> Type TyName uni ann
 -> Term TyName Name uni fun ann
 -> Term TyName Name uni fun ann)
-> m (Type TyName uni ann)
-> m (Type TyName uni ann
      -> Term TyName Name uni fun ann -> Term TyName Name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann)
goT Type NamedTyDeBruijn uni ann
pat m (Type TyName uni ann
   -> Term TyName Name uni fun ann -> Term TyName Name uni fun ann)
-> m (Type TyName uni ann)
-> m (Term TyName Name uni fun ann -> Term TyName 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
<*> Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann)
goT Type NamedTyDeBruijn uni ann
arg m (Term TyName Name uni fun ann -> Term TyName Name uni fun ann)
-> m (Term TyName Name uni fun ann)
-> m (Term TyName 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 NamedTyDeBruijn NamedDeBruijn uni fun ann
-> m (Term TyName Name uni fun ann)
go Term NamedTyDeBruijn NamedDeBruijn uni fun ann
t
        Error ann
ann Type NamedTyDeBruijn uni ann
ty -> ann -> Type TyName uni ann -> Term TyName Name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann -> Type tyname uni ann -> Term tyname name uni fun ann
Error ann
ann (Type TyName uni ann -> Term TyName Name uni fun ann)
-> m (Type TyName uni ann) -> m (Term TyName Name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann)
goT Type NamedTyDeBruijn uni ann
ty
        Constr ann
ann Type NamedTyDeBruijn uni ann
ty Word64
i [Term NamedTyDeBruijn NamedDeBruijn uni fun ann]
es -> ann
-> Type TyName uni ann
-> Word64
-> [Term TyName Name uni fun ann]
-> Term TyName Name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Word64
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
Constr ann
ann (Type TyName uni ann
 -> Word64
 -> [Term TyName Name uni fun ann]
 -> Term TyName Name uni fun ann)
-> m (Type TyName uni ann)
-> m (Word64
      -> [Term TyName Name uni fun ann] -> Term TyName Name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann)
goT Type NamedTyDeBruijn uni ann
ty m (Word64
   -> [Term TyName Name uni fun ann] -> Term TyName Name uni fun ann)
-> m Word64
-> m ([Term TyName Name uni fun ann]
      -> Term TyName 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
<*> Word64 -> m Word64
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word64
i m ([Term TyName Name uni fun ann] -> Term TyName Name uni fun ann)
-> m [Term TyName Name uni fun ann]
-> m (Term TyName 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 NamedTyDeBruijn NamedDeBruijn uni fun ann
 -> m (Term TyName Name uni fun ann))
-> [Term NamedTyDeBruijn NamedDeBruijn uni fun ann]
-> m [Term TyName 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 NamedTyDeBruijn NamedDeBruijn uni fun ann
-> m (Term TyName Name uni fun ann)
go [Term NamedTyDeBruijn NamedDeBruijn uni fun ann]
es
        Case ann
ann Type NamedTyDeBruijn uni ann
ty Term NamedTyDeBruijn NamedDeBruijn uni fun ann
arg [Term NamedTyDeBruijn NamedDeBruijn uni fun ann]
cs -> ann
-> Type TyName uni ann
-> Term TyName Name uni fun ann
-> [Term TyName Name uni fun ann]
-> Term TyName Name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
Case ann
ann (Type TyName uni ann
 -> Term TyName Name uni fun ann
 -> [Term TyName Name uni fun ann]
 -> Term TyName Name uni fun ann)
-> m (Type TyName uni ann)
-> m (Term TyName Name uni fun ann
      -> [Term TyName Name uni fun ann] -> Term TyName Name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann)
goT Type NamedTyDeBruijn uni ann
ty m (Term TyName Name uni fun ann
   -> [Term TyName Name uni fun ann] -> Term TyName Name uni fun ann)
-> m (Term TyName Name uni fun ann)
-> m ([Term TyName Name uni fun ann]
      -> Term TyName 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 NamedTyDeBruijn NamedDeBruijn uni fun ann
-> m (Term TyName Name uni fun ann)
go Term NamedTyDeBruijn NamedDeBruijn uni fun ann
arg m ([Term TyName Name uni fun ann] -> Term TyName Name uni fun ann)
-> m [Term TyName Name uni fun ann]
-> m (Term TyName 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 NamedTyDeBruijn NamedDeBruijn uni fun ann
 -> m (Term TyName Name uni fun ann))
-> [Term NamedTyDeBruijn NamedDeBruijn uni fun ann]
-> m [Term TyName 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 NamedTyDeBruijn NamedDeBruijn uni fun ann
-> m (Term TyName Name uni fun ann)
go [Term NamedTyDeBruijn NamedDeBruijn uni fun ann]
cs
        -- boring non-recursive cases
        Constant ann
ann Some (ValueOf uni)
con -> Term TyName Name uni fun ann -> m (Term TyName Name uni fun ann)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term TyName Name uni fun ann -> m (Term TyName Name uni fun ann))
-> Term TyName Name uni fun ann -> m (Term TyName Name uni fun ann)
forall a b. (a -> b) -> a -> b
$ ann -> Some (ValueOf uni) -> Term TyName Name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann -> Some (ValueOf uni) -> Term tyname name uni fun ann
Constant ann
ann Some (ValueOf uni)
con
        Builtin ann
ann fun
bn -> Term TyName Name uni fun ann -> m (Term TyName Name uni fun ann)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term TyName Name uni fun ann -> m (Term TyName Name uni fun ann))
-> Term TyName Name uni fun ann -> m (Term TyName Name uni fun ann)
forall a b. (a -> b) -> a -> b
$ ann -> fun -> Term TyName Name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann -> fun -> Term tyname name uni fun ann
Builtin ann
ann fun
bn