Implemented rewrite-type, but it does not work for vectors, because (λ ([x : (Vector String)]) (match x [(vector a) (cons 1 a)] [_ 'continue])) can yield 'continue, and it does not work for lists because of some type inference issues.

This commit is contained in:
Georges Dupéron 2015-11-09 13:02:30 +01:00
parent 449a6f4a09
commit 4a25c49169
3 changed files with 230 additions and 58 deletions

View File

@ -11,3 +11,99 @@
[new-z z])
(list new-x new-y new-z))])
(λ ((v : (List Symbol String)))
(match-abort
v
((list Symbol1 String2)
(let-abort
((Symbol3 (protected Symbol1)) (String4 (match-abort String2 ((and String5) (string-length String5)))))
(list (unprotect Symbol3) (unprotect String4))))))
(λ ([v : (List Symbol String)])
(match-abort
v
((list Symbol1 String2)
(let-abort
((Symbol3 #t) (String4 (match-abort String2 ((and String5) (string-length String5)))))
(list Symbol3 String4)))))
(λ ((v : (List Symbol String)))
(unprotect
(match-abort
v
((list Symbol1 String2)
(let-abort
((Symbol3 (protected Symbol1)) (String4 (match-abort String2 ((and String5) (protected (string-length String5))))))
(protected (list (unprotect Symbol3) (unprotect String4))))))))
(begin
(:
test1
( (List (Pairof (List Symbol (Listof String)) String)) (List (Pairof (List Symbol (Listof Number)) Number))))
(define (test1 v)
(unprotect
(match-abort
v
((list temp1)
(let-abort
((temp2
(match-abort
temp1
((cons temp3 String4)
(let-abort
((temp5
(match-abort
temp3
((list Symbol7 temp8)
(let-abort
((Symbol9 (protected Symbol7))
(temp10
(match-abort
temp8
((list String11 ...)
#;(map (λ ([String12 : String])
(unprotect (match-abort String12 ((and String13) (protected (string-length String13))))))
String11)
#;(map-abort
String11
String12
3 #;(match-abort String12 ((and String13) (protected (string-length String13)))))
(let ([l String11])
(if (null? l)
;; Special-case to avoid type inference issues with an empty
;; result-list.
'()
(let ([result-list (list (let ([String12 (car l)]) 3))])
(set! l (cdr l))
(do : (U 'continue 'break (Listof Number)) ([stop : (U #f #t 'continue 'break)
#f])
(stop (if (eq? stop 'continue)
'continue
(if (eq? stop 'break)
'break
(reverse result-list))))
(if (null? l)
(set! stop #t)
(let ([result (let ([String12 (car l)]) 3)])
(if (or (eq? result 'continue) (eq? result 'break))
(set! stop result)
(begin
(set! result-list (cons result result-list))
(set! l (cdr l))))))))))
))))
(protected (list (unprotect Symbol9) (unprotect temp10)))))))
(String6 (match-abort String4 ((and String14) (protected (string-length String14))))))
(protected (cons (unprotect temp5) (unprotect String6))))))))
(protected (list (unprotect temp2)))))))))

View File

@ -1,9 +1,23 @@
#lang typed/racket
(provide cond-abort
(provide (struct-out protected)
unprotect
cond-abort
match-abort
let-abort
let*-abort)
let*-abort
map-abort)
(struct (A) protected ([value : A]))
(define-syntax (unprotect stx)
(syntax-case stx ()
[(_ e0 . e)
(with-syntax ([(tmp) (generate-temporaries #'(e0))])
#'(let ([tmp (let () e0 . e)])
(if (protected? tmp)
(protected-value tmp)
tmp)))]))
(define-syntax (cond-abort orig-stx)
(let rec ([stx orig-stx])
@ -44,7 +58,7 @@
(cond
[(or (eq? 'continue binding) (eq? 'break binding)) binding]
...
[else (begin . body)])))
[else (let () . body)])))
(define-syntax (let*-abort stx)
(syntax-case stx ()
@ -56,6 +70,30 @@
binding
(let*-abort rest . body)))]))
(define-syntax (map-abort stx)
(syntax-case stx ()
[(_ lst var . body)
#'(let ([l lst])
(if (null? l)
;; Special-case to avoid type inference issues with an empty
;; result-list.
'()
(let ([result-list (list (let ([var (car l)]) . body))])
(set! l (cdr l))
(do ([stop : (U #f #t 'continue 'break)
#f])
(stop (if (or (eq? stop 'continue) (eq? stop 'break))
stop
(reverse result-list)))
(if (null? l)
(set! stop #t)
(let ([result (let ([var (car l)]) . body)])
(if (or (eq? result 'continue) (eq? result 'break))
(set! stop result)
(begin
(set! result-list (cons result result-list))
(set! l (cdr l))))))))))]))
(module* test typed/racket
(require typed/rackunit)
(require (submod ".."))

View File

@ -11,21 +11,41 @@ result.
For example, one could replace all strings in a data structure by their length:
@CHUNK[<test-example>
(define-syntax (make-replace stx)
(syntax-case stx ()
[(_ name type . replace)
(displayln (syntax->datum #`(begin
(: name ( type #,(replace-in-data-structure #'type #'replace)))
(define (name v)
#,(replace-in-instance #'v #'type #'replace)))))
#'(list)]))
(make-replace test1
(List (Pairof (List Symbol (Listof String)) String))
[String Number string-length])
;(test1 '((#(sym ("ab" "abc" "abcd")) . "a")))
(begin-for-syntax
#;(displayln
(syntax->datum
(replace-in-instance #'(List (Pairof (Vector Symbol
(Vectorof String))
String))
#'([String Number string-length]))))
(syntax->datum
(replace-in-instance #'v
#'(List (Pairof (Vector Symbol
(Vectorof String))
String))
#'([String Number string-length]))))
(displayln
(syntax->datum
(replace-in-instance #'(List Symbol String)
#'([String Number string-length])))))
#;(define-syntax (string→number stx)
(replace-in-data-structure
#'(List (Pairof Symbol String))
#'[String Number string-length]))]
(replace-in-instance #'v
#'(List Symbol String)
#'([String Number string-length])))))
(define-syntax (string→number stx)
#`(define-type new-t
#,(replace-in-data-structure
#'(List (Pairof (Vector Symbol (Vectorof String)) String))
#'([String Number string-length]))))
(string→number)]
@CHUNK[<replace-in-data-structure>
(define-for-syntax (replace-in-data-structure t r)
@ -51,52 +71,70 @@ For example, one could replace all strings in a data structure by their length:
[x:id #'x]))]
@CHUNK[<replace-in-instance>
(define-for-syntax (replace-in-instance t r)
(define-for-syntax (replace-in-instance val t r)
(define/with-syntax ([from to fun] ...) r)
(define (recursive-replace type)
(define (recursive-replace stx-val type)
(define/with-syntax val stx-val)
(syntax-parse type
[x:id
#:attr assoc-from-to (cdr-stx-assoc #'x #'((from . (to . fun)) ...))
#:when (attribute assoc-from-to)
#:with (to-type . to-fun) #'assoc-from-to
(define/with-syntax (tmp) (generate-temporaries #'(x)))
;; TODO: Add predicate for to-type in the pattern.
(cons #`(and tmp) #`(to-fun tmp))]
[((~literal List) a ...)
(define/with-syntax (tmp ...) (generate-temporaries #'(a ...)))
(define rec (stx-map recursive-replace #'(a ...)))
(cons #`(list #,@(map car rec))
#`(list #,@(map cdr rec)))]
[((~literal Pairof) a b)
(define/with-syntax (tmpa tmpb) (generate-temporaries #'(a b)))
(define reca (recursive-replace #'a))
(define recb (recursive-replace #'b))
(cons #`(cons #,(car reca) #,(car recb))
#`(cons #,(cdr reca) #,(cdr recb)))]
#| TODO:
[((~literal Listof) a)
#`(Listof #,(recursive-replace #'x))]
[((~literal Vector) a ...)
#`(Vector #,@(stx-map recursive-replace #'(a ...)))]
[((~literal Vectorof) a)
#`(Vectorof #,(recursive-replace #'a))]
|#
#|
[((~literal U) a ...)
;; Use (app (λ _ 'a) U-case) to set U-case, so that we can do a
;; very simple cond in the replacement.
;; TODO: write a `bind` match-expander, much like syntax-parse's
;; ~bind.
(define/with-syntax (tmp ...) (generate-temporaries #'(a ...)))
(cons #`(or (app (λ _')]
;; DOES NOT ACTUALLY WORK, because match wants all `or` branches to
;; have the same variables.
|#
[x:id
(define/with-syntax (tmp) (generate-temporaries #'(x)))
(cons #'tmp #'tmp)]))
(define whole-rec (recursive-replace t))
#`(λ (v) (match-abort v [#,(car whole-rec) #,(cdr whole-rec)])))]
[x:id
#:attr assoc-from-to (cdr-stx-assoc #'x
#'((from . (to . fun)) ...))
#:when (attribute assoc-from-to)
#:with (to-type . to-fun) #'assoc-from-to
(define/with-syntax (tmp) (generate-temporaries #'(x)))
;; TODO: Add predicate for to-type in the pattern.
#`(match-abort val [(and tmp) (protected (to-fun tmp))])]
[((~literal List) a ...)
(define/with-syntax (tmp1 ...) (generate-temporaries #'(a ...)))
(define/with-syntax (tmp2 ...) (generate-temporaries #'(a ...)))
(define/with-syntax (rec ...)
(stx-map recursive-replace #'(tmp1 ...) #'(a ...)))
#`(match-abort val
[(list tmp1 ...)
(let-abort ([tmp2 rec] ...)
(protected (list (unprotect tmp2) ...)))])]
[((~literal Pairof) a b)
(define/with-syntax (tmpa1 tmpb1) (generate-temporaries #'(a b)))
(define/with-syntax (tmpa2 tmpb2) (generate-temporaries #'(a b)))
(define/with-syntax reca (recursive-replace #'tmpa1 #'a))
(define/with-syntax recb (recursive-replace #'tmpb1 #'b))
#'(match-abort val
[(cons tmpa1 tmpb1)
(let-abort ([tmpa2 reca] [tmpb2 recb])
(protected (cons (unprotect tmpa2)
(unprotect tmpb2))))])]
#| TODO: |#
[((~literal Listof) a)
(define/with-syntax (tmp1) (generate-temporaries #'(a)))
(define/with-syntax (tmp1x) (generate-temporaries #'(a)))
(define/with-syntax rec (recursive-replace #'tmp1x #'a))
#'(match-abort val
[(list tmp1 (... ...))
(map-abort tmp1 tmp1x rec)])]
[((~literal Vector) a ...)
(define/with-syntax (tmp1 ...) (generate-temporaries #'(a ...)))
(define/with-syntax (tmp2 ...) (generate-temporaries #'(a ...)))
(define/with-syntax (rec ...)
(stx-map recursive-replace #'(tmp1 ...) #'(a ...)))
#`(match-abort val
[(vector tmp1 ...)
(let-abort ([tmp2 rec] ...)
(protected (list (unprotect tmp2) ...)))])]
#| TODO:
[((~literal Vectorof) a)
#`(Vectorof #,(recursive-replace #'a))]
;|#
[((~literal U) a ...)
(define/with-syntax (tmp1 ...) (generate-temporaries #'(a ...)))
(define/with-syntax (rec ...)
(stx-map recursive-replace #'(tmp1 ...) #'(a ...)))
#`(match-abort val
[tmp1 rec]
...)]
[x:id
#'(protected val)]))
;; TODO: if we recieve a 'continue or 'break, give a type error.
#`(unprotect #,(recursive-replace val t)))]
@chunk[<*>
(begin