Library zoo_std.deque__code

Require Import zoo.prelude.
Require Import zoo.language.typeclasses.
Require Import zoo.language.notations.
Require Import zoo_std.xdeque.
Require Import zoo.options.

Definition deque ٠ create : val :=
  xdeque ٠ create.

Definition deque ٠ is_empty : val :=
  xdeque ٠ is_empty.

Definition deque ٠ push_front : val :=
  𝗳𝘂𝗻 "t" "v" →
    xdeque ٠ push_front "t" { "t", "t", "v" }.

Definition deque ٠ push_back : val :=
  𝗳𝘂𝗻 "t" "v" →
    xdeque ٠ push_back "t" { "t", "t", "v" }.

Definition deque ٠ pop_front : val :=
  𝗳𝘂𝗻 "t" →
    𝗺𝗮𝘁𝗰𝗵 xdeque ٠ pop_front "t" 𝘄𝗶𝘁𝗵
    | None →
        §None
    | Some "node" →
        ‘Some ( "node".{xdeque ٠ data } )
    𝗲𝗻𝗱.

Definition deque ٠ pop_back : val :=
  𝗳𝘂𝗻 "t" →
    𝗺𝗮𝘁𝗰𝗵 xdeque ٠ pop_back "t" 𝘄𝗶𝘁𝗵
    | None →
        §None
    | Some "node" →
        ‘Some ( "node".{xdeque ٠ data } )
    𝗲𝗻𝗱.

Definition deque ٠ iter : val :=
  𝗳𝘂𝗻 "fn" →
    xdeque ٠ iter (𝗳𝘂𝗻 "node" → "fn" "node".{xdeque ٠ data }).