--- This module provides an implementation of a First-In, First-Out (FIFO)
--- queue based on Okasaki's "Purely Functional Data Structures." Ch.3.
---
--- This Okasaki Queue version data structure ensures amortized constant-time
--- performance for basic operations such as push, pop, and front.
---
--- The Okasaki Queue consists of two lists (front and back) to separate
--- the concerns of adding and removing elements for ensuring efficient
--- performance.
module Stdlib.Data.Queue.Base;

import Stdlib.Data.List open;
import Stdlib.Data.Bool open;
import Stdlib.Data.Maybe open;
import Stdlib.Data.Pair open;
import Stdlib.Data.Nat open;
import Stdlib.Function open;
import Stdlib.Trait.Foldable open;

--- A first-in-first-out data structure
type Queue (A : Type) :=
  mkQueue@{
    front : List A;
    back : List A;
  };

--- 𝒪(1). The empty ;Queue;.
empty {A} : Queue A := mkQueue nil nil;

--- 𝒪(1). Returns ;true; when the ;Queue; has no elements.
isEmpty {A} (queue : Queue A) : Bool :=
  case queue of
    | mkQueue nil nil := true
    | _ := false;

--- 𝒪(1). Returns first element of the ;Queue;, if any.
head {A} (queue : Queue A) : Maybe A :=
  case queue of
    | mkQueue nil _ := nothing
    | mkQueue (x :: _) _ := just x;

--- 𝒪(1). Removes the first element from the ;Queue;. If the ;Queue; is empty
--  then returns ;nothing;.
tail {A} (queue : Queue A) : Maybe (Queue A) :=
  case queue of
    | mkQueue nil _ := nothing
    | mkQueue (_ :: front) back := just (mkQueue front back);

--- 𝒪(n) worst-case, but 𝒪(1) amortized
{-# inline: true #-}
check {A} (queue : Queue A) : Queue A :=
  case queue of
    | mkQueue nil back := mkQueue (reverse back) nil
    | q := q;

--- 𝒪(n) worst-case, but 𝒪(1) amortized. Returns the first element and the
--  rest of the ;Queue;. If the ;Queue; is empty then returns ;nothing;.
pop {A} (queue : Queue A) : Maybe (Pair A (Queue A)) :=
  case queue of
    | mkQueue nil _ := nothing
    | mkQueue (x :: front) back := just (x, check (mkQueue front back));

--- 𝒪(1). Adds an element to the end of the ;Queue;.
push {A} (x : A) (queue : Queue A) : Queue A :=
  case queue of mkQueue front back := check (mkQueue front (x :: back));

--- 𝒪(n). Adds a list of elements to the end of the ;Queue;.
pushMany {A} (list : List A) (queue : Queue A) : Queue A :=
  for (acc := queue) (x in list) {
    push x acc
  };

--- 𝒪(n). Build a ;Queue; from a ;List;.
fromList {A} (list : List A) : Queue A := pushMany list empty;

--- toList: O(n). Returns a ;List; of the elements in the ;Queue;.
--- The elements are in the same order as they appear in the ;Queue;
--- (i.e. the first element of the ;Queue; is the first element of the ;List;).
toList {A} (queue : Queue A) : List A :=
  case queue of mkQueue front back := front ++ reverse back;

--- 𝒪(n). Returns the number of elements in the ;Queue;.
size {A} (queue : Queue A) : Nat :=
  case queue of mkQueue front back := length front + length back;

instance
eqQueueI {A} {{Eq A}} : Eq (Queue A) := mkEq ((==) on toList);

instance
showQueueI {A} {{Show A}} : Show (Queue A) := mkShow (toList >> Show.show);

instance
ordQueueI {A} {{Ord A}} : Ord (Queue A) := mkOrd (Ord.cmp on toList);