56: Write more text in rewrite-type.lp2.rkt
This commit is contained in:
Georges Dupéron
parent
e8ab36d022
commit
116d16f74e
34
graph/graph/graph2.lp2.rkt
Normal file
34
graph/graph/graph2.lp2.rkt
Normal file
|
|
@ -0,0 +1,34 @@
|
|||
#lang scribble/lp2
|
||||
@(require "../lib/doc.rkt")
|
||||
@doc-lib-setup
|
||||
|
||||
@title[#:style manual-doc-style]{Graph library}
|
||||
|
||||
@(table-of-contents)
|
||||
|
||||
@section{Introduction}
|
||||
|
||||
|
||||
|
||||
@section{Conclusion}
|
||||
|
||||
@chunk[<*>
|
||||
(begin
|
||||
(module main typed/racket
|
||||
(require (for-syntax syntax/parse
|
||||
racket/syntax
|
||||
"../lib/low-untyped.rkt")
|
||||
"../lib/low.rkt")
|
||||
|
||||
)
|
||||
|
||||
(require 'main)
|
||||
(provide (all-from-out 'main))
|
||||
|
||||
(module* test typed/racket
|
||||
(require (submod "..")
|
||||
typed/rackunit)
|
||||
|
||||
|
||||
|
||||
(require (submod ".." doc))))]
|
||||
|
|
@ -4,6 +4,7 @@
|
|||
|
||||
@title[#:style manual-doc-style]{Rewriting data structures and their types}
|
||||
|
||||
@section[#:tag "sec:intro-example"]{Introductory example}
|
||||
This module allows purely functional substitution inside a data structure of
|
||||
arbitrarily deep elements of a given type, while also computing the type of the
|
||||
result.
|
||||
|
|
@ -11,15 +12,42 @@ result.
|
|||
For example, one could replace all strings in a data structure by their length:
|
||||
|
||||
@CHUNK[<test-example>
|
||||
(make-replace test-example
|
||||
(Vectorof (U (List 'tag1 String) (List 'tag2 Number)))
|
||||
[String Number string-length])]
|
||||
|
||||
The result's type would be derived from the original one, but all occurrences of
|
||||
@tc[String] have been replaced by @tc[Number]. The result itself would have the
|
||||
value returned by string-length instead of each string, everything else being
|
||||
identical.
|
||||
|
||||
@CHUNK[<test-example>
|
||||
(check-equal?
|
||||
(ann (test-example '#((tag1 "a") (tag2 7) (tag1 "bcd")))
|
||||
(Vectorof (U (List 'tag1 Number) (List 'tag2 Number))))
|
||||
'#((tag1 1) (tag2 7) (tag1 3)))]
|
||||
|
||||
In this example, we used @tc[make-replace], a test macro defined below which
|
||||
relies on the lower-level utilities provided by this module, namely
|
||||
@tc[replace-in-type] and @tc[replace-in-instance].
|
||||
|
||||
@CHUNK[<test-make-replace>
|
||||
(define-syntax (make-replace stx)
|
||||
(syntax-case stx ()
|
||||
[(_ name type . replace)
|
||||
#`(begin
|
||||
(: name (→ type #,(replace-in-data-structure #'type #'replace)))
|
||||
(: name (→ type #,(replace-in-type #'type #'replace)))
|
||||
(define (name v)
|
||||
#,(replace-in-instance #'v #'type #'replace)))]))
|
||||
|
||||
(make-replace test1
|
||||
#,(replace-in-instance #'v #'type #'replace)))]))]
|
||||
|
||||
@subsection{A bigger example}
|
||||
|
||||
We would expect this to work on bigger types without any extra efforts. In the
|
||||
following example, we replace all strings with their length, on a bigger
|
||||
example:
|
||||
|
||||
@CHUNK[<test-big>
|
||||
(make-replace test-big
|
||||
(List (Pairof (U (List 'tag1 (List (Vector Symbol)
|
||||
Number
|
||||
(Listof String)))
|
||||
|
|
@ -27,10 +55,14 @@ For example, one could replace all strings in a data structure by their length:
|
|||
Number
|
||||
(Listof String))))
|
||||
String))
|
||||
[String Number string-length])
|
||||
|
||||
[String Number string-length])]
|
||||
|
||||
The replacement function @tc[test-big] defined above will, as expected, have a
|
||||
return type containing no more strings, and the correct return value.
|
||||
|
||||
@CHUNK[<test-big>
|
||||
(check-equal?
|
||||
(ann (test1 '(((tag2 (#(sym) 7 ("ab" "abc" "abcd"))) . "a")))
|
||||
(ann (test-big '(((tag2 (#(sym) 7 ("ab" "abc" "abcd"))) . "a")))
|
||||
(List (Pairof (U (List 'tag1 (List (Vector Symbol)
|
||||
Number
|
||||
(Listof Number)))
|
||||
|
|
@ -40,84 +72,142 @@ For example, one could replace all strings in a data structure by their length:
|
|||
Number)))
|
||||
'(((tag2 (#(sym) 7 (2 3 4))) . 1)))]
|
||||
|
||||
@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))
|
||||
@section{Replacing parts of a type}
|
||||
|
||||
The @tc[replace-in-type] @tc[for-syntax] function is pretty straightforward: it
|
||||
checks whether the given type matches one of the substitution rules given in
|
||||
@tc[r]. If no substitution rule was found, it matches the type against a small
|
||||
set of known type constructors like @tc[List] or @tc[Pairof], and recursively
|
||||
calls itself on the components of the type.
|
||||
|
||||
@CHUNK[<replace-in-type>
|
||||
(define-for-syntax (replace-in-type t r)
|
||||
(define (recursive-replace new-t) (replace-in-type new-t r))
|
||||
(define/with-syntax ([from to fun] ...) r)
|
||||
(syntax-parse t
|
||||
[x:id
|
||||
#:attr assoc-from-to (cdr-stx-assoc #'x #'((from . to) ...))
|
||||
#:when (attribute assoc-from-to)
|
||||
#'assoc-from-to]
|
||||
[((~literal List) a ...)
|
||||
#`(List #,@(stx-map recursive-replace #'(a ...)))]
|
||||
[((~literal Pairof) a b)
|
||||
#`(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 ...)))]
|
||||
[((~literal quote) a)
|
||||
;; TODO: if the quoted type is a primitive, we should replace it too
|
||||
#`(quote a)]
|
||||
[x:id #'x]))]
|
||||
<replace-in-type-substitute>
|
||||
<replace-in-type-other-cases>))]
|
||||
|
||||
The clause that matches the type against the substitution rules uses the
|
||||
@tc[stx-assoc] function defined in our library, which uses
|
||||
@tc[free-identifier=?] to find the first pair which @tc[car] or @tc[stx-car]
|
||||
matches the given type @tc[#'x].
|
||||
|
||||
@CHUNK[<replace-in-type-substitute>
|
||||
[x:id
|
||||
#:attr assoc-from-to (cdr-stx-assoc #'x #'((from . to) ...))
|
||||
#:when (attribute assoc-from-to)
|
||||
#'assoc-from-to]]
|
||||
|
||||
The other cases use @tc[~literal] and a syntax pattern to find uses of
|
||||
@tc[List], @tc[Pairof], @tc[Vectorof] etc.
|
||||
|
||||
@CHUNK[<replace-in-type-other-cases>
|
||||
[((~literal List) a ...)
|
||||
#`(List #,@(stx-map recursive-replace #'(a ...)))]
|
||||
[((~literal Pairof) a b)
|
||||
#`(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 ...)))]
|
||||
<replace-in-type-case-quote>
|
||||
[x:id
|
||||
#'x]]
|
||||
|
||||
TODO: If the type is a quoted primitive, we should replace it too, for example
|
||||
@tc['("abc" symbol)] should be transformed into @tc['(3 symbol)] if we apply the
|
||||
@tc[[String Number string-length]] substitution from the example in section
|
||||
@secref{sec:intro-example}.
|
||||
|
||||
@CHUNK[<replace-in-type-case-quote>
|
||||
[((~literal quote) a)
|
||||
#`(quote a)]]
|
||||
|
||||
@section{Replacing parts of an instance}
|
||||
|
||||
The @tc[replace-in-instance] for-syntax function is defined in a similar way,
|
||||
with an internal definition for @tc[recursive-replace]. The case of unions is
|
||||
offloaded to a separate subroutine.
|
||||
|
||||
@CHUNK[<replace-in-instance>
|
||||
(define-for-syntax (replace-in-instance val t r)
|
||||
(define/with-syntax ([from to fun] ...) r)
|
||||
<recursive-replace-in-instance>
|
||||
<replace-in-union>
|
||||
(define (recursive-replace stx-val type)
|
||||
(define/with-syntax val stx-val)
|
||||
(define/with-syntax (v-cache) (generate-temporaries #'(val-cache)))
|
||||
(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.
|
||||
#`(to-fun val)]
|
||||
[((~literal List) a ...)
|
||||
(define/with-syntax (tmp ...) (generate-temporaries #'(a ...)))
|
||||
#`(let-values ([(tmp ...) (apply values val)])
|
||||
(list #,@(stx-map recursive-replace #'(tmp ...) #'(a ...))))]
|
||||
[((~literal Pairof) a b)
|
||||
#`(let ([v-cache val])
|
||||
(cons #,(recursive-replace #'(car v-cache) #'a)
|
||||
#,(recursive-replace #'(cdr v-cache) #'b)))]
|
||||
[((~literal Listof) a)
|
||||
(define/with-syntax (tmp) (generate-temporaries #'(a)))
|
||||
#`(map (λ ([tmp : a]) #,(recursive-replace #'tmp #'a))
|
||||
val)]
|
||||
[((~literal Vector) a ...)
|
||||
(define/with-syntax (tmp ...) (generate-temporaries #'(a ...)))
|
||||
(define/with-syntax (idx ...) (generate-indices #'(a ...)))
|
||||
#`(let ([v-cache val])
|
||||
(let ([tmp (vector-ref v-cache idx)]
|
||||
...)
|
||||
(vector #,@(stx-map recursive-replace
|
||||
#'(tmp ...)
|
||||
#'(a ...)))))]
|
||||
[((~literal Vectorof) a)
|
||||
(define/with-syntax (tmp) (generate-temporaries #'(a)))
|
||||
#`(vector-map (λ ([tmp : a]) #,(recursive-replace #'tmp #'a))
|
||||
val)]
|
||||
[((~literal U) a ...)
|
||||
#`(let ([v-cache val])
|
||||
(cond
|
||||
#,@(stx-map (λ (ta) (replace-in-union #'v-cache ta r))
|
||||
#'(a ...))))]
|
||||
[((~literal quote) a)
|
||||
#'val]
|
||||
[x:id
|
||||
#'val]))
|
||||
(recursive-replace val t))]
|
||||
|
||||
The @tc[recursive-replace] internal function defined below takes a type
|
||||
@tc[type] and produces an expression that transforms instances of that type
|
||||
using the substitution rules given in the parameter @tc[r] of the enclosing
|
||||
function.
|
||||
|
||||
The expression assumes that the instance to be transformed is located in the
|
||||
variable or expression @tc[stx-val], and caching is used where needed to avoid
|
||||
evaluating @tc[stx-val] twice. Here is the case that handles @tc[Pairof], which
|
||||
caches @tc[val] and calls @tc[recursive-replace] with the @tc[car] and @tc[cdr]
|
||||
as expressions:
|
||||
|
||||
@CHUNK[<replace-in-instance-case-pairof>
|
||||
[((~literal Pairof) a b)
|
||||
#`(let ([v-cache val])
|
||||
(cons #,(recursive-replace #'(car v-cache) #'a)
|
||||
#,(recursive-replace #'(cdr v-cache) #'b)))]]
|
||||
|
||||
The other cases are similarly defined:
|
||||
|
||||
@CHUNK[<recursive-replace-in-instance>
|
||||
(define (recursive-replace stx-val type)
|
||||
(define/with-syntax val stx-val)
|
||||
(define/with-syntax (v-cache) (generate-temporaries #'(val-cache)))
|
||||
(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.
|
||||
#`(to-fun val)]
|
||||
[((~literal List) a ...)
|
||||
(define/with-syntax (tmp ...) (generate-temporaries #'(a ...)))
|
||||
#`(let-values ([(tmp ...) (apply values val)])
|
||||
(list #,@(stx-map recursive-replace #'(tmp ...) #'(a ...))))]
|
||||
<replace-in-instance-case-pairof>
|
||||
[((~literal Listof) a)
|
||||
(define/with-syntax (tmp) (generate-temporaries #'(a)))
|
||||
#`(map (λ ([tmp : a]) #,(recursive-replace #'tmp #'a))
|
||||
val)]
|
||||
[((~literal Vector) a ...)
|
||||
(define/with-syntax (tmp ...) (generate-temporaries #'(a ...)))
|
||||
(define/with-syntax (idx ...) (generate-indices #'(a ...)))
|
||||
#`(let ([v-cache val])
|
||||
(let ([tmp (vector-ref v-cache idx)]
|
||||
...)
|
||||
(vector #,@(stx-map recursive-replace
|
||||
#'(tmp ...)
|
||||
#'(a ...)))))]
|
||||
[((~literal Vectorof) a)
|
||||
(define/with-syntax (tmp) (generate-temporaries #'(a)))
|
||||
#`(vector-map (λ ([tmp : a]) #,(recursive-replace #'tmp #'a))
|
||||
val)]
|
||||
[((~literal U) a ...)
|
||||
#`(let ([v-cache val])
|
||||
(cond
|
||||
#,@(stx-map (λ (ta) (replace-in-union #'v-cache ta r))
|
||||
#'(a ...))))]
|
||||
[((~literal quote) a)
|
||||
#'val]
|
||||
[x:id
|
||||
#'val]))]
|
||||
|
||||
For unions, we currently support only tagged unions, that is unions where each
|
||||
possible type is a @tc[List] with a distinct @tc[tag] in its first element.
|
||||
TODO: we currently don't check that each @tc[tag] is distinct.
|
||||
|
||||
@CHUNK[<replace-in-union>
|
||||
(define (replace-in-union stx-v-cache t r)
|
||||
(define/with-syntax v-cache stx-v-cache)
|
||||
|
|
@ -126,76 +216,34 @@ For example, one could replace all strings in a data structure by their length:
|
|||
<replace-in-tagged-union-instance>]
|
||||
[_ (error "Type-replace on untagged Unions isn't supported yet!")]))]
|
||||
|
||||
For cases of the union which are a tagged list, we use a simple guard, and call
|
||||
@tc[recursive-replace] on the whole @tc[(List 'tag b ...)] type.
|
||||
|
||||
@CHUNK[<replace-in-tagged-union-instance>
|
||||
#`[(and (list? v-cache) (eq? 'tag (car v-cache)))
|
||||
#`[(and (list? v-cache)
|
||||
(not (null? v-cache))
|
||||
(eq? 'tag (car v-cache)))
|
||||
#,(recursive-replace #'v-cache t)]]
|
||||
|
||||
Handling freer forms of unions causes some problems:
|
||||
|
||||
@CHUNK[<replace-in-instance_old>
|
||||
(define-for-syntax (replace-in-instance val t r)
|
||||
(define/with-syntax ([from to fun] ...) r)
|
||||
(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.
|
||||
#`(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)))]
|
||||
@itemlist[
|
||||
@item{There are some types without make-predicate, so we can't use
|
||||
@racket[(make-predicate T)] to know what case of the union we are in}
|
||||
@item{There are some types for which there is no predicate, like function types
|
||||
with the same arity}
|
||||
@item{There are some types for which the type system doesn't acknowledge the
|
||||
predicates, e.g. @racket[(U (Vector Number) (Vector String String))]: we can't
|
||||
even bound the type of @racket[(vector-ref x 0)] in that case, it defaults to
|
||||
@racket[Any].}]
|
||||
|
||||
These issues and possible solutions are addressed in more
|
||||
detail in the
|
||||
@hyperlink[(string-append "https://phc.fogbugz.com/f/cases/54/"
|
||||
"Rethink-how-to-do-the-multi-step-types-more-inside")]
|
||||
{FogBugz case 54}.
|
||||
|
||||
@section{Conclusion}
|
||||
|
||||
@chunk[<*>
|
||||
(begin
|
||||
|
|
@ -209,10 +257,10 @@ For example, one could replace all strings in a data structure by their length:
|
|||
"../type-expander/multi-id.lp2.rkt"
|
||||
"../type-expander/type-expander.lp2.rkt"
|
||||
"cond-abort.rkt")
|
||||
(begin-for-syntax (provide replace-in-data-structure
|
||||
(begin-for-syntax (provide replace-in-type
|
||||
replace-in-instance))
|
||||
|
||||
<replace-in-data-structure>
|
||||
<replace-in-type>
|
||||
<replace-in-instance>)
|
||||
|
||||
(require 'main)
|
||||
|
|
@ -227,6 +275,8 @@ For example, one could replace all strings in a data structure by their length:
|
|||
"../type-expander/type-expander.lp2.rkt"
|
||||
"cond-abort.rkt")
|
||||
|
||||
<test-make-replace>
|
||||
<test-example>
|
||||
<test-big>
|
||||
|
||||
(require (submod ".." doc))))]
|
||||
|
|
@ -30,12 +30,16 @@ Blah @math{n}, as described by M@._ Foo@.__
|
|||
(define (foo)
|
||||
(syntax-e #`#,"foo"))]
|
||||
|
||||
@itemlist[
|
||||
@item{Item 1}
|
||||
@item{Item 2}]
|
||||
|
||||
@(define to-insert 42)
|
||||
@chunk[<*>
|
||||
;(displayln #,to-insert) ;; Should work.
|
||||
(provide foo)
|
||||
<foo>
|
||||
|
||||
|
||||
(module* test racket
|
||||
(require (submod ".."))
|
||||
(require rackunit)
|
||||
|
|
@ -56,4 +60,4 @@ But we would actually want:
|
|||
(define-syntax-rule (double x) -- should be greyed out
|
||||
(let ((x-cache x))
|
||||
(+ x-cache x-cache))) -- everything except the changed bits should
|
||||
-- be greyed out]
|
||||
-- be greyed out]
|
||||
Loading…
Reference in New Issue
Block a user