------------------------------------------------------------------------
-- 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 --cubical-compatible --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
_!|>′_ = _!|>_