diff --git a/.gitignore b/.gitignore deleted file mode 100644 index 33ed4b8..0000000 --- a/.gitignore +++ /dev/null @@ -1,7 +0,0 @@ -*~ -\#* -.\#* -.DS_Store -compiled/ -/doc/ -/.~*.vue \ No newline at end of file diff --git a/.travis.yml b/.travis.yml deleted file mode 100644 index 12b2795..0000000 --- a/.travis.yml +++ /dev/null @@ -1,60 +0,0 @@ -language: c - -# Based from: https://github.com/greghendershott/travis-racket - -# Optional: Remove to use Travis CI's older infrastructure. -sudo: false - -env: - global: - # Supply a global RACKET_DIR environment variable. This is where - # Racket will be installed. A good idea is to use ~/racket because - # that doesn't require sudo to install and is therefore compatible - # with Travis CI's newer container infrastructure. - - RACKET_DIR=~/racket - matrix: - # Supply at least one RACKET_VERSION environment variable. This is - # used by the install-racket.sh script (run at before_install, - # below) to select the version of Racket to download and install. - # - # Supply more than one RACKET_VERSION (as in the example below) to - # create a Travis-CI build matrix to test against multiple Racket - # versions. - #- RACKET_VERSION=6.0 - #- RACKET_VERSION=6.1 - #- RACKET_VERSION=6.1.1 - #- RACKET_VERSION=6.2 - #- RACKET_VERSION=6.3 - #- RACKET_VERSION=6.4 - #- RACKET_VERSION=6.5 - #- RACKET_VERSION=6.6 - #- RACKET_VERSION=6.7 - - RACKET_VERSION=HEAD - -matrix: - allow_failures: -# - env: RACKET_VERSION=HEAD - fast_finish: true - -before_install: -- git clone https://github.com/greghendershott/travis-racket.git ~/travis-racket -- cat ~/travis-racket/install-racket.sh | bash # pipe to bash not sh! -- export PATH="${RACKET_DIR}/bin:${PATH}" #install-racket.sh can't set for us - -install: - - raco pkg install -j 2 --deps search-auto - -before_script: - -# Here supply steps such as raco make, raco test, etc. You can run -# `raco pkg install --deps search-auto` to install any required -# packages without it getting stuck on a confirmation prompt. -script: - - raco test -p phc-graph - - raco setup --check-pkg-deps --no-zo --no-launcher --no-install --no-post-install --no-docs --pkgs phc-graph - - raco pkg install --deps search-auto doc-coverage - - raco doc-coverage phc-graph - -after_success: - - raco pkg install --deps search-auto cover cover-coveralls - - raco cover -b -f coveralls -d $TRAVIS_BUILD_DIR/coverage . diff --git a/Graph-notes-copy2.vue b/Graph-notes-copy2.vue deleted file mode 100644 index bf02533..0000000 --- a/Graph-notes-copy2.vue +++ /dev/null @@ -1,3887 +0,0 @@ - - - - - - - - - Graph-notes-copy2.vue - - - #FFFFFF - #404040 - #000000 - SansSerif-plain-14 - http://vue.tufts.edu/rdf/resource/6dbf6af7c0a80026548592b8dffca40a - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6dbf6afcc0a80026548592b833e3a781 - - - - #8AEE95 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6dbf6afec0a80026548592b88abb8384 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6dbf6affc0a80026548592b80b4ee7cc - - - 6 - 7 - - - #8AEE95 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6dbf6b03c0a80026548592b81914701e - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6dbf6b04c0a80026548592b8c27d0837 - - - 6 - 11 - - - #8AEE95 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6dbf6b05c0a80026548592b80343782b - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6dbf6b06c0a80026548592b870fb7c6a - - - 6 - 13 - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6dbf6b07c0a80026548592b8f5e19e10 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6dbf6b08c0a80026548592b840ee8fa0 - - - 6 - 15 - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6dbf6b09c0a80026548592b8217a1807 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6dbf6b09c0a80026548592b8dfab693e - - - 13 - 17 - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6dbf6b0ac0a80026548592b87ee8d14b - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6dbf6b11c0a80026548592b89f9e9272 - - - 13 - 19 - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6dbf6b12c0a80026548592b83be06baa - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6dbf6b13c0a80026548592b8f03d2a45 - - - 13 - 21 - - - #8AEE95 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6dbf6b14c0a80026548592b8bc35fbb9 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6dbf6b14c0a80026548592b87410806e - - - 15 - 23 - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6dc1a307c0a80026548592b8c2af76c4 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6dc1a307c0a80026548592b8a04c0bf0 - - - 11 - 25 - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6dc1a308c0a80026548592b8ff6b1596 - - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6dc1a309c0a80026548592b84e893214 - - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6dc1a30ac0a80026548592b8ea42a1af - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6dc1a30ac0a80026548592b87117f4c4 - - - 25 - 33 - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6dc1a30bc0a80026548592b83098fe4a - - - 33 - 29 - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6dc1a30bc0a80026548592b8e12add9f - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6dc1a30cc0a80026548592b879e5ac96 - - - 33 - 36 - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6dc99799c0a80026548592b87d2d4299 - - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6dcae10dc0a80026548592b847b6398e - - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6dd89bd2c0a80026548592b8d3f60760 - - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6dd89bd4c0a80026548592b8697d13c4 - - - - #FEFEC9 - #EA2218 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6dd89bd5c0a80026548592b8ddb5b6c7 - - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6dd89bd6c0a80026548592b853276e56 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6dd89bd6c0a80026548592b89262c338 - - - 90 - 105 - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6dd89bd6c0a80026548592b8c817c8d9 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6dd89bd6c0a80026548592b88ac312bd - - - 90 - 107 - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6dda878ec0a80026548592b8416c8f4f - - - - #000000 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6dda878ec0a80026548592b8d9e1112c - - - 107 - 109 - - - #F2AE45 - #000000 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44031c0a80026548592b83703e1b4 - - - - #C1F780 - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44031c0a80026548592b885daa51d - - - - #FFFFFF - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44031c0a80026548592b88d7a52cf - - - - #FFFFFF - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44031c0a80026548592b8fe262430 - - - - #C1F780 - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44031c0a80026548592b8ba0f1bbc - - - - #C1F780 - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44032c0a80026548592b8ce56fcb8 - - - - #C1F780 - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44032c0a80026548592b84c0668a9 - - - - #C1F780 - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44032c0a80026548592b844ae0a4b - - - - #F2AE45 - #000000 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44032c0a80026548592b8746d8906 - - - - #C1F780 - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44032c0a80026548592b8eab64176 - - - - #FFFFFF - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44032c0a80026548592b8e2b0179a - - - - #FFFFFF - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44032c0a80026548592b8f1e9514a - - - - #FFFFFF - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44032c0a80026548592b8726ffcc1 - - - - #C1F780 - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44033c0a80026548592b8ff3e3904 - - - - #FFFFFF - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44033c0a80026548592b8e43cd085 - - - - #C1F780 - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44033c0a80026548592b80a95f30b - - - - #F2AE45 - #000000 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44033c0a80026548592b8a738f623 - - - - #C1F780 - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44033c0a80026548592b840e9de75 - - - - #FFFFFF - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44033c0a80026548592b869523b7f - - - - #FFFFFF - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44033c0a80026548592b80ecff1d4 - - - - #FFFFFF - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44033c0a80026548592b8868c3bd4 - - - - #FFFFFF - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44033c0a80026548592b8f1f2c034 - - - - #C1F780 - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44033c0a80026548592b81f88086b - - - - #C1F780 - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44034c0a80026548592b8a06db952 - - - - #F2AE45 - #000000 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44034c0a80026548592b84247db44 - - - - #FFFFFF - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44034c0a80026548592b80183cc60 - - - - #FFFFFF - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44034c0a80026548592b8a53213f5 - - - - #FFFFFF - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44034c0a80026548592b88fe1f15c - - - - #C1F780 - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44034c0a80026548592b804a1a9ba - - - - #C1F780 - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44034c0a80026548592b8ad21ad51 - - - - #FFFFFF - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44034c0a80026548592b8f7cab75e - - - - #FFFFFF - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44035c0a80026548592b824a5ea38 - - - - #F2AE45 - #000000 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44035c0a80026548592b8fcd64fad - - #FFC63B - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6dcc935cc0a80026548592b89128dae1 - - - - - - #FFFFFF - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44035c0a80026548592b8414a595b - - - - #FFFFFF - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44035c0a80026548592b8e07930e9 - - - - #FFFFFF - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44035c0a80026548592b861833437 - - - - #C1F780 - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44035c0a80026548592b82804bc71 - - - - #FFFFFF - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44035c0a80026548592b80db43a99 - - - - #FFFFFF - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44035c0a80026548592b86a9bcf32 - - - - #FFFFFF - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44036c0a80026548592b82c6a1147 - - - - #F2AE45 - #000000 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44036c0a80026548592b88c7132d7 - - - - #C1F780 - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44036c0a80026548592b82856a3fe - - - - #FFFFFF - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44036c0a80026548592b8125e3add - - - - #FFFFFF - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44036c0a80026548592b8242976ae - - - - #FFFFFF - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44036c0a80026548592b8700f0c58 - - - - #C1F780 - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44036c0a80026548592b888f9f0fc - - - - #C1F780 - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44036c0a80026548592b829d22ddb - - - - #C1F780 - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44036c0a80026548592b8fb44d733 - - - - #F2AE45 - #000000 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44036c0a80026548592b8010e8b83 - - - - #C1F780 - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44037c0a80026548592b8b07192d1 - - - - #FFFFFF - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44037c0a80026548592b85d8d2676 - - - - #FFFFFF - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44037c0a80026548592b818309ef9 - - - - #FFFFFF - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44037c0a80026548592b8ce547432 - - - - #C1F780 - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44037c0a80026548592b8808f7487 - - - - #FFFFFF - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44037c0a80026548592b8f5b31808 - - - - #C1F780 - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6de44037c0a80026548592b8b71cf339 - - - - #F2AE45 - #000000 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6deb6c15c0a80026548592b8b3165e14 - - - - #F2AE45 - #000000 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6deb6c16c0a80026548592b8a5a2565a - - - - #F2AE45 - #000000 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6deb6c16c0a80026548592b82772e2e6 - - - - #F2AE45 - #000000 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6deb6c16c0a80026548592b844d9ed3a - - - - #F2AE45 - #000000 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6deb6c16c0a80026548592b8c110cac6 - - #F2AE45 - #000000 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6e0db15543a6be970d2ffe259c8e4183 - - - - #F2AE45 - #000000 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6e0db15643a6be970d2ffe25e7c11d51 - - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6e13f9e943a6be970d2ffe25a12d6061 - - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/518eb6ce534430712734d86a5ed52578 - - - - - - #F2AE45 - #000000 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6deb6c16c0a80026548592b84cf1af9a - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6dda878fc0a80026548592b8d8c09cc8 - - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6dda878ec0a80026548592b8a59d8be9 - - - - - - #F2AE45 - #000000 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6deb6c16c0a80026548592b8ef57e7b6 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6df4a0bec0a80026548592b8679982c0 - - - 17 - 188 - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6df4a0bec0a80026548592b8c719c5c2 - - - 17 - 179 - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6df4a0bec0a80026548592b87ce595a9 - - - 17 - 170 - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6df4a0bec0a80026548592b83272ecb3 - - - 19 - 161 - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6df4a0bec0a80026548592b847abd123 - - - 19 - 152 - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6df4a0bfc0a80026548592b82421558c - - - 21 - 143 - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6df4a0bfc0a80026548592b890a669f0 - - - 21 - 134 - - - #404040 - #404040 - Arial-plain-11 - http://vue.tufts.edu/rdf/resource/6df4a0bfc0a80026548592b8ab3caf16 - - - 68 - 211 - - - #F2AE45 - #000000 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6df83301c0a80026548592b8cadb0885 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6df83301c0a80026548592b86616b05c - - - 229 - 217 - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6dfdd7b2c0a80026548592b8f9159d49 - - - - #000000 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6dfdd7b2c0a80026548592b838839b4e - - - 107 - 231 - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6dfdd7b2c0a80026548592b8fe58d8d6 - - - - #000000 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6dfdd7b2c0a80026548592b8472714c9 - - - 107 - 233 - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6dff35b5c0a80026548592b8604b935b - - - - #000000 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6dff35b5c0a80026548592b8b8ea0a14 - - - 21 - 239 - - - #C1F780 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6e09fb5843a6be970d2ffe2507ab588a - - - - #000000 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6e09fb5a43a6be970d2ffe25101bab58 - - - 11 - 241 - - - #A6A6A6 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6e0b664b43a6be970d2ffe25608d7f84 - - - - #000000 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6e0b664b43a6be970d2ffe252aafd35e - - - 11 - 244 - - - #A6A6A6 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6e0b664c43a6be970d2ffe253b42a8fa - - - - #000000 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6e0b664c43a6be970d2ffe25426d76fa - - - 244 - 246 - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6e12548843a6be970d2ffe259bb5e939 - - - - #000000 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6e12548843a6be970d2ffe25f25ed174 - - - 23 - 252 - - - #FFFFFF - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6e18c7df43a6be970d2ffe25f6c630d7 - - - - #FFFFFF - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6e18c7df43a6be970d2ffe259db0c3ce - - - - #FFFFFF - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6e18c7df43a6be970d2ffe25e603c10f - - - - #FFFFFF - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6e18c7df43a6be970d2ffe25580295ca - - - - #FFFFFF - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6e18c7df43a6be970d2ffe250d1629cb - - - - #C1F780 - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6e18c7e043a6be970d2ffe25e477a71a - - - - #FFFFFF - #D0D0D0 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6e18c7e043a6be970d2ffe25b3ec0015 - - - - #F2AE45 - #000000 - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6e18c7e043a6be970d2ffe25522374c0 - - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6e18c7e043a6be970d2ffe25045c93ba - - - - #000000 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6e18c7e043a6be970d2ffe25f58b5507 - - - 216 - 269 - - - #000000 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6e18c7e043a6be970d2ffe25213bebda - - - 269 - 215 - - - #000000 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6e18c7e043a6be970d2ffe25b2914e66 - - - 264 - 269 - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6e1c69c643a6be970d2ffe25714e5bc9 - - - - #000000 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6e1c69c643a6be970d2ffe25ca3da090 - - - 90 - 278 - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6e1c69c643a6be970d2ffe25751b3e9d - - - - #000000 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6e1c69c643a6be970d2ffe25264e9ee1 - - - 90 - 280 - - - #000000 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6e1c69c643a6be970d2ffe25391232ea - - - 278 - 216 - - - #000000 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6e1c69c643a6be970d2ffe253e59616a - - - 278 - 264 - - - #000000 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6e1c69c643a6be970d2ffe2578e91de4 - - - 280 - 215 - - - #000000 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6e1c69c743a6be970d2ffe258016a9d1 - - - 280 - 214 - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6e1dc69443a6be970d2ffe25c307cfac - - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6e1fb64c43a6be970d2ffe25894f7080 - - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6e218e1c43a6be970d2ffe25c3d8bcae - - - - #000000 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6e218e1d43a6be970d2ffe253b54752d - - - 143 - 295 - - - #C1F780 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6e2c94fe43a6be970d2ffe25ab2d9e8d - - #404040 - #000000 - SansSerif-plain-14 - http://vue.tufts.edu/rdf/resource/6e2c950143a6be970d2ffe25c8aa5ef1 - <html> - <head> - <style type="text/css"> - <!-- - body { margin-top: 0px; margin-bottom: 0px; margin-left: 0px; margin-right: 0px; font-size: 12; font-family: SansSerif; color: #000000 } - ol { margin-top: 6; font-family: SansSerif; vertical-align: middle; margin-left: 30; font-size: 12; list-style-position: outside } - p { margin-top: 0; margin-left: 0; margin-right: 0; margin-bottom: 0; color: #000000 } - ul { margin-top: 6; font-size: 12; margin-left: 30; vertical-align: middle; list-style-position: outside; font-family: SansSerif } - --> - </style> - - </head> - <body> - <p> - <font face="DejaVu Sans Mono">(invariants-wrapper </font> - </p> - <p> - <font face="DejaVu Sans Mono">(case (&#8594; inv&#8321; inv-arg &#8230; #t) </font> - </p> - <p> - <font face="DejaVu Sans Mono">&#8230; </font> - </p> - <p> - <font face="DejaVu Sans Mono">(&#8594; inv&#8345; inv-arg &#8230; #t)))</font> - </p> - </body> -</html> - - - - - - - #000000 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6e309f2643a6be970d2ffe2565dbc3a9 - - - 291 - 314 - - - #C1F780 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6e309f2643a6be970d2ffe2541159360 - - #404040 - #000000 - -plain-12 - http://vue.tufts.edu/rdf/resource/6e309f2643a6be970d2ffe254bc731a8 - <html> - <head color="#000000" style="color: #000000"> - <style type="text/css"> - <!-- - body { margin-top: 0px; margin-bottom: 0px; margin-left: 0px; margin-right: 0px; font-size: 11; font-family: SansSerif; color: #000000 } - ol { margin-top: 6; font-family: SansSerif; vertical-align: middle; margin-left: 30; font-size: 11; list-style-position: outside } - p { margin-top: 0; margin-left: 0; margin-right: 0; margin-bottom: 0; color: #000000 } - ul { margin-top: 6; font-size: 11; margin-left: 30; vertical-align: middle; list-style-position: outside; font-family: SansSerif } - --> - </style> - - </head> - <body> - <p> - <font style="font-size:12;" color="#000000" face="DejaVu Sans Mono">(struct - invariants-wrapper ())</font> - </p> - </body> -</html> - - - - - - - #000000 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6e309f2643a6be970d2ffe25415de0b8 - - - 314 - 318 - - - #C1F780 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6e380d1843a6be970d2ffe256d1f3a53 - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6e38dc3343a6be970d2ffe25548c6fd1 - - - - #404040 - #000000 - SansSerif-plain-14 - http://vue.tufts.edu/rdf/resource/6e380d1843a6be970d2ffe2537b566f6 - <html> - <head color="#000000" style="color: #000000"> - <style type="text/css"> - <!-- - body { margin-top: 0px; margin-bottom: 0px; margin-left: 0px; margin-right: 0px; font-size: 12; font-family: SansSerif; color: #000000 } - ol { margin-top: 6; font-family: SansSerif; vertical-align: middle; margin-left: 30; font-size: 12; list-style-position: outside } - p { margin-top: 0; margin-left: 0; margin-right: 0; margin-bottom: 0; color: #000000 } - ul { margin-top: 6; font-size: 12; margin-left: 30; vertical-align: middle; list-style-position: outside; font-family: SansSerif } - --> - </style> - - </head> - <body> - <p color="#000000" style="color: #000000"> - <font face="DejaVu Sans Mono">(define-for-syntax invariant-introducer </font> - </p> - <p color="#000000" style="color: #000000"> - <font face="DejaVu Sans Mono">(make-syntax-introducer)) </font> - </p> - <p color="#000000" style="color: #000000"> - <font face="DejaVu Sans Mono">;; the body should return the syntax for a - type, </font> - </p> - <p color="#000000" style="color: #000000"> - <font face="DejaVu Sans Mono">;; such that less precise invariants are - supertypes of that type. </font> - </p> - <p color="#000000" style="color: #000000"> - <font face="DejaVu Sans Mono">(define-syntax/parse - (define-graph-invariant (name g-descriptor arg &#8230;) . body) </font> - </p> - <p color="#000000" style="color: #000000"> - <font face="DejaVu Sans Mono">#'(define-syntax name </font> - </p> - <p color="#000000" style="color: #000000"> - <font face="DejaVu Sans Mono">(graph-invariant </font> - </p> - <p color="#000000" style="color: #000000"> - <font face="DejaVu Sans Mono">(&#955; (g-descriptor arg &#8230;) . body))))</font> - </p> - </body> -</html> - - - - - - - #000000 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6e380d1943a6be970d2ffe25baaa9b00 - - - 318 - 326 - - - #C1F780 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6e3ba69443a6be970d2ffe2557b43407 - - - - #000000 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6e3ba69443a6be970d2ffe25f3986e24 - - - 325 - 332 - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6e9111d2c0a80026616d9239e83b633f - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6e9111d3c0a80026616d923930b32673 - - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6e9407e3c0a80026616d9239a5640863 - - - - #404040 - #000000 - -plain-12 - http://vue.tufts.edu/rdf/resource/6e8fd854c0a80026616d9239752cb6ef - <html> - <head color="#000000" style="color: #000000"> - <style type="text/css"> - <!-- - body { margin-top: 0px; margin-bottom: 0px; margin-left: 0px; margin-right: 0px; font-size: 13; font-family: Arial; color: #000000 } - ol { margin-top: 6; font-family: Arial; vertical-align: middle; margin-left: 30; font-size: 13; list-style-position: outside } - p { margin-top: 0; margin-left: 0; margin-right: 0; margin-bottom: 0; color: #000000 } - ul { margin-top: 6; font-size: 13; margin-left: 30; vertical-align: middle; list-style-position: outside; font-family: Arial } - --> - </style> - - </head> - <body> - <p color="#000000" style="color: #000000"> - <font style="font-size:12;" face="DejaVu Sans Mono">(define-syntax/parse - (define-graph-contract (name g-descriptor arg &#8230;) . body) </font> - </p> - <p color="#000000" style="color: #000000"> - <font style="font-size:12;" face="DejaVu Sans Mono">#'(define-syntax - name </font> - </p> - <p color="#000000" style="color: #000000"> - <font style="font-size:12;" face="DejaVu Sans Mono">(graph-contract </font> - </p> - <p color="#000000" style="color: #000000"> - <font style="font-size:12;" face="DejaVu Sans Mono">(&#955; (g-descriptor arg - &#8230;) . body)))) </font> - </p> - <p color="#000000" style="color: #000000"> - - </p> - </body> -</html> - - - - - - - #000000 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6e9111d4c0a80026616d9239034cd2a4 - - - 293 - 335 - - - #000000 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6e9111d4c0a80026616d92391e592054 - - - 328 - 335 - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6ec139a9c0a80026616d923967bf1cb6 - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6ee8e020c0a80026616d9239a263353a - - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6ee8e021c0a80026616d9239ad712d82 - - - - #404040 - #000000 - DejaVu Sans Mono-plain-12 - http://vue.tufts.edu/rdf/resource/6ee8e021c0a80026616d92391acf1941 - <html> - <head color="#000000" style="color: #000000"> - <style type="text/css"> - <!-- - body { margin-top: 0px; margin-bottom: 0px; margin-left: 0px; margin-right: 0px; font-size: 12; font-family: SansSerif; color: #000000 } - ol { margin-top: 6; font-family: SansSerif; vertical-align: middle; margin-left: 30; font-size: 12; list-style-position: outside } - p { margin-top: 0; margin-left: 0; margin-right: 0; margin-bottom: 0; color: #000000 } - ul { margin-top: 6; font-size: 12; margin-left: 30; vertical-align: middle; list-style-position: outside; font-family: SansSerif } - --> - </style> - - </head> - <body> - <p color="#000000" style="color: #000000"> - <font face="DejaVu Sans Mono">(-&gt; syntax? (listof syntax?) (values - boolean? syntax?))</font> - </p> - </body> -</html> - - - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6ee8e021c0a80026616d9239b05b1b10 - - - - #404040 - #000000 - SansSerif-plain-14 - http://vue.tufts.edu/rdf/resource/6ec139a9c0a80026616d9239a14dd476 - <html> - <head color="#000000" style="color: #000000"> - <style type="text/css"> - <!-- - body { margin-top: 0px; margin-bottom: 0px; margin-left: 0px; margin-right: 0px; font-size: 12; font-family: SansSerif; color: #000000 } - ol { margin-top: 6; font-family: SansSerif; vertical-align: middle; margin-left: 30; font-size: 12; list-style-position: outside } - p { margin-top: 0; margin-left: 0; margin-right: 0; margin-bottom: 0; color: #000000 } - ul { margin-top: 6; font-size: 12; margin-left: 30; vertical-align: middle; list-style-position: outside; font-family: SansSerif } - --> - </style> - - </head> - <body> - <p color="#000000" style="color: #000000"> - <font face="DejaVu Sans Mono">(define-syntax/parse (define-graph-wrapper - (name g-descriptor arg&#7522; &#8230;) . body) </font> - </p> - <p color="#000000" style="color: #000000"> - <font face="DejaVu Sans Mono">#'(define-syntax name </font> - </p> - <p color="#000000" style="color: #000000"> - <font face="DejaVu Sans Mono">(graph-wrapper </font> - </p> - <p color="#000000" style="color: #000000"> - <font face="DejaVu Sans Mono">(&#955; (g-descriptor arg&#7522; &#8230;) . body))))</font> - </p> - </body> -</html> - - - - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6ec139aac0a80026616d92397220832f - - - 293 - 342 - - - #8AEE95 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6f9963d1c0a80026616d92398f0f2135 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6f9963d1c0a80026616d92393e0bc6fe - - - 15 - 353 - - - #A6A6A6 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6f9963d1c0a80026616d9239f16e4b43 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6f9963d1c0a80026616d923937836369 - - - 353 - 355 - - - #8AEE95 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6fe22188c0a80026616d92392b2a40f2 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6fe22188c0a80026616d9239f2e33d1e - - - 6 - 357 - - - #8AEE95 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6fe22188c0a80026616d9239be9c047a - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6fe22189c0a80026616d9239eb7ccf81 - - - 6 - 359 - - - #FEFD8C - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6fe26c5ec0a80026616d9239fd7f5890 - - #C1F780 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6fe8bf99c0a80026616d9239dee715fd - - - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6fe26c5ec0a80026616d92393d9d5229 - - - 359 - 361 - - - #C1F780 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6fe26c5ec0a80026616d92392fbc03c6 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6fe26c5ec0a80026616d9239976c9ae7 - - - 357 - 363 - - - #FEFD8C - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6feebb15c0a80026616d923958a3c2b1 - - #FEFD8C - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6feebb15c0a80026616d9239749dd475 - - - - #FEFD8C - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6feebb15c0a80026616d9239715edb34 - - - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6feebb15c0a80026616d9239cdd2238d - - - 359 - 366 - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6feebb15c0a80026616d9239ae9362ed - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/6feebb15c0a80026616d92394b902499 - - - 359 - 370 - - - #C1F780 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/7002a307c0a80026616d9239fea067fb - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/7002a308c0a80026616d9239fd1b7118 - - - 357 - 372 - - - #C1F780 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/72463402c0a8002633539faa9129b25a - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/72463402c0a8002633539faadc8678cc - - - 363 - 376 - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/7249df95c0a8002633539faa8116b929 - - #A6A6A6 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/7249df95c0a8002633539faa04884126 - - - - #FEFD8C - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/7254d752c0a8002633539faa3f2cc14b - - - - #E6F7FD - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/725bf582c0a8002633539faa375d2f0c - - - - #E6F7FD - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/72463400c0a8002633539faa503d1c44 - - - - #E6F7FD - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/725bf582c0a8002633539faae6c01aeb - - - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/7249df95c0a8002633539faa48b8542b - - - 363 - 380 - - - #FC938D - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/725bf583c0a8002633539faa15a27783 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/725bf583c0a8002633539faa21ba73d6 - - - 382 - 387 - - - #A6A6A6 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/72668aa3c0a8002633539faafb0eb90d - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/72668aa3c0a8002633539faa97a18d9d - - - 387 - 395 - - - #8AEE95 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/72668aa3c0a8002633539faacd029888 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/72668aa3c0a8002633539faa2503ab0e - - - 6 - 397 - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/72668aa4c0a8002633539faaa932392e - - - 397 - 357 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/72668aa4c0a8002633539faa8f40befb - - - 357 - 397 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/72668aa4c0a8002633539faa3cb33fdb - - - 134 - 293 - - - - #000000 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/72668aa4c0a8002633539faa9a64a9f9 - - - 295 - 291 - - - - #000000 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/72688d2cc0a8002633539faa2223c3fb - - - 25 - 44 - - - - #000000 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/72688d2cc0a8002633539faacb736715 - - - 25 - 42 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/72688d2cc0a8002633539faad8be8121 - - - 25 - 27 - - - - #FEFD8C - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/7279521dc0a8002633539faa9926c093 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/7279521dc0a8002633539faa28480501 - - - 397 - 412 - - - #A6A6A6 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/7287a2ccc0a8002633539faa8697b9f3 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/7287a2ccc0a8002633539faa2c556ff8 - - - 395 - 414 - - - #FC938D - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/7288d8b8c0a8002633539faa3849d5b4 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/7289950ec0a8002633539faa78352364 - - - 382 - 376 - - - - #FC938D - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/734b04c1afd9d7675fea10f2925b4ae0 - - - - #E6F7FD - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/7353a85bafd9d7675fea10f24895dc43 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/7353a85bafd9d7675fea10f2505e36aa - - - 383 - 423 - - - #FC938D - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/725bf582c0a8002633539faa75b6ba0c - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/7355c611afd9d7675fea10f2464a6ef0 - - - 393 - 394 - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/735e8357afd9d7675fea10f25dfdfc46 - - - 414 - 420 - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/735e8357afd9d7675fea10f2729a7e75 - - - 414 - 416 - - - - #A6A6A6 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/73636845afd9d7675fea10f2a9ff2eca - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/73636845afd9d7675fea10f26ca61710 - - - 395 - 428 - - - - #FC938D - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/736a755dafd9d7675fea10f20c6acfd9 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/736a755dafd9d7675fea10f2f958e7ad - - - 428 - 431 - - - #A6A6A6 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/77fa5631c0a83801659a3967307a2681 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/77fa5637c0a83801659a39672e53f0db - - - 378 - 433 - - - #FC938D - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/784b6258c0a83801659a396706b41c0d - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/784b6259c0a83801659a3967a5919df0 - - - 433 - 439 - - - #C1F780 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/784b6259c0a83801659a396709970398 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/784b6259c0a83801659a39670a45e1ce - - - 363 - 443 - - - #A6A6A6 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/784b6259c0a83801659a3967733b628e - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/784b625ac0a83801659a3967666d1aa4 - - - 443 - 445 - - - #A6A6A6 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/784b625ac0a83801659a3967a167ad78 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/784b625ac0a83801659a396755702e91 - - - 443 - 447 - - - #FC938D - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/784e56c5c0a83801659a39679b10ce32 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/784e56cfc0a83801659a396764247fc5 - - - 445 - 451 - - - #A6A6A6 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/784e56cfc0a83801659a3967c532603f - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/784e56cfc0a83801659a39678a19388f - - - 447 - 455 - - - #FC938D - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/784e56d0c0a83801659a396759692c9e - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/784e56d0c0a83801659a3967b64162ba - - - 455 - 457 - - - #A6A6A6 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/7872f6c7c0a83801659a3967b9244b5d - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/7872f6c7c0a83801659a3967fb310cfc - - - 457 - 463 - - - #FEFD8C - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/787577e6c0a83801659a3967e32a4328 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/787577e7c0a83801659a39671d0d1cc7 - - - 357 - 465 - - - #FEFD8C - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/787577e7c0a83801659a3967df77be38 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/787577e7c0a83801659a39674bacedb2 - - - 465 - 467 - - - #FC938D - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/78b501a5c0a83801659a39678e8cb2cd - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/78b501a6c0a83801659a39673e57b5e0 - - - 463 - 471 - - - #A6A6A6 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/78b501a6c0a83801659a396729606ba0 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/78b501a6c0a83801659a39679b169ce5 - - - 471 - 473 - - - #A6A6A6 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/78b782c0c0a83801659a396727249705 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/78b782c1c0a83801659a3967c215e1f3 - - - 443 - 475 - - - - #A6A6A6 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/78b9713fc0a83801659a396797741710 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/78b9713fc0a83801659a39678b01ea9d - - - 443 - 478 - - - #FC938D - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/78b9713fc0a83801659a39670e4489d6 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/78b97140c0a83801659a396776a928b8 - - - 478 - 482 - - - #FC938D - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/78b97140c0a83801659a396750c3a7da - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/78b97140c0a83801659a396707564963 - - - 478 - 484 - - - #C1F780 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/78ba99b9c0a83801659a396792c09d82 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/78ba99b9c0a83801659a396789c84846 - - - 443 - 488 - - - #FC938D - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/78bd72dec0a83801659a39679db74cd5 - - - - #F4F5E9 - #776D6D - #000000 - SansSerif-plain-18 - http://vue.tufts.edu/rdf/resource/45873cde534430712734d86ab1152fe7 - - #FFC63B - #776D6D - #000000 - SansSerif-plain-16 - http://vue.tufts.edu/rdf/resource/45873cde534430712734d86a6173ded7 - - - - #FC938D - #776D6D - #000000 - SansSerif-plain-16 - http://vue.tufts.edu/rdf/resource/45873cdf534430712734d86a3f094d92 - - - - #FEFD8C - #776D6D - #000000 - SansSerif-plain-16 - http://vue.tufts.edu/rdf/resource/45873cdf534430712734d86a14e4a638 - - - - #C1F780 - #5491A4 - #000000 - SansSerif-plain-16 - http://vue.tufts.edu/rdf/resource/45873cdf534430712734d86a1e77c5e8 - - - - #E6F7FD - #776D6D - #000000 - SansSerif-plain-16 - http://vue.tufts.edu/rdf/resource/45bba55b534430712734d86a7b98e7af - - - - #A6A6A6 - #776D6D - #000000 - SansSerif-plain-16 - http://vue.tufts.edu/rdf/resource/45873cdf534430712734d86aab608348 - - - - - - #FC938D - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/45bba55c534430712734d86a16caa731 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/45bbf23d534430712734d86a4fad75b2 - - - 423 - 503 - - - #A6A6A6 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/45e66670534430712734d86a57e07278 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/45e66670534430712734d86a070392ee - - - 488 - 507 - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/45e66670534430712734d86a90157415 - - - 507 - 490 - - - #C1F780 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/45e66670534430712734d86a3a5e0161 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/45e66670534430712734d86ac0cf2c24 - - - 488 - 510 - - - #FEFD8C - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/45ec4fff534430712734d86aa07fbb12 - - - - #404040 - #404040 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/45ec4fff534430712734d86a24c87b1e - - - 510 - 512 - - - #FC938D - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/45ec4fff534430712734d86a19adbd4d - - - - #404040 - #404040 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/45ec4fff534430712734d86a0c6770e9 - - - 512 - 514 - - - #FFC63B - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/45ec4fff534430712734d86a0944806f - - - - #404040 - #404040 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/45ec4fff534430712734d86a1c61af46 - - - 514 - 517 - - - #FC938D - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/4b10aeea534430712734d86a7563260a - - - - #404040 - #404040 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/4b10aeea534430712734d86a3bbe533b - - - 512 - 519 - - - #FFC63B - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/4b10aeea534430712734d86afd00a858 - - - - #404040 - #404040 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/4b10aeea534430712734d86ae4487e0b - - - 519 - 521 - - - #FFC63B - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/4b15d0d1534430712734d86a297e96f8 - - - - #404040 - #404040 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/4b15d0d1534430712734d86ae98942d0 - - - 510 - 523 - - - #FC938D - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/4b15d0d1534430712734d86a64c609f2 - - - - #404040 - #404040 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/4b15d0d1534430712734d86ac3110955 - - - 523 - 525 - - - #FEFD8C - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/4c0c7efe534430712734d86a6143bf3b - - - - #404040 - #404040 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/4c0c7efe534430712734d86a20138645 - - - 523 - 528 - - - #404040 - #404040 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/4c0c7efe534430712734d86a22d85a28 - - - 525 - 528 - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/6dbf6b00c0a80026548592b8a0766ac6 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/4c709721534430712734d86a3c298a33 - - - 7 - 9 - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/4c7aa01c534430712734d86a674135d7 - - - 90 - 103 - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/4c7aa01c534430712734d86af85a0d62 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/4c7aa01c534430712734d86aedc8c725 - - - 103 - 535 - - - #E6F7FD - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/a46d8f60c0a801286acbb58b97c6fd0a - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/a46d8f61c0a801286acbb58b996c697e - - - 393 - 538 - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/a46d8f61c0a801286acbb58b2b628a00 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/a46d8f62c0a801286acbb58b19d6b212 - - - 353 - 540 - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/a46d8f62c0a801286acbb58beacd7655 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/a46d8f62c0a801286acbb58b90bacc82 - - - 540 - 542 - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/a68081d4c0a801286ae39894efbfa682 - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/a68081d5c0a801286ae398949e441433 - - - 357 - 544 - - - #F2AE45 - #776D6D - #000000 - SansSerif-plain-12 - http://vue.tufts.edu/rdf/resource/a68081d5c0a801286ae398942effba1f - - - - #404040 - #404040 - SansSerif-plain-11 - http://vue.tufts.edu/rdf/resource/a68081d6c0a801286ae398944c00f8fa - - - 544 - 546 - - - http://vue.tufts.edu/rdf/resource/6dbf6b15c0a80026548592b8d2f3fee2 - - 0.75 - - #FFFFFF - - - #B3993333 - #000000 - SansSerif-plain-14 - http://vue.tufts.edu/rdf/resource/6dbf6b16c0a80026548592b8204729d3 - - #000000 - #404040 - #000000 - SansSerif-plain-14 - http://vue.tufts.edu/rdf/resource/6dbf6b16c0a80026548592b817230376 - - #404040 - #FFFFFF - Gill Sans-plain-36 - http://vue.tufts.edu/rdf/resource/6dbf6b17c0a80026548592b88a8fba25 - - - - #404040 - #FFFFFF - Gill Sans-plain-22 - http://vue.tufts.edu/rdf/resource/6dbf6b17c0a80026548592b8c426a9c8 - - - - #404040 - #B3BFE3 - Gill Sans-plain-18 - http://vue.tufts.edu/rdf/resource/6dbf6b18c0a80026548592b8ea0d19d7 - - - - - - 2016-11-16 - 6 - /home/georges/phc/racket-packages/phc-graph - /home/georges/phc/racket-packages/phc-graph/Graph-notes-copy2.vue - diff --git a/LICENSE.txt b/LICENSE.txt deleted file mode 100644 index cc176a4..0000000 --- a/LICENSE.txt +++ /dev/null @@ -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. diff --git a/README.md b/README.md deleted file mode 100644 index 07f1324..0000000 --- a/README.md +++ /dev/null @@ -1,3 +0,0 @@ -phc-graph -========= -README text here. diff --git a/alpha-equivalence-normal-form.rkt b/alpha-equivalence-normal-form.rkt deleted file mode 100644 index 1a06991..0000000 --- a/alpha-equivalence-normal-form.rkt +++ /dev/null @@ -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)) \ No newline at end of file diff --git a/bench001.rkt b/bench001.rkt deleted file mode 100644 index 5e8f442..0000000 --- a/bench001.rkt +++ /dev/null @@ -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)) \ No newline at end of file diff --git a/dispatch-union.rkt b/dispatch-union.rkt deleted file mode 100644 index aac6416..0000000 --- a/dispatch-union.rkt +++ /dev/null @@ -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 …))]))) \ No newline at end of file diff --git a/features-and-implementation b/features-and-implementation deleted file mode 100644 index b29019a..0000000 --- a/features-and-implementation +++ /dev/null @@ -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). diff --git a/features-and-implementation2 b/features-and-implementation2 deleted file mode 100644 index 331ce53..0000000 --- a/features-and-implementation2 +++ /dev/null @@ -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? \ No newline at end of file diff --git a/features-and-implementation3 b/features-and-implementation3 deleted file mode 100644 index 5744da7..0000000 --- a/features-and-implementation3 +++ /dev/null @@ -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? \ No newline at end of file diff --git a/flexible-with-utils.hl.rkt b/flexible-with-utils.hl.rkt deleted file mode 100644 index aa5162d..0000000 --- a/flexible-with-utils.hl.rkt +++ /dev/null @@ -1,118 +0,0 @@ -#lang aful/unhygienic hyper-literate type-expander/lang - -@(require scribble-math) - -@title[#:tag-prefix "utils" - #:style manual-doc-style]{Utility math functions for binary tree - manipulation} - -@(chunks-toc-prefix - '("(lib phc-graph/scribblings/phc-graph-implementation.scrbl)" - "phc-graph/flexible-with" - "utils")) - -@defmodule[(lib "phc-graph/flexible-with-utils.hl.rkt")] - -@(unless-preexpanding - (require (for-label (submod "..")))) - -@chunk[<*> - (require (for-syntax racket/base)) - - (provide (for-syntax to-bits - from-bits - floor-log2 - ceiling-log2)) - - - - - - - (module* test racket/base - (require (for-template (submod ".."))) - (require rackunit) - - )] - -@defproc[(to-bits [n exact-nonnegative-integer?]) (listof boolean?)]{} - -@CHUNK[ - ; 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[ - (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[ - (define-for-syntax (from-bits b) - (foldl (λ (bᵢ acc) - (+ (* acc 2) (if bᵢ 1 0))) - 0 - b))] - -@chunk[ - (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[ - (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[ - (define-for-syntax (ceiling-log2 n) - (floor-log2 (sub1 (* n 2))))] diff --git a/flexible-with.hl.rkt b/flexible-with.hl.rkt deleted file mode 100644 index 9ca5e05..0000000 --- a/flexible-with.hl.rkt +++ /dev/null @@ -1,365 +0,0 @@ -#lang aful/unhygienic hyper-literate type-expander/lang - -@title[#:style manual-doc-style ;#:style (with-html5 manual-doc-style) - #:tag "flexible-with" - #:tag-prefix "phc-graph/flexible-with"]{Flexible functional - modification and extension of records} - -@(chunks-toc-prefix - '("(lib phc-graph/scribblings/phc-graph-implementation.scrbl)" - "phc-graph/flexible-with")) - -@section{Type of a tree-record, with a hole} - -@CHUNK[ - (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[ - (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[ - (: replace-right (∀ (A B C R) (→ (→ (Promise B) R (Promise C)) - (Promise (Pairof A B)) - R - (Promise (Pairof A C))))) - (define-pure/stateless - #:∀ (A B C R) - (replace-right [next-id : (→ (Promise B) R (Promise C))] - [tree-thunk : (Promise (Pairof A B))] - [replacement : R]) - (delay/pure/stateless - (let ([tree (force tree-thunk)]) - (let ([left-subtree (car tree)] - [right-subtree (cdr tree)]) - (cons left-subtree - (force (next-id (delay/pure/stateless right-subtree) - replacement))))))) - (: replace-left (∀ (A B C R) (→ (→ (Promise A) R (Promise C)) - (Promise (Pairof A B)) - R - (Promise (Pairof C B))))) - (define-pure/stateless - #:∀ (A B C R) - (replace-left [next-id : (→ (Promise A) R (Promise C))] - [tree-thunk : (Promise (Pairof A B))] - [replacement : R]) - (delay/pure/stateless - (let ([tree (force tree-thunk)]) - (let ([left-subtree (car tree)] - [right-subtree (cdr tree)]) - (cons (force (next-id (delay/pure/stateless left-subtree) - replacement)) - right-subtree))))) - - (define-for-syntax (define-replace-in-tree low-names names rm-names τ* i depth) - (define/with-syntax name (vector-ref names (sub1 i))) - (define/with-syntax rm-name (vector-ref rm-names (sub1 i))) - (define/with-syntax low-name (vector-ref low-names (sub1 i))) - (define/with-syntax tree-type-with-replacement-name (gensym 'tree-type-with-replacement)) - (define/with-syntax tree-replacement-type-name (gensym 'tree-replacement-type)) - (define τ*-limited (take τ* depth)) - (define τ*-limited+T-next (if (= depth 0) - (list #'T) - (append (take τ* (sub1 depth)) (list #'T)))) - #`(begin - (provide name rm-name) - (define-type (tree-type-with-replacement-name #,@τ*-limited T) - (Promise #,(tree-type-with-replacement i #'T τ*-limited))) - - (: low-name - (∀ (#,@τ*-limited T) - (→ (tree-type-with-replacement-name #,@τ*-limited Any) - T - (tree-type-with-replacement-name #,@τ*-limited T)))) - (define-pure/stateless - #:∀ (#,@τ*-limited T) - (low-name [tree-thunk : (tree-type-with-replacement-name #,@τ*-limited Any)] - [replacement : T]) - : (Promise #,(tree-type-with-replacement i #'T τ*-limited)) - #,) - - (: 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[ - (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) - - ;; 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-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[ - (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[ - (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-for-syntax (define-trees stx) - (syntax-case stx () - [(bt-fields-id (field …) [struct struct-field …] …) - (let () - - (define ∀-types (map #λ(format-id #'here "τ~a" %) - (range (add1 depth-above)))) - (define total-nb-functions (vector-length names)) - )]))] - -@CHUNK[ - (define-for-syntax (bt-fields-type fields) - (λ (stx) - (syntax-case stx () - [(_ . fs) - #`(∀ fs (Promise #,(τ-tree-with-fields #'fs - fields)))])))] - -@CHUNK[ - #`(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[ - (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) - ) - - - - - ; - - - <τ-tree-with-fields> - - - ] - -@include-section[(submod "flexible-with-utils.hl.rkt" doc)] \ No newline at end of file diff --git a/free-identifier-tree-equal.rkt b/free-identifier-tree-equal.rkt deleted file mode 100644 index 1eac8b2..0000000 --- a/free-identifier-tree-equal.rkt +++ /dev/null @@ -1,91 +0,0 @@ -#lang racket - -(require racket/struct - ;; TODO: move delay-pure/private/immutable-struct to a separate package - delay-pure/private/immutable-struct) ;; for immutable-struct? below. - -(provide free-id-tree=? - free-id-tree-hash-code - free-id-tree-secondary-hash-code - - free-id-tree-table? - immutable-free-id-tree-table? - mutable-free-id-tree-table? - weak-free-id-tree-table? - make-immutable-free-id-tree-table - make-mutable-free-id-tree-table - make-weak-free-id-tree-table) - -;; Contract: -;; TODO: move to tr-immutable -(define isyntax/c - (flat-rec-contract isyntax - (or/c boolean? - char? - number? - keyword? - null? - (and/c string? immutable?) - symbol? - (box/c isyntax #:immutable #t) - (cons/c isyntax isyntax) - (vectorof isyntax #:immutable #t) - (syntax/c isyntax) - (and/c immutable-struct? - prefab-struct-key - (λ (v) - (andmap isyntax/c (struct->list v))))))) - -(define/contract (free-id-tree=? a b [r equal?]) - (-> isyntax/c isyntax/c boolean?) - (define (rec=? a b) (free-id-tree=? a b r)) - (cond - [(identifier? a) (and (identifier? b) - (free-identifier=? a b))] - [(syntax? a) (and (syntax? b) - (rec=? (syntax-e a) - (syntax-e b)))] - [(pair? a) (and (pair? b) - (rec=? (car a) (car b)) - (rec=? (cdr a) (cdr b)))] - [(vector? a) (and (vector? b) - (rec=? (vector->list a) - (vector->list b)))] - [(box? a) (and (box? b) - (rec=? (unbox a) - (unbox b)))] - [(prefab-struct-key a) - => (λ (a-key) - (let ([b-key (prefab-struct-key b)]) - (and (equal? a-key b-key) - (rec=? (struct->list a) - (struct->list b)))))] - [(null? a) (null? b)] - [else (equal? a b)])) - -(define/contract ((free-id-tree-hash hc) a) - (-> (-> any/c fixnum?) (-> isyntax/c fixnum?)) - (define rec-hash (free-id-tree-hash hc)) - (cond - [(identifier? a) (hc (syntax-e #'a))] - [(syntax? a) (rec-hash (syntax-e a))] - [(pair? a) (hc (cons (rec-hash (car a)) - (rec-hash (cdr a))))] - [(vector? a) (hc (list->vector (map rec-hash (vector->list a))))] - [(box? a) (hc (box (rec-hash (unbox a))))] - [(prefab-struct-key a) - => (λ (a-key) - (hc (apply make-prefab-struct a-key - (rec-hash (struct->list a)))))] - [else (hc a)])) - -(define free-id-tree-hash-code - (free-id-tree-hash equal-hash-code)) -(define free-id-tree-secondary-hash-code - (free-id-tree-hash equal-secondary-hash-code)) - -(define-custom-hash-types free-id-tree-table - #:key? syntax? - free-id-tree=? - free-id-tree-hash-code - free-id-tree-secondary-hash-code) diff --git a/graph-info.hl.rkt b/graph-info.hl.rkt deleted file mode 100644 index 06f5589..0000000 --- a/graph-info.hl.rkt +++ /dev/null @@ -1,347 +0,0 @@ -#lang hyper-literate racket #:no-auto-require - -@require[scribble-math - scribble-enhanced/doc - "notations.rkt" - (for-label racket)] - -@title[#:style (with-html5 manual-doc-style) - #:tag "graph-info" - #:tag-prefix "phc-graph/graph-info"]{Compile-time graph metadata} - -@(chunks-toc-prefix - '("(lib phc-graph/scribblings/phc-graph-implementation.scrbl)" - "phc-graph/graph-info")) - -We define here the compile-time metadata describing a graph type. - -@section{Graph type information} - -The type of a graph is actually the type of its constituent nodes. The node -types may be polymorphic in the @racket[_tvars] type variables. The root node -name and the order of the nodes are purely indicative here, as a reference to -any node in the graph instance would be indistinguishable from a graph rooted -in that node type. - -The @racket[_invariants] are not enforced by the node types. Instead, the node -types just include the invariant type as a witness (inside the @racket[raw] -field). The invariant is enforced either by construction, or with a run-time -check performed during the graph creation. - -@chunk[ - (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[ - (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[ - (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[ - (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[ - (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[ - (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[ - (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[ - (struct+/contract invariant-info - ([predicate identifier?] ; (→ RootNode Boolean : +witness-type) - [witness-type stx-type/c]) - #:transparent - #:methods gen:custom-write - [(define write-proc (struct-printer 'invariant-info))] - #:property prop:custom-print-quotable 'never - #:methods gen:equal+hash - [(define (equal-proc a b r) - (free-id-tree=? (vector->immutable-vector (struct->vector a)) - (vector->immutable-vector (struct->vector b)))) - (define (hash-proc a r) - (free-id-tree-hash-code - (vector->immutable-vector (struct->vector a)))) - (define (hash2-proc a r) - (free-id-tree-secondary-hash-code - (vector->immutable-vector (struct->vector a))))])] - -@section{Dependent invariant information} - -The invariants described in the previous section assert properties of a graph -instance in isolation. It is however desirable to also describe invariants -which relate the old and the new graph in a graph transformation. - -@chunk[ - (struct+/contract dependent-invariant-info - ([checker identifier?] ; (→ RootMappingArguments… NewGraphRoot Boolean) - [name identifier?]) - #:transparent - #:methods gen:custom-write - [(define write-proc (struct-printer 'dependent-invariant-info))] - #:property prop:custom-print-quotable 'never - #:methods gen:equal+hash - [(define (equal-proc a b r) - (free-id-tree=? (vector->immutable-vector (struct->vector a)) - (vector->immutable-vector (struct->vector b)))) - (define (hash-proc a r) - (free-id-tree-hash-code - (vector->immutable-vector (struct->vector a)))) - (define (hash2-proc a r) - (free-id-tree-secondary-hash-code - (vector->immutable-vector (struct->vector a))))])] - -@section{Mapping information} - -@chunk[ - (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{# - (define (to-datum v) - (syntax->datum (datum->syntax #f v))) - - (define ((syntax-convert old-print-convert-hook) - val basic-convert sub-convert) - (cond - [(set? val) - (cons 'set (map sub-convert (set->list val)))] - [(and (hash? val) (immutable? val)) - (cons 'hash - (append-map (λ (p) (list (sub-convert (car p)) - (sub-convert (cdr p)))) - (hash->list val)))] - [(syntax? val) - (list 'syntax (to-datum val))] - [else - (old-print-convert-hook val basic-convert sub-convert)])) - - (define ((struct-printer ctor) st port mode) - (match-define (vector name fields ...) (struct->vector st)) - (define-values (info skipped?) (struct-info st)) - (define-values (-short-name _2 _3 _4 _5 _6 _7 _8) - (struct-type-info info)) - (define short-name (or ctor -short-name)) - (define (to-datum v) - (syntax->datum (datum->syntax #f v))) - (case mode - [(#t) - (display "#(" port) - (display name port) - (for-each (λ (f) - (display " " port) - (write (to-datum f) port)) - fields) - (display ")" port)] - [(#f) - (display "#(" port) - (display name port) - (for-each (λ (f) - (display " " port) - (display (to-datum f) port)) - fields) - (display ")" port)] - [else - (let ([old-print-convert-hook (current-print-convert-hook)]) - (parameterize ([constructor-style-printing #t] - [show-sharing #f] - [current-print-convert-hook - (syntax-convert old-print-convert-hook)]) - (write - (cons short-name - (map print-convert - ;; to-datum doesn't work if I map it on the fields? - fields)) - port)))]))] - -@CHUNK[<*> - (require phc-toolkit/untyped - type-expander/expander - racket/struct - mzlib/pconvert - "free-identifier-tree-equal.rkt" - (for-syntax phc-toolkit/untyped - syntax/parse - syntax/parse/experimental/template - racket/syntax)) - - (define-syntax/parse - (struct+/contract name {~optional parent} - {~optional ([parent-field parent-contract] ...)} - ([field contract] ...) - {~optional {~and transparent #:transparent}} - (~and {~seq methods+props ...} - (~seq (~or {~seq #:methods _ _} - {~seq #:property _ _}) - ...))) - #:with name/c (format-id #'name "~a/c" #'name) - ;(quasisyntax/loc (stx-car this-syntax) - ; #, - (template - (begin - (struct name (?? parent) (field ...) - (?? transparent) - methods+props ...) - (define name/c - (struct/c name - (?? (?@ parent-contract ...)) - contract ...)) - (module+ test - (require rackunit) - (check-pred flat-contract? name/c)) - (provide name/c - (contract-out (struct (?? (name parent) name) - ((?? (?@ [parent-field parent-contract] - ...)) - [field contract] - ...))))))) - - ; - - - - - - - - - ] diff --git a/graph-type.hl.rkt b/graph-type.hl.rkt deleted file mode 100644 index d10cf26..0000000 --- a/graph-type.hl.rkt +++ /dev/null @@ -1,144 +0,0 @@ -#lang aful/unhygienic hyper-literate typed/racket #:no-auto-require - -@require[scribble-math - scribble-enhanced/doc - "notations.rkt" - (for-label racket)] - -@title[#:style (with-html5 manual-doc-style) - #:tag "graph-type" - #:tag-prefix "phc-graph/graph-type"]{Declaring graph types} - -@(chunks-toc-prefix - '("(lib phc-graph/scribblings/phc-graph-implementation.scrbl)" - "phc-graph/graph-type")) - -The @racket[define-graph-type] form binds @racket[name] to a -@racket[graph-info] struct. The @racket[name] therefore contains metadata -describing among other things the types of nodes, the invariants that -instances of this graph type will satisfy. - -@chunk[ - (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[ - (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 - - (define-syntax name - (build-graph-info (quote-syntax whole)))))] - -@section{Declaring the node types} - -@chunk[ - (define-type nodeᵢ - (Promise - ((!check-remembered-node! nodeᵢ fieldᵢⱼ …) τᵢⱼ … - 'Database - 'Index))) - …] - -@section{Creating the @racket[graph-info] instance} - -@CHUNK[ - (define-for-syntax (build-graph-info stx) - (parameterize ([disable-remember-immediate-error #t]) - (syntax-parse stx - [:signature - ])))] - -@chunk[ - (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ᵢ node-incompleteᵢ - [fieldᵢⱼ τᵢⱼ] …] …)))) - (list->set - (append - (stx-map (λ/syntax-case (op a b) () ) - #'([op a b] …)) - (stx-map (λ/syntax-case p () ) - #'(p …)))))] - -@chunk[ - (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ᵢⱼ τᵢⱼ] …)))) - #'nodeᵢ ; promise type - #;(meta-struct-constructor - (check-remembered-tagged! #'(node-incompleteᵢ fieldᵢⱼ …))) - #;(check-remembered-tagged! #'(node-incompleteᵢ fieldᵢⱼ …)))] - -@chunk[ - (field-info #'τᵢⱼ)] - -@chunk[ - (invariant-info #'predicateTODO - #'witnessTODO)] - -@chunk[ - (invariant-info #'predicateTODO - #'witnessTODO)] - -@section{Putting it all together} - -@chunk[<*> - (require racket/require - phc-toolkit - remember - (lib "phc-adt/tagged-structure-low-level.hl.rkt") - (for-syntax "graph-info.hl.rkt" - type-expander/expander - phc-toolkit/untyped - (subtract-in syntax/parse phc-graph/subtemplate) - racket/set - phc-graph/subtemplate-override - racket/syntax - extensible-parser-specifications - backport-template-pr1514/experimental/template) - (for-meta 2 racket/base)) - - (provide define-graph-type) - - - - ] \ No newline at end of file diff --git a/graph.hl.rkt b/graph.hl.rkt deleted file mode 100644 index 649deb7..0000000 --- a/graph.hl.rkt +++ /dev/null @@ -1,119 +0,0 @@ -#lang hyper-literate typed/racket/base #:no-auto-require -@(require scribble-math - racket/require - scribble-enhanced/doc - racket/require - hyper-literate - (subtract-in scribble/struct scribble-enhanced/doc) - scribble/decode - (for-label racket/format - racket/promise - racket/list - type-expander - (except-in (subtract-in typed/racket/base type-expander) - values) - (only-in racket/base values) - (subtract-in racket/contract typed/racket/base) - phc-toolkit - phc-toolkit/untyped-only - remember)) -@(unless-preexpanding - (require (for-label (submod "..")))) -@doc-lib-setup - -@title[#:style (with-html5 manual-doc-style) - #:tag "graph-impl" - #:tag-prefix "phc-graph/graph-impl"]{Implementation of the graph macro} - -@(chunks-toc-prefix - '("(lib phc-graph/scribblings/phc-graph-implementation.scrbl)" - "phc-graph/graph-impl")) - - -@chunk[ - (define-syntax define-graph - (syntax-parser - [ - ]))] - -@chunk[ - (_ _name - [[_nodeᵢ [_fieldᵢⱼ :colon _τᵢⱼ] …] …] - [[(_mappingₖ [_argₖₗ _τₖₗ] …) :colon _return-typeₖ . _bodyₖ] …])] - -@chunk[ - #'()] - -@section{Overview of the implementation (draft)} - -@chunk[ - - - - ] - -@chunk[ - (define/with-syntax (_indexₖ …) (stx-map gensym #'(_idxₖ …))) - #'(begin - (define-type _indexₖ (graph-index '_indexₖ)) - …)] - -@chunk[ - (struct (K) graph-index ([key : K] [index : Index]))] - -Create one queue @racket[_Qₖ] for each mapping: - -@chunk[ - #'(begin - (define _Qₖ ) - (define _Qₖ-enqueue ) - (define _Qₖ-pop ) - …)] - -Re-bind mappings to catch outbound calls: - -@chunk[ - #'(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[ - #'(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[ - #'(define (entry-point #:mappingₖ [_argsₖ* : (Listof (List τₖₗ …)) '()]) - (for ([_argsₖ (in-list _argsₖ*)]) - (let-values ([(_argₖₗ …) _argsₖ]) - (Qₖ-enqueue _argₖₗ …))))] - -@chunk[ - (until queues are all empty - process item, see below)] - -@itemlist[ - @item{Find and replace references to old nodes and new incomplete nodes and - new placeholder nodes, instead insert indices.} - @item{Problem: we need to actually insert indices for references to nodes, - not for references to mappings (those have to be inlined).}] - - -@chunk[<*> - (require racket/require - (for-syntax (subtract-in (combine-in racket/base - syntax/parse) - "subtemplate-override.rkt") - phc-toolkit/untyped - type-expander/expander - "subtemplate-override.rkt") - "traversal.hl.rkt" - phc-toolkit) - - ] \ No newline at end of file diff --git a/info.rkt b/info.rkt deleted file mode 100644 index a7b836e..0000000 --- a/info.rkt +++ /dev/null @@ -1,32 +0,0 @@ -#lang info -(define collection "phc-graph") -(define deps '("base" - "rackunit-lib" - "phc-toolkit" - "phc-adt" - "type-expander" - "hyper-literate" - "scribble-enhanced" - "typed-racket-lib" - "srfi-lite-lib" - "delay-pure" - "backport-template-pr1514" - "typed-map" - "scribble-lib" - "pconvert-lib" - "remember" - "extensible-parser-specifications")) -(define build-deps '("scribble-lib" - "racket-doc" - "remember" - "typed-racket-doc" - "aful" - "scribble-math")) -(define scribblings - '(("scribblings/phc-graph.scrbl" () - ("Data Structures")) - ("scribblings/phc-graph-implementation.scrbl" (multi-page) - ("Data Structures")))) -(define pkg-desc "Description Here") -(define version "0.0") -(define pkg-authors '("Georges Dupéron")) diff --git a/invariants-phantom.hl.rkt b/invariants-phantom.hl.rkt deleted file mode 100644 index 9c2a84b..0000000 --- a/invariants-phantom.hl.rkt +++ /dev/null @@ -1,483 +0,0 @@ -#lang aful/unhygienic hyper-literate type-expander/lang - -@require[scribble-math - scribble-enhanced/doc - "notations.rkt"] - -@title[#:style (with-html5 manual-doc-style) - #:tag "inv-phantom" - #:tag-prefix "phc-graph/inv-phantom"]{Tracking checked contracts - via refinement types} - -@(chunks-toc-prefix - '("(lib phc-graph/scribblings/phc-graph-implementation.scrbl)" - "phc-graph/inv-phantom")) - -@section{Introduction} - -The cautious compiler writer will no doubt want to check that the graph used -to represent the program verifies some structural properties. For example, the -compiled language might not allow cycles between types. Another desirable -property is that the @racket[in-method] field of an instruction points back to -the method containing it. We will use this second property as a running -example in this section. - -@section{Implementation overview : subtyping, variance and phantom types} - -It is possible to express with Typed/Racket that a @racket[Method] should -contain a list of @racket[Instruction]s, and that @racket[Instruction]s should -point to a @racket[Method]@note{We are not concerned here about the ability to - create such values, which necessarily contain some form of cycle. The goal of - the graph library is indeed to handle the creation and traversal of such - cyclic data structures in a safe way}: - -@chunk[ - (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[ - (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[ - (λ ([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[ - (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[ - (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[ - (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[ - (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[ - (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[ - (define-type At-Least-InvB+InvD - (→ (U 'InvB 'InvD) Void))] - -In the case where no invariant is present in the untagged union, the type -@racket[(U)] a.k.a @racket[Nothing], the bottom type with no value, would -appear. This type is somewhat pathological and allows absurd reasoning (a -function accepting @racket[Nothing] can never be called, which may incite the -type checker to perform excessive elision). To avoid any pitfalls, we will -systematically include a dummy element @racket[Or] in the union, to make sure -the union never becomes empty. - -This solution also has the advantage that the size of the run-time witness is -constant, and does not depend on the number of checked contracts (unlike the -representation using a list). In practice the function should never be called. -It can however simply be implemented in a way which pleases the type checked -as a function accepting anything and returning void. - -In addition to testifying that a graph node was checked against multiple, -separate contracts, there might be some contracts which check stronger -properties than others. A way to encode this relationship in the type system -is to have subtyping relationships between the contract witnesses, so that -@; TODO: get rid of the textit -@${\textit{P}₁(x) ⇒ \textit{P}₂(x) ⇒ \textit{Inv}₁ @texsubtype \textit{Inv}₂}: - -@chunk[ - (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[ - (struct InvStrongContra ()) - (struct InvWeakContra InvStrongContra ())] - -Alternatively, it is possible to use a second contravariant position to -reverse the subtyping relationship again: - -@chunk[ - (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[ - (code:comment "Draft ideas") - - (struct ∈ ()) - (struct ≡ ()) - (struct ∉ ()) - - ;(List Rel From Path1 Path2) - (List ≡ ANodeName (List f1 f2) (List)) - (List ∈ ANodeName (List f1 f2) (List)) - (List ∉ ANodeName (List f1 f2) (List)) - (List ∉ ANodeName (List (* f1 f2 f3 f4) (* f5 f6)) (List)) - - ;(List From Path+Rel) - (List ANodeName (List f1 f2 ≡)) - (List ANodeName (List f1 f2 ∈)) - (List ANodeName (List f1 f2 ∉)) - (List ANodeName (List (List f1 ∉) - (List f2 ∉) - (List f3 ∉) - (List f4 - (List f5 ∉) - (List f6 ∉)))) - - ;; How to make it have the right kind of subtyping? - - - ] - -@subsection{Properties applying to all reachable nodes from @racket[x]} - -The property @racket[x ≢ x.**] can be expanded to a series of properties. For -example, if @racket[x] has two fields @racket[a] and @racket[d], the former -itself having two fields @racket[b] and @racket[c], and the latter having a -field @racket[e], itself with a field @racket[f]: -@chunk[ - (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[ - (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[ - ((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 (→ Any Void)) - (define witness-value (λ (x) (void)))] - -@subsection{Grouping multiple invariants} - -As mentioned earlier, we group invariants together using an untagged union -@racket[U], which must appear in a contravariant position. We wish to express -witnesses for stronger invariants as subtypes of witnesses for weaker -invariants, and therefore use a second nested function type to flip again the -variance direction. We always include the Or element in the union, to avoid -having an empty union. - -@chunk[ - (struct Or ()) - (define-type-expander (Invariants stx) - (syntax-case stx () - [(_ invᵢ …) - #'(→ (U Or (→ invᵢ Void) …) Void) - #;#'(→ (→ (∩ invᵢ …) Void) Void)]))] - -@subsection{Structural (in)equality and (non-)membership invariants} - -@subsubsection{Comparison operator tokens} - -We define some tokens which will be used to identify the operator which -relates two nodes in the graph. - -@chunk[ - (struct (A) inv≡ ([a : A])) - (struct (A) inv≢ ([a : A])) - ;(struct inv∈ ()) ;; Can be expressed in terms of ≡ - ;(struct inv∉ ()) ;; Can be expressed in terms of ≢ - ] - -@CHUNK[<≡> - (define-for-syntax (relation inv) - (syntax-parser - [(_ (pre-a … {~literal _} post-a …) - (pre-b … {~literal _} post-b …)) - #:with (r-pre-a …) (reverse (syntax->list #'(pre-a …))) - #:with (r-pre-b …) (reverse (syntax->list #'(pre-b …))) - ;; Use U to make it order-independent - #`(#,inv (U (Pairof (Cycle r-pre-a …) - (Cycle post-a …)) - (Pairof (Cycle r-pre-b …) - (Cycle post-b …))))])) - - (define-type-expander ≡ (relation #'inv≡)) - (define-type-expander ≢ (relation #'inv≢))] - -@chunk[ - (struct ε () #:transparent) - (struct (T) Target () #:transparent) - (struct (T) NonTarget Target ([x : T]) #:transparent) - - (define-type-expander Cycle - (syntax-parser - [(_ field:id … {~literal ↙} loop1:id … (target:id) loop2:id …) - #'(List* (NonTarget ε) - (NonTarget 'field) … - (Rec R (List* (NonTarget 'loop1) … ;(NonTarget 'loop1) … - (Target 'target) ;(NonTarget 'target) - (NonTarget 'loop2) … ;(NonTarget 'loop2) … - R)))] - [(_ field … target) - ;; TODO: something special at the end? - #'(List (NonTarget ε) (NonTarget 'field) … (Target 'target))] - [(_) - #'(List (Target ε))]))] - -@;{@[ - - ;.a.b = .x.y - ;(l1=a ∧ l2=b ∧ r1=x ∧ r2=y) ⇒ eq - ;¬(l1=a ∧ l2=b ∧ r1=x ∧ r2=y) ∨ eq - ;¬l1=a ∨ ¬l2=b ∨ ¬r1=x ∨ ¬r2=y ∨ eq - - ;.a.c = .x.y - ;(l1=a ∧ l2=c ∧ r1=x ∧ r2=y) ⇒ eq - - ;.a.c = .x.z - ;(l1=a ∧ l2=b ∧ r1=x ∧ r2=z) ⇒ eq - ;¬l1=a ∨ ¬l2=b ∨ ¬r1=x ∨ ¬r2=z ∨ eq - - - ;.a.b = .x.y ∧ .a.c = .x.z - ;(¬l1=a ∨ ¬l2=b ∨ ¬r1=x ∨ ¬r2=y ∨ eq) ∧ (¬l1=a ∨ ¬l2=b ∨ ¬r1=x ∨ ¬r2=z ∨ eq) - ;¬¬(¬l1=a ∨ ¬l2=b ∨ ¬r1=x ∨ ¬r2=y ∨ eq) ∧ (¬l1=a ∨ ¬l2=b ∨ ¬r1=x ∨ ¬r2=z ∨ eq) - ;¬(l1=a ∧ l2=b ∧ r1=x ∧ r2=y ∧ eq) ∨ (l1=a ∧ l2=b ∧ r1=x ∧ r2=z ∧ ¬eq) - ]} - -@; Problem with ∩: it factors out too much, (∩ '(a . b) '(a . c) '(x . b)) -@; becomes (Pairof (∩ 'a 'x) (∩ 'b 'c)), which is equivalent to have all four -@; elements of {a,x} × {b,c}, but we only want three out of these four. - -Two sorts of paths inside (in)equality constraints: - -@itemlist[ - @item{those anchored on a node, stating that - @$${ - ∀\ \textit{node} : \textit{NodeType},\quad - \textit{node}.\textit{path}₁ ≡ \textit{node}.\textit{path}₂}} - @item{those not anchored on a node, stating that - @$${ - \begin{array}{c} - ∀\ \textit{node}₁ : \textit{NodeType}₁,\quad - ∀\ \textit{node}₂ : \textit{NodeType}₂,\\ - \textit{node}₁.\textit{path}₁ ≡ \textit{node}₂.\textit{path}₂ - \end{array}}}] - -@subsection{Putting it all together} - -@chunk[ - (define-syntax (check-a-stronger-or-same-b stx) - (syntax-case stx () - [(_ stronger weaker) - (syntax/top-loc stx - (check-ann (ann witness-value stronger) - weaker))])) - - (define-syntax (check-a-same-b stx) - (syntax-case stx () - [(_ a b) - (syntax/top-loc stx - (begin - (check-ann (ann witness-value a) b) - (check-ann (ann witness-value b) a)))]))] - -@chunk[<*> - (require (for-syntax phc-toolkit/untyped - syntax/parse)) - - - - - - <≡> - - (module+ test - (require phc-toolkit) - - - (ann witness-value (Invariants)) ;; No invariants - (ann witness-value (Invariants (≡ (_ a) (_ a b c)))) - - (check-a-stronger-or-same-b (Invariants (≡ (_ a) (_ a b c))) - (Invariants)) - - (check-a-same-b (Invariants (≡ (_ a) (_ a b c))) - (Invariants (≡ (_ a b c) (_ a)))) - - (check-a-stronger-or-same-b (Invariants (≡ (_) (_ b c)) - (≡ (_) (_ b d))) - (Invariants (≡ (_) (_ b c)))) - (check-a-stronger-or-same-b (Invariants (≡ (_) (_ b d)) - (≡ (_) (_ b c))) - (Invariants (≡ (_) (_ b c)))) - - (check-a-stronger-or-same-b (Invariants (≡ (_) - (_ b d a b d ↙ a b (d)))) - (Invariants (≡ (_) - (_ b d ↙ a b (d))))))] diff --git a/main.rkt b/main.rkt deleted file mode 100644 index 216dcac..0000000 --- a/main.rkt +++ /dev/null @@ -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 <> -;; To uninstall: -;; $ raco pkg remove <> -;; To view documentation: -;; $ raco docs <> -;; -;; 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. - ) diff --git a/notations.rkt b/notations.rkt deleted file mode 100644 index e82ddf5..0000000 --- a/notations.rkt +++ /dev/null @@ -1,7 +0,0 @@ -#lang racket - -(require scribble/base) - -(provide texsubtype) - -(define texsubtype "<:") \ No newline at end of file diff --git a/scribblings/phc-graph-implementation.scrbl b/scribblings/phc-graph-implementation.scrbl deleted file mode 100644 index 6c32fec..0000000 --- a/scribblings/phc-graph-implementation.scrbl +++ /dev/null @@ -1,19 +0,0 @@ -#lang scribble/manual -@require[@for-label[phc-graph - racket/base]] - -@title{Ph.C Graph library: Implementation} -@author[@author+email["Georges Dupéron" "georges.duperon@gmail.com"]] - -This library is implemented using literate programming. The implementation -details are presented in the following sections. The user documentation is in -the @other-doc['(lib "phc-graph/scribblings/phc-graph.scrbl")] document. - -@(table-of-contents) - -@include-section[(submod "../traversal.hl.rkt" doc)] -@include-section[(submod "../flexible-with.hl.rkt" doc)] -@include-section[(submod "../invariants-phantom.hl.rkt" doc)] -@include-section[(submod "../graph-info.hl.rkt" doc)] -@include-section[(submod "../graph-type.hl.rkt" doc)] -@include-section[(submod "../graph.hl.rkt" doc)] \ No newline at end of file diff --git a/scribblings/phc-graph.scrbl b/scribblings/phc-graph.scrbl deleted file mode 100644 index efaac71..0000000 --- a/scribblings/phc-graph.scrbl +++ /dev/null @@ -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 diff --git a/test/adt-pre-declarations.rkt b/test/adt-pre-declarations.rkt deleted file mode 100644 index 2ec4282..0000000 --- a/test/adt-pre-declarations.rkt +++ /dev/null @@ -1,17 +0,0 @@ -#lang s-exp phc-adt/declarations -(remembered! tagged-structure (tg a b)) -(remembered! tagged-structure (tg a c)) -(remembered! tagged-structure (t0)) -(remembered! tagged-structure (City citizens name streets)) -(remembered! tagged-structure (Street houses name)) -(remembered! tagged-structure (House owner)) -(remembered! tagged-structure (Person name)) -(remembered! tagged-structure (node-incompleteᵢ citizens name streets)) -(remembered! tagged-structure (node-incompleteᵢ houses name)) -(remembered! tagged-structure (node-incompleteᵢ owner)) -(remembered! tagged-structure (node-incompleteᵢ name)) -(remembered! tagged-structure (| City-incomplete| citizens name streets)) -(remembered! tagged-structure (| Street-incomplete| houses name)) -(remembered! tagged-structure (| House-incomplete| owner)) -(remembered! tagged-structure (| Person-incomplete| name)) -(remembered! tagged-structure (City name)) diff --git a/test/assumption-equivalent-types-same-type.rkt b/test/assumption-equivalent-types-same-type.rkt deleted file mode 100644 index ce299be..0000000 --- a/test/assumption-equivalent-types-same-type.rkt +++ /dev/null @@ -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)) \ No newline at end of file diff --git a/test/ck.rkt b/test/ck.rkt deleted file mode 100644 index dc7bb7d..0000000 --- a/test/ck.rkt +++ /dev/null @@ -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 ...)))])) - \ No newline at end of file diff --git a/test/invariant-phantom-tr-assumptions.rkt b/test/invariant-phantom-tr-assumptions.rkt deleted file mode 100644 index d0d8287..0000000 --- a/test/invariant-phantom-tr-assumptions.rkt +++ /dev/null @@ -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)) \ No newline at end of file diff --git a/test/invariant-phantom-tr-assumptions2.rkt b/test/invariant-phantom-tr-assumptions2.rkt deleted file mode 100644 index 5a8d850..0000000 --- a/test/invariant-phantom-tr-assumptions2.rkt +++ /dev/null @@ -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)) \ No newline at end of file diff --git a/test/test-flexible-with.rkt b/test/test-flexible-with.rkt deleted file mode 100644 index c4ab572..0000000 --- a/test/test-flexible-with.rkt +++ /dev/null @@ -1,79 +0,0 @@ -#lang aful/unhygienic type-expander/lang - -(require (lib "phc-graph/flexible-with.hl.rkt") - (for-syntax racket/syntax - racket/list - (rename-in racket/base [... …])) - phc-toolkit - typed-map - type-expander) - -(define-syntax (gs stx) - (syntax-case stx () - [(_ bt-fields-id nfields (f …) [struct struct-field …] …) - (let () - (define/with-syntax (field …) - (append (syntax->list #'(f …)) - (map (λ (_) (datum->syntax #'nfields (gensym 'g))) - (range (- (syntax-e #'nfields) - (length (syntax->list #'(f …)))))))) - (define-trees #'(bt-fields-id - (field …) - [struct struct-field …] …)))])) - -(gs bt-fields - 16 - (a b c) - [sab a b] - [sbc b c] - [sabc a b c]) - -(define-type btac (bt-fields a c)) - -(check-equal?: - (~> (ann (with-c (sab→tree 1 2) 'nine) - ((bt-fields a b c) One Positive-Byte 'nine)) - force - flatten - (filter Some? _) - (map Some-v _) - list->set) - (set 1 2 'nine)) - - -(check-equal?: - (call-with-values - #λ(tree→sab (sab→tree 1 2)) - list) - '(1 2)) - -(check-equal?: - (call-with-values - #λ(tree→sabc (ann (with-c (sab→tree 1 2) 'nine) - ((bt-fields a b c) One Positive-Byte 'nine))) - list) - '(1 2 nine)) - -(check-equal?: - (call-with-values - #λ(tree→sabc (with-c (sab→tree 'NONE 'NONE) 'NONE)) - list) - '(NONE NONE NONE)) - -(check-equal?: - (call-with-values - #λ(tree→sab (without-c (with-c (sab→tree 'NONE 'NONE) 'NONE))) - list) - '(NONE NONE)) - -(check-equal?: - (call-with-values - #λ(tree→sbc (without-a (with-c (sab→tree 'NONE 'NONE) 'NONE))) - list) - '(NONE NONE)) - -(check-equal?: - (call-with-values - #λ(tree→sbc (without-a (with-c (sab→tree 1 2) 3))) - list) - '(2 3)) \ No newline at end of file diff --git a/test/test-graph-type.rkt b/test/test-graph-type.rkt deleted file mode 100644 index 9416977..0000000 --- a/test/test-graph-type.rkt +++ /dev/null @@ -1,39 +0,0 @@ -#lang typed/racket - -(require phc-adt - (lib "phc-graph/graph-type.hl.rkt")) -(adt-init) - -(provide g1) - -(define-graph-type g1 - [City [name : String] - [streets : (Listof Street)] - [citizens : (Listof Person)]] - [Street [name : String] - [houses : (Listof House)]] - [House [owner : Person]] - [Person [name : String]] - #:invariant City.citizens._ ∈ City.streets._.houses._.owner - #:invariant City.citizens._ ∋ City.streets._.houses._.owner) - -(require (for-syntax racket/pretty - racket/base)) -(eval #'(begin - (define-syntax (dbg _stx) - (parameterize ([pretty-print-columns 188]) - (pretty-print (syntax-local-value #'g1))) - #'(void)) - (dbg))) - -(require (for-syntax syntax/parse - "../graph-info.hl.rkt")) - -(define-syntax dbg - (syntax-parser - [(_ t) - #`(define-type t - #,(node-info-promise-type - (hash-ref (graph-info-nodes (syntax-local-value #'g1)) 'City)))])) -(dbg t-city) -;(define-type expected (t-city Number String Symbol 'Database 'Index)) \ No newline at end of file diff --git a/test/test-traversal-1.rkt b/test/test-traversal-1.rkt deleted file mode 100644 index 54af2d9..0000000 --- a/test/test-traversal-1.rkt +++ /dev/null @@ -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) diff --git a/test/test-traversal-2.rkt b/test/test-traversal-2.rkt deleted file mode 100644 index d990c25..0000000 --- a/test/test-traversal-2.rkt +++ /dev/null @@ -1,114 +0,0 @@ -#lang typed/racket - -(require "traversal-util.rkt" - type-expander - phc-adt - "ck.rkt" - "../dispatch-union.rkt") ;; DEBUG -(adt-init) - -(define-fold f₁ t₁ (tagged tg [a String] [b Boolean]) String) -(define-fold f₂ t₂ (U (tagged tg [a String] [b Boolean])) String) -(define-fold f₃ t₃ (U (tagged tg [a String] [b Boolean]) - (tagged tg [a Boolean] [c String])) - String) -(define-fold f₄ t₄ (U (tagged tg [a String] [b Boolean]) - String - (tagged tg [a Boolean] [c String])) - String) -(define-fold f₅ t₅ (U (tagged t0) - String - (tagged tg [a Boolean] [c String])) - String) -(define-fold f₆ t₆ (U String - (tagged tg [a String] [b Boolean])) - String) - -(define (string->symbol+acc [x : String] [acc : Integer]) - (values (string->symbol x) (add1 acc))) - -(check-equal?-values: - ((f₁ string? string->symbol+acc) (tagged tg [a "abc"] [b #f]) 0) - : (Values (tagged tg [a Symbol] [b Boolean]) Integer) - (tagged tg [a 'abc] [b #f]) 1) - -(check-equal?-values: - ((f₂ string? string->symbol+acc) (tagged tg [a "abc"] [b #f]) 0) - : (Values (U (tagged tg [a Symbol] [b Boolean])) Integer) - (tagged tg [a 'abc] [b #f]) 1) - -(check-equal?-values: - ((f₃ string? string->symbol+acc) (tagged tg [a "abc"] [b #f]) 0) - : (Values (U (tagged tg [a Symbol] [b Boolean]) - (tagged tg [a Boolean] [c Symbol])) - Integer) - (tagged tg [a 'abc] [b #f]) 1) - -(check-equal?-values: - ((f₃ string? string->symbol+acc) (tagged tg [a #t] [c "def"]) 0) - : (Values (U (tagged tg [a Symbol] [b Boolean]) - (tagged tg [a Boolean] [c Symbol])) - Integer) - (tagged tg [a #t] [c 'def]) 1) - -(check-equal?-values: - ((f₄ string? string->symbol+acc) (tagged tg [a "abc"] [b #f]) 0) - : (Values (U (tagged tg [a Symbol] [b Boolean]) - Symbol - (tagged tg [a Boolean] [c Symbol])) - Integer) - (tagged tg [a 'abc] [b #f]) 1) - -(check-equal?-values: - ((f₄ string? string->symbol+acc) "ghi" 0) - : (Values (U (tagged tg [a Symbol] [b Boolean]) - Symbol - (tagged tg [a Boolean] [c Symbol])) - Integer) - 'ghi 1) - -(check-equal?-values: - ((f₄ string? string->symbol+acc) (tagged tg [a #t] [c "def"]) 0) - : (Values (U (tagged tg [a Symbol] [b Boolean]) - Symbol - (tagged tg [a Boolean] [c Symbol])) - Integer) - (tagged tg [a #t] [c 'def]) 1) - -(check-equal?-values: - ((f₅ string? string->symbol+acc) (tagged t0 #:instance) 0) - : (Values (U (tagged t0) - Symbol - (tagged tg [a Boolean] [c Symbol])) - Integer) - (tagged t0 #:instance) 0) - -(check-equal?-values: - ((f₅ string? string->symbol+acc) "ghi" 0) - : (Values (U (tagged t0) - Symbol - (tagged tg [a Boolean] [c Symbol])) - Integer) - 'ghi 1) - -(check-equal?-values: - ((f₅ string? string->symbol+acc) (tagged tg [a #t] [c "def"]) 0) - : (Values (U (tagged t0) - Symbol - (tagged tg [a Boolean] [c Symbol])) - Integer) - (tagged tg [a #t] [c 'def]) 1) - -(check-equal?-values: - ((f₆ string? string->symbol+acc) (tagged tg [a "abc"] [b #f]) 0) - : (Values (U (tagged tg [a Symbol] [b Boolean]) - Symbol) - Integer) - (tagged tg [a 'abc] [b #f]) 1) - -(check-equal?-values: - ((f₆ string? string->symbol+acc) "ghi" 0) - : (Values (U (tagged tg [a Symbol] [b Boolean]) - Symbol) - Integer) - 'ghi 1) diff --git a/test/traversal-util.rkt b/test/traversal-util.rkt deleted file mode 100644 index 62cef73..0000000 --- a/test/traversal-util.rkt +++ /dev/null @@ -1,22 +0,0 @@ -#lang typed/racket -(require (for-syntax syntax/parse - backport-template-pr1514/experimental/template - type-expander/expander) - "../traversal.hl.rkt") - -(provide define-fold) - -(define-syntax define-fold - (syntax-parser - [(_ _function-name:id - _type-name:id - whole-type:type - _type-to-replaceᵢ:type ...) - (with-folds - (λ () - (template - (begin - (define-type _type-name - (∀-replace-in-type whole-type _type-to-replaceᵢ ...)) - (define _function-name - (λ-replace-in-instance whole-type _type-to-replaceᵢ ...))))))])) \ No newline at end of file diff --git a/thoughts.rkt b/thoughts.rkt deleted file mode 100644 index e265ef2..0000000 --- a/thoughts.rkt +++ /dev/null @@ -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") -|# \ No newline at end of file diff --git a/times.rkt.txt b/times.rkt.txt deleted file mode 100644 index 97f74de..0000000 --- a/times.rkt.txt +++ /dev/null @@ -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) - ))))) - diff --git a/traversal.hl.rkt b/traversal.hl.rkt deleted file mode 100644 index bff6c0e..0000000 --- a/traversal.hl.rkt +++ /dev/null @@ -1,397 +0,0 @@ -#lang hyper-literate typed/racket/base #:no-require-lang #:no-auto-require -@(require racket/require - scribble-enhanced/doc - racket/require - hyper-literate - (subtract-in scribble/struct scribble-enhanced/doc) - scribble/decode - (for-label racket/format - racket/promise - racket/list - syntax/parse - syntax/parse/experimental/template - type-expander - (except-in (subtract-in typed/racket/base type-expander) - values) - (only-in racket/base values) - (subtract-in racket/contract typed/racket/base) - phc-toolkit - phc-toolkit/untyped-only - remember)) -@(unless-preexpanding - (require (for-label (submod "..")))) -@doc-lib-setup - -@title[#:style manual-doc-style - #:tag "traversal" - #:tag-prefix "phc-graph/traversal"]{Parametric replacement of parts of - data structures} - -@(chunks-toc-prefix - '("(lib phc-graph/scribblings/phc-graph-implementation.scrbl)" - "phc-graph/traversal")) - -@(table-of-contents) - -@(declare-exporting (lib "phc-graph/traversal.hl.rkt")) - -@section{Introduction} - -This utility allows functionally updating parts of data structures. The -@racket[define-fold] macro takes the type of the whole data structure and a -list of type names associated with their predicate. It locates all literal -occurrences of those type names within the data structure, and identifies -those locations as the parts to replace. The type of the whole data structure -is expressed as a syntactic tree. Within that syntactic tree, only the parts -which are syntactically equal to one of the types to replace are considered. - -As an example, suppose the whole type is -@racket[(List Foo Number (Listof String))], and @racket[Foo] is defined as: - -@racketblock[(define-type Foo (Listof String))] - -If @racket[Foo] is given as a type to replace, and its replacement type is -@racket[(Listof Symbol)], then the type of the result would be: - -@racketblock[(List (Listof Symbol) Number (Listof String))] - -The second occurrence of @racket[(Listof String)], although semantically -equivalent to the type to replace, @racket[Foo], will not be altered, as it is -not expressed syntactically using the @racket[Foo] identifier. - -@defform[(define-fold function-name type-name whole-type type-to-replaceᵢ ...)]{ - The @racket[define-fold] macro takes the type of the whole data structure, and - a list of types to replace, each associated with a predicate for that type. It - @;defines @racket[_name] as a macro, which behaves as follows: - defines @racket[(type-name Tᵢ ...)] as a polymorphic type, with one type - argument for each @racket[type-to-replaceᵢ], such that - - @racketblock[(type-name type-to-replaceᵢ ...)] - - is the same type as - - @racketblock[whole-type] - - In other words, @racket[type-name] is defined as @racket[whole-type], except - that each syntactic occurrence of a @racket[type-to-replaceᵢ] is replaced with - the corresponding type argument @racket[Tᵢ]. - - It also defines @racket[function-name] as a function, with the type - - @racketblock[(∀ (Aᵢ ... Bᵢ ... Acc) - (→ (?@ (→ Any Boolean : Aᵢ) - (→ Aᵢ Acc (Values Bᵢ Acc))) - ... - (→ (type-name Aᵢ ...) - Acc - (Values (type-name Bᵢ ...) - Acc))))] - - We use the @racket[?@] notation from - @racketmodname[syntax/parse/experimental/template] to indicate that the - function accepts a predicate, followed by an update function, followed by - another predicate, and so on. For example, the function type when there are - three @racket[type-to-replaceᵢ] would be: - - @racketblock[(∀ (A₁ A₂ A₃ B₁ B₂ B₃ Acc) - (→ (→ Any Boolean : A₁) - (→ A₁ Acc (Values B₁ Acc)) - (→ Any Boolean : A₂) - (→ A₂ Acc (Values B₂ Acc)) - (→ Any Boolean : A₃) - (→ A₃ Acc (Values B₃ Acc)) - (→ (type-name A₁ A₂ A₃) - Acc - (Values (type-name B₁ B₂ B₃) - Acc))))] - - The @racket[function-name] replaces all values in the whole data structure - which are present in locations corresponding to a @racket[type-to-replaceᵢ] in - the @racket[whole-type]. It expects those values to have the type @racket[Aᵢ], - i.e. its input type is not restricted to @racket[whole-type], any polymorphic - instance of @racket[type-name] is valid. Each value is passed as an argument - to the corresponding update function with type - @racket[(→ Aᵢ Acc (Values Bᵢ Acc))], and the result of type @racket[Bᵢ] is - used as a replacement. - - An accumulator value, with the type @racket[Acc], is threaded through all - calls to all update functions, so that the update functions can communicate - state in a functional way.} - -@section{Implementation} - -@subsection{Caching the results of @racket[define-fold]} - -@chunk[ - (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[ - (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[ - (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[ - (define fold-τ - (syntax-parser - [(_whole-type:type _type-to-replaceᵢ:type …) - #:with rec-args #'([_type-to-replaceᵢ _Tᵢ] …) - (cached [τ- - (get-τ-cache) - (get-τ-defs) - #'(_whole-type _type-to-replaceᵢ …)] - (define replacements (make-immutable-free-id-tree-table - (map syntax-e - (syntax->list - #'([_type-to-replaceᵢ . _Tᵢ] …))))) - #`(∀ (_Tᵢ …) - #,(syntax-parse #'_whole-type - #:literals (Null Pairof Listof List Vectorof Vector U tagged) - )))]))] - -@CHUNK[ - (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[ - (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[ - (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[ - (define fold-f - (syntax-parser - [(_whole-type:type _type-to-replaceᵢ:type …) - #:with rec-args #'([_type-to-replaceᵢ _predicateᵢ _updateᵢ] …) - (define replacements (make-immutable-free-id-tree-table - (map syntax-e - (syntax->list - #'([_type-to-replaceᵢ . _updateᵢ] …))))) - (define/with-syntax _args #'({?@ _predicateᵢ _updateᵢ} …)) - (cached [f- - (get-f-cache) - (get-f-defs) - #'(_whole-type _type-to-replaceᵢ …)] - #`[(λ ({?@ _predicateᵢ _updateᵢ} …) - (λ (v acc) - #,(syntax-parse #'_whole-type - #:literals (Null Pairof Listof List Vectorof Vector U tagged) - ))) - (∀ (_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[ - [t - #:when (dict-has-key? replacements #'t) - #:with _update (dict-ref replacements #'t) - #'(_update v acc)]] - -@chunk[ - [t - #:when (dict-has-key? replacements #'t) - #:with _T (dict-ref replacements #'t) - #'_T]] - -@chunk[ - [(~or Null (List)) - #'Null]] - -@chunk[ - [(~or Null (List)) - #'(values v acc)]] - - -@CHUNK[ - [(Pairof X Y) - #'(Pairof (replace-in-type X . rec-args) - (replace-in-type Y . rec-args))]] - -@CHUNK[ - [(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[ - [(Listof X) - #'(Listof (replace-in-type X . rec-args))]] - -@CHUNK[ - [(Listof X) - #'(foldl-map (replace-in-instance X . rec-args) - acc v)]] - -@CHUNK[ - [(Vectorof X) - #'(Vectorof (replace-in-type X . rec-args))]] - -@CHUNK[ - [(Vectorof X) - #'(vector->immutable-vector - (list->vector - (foldl-map (replace-in-instance X . rec-args) - acc - (vector->list v))))]] - - -@CHUNK[ - [(List X Y …) - #'(Pairof (replace-in-type X . rec-args) - (replace-in-type (List Y …) . rec-args))]] - -@CHUNK[ - [(List X Y …) - #'(let*-values ([(result-x acc-x) ((replace-in-instance X . rec-args) - (car v) - acc)] - [(result-y* acc-y*) ((replace-in-instance (List Y …) . rec-args) - (cdr v) - acc-x)]) - (values (cons result-x result-y*) acc-y*))]] - -@CHUNK[ - [(U _Xⱼ …) - #'(U (replace-in-type _Xⱼ . rec-args) …)]] - -@CHUNK[ - [(U _Xⱼ …) - #'(dispatch-union v - ([_type-to-replaceᵢ Aᵢ _predicateᵢ] …) - [_Xⱼ ((replace-in-instance _Xⱼ . rec-args) v acc)] - …)]] - -@CHUNK[ - [(tagged _name [_fieldⱼ (~optional :colon) _Xⱼ] …) - #'(tagged _name [_fieldⱼ : (replace-in-type _Xⱼ . rec-args)] …)]] - -@CHUNK[ - [(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[ - [else-T - #'else-T]] - -@chunk[ - [else-T - #'(values v acc)]] - - -where @racket[foldl-map] is defined as: - -@chunk[ - (: foldl-map (∀ (A B Acc) (→ (→ A Acc (Values B Acc)) - Acc - (Listof A) - (Values (Listof B) Acc)))) - (define (foldl-map f acc l) - (if (null? l) - (values l - acc) - (let*-values ([(v a) (f (car l) acc)] - [(ll aa) (foldl-map f a (cdr l))]) - (values (cons v ll) - aa))))] - -@section{Putting it all together} - -@chunk[<*> - (require racket/require - phc-toolkit - type-expander - phc-adt - "dispatch-union.rkt" - (for-syntax "subtemplate-override.rkt" - (subtract-in (combine-in racket/base - syntax/parse) - "subtemplate-override.rkt") - backport-template-pr1514/experimental/template - phc-toolkit/untyped - racket/syntax - type-expander/expander - "free-identifier-tree-equal.rkt" - racket/dict) - (for-meta 2 racket/base) - (for-meta 2 phc-toolkit/untyped) - (for-meta 2 syntax/parse)) - - (provide (for-syntax with-folds - replace-in-type - ∀-replace-in-type - replace-in-instance - λ-replace-in-instance)) - - - - (begin-for-syntax - - - )] \ No newline at end of file