diff --git a/graph/graph/graph2.lp2.rkt b/graph/graph/graph2.lp2.rkt
new file mode 100644
index 00000000..c577465d
--- /dev/null
+++ b/graph/graph/graph2.lp2.rkt
@@ -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))))]
\ No newline at end of file
diff --git a/graph/graph/rewrite-type.lp2.rkt b/graph/graph/rewrite-type.lp2.rkt
index cbfb0935..9ea4e166 100644
--- a/graph/graph/rewrite-type.lp2.rkt
+++ b/graph/graph/rewrite-type.lp2.rkt
@@ -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))))]
\ No newline at end of file
diff --git a/graph/lib/doc/example.lp2.rkt b/graph/lib/doc/example.lp2.rkt
index 9ac17225..65ae1c04 100644
--- a/graph/lib/doc/example.lp2.rkt
+++ b/graph/lib/doc/example.lp2.rkt
@@ -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]
\ No newline at end of file
+ -- be greyed out]
\ No newline at end of file