-- | Contexts with at most one hole.

module Agda.Utils.AffineHole where



data AffineHole r a
  = ZeroHoles a
      -- ^ A constant term.
  | OneHole (r -> a) r
      -- ^ A term with one hole and the (old) contents.
  | ManyHoles
      -- ^ A term with many holes (error value).
  deriving (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
<$ :: forall a b. a -> AffineHole r b -> AffineHole r a
$c<$ :: forall r a b. a -> AffineHole r b -> AffineHole r a
fmap :: forall a b. (a -> b) -> AffineHole r a -> AffineHole r b
$cfmap :: forall r a b. (a -> b) -> AffineHole r a -> AffineHole r b
Functor)

instance Applicative (AffineHole r) where
  pure :: forall a. a -> AffineHole r a
pure = 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 = forall r a. a -> AffineHole r a
ZeroHoles forall a b. (a -> b) -> a -> b
$ a -> b
f a
a
  ZeroHoles a -> b
f <*> OneHole r -> a
g r
y = forall r a. (r -> a) -> r -> AffineHole r a
OneHole (a -> b
f 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 = 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
_ = forall r a. AffineHole r a
ManyHoles

-- NB: @AffineHole r@ is not a monad.
-- @
--   OneHole (h :: r -> a) >>= (k :: a -> AffineHole r b) = _ :: AffineHole r b
-- @
-- We are lacking an @r@ to make use of @h@.