Extracted subtemplate from phc-graph
This commit is contained in:
Georges Dupéron
parent
f500dfcb1a
commit
bcced0995d
7
.gitignore
vendored
7
.gitignore
vendored
|
|
@ -1,7 +0,0 @@
|
|||
*~
|
||||
\#*
|
||||
.\#*
|
||||
.DS_Store
|
||||
compiled/
|
||||
/doc/
|
||||
/.~*.vue
|
||||
60
.travis.yml
60
.travis.yml
|
|
@ -1,60 +0,0 @@
|
|||
language: c
|
||||
|
||||
# Based from: https://github.com/greghendershott/travis-racket
|
||||
|
||||
# Optional: Remove to use Travis CI's older infrastructure.
|
||||
sudo: false
|
||||
|
||||
env:
|
||||
global:
|
||||
# Supply a global RACKET_DIR environment variable. This is where
|
||||
# Racket will be installed. A good idea is to use ~/racket because
|
||||
# that doesn't require sudo to install and is therefore compatible
|
||||
# with Travis CI's newer container infrastructure.
|
||||
- RACKET_DIR=~/racket
|
||||
matrix:
|
||||
# Supply at least one RACKET_VERSION environment variable. This is
|
||||
# used by the install-racket.sh script (run at before_install,
|
||||
# below) to select the version of Racket to download and install.
|
||||
#
|
||||
# Supply more than one RACKET_VERSION (as in the example below) to
|
||||
# create a Travis-CI build matrix to test against multiple Racket
|
||||
# versions.
|
||||
#- RACKET_VERSION=6.0
|
||||
#- RACKET_VERSION=6.1
|
||||
#- RACKET_VERSION=6.1.1
|
||||
#- RACKET_VERSION=6.2
|
||||
#- RACKET_VERSION=6.3
|
||||
#- RACKET_VERSION=6.4
|
||||
#- RACKET_VERSION=6.5
|
||||
#- RACKET_VERSION=6.6
|
||||
#- RACKET_VERSION=6.7
|
||||
- RACKET_VERSION=HEAD
|
||||
|
||||
matrix:
|
||||
allow_failures:
|
||||
# - env: RACKET_VERSION=HEAD
|
||||
fast_finish: true
|
||||
|
||||
before_install:
|
||||
- git clone https://github.com/greghendershott/travis-racket.git ~/travis-racket
|
||||
- cat ~/travis-racket/install-racket.sh | bash # pipe to bash not sh!
|
||||
- export PATH="${RACKET_DIR}/bin:${PATH}" #install-racket.sh can't set for us
|
||||
|
||||
install:
|
||||
- raco pkg install -j 2 --deps search-auto
|
||||
|
||||
before_script:
|
||||
|
||||
# Here supply steps such as raco make, raco test, etc. You can run
|
||||
# `raco pkg install --deps search-auto` to install any required
|
||||
# packages without it getting stuck on a confirmation prompt.
|
||||
script:
|
||||
- raco test -p phc-graph
|
||||
- raco setup --check-pkg-deps --no-zo --no-launcher --no-install --no-post-install --no-docs --pkgs phc-graph
|
||||
- raco pkg install --deps search-auto doc-coverage
|
||||
- raco doc-coverage phc-graph
|
||||
|
||||
after_success:
|
||||
- raco pkg install --deps search-auto cover cover-coveralls
|
||||
- raco cover -b -f coveralls -d $TRAVIS_BUILD_DIR/coverage .
|
||||
File diff suppressed because it is too large
Load Diff
11
LICENSE.txt
11
LICENSE.txt
|
|
@ -1,11 +0,0 @@
|
|||
phc-graph
|
||||
Copyright (c) 2016 georges
|
||||
|
||||
This package is distributed under the GNU Lesser General Public
|
||||
License (LGPL). This means that you can link phc-graph into proprietary
|
||||
applications, provided you follow the rules stated in the LGPL. You
|
||||
can also modify this package; if you distribute a modified version,
|
||||
you must distribute it under the terms of the LGPL, which in
|
||||
particular means that you must release the source code for the
|
||||
modified software. See http://www.gnu.org/copyleft/lesser.html
|
||||
for more information.
|
||||
|
|
@ -1,79 +0,0 @@
|
|||
#lang racket
|
||||
(let ()
|
||||
;; Given an order-independent let
|
||||
(let ([x 'b]
|
||||
[y 'a])
|
||||
(cons x y))
|
||||
|
||||
;; e.g. represented roughly as:
|
||||
(list 'let
|
||||
(set (cons 'x ''b) (cons 'y ''a)) ;; bindings
|
||||
(list 'cons 'x 'y)) ;; body
|
||||
|
||||
;; Can we devise an α-equivalence normal form?
|
||||
|
||||
;; Let's sort the right-hand side of the let bindings, and number them in that
|
||||
;; order. x gets renamed to var1, and y gets renamed to var0, given the order
|
||||
;; ('a, 'b)
|
||||
(let ([var0 'a]
|
||||
[var1 'b])
|
||||
(cons var1 var0))
|
||||
|
||||
;; The idea roughly amounts to transforming sets into lists by sorting their
|
||||
;; contents, knowing that the sort operation must not depend on unrenamed
|
||||
;; variables. Given a letrec, what can we do?
|
||||
|
||||
(let ([x 'b]
|
||||
[y 'a])
|
||||
(letrec ([f (λ (v) (f (cons v x)))]
|
||||
[g (λ (v) (g (cons v y)))])
|
||||
'…))
|
||||
|
||||
;; In the example above, x and y can be renamed first, giving var1 and var0
|
||||
;; respectively. Then it becomes possible to sort f and g, as they differ
|
||||
;; by their references to var1 and var0 respectively, and these have already
|
||||
;; been assigned a new number.
|
||||
|
||||
(letrec ([f (λ (v) (f v))]
|
||||
[g (λ (v) (f v))])
|
||||
'…)
|
||||
|
||||
;; Here, we have no difference in the values, but there is a difference in the
|
||||
;; way these values refer to the bingings: f refers to itself, while g refers to
|
||||
;; f. Topologically sorting that graph would give a cannon order.
|
||||
|
||||
(letrec ([f (λ (v) (g v))]
|
||||
[g (λ (v) (f v))])
|
||||
'…)
|
||||
|
||||
;; Here, there is no difference in the values, and swapping them gives a new
|
||||
;; graph isomorphic to the original. Another more complex case follows:
|
||||
|
||||
(letrec ([f (λ (v) (g v))]
|
||||
[g (λ (v) (h v))]
|
||||
[h (λ (v) (f v))])
|
||||
'…)
|
||||
|
||||
;; In these cases, the order we assign to each variable does not matter, as they
|
||||
;; are strictly symmetric (in the sense that the bound values are at run-time
|
||||
;; observarionally identical).
|
||||
|
||||
;; What general solution can we find?
|
||||
;; * What if we topo-sort bindings which cannot be distinguished by their values
|
||||
;; * then, within each SCC, if there are some values which are isomorphic to
|
||||
;; each other, they can be grouped together for the purpose of numbering.
|
||||
;; this operation can be repeated.
|
||||
;; * By alternating these two steps, do we systematically get a
|
||||
;; topologically-sorted DAG, where some nodes are a group of nodes which were
|
||||
;; isomorphic one level down?
|
||||
;;
|
||||
;; Relevant:
|
||||
;; @inproceedings{babai1983canonical,
|
||||
;; title={Canonical labeling of graphs},
|
||||
;; author={Babai, L{\'a}szl{\'o} and Luks, Eugene M},
|
||||
;; booktitle={Proceedings of the fifteenth annual ACM symposium on Theory of computing},
|
||||
;; pages={171--183},
|
||||
;; year={1983},
|
||||
;; organization={ACM}
|
||||
;; }
|
||||
(void))
|
||||
32
bench001.rkt
32
bench001.rkt
|
|
@ -1,32 +0,0 @@
|
|||
#lang type-expander/lang
|
||||
(require (for-syntax racket
|
||||
phc-toolkit))
|
||||
|
||||
(struct Or ())
|
||||
(define-type-expander (Invariants stx)
|
||||
(syntax-case stx ()
|
||||
[(_ invᵢ …)
|
||||
#'(→ (U Or (→ invᵢ Void) …) Void)
|
||||
#;#'(→ (→ (∩ invᵢ …) Void) Void)]))
|
||||
|
||||
|
||||
|
||||
(define-syntax (foo stx)
|
||||
(syntax-case stx ()
|
||||
[(_ T nb)
|
||||
#`(define-type T
|
||||
(Invariants
|
||||
#,@(map (λ (x) #`(List 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j 'k #,x 'm 'n))
|
||||
(range (syntax-e #'nb)))))]))
|
||||
(foo T0 600)
|
||||
(foo T1 550)
|
||||
|
||||
(define f0 : T0 (λ (x) (void)))
|
||||
|
||||
(define-syntax (repeat stx)
|
||||
(syntax-case stx ()
|
||||
[(_ n body)
|
||||
#`(begin #,@(map (const #'body)
|
||||
(range (syntax-e #'n))))]))
|
||||
(repeat 100
|
||||
(ann f0 T1))
|
||||
|
|
@ -1,52 +0,0 @@
|
|||
#lang typed/racket/base
|
||||
|
||||
(require racket/require
|
||||
phc-toolkit
|
||||
phc-adt
|
||||
(for-syntax racket/base
|
||||
phc-toolkit/untyped
|
||||
racket/syntax
|
||||
racket/format
|
||||
syntax/parse
|
||||
syntax/parse/experimental/template
|
||||
type-expander/expander
|
||||
"free-identifier-tree-equal.rkt")
|
||||
(for-meta 2 racket/base)
|
||||
(for-meta 2 phc-toolkit/untyped)
|
||||
(for-meta 2 syntax/parse))
|
||||
|
||||
(provide dispatch-union)
|
||||
|
||||
(define-syntax/parse (dispatch-union v
|
||||
([type-to-replaceᵢ Aᵢ predicateᵢ] …)
|
||||
[Xⱼ resultⱼ] …)
|
||||
(define-syntax-class to-replace
|
||||
(pattern [t result]
|
||||
#:with (_ predicate)
|
||||
(findf (λ (r) (free-id-tree=? #'t (stx-car r)))
|
||||
(syntax->list
|
||||
#'([type-to-replaceᵢ predicateᵢ] …)))
|
||||
#:with clause #`[(predicate v) result]))
|
||||
|
||||
(define-syntax-class tagged
|
||||
#:literals (tagged)
|
||||
(pattern [(tagged name [fieldₖ (~optional :colon) typeₖ] …) result]
|
||||
#:with clause #`[((tagged? name fieldₖ …) v) result]))
|
||||
|
||||
(define-syntax-class other
|
||||
(pattern [other result]
|
||||
#:with clause #`[else result]))
|
||||
|
||||
((λ (x) (local-require racket/pretty) #;(pretty-write (syntax->datum x)) x)
|
||||
(syntax-parse #'([Xⱼ resultⱼ] …)
|
||||
[({~or to-replace:to-replace
|
||||
tagged:tagged
|
||||
{~between other:other 0 1
|
||||
#:too-many (~a "only one non-tagged type can be part of"
|
||||
" the union")}}
|
||||
…)
|
||||
(quasisyntax/top-loc stx
|
||||
(cond
|
||||
to-replace.clause …
|
||||
tagged.clause …
|
||||
other.clause …))])))
|
||||
|
|
@ -1,40 +0,0 @@
|
|||
* gc
|
||||
* automatic generation of mappings Old → New
|
||||
|
||||
|
||||
* safe and automatic generation of 1↔1, 1↔many and many↔1 backward references
|
||||
|
||||
** global directives which apply to all nodes types: insert a pointer to the root, insert a backward pointer for every link (i.e. .back brings back to the previous node)
|
||||
|
||||
** the backward references specify the link that should be reversed, as well as a path from there. That way, methods can have a backward pointer to the "call" instructions referencing them, but the backward pointer should not
|
||||
directly point to the "call" instruction, but instead to the instruction's containing method, accessed with ".method". Maybe some syntactic sugar can allow this to be specified as #:backward-reference method.instructions.*[call]
|
||||
|
||||
* try to think about PHOAS
|
||||
|
||||
** Strong HOAS article: https://www.schoolofhaskell.com/user/edwardk/phoas
|
||||
|
||||
|
||||
|
||||
* mapping-placeholder = Placeholder type, one for each mapping
|
||||
* mapping-incomplete-result = (~> mapping) types within the mapping's result type are replaced by (U mapping-placeholder mapping-incomplete-result), and node types are replaced by (U xxx old-node)
|
||||
* mapping-with-promises-result = node types within the mapping's result type are replaced by node-promise
|
||||
|
||||
* node-promise = (Promise node-with-promises)
|
||||
* node-with-promises = node types within the node's fields are replaced by node-promise
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
To discuss:
|
||||
* maybe add a "self" variable, so that a mapping can give to others a placeholder for the node it is currently generating? That wouldn't play well with mappings which generate multiple nodes and/or part of a node.
|
||||
** self is a opaque "SELF" token, not an actual placeholder
|
||||
|
||||
Minor TODOs:
|
||||
* If we can guarantee that any two nodes within the same graph are (not (equal? …)), then we can implement a fast negative equality test, in addition to the existing fast equality test (which compares the "raw" field of nodes).
|
||||
|
|
@ -1,142 +0,0 @@
|
|||
On verification
|
||||
===============
|
||||
|
||||
* Some guarantees can be enforced statically using the type system.
|
||||
They are in a way proven to be enforeced in the expanded code,
|
||||
but in order to write verified compilers, it would be necessary to
|
||||
prove that the type indeed enforces the desired property, for all
|
||||
possible macro inputs.
|
||||
|
||||
Advantage: these proofs need to be written only once for the graph macro,
|
||||
and can be relied on by all compilers written using these static guarantees.
|
||||
* Some guarantees can be enforced statically "by construction",
|
||||
and the design patterns used to enforce them are guaranteed to be
|
||||
correctly applied because the code is macro-generated.
|
||||
In order to write verified compilers, it would be necessary to
|
||||
prove that the macro-generated code always enforces the desired property.
|
||||
|
||||
Advantage: these proofs need to be written only once for the graph macro,
|
||||
and can be relied on by all compilers written using these static guarantees.
|
||||
* Some guarantees can be enforced at run-time.
|
||||
This allows catching bugs early, and ensures no incorrect output can occur
|
||||
when these guarantees are broken. It does not however ensure that the compiler
|
||||
will never break these guarantees. It is therefore still possible to ship a
|
||||
broken compiler which fails on valid inputs.
|
||||
|
||||
Drawback: it is necessary for every compiler written using such guards to prove
|
||||
that the guards are never raised.
|
||||
|
||||
|
||||
Features
|
||||
========
|
||||
|
||||
* GC:
|
||||
* Group nodes by SCC
|
||||
* Two kinds of "indices" pointers:
|
||||
* index within the current strongly-connected component
|
||||
* direct pointer to a descendant SCC + index within it
|
||||
* To limit the waste when there is an SCC not containing nodes of a given type,
|
||||
do not use a fixed tuple of vectors of nodes. Instead, use a "list with possible omissions".
|
||||
Problem: the size of the fully-expanded type in TR is O(2ⁿ) for these.
|
||||
Either:
|
||||
* use casts
|
||||
* pay the compile-time price of a huge type (not feasible with large N)
|
||||
* pay the run-time price of bloated components (feasible but costly with large N)
|
||||
* use a case→ function, which returns the empty vector as a fallback. With pure functions, this could be doable.
|
||||
* Problem: generating all the possible functions means O(2^n) templates for closures that may be used at
|
||||
run-time
|
||||
* Otherwise, generate one closure over 1 array, one closure over 2 arrays, one over 3 arrays, etc.
|
||||
and also close over some markers indicating to which "real" arrays these correspond.
|
||||
This means O(2n) space usage worst-case.
|
||||
Problem again: the construction function for such a case→ while minimizing the number of values closed on
|
||||
has a large O(2^n) type too.
|
||||
* typed clojure has typed heterogeneous maps https://github.com/clojure/core.typed/wiki/Types#heterogeneous-maps
|
||||
* In theory it could be possible to give hints to the GC,
|
||||
but Racket's GC does not offer that possibility.
|
||||
|
||||
GC Implementation:
|
||||
* Must be optional
|
||||
* Initially, all nodes within a single component, all indices are of the "slef + index" kind.
|
||||
* Use tarjan's algorithm
|
||||
* group nodes by SCC
|
||||
Update references to nodes in the same SCC, using just an index
|
||||
Update references to nodes in "lower" SCCs, using a pointer to the SCC + an index.
|
||||
* Due to the higher memory cost (+ 1 reference for references to other SCCs),
|
||||
and the poor set of options for implementation (cast, exponential size of type, or large memory usage)
|
||||
we will not implement the GC.
|
||||
|
||||
We argue that in most cases it would not be useful, as compilers will normally work on the whole graph, and
|
||||
not on a subgraph. In the rare case where only part of a graph is needed, applying the graph-level identity
|
||||
transformation to the nodes of interest would effectively copy them and the nodes reachable from these new roots,
|
||||
thereby allowing the original graph to be freed.
|
||||
|
||||
* Invariants
|
||||
* Scope of the invariants:
|
||||
* Input contracts, types and structural properties
|
||||
* Output contracts, types and structural properties
|
||||
* Transformation invariants (relate the input and output graphs)
|
||||
* Time of verification:
|
||||
* Run-time
|
||||
Should be easy enough to implement: Add a define-graph-invariant form, recognize these options, and check
|
||||
them at run-time. Implemented as some sorts of contracts.
|
||||
* Compile-time
|
||||
* Node types
|
||||
* Statically-enforced structural invariants at the level of node types
|
||||
(e.g. disallow cycles in the types, to ensure there are no cycles in the instance)
|
||||
* Macros can be used to generate code which is known to be correct
|
||||
e.g. paths
|
||||
* Concern: static "by construction" guarantees may interfere with each other, if they fill in some nodes,
|
||||
e.g. a "no cycles starting from this node" constraint would not work as expected if a "backwards link"
|
||||
is filled in afterwards. We probably need to hardcode a set of constraints which know about eachother
|
||||
and about the potential interactions.
|
||||
* Conserve well-scopedness within a transition: pass in nodes flagged with a ∀ type, and check
|
||||
that the output contains that flag.
|
||||
* PHOAS
|
||||
* Specification
|
||||
* Invariants specified in the graph type
|
||||
* Transformation invariants specified on the graph creation code
|
||||
* Checks (run-time or the various compile-time mechanisms) are specified in the graph creation code
|
||||
The graph creation code must enforce all invariants within the type
|
||||
That way, it is guaranteed that any instance of the graph type satisfies its invariants, either by
|
||||
construction, or as a guard at the end of the construction.
|
||||
|
||||
* Automatic generation of mappings
|
||||
* when there is no mapping taking an old node as an input, a mapping is automatically generated.
|
||||
The mapping simply translates the old node to the new node type, and recursively transforms its fields,
|
||||
traversing lists etc.
|
||||
* When there is a mapping with more than one argument, then no mapping is auto-generated for that input node type,
|
||||
and instead calls to the mapping must be explicit (i.e. can't return the old node type).
|
||||
* This means that we have a mechanism before the actual core graph macro, which checks and decides which mappings
|
||||
to auto-generate.
|
||||
* We also have a mechanism for auto-calling transformations on input node types
|
||||
* Possibility to escape this, in order to actually insert a reference to the old graph?
|
||||
* Some notation in the type, to indicate that it's "protected" in some way?
|
||||
* Some wrapper indicating that it should merely be unwrapped, not processed? (I think that's better).
|
||||
|
||||
* Structural node equality
|
||||
* Would be nice to coalesce nodes which are equal? (i.e. hash consing)
|
||||
so that any two nodes which are equal? within the same graph have the same index.
|
||||
I suppose this would be rather costly: O(n log n) comparisons, with each comparison potentially
|
||||
costly, in principle. If we cached results, we could achieve a better run-time in practice, and
|
||||
perhaps a better theoretical complexity if we handled cycles ourselves.
|
||||
* The general algorithm when there are no unordered sets is deterministic finite automaton minimization
|
||||
* The general algorithm when there are unordered sets is nondeterministic finite automaton minimization
|
||||
* We could cache all calls to equal? on two nodes for a limited dynamic scope.
|
||||
* If we have this, then we can, for comparisons within the same graph, quickly return #t or #f based on eq?
|
||||
* Alpha-equivalence comparisons
|
||||
(i.e. ignore the actual values of some fields, except for constraining the shape of the graph)
|
||||
Possibility: create values which are unique within the graph, but are ignored when comparing
|
||||
nodes from different graphs.
|
||||
I'm not sure whether plainly erasing the information won't be enough, for a weaker form of alpha-equivalence?
|
||||
* Alpha-equivalence can't easily be implemented atop equal?, dropping it for now.
|
||||
It's not extremely useful anyway, as thanks to the full-blown graph representation, we are likely to
|
||||
discard names early on (keeping them just for printing / debuggin purposes).
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
* Coloring: the existing graph library for Racket has some coloring algorithms:
|
||||
http://docs.racket-lang.org/graph/index.html#%28def._%28%28lib._graph%2Fmain..rkt%29._coloring%2Fgreedy%29%29
|
||||
Maybe we can build a wrapper for those?
|
||||
|
|
@ -1,99 +0,0 @@
|
|||
* Invariants
|
||||
* Scope of the invariants:
|
||||
* Input contracts, types and structural properties
|
||||
* Output contracts, types and structural properties
|
||||
* Transformation invariants (relate the input and output graphs)
|
||||
* Time of verification:
|
||||
* Run-time
|
||||
Should be easy enough to implement: Add a define-graph-invariant form, recognize these options, and check
|
||||
them at run-time. Implemented as some sorts of contracts.
|
||||
* Compile-time
|
||||
* Node types
|
||||
* Statically-enforced structural invariants at the level of node types
|
||||
(e.g. disallow cycles in the types, to ensure there are no cycles in the instance)
|
||||
* Macros can be used to generate code which is known to be correct
|
||||
e.g. paths
|
||||
* Concern: static "by construction" guarantees may interfere with each other, if they fill in some nodes,
|
||||
e.g. a "no cycles starting from this node" constraint would not work as expected if a "backwards link"
|
||||
is filled in afterwards. We probably need to hardcode a set of constraints which know about eachother
|
||||
and about the potential interactions.
|
||||
* Conserve well-scopedness within a transition: pass in nodes flagged with a ∀ type, and check
|
||||
that the output contains that flag. Potentially out-of-scope fields in the input do not have the flag.
|
||||
* PHOAS
|
||||
* Specification
|
||||
* Invariants specified in the graph type
|
||||
* Transformation invariants specified on the graph creation code
|
||||
* Checks (run-time or the various compile-time mechanisms) are specified in the graph creation code
|
||||
The graph creation code must enforce all invariants within the type
|
||||
That way, it is guaranteed that any instance of the graph type satisfies its invariants, either by
|
||||
construction, or as a guard at the end of the construction.
|
||||
|
||||
; The body should produce a function of type (→ (Listof Nodeᵢ) … Boolean)
|
||||
; The body should also return an indication about which invariants it ensures. Maybe use {~seq #:ensures (invariant-name inariant-arg …)} …
|
||||
however this does not allow the body to perform some minimal amount of rewriting on the "ensures" options.
|
||||
(define-syntax/parse (define-graph-contract (name g-descriptor arg …) . body)
|
||||
#'(define-syntax name
|
||||
(graph-contract
|
||||
(λ (g-descriptor arg …) . body))))
|
||||
|
||||
;; TODO: find a way to translate this to a type, with subtyping for weaker invariants.
|
||||
;; The type only serves to testify that the invariant was statically enforced or dynamically checked at construction, it does not actually encode the property using the type system.
|
||||
(struct invariants-wrapper ()) ;; Use a private struct to prevent forging of the invariants aggregated in a case→ (since it is never executed, any non-terminating λ could otherwise be supplied).
|
||||
(define-for-syntax invariant-introducer
|
||||
(make-syntax-introducer))
|
||||
;; the body should return the syntax for a type, such that less precise invariants are supertypes of that type.
|
||||
(define-syntax/parse (define-graph-invariant (name g-descriptor arg …) . body)
|
||||
#'(define-syntax name
|
||||
(graph-invariant
|
||||
(λ (g-descriptor arg …) . body))))
|
||||
|
||||
The type of a graph node with the invariants inv₁ … invₙ on the graph must include an extra dummy field with type
|
||||
(invariants-wrapper
|
||||
(case (→ inv₁ inv-arg … #t)
|
||||
…
|
||||
(→ invₙ inv-arg … #t)))
|
||||
|
||||
The invariant arguments can be symbols, to indicate node types or field names.
|
||||
|
||||
Concern: invariants on a graph may not have the same semantics if the graph has more or fewer nodes?
|
||||
|
||||
* Automatic generation of mappings
|
||||
* when there is no mapping taking an old node as an input, a mapping is automatically generated.
|
||||
The mapping simply translates the old node to the new node type, and recursively transforms its fields,
|
||||
traversing lists etc.
|
||||
* When there is a mapping with more than one argument, then no mapping is auto-generated for that input node type,
|
||||
and instead calls to the mapping must be explicit (i.e. can't return the old node type).
|
||||
* This means that we have a mechanism before the actual core graph macro, which checks and decides which mappings
|
||||
to auto-generate.
|
||||
* We also have a mechanism for auto-calling transformations on input node types
|
||||
* Possibility to escape this, in order to actually insert a reference to the old graph?
|
||||
* Some notation in the type, to indicate that the output should be an "old" node here
|
||||
* In the rare case where we have an (U (Old nd) nd), in the mapping use some (old v) wrapper
|
||||
indicating that the returned it should merely be unwrapped, not processed.
|
||||
|
||||
(define-syntax define-graph-type
|
||||
(syntax-parser
|
||||
[(_ _name [_nodeᵢ [_fieldᵢⱼ :colon _τᵢⱼ] …] …)
|
||||
;; save the graph type metadata
|
||||
]))
|
||||
|
||||
(define-syntax define-graph-transformer
|
||||
(syntax-parser
|
||||
[(_ _name graph-type)
|
||||
;; TODO
|
||||
]))
|
||||
|
||||
* Structural node equality
|
||||
* Would be nice to coalesce nodes which are equal? (i.e. hash consing)
|
||||
so that any two nodes which are equal? within the same graph have the same index.
|
||||
I suppose this would be rather costly: O(n log n) comparisons, with each comparison potentially
|
||||
costly, in principle. If we cached results, we could achieve a better run-time in practice, and
|
||||
perhaps a better theoretical complexity if we handled cycles ourselves.
|
||||
* The general algorithm when there are no unordered sets is deterministic finite automaton minimization
|
||||
* The general algorithm when there are unordered sets is nondeterministic finite automaton minimization
|
||||
* We could cache all calls to equal? on two nodes for a limited dynamic scope.
|
||||
* If we have this, then we can, for comparisons within the same graph, quickly return #t or #f based on eq?
|
||||
|
||||
* Coloring: the existing graph library for Racket has some coloring algorithms:
|
||||
http://docs.racket-lang.org/graph/index.html#%28def._%28%28lib._graph%2Fmain..rkt%29._coloring%2Fgreedy%29%29
|
||||
Maybe we can build a wrapper for those?
|
||||
|
|
@ -1,118 +0,0 @@
|
|||
#lang aful/unhygienic hyper-literate type-expander/lang
|
||||
|
||||
@(require scribble-math)
|
||||
|
||||
@title[#:tag-prefix "utils"
|
||||
#:style manual-doc-style]{Utility math functions for binary tree
|
||||
manipulation}
|
||||
|
||||
@(chunks-toc-prefix
|
||||
'("(lib phc-graph/scribblings/phc-graph-implementation.scrbl)"
|
||||
"phc-graph/flexible-with"
|
||||
"utils"))
|
||||
|
||||
@defmodule[(lib "phc-graph/flexible-with-utils.hl.rkt")]
|
||||
|
||||
@(unless-preexpanding
|
||||
(require (for-label (submod ".."))))
|
||||
|
||||
@chunk[<*>
|
||||
(require (for-syntax racket/base))
|
||||
|
||||
(provide (for-syntax to-bits
|
||||
from-bits
|
||||
floor-log2
|
||||
ceiling-log2))
|
||||
|
||||
<to-bits>
|
||||
<from-bits>
|
||||
<floor-log2>
|
||||
<ceiling-log2>
|
||||
|
||||
(module* test racket/base
|
||||
(require (for-template (submod "..")))
|
||||
(require rackunit)
|
||||
<test-to-bits>
|
||||
<test-from-bits>)]
|
||||
|
||||
@defproc[(to-bits [n exact-nonnegative-integer?]) (listof boolean?)]{}
|
||||
|
||||
@CHUNK[<to-bits>
|
||||
; 1 => 1
|
||||
; 2 3 => 10 11
|
||||
;4 5 6 7 => 100 101 110 111
|
||||
;89 ab cd ef => 1000 1001 1010 1011 1100 1101 1110 1111
|
||||
|
||||
; 1 => ""
|
||||
; 2 3 => 0 1
|
||||
;4 5 6 7 => 00 01 10 11
|
||||
;89 ab cd ef => 000 001 010 011 100 101 110 111
|
||||
|
||||
; 0 => 0
|
||||
; 1 2 => 1 10
|
||||
;3 4 5 6 => 11 100 101 110
|
||||
;78 9a bc de => 111 1000 1001 1010 1011 1100 1101 1110
|
||||
|
||||
|
||||
(define-for-syntax (to-bits n)
|
||||
(reverse
|
||||
(let loop ([n n])
|
||||
(if (= n 0)
|
||||
null
|
||||
(let-values ([(q r) (quotient/remainder n 2)])
|
||||
(cons (if (= r 1) #t #f) (loop q)))))))]
|
||||
|
||||
@chunk[<test-to-bits>
|
||||
(check-equal? (to-bits 0) '())
|
||||
(check-equal? (to-bits 1) '(#t))
|
||||
(check-equal? (to-bits 2) '(#t #f))
|
||||
(check-equal? (to-bits 3) '(#t #t))
|
||||
(check-equal? (to-bits 4) '(#t #f #f))
|
||||
(check-equal? (to-bits 5) '(#t #f #t))
|
||||
(check-equal? (to-bits 6) '(#t #t #f))
|
||||
(check-equal? (to-bits 7) '(#t #t #t))
|
||||
(check-equal? (to-bits 8) '(#t #f #f #f))
|
||||
(check-equal? (to-bits 12) '(#t #t #f #f))
|
||||
(check-equal? (to-bits 1024) '(#t #f #f #f #f #f #f #f #f #f #f))]
|
||||
|
||||
@defproc[(from-bits [n (listof boolean?)]) exact-nonnegative-integer?]{}
|
||||
|
||||
@CHUNK[<from-bits>
|
||||
(define-for-syntax (from-bits b)
|
||||
(foldl (λ (bᵢ acc)
|
||||
(+ (* acc 2) (if bᵢ 1 0)))
|
||||
0
|
||||
b))]
|
||||
|
||||
@chunk[<test-from-bits>
|
||||
(check-equal? (from-bits '()) 0)
|
||||
(check-equal? (from-bits '(#t)) 1)
|
||||
(check-equal? (from-bits '(#t #f)) 2)
|
||||
(check-equal? (from-bits '(#t #t)) 3)
|
||||
(check-equal? (from-bits '(#t #f #f)) 4)
|
||||
(check-equal? (from-bits '(#t #f #t)) 5)
|
||||
(check-equal? (from-bits '(#t #t #f)) 6)
|
||||
(check-equal? (from-bits '(#t #t #t)) 7)
|
||||
(check-equal? (from-bits '(#t #f #f #f)) 8)
|
||||
(check-equal? (from-bits '(#t #t #f #f)) 12)
|
||||
(check-equal? (from-bits '(#t #f #f #f #f #f #f #f #f #f #f)) 1024)]
|
||||
|
||||
@defproc[(floor-log2 [n exact-positive-integer?])
|
||||
exact-nonnegative-integer?]{
|
||||
Exact computation of @${\lfloor\log_2(n)\rfloor}.
|
||||
}
|
||||
|
||||
@chunk[<floor-log2>
|
||||
(define-for-syntax (floor-log2 n)
|
||||
(if (<= n 1)
|
||||
0
|
||||
(add1 (floor-log2 (quotient n 2)))))]
|
||||
|
||||
@defproc[(ceiling-log2 [n exact-positive-integer?])
|
||||
exact-nonnegative-integer?]{
|
||||
Exact computation of @${\lceil\log_2(n)\rceil}.
|
||||
}
|
||||
|
||||
@chunk[<ceiling-log2>
|
||||
(define-for-syntax (ceiling-log2 n)
|
||||
(floor-log2 (sub1 (* n 2))))]
|
||||
|
|
@ -1,365 +0,0 @@
|
|||
#lang aful/unhygienic hyper-literate type-expander/lang
|
||||
|
||||
@title[#:style manual-doc-style ;#:style (with-html5 manual-doc-style)
|
||||
#:tag "flexible-with"
|
||||
#:tag-prefix "phc-graph/flexible-with"]{Flexible functional
|
||||
modification and extension of records}
|
||||
|
||||
@(chunks-toc-prefix
|
||||
'("(lib phc-graph/scribblings/phc-graph-implementation.scrbl)"
|
||||
"phc-graph/flexible-with"))
|
||||
|
||||
@section{Type of a tree-record, with a hole}
|
||||
|
||||
@CHUNK[<tree-type-with-replacement>
|
||||
(define-for-syntax (tree-type-with-replacement n last τ*)
|
||||
(define-values (next mod) (quotient/remainder n 2))
|
||||
(cond [(null? τ*) last]
|
||||
[(= mod 0)
|
||||
(tree-type-with-replacement next
|
||||
#`(Pairof #,last #,(car τ*))
|
||||
(cdr τ*))]
|
||||
[else
|
||||
(tree-type-with-replacement next
|
||||
#`(Pairof #,(car τ*) #,last)
|
||||
(cdr τ*))]))]
|
||||
|
||||
@section{Functionally updating a tree-record}
|
||||
|
||||
@subsection{Adding and modifying fields}
|
||||
|
||||
Since we only deal with functional updates of immutable records, modifying a
|
||||
field does little more than discarding the old value, and injecting the new
|
||||
value instead into the new, updated record.
|
||||
|
||||
Adding a new field is done using the same exact operation: missing fields are
|
||||
denoted by a special value, @racket['NONE], while present fields are
|
||||
represented as instances of the polymorphic struct @racket[(Some T)]. Adding a
|
||||
new field is therefore as simple as discarding the old @racket['NONE] marker,
|
||||
and replacing it with the new value, wrapped with @racket[Some]. A field
|
||||
update would instead discard the old instance of @racket[Some], and replace it
|
||||
with a new one.
|
||||
|
||||
@CHUNK[<make-replace-in-tree-body>
|
||||
(if (= i 1)
|
||||
#'(delay/pure/stateless replacement)
|
||||
(let* ([bits (to-bits i)]
|
||||
[next (from-bits (cons #t (cddr bits)))]
|
||||
[mod (cadr bits)])
|
||||
(define/with-syntax next-id (vector-ref low-names (sub1 next)))
|
||||
(if mod
|
||||
#`(replace-right (inst next-id #,@τ*-limited+T-next)
|
||||
tree-thunk
|
||||
replacement)
|
||||
#`(replace-left (inst next-id #,@τ*-limited+T-next)
|
||||
tree-thunk
|
||||
replacement))))]
|
||||
|
||||
@CHUNK[<define-replace-in-tree>
|
||||
(: replace-right (∀ (A B C R) (→ (→ (Promise B) R (Promise C))
|
||||
(Promise (Pairof A B))
|
||||
R
|
||||
(Promise (Pairof A C)))))
|
||||
(define-pure/stateless
|
||||
#:∀ (A B C R)
|
||||
(replace-right [next-id : (→ (Promise B) R (Promise C))]
|
||||
[tree-thunk : (Promise (Pairof A B))]
|
||||
[replacement : R])
|
||||
(delay/pure/stateless
|
||||
(let ([tree (force tree-thunk)])
|
||||
(let ([left-subtree (car tree)]
|
||||
[right-subtree (cdr tree)])
|
||||
(cons left-subtree
|
||||
(force (next-id (delay/pure/stateless right-subtree)
|
||||
replacement)))))))
|
||||
(: replace-left (∀ (A B C R) (→ (→ (Promise A) R (Promise C))
|
||||
(Promise (Pairof A B))
|
||||
R
|
||||
(Promise (Pairof C B)))))
|
||||
(define-pure/stateless
|
||||
#:∀ (A B C R)
|
||||
(replace-left [next-id : (→ (Promise A) R (Promise C))]
|
||||
[tree-thunk : (Promise (Pairof A B))]
|
||||
[replacement : R])
|
||||
(delay/pure/stateless
|
||||
(let ([tree (force tree-thunk)])
|
||||
(let ([left-subtree (car tree)]
|
||||
[right-subtree (cdr tree)])
|
||||
(cons (force (next-id (delay/pure/stateless left-subtree)
|
||||
replacement))
|
||||
right-subtree)))))
|
||||
|
||||
(define-for-syntax (define-replace-in-tree low-names names rm-names τ* i depth)
|
||||
(define/with-syntax name (vector-ref names (sub1 i)))
|
||||
(define/with-syntax rm-name (vector-ref rm-names (sub1 i)))
|
||||
(define/with-syntax low-name (vector-ref low-names (sub1 i)))
|
||||
(define/with-syntax tree-type-with-replacement-name (gensym 'tree-type-with-replacement))
|
||||
(define/with-syntax tree-replacement-type-name (gensym 'tree-replacement-type))
|
||||
(define τ*-limited (take τ* depth))
|
||||
(define τ*-limited+T-next (if (= depth 0)
|
||||
(list #'T)
|
||||
(append (take τ* (sub1 depth)) (list #'T))))
|
||||
#`(begin
|
||||
(provide name rm-name)
|
||||
(define-type (tree-type-with-replacement-name #,@τ*-limited T)
|
||||
(Promise #,(tree-type-with-replacement i #'T τ*-limited)))
|
||||
|
||||
(: low-name
|
||||
(∀ (#,@τ*-limited T)
|
||||
(→ (tree-type-with-replacement-name #,@τ*-limited Any)
|
||||
T
|
||||
(tree-type-with-replacement-name #,@τ*-limited T))))
|
||||
(define-pure/stateless
|
||||
#:∀ (#,@τ*-limited T)
|
||||
(low-name [tree-thunk : (tree-type-with-replacement-name #,@τ*-limited Any)]
|
||||
[replacement : T])
|
||||
: (Promise #,(tree-type-with-replacement i #'T τ*-limited))
|
||||
#,<make-replace-in-tree-body>)
|
||||
|
||||
(: name
|
||||
(∀ (#,@τ*-limited T)
|
||||
(→ (tree-type-with-replacement-name #,@τ*-limited Any)
|
||||
T
|
||||
(tree-type-with-replacement-name #,@τ*-limited (Some T)))))
|
||||
(define (name tree-thunk replacement)
|
||||
(low-name tree-thunk (Some replacement)))
|
||||
|
||||
(: rm-name
|
||||
(∀ (#,@τ*-limited)
|
||||
(→ (tree-type-with-replacement-name #,@τ*-limited (Some Any))
|
||||
(tree-type-with-replacement-name #,@τ*-limited 'NONE))))
|
||||
(define (rm-name tree-thunk)
|
||||
(low-name tree-thunk 'NONE))))]
|
||||
|
||||
@section{Auxiliary values}
|
||||
|
||||
The following sections reuse a few values which are derived from the list of
|
||||
fields:
|
||||
|
||||
@CHUNK[<utils>
|
||||
(define all-fields #'(field …))
|
||||
(define depth-above (ceiling-log2 (length (syntax->list #'(field …)))))
|
||||
(define offset (expt 2 depth-above))
|
||||
(define i*-above (range 1 (expt 2 depth-above)))
|
||||
(define names (list->vector
|
||||
(append (map (λ (i) (format-id #'here "-with-~a" i))
|
||||
i*-above)
|
||||
(stx-map (λ (f) (format-id f "with-~a" f))
|
||||
#'(field …)))))
|
||||
(define rm-names (list->vector
|
||||
(append (map (λ (i) (format-id #'here "-without-~a" i))
|
||||
i*-above)
|
||||
(stx-map (λ (f) (format-id f "without-~a" f))
|
||||
#'(field …)))))
|
||||
(define low-names (list->vector
|
||||
(append (map (λ (i) (format-id #'here "-u-with-~a" i))
|
||||
i*-above)
|
||||
(stx-map (λ (f) (format-id f "u-with-~a" f))
|
||||
#'(field …)))))]
|
||||
|
||||
@section{Type of a tree-record}
|
||||
|
||||
@CHUNK[<τ-tree-with-fields>
|
||||
(define-for-syntax (τ-tree-with-fields struct-fields fields)
|
||||
(define/with-syntax (struct-field …) struct-fields)
|
||||
(define/with-syntax (field …) fields)
|
||||
<utils>
|
||||
;; Like in convert-from-struct
|
||||
(define lookup
|
||||
(make-free-id-table
|
||||
(for/list ([n (in-syntax all-fields)]
|
||||
[i (in-naturals)])
|
||||
(cons n (+ i offset)))))
|
||||
(define fields+indices
|
||||
(sort (stx-map #λ(cons % (free-id-table-ref lookup %))
|
||||
#'(struct-field …))
|
||||
<
|
||||
#:key cdr))
|
||||
|
||||
(define up (* offset 2))
|
||||
|
||||
;; Like in convert-fields, but with Pairof
|
||||
(define (f i)
|
||||
;(displayln (list i '/ up (syntax->datum #`#,fields+indices)))
|
||||
(if (and (pair? fields+indices) (= i (cdar fields+indices)))
|
||||
(begin0
|
||||
`(Some ,(caar fields+indices))
|
||||
(set! fields+indices (cdr fields+indices)))
|
||||
(if (>= (* i 2) up) ;; DEPTH
|
||||
''NONE
|
||||
(begin
|
||||
`(Pairof ,(f (* i 2))
|
||||
,(f (add1 (* i 2))))))))
|
||||
(f 1))]
|
||||
|
||||
@section{Conversion to and from record-trees}
|
||||
|
||||
@CHUNK[<define-struct↔tree>
|
||||
(define-for-syntax (define-struct↔tree
|
||||
offset all-fields τ* struct-name fields)
|
||||
(define/with-syntax (field …) fields)
|
||||
(define/with-syntax fields→tree-name
|
||||
(format-id struct-name "~a→tree" struct-name))
|
||||
(define/with-syntax tree→fields-name
|
||||
(format-id struct-name "tree→~a" struct-name))
|
||||
(define lookup
|
||||
(make-free-id-table
|
||||
(for/list ([n (in-syntax all-fields)]
|
||||
[i (in-naturals)])
|
||||
(cons n (+ i offset)))))
|
||||
(define fields+indices
|
||||
(sort (stx-map #λ(cons % (free-id-table-ref lookup %))
|
||||
fields)
|
||||
<
|
||||
#:key cdr))
|
||||
#`(begin
|
||||
(: fields→tree-name (∀ (field …)
|
||||
(→ field …
|
||||
(Promise #,(τ-tree-with-fields #'(field …)
|
||||
all-fields)))))
|
||||
(define (fields→tree-name field …)
|
||||
(delay/pure/stateless
|
||||
#,(convert-fields (* offset 2) fields+indices)))
|
||||
|
||||
(: tree→fields-name (∀ (field …)
|
||||
(→ (Promise #,(τ-tree-with-fields #'(field …)
|
||||
all-fields))
|
||||
(Values field …))))
|
||||
(define (tree→fields-name tree-thunk)
|
||||
(define tree (force tree-thunk))
|
||||
#,(convert-back-fields (* offset 2) fields+indices))))]
|
||||
|
||||
@subsection{Creating a new tree-record}
|
||||
|
||||
@CHUNK[<convert-fields>
|
||||
(define-for-syntax (convert-fields up fields+indices)
|
||||
;(displayln fields+indices)
|
||||
(define (f i)
|
||||
;(displayln (list i '/ up (syntax->datum #`#,fields+indices)))
|
||||
(if (and (pair? fields+indices) (= i (cdar fields+indices)))
|
||||
(begin0
|
||||
`(Some ,(caar fields+indices))
|
||||
(set! fields+indices (cdr fields+indices)))
|
||||
(if (>= (* i 2) up) ;; DEPTH
|
||||
''NONE
|
||||
`(cons ,(f (* i 2))
|
||||
,(f (add1 (* i 2)))))))
|
||||
;(displayln (syntax->datum #`#,(f 1)))
|
||||
(f 1))]
|
||||
|
||||
|
||||
@subsection{Extracting all the fields from a tree-record}
|
||||
|
||||
We traverse the tree in preorder, and accumulate definitions naming the
|
||||
interesting subparts of the trees (those where there are fields).
|
||||
|
||||
@CHUNK[<convert-back-fields>
|
||||
(define-for-syntax (convert-back-fields up fields+indices)
|
||||
(define result '())
|
||||
(define definitions '())
|
||||
(define (f i t)
|
||||
(if (and (pair? fields+indices) (= i (cdar fields+indices)))
|
||||
(begin0
|
||||
(begin
|
||||
(set! result (cons #`(Some-v #,t) result))
|
||||
#t)
|
||||
(set! fields+indices (cdr fields+indices)))
|
||||
(if (>= (* i 2) up) ;; DEPTH
|
||||
#f
|
||||
(let* ([left-t (string->symbol
|
||||
(format "subtree-~a" (* i 2)))]
|
||||
[right-t (string->symbol
|
||||
(format "subtree-~a" (add1 (* i 2))))]
|
||||
[left (f (* i 2) left-t)]
|
||||
[right (f (add1 (* i 2)) right-t)])
|
||||
(cond
|
||||
[(and left right)
|
||||
(set! definitions (cons #`(define #,left-t (car #,t))
|
||||
definitions))
|
||||
(set! definitions (cons #`(define #,right-t (cdr #,t))
|
||||
definitions))
|
||||
#t]
|
||||
[left
|
||||
(set! definitions (cons #`(define #,left-t (car #,t))
|
||||
definitions))
|
||||
#t]
|
||||
[right
|
||||
(set! definitions (cons #`(define #,right-t (cdr #,t))
|
||||
definitions))
|
||||
#t]
|
||||
[else
|
||||
#f])))))
|
||||
(f 1 #'tree)
|
||||
#`(begin #,@definitions (values . #,(reverse result))))]
|
||||
|
||||
@section{Defining the converters and accessors for each known record type}
|
||||
|
||||
@CHUNK[<define-trees>
|
||||
(define-for-syntax (define-trees stx)
|
||||
(syntax-case stx ()
|
||||
[(bt-fields-id (field …) [struct struct-field …] …)
|
||||
(let ()
|
||||
<utils>
|
||||
(define ∀-types (map #λ(format-id #'here "τ~a" %)
|
||||
(range (add1 depth-above))))
|
||||
(define total-nb-functions (vector-length names))
|
||||
<define-trees-result>)]))]
|
||||
|
||||
@CHUNK[<bt-fields-type>
|
||||
(define-for-syntax (bt-fields-type fields)
|
||||
(λ (stx)
|
||||
(syntax-case stx ()
|
||||
[(_ . fs)
|
||||
#`(∀ fs (Promise #,(τ-tree-with-fields #'fs
|
||||
fields)))])))]
|
||||
|
||||
@CHUNK[<define-trees-result>
|
||||
#`(begin
|
||||
(define-type-expander bt-fields-id
|
||||
(bt-fields-type #'#,(syntax-local-introduce #'(field …))))
|
||||
#,@(map #λ(define-replace-in-tree low-names names rm-names ∀-types % (floor-log2 %))
|
||||
(range 1 (add1 total-nb-functions)))
|
||||
#;#,@(map #λ(define-remove-in-tree rm-names ∀-types % (floor-log2 %))
|
||||
(range 1 (add1 total-nb-functions)))
|
||||
#,@(map #λ(define-struct↔tree
|
||||
offset all-fields ∀-types %1 %2)
|
||||
(syntax->list #'(struct …))
|
||||
(syntax->list #'([struct-field …] …))))]
|
||||
|
||||
@subsection{Putting it all together}
|
||||
|
||||
@chunk[<maybe>
|
||||
(struct (T) Some ([v : T]) #:transparent)
|
||||
(define-type (Maybe T) (U (Some T) 'NONE))]
|
||||
|
||||
@chunk[<*>
|
||||
(require delay-pure
|
||||
"flexible-with-utils.hl.rkt"
|
||||
(for-syntax (rename-in racket/base [... …])
|
||||
syntax/stx
|
||||
racket/syntax
|
||||
racket/list
|
||||
syntax/id-table
|
||||
racket/sequence)
|
||||
(for-meta 2 racket/base))
|
||||
|
||||
(provide (for-syntax define-trees)
|
||||
;; For tests:
|
||||
(struct-out Some)
|
||||
|
||||
;;DEBUG:
|
||||
(for-syntax τ-tree-with-fields)
|
||||
)
|
||||
|
||||
<maybe>
|
||||
<tree-type-with-replacement>
|
||||
<define-replace-in-tree>
|
||||
;<define-remove-in-tree>
|
||||
<convert-fields>
|
||||
<convert-back-fields>
|
||||
<τ-tree-with-fields>
|
||||
<define-struct↔tree>
|
||||
<define-trees>
|
||||
<bt-fields-type>]
|
||||
|
||||
@include-section[(submod "flexible-with-utils.hl.rkt" doc)]
|
||||
|
|
@ -1,91 +0,0 @@
|
|||
#lang racket
|
||||
|
||||
(require racket/struct
|
||||
;; TODO: move delay-pure/private/immutable-struct to a separate package
|
||||
delay-pure/private/immutable-struct) ;; for immutable-struct? below.
|
||||
|
||||
(provide free-id-tree=?
|
||||
free-id-tree-hash-code
|
||||
free-id-tree-secondary-hash-code
|
||||
|
||||
free-id-tree-table?
|
||||
immutable-free-id-tree-table?
|
||||
mutable-free-id-tree-table?
|
||||
weak-free-id-tree-table?
|
||||
make-immutable-free-id-tree-table
|
||||
make-mutable-free-id-tree-table
|
||||
make-weak-free-id-tree-table)
|
||||
|
||||
;; Contract:
|
||||
;; TODO: move to tr-immutable
|
||||
(define isyntax/c
|
||||
(flat-rec-contract isyntax
|
||||
(or/c boolean?
|
||||
char?
|
||||
number?
|
||||
keyword?
|
||||
null?
|
||||
(and/c string? immutable?)
|
||||
symbol?
|
||||
(box/c isyntax #:immutable #t)
|
||||
(cons/c isyntax isyntax)
|
||||
(vectorof isyntax #:immutable #t)
|
||||
(syntax/c isyntax)
|
||||
(and/c immutable-struct?
|
||||
prefab-struct-key
|
||||
(λ (v)
|
||||
(andmap isyntax/c (struct->list v)))))))
|
||||
|
||||
(define/contract (free-id-tree=? a b [r equal?])
|
||||
(-> isyntax/c isyntax/c boolean?)
|
||||
(define (rec=? a b) (free-id-tree=? a b r))
|
||||
(cond
|
||||
[(identifier? a) (and (identifier? b)
|
||||
(free-identifier=? a b))]
|
||||
[(syntax? a) (and (syntax? b)
|
||||
(rec=? (syntax-e a)
|
||||
(syntax-e b)))]
|
||||
[(pair? a) (and (pair? b)
|
||||
(rec=? (car a) (car b))
|
||||
(rec=? (cdr a) (cdr b)))]
|
||||
[(vector? a) (and (vector? b)
|
||||
(rec=? (vector->list a)
|
||||
(vector->list b)))]
|
||||
[(box? a) (and (box? b)
|
||||
(rec=? (unbox a)
|
||||
(unbox b)))]
|
||||
[(prefab-struct-key a)
|
||||
=> (λ (a-key)
|
||||
(let ([b-key (prefab-struct-key b)])
|
||||
(and (equal? a-key b-key)
|
||||
(rec=? (struct->list a)
|
||||
(struct->list b)))))]
|
||||
[(null? a) (null? b)]
|
||||
[else (equal? a b)]))
|
||||
|
||||
(define/contract ((free-id-tree-hash hc) a)
|
||||
(-> (-> any/c fixnum?) (-> isyntax/c fixnum?))
|
||||
(define rec-hash (free-id-tree-hash hc))
|
||||
(cond
|
||||
[(identifier? a) (hc (syntax-e #'a))]
|
||||
[(syntax? a) (rec-hash (syntax-e a))]
|
||||
[(pair? a) (hc (cons (rec-hash (car a))
|
||||
(rec-hash (cdr a))))]
|
||||
[(vector? a) (hc (list->vector (map rec-hash (vector->list a))))]
|
||||
[(box? a) (hc (box (rec-hash (unbox a))))]
|
||||
[(prefab-struct-key a)
|
||||
=> (λ (a-key)
|
||||
(hc (apply make-prefab-struct a-key
|
||||
(rec-hash (struct->list a)))))]
|
||||
[else (hc a)]))
|
||||
|
||||
(define free-id-tree-hash-code
|
||||
(free-id-tree-hash equal-hash-code))
|
||||
(define free-id-tree-secondary-hash-code
|
||||
(free-id-tree-hash equal-secondary-hash-code))
|
||||
|
||||
(define-custom-hash-types free-id-tree-table
|
||||
#:key? syntax?
|
||||
free-id-tree=?
|
||||
free-id-tree-hash-code
|
||||
free-id-tree-secondary-hash-code)
|
||||
|
|
@ -1,347 +0,0 @@
|
|||
#lang hyper-literate racket #:no-auto-require
|
||||
|
||||
@require[scribble-math
|
||||
scribble-enhanced/doc
|
||||
"notations.rkt"
|
||||
(for-label racket)]
|
||||
|
||||
@title[#:style (with-html5 manual-doc-style)
|
||||
#:tag "graph-info"
|
||||
#:tag-prefix "phc-graph/graph-info"]{Compile-time graph metadata}
|
||||
|
||||
@(chunks-toc-prefix
|
||||
'("(lib phc-graph/scribblings/phc-graph-implementation.scrbl)"
|
||||
"phc-graph/graph-info"))
|
||||
|
||||
We define here the compile-time metadata describing a graph type.
|
||||
|
||||
@section{Graph type information}
|
||||
|
||||
The type of a graph is actually the type of its constituent nodes. The node
|
||||
types may be polymorphic in the @racket[_tvars] type variables. The root node
|
||||
name and the order of the nodes are purely indicative here, as a reference to
|
||||
any node in the graph instance would be indistinguishable from a graph rooted
|
||||
in that node type.
|
||||
|
||||
The @racket[_invariants] are not enforced by the node types. Instead, the node
|
||||
types just include the invariant type as a witness (inside the @racket[raw]
|
||||
field). The invariant is enforced either by construction, or with a run-time
|
||||
check performed during the graph creation.
|
||||
|
||||
@chunk[<graph-info>
|
||||
(struct+/contract graph-info
|
||||
([name identifier?]
|
||||
[tvars (listof identifier?)]
|
||||
[root-node identifier?]
|
||||
[node-order (listof identifier?)]
|
||||
[nodes (hash/c symbol? node-info? #:immutable #t)]
|
||||
[invariants (set/c invariant-info? #:kind 'immutable #:cmp 'equal)])
|
||||
#:transparent
|
||||
#:methods gen:custom-write
|
||||
[(define write-proc (struct-printer 'graph-info))]
|
||||
#:property prop:custom-print-quotable 'never)]
|
||||
|
||||
@;{
|
||||
Since sets created with @racket[set] cannot be used within syntax objects
|
||||
(they cannot be marshalled into compiled code), we fake sets using hashes with
|
||||
empty values:
|
||||
|
||||
@chunk[<hash-set/c>
|
||||
(provide hash-set/c)
|
||||
(define/contract (hash-set/c elem/c
|
||||
#:kind [kind 'dont-care]
|
||||
#:cmp [cmp 'dont-care])
|
||||
(->* (chaperone-contract?)
|
||||
(#:kind (or/c 'dont-care 'immutable 'mutable
|
||||
'weak 'mutable-or-weak)
|
||||
#:cmp (or/c 'dont-care 'equal 'eqv 'eq))
|
||||
contract?)
|
||||
(define immutable
|
||||
(case kind
|
||||
[(immutable) #t]
|
||||
[(dont-care) 'dont-care]
|
||||
[else #f]))
|
||||
(define h (hash/c elem/c
|
||||
null?
|
||||
#:immutable immutable))
|
||||
(define cmp-contracts
|
||||
(case cmp
|
||||
[(dont-care) empty]
|
||||
[(equal) (list hash-equal?)]
|
||||
[(eqv) (list hash-eqv?)]
|
||||
[(eq) (list hash-eq?)]))
|
||||
(define weak-contracts
|
||||
(case kind
|
||||
[(weak) (list hash-weak?)]
|
||||
;; This is redundant: the mutable check is already included above
|
||||
[(mutable-or-weak) (list (or/c hash-weak? (not/c immutable?)))]
|
||||
[(dont-care) empty]
|
||||
[else (list (not/c hash-weak?))]))
|
||||
(if (empty? (append cmp-contracts weak-contracts))
|
||||
h
|
||||
(apply and/c (append (list h) cmp-contracts weak-contracts))))]
|
||||
|
||||
@chunk[<hash-set/c>
|
||||
(provide equal-hash-set/c)
|
||||
(define/contract (equal-hash-set/c elem/c
|
||||
#:kind [kind 'dont-care])
|
||||
(->* (chaperone-contract?)
|
||||
(#:kind (or/c 'dont-care 'immutable 'mutable
|
||||
'weak 'mutable-or-weak))
|
||||
contract?)
|
||||
(hash-set/c elem/c #:kind kind #:cmp 'equal))]
|
||||
|
||||
@chunk[<hash-set/c>
|
||||
(provide list->equal-hash-set)
|
||||
(define/contract (list->equal-hash-set l)
|
||||
(-> (listof any/c) (equal-hash-set/c any/c #:kind 'immutable))
|
||||
(make-immutable-hash (map (λ (v) (cons v null)) l)))]
|
||||
}
|
||||
|
||||
@section{Graph builder information}
|
||||
|
||||
The information about a graph type is valid regardless of how the graph
|
||||
instances are constructed, and is therefore rather succinct.
|
||||
|
||||
The @racket[graph-builder-info] @racket[struct] extends this with meaningful
|
||||
information about graph transformations. Two transformations which have the
|
||||
same output graph type may use different sets of mapping functions.
|
||||
Furthermore, the @racket[_dependent-invariants] are invariants relating the
|
||||
input and output of a graph transformation.
|
||||
|
||||
The @racket[_multi-constructor] identifier refers to a function which takes
|
||||
@${n} lists of lists of mapping argument tuples, and returns @${n} lists of
|
||||
lists of nodes. It is the most general function allowing the creation of
|
||||
instances of the graph. Wrappers which accept a single tuple of arguments and
|
||||
return the corresponding node can be written based on it.
|
||||
|
||||
@chunk[<graph-builder-info>
|
||||
(struct+/contract graph-builder-info graph-info
|
||||
([name identifier?]
|
||||
[tvars (listof identifier?)]
|
||||
[root-node identifier?]
|
||||
[node-order (listof identifier?)]
|
||||
[nodes (hash/c symbol? node-info? #:immutable #t)]
|
||||
[invariants (set/c invariant-info? #:kind 'immutable #:cmp 'equal)])
|
||||
([multi-constructor identifier?]
|
||||
[root-mapping identifier?]
|
||||
[mapping-order (listof identifier?)]
|
||||
[mappings (hash/c symbol? mapping-info? #:immutable #t)]
|
||||
[dependent-invariants (set/c dependent-invariant-info?
|
||||
#:kind 'immutable
|
||||
#:cmp 'equal)])
|
||||
#:transparent
|
||||
#:methods gen:custom-write
|
||||
[(define write-proc (struct-printer 'graph-builder-info))]
|
||||
#:property prop:custom-print-quotable 'never)]
|
||||
|
||||
@section{Node information}
|
||||
|
||||
@chunk[<node-info>
|
||||
(struct+/contract node-info
|
||||
([predicate? identifier?]
|
||||
[field-order (listof identifier?)]
|
||||
[fields (hash/c symbol? field-info? #:immutable #t)]
|
||||
[promise-type stx-type/c]
|
||||
;; Wrappers can mean that we have incomplete types with fewer
|
||||
;; fields than the final node type.
|
||||
;[make-incomplete-type identifier?]
|
||||
;[incomplete-type identifier?]
|
||||
)
|
||||
#:transparent
|
||||
#:methods gen:custom-write
|
||||
[(define write-proc (struct-printer 'node-info))]
|
||||
#:property prop:custom-print-quotable 'never)]
|
||||
|
||||
@section{Field information}
|
||||
|
||||
A field has a type.
|
||||
|
||||
@chunk[<field-info>
|
||||
(struct+/contract field-info
|
||||
([type stx-type/c])
|
||||
#:transparent
|
||||
#:methods gen:custom-write
|
||||
[(define write-proc (struct-printer 'field-info))]
|
||||
#:property prop:custom-print-quotable 'never)]
|
||||
|
||||
@;[incomplete-type identifier?]
|
||||
|
||||
@section{Invariant information}
|
||||
|
||||
@chunk[<invariant-info>
|
||||
(struct+/contract invariant-info
|
||||
([predicate identifier?] ; (→ RootNode Boolean : +witness-type)
|
||||
[witness-type stx-type/c])
|
||||
#:transparent
|
||||
#:methods gen:custom-write
|
||||
[(define write-proc (struct-printer 'invariant-info))]
|
||||
#:property prop:custom-print-quotable 'never
|
||||
#:methods gen:equal+hash
|
||||
[(define (equal-proc a b r)
|
||||
(free-id-tree=? (vector->immutable-vector (struct->vector a))
|
||||
(vector->immutable-vector (struct->vector b))))
|
||||
(define (hash-proc a r)
|
||||
(free-id-tree-hash-code
|
||||
(vector->immutable-vector (struct->vector a))))
|
||||
(define (hash2-proc a r)
|
||||
(free-id-tree-secondary-hash-code
|
||||
(vector->immutable-vector (struct->vector a))))])]
|
||||
|
||||
@section{Dependent invariant information}
|
||||
|
||||
The invariants described in the previous section assert properties of a graph
|
||||
instance in isolation. It is however desirable to also describe invariants
|
||||
which relate the old and the new graph in a graph transformation.
|
||||
|
||||
@chunk[<dependent-invariant-info>
|
||||
(struct+/contract dependent-invariant-info
|
||||
([checker identifier?] ; (→ RootMappingArguments… NewGraphRoot Boolean)
|
||||
[name identifier?])
|
||||
#:transparent
|
||||
#:methods gen:custom-write
|
||||
[(define write-proc (struct-printer 'dependent-invariant-info))]
|
||||
#:property prop:custom-print-quotable 'never
|
||||
#:methods gen:equal+hash
|
||||
[(define (equal-proc a b r)
|
||||
(free-id-tree=? (vector->immutable-vector (struct->vector a))
|
||||
(vector->immutable-vector (struct->vector b))))
|
||||
(define (hash-proc a r)
|
||||
(free-id-tree-hash-code
|
||||
(vector->immutable-vector (struct->vector a))))
|
||||
(define (hash2-proc a r)
|
||||
(free-id-tree-secondary-hash-code
|
||||
(vector->immutable-vector (struct->vector a))))])]
|
||||
|
||||
@section{Mapping information}
|
||||
|
||||
@chunk[<mapping-info>
|
||||
(struct+/contract mapping-info
|
||||
([mapping-function identifier?]
|
||||
[with-promises-type identifier?]
|
||||
[make-placeholder-type identifier?]
|
||||
[placeholder-type identifier?])
|
||||
#:transparent
|
||||
#:methods gen:custom-write
|
||||
[(define write-proc (struct-printer 'mapping-info))]
|
||||
#:property prop:custom-print-quotable 'never)]
|
||||
|
||||
@section{Printing}
|
||||
|
||||
It is much easier to debug graph information if it is free from the visual
|
||||
clutter of printed syntax objects (which waste most of the screen real estate
|
||||
printing @tt{#<syntax:/path/to/file}, when the interesting part is the
|
||||
contents of the syntax object).
|
||||
|
||||
We therefore pre-process the fields, transforming syntax objects into regular
|
||||
data.
|
||||
|
||||
@chunk[<printer>
|
||||
(define (to-datum v)
|
||||
(syntax->datum (datum->syntax #f v)))
|
||||
|
||||
(define ((syntax-convert old-print-convert-hook)
|
||||
val basic-convert sub-convert)
|
||||
(cond
|
||||
[(set? val)
|
||||
(cons 'set (map sub-convert (set->list val)))]
|
||||
[(and (hash? val) (immutable? val))
|
||||
(cons 'hash
|
||||
(append-map (λ (p) (list (sub-convert (car p))
|
||||
(sub-convert (cdr p))))
|
||||
(hash->list val)))]
|
||||
[(syntax? val)
|
||||
(list 'syntax (to-datum val))]
|
||||
[else
|
||||
(old-print-convert-hook val basic-convert sub-convert)]))
|
||||
|
||||
(define ((struct-printer ctor) st port mode)
|
||||
(match-define (vector name fields ...) (struct->vector st))
|
||||
(define-values (info skipped?) (struct-info st))
|
||||
(define-values (-short-name _2 _3 _4 _5 _6 _7 _8)
|
||||
(struct-type-info info))
|
||||
(define short-name (or ctor -short-name))
|
||||
(define (to-datum v)
|
||||
(syntax->datum (datum->syntax #f v)))
|
||||
(case mode
|
||||
[(#t)
|
||||
(display "#(" port)
|
||||
(display name port)
|
||||
(for-each (λ (f)
|
||||
(display " " port)
|
||||
(write (to-datum f) port))
|
||||
fields)
|
||||
(display ")" port)]
|
||||
[(#f)
|
||||
(display "#(" port)
|
||||
(display name port)
|
||||
(for-each (λ (f)
|
||||
(display " " port)
|
||||
(display (to-datum f) port))
|
||||
fields)
|
||||
(display ")" port)]
|
||||
[else
|
||||
(let ([old-print-convert-hook (current-print-convert-hook)])
|
||||
(parameterize ([constructor-style-printing #t]
|
||||
[show-sharing #f]
|
||||
[current-print-convert-hook
|
||||
(syntax-convert old-print-convert-hook)])
|
||||
(write
|
||||
(cons short-name
|
||||
(map print-convert
|
||||
;; to-datum doesn't work if I map it on the fields?
|
||||
fields))
|
||||
port)))]))]
|
||||
|
||||
@CHUNK[<*>
|
||||
(require phc-toolkit/untyped
|
||||
type-expander/expander
|
||||
racket/struct
|
||||
mzlib/pconvert
|
||||
"free-identifier-tree-equal.rkt"
|
||||
(for-syntax phc-toolkit/untyped
|
||||
syntax/parse
|
||||
syntax/parse/experimental/template
|
||||
racket/syntax))
|
||||
|
||||
(define-syntax/parse
|
||||
(struct+/contract name {~optional parent}
|
||||
{~optional ([parent-field parent-contract] ...)}
|
||||
([field contract] ...)
|
||||
{~optional {~and transparent #:transparent}}
|
||||
(~and {~seq methods+props ...}
|
||||
(~seq (~or {~seq #:methods _ _}
|
||||
{~seq #:property _ _})
|
||||
...)))
|
||||
#:with name/c (format-id #'name "~a/c" #'name)
|
||||
;(quasisyntax/loc (stx-car this-syntax)
|
||||
; #,
|
||||
(template
|
||||
(begin
|
||||
(struct name (?? parent) (field ...)
|
||||
(?? transparent)
|
||||
methods+props ...)
|
||||
(define name/c
|
||||
(struct/c name
|
||||
(?? (?@ parent-contract ...))
|
||||
contract ...))
|
||||
(module+ test
|
||||
(require rackunit)
|
||||
(check-pred flat-contract? name/c))
|
||||
(provide name/c
|
||||
(contract-out (struct (?? (name parent) name)
|
||||
((?? (?@ [parent-field parent-contract]
|
||||
...))
|
||||
[field contract]
|
||||
...)))))))
|
||||
|
||||
;<hash-set/c>
|
||||
<printer>
|
||||
|
||||
<field-info>
|
||||
<node-info>
|
||||
<invariant-info>
|
||||
<dependent-invariant-info>
|
||||
<graph-info>
|
||||
<mapping-info>
|
||||
<graph-builder-info>]
|
||||
|
|
@ -1,144 +0,0 @@
|
|||
#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"))
|
||||
|
||||
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
|
||||
(~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}))))]
|
||||
|
||||
@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>])))]
|
||||
|
||||
@chunk[<graph-info>
|
||||
(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ᵢⱼ τᵢⱼ] …))))
|
||||
#'nodeᵢ ; promise type
|
||||
#;(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)]
|
||||
|
||||
@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
|
||||
extensible-parser-specifications
|
||||
backport-template-pr1514/experimental/template)
|
||||
(for-meta 2 racket/base))
|
||||
|
||||
(provide define-graph-type)
|
||||
|
||||
<signature>
|
||||
<build-graph-info>
|
||||
<define-graph-type>]
|
||||
119
graph.hl.rkt
119
graph.hl.rkt
|
|
@ -1,119 +0,0 @@
|
|||
#lang hyper-literate typed/racket/base #:no-auto-require
|
||||
@(require scribble-math
|
||||
racket/require
|
||||
scribble-enhanced/doc
|
||||
racket/require
|
||||
hyper-literate
|
||||
(subtract-in scribble/struct scribble-enhanced/doc)
|
||||
scribble/decode
|
||||
(for-label racket/format
|
||||
racket/promise
|
||||
racket/list
|
||||
type-expander
|
||||
(except-in (subtract-in typed/racket/base type-expander)
|
||||
values)
|
||||
(only-in racket/base values)
|
||||
(subtract-in racket/contract typed/racket/base)
|
||||
phc-toolkit
|
||||
phc-toolkit/untyped-only
|
||||
remember))
|
||||
@(unless-preexpanding
|
||||
(require (for-label (submod ".."))))
|
||||
@doc-lib-setup
|
||||
|
||||
@title[#:style (with-html5 manual-doc-style)
|
||||
#:tag "graph-impl"
|
||||
#:tag-prefix "phc-graph/graph-impl"]{Implementation of the graph macro}
|
||||
|
||||
@(chunks-toc-prefix
|
||||
'("(lib phc-graph/scribblings/phc-graph-implementation.scrbl)"
|
||||
"phc-graph/graph-impl"))
|
||||
|
||||
|
||||
@chunk[<graph>
|
||||
(define-syntax define-graph
|
||||
(syntax-parser
|
||||
[<signature>
|
||||
<implementation>]))]
|
||||
|
||||
@chunk[<signature>
|
||||
(_ _name
|
||||
[[_nodeᵢ [_fieldᵢⱼ :colon _τᵢⱼ] …] …]
|
||||
[[(_mappingₖ [_argₖₗ _τₖₗ] …) :colon _return-typeₖ . _bodyₖ] …])]
|
||||
|
||||
@chunk[<implementation>
|
||||
#'()]
|
||||
|
||||
@section{Overview of the implementation (draft)}
|
||||
|
||||
@chunk[<implementation-draft>
|
||||
<create-Qₖ>
|
||||
<re-bind-mappings>
|
||||
<define-indices>
|
||||
<process-queues>]
|
||||
|
||||
@chunk[<define-indices>
|
||||
(define/with-syntax (_indexₖ …) (stx-map gensym #'(_idxₖ …)))
|
||||
#'(begin
|
||||
(define-type _indexₖ (graph-index '_indexₖ))
|
||||
…)]
|
||||
|
||||
@chunk[<define-index>
|
||||
(struct (K) graph-index ([key : K] [index : Index]))]
|
||||
|
||||
Create one queue @racket[_Qₖ] for each mapping:
|
||||
|
||||
@chunk[<create-Qₖ>
|
||||
#'(begin
|
||||
(define _Qₖ <create-queue>)
|
||||
(define _Qₖ-enqueue <TODO>)
|
||||
(define _Qₖ-pop <TODO>)
|
||||
…)]
|
||||
|
||||
Re-bind mappings to catch outbound calls:
|
||||
|
||||
@chunk[<re-bind-mappings>
|
||||
#'(let ([_mappingₖ _make-placeholderₖ] …)
|
||||
. bodyₖ)]
|
||||
|
||||
Define functions which enqueue into a given @racket[_Qₖ] and start processing.
|
||||
The final @racket[_name] macro dispatches to these functions.
|
||||
|
||||
@chunk[<entry-pointₖ>
|
||||
#'(begin
|
||||
(define (_entry-pointₖ _argₖₗ …)
|
||||
(entry-point #:mappingₖ (list (list _argₖₗ …))))
|
||||
…)]
|
||||
|
||||
These are based upon the main @racket[entry-point], which takes any number of
|
||||
initial elements to enqueue, and processes the queues till they are all empty.
|
||||
|
||||
@chunk[<entry-point>
|
||||
#'(define (entry-point #:mappingₖ [_argsₖ* : (Listof (List τₖₗ …)) '()])
|
||||
(for ([_argsₖ (in-list _argsₖ*)])
|
||||
(let-values ([(_argₖₗ …) _argsₖ])
|
||||
(Qₖ-enqueue _argₖₗ …))))]
|
||||
|
||||
@chunk[<process-queues>
|
||||
(until queues are all empty
|
||||
process item, see below)]
|
||||
|
||||
@itemlist[
|
||||
@item{Find and replace references to old nodes and new incomplete nodes and
|
||||
new placeholder nodes, instead insert indices.}
|
||||
@item{Problem: we need to actually insert indices for references to nodes,
|
||||
not for references to mappings (those have to be inlined).}]
|
||||
|
||||
|
||||
@chunk[<*>
|
||||
(require racket/require
|
||||
(for-syntax (subtract-in (combine-in racket/base
|
||||
syntax/parse)
|
||||
"subtemplate-override.rkt")
|
||||
phc-toolkit/untyped
|
||||
type-expander/expander
|
||||
"subtemplate-override.rkt")
|
||||
"traversal.hl.rkt"
|
||||
phc-toolkit)
|
||||
<define-index>
|
||||
<graph>]
|
||||
32
info.rkt
32
info.rkt
|
|
@ -1,32 +0,0 @@
|
|||
#lang info
|
||||
(define collection "phc-graph")
|
||||
(define deps '("base"
|
||||
"rackunit-lib"
|
||||
"phc-toolkit"
|
||||
"phc-adt"
|
||||
"type-expander"
|
||||
"hyper-literate"
|
||||
"scribble-enhanced"
|
||||
"typed-racket-lib"
|
||||
"srfi-lite-lib"
|
||||
"delay-pure"
|
||||
"backport-template-pr1514"
|
||||
"typed-map"
|
||||
"scribble-lib"
|
||||
"pconvert-lib"
|
||||
"remember"
|
||||
"extensible-parser-specifications"))
|
||||
(define build-deps '("scribble-lib"
|
||||
"racket-doc"
|
||||
"remember"
|
||||
"typed-racket-doc"
|
||||
"aful"
|
||||
"scribble-math"))
|
||||
(define scribblings
|
||||
'(("scribblings/phc-graph.scrbl" ()
|
||||
("Data Structures"))
|
||||
("scribblings/phc-graph-implementation.scrbl" (multi-page)
|
||||
("Data Structures"))))
|
||||
(define pkg-desc "Description Here")
|
||||
(define version "0.0")
|
||||
(define pkg-authors '("Georges Dupéron"))
|
||||
|
|
@ -1,483 +0,0 @@
|
|||
#lang aful/unhygienic hyper-literate type-expander/lang
|
||||
|
||||
@require[scribble-math
|
||||
scribble-enhanced/doc
|
||||
"notations.rkt"]
|
||||
|
||||
@title[#:style (with-html5 manual-doc-style)
|
||||
#:tag "inv-phantom"
|
||||
#:tag-prefix "phc-graph/inv-phantom"]{Tracking checked contracts
|
||||
via refinement types}
|
||||
|
||||
@(chunks-toc-prefix
|
||||
'("(lib phc-graph/scribblings/phc-graph-implementation.scrbl)"
|
||||
"phc-graph/inv-phantom"))
|
||||
|
||||
@section{Introduction}
|
||||
|
||||
The cautious compiler writer will no doubt want to check that the graph used
|
||||
to represent the program verifies some structural properties. For example, the
|
||||
compiled language might not allow cycles between types. Another desirable
|
||||
property is that the @racket[in-method] field of an instruction points back to
|
||||
the method containing it. We will use this second property as a running
|
||||
example in this section.
|
||||
|
||||
@section{Implementation overview : subtyping, variance and phantom types}
|
||||
|
||||
It is possible to express with Typed/Racket that a @racket[Method] should
|
||||
contain a list of @racket[Instruction]s, and that @racket[Instruction]s should
|
||||
point to a @racket[Method]@note{We are not concerned here about the ability to
|
||||
create such values, which necessarily contain some form of cycle. The goal of
|
||||
the graph library is indeed to handle the creation and traversal of such
|
||||
cyclic data structures in a safe way}:
|
||||
|
||||
@chunk[<invariant-1>
|
||||
(struct Instruction ([opcode : Byte]
|
||||
[in-method : Method]))
|
||||
(struct Method ([body : (Listof Instruction)]))]
|
||||
|
||||
This type does not, however, encode the fact that an instruction should point
|
||||
to the method containing it. Typed/Racket does not really have a notion of
|
||||
singleton types, aside from symbols and other primitive data. It also lacks a
|
||||
way to type "the value itself" (e.g. to describe a single-field structure
|
||||
pointing to itself, possibly via a @racket[Promise]). This means that the
|
||||
property could only be expressed in a rather contrived way, if it is at all
|
||||
possible.
|
||||
|
||||
@; (define-type Self-Loop (∀ (A) (→ (Pairof Integer (Self-Loop A)))))
|
||||
|
||||
We decide to rely instead on a run-time check, i.e. a sort of contract which
|
||||
checks the structural invariant on the whole graph. In order to let the
|
||||
type-checker know whether a value was checked against that contract or not, we
|
||||
include within the node a phantom type which is used as a flag, indicating
|
||||
that the graph was checked against that contract. This phantom type in a sense
|
||||
refines the node type, indicating an additional property (which, in our case,
|
||||
is not checked at compile-time but instead enforced at run-time).
|
||||
|
||||
@chunk[<invariant-2>
|
||||
(struct (Flag) Instruction ([opcode : Byte]
|
||||
[in-method : (Method Flag)]))
|
||||
(struct (Flag) Method ([body : (Listof (Instruction Flag))]))]
|
||||
|
||||
We would then write a function accepting a @racket[Method] for which the
|
||||
contract @racket[method→instruction→same-method] was checked like this:
|
||||
|
||||
@chunk[<invariant-2-use>
|
||||
(λ ([m : (Method 'method→instruction→same-method)])
|
||||
…)]
|
||||
|
||||
Unfortunately, this attempt fails to catch errors as one would expect, because
|
||||
Typed/Racket discards unused polymorphic arguments, as can be seen in the
|
||||
following example, which type-checks without any complaint:
|
||||
|
||||
@chunk[<phantom-types-ignored>
|
||||
(struct (Phantom) S ([x : Integer]))
|
||||
(define inst-sa : (S 'a) (S 1))
|
||||
(ann inst-sa (S 'b))]
|
||||
|
||||
We must therefore make a field with the @racket[Flag] type actually appear
|
||||
within the instance:
|
||||
|
||||
@chunk[<invariant-3>
|
||||
(struct (Flag) Instruction ([opcode : Byte]
|
||||
[in-method : (Method Flag)]
|
||||
[flag : Flag]))
|
||||
(struct (Flag) Method ([body : (Listof (Instruction Flag))]
|
||||
[flag : Flag]))]
|
||||
|
||||
Another issue is that the flag can easily be forged. We would therefore like
|
||||
to wrap it in a struct type which is only accessible by the graph library:
|
||||
|
||||
@chunk[<invariant-4>
|
||||
(struct (Flag) Flag-Wrapper-Struct ([flag : Flag]))
|
||||
(define-type Flag-Wrapper Flag-Wrapper-Struct)
|
||||
(code:comment "provide only the type, not the constructor or accessor")
|
||||
(provide Flag-Wrapper)]
|
||||
|
||||
We would like to be able to indicate that a graph node has validated several
|
||||
invariants. For that, we need a way to represent the type of a "set" of
|
||||
invariant witnesses. We also want some subtyping relationship between the
|
||||
sets: a set @${s₁} with more invariant witnesses should be a subtype of a
|
||||
subset @${s₂ ⊆ s₁}. We can order the invariant witnesses and use @racket[Rec]
|
||||
to build the type of a list of invariant witnesses, where some may be missing:
|
||||
|
||||
@chunk[<invariant-set-as-List+Rec>
|
||||
(define-type At-Least-InvB+InvD
|
||||
(Rec R₁ (U (Pairof Any R₁)
|
||||
(Pairof 'InvB (Rec R₂ (U (Pairof Any R₂)
|
||||
(Pairof 'InvD (Listof Any))))))))]
|
||||
|
||||
@chunk[<invariant-set-as-List+Rec-use>
|
||||
(ann '(InvA InvB InvC InvD InvE) At-Least-InvB+InvD)
|
||||
(ann '(InvB InvD) At-Least-InvB+InvD)
|
||||
(code:comment "Rejected, because it lacks 'InvD")
|
||||
(code:comment "(ann '(InvB InvC InvE) At-Least-InvB+InvD)")
|
||||
(code:comment "The elements must be in the right order,")
|
||||
(code:comment "this would be rejected by the typechecker:")
|
||||
(code:comment "(ann '(InvD InvB) At-Least-InvB+InvD)")]
|
||||
|
||||
Another solution is to group the witnesses in an untagged union with
|
||||
@racket[U], and place it in a contravariant position:
|
||||
|
||||
@chunk[<invariant-set-as-contravariant-U>
|
||||
(define-type At-Least-InvB+InvD
|
||||
(→ (U 'InvB 'InvD) Void))]
|
||||
|
||||
In the case where no invariant is present in the untagged union, the type
|
||||
@racket[(U)] a.k.a @racket[Nothing], the bottom type with no value, would
|
||||
appear. This type is somewhat pathological and allows absurd reasoning (a
|
||||
function accepting @racket[Nothing] can never be called, which may incite the
|
||||
type checker to perform excessive elision). To avoid any pitfalls, we will
|
||||
systematically include a dummy element @racket[Or] in the union, to make sure
|
||||
the union never becomes empty.
|
||||
|
||||
This solution also has the advantage that the size of the run-time witness is
|
||||
constant, and does not depend on the number of checked contracts (unlike the
|
||||
representation using a list). In practice the function should never be called.
|
||||
It can however simply be implemented in a way which pleases the type checked
|
||||
as a function accepting anything and returning void.
|
||||
|
||||
In addition to testifying that a graph node was checked against multiple,
|
||||
separate contracts, there might be some contracts which check stronger
|
||||
properties than others. A way to encode this relationship in the type system
|
||||
is to have subtyping relationships between the contract witnesses, so that
|
||||
@; TODO: get rid of the textit
|
||||
@${\textit{P}₁(x) ⇒ \textit{P}₂(x) ⇒ \textit{Inv}₁ @texsubtype \textit{Inv}₂}:
|
||||
|
||||
@chunk[<invariant-contract-subtyping>
|
||||
(struct InvWeak ())
|
||||
(struct InvStrong InvWeak ())]
|
||||
|
||||
If the witnesses must appear in a contravariant position (when using
|
||||
@racket[U] to group them), the relationship must be reversed:
|
||||
|
||||
@chunk[<invariant-contract-subtyping>
|
||||
(struct InvStrongContra ())
|
||||
(struct InvWeakContra InvStrongContra ())]
|
||||
|
||||
Alternatively, it is possible to use a second contravariant position to
|
||||
reverse the subtyping relationship again:
|
||||
|
||||
@chunk[<invariant-contract-subtyping>
|
||||
(struct InvWeak ())
|
||||
(struct InvStrong InvWeak ())
|
||||
|
||||
(define InvWeakContra (→ InvWeak Void))
|
||||
(define InvStrongContra (→ InvStrong Void))]
|
||||
|
||||
Finally, we note that the invariants should always be represented using a
|
||||
particular struct type, instead of using a symbol, so that name clashes are
|
||||
not a problem.
|
||||
|
||||
@section{Encoding property implication as subtyping}
|
||||
|
||||
The witness for a strong property should be a subtype of the witness for a
|
||||
weaker property. This allows a node with a strong property to be passed where
|
||||
a node with a weaker property is passed.
|
||||
|
||||
@chunk[<structural-draft>
|
||||
(code:comment "Draft ideas")
|
||||
|
||||
(struct ∈ ())
|
||||
(struct ≡ ())
|
||||
(struct ∉ ())
|
||||
|
||||
;(List Rel From Path1 Path2)
|
||||
(List ≡ ANodeName (List f1 f2) (List))
|
||||
(List ∈ ANodeName (List f1 f2) (List))
|
||||
(List ∉ ANodeName (List f1 f2) (List))
|
||||
(List ∉ ANodeName (List (* f1 f2 f3 f4) (* f5 f6)) (List))
|
||||
|
||||
;(List From Path+Rel)
|
||||
(List ANodeName (List f1 f2 ≡))
|
||||
(List ANodeName (List f1 f2 ∈))
|
||||
(List ANodeName (List f1 f2 ∉))
|
||||
(List ANodeName (List (List f1 ∉)
|
||||
(List f2 ∉)
|
||||
(List f3 ∉)
|
||||
(List f4
|
||||
(List f5 ∉)
|
||||
(List f6 ∉))))
|
||||
|
||||
;; How to make it have the right kind of subtyping?
|
||||
|
||||
|
||||
]
|
||||
|
||||
@subsection{Properties applying to all reachable nodes from @racket[x]}
|
||||
|
||||
The property @racket[x ≢ x.**] can be expanded to a series of properties. For
|
||||
example, if @racket[x] has two fields @racket[a] and @racket[d], the former
|
||||
itself having two fields @racket[b] and @racket[c], and the latter having a
|
||||
field @racket[e], itself with a field @racket[f]:
|
||||
@chunk[<expanded-path-set>
|
||||
(x ≢ x.a)
|
||||
(x ≢ x.a.b)
|
||||
(x ≢ x.a.c)
|
||||
(x ≢ x.d)
|
||||
(x ≢ x.d.e)
|
||||
(x ≢ x.d.e.f)]
|
||||
|
||||
@subsection{Prefix trees to the rescue}
|
||||
|
||||
This expanded representation is however costly, and can be expressed more
|
||||
concisely by factoring out the prefixes.
|
||||
|
||||
@chunk[<prefixes>
|
||||
(x ≢ (x (a (b) (c))
|
||||
(d (e (f)))))]
|
||||
|
||||
One thing which notably cannot be represented concisely in this way is
|
||||
@racket[x.a.** ≢ x.b.**], meaning that the subgraphs rooted at @racket[x.a]
|
||||
and @racket[x.b] are disjoint. It would be possible to have a representation
|
||||
combining a prefix-tree on the left, and a prefix-tree on the right, implying
|
||||
the cartesian product of both sets of paths. This has a negligible cost in the
|
||||
size of the type for the case where one of the members of the cartesian
|
||||
product, as we end up with the following (the left-hand-side @racket[x] gains
|
||||
an extra pair of parentheses, because it is now an empty tree):
|
||||
|
||||
@chunk[<prefixes>
|
||||
((x) ≢ (x (a (b) (c))
|
||||
(d (e (f)))))]
|
||||
|
||||
This does not allow concise expression of all properties, i.e. this is a form
|
||||
of compression, which encodes concisely likely sets of pairs of paths, but is
|
||||
of little help for more random properties. For example, if a random subset of
|
||||
the cartesian product of reachable paths is selected, there is no obvious way
|
||||
to encode it in a significantly more concise way than simply listing the pairs
|
||||
of paths one by one.
|
||||
|
||||
@subsection{Cycles in properties}
|
||||
|
||||
If a @racket[**] path element (i.e. a set of paths representing any path of
|
||||
any length) corresponds to a part of the graph which contains a cycle in the
|
||||
type, it is necessary to make that cycle appear in the expanded form. For
|
||||
that, we use @racket[Rec]. Supposing that the node @racket[x] has two fields,
|
||||
@racket[a] and @racket[c], the first itself having a field @racket[b] of type
|
||||
@racket[x]. We would expand @racket[x.**] to the following shape:
|
||||
|
||||
@racket[(Rec X (≢ (Node0 'x)
|
||||
(Node2 'x
|
||||
(Field1 'a (Field1 'b (Field1 X)))
|
||||
(Field1 'c))))]
|
||||
|
||||
If one of the fields refers not to the root, but to
|
||||
|
||||
TODO: distinction between root nodes and fields in the path. Add an @racket[ε]
|
||||
component at the root of each path?
|
||||
|
||||
@subsection{Partial paths}
|
||||
|
||||
Partial paths: if a property holds between @racket[x.a] and @racket[x.b], then
|
||||
it is stronger than a property which holds between @racket[y.fx.a] and
|
||||
@racket[y.fx.b] (i.e. the common prefix path narrows down the set of pairs of
|
||||
values which are related by the property).
|
||||
|
||||
A possible solution idea: mask the "beginning" of the path with a @racket[∀]
|
||||
or @racket[Any]. Either use
|
||||
@racket[(Rec Ign (U (Field1 Any Ign) Actual-tail-of-type))], or reverse the
|
||||
``list'', so that one writes @racket[(Field1 'b (Field1 'a Any))], i.e. we
|
||||
have @racket[(Field1 field-name up)] instead of
|
||||
@racket[(Field1 field-name children)]. The problem with the reversed version
|
||||
is that two child fields @racket[b] and @racket[c] need to refer to the same
|
||||
parent @racket[a], which leads to duplication or naming (in the case of
|
||||
naming, Typed/Racket tends to perform some inlining anyway, except if tricks
|
||||
are used to force the type to be recursive (in which case the subtyping / type
|
||||
matching is less good and fails to recognise weaker or equivalent formulations
|
||||
of the type)). The problem with the @racket[Rec] solution for an ignored head
|
||||
of any length is that the number of fields is not known in advance (but
|
||||
hopefully our representation choices to allow weaker properties with missing
|
||||
fields could make this a non-problem?).
|
||||
|
||||
@subsection{Array and list indices}
|
||||
|
||||
When a path reaches an array, list, set or another similar collection, the
|
||||
special path element @racket[*] can be used to indicate ``any element in the
|
||||
array or list''. Specific indices can be indicated by an integer, or for lists
|
||||
with @racket[car], @racket[first], @racket[second], @racket[third] and so on.
|
||||
The special path elements @racket[cdr] and @racket[rest] access the rest of
|
||||
the list, i.e. everything but the first element.
|
||||
|
||||
@subsection{Other richer properties}
|
||||
|
||||
Other richer properties can be expressed, like
|
||||
@racket[x.len = (length x.somelist)]. This property calls some racket
|
||||
primitives (@racket[length]), and compares numeric values. However, we do not
|
||||
attempt to make the type checker automatically recognise weaker or equivalent
|
||||
properties. Instead, we simply add to the phantom type a literal description
|
||||
of the checked property, which will only match the same exact property.
|
||||
|
||||
@section{Implementation}
|
||||
|
||||
@subsection{The witness value}
|
||||
|
||||
Since all witnesses will have a type of the form
|
||||
@racket[(→ (U (→ invᵢ Void) …) Void)], they can all be represented at run-time
|
||||
by a single value: a function accepting any argument and returning
|
||||
@racket[Void]. Note that the type of the witness is normally a phantom type,
|
||||
and an actual value is supplied only because Typed/Racket drops phantom types
|
||||
before typechecking, as mentioned earlier.
|
||||
|
||||
@chunk[<witness-value>
|
||||
(: witness-value (→ Any Void))
|
||||
(define witness-value (λ (x) (void)))]
|
||||
|
||||
@subsection{Grouping multiple invariants}
|
||||
|
||||
As mentioned earlier, we group invariants together using an untagged union
|
||||
@racket[U], which must appear in a contravariant position. We wish to express
|
||||
witnesses for stronger invariants as subtypes of witnesses for weaker
|
||||
invariants, and therefore use a second nested function type to flip again the
|
||||
variance direction. We always include the Or element in the union, to avoid
|
||||
having an empty union.
|
||||
|
||||
@chunk[<grouping-invariants>
|
||||
(struct Or ())
|
||||
(define-type-expander (Invariants stx)
|
||||
(syntax-case stx ()
|
||||
[(_ invᵢ …)
|
||||
#'(→ (U Or (→ invᵢ Void) …) Void)
|
||||
#;#'(→ (→ (∩ invᵢ …) Void) Void)]))]
|
||||
|
||||
@subsection{Structural (in)equality and (non-)membership invariants}
|
||||
|
||||
@subsubsection{Comparison operator tokens}
|
||||
|
||||
We define some tokens which will be used to identify the operator which
|
||||
relates two nodes in the graph.
|
||||
|
||||
@chunk[<comparison-operators>
|
||||
(struct (A) inv≡ ([a : A]))
|
||||
(struct (A) inv≢ ([a : A]))
|
||||
;(struct inv∈ ()) ;; Can be expressed in terms of ≡
|
||||
;(struct inv∉ ()) ;; Can be expressed in terms of ≢
|
||||
]
|
||||
|
||||
@CHUNK[<≡>
|
||||
(define-for-syntax (relation inv)
|
||||
(syntax-parser
|
||||
[(_ (pre-a … {~literal _} post-a …)
|
||||
(pre-b … {~literal _} post-b …))
|
||||
#:with (r-pre-a …) (reverse (syntax->list #'(pre-a …)))
|
||||
#:with (r-pre-b …) (reverse (syntax->list #'(pre-b …)))
|
||||
;; Use U to make it order-independent
|
||||
#`(#,inv (U (Pairof (Cycle r-pre-a …)
|
||||
(Cycle post-a …))
|
||||
(Pairof (Cycle r-pre-b …)
|
||||
(Cycle post-b …))))]))
|
||||
|
||||
(define-type-expander ≡ (relation #'inv≡))
|
||||
(define-type-expander ≢ (relation #'inv≢))]
|
||||
|
||||
@chunk[<cycles>
|
||||
(struct ε () #:transparent)
|
||||
(struct (T) Target () #:transparent)
|
||||
(struct (T) NonTarget Target ([x : T]) #:transparent)
|
||||
|
||||
(define-type-expander Cycle
|
||||
(syntax-parser
|
||||
[(_ field:id … {~literal ↙} loop1:id … (target:id) loop2:id …)
|
||||
#'(List* (NonTarget ε)
|
||||
(NonTarget 'field) …
|
||||
(Rec R (List* (NonTarget 'loop1) … ;(NonTarget 'loop1) …
|
||||
(Target 'target) ;(NonTarget 'target)
|
||||
(NonTarget 'loop2) … ;(NonTarget 'loop2) …
|
||||
R)))]
|
||||
[(_ field … target)
|
||||
;; TODO: something special at the end?
|
||||
#'(List (NonTarget ε) (NonTarget 'field) … (Target 'target))]
|
||||
[(_)
|
||||
#'(List (Target ε))]))]
|
||||
|
||||
@;{@[
|
||||
|
||||
;.a.b = .x.y
|
||||
;(l1=a ∧ l2=b ∧ r1=x ∧ r2=y) ⇒ eq
|
||||
;¬(l1=a ∧ l2=b ∧ r1=x ∧ r2=y) ∨ eq
|
||||
;¬l1=a ∨ ¬l2=b ∨ ¬r1=x ∨ ¬r2=y ∨ eq
|
||||
|
||||
;.a.c = .x.y
|
||||
;(l1=a ∧ l2=c ∧ r1=x ∧ r2=y) ⇒ eq
|
||||
|
||||
;.a.c = .x.z
|
||||
;(l1=a ∧ l2=b ∧ r1=x ∧ r2=z) ⇒ eq
|
||||
;¬l1=a ∨ ¬l2=b ∨ ¬r1=x ∨ ¬r2=z ∨ eq
|
||||
|
||||
|
||||
;.a.b = .x.y ∧ .a.c = .x.z
|
||||
;(¬l1=a ∨ ¬l2=b ∨ ¬r1=x ∨ ¬r2=y ∨ eq) ∧ (¬l1=a ∨ ¬l2=b ∨ ¬r1=x ∨ ¬r2=z ∨ eq)
|
||||
;¬¬(¬l1=a ∨ ¬l2=b ∨ ¬r1=x ∨ ¬r2=y ∨ eq) ∧ (¬l1=a ∨ ¬l2=b ∨ ¬r1=x ∨ ¬r2=z ∨ eq)
|
||||
;¬(l1=a ∧ l2=b ∧ r1=x ∧ r2=y ∧ eq) ∨ (l1=a ∧ l2=b ∧ r1=x ∧ r2=z ∧ ¬eq)
|
||||
]}
|
||||
|
||||
@; Problem with ∩: it factors out too much, (∩ '(a . b) '(a . c) '(x . b))
|
||||
@; becomes (Pairof (∩ 'a 'x) (∩ 'b 'c)), which is equivalent to have all four
|
||||
@; elements of {a,x} × {b,c}, but we only want three out of these four.
|
||||
|
||||
Two sorts of paths inside (in)equality constraints:
|
||||
|
||||
@itemlist[
|
||||
@item{those anchored on a node, stating that
|
||||
@$${
|
||||
∀\ \textit{node} : \textit{NodeType},\quad
|
||||
\textit{node}.\textit{path}₁ ≡ \textit{node}.\textit{path}₂}}
|
||||
@item{those not anchored on a node, stating that
|
||||
@$${
|
||||
\begin{array}{c}
|
||||
∀\ \textit{node}₁ : \textit{NodeType}₁,\quad
|
||||
∀\ \textit{node}₂ : \textit{NodeType}₂,\\
|
||||
\textit{node}₁.\textit{path}₁ ≡ \textit{node}₂.\textit{path}₂
|
||||
\end{array}}}]
|
||||
|
||||
@subsection{Putting it all together}
|
||||
|
||||
@chunk[<check-a-stronger-b>
|
||||
(define-syntax (check-a-stronger-or-same-b stx)
|
||||
(syntax-case stx ()
|
||||
[(_ stronger weaker)
|
||||
(syntax/top-loc stx
|
||||
(check-ann (ann witness-value stronger)
|
||||
weaker))]))
|
||||
|
||||
(define-syntax (check-a-same-b stx)
|
||||
(syntax-case stx ()
|
||||
[(_ a b)
|
||||
(syntax/top-loc stx
|
||||
(begin
|
||||
(check-ann (ann witness-value a) b)
|
||||
(check-ann (ann witness-value b) a)))]))]
|
||||
|
||||
@chunk[<*>
|
||||
(require (for-syntax phc-toolkit/untyped
|
||||
syntax/parse))
|
||||
|
||||
<witness-value>
|
||||
<grouping-invariants>
|
||||
<cycles>
|
||||
<comparison-operators>
|
||||
<≡>
|
||||
|
||||
(module+ test
|
||||
(require phc-toolkit)
|
||||
<check-a-stronger-b>
|
||||
|
||||
(ann witness-value (Invariants)) ;; No invariants
|
||||
(ann witness-value (Invariants (≡ (_ a) (_ a b c))))
|
||||
|
||||
(check-a-stronger-or-same-b (Invariants (≡ (_ a) (_ a b c)))
|
||||
(Invariants))
|
||||
|
||||
(check-a-same-b (Invariants (≡ (_ a) (_ a b c)))
|
||||
(Invariants (≡ (_ a b c) (_ a))))
|
||||
|
||||
(check-a-stronger-or-same-b (Invariants (≡ (_) (_ b c))
|
||||
(≡ (_) (_ b d)))
|
||||
(Invariants (≡ (_) (_ b c))))
|
||||
(check-a-stronger-or-same-b (Invariants (≡ (_) (_ b d))
|
||||
(≡ (_) (_ b c)))
|
||||
(Invariants (≡ (_) (_ b c))))
|
||||
|
||||
(check-a-stronger-or-same-b (Invariants (≡ (_)
|
||||
(_ b d a b d ↙ a b (d))))
|
||||
(Invariants (≡ (_)
|
||||
(_ b d ↙ a b (d))))))]
|
||||
35
main.rkt
35
main.rkt
|
|
@ -1,35 +0,0 @@
|
|||
#lang racket/base
|
||||
|
||||
(module+ test
|
||||
(require rackunit))
|
||||
|
||||
;; Notice
|
||||
;; To install (from within the package directory):
|
||||
;; $ raco pkg install
|
||||
;; To install (once uploaded to pkgs.racket-lang.org):
|
||||
;; $ raco pkg install <<name>>
|
||||
;; To uninstall:
|
||||
;; $ raco pkg remove <<name>>
|
||||
;; To view documentation:
|
||||
;; $ raco docs <<name>>
|
||||
;;
|
||||
;; For your convenience, we have included a LICENSE.txt file, which links to
|
||||
;; the GNU Lesser General Public License.
|
||||
;; If you would prefer to use a different license, replace LICENSE.txt with the
|
||||
;; desired license.
|
||||
;;
|
||||
;; Some users like to add a `private/` directory, place auxiliary files there,
|
||||
;; and require them in `main.rkt`.
|
||||
;;
|
||||
;; See the current version of the racket style guide here:
|
||||
;; http://docs.racket-lang.org/style/index.html
|
||||
|
||||
;; Code here
|
||||
|
||||
(module+ test
|
||||
;; Tests to be run with raco test
|
||||
)
|
||||
|
||||
(module+ main
|
||||
;; Main entry point, executed when run with the `racket` executable or DrRacket.
|
||||
)
|
||||
|
|
@ -1,7 +0,0 @@
|
|||
#lang racket
|
||||
|
||||
(require scribble/base)
|
||||
|
||||
(provide texsubtype)
|
||||
|
||||
(define texsubtype "<:")
|
||||
|
|
@ -1,19 +0,0 @@
|
|||
#lang scribble/manual
|
||||
@require[@for-label[phc-graph
|
||||
racket/base]]
|
||||
|
||||
@title{Ph.C Graph library: Implementation}
|
||||
@author[@author+email["Georges Dupéron" "georges.duperon@gmail.com"]]
|
||||
|
||||
This library is implemented using literate programming. The implementation
|
||||
details are presented in the following sections. The user documentation is in
|
||||
the @other-doc['(lib "phc-graph/scribblings/phc-graph.scrbl")] document.
|
||||
|
||||
@(table-of-contents)
|
||||
|
||||
@include-section[(submod "../traversal.hl.rkt" doc)]
|
||||
@include-section[(submod "../flexible-with.hl.rkt" doc)]
|
||||
@include-section[(submod "../invariants-phantom.hl.rkt" doc)]
|
||||
@include-section[(submod "../graph-info.hl.rkt" doc)]
|
||||
@include-section[(submod "../graph-type.hl.rkt" doc)]
|
||||
@include-section[(submod "../graph.hl.rkt" doc)]
|
||||
|
|
@ -1,14 +0,0 @@
|
|||
#lang scribble/manual
|
||||
@require[@for-label[phc-graph
|
||||
racket/base]]
|
||||
|
||||
@title{Ph.C Graph library}
|
||||
@author[@author+email["Georges Dupéron" "georges.duperon@gmail.com"]]
|
||||
|
||||
This library is implmented using literate programming. The
|
||||
implementation details are presented in
|
||||
@other-doc['(lib "phc-graph/scribblings/phc-graph-implementation.scrbl")].
|
||||
|
||||
@defmodule[phc-graph]
|
||||
|
||||
Package Description Here
|
||||
|
|
@ -1,17 +0,0 @@
|
|||
#lang s-exp phc-adt/declarations
|
||||
(remembered! tagged-structure (tg a b))
|
||||
(remembered! tagged-structure (tg a c))
|
||||
(remembered! tagged-structure (t0))
|
||||
(remembered! tagged-structure (City citizens name streets))
|
||||
(remembered! tagged-structure (Street houses name))
|
||||
(remembered! tagged-structure (House owner))
|
||||
(remembered! tagged-structure (Person name))
|
||||
(remembered! tagged-structure (node-incompleteᵢ citizens name streets))
|
||||
(remembered! tagged-structure (node-incompleteᵢ houses name))
|
||||
(remembered! tagged-structure (node-incompleteᵢ owner))
|
||||
(remembered! tagged-structure (node-incompleteᵢ name))
|
||||
(remembered! tagged-structure (| City-incomplete| citizens name streets))
|
||||
(remembered! tagged-structure (| Street-incomplete| houses name))
|
||||
(remembered! tagged-structure (| House-incomplete| owner))
|
||||
(remembered! tagged-structure (| Person-incomplete| name))
|
||||
(remembered! tagged-structure (City name))
|
||||
|
|
@ -1,49 +0,0 @@
|
|||
#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))
|
||||
21
test/ck.rkt
21
test/ck.rkt
|
|
@ -1,21 +0,0 @@
|
|||
#lang typed/racket/base
|
||||
|
||||
(require phc-toolkit
|
||||
(for-syntax racket/base
|
||||
syntax/parse
|
||||
type-expander/expander
|
||||
phc-toolkit/untyped))
|
||||
|
||||
(provide check-equal?-values:)
|
||||
|
||||
(define-syntax check-equal?-values:
|
||||
(syntax-parser
|
||||
[(_ actual {~maybe :colon type:type-expand!} expected ...)
|
||||
(quasisyntax/top-loc this-syntax
|
||||
(check-equal?: (call-with-values (ann (λ () actual)
|
||||
(-> #,(if (attribute type)
|
||||
#'type.expanded
|
||||
#'AnyValues)))
|
||||
(λ l l))
|
||||
(list expected ...)))]))
|
||||
|
||||
|
|
@ -1,42 +0,0 @@
|
|||
#lang typed/racket
|
||||
|
||||
(struct A ())
|
||||
(struct B A ())
|
||||
(struct C A ())
|
||||
|
||||
(: f (→ (U 'x A) Void))
|
||||
(define (f _) (void))
|
||||
|
||||
(let ()
|
||||
(ann f (→ (U B C) Void))
|
||||
(ann f (→ (U 'x B C) Void))
|
||||
(ann f (→ (U 'x C) Void))
|
||||
(ann f (→ (U 'x A C) Void))
|
||||
(ann f (→ (U 'x) Void))
|
||||
(ann f (→ (U) Void))
|
||||
(void))
|
||||
|
||||
;;;;;;;;;;
|
||||
|
||||
;; Reverse order (BB, CC and DD are more precise invariants than AA)
|
||||
(struct AA ())
|
||||
(struct BB AA ())
|
||||
(struct CC AA ())
|
||||
(struct DD AA ())
|
||||
|
||||
(define-type (Invariant X) (→ X Void))
|
||||
|
||||
(: g (→ (U (Invariant 'x) (Invariant BB) (Invariant CC)) Void))
|
||||
(define (g _) (void))
|
||||
|
||||
;; Everything works as expected
|
||||
(let ()
|
||||
(ann g (→ (U (Invariant BB) (Invariant CC)) Void))
|
||||
(ann g (→ (U (Invariant 'x) (Invariant BB) (Invariant CC)) Void))
|
||||
(ann g (→ (U (Invariant 'x) (Invariant CC)) Void))
|
||||
(ann g (→ (U (Invariant 'x)) Void))
|
||||
(ann g (→ (U) Void))
|
||||
;; AA works, as it should
|
||||
(ann g (→ (U (Invariant 'x) (Invariant AA) (Invariant CC)) Void))
|
||||
(ann g (→ (U (Invariant 'x) (Invariant AA)) Void))
|
||||
(void))
|
||||
|
|
@ -1,69 +0,0 @@
|
|||
#lang typed/racket
|
||||
|
||||
(: f (→ (→ (U (Rec R (List (List 'a R)
|
||||
(List 'b R)))
|
||||
(Rec R (List (List 'a R)
|
||||
(List 'c R))))
|
||||
Void)
|
||||
Void))
|
||||
(define (f x) (void))
|
||||
|
||||
(ann f (→ (→ (U (Rec K (List (List 'a K) (List 'c K)))
|
||||
(Rec W (List (List 'a W) (List 'b W))))
|
||||
Void) Void))
|
||||
|
||||
(ann f (→ (→ (U (Rec W (List (List 'a W) (List 'b W)))
|
||||
(Rec K (List (List 'a K) (List 'c K))))
|
||||
Void) Void))
|
||||
|
||||
(: g (→ (→ (Rec A (Rec B (List (List 'a A)
|
||||
(List 'b B))))
|
||||
Void)
|
||||
Void))
|
||||
(define (g x) (void))
|
||||
|
||||
(ann g
|
||||
(→ (→ (Rec B (Rec A (List (List 'a A)
|
||||
(List 'b B))))
|
||||
Void)
|
||||
Void))
|
||||
|
||||
(ann g
|
||||
(→ (→ (Rec X (List (List 'a X)
|
||||
(List 'b X)))
|
||||
Void)
|
||||
Void))
|
||||
|
||||
(define-type (≡ X Y) (List '≡ X Y))
|
||||
|
||||
(: h (→ (→ (∀ (X1 X2) (→ (U (≡ (List 'a 'b X1)
|
||||
(List 'c 'd X1))
|
||||
(≡ (List 'e 'f X2)
|
||||
(List 'g 'g X2)))))
|
||||
Void)
|
||||
Void))
|
||||
(define (h x) (void))
|
||||
|
||||
|
||||
(ann (λ ([x : (Rec R (Pairof 'a (Pairof 'b R)))]) (void))
|
||||
(-> (Rec R (Pairof 'a (Pairof 'b R))) Void))
|
||||
|
||||
(ann (λ ([x : (Rec R (Pairof 'a (Pairof 'b R)))]) (void))
|
||||
(-> (Pairof 'a (Rec R (Pairof 'b (Pairof 'a R)))) Void))
|
||||
|
||||
(ann (λ ([x : (Rec R (List 'a (List 'b R)))]) (void))
|
||||
(-> (List 'a (Rec R (List 'b (List 'a R)))) Void))
|
||||
|
||||
(ann (λ ([x : (Rec R (List 'a R (List 'b R)))]) (void))
|
||||
(-> (Rec R (Pairof 'a (Pairof R (Pairof (List 'b R) Null)))) Void))
|
||||
|
||||
(ann (λ ([x : (Rec R (List 'a R (List 'b R)))]) (void))
|
||||
(-> (Pairof 'a (Rec R (Pairof (Pairof 'a R) (Pairof (List 'b (Pairof 'a R)) Null)))) Void))
|
||||
|
||||
(ann (λ ([x : (Rec R (List 'a R (List 'b R)))]) (void))
|
||||
(-> (Pairof 'a (Pairof (Pairof 'a
|
||||
(Rec R (Pairof (Pairof 'a R) (Pairof (List 'b (Pairof 'a R)) Null)))
|
||||
)
|
||||
(Pairof (List 'b (Pairof 'a
|
||||
(Rec R (Pairof (Pairof 'a R) (Pairof (List 'b (Pairof 'a R)) Null)))
|
||||
)) Null))) Void))
|
||||
|
|
@ -1,79 +0,0 @@
|
|||
#lang aful/unhygienic type-expander/lang
|
||||
|
||||
(require (lib "phc-graph/flexible-with.hl.rkt")
|
||||
(for-syntax racket/syntax
|
||||
racket/list
|
||||
(rename-in racket/base [... …]))
|
||||
phc-toolkit
|
||||
typed-map
|
||||
type-expander)
|
||||
|
||||
(define-syntax (gs stx)
|
||||
(syntax-case stx ()
|
||||
[(_ bt-fields-id nfields (f …) [struct struct-field …] …)
|
||||
(let ()
|
||||
(define/with-syntax (field …)
|
||||
(append (syntax->list #'(f …))
|
||||
(map (λ (_) (datum->syntax #'nfields (gensym 'g)))
|
||||
(range (- (syntax-e #'nfields)
|
||||
(length (syntax->list #'(f …))))))))
|
||||
(define-trees #'(bt-fields-id
|
||||
(field …)
|
||||
[struct struct-field …] …)))]))
|
||||
|
||||
(gs bt-fields
|
||||
16
|
||||
(a b c)
|
||||
[sab a b]
|
||||
[sbc b c]
|
||||
[sabc a b c])
|
||||
|
||||
(define-type btac (bt-fields a c))
|
||||
|
||||
(check-equal?:
|
||||
(~> (ann (with-c (sab→tree 1 2) 'nine)
|
||||
((bt-fields a b c) One Positive-Byte 'nine))
|
||||
force
|
||||
flatten
|
||||
(filter Some? _)
|
||||
(map Some-v _)
|
||||
list->set)
|
||||
(set 1 2 'nine))
|
||||
|
||||
|
||||
(check-equal?:
|
||||
(call-with-values
|
||||
#λ(tree→sab (sab→tree 1 2))
|
||||
list)
|
||||
'(1 2))
|
||||
|
||||
(check-equal?:
|
||||
(call-with-values
|
||||
#λ(tree→sabc (ann (with-c (sab→tree 1 2) 'nine)
|
||||
((bt-fields a b c) One Positive-Byte 'nine)))
|
||||
list)
|
||||
'(1 2 nine))
|
||||
|
||||
(check-equal?:
|
||||
(call-with-values
|
||||
#λ(tree→sabc (with-c (sab→tree 'NONE 'NONE) 'NONE))
|
||||
list)
|
||||
'(NONE NONE NONE))
|
||||
|
||||
(check-equal?:
|
||||
(call-with-values
|
||||
#λ(tree→sab (without-c (with-c (sab→tree 'NONE 'NONE) 'NONE)))
|
||||
list)
|
||||
'(NONE NONE))
|
||||
|
||||
(check-equal?:
|
||||
(call-with-values
|
||||
#λ(tree→sbc (without-a (with-c (sab→tree 'NONE 'NONE) 'NONE)))
|
||||
list)
|
||||
'(NONE NONE))
|
||||
|
||||
(check-equal?:
|
||||
(call-with-values
|
||||
#λ(tree→sbc (without-a (with-c (sab→tree 1 2) 3)))
|
||||
list)
|
||||
'(2 3))
|
||||
|
|
@ -1,39 +0,0 @@
|
|||
#lang typed/racket
|
||||
|
||||
(require phc-adt
|
||||
(lib "phc-graph/graph-type.hl.rkt"))
|
||||
(adt-init)
|
||||
|
||||
(provide g1)
|
||||
|
||||
(define-graph-type g1
|
||||
[City [name : String]
|
||||
[streets : (Listof Street)]
|
||||
[citizens : (Listof Person)]]
|
||||
[Street [name : String]
|
||||
[houses : (Listof House)]]
|
||||
[House [owner : Person]]
|
||||
[Person [name : String]]
|
||||
#:invariant City.citizens._ ∈ City.streets._.houses._.owner
|
||||
#:invariant City.citizens._ ∋ City.streets._.houses._.owner)
|
||||
|
||||
(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))
|
||||
|
|
@ -1,102 +0,0 @@
|
|||
#lang type-expander
|
||||
|
||||
(require "traversal-util.rkt"
|
||||
"ck.rkt")
|
||||
|
||||
(define-type Foo (Listof String))
|
||||
|
||||
(define-fold f₁ t₁ Null String)
|
||||
(define-fold f₂ t₂ (Pairof Null Null) String)
|
||||
(define-fold f₃ t₃ String String)
|
||||
(define-fold f₄ t₄ (Pairof Null String) String)
|
||||
(define-fold f₅ t₅ (Listof Null) String)
|
||||
(define-fold f₆ t₆ (List Null (Pairof Null Null) Null) String)
|
||||
(define-fold f₇ t₇ (Listof String) String)
|
||||
(define-fold f₈ t₈ (List String Foo (Listof String)) String)
|
||||
(define-fold f₉ t₉ (List (Listof String) Foo (Listof String)) (Listof String))
|
||||
(define-fold f₁₀ t₁₀ (List String Foo (Listof String)) (Listof String))
|
||||
(define-fold f₁₁ t₁₁ (List (Listof String) (Listof Number)) (Listof String))
|
||||
(define-fold f₁₂ t₁₂ (List (Listof String) (Listof String)) (Listof String))
|
||||
(define-fold f₁₃ t₁₃
|
||||
(List Null
|
||||
(Pairof (List (List Null))
|
||||
(List (List Null)))
|
||||
Null)
|
||||
String)
|
||||
|
||||
(define (string->symbol+acc [x : String] [acc : Integer])
|
||||
(values (string->symbol x) (add1 acc)))
|
||||
|
||||
(check-equal?-values: ((f₁ string? string->symbol+acc) '() 0)
|
||||
'() 0)
|
||||
|
||||
(check-equal?-values: ((f₁ string? string->symbol+acc) '() 0)
|
||||
: (Values Null Integer)
|
||||
'() 0)
|
||||
|
||||
(check-equal?-values: ((f₂ string? string->symbol+acc) '(() . ()) 0)
|
||||
: (Values (Pairof Null Null) Integer)
|
||||
'(() . ()) 0)
|
||||
|
||||
(check-equal?-values: ((f₃ string? string->symbol+acc) "abc" 0)
|
||||
: (Values Symbol Integer)
|
||||
'abc 1)
|
||||
|
||||
(check-equal?-values: ((f₄ string? string->symbol+acc) '(() . "def") 0)
|
||||
: (Values (Pairof Null Symbol) Integer)
|
||||
'(() . def) 1)
|
||||
|
||||
(check-equal?-values: ((f₅ string? string->symbol+acc) '(() () () ()) 0)
|
||||
: (Values (Listof Null) Integer)
|
||||
'(() () () ()) 0)
|
||||
|
||||
(check-equal?-values: ((f₅ string? string->symbol+acc) '(()) 0)
|
||||
: (Values (Listof Null) Integer)
|
||||
'(()) 0)
|
||||
|
||||
(check-equal?-values: ((f₅ string? string->symbol+acc) '() 0)
|
||||
: (Values (Listof Null) Integer)
|
||||
'() 0)
|
||||
|
||||
(check-equal?-values: ((f₆ string? string->symbol+acc) '(() (() . ()) ()) 0)
|
||||
: (Values (List Null (Pairof Null Null) Null) Integer)
|
||||
'(() (() . ()) ()) 0)
|
||||
|
||||
(check-equal?-values: ((f₇ string? string->symbol+acc) '("abc" "def" "ghi") 0)
|
||||
: (Values (Listof Symbol) Integer)
|
||||
'(abc def ghi) 3)
|
||||
|
||||
(check-equal?-values: ((f₈ string? string->symbol+acc) '("abc" ("def" "ghi")
|
||||
("jkl" "mno"))
|
||||
0)
|
||||
: (Values (List Symbol (Listof String) (Listof Symbol))
|
||||
Integer)
|
||||
'(abc ("def" "ghi") (jkl mno)) 3)
|
||||
|
||||
(check-equal?-values: ((f₉ (make-predicate (Listof String))
|
||||
(λ ([l : (Listof String)] [acc : Integer])
|
||||
(values (map string->symbol l)
|
||||
(add1 acc))))
|
||||
'(("a" "b" "c")
|
||||
("def" "ghi")
|
||||
("jkl" "mno"))
|
||||
0)
|
||||
: (Values (List (Listof Symbol)
|
||||
(Listof String)
|
||||
(Listof Symbol))
|
||||
Integer)
|
||||
'((a b c) ("def" "ghi") (jkl mno)) 2)
|
||||
|
||||
(check-equal?-values: ((f₁₀ (make-predicate (Listof String))
|
||||
(λ ([l : (Listof String)] [acc : Integer])
|
||||
(values (map string->symbol l)
|
||||
(add1 acc))))
|
||||
'("abc"
|
||||
("def" "ghi")
|
||||
("jkl" "mno"))
|
||||
0)
|
||||
: (Values (List String
|
||||
(Listof String)
|
||||
(Listof Symbol))
|
||||
Integer)
|
||||
'("abc" ("def" "ghi") (jkl mno)) 1)
|
||||
|
|
@ -1,114 +0,0 @@
|
|||
#lang typed/racket
|
||||
|
||||
(require "traversal-util.rkt"
|
||||
type-expander
|
||||
phc-adt
|
||||
"ck.rkt"
|
||||
"../dispatch-union.rkt") ;; DEBUG
|
||||
(adt-init)
|
||||
|
||||
(define-fold f₁ t₁ (tagged tg [a String] [b Boolean]) String)
|
||||
(define-fold f₂ t₂ (U (tagged tg [a String] [b Boolean])) String)
|
||||
(define-fold f₃ t₃ (U (tagged tg [a String] [b Boolean])
|
||||
(tagged tg [a Boolean] [c String]))
|
||||
String)
|
||||
(define-fold f₄ t₄ (U (tagged tg [a String] [b Boolean])
|
||||
String
|
||||
(tagged tg [a Boolean] [c String]))
|
||||
String)
|
||||
(define-fold f₅ t₅ (U (tagged t0)
|
||||
String
|
||||
(tagged tg [a Boolean] [c String]))
|
||||
String)
|
||||
(define-fold f₆ t₆ (U String
|
||||
(tagged tg [a String] [b Boolean]))
|
||||
String)
|
||||
|
||||
(define (string->symbol+acc [x : String] [acc : Integer])
|
||||
(values (string->symbol x) (add1 acc)))
|
||||
|
||||
(check-equal?-values:
|
||||
((f₁ string? string->symbol+acc) (tagged tg [a "abc"] [b #f]) 0)
|
||||
: (Values (tagged tg [a Symbol] [b Boolean]) Integer)
|
||||
(tagged tg [a 'abc] [b #f]) 1)
|
||||
|
||||
(check-equal?-values:
|
||||
((f₂ string? string->symbol+acc) (tagged tg [a "abc"] [b #f]) 0)
|
||||
: (Values (U (tagged tg [a Symbol] [b Boolean])) Integer)
|
||||
(tagged tg [a 'abc] [b #f]) 1)
|
||||
|
||||
(check-equal?-values:
|
||||
((f₃ string? string->symbol+acc) (tagged tg [a "abc"] [b #f]) 0)
|
||||
: (Values (U (tagged tg [a Symbol] [b Boolean])
|
||||
(tagged tg [a Boolean] [c Symbol]))
|
||||
Integer)
|
||||
(tagged tg [a 'abc] [b #f]) 1)
|
||||
|
||||
(check-equal?-values:
|
||||
((f₃ string? string->symbol+acc) (tagged tg [a #t] [c "def"]) 0)
|
||||
: (Values (U (tagged tg [a Symbol] [b Boolean])
|
||||
(tagged tg [a Boolean] [c Symbol]))
|
||||
Integer)
|
||||
(tagged tg [a #t] [c 'def]) 1)
|
||||
|
||||
(check-equal?-values:
|
||||
((f₄ string? string->symbol+acc) (tagged tg [a "abc"] [b #f]) 0)
|
||||
: (Values (U (tagged tg [a Symbol] [b Boolean])
|
||||
Symbol
|
||||
(tagged tg [a Boolean] [c Symbol]))
|
||||
Integer)
|
||||
(tagged tg [a 'abc] [b #f]) 1)
|
||||
|
||||
(check-equal?-values:
|
||||
((f₄ string? string->symbol+acc) "ghi" 0)
|
||||
: (Values (U (tagged tg [a Symbol] [b Boolean])
|
||||
Symbol
|
||||
(tagged tg [a Boolean] [c Symbol]))
|
||||
Integer)
|
||||
'ghi 1)
|
||||
|
||||
(check-equal?-values:
|
||||
((f₄ string? string->symbol+acc) (tagged tg [a #t] [c "def"]) 0)
|
||||
: (Values (U (tagged tg [a Symbol] [b Boolean])
|
||||
Symbol
|
||||
(tagged tg [a Boolean] [c Symbol]))
|
||||
Integer)
|
||||
(tagged tg [a #t] [c 'def]) 1)
|
||||
|
||||
(check-equal?-values:
|
||||
((f₅ string? string->symbol+acc) (tagged t0 #:instance) 0)
|
||||
: (Values (U (tagged t0)
|
||||
Symbol
|
||||
(tagged tg [a Boolean] [c Symbol]))
|
||||
Integer)
|
||||
(tagged t0 #:instance) 0)
|
||||
|
||||
(check-equal?-values:
|
||||
((f₅ string? string->symbol+acc) "ghi" 0)
|
||||
: (Values (U (tagged t0)
|
||||
Symbol
|
||||
(tagged tg [a Boolean] [c Symbol]))
|
||||
Integer)
|
||||
'ghi 1)
|
||||
|
||||
(check-equal?-values:
|
||||
((f₅ string? string->symbol+acc) (tagged tg [a #t] [c "def"]) 0)
|
||||
: (Values (U (tagged t0)
|
||||
Symbol
|
||||
(tagged tg [a Boolean] [c Symbol]))
|
||||
Integer)
|
||||
(tagged tg [a #t] [c 'def]) 1)
|
||||
|
||||
(check-equal?-values:
|
||||
((f₆ string? string->symbol+acc) (tagged tg [a "abc"] [b #f]) 0)
|
||||
: (Values (U (tagged tg [a Symbol] [b Boolean])
|
||||
Symbol)
|
||||
Integer)
|
||||
(tagged tg [a 'abc] [b #f]) 1)
|
||||
|
||||
(check-equal?-values:
|
||||
((f₆ string? string->symbol+acc) "ghi" 0)
|
||||
: (Values (U (tagged tg [a Symbol] [b Boolean])
|
||||
Symbol)
|
||||
Integer)
|
||||
'ghi 1)
|
||||
|
|
@ -1,22 +0,0 @@
|
|||
#lang typed/racket
|
||||
(require (for-syntax syntax/parse
|
||||
backport-template-pr1514/experimental/template
|
||||
type-expander/expander)
|
||||
"../traversal.hl.rkt")
|
||||
|
||||
(provide define-fold)
|
||||
|
||||
(define-syntax define-fold
|
||||
(syntax-parser
|
||||
[(_ _function-name:id
|
||||
_type-name:id
|
||||
whole-type:type
|
||||
_type-to-replaceᵢ:type ...)
|
||||
(with-folds
|
||||
(λ ()
|
||||
(template
|
||||
(begin
|
||||
(define-type _type-name
|
||||
(∀-replace-in-type whole-type _type-to-replaceᵢ ...))
|
||||
(define _function-name
|
||||
(λ-replace-in-instance whole-type _type-to-replaceᵢ ...))))))]))
|
||||
124
thoughts.rkt
124
thoughts.rkt
|
|
@ -1,124 +0,0 @@
|
|||
#lang type-expander/lang
|
||||
|
||||
#|
|
||||
Adding fields to the prefix path makes it weaker
|
||||
Adding fields to the postfix path makes it stronger
|
||||
|
||||
(Expand prefix postfix)
|
||||
=> (and prefixᵢ postfix) …
|
||||
Also could be expanded as:
|
||||
=> (and prefix postfixᵢ) …
|
||||
|
||||
Rewording ((u pre_x pre_x2) pre_a _ post_b (u post_c post_c2)
|
||||
=> property holds iff
|
||||
pre1 = a
|
||||
and (pre2 = x or pre2 = x2)
|
||||
and post1 = b
|
||||
and (post2 = c or post2 = c2)
|
||||
|#
|
||||
|
||||
(define-type (F A) (I (I A)))
|
||||
(define-type (I A) (→ A Void))
|
||||
|
||||
(define-type eqA1 (F (Pairof (List* (∩ (G 'a1) (G 'a2)) (∩ (G 'u1) (G 'u2)))
|
||||
(List (G 'b) (G 'c)))))
|
||||
|
||||
(define-type eqB1 (F (∩ (Pairof (List* (G 'a1) (∩ (G 'u1) (G 'u2)))
|
||||
(List (G 'b) (G 'c)))
|
||||
(Pairof (List* (G 'a2) (∩ (G 'u1) (G 'u2)))
|
||||
(List (G 'b) (G 'c))))))
|
||||
|
||||
(define-type eqC1 (F (∩ (Pairof (List* (∩ (G 'a1) (G 'a2)) (∩ (G 'u1)))
|
||||
(List (G 'b) (G 'c)))
|
||||
(Pairof (List* (∩ (G 'a1) (G 'a2)) (∩ (G 'u2)))
|
||||
(List (G 'b) (G 'c))))))
|
||||
|
||||
(define-type weakerD1 (F (∩ (Pairof (List* (∩ (G 'a1) (G 'a2)) (∩ (G 'u1)))
|
||||
(List (G 'b) (G 'c))))))
|
||||
|
||||
(define-type strongerE1 (F (∩ (Pairof (List* (∩ (G 'a1) (G 'a2)) (∩ (G 'u1) (G 'u2)))
|
||||
(∩ (List (G 'b) (G 'c))
|
||||
(List (G 'b2) (G 'c)))))))
|
||||
|
||||
(define-type strongerF1 (F (∩ (Pairof (List* (∩ (G 'a1) (G 'a2)) (∩ (G 'u1) (G 'u2)))
|
||||
(Pairof (G 'b) (∩ (List (G 'c))
|
||||
(List (G 'c2))))))))
|
||||
|
||||
(define-type altF1 (F (∩ (Pairof (List* (∩ (G 'a1) (G 'a2)) (∩ (G 'u1) (G 'u2)))
|
||||
(Pairof (G 'b) (List (G 'c))))
|
||||
(Pairof (List* (∩ (G 'a1) (G 'a2)) (∩ (G 'u1) (G 'u2)))
|
||||
(Pairof (G 'b) (List (G 'c2)))))))
|
||||
|
||||
(ann (ann (λ (x) (void)) eqA1) eqB1)
|
||||
(ann (ann (λ (x) (void)) eqA1) eqC1)
|
||||
(ann (ann (λ (x) (void)) eqB1) eqA1)
|
||||
(ann (ann (λ (x) (void)) eqB1) eqC1)
|
||||
(ann (ann (λ (x) (void)) eqC1) eqA1)
|
||||
(ann (ann (λ (x) (void)) eqC1) eqB1)
|
||||
(ann (ann (λ (x) (void)) eqA1) weakerD1)
|
||||
(ann (ann (λ (x) (void)) eqB1) weakerD1)
|
||||
(ann (ann (λ (x) (void)) eqC1) weakerD1)
|
||||
;(ann (ann (λ (x) (void)) eqA1) strongerD1) ;; rejected, as it should
|
||||
(ann (ann (λ (x) (void)) strongerE1) eqA1)
|
||||
;(ann (ann (λ (x) (void)) eqA1) strongerE1) ;; rejected, as it should
|
||||
(ann (ann (λ (x) (void)) strongerF1) eqA1)
|
||||
;(ann (ann (λ (x) (void)) eqA1) strongerF1) ;; rejected, as it should
|
||||
(ann (ann (λ (x) (void)) altF1) eqA1)
|
||||
;(ann (ann (λ (x) (void)) eqA1) altF1) ;; rejected, as it should
|
||||
(ann (ann (λ (x) (void)) altF1) strongerF1)
|
||||
(ann (ann (λ (x) (void)) strongerF1) altF1)
|
||||
|
||||
|
||||
|
||||
|
||||
(let ()
|
||||
(define-type eqA2 (F (case→ (→ (List 'b 'c) 'a1)
|
||||
(→ (List 'b 'c) 'a2))))
|
||||
|
||||
(define-type eqB2 (F (case→ (→ (List 'b 'c)
|
||||
(U 'a1 'a2)))))
|
||||
|
||||
(ann (ann (λ (x) (void)) eqA2) eqB2)
|
||||
#;(ann (ann (λ (x) (void)) eqB2) eqA2))
|
||||
|
||||
;(let ()
|
||||
(define-type (G A) (F A))
|
||||
(define-type-expander (+ stx) (syntax-case stx () [(_ . rest) #'(∩ . rest)]))
|
||||
(define-type-expander (* stx) (syntax-case stx () [(_ . rest) #'(U . rest)]))
|
||||
|
||||
(define-type eqA2 (F (+ (* (G 'b) (G 'c) (G 'a1))
|
||||
(* (G 'b) (G 'c) (G 'a2)))))
|
||||
|
||||
(define-type eqB2 (F (+ (* (G 'b) (G 'c) (+ (G 'a1) (G 'a2))))))
|
||||
|
||||
(define-type Weaker2 (F (+ (* (G 'b) (G 'c) (G 'a1)))))
|
||||
|
||||
(ann (ann (λ (x) (void)) eqA2) eqB2)
|
||||
(ann (ann (λ (x) (void)) eqB2) eqA2)
|
||||
(ann (ann (λ (x) (void)) eqA2) Weaker2)
|
||||
(ann (ann (λ (x) (void)) eqB2) Weaker2)
|
||||
;(ann (ann (λ (x) (void)) Weaker2) eqA2)
|
||||
;(ann (ann (λ (x) (void)) Weaker2) eqB2)
|
||||
;)
|
||||
|
||||
|
||||
|
||||
(let ()
|
||||
(define-type weaker3
|
||||
(F (∩ (G (Rec R (List* 'a Any R)))
|
||||
(G (Rec R (List* Any 'b R))))))
|
||||
(define-type stronger3
|
||||
(F (∩ (G (List* 'a Any (Rec R (List* 'a Any R))))
|
||||
(G (List* Any 'b (Rec R (List* Any 'b R)))))))
|
||||
|
||||
(ann (ann (λ (x) (void)) stronger3) weaker3)
|
||||
)
|
||||
|
||||
#|
|
||||
Put the U ∩ inside the positional list?
|
||||
What about loops of different sizes => won't work
|
||||
What about merging all the invariants blindly => won't work, but we can
|
||||
special-case merging these regexp-like invariants, as long as the merging
|
||||
doesn't need any info about the regexp itself
|
||||
(e.g. all are "merge the second elements")
|
||||
|#
|
||||
|
|
@ -1,76 +0,0 @@
|
|||
#lang racket
|
||||
(require plot)
|
||||
(parameterize ([plot-x-transform log-transform]
|
||||
[plot-x-ticks (log-ticks #:base 2)]
|
||||
[plot-y-transform log-transform]
|
||||
[plot-y-ticks (log-ticks #:base 2)])
|
||||
(plot
|
||||
#:x-min 1 #:x-max 3000
|
||||
#:y-min 1 #:y-max 3000
|
||||
(list
|
||||
(lines #:color 1
|
||||
'(#(16 16)
|
||||
#(17 25)
|
||||
#(20 26)
|
||||
#(24 29)
|
||||
#(28 31)
|
||||
#(32 35) ; 20 with shared implementation & type, 22 shrd impl only
|
||||
#(33 60)
|
||||
#(40 67)
|
||||
#(48 77)
|
||||
#(56 80)
|
||||
#(64 92) ;; 46
|
||||
#(65 168)
|
||||
#(80 189)
|
||||
#(96 216)
|
||||
#(128 276)
|
||||
#(129 562)
|
||||
#(256 911)
|
||||
#(257 2078)
|
||||
#(512 3000) ;; rough estimation
|
||||
))
|
||||
;; with shared implementation & type:
|
||||
(lines #:color 2
|
||||
'(#(16 11)
|
||||
;#(17 25)
|
||||
;#(20 26)
|
||||
;#(24 29)
|
||||
;#(28 31)
|
||||
#(32 20)
|
||||
;#(33 60)
|
||||
;#(40 67)
|
||||
;#(48 77)
|
||||
;#(56 80)
|
||||
#(64 46)
|
||||
;#(65 168)
|
||||
;#(80 189)
|
||||
;#(96 216)
|
||||
#(128 120)
|
||||
;#(129 562)
|
||||
#(256 363)
|
||||
;#(257 2078)
|
||||
#(512 1317)
|
||||
))
|
||||
;; further optimisations
|
||||
(lines #:color 3
|
||||
'(#(16 10)
|
||||
#(17 12)
|
||||
#(20 13)
|
||||
#(24 13)
|
||||
#(28 14)
|
||||
#(32 15)
|
||||
#(33 22)
|
||||
#(40 24)
|
||||
#(48 26)
|
||||
#(56 28)
|
||||
#(64 30)
|
||||
#(65 49)
|
||||
#(80 54)
|
||||
#(96 57)
|
||||
#(128 69)
|
||||
#(129 129)
|
||||
#(256 186)
|
||||
#(257 372)
|
||||
#(512 587)
|
||||
)))))
|
||||
|
||||
397
traversal.hl.rkt
397
traversal.hl.rkt
|
|
@ -1,397 +0,0 @@
|
|||
#lang hyper-literate typed/racket/base #:no-require-lang #:no-auto-require
|
||||
@(require racket/require
|
||||
scribble-enhanced/doc
|
||||
racket/require
|
||||
hyper-literate
|
||||
(subtract-in scribble/struct scribble-enhanced/doc)
|
||||
scribble/decode
|
||||
(for-label racket/format
|
||||
racket/promise
|
||||
racket/list
|
||||
syntax/parse
|
||||
syntax/parse/experimental/template
|
||||
type-expander
|
||||
(except-in (subtract-in typed/racket/base type-expander)
|
||||
values)
|
||||
(only-in racket/base values)
|
||||
(subtract-in racket/contract typed/racket/base)
|
||||
phc-toolkit
|
||||
phc-toolkit/untyped-only
|
||||
remember))
|
||||
@(unless-preexpanding
|
||||
(require (for-label (submod ".."))))
|
||||
@doc-lib-setup
|
||||
|
||||
@title[#:style manual-doc-style
|
||||
#:tag "traversal"
|
||||
#:tag-prefix "phc-graph/traversal"]{Parametric replacement of parts of
|
||||
data structures}
|
||||
|
||||
@(chunks-toc-prefix
|
||||
'("(lib phc-graph/scribblings/phc-graph-implementation.scrbl)"
|
||||
"phc-graph/traversal"))
|
||||
|
||||
@(table-of-contents)
|
||||
|
||||
@(declare-exporting (lib "phc-graph/traversal.hl.rkt"))
|
||||
|
||||
@section{Introduction}
|
||||
|
||||
This utility allows functionally updating parts of data structures. The
|
||||
@racket[define-fold] macro takes the type of the whole data structure and a
|
||||
list of type names associated with their predicate. It locates all literal
|
||||
occurrences of those type names within the data structure, and identifies
|
||||
those locations as the parts to replace. The type of the whole data structure
|
||||
is expressed as a syntactic tree. Within that syntactic tree, only the parts
|
||||
which are syntactically equal to one of the types to replace are considered.
|
||||
|
||||
As an example, suppose the whole type is
|
||||
@racket[(List Foo Number (Listof String))], and @racket[Foo] is defined as:
|
||||
|
||||
@racketblock[(define-type Foo (Listof String))]
|
||||
|
||||
If @racket[Foo] is given as a type to replace, and its replacement type is
|
||||
@racket[(Listof Symbol)], then the type of the result would be:
|
||||
|
||||
@racketblock[(List (Listof Symbol) Number (Listof String))]
|
||||
|
||||
The second occurrence of @racket[(Listof String)], although semantically
|
||||
equivalent to the type to replace, @racket[Foo], will not be altered, as it is
|
||||
not expressed syntactically using the @racket[Foo] identifier.
|
||||
|
||||
@defform[(define-fold function-name type-name whole-type type-to-replaceᵢ ...)]{
|
||||
The @racket[define-fold] macro takes the type of the whole data structure, and
|
||||
a list of types to replace, each associated with a predicate for that type. It
|
||||
@;defines @racket[_name] as a macro, which behaves as follows:
|
||||
defines @racket[(type-name Tᵢ ...)] as a polymorphic type, with one type
|
||||
argument for each @racket[type-to-replaceᵢ], such that
|
||||
|
||||
@racketblock[(type-name type-to-replaceᵢ ...)]
|
||||
|
||||
is the same type as
|
||||
|
||||
@racketblock[whole-type]
|
||||
|
||||
In other words, @racket[type-name] is defined as @racket[whole-type], except
|
||||
that each syntactic occurrence of a @racket[type-to-replaceᵢ] is replaced with
|
||||
the corresponding type argument @racket[Tᵢ].
|
||||
|
||||
It also defines @racket[function-name] as a function, with the type
|
||||
|
||||
@racketblock[(∀ (Aᵢ ... Bᵢ ... Acc)
|
||||
(→ (?@ (→ Any Boolean : Aᵢ)
|
||||
(→ Aᵢ Acc (Values Bᵢ Acc)))
|
||||
...
|
||||
(→ (type-name Aᵢ ...)
|
||||
Acc
|
||||
(Values (type-name Bᵢ ...)
|
||||
Acc))))]
|
||||
|
||||
We use the @racket[?@] notation from
|
||||
@racketmodname[syntax/parse/experimental/template] to indicate that the
|
||||
function accepts a predicate, followed by an update function, followed by
|
||||
another predicate, and so on. For example, the function type when there are
|
||||
three @racket[type-to-replaceᵢ] would be:
|
||||
|
||||
@racketblock[(∀ (A₁ A₂ A₃ B₁ B₂ B₃ Acc)
|
||||
(→ (→ Any Boolean : A₁)
|
||||
(→ A₁ Acc (Values B₁ Acc))
|
||||
(→ Any Boolean : A₂)
|
||||
(→ A₂ Acc (Values B₂ Acc))
|
||||
(→ Any Boolean : A₃)
|
||||
(→ A₃ Acc (Values B₃ Acc))
|
||||
(→ (type-name A₁ A₂ A₃)
|
||||
Acc
|
||||
(Values (type-name B₁ B₂ B₃)
|
||||
Acc))))]
|
||||
|
||||
The @racket[function-name] replaces all values in the whole data structure
|
||||
which are present in locations corresponding to a @racket[type-to-replaceᵢ] in
|
||||
the @racket[whole-type]. It expects those values to have the type @racket[Aᵢ],
|
||||
i.e. its input type is not restricted to @racket[whole-type], any polymorphic
|
||||
instance of @racket[type-name] is valid. Each value is passed as an argument
|
||||
to the corresponding update function with type
|
||||
@racket[(→ Aᵢ Acc (Values Bᵢ Acc))], and the result of type @racket[Bᵢ] is
|
||||
used as a replacement.
|
||||
|
||||
An accumulator value, with the type @racket[Acc], is threaded through all
|
||||
calls to all update functions, so that the update functions can communicate
|
||||
state in a functional way.}
|
||||
|
||||
@section{Implementation}
|
||||
|
||||
@subsection{Caching the results of @racket[define-fold]}
|
||||
|
||||
@chunk[<with-folds>
|
||||
(define-for-syntax get-f-cache (make-parameter #f))
|
||||
(define-for-syntax get-τ-cache (make-parameter #f))
|
||||
(define-for-syntax get-f-defs (make-parameter #f))
|
||||
(define-for-syntax get-τ-defs (make-parameter #f))
|
||||
(define-for-syntax (with-folds thunk)
|
||||
;; TODO: should probably use bound-id instead.
|
||||
(parameterize ([get-f-cache (make-mutable-free-id-tree-table)]
|
||||
[get-τ-cache (make-mutable-free-id-tree-table)]
|
||||
[get-f-defs (box '())]
|
||||
[get-τ-defs (box '())])
|
||||
(define/with-syntax thunk-result (thunk))
|
||||
(with-syntax ([([f-id f-body f-type] …) (unbox (get-f-defs))]
|
||||
[([τ-id . τ-body] …) (unbox (get-τ-defs))])
|
||||
#`(begin (define-type τ-id τ-body) …
|
||||
(: f-id f-type) …
|
||||
(define f-id f-body) …
|
||||
thunk-result))))]
|
||||
|
||||
@;@subsection{…}
|
||||
|
||||
|
||||
@; TODO: recursively go down the tree. If there are no replacements, return #f
|
||||
@; all the way up, so that a simple identity function can be applied in these
|
||||
@; cases.
|
||||
|
||||
|
||||
@CHUNK[<api>
|
||||
(define-template-metafunction (replace-in-type stx)
|
||||
(syntax-case stx ()
|
||||
[(_ _whole-type [_type-to-replaceᵢ _Tᵢ] …)
|
||||
#`(#,(syntax-local-template-metafunction-introduce
|
||||
(fold-τ #'(_whole-type _type-to-replaceᵢ …))) _Tᵢ …)]))]
|
||||
|
||||
@CHUNK[<api>
|
||||
(define-template-metafunction (∀-replace-in-type stx)
|
||||
(syntax-case stx ()
|
||||
[(_ _whole-type _type-to-replaceᵢ …)
|
||||
(syntax-local-template-metafunction-introduce
|
||||
(fold-τ #'(_whole-type _type-to-replaceᵢ …)))]))]
|
||||
|
||||
@CHUNK[<fold-τ>
|
||||
(define fold-τ
|
||||
(syntax-parser
|
||||
[(_whole-type:type _type-to-replaceᵢ:type …)
|
||||
#:with rec-args #'([_type-to-replaceᵢ _Tᵢ] …)
|
||||
(cached [τ-
|
||||
(get-τ-cache)
|
||||
(get-τ-defs)
|
||||
#'(_whole-type _type-to-replaceᵢ …)]
|
||||
(define replacements (make-immutable-free-id-tree-table
|
||||
(map syntax-e
|
||||
(syntax->list
|
||||
#'([_type-to-replaceᵢ . _Tᵢ] …)))))
|
||||
#`(∀ (_Tᵢ …)
|
||||
#,(syntax-parse #'_whole-type
|
||||
#:literals (Null Pairof Listof List Vectorof Vector U tagged)
|
||||
<type-cases>)))]))]
|
||||
|
||||
@CHUNK[<cached>
|
||||
(begin-for-syntax
|
||||
(define-syntax-rule (cached [base cache defs key] . body)
|
||||
(begin
|
||||
(unless (and cache defs)
|
||||
(error "fold-τ and fold-f must be called within with-folds"))
|
||||
(if (dict-has-key? cache key)
|
||||
(dict-ref cache key)
|
||||
(let ([base #`#,(gensym 'base)])
|
||||
(dict-set! cache key base)
|
||||
(let ([result (let () . body)])
|
||||
(set-box! defs `([,base . ,result] . ,(unbox defs)))
|
||||
base))))))]
|
||||
|
||||
@CHUNK[<api>
|
||||
(define-template-metafunction (replace-in-instance stx)
|
||||
(syntax-case stx ()
|
||||
[(_ _whole-type [_type-to-replaceᵢ _predicateᵢ _updateᵢ] …)
|
||||
#`(#,(syntax-local-template-metafunction-introduce
|
||||
(fold-f #'(_whole-type _type-to-replaceᵢ …)))
|
||||
{?@ _predicateᵢ _updateᵢ} …)]))]
|
||||
|
||||
@CHUNK[<api>
|
||||
(define-template-metafunction (λ-replace-in-instance stx)
|
||||
(syntax-case stx ()
|
||||
[(_ _whole-type _type-to-replaceᵢ …)
|
||||
(syntax-local-introduce
|
||||
(fold-f #'(_whole-type _type-to-replaceᵢ …)))]))]
|
||||
|
||||
@CHUNK[<fold-f>
|
||||
(define fold-f
|
||||
(syntax-parser
|
||||
[(_whole-type:type _type-to-replaceᵢ:type …)
|
||||
#:with rec-args #'([_type-to-replaceᵢ _predicateᵢ _updateᵢ] …)
|
||||
(define replacements (make-immutable-free-id-tree-table
|
||||
(map syntax-e
|
||||
(syntax->list
|
||||
#'([_type-to-replaceᵢ . _updateᵢ] …)))))
|
||||
(define/with-syntax _args #'({?@ _predicateᵢ _updateᵢ} …))
|
||||
(cached [f-
|
||||
(get-f-cache)
|
||||
(get-f-defs)
|
||||
#'(_whole-type _type-to-replaceᵢ …)]
|
||||
#`[(λ ({?@ _predicateᵢ _updateᵢ} …)
|
||||
(λ (v acc)
|
||||
#,(syntax-parse #'_whole-type
|
||||
#:literals (Null Pairof Listof List Vectorof Vector U tagged)
|
||||
<f-cases>)))
|
||||
(∀ (_Aᵢ … _Bᵢ … Acc)
|
||||
(→ (?@ (→ Any Boolean : _Aᵢ)
|
||||
(→ _Aᵢ Acc (Values _Bᵢ Acc)))
|
||||
…
|
||||
(→ (replace-in-type _whole-type
|
||||
[_type-to-replaceᵢ _Aᵢ] …)
|
||||
Acc
|
||||
(Values (replace-in-type _whole-type
|
||||
[_type-to-replaceᵢ _Bᵢ] …)
|
||||
Acc))))])]))]
|
||||
|
||||
@chunk[<f-cases>
|
||||
[t
|
||||
#:when (dict-has-key? replacements #'t)
|
||||
#:with _update (dict-ref replacements #'t)
|
||||
#'(_update v acc)]]
|
||||
|
||||
@chunk[<type-cases>
|
||||
[t
|
||||
#:when (dict-has-key? replacements #'t)
|
||||
#:with _T (dict-ref replacements #'t)
|
||||
#'_T]]
|
||||
|
||||
@chunk[<type-cases>
|
||||
[(~or Null (List))
|
||||
#'Null]]
|
||||
|
||||
@chunk[<f-cases>
|
||||
[(~or Null (List))
|
||||
#'(values v acc)]]
|
||||
|
||||
|
||||
@CHUNK[<type-cases>
|
||||
[(Pairof X Y)
|
||||
#'(Pairof (replace-in-type X . rec-args)
|
||||
(replace-in-type Y . rec-args))]]
|
||||
|
||||
@CHUNK[<f-cases>
|
||||
[(Pairof X Y)
|
||||
#'(let*-values ([(result-x acc-x)
|
||||
((replace-in-instance X . rec-args) (car v) acc)]
|
||||
[(result-y acc-y)
|
||||
((replace-in-instance Y . rec-args) (cdr v) acc-x)])
|
||||
(values (cons result-x result-y) acc-y))]]
|
||||
|
||||
@CHUNK[<type-cases>
|
||||
[(Listof X)
|
||||
#'(Listof (replace-in-type X . rec-args))]]
|
||||
|
||||
@CHUNK[<f-cases>
|
||||
[(Listof X)
|
||||
#'(foldl-map (replace-in-instance X . rec-args)
|
||||
acc v)]]
|
||||
|
||||
@CHUNK[<type-cases>
|
||||
[(Vectorof X)
|
||||
#'(Vectorof (replace-in-type X . rec-args))]]
|
||||
|
||||
@CHUNK[<ftype-cases>
|
||||
[(Vectorof X)
|
||||
#'(vector->immutable-vector
|
||||
(list->vector
|
||||
(foldl-map (replace-in-instance X . rec-args)
|
||||
acc
|
||||
(vector->list v))))]]
|
||||
|
||||
|
||||
@CHUNK[<type-cases>
|
||||
[(List X Y …)
|
||||
#'(Pairof (replace-in-type X . rec-args)
|
||||
(replace-in-type (List Y …) . rec-args))]]
|
||||
|
||||
@CHUNK[<f-cases>
|
||||
[(List X Y …)
|
||||
#'(let*-values ([(result-x acc-x) ((replace-in-instance X . rec-args)
|
||||
(car v)
|
||||
acc)]
|
||||
[(result-y* acc-y*) ((replace-in-instance (List Y …) . rec-args)
|
||||
(cdr v)
|
||||
acc-x)])
|
||||
(values (cons result-x result-y*) acc-y*))]]
|
||||
|
||||
@CHUNK[<type-cases>
|
||||
[(U _Xⱼ …)
|
||||
#'(U (replace-in-type _Xⱼ . rec-args) …)]]
|
||||
|
||||
@CHUNK[<f-cases>
|
||||
[(U _Xⱼ …)
|
||||
#'(dispatch-union v
|
||||
([_type-to-replaceᵢ Aᵢ _predicateᵢ] …)
|
||||
[_Xⱼ ((replace-in-instance _Xⱼ . rec-args) v acc)]
|
||||
…)]]
|
||||
|
||||
@CHUNK[<type-cases>
|
||||
[(tagged _name [_fieldⱼ (~optional :colon) _Xⱼ] …)
|
||||
#'(tagged _name [_fieldⱼ : (replace-in-type _Xⱼ . rec-args)] …)]]
|
||||
|
||||
@CHUNK[<f-cases>
|
||||
[(tagged _name [_fieldⱼ (~optional :colon) _Xⱼ] …)
|
||||
#'(let*-values
|
||||
([(_resultⱼ acc)
|
||||
((replace-in-instance _Xⱼ . rec-args) (uniform-get v _fieldⱼ)
|
||||
acc)]
|
||||
…)
|
||||
(values (tagged _name #:instance [_fieldⱼ _resultⱼ] …)
|
||||
acc))]]
|
||||
|
||||
@chunk[<type-cases>
|
||||
[else-T
|
||||
#'else-T]]
|
||||
|
||||
@chunk[<f-cases>
|
||||
[else-T
|
||||
#'(values v acc)]]
|
||||
|
||||
|
||||
where @racket[foldl-map] is defined as:
|
||||
|
||||
@chunk[<foldl-map>
|
||||
(: foldl-map (∀ (A B Acc) (→ (→ A Acc (Values B Acc))
|
||||
Acc
|
||||
(Listof A)
|
||||
(Values (Listof B) Acc))))
|
||||
(define (foldl-map f acc l)
|
||||
(if (null? l)
|
||||
(values l
|
||||
acc)
|
||||
(let*-values ([(v a) (f (car l) acc)]
|
||||
[(ll aa) (foldl-map f a (cdr l))])
|
||||
(values (cons v ll)
|
||||
aa))))]
|
||||
|
||||
@section{Putting it all together}
|
||||
|
||||
@chunk[<*>
|
||||
(require racket/require
|
||||
phc-toolkit
|
||||
type-expander
|
||||
phc-adt
|
||||
"dispatch-union.rkt"
|
||||
(for-syntax "subtemplate-override.rkt"
|
||||
(subtract-in (combine-in racket/base
|
||||
syntax/parse)
|
||||
"subtemplate-override.rkt")
|
||||
backport-template-pr1514/experimental/template
|
||||
phc-toolkit/untyped
|
||||
racket/syntax
|
||||
type-expander/expander
|
||||
"free-identifier-tree-equal.rkt"
|
||||
racket/dict)
|
||||
(for-meta 2 racket/base)
|
||||
(for-meta 2 phc-toolkit/untyped)
|
||||
(for-meta 2 syntax/parse))
|
||||
|
||||
(provide (for-syntax with-folds
|
||||
replace-in-type
|
||||
∀-replace-in-type
|
||||
replace-in-instance
|
||||
λ-replace-in-instance))
|
||||
<foldl-map>
|
||||
<with-folds>
|
||||
<cached>
|
||||
(begin-for-syntax
|
||||
<api>
|
||||
<fold-τ>
|
||||
<fold-f>)]
|
||||
Loading…
Reference in New Issue
Block a user