sequence.rkt (9973B)
1 #lang typed/racket 2 (require "typed-untyped.rkt") 3 (define-typed/untyped-modules 4 (provide sequence-length>= 5 in-last? 6 in-tails 7 in-heads 8 in-split 9 in-split* 10 *in-split 11 Syntax-Listof 12 my-in-syntax 13 in-syntax 14 sequence-cons 15 sequence-null 16 sequence-list) 17 18 (require racket/sequence) 19 20 ;; sequence-length>= 21 (begin 22 (: sequence-length>= (→ (Sequenceof Any) Index Boolean)) 23 (define (sequence-length>= s l) 24 (let-values ([(more? next) (sequence-generate s)]) 25 (define (rec [remaining : Index]) : Boolean 26 (if (= remaining 0) 27 #t 28 (and (more?) 29 (begin (next) 30 (rec (sub1 remaining)))))) 31 (rec l)))) 32 33 ;; in-last? 34 ;; Returns a sequence of the same length as `s`. All values in the sequence 35 ;; are #f, except for the last one which is 'last. 36 (begin 37 (: in-last? (→ (Sequenceof Any) (Sequenceof (U #f 'last)))) 38 (define (in-last? s) 39 (if (sequence-length>= s 1) 40 (sequence-append (sequence-map (λ _ #f) (sequence-tail s 1)) 41 (in-value 'last)) 42 empty-sequence))) 43 44 ;; in-heads and in-tails 45 (begin 46 (: in-tails (∀ (T) (→ (Listof T) (Listof (Pairof T (Listof T)))))) 47 (define (in-tails l) 48 (if (null? l) 49 '() 50 (cons l (in-tails (cdr l))))) 51 52 (module+ test 53 (require typed/rackunit) 54 (check-equal? (for/list : (Listof (Listof Number)) 55 ([x : (Listof Number) (in-tails '(1 2 3 4 5))]) x) 56 '((1 2 3 4 5) (2 3 4 5) (3 4 5) (4 5) (5))) 57 (let ((l '(1 2 3 4 5))) 58 (check-true (eq? (caddr (for/list : (Listof (Listof Number)) 59 ([x : (Listof Number) (in-tails l)]) x)) 60 (cddr l))))) 61 62 (: in-heads (∀ (T) (→ (Listof T) (Listof (Pairof T (Listof T)))))) 63 (define (in-heads l) 64 (: my-append1 (→ (Listof T) T (Pairof T (Listof T)))) 65 (define (my-append1 x y) 66 (if (null? x) 67 (list y) 68 (cons (car x) (my-append1 (cdr x) y)))) 69 70 (define (on-heads/private [acc-head : (Listof T)] [l : (Listof T)]) 71 : (Listof (Pairof T (Listof T))) 72 (if (null? l) 73 '() 74 (let ([new-head (my-append1 acc-head (car l))]) 75 (cons new-head (on-heads/private new-head (cdr l)))))) 76 (on-heads/private '() l)) 77 78 (module+ test 79 (require typed/rackunit) 80 (check-equal? (for/list : (Listof (Listof Number)) 81 ([x : (Listof Number) (in-heads '(1 2 3 4 5))]) x) 82 '((1) (1 2) (1 2 3) (1 2 3 4) (1 2 3 4 5))))) 83 84 ;; in-split, in-split*, *in-split, *in-split* 85 (begin 86 ;; Can't write the type of in-split, because typed/racket doesn't allow 87 ;; writing (Sequenceof A B), just (Sequenceof A). 88 ;; in-parallel's type has access to the multi-valued version of Sequenceof, 89 ;; though, so we let typed/racket propagate the inferred type. 90 (define #:∀ (T) (in-split [l : (Listof T)]) 91 (in-parallel (sequence-append (in-value '()) (in-heads l)) 92 (sequence-append (in-tails l) (in-value '())))) 93 94 ;; Same as in-split, but without the empty tail. 95 (define #:∀ (T) (in-split* [l : (Listof T)]) 96 (in-parallel (sequence-append (in-value '()) (in-heads l)) 97 (sequence-append (in-tails l)))) 98 99 ;; Same as in-split, but without the empty head. 100 (define #:∀ (T) (*in-split [l : (Listof T)]) 101 (in-parallel (in-heads l) 102 (sequence-append (sequence-tail (in-tails l) 1) 103 (in-value '())))) 104 105 (define #:∀ (T) (*in-split* [l : (Listof T)]) 106 (in-parallel (in-heads l) 107 (sequence-tail (in-tails l) 1)))) 108 109 ;; my-in-syntax and Syntax-Listof 110 (begin 111 ;; See also syntax-e, which does not flatten syntax pairs, and syntax->list, 112 ;; which isn't correctly typed (won't take #'(a . (b c d e))). 113 (define-type (Syntax-Listof T) 114 (Rec R (Syntaxof (U Null 115 (Pairof T R) 116 (Listof T))))) 117 118 ;; in-syntax is now provided by racket/sequence. 119 (: my-in-syntax (∀ (T) (→ (Syntax-Listof T) 120 (Listof T)))) 121 (define (my-in-syntax stx) 122 (let ((e (syntax-e stx))) 123 (if (null? e) 124 e 125 (if (syntax? (cdr e)) 126 (cons (car e) (my-in-syntax (cdr e))) 127 e)))) 128 129 (define (test-in-syntax) 130 ; (ann `(,#'(a . b) ,#'(c . d)) 131 ; (Listof (Syntaxof (U (Pairof (Syntaxof 'a) (Syntaxof 'b)) 132 ; (Pairof (Syntaxof 'c) (Syntaxof 'c)))))) 133 (my-in-syntax #'((a . b) (c . d))) 134 ; (ann `(,#'a ,#'b ,#'c ,#'d ,#'e) (Listof (Syntaxof (U 'a 'b 'c 'd)))) 135 (my-in-syntax #'(a . (b c d e))) 136 ; (ann '() (Listof (Syntaxof Nothing))) 137 (my-in-syntax #'()))) 138 139 ;; combining sequences: 140 ;; sequence-cons 141 ;; sequence-null 142 ;; sequence-list 143 144 (begin 145 (: sequence-cons (∀ (A B) (→ (Sequenceof A) (Sequenceof B) 146 (Sequenceof (cons A B))))) 147 (define (sequence-cons sa sb) 148 (sequence-map (λ ([x : (List A B)]) (cons (car x) (cadr x))) 149 (in-values-sequence (in-parallel sa sb)))) 150 151 (: sequence-null (Sequenceof Null)) 152 (define sequence-null (in-cycle (in-value '()))) 153 154 (define #:∀ (A) (sequence-head [s : (Sequenceof A)]) 155 (sequence-ref s 0)) 156 157 (define #:∀ (A) (sequence-tail1 [s : (Sequenceof A)]) 158 (sequence-tail s 1)) 159 160 ;; sequence-list should have the type: 161 ;; (∀ (A ...) (→ (Sequenceof A) ... (Sequenceof (List A ...))))) 162 ;; But the type system rejects the two definitions below. 163 ;; This definition works, but it's the wrong type: 164 #;(: sequence-list (∀ (A) (→ (Sequenceof A) * 165 (Sequenceof (Listof A))))) 166 #;(define (sequence-list . sequences) 167 (if (null? sequences) 168 sequence-null 169 (sequence-cons (car sequences) 170 (apply sequence-list (cdr sequences))))) 171 172 ;; This definition works: 173 (: sequence-list (∀ (A ...) (→ (Sequenceof A) ... 174 (Sequenceof (List A ...))))) 175 176 (define (sequence-list . seqs) 177 (let ([more?+next 178 (map (λ #:∀ (T) ([s : (Sequenceof T)]) 179 (let-values ([(more? next) (sequence-generate s)]) 180 (cons more? next))) 181 seqs)]) 182 ((inst make-do-sequence Void (List A ...)) 183 (λ () [values (λ (_) 184 (map (λ #:∀ (T) ([mn : (Pairof (→ Boolean) (→ T))]) 185 ((cdr mn))) 186 more?+next)) 187 (λ (_) 188 (void)) 189 190 (void) 191 (λ (_) 192 (andmap (λ #:∀ (T) ([mn : (Pairof (→ Boolean) (→ T))]) 193 ((car mn))) 194 more?+next)) 195 #f 196 #f])))) 197 198 #;(define (sequence-list . seqs) 199 (let ([more?+next (map (λ #:∀ (T) ([s : (Sequenceof T)]) 200 : (Pairof (→ Boolean) (→ T)) 201 (let-values ([(more? next) 202 (sequence-generate s)]) 203 (cons more? next))) 204 seqs)]) 205 ((inst make-do-sequence 206 (List (Sequenceof A) ...) 207 (List A ...)) 208 (λ () 209 [values (λ (seqs2) 210 (map sequence-head 211 seqs2)) 212 (λ (seqs2) 213 (map sequence-tail1 214 seqs2)) 215 seqs 216 (λ (_) 217 (andmap (λ #:∀ (T) ([mn : (Pairof (→ Boolean) (→ T))]) 218 ((car mn))) 219 more?+next)) 220 (λ (seqs2) 221 'todo) 222 (λ _ 223 #t) 224 (λ _ 225 #t)])))) 226 227 (module+ test 228 (require typed/rackunit) 229 (check-equal? 230 (let-values ([(more? next) (sequence-generate 231 (sequence-list (in-list '(1 2 3)) 232 (in-vector #(a b c)) 233 (in-list '("x" "y" "z"))))]) 234 (list (more?) 235 (more?) 236 (next) 237 (next) 238 (more?) 239 (more?) 240 (more?) 241 (next) 242 (more?) 243 (more?) 244 (more?))) 245 '(#t #t (1 a "x") (2 b "y") #t #t #t (3 c "z") #f #f #f))) 246 247 #| 248 (: sequence-list (∀ (A ...) (→ (Sequenceof A) ... 249 (Sequenceof (List A ...))))) 250 (define (sequence-list . sequences) 251 (if (null? sequences) 252 sequence-null 253 (sequence-cons (car sequences) 254 (apply sequence-list (cdr sequences))))) 255 |# 256 257 #| 258 (: sequence-list (∀ (F R ...) 259 (case→ [→ (Sequenceof Null)] 260 [→ (Sequenceof F) (Sequenceof R) ... 261 (Sequenceof (List F R ...))]))) 262 (define sequence-list 263 (case-lambda 264 [() 265 sequence-null] 266 [(sequence . sequences) 267 (sequence-cons sequence (apply sequence-list sequences))])) 268 |#))