{-# LANGUAGE DerivingStrategies    #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings     #-}
-- | Support for using de Bruijn indices for term and type names.
module PlutusCore.DeBruijn
    ( Index (..)
    , HasIndex (..)
    , DeBruijn (..)
    , NamedDeBruijn (..)
    , TyDeBruijn (..)
    , NamedTyDeBruijn (..)
    , FreeVariableError (..)
    , AsFreeVariableError (..)
    , unNameDeBruijn
    , unNameTyDeBruijn
    , fakeNameDeBruijn
    , deBruijnTy
    , deBruijnTerm
    , unDeBruijnTy
    , unDeBruijnTerm
    -- * unsafe api, use with care
    , deBruijnTyWith
    , deBruijnTermWith
    , unDeBruijnTyWith
    , unDeBruijnTermWith
    , freeIndexAsConsistentLevel
    , deBruijnInitIndex
    ) where

import PlutusCore.DeBruijn.Internal

import PlutusCore.Core.Type
import PlutusCore.Name
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 Levels m Unique)
    -> Type NamedTyDeBruijn uni ann
    -> m (Type TyName uni ann)
unDeBruijnTyWith :: (Index -> ReaderT Levels m Unique)
-> Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann)
unDeBruijnTyWith = (ReaderT Levels m (Type TyName uni ann) -> m (Type TyName uni ann)
forall (m :: * -> *) a. ReaderT Levels m a -> m a
runDeBruijnT (ReaderT Levels m (Type TyName uni ann) -> m (Type TyName uni ann))
-> (Type NamedTyDeBruijn uni ann
    -> ReaderT Levels 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 Levels m (Type TyName uni ann))
 -> Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann))
-> ((Index -> ReaderT Levels m Unique)
    -> Type NamedTyDeBruijn uni ann
    -> ReaderT Levels m (Type TyName uni ann))
-> (Index -> ReaderT Levels m Unique)
-> Type NamedTyDeBruijn uni ann
-> m (Type TyName uni ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Index -> ReaderT Levels m Unique)
-> Type NamedTyDeBruijn uni ann
-> ReaderT Levels m (Type TyName uni ann)
forall (m :: * -> *) (uni :: * -> *) ann.
(MonadReader Levels 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 Levels m Unique)
    -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
    -> m (Term TyName Name uni fun ann)
unDeBruijnTermWith :: (Index -> ReaderT Levels m Unique)
-> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
-> m (Term TyName Name uni fun ann)
unDeBruijnTermWith = (ReaderT Levels m (Term TyName Name uni fun ann)
-> m (Term TyName Name uni fun ann)
forall (m :: * -> *) a. ReaderT Levels m a -> m a
runDeBruijnT (ReaderT Levels m (Term TyName Name uni fun ann)
 -> m (Term TyName Name uni fun ann))
-> (Term NamedTyDeBruijn NamedDeBruijn uni fun ann
    -> ReaderT Levels 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 Levels m (Term TyName Name uni fun ann))
 -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
 -> m (Term TyName Name uni fun ann))
-> ((Index -> ReaderT Levels m Unique)
    -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
    -> ReaderT Levels m (Term TyName Name uni fun ann))
-> (Index -> ReaderT Levels 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 Levels m Unique)
-> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
-> ReaderT Levels m (Term TyName Name uni fun ann)
forall (m :: * -> *) (uni :: * -> *) fun ann.
(MonadReader Levels 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 :: Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann)
unDeBruijnTy = (Index -> ReaderT Levels m Unique)
-> Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann)
forall (m :: * -> *) (uni :: * -> *) ann.
MonadQuote m =>
(Index -> ReaderT Levels m Unique)
-> Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann)
unDeBruijnTyWith Index -> ReaderT Levels 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 :: Term NamedTyDeBruijn NamedDeBruijn uni fun ann
-> m (Term TyName Name uni fun ann)
unDeBruijnTerm = (Index -> ReaderT Levels m Unique)
-> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
-> m (Term TyName Name uni fun ann)
forall (m :: * -> *) (uni :: * -> *) fun ann.
MonadQuote m =>
(Index -> ReaderT Levels m Unique)
-> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
-> m (Term TyName Name uni fun ann)
unDeBruijnTermWith Index -> ReaderT Levels 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 :: Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann)
deBruijnTy = (Unique -> ReaderT Levels m Index)
-> Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann)
forall (m :: * -> *) (uni :: * -> *) ann.
Monad m =>
(Unique -> ReaderT Levels m Index)
-> Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann)
deBruijnTyWith Unique -> ReaderT Levels 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 :: Term TyName Name uni fun ann
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
deBruijnTerm = (Unique -> ReaderT Levels m Index)
-> Term TyName Name uni fun ann
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
forall (m :: * -> *) (uni :: * -> *) fun ann.
Monad m =>
(Unique -> ReaderT Levels m Index)
-> Term TyName Name uni fun ann
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
deBruijnTermWith Unique -> ReaderT Levels m Index
forall e (m :: * -> *).
(AsFreeVariableError e, MonadError e m) =>
Unique -> m Index
freeUniqueThrow

deBruijnTermWith
    :: Monad m
    => (Unique -> ReaderT Levels m Index)
    -> Term TyName Name uni fun ann
    -> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
deBruijnTermWith :: (Unique -> ReaderT Levels m Index)
-> Term TyName Name uni fun ann
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
deBruijnTermWith = (ReaderT Levels m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
forall (m :: * -> *) a. ReaderT Levels m a -> m a
runDeBruijnT (ReaderT Levels m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
 -> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann))
-> (Term TyName Name uni fun ann
    -> ReaderT
         Levels 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
       Levels m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann))
 -> Term TyName Name uni fun ann
 -> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann))
-> ((Unique -> ReaderT Levels m Index)
    -> Term TyName Name uni fun ann
    -> ReaderT
         Levels m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann))
-> (Unique -> ReaderT Levels 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 Levels m Index)
-> Term TyName Name uni fun ann
-> ReaderT
     Levels m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
forall (m :: * -> *) (uni :: * -> *) fun ann.
MonadReader Levels m =>
(Unique -> m Index)
-> Term TyName Name uni fun ann
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
deBruijnTermWithM

deBruijnTyWith
    :: Monad m
    => (Unique -> ReaderT Levels m Index)
    -> Type TyName uni ann
    -> m (Type NamedTyDeBruijn uni ann)
deBruijnTyWith :: (Unique -> ReaderT Levels m Index)
-> Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann)
deBruijnTyWith = (ReaderT Levels m (Type NamedTyDeBruijn uni ann)
-> m (Type NamedTyDeBruijn uni ann)
forall (m :: * -> *) a. ReaderT Levels m a -> m a
runDeBruijnT (ReaderT Levels m (Type NamedTyDeBruijn uni ann)
 -> m (Type NamedTyDeBruijn uni ann))
-> (Type TyName uni ann
    -> ReaderT Levels 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 Levels m (Type NamedTyDeBruijn uni ann))
 -> Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann))
-> ((Unique -> ReaderT Levels m Index)
    -> Type TyName uni ann
    -> ReaderT Levels m (Type NamedTyDeBruijn uni ann))
-> (Unique -> ReaderT Levels m Index)
-> Type TyName uni ann
-> m (Type NamedTyDeBruijn uni ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Unique -> ReaderT Levels m Index)
-> Type TyName uni ann
-> ReaderT Levels m (Type NamedTyDeBruijn uni ann)
forall (m :: * -> *) (uni :: * -> *) ann.
MonadReader Levels 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 Levels m
    => (Unique -> m Index)
    -> Type TyName uni ann
    -> m (Type NamedTyDeBruijn uni ann)
deBruijnTyWithM :: (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 Levels 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 Levels 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 Levels 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 Levels 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 Levels 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 Levels 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 Levels 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 (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 (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 (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
        -- boring non-recursive cases
        TyBuiltin ann
ann SomeTypeIn uni
con -> Type NamedTyDeBruijn uni ann -> m (Type NamedTyDeBruijn uni ann)
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
con

deBruijnTermWithM
    :: forall m uni fun ann. (MonadReader Levels m)
    => (Unique -> m Index)
    -> Term TyName Name uni fun ann
    -> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
deBruijnTermWithM :: (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 Levels 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 Levels 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 Levels 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 Levels 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 Levels 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 Levels 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 Levels 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 Levels 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 (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 (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 (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 (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 (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
        -- 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 (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 (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 Levels m, MonadQuote m)
    => (Index -> m Unique)
    -> Type NamedTyDeBruijn uni ann
    -> m (Type TyName uni ann)
unDeBruijnTyWithM :: (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 Levels 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 Levels 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 Levels 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
index Index
deBruijnInitIndex NamedTyDeBruijn
tn
            m (Type TyName uni ann) -> m (Type TyName uni ann)
forall (m :: * -> *) a. MonadReader Levels 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 Levels 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 Levels 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
index Index
deBruijnInitIndex NamedTyDeBruijn
tn
            m (Type TyName uni ann) -> m (Type TyName uni ann)
forall (m :: * -> *) a. MonadReader Levels 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 (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 (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 (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
      -- boring non-recursive cases
      TyBuiltin ann
ann SomeTypeIn uni
con -> Type TyName uni ann -> m (Type TyName uni ann)
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
con

-- | Takes a "handler" function to execute when encountering free variables.
unDeBruijnTermWithM
    :: forall m uni fun ann. (MonadReader Levels m, MonadQuote m)
    => (Index -> m Unique)
    -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann
    -> m (Term TyName Name uni fun ann)
unDeBruijnTermWithM :: (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 Levels 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 Levels 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 Levels 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 Levels 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
index Index
deBruijnInitIndex NamedTyDeBruijn
tn
              m (Term TyName Name uni fun ann)
-> m (Term TyName Name uni fun ann)
forall (m :: * -> *) a. MonadReader Levels 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 Levels 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 Levels m =>
(Index -> m Unique) -> NamedDeBruijn -> m Name
deBruijnToName Index -> m Unique
h (NamedDeBruijn -> m Name) -> NamedDeBruijn -> m Name
forall a b. (a -> b) -> a -> b
$ ASetter NamedDeBruijn NamedDeBruijn Index Index
-> Index -> NamedDeBruijn -> NamedDeBruijn
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter NamedDeBruijn NamedDeBruijn Index Index
forall a. HasIndex a => Lens' a Index
index Index
deBruijnInitIndex NamedDeBruijn
n
              m (Term TyName Name uni fun ann)
-> m (Term TyName Name uni fun ann)
forall (m :: * -> *) a. MonadReader Levels 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 (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 (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 (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 (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 (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
        -- 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 (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 (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