include "utilities/monad.ma".
include "basics/lists/list.ma".

inductive bind_list
  (B : Type[0])
  (T : Type[0])
  (E : Type[0])
  : Type[0] ≝
  | bnil : bind_list B T E
  | bcons : E → bind_list B T E → bind_list B T E
  | bnew : T → (B → bind_list B T E) → bind_list B T E.
  
interpretation "new blist" 'new t f = (bnew ??? t f).
interpretation "cons blist" 'cons hd tl = (bcons ??? hd tl).
interpretation "nil blist" 'nil = (bnil ???).

notation > "ν list1 ident x sep , opt('of' t) 'in' f"
  with precedence 48 for
  ${ default
    @{ ${ fold right @{$f} rec acc @{'new $t (λ${ident x}.$acc)} } }
    @{ ${ fold right @{$f} rec acc @{'new 'it (λ${ident x}.$acc)} } }
  }.

notation < "hvbox(ν ident i \nbsp 'of' \nbsp t \nbsp 'in' \nbsp break p)"
 with precedence 48 for
  @{'new $t (λ${ident i} : $ty. $p) }.

interpretation "unit it" 'it = it.

notation < "hvbox(ν ident i \nbsp 'in' \nbsp break p)"
 with precedence 48 for
    @{'new 'it (λ${ident i} : $ty. $p) }.
    
let rec bnews B T E (tys : list T) (f : list B → bind_list B T E) on tys : bind_list B T E ≝
  match tys with
  [ nil ⇒ f [ ]
  | cons ty tys ⇒ νx of ty in bnews … tys (λl. f (x :: l))
  ].
  
let rec bnews_strong B T E (tys : list T) (f : ∀l : list B.|l| = |tys| → bind_list B T E) on tys : bind_list B T E ≝
  match tys return λx.x = tys → bind_list B T E with
  [ nil ⇒ λprf.f [ ] ?
  | cons ty tys' ⇒ λprf.νx of ty in bnews_strong … tys' (λl',prf'. f (x :: l') ?)
  ] (refl …). destruct normalize // qed.
  
let rec bnews_n B E n (f : list B → bind_list B unit E) on n : bind_list B unit E ≝
  match n with
  [ O ⇒ f [ ]
  | S n ⇒ νx in bnews_n … n (λl. f (x :: l))
  ].
  
let rec bnews_n_strong B E n (f : ∀l:list B.|l| = n → bind_list B unit E) on n : bind_list B unit E ≝
  match n return λx.x = n → bind_list B unit E with
  [ O ⇒ λprf.f [ ] ?
  | S n' ⇒ λprf.νx in bnews_n_strong … n' (λl',prf'. f (x :: l') ?)
  ] (refl …). normalize // qed.
  
interpretation "iterated typed new" 'tnews ts f = (bnews ??? ts f).
interpretation "iterated untyped new" 'unews n f = (bnews_n ?? n f).
interpretation "iterated typed new strong" 'stnews ts f = (bnews_strong ??? ts f).
interpretation "iterated untyped new strong" 'sunews n f = (bnews_n_strong ?? n f).

notation > "νν ident l 'of' ts opt('with' ident EQ) 'in' f" with precedence 47 for
 ${default
   @{ 'stnews $ts (λ${ident l}.λ${ident EQ}.$f) }
   @{ 'tnews $ts (λ${ident l}.$f)}
 }.
 
notation > "νν ident l : ty 'of' ts opt('with' ident EQ) 'in' f" with precedence 47 for
 ${default
   @{ 'stnews $ts (λ${ident l}:$ty.λ${ident EQ}.$f) }
   @{ 'tnews $ts (λ${ident l}:$ty.$f)}
 }.
 
notation < "hvbox(νν ident l : ty\nbsp 'of' \nbsp ts \nbsp 'with' \nbsp ident EQ : tyeq \nbsp 'in' \nbsp break f)" with precedence 47 for
   @{ 'stnews $ts (λ${ident l} : $ty.λ${ident EQ} : $tyeq.$f) }.
notation < "hvbox(νν ident l : ty\nbsp 'of' \nbsp ts \nbsp 'in'  break f)" with precedence 47 for
   @{ 'tnews $ts (λ${ident l} : $ty.$f) }.

notation > "νν ident l ^ n opt('with' ident EQ) 'in' f" with precedence 47 for
 ${default
   @{ 'sunews $n (λ${ident l}.λ${ident EQ}.$f) }
   @{ 'unews $n (λ${ident l}.$f)}
 }.
 
notation > "νν ident l : ty ^ n opt('with' ident EQ) 'in' f" with precedence 47 for
 ${default
   @{ 'sunews $n (λ${ident l}:$ty.λ${ident EQ}.$f) }
   @{ 'unews $n (λ${ident l}:$ty.$f)}
 }.
 
notation < "hvbox(νν \nbsp ident l : ty ^ n \nbsp 'with' \nbsp ident EQ : tyeq \nbsp 'in' \nbsp break f)" with precedence 47 for
   @{ 'sunews $n (λ${ident l} : $ty.λ${ident EQ} : $tyeq.$f) }.
notation < "hvbox(νν_ n \nbsp ident l : ty ^ n \nbsp 'in' \nbsp break f)" with precedence 47 for
   @{ 'unews $n (λ${ident l} : $ty.$f) }.


axiom bnew_proper : ∀B,T,E. bnew B T E ⊨ eq ? ++> (eq ? ++> eq ?) ++> eq ?.
(* the following is equivalent to the above *)
theorem bnew_proper' : ∀X,Y,Z.Y (* non-empty *) →
  ∀f,g : X → bind_list X Y Z.  (∀x. f x = g x) → f = g.
#X#Y#Z#y#f#g#eqf
cut ('new y f = 'new y g) /2 by bnew_proper/
#eq destruct //
qed.

definition blist_of_list : ∀B,T,E. list E →
  bind_list B T E ≝
  λB,T,E,l.
  let f ≝ λe.λbl. e :: bl in
  foldr … f [] l.
  
  
coercion blist_from_list :
  ∀B,T,E. ∀l:list E. bind_list B T E ≝ blist_of_list on _l : list ? to bind_list ???.

let rec bappend A B C (l1 : bind_list A B C) l2 on l1 : bind_list A B C ≝
match l1 with
[ bnil ⇒ l2
| bcons x l1' ⇒ x :: (bappend … l1' l2)
| bnew t l1' ⇒ νx of t in bappend … (l1' x) l2
].

interpretation "append blist" 'append l1 l2 = (bappend ??? l1 l2).

let rec bbind A B C D (l : bind_list A B C) (f : C → bind_list A B D) on l
  : bind_list A B D ≝
  match l with
  [ bnil ⇒ bnil …
  | bcons x l1' ⇒ bappend … (f x) (bbind … l1' f)
  | bnew t l1' ⇒ bnew … t (λx. bbind … (l1' x) f)
  ].
  
interpretation "bind_list bind" 'm_bind m f = (bbind ? ? ? ? m f).

include "utilities/proper.ma".

lemma bappend_assoc : ∀A,B,C.∀l1,l2,l3:bind_list A B C.
  ((l1@l2)@l3) = (l1 @ l2 @ l3).
#A#B#C#l1 elim l1 normalize
[
(* case bnil *)
  #l2#l3 //
| #x#l'#Hi#l2#l3 >Hi //
| #t#l'#Hi#l2#l3 @bnew_proper //
qed.

lemma bbind_bappend : ∀A,B,C,D.∀l1,l2:bind_list A B C.∀f:C→bind_list A B D.
  ((l1 @ l2) »= f) = ((l1 »= f) @ (l2 »= f)).
#A#B#C#D#l1 elim l1 normalize /2 by bnew_proper/ qed.

lemma bappend_bnil : ∀A,B,C.∀l : bind_list A B C.( l@[ ]) = l.
#A#B#C#l elim l normalize /2 by bnew_proper/ qed.
  
definition BindList ≝
  λB,T.MakeMonadProps
  (* the monad *)
  (λX.bind_list B T X)
  (* return *)
  (λE,x.[x])
  (* bind *)
  (bbind B T)
  ???.
[(* ret_bind *)
  #X#Y#x#f normalize @bappend_bnil
|(* bind_ret *)
 #X#m elim m normalize /2 by /
 #t #l' #Hi @bnew_proper // normalize #s#t#eq destruct @Hi
|(* bind_bind *)
 #X#Y#Z#m#f#g elim m normalize
 [//
 |(* case bcons *)
  #x #l1' #Hi <Hi @bbind_bappend
 |(* case bnew *)
  #t #l #Hi @bnew_proper //
  #x#y #x_eq_y destruct(x_eq_y) @Hi
 ]
]
qed.

unification hint 0 ≔ B, T, X;
  N ≟ BindList B T, M ≟ max_def N, O ≟ m_def M
(*--------------------------------------------*) ⊢
  bind_list B T X ≡ monad O X.

include "utilities/state.ma".

let rec bcompile R T E U
  (fresh : T → state_monad U R)
  (blist : bind_list R T E) on blist : state_monad U (list E) ≝
  match blist with
  [ bnil ⇒ return [ ]
  | bcons x l ⇒
    ! res ← bcompile … fresh l ;
    return (x :: res)
  | bnew t f ⇒
    ! r ← fresh t ;
    bcompile … fresh (f r)
  ].
  
theorem bcompile_append :
  ∀E, R, T, U, fresh, bl1, bl2.
  (bcompile E R T U fresh (bl1 @ bl2)) ≅
  (
  ! l1 ← bcompile … fresh bl1 ;
  ! l2 ← bcompile … fresh bl2 ;
  return (l1 @ l2)
  ).
  #E#R#T#U#fresh#bl1#bl2
  elim bl1 normalize
   [
     #u @pair_elim //
   |
    #x#bl1' #Hi #u0 >Hi -Hi
    elim (bcompile E R T U fresh bl1' u0) #u1 #l1
    normalize
    elim (bcompile E R T U fresh bl2 u1) #u2 #l2
    normalize //
   |
    #t #blf #Hi #u0
    @pair_elim normalize #u #r
    >(Hi r) -Hi //
qed.