Finished implementing FB case 86 (Graph: Multiple constructors).

This commit is contained in:
Georges Dupéron 2016-02-02 21:38:09 +01:00
parent 75210b1209
commit 4d911ef7d6
8 changed files with 161 additions and 137 deletions

View File

@ -10,7 +10,6 @@
: (g2 b) : (g2 b)
(error "niy!"))|# (error "niy!"))|#
;#|
#| #|
(module mm typed/racket (module mm typed/racket
(require ;(submod "graph.lp2.rkt" test) (require ;(submod "graph.lp2.rkt" test)
@ -41,41 +40,36 @@
(define-graph g2 [a [v : Number] ((ma) (a 1))]) (define-graph g2 [a [v : Number] ((ma) (a 1))])
|# |#
(require "graph-5-multi-ctors.lp2.rkt") (require "graph-5-multi-ctors.lp2.rkt"
(require "../lib/low.rkt" "../lib/low.rkt"
"graph.lp2.rkt" "graph.lp2.rkt"
"get.lp2.rkt" "get.lp2.rkt"
"../type-expander/type-expander.lp2.rkt" "../type-expander/type-expander.lp2.rkt"
"../type-expander/multi-id.lp2.rkt") "../type-expander/multi-id.lp2.rkt"
(for-syntax syntax/parse))
(define-graph/multi-ctor gm ([a [b1 : b] [b2 : b] [v : Number]] (define-graph/multi-ctor gm ([a [b1 : b] [b2 : b] [s : String] [v : Number]]
[b [a : a] [s : String] [v : Number]]) [b [a : a] [s : String] [v : Number]])
[(r [v : Number] [w : String]) [(r [v : Integer] [w : String])
: a : a
(a (bx (if (> 0 v) (sub1 v) (+ v (string-length w)))) (printf "r ~a ~a\n" v w)
(by (if (> 0 v) (sub1 v) (+ v (string-length w))) "xyz") (a (bx (if (> v 0) (sub1 v) (string-length w)))
(by (if (> v 0) (sub1 v) (string-length w)) "xyz")
w
v)] v)]
[(bx [v : Number]) [(bx [v : Integer])
: b : b
(b (r v) "x" v)] (printf "bx ~a\n" v)
[(by [v : Number] [w : String]) (b (r v "one") "x" v)]
[(by [v : Integer] [w : String])
: b : b
(b (r v) "y" (+ v (string-length w)))]) (printf "by ~a ~a\n" v w)
(b (r v "two") "y" (+ v (string-length w)))])
(define gmi (gm 3 "b"))
(check-equal?: (get gmi v) 3)
(check-equal?: (get gmi b1 v) 2)
(check-equal?: (get gmi b1 s) "x")
(check-equal?: (get gmi b1 a v) 2)
;(check-equal?: (get gmi b1 a b1 a v) 1)
;(check-equal?: (get gmi b1 a b1 a b1 v) 1)

View File

@ -154,7 +154,7 @@
(check-equal?: 'aa.….bb.cc.d (list 'get 'aa ' 'bb 'cc 'd)) (check-equal?: 'aa.….bb.cc.d (list 'get 'aa ' 'bb 'cc 'd))
(check-equal?: 'aa…bb (list 'get 'aa ' 'bb)) (check-equal?: 'aa…bb (list 'get 'aa ' 'bb))
(check-equal?: 'aa… (slen 2 "a…")) (check-equal?: 'aa… (slen 3 "aa…"))
(check-equal?: ' (slen 1 "")) (check-equal?: ' (slen 1 ""))

View File

@ -133,7 +133,7 @@ database type opaque, and use an accessor with signature
(match q (match q
[(list h (cons e rest-rs) s i) [(list h (cons e rest-rs) s i)
(values e (values e
(list h rest-rs s (assert (- i 1) index?)))] (list h rest-rs s i #;(assert (- i 1) index?)))]
[(list h '() s i) [(list h '() s i)
(Δ-hash2-dequeue (list h (reverse s) '() i))]))] (Δ-hash2-dequeue (list h (reverse s) '() i))]))]
@ -219,58 +219,6 @@ position in the vector equal to the index associated to it in the hash table:
Δ-hash2-enqueue) Δ-hash2-enqueue)
(process-queues new-Δ-queues (name/Δ-results-add results result)))] (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
added to the @tc[Δ-Hash] since its creation from a simple @tc[HashTable].
@chunk[<Δ-hash>
(module Δ-hash typed/racket
(require "../lib/low.rkt")
(define-type (Δ-Hash A B)
(Pairof (HashTable A B)
(Setof (Pairof A B))))
(: empty-Δ-hash ( (K V) ( (Δ-Hash K V))))
(define (empty-Δ-hash)
(cons ((inst hash K V)) ((inst set (Pairof K V)))))
(: Δ-hash ( (K V) ( (HashTable K V) (Δ-Hash K V))))
(define (Δ-hash h)
(cons h ((inst set (Pairof K V)))))
(: Δ-hash-add ( (K V Acc) ( (Δ-Hash K V)
K
Acc
( K Acc (values V Acc))
(values (Δ-Hash K V)
Acc))))
(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}
@chunk[<module-main> @chunk[<module-main>
@ -284,8 +232,6 @@ added to the @tc[Δ-Hash] since its creation from a simple @tc[HashTable].
(provide fold-queues) (provide fold-queues)
<cond-let>
<Δ-hash>
<fold-queue-multi-sets-immutable-tags>)] <fold-queue-multi-sets-immutable-tags>)]
@chunk[<module-test> @chunk[<module-test>

View File

@ -38,8 +38,11 @@ And @tc[<mapping-declaration>] is:
(define-temp-ids "~a/mapping" (node )) (define-temp-ids "~a/mapping" (node ))
(define-temp-ids "~a/arg" (node )) (define-temp-ids "~a/arg" (node ))
(define-temp-ids "~a/function" (mapping )) (define-temp-ids "~a/function" (mapping ))
(define-temp-ids "~a/placeholder" (mapping ))
(define-temp-ids "~a/hide" (node )) (define-temp-ids "~a/hide" (node ))
(define-temp-ids "~a/hide" (result-node )) (define-temp-ids "~a/hide" (result-node ))
;(define/with-syntax (result-node/hide …)
; (cdr-assoc-syntax #'([node . node/hide] …)))
(define/with-syntax ([(grouped-mapping (define/with-syntax ([(grouped-mapping
grouped-mapping/function grouped-mapping/function
[(grouped-param . grouped-param-type) ] [(grouped-param . grouped-param-type) ]
@ -53,6 +56,8 @@ And @tc[<mapping-declaration>] is:
result-node result-node
body) ))) body) )))
#'(node ))) #'(node )))
(define/with-syntax ((node/arg↓ ) )
(repeat-stx (node/arg ) ((grouped-mapping ) )))
(define/with-syntax (mapping/grouped ) (define/with-syntax (mapping/grouped )
(stx-map (λ (mr) (cdr-assoc-syntax mr #'([node . node/mapping] ))) (stx-map (λ (mr) (cdr-assoc-syntax mr #'([node . node/mapping] )))
#'(result-node ))) #'(result-node )))
@ -65,30 +70,31 @@ And @tc[<mapping-declaration>] is:
(define/with-syntax ((root-param ) . _) #'((param ) )) (define/with-syntax ((root-param ) . _) #'((param ) ))
(define/with-syntax ((root-param-type ) . _) #'((param-type ) )) (define/with-syntax ((root-param-type ) . _) #'((param-type ) ))
#`(debug (quasitemplate
(begin ;(debug
(define-graph name/wrapped (begin
#:definitions (define-graph name/wrapped
((define-multi-id name #:definitions
#:type-expander ((define-multi-id name
(λ (stx) #:type-expander
(syntax-case stx () (λ (stx)
[(_ . rest) #'(name/wrapped . rest)])) (syntax-case stx ()
#:call (λ (stx) [(_ . rest) #'(name/wrapped . rest)]))
(syntax-parse stx #:call (λ (stx)
[(_ . rest) (syntax-parse stx
(syntax/loc stx [(_ . rest)
(name/constructor . rest))])) (syntax/loc stx
#:id (λ (stx) (name/constructor . rest))]))
(syntax/loc stx name/constructor))) #:id (λ (stx)
(define (name/constructor [root-param : root-param-type] ) (syntax/loc stx name/constructor)))
(name/wrapped #:root root-node (list 'root-mapping (define (name/constructor [root-param : root-param-type] )
root-param ))) (name/wrapped #:root root-node (list 'root-mapping
<define-mappings>) root-param )))
[node [field c field-type] <define-mappings>)
((node/mapping [node/arg : <node-arg-type>]) [node [field c field-type]
<mapping-body>)] ((node/mapping [node/arg : <node-arg-type>])
))))] <mapping-body>)]
))#|)|#))]
Where the type for the merged mapping is: Where the type for the merged mapping is:
@ -96,32 +102,39 @@ Where the type for the merged mapping is:
(U (List 'grouped-mapping grouped-param-type ) )] (U (List 'grouped-mapping grouped-param-type ) )]
@chunk[<define-mappings> @chunk[<define-mappings>
(define (mapping/function node/hide ; nodes ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
result-node/hide ; self ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
[param : param-type] ) (begin
: (name result-node) (: mapping/placeholder ( param-type
(let ([node node/hide] ) (name/wrapped #:placeholder result-node)))
(let ([result-node result-node/hide]) (define (mapping/placeholder param )
(? '<bdy>)))) ((tmpl-cdr-assoc-syntax result-node [node . node/mapping] )
(list 'mapping param )))
(: mapping/function ( ;(name/wrapped #:make-placeholder node) …
;(name/wrapped #:make-incomplete result-node)
param-type
(name/wrapped #:incomplete result-node)))
(define (mapping/function ;node/hide … ; nodes
;result-node/hide ; self
param )
(let ([result-node/hide result-node])
(let ([mapping mapping/placeholder] )
(let ([result-node result-node/hide])
. body)))))
] ]
@chunk[<bdy>
(let ([node-names… node_]
;[mapping mapping/grouped] …
[node-name_ node_])
body)]
We then select in the grouped mapping which one to call. We then select in the grouped mapping which one to call.
@chunk[<mapping-body> @chunk[<mapping-body>
(let ((a node/arg)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(cond ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
[(eq? (car a) 'grouped-mapping) (cond
(apply grouped-mapping/function [(eq? (car node/arg↓) 'grouped-mapping)
#,@#'(node ) (apply grouped-mapping/function
grouped-result-node ;#,@#'(node …)
(cdr a))] ;grouped-result-node
))] (cdr node/arg↓))]
)]
TODO: At the call site, use a macro and annotate the function (given by its TODO: At the call site, use a macro and annotate the function (given by its
name) with the right type, so that the user doesn't see all the types in the name) with the right type, so that the user doesn't see all the types in the
@ -135,6 +148,7 @@ name) with the right type, so that the user doesn't see all the types in the
@chunk[<module-main> @chunk[<module-main>
(module main typed/racket (module main typed/racket
(require (for-syntax syntax/parse (require (for-syntax syntax/parse
syntax/parse/experimental/template
racket/syntax racket/syntax
syntax/stx syntax/stx
"../lib/low-untyped.rkt" "../lib/low-untyped.rkt"

View File

@ -553,10 +553,16 @@ via @tc[(g Street)].
@chunk[<graph-type-expander> @chunk[<graph-type-expander>
(λ (stx) (λ (stx)
(syntax-parse stx (syntax-parse stx
[(_ (~datum node)) #'node/with-promises-type] [(_ (~datum node)) #'node/with-promises-type]
[(_ #:incomplete (~datum node)) #'node/incomplete-type]
[(_ #:incomplete (~datum node)) #'node/incomplete-type] [(_ #:make-incomplete (~datum node))
))] #'( <field/incomplete-type> node/incomplete-type)]
[(_ #:incomplete (~datum node) fld)
(syntax-parse #'fld
[(~datum field) #'<field/incomplete-type>] )]
[(_ #:make-placeholder (~datum node))
#'( param-type node/placeholder-type)]
[(_ #:placeholder (~datum node)) #'node/placeholder-type] ))]
We will be able to use this type expander in function types, for example: We will be able to use this type expander in function types, for example:

View File

@ -78,3 +78,10 @@
(structure v w) (structure v w)
(structure v w) (structure v w)
(structure v w) (structure v w)
(structure b1 b2 s v)
(structure b1 b2 s v)
(structure b1 b2 s v)
(structure ab v)
(structure ba v)
(structure ab v)
(structure ab v)

View File

@ -1423,12 +1423,34 @@
;; ==== low/typed-not-implemented-yet.rkt ==== ;; ==== low/typed-not-implemented-yet.rkt ====
(provide ?) (provide ? ?*)
(define-syntax (?* stx)
(syntax-case stx ()
[(q . rest)
(quasisyntax/loc stx
((λ () : (U) #,(syntax/loc #'q (error "Not implemented yet"))
. rest)))]))
(define-syntax (? stx) (define-syntax (? stx)
(syntax-case stx () (syntax-case stx ()
[(q t . rest) [(q t . rest)
(quasisyntax/loc stx (quasisyntax/loc stx
((λ () : t #,(syntax/loc #'q (error "Not implemented yet")) ((ann (λ () #,(syntax/loc #'q (error "Not implemented yet"))
. rest)))])) . rest)
( t))))]))
;; ==== low/cond-let.rkt ====
(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 )))]))
;; ==== end ==== ;; ==== end ====

View File

@ -0,0 +1,35 @@
#lang typed/racket
(require "../../lib/low.rkt"
"../../graph/graph.lp2.rkt"
"../../graph/get.lp2.rkt"
"../../type-expander/type-expander.lp2.rkt")
(define-graph g2
[a [v : Number] [ab : b]
((ma [arga2 : Integer] [arg3 : String])
(a arga2 (mb (max 0 (sub1 arga2)))))]
[b [v : Number] [ba : a]
((mb [argb2 : Integer])
(b argb2 (ma (sub1 argb2) "z")))])
(define gi (g2 3 "b"))
(check-equal?: (get gi v) 3)
(check-equal?: (get gi ab v) 2)
(check-equal?: (get gi ab ba v) 1) ;; should be 1, but was 3 (bug now fixed)
(define-graph g3
[a [v : Number] [ab : b]
((ma [arg : (List 'r Integer String)])
(a (cadr arg) (mb (list 'b1 (if (> (cadr arg) 0)
(sub1 (cadr arg))
(string-length (caddr arg)))))))]
[b [v : Number] [ba : a]
((mb [arg : (List 'b1 Integer)])
(b (cadr arg) (ma (list 'r (cadr arg) "z"))))])
(define gi3 (g3 (list 'r 3 "b")))
(check-equal?: (get gi3 v) 3)
(check-equal?: (get gi3 ab v) 2)
(check-equal?: (get gi3 ab ba v) 2) ;; should be 2, but was 3 (bug now fixed)