From 1273cd0e4e312fb9307fbddd17a90737b648e082 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Georges=20Dup=C3=A9ron?= <georges.duperon@gmail.com>
Date: Wed, 28 Oct 2015 19:28:46 +0100
Subject: [PATCH] Work done last week.

---
 graph/graph/rewrite-type.lp2.rkt | 69 ++++++++++++++++++++++++++++++++
 graph/lib/low-untyped.rkt        |  7 +++-
 graph/lib/low.rkt                | 31 +++++++++++++-
 3 files changed, 104 insertions(+), 3 deletions(-)
 create mode 100644 graph/graph/rewrite-type.lp2.rkt

diff --git a/graph/graph/rewrite-type.lp2.rkt b/graph/graph/rewrite-type.lp2.rkt
new file mode 100644
index 00000000..1089b04f
--- /dev/null
+++ b/graph/graph/rewrite-type.lp2.rkt
@@ -0,0 +1,69 @@
+#lang scribble/lp2
+@(require "../lib/doc.rkt")
+@doc-lib-setup
+
+@title[#:style manual-doc-style]{Rewriting data structures and their types}
+
+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.
+
+For example, one could replace all strings in a data structure by their length:
+
+@chunk[<test-example>
+       'a
+       (begin-for-syntax 
+         (displayln
+          (syntax->datum
+           (replace-in-data-structure #'(List (Pairof Symbol String))
+                                      #'([String Number string-length])))))
+       #;(define-syntax (string→number stx)
+           (replace-in-data-structure
+            #'(List (Pairof Symbol String))
+            #'[String Number string-length]))]
+
+@CHUNK[<replace-in-data-structure>
+       (define-for-syntax (replace-in-data-structure t r)
+         (define/with-syntax ([from to fun] ...) r)
+         (syntax-parse t
+           [x:id
+            #:attr assoc-from-to (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 ...)))]
+           [((~literal Pairof) a b)
+            #`(Pairof #,(replace-in-data-structure #'a r)
+                      #,(replace-in-data-structure #'b r))]
+           [x:id #'x]))]
+
+@chunk[<*>
+       (begin
+         (module main typed/racket;;;;;;;;;;
+           (require (for-syntax syntax/parse
+                                racket/syntax
+                                syntax/stx
+                                "../lib/low-untyped.rkt")
+                    "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))
+           
+           <replace-in-data-structure>)
+         
+         (require 'main)
+         (provide (all-from-out 'main))
+         
+         (module* test typed/racket
+           (require (submod "..")
+                    typed/rackunit
+                    "structure.lp2.rkt"
+                    "variant.lp2.rkt"
+                    "../type-expander/multi-id.lp2.rkt"
+                    "../type-expander/type-expander.lp2.rkt")
+           
+           <test-example>
+           
+           (require (submod ".." doc))))]
\ No newline at end of file
diff --git a/graph/lib/low-untyped.rkt b/graph/lib/low-untyped.rkt
index f4c9ce0f..3857c30d 100644
--- a/graph/lib/low-untyped.rkt
+++ b/graph/lib/low-untyped.rkt
@@ -6,11 +6,14 @@
 ;(require sugar/include)
 ;(include-without-lang-line "low.rkt")
 
-;; typed/racket/no-check does not require (for-syntax racket/base). TODO: file a bug report?
+;; typed/racket/no-check does not require (for-syntax racket/base).
+;; TODO: file a bug report?
 (require (for-syntax racket/base))
 (include/reader "low.rkt" (λ (source-name in)
                             (port-count-lines! in)
                             (do ()
-                              [(let-values ([(line column position) (port-next-location in)]) (> line 1))]
+                              [(let-values ([(line column position)
+                                             (port-next-location in)])
+                                 (> line 1))]
                               (read-line in))
                             (read-syntax source-name in)))
\ No newline at end of file
diff --git a/graph/lib/low.rkt b/graph/lib/low.rkt
index cbf95464..ff27b5be 100644
--- a/graph/lib/low.rkt
+++ b/graph/lib/low.rkt
@@ -378,7 +378,7 @@
 (define-modules ([no-submodule] [ids-untyped typed/racket/no-check])
   (provide format-ids
            hyphen-ids
-           format-temp-ids
+           format-temp-ids;
            #|t/gen-temp|#)
   
   (require/typed racket/syntax
@@ -496,4 +496,33 @@
      (generate-temporaries #'(id ...))]))
 |#
 
+;; ==== syntax.rkt ====
+
+(provide 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)
+                (∀ (a b c) (case→ [→ Any
+                                     (Listof (Pairof a b))
+                                     (U False (Pairof a b))]
+                                  [-> c
+                                      (Listof (Pairof a b))
+                                      (→ c a Boolean)
+                                      (U False (Pairof a b))]))])
+
+(: stx-assoc (∀ (T) (→ Identifier
+                       (U (Syntaxof (Listof (Syntaxof (Pairof Identifier T))))
+                          (Listof (Syntaxof (Pairof Identifier T)))
+                          (Listof (Pairof Identifier T)))
+                       (U (Pairof Identifier T) #f))))
+(define (stx-assoc id alist)
+  (let* ([e-alist (if (syntax? alist)
+                      (syntax->list alist)
+                      alist)]
+         [e-e-alist (cond
+                        [(null? e-alist) '()]
+                        [(syntax? (car e-alist)) (map (inst syntax-e (Pairof Identifier T)) e-alist)]
+                        [else e-alist])])
+    (assoc3 id e-e-alist free-identifier=?)))
+
 ;; ==== end ====
\ No newline at end of file