Library zoo_std.clist

From zoo Require Import
  prelude.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_std Require Export
  base
  clist__types
  clist__code.
From zoo Require Import
  options.

Implicit Types v t fn : val.

Inductive clist :=
  | ClistClosed
  | ClistOpen
  | ClistCons v (cvs : clist).
Implicit Types cvs : clist.

Fixpoint clist_to_val cvs :=
  match cvs with
  | ClistClosed ⇒
      §ClistClosed
  | ClistOpen ⇒
      §ClistOpen
  | ClistCons v cvs ⇒
      ‘ClistCons[ v, clist_to_val cvs ]
  end%V.
Coercion clist_to_val : clist >-> val.

#[global] Instance clist_to_val_inj_similar :
  Inj (=) (≈@{val}) clist_to_val.
#[global] Instance clist_to_val_inj :
  Inj (=) (=) clist_to_val.

Fixpoint list_to_clist_open vs :=
  match vs with
  | [] ⇒
      ClistOpen
  | v :: vs ⇒
      ClistCons v (list_to_clist_open vs)
  end.
Fixpoint list_to_clist_closed vs :=
  match vs with
  | [] ⇒
      ClistClosed
  | v :: vs ⇒
      ClistCons v (list_to_clist_closed vs)
  end.

#[global] Instance list_to_clist_open_inj :
  Inj (=) (=) list_to_clist_open.
#[global] Instance list_to_clist_closed_inj :
  Inj (=) (=) list_to_clist_closed.
Lemma list_to_clist_open_closed vs1 vs2 :
  list_to_clist_open vs1 ≠ list_to_clist_closed vs2.
Lemma list_to_clist_open_not_closed vs :
  list_to_clist_open vs ≠ ClistClosed.
Lemma list_to_clist_open_not_closed' vs :
  ClistClosed ≠ list_to_clist_open vs.

Fixpoint clist_app vs1 cvs2 :=
  match vs1 with
  | [] ⇒
      cvs2
  | v :: vs1 ⇒
      ClistCons v (clist_app vs1 cvs2)
  end.

Lemma clist_app_open {vs1 cvs2} vs2 :
  cvs2 = list_to_clist_open vs2 →
  clist_app vs1 cvs2 = list_to_clist_open (vs1 ++ vs2).
Lemma clist_app_ClistOpen vs :
  clist_app vs ClistOpen = list_to_clist_open vs.
Lemma clist_app_closed {vs1 cvs2} vs2 :
  cvs2 = list_to_clist_closed vs2 →
  clist_app vs1 cvs2 = list_to_clist_closed (vs1 ++ vs2).
Lemma clist_app_ClistClosed vs :
  clist_app vs ClistClosed = list_to_clist_closed vs.
Lemma clist_app_assoc vs1 vs2 cvs :
  clist_app (vs1 ++ vs2) cvs = clist_app vs1 (clist_app vs2 cvs).

Section zoo_G.
  Context `{zoo_G : !ZooG Σ}.

  Lemma wp_match_clist_open vs e1 x2 e2 Φ :
    WP subst' x2 (list_to_clist_open vs) e2 {{ Φ }} ⊢
    WP match: list_to_clist_open vs with ClistClosed ⇒ e1 |_ as: x2 ⇒ e2 end {{ Φ }}.

  Lemma clist٠app𑁒spec {t1} vs1 {t2} cvs2 :
    t1 = list_to_clist_open vs1 →
    t2 = cvs2 →
    {{{
      True
    }}}
      clist٠app t1 t2
    {{{
      RET clist_app vs1 cvs2;
      True
    }}}.

  Lemma clist٠rev_app𑁒spec {t1} vs1 {t2} cvs2 :
    t1 = list_to_clist_open vs1 →
    t2 = cvs2 →
    {{{
      True
    }}}
      clist٠rev_app t1 t2
    {{{
      RET clist_app (reverse vs1) cvs2;
      True
    }}}.

  #[local] Lemma clist٠iter𑁒spec_aux vs_left Ψ vs fn t vs_right :
    vs = vs_left ++ vs_right →
    t = list_to_clist_open vs_right →
    {{{
      ▷ Ψ vs_left ∗
      ( [∗ list] i ↦ v ∈ vs_right,
        Ψ (vs_left ++ take i vs_right) -∗
        WP fn v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ (vs_left ++ take i vs_right ++ [v])
        }}
      )
    }}}
      clist٠iter fn t
    {{{
      RET ();
      Ψ vs
    }}}.
  Lemma clist٠iter𑁒spec Ψ t vs fn :
    t = list_to_clist_open vs →
    {{{
      ▷ Ψ [] ∗
      ( [∗ list] i ↦ v ∈ vs,
        Ψ (take i vs) -∗
        WP fn v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ (take i vs ++ [v])
        }}
      )
    }}}
      clist٠iter fn t
    {{{
      RET ();
      Ψ vs
    }}}.
  Lemma clist٠iter𑁒spec_disentangled Ψ t vs fn :
    t = list_to_clist_open vs →
    {{{
      [∗ list] v ∈ vs,
        WP fn v {{ res,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ v
        }}
    }}}
      clist٠iter fn t
    {{{
      RET ();
      [∗ list] v ∈ vs,
        Ψ v
    }}}.
End zoo_G.

From zoo_std Require
  clist__opaque.