------------------------------------------------------------------------
-- The Agda standard library
--
-- Examples showing how the case expressions can be used with anonymous
-- pattern-matching lambda abstractions
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module README.Case where

open import Data.Fin   hiding (pred)
open import Data.Maybe hiding (from-just)
open import Data.Nat   hiding (pred)
open import Function.Base using (case_of_; case_returning_of_)
open import Relation.Nullary

------------------------------------------------------------------------
-- Different types of pattern-matching lambdas

-- absurd pattern

empty : ∀ {a} {A : Set a} → Fin 0 → A
empty i = case i of λ ()

-- {}-delimited and ;-separated list of clauses
-- Note that they do not need to be on different lines

pred : ℕ → ℕ
pred n = case n of λ
  { zero    → zero
  ; (suc n) → n
  }

-- where-introduced and indentation-identified block of list of clauses

from-just : ∀ {a} {A : Set a} (x : Maybe A) → From-just x
from-just x = case x returning From-just of λ where
  (just x) → x
  nothing  → _

------------------------------------------------------------------------
-- We can define some recursive functions with case

plus : ℕ → ℕ → ℕ
plus m n = case m of λ
   { zero    → n
   ; (suc m) → suc (plus m n)
   }

div2 : ℕ → ℕ
div2 zero    = zero
div2 (suc m) = case m of λ where
  zero     → zero
  (suc m′) → suc (div2 m′)


-- Note that some natural uses of case are rejected by the termination
-- checker:

-- module _ {a} {A : Set a} (eq? : Decidable {A = A} _≡_) where

--  pairBy : List A → List (A ⊎ (A × A))
--  pairBy []           = []
--  pairBy (x ∷ [])     = inj₁ x ∷ []
--  pairBy (x ∷ y ∷ xs) = case eq? x y of λ where
--    (yes _) → inj₂ (x , y) ∷ pairBy xs
--    (no _)  → inj₁ x ∷ pairBy (y ∷ xs)