From 116d16f74e6cb08f1890c7059bd3e45dd47a46a1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Georges=20Dup=C3=A9ron?= <georges.duperon@gmail.com>
Date: Tue, 10 Nov 2015 17:51:55 +0100
Subject: [PATCH] 56: Write more text in rewrite-type.lp2.rkt

---
 graph/graph/graph2.lp2.rkt       |  34 ++++
 graph/graph/rewrite-type.lp2.rkt | 338 ++++++++++++++++++-------------
 graph/lib/doc/example.lp2.rkt    |   8 +-
 3 files changed, 234 insertions(+), 146 deletions(-)
 create mode 100644 graph/graph/graph2.lp2.rkt

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