{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
module PlutusCore.DeBruijn
( Index (..)
, Level (..)
, LevelInfo (..)
, HasIndex (..)
, DeBruijn (..)
, NamedDeBruijn (..)
, FakeNamedDeBruijn (unFakeNamedDeBruijn)
, TyDeBruijn (..)
, NamedTyDeBruijn (..)
, FreeVariableError (..)
, AsFreeVariableError (..)
, unNameDeBruijn
, unNameTyDeBruijn
, fakeNameDeBruijn
, fakeTyNameDeBruijn
, deBruijnTy
, deBruijnTerm
, unDeBruijnTy
, unDeBruijnTerm
, 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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
TyForall ann
ann NamedTyDeBruijn
tn Kind ann
k Type NamedTyDeBruijn uni ann
ty ->
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 ->
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
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
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
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
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
TyAbs ann
ann NamedTyDeBruijn
tn Kind ann
k Term NamedTyDeBruijn NamedDeBruijn uni fun ann
t ->
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 ->
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
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
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