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