{-# OPTIONS_GHC -Wunused-imports #-}
module Agda.Utils.AffineHole where
data AffineHole r a
= ZeroHoles a
| OneHole (r -> a) r
| ManyHoles
deriving ((forall a b. (a -> b) -> AffineHole r a -> AffineHole r b)
-> (forall a b. a -> AffineHole r b -> AffineHole r a)
-> Functor (AffineHole r)
forall a b. a -> AffineHole r b -> AffineHole r a
forall a b. (a -> b) -> AffineHole r a -> AffineHole r b
forall r a b. a -> AffineHole r b -> AffineHole r a
forall r a b. (a -> b) -> AffineHole r a -> AffineHole r b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall r a b. (a -> b) -> AffineHole r a -> AffineHole r b
fmap :: forall a b. (a -> b) -> AffineHole r a -> AffineHole r b
$c<$ :: forall r a b. a -> AffineHole r b -> AffineHole r a
<$ :: forall a b. a -> AffineHole r b -> AffineHole r a
Functor)
instance Applicative (AffineHole r) where
pure :: forall a. a -> AffineHole r a
pure = a -> AffineHole r a
forall r a. a -> AffineHole r a
ZeroHoles
ZeroHoles a -> b
f <*> :: forall a b.
AffineHole r (a -> b) -> AffineHole r a -> AffineHole r b
<*> ZeroHoles a
a = b -> AffineHole r b
forall r a. a -> AffineHole r a
ZeroHoles (b -> AffineHole r b) -> b -> AffineHole r b
forall a b. (a -> b) -> a -> b
$ a -> b
f a
a
ZeroHoles a -> b
f <*> OneHole r -> a
g r
y = (r -> b) -> r -> AffineHole r b
forall r a. (r -> a) -> r -> AffineHole r a
OneHole (a -> b
f (a -> b) -> (r -> a) -> r -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. r -> a
g) r
y
OneHole r -> a -> b
h r
x <*> ZeroHoles a
a = (r -> b) -> r -> AffineHole r b
forall r a. (r -> a) -> r -> AffineHole r a
OneHole (r -> a -> b
`h` a
a) r
x
AffineHole r (a -> b)
_ <*> AffineHole r a
_ = AffineHole r b
forall r a. AffineHole r a
ManyHoles