graph-type.hl.rkt (5456B)
1 #lang aful/unhygienic hyper-literate typed/racket #:no-auto-require 2 3 @require[scribble-math 4 scribble-enhanced/doc 5 "notations.rkt" 6 (for-label racket)] 7 8 @title[#:style (with-html5 manual-doc-style) 9 #:tag "graph-type" 10 #:tag-prefix "phc-graph/graph-type"]{Declaring graph types} 11 12 @(chunks-toc-prefix 13 '("(lib phc-graph/scribblings/phc-graph-implementation.scrbl)" 14 "phc-graph/graph-type")) 15 16 The @racket[define-graph-type] form binds @racket[name] to a 17 @racket[graph-info] struct. The @racket[name] therefore contains metadata 18 describing among other things the types of nodes, the invariants that 19 instances of this graph type will satisfy. 20 21 @chunk[<signature> 22 (begin-for-syntax 23 (define-syntax-class signature 24 #:datum-literals (∈ ∋ ≡ ≢ ∉) 25 #:literals (:) 26 (pattern 27 (~no-order {~once name} 28 {~maybe #:∀ (tvar …)} 29 {~once (~and {~seq (nodeᵢ:id [fieldᵢⱼ:id : τᵢⱼ:type] 30 …) …} 31 {~seq [root-node . _] _ …})} 32 {~seq #:invariant a {~and op {~or ∈ ∋ ≡ ≢ ∉}} b} 33 {~seq #:invariant p}))))] 34 35 @section{Implementation} 36 37 The @racket[define-graph-type] macro expands to code which defines names for 38 the node types. It then binds the given @racket[name] to the 39 @racket[graph-info] instance built by @racket[build-graph-info]. 40 41 @CHUNK[<define-graph-type> 42 (begin-for-syntax 43 (define-template-metafunction (!check-remembered-node! stx) 44 (syntax-case stx () 45 [(_ nodeᵢ fieldᵢⱼ …) 46 (syntax-local-template-metafunction-introduce 47 (check-remembered-node! #'(nodeᵢ fieldᵢⱼ …)))]))) 48 49 (define-syntax/parse (define-graph-type . {~and whole :signature}) 50 ;; fire off the eventual delayed errors added by build-graph-info 51 (lift-maybe-delayed-errors) 52 #`(begin 53 <declare-node-types> 54 (define-syntax name 55 (build-graph-info (quote-syntax whole)))))] 56 57 @section{Declaring the node types} 58 59 @chunk[<declare-node-types> 60 (define-type nodeᵢ 61 (Promise 62 ((!check-remembered-node! nodeᵢ fieldᵢⱼ …) τᵢⱼ … 63 'Database 64 'Index))) 65 …] 66 67 @section{Creating the @racket[graph-info] instance} 68 69 @CHUNK[<build-graph-info> 70 (define-for-syntax (build-graph-info stx) 71 (parameterize ([disable-remember-immediate-error #t]) 72 (syntax-parse stx 73 [:signature 74 <graph-info>])))] 75 76 @chunk[<graph-info> 77 (graph-info #'name 78 (syntax->list (if (attribute tvar) #'(tvar …) #'())) 79 #'root-node 80 (syntax->list #'(nodeᵢ …)) 81 (make-immutable-hash 82 (map cons 83 (stx-map syntax-e #'(nodeᵢ …)) 84 (stx-map (λ/syntax-case (nodeᵢ node-incompleteᵢ 85 [fieldᵢⱼ τᵢⱼ] …) () 86 <node-info>) 87 #'([nodeᵢ node-incompleteᵢ 88 [fieldᵢⱼ τᵢⱼ] …] …)))) 89 (list->set 90 (append 91 (stx-map (λ/syntax-case (op a b) () <invariant-info-op>) 92 #'([op a b] …)) 93 (stx-map (λ/syntax-case p () <invariant-info-p>) 94 #'(p …)))))] 95 96 @chunk[<node-info> 97 (node-info (meta-struct-predicate 98 (check-remembered-node! #'(nodeᵢ fieldᵢⱼ …))) 99 (syntax->list #'(fieldᵢⱼ …)) 100 (make-immutable-hash 101 (map cons 102 (stx-map syntax-e #'(fieldᵢⱼ …)) 103 (stx-map (λ/syntax-case (fieldᵢⱼ τᵢⱼ) () 104 <field-info>) 105 #'([fieldᵢⱼ τᵢⱼ] …)))) 106 #'nodeᵢ ; promise type 107 #;(meta-struct-constructor 108 (check-remembered-tagged! #'(node-incompleteᵢ fieldᵢⱼ …))) 109 #;(check-remembered-tagged! #'(node-incompleteᵢ fieldᵢⱼ …)))] 110 111 @chunk[<field-info> 112 (field-info #'τᵢⱼ)] 113 114 @chunk[<invariant-info-op> 115 (invariant-info #'predicateTODO 116 #'witnessTODO)] 117 118 @chunk[<invariant-info-p> 119 (invariant-info #'predicateTODO 120 #'witnessTODO)] 121 122 @section{Putting it all together} 123 124 @chunk[<*> 125 (require racket/require 126 phc-toolkit 127 remember 128 (lib "phc-adt/tagged-structure-low-level.hl.rkt") 129 (for-syntax "graph-info.hl.rkt" 130 type-expander/expander 131 phc-toolkit/untyped 132 racket/set 133 subtemplate/override 134 extensible-parser-specifications) 135 (for-meta 2 racket/base)) 136 137 (provide define-graph-type) 138 139 <signature> 140 <build-graph-info> 141 <define-graph-type>]