source: extracted/bind_new.ml @ 2746

Last change on this file since 2746 was 2743, checked in by sacerdot, 7 years ago

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

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_20622 -> h_bret x_20622
38| Bnew x_20624 ->
39  h_bnew x_20624 (fun x_20623 ->
40    bind_new_rect_Type4 h_bret h_bnew (x_20624 x_20623))
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_20634 -> h_bret x_20634
47| Bnew x_20636 ->
48  h_bnew x_20636 (fun x_20635 ->
49    bind_new_rect_Type3 h_bret h_bnew (x_20636 x_20635))
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_20640 -> h_bret x_20640
56| Bnew x_20642 ->
57  h_bnew x_20642 (fun x_20641 ->
58    bind_new_rect_Type2 h_bret h_bnew (x_20642 x_20641))
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_20646 -> h_bret x_20646
65| Bnew x_20648 ->
66  h_bnew x_20648 (fun x_20647 ->
67    bind_new_rect_Type1 h_bret h_bnew (x_20648 x_20647))
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_20652 -> h_bret x_20652
74| Bnew x_20654 ->
75  h_bnew x_20654 (fun x_20653 ->
76    bind_new_rect_Type0 h_bret h_bnew (x_20654 x_20653))
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.