From d211bd115429deb37c49a2c7f1e3f191641727fc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Georges=20Dup=C3=A9ron?= Date: Sat, 20 May 2017 02:46:06 +0200 Subject: [PATCH] Put type within the use of define-pure/stateless --- flexible-with.hl.rkt | 83 ++++++++------- flexible-with2.hl.rkt | 116 +++++++++++++-------- scribblings/phc-graph-implementation.scrbl | 2 +- 3 files changed, 116 insertions(+), 85 deletions(-) diff --git a/flexible-with.hl.rkt b/flexible-with.hl.rkt index 39b4d00..10f120a 100644 --- a/flexible-with.hl.rkt +++ b/flexible-with.hl.rkt @@ -56,38 +56,40 @@ with a new one. 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))))) + (: replace-right (∀ (A B C R) (→ (→ (Promise B) R (Promise C)) + (Promise (Pairof A B)) + R + (Promise (Pairof A C))))) + (define + #:∀ (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)))))))) (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))))) + (: replace-left (∀ (A B C R) (→ (→ (Promise A) R (Promise C)) + (Promise (Pairof A B)) + R + (Promise (Pairof C B))))) + (define + #:∀ (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))) @@ -104,17 +106,18 @@ with a new one. (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)) - #,) + (: low-name + (∀ (#,@τ*-limited T) + (→ (tree-type-with-replacement-name #,@τ*-limited Any) + T + (tree-type-with-replacement-name #,@τ*-limited T)))) + (define + #:∀ (#,@τ*-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) diff --git a/flexible-with2.hl.rkt b/flexible-with2.hl.rkt index 3976f31..f137ed4 100644 --- a/flexible-with2.hl.rkt +++ b/flexible-with2.hl.rkt @@ -14,16 +14,17 @@ 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). +they have the same fields and the type of the fields is the same in both record +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. +order to avoid storing in-memory a huge tree for every 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 @@ -35,6 +36,30 @@ 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[ @@ -82,38 +107,40 @@ with a new one. 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))))) + (: replace-right (∀ (A B C R) (→ (→ (Promise B) R (Promise C)) + (Promise (Pairof A B)) + R + (Promise (Pairof A C))))) + (define + #:∀ (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)))))))) (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 + (: replace-left (∀ (A B C R) (→ (→ (Promise A) R (Promise C)) + (Promise (Pairof A B)) + R + (Promise (Pairof C B))))) + #:∀ (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))) @@ -130,17 +157,18 @@ with a new one. (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)) - #,) + (: low-name + (∀ (#,@τ*-limited T) + (→ (tree-type-with-replacement-name #,@τ*-limited Any) + T + (tree-type-with-replacement-name #,@τ*-limited T)))) + (define + #:∀ (#,@τ*-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) diff --git a/scribblings/phc-graph-implementation.scrbl b/scribblings/phc-graph-implementation.scrbl index 3c8e70e..6ed8bef 100644 --- a/scribblings/phc-graph-implementation.scrbl +++ b/scribblings/phc-graph-implementation.scrbl @@ -12,7 +12,7 @@ the @other-doc['(lib "phc-graph/scribblings/phc-graph.scrbl")] document. @(table-of-contents) @include-section[(submod "../traversal.hl.rkt" doc)] -@include-section[(submod "../flexible-with.hl.rkt" doc)] +@include-section[(submod "../flexible-with2.hl.rkt" doc)] @include-section[(submod "../invariants-phantom.hl.rkt" doc)] @include-section[(submod "../graph-info.hl.rkt" doc)] @include-section[(submod "../graph-type.hl.rkt" doc)]