commit 8ff2a1d267e0d529e19fcdb16c56bb8040ed2555
parent b6043def446124c9a21de2ea45bdfcfbf33fddcd
Author: Georges Dupéron <georges.duperon@gmail.com>
Date: Fri, 12 May 2017 01:08:02 +0200
TR Bug in flexible-with-generalized-ctor.hl.rkt: typed-racket-lib/typed-racket/types/overlap.rkt:40:0: mask-accessor: contract violation expected: mask? given: #f
Diffstat:
9 files changed, 582 insertions(+), 2 deletions(-)
diff --git a/.travis.yml b/.travis.yml
@@ -28,7 +28,8 @@ env:
#- RACKET_VERSION=6.4
#- RACKET_VERSION=6.5
#- RACKET_VERSION=6.6
- #- RACKET_VERSION=6.7
+ - RACKET_VERSION=6.8
+ - RACKET_VERSION=6.9
- RACKET_VERSION=HEAD
matrix:
diff --git a/TODO.txt b/TODO.txt
@@ -0,0 +1,57 @@
+:::::::::Current task:
+
+with*: optimize by naming clusters of "missing", and naming types for known flex structs
+
+with*: call from phc-adt, wrappers to and from the actual structs
+
+:::::::::In progress:
+
+Draft the graph implementation
+
+Modularity
+
+:::::::::Ready:
+
+Run-time checkers for invariants
+
+Cleanup invariants-phantom.hl.rkt
+
+Implement graph
+
+Implement the first graph generation pass, with a placeholder wrapping each mapping result
+
+Implement the second graph generation pass: inline nodes
+
+Implement the third graph generation pass: replacing indices with promises
+
+Combine the graph passes into a single macro
+
+Relicensing
+
+Write "middle-dot" language extension
+
+Drop MathJax, directly print Unicode or render via LaTeX (speed & licensing issues)
+
+::::::::Later:
+
+Garbage collect graph
+
+Merge tagged-anytag-match into the regular match for tagged structures
+
+Check for non-intersection of the union types in traversal.hl.rkt, using the non-intersection implementation from phc-adt.
+
+to infer the type for curry, check using identifier-binding if the id is imported, if so try to print its type using eval
+
+:::::::::Backlog:
+
+Translate https://github.com/nanopass/nanopass-framework-scheme
+
+Translate https://github.com/akeep/scheme-to-c
+
+Formalise what well-typed means for typed-nanopass+graph means
+
+Formalise the semantics of typed-nanopass+graph programs (using redex?)
+
+Write memoir
+
+Proof that well-typed programs with the extensions translate to well-typed programs in plain TR, with the same semantics
+\ No newline at end of file
diff --git a/flexible-with-generalized-ctor.hl.rkt b/flexible-with-generalized-ctor.hl.rkt
@@ -0,0 +1,69 @@
+#lang type-expander/lang
+#|hyper-literate #:♦ #:no-auto-require (dotlambda/unhygienic
+ . type-expander/lang)
+
+♦chunk[<*>|#
+
+(provide builder-τ)
+
+(require racket/require
+ (for-syntax (subtract-in racket/base subtemplate/override)
+ racket/list
+ racket/function
+ subtemplate/override))
+
+(struct (T) Some ([f : T]))
+(struct (T) None ([f : T]))
+
+(define-type-expander BinaryTree
+ (syntax-parser
+ [(_ leafⱼ …)
+ ;; TODO: implement BinaryTree.
+ #'(List leafⱼ …)]))
+
+(define-type-expander builder-τ
+ (syntax-parser
+ [(_ n m)
+ #:with (Nᵢ …) (range n)
+ #:with (Mⱼ …) (range m)
+ #:with ((Kᵢⱼ …) …) (map (const (Kⱼ …)) (Nᵢ …))
+ #:with ((Xᵢⱼ …) …) (map (const (Xⱼ …)) (Nᵢ …))
+ #:with ((Nᵢⱼ …) …) (map (λ (ni) (map (const ni) (Xⱼ …))) (Nᵢ …))
+ (define Ns (Nᵢ …))
+ (define Ms (Mⱼ …))
+ ;(define/with-syntax exceptⱼ (remove Mⱼ Ns)) …
+ ; (define/with-syntax ((exceptᵢⱼ …) …)
+ ; (map (const (exceptⱼ …)) (Nᵢ …)))
+ (define/with-syntax (exceptᵢ …) ((remove Nᵢ Ns) …))
+ (define/with-syntax ((exceptᵢⱼ …) …)
+ ((map (const (remove Nᵢ Ns)) Ms) …))
+
+ #'(∀ ((?@ Kⱼ Xⱼ) …)
+ (→ (?@ Kⱼ Xⱼ) …
+ (BinaryTree
+ (U (Pairof Nᵢ
+ ;; If Kⱼ is Nᵢ, then {∩ Kᵢⱼ {U . exceptᵢⱼ}} will
+ ;; Nothing. We multiply the Nothing together by
+ ;; building a List out of them (a single occurrence
+ ;; of Nothing should collapse the list), so that the
+ ;; result should be Nothing only if there is no Kⱼ
+ ;; equal to Nᵢ. To force TR to propagate Nothing as
+ ;; much as possible, we intersect it with
+ ;; (None Any), which should be a no-op, but makes
+ ;; sure the simplifier which runs with ∩ kicks in.
+ ;; Therefore, the (None whatever) should appear only
+ ;; if there is indeed no key provided for that leaf.
+ (∩ (None (List {∩ Kᵢⱼ {U . exceptᵢⱼ}} …))
+ (None Any)))
+ (∩ (Pairof Kᵢⱼ (Some Xᵢⱼ))
+ (Pairof Nᵢⱼ Any))
+ …)
+ …)))]))
+
+; ../../../.racket/snapshot/pkgs/typed-racket-lib/typed-racket/types/overlap.rkt:40:0: mask-accessor: contract violation
+; expected: mask?
+; given: #f
+(define-type τ-4-2 (builder-τ 4 2))
+
+;]
+
diff --git a/flexible-with2.hl.rkt b/flexible-with2.hl.rkt
@@ -0,0 +1,392 @@
+#lang hyper-literate #:♦ (dotlambda/unhygienic . type-expander/lang)
+
+♦title[#:style manual-doc-style ;#:style (with-html5 manual-doc-style)
+ #:tag "flexible-with"
+ #:tag-prefix "phc-graph/flexible-with"]{Flexible functional
+ modification and extension of records}
+
+♦(chunks-toc-prefix
+ '("(lib phc-graph/scribblings/phc-graph-implementation.scrbl)"
+ "phc-graph/flexible-with"))
+
+♦section{Goals}
+
+Our goal here is to have strongly typed records, with row polymorphism (a
+♦racket[Rest] row type variable can range over multiple possibly-present
+fields), and structural type equivalence (two record types are identical if
+they have the same fields, and these fields have the same types).
+
+♦section{Overview}
+
+We represent flexible records using a tree, where the leaves are field values.
+Every field which occurs anywhere in the program is assigned a constant index.
+This index determines which leaf is used to store that field's values. In
+order to avoid storing a huge tree for every tree-record, the actual fields
+are captured by a closure, and the tree is lazily generated (node by node)
+upon access.
+
+The type for a flexible record can support row polymorphism: the type of
+fields which may optionally be present are represented by a polymorphic type
+variable. Note that this means that no only one row type variable is used, but
+several. We define below facilities to automatically generate this list of
+polymorphic type variables. In order to avoid having a huge number of type
+variables, a branch containing only optional fields can be collapsed into a
+single type variable. An exception to this rule is when a field needs to be
+added by the user code in the middle of a branch: in this case the branch may
+not be collapsed.
+
+♦section{Type of a tree-record, with a hole}
+
+♦CHUNK[<tree-type-with-replacement>
+ (define-for-syntax (tree-type-with-replacement n last τ*)
+ (define-values (next mod) (quotient/remainder n 2))
+ (cond [(null? τ*) last]
+ [(= mod 0)
+ (tree-type-with-replacement next
+ #`(Pairof #,last #,(car τ*))
+ (cdr τ*))]
+ [else
+ (tree-type-with-replacement next
+ #`(Pairof #,(car τ*) #,last)
+ (cdr τ*))]))]
+
+♦section{Functionally updating a tree-record}
+
+♦subsection{Adding and modifying fields}
+
+Since we only deal with functional updates of immutable records, modifying a
+field does little more than discarding the old value, and injecting the new
+value instead into the new, updated record.
+
+Adding a new field is done using the same exact operation: missing fields are
+denoted by a special value, ♦racket['NONE], while present fields are
+represented as instances of the polymorphic struct ♦racket[(Some T)]. Adding a
+new field is therefore as simple as discarding the old ♦racket['NONE] marker,
+and replacing it with the new value, wrapped with ♦racket[Some]. A field
+update would instead discard the old instance of ♦racket[Some], and replace it
+with a new one.
+
+♦CHUNK[<make-replace-in-tree-body>
+ (if (= i 1)
+ #'(delay/pure/stateless replacement)
+ (let* ([bits (to-bits i)]
+ [next (from-bits (cons #t (cddr bits)))]
+ [mod (cadr bits)])
+ (define/with-syntax next-id (vector-ref low-names (sub1 next)))
+ (if mod
+ #`(replace-right (inst next-id #,@τ*-limited+T-next)
+ tree-thunk
+ replacement)
+ #`(replace-left (inst next-id #,@τ*-limited+T-next)
+ tree-thunk
+ replacement))))]
+
+♦CHUNK[<define-replace-in-tree>
+ (: replace-right (∀ (A B C R) (→ (→ (Promise B) R (Promise C))
+ (Promise (Pairof A B))
+ R
+ (Promise (Pairof A C)))))
+ (define-pure/stateless
+ #:∀ (A B C R)
+ (replace-right [next-id : (→ (Promise B) R (Promise C))]
+ [tree-thunk : (Promise (Pairof A B))]
+ [replacement : R])
+ (delay/pure/stateless
+ (let ([tree (force tree-thunk)])
+ (let ([left-subtree (car tree)]
+ [right-subtree (cdr tree)])
+ (cons left-subtree
+ (force (next-id (delay/pure/stateless right-subtree)
+ replacement)))))))
+ (: replace-left (∀ (A B C R) (→ (→ (Promise A) R (Promise C))
+ (Promise (Pairof A B))
+ R
+ (Promise (Pairof C B)))))
+ (define-pure/stateless
+ #:∀ (A B C R)
+ (replace-left [next-id : (→ (Promise A) R (Promise C))]
+ [tree-thunk : (Promise (Pairof A B))]
+ [replacement : R])
+ (delay/pure/stateless
+ (let ([tree (force tree-thunk)])
+ (let ([left-subtree (car tree)]
+ [right-subtree (cdr tree)])
+ (cons (force (next-id (delay/pure/stateless left-subtree)
+ replacement))
+ right-subtree)))))
+
+ (define-for-syntax (define-replace-in-tree low-names names rm-names τ* i depth)
+ (define/with-syntax name (vector-ref names (sub1 i)))
+ (define/with-syntax rm-name (vector-ref rm-names (sub1 i)))
+ (define/with-syntax low-name (vector-ref low-names (sub1 i)))
+ (define/with-syntax tree-type-with-replacement-name (gensym 'tree-type-with-replacement))
+ (define/with-syntax tree-replacement-type-name (gensym 'tree-replacement-type))
+ (define τ*-limited (take τ* depth))
+ (define τ*-limited+T-next (if (= depth 0)
+ (list #'T)
+ (append (take τ* (sub1 depth)) (list #'T))))
+ #`(begin
+ (provide name rm-name)
+ (define-type (tree-type-with-replacement-name #,@τ*-limited T)
+ (Promise #,(tree-type-with-replacement i #'T τ*-limited)))
+
+ (: low-name
+ (∀ (#,@τ*-limited T)
+ (→ (tree-type-with-replacement-name #,@τ*-limited Any)
+ T
+ (tree-type-with-replacement-name #,@τ*-limited T))))
+ (define-pure/stateless
+ #:∀ (#,@τ*-limited T)
+ (low-name [tree-thunk : (tree-type-with-replacement-name #,@τ*-limited Any)]
+ [replacement : T])
+ : (Promise #,(tree-type-with-replacement i #'T τ*-limited))
+ #,<make-replace-in-tree-body>)
+
+ (: name
+ (∀ (#,@τ*-limited T)
+ (→ (tree-type-with-replacement-name #,@τ*-limited Any)
+ T
+ (tree-type-with-replacement-name #,@τ*-limited (Some T)))))
+ (define (name tree-thunk replacement)
+ (low-name tree-thunk (Some replacement)))
+
+ (: rm-name
+ (∀ (#,@τ*-limited)
+ (→ (tree-type-with-replacement-name #,@τ*-limited (Some Any))
+ (tree-type-with-replacement-name #,@τ*-limited 'NONE))))
+ (define (rm-name tree-thunk)
+ (low-name tree-thunk 'NONE))))]
+
+♦section{Auxiliary values}
+
+The following sections reuse a few values which are derived from the list of
+fields:
+
+♦CHUNK[<utils>
+ (define all-fields #'(field …))
+ (define depth-above (ceiling-log2 (length (syntax->list #'(field …)))))
+ (define offset (expt 2 depth-above))
+ (define i*-above (range 1 (expt 2 depth-above)))
+ (define names (list->vector
+ (append (map (λ (i) (format-id #'here "-with-~a" i))
+ i*-above)
+ (stx-map (λ (f) (format-id f "with-~a" f))
+ #'(field …)))))
+ (define rm-names (list->vector
+ (append (map (λ (i) (format-id #'here "-without-~a" i))
+ i*-above)
+ (stx-map (λ (f) (format-id f "without-~a" f))
+ #'(field …)))))
+ (define low-names (list->vector
+ (append (map (λ (i) (format-id #'here "-u-with-~a" i))
+ i*-above)
+ (stx-map (λ (f) (format-id f "u-with-~a" f))
+ #'(field …)))))]
+
+♦section{Type of a tree-record}
+
+♦CHUNK[<τ-tree-with-fields>
+ (define-for-syntax (τ-tree-with-fields struct-fields fields)
+ (define/with-syntax (struct-field …) struct-fields)
+ (define/with-syntax (field …) fields)
+ <utils>
+ ;; Like in convert-from-struct
+ (define lookup
+ (make-free-id-table
+ (for/list ([n (in-syntax all-fields)]
+ [i (in-naturals)])
+ (cons n (+ i offset)))))
+ (define fields+indices
+ (sort (stx-map λ.(cons % (free-id-table-ref lookup %))
+ #'(struct-field …))
+ <
+ #:key cdr))
+
+ (define up (* offset 2))
+
+ ;; Like in convert-fields, but with Pairof
+ (define (f i)
+ ;(displayln (list i '/ up (syntax->datum #`#,fields+indices)))
+ (if (and (pair? fields+indices) (= i (cdar fields+indices)))
+ (begin0
+ `(Some ,(caar fields+indices))
+ (set! fields+indices (cdr fields+indices)))
+ (if (>= (* i 2) up) ;; DEPTH
+ ''NONE
+ (begin
+ `(Pairof ,(f (* i 2))
+ ,(f (add1 (* i 2))))))))
+ (f 1))]
+
+♦section{Conversion to and from record-trees}
+
+♦CHUNK[<define-struct↔tree>
+ (define-for-syntax (define-struct↔tree
+ offset all-fields τ* struct-name fields)
+ (define/with-syntax (field …) fields)
+ (define/with-syntax fields→tree-name
+ (format-id struct-name "~a→tree" struct-name))
+ (define/with-syntax tree→fields-name
+ (format-id struct-name "tree→~a" struct-name))
+ (define lookup
+ (make-free-id-table
+ (for/list ([n (in-syntax all-fields)]
+ [i (in-naturals)])
+ (cons n (+ i offset)))))
+ (define fields+indices
+ (sort (stx-map λ.(cons % (free-id-table-ref lookup %))
+ fields)
+ <
+ #:key cdr))
+ #`(begin
+ (: fields→tree-name (∀ (field …)
+ (→ field …
+ (Promise #,(τ-tree-with-fields #'(field …)
+ all-fields)))))
+ (define (fields→tree-name field …)
+ (delay/pure/stateless
+ #,(convert-fields (* offset 2) fields+indices)))
+
+ (: tree→fields-name (∀ (field …)
+ (→ (Promise #,(τ-tree-with-fields #'(field …)
+ all-fields))
+ (Values field …))))
+ (define (tree→fields-name tree-thunk)
+ (define tree (force tree-thunk))
+ #,(convert-back-fields (* offset 2) fields+indices))))]
+
+♦subsection{Creating a new tree-record}
+
+♦CHUNK[<convert-fields>
+ (define-for-syntax (convert-fields up fields+indices)
+ ;(displayln fields+indices)
+ (define (f i)
+ ;(displayln (list i '/ up (syntax->datum #`#,fields+indices)))
+ (if (and (pair? fields+indices) (= i (cdar fields+indices)))
+ (begin0
+ `(Some ,(caar fields+indices))
+ (set! fields+indices (cdr fields+indices)))
+ (if (>= (* i 2) up) ;; DEPTH
+ ''NONE
+ `(cons ,(f (* i 2))
+ ,(f (add1 (* i 2)))))))
+ ;(displayln (syntax->datum #`#,(f 1)))
+ (f 1))]
+
+
+♦subsection{Extracting all the fields from a tree-record}
+
+We traverse the tree in preorder, and accumulate definitions naming the
+interesting subparts of the trees (those where there are fields).
+
+♦CHUNK[<convert-back-fields>
+ (define-for-syntax (convert-back-fields up fields+indices)
+ (define result '())
+ (define definitions '())
+ (define (f i t)
+ (if (and (pair? fields+indices) (= i (cdar fields+indices)))
+ (begin0
+ (begin
+ (set! result (cons #`(Some-v #,t) result))
+ #t)
+ (set! fields+indices (cdr fields+indices)))
+ (if (>= (* i 2) up) ;; DEPTH
+ #f
+ (let* ([left-t (string->symbol
+ (format "subtree-~a" (* i 2)))]
+ [right-t (string->symbol
+ (format "subtree-~a" (add1 (* i 2))))]
+ [left (f (* i 2) left-t)]
+ [right (f (add1 (* i 2)) right-t)])
+ (cond
+ [(and left right)
+ (set! definitions (cons #`(define #,left-t (car #,t))
+ definitions))
+ (set! definitions (cons #`(define #,right-t (cdr #,t))
+ definitions))
+ #t]
+ [left
+ (set! definitions (cons #`(define #,left-t (car #,t))
+ definitions))
+ #t]
+ [right
+ (set! definitions (cons #`(define #,right-t (cdr #,t))
+ definitions))
+ #t]
+ [else
+ #f])))))
+ (f 1 #'tree)
+ #`(begin #,@definitions (values . #,(reverse result))))]
+
+♦section{Defining the converters and accessors for each known record type}
+
+♦CHUNK[<define-trees>
+ (define-for-syntax (define-trees stx)
+ (syntax-case stx ()
+ [(bt-fields-id (field …) [struct struct-field …] …)
+ (let ()
+ <utils>
+ (define ∀-types (map λ.(format-id #'here "τ~a" %)
+ (range (add1 depth-above))))
+ (define total-nb-functions (vector-length names))
+ <define-trees-result>)]))]
+
+♦CHUNK[<bt-fields-type>
+ (define-for-syntax (bt-fields-type fields)
+ (λ (stx)
+ (syntax-case stx ()
+ [(_ . fs)
+ #`(∀ fs (Promise #,(τ-tree-with-fields #'fs
+ fields)))])))]
+
+♦CHUNK[<define-trees-result>
+ #`(begin
+ (define-type-expander bt-fields-id
+ (bt-fields-type #'#,(syntax-local-introduce #'(field …))))
+ #,@(map λ.(define-replace-in-tree low-names
+ names rm-names ∀-types % (floor-log2 %))
+ (range 1 (add1 total-nb-functions)))
+ #;#,@(map λ.(define-remove-in-tree rm-names ∀-types % (floor-log2 %))
+ (range 1 (add1 total-nb-functions)))
+ #,@(map λ.(define-struct↔tree
+ offset all-fields ∀-types %1 %2)
+ (syntax->list #'(struct …))
+ (syntax->list #'([struct-field …] …))))]
+
+♦subsection{Putting it all together}
+
+♦chunk[<maybe>
+ (struct (T) Some ([v : T]) #:transparent)
+ (define-type (Maybe T) (U (Some T) 'NONE))]
+
+♦chunk[<*>
+ (require delay-pure
+ "flexible-with-utils.hl.rkt"
+ (for-syntax (rename-in racket/base [... …])
+ syntax/stx
+ racket/syntax
+ racket/list
+ syntax/id-table
+ racket/sequence)
+ (for-meta 2 racket/base))
+
+ (provide (for-syntax define-trees)
+ ;; For tests:
+ (struct-out Some)
+
+ ;;DEBUG:
+ (for-syntax τ-tree-with-fields)
+ )
+
+ <maybe>
+ <tree-type-with-replacement>
+ <define-replace-in-tree>
+ ;<define-remove-in-tree>
+ <convert-fields>
+ <convert-back-fields>
+ <τ-tree-with-fields>
+ <define-struct↔tree>
+ <define-trees>
+ <bt-fields-type>]
+
+♦include-section[(submod "flexible-with-utils.hl.rkt" doc)]
+\ No newline at end of file
diff --git a/info.rkt b/info.rkt
@@ -24,7 +24,8 @@
"remember"
"typed-racket-doc"
"aful"
- "scribble-math"))
+ "scribble-math"
+ "at-exp-lib"))
(define scribblings
'(("scribblings/phc-graph.scrbl" ()
("Data Structures"))
diff --git a/main-draft.hl.rkt b/main-draft.hl.rkt
@@ -37,6 +37,8 @@
<polymorphic-node-types-and-mappings>
;<general-purpose-graph-algorithms>
;<garbage-collection>
+
+
|<phase~1: call mappings and extract placeholders>|
]))]
diff --git a/make-lang-example.rkt b/make-lang-example.rkt
@@ -0,0 +1,3 @@
+#lang phc-graph/make-lang
+
+#:require (type-expander/lang phc-toolkit)
+\ No newline at end of file
diff --git a/make-lang-use-example.rkt b/make-lang-use-example.rkt
@@ -0,0 +1,5 @@
+#lang phc-graph/make-lang-example
+(let ()
+ (ann 1 Number) ;; from type-expander/lang
+ (ann (∘ add1 sub1) (-> Number Number)) ;; From phc-toolkit
+ (void))
+\ No newline at end of file
diff --git a/make-lang.rkt b/make-lang.rkt
@@ -0,0 +1,46 @@
+#lang at-exp racket/base
+
+(module reader syntax/module-reader
+ phc-graph/make-lang)
+
+(provide (rename-out [-#%module-begin #%module-begin]))
+
+(require (for-syntax racket/base
+ setup/collects)
+ scribble/manual)
+
+(define-syntax (-#%module-begin stx)
+ (syntax-case stx ()
+ [(self #:require req)
+ ;; TODO: isn't there a more reliable way to get the "require path"
+ ;; for the source module of #'self ?
+ (let* ([src (syntax-source #'self)]
+ [modpath (path->module-path src)]
+ [md (if (and (pair? modpath)
+ (eq? (car modpath) 'lib)
+ (string? (cadr modpath))
+ (null? (cddr modpath))
+ (regexp-match ".rkt$" (cadr modpath)))
+ (string->symbol
+ (substring (cadr modpath)
+ 0
+ (- (string-length (cadr modpath)) 4)))
+ modpath)])
+ #`(-#%module-begin #:module #,md #:require req))]
+ [(_ #:module md ;; TODO: detect this automatically
+ #:require (req ...))
+ #`(#%module-begin
+ (module reader syntax/module-reader
+ md)
+ @module[scrbl racket/base (require scribble/manual)]{
+ @defmodule[md]{
+ This module language re-provides the following modules:
+ @itemlist[(item (racketmodname req)) ...]
+ }
+ }
+ (module doc racket/base
+ (require (submod ".." scrbl))
+ (provide (all-from-out (submod ".." scrbl))))
+ (require req ...)
+ (provide (all-from-out req ...)))]))
+
