{-# OPTIONS --without-K #-}
module Class.Applicative.Instances where

open import Class.Prelude
open import Class.Functor.Core
open import Class.Functor.Instances
open import Class.Applicative.Core

instance
  Applicative-Maybe : Applicative Maybe
  Applicative-Maybe = λ where
    .pure → just
    ._<*>_ → maybe fmap (const nothing)

  Applicative₀-Maybe : Applicative₀ Maybe
  Applicative₀-Maybe .ε₀ = nothing

  Alternative-Maybe : Alternative Maybe
  Alternative-Maybe ._<|>_ = May._<∣>_
    where import Data.Maybe as May

  Applicative-List : Applicative List
  Applicative-List = λ where
    .pure → [_]
    ._<*>_ → flip $ concatMap ∘ _<&>_

  Applicative₀-List : Applicative₀ List
  Applicative₀-List .ε₀ = []

  Alternative-List : Alternative List
  Alternative-List ._<|>_ = _++_

  Applicative-List⁺ : Applicative List⁺
  Applicative-List⁺ = λ where
    .pure → L⁺.[_]
    ._<*>_ → flip $ L⁺.concatMap ∘ _<&>_
   where import Data.List.NonEmpty as L⁺

  Applicative-Vec : ∀ {n} → Applicative (flip Vec n)
  Applicative-Vec = λ where
    .pure → V.replicate _
    ._<*>_ → V._⊛_
   where import Data.Vec as V


  Applicative₀-Vec : Applicative₀ (flip Vec )
  Applicative₀-Vec .ε₀ = []

  -- Applicative-∃Vec : Applicative (∃ ∘ Vec)
  -- Applicative-∃Vec = λ where
  --   .pure x → 1 , pure x
  --   ._<*>_ (n , xs) (m , ys) → {! (n ⊔ m) , zipWith _$_ xs ys  -- (+ zipWith-⊔ lemma) !}

  private module M where
    open import Reflection.TCM.Syntax public
    open import Reflection.TCM public

  Alternative-TC : Alternative TC
  Alternative-TC = record {M}

  Applicative-TC : Applicative TC
  Applicative-TC = record {M}