source: extracted/bind_new.ml @ 3009

Last change on this file since 3009 was 2951, checked in by sacerdot, 7 years ago

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

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_18232 -> h_bret x_18232
38| Bnew x_18234 ->
39  h_bnew x_18234 (fun x_18233 ->
40    bind_new_rect_Type4 h_bret h_bnew (x_18234 x_18233))
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_18244 -> h_bret x_18244
47| Bnew x_18246 ->
48  h_bnew x_18246 (fun x_18245 ->
49    bind_new_rect_Type3 h_bret h_bnew (x_18246 x_18245))
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_18250 -> h_bret x_18250
56| Bnew x_18252 ->
57  h_bnew x_18252 (fun x_18251 ->
58    bind_new_rect_Type2 h_bret h_bnew (x_18252 x_18251))
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_18256 -> h_bret x_18256
65| Bnew x_18258 ->
66  h_bnew x_18258 (fun x_18257 ->
67    bind_new_rect_Type1 h_bret h_bnew (x_18258 x_18257))
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_18262 -> h_bret x_18262
74| Bnew x_18264 ->
75  h_bnew x_18264 (fun x_18263 ->
76    bind_new_rect_Type0 h_bret h_bnew (x_18264 x_18263))
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.