open Preamble

open Jmeq

open Russell

open Bool

open Nat

open List

open Setoids

open Relations

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Monad

type ('b, 'e) bind_new =
| Bret of 'e
| Bnew of ('b -> ('b, 'e) bind_new)

(** val bind_new_rect_Type4 :
    ('a2 -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new) -> ('a1 -> 'a3) -> 'a3) ->
    ('a1, 'a2) bind_new -> 'a3 **)
let rec bind_new_rect_Type4 h_bret h_bnew = function
| Bret x_18204 -> h_bret x_18204
| Bnew x_18206 ->
  h_bnew x_18206 (fun x_18205 ->
    bind_new_rect_Type4 h_bret h_bnew (x_18206 x_18205))

(** val bind_new_rect_Type3 :
    ('a2 -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new) -> ('a1 -> 'a3) -> 'a3) ->
    ('a1, 'a2) bind_new -> 'a3 **)
let rec bind_new_rect_Type3 h_bret h_bnew = function
| Bret x_18216 -> h_bret x_18216
| Bnew x_18218 ->
  h_bnew x_18218 (fun x_18217 ->
    bind_new_rect_Type3 h_bret h_bnew (x_18218 x_18217))

(** val bind_new_rect_Type2 :
    ('a2 -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new) -> ('a1 -> 'a3) -> 'a3) ->
    ('a1, 'a2) bind_new -> 'a3 **)
let rec bind_new_rect_Type2 h_bret h_bnew = function
| Bret x_18222 -> h_bret x_18222
| Bnew x_18224 ->
  h_bnew x_18224 (fun x_18223 ->
    bind_new_rect_Type2 h_bret h_bnew (x_18224 x_18223))

(** val bind_new_rect_Type1 :
    ('a2 -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new) -> ('a1 -> 'a3) -> 'a3) ->
    ('a1, 'a2) bind_new -> 'a3 **)
let rec bind_new_rect_Type1 h_bret h_bnew = function
| Bret x_18228 -> h_bret x_18228
| Bnew x_18230 ->
  h_bnew x_18230 (fun x_18229 ->
    bind_new_rect_Type1 h_bret h_bnew (x_18230 x_18229))

(** val bind_new_rect_Type0 :
    ('a2 -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new) -> ('a1 -> 'a3) -> 'a3) ->
    ('a1, 'a2) bind_new -> 'a3 **)
let rec bind_new_rect_Type0 h_bret h_bnew = function
| Bret x_18234 -> h_bret x_18234
| Bnew x_18236 ->
  h_bnew x_18236 (fun x_18235 ->
    bind_new_rect_Type0 h_bret h_bnew (x_18236 x_18235))

(** val bind_new_inv_rect_Type4 :
    ('a1, 'a2) bind_new -> ('a2 -> __ -> 'a3) -> (('a1 -> ('a1, 'a2)
    bind_new) -> ('a1 -> __ -> 'a3) -> __ -> 'a3) -> 'a3 **)
let bind_new_inv_rect_Type4 hterm h1 h2 =
  let hcut = bind_new_rect_Type4 h1 h2 hterm in hcut __

(** val bind_new_inv_rect_Type3 :
    ('a1, 'a2) bind_new -> ('a2 -> __ -> 'a3) -> (('a1 -> ('a1, 'a2)
    bind_new) -> ('a1 -> __ -> 'a3) -> __ -> 'a3) -> 'a3 **)
let bind_new_inv_rect_Type3 hterm h1 h2 =
  let hcut = bind_new_rect_Type3 h1 h2 hterm in hcut __

(** val bind_new_inv_rect_Type2 :
    ('a1, 'a2) bind_new -> ('a2 -> __ -> 'a3) -> (('a1 -> ('a1, 'a2)
    bind_new) -> ('a1 -> __ -> 'a3) -> __ -> 'a3) -> 'a3 **)
let bind_new_inv_rect_Type2 hterm h1 h2 =
  let hcut = bind_new_rect_Type2 h1 h2 hterm in hcut __

(** val bind_new_inv_rect_Type1 :
    ('a1, 'a2) bind_new -> ('a2 -> __ -> 'a3) -> (('a1 -> ('a1, 'a2)
    bind_new) -> ('a1 -> __ -> 'a3) -> __ -> 'a3) -> 'a3 **)
let bind_new_inv_rect_Type1 hterm h1 h2 =
  let hcut = bind_new_rect_Type1 h1 h2 hterm in hcut __

(** val bind_new_inv_rect_Type0 :
    ('a1, 'a2) bind_new -> ('a2 -> __ -> 'a3) -> (('a1 -> ('a1, 'a2)
    bind_new) -> ('a1 -> __ -> 'a3) -> __ -> 'a3) -> 'a3 **)
let bind_new_inv_rect_Type0 hterm h1 h2 =
  let hcut = bind_new_rect_Type0 h1 h2 hterm in hcut __

(** val bind_new_discr : ('a1, 'a2) bind_new -> ('a1, 'a2) bind_new -> __ **)
let bind_new_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Bret a0 -> Obj.magic (fun _ dH -> dH __)
     | Bnew a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val bind_new_jmdiscr :
    ('a1, 'a2) bind_new -> ('a1, 'a2) bind_new -> __ **)
let bind_new_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Bret a0 -> Obj.magic (fun _ dH -> dH __)
     | Bnew a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val bnews :
    Nat.nat -> ('a1 List.list -> ('a1, 'a2) bind_new) -> ('a1, 'a2) bind_new **)
let rec bnews n f =
  match n with
  | Nat.O -> f List.Nil
  | Nat.S x -> Bnew (fun y -> bnews x (fun l -> f (List.Cons (y, l))))

(** val bnews_strong :
    Nat.nat -> ('a1 List.list -> __ -> ('a1, 'a2) bind_new) -> ('a1, 'a2)
    bind_new **)
let rec bnews_strong n f =
  (match n with
   | Nat.O -> (fun _ -> f List.Nil __)
   | Nat.S n' ->
     (fun _ -> Bnew (fun x ->
       bnews_strong n' (fun l' _ -> f (List.Cons (x, l')) __)))) __

(** val bbind :
    ('a1, 'a2) bind_new -> ('a2 -> ('a1, 'a3) bind_new) -> ('a1, 'a3)
    bind_new **)
let rec bbind l f =
  match l with
  | Bret x -> f x
  | Bnew n -> Bnew (fun x -> bbind (n x) f)

(** val bindNew : Monad.monadProps **)
let bindNew =
  Monad.makeMonadProps (fun _ x -> Bret x) (fun _ _ -> bbind)

open State

(** val bcompile :
    'a2 Monad.smax_def__o__monad -> ('a2, 'a3) bind_new -> 'a3
    Monad.smax_def__o__monad **)
let rec bcompile fresh = function
| Bret x -> Monad.m_return0 (Monad.smax_def State.state_monad) x
| Bnew f ->
  Monad.m_bind0 (Monad.smax_def State.state_monad) fresh (fun r ->
    bcompile fresh (f r))