include "utilities/bind_new.ma".

definition bind_list ≝ λB,E.bind_new B (list E).

coercion blist_from_list :
  ∀B,E. ∀l:list E. bind_list B E ≝ λB,E,l.bret … l on _l : list ? to bind_list ??.

unification hint 0 ≔ B,E;
Es ≟ list E
(*--------------------------*)⊢
bind_list B E ≡ bind_new B Es.

definition bappend : ∀B,E.bind_list B E → bind_list B E →
  bind_list B E ≝ λB,E. m_bin_op … (append ?).

include "ASM/Vector.ma".
interpretation "append blist" 'vappend l1 l2 = (bappend ?? l1 l2).

definition bcons : ∀B,E.E → bind_list B E → bind_list B E ≝
  λB,E,e.m_map … (cons … e).
interpretation "cons blist" 'vcons l1 l2 = (bcons ?? l1 l2).

include "utilities/lists.ma".
  
theorem bcompile_append :
  ∀U, R, E, fresh, bl1, bl2.
  (bcompile U R (list E) fresh (bl1 @@ bl2)) ≅
  (
  ! l1 ← bcompile … fresh bl1 ;
  ! l2 ← bcompile … fresh bl2 ;
  return (l1 @ l2)
  ).
  #U#R#E#fresh#bl1#bl2
  #u >bcompile_bbind normalize @pair_elim
  #u' #l' normalize @pair_elim
  #u'' #l'' normalize >bcompile_bbind #EQ #EQ'
  normalize >EQ normalize //
qed.

theorem bcompile_cons :
  ∀U, R, E, fresh, e, bl2.
  (bcompile U R (list E) fresh (e ::: bl2)) ≅
    ! l ← bcompile … fresh bl2 ; return (e :: l).
      #U#R#E#fresh#e#bl2 #u @bcompile_bbind
qed.