WIP on the graph draft

info.rkt

@@ -17,7 +17,8 @@
                "extensible-parser-specifications"
                "subtemplate"
                "stxparse-info"
-               "dotlambda"))
+               "dotlambda"
+               "typed-worklist"))
 (define build-deps '("scribble-lib"
                      "racket-doc"
                      "remember"

literals.rkt

@@ -0,0 +1,12 @@
+#lang racket
+
+(define-syntax-rule (provide-literals name ...)
+  (begin
+    (provide name ...)
+    (define-syntax (name stx)
+      (raise-syntax-error 'name
+                          "can only be used in some special contexts"
+                          stx))
+    ...))
+
+(provide-literals mapping node)

main-draft.hl.rkt

@@ -1,79 +1,153 @@
-#lang aful/unhygienic hyper-literate type-expander/lang
+#lang hyper-literate #:♦ #:no-auto-require (dotlambda/unhygienic . racket/base)
 
-@chunk[<overview>
-       #;(define-syntax low-graph
-           (syntax-parser
-             [<signature>
-              <metadata>
-              ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-              <worklist>
-              <call-mapping-functions+placeholders>
-              <extract-placeholders> ;; and put them into the worklist
-              ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-              <inline-placeholders-within-node-boundaries>
-              ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-              <replace-indices-with-promises>
-              ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-              <equality-coalescing> ;; leave off as always-#f-unless-eq?
-              <invariants+auto-fill>
-              <inflexible-row-polymorphism>
-              <flexible-row-polymorphism>
-              <polymorphic-node-types-and-mappings>
-              ;<general-purpose-graph-algorithms>
-              ;<garbage-collection>
-              ]))
+♦require[scribble-math
+         racket/require
+         (for-label (subtract-in (only-meta-in 0 type-expander/lang)
+                                 subtemplate/override)
+                    typed-worklist
+                    type-expander/expander
+                    phc-toolkit/untyped/aliases
+                    phc-toolkit/untyped/syntax-parse
+                    subtemplate/override)]
 
-       (define-syntax low-graph
+♦title[#:style (with-html5 manual-doc-style)
+       #:tag "graph-draft"
+       #:tag-prefix "phc-graph/graph-draft"]{Draft of the implementation of
+ the graph macro}
+
+♦(chunks-toc-prefix
+  '("(lib phc-graph/scribblings/phc-graph-implementation.scrbl)"
+    "phc-graph/graph-draft"))
+
+♦chunk[<overview>
+       (define low-graph-impl
          (syntax-parser
            [<signature+metadata>
-            ;; Phase 1: call the mapping functions on the input data
-            (: phase-1 (∀ (nodes-pvar … mapping-pvar … …)
-                          (→ (List (Listof mapping-arg-type) ddd)
-                             (List (Listof mapping-result-type) ddd))))
-            (define (phase-1 roots)
-              (work
-               roots
-               ((λ (mapping-arguments)
-                  (define result
-                    (let* ([mapping-name make-placeholder]
-                           …
-                           [arg convert-inflexible-to-flexible?]
-                           …
-                           [arg invariant-well-scopedness?]
-                           …)
-                      mapping-code))
-                  ;; returns placeholders + the result:
-                  (extract-placeholders result))
-                …)
-               (mapping-arg-type mapping-result-type) …))
-            (begin
-              ;; Maybe this should be done last, when all phases are available?
-              (define (phase1-many-roots) 'TODO)
-              (define (phase1-single-root-for-mapping) 'TODO)
-              …)
-            ;; Phase 2: inline placeholders within node boundaries
-            (generate-worklist
-             nodes
-             #'(…?))
-            (funcion which for a mapping-result → inserts nodes into worklist) …
-            (for the root mapping results
-              call the function to insert nodes and keep the surrounding part)
-            (for each mapping result
-              call the function to insert nodes)
-            ;; Phase 3: Replace indices with promises
-            ;; Phase 3a: have an empty set of invariant witnesses, and call the
-            ;;           invariants for checking
-            ;; Phase 3b: have the full set of invariant witnesses.
-            ;; TODO phase 3: auto-fill.
-            ]))
+            ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+            |<phase 1: call mappings and extract placeholders>|
+            ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+            |<phase 2: inline placeholders within node boundaries>|
+            ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+            |<phase 3: replace indices with promises>|
+            ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+            <equality-coalescing>
+            <invariants+auto-fill>
+            <inflexible-row-polymorphism>
+            <flexible-row-polymorphism>
+            <polymorphic-node-types-and-mappings>
+            ;<general-purpose-graph-algorithms>
+            ;<garbage-collection>
+            |<phase~1: call mappings and extract placeholders>|
+            ]))]
 
+♦chunk[<signature+metadata>
+       <signature>
+       <metadata>]
+
+♦chunk[<signature>
+       (_ graph-name
+          #:∀ (pvarₕ …)
+          ({~lit node} nodeᵢ [fieldᵢⱼ :colon field-τᵢⱼ] …)
+          …
+          ({~lit mapping} (mappingₖ [argₖₗ :colon arg-τₖₗ] …)
+                          :colon result-τₖ
+                          . bodyₖ)
+          …)]
+
+♦chunk[<metadata>
+       (void)]
+
+♦chunk[|<phase 1: call mappings and extract placeholders>|
+       '<worklist>
+       '<call-mapping-functions+placeholders>
+       '<extract-placeholders> ;; and put them into the worklist
+       ]
+
+♦chunk[|<phase~1: call mappings and extract placeholders>|
+       #'(begin
+           (define (make-placeholderₖ argₖₗ …)
+             (list 'placeholderₖ argₖₗ …))
+           …
+           
+           (define (graph-name [rootₖ : (Listof (List arg-τₖₗ …))] …)
+             (worklist
+              (list rootₖ …)
+              ((λ (args)
+                 (define-values (argₖₗ …) (apply values args))
+                 (define result
+                   (let* ([mappingₖ make-placeholderₖ]
+                          …
+                          [argₖₗ convert-inflexible-to-flexible?]
+                          …
+                          [argₖₗ invariant-well-scopedness?]
+                          …)
+                     . bodyₖ))
+                 ;; returns placeholders + the result:
+                 (extract-placeholders result))
+               …)
+              ((List arg-τₖₗ …) result-τₖ) …)))]
+
+♦chunk[|<phase 1: call mappings and extract placeholders>|
+       ;; Phase 1: call the mapping functions on the input data
+       #'(: phase-1 (∀ (pvarₕ …) ;; or use this? (nodes-pvar … mapping-pvar … …)
+                       (→ (List (Listof mapping-arg-type) ddd)
+                          (List (Listof mapping-result-type) ddd))))
+       #'(begin
+           ;; Maybe this should be done last, when all phases are available?
+           (define (phase1-many-roots (argₖₗ …) …) 'TODO)
+           (define (phase1-single-root-for-mapping (argₖₗ …)) 'TODO)
+           …)]
+
+♦chunk[|<phase 2: inline placeholders within node boundaries>|
+       ;; Phase 2: inline placeholders within node boundaries
+       '(generate-worklist
+         nodes
+         #'(…?))
+       '{(funcion which for a mapping-result → inserts nodes into worklist) …}
+       '(for the root mapping results
+          call the function to insert nodes and keep the surrounding part)
+       '(for each mapping result
+          call the function to insert nodes)]
+
+♦chunk[|<phase 3: replace indices with promises>|
+       ;; Phase 3: Replace indices with promises
+       ;; Phase 3a: have an empty set of invariant witnesses, and call the
+       ;;           invariants for checking
+       ;; Phase 3b: have the full set of invariant witnesses.
+       ;; TODO phase 3: auto-fill.
+       (void)]
+
+♦chunk[<equality-coalescing>
+       ;; implement as always-#f-unless-eq? for now
+       (void)]
+♦chunk[<invariants+auto-fill>
+       (void)]
+♦chunk[<inflexible-row-polymorphism>
+       (void)]
+♦chunk[<flexible-row-polymorphism>
+       (void)]
+♦chunk[<polymorphic-node-types-and-mappings>
+       (void)]
+
+♦chunk[<overview>
        ; high-level graph API:
-       '(<metadata2>
-         <extending-existing-graph-types>
-         <invariants-for-extended-graph-types>
-         <auto-generate-mappings>)]
+       #;(<metadata2>
+          <extending-existing-graph-types>
+          <invariants-for-extended-graph-types>
+          <auto-generate-mappings>)]
 
 Row polymorphism: make a generic struct->vector and vector->struct?
 
-@chunk[<*>
-       (void)]
+♦chunk[<*>
+       (provide low-graph-impl
+                (for-template (all-from-out "literals.rkt")))
+       
+       (require (for-template (only-meta-in 0 type-expander/lang)
+                              typed-worklist)
+                type-expander/expander
+                phc-toolkit/untyped/aliases
+                phc-toolkit/untyped/syntax-parse
+                subtemplate/override)
+
+       (require (for-template "literals.rkt"))
+       <overview>]

scribblings/phc-graph-implementation.scrbl

@@ -16,4 +16,5 @@ the @other-doc['(lib "phc-graph/scribblings/phc-graph.scrbl")] document.
 @include-section[(submod "../invariants-phantom.hl.rkt" doc)]
 @include-section[(submod "../graph-info.hl.rkt" doc)]
 @include-section[(submod "../graph-type.hl.rkt" doc)]
-@include-section[(submod "../graph.hl.rkt" doc)]
+@include-section[(submod "../graph.hl.rkt" doc)]
+@include-section[(submod "../main-draft.hl.rkt" doc)]

test/test-graph-low1.rkt

@@ -0,0 +1,17 @@
+#lang dotlambda/unhygienic type-expander/lang
+
+(require (for-syntax (lib "phc-graph/main-draft.hl.rkt")))
+
+(define-syntax low-graph low-graph-impl)
+
+(low-graph
+ g
+ #:∀ (A)
+ (node City [streets : (Listof Street)])
+ (node Street [name : String] [a : A])
+ (mapping (make-city [names : (Listof (Pairof String A))])
+   : City
+   (City (map make-street names)))
+ (mapping (make-street [p : (Pairof String A)])
+   : Street
+   (Street (car p) (cdr p))))