From 2982e49e6ea2ce3e5ca8490206f40250d53f4e5a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Georges=20Dup=C3=A9ron?= Date: Fri, 25 Mar 2016 18:38:05 +0100 Subject: [PATCH] Fixed bug with rich-returns, the procedure generated by inline-instance* had the wrong return type. --- graph-lib/graph/__DEBUG_graph6.rkt | 291 +++++++++++++++++- graph-lib/graph/graph-6-rich-returns-test.rkt | 7 +- graph-lib/graph/graph-6-rich-returns.lp2.rkt | 62 ++-- graph-lib/graph/rewrite-type.lp2.rkt | 5 +- 4 files changed, 337 insertions(+), 28 deletions(-) diff --git a/graph-lib/graph/__DEBUG_graph6.rkt b/graph-lib/graph/__DEBUG_graph6.rkt index 57fd0d29..3331352a 100644 --- a/graph-lib/graph/__DEBUG_graph6.rkt +++ b/graph-lib/graph/__DEBUG_graph6.rkt @@ -94,7 +94,7 @@ ;; DEBUG: -#;(require (for-syntax racket/format +(require (for-syntax racket/format "rewrite-type.lp2.rkt" racket/syntax syntax/parse @@ -122,3 +122,292 @@ +#;(define-graph + grr31/first-step + #:definitions + ((define-type-expander + (~> stx) + (syntax-parse + stx + ((_ (~datum m-cities)) + (template + (U + (grr31/first-step + #:placeholder + m-cities4/node) + (Listof + (grr31/first-step + #:placeholder + City))))) + ((_ (~datum m-streets)) + (template + (U + (grr31/first-step + #:placeholder + m-streets5/node) + (Listof + (grr31/first-step + #:placeholder + Street))))))) + (define-type-expander + (first-step-expander2 stx) + (syntax-parse + stx + ((_ (~datum m-cities)) + #'(U + m-cities4/node + (Listof City))) + ((_ (~datum m-streets)) + #'(U + m-streets5/node + (Listof Street)))))) + (City + (streets + : + (Let + (~> first-step-expander2) + (~> m-streets))) + ((City2/simple-mapping + (streets + : + (~> m-streets))) + (City streets))) + (Street + (sname + : + (Let + (~> first-step-expander2) + String)) + ((Street3/simple-mapping + (sname : String)) + (Street sname))) + (m-cities4/node + (returned : (Listof City)) + ((m-cities + (cnames + : + (Listof + (Listof bubble)))) + (m-cities4/node + (let ((City + City2/simple-mapping) + (Street + Street3/simple-mapping)) + (define (strings→city + (s + : + (Listof + blob))) + (City (m-streets s))) + (map + strings→city + cnames))))) + (m-streets5/node + (returned + : + (Listof Street)) + ((m-streets + (snames + : + (Listof String))) + (m-streets5/node + (let ((City + City2/simple-mapping) + (Street + Street3/simple-mapping)) + (map + Street + snames)))))) + + +#;(define-graph + grr3 + #:definitions + ((define-type-expander + (~>-to-result-type stx) + (syntax-parse + stx + ((_ (~datum m-cities)) #'(Listof City)) + ((_ (~datum m-streets)) #'(Listof Street)))) + (define-type + m-cities10/node-marker + (Listof (grr3 #:placeholder City)); + #;(U (grr31/first-step m-cities4/node) (Listof (grr31/first-step City)))) + (define-type + m-streets11/node-marker + (Listof (grr3 #:placeholder Street)); + #;(U (grr31/first-step m-streets5/node) (Listof (grr31/first-step Street)))) + (define-type-expander + (second-step-marker-expander stx) + (syntax-parse + stx + ((_ (~datum m-cities)) #'m-cities10/node-marker) + ((_ (~datum m-streets)) #'m-streets11/node-marker))) + (define-type + second-step-m-cities16/node-of-first + (grr31/first-step m-cities4/node)) + (define-type + second-step-m-streets17/node-of-first + (grr31/first-step m-streets5/node)) + (define-type second-step-City18-of-first (grr31/first-step City)) + (define-type second-step-Street19-of-first (grr31/first-step Street)) + (define-type-expander + (second-step-marker2-expander stx) + (syntax-parse + stx + ((_ (~datum m-cities)) + #'(U + second-step-m-cities16/node-of-first + (Listof City #;(grr31/first-step City)))) + ((_ (~datum m-streets)) + #'(U + second-step-m-streets17/node-of-first + (Listof Street #;(grr31/first-step Street)))))) ;;;;;;;;;SHOULD BE A MARKER! (done here) + (define-type-expander + (inline-type* stx) + (dbg + ("inline-type*" stx) + (syntax-parse + stx + ((_ i-tyy (~and seen (:id …)) (~optional msg)) + (when (attribute msg) (displayln (syntax-e #'msg))) + (define/with-syntax replt #'i-tyy) + #'(inline-type replt seen))))) + (define-type-expander + (inline-type stx) + (dbg + ("inline-type" stx) + (syntax-parse + stx + ((_ i-t (~and seen (:id …))) + (let ((seen-list (syntax->list #'seen))) + (when (and + (not (null? seen-list)) + (member (car seen-list) (cdr seen-list) free-identifier=?)) + (raise-syntax-error + 'define-graph/rich-returns + (~a + "Cycles in types are not allowed." + " The following types were already inlined: " + (syntax->datum #'seen) + ", but " + #'t + " appeared a second time.") + #'t))) + (replace-in-type + #'(Let ((~> second-step-marker-expander)) i-t) + #'((second-step-m-cities16/node-of-first + (inline-type* (Listof City) (m-cities4/node . seen))) + (second-step-m-streets17/node-of-first + (inline-type* (Listof Street) (m-streets5/node . seen))) + (City (grr3 #:placeholder City)) + (Street (grr3 #:placeholder Street)))))))) + (define-syntax (inline-instance* stx) + (dbg + ("inline-instance*" stx) + (syntax-parse + stx + ((_ i-ty seen) + (define/with-syntax + replt + (replace-in-type + #'(Let (~> second-step-marker2-expander) i-ty) + #'((City second-step-City18-of-first) + (Street second-step-Street19-of-first)))) + (displayln (list "replt=" #'replt)) + #'(inline-instance replt seen))))) + (define-syntax (inline-instance stx) + (dbg + ("inline-instance" stx) + (syntax-parse + stx + ((_ i-t (~and seen (:id …))) + (define/with-syntax typp #'i-t) + (define/with-syntax + repl + (replace-in-instance + #'typp + #'((second-step-m-cities16/node-of-first + (inline-type* (Listof City) (m-cities4/node . seen) "RESSSS") + (grr31/first-step #:? m-cities4/node) + (λ ((x : second-step-m-cities16/node-of-first)) + ((inline-instance* (Listof City) (m-cities4/node . seen)) + (get x returned)))) + (second-step-m-streets17/node-of-first + (inline-type* (Listof Street) (m-streets5/node . seen) "RESSSS") + (grr31/first-step #:? m-streets5/node) + (λ ((x : second-step-m-streets17/node-of-first)) + ((inline-instance* (Listof Street) (m-streets5/node . seen)) + (get x returned)))) + (second-step-City18-of-first + (grr3 #:placeholder City) + (grr31/first-step #:? City) + City6/extract/mapping) + (second-step-Street19-of-first + (grr3 #:placeholder Street) + (grr31/first-step #:? Street) + Street7/extract/mapping)))) + (displayln (list "i-t=" #'typp)) + (let ((seen-list (syntax->list #'seen))) + (when (and + (not (null? seen-list)) + (member (car seen-list) (cdr seen-list) free-identifier=?)) + (raise-syntax-error + 'define-graph/rich-returns + (~a + "Cycles in types are not allowed." + " The following types were already inlined: " + (syntax->datum #'seen) + ", but " + #'t + " appeared a second time.") + #'t))) + #'repl))))) + (City + (streets : (Let (~> ~>-to-result-type) (~> m-streets))) + ((City6/extract/mapping (from : (grr31/first-step City))) + (City ((inline-instance* (~> m-streets) ()) + #;(λ ((val : (U second-step-m-streets17/node-of-first (Listof (grr31/first-step Street))))) + (first-value + ((λ ((val : (U second-step-m-streets17/node-of-first (Listof (grr31/first-step Street)))) (acc : Void)) + : + (values m-streets11/node-marker ;(U (inline-type* (Listof Street) (m-streets5/node) "RE1234") + ; (Listof (grr31/first-step Street))) + Void) + (cond + (((grr31/first-step #:? m-streets5/node) val) + ((ann + (λ ((x : second-step-m-streets17/node-of-first) (acc : Void)) + (values ((λ ((x : second-step-m-streets17/node-of-first)) ((inline-instance* (Listof Street) (m-streets5/node)) (get x returned))) x) acc)) + (→ second-step-m-streets17/node-of-first Void (values (inline-type* (Listof Street) (m-streets5/node) "RESSSS") Void))) + val + acc)) + (#t + ((λ ((val : (Listof (grr31/first-step Street))) (acc : Void)) + : + (values m-streets11/node-marker ;(Listof (grr31/first-step Street)) + Void) + (let ((f + ((inst foldl (grr31/first-step Street) (Pairof (Listof (grr31/first-step Street)) Void) Nothing Nothing) + (λ ((x : (grr31/first-step Street)) + (acc1 : (Pairof m-streets11/node-marker;(Listof (grr31/first-step Street)) + Void))) + (let-values (((res res-acc) ((inst values (grr31/first-step Street) Void) x (cdr acc1)))) + (cons (cons res (car acc1)) res-acc))) + (cons '() acc) + val))) + (values (reverse (car f)) (cdr f)))) + val + acc)) + (else + (typecheck-fail + (U second-step-m-streets17/node-of-first (Listof (grr31/first-step Street))) + "Unhandled union case in (U second-step-m-streets17/node-of-first (Listof (grr31/first-step Street))), whole type was:(U second-step-m-streets17/node-of-first (Listof (grr31/first-step Street)))")))) + val + (void)))) + (get from streets))) + )) + (Street + (sname : (Let (~> ~>-to-result-type) String)) + ((Street7/extract/mapping (from : (grr31/first-step Street))) + (Street ((inline-instance* String ()) (get from sname)))))) \ No newline at end of file diff --git a/graph-lib/graph/graph-6-rich-returns-test.rkt b/graph-lib/graph/graph-6-rich-returns-test.rkt index 3bbcc3ed..1d5a2d6f 100644 --- a/graph-lib/graph/graph-6-rich-returns-test.rkt +++ b/graph-lib/graph/graph-6-rich-returns-test.rkt @@ -1,5 +1,9 @@ #lang typed/racket +(module test-stx racket + ;(inline-type* ????) + ) + (module test typed/racket (require (for-syntax (submod "graph-6-rich-returns.lp2.rkt" test-syntax) syntax/strip-context)) @@ -12,4 +16,5 @@ typed/rackunit) ;(insert-tests);; TODO: FIXME - ) \ No newline at end of file + + (require (submod ".." test-stx))) \ No newline at end of file diff --git a/graph-lib/graph/graph-6-rich-returns.lp2.rkt b/graph-lib/graph/graph-6-rich-returns.lp2.rkt index 89723d4f..05222a4b 100644 --- a/graph-lib/graph/graph-6-rich-returns.lp2.rkt +++ b/graph-lib/graph/graph-6-rich-returns.lp2.rkt @@ -188,7 +188,10 @@ produced by the first step. … |# (define-type mapping/node-marker - (U (name/first-step mapping/node) + (tmpl-replace-in-type result-type + [mapping/node mapping/node-marker] ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;TODO: test: I'm unsure here + [node (name #:placeholder City)]) + #;(U (name/first-step mapping/node) (tmpl-replace-in-type result-type [mapping/node (name/first-step mapping/node)] [node (name/first-step node)]))) @@ -214,9 +217,9 @@ produced by the first step. (syntax-parse stx ;; TODO: should be ~literal [(_ (~datum mapping)) #'(U second-step-mapping/node-of-first - (tmpl-replace-in-type result-type - [mapping/node (name/first-step mapping/node)] - [node (name/first-step node)]))] + result-type #;(tmpl-replace-in-type result-type + [mapping/node (name/first-step mapping/node)] + [node (name/first-step node)]))] … ;; TODO: should fall-back to outer definition of ~>, if any? ))] @@ -281,10 +284,6 @@ To inline the temporary nodes in the instance, we use @tc[replace-in-instance], and call the inline-instance recursively: -;; HERE, we should expand a type of the shape: - -(foo bar (U m-street (Listof Street)) baz quux) - @CHUNK[ (define-syntax (inline-instance* stx) (dbg @@ -309,18 +308,16 @@ recursively: ))) (displayln (list "i-t=" #'typp)) - #'(λ ([x : i-t]) - ;( - repl - ;x) - (error "NIY2")) - #;(replace-in-instance #'(Let (id-~> second-step-marker2-expander) i-t) - #'( - ))])))] + #'repl + #;#'(λ ([x : i-t]) + : (inline-type* i-t seen) + (ann (repl x) + (inline-type* i-t seen "HERE")) + #;(error "NIY2"))])))] @chunk[ [second-step-mapping/node-of-first ;; from - (inline-type* result-type (mapping/node . seen)) ;; to + (inline-type* result-type (mapping/node . seen) "RESSSS") ;; to (name/first-step #:? mapping/node) ;; pred? (λ ([x : second-step-mapping/node-of-first]) ;; fun ((inline-instance* result-type (mapping/node . seen)) @@ -334,6 +331,20 @@ recursively: node/extract/mapping] ;; call mapping ;; fun …] +@subsection{Inlining instances, at the top} + +We need to inline the mapping nodes between the root mapping node and the first +layer of actual nodes. We do this in three steps: + +@itemlist[ + @item{First, we replace the actual nodes with + placeholders, which contain just an index, and aggregate + these nodes in lists (one per node type)} + @item{Then, we create the second-pass graph, using these + nodes as the roots} + @item{Finally, we replace the placeholders with the + second-pass nodes returned by the graph.}] + @subsection{Inlining types} The input type for the inlining of field @tc[streets] of the node @tc[City] is: @@ -448,12 +459,15 @@ which does not allow variants of (~> …). @chunk[ (define-type-expander (inline-type* stx) (dbg - ("inline-type" stx) + ("inline-type*" stx) (syntax-parse stx - [(_ i-tyy (~and seen (:id (… …)))) + [(_ i-tyy (~and seen (:id (… …))) (~optional msg)) + (when (attribute msg) + (displayln (syntax-e #'msg))) (define/with-syntax replt ;; Same as above in inline-instance*, TODO: factor it out. - (replace-in-type #'(Let (id-~> second-step-marker2-expander) i-tyy) + #'i-tyy + #;(replace-in-type #'(Let (id-~> second-step-marker-expander) i-tyy) #'([node second-step-node-of-first] …))) #'(inline-type replt seen)]))) @@ -469,12 +483,12 @@ which does not allow variants of (~> …). @chunk[ - [mapping/node-marker ;; from - (inline-type result-type (mapping/node . seen))] ;; to + [second-step-mapping/node-of-first ;mapping/node-marker ;; from + (inline-type* result-type (mapping/node . seen))] ;; to …] @chunk[ - [second-step-node-of-first ;; generated by the first pass + [node ;second-step-node-of-first ;; generated by the first pass (name #:placeholder node)] ;; new type …] @@ -566,7 +580,7 @@ encapsulating the result types of mappings. (display ">>> ")(displayln (list . log)) (let ((res (let () . body))) (display "<<< ")(displayln (list . log)) - (display "<<<= ")(display (car (list . log)))(displayln res) + (display "<<<= ")(display (car (list . log)))(display res)(displayln ".") res)))) )] diff --git a/graph-lib/graph/rewrite-type.lp2.rkt b/graph-lib/graph/rewrite-type.lp2.rkt index a53afc45..d10e0a8f 100644 --- a/graph-lib/graph/rewrite-type.lp2.rkt +++ b/graph-lib/graph/rewrite-type.lp2.rkt @@ -84,10 +84,10 @@ set of known type constructors like @tc[List] or @tc[Pairof], and recursively calls itself on the components of the type. @CHUNK[ - (define (replace-in-type t r) + (define/debug (replace-in-type t r) (define (recursive-replace new-t) (replace-in-type new-t r)) (define/with-syntax ([from to] ...) r) - #;(displayln (format "~a\n=> ~a" + (displayln (format "~a\n=> ~a" (syntax->datum t) (syntax->datum (expand-type t)))) (syntax-parse (expand-type t) @@ -554,6 +554,7 @@ These metafunctions just extract the arguments for @tc[replace-in-type] and "meta-struct.rkt" "../lib/low/backtrace.rkt" racket/require + debug ;; DEBUG (for-template (subtract-in typed/racket "../type-expander/type-expander.lp2.rkt")