Library zoo_std.stack

Require Import zoo.prelude.
Require Import zoo.base.
Require Export zoo_std.stack__code.
Require Import zoo_std.stack__types.
Require Import zoo.options.

Implicit Type v t : val.

Section zoo ۰ G.
  Context `{zoo ۰ G : !ZooG Σ}.

  Definition stack ۰ model t vs :=
    dynarray_1 ۰ model t (reverse vs).

  #[global] Instance stack ۰ model ｰ timeless t vs :
    Timeless (stack ۰ model t vs).

  Lemma stack ٠ make ｰ spec :
    {{{
      True
    }}}
      stack ٠ create ()
    {{{
      t
    , RET t ;
      stack ۰ model t []
    }}}.

  Lemma stack ٠ is_empty ｰ spec t vs :
    {{{
      stack ۰ model t vs
    }}}
      stack ٠ is_empty t
    {{{
      RET #(bool_decide (vs = []%list));
      stack ۰ model t vs
    }}}.

  Lemma stack ٠ push ｰ spec t vs v :
    {{{
      stack ۰ model t vs
    }}}
      stack ٠ push t v
    {{{
      RET ();
      stack ۰ model t (v :: vs)
    }}}.

  Lemma stack ٠ pop ｰ spec {t vs} v vs' :
    vs = v :: vs' →
    {{{
      stack ۰ model t vs
    }}}
      stack ٠ pop t
    {{{
      RET v ;
      stack ۰ model t vs'
    }}}.
End zoo ۰ G.

Require zoo_std.stack__opaque.

#[global] Opaque stack ۰ model.