Compare commits
No commits in common. "main" and "auto-push" have entirely different histories.
54
.travis.yml
54
.travis.yml
|
|
@ -1,64 +1,10 @@
|
|||
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.8
|
||||
- RACKET_VERSION=6.9
|
||||
- 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 .
|
||||
|
||||
after_success:
|
||||
- sh ./auto-push-master.sh
|
||||
|
|
|
|||
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.
|
||||
57
TODO.txt
57
TODO.txt
|
|
@ -1,57 +0,0 @@
|
|||
:::::::::Current task:
|
||||
|
||||
with*: optimize by naming clusters of "missing", and naming types for known flex structs
|
||||
|
||||
with*: call from phc-adt, wrappers to and from the actual structs
|
||||
|
||||
:::::::::In progress:
|
||||
|
||||
Draft the graph implementation
|
||||
|
||||
Modularity
|
||||
|
||||
:::::::::Ready:
|
||||
|
||||
Run-time checkers for invariants
|
||||
|
||||
Cleanup invariants-phantom.hl.rkt
|
||||
|
||||
Implement graph
|
||||
|
||||
Implement the first graph generation pass, with a placeholder wrapping each mapping result
|
||||
|
||||
Implement the second graph generation pass: inline nodes
|
||||
|
||||
Implement the third graph generation pass: replacing indices with promises
|
||||
|
||||
Combine the graph passes into a single macro
|
||||
|
||||
Relicensing
|
||||
|
||||
Write "middle-dot" language extension
|
||||
|
||||
Drop MathJax, directly print Unicode or render via LaTeX (speed & licensing issues)
|
||||
|
||||
::::::::Later:
|
||||
|
||||
Garbage collect graph
|
||||
|
||||
Merge tagged-anytag-match into the regular match for tagged structures
|
||||
|
||||
Check for non-intersection of the union types in traversal.hl.rkt, using the non-intersection implementation from phc-adt.
|
||||
|
||||
to infer the type for curry, check using identifier-binding if the id is imported, if so try to print its type using eval
|
||||
|
||||
:::::::::Backlog:
|
||||
|
||||
Translate https://github.com/nanopass/nanopass-framework-scheme
|
||||
|
||||
Translate https://github.com/akeep/scheme-to-c
|
||||
|
||||
Formalise what well-typed means for typed-nanopass+graph means
|
||||
|
||||
Formalise the semantics of typed-nanopass+graph programs (using redex?)
|
||||
|
||||
Write memoir
|
||||
|
||||
Proof that well-typed programs with the extensions translate to well-typed programs in plain TR, with the same semantics
|
||||
|
|
@ -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))
|
||||
|
|
@ -5,17 +5,17 @@ if test "$(git config remote.origin.url)" != "https://github.com/jsmaniac/phc-gr
|
|||
echo "Not on official repo, will not auto-push to master."
|
||||
elif test "$TRAVIS_PULL_REQUEST" != "false"; then
|
||||
echo "This is a Pull Request, will not auto-push to master."
|
||||
elif test "$TRAVIS_BRANCH" != "dev"; then
|
||||
echo "Not on dev branch (TRAVIS_BRANCH = $TRAVIS_BRANCH), will not auto-push to master."
|
||||
elif test "$TRAVIS_BRANCH" != "auto-push"; then
|
||||
echo "Not on auto-push branch (TRAVIS_BRANCH = $TRAVIS_BRANCH), will not auto-push to master."
|
||||
elif test -z "${encrypted_c195df270029_key:-}" -o -z "${encrypted_c195df270029_iv:-}"; then
|
||||
echo "Travis CI secure environment variables are unavailable, will not auto-push to master."
|
||||
else
|
||||
set -x
|
||||
echo "Automatic push to master"
|
||||
|
||||
# Git configuration:
|
||||
git config --global user.name "$(git log --format="%aN" HEAD -1) (Travis CI automatic commit)"
|
||||
git config --global user.email "$(git log --format="%aE" HEAD -1)"
|
||||
## Git configuration:
|
||||
#git config --global user.name "$(git log --format="%aN" HEAD -1) (Travis CI automatic commit)"
|
||||
#git config --global user.email "$(git log --format="%aE" HEAD -1)"
|
||||
|
||||
# SSH configuration
|
||||
mkdir -p ~/.ssh
|
||||
|
|
@ -26,24 +26,22 @@ else
|
|||
else
|
||||
echo "Error while decrypting key."
|
||||
fi
|
||||
mv travis-deploy-key-id_rsa ~/.ssh/travis-deploy-key-id_rsa
|
||||
set -x
|
||||
mv travis-deploy-key-id_rsa ~/.ssh/travis-deploy-key-id_rsa
|
||||
chmod 600 ~/.ssh/travis-deploy-key-id_rsa
|
||||
set +x
|
||||
eval `ssh-agent -s`
|
||||
set -x
|
||||
ssh-add ~/.ssh/travis-deploy-key-id_rsa
|
||||
|
||||
# Push to the auto-git branch, which can then auto-push to master, after this build finished
|
||||
# Fetch commit
|
||||
repo_url="$(git config remote.origin.url)"
|
||||
commit_hash="$(cat commit_hash)"
|
||||
ssh_repo_url="$(echo "$repo_url" | sed -e 's|^https://github.com/|git@github.com:|')"
|
||||
commit_hash="$(git rev-parse HEAD)"
|
||||
git log --oneline --decorate --graph -10
|
||||
git fetch origin auto-push
|
||||
git checkout FETCH_HEAD
|
||||
echo "$commit_hash" > commit_hash
|
||||
git add commit_hash
|
||||
git commit -m "Request to auto-push $commit_hash to master" --allow-empty
|
||||
git log --oneline --decorate --graph -10
|
||||
git push --quiet "$ssh_repo_url" HEAD:auto-push || true # do not cause a tantrum in case of race conditions.
|
||||
git clone "$repo_url" auto-git/
|
||||
cd auto-git/
|
||||
echo "[$commit_hash]"
|
||||
git checkout -qf "$commit_hash"
|
||||
git log --oneline --decorate --graph -10 "$commit_hash"
|
||||
git push --quiet "$ssh_repo_url" "$commit_hash:master" || true # Do not make a tantrum in case of race conditions
|
||||
fi
|
||||
|
|
|
|||
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,12 +0,0 @@
|
|||
#lang type-expander
|
||||
|
||||
(provide BinaryTree)
|
||||
|
||||
(require (for-syntax syntax/parse
|
||||
phc-toolkit/aliases))
|
||||
|
||||
(define-type-expander BinaryTree
|
||||
(syntax-parser
|
||||
[(_ leafⱼ …)
|
||||
;; TODO: implement BinaryTree.
|
||||
#'(List leafⱼ …)]))
|
||||
1
commit_hash
Normal file
1
commit_hash
Normal file
|
|
@ -0,0 +1 @@
|
|||
eb2aed91c1b1bc28d2fd7f15c8abd9d4d4d06217
|
||||
58
def.rkt
58
def.rkt
|
|
@ -1,58 +0,0 @@
|
|||
#lang typed/racket
|
||||
(require syntax/parse
|
||||
phc-toolkit/percent
|
||||
(for-syntax syntax/parse))
|
||||
|
||||
(begin-for-syntax
|
||||
(define-syntax-class parse-args
|
||||
(pattern rest:id
|
||||
#:with sig #'rest
|
||||
#:with {extract ...} #'{})
|
||||
(pattern ({~or {~literal syntax} {~literal unsyntax}} . rest)
|
||||
;; The rest would need to be an stx, but that's normally impossible
|
||||
;; (unless there was some extension to #%app and function
|
||||
;; definitions which allowed this).
|
||||
#:with sig (raise-syntax-error
|
||||
"Unexpected syntax pattern in a tail position")
|
||||
#:with {extract ...} #'{})
|
||||
(pattern (({~literal syntax} hd) . tl:parse-args)
|
||||
#:with (tmp) (generate-temporaries #'(hd))
|
||||
#:with sig #'(tmp . tl.sig)
|
||||
#:with {extract ...} #`{#'hd = tmp tl.extract ...})
|
||||
(pattern (({~literal unsyntax} hd:parse-args) . tl:parse-args)
|
||||
#:with (tmp) (generate-temporaries #'(hd))
|
||||
#:with sig #'(tmp . tl.sig)
|
||||
#:with {extract ...} #'{hd.sig = (syntax->datum tmp)
|
||||
hd.extract ...
|
||||
tl.extract ...})
|
||||
(pattern (hd:id . tl:parse-args)
|
||||
#:with sig #'(hd . tl.sig)
|
||||
#:with {extract ...} #'{tl.extract ...})
|
||||
(pattern {~and last ()}
|
||||
#:with sig #'last
|
||||
#:with {extract ...} #'{})))
|
||||
|
||||
(define-syntax def
|
||||
(syntax-parser
|
||||
[(_ ({~literal syntax} name:id) . body)
|
||||
#'(define-syntax name
|
||||
(syntax-parser
|
||||
[self:id . body]))]
|
||||
[(_ (name:id . args:parse-args) . body)
|
||||
#`(define (name . args.sig)
|
||||
(% args.extract ...
|
||||
. body))]))
|
||||
|
||||
#;{
|
||||
(def (foo #'(aa . bb) x)
|
||||
#`(#,x bb . aa))
|
||||
|
||||
(def (bar #,(aa . bb) x)
|
||||
(list x bb aa))
|
||||
|
||||
(module+ test
|
||||
(require rackunit)
|
||||
(check-equal? (syntax->datum
|
||||
(foo #'(xx . yy) 42))
|
||||
'(42 yy . xx)))
|
||||
}
|
||||
|
|
@ -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,9 +0,0 @@
|
|||
#lang typed/racket
|
||||
|
||||
(provide dot λdot)
|
||||
|
||||
(define-syntax (dot stx)
|
||||
(raise-syntax-error 'dot "Dot is not implemented yet" stx))
|
||||
|
||||
(define-syntax (λdot stx)
|
||||
(raise-syntax-error 'dot "Dot is not implemented yet" stx))
|
||||
|
|
@ -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,28 +0,0 @@
|
|||
#lang type-expander
|
||||
(require "flexible-with-generalized-ctor.hl.rkt"
|
||||
"binarytree.hl.rkt")
|
||||
(provide f-4-2 f-8-3)
|
||||
|
||||
(builder-f f-4-2 4 2)
|
||||
|
||||
(ann ((inst f-4-2 propagate-τ '|1| Number '|3| String)
|
||||
oracle '|1| 100 '|3| "bee")
|
||||
(BinaryTree
|
||||
(Promise (Pairof #f Any))
|
||||
(Promise (Pairof '|1| Number))
|
||||
(Promise (Pairof #f Any))
|
||||
(Promise (Pairof '|3| String))))
|
||||
|
||||
(builder-f f-8-3 8 3)
|
||||
|
||||
(ann ((inst f-8-3 propagate-τ '|1| Number '|3| String '|7| Symbol)
|
||||
oracle '|1| 100 '|3| "bee" '|7| 'buzz)
|
||||
(BinaryTree
|
||||
(Promise (Pairof #f Any))
|
||||
(Promise (Pairof '|1| Number))
|
||||
(Promise (Pairof #f Any))
|
||||
(Promise (Pairof '|3| String))
|
||||
(Promise (Pairof #f Any))
|
||||
(Promise (Pairof #f Any))
|
||||
(Promise (Pairof #f Any))
|
||||
(Promise (Pairof '|7| Symbol))))
|
||||
|
|
@ -1,246 +0,0 @@
|
|||
#lang hyper-literate #:꩜ #:no-auto-require (dotlambda/unhygienic
|
||||
. type-expander/lang)
|
||||
|
||||
꩜title[#:tag "generalized-flex-ctor"]{Generalised constructor functions for
|
||||
flexible structures}
|
||||
|
||||
꩜(require hyper-literate/diff1)
|
||||
|
||||
꩜chunk[<*>
|
||||
(provide builder-τ
|
||||
propagate-τ
|
||||
oracle
|
||||
builder-f)
|
||||
|
||||
(require racket/require
|
||||
(for-syntax (subtract-in racket/base subtemplate/override)
|
||||
syntax/stx
|
||||
racket/list
|
||||
racket/function
|
||||
subtemplate/override)
|
||||
(for-meta 2 racket/base)
|
||||
"binarytree.hl.rkt")
|
||||
|
||||
<propagate-τ>
|
||||
<oracle-τ>
|
||||
<oracle>
|
||||
<builder-τ>
|
||||
<builder-f>]
|
||||
|
||||
We first define the builder function's type. Since this type is rather
|
||||
complex, we define it using a macro. The type expander takes two arguments.
|
||||
The first argument ꩜racket[n] indicates the total number of fields which
|
||||
appear in the program (i.e. on the number of leaves of the generated tree
|
||||
type), and the second argument ꩜racket[m] indicates how many key/value pairs
|
||||
the function accepts.
|
||||
|
||||
꩜chunk[<builder-τ>
|
||||
(define-type-expander builder-τ
|
||||
(syntax-parser
|
||||
[(_ n m)
|
||||
<builder-τ-with-1>
|
||||
<builder-τ-with-2>
|
||||
<builder-τ-with-3>
|
||||
#'|<builder-function-type″>|]))]
|
||||
|
||||
We start by defining a few syntax pattern variables which will be used in the
|
||||
later definitions. The lists ꩜racket[Nᵢ] and ꩜racket[Mⱼ] range over the field
|
||||
and argument indices, respectively:
|
||||
|
||||
꩜chunk[<builder-τ-with-1>
|
||||
#:with (Nᵢ …) (range n)
|
||||
#:with (Mⱼ …) (range m)]
|
||||
|
||||
The builder function takes a number of keys and values, and builds a (promise
|
||||
for) a binary tree where the leaves corresponding to those keys contain given
|
||||
value, and other leaves contain ꩜racket[None]. We could write (a simplified
|
||||
form of) the builder function type as follows:
|
||||
|
||||
꩜chunk[<builder-function-type>
|
||||
(∀ ({?@ Kⱼ Xⱼ} …)
|
||||
(→ (code:comment "; Keys and values:")
|
||||
{?@ (∩ Kⱼ (U 'NSymⱼᵢ …)) Xⱼ} …
|
||||
;; Result type:
|
||||
(BinaryTree (Promise |<Some or None>|) …)))]
|
||||
|
||||
We expect each key ꩜racket[Kⱼ] to be a symbol of the shape ꩜racket[|0|],
|
||||
꩜racket[|1|], ꩜racket[|2|] and so on:
|
||||
|
||||
꩜chunk[<builder-τ-with-2>
|
||||
#:with (NSymᵢ …) ((string->symbol (format "~a" Nᵢ)) …)
|
||||
#:with ((NSymⱼᵢ …) …) (map (const (NSymᵢ …)) (Mⱼ …))]
|
||||
|
||||
The type of each leaf of the binary tree should be ꩜racket[(Some Xⱼ)] if a
|
||||
corresponding ꩜racket[Kⱼ] matches the leaf name, and ꩜racket[None] otherwise.
|
||||
|
||||
꩜chunk[|<Some or None>|
|
||||
(U |<(Some Xⱼ) if Kⱼ = NSymᵢ>|
|
||||
|<None if ∀ k ∈ Kⱼ , k ≠ NSymᵢ>|)]
|
||||
|
||||
This type-level conditional is achieved via a trick involving intersection
|
||||
types. The ꩜racket[Kⱼ] type should be a singleton type containing exactly one
|
||||
of the ꩜racket['NSymᵢ …] symbols. For a given leaf with index ꩜racket[i], if
|
||||
the ꩜racket[Kⱼ] key is the type ꩜racket['NSymᵢ], then the intersection type
|
||||
꩜racket[(∩ Kⱼ 'NSymᵢ)] is ꩜racket['NSymᵢ]. Conversely, if the ꩜racket[Kⱼ] key
|
||||
is not ꩜racket['NSymᵢ], the intersection will be the bottom type
|
||||
꩜racket[Nothing]. No values inhabit the bottom type, and Typed Racket can
|
||||
determine that there is no pair whose first (or second) element has the type
|
||||
꩜racket[Nothing], since no concrete value could be used to construct such a
|
||||
pair.
|
||||
|
||||
꩜chunk[|<(Some Xⱼ) if Kⱼ = NSymᵢ>|
|
||||
(Pairof (∩ Kᵢⱼ 'NSymᵢⱼ)
|
||||
Xᵢⱼ)
|
||||
…]
|
||||
|
||||
where ꩜racket[Kᵢⱼ], ꩜racket[Xᵢⱼ] and ꩜racket[NSymᵢⱼ] are defined as follows:
|
||||
|
||||
꩜chunk[<builder-τ-with-3>
|
||||
#:with ((Kᵢⱼ …) …) (map (const #'(Kⱼ …)) (Nᵢ …))
|
||||
#:with ((Xᵢⱼ …) …) (map (const #'(Xⱼ …)) (Nᵢ …))
|
||||
#:with ((NSymᵢⱼ …) …) (map λni.(map (const ni) (Xⱼ …)) (NSymᵢ …))]
|
||||
|
||||
We use this fact to construct a pair above. Its first element is either
|
||||
꩜racket['NSymᵢ] when ꩜racket[Kⱼ] is ꩜racket['NSymᵢ], and ꩜racket[Nothing]
|
||||
otherwise. The second element of the pair contains our expected
|
||||
꩜racket[(Some Xⱼ)] type, but the whole pair is collapsed to ꩜racket[Nothing]
|
||||
when ꩜racket[Kⱼ] is not ꩜racket['NSymᵢ].
|
||||
|
||||
We use a similar approach to conditionally produce the ꩜racket[None] element
|
||||
(which we represent as ꩜racket[#f]), but instead of intersecting ꩜racket[Kⱼ]
|
||||
with ꩜racket['NSymᵢ], we intersect it with the complement of ꩜racket['NSymᵢ].
|
||||
Typed Racket lacks the possibility to negate a type, so we manually compute
|
||||
the complement of ꩜racket['NSymᵢ] in the set of possible keys (that is,
|
||||
꩜racket['NSymᵢ …]).
|
||||
|
||||
꩜chunk[<builder-τ-with-3>
|
||||
#:with NSyms (NSymᵢ …)
|
||||
#:with Ms (Mⱼ …)
|
||||
#:with (exceptᵢ …) ((remove NSymᵢ NSyms) …)
|
||||
#:with (((exceptᵢⱼ …) …) …) ((map (const exceptᵢ) Ms) …)]
|
||||
|
||||
If ꩜racket[Kⱼ] is ꩜racket[Nᵢ], then ꩜racket[{∩ Kⱼ {U . exceptᵢ}}] will be
|
||||
꩜racket[Nothing]. We take the Cartesian product of the intersections by
|
||||
building a ꩜racket[List] out of them. A single occurrence of ꩜racket[Nothing]
|
||||
will collapse the whole list to ꩜racket[Nothing], because the Cartesian
|
||||
product of the empty set and any other set will produce the empty set.
|
||||
|
||||
The resulting type should therefore be ꩜racket[Nothing] only if there is no
|
||||
꩜racket[Kⱼ] equal to ꩜racket[Nᵢ], and be the list of symbols
|
||||
꩜racket[(List . exceptᵢ)] otherwise.
|
||||
|
||||
꩜chunk[|<None if ∀ k ∈ Kⱼ , k ≠ NSymᵢ>|
|
||||
(Pairof #f (List {∩ Kᵢⱼ {U 'exceptᵢⱼ …}} …))]
|
||||
|
||||
This approach relies on the fact that occurrences of ꩜racket[Nothing] within
|
||||
structs and pairs containing collapse the entire struct or pair type to
|
||||
꩜racket[Nothing]. Unfortunately, current versions of Typed Racket perform this
|
||||
simplification step in some situations but not others:
|
||||
|
||||
꩜itemlist[
|
||||
꩜item{It simplifies polymorphic types when they are defined;}
|
||||
꩜item{When a polymorphic type is instantiated, the parts which are directly
|
||||
affected by the intersection with a polymorphic type variable are subject to
|
||||
this simplification;}
|
||||
꩜item{However, occurrences of ꩜racket[Nothing] which occur as a result of
|
||||
instantiating the type variable do not propagate outside of the intersection
|
||||
itself. This means that given the following type:
|
||||
꩜racketblock[(define-type (Foo A) (U (Pairof (∩ Integer A) String) Boolean))]
|
||||
its instantiation ꩜racket[(Foo Symbol)] will produce the type
|
||||
꩜racket[(U (Pairof Nothing String) Boolean)], but this type will not be
|
||||
simplified to ꩜racket[(U Nothing Boolean)] or equivalently to
|
||||
꩜racket[Boolean].}]
|
||||
|
||||
To force Typed Racket to propagate ꩜racket[Nothing] outwards as much as
|
||||
we need, we intersect the whole form with a polymorphic type ꩜racket[A]:
|
||||
|
||||
꩜hlite[|<builder-function-type′>|
|
||||
{/(∀(+ _ / _ _)(→ _ _ ooo (bt (p + (∩ / _ + A)) / ooo)))}
|
||||
(∀ (A {?@ Kⱼ Xⱼ} …)
|
||||
(→ (code:comment "; Keys and values:")
|
||||
{?@ (∩ Kⱼ (U 'NSymⱼᵢ …)) Xⱼ} …
|
||||
;; Result type:
|
||||
(BinaryTree (Promise (∩ |<Some or None>| A)) …)))]
|
||||
|
||||
The type ꩜racket[propagate-τ] defined below is used to instantiate ꩜racket[A],
|
||||
and is carefully picked so that its intersection will in no way change the
|
||||
result type (i.e. the intersection with ꩜racket[A] will be an identity
|
||||
operation where it is used). In other words, ꩜racket[propagate-τ] has the same
|
||||
shape as the leaves of the binary tree. This intersection however forces the
|
||||
simplification step to be performed on the affected parts once the type is
|
||||
instantiated.
|
||||
|
||||
꩜chunk[<propagate-τ>
|
||||
(define-type propagate-τ
|
||||
(U (Pairof Symbol Any)
|
||||
(Pairof #f (Listof Symbol))))]
|
||||
|
||||
꩜;Use chunkref instead of ꩜racket[|<Some or None>|] ?
|
||||
|
||||
The implementation of the builder function will need to convert values with
|
||||
the ꩜racket[|<Some or None>|] type to values of type
|
||||
꩜racket[(∩ |<Some or None>| A)]. Since the intersection could, in principle,
|
||||
be any subtype of ꩜racket[|<Some or None>|], we request that the caller
|
||||
supplies a proof that the conversion is possible. This proof takes the form of
|
||||
an ꩜racket[oracle] function, which transforms an element with the type
|
||||
꩜racket[propagate-τ] (which is a supertype of every possible
|
||||
꩜racket[|<Some or None>|] type) into an element with the type
|
||||
꩜racket[(∩ A B)], where ꩜racket[B] is the original type of the value to
|
||||
upgrade.
|
||||
|
||||
꩜chunk[<oracle-τ>
|
||||
(define-type (oracle-τ A)
|
||||
(∀ (B) (→ (∩ B
|
||||
(U (Pairof Symbol Any)
|
||||
(Pairof #f (Listof Symbol))))
|
||||
(∩ A B))))]
|
||||
|
||||
The oracle does nothing more than return its argument unchanged:
|
||||
|
||||
꩜chunk[<oracle>
|
||||
(: oracle (oracle-τ propagate-τ))
|
||||
(define (oracle v) v)]
|
||||
|
||||
We update the builder function type to accept an extra argument for the
|
||||
oracle:
|
||||
|
||||
꩜hlite[|<builder-function-type″>|
|
||||
{/(∀(_ _ _)(→ + _ _ / _ _ ooo _))}
|
||||
(∀ (A {?@ Kⱼ Xⱼ} …)
|
||||
(→ (code:comment "; Oracle:")
|
||||
(oracle-τ A)
|
||||
(code:comment "; Keys and values:")
|
||||
{?@ (∩ Kⱼ (U 'NSymⱼᵢ …)) Xⱼ} …
|
||||
;; Result type:
|
||||
(BinaryTree (Promise (∩ |<Some or None>| A)) …)))]
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
꩜chunk[<builder-f>
|
||||
(define-syntax builder-f
|
||||
(syntax-parser
|
||||
[(_ name n m)
|
||||
<builder-τ-with-1>
|
||||
<builder-τ-with-2>
|
||||
<builder-τ-with-3>
|
||||
<builder-τ-with-4>
|
||||
#'(begin |<builder-function-implementation>|)]))]
|
||||
|
||||
꩜chunk[<builder-τ-with-4>
|
||||
#:with ((kᵢⱼ …) …) (map (const #'(kⱼ …)) (Nᵢ …))
|
||||
#:with ((xᵢⱼ …) …) (map (const #'(xⱼ …)) (Nᵢ …))]
|
||||
|
||||
꩜chunk[<builder-function-implementation>
|
||||
(: name |<builder-function-type″>| #;(builder-τ n m))
|
||||
(define (name oracle {?@ kⱼ xⱼ} …)
|
||||
(list (delay
|
||||
(cond
|
||||
[((make-predicate 'NSymᵢⱼ) kᵢⱼ)
|
||||
((inst oracle (Pairof (∩ Kᵢⱼ 'NSymᵢⱼ) Xᵢⱼ)) (cons kᵢⱼ xᵢⱼ))]
|
||||
…
|
||||
[else
|
||||
((inst oracle (Pairof #f (List (∩ Kᵢⱼ (U 'exceptᵢⱼ …)) …)))
|
||||
(cons #f (list kᵢⱼ …)))]))
|
||||
…))]
|
||||
|
|
@ -1,117 +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,369 +0,0 @@
|
|||
#lang hyper-literate #:♦ (dotlambda/unhygienic . 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>
|
||||
(define-pure/stateless
|
||||
(: replace-right (∀ (A B C R) (→ (→ (Promise B) R (Promise C))
|
||||
(Promise (Pairof A B))
|
||||
R
|
||||
(Promise (Pairof A C)))))
|
||||
(define
|
||||
#:∀ (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))))))))
|
||||
(define-pure/stateless
|
||||
(: replace-left (∀ (A B C R) (→ (→ (Promise A) R (Promise C))
|
||||
(Promise (Pairof A B))
|
||||
R
|
||||
(Promise (Pairof C B)))))
|
||||
(define
|
||||
#:∀ (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)))
|
||||
|
||||
(define-pure/stateless
|
||||
(: low-name
|
||||
(∀ (#,@τ*-limited T)
|
||||
(→ (tree-type-with-replacement-name #,@τ*-limited Any)
|
||||
T
|
||||
(tree-type-with-replacement-name #,@τ*-limited T))))
|
||||
(define
|
||||
#:∀ (#,@τ*-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)]
|
||||
File diff suppressed because it is too large
Load Diff
|
|
@ -1,99 +0,0 @@
|
|||
#lang racket
|
||||
|
||||
(require racket/struct
|
||||
;; TODO: move delay-pure/private/immutable-struct to a separate package
|
||||
phc-toolkit/untyped/meta-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 struct-instance-is-immutable?
|
||||
(λ (v)
|
||||
(andmap isyntax/c (struct->list v)))))))
|
||||
|
||||
(define/contract (free-id-tree=? a b [r equal?])
|
||||
(->* {isyntax/c isyntax/c}
|
||||
{(-> isyntax/c isyntax/c boolean?)}
|
||||
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)))))]
|
||||
[(struct? a)
|
||||
(and (struct? b)
|
||||
(rec=? (vector->immutable-vector (struct->vector a))
|
||||
(vector->immutable-vector (struct->vector b))))]
|
||||
[(null? a) (null? b)]
|
||||
[else (equal? a b)]))
|
||||
|
||||
(define/contract ((free-id-tree-hash default-hc) a [hc default-hc])
|
||||
(-> (-> any/c fixnum?) (->* {isyntax/c} {(-> isyntax/c fixnum?)} 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 (vector->immutable-vector
|
||||
(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)))))]
|
||||
[(struct? a)
|
||||
(rec-hash (vector->immutable-vector (struct->vector 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,339 +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
|
||||
|<gen:equal+hash free-id-tree=?>|)]
|
||||
|
||||
Instances of @racket[invariant-info] are compared pointwise with
|
||||
@racket[free-id-tree=?]:
|
||||
|
||||
@chunk[|<gen:equal+hash free-id-tree=?>|
|
||||
[(define equal-proc free-id-tree=?)
|
||||
(define hash-proc free-id-tree-hash-code)
|
||||
(define hash2-proc free-id-tree-secondary-hash-code)]]
|
||||
|
||||
@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
|
||||
|<gen:equal+hash free-id-tree=?>|)]
|
||||
|
||||
Instances of @racket[dependent-invariant-info] are compared pointwise with
|
||||
@racket[free-id-tree=?], like @racket[invariant-info].
|
||||
|
||||
@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)
|
||||
(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]
|
||||
...)))))))
|
||||
|
||||
<printer>
|
||||
|
||||
<field-info>
|
||||
<node-info>
|
||||
<invariant-info>
|
||||
<dependent-invariant-info>
|
||||
<graph-info>
|
||||
<mapping-info>
|
||||
<graph-builder-info>]
|
||||
|
|
@ -1,141 +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
|
||||
racket/set
|
||||
subtemplate/override
|
||||
extensible-parser-specifications)
|
||||
(for-meta 2 racket/base))
|
||||
|
||||
(provide define-graph-type)
|
||||
|
||||
<signature>
|
||||
<build-graph-info>
|
||||
<define-graph-type>]
|
||||
118
graph.hl.rkt
118
graph.hl.rkt
|
|
@ -1,118 +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 racket/base
|
||||
subtemplate/override)
|
||||
phc-toolkit/untyped
|
||||
type-expander/expander
|
||||
subtemplate/override)
|
||||
"traversal.hl.rkt"
|
||||
phc-toolkit)
|
||||
<define-index>
|
||||
<graph>]
|
||||
36
info.rkt
36
info.rkt
|
|
@ -1,36 +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"
|
||||
"typed-map"
|
||||
"scribble-lib"
|
||||
"pconvert-lib"
|
||||
"remember"
|
||||
"extensible-parser-specifications"
|
||||
"subtemplate"
|
||||
"stxparse-info"
|
||||
"dotlambda"
|
||||
"typed-worklist"))
|
||||
(define build-deps '("scribble-lib"
|
||||
"racket-doc"
|
||||
"remember"
|
||||
"typed-racket-doc"
|
||||
"aful"
|
||||
"scribble-math"
|
||||
"at-exp-lib"))
|
||||
(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,706 +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 Abstract
|
||||
Syntax Tree or 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 the
|
||||
node representing 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 will match all witness
|
||||
types, 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 inv∈ ())
|
||||
(struct inv≡ ())
|
||||
(struct inv∉ ())
|
||||
|
||||
;(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 @racket[Or] element in the union, to
|
||||
avoid ever having an empty union.
|
||||
|
||||
@chunk[<Or>
|
||||
(struct Or ())]
|
||||
|
||||
@chunk[<grouping-invariants>
|
||||
(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{Invariants and their relationships}
|
||||
|
||||
We design our typing hierarchy to allow encoding the equality, inequality,
|
||||
membership and non-membership between paths. A simple example would be
|
||||
the property @racket[:A.b.c ≡ :A.d.e], which would hold for all nodes of type
|
||||
@racket[A].
|
||||
|
||||
These paths patterns form a suffix of actual paths. Let @${S₁} and @${S₂} be
|
||||
two sets of pairs of suffixes. If the set of pairs of actual paths covered by
|
||||
@${S₁} is a superset the set of pairs of actual paths covered by @${S₂}, then
|
||||
@${S₁} can be used to express a property over more pairs of actual paths,
|
||||
and the resulting property on the graph as a whole is therefore more precise.
|
||||
|
||||
Our implementation allows the concise expression of a set of paths using a
|
||||
template within which sections of the path may be repeated any number of
|
||||
times. For example, the template @racket[:A.b(.c)*.d] corresponds to the set of
|
||||
paths containing @racket[:A.b.d], @racket[:A.b.c.d], @racket[:A.b.c.c.d] and so
|
||||
on.
|
||||
|
||||
When path elements may produce a value whose type is a variant (i.e. a union
|
||||
of several constructors), it can be necessary to distinguish which
|
||||
constructor(s) the path applies to. We use a syntax inspired from that of
|
||||
@racketmodname[syntax/parse] for that purpose. Any point in a path can be
|
||||
followed by @racket[:node-name], which effectively refines the set of actual
|
||||
paths so that it contains only paths where the value at that point is of the
|
||||
given type. The syntax @racket[:A.b.c] therefore indicates that the path must
|
||||
start on an element of type @racket[A], and follow its fields @racket[b] then
|
||||
@racket[c]. The syntax @racket[.x:T.y.z] indicates paths @racket[.x.y.z], where
|
||||
the element accessed by @racket[.x] has the type @racket[T].
|
||||
|
||||
The @racket[?] path element indicates that any field can be used at the given
|
||||
point. The syntax @racket[.x.?.y] therefore indicates the paths
|
||||
@racket[.x.f.y], @racket[.x.g.y], @racket[.x.h.y] and so on, where @racket[f],
|
||||
@racket[g] and @racket[h] are the fields of the value obtained after
|
||||
@racket[.x]. The @racket[?] path element can be used to describe all fields,
|
||||
including those hidden away by row polymorphism.
|
||||
|
||||
It would be possible to represent sets of path concisely by reversing all
|
||||
these paths so that they start with their target element, and building a
|
||||
prefix tree. Unfortunately, Typed Racket does not currently does not
|
||||
automatically detect the equivalence between the types
|
||||
@racket[(U (Pairof A B) (Pairof A C))] and @racket[(Pairof A (U B C))]. @;{
|
||||
TODO: insert reference to the relevant bug.} In other words, at the type
|
||||
level, unions do not implicitly distribute onto pairs. When a set of
|
||||
properties @racket[S] is extended with a new property @racket[p], the
|
||||
resulting set of properties will be encoded as @racket[(U S p)]. If @racket[S]
|
||||
is encoded as a prefix tree, @racket[p] will not implicitly be merged into the
|
||||
prefix tree. This means that if prefix trees were to be used, extending a set
|
||||
of properties with a new property would give one representation, and directly
|
||||
encoding that set would give another representation, and the two
|
||||
representations would be incomparable.
|
||||
|
||||
We therefore represent sets of paths using a more costly representation, by
|
||||
making a union of all paths, without factoring out common parts.
|
||||
|
||||
@subsection{Parsing paths}
|
||||
|
||||
@; TODO: make sure the literal "dot" is provided.
|
||||
|
||||
@; .a.b(.c.d)*.e
|
||||
@; ⇒ (λdot a b) ((λdot c d)) * (λdot e)
|
||||
|
||||
@chunk[<parse>
|
||||
(begin-for-syntax
|
||||
(define (match-id rx id)
|
||||
(let ([m (regexp-match rx (identifier→string id))])
|
||||
(and m (map (λ (%) (datum->syntax id (string->symbol %) id id))
|
||||
(cdr m)))))
|
||||
(define-syntax ~rx-id
|
||||
(pattern-expander
|
||||
(λ (stx)
|
||||
(syntax-case stx ()
|
||||
[(_ rx g …)
|
||||
#'(~and x:id
|
||||
{~parse (g …) (match-id rx #'x)})]))))
|
||||
|
||||
(define-syntax-class f+τ
|
||||
#:attributes (f τ)
|
||||
(pattern {~rx-id #px"^([^:]+):([^:]+)$" f τ})
|
||||
(pattern {~rx-id #px"^([^:]+)$" f} #:with ({~optional τ}) #'())
|
||||
(pattern {~rx-id #px"^:([^:]+)$" τ} #:with ({~optional f}) #'())
|
||||
(pattern {~rx-id #px"^:$"} #:with ({~optional (f τ)}) #'()))
|
||||
(define-syntax-class just-τ
|
||||
#:attributes (τ)
|
||||
(pattern {~rx-id #px"^:([^:]+)$" τ}))
|
||||
(define-syntax-class π-elements
|
||||
#:literals (#%dotted-id #%dot-separator)
|
||||
#:attributes ([f 1] [τ 1])
|
||||
(pattern (#%dotted-id {~seq #%dot-separator :f+τ} …)))
|
||||
(define-syntax-class extract-star
|
||||
#:literals (* #%dotted-id)
|
||||
(pattern (#%dotted-id {~and st *} . rest)
|
||||
#:with {extracted-star …} #'{st (#%dotted-id . rest)})
|
||||
(pattern other
|
||||
#:with {extracted-star …} #'{other}))
|
||||
(define-syntax-class sub-elements
|
||||
#:literals (* #%dot-separator)
|
||||
#:attributes ([f 2] [τ 2] [sub 1])
|
||||
(pattern
|
||||
(:extract-star …)
|
||||
#:with ({~either :π-elements {~seq sub:sub-elements *}} …)
|
||||
#| |# #'(extracted-star … …))))]
|
||||
|
||||
@chunk[<parse>
|
||||
(define-type-expander <~τ
|
||||
(syntax-parser
|
||||
[(_ τ) #'τ]
|
||||
[(_ f₀ . more)
|
||||
#`(f₀ (<~τ . more))]))
|
||||
(begin-for-syntax
|
||||
(define-template-metafunction generate-sub-π
|
||||
(syntax-parser
|
||||
[(_ :sub-elements after)
|
||||
#:with R (gensym 'R)
|
||||
(template
|
||||
(Rec R
|
||||
(U (<~τ (?? (∀ (more) (generate-sub-π sub more))
|
||||
(∀ (more) (List* (Pairof (?? 'f AnyField)
|
||||
(?? τ AnyType))
|
||||
…
|
||||
more)))
|
||||
…
|
||||
R)
|
||||
after)))])))
|
||||
(define-type-expander Π
|
||||
(syntax-parser
|
||||
#:literals (#%dotted-id #%dot-separator)
|
||||
[(_ {~optional (~or (#%dotted-id fst-τ:just-τ
|
||||
{~seq #%dot-separator fst:f+τ} …)
|
||||
{~datum :}
|
||||
(~and fst-τ:just-τ
|
||||
{~parse (fst:f+τ …) #'()}))}
|
||||
. :sub-elements)
|
||||
#:with R (gensym 'R)
|
||||
(template/top-loc
|
||||
this-syntax
|
||||
(Rec R (U (Pairof Any R)
|
||||
(List* (?? (?@ (Pairof AnyField fst-τ.τ)
|
||||
(Pairof (?? 'fst.f AnyField)
|
||||
(?? fst.τ AnyType))
|
||||
…))
|
||||
<π>))))]))]
|
||||
|
||||
@chunk[<π>
|
||||
(<~τ (?? (∀ (more) (generate-sub-π sub more))
|
||||
(∀ (more) (List* (Pairof (?? 'f AnyField) (?? τ AnyType))
|
||||
…
|
||||
more)))
|
||||
…
|
||||
Null)]
|
||||
|
||||
@chunk[<Invariant>
|
||||
(define-type-expander Invariant
|
||||
(syntax-parser
|
||||
#:literals (≡ ≢ ∈ ∉ ∋ ∌ = ≤ ≥ length +)
|
||||
[(_ π₁ … ≡ π₂ …) #`(U (inv≡ (Π π₁ …) (Π π₂ …))
|
||||
(inv≡ (Π π₂ …) (Π π₁ …)))]
|
||||
[(_ π₁ … ≢ π₂ …) #`(U (inv≢ (Π π₁ …) (Π π₂ …))
|
||||
(inv≢ (Π π₂ …) (Π π₁ …)))]
|
||||
[(_ π₁ … ∈ π₂ …) #`(inv∈ (Π π₁ …) (Π π₂ …))]
|
||||
[(_ π₁ … ∋ π₂ …) #`(inv∈ (Π π₂ …) (Π π₁ …))]
|
||||
[(_ π₁ … ∉ π₂ …)
|
||||
#`(U (inv≢ (Π π₁ …) (Π π₂ … (#%dotted-id #%dot-separator :)))
|
||||
(inv≢ (Π π₂ … (#%dotted-id #%dot-separator :)) (Π π₁ …)))]
|
||||
[(_ π₁ … ∌ π₂ …)
|
||||
#`(U (inv≢ (Π π₂ …) (Π π₁ … (#%dotted-id #%dot-separator :)))
|
||||
(inv≢ (Π π₁ … (#%dotted-id #%dot-separator :)) (Π π₂ …)))]
|
||||
;; TODO: = should use a combination of ≤ and ≥
|
||||
[(_ π₁ …
|
||||
{~and op {~or = ≤ ≥}}
|
||||
(~or (+ (length π₂ …) n:nat)
|
||||
{~and (length π₂ …) {~parse n 0}}))
|
||||
#:with opN (syntax-case #'op (= ≤ ≥)
|
||||
[= #'=N]
|
||||
[≤ #'≤N]
|
||||
[≥ #'≥N])
|
||||
#`(→ (invLength (opN n) (Π π₁ …) (Π π₂ …)) Void)]))]
|
||||
|
||||
@CHUNK[<=>
|
||||
(define-type (P A B) (Promise (Pairof A B)))
|
||||
(define-type a 'a)
|
||||
(define-type x 'x)
|
||||
(define-type ax (U a x))
|
||||
(define-type x* (Rec R (P x R)))
|
||||
(define-type ax* (Rec R (P ax R)))
|
||||
(define-type-expander =N
|
||||
(syntax-parser
|
||||
[(_ 0) #'x*]
|
||||
[(_ n:nat) #`(P a (=N #,(sub1 (syntax-e #'n))))]))
|
||||
(define-type-expander ≥N
|
||||
(syntax-parser
|
||||
[(_ 0) #'ax*]
|
||||
[(_ n:nat) #`(P a (≥N #,(sub1 (syntax-e #'n))))]))
|
||||
(define-type-expander ≤N
|
||||
(syntax-parser
|
||||
[(_ 0) #'x*]
|
||||
[(_ n:nat) #`(P ax (≤N #,(sub1 (syntax-e #'n))))]))]
|
||||
|
||||
@chunk[<Invariants>
|
||||
(define-type-expander Invariants
|
||||
(syntax-parser
|
||||
[(_ inv …)
|
||||
#`(→ (U Or (Invariant . inv) …) Void)]))]
|
||||
|
||||
@chunk[<Any*>
|
||||
(define-type AnyField Symbol);(struct AnyField () #:transparent)
|
||||
(struct AnyType () #:transparent)
|
||||
(define-type ε (Π))]
|
||||
|
||||
@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 B) inv≡ ([a : A] [b : B]))
|
||||
(struct (A B) inv≢ ([a : A] [b : B]))
|
||||
(struct (A B) inv∈ ([a : A] [b : B]))
|
||||
(struct (A B C) invLength ([a : A] [b : B] [c : C]))
|
||||
;(struct inv∉ ()) ;; Can be expressed in terms of ≢
|
||||
|
||||
(module literals typed/racket
|
||||
(define-syntax-rule (define-literals name ...)
|
||||
(begin
|
||||
(provide name ...)
|
||||
(define-syntax name
|
||||
(λ (stx)
|
||||
(raise-syntax-error 'name
|
||||
"Can only be used in special contexts"
|
||||
stx)))
|
||||
...))
|
||||
|
||||
(define-literals ≡ ≢ ∈ ∉ ∋ ∌ ≥ ≤))
|
||||
(require 'literals)]
|
||||
|
||||
@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 ≡x (relation #'inv≡))
|
||||
(define-type-expander ≢x (relation #'inv≢))]
|
||||
|
||||
@chunk[<cycles>
|
||||
(struct ε () #:transparent)
|
||||
(struct (T) Target ([x : T]) #:transparent)
|
||||
(struct (T) NonTarget Target () #: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)
|
||||
(U (List* (NonTarget 'loop2) … ;(NonTarget 'loop2) …
|
||||
R)
|
||||
Null)))) Void)]
|
||||
[(_ field … target)
|
||||
#'(→ (List (NonTarget ε)
|
||||
(NonTarget 'field)
|
||||
…
|
||||
(Target 'target)) Void)]
|
||||
[(_)
|
||||
#'(→ (List (Target ε)) Void)]))]
|
||||
|
||||
@;{@[
|
||||
|
||||
;.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[<*>
|
||||
(require (only-in typed/dotlambda #%dotted-id #%dot-separator)
|
||||
"dot-lang.rkt"
|
||||
(for-syntax racket/base
|
||||
racket/list
|
||||
phc-toolkit/untyped
|
||||
syntax/parse
|
||||
syntax/parse/experimental/template)
|
||||
(for-meta 2 racket/base)
|
||||
(for-meta 2 phc-toolkit/untyped/aliases)
|
||||
(for-meta 3 racket/base))
|
||||
|
||||
(begin-for-syntax
|
||||
(define-syntax-rule (quasisyntax e)
|
||||
(quasisyntax/top-loc this-syntax e))
|
||||
(define-syntax-rule (template/top-loc loc e)
|
||||
(quasisyntax/top-loc loc #,(template e))))
|
||||
|
||||
(provide ≡ ≢ ∈ ∉ ∋ ∌ ≥ ≤)
|
||||
|
||||
;; For testing:
|
||||
(provide Invariants
|
||||
inv≡
|
||||
inv≢
|
||||
Or
|
||||
;Target
|
||||
;NonTarget
|
||||
ε
|
||||
witness-value
|
||||
Π
|
||||
AnyType
|
||||
AnyField
|
||||
Invariant)
|
||||
|
||||
<parse>
|
||||
|
||||
<witness-value>
|
||||
<Any*>
|
||||
<comparison-operators>
|
||||
<Invariant>
|
||||
<Invariants>
|
||||
<Or>
|
||||
<=>]
|
||||
12
literals.rkt
12
literals.rkt
|
|
@ -1,12 +0,0 @@
|
|||
#lang racket
|
||||
|
||||
(define-syntax-rule (provide-literals name ...)
|
||||
(begin
|
||||
(provide name ...)
|
||||
(define-syntax (name stx)
|
||||
(raise-syntax-error 'name
|
||||
"can only be used in some special contexts"
|
||||
stx))
|
||||
...))
|
||||
|
||||
(provide-literals mapping node)
|
||||
|
|
@ -1,166 +0,0 @@
|
|||
#lang hyper-literate #:♦ #:no-auto-require (dotlambda/unhygienic . racket/base)
|
||||
|
||||
♦require[scribble-math
|
||||
racket/require
|
||||
(for-label (subtract-in (only-meta-in 0 type-expander/lang)
|
||||
subtemplate/override)
|
||||
typed-worklist
|
||||
type-expander/expander
|
||||
phc-toolkit/untyped/aliases
|
||||
phc-toolkit/untyped/syntax-parse
|
||||
subtemplate/override)]
|
||||
|
||||
♦title[#:style (with-html5 manual-doc-style)
|
||||
#:tag "graph-draft"
|
||||
#:tag-prefix "phc-graph/graph-draft"]{Draft of the implementation of
|
||||
the graph macro}
|
||||
|
||||
♦(chunks-toc-prefix
|
||||
'("(lib phc-graph/scribblings/phc-graph-implementation.scrbl)"
|
||||
"phc-graph/graph-draft"))
|
||||
|
||||
♦chunk[<overview>
|
||||
(define low-graph-impl
|
||||
(syntax-parser
|
||||
[<signature+metadata>
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
|<phase 1: call mappings and extract placeholders>|
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
|<phase 2: inline placeholders within node boundaries>|
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
|<phase 3: replace indices with promises>|
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
<equality-coalescing>
|
||||
<invariants+auto-fill>
|
||||
<inflexible-row-polymorphism>
|
||||
<flexible-row-polymorphism>
|
||||
<polymorphic-node-types-and-mappings>
|
||||
;<general-purpose-graph-algorithms>
|
||||
;<garbage-collection>
|
||||
|
||||
|
||||
|<phase~1: call mappings and extract placeholders>|
|
||||
]))]
|
||||
|
||||
♦chunk[<signature+metadata>
|
||||
<signature>
|
||||
<metadata>]
|
||||
|
||||
♦chunk[<signature>
|
||||
(_ graph-name
|
||||
#:∀ (pvarₕ …)
|
||||
({~lit node} nodeᵢ [fieldᵢⱼ cᵢⱼ:colon field-τᵢⱼ] …)
|
||||
…
|
||||
({~lit mapping} (mappingₖ [argₖₗ :colon arg-τₖₗ] …)
|
||||
:colon result-τₖ
|
||||
. bodyₖ)
|
||||
…)]
|
||||
|
||||
♦chunk[<metadata>
|
||||
(void)]
|
||||
|
||||
♦chunk[|<phase 1: call mappings and extract placeholders>|
|
||||
'<worklist>
|
||||
'<call-mapping-functions+placeholders>
|
||||
'<extract-placeholders> ;; and put them into the worklist
|
||||
]
|
||||
|
||||
♦chunk[|<phase~1: call mappings and extract placeholders>|
|
||||
#'(begin
|
||||
(define
|
||||
#:∀ (pvarₕ …)
|
||||
(graph-name [rootₖ : (Listof (List arg-τₖₗ …))] …)
|
||||
|
||||
;; TODO: move these to a separate literate programming chunk
|
||||
(define-type nodeᵢ (tagged nodeᵢ [fieldᵢⱼ cᵢⱼ field-τᵢⱼ] …))
|
||||
…
|
||||
|
||||
(define (make-placeholderₖ argₖₗ …)
|
||||
(list 'placeholderₖ argₖₗ …))
|
||||
…
|
||||
|
||||
(worklist
|
||||
(list rootₖ …)
|
||||
((λ ([args : (List arg-τₖₗ …)])
|
||||
(define-values (argₖₗ …) (apply values args))
|
||||
(define result
|
||||
(let* ([mappingₖ make-placeholderₖ]
|
||||
…
|
||||
[argₖₗ 'convert-inflexible-to-flexible?]
|
||||
…
|
||||
[argₖₗ 'invariant-well-scopedness?]
|
||||
…)
|
||||
(error "NOT IMPL YET.787543")
|
||||
;. bodyₖ
|
||||
'(bodyₖ)))
|
||||
;; returns placeholders + the result:
|
||||
'(extract-placeholders result)
|
||||
(error "NOT IMPL YET.8946513648"))
|
||||
…)
|
||||
((List arg-τₖₗ …) result-τₖ) …)))]
|
||||
|
||||
♦chunk[|<phase 1: call mappings and extract placeholders>|
|
||||
;; Phase 1: call the mapping functions on the input data
|
||||
#'(: phase-1 (∀ (pvarₕ …) ;; or use this? (nodes-pvar … mapping-pvar … …)
|
||||
(→ (List (Listof mapping-arg-type) ddd)
|
||||
(List (Listof mapping-result-type) ddd))))
|
||||
#'(begin
|
||||
;; Maybe this should be done last, when all phases are available?
|
||||
(define (phase1-many-roots (argₖₗ …) …) 'TODO)
|
||||
(define (phase1-single-root-for-mapping (argₖₗ …)) 'TODO)
|
||||
…)]
|
||||
|
||||
♦chunk[|<phase 2: inline placeholders within node boundaries>|
|
||||
;; Phase 2: inline placeholders within node boundaries
|
||||
'(generate-worklist
|
||||
nodes
|
||||
#'(…?))
|
||||
'{(funcion which for a mapping-result → inserts nodes into worklist) …}
|
||||
'(for the root mapping results
|
||||
call the function to insert nodes and keep the surrounding part)
|
||||
'(for each mapping result
|
||||
call the function to insert nodes)]
|
||||
|
||||
♦chunk[|<phase 3: replace indices with promises>|
|
||||
;; Phase 3: Replace indices with promises
|
||||
;; Phase 3a: have an empty set of invariant witnesses, and call the
|
||||
;; invariants for checking
|
||||
;; Phase 3b: have the full set of invariant witnesses.
|
||||
;; TODO phase 3: auto-fill.
|
||||
(void)]
|
||||
|
||||
♦chunk[<equality-coalescing>
|
||||
;; implement as always-#f-unless-eq? for now
|
||||
(void)]
|
||||
♦chunk[<invariants+auto-fill>
|
||||
(void)]
|
||||
♦chunk[<inflexible-row-polymorphism>
|
||||
(void)]
|
||||
♦chunk[<flexible-row-polymorphism>
|
||||
(void)]
|
||||
♦chunk[<polymorphic-node-types-and-mappings>
|
||||
(void)]
|
||||
|
||||
♦chunk[<overview>
|
||||
; high-level graph API:
|
||||
#;(<metadata2>
|
||||
<extending-existing-graph-types>
|
||||
<invariants-for-extended-graph-types>
|
||||
<auto-generate-mappings>)]
|
||||
|
||||
Row polymorphism: make a generic struct->vector and vector->struct?
|
||||
|
||||
♦chunk[<*>
|
||||
(provide low-graph-impl
|
||||
(for-template (all-from-out "literals.rkt")))
|
||||
|
||||
(require (for-template (only-meta-in 0 type-expander/lang)
|
||||
typed-worklist
|
||||
phc-adt)
|
||||
type-expander/expander
|
||||
phc-toolkit/untyped/aliases
|
||||
phc-toolkit/untyped/syntax-parse
|
||||
subtemplate/override)
|
||||
|
||||
(require (for-template "literals.rkt"))
|
||||
<overview>]
|
||||
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,3 +0,0 @@
|
|||
#lang phc-graph/make-lang
|
||||
|
||||
#:require (type-expander/lang phc-toolkit)
|
||||
|
|
@ -1,5 +0,0 @@
|
|||
#lang phc-graph/make-lang-example
|
||||
(let ()
|
||||
(ann 1 Number) ;; from type-expander/lang
|
||||
(ann (∘ add1 sub1) (-> Number Number)) ;; From phc-toolkit
|
||||
(void))
|
||||
|
|
@ -1,46 +0,0 @@
|
|||
#lang at-exp racket/base
|
||||
|
||||
(module reader syntax/module-reader
|
||||
phc-graph/make-lang)
|
||||
|
||||
(provide (rename-out [-#%module-begin #%module-begin]))
|
||||
|
||||
(require (for-syntax racket/base
|
||||
setup/collects)
|
||||
scribble/manual)
|
||||
|
||||
(define-syntax (-#%module-begin stx)
|
||||
(syntax-case stx ()
|
||||
[(self #:require req)
|
||||
;; TODO: isn't there a more reliable way to get the "require path"
|
||||
;; for the source module of #'self ?
|
||||
(let* ([src (syntax-source #'self)]
|
||||
[modpath (path->module-path src)]
|
||||
[md (if (and (pair? modpath)
|
||||
(eq? (car modpath) 'lib)
|
||||
(string? (cadr modpath))
|
||||
(null? (cddr modpath))
|
||||
(regexp-match ".rkt$" (cadr modpath)))
|
||||
(string->symbol
|
||||
(substring (cadr modpath)
|
||||
0
|
||||
(- (string-length (cadr modpath)) 4)))
|
||||
modpath)])
|
||||
#`(-#%module-begin #:module #,md #:require req))]
|
||||
[(_ #:module md ;; TODO: detect this automatically
|
||||
#:require (req ...))
|
||||
#`(#%module-begin
|
||||
(module reader syntax/module-reader
|
||||
md)
|
||||
@module[scrbl racket/base (require scribble/manual)]{
|
||||
@defmodule[md]{
|
||||
This module language re-provides the following modules:
|
||||
@itemlist[(item (racketmodname req)) ...]
|
||||
}
|
||||
}
|
||||
(module doc racket/base
|
||||
(require (submod ".." scrbl))
|
||||
(provide (all-from-out (submod ".." scrbl))))
|
||||
(require req ...)
|
||||
(provide (all-from-out req ...)))]))
|
||||
|
||||
|
|
@ -1,7 +0,0 @@
|
|||
#lang racket
|
||||
|
||||
(require scribble/base)
|
||||
|
||||
(provide texsubtype)
|
||||
|
||||
(define texsubtype "<:")
|
||||
Binary file not shown.
|
Before Width: | Height: | Size: 76 KiB |
Binary file not shown.
|
Before Width: | Height: | Size: 61 KiB |
Binary file not shown.
|
Before Width: | Height: | Size: 49 KiB |
|
|
@ -1,21 +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-with2.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)]
|
||||
@include-section[(submod "../main-draft.hl.rkt" doc)]
|
||||
@include-section[(submod "../flexible-with-generalized-ctor.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,20 +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))
|
||||
(remembered! tagged-structure (t0 w))
|
||||
(remembered! tagged-structure (City streets))
|
||||
(remembered! tagged-structure (Street a 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,144 +0,0 @@
|
|||
#lang typed/dotlambda
|
||||
(require type-expander)
|
||||
|
||||
(require (lib "phc-graph/invariants-phantom.hl.rkt")
|
||||
"util.rkt"
|
||||
phc-graph/dot-lang
|
||||
phc-toolkit)
|
||||
|
||||
(check-same-type
|
||||
(Π .a.aa(.b.c)*.d.e)
|
||||
(Rec
|
||||
R1
|
||||
(U (Pairof Any R1)
|
||||
(Pairof
|
||||
(Pairof 'a AnyType)
|
||||
(Pairof
|
||||
(Pairof 'aa AnyType)
|
||||
(Rec
|
||||
R2
|
||||
(U (Pairof
|
||||
(Pairof 'b AnyType)
|
||||
(Pairof (Pairof 'c AnyType) R2))
|
||||
(List (Pairof 'd AnyType) (Pairof 'e AnyType)))))))))
|
||||
|
||||
(struct a AnyType ()); the node type a.
|
||||
(struct b AnyType ()); the node type b.
|
||||
|
||||
(check-same-type
|
||||
(Π :a.aa(.b.c)*.d.e)
|
||||
(Rec
|
||||
R1
|
||||
(U (Pairof Any R1)
|
||||
(Pairof
|
||||
(Pairof AnyField a)
|
||||
(Pairof
|
||||
(Pairof 'aa AnyType)
|
||||
(Rec
|
||||
R2
|
||||
(U (List (Pairof 'd AnyType) (Pairof 'e AnyType))
|
||||
(Pairof (Pairof 'b AnyType) (Pairof (Pairof 'c AnyType) R2)))))))))
|
||||
(check-same-type
|
||||
(Π :a(.b.c)*.d.e)
|
||||
(Rec
|
||||
R1
|
||||
(U (Pairof Any R1)
|
||||
(Pairof
|
||||
(Pairof AnyField a)
|
||||
(Rec
|
||||
R2
|
||||
(U (List (Pairof 'd AnyType) (Pairof 'e AnyType))
|
||||
(Pairof (Pairof 'b AnyType) (Pairof (Pairof 'c AnyType) R2))))))))
|
||||
|
||||
(check-same-type
|
||||
(Π :a(.b.c(.w)*.x.y)*.d.e)
|
||||
(Rec
|
||||
R1
|
||||
(U (Pairof Any R1)
|
||||
(Pairof
|
||||
(Pairof AnyField a)
|
||||
(Rec
|
||||
R2
|
||||
(U (List (Pairof 'd AnyType) (Pairof 'e AnyType))
|
||||
(Pairof
|
||||
(Pairof 'b AnyType)
|
||||
(Pairof
|
||||
(Pairof 'c AnyType)
|
||||
(Rec
|
||||
R3
|
||||
(U (Pairof (Pairof 'w AnyType) R3)
|
||||
(Pairof
|
||||
(Pairof 'x AnyType)
|
||||
(Pairof (Pairof 'y AnyType) R2))))))))))))
|
||||
|
||||
;; TODO: test with deeper nesting of ()*
|
||||
|
||||
(check-same-type
|
||||
(Invariant :a(.b.c(.w)*.x.y)*.d.e ≡ :a(.b.c)*.d.e)
|
||||
(Invariant :a(.b.c(.w)*.x.y)*.d.e ≡ :a(.b.c)*.d.e))
|
||||
|
||||
(check-same-type
|
||||
(Invariant :a(.b.c(.w)*.x.y)*.d.e
|
||||
∈
|
||||
:a(.b.c)*.d.e)
|
||||
(Invariant :a(.b.c)*.d.e
|
||||
∋
|
||||
:a(.b.c(.w)*.x.y)*.d.e))
|
||||
|
||||
|
||||
;;;
|
||||
|
||||
(check-ann witness-value (Invariants)) ;; No invariants
|
||||
(check-ann witness-value (Invariants (:a ≡ :a.b.c)))
|
||||
|
||||
(check-a-stronger-than-b (Invariants (:a ≡ :a.b.c))
|
||||
(Invariants))
|
||||
(check-a-same-as-b (Invariants (:a ≡ :a.b.c))
|
||||
(Invariants (:a.b.c ≡ :a)))
|
||||
(check-a-stronger-than-b (Invariants (: ≡ :b.c)
|
||||
(: ≡ :b.d))
|
||||
(Invariants (: ≡ :b.c)))
|
||||
(check-a-stronger-than-b (Invariants (: ≡ :b.d)
|
||||
(: ≡ :b.c))
|
||||
(Invariants (: ≡ :b.c)))
|
||||
|
||||
;; ∀ .b.d(.a.b.>d)* of length ≥ 5
|
||||
;; is stronger than
|
||||
;; ∀ .b.d(.a.b.>d)* of length ≥ 8
|
||||
;; as the elements of the latter are included in the former, but
|
||||
;; the first element (length = 5) is missing in the latter, so the
|
||||
;; former constrains more paths.
|
||||
(check-a-stronger-than-b (Invariants (: ≡ .b.d(.a.b.d)*))
|
||||
(Invariants (: ≡ .b.d.a.b.d(.a.b.d)*)))
|
||||
|
||||
(check-a-stronger-than-b (Invariants (: ≡ .a.b.c(.d.e)*))
|
||||
(Invariants (: ≡ .a.b.c.d.e)))
|
||||
|
||||
|
||||
(check-a-stronger-than-b (Invariants (.l ≥ (+ (length .a.b.c(.d.e)*) 3)))
|
||||
(Invariants (.l ≥ (+ (length .a.b.c(.d.e)*) 2))))
|
||||
|
||||
(check-a-stronger-than-b (Invariants (.l ≥ (+ (length .a.b.c(.d.e)*) 1)))
|
||||
(Invariants (.l ≥ (length .a.b.c(.d.e)*))))
|
||||
|
||||
(check-a-stronger-than-b (Invariants (.l ≤ (+ (length .a.b.c(.d.e)*) 2)))
|
||||
(Invariants (.l ≤ (+ (length .a.b.c(.d.e)*) 3))))
|
||||
|
||||
(check-a-stronger-than-b (Invariants (.l ≤ (length .a.b.c(.d.e)*)))
|
||||
(Invariants (.l ≤ (+ (length .a.b.c(.d.e)*) 1))))
|
||||
|
||||
(check-a-stronger-than-b (Invariants (.l = (length .a.b.c(.d.e)*)))
|
||||
(Invariants (.l ≥ (length .a.b.c(.d.e)*))))
|
||||
|
||||
(check-a-stronger-than-b (Invariants (.l = (+ (length .a.b.c(.d.e)*) 1)))
|
||||
(Invariants (.l ≤ (+ (length .a.b.c(.d.e)*) 1))))
|
||||
|
||||
(check-same-type (Invariants (.l = (length .a.b.c(.d.e)*)))
|
||||
(Invariants (.l = (+ (length .a.b.c(.d.e)*) 0))))
|
||||
|
||||
(check-a-stronger-than-b (Invariants (:a.l ≥ (+ (length :a.f.g) 3))
|
||||
(:a ≡ :a.f.h)
|
||||
(:a ∉ :a.f.g))
|
||||
(Invariants (:a.l ≥ (+ (length :a.f.g) 2))
|
||||
(:a ≢ :a.f.g.0)
|
||||
(:a ≢ :a.f.g.1)))
|
||||
|
|
@ -1,36 +0,0 @@
|
|||
#lang type-expander
|
||||
|
||||
(provide check-a-same-as-b
|
||||
check-a-stronger-than-b
|
||||
check-same-type)
|
||||
|
||||
(require phc-toolkit
|
||||
(lib "phc-graph/invariants-phantom.hl.rkt")
|
||||
(for-syntax phc-toolkit/untyped))
|
||||
|
||||
(define-syntax (check-a-stronger-than-b stx)
|
||||
(syntax-case stx ()
|
||||
[(_ stronger weaker)
|
||||
(syntax/top-loc stx
|
||||
(begin (check-ann (ann witness-value stronger)
|
||||
weaker)
|
||||
(check-not-tc
|
||||
(ann (ann witness-value weaker) stronger))))]))
|
||||
|
||||
(define-syntax (check-a-same-as-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)))]))
|
||||
|
||||
(define-syntax (check-same-type stx)
|
||||
(syntax-case stx ()
|
||||
[(_ a b)
|
||||
(syntax/top-loc stx
|
||||
(begin
|
||||
(check-not-exn:
|
||||
(λ () (λ ([x : a]) (check-ann x b))))
|
||||
(check-not-exn:
|
||||
(λ () (λ ([x : b]) (check-ann x a))))))]))
|
||||
|
|
@ -1,22 +0,0 @@
|
|||
#lang type-expander
|
||||
|
||||
(require (for-syntax racket))
|
||||
|
||||
;; This seems to be a slow-starting exponential, with a factor of ×2.5
|
||||
;; each time n is increased by 100.
|
||||
;; n=500 takes nearly 3 minutes, n=1000 should, by projection, take 4.5 hours.
|
||||
(define-for-syntax n 200)
|
||||
|
||||
(: f ((Λ (_)
|
||||
(with-syntax ([(T ...)
|
||||
(map (λ (i) (gensym 'τ)) (range n))])
|
||||
#'(∀ (A B T ...)
|
||||
(→ (List A T ...) B (List B T ...)))))))
|
||||
(define (f l v)
|
||||
(cons v (cdr l)))
|
||||
|
||||
(define-syntax (callf stx)
|
||||
(with-syntax ([(v ...) (range n)])
|
||||
#'(f (list "a" v ...) 'x)))
|
||||
|
||||
(define cf (callf))
|
||||
|
|
@ -1,49 +0,0 @@
|
|||
#lang type-expander
|
||||
|
||||
(require (for-syntax racket))
|
||||
|
||||
;; This seems to be a slow-starting exponential, with a factor of ×2.5
|
||||
;; each time n is increased by 100.
|
||||
;; n=500 takes nearly 3 minutes, n=1000 should, by projection, take 4.5 hours.
|
||||
(define-for-syntax n 200)
|
||||
|
||||
(: kons (∀ (A B) (→ A B (Pairof A B))))
|
||||
(define kons cons)
|
||||
|
||||
(: f ((Λ (_)
|
||||
(with-syntax ([(T ...)
|
||||
(map (λ (i) (gensym 'τ)) (range n))]
|
||||
[(T₂ ...)
|
||||
(map (λ (i) (gensym 'τ)) (range n))]
|
||||
[(T₃ ...)
|
||||
(map (λ (i) (gensym 'τ)) (range n))])
|
||||
#'(∀ (A B T ...)
|
||||
(→ (List A T ...)
|
||||
B
|
||||
(∀ (A₂ T₂ ...)
|
||||
(→ (List A₂ T₂ ...)
|
||||
(∀ (A₃ T₃ ...)
|
||||
(→ (List (List A T ...)
|
||||
(List A₂ T₂ ...)
|
||||
(List A₃ T₃ ...))
|
||||
(List (List B T ...)
|
||||
(List B T₂ ...)
|
||||
(List B T₃ ...))))))))))))
|
||||
(define (((f l v) ll) alll)
|
||||
(list (kons v (cdr (car alll)))
|
||||
(kons v (cdr (cadr alll)))
|
||||
(kons v (cdr (caddr alll)))))
|
||||
|
||||
(define-syntax (callf stx)
|
||||
(with-syntax ([(v ...) (range n)]
|
||||
[(v₂ ...) (map number->string (range n))]
|
||||
[(v₃ ...) (map string->symbol (map number->string (range n)))])
|
||||
#'(((f
|
||||
(list "a" v ...)
|
||||
'x)
|
||||
(list "aa" v₂ ...))
|
||||
(list (list "a" v ...)
|
||||
(list "aa" v₂ ...)
|
||||
(list 'aaa 'v₃ ...)))))
|
||||
|
||||
(define cf (callf))
|
||||
|
|
@ -1,79 +0,0 @@
|
|||
#lang dotlambda/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,57 +0,0 @@
|
|||
#lang type-expander
|
||||
|
||||
(require "../flexible-with2.hl.rkt"
|
||||
phc-toolkit/typed-rackunit-extensions)
|
||||
|
||||
(check-ann ((record-builder 4 1 2 4 7 14) 'a 'b 'c 'd 'e)
|
||||
(Pairof
|
||||
(Pairof
|
||||
(Pairof (Pairof empty1/τ 'a) (Pairof 'b empty1/τ))
|
||||
(Pairof (Pairof 'c empty1/τ) (Pairof empty1/τ 'd)))
|
||||
(Pairof empty4/τ (Pairof empty2/τ (Pairof 'e empty1/τ)))))
|
||||
|
||||
(with-ρ (Row)
|
||||
(define-type test
|
||||
(∀ρ (A #:ρ Row)
|
||||
(→ (List A Row)
|
||||
(record a b . Row)
|
||||
(List A Row)
|
||||
(record a c . Row)))))
|
||||
|
||||
;; TODO: I'm pretty sure that the lift-ing will cause some unbound identifier
|
||||
;; or out of context id errors, when τ' refers to a locally-declared type.
|
||||
|
||||
(with-ρ (Row)
|
||||
(define-type testf-τ (∀ρ (A #:ρ Row)
|
||||
(→ (→ (List A Row)
|
||||
(record x y . Row)
|
||||
(List A Row)
|
||||
(record y z . Row))
|
||||
Void)))
|
||||
(: testf
|
||||
(∀ρ (A #:ρ Row)
|
||||
(→ (→ (List A Row)
|
||||
(record x y . Row)
|
||||
(List A Row)
|
||||
(record y z . Row))
|
||||
Void)))
|
||||
(define (testf f)
|
||||
(: tmp (→ (record w x . Row) Any))
|
||||
(define (tmp r) r)
|
||||
(void)))
|
||||
|
||||
(let ()
|
||||
(with-ρ (Row)
|
||||
(define-type Naht Integer)
|
||||
(: testf
|
||||
(∀ρ (A #:ρ Row)
|
||||
(→ (→ (List Naht A Row)
|
||||
(record x y . Row)
|
||||
(List Naht A Row)
|
||||
(record y z . Row))
|
||||
Void)))
|
||||
(define (testf f)
|
||||
(: tmp (→ (record w x . Row) Any))
|
||||
(define (tmp r) r)
|
||||
(void)))
|
||||
testf)
|
||||
|
|
@ -1,14 +0,0 @@
|
|||
#lang type-expander
|
||||
|
||||
(require (lib "phc-graph/flexible-with2.hl.rkt")
|
||||
phc-toolkit/typed-rackunit-extensions)
|
||||
|
||||
(with-ρ (Row)
|
||||
(define-type test
|
||||
(∀ρ (A #:ρ Row)
|
||||
(→ Any Any))))
|
||||
|
||||
(with-ρ (Row)
|
||||
(define-type test2
|
||||
(∀ρ (A #:ρ Row)
|
||||
(→ Any Any))))
|
||||
|
|
@ -1,19 +0,0 @@
|
|||
#lang dotlambda/unhygienic type-expander/lang
|
||||
|
||||
(require (for-syntax (lib "phc-graph/main-draft.hl.rkt")))
|
||||
(require phc-adt)
|
||||
(adt-init)
|
||||
|
||||
(define-syntax low-graph low-graph-impl)
|
||||
|
||||
(low-graph
|
||||
g
|
||||
#:∀ (A)
|
||||
(node City [streets : (Listof Street)])
|
||||
(node Street [name : String] [a : A])
|
||||
(mapping (make-city [names : (Listof (Pairof String A))])
|
||||
: City
|
||||
(City (map make-street names)))
|
||||
(mapping (make-street [p : (Pairof String A)])
|
||||
: Street
|
||||
(Street (car p) (cdr p))))
|
||||
|
|
@ -1,43 +0,0 @@
|
|||
#lang typed/racket
|
||||
;; 1.36s
|
||||
(require phc-adt)
|
||||
;; 3.26s
|
||||
(require (lib "phc-graph/graph-type.hl.rkt"))
|
||||
;; 3.46s
|
||||
(adt-init)
|
||||
;; 3.36
|
||||
(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)
|
||||
;; 5.46
|
||||
(provide g1)
|
||||
;; 5.51s
|
||||
(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)))
|
||||
;; 5.40
|
||||
|
||||
(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))
|
||||
;; 6.76s
|
||||
|
|
@ -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,116 +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 stxparse-info/parse
|
||||
stxparse-info/parse/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)
|
||||
)))))
|
||||
|
||||
406
traversal.hl.rkt
406
traversal.hl.rkt
|
|
@ -1,406 +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
|
||||
(except-in subtemplate/override begin let)
|
||||
type-expander
|
||||
phc-adt
|
||||
(except-in (subtract-in typed/racket/base
|
||||
type-expander
|
||||
subtemplate/override)
|
||||
values)
|
||||
(only-in racket/base values)
|
||||
(subtract-in racket/contract typed/racket/base)
|
||||
(except-in phc-toolkit generate-temporary)
|
||||
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
|
||||
(list [cons #'_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
|
||||
(list [cons #'_type-to-replaceᵢ #'_updateᵢ] …)))
|
||||
(define/with-syntax _args #'({?@ _predicateᵢ _updateᵢ} …))
|
||||
(cached [f-
|
||||
(get-f-cache)
|
||||
(get-f-defs)
|
||||
#'(_whole-type _type-to-replaceᵢ …)]
|
||||
#`[<fold-f-proc>
|
||||
<fold-f-type>])]))]
|
||||
|
||||
@CHUNK[<fold-f-proc>
|
||||
(λ ({?@ _predicateᵢ _updateᵢ} …)
|
||||
(λ (v acc)
|
||||
#,(syntax-parse #'_whole-type
|
||||
#:literals (Null Pairof Listof List
|
||||
Vectorof Vector U tagged)
|
||||
<f-cases>)))]
|
||||
|
||||
@chunk[<fold-f-type>
|
||||
(∀ (_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) <f-list-car>]
|
||||
[(result-y* acc-y*) <f-list-cdr>])
|
||||
(values (cons result-x result-y*) acc-y*))]]
|
||||
|
||||
where the replacement is applied to the @racket[car], and to the @racket[cdr]
|
||||
as a whole (i.e. by recursion on the whole remaining list of types):
|
||||
|
||||
@chunk[<f-list-car>
|
||||
((!replace-in-instance X . rec-args) (car v) acc)]
|
||||
|
||||
@chunk[<f-list-cdr>
|
||||
((!replace-in-instance (List Y …) . rec-args) (cdr v) acc-x)]
|
||||
|
||||
@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 (subtract-in racket/base
|
||||
subtemplate/override)
|
||||
subtemplate/override
|
||||
phc-toolkit/untyped
|
||||
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