Function.Strict

------------------------------------------------------------------------
-- The Agda standard library
--
-- Strict combinators (i.e. that use call-by-value)
------------------------------------------------------------------------

-- The contents of this module is also accessible via the `Function`
-- module.

{-# OPTIONS --without-K --safe #-}

module Function.Strict where

open import Agda.Builtin.Equality using (_≡_)
open import Function.Base using (flip)
open import Level using (Level)

private
  variable
    a b : Level
    A B : Set a

infixl 0 _!|>_ _!|>′_
infixr -1 _$!_ _$!′_

------------------------------------------------------------------------
-- Dependent combinators

-- These are functions whose output has a type that depends on the
-- value of the input to the function.

open import Agda.Builtin.Strict public
  renaming
  ( primForce      to force
  ; primForceLemma to force-≡
  )

-- Application
_$!_ : ∀ {A : Set a} {B : A → Set b} →
       ((x : A) → B x) → ((x : A) → B x)
f $! x = force x f

-- Flipped application
_!|>_ : ∀ {A : Set a} {B : A → Set b} →
       (a : A) → (∀ a → B a) → B a
_!|>_ = flip _$!_

------------------------------------------------------------------------
-- Non-dependent combinators

-- Any of the above operations for dependent functions will also work
-- for non-dependent functions but sometimes Agda has difficulty
-- inferring the non-dependency. Primed (′ = \prime) versions of the
-- operations are therefore provided below that sometimes have better
-- inference properties.

seq : A → B → B
seq a b = force a (λ _ → b)

seq-≡ : (a : A) (b : B) → seq a b ≡ b
seq-≡ a b = force-≡ a (λ _ → b)

force′ : A → (A → B) → B
force′ = force

force′-≡ : (a : A) (f : A → B) → force′ a f ≡ f a
force′-≡ = force-≡

-- Application
_$!′_ : (A → B) → (A → B)
_$!′_ = _$!_

-- Flipped application
_!|>′_ : A → (A → B) → B
_!|>′_ = _!|>_