{-# OPTIONS --safe #-}
module Cubical.Data.Bool.SwitchStatement where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Bool.Base
open import Cubical.Data.Nat

{-
  Switch-case:

    _==_ : A → A → Bool

    _ : B
    _ = switch (λ x → x == fixedValue) cases
           case value1 ⇒ result1 break
           case value2 ⇒ result2 break
           ...
           case valueN ⇒ resultN break
           default⇒ defaultResult
-}


private
  variable
     ℓ' : Level


infixr 6 default⇒_
infixr 5 case_⇒_break_
infixr 4 switch_cases_

switch_cases_ : {A : Type } {B : Type ℓ'}  (A  Bool)  ((A  Bool)  B)  B
switch caseIndicator cases caseData = caseData caseIndicator

case_⇒_break_ : {A : Type } {B : Type ℓ'}  A  B  (otherCases : (A  Bool)  B)  (A  Bool)  B
case forValue  result break otherCases = λ caseIndicator  if (caseIndicator forValue) then result else (otherCases caseIndicator)

default⇒_ : {A : Type } {B : Type ℓ'}  B  (A  Bool)  B
default⇒_ value caseIndicator = value