suzanne.soy/type-expander
1
0
Fork 0
Code Issues 8 Pull Requests Actions Packages Projects Releases Wiki Activity

Wrote cond-abort module, started using it in rewrite-type.

Browse Source
This commit is contained in:
Georges Dupéron 2015-11-06 13:36:50 +01:00
parent 1273cd0e4e
commit 40fe7e03d5
3 changed files with 180 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

92
graph/graph/cond-abort.rkt Normal file
View File

@ -0,0 +1,92 @@
#lang typed/racket
(provide cond-abort
match-abort)
(define-syntax (cond-abort orig-stx)
(let rec ([stx orig-stx])
(syntax-case stx (else =>)
[(_)
#`(typecheck-fail #,orig-stx)]
[(_ [else body0 . body])
#`(let () body0 . body)]
[(_ [condition] . rest)
;; TODO: this does not work when body returns multiple values.
#`(let ([result condition])
(if (or (not result) (eq? result 'continue))
#,(rec #'(cond-abort . rest))
(if (eq? result 'break)
'continue
result)))]
[(_ [condition body0 . body] . rest)
;; TODO: this does not work when body returns multiple values.
#`(let ([result (if condition
(let () body0 . body)
'continue)])
(if (eq? result 'continue)
#,(rec #'(cond-abort . rest))
(if (eq? result 'break)
'continue
result)))])))
(define-syntax-rule (match-abort v [pattern body0 . body] ...)
(let ([v-cache v])
(cond-abort
[#t (match v-cache
[pattern (let () body0 . body)]
[_ 'continue])]
...)))
(module* test typed/racket
(require typed/rackunit)
(require (submod ".."))
;; Type Checker: Incomplete case coverage in: (cond-abort)
;(cond-abort)
(check-equal? (cond-abort [else 1]) 1)
(check-equal? (cond-abort [#f 0] [else 1]) 1)
(check-equal? (cond-abort [#t 2]) 2)
(check-equal? (cond-abort [#f 0] [#t 2]) 2)
(check-equal? (cond-abort [#t 'continue]
[#f (typecheck-fail #'"We should never get here")]
[#t 3])
3)
(check-equal?
(cond-abort
[#t 'continue]
[#t (let ([ret (cond-abort
[#t 'continue]
[#f (typecheck-fail #'"We should never get here")]
[#t 'break]
[#t (typecheck-fail #'"We should never get here")]
[#t 'continue]
[#t (typecheck-fail #'"We should never get here")])])
(ann ret 'continue))]
[#t 4])
4)
(check-equal?
(ann (let ([f (λ ([x : Integer])
(cond-abort
[#t (if (< x 3) 'continue x)]
[#f (typecheck-fail #'"We should never get here")]
[#t 4]
[else (typecheck-fail #'"We should never get here")]))])
(list (f 2) (f 7)))
(Listof Positive-Integer))
'(4 7))
(check-equal?
(match-abort '(1 2 3)
[(cons a b)
(match-abort b
[(list x y z) 'one]
[(cons x y) 'break]
[_ (typecheck-fail #'"We should never get here")])]
[(list a b c)
'two])
'two))

90
graph/graph/rewrite-type.lp2.rkt
View File

@ -10,13 +10,18 @@ result.
For example, one could replace all strings in a data structure by their length:
@chunk[<test-example>
'a
@CHUNK[<test-example>
(begin-for-syntax
#;(displayln
(syntax->datum
(replace-in-instance #'(List (Pairof (Vector Symbol
(Vectorof String))
String))
#'([String Number string-length]))))
(displayln
(syntax->datum
(replace-in-data-structure #'(List (Pairof Symbol String))
#'([String Number string-length])))))
(replace-in-instance #'(List Symbol String)
#'([String Number string-length])))))
#;(define-syntax (string→number stx)
(replace-in-data-structure
#'(List (Pairof Symbol String))
@ -24,20 +29,75 @@ For example, one could replace all strings in a data structure by their length:
@CHUNK[<replace-in-data-structure>
(define-for-syntax (replace-in-data-structure t r)
(define (recursive-replace new-t) (replace-in-data-structure new-t r))
(define/with-syntax ([from to fun] ...) r)
(syntax-parse t
[x:id
#:attr assoc-from-to (stx-assoc #'x #'((from . to) ...))
#:attr assoc-from-to (cdr-stx-assoc #'x #'((from . to) ...))
#:when (attribute assoc-from-to)
#'assoc-from-to]
[((~literal List) a ...)
#`(List #,@(stx-map (λ (x) (replace-in-data-structure x r))
#'(a ...)))]
#`(List #,@(stx-map recursive-replace #'(a ...)))]
[((~literal Pairof) a b)
#`(Pairof #,(replace-in-data-structure #'a r)
#,(replace-in-data-structure #'b r))]
#`(Pairof #,(recursive-replace #'a) #,(recursive-replace #'b))]
[((~literal Listof) a)
#`(Listof #,(recursive-replace #'a))]
[((~literal Vector) a ...)
#`(Vector #,@(stx-map recursive-replace #'(a ...)))]
[((~literal Vectorof) a)
#`(Vectorof #,(recursive-replace #'a))]
[((~literal U) a ...)
#`(U #,@(stx-map recursive-replace #'(a ...)))]
[x:id #'x]))]
@CHUNK[<replace-in-instance>
(define-for-syntax (replace-in-instance t r)
(define/with-syntax ([from to fun] ...) r)
(define (recursive-replace type)
(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)])))]
@chunk[<*>
(begin
(module main typed/racket;;;;;;;;;;
@ -48,10 +108,13 @@ For example, one could replace all strings in a data structure by their length:
"structure.lp2.rkt"
"variant.lp2.rkt"
"../type-expander/multi-id.lp2.rkt"
"../type-expander/type-expander.lp2.rkt")
(begin-for-syntax (provide replace-in-data-structure))
"../type-expander/type-expander.lp2.rkt"
"cond-abort.rkt")
(begin-for-syntax (provide replace-in-data-structure
replace-in-instance))
<replace-in-data-structure>)
<replace-in-data-structure>
<replace-in-instance>)
(require 'main)
(provide (all-from-out 'main))
@ -62,7 +125,8 @@ For example, one could replace all strings in a data structure by their length:
"structure.lp2.rkt"
"variant.lp2.rkt"
"../type-expander/multi-id.lp2.rkt"
"../type-expander/type-expander.lp2.rkt")
"../type-expander/type-expander.lp2.rkt"
"cond-abort.rkt")
<test-example>

12
graph/lib/low.rkt
View File

@ -498,7 +498,7 @@
;; ==== syntax.rkt ====
(provide stx-assoc)
(provide stx-assoc cdr-stx-assoc)
;(require/typed racket/base [(assoc assoc3) (∀ (a b) (→ Any (Listof (Pairof a b)) (U False (Pairof a b))))])
(require/typed racket/base
[(assoc assoc3)
@ -525,4 +525,14 @@
[else e-alist])])
(assoc3 id e-e-alist free-identifier=?)))
(: cdr-stx-assoc
(∀ (T) (→ Identifier
(U (Syntaxof (Listof (Syntaxof (Pairof Identifier T))))
(Listof (Syntaxof (Pairof Identifier T)))
(Listof (Pairof Identifier T)))
(U T #f))))
(define (cdr-stx-assoc id alist)
(let ((res (stx-assoc id alist)))
(if res (cdr res) #f)))
;; ==== end ====