Library zoo_std.deque__code

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

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

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

Definition deque٠push_front : val :=
  fun: "t" "v" ⇒
    xdeque٠push_front "t" { "t", "t", "v" }.

Definition deque٠push_back : val :=
  fun: "t" "v" ⇒
    xdeque٠push_back "t" { "t", "t", "v" }.

Definition deque٠pop_front : val :=
  fun: "t" ⇒
    match: xdeque٠pop_front "t" with
    | None ⇒
        §None
    | Some "node" ⇒
        ‘Some( "node".{xdeque_data} )
    end.

Definition deque٠pop_back : val :=
  fun: "t" ⇒
    match: xdeque٠pop_back "t" with
    | None ⇒
        §None
    | Some "node" ⇒
        ‘Some( "node".{xdeque_data} )
    end.

Definition deque٠iter : val :=
  fun: "fn" ⇒
    xdeque٠iter (fun: "node" ⇒ "fn" "node".{xdeque_data}).