include "utilities/monad.ma".

inductive bind_new
  (B : Type[0])
  (E : Type[0])
  : Type[0] ≝
  | bret : E → bind_new B E
  | bnew : (B → bind_new B E) → bind_new B E.
  
interpretation "new bind_new" 'new f = (bnew ?? f).

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

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

let rec bnews B E n (f : list B → bind_new B E) on n : bind_new B E ≝
  match n with
  [ O ⇒ f [ ]
  | S x ⇒ νy in bnews … x (λl. f (y :: l))
  ].
  
let rec bnews_strong B E n (f : ∀l:list B.|l| = n → bind_new B E) on n
  : bind_new B E ≝
  match n return λx.x = n → bind_new B E with
  [ O ⇒ λprf.f [ ] ?
  | S n' ⇒ λprf.νx in bnews_strong … n' (λl',prf'. f (x :: l') ?)
  ] (refl …). normalize // qed.
  
interpretation "iterated new" 'unews n f = (bnews ?? n f).
interpretation "iterated new strong" 'sunews n f = (bnews_strong ?? n f).

notation > "νν n 'as' ident l opt('with' ident EQ) 'in' f" with precedence 47 for
 ${default
   @{ 'sunews $n (λ${ident l}.λ${ident EQ}.$f) }
   @{ 'unews $n (λ${ident l}.$f)}
 }.
 
notation > "νν n 'as' ident l : ty 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(νν n \nbsp 'as' ident l \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 'as' ident l \nbsp 'in' \nbsp break f)" with precedence 47 for
   @{ 'unews $n (λ${ident l} : $ty.$f) }.


axiom bnew_proper : ∀B,E,f,g. (∀x. f x = g x) → bnew B E f = bnew B E g.

let rec bbind A B C (l : bind_new A B) (f : B → bind_new A C) on l
  : bind_new A C ≝
  match l with
  [ bret x ⇒ f x
  | bnew n ⇒ bnew … (λx. bbind … (n x) f)
  ].
  
definition BindNew ≝
  λB.MakeMonadProps
  (* the monad *)
  (bind_new B)
  (* return *)
  (λX,x.bret … x)
  (* bind *)
  (bbind B)
  ????.
[ (* ret_bind *)
  //
|(* bind_ret *)
 #X#m elim m normalize [//]
 #l' #Hi @bnew_proper //
|(* bind_bind *)
 #X#Y#Z#m#f#g elim m normalize
 [//
 |(* case bnew *)
  #l #Hi @bnew_proper //
 ]
| #X#Y #m #f #g #H elim m normalize [ /2/ ] #k #IH @bnew_proper #x
  >IH %
]
qed.

unification hint 0 ≔ B, X;
  N ≟ BindNew B, M ≟ max_def N
(*--------------------------------------------*) ⊢
  bind_new B X ≡ monad M X.

include "utilities/state.ma".

let rec bcompile U R E
  (fresh : state_monad U R)
  (b : bind_new R E) on b : state_monad U E ≝
  match b with
  [ bret x ⇒ return x
  | bnew f ⇒
    ! r ← fresh ;
    bcompile … fresh (f r)
  ].
  
theorem bcompile_bbind :
  ∀U,R,E,F.∀fresh : state_monad U R.∀ b : bind_new R E.∀f : E → bind_new R F.
    bcompile … fresh (! x ← b ;
                    f x) ≅ 
    ! x ← bcompile … fresh b ;
    bcompile … fresh (f x).
  #U#R#E#F#fresh#b#f
  elim b normalize
   [ //
   |
     #bf #Hi #u0
    @pair_elim normalize #u #r
    >(Hi r) -Hi //
   ]
qed.