source: extracted/bind_new.ml @ 2717

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

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

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_17542 -> h_bret x_17542
38| Bnew x_17544 ->
39  h_bnew x_17544 (fun x_17543 ->
40    bind_new_rect_Type4 h_bret h_bnew (x_17544 x_17543))
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_17554 -> h_bret x_17554
47| Bnew x_17556 ->
48  h_bnew x_17556 (fun x_17555 ->
49    bind_new_rect_Type3 h_bret h_bnew (x_17556 x_17555))
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_17560 -> h_bret x_17560
56| Bnew x_17562 ->
57  h_bnew x_17562 (fun x_17561 ->
58    bind_new_rect_Type2 h_bret h_bnew (x_17562 x_17561))
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_17566 -> h_bret x_17566
65| Bnew x_17568 ->
66  h_bnew x_17568 (fun x_17567 ->
67    bind_new_rect_Type1 h_bret h_bnew (x_17568 x_17567))
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_17572 -> h_bret x_17572
74| Bnew x_17574 ->
75  h_bnew x_17574 (fun x_17573 ->
76    bind_new_rect_Type0 h_bret h_bnew (x_17574 x_17573))
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.