diff --git a/.travis.yml b/.travis.yml index e65885f..563e7c1 100644 --- 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 new file mode 100644 index 0000000..154cba7 --- /dev/null +++ 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 new file mode 100644 index 0000000..6563933 --- /dev/null +++ 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 new file mode 100644 index 0000000..3976f31 --- /dev/null +++ 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[ + (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[ + (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[ + (: 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)) + #,) + + (: 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[ + (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) + + ;; 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-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[ + (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[ + (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-for-syntax (define-trees stx) + (syntax-case stx () + [(bt-fields-id (field …) [struct struct-field …] …) + (let () + + (define ∀-types (map λ.(format-id #'here "τ~a" %) + (range (add1 depth-above)))) + (define total-nb-functions (vector-length names)) + )]))] + +♦CHUNK[ + (define-for-syntax (bt-fields-type fields) + (λ (stx) + (syntax-case stx () + [(_ . fs) + #`(∀ fs (Promise #,(τ-tree-with-fields #'fs + fields)))])))] + +♦CHUNK[ + #`(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[ + (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) + ) + + + + + ; + + + <τ-tree-with-fields> + + + ] + +♦include-section[(submod "flexible-with-utils.hl.rkt" doc)] \ No newline at end of file diff --git a/info.rkt b/info.rkt index c190ec0..b8a96e6 100644 --- 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 index 65bad4e..e096a34 100644 --- a/main-draft.hl.rkt +++ b/main-draft.hl.rkt @@ -37,6 +37,8 @@ ; ; + + || ]))] diff --git a/make-lang-example.rkt b/make-lang-example.rkt new file mode 100644 index 0000000..3fb94a1 --- /dev/null +++ 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 new file mode 100644 index 0000000..18c6b07 --- /dev/null +++ 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 new file mode 100644 index 0000000..abbab26 --- /dev/null +++ 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 ...)))])) +