103 lines
4.1 KiB
Racket
103 lines
4.1 KiB
Racket
#lang aful/unhygienic hyper-literate typed/racket #:no-auto-require
|
|
|
|
@require[scribble-math
|
|
scribble-enhanced/doc
|
|
"notations.rkt"
|
|
(for-label racket)]
|
|
|
|
@title[#:style (with-html5 manual-doc-style)
|
|
#:tag "graph-type"
|
|
#:tag-prefix "phc-graph/graph-type"]{Declaring graph types}
|
|
|
|
@(chunks-toc-prefix
|
|
'("(lib phc-graph/scribblings/phc-graph-implementation.scrbl)"
|
|
"phc-graph/graph-type"))
|
|
|
|
@CHUNK[<define-graph-type>
|
|
(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} …))))
|
|
|
|
(define-for-syntax (compute-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)))))]
|
|
|
|
@chunk[<graph-info>
|
|
#:with (node-incompleteᵢ …) (stx-map #λ(format-id % " ~a-incomplete" %)
|
|
#'(nodeᵢ …))
|
|
(graph-info #'name
|
|
(syntax->list (if (attribute tvar) #'(tvar …) #'()))
|
|
#'root-node
|
|
(syntax->list #'(nodeᵢ …))
|
|
(make-immutable-hash
|
|
(map cons
|
|
(stx-map syntax-e #'(nodeᵢ …))
|
|
(stx-map (λ/syntax-case (nodeᵢ node-incompleteᵢ
|
|
[fieldᵢⱼ τᵢⱼ] …) ()
|
|
<node-info>)
|
|
#'([nodeᵢ node-incompleteᵢ
|
|
[fieldᵢⱼ τᵢⱼ] …] …))))
|
|
(list->set
|
|
(append
|
|
(stx-map (λ/syntax-case (op a b) () <invariant-info-op>)
|
|
#'([op a b] …))
|
|
(stx-map (λ/syntax-case p () <invariant-info-p>)
|
|
#'(p …)))))]
|
|
|
|
@chunk[<node-info>
|
|
(node-info (meta-struct-predicate
|
|
(check-remembered-node! #'(nodeᵢ fieldᵢⱼ …)))
|
|
(syntax->list #'(fieldᵢⱼ …))
|
|
(make-immutable-hash
|
|
(map cons
|
|
(stx-map syntax-e #'(fieldᵢⱼ …))
|
|
(stx-map (λ/syntax-case (fieldᵢⱼ τᵢⱼ) ()
|
|
<field-info>)
|
|
#'([fieldᵢⱼ τᵢⱼ] …))))
|
|
(check-remembered-node! #'(nodeᵢ fieldᵢⱼ …))
|
|
#;(meta-struct-constructor
|
|
(check-remembered-tagged! #'(node-incompleteᵢ fieldᵢⱼ …)))
|
|
#;(check-remembered-tagged! #'(node-incompleteᵢ fieldᵢⱼ …)))]
|
|
|
|
@chunk[<field-info>
|
|
(field-info #'τᵢⱼ)]
|
|
|
|
@chunk[<invariant-info-op>
|
|
(invariant-info #'predicateTODO
|
|
#'witnessTODO)]
|
|
|
|
@chunk[<invariant-info-p>
|
|
(invariant-info #'predicateTODO
|
|
#'witnessTODO)]
|
|
|
|
@chunk[<*>
|
|
(require racket/require
|
|
phc-toolkit
|
|
remember
|
|
(lib "phc-adt/tagged-structure-low-level.hl.rkt")
|
|
(for-syntax "graph-info.hl.rkt"
|
|
phc-toolkit/untyped
|
|
(subtract-in syntax/parse phc-graph/subtemplate)
|
|
racket/set
|
|
phc-graph/subtemplate-override
|
|
racket/syntax)
|
|
(for-meta 2 racket/base))
|
|
|
|
(provide define-graph-type)
|
|
|
|
<define-graph-type>] |