infinite-pigeonhole/IPP_proof.scm 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
;; This extracted scheme code relies on some additional macros
;; available at http://www.pps.univ-paris-diderot.fr/~letouzey/scheme
(load "macros_extr.scm")

(define __ (lambda (_) __))


(define projT1 (lambda (x) (match x
                              ((ExistT a _) a))))

(define callcc call/cc)

(define throw (lambda (x) x))

(define head (lambda (s) (match (force
                            s)
                            ((Build_stream head0 _) head0))))

(define tail (lambda (s) (match (force
                            s)
                            ((Build_stream _ tail0) tail0))))

(define depth (lambda (i)
  (match (force
     i)
     ((Build_ipp_stream depth0 _) depth0))))

(define rest (lambda (i)
  (match (force
     i)
     ((Build_ipp_stream _ rest0) rest0))))

(define coiter (lambdas (base next s) (delay `(Build_ipp_stream
  ,(@ base __ s) ,(lambda (_) (@ coiter base next (@ next __ s)))))))

(define corecM (lambdas (base next s) (delay `(Build_ipp_stream
  ,(@ base __ s) ,(lambda (_)
  (match (@ next __ s)
     ((Inl s0) s0)
     ((Inr x) (@ corecM base next x))))))))

(define corecC (lambdas (base next)
  (@ corecM base (lambdas (_ s)
    (callcc (lambda (disjret) `(Inr
      ,(@ next __ s (lambda (ret) (disjret `(Inl ,ret)))))))))))

(define bool_dec (lambdas (b b~)
  (match b
     ((True) (match b~
                ((True) `(Left))
                ((False) `(Right))))
     ((False) (match b~
                 ((True) `(Right))
                 ((False) `(Left)))))))

(define infinite_bool (lambda (bs)
  (let ((b0 (head bs)))
    (callcc (lambda (start)
      (@ coiter (lambdas (_ pat)
        (match pat
           ((ExistT x _) (match x
                            ((ExistT depth0 _) depth0))))) (lambdas (_ pat)
        (match pat
           ((ExistT x s)
             (match x
                ((ExistT depth0 rest0)
                  (match (@ bool_dec (head rest0) b0)
                     ((Left) `(ExistT ,`(ExistT ,`(S ,depth0) ,(tail rest0))
                       ,s))
                     ((Right)
                       (callcc (lambda (restart)
                         (@ throw s
                           (@ corecC (lambda (_) projT1) (lambdas (_ pat0
                             ret)
                             (match pat0
                                ((ExistT depth1 rest1)
                                  (match (@ bool_dec (head rest1) b0)
                                     ((Left)
                                       (@ throw restart `(ExistT ,`(ExistT
                                         ,`(S ,depth1) ,(tail rest1)) ,ret)))
                                     ((Right) `(ExistT ,`(S ,depth1)
                                       ,(tail rest1))))))) `(ExistT ,`(S
                             ,depth0) ,(tail rest0))))))))))))) `(ExistT
        ,`(ExistT ,`(O) ,(tail bs)) ,start)))))))

(define ipp_stream_depths (lambdas (bs k _ ms)
  (match k
     ((O) `(Nil))
     ((S k~)
       (match k~
          ((O) `(Cons ,(depth ms) ,`(Nil)))
          ((S _)
            (let ((d (depth ms)))
              (let ((ms~ (@ rest ms `(Tt))))
                `(Cons ,d ,(@ ipp_stream_depths bs k~ `(Some ,d) ms~))))))))))

(define take_ipp (lambdas (bs ms n) (@ ipp_stream_depths bs n `(None) ms)))

(define wrap (lambda (f) (f '(Tt))))

(define always_false (delay `(Build_stream ,`(False) ,always_false)))

(define test_stream (delay `(Build_stream ,`(True) (Build_stream ,`(False)
  (Build_stream ,`(True) (Build_stream ,`(False) (Build_stream ,`(True)
  (Build_stream ,`(True) (Build_stream ,`(False) (Build_stream ,`(False)
  (Build_stream ,`(True) (Build_stream ,`(True) ,always_false))))))))))))

(define test1
  (wrap (lambda (_)
    (@ take_ipp test_stream (infinite_bool test_stream) `(S ,`(O))))))

(define test2
  (wrap (lambda (_)
    (@ take_ipp test_stream (infinite_bool test_stream) `(S ,`(S ,`(O)))))))

(define test3
  (wrap (lambda (_)
    (@ take_ipp test_stream (infinite_bool test_stream) `(S ,`(S ,`(S
      ,`(O))))))))

(define test4
  (wrap (lambda (_)
    (@ take_ipp test_stream (infinite_bool test_stream) `(S ,`(S ,`(S ,`(S
      ,`(O)))))))))

(define test5
  (wrap (lambda (_)
    (@ take_ipp test_stream (infinite_bool test_stream) `(S ,`(S ,`(S ,`(S
      ,`(S ,`(O))))))))))

(define test6
  (wrap (lambda (_)
    (@ take_ipp test_stream (infinite_bool test_stream) `(S ,`(S ,`(S ,`(S
      ,`(S ,`(S ,`(O)))))))))))

(define test7
  (wrap (lambda (_)
    (@ take_ipp test_stream (infinite_bool test_stream) `(S ,`(S ,`(S ,`(S
      ,`(S ,`(S ,`(S ,`(O))))))))))))