From 693ab9e84e6e2ad0890128dff21bde4445d9fc51 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Georges=20Dup=C3=A9ron?= Date: Fri, 20 Jan 2017 18:28:33 +0100 Subject: [PATCH] Closes FB case 176 Fix the type of nodes for (non-)polymorphic graph types --- graph-info.hl.rkt | 4 +- graph-type.hl.rkt | 81 ++++++++++++++----- info.rkt | 3 +- .../assumption-equivalent-types-same-type.rkt | 49 +++++++++++ test/test-graph-type.rkt | 30 ++++--- 5 files changed, 134 insertions(+), 33 deletions(-) create mode 100644 test/assumption-equivalent-types-same-type.rkt diff --git a/graph-info.hl.rkt b/graph-info.hl.rkt index b4514b9..06f5589 100644 --- a/graph-info.hl.rkt +++ b/graph-info.hl.rkt @@ -265,7 +265,7 @@ data. (syntax->datum (datum->syntax #f v))) (case mode [(#t) - (display "#(~#t~" port) + (display "#(" port) (display name port) (for-each (λ (f) (display " " port) @@ -273,7 +273,7 @@ data. fields) (display ")" port)] [(#f) - (display "#(~#f~" port) + (display "#(" port) (display name port) (for-each (λ (f) (display " " port) diff --git a/graph-type.hl.rkt b/graph-type.hl.rkt index 38dc5bf..d10cf26 100644 --- a/graph-type.hl.rkt +++ b/graph-type.hl.rkt @@ -13,33 +13,67 @@ '("(lib phc-graph/scribblings/phc-graph-implementation.scrbl)" "phc-graph/graph-type")) -@CHUNK[ +The @racket[define-graph-type] form binds @racket[name] to a +@racket[graph-info] struct. The @racket[name] therefore contains metadata +describing among other things the types of nodes, the invariants that +instances of this graph type will satisfy. + +@chunk[ (begin-for-syntax (define-syntax-class signature #:datum-literals (∈ ∋ ≡ ≢ ∉) #:literals (:) - (pattern (name - {~maybe #:∀ (tvar …)} - (~and {~seq [nodeᵢ:id [fieldᵢⱼ:id : τ] …] …} - {~seq [root-node . _] _ …}) - {~seq #:invariant a {~and op {~or ∈ ∋ ≡ ≢ ∉}} b} … - {~seq #:invariant p} …)))) + (pattern + (~no-order {~once name} + {~maybe #:∀ (tvar …)} + {~once (~and {~seq (nodeᵢ:id [fieldᵢⱼ:id : τᵢⱼ:type] + …) …} + {~seq [root-node . _] _ …})} + {~seq #:invariant a {~and op {~or ∈ ∋ ≡ ≢ ∉}} b} + {~seq #:invariant p}))))] - (define-for-syntax (compute-graph-info stx) +@section{Implementation} + +The @racket[define-graph-type] macro expands to code which defines names for +the node types. It then binds the given @racket[name] to the +@racket[graph-info] instance built by @racket[build-graph-info]. + +@CHUNK[ + (begin-for-syntax + (define-template-metafunction (!check-remembered-node! stx) + (syntax-case stx () + [(_ nodeᵢ fieldᵢⱼ …) + (syntax-local-template-metafunction-introduce + (check-remembered-node! #'(nodeᵢ fieldᵢⱼ …)))]))) + + (define-syntax/parse (define-graph-type . {~and whole :signature}) + ;; fire off the eventual delayed errors added by build-graph-info + (lift-maybe-delayed-errors) + #`(begin + + (define-syntax name + (build-graph-info (quote-syntax whole)))))] + +@section{Declaring the node types} + +@chunk[ + (define-type nodeᵢ + (Promise + ((!check-remembered-node! nodeᵢ fieldᵢⱼ …) τᵢⱼ … + 'Database + 'Index))) + …] + +@section{Creating the @racket[graph-info] instance} + +@CHUNK[ + (define-for-syntax (build-graph-info stx) (parameterize ([disable-remember-immediate-error #t]) (syntax-parse stx [:signature - ]))) - (define-syntax/parse (define-graph-type . whole:signature) - ;; fire off the eventual delayed errors added by compute-graph-info - (lift-maybe-delayed-errors) - #`(begin - (define-syntax whole.name - (compute-graph-info (quote-syntax whole)))))] + ])))] @chunk[ - #:with (node-incompleteᵢ …) (stx-map #λ(format-id % " ~a-incomplete" %) - #'(nodeᵢ …)) (graph-info #'name (syntax->list (if (attribute tvar) #'(tvar …) #'())) #'root-node @@ -69,7 +103,7 @@ (stx-map (λ/syntax-case (fieldᵢⱼ τᵢⱼ) () ) #'([fieldᵢⱼ τᵢⱼ] …)))) - (check-remembered-node! #'(nodeᵢ fieldᵢⱼ …)) + #'nodeᵢ ; promise type #;(meta-struct-constructor (check-remembered-tagged! #'(node-incompleteᵢ fieldᵢⱼ …))) #;(check-remembered-tagged! #'(node-incompleteᵢ fieldᵢⱼ …)))] @@ -85,19 +119,26 @@ (invariant-info #'predicateTODO #'witnessTODO)] +@section{Putting it all together} + @chunk[<*> (require racket/require phc-toolkit remember (lib "phc-adt/tagged-structure-low-level.hl.rkt") (for-syntax "graph-info.hl.rkt" + type-expander/expander phc-toolkit/untyped (subtract-in syntax/parse phc-graph/subtemplate) racket/set phc-graph/subtemplate-override - racket/syntax) + racket/syntax + extensible-parser-specifications + backport-template-pr1514/experimental/template) (for-meta 2 racket/base)) (provide define-graph-type) - + + + ] \ No newline at end of file diff --git a/info.rkt b/info.rkt index 35054ba..a7b836e 100644 --- a/info.rkt +++ b/info.rkt @@ -14,7 +14,8 @@ "typed-map" "scribble-lib" "pconvert-lib" - "remember")) + "remember" + "extensible-parser-specifications")) (define build-deps '("scribble-lib" "racket-doc" "remember" diff --git a/test/assumption-equivalent-types-same-type.rkt b/test/assumption-equivalent-types-same-type.rkt new file mode 100644 index 0000000..ce299be --- /dev/null +++ b/test/assumption-equivalent-types-same-type.rkt @@ -0,0 +1,49 @@ +#lang typed/racket + +;; Check that equivalent type specifications are correctly interpreted as +;; being the same type by Typed/Racket. +;; +;; This was not the case in some situations in older versions of Typed/Racket, +;; but I am not sure whether this reproduces the same issue, or whether this +;; file would typecheck in older versions too. + +(let () + (define-type (Foo X) + (U X (List 'foo (Bar X) (Foo X)))) + + (define-type (Bar Y) + (List 'bar (Foo Y))) + + (define-type (Foo2 X) + (U X (List 'foo (Bar2 X) (Foo2 X)))) + + (define-type (Bar2 Y) + (List 'bar (Foo2 Y))) + + (λ #:∀ (A) ([x : (Foo A)]) + ;; Check here: + (ann (ann x (Foo2 A)) (Foo A))) + + (void)) + +(struct (a b) st-foo ([a : a] [b : b])) +(struct (a) st-bar ([a : a])) + +(let () + (define-type (Foo X) + (U X (st-foo (Bar X) (Foo X)))) + + (define-type (Bar Y) + (st-bar (Foo Y))) + + (define-type (Foo2 X) + (U X (st-foo (Bar2 X) (Foo2 X)))) + + (define-type (Bar2 Y) + (st-bar (Foo2 Y))) + + (λ #:∀ (A) ([x : (Foo A)]) + ;; Check here: + (ann (ann x (Foo2 A)) (Foo A))) + + (void)) \ No newline at end of file diff --git a/test/test-graph-type.rkt b/test/test-graph-type.rkt index 3ca5006..9416977 100644 --- a/test/test-graph-type.rkt +++ b/test/test-graph-type.rkt @@ -17,13 +17,23 @@ #:invariant City.citizens._ ∈ City.streets._.houses._.owner #:invariant City.citizens._ ∋ City.streets._.houses._.owner) -(module* test racket/base - (require (for-syntax racket/pretty - racket/base) - (submod "..")) - (eval #'(begin - (define-syntax (dbg _stx) - (parameterize ([pretty-print-columns 188]) - (pretty-print (syntax-local-value #'g1))) - #'(void)) - (dbg)))) \ No newline at end of file +(require (for-syntax racket/pretty + racket/base)) +(eval #'(begin + (define-syntax (dbg _stx) + (parameterize ([pretty-print-columns 188]) + (pretty-print (syntax-local-value #'g1))) + #'(void)) + (dbg))) + +(require (for-syntax syntax/parse + "../graph-info.hl.rkt")) + +(define-syntax dbg + (syntax-parser + [(_ t) + #`(define-type t + #,(node-info-promise-type + (hash-ref (graph-info-nodes (syntax-local-value #'g1)) 'City)))])) +(dbg t-city) +;(define-type expected (t-city Number String Symbol 'Database 'Index)) \ No newline at end of file