extracted/bind_new.ml

   1 open Preamble
   2
   3 open Jmeq
   4
   5 open Russell
   6
   7 open Bool
   8
   9 open Nat
  10
  11 open List
  12
  13 open Setoids
  14
  15 open Relations
  16
  17 open Hints_declaration
  18
  19 open Core_notation
  20
  21 open Pts
  22
  23 open Logic
  24
  25 open Types
  26
  27 open Monad
  28
  29 type ('b, 'e) bind_new =
  30 | Bret of 'e
  31 | Bnew of ('b -> ('b, 'e) bind_new)
  32
  33 (** val bind_new_rect_Type4 :
  34     ('a2 -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new) -> ('a1 -> 'a3) -> 'a3) ->
  35     ('a1, 'a2) bind_new -> 'a3 **)
  36 let rec bind_new_rect_Type4 h_bret h_bnew = function
  37 | Bret x_18204 -> h_bret x_18204
  38 | Bnew x_18206 ->
  39   h_bnew x_18206 (fun x_18205 ->
  40     bind_new_rect_Type4 h_bret h_bnew (x_18206 x_18205))
  41
  42 (** val bind_new_rect_Type3 :
  43     ('a2 -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new) -> ('a1 -> 'a3) -> 'a3) ->
  44     ('a1, 'a2) bind_new -> 'a3 **)
  45 let rec bind_new_rect_Type3 h_bret h_bnew = function
  46 | Bret x_18216 -> h_bret x_18216
  47 | Bnew x_18218 ->
  48   h_bnew x_18218 (fun x_18217 ->
  49     bind_new_rect_Type3 h_bret h_bnew (x_18218 x_18217))
  50
  51 (** val bind_new_rect_Type2 :
  52     ('a2 -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new) -> ('a1 -> 'a3) -> 'a3) ->
  53     ('a1, 'a2) bind_new -> 'a3 **)
  54 let rec bind_new_rect_Type2 h_bret h_bnew = function
  55 | Bret x_18222 -> h_bret x_18222
  56 | Bnew x_18224 ->
  57   h_bnew x_18224 (fun x_18223 ->
  58     bind_new_rect_Type2 h_bret h_bnew (x_18224 x_18223))
  59
  60 (** val bind_new_rect_Type1 :
  61     ('a2 -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new) -> ('a1 -> 'a3) -> 'a3) ->
  62     ('a1, 'a2) bind_new -> 'a3 **)
  63 let rec bind_new_rect_Type1 h_bret h_bnew = function
  64 | Bret x_18228 -> h_bret x_18228
  65 | Bnew x_18230 ->
  66   h_bnew x_18230 (fun x_18229 ->
  67     bind_new_rect_Type1 h_bret h_bnew (x_18230 x_18229))
  68
  69 (** val bind_new_rect_Type0 :
  70     ('a2 -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new) -> ('a1 -> 'a3) -> 'a3) ->
  71     ('a1, 'a2) bind_new -> 'a3 **)
  72 let rec bind_new_rect_Type0 h_bret h_bnew = function
  73 | Bret x_18234 -> h_bret x_18234
  74 | Bnew x_18236 ->
  75   h_bnew x_18236 (fun x_18235 ->
  76     bind_new_rect_Type0 h_bret h_bnew (x_18236 x_18235))
  77
  78 (** val bind_new_inv_rect_Type4 :
  79     ('a1, 'a2) bind_new -> ('a2 -> __ -> 'a3) -> (('a1 -> ('a1, 'a2)
  80     bind_new) -> ('a1 -> __ -> 'a3) -> __ -> 'a3) -> 'a3 **)
  81 let bind_new_inv_rect_Type4 hterm h1 h2 =
  82   let hcut = bind_new_rect_Type4 h1 h2 hterm in hcut __
  83
  84 (** val bind_new_inv_rect_Type3 :
  85     ('a1, 'a2) bind_new -> ('a2 -> __ -> 'a3) -> (('a1 -> ('a1, 'a2)
  86     bind_new) -> ('a1 -> __ -> 'a3) -> __ -> 'a3) -> 'a3 **)
  87 let bind_new_inv_rect_Type3 hterm h1 h2 =
  88   let hcut = bind_new_rect_Type3 h1 h2 hterm in hcut __
  89
  90 (** val bind_new_inv_rect_Type2 :
  91     ('a1, 'a2) bind_new -> ('a2 -> __ -> 'a3) -> (('a1 -> ('a1, 'a2)
  92     bind_new) -> ('a1 -> __ -> 'a3) -> __ -> 'a3) -> 'a3 **)
  93 let bind_new_inv_rect_Type2 hterm h1 h2 =
  94   let hcut = bind_new_rect_Type2 h1 h2 hterm in hcut __
  95
  96 (** val bind_new_inv_rect_Type1 :
  97     ('a1, 'a2) bind_new -> ('a2 -> __ -> 'a3) -> (('a1 -> ('a1, 'a2)
  98     bind_new) -> ('a1 -> __ -> 'a3) -> __ -> 'a3) -> 'a3 **)
  99 let bind_new_inv_rect_Type1 hterm h1 h2 =
 100   let hcut = bind_new_rect_Type1 h1 h2 hterm in hcut __
 101
 102 (** val bind_new_inv_rect_Type0 :
 103     ('a1, 'a2) bind_new -> ('a2 -> __ -> 'a3) -> (('a1 -> ('a1, 'a2)
 104     bind_new) -> ('a1 -> __ -> 'a3) -> __ -> 'a3) -> 'a3 **)
 105 let bind_new_inv_rect_Type0 hterm h1 h2 =
 106   let hcut = bind_new_rect_Type0 h1 h2 hterm in hcut __
 107
 108 (** val bind_new_discr : ('a1, 'a2) bind_new -> ('a1, 'a2) bind_new -> __ **)
 109 let bind_new_discr x y =
 110   Logic.eq_rect_Type2 x
 111     (match x with
 112      | Bret a0 -> Obj.magic (fun _ dH -> dH __)
 113      | Bnew a0 -> Obj.magic (fun _ dH -> dH __)) y
 114
 115 (** val bind_new_jmdiscr :
 116     ('a1, 'a2) bind_new -> ('a1, 'a2) bind_new -> __ **)
 117 let bind_new_jmdiscr x y =
 118   Logic.eq_rect_Type2 x
 119     (match x with
 120      | Bret a0 -> Obj.magic (fun _ dH -> dH __)
 121      | Bnew a0 -> Obj.magic (fun _ dH -> dH __)) y
 122
 123 (** val bnews :
 124     Nat.nat -> ('a1 List.list -> ('a1, 'a2) bind_new) -> ('a1, 'a2) bind_new **)
 125 let rec bnews n f =
 126   match n with
 127   | Nat.O -> f List.Nil
 128   | Nat.S x -> Bnew (fun y -> bnews x (fun l -> f (List.Cons (y, l))))
 129
 130 (** val bnews_strong :
 131     Nat.nat -> ('a1 List.list -> __ -> ('a1, 'a2) bind_new) -> ('a1, 'a2)
 132     bind_new **)
 133 let rec bnews_strong n f =
 134   (match n with
 135    | Nat.O -> (fun _ -> f List.Nil __)
 136    | Nat.S n' ->
 137      (fun _ -> Bnew (fun x ->
 138        bnews_strong n' (fun l' _ -> f (List.Cons (x, l')) __)))) __
 139
 140 (** val bbind :
 141     ('a1, 'a2) bind_new -> ('a2 -> ('a1, 'a3) bind_new) -> ('a1, 'a3)
 142     bind_new **)
 143 let rec bbind l f =
 144   match l with
 145   | Bret x -> f x
 146   | Bnew n -> Bnew (fun x -> bbind (n x) f)
 147
 148 (** val bindNew : Monad.monadProps **)
 149 let bindNew =
 150   Monad.makeMonadProps (fun _ x -> Bret x) (fun _ _ -> bbind)
 151
 152 open State
 153
 154 (** val bcompile :
 155     'a2 Monad.smax_def__o__monad -> ('a2, 'a3) bind_new -> 'a3
 156     Monad.smax_def__o__monad **)
 157 let rec bcompile fresh = function
 158 | Bret x -> Monad.m_return0 (Monad.smax_def State.state_monad) x
 159 | Bnew f ->
 160   Monad.m_bind0 (Monad.smax_def State.state_monad) fresh (fun r ->
 161     bcompile fresh (f r))
 162