{-# 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 (a
x, 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 a b.
StateT IState (ExceptT Err IO) (a -> b)
-> StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) 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 (vs
v, a
x, 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 a b.
StateT IState (ExceptT Err IO) (a -> b)
-> StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) 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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 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 (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
instance Optimisable Raw where
applyOpts :: Raw -> Idris Raw
applyOpts t :: Raw
t@(RApp Raw
f Raw
a)
| (Var Name
n, [Raw]
args) <- Raw -> (Raw, [Raw])
raw_unapply Raw
t
= 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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 a b.
StateT IState (ExceptT Err IO) (a -> b)
-> StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
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 Name
n Binder Raw
b 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 a b.
StateT IState (ExceptT Err IO) (a -> b)
-> StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
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 Raw
t = Raw -> Idris Raw
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Raw
t
instance Optimisable (Binder (TT Name)) where
applyOpts :: Binder (TT Name) -> Idris (Binder (TT Name))
applyOpts (Let RigCount
r TT Name
t 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 a. a -> StateT IState (ExceptT Err IO) a
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 a b.
StateT IState (ExceptT Err IO) (a -> b)
-> StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
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 Binder (TT Name)
b = Binder (TT Name) -> Idris (Binder (TT Name))
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Binder (TT Name)
b { binderTy = Erased })
instance Optimisable (Binder Raw) where
applyOpts :: Binder Raw -> StateT IState (ExceptT Err IO) (Binder Raw)
applyOpts 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 a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Binder Raw
b { binderTy = t' })
prel :: [Text]
prel = [String -> Text
txt String
"Nat", String -> Text
txt String
"Prelude"]
instance Optimisable (TT Name) where
applyOpts :: TT Name -> StateT IState (ExceptT Err IO) (TT Name)
applyOpts (P NameType
_ (NS (UN Text
fn) [Text]
mod) TT Name
_)
| Text
fn Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"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 a. a -> StateT IState (ExceptT Err IO) a
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 String
"prim__addBigInt") TT Name
forall n. TT n
Erased)
applyOpts (P NameType
_ (NS (UN Text
fn) [Text]
mod) TT Name
_)
| Text
fn Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"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 a. a -> StateT IState (ExceptT Err IO) a
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 String
"prim__mulBigInt") TT Name
forall n. TT n
Erased)
applyOpts (P NameType
_ (NS (UN Text
fn) [Text]
mod) TT Name
_)
| Text
fn Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"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 a. a -> StateT IState (ExceptT Err IO) a
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 String
"prim__sdivBigInt") TT Name
forall n. TT n
Erased)
applyOpts (P NameType
_ (NS (UN Text
fn) [Text]
mod) TT Name
_)
| Text
fn Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"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 a. a -> StateT IState (ExceptT Err IO) a
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 String
"prim__sremBigInt") TT Name
forall n. TT n
Erased)
applyOpts (App AppStatus Name
_ (P NameType
_ (NS (UN Text
fn) [Text]
mod) TT Name
_) TT Name
x)
| Text
fn Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"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 NameType
_ (NS (UN Text
fn) [Text]
mod) TT Name
_)
| Text
fn Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"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 a. a -> StateT IState (ExceptT Err IO) a
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 String
"id") [String
"Basics",String
"Prelude"]) TT Name
forall n. TT n
Erased) TT Name
forall n. TT n
Erased)
applyOpts (P NameType
_ (NS (UN Text
fn) [Text]
mod) TT Name
_)
| Text
fn Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"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 a. a -> StateT IState (ExceptT Err IO) a
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 String
"id") [String
"Basics",String
"Prelude"]) TT Name
forall n. TT n
Erased) TT Name
forall n. TT n
Erased)
applyOpts c :: TT Name
c@(P (DCon Int
t Int
arity Bool
uniq) Name
n TT Name
_)
= TT Name -> StateT IState (ExceptT Err IO) (TT Name)
forall a. a -> StateT IState (ExceptT Err IO) a
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 AppStatus Name
s TT Name
f TT Name
a)
| (c :: TT Name
c@(P (DCon Int
t Int
arity Bool
uniq) Name
n TT Name
_), [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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 a b.
StateT IState (ExceptT Err IO) (a -> b)
-> StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
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 Name
n Binder (TT Name)
b 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 a b.
StateT IState (ExceptT Err IO) (a -> b)
-> StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
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 TT Name
t 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 a b.
StateT IState (ExceptT Err IO) (a -> b)
-> StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> StateT IState (ExceptT Err IO) Int
forall a. a -> StateT IState (ExceptT Err IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
i
applyOpts TT Name
t = TT Name -> StateT IState (ExceptT Err IO) (TT Name)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return TT Name
t
applyDataOptRT :: Name -> Int -> Int -> Bool -> [Term] -> Term
applyDataOptRT :: Name -> Int -> Int -> Bool -> [TT Name] -> TT Name
applyDataOptRT Name
n Int
tag Int
arity Bool
uniq [TT Name]
args
| [TT Name] -> Int
forall a. [a] -> 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 a. [a] -> 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 a. [a] -> 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 (\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 Int
n = (Int -> Name) -> [Int] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (\Int
i -> Int -> String -> Name
sMN Int
i String
"sat") [Int
1..Int
n]
bind :: [n] -> TT n -> TT n
bind [] TT n
tm = TT n
tm
bind (n
n:[n]
ns) 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))
doOpts :: Name -> [TT Name] -> TT Name
doOpts (NS (UN Text
z) [Text
nat, Text
prelude]) []
| Text
z Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"Z" Bool -> Bool -> Bool
&& Text
nat Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"Nat" Bool -> Bool -> Bool
&& Text
prelude Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"Prelude"
= Const -> TT Name
forall n. Const -> TT n
Constant (Integer -> Const
BI Integer
0)
doOpts (NS (UN Text
s) [Text
nat, Text
prelude]) [TT Name
k]
| Text
s Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"S" Bool -> Bool -> Bool
&& Text
nat Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"Nat" Bool -> Bool -> Bool
&& Text
prelude Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"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 String
"prim__addBigInt") TT Name
forall n. TT n
Erased) TT Name
k) (Const -> TT Name
forall n. Const -> TT n
Constant (Integer -> Const
BI Integer
1))
doOpts Name
n [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