Compiles and typecheck, but the queues need two lists to be implemented (for now they are stacks).
This commit is contained in:
parent
80a056791d
commit
04ddaf308c
18
graph/graph/_experiment_queues_without_list.rkt
Normal file
18
graph/graph/_experiment_queues_without_list.rkt
Normal file
|
@ -0,0 +1,18 @@
|
||||||
|
#lang typed/racket
|
||||||
|
|
||||||
|
#|
|
||||||
|
(let ([res-zero '()]
|
||||||
|
[res-one '()]
|
||||||
|
[res-two '()]
|
||||||
|
|#
|
||||||
|
|
||||||
|
(define (process-zero v res-zero)
|
||||||
|
(cons v res-zero))
|
||||||
|
|
||||||
|
(define (enqueue [v : Integer])
|
||||||
|
(let ([name : (U 'zero 'one 'two) (cond [(= (modulo v 3) 0) 'zero]
|
||||||
|
[(= (modulo v 3) 1) 'one]
|
||||||
|
[else 'two])])
|
||||||
|
(cond [(eq? name 'zero) ]
|
||||||
|
[(eq? name 'one) ]
|
||||||
|
[(eq? name 'two) ])))
|
|
@ -15,48 +15,219 @@
|
||||||
[(name [element (~literal :) Element-Type]
|
[(name [element (~literal :) Element-Type]
|
||||||
[Δ-queues (~literal :) Δ-Queues-Type-Name]
|
[Δ-queues (~literal :) Δ-Queues-Type-Name]
|
||||||
enqueue)
|
enqueue)
|
||||||
(~literal :) result-type
|
(~literal :) Result-Type
|
||||||
. body]
|
. body]
|
||||||
...)]
|
…
|
||||||
|
(~parse (root-name . _) #'(name …)))]
|
||||||
|
|
||||||
@chunk[<define-enqueue-type>
|
@chunk[<enqueue-type>
|
||||||
(define/with-syntax enqueue/type
|
(case→ (→ 'name
|
||||||
#'(case→ (→ 'name
|
|
||||||
Element-Type
|
Element-Type
|
||||||
Δ-Queues-Type-Name
|
Δ-Queues-Type-Name
|
||||||
(values Index
|
(values Index
|
||||||
Δ-Queues-Type-Name))
|
Δ-Queues-Type-Name))
|
||||||
…))]
|
…)]
|
||||||
|
|
||||||
@chunk[<define-Δ-queues-type>
|
@chunk[<define-queues-type___>
|
||||||
(define/with-syntax Δ-queues/type
|
(define/with-syntax queues-type
|
||||||
#'(List (Δ-Hash Element-Type Index) ...))]
|
#'(List (Δ-Hash Element-Type Index) …))]
|
||||||
|
|
||||||
@chunk[<λ-type>
|
@chunk[<define-ids>
|
||||||
|
(define-temp-ids "~a/process-element" (name …))
|
||||||
|
(define-temp-ids "~a/Δ-results-add" (name …))]
|
||||||
|
|
||||||
|
@chunk[<process-element-type>
|
||||||
(∀ (Δ-Queues-Type-Name)
|
(∀ (Δ-Queues-Type-Name)
|
||||||
(→ Element-Type
|
(→ Element-Type
|
||||||
Δ-Queues-Type-Name
|
Δ-Queues-Type-Name
|
||||||
enqueue/type
|
<enqueue-type>
|
||||||
(values result-type
|
(values Result-Type
|
||||||
Δ-Queues-Type-Name)))]
|
Δ-Queues-Type-Name)))]
|
||||||
|
|
||||||
@chunk[<fold-queue-multi-sets-immutable-tags>
|
@chunk[<fold-queue-multi-sets-immutable-tags>
|
||||||
(define-syntax/parse <fold-queues-signature>
|
(define-syntax/parse <fold-queues-signature>
|
||||||
<define-enqueue-type>
|
;<define-queues-type>
|
||||||
<define-Δ-queues-type>
|
<define-ids>
|
||||||
#'(begin
|
((λ (x) (pretty-write (syntax->datum x)) x)
|
||||||
(list (ann (λ (element Δ-queues enqueue)
|
#'(let ()
|
||||||
. body)
|
(begin
|
||||||
<λ-type>)
|
(: name/process-element <process-element-type>)
|
||||||
...)
|
(define (name/process-element element Δ-queues enqueue) . body))
|
||||||
((ann (λ _ (error "Not implemented yet"))
|
…
|
||||||
(→ (List (Vectorof result-type) …))))))]
|
<Δ-hash2-definitions>
|
||||||
|
<Δ-results-definitions>
|
||||||
|
<process-queues>
|
||||||
|
;((ann (λ _ (error "fold-queues: Not implemented yet"))
|
||||||
|
; (→ (List (Vectorof Result-Type) …))))
|
||||||
|
)))]
|
||||||
|
|
||||||
|
@subsection{Representation of the queues}
|
||||||
|
|
||||||
|
@;Each queue will be represented as a hash table associating
|
||||||
|
|
||||||
|
In order to have the indices in the right order, without having to sort the
|
||||||
|
result, the queues have to be simple lists.
|
||||||
|
|
||||||
|
However, the @tc[enqueue] function needs to detect duplicate elements, so it
|
||||||
|
needs the @tc[(HashTable Element-Type Index)].
|
||||||
|
|
||||||
|
We shall use both representation for the queues, adding a third integer value
|
||||||
|
which tracks the length of the list (i.e. the first unallocated result index):
|
||||||
|
|
||||||
|
@chunk[<Δ-hash2-definitions>
|
||||||
|
<Δ-hash2-type>
|
||||||
|
<Δ-hash2-empty>
|
||||||
|
<Δ-hash2-enqueue>
|
||||||
|
<Δ-hash2-dequeue>]
|
||||||
|
|
||||||
|
@chunk[<Δ-hash2-queue-type>
|
||||||
|
(List (HashTable Element-Type Index)
|
||||||
|
(Listof Element-Type)
|
||||||
|
Index)]
|
||||||
|
|
||||||
|
@chunk[<Δ-hash2-type>
|
||||||
|
(define-type Δ-hash2-type (List <Δ-hash2-queue-type> …))]
|
||||||
|
|
||||||
|
@subsubsection{Notes on parallelism}
|
||||||
|
|
||||||
|
For parallelism, we can later change the signature of @tc[fold-queues], and say
|
||||||
|
we return a @tc[(Vectorof (Vectorof Result-Type))], with one vector for each
|
||||||
|
core. The tags will then be a pair of integers (or use modulo, and interleave
|
||||||
|
the queues). We should, for forward planning, make the index type and the result
|
||||||
|
database type opaque, and use an accessor with signature
|
||||||
|
@tc[(→ Opaque-Database Opaque-Index Result-Type)].
|
||||||
|
|
||||||
|
@subsubsection{Adding elements to the queues}
|
||||||
|
|
||||||
|
@chunk[<Δ-hash2-enqueue>
|
||||||
|
(: Δ-hash2-enqueue (case→ (→ 'name
|
||||||
|
Element-Type
|
||||||
|
Δ-hash2-type
|
||||||
|
(values Index
|
||||||
|
Δ-hash2-type))
|
||||||
|
…))
|
||||||
|
(define (Δ-hash2-enqueue selector elt qs)
|
||||||
|
(match-let ([(list name/queue …) qs])
|
||||||
|
(cond [(eq? selector 'name)
|
||||||
|
(if (hash-has-key? (car name/queue) elt)
|
||||||
|
(values (hash-ref (car name/queue) elt)
|
||||||
|
qs)
|
||||||
|
(match-let ([(list h l i) name/queue])
|
||||||
|
(let* ([new-h (hash-set h elt i)]
|
||||||
|
[new-l (cons elt l)] ;; whoops, should append, not cons!
|
||||||
|
[new-i (+ i 1)]
|
||||||
|
[new-i-index (if (index? new-i)
|
||||||
|
new-i
|
||||||
|
(error "Too many elements"))]
|
||||||
|
[name/queue (list new-h new-l new-i-index)])
|
||||||
|
(values i
|
||||||
|
(list name/queue …)))))]
|
||||||
|
…)))]
|
||||||
|
|
||||||
|
@subsubsection{Popping elements from the queues}
|
||||||
|
|
||||||
|
@chunk[<Δ-hash2-dequeue>
|
||||||
|
(: Δ-hash2-dequeue (case→ (→ (List (HashTable Element-Type Index)
|
||||||
|
(Pairof Element-Type
|
||||||
|
(Listof Element-Type))
|
||||||
|
Index)
|
||||||
|
(values Element-Type
|
||||||
|
<Δ-hash2-queue-type>))
|
||||||
|
…))
|
||||||
|
(define (Δ-hash2-dequeue q)
|
||||||
|
(match-let* ([(list h (cons e rest-l) i) q])
|
||||||
|
(values e
|
||||||
|
(list h rest-l (assert (- i 1) index?)))))]
|
||||||
|
|
||||||
|
@subsubsection{Constructor for the queues}
|
||||||
|
|
||||||
|
@chunk[<Δ-hash2-empty>
|
||||||
|
(define Δ-hash2-empty
|
||||||
|
(list (list ((inst hash Element-Type Index)) '() 0)
|
||||||
|
…))]
|
||||||
|
|
||||||
|
@subsection{Result lists}
|
||||||
|
|
||||||
|
We accumulate results in lists, one per queue. Since the elements are processed
|
||||||
|
in the order in which they are added, the result lists contain them in reverse
|
||||||
|
order: the element at position @${i} in a list is associated with the index
|
||||||
|
@${n-i} in the hash table, where @${n} is the number of elements processed so
|
||||||
|
far for that queue.
|
||||||
|
|
||||||
|
The datatype is defined as follows:
|
||||||
|
|
||||||
|
@chunk[<Δ-results-definitions>
|
||||||
|
<Δ-results-type>
|
||||||
|
<Δ-results-add>
|
||||||
|
<Δ-results-empty>
|
||||||
|
<Δ-results-to-vectors>]
|
||||||
|
|
||||||
|
@chunk[<Δ-results-type>
|
||||||
|
(define-type Δ-results-type (List (Listof Result-Type) …))]
|
||||||
|
|
||||||
|
We have a constructor for empty lists of results:
|
||||||
|
|
||||||
|
@chunk[<Δ-results-empty>
|
||||||
|
(define Δ-results-empty (list (ann '() (Listof Result-Type)) …))]
|
||||||
|
|
||||||
|
And an operation to add a new result, for each queue name:
|
||||||
|
|
||||||
|
@chunk[<Δ-results-add>
|
||||||
|
(begin
|
||||||
|
(: name/Δ-results-add (→ Δ-results-type Result-Type Δ-results-type))
|
||||||
|
(define (name/Δ-results-add Δ-results value)
|
||||||
|
(match-let ([(list name/queue …) Δ-results])
|
||||||
|
(let ([name/queue (cons value name/queue)]) ;; to shadow name/queue
|
||||||
|
(list name/queue …)))))
|
||||||
|
…]
|
||||||
|
|
||||||
|
Finally, we will need to return a list of vectors, with each element having its
|
||||||
|
position in the vector equal to the index associated to it in the hash table:
|
||||||
|
|
||||||
|
@chunk[<Δ-results-to-vectors>
|
||||||
|
(: Δ-results-to-vectors (→ Δ-results-type
|
||||||
|
(List (Vectorof Result-Type) …)))
|
||||||
|
(define (Δ-results-to-vectors Δ-results)
|
||||||
|
(match-let ([(list name/queue …) (ann Δ-results (List (Listof Result-Type) …))])
|
||||||
|
(list (vector->immutable-vector
|
||||||
|
(ann (list->vector name/queue)
|
||||||
|
(Vectorof Result-Type)))
|
||||||
|
…)))]
|
||||||
|
|
||||||
|
@subsection{Processing the queues}
|
||||||
|
|
||||||
|
@chunk[<define-ids>
|
||||||
|
(define-temp-ids "~a/queue" (name …))]
|
||||||
|
|
||||||
|
@chunk[<process-queues>
|
||||||
|
(define (process-queues [queues : Δ-hash2-type]
|
||||||
|
[results : Δ-results-type])
|
||||||
|
: (List (Vectorof Result-Type) …)
|
||||||
|
(match-let ([(list name/queue …) queues])
|
||||||
|
(cond [(not (empty? (cadr name/queue)))
|
||||||
|
<process-queue>]
|
||||||
|
…
|
||||||
|
[else (Δ-results-to-vectors results)])))
|
||||||
|
|
||||||
|
#;(process-queues (list ((inst empty-Δ-hash Element-Type Index)) …))
|
||||||
|
(% index Δ-hash = (Δ-hash2-enqueue 'root-name root-value Δ-hash2-empty)
|
||||||
|
(process-queues Δ-hash Δ-results-empty))]
|
||||||
|
|
||||||
|
@chunk[<process-queue>
|
||||||
|
(% e name/queue = (Δ-hash2-dequeue name/queue) ;; to hide name/queue
|
||||||
|
result new-Δ-queues = (name/process-element e
|
||||||
|
(list name/queue …)
|
||||||
|
Δ-hash2-enqueue)
|
||||||
|
(process-queues new-Δ-queues (name/Δ-results-add results result)))]
|
||||||
|
|
||||||
|
@subsection{Δ-Hash}
|
||||||
|
|
||||||
@tc[Δ-Hash] is a type encapsulating both a hash, and a set of key-value pairs
|
@tc[Δ-Hash] is a type encapsulating both a hash, and a set of key-value pairs
|
||||||
added to the @tc[Δ-Hash] since its creation from a simple @tc[HashTable].
|
added to the @tc[Δ-Hash] since its creation from a simple @tc[HashTable].
|
||||||
|
|
||||||
@chunk[<Δ-hash>
|
@chunk[<Δ-hash>
|
||||||
|
(module Δ-hash typed/racket
|
||||||
|
(require "../lib/low.rkt")
|
||||||
(define-type (Δ-Hash A B)
|
(define-type (Δ-Hash A B)
|
||||||
(Pairof (HashTable A B)
|
(Pairof (HashTable A B)
|
||||||
(Setof (Pairof A B))))
|
(Setof (Pairof A B))))
|
||||||
|
@ -69,13 +240,37 @@ added to the @tc[Δ-Hash] since its creation from a simple @tc[HashTable].
|
||||||
(define (Δ-hash h)
|
(define (Δ-hash h)
|
||||||
(cons h ((inst set (Pairof K V)))))
|
(cons h ((inst set (Pairof K V)))))
|
||||||
|
|
||||||
(: Δ-hash-add (∀ (K V) (→ (Δ-Hash K V) K V
|
(: Δ-hash-add (∀ (K V Acc) (→ (Δ-Hash K V)
|
||||||
(Δ-Hash K V))))
|
K
|
||||||
(define (Δ-hash-add dh k v)
|
Acc
|
||||||
(if (hash-has-key? (car dh) k)
|
(→ K Acc (values V Acc))
|
||||||
dh
|
(values (Δ-Hash K V)
|
||||||
(cons (hash-set (car dh) k v)
|
Acc))))
|
||||||
(set-add (cdr dh) (cons k v)))))]
|
(define (Δ-hash-add Δ-hash k acc make-v)
|
||||||
|
(if (hash-has-key? (car Δ-hash) k)
|
||||||
|
(values Δ-hash acc)
|
||||||
|
(% v new-acc = (make-v k acc)
|
||||||
|
(values (cons (hash-set (car Δ-hash) k v)
|
||||||
|
(set-add (cdr Δ-hash) (cons k v)))
|
||||||
|
new-acc))))
|
||||||
|
|
||||||
|
(: Δ-hash-get-Δ (∀ (K V) (→ (Δ-Hash K V) (Setof (Pairof K V)))))
|
||||||
|
(define (Δ-hash-get-Δ Δ-hash) (cdr Δ-hash)))]
|
||||||
|
|
||||||
|
@section{@racket{cond-let}}
|
||||||
|
|
||||||
|
@CHUNK[<cond-let>
|
||||||
|
(define-syntax (cond-let stx)
|
||||||
|
(syntax-parse stx
|
||||||
|
[(_)
|
||||||
|
#'(typecheck-fail #,stx)]
|
||||||
|
[(_ #:let bindings:expr clause …)
|
||||||
|
#'(let bindings (cond-let clause …))]
|
||||||
|
[(_ [condition:expr (~seq #:else-let binding …) … . body] clause …)
|
||||||
|
#'(if condition
|
||||||
|
(begin . body)
|
||||||
|
(let (binding … …)
|
||||||
|
(cond-let clause …)))]))]
|
||||||
|
|
||||||
@section{Conclusion}
|
@section{Conclusion}
|
||||||
|
|
||||||
|
@ -83,11 +278,13 @@ added to the @tc[Δ-Hash] since its creation from a simple @tc[HashTable].
|
||||||
(module main typed/racket
|
(module main typed/racket
|
||||||
(require (for-syntax syntax/parse
|
(require (for-syntax syntax/parse
|
||||||
racket/syntax
|
racket/syntax
|
||||||
|
racket/pretty; DEBUG
|
||||||
"../lib/low-untyped.rkt")
|
"../lib/low-untyped.rkt")
|
||||||
"../lib/low.rkt")
|
"../lib/low.rkt")
|
||||||
|
|
||||||
(provide fold-queues)
|
(provide fold-queues)
|
||||||
|
|
||||||
|
<cond-let>
|
||||||
<Δ-hash>
|
<Δ-hash>
|
||||||
<fold-queue-multi-sets-immutable-tags>)]
|
<fold-queue-multi-sets-immutable-tags>)]
|
||||||
|
|
||||||
|
|
|
@ -155,7 +155,7 @@ wrapper macros.
|
||||||
@chunk[<signature>
|
@chunk[<signature>
|
||||||
(make-graph ([node <field-signature> … <mapping-declaration>]
|
(make-graph ([node <field-signature> … <mapping-declaration>]
|
||||||
…)
|
…)
|
||||||
(root-expr:expr …))]
|
root-expr:expr …)]
|
||||||
|
|
||||||
Where @tc[<field-signature>] is:
|
Where @tc[<field-signature>] is:
|
||||||
|
|
||||||
|
@ -292,7 +292,7 @@ modified copy, in addition to the tag. The queue's processing body should return
|
||||||
two values: the result of processing the element, and the latest version of
|
two values: the result of processing the element, and the latest version of
|
||||||
@tc[Δ-queues], which stores the new elements to be added to the queue.
|
@tc[Δ-queues], which stores the new elements to be added to the queue.
|
||||||
|
|
||||||
@chunk[<fold-queue>
|
@chunk[<fold-queues>
|
||||||
(fold-queues <root-placeholder>
|
(fold-queues <root-placeholder>
|
||||||
[(node/placeholder-queue [e : <fold-queue-type-element>]
|
[(node/placeholder-queue [e : <fold-queue-type-element>]
|
||||||
[Δ-queues : Δ-Queues]
|
[Δ-queues : Δ-Queues]
|
||||||
|
@ -588,7 +588,7 @@ are replaced by tagged indices:
|
||||||
(begin <define-with-promises>) …
|
(begin <define-with-promises>) …
|
||||||
(begin <define-incomplete>) …
|
(begin <define-incomplete>) …
|
||||||
(begin <define-mapping-function>) …
|
(begin <define-mapping-function>) …
|
||||||
(let*-values ([(rs) <fold-queue>]
|
(let*-values ([(rs) <fold-queues>]
|
||||||
[(node/database rs)
|
[(node/database rs)
|
||||||
(values (ann (car rs)
|
(values (ann (car rs)
|
||||||
(Vectorof node/with-indices-type))
|
(Vectorof node/with-indices-type))
|
||||||
|
@ -660,6 +660,7 @@ are replaced by tagged indices:
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
(require (submod ".." doc)))]
|
(require (submod ".." doc)))]
|
||||||
|
|
Loading…
Reference in New Issue
Block a user