source: driver/extracted/bind_new.ml @ 3106

Last change on this file since 3106 was 3059, checked in by sacerdot, 7 years ago

New extraction

File size: 4.8 KB
Line 
1open Preamble
2
3open Jmeq
4
5open Russell
6
7open Bool
8
9open Nat
10
11open List
12
13open Setoids
14
15open Relations
16
17open Hints_declaration
18
19open Core_notation
20
21open Pts
22
23open Logic
24
25open Types
26
27open Monad
28
29type ('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 **)
36let 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 **)
45let 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 **)
54let 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 **)
63let 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 **)
72let 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 **)
81let 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 **)
87let 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 **)
93let 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 **)
99let 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 **)
105let 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 -> __ **)
109let 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 -> __ **)
117let 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 **)
125let 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 **)
133let 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 **)
143let 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 **)
149let bindNew =
150  Monad.makeMonadProps (fun _ x -> Bret x) (fun _ _ -> bbind)
151
152open State
153
154(** val bcompile :
155    'a2 Monad.smax_def__o__monad -> ('a2, 'a3) bind_new -> 'a3
156    Monad.smax_def__o__monad **)
157let 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
Note: See TracBrowser for help on using the repository browser.