From 35fe2e31f48bd9c58c859606ba9b6936d8375736 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Georges=20Dup=C3=A9ron?= <georges.duperon@gmail.com>
Date: Thu, 27 Apr 2017 02:02:56 +0200
Subject: [PATCH] WIP on the graph draft
---
info.rkt | 3 +-
literals.rkt | 12 ++
main-draft.hl.rkt | 214 ++++++++++++++-------
scribblings/phc-graph-implementation.scrbl | 3 +-
test/test-graph-low1.rkt | 17 ++
5 files changed, 177 insertions(+), 72 deletions(-)
create mode 100644 literals.rkt
create mode 100644 test/test-graph-low1.rkt
diff --git a/info.rkt b/info.rkt
index eb4e939..c190ec0 100644
--- a/info.rkt
+++ b/info.rkt
@@ -17,7 +17,8 @@
"extensible-parser-specifications"
"subtemplate"
"stxparse-info"
- "dotlambda"))
+ "dotlambda"
+ "typed-worklist"))
(define build-deps '("scribble-lib"
"racket-doc"
"remember"
diff --git a/literals.rkt b/literals.rkt
new file mode 100644
index 0000000..57dd0c1
--- /dev/null
+++ b/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)
\ No newline at end of file
diff --git a/main-draft.hl.rkt b/main-draft.hl.rkt
index 77f7009..c0b7bc1 100644
--- a/main-draft.hl.rkt
+++ b/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)]
\ No newline at end of file
+♦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>]
\ No newline at end of file
diff --git a/scribblings/phc-graph-implementation.scrbl b/scribblings/phc-graph-implementation.scrbl
index 6c32fec..d3fe94f 100644
--- a/scribblings/phc-graph-implementation.scrbl
+++ b/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)]
\ No newline at end of file
+@include-section[(submod "../graph.hl.rkt" doc)]
+@include-section[(submod "../main-draft.hl.rkt" doc)]
\ No newline at end of file
diff --git a/test/test-graph-low1.rkt b/test/test-graph-low1.rkt
new file mode 100644
index 0000000..c7a6a91
--- /dev/null
+++ b/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))))
\ No newline at end of file