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

module OWL2.Foundation.NonEmpty where

open import OWL2.Prelude

record OneOrMore {ℓ : Level} (A : Type ℓ) : Type ℓ where
  constructor oneOrMore
  field
    head : A
    tail : List A

open OneOrMore public

record TwoOrMore {ℓ : Level} (A : Type ℓ) : Type ℓ where
  constructor twoOrMore
  field
    first  : A
    second : A
    rest   : List A

open TwoOrMore public

oneOrMoreToList : ∀ {ℓ} {A : Type ℓ} → OneOrMore A → List A
oneOrMoreToList xs =
  head xs ∷ tail xs

twoOrMoreToList : ∀ {ℓ} {A : Type ℓ} → TwoOrMore A → List A
twoOrMoreToList xs =
  first xs ∷ second xs ∷ rest xs

twoOrMoreToOneOrMore :
  ∀ {ℓ} {A : Type ℓ} → TwoOrMore A → OneOrMore A
twoOrMoreToOneOrMore xs =
  oneOrMore (first xs) (second xs ∷ rest xs)

mapOneOrMore :
  ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} →
  (A → B) → OneOrMore A → OneOrMore B
mapOneOrMore f xs =
  oneOrMore (f (head xs)) (map f (tail xs))

mapTwoOrMore :
  ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} →
  (A → B) → TwoOrMore A → TwoOrMore B
mapTwoOrMore f xs =
  twoOrMore (f (first xs)) (f (second xs)) (map f (rest xs))

listToOneOrMore : ∀ {ℓ} {A : Type ℓ} → List A → Optional (OneOrMore A)
listToOneOrMore [] =
  absent
listToOneOrMore (x ∷ xs) =
  present (oneOrMore x xs)

listToTwoOrMore : ∀ {ℓ} {A : Type ℓ} → List A → Optional (TwoOrMore A)
listToTwoOrMore [] =
  absent
listToTwoOrMore (x ∷ []) =
  absent
listToTwoOrMore (x ∷ y ∷ xs) =
  present (twoOrMore x y xs)