Closes FB case 176 Fix the type of nodes for (non-)polymorphic graph types
This commit is contained in:
Georges Dupéron
parent
7991ed7d7e
commit
693ab9e84e
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -13,33 +13,67 @@
|
|||
'("(lib phc-graph/scribblings/phc-graph-implementation.scrbl)"
|
||||
"phc-graph/graph-type"))
|
||||
|
||||
@CHUNK[<define-graph-type>
|
||||
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[<signature>
|
||||
(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[<define-graph-type>
|
||||
(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
|
||||
<declare-node-types>
|
||||
(define-syntax name
|
||||
(build-graph-info (quote-syntax whole)))))]
|
||||
|
||||
@section{Declaring the node types}
|
||||
|
||||
@chunk[<declare-node-types>
|
||||
(define-type nodeᵢ
|
||||
(Promise
|
||||
((!check-remembered-node! nodeᵢ fieldᵢⱼ …) τᵢⱼ …
|
||||
'Database
|
||||
'Index)))
|
||||
…]
|
||||
|
||||
@section{Creating the @racket[graph-info] instance}
|
||||
|
||||
@CHUNK[<build-graph-info>
|
||||
(define-for-syntax (build-graph-info stx)
|
||||
(parameterize ([disable-remember-immediate-error #t])
|
||||
(syntax-parse stx
|
||||
[:signature
|
||||
<graph-info>])))
|
||||
(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)))))]
|
||||
<graph-info>])))]
|
||||
|
||||
@chunk[<graph-info>
|
||||
#: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-info>)
|
||||
#'([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)
|
||||
|
||||
<signature>
|
||||
<build-graph-info>
|
||||
<define-graph-type>]
|
||||
3
info.rkt
3
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"
|
||||
|
|
|
|||
49
test/assumption-equivalent-types-same-type.rkt
Normal file
49
test/assumption-equivalent-types-same-type.rkt
Normal file
|
|
@ -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))
|
||||
|
|
@ -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))))
|
||||
(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))
|
||||
Loading…
Reference in New Issue
Block a user