infinite-pigeonhole/IPP_Escardo_program.ml at main · herbelin/infinite-pigeonhole · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302

type empty_set = |

type nat =
| O
| S of nat


type ('a, 'p) sigT =
| ExistT of 'a * 'p

(** val projT1 : ('a1, 'a2) sigT -> 'a1 **)

let projT1 = function
| ExistT (a, _) -> a

open Delimcc
let p = (new_prompt () : _ prompt)

type 'a cont = 'a -> empty_set

(** val callcc : ('a1 cont -> 'a1) -> 'a1 **)

let callcc = fun c -> shift p (fun k -> k (c (fun x -> abort p (k x))))

(** val throw : 'a1 cont -> 'a1 -> 'a2 **)

let throw = fun (k : 'a cont) x -> match k x with _ -> .

type 'a stream = 'a __stream Lazy.t
and 'a __stream =
| Build_stream of 'a * 'a stream

(** val head : 'a1 stream -> 'a1 **)

let head s =
  let Build_stream (head0, _) = Lazy.force s in head0

(** val tail : 'a1 stream -> 'a1 stream **)

let tail s =
  let Build_stream (_, tail0) = Lazy.force s in tail0

type ipp_stream = __ipp_stream Lazy.t
and __ipp_stream =
| Build_ipp_stream of nat * (unit -> ipp_stream)

(** val depth : ipp_stream -> nat **)

let depth i =
  let Build_ipp_stream (depth0, _) = Lazy.force i in depth0

(** val rest : ipp_stream -> unit -> ipp_stream **)

let rest i =
  let Build_ipp_stream (_, rest0) = Lazy.force i in rest0

(** val coiter : ('a1 -> nat) -> ('a1 -> 'a1) -> 'a1 -> ipp_stream **)

let rec coiter base next s =
  lazy (Build_ipp_stream ((base s), (fun _ -> coiter base next (next s))))

(** val bool_dec : bool -> bool -> bool **)

let bool_dec b b' =
  if b then b' else if b' then false else true

(** val infinite_bool : bool stream -> ipp_stream **)

let infinite_bool bs =
  let b0 = head bs in
  callcc (fun start ->
    coiter (fun pat -> let ExistT (depth0, _) = pat in depth0) (fun pat ->
      let ExistT (depth0, rest0) = pat in
      if bool_dec (head rest0) b0
      then ExistT ((S depth0), (tail rest0))
      else callcc (fun restart ->
             throw start
               (coiter projT1 (fun pat0 ->
                 let ExistT (depth1, rest1) = pat0 in
                 if bool_dec (head rest1) b0
                 then throw restart (ExistT ((S depth1), (tail rest1)))
                 else ExistT ((S depth1), (tail rest1))) (ExistT ((S depth0),
                 (tail rest0)))))) (ExistT (O, (tail bs))))

(** val take_ipp : ipp_stream -> nat -> nat list **)

let rec take_ipp s = function
| O -> []
| S n' ->
  (match n' with
   | O -> (depth s) :: []
   | S _ -> (depth s) :: (take_ipp (rest s ()) n'))

(** val always_true : bool stream **)

let rec always_true =
  lazy (Build_stream (true, always_true))

(** val always_false : bool stream **)

let rec always_false =
  lazy (Build_stream (false, always_false))

(** val test_stream : bool stream **)

let test_stream =
  lazy (Build_stream (true, (lazy (Build_stream (false,
    (lazy (Build_stream (true, (lazy (Build_stream (false,
    (lazy (Build_stream (true, (lazy (Build_stream (true,
    (lazy (Build_stream (false, (lazy (Build_stream (false,
    (lazy (Build_stream (true, (lazy (Build_stream (true,
    always_false)))))))))))))))))))))))))))))

(** val test1 : nat list **)

let test1 =
  push_prompt p (fun _ -> take_ipp (infinite_bool test_stream) (S O))

(** val test2 : nat list **)

let test2 =
  push_prompt p (fun _ -> take_ipp (infinite_bool test_stream) (S (S O)))

(** val test3 : nat list **)

let test3 =
  push_prompt p (fun _ -> take_ipp (infinite_bool test_stream) (S (S (S O))))

(** val test4 : nat list **)

let test4 =
  push_prompt p (fun _ ->
    take_ipp (infinite_bool test_stream) (S (S (S (S O)))))

(** val test5 : nat list **)

let test5 =
  push_prompt p (fun _ ->
    take_ipp (infinite_bool test_stream) (S (S (S (S (S O))))))

(** val test6 : nat list **)

let test6 =
  push_prompt p (fun _ ->
    take_ipp (infinite_bool test_stream) (S (S (S (S (S (S O)))))))

(** val test7 : nat list **)

let test7 =
  push_prompt p (fun _ ->
    take_ipp (infinite_bool test_stream) (S (S (S (S (S (S (S O))))))))

(** val prova1 : bool stream **)

let rec prova1 =
  lazy (Build_stream (true, (lazy (Build_stream (true,
    (lazy (Build_stream (false, (lazy (Build_stream (false, prova1)))))))))))

(** val prova2 : bool stream **)

let rec prova2 =
  lazy (Build_stream (true, (lazy (Build_stream (true,
    (lazy (Build_stream (false, (lazy (Build_stream (false,
    (lazy (Build_stream (false, prova2))))))))))))))

(** val prova3 : bool stream **)

let prova3 =
  lazy (Build_stream (true, (lazy (Build_stream (true,
    (lazy (Build_stream (false, (lazy (Build_stream (false,
    always_false)))))))))))

(** val prova4 : bool stream **)

let prova4 =
  lazy (Build_stream (true, (lazy (Build_stream (true,
    (lazy (Build_stream (false, (lazy (Build_stream (false,
    always_true)))))))))))

(** val testprova1 : nat list **)

let testprova1 =
  push_prompt p (fun _ -> take_ipp (infinite_bool prova1) (S (S O)))

(** val testprova2 : nat list **)

let testprova2 =
  push_prompt p (fun _ -> take_ipp (infinite_bool prova2) (S (S O)))

(** val testprova3 : nat list **)

let testprova3 =
  push_prompt p (fun _ -> take_ipp (infinite_bool prova3) (S (S O)))

(** val testprova4 : nat list **)

let testprova4 =
  push_prompt p (fun _ -> take_ipp (infinite_bool prova4) (S (S O)))

(** val example_ET : bool stream **)

let rec example_ET =
  lazy (Build_stream (true, (lazy (Build_stream (false,
    (lazy (Build_stream (true, (lazy (Build_stream (false,
    example_ET)))))))))))

(** val example_EF : bool stream **)

let rec example_EF =
  lazy (Build_stream (false, (lazy (Build_stream (true,
    (lazy (Build_stream (false, (lazy (Build_stream (true,
    example_EF)))))))))))

(** val example_ET1 : bool stream **)

let example_ET1 =
  lazy (Build_stream (true, (lazy (Build_stream (false,
    (lazy (Build_stream (true, (lazy (Build_stream (false,
    always_true)))))))))))

(** val example_EF1 : bool stream **)

let example_EF1 =
  lazy (Build_stream (false, (lazy (Build_stream (true,
    (lazy (Build_stream (false, (lazy (Build_stream (true,
    always_false)))))))))))

(** val example_ET2 : bool stream **)

let example_ET2 =
  lazy (Build_stream (true, (lazy (Build_stream (false,
    (lazy (Build_stream (true, (lazy (Build_stream (false,
    always_false)))))))))))

(** val example_EF2 : bool stream **)

let example_EF2 =
  lazy (Build_stream (false, (lazy (Build_stream (true,
    (lazy (Build_stream (false, (lazy (Build_stream (true,
    always_true)))))))))))

(** val example_ET3 : bool stream **)

let example_ET3 =
  lazy (Build_stream (true, (lazy (Build_stream (false,
    (lazy (Build_stream (true, (lazy (Build_stream (false,
    (lazy (Build_stream (true, (lazy (Build_stream (true,
    (lazy (Build_stream (true, always_true))))))))))))))))))))

(** val example_EF3 : bool stream **)

let example_EF3 =
  lazy (Build_stream (true, (lazy (Build_stream (false,
    (lazy (Build_stream (true, (lazy (Build_stream (false,
    (lazy (Build_stream (true, (lazy (Build_stream (true,
    (lazy (Build_stream (true, always_false))))))))))))))))))))

(** val test_ET : nat list **)

let test_ET =
  push_prompt p (fun _ -> take_ipp (infinite_bool example_ET) (S (S O)))

(** val test_EF : nat list **)

let test_EF =
  push_prompt p (fun _ -> take_ipp (infinite_bool example_EF) (S (S O)))

(** val test_ET1 : nat list **)

let test_ET1 =
  push_prompt p (fun _ -> take_ipp (infinite_bool example_ET1) (S (S O)))

(** val test_EF1 : nat list **)

let test_EF1 =
  push_prompt p (fun _ -> take_ipp (infinite_bool example_EF1) (S (S O)))

(** val test_ET2 : nat list **)

let test_ET2 =
  push_prompt p (fun _ ->
    take_ipp (infinite_bool example_ET2) (S (S (S (S O)))))

(** val test_EF2 : nat list **)

let test_EF2 =
  push_prompt p (fun _ ->
    take_ipp (infinite_bool example_EF2) (S (S (S (S O)))))

(** val test_ET3 : nat list **)

let test_ET3 =
  push_prompt p (fun _ ->
    take_ipp (infinite_bool example_ET3) (S (S (S (S (S (S O)))))))

(** val test_EF3 : nat list **)

let test_EF3 =
  push_prompt p (fun _ ->
    take_ipp (infinite_bool example_EF3) (S (S (S (S (S (S O)))))))