main.rkt (5876B)
1 #lang typed/racket 2 3 (provide worklist) 4 5 (require (only-in type-expander unsafe-cast)) 6 7 (struct (A) I ([v : A]) #:transparent) 8 (struct (A) O ([v : A]) #:transparent) 9 10 (: kons (∀ (A B) (→ A B (Pairof A B)))) 11 (define kons cons) 12 13 (begin 14 ;; Typed version of: 15 #;(define (append-inner-inner lll) 16 (apply map append lll)) 17 18 (: append-inner-inner (∀ (A ...) 19 (→ (Pairof (List (Listof (∩ I* A)) ...) 20 (Listof (List (Listof (∩ I* A)) ...))) 21 (List (Listof (∩ I* A)) ... A)))) 22 (define (append-inner-inner lll) 23 (if (null? lll) 24 '() 25 ;; Could also just use recursion here. 26 ((inst foldl 27 (List (Listof (∩ I* A)) ...) 28 (List (Listof (∩ I* A)) ...) 29 Nothing 30 Nothing) 31 map-append2 32 (car lll) 33 (cdr lll)))) 34 35 36 (: map-append2 (∀ (A ...) (→ (List (Listof A) ...) 37 (List (Listof A) ...) 38 (List (Listof A) ...)))) 39 (define (map-append2 la lb) 40 (map 41 (ann append (∀ (X) (→ (Listof X) (Listof X) (Listof X)))) la lb))) 42 43 (: map-cdr (∀ (A ...) (→ (List (Pairof Any A) ...) (List A ...)))) 44 (define (map-cdr l) 45 (map (λ #:∀ (X) ([x : (Pairof Any X)]) (cdr x)) l)) 46 47 (: map-car (∀ (A ...) (→ (List (Pairof A Any) ...) (List A ...)))) 48 (define (map-car l) 49 (map (λ #:∀ (X) ([x : (Pairof X Any)]) (car x)) l)) 50 51 (define-type I* (I Any)) 52 (define-type O* (O Any)) 53 54 (: worklist-function 55 (∀ (A ...) 56 (case→ (→ (List (Listof (∩ A I*)) ...) 57 (List (→ (∩ A I*) (List (∩ A O*) (Listof (∩ A I*)) ...)) ...) 58 (List (Listof (Pairof (∩ A I*) (∩ A O*))) ...))))) 59 60 (define (worklist-function roots processors) 61 (define nulls (map (λ (_) (ann '() (Listof Nothing))) processors)) 62 (define empty-sets (map list->set nulls)) 63 64 (define wrapped-processors 65 : (List (→ (∩ A I*) (List (Pairof (∩ A I*) (∩ A O*)) (Listof (∩ A I*)) ...)) 66 ...) 67 (map (λ #:∀ (In Out More) ([l : (Listof In)] [f : (→ In (Pairof Out More))]) 68 (λ ([in : In]) : (Pairof (Pairof In Out) More) 69 (let ([out (f in)]) 70 (cons (cons in (car out)) 71 (cdr out))))) 72 roots 73 processors)) 74 75 (define (loop [queue* : (List (Setof (∩ A I*)) ...)] 76 [done* : (List (Setof A) ...)]) 77 : (List (Listof (Pairof (∩ A I*) (∩ A O*))) ...) 78 79 (if (andmap set-empty? queue*) 80 (ann nulls (List (Listof (Pairof (∩ A I*) (∩ A O*))) ...)) 81 (let () 82 (define lqueue* (map set->list queue*)) 83 (define res (map map wrapped-processors lqueue*)) 84 (define new-done* (map set-union done* queue*)) 85 (define new-inputs 86 ((inst append-inner-inner A ... A) 87 (kons nulls 88 (map (λ ([x : (Listof 89 (Pairof Any (List (Listof (∩ A I*)) ...)))]) 90 ((inst append-inner-inner A ... A) 91 (kons nulls 92 (map-cdr x)))) 93 res)))) 94 95 (define outputs (map map-car res)) 96 97 (define new-to-do 98 (map set-subtract (map list->set new-inputs) new-done*)) 99 100 (map append 101 outputs 102 (loop new-to-do new-done*))))) 103 104 (loop (map list->set roots) empty-sets)) 105 106 ;(:type mapf) 107 ;(define (mapf vs procs) 108 ; (error "NIY")) 109 110 (define-syntax-rule (inst-worklist (In Out) ...) 111 ;; The unsafe-cast seems unnecessary on recent Typed Racket versions, and can 112 ;; be replaced with "ann". We should use a version check to use it only for 113 ;; backward-compatibility on older versions. 114 (unsafe-cast 115 (inst worklist-function 116 (U (I In) (O Out)) 117 ...) 118 ;; cast to its own type, circumventing the fact that TR doesn't seem to apply 119 ;; intersections in this case. 120 (-> (List (Listof (I In)) ...) 121 (List 122 (-> (I In) 123 (List 124 (O Out) 125 (Listof (I In)) 126 ...)) 127 ...) 128 (List (Listof (Pairof (I In) 129 (O Out))) 130 ...)))) 131 132 (: i* (∀ (A) (→ (Listof A) (Listof (I A))))) 133 (define (i* l) (map (inst I A) l)) 134 135 (: i** (∀ (A ...) (→ (List (Listof A) ...) (List (Listof (I A)) ...)))) 136 (define (i** ll) (map i* ll)) 137 138 (: wrap-io (∀ (A B C ...) (→ (→ A (List B (Listof C) ...)) 139 (→ (I A) (List (O B) (Listof (I C)) ...))))) 140 (define (wrap-io f) 141 (λ ([arg : (I A)]) 142 (define result (f (I-v arg))) 143 (kons (O (car result)) (map i* (cdr result))))) 144 145 (: unwrap-io1 (∀ (A B) (→ (Listof (Pairof (I A) (O B))) 146 (HashTable A B)))) 147 (define (unwrap-io1 l) 148 (make-immutable-hash 149 (map (λ ([x : (Pairof (I A) (O B))]) 150 (kons (I-v (car x)) (O-v (cdr x)))) 151 l))) 152 153 (define-syntax-rule (unwrap-io first-l (_ proc) ...) 154 (let*-values ([(new-l l) (values '() first-l)] 155 [(new-l l) 156 (begin proc 157 (values (kons (unwrap-io1 (car l)) 158 new-l) 159 (cdr l)))] 160 ... 161 [(new-l-reverse new-l-rest) (values '() new-l)] 162 [(new-l-reverse new-l-rest) 163 (begin proc 164 (values (kons (car new-l-rest) 165 new-l-reverse) 166 (cdr new-l-rest)))] 167 ...) 168 new-l)) 169 170 (define-syntax-rule (worklist roots (proc ...) (In Out) ... ) 171 (unwrap-io ((inst-worklist (In Out) ...) 172 (i** roots) 173 (list (wrap-io proc) ...)) 174 (proc 'dummy) ...))