{-|
Module      : Idris.DataOpts
Description : Optimisations for Idris code i.e. Forcing, detagging and collapsing.

License     : BSD3
Maintainer  : The Idris Community.
-}
{-# LANGUAGE FlexibleInstances, PatternGuards #-}

module Idris.DataOpts(applyOpts) where

import Idris.AbsSyntax
import Idris.Core.TT

class Optimisable term where
    applyOpts :: term -> Idris term

instance (Optimisable a, Optimisable b) => Optimisable (a, b) where
    applyOpts :: (a, b) -> Idris (a, b)
applyOpts (x :: a
x, y :: b
y) = (,) (a -> b -> (a, b))
-> StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) (b -> (a, b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> StateT IState (ExceptT Err IO) a
forall term. Optimisable term => term -> Idris term
applyOpts a
x StateT IState (ExceptT Err IO) (b -> (a, b))
-> StateT IState (ExceptT Err IO) b -> Idris (a, b)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> b -> StateT IState (ExceptT Err IO) b
forall term. Optimisable term => term -> Idris term
applyOpts b
y

instance (Optimisable a, Optimisable b) => Optimisable (vs, a, b) where
    applyOpts :: (vs, a, b) -> Idris (vs, a, b)
applyOpts (v :: vs
v, x :: a
x, y :: b
y) = (,,) vs
v (a -> b -> (vs, a, b))
-> StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) (b -> (vs, a, b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> StateT IState (ExceptT Err IO) a
forall term. Optimisable term => term -> Idris term
applyOpts a
x StateT IState (ExceptT Err IO) (b -> (vs, a, b))
-> StateT IState (ExceptT Err IO) b -> Idris (vs, a, b)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> b -> StateT IState (ExceptT Err IO) b
forall term. Optimisable term => term -> Idris term
applyOpts b
y

instance Optimisable a => Optimisable [a] where
    applyOpts :: [a] -> Idris [a]
applyOpts = (a -> StateT IState (ExceptT Err IO) a) -> [a] -> Idris [a]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM a -> StateT IState (ExceptT Err IO) a
forall term. Optimisable term => term -> Idris term
applyOpts

instance Optimisable a => Optimisable (Either a (a, a)) where
    applyOpts :: Either a (a, a) -> Idris (Either a (a, a))
applyOpts (Left  t :: a
t) = a -> Either a (a, a)
forall a b. a -> Either a b
Left  (a -> Either a (a, a))
-> StateT IState (ExceptT Err IO) a -> Idris (Either a (a, a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> StateT IState (ExceptT Err IO) a
forall term. Optimisable term => term -> Idris term
applyOpts a
t
    applyOpts (Right t :: (a, a)
t) = (a, a) -> Either a (a, a)
forall a b. b -> Either a b
Right ((a, a) -> Either a (a, a))
-> StateT IState (ExceptT Err IO) (a, a) -> Idris (Either a (a, a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a, a) -> StateT IState (ExceptT Err IO) (a, a)
forall term. Optimisable term => term -> Idris term
applyOpts (a, a)
t

-- Raw is for compile time optimisation (before type checking)
-- Term is for run time optimisation (after type checking, collapsing allowed)
-- Compile time: no collapsing

instance Optimisable Raw where
    applyOpts :: Raw -> Idris Raw
applyOpts t :: Raw
t@(RApp f :: Raw
f a :: Raw
a)
        | (Var n :: Name
n, args :: [Raw]
args) <- Raw -> (Raw, [Raw])
raw_unapply Raw
t -- MAGIC HERE
            = Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var Name
n) ([Raw] -> Raw) -> StateT IState (ExceptT Err IO) [Raw] -> Idris Raw
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Raw -> Idris Raw) -> [Raw] -> StateT IState (ExceptT Err IO) [Raw]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Raw -> Idris Raw
forall term. Optimisable term => term -> Idris term
applyOpts [Raw]
args
        | Bool
otherwise = Raw -> Raw -> Raw
RApp (Raw -> Raw -> Raw)
-> Idris Raw -> StateT IState (ExceptT Err IO) (Raw -> Raw)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Raw -> Idris Raw
forall term. Optimisable term => term -> Idris term
applyOpts Raw
f StateT IState (ExceptT Err IO) (Raw -> Raw)
-> Idris Raw -> Idris Raw
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Raw -> Idris Raw
forall term. Optimisable term => term -> Idris term
applyOpts Raw
a

    applyOpts (RBind n :: Name
n b :: Binder Raw
b t :: Raw
t) = Name -> Binder Raw -> Raw -> Raw
RBind Name
n (Binder Raw -> Raw -> Raw)
-> StateT IState (ExceptT Err IO) (Binder Raw)
-> StateT IState (ExceptT Err IO) (Raw -> Raw)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Binder Raw -> StateT IState (ExceptT Err IO) (Binder Raw)
forall term. Optimisable term => term -> Idris term
applyOpts Binder Raw
b StateT IState (ExceptT Err IO) (Raw -> Raw)
-> Idris Raw -> Idris Raw
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Raw -> Idris Raw
forall term. Optimisable term => term -> Idris term
applyOpts Raw
t
    applyOpts t :: Raw
t = Raw -> Idris Raw
forall (m :: * -> *) a. Monad m => a -> m a
return Raw
t

-- Erase types (makes ibc smaller, and we don't need them)
instance Optimisable (Binder (TT Name)) where
    applyOpts :: Binder (TT Name) -> Idris (Binder (TT Name))
applyOpts (Let r :: RigCount
r t :: TT Name
t v :: TT Name
v) = RigCount -> TT Name -> TT Name -> Binder (TT Name)
forall b. RigCount -> b -> b -> Binder b
Let RigCount
r (TT Name -> TT Name -> Binder (TT Name))
-> StateT IState (ExceptT Err IO) (TT Name)
-> StateT IState (ExceptT Err IO) (TT Name -> Binder (TT Name))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TT Name -> StateT IState (ExceptT Err IO) (TT Name)
forall (m :: * -> *) a. Monad m => a -> m a
return TT Name
forall n. TT n
Erased StateT IState (ExceptT Err IO) (TT Name -> Binder (TT Name))
-> StateT IState (ExceptT Err IO) (TT Name)
-> Idris (Binder (TT Name))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TT Name -> StateT IState (ExceptT Err IO) (TT Name)
forall term. Optimisable term => term -> Idris term
applyOpts TT Name
v
    applyOpts b :: Binder (TT Name)
b = Binder (TT Name) -> Idris (Binder (TT Name))
forall (m :: * -> *) a. Monad m => a -> m a
return (Binder (TT Name)
b { binderTy :: TT Name
binderTy = TT Name
forall n. TT n
Erased })

instance Optimisable (Binder Raw) where
    applyOpts :: Binder Raw -> StateT IState (ExceptT Err IO) (Binder Raw)
applyOpts b :: Binder Raw
b = do Raw
t' <- Raw -> Idris Raw
forall term. Optimisable term => term -> Idris term
applyOpts (Binder Raw -> Raw
forall b. Binder b -> b
binderTy Binder Raw
b)
                     Binder Raw -> StateT IState (ExceptT Err IO) (Binder Raw)
forall (m :: * -> *) a. Monad m => a -> m a
return (Binder Raw
b { binderTy :: Raw
binderTy = Raw
t' })

-- Run-time: do everything

prel :: [Text]
prel = [String -> Text
txt "Nat", String -> Text
txt "Prelude"]

instance Optimisable (TT Name) where
    applyOpts :: TT Name -> StateT IState (ExceptT Err IO) (TT Name)
applyOpts (P _ (NS (UN fn :: Text
fn) mod :: [Text]
mod) _)
       | Text
fn Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt "plus" Bool -> Bool -> Bool
&& [Text]
mod [Text] -> [Text] -> Bool
forall a. Eq a => a -> a -> Bool
== [Text]
prel
        = TT Name -> StateT IState (ExceptT Err IO) (TT Name)
forall (m :: * -> *) a. Monad m => a -> m a
return (NameType -> Name -> TT Name -> TT Name
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref (String -> Name
sUN "prim__addBigInt") TT Name
forall n. TT n
Erased)
    applyOpts (P _ (NS (UN fn :: Text
fn) mod :: [Text]
mod) _)
       | Text
fn Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt "mult" Bool -> Bool -> Bool
&& [Text]
mod [Text] -> [Text] -> Bool
forall a. Eq a => a -> a -> Bool
== [Text]
prel
        = TT Name -> StateT IState (ExceptT Err IO) (TT Name)
forall (m :: * -> *) a. Monad m => a -> m a
return (NameType -> Name -> TT Name -> TT Name
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref (String -> Name
sUN "prim__mulBigInt") TT Name
forall n. TT n
Erased)
    applyOpts (P _ (NS (UN fn :: Text
fn) mod :: [Text]
mod) _)
       | Text
fn Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt "divNat" Bool -> Bool -> Bool
&& [Text]
mod [Text] -> [Text] -> Bool
forall a. Eq a => a -> a -> Bool
== [Text]
prel
        = TT Name -> StateT IState (ExceptT Err IO) (TT Name)
forall (m :: * -> *) a. Monad m => a -> m a
return (NameType -> Name -> TT Name -> TT Name
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref (String -> Name
sUN "prim__sdivBigInt") TT Name
forall n. TT n
Erased)
    applyOpts (P _ (NS (UN fn :: Text
fn) mod :: [Text]
mod) _)
       | Text
fn Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt "modNat" Bool -> Bool -> Bool
&& [Text]
mod [Text] -> [Text] -> Bool
forall a. Eq a => a -> a -> Bool
== [Text]
prel
        = TT Name -> StateT IState (ExceptT Err IO) (TT Name)
forall (m :: * -> *) a. Monad m => a -> m a
return (NameType -> Name -> TT Name -> TT Name
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref (String -> Name
sUN "prim__sremBigInt") TT Name
forall n. TT n
Erased)
    applyOpts (App _ (P _ (NS (UN fn :: Text
fn) mod :: [Text]
mod) _) x :: TT Name
x)
       | Text
fn Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt "fromIntegerNat" Bool -> Bool -> Bool
&& [Text]
mod [Text] -> [Text] -> Bool
forall a. Eq a => a -> a -> Bool
== [Text]
prel
        = TT Name -> StateT IState (ExceptT Err IO) (TT Name)
forall term. Optimisable term => term -> Idris term
applyOpts TT Name
x
    applyOpts (P _ (NS (UN fn :: Text
fn) mod :: [Text]
mod) _)
       | Text
fn Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt "fromIntegerNat" Bool -> Bool -> Bool
&& [Text]
mod [Text] -> [Text] -> Bool
forall a. Eq a => a -> a -> Bool
== [Text]
prel
        = TT Name -> StateT IState (ExceptT Err IO) (TT Name)
forall (m :: * -> *) a. Monad m => a -> m a
return (AppStatus Name -> TT Name -> TT Name -> TT Name
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
forall n. AppStatus n
Complete (NameType -> Name -> TT Name -> TT Name
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref (Name -> [String] -> Name
sNS (String -> Name
sUN "id") ["Basics","Prelude"]) TT Name
forall n. TT n
Erased) TT Name
forall n. TT n
Erased)
    applyOpts (P _ (NS (UN fn :: Text
fn) mod :: [Text]
mod) _)
       | Text
fn Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt "toIntegerNat" Bool -> Bool -> Bool
&& [Text]
mod [Text] -> [Text] -> Bool
forall a. Eq a => a -> a -> Bool
== [Text]
prel
         = TT Name -> StateT IState (ExceptT Err IO) (TT Name)
forall (m :: * -> *) a. Monad m => a -> m a
return (AppStatus Name -> TT Name -> TT Name -> TT Name
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
forall n. AppStatus n
Complete (NameType -> Name -> TT Name -> TT Name
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref (Name -> [String] -> Name
sNS (String -> Name
sUN "id") ["Basics","Prelude"]) TT Name
forall n. TT n
Erased) TT Name
forall n. TT n
Erased)
    applyOpts c :: TT Name
c@(P (DCon t :: Int
t arity :: Int
arity uniq :: Bool
uniq) n :: Name
n _)
        = TT Name -> StateT IState (ExceptT Err IO) (TT Name)
forall (m :: * -> *) a. Monad m => a -> m a
return (TT Name -> StateT IState (ExceptT Err IO) (TT Name))
-> TT Name -> StateT IState (ExceptT Err IO) (TT Name)
forall a b. (a -> b) -> a -> b
$ Name -> Int -> Int -> Bool -> [TT Name] -> TT Name
applyDataOptRT Name
n Int
t Int
arity Bool
uniq []
    applyOpts t :: TT Name
t@(App s :: AppStatus Name
s f :: TT Name
f a :: TT Name
a)
        | (c :: TT Name
c@(P (DCon t :: Int
t arity :: Int
arity uniq :: Bool
uniq) n :: Name
n _), args :: [TT Name]
args) <- TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
t
            = Name -> Int -> Int -> Bool -> [TT Name] -> TT Name
applyDataOptRT Name
n Int
t Int
arity Bool
uniq ([TT Name] -> TT Name)
-> StateT IState (ExceptT Err IO) [TT Name]
-> StateT IState (ExceptT Err IO) (TT Name)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TT Name -> StateT IState (ExceptT Err IO) (TT Name))
-> [TT Name] -> StateT IState (ExceptT Err IO) [TT Name]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TT Name -> StateT IState (ExceptT Err IO) (TT Name)
forall term. Optimisable term => term -> Idris term
applyOpts [TT Name]
args
        | Bool
otherwise = AppStatus Name -> TT Name -> TT Name -> TT Name
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
s (TT Name -> TT Name -> TT Name)
-> StateT IState (ExceptT Err IO) (TT Name)
-> StateT IState (ExceptT Err IO) (TT Name -> TT Name)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TT Name -> StateT IState (ExceptT Err IO) (TT Name)
forall term. Optimisable term => term -> Idris term
applyOpts TT Name
f StateT IState (ExceptT Err IO) (TT Name -> TT Name)
-> StateT IState (ExceptT Err IO) (TT Name)
-> StateT IState (ExceptT Err IO) (TT Name)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TT Name -> StateT IState (ExceptT Err IO) (TT Name)
forall term. Optimisable term => term -> Idris term
applyOpts TT Name
a
    applyOpts (Bind n :: Name
n b :: Binder (TT Name)
b t :: TT Name
t) = Name -> Binder (TT Name) -> TT Name -> TT Name
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (Binder (TT Name) -> TT Name -> TT Name)
-> Idris (Binder (TT Name))
-> StateT IState (ExceptT Err IO) (TT Name -> TT Name)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Binder (TT Name) -> Idris (Binder (TT Name))
forall term. Optimisable term => term -> Idris term
applyOpts Binder (TT Name)
b StateT IState (ExceptT Err IO) (TT Name -> TT Name)
-> StateT IState (ExceptT Err IO) (TT Name)
-> StateT IState (ExceptT Err IO) (TT Name)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TT Name -> StateT IState (ExceptT Err IO) (TT Name)
forall term. Optimisable term => term -> Idris term
applyOpts TT Name
t
    applyOpts (Proj t :: TT Name
t i :: Int
i) = TT Name -> Int -> TT Name
forall n. TT n -> Int -> TT n
Proj (TT Name -> Int -> TT Name)
-> StateT IState (ExceptT Err IO) (TT Name)
-> StateT IState (ExceptT Err IO) (Int -> TT Name)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TT Name -> StateT IState (ExceptT Err IO) (TT Name)
forall term. Optimisable term => term -> Idris term
applyOpts TT Name
t StateT IState (ExceptT Err IO) (Int -> TT Name)
-> StateT IState (ExceptT Err IO) Int
-> StateT IState (ExceptT Err IO) (TT Name)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> StateT IState (ExceptT Err IO) Int
forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
i
    applyOpts t :: TT Name
t = TT Name -> StateT IState (ExceptT Err IO) (TT Name)
forall (m :: * -> *) a. Monad m => a -> m a
return TT Name
t

-- | Need to saturate arguments first to ensure that optimisation happens uniformly
applyDataOptRT :: Name -> Int -> Int -> Bool -> [Term] -> Term
applyDataOptRT :: Name -> Int -> Int -> Bool -> [TT Name] -> TT Name
applyDataOptRT n :: Name
n tag :: Int
tag arity :: Int
arity uniq :: Bool
uniq args :: [TT Name]
args
    | [TT Name] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TT Name]
args Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
arity = Name -> [TT Name] -> TT Name
doOpts Name
n [TT Name]
args
    | Bool
otherwise = let extra :: [Name]
extra = Int -> [Name]
satArgs (Int
arity Int -> Int -> Int
forall a. Num a => a -> a -> a
- [TT Name] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TT Name]
args)
                      tm :: TT Name
tm = Name -> [TT Name] -> TT Name
doOpts Name
n ((TT Name -> TT Name) -> [TT Name] -> [TT Name]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> TT Name -> TT Name
forall n. Int -> TT n -> TT n
weakenTm ([Name] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
extra)) [TT Name]
args [TT Name] -> [TT Name] -> [TT Name]
forall a. [a] -> [a] -> [a]
++ (Name -> TT Name) -> [Name] -> [TT Name]
forall a b. (a -> b) -> [a] -> [b]
map (\n :: Name
n -> NameType -> Name -> TT Name -> TT Name
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n TT Name
forall n. TT n
Erased) [Name]
extra)
                  in [Name] -> TT Name -> TT Name
forall n. Eq n => [n] -> TT n -> TT n
bind [Name]
extra TT Name
tm
  where
    satArgs :: Int -> [Name]
satArgs n :: Int
n = (Int -> Name) -> [Int] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (\i :: Int
i -> Int -> String -> Name
sMN Int
i "sat") [1..Int
n]

    bind :: [n] -> TT n -> TT n
bind [] tm :: TT n
tm = TT n
tm
    bind (n :: n
n:ns :: [n]
ns) tm :: TT n
tm = n -> Binder (TT n) -> TT n -> TT n
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
n (RigCount -> TT n -> Binder (TT n)
forall b. RigCount -> b -> Binder b
Lam RigCount
RigW TT n
forall n. TT n
Erased) (n -> TT n -> TT n
forall n. Eq n => n -> TT n -> TT n
pToV n
n ([n] -> TT n -> TT n
bind [n]
ns TT n
tm))

    -- Nat special cases
    -- TODO: Would be nice if this was configurable in idris source!
    -- Issue #1597 https://github.com/idris-lang/Idris-dev/issues/1597
    doOpts :: Name -> [TT Name] -> TT Name
doOpts (NS (UN z :: Text
z) [nat :: Text
nat, prelude :: Text
prelude]) []
        | Text
z Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt "Z" Bool -> Bool -> Bool
&& Text
nat Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt "Nat" Bool -> Bool -> Bool
&& Text
prelude Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt "Prelude"
          = Const -> TT Name
forall n. Const -> TT n
Constant (Integer -> Const
BI 0)
    doOpts (NS (UN s :: Text
s) [nat :: Text
nat, prelude :: Text
prelude]) [k :: TT Name
k]
        | Text
s Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt "S" Bool -> Bool -> Bool
&& Text
nat Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt "Nat" Bool -> Bool -> Bool
&& Text
prelude Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt "Prelude"
          = AppStatus Name -> TT Name -> TT Name -> TT Name
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
forall n. AppStatus n
Complete (AppStatus Name -> TT Name -> TT Name -> TT Name
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
forall n. AppStatus n
Complete (NameType -> Name -> TT Name -> TT Name
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref (String -> Name
sUN "prim__addBigInt") TT Name
forall n. TT n
Erased) TT Name
k) (Const -> TT Name
forall n. Const -> TT n
Constant (Integer -> Const
BI 1))

    doOpts n :: Name
n args :: [TT Name]
args = TT Name -> [TT Name] -> TT Name
forall n. TT n -> [TT n] -> TT n
mkApp (NameType -> Name -> TT Name -> TT Name
forall n. NameType -> n -> TT n -> TT n
P (Int -> Int -> Bool -> NameType
DCon Int
tag Int
arity Bool
uniq) Name
n TT Name
forall n. TT n
Erased) [TT Name]
args