split-xlist.rkt (5640B)
1 #lang typed/racket 2 3 (require (for-syntax phc-toolkit/untyped 4 syntax/parse 5 syntax/parse/experimental/template 6 racket/pretty 7 racket/list) 8 (submod "implementation.rkt" typed) 9 "caret-identifier.rkt" 10 "infinity-identifier.rkt" 11 "once-identifier.rkt" 12 type-expander) 13 14 (provide split-xlist f-split-list m-split-xlist*) 15 16 (: f-split-list (∀ (A B) (→ (→ Any Boolean : B) 17 (→ (Rec R (U (Pairof A R) B)) 18 (List (Listof A) 19 B))))) 20 (define (f-split-list pred-b?) 21 (: recur (→ (Rec R (U (Pairof A R) B)) 22 (List (Listof A) 23 B))) 24 (define (recur l) 25 (if (pred-b? l) 26 (list '() l) 27 (let ([split-rest (recur (cdr l))]) 28 (cons (cons (car l) 29 (car split-rest)) 30 (cdr split-rest))))) 31 recur) 32 33 (define-syntax-rule (m-split-list v (xlist τ₁ ^ *₁ . whole-τ-rest)) 34 (((inst f-split-list τ₁ (xlist . whole-τ-rest)) 35 ;; TODO: could drop the tail type after the first mandatory repeat 36 ;; Not sure if that would make it possible to typecheck more easily 37 ;; though, as the rest of the type will be used to split the rest 38 ;; anyway. 39 (make-predicate (xlist . whole-τ-rest))) 40 v)) 41 42 (define-syntax (bounded-filter stx) 43 (syntax-case stx () 44 [(_ 0 heads t l) 45 #'(values (list . heads) l)] 46 [(_ n (headᵢ …) t l) 47 #`(if ((make-predicate t) l) 48 (values (list headᵢ …) l) 49 (bounded-filter #,(sub1 (syntax-e #'n)) 50 (headᵢ … (car l)) 51 t 52 (cdr l)))])) 53 54 (define-syntax m-split-xlist* 55 (λ (stx) 56 ((syntax-parser 57 #:literals (^ + - * once ∞) 58 [(_ v [v₁ vᵢ …] τ₁ ^ (once) {~seq τᵢ ^ *ᵢ} … #:rest r) 59 (template 60 (begin 61 (define v₁ (car v)) 62 (m-split-xlist* (cdr v) [vᵢ …] (?@ τᵢ ^ *ᵢ) … #:rest r)))] 63 [(_ v [v₁ vᵢ …] τ₁ ^ (power:nat) {~seq τᵢ ^ *ᵢ} … #:rest r) 64 #:with (tmp-car …) (map (λ _ (gensym 'car)) (range (syntax-e #'power))) 65 (template 66 (begin 67 (define-values (v₁ remaining-v) 68 (let* ([remaining-v v] 69 (?@ [tmp-car (car remaining-v)] 70 [remaining-v (cdr remaining-v)]) 71 …) 72 (values (list tmp-car …) remaining-v))) 73 (m-split-xlist* remaining-v [vᵢ …] (?@ τᵢ ^ *ᵢ) … #:rest r)))] 74 [(_ v [v₁ vᵢ …] τ₁ ^ (power:nat +) {~seq τᵢ ^ *ᵢ} … #:rest r) 75 #:with (tmp-car …) (map (λ _ (gensym 'car)) (range (syntax-e #'power))) 76 (template 77 (begin 78 (define-values (v₁ remaining-v) 79 (let* ([remaining-v v] 80 (?@ [tmp-car (car remaining-v)] 81 [remaining-v (cdr remaining-v)]) 82 …) 83 (define remaining-split 84 (m-split-list remaining-v 85 (xlist τ₁ ^ *₁ (?@ τᵢ ^ *ᵢ) … #:rest r))) 86 (values (list* tmp-car … (car remaining-split)) 87 (cdr remaining-split)))) 88 (m-split-xlist* remaining-v 89 [vᵢ …] (?@ τᵢ ^ *ᵢ) … #:rest r)))] 90 [(_ v [v₁ vᵢ …] τ₁ ^ (from:nat - to:nat) {~seq τᵢ ^ *ᵢ} … #:rest r) 91 #:with (tmp-car …) (map (λ _ (gensym 'car)) (range (syntax-e #'from))) 92 #:with difference (- (syntax-e #'to) (syntax-e #'from)) 93 (when (< (syntax-e #'difference) 0) 94 (raise-syntax-error 'xlist "invalid range: m is larger than n" #'-)) 95 (template 96 (begin 97 (define-values (v₁ remaining-v) 98 (let* ([remaining-v v] 99 (?@ [tmp-car (car remaining-v)] 100 [remaining-v (cdr remaining-v)]) 101 …) 102 (define-values (before remaining-after) 103 (bounded-filter difference 104 (tmp-car …) 105 (xlist (?@ τᵢ ^ *ᵢ) … #:rest r) 106 remaining-v)) 107 (values before 108 remaining-after))) 109 (m-split-xlist* remaining-v 110 [vᵢ …] (?@ τᵢ ^ *ᵢ) … #:rest r)))] 111 [(_ v [v₁ vᵢ …] τ₁ ^ *₁ {~seq τᵢ ^ *ᵢ} … #:rest r) 112 (template 113 (begin 114 (define split 115 (m-split-list v (xlist τ₁ ^ *₁ (?@ τᵢ ^ *ᵢ) … #:rest r))) 116 (define v₁ (car split)) 117 (m-split-xlist* (cadr split) [vᵢ …] (?@ τᵢ ^ *ᵢ) … #:rest r)))] 118 [(_ v [vr] #:rest r) 119 #'(define vr v)]) 120 stx))) 121 122 (define-match-expander split-xlist 123 (syntax-parser 124 #:literals (^) 125 [(_ pat . whole-τ) 126 (define/with-parse ({~seq normalized-τᵢ ^ normalized-*ᵢ} … #:rest τ-rest) 127 (normalize-xlist-type #'whole-τ this-syntax)) 128 129 (define-temp-ids "~a/v" (normalized-τᵢ …)) 130 ((λ (x) #;(pretty-write (syntax->datum x)) x) 131 (template 132 (app (λ (l) 133 (m-split-xlist* l 134 [normalized-τᵢ/v … rest/v] 135 (?@ normalized-τᵢ ^ normalized-*ᵢ) … 136 #:rest τ-rest) 137 (list normalized-τᵢ/v … rest/v)) 138 pat)))]))