From e9089b872ccdd1b1f0353ba6905de03e1c3774a3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Georges=20Dup=C3=A9ron?= Date: Thu, 13 Apr 2017 18:37:37 +0200 Subject: [PATCH] Initial commit --- .gitignore | 6 ++ .travis.yml | 32 ++++++++ LICENSE-more.md | 24 ++++++ LICENSE.txt | 116 +++++++++++++++++++++++++++++ README.md | 11 +++ experiment.rkt | 123 +++++++++++++++++++++++++++++++ info.rkt | 10 +++ main.rkt | 1 + scribblings/typed-worklist.scrbl | 9 +++ 9 files changed, 332 insertions(+) create mode 100644 .gitignore create mode 100644 .travis.yml create mode 100644 LICENSE-more.md create mode 100644 LICENSE.txt create mode 100644 README.md create mode 100644 experiment.rkt create mode 100644 info.rkt create mode 100644 main.rkt create mode 100644 scribblings/typed-worklist.scrbl diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..1a59348 --- /dev/null +++ b/.gitignore @@ -0,0 +1,6 @@ +*~ +\#* +.\#* +.DS_Store +compiled/ +/doc/ diff --git a/.travis.yml b/.travis.yml new file mode 100644 index 0000000..5fd7e5b --- /dev/null +++ b/.travis.yml @@ -0,0 +1,32 @@ +language: c +sudo: false + +env: + global: + # RACKET_DIR is an argument to install-racket.sh + - RACKET_DIR=~/racket + - PATH="$RACKET_DIR/bin:$PATH" + matrix: + # RACKET_VERSION is an argument to install-racket.sh + - RACKET_VERSION=6.4 + - RACKET_VERSION=6.5 + - RACKET_VERSION=6.6 + - RACKET_VERSION=6.7 + - RACKET_VERSION=6.8 + - RACKET_VERSION=RELEASE + - RACKET_VERSION=HEAD + +before_install: +- curl -L https://raw.githubusercontent.com/greghendershott/travis-racket/master/install-racket.sh | bash +- raco pkg install --deps search-auto doc-coverage cover cover-codecov # or cover-coveralls + +install: +- raco pkg install --deps search-auto -j 2 + +script: +- raco test -x -p "$(basename "$TRAVIS_BUILD_DIR")" +- raco setup --check-pkg-deps --no-zo --no-launcher --no-install --no-post-install --no-docs --pkgs "$(basename "$TRAVIS_BUILD_DIR")" +- raco doc-coverage "$(basename "$TRAVIS_BUILD_DIR")" +- raco cover -s main -s test -s doc -f codecov -f html -d ~/coverage . || true +# TODO: add an option to cover to run the "outer" module too, not just the submodules. +# TODO: deploy the coverage info. \ No newline at end of file diff --git a/LICENSE-more.md b/LICENSE-more.md new file mode 100644 index 0000000..e4716f7 --- /dev/null +++ b/LICENSE-more.md @@ -0,0 +1,24 @@ +anaphoric +Copyright (c) 2016-2017 Georges Dupéron + + + +This package is in distributed under the Creative Commons CC0 license +https://creativecommons.org/publicdomain/zero/1.0/, as specified by +the LICENSE.txt file. + + + +The CC0 license is equivalent to a dedication to the Public Domain +in most countries, but is also effective in countries which do not +recognize explicit dedications to the Public Domain. + + + +In order to avoid any potential licensing issues, this package is explicitly +distributed under the Creative Commons CC0 license +https://creativecommons.org/publicdomain/zero/1.0/, or under the GNU Lesser +General Public License (LGPL) https://opensource.org/licenses/LGPL-3.0, or +under the Apache License Version 2.0 +https://opensource.org/licenses/Apache-2.0, or under the MIT license +https://opensource.org/licenses/MIT, at your option. diff --git a/LICENSE.txt b/LICENSE.txt new file mode 100644 index 0000000..670154e --- /dev/null +++ b/LICENSE.txt @@ -0,0 +1,116 @@ +CC0 1.0 Universal + +Statement of Purpose + +The laws of most jurisdictions throughout the world automatically confer +exclusive Copyright and Related Rights (defined below) upon the creator and +subsequent owner(s) (each and all, an "owner") of an original work of +authorship and/or a database (each, a "Work"). + +Certain owners wish to permanently relinquish those rights to a Work for the +purpose of contributing to a commons of creative, cultural and scientific +works ("Commons") that the public can reliably and without fear of later +claims of infringement build upon, modify, incorporate in other works, reuse +and redistribute as freely as possible in any form whatsoever and for any +purposes, including without limitation commercial purposes. These owners may +contribute to the Commons to promote the ideal of a free culture and the +further production of creative, cultural and scientific works, or to gain +reputation or greater distribution for their Work in part through the use and +efforts of others. + +For these and/or other purposes and motivations, and without any expectation +of additional consideration or compensation, the person associating CC0 with a +Work (the "Affirmer"), to the extent that he or she is an owner of Copyright +and Related Rights in the Work, voluntarily elects to apply CC0 to the Work +and publicly distribute the Work under its terms, with knowledge of his or her +Copyright and Related Rights in the Work and the meaning and intended legal +effect of CC0 on those rights. + +1. Copyright and Related Rights. A Work made available under CC0 may be +protected by copyright and related or neighboring rights ("Copyright and +Related Rights"). Copyright and Related Rights include, but are not limited +to, the following: + + i. the right to reproduce, adapt, distribute, perform, display, communicate, + and translate a Work; + + ii. moral rights retained by the original author(s) and/or performer(s); + + iii. publicity and privacy rights pertaining to a person's image or likeness + depicted in a Work; + + iv. rights protecting against unfair competition in regards to a Work, + subject to the limitations in paragraph 4(a), below; + + v. rights protecting the extraction, dissemination, use and reuse of data in + a Work; + + vi. database rights (such as those arising under Directive 96/9/EC of the + European Parliament and of the Council of 11 March 1996 on the legal + protection of databases, and under any national implementation thereof, + including any amended or successor version of such directive); and + + vii. other similar, equivalent or corresponding rights throughout the world + based on applicable law or treaty, and any national implementations thereof. + +2. Waiver. To the greatest extent permitted by, but not in contravention of, +applicable law, Affirmer hereby overtly, fully, permanently, irrevocably and +unconditionally waives, abandons, and surrenders all of Affirmer's Copyright +and Related Rights and associated claims and causes of action, whether now +known or unknown (including existing as well as future claims and causes of +action), in the Work (i) in all territories worldwide, (ii) for the maximum +duration provided by applicable law or treaty (including future time +extensions), (iii) in any current or future medium and for any number of +copies, and (iv) for any purpose whatsoever, including without limitation +commercial, advertising or promotional purposes (the "Waiver"). Affirmer makes +the Waiver for the benefit of each member of the public at large and to the +detriment of Affirmer's heirs and successors, fully intending that such Waiver +shall not be subject to revocation, rescission, cancellation, termination, or +any other legal or equitable action to disrupt the quiet enjoyment of the Work +by the public as contemplated by Affirmer's express Statement of Purpose. + +3. Public License Fallback. Should any part of the Waiver for any reason be +judged legally invalid or ineffective under applicable law, then the Waiver +shall be preserved to the maximum extent permitted taking into account +Affirmer's express Statement of Purpose. In addition, to the extent the Waiver +is so judged Affirmer hereby grants to each affected person a royalty-free, +non transferable, non sublicensable, non exclusive, irrevocable and +unconditional license to exercise Affirmer's Copyright and Related Rights in +the Work (i) in all territories worldwide, (ii) for the maximum duration +provided by applicable law or treaty (including future time extensions), (iii) +in any current or future medium and for any number of copies, and (iv) for any +purpose whatsoever, including without limitation commercial, advertising or +promotional purposes (the "License"). The License shall be deemed effective as +of the date CC0 was applied by Affirmer to the Work. Should any part of the +License for any reason be judged legally invalid or ineffective under +applicable law, such partial invalidity or ineffectiveness shall not +invalidate the remainder of the License, and in such case Affirmer hereby +affirms that he or she will not (i) exercise any of his or her remaining +Copyright and Related Rights in the Work or (ii) assert any associated claims +and causes of action with respect to the Work, in either case contrary to +Affirmer's express Statement of Purpose. + +4. Limitations and Disclaimers. + + a. No trademark or patent rights held by Affirmer are waived, abandoned, + surrendered, licensed or otherwise affected by this document. + + b. Affirmer offers the Work as-is and makes no representations or warranties + of any kind concerning the Work, express, implied, statutory or otherwise, + including without limitation warranties of title, merchantability, fitness + for a particular purpose, non infringement, or the absence of latent or + other defects, accuracy, or the present or absence of errors, whether or not + discoverable, all to the greatest extent permissible under applicable law. + + c. Affirmer disclaims responsibility for clearing rights of other persons + that may apply to the Work or any use thereof, including without limitation + any person's Copyright and Related Rights in the Work. Further, Affirmer + disclaims responsibility for obtaining any necessary consents, permissions + or other rights required for any use of the Work. + + d. Affirmer understands and acknowledges that Creative Commons is not a + party to this document and has no duty or obligation with respect to this + CC0 or use of the Work. + +For more information, please see + diff --git a/README.md b/README.md new file mode 100644 index 0000000..a94f238 --- /dev/null +++ b/README.md @@ -0,0 +1,11 @@ +[![Build Status,](https://img.shields.io/travis/jsmaniac/delay-pure/master.svg)](https://travis-ci.org/jsmaniac/delay-pure) +[![Coverage Status,](https://img.shields.io/coveralls/jsmaniac/delay-pure/master.svg)](https://coveralls.io/github/jsmaniac/delay-pure) +[![Build Stats,](https://img.shields.io/badge/build-stats-blue.svg)](http://jsmaniac.github.io/travis-stats/#jsmaniac/delay-pure) +[![Online Documentation.](https://img.shields.io/badge/docs-online-blue.svg)](http://docs.racket-lang.org/delay-pure/) +[![License: CC0 v1.0.](https://img.shields.io/badge/license-CC0-blue.svg)](https://creativecommons.org/publicdomain/zero/1.0/) + +delay-pure +========== + +Non-cached promises for Typed/Racket, like delay/name. Should be sound for +occurrence typing (unlike delay/name) because only pure functions are allowed. diff --git a/experiment.rkt b/experiment.rkt new file mode 100644 index 0000000..2df698a --- /dev/null +++ b/experiment.rkt @@ -0,0 +1,123 @@ +#lang type-expander + +;; TODO: write a macro wrapper which does the unsafe-cast (until the bug in TR +;; is fixed), and (un)wraps the inputs and outputs. +(provide worklist) + +#;(struct (A) I ([v : A]) #:transparent) +#;(struct (A) O ([v : A]) #:transparent) + +(define-type (I A) (Pairof 'I A)) +(define-type (O A) (Pairof 'O A)) + +(define #:∀ (A) (i [a : A]) : (I A) (cons 'I a)) +(define #:∀ (A) (o [a : A]) : (O A) (cons 'O a)) + +(define #:∀ (A) (i-v [w : (I A)]) : A (cdr w)) +(define #:∀ (A) (o-v [w : (O A)]) : A (cdr w)) + +(: worklist + (∀ (II OO A ...) + (→ (List (Listof (∩ A II)) ...) + (List (→ (∩ A II) (List (∩ A OO) (Listof (∩ A II)) ...)) ...) + (List (Listof (∩ A OO)) ...)))) + +(: kons (∀ (A B) (→ A B (Pairof A B)))) +(define kons cons) + +(begin + ;; Typed version of: + #;(define (append-inner-inner lll) + (apply map append lll)) + + (: append-inner-inner (∀ (OO A ...) (→ (Pairof (List (Listof (∩ OO A)) ...) + (Listof (List (Listof (∩ OO A)) ...))) + (List (Listof (∩ OO A)) ... A)))) + (define (append-inner-inner lll) + (if (null? lll) + '() + ;; Could also just use recursion here. + ((inst foldl + (List (Listof (∩ OO A)) ...) + (List (Listof (∩ OO A)) ...) + Nothing + Nothing) + map-append2 + (car lll) + (cdr lll)))) + + (: map-append2 (∀ (A ...) (→ (List (Listof A) ...) + (List (Listof A) ...) + (List (Listof A) ...)))) + (define (map-append2 la lb) + (map + (ann append (∀ (X) (→ (Listof X) (Listof X) (Listof X)))) la lb))) + +(define (worklist roots processors) + (define res + (map (λ #:∀ (Input Output) ([x : (Listof Input)] + [f : (→ Input + (List Output (Listof (∩ A II)) ...))]) + (map (λ ([x : (List Output (Listof (∩ A II)) ...)]) + ;; TODO: enqueue these instead of making a recursive call, + ;; and discard the already-processed elements as well as those + ;; already present in the queue. + (kons (car x) + ((inst worklist II OO A ... A) (cdr x) processors))) + (map f x))) + roots processors)) + + (define nulls + (map (λ #:∀ (Input Output) ([f : (→ Input + (List Output (Listof (∩ A II)) ...))]) + (ann '() (Listof Output))) + processors)) + + ((inst append-inner-inner OO A ... A) + (kons nulls + (map (λ #:∀ (Output) ([x : (Listof (Pairof Output + (List (Listof (∩ A OO)) + ...)))]) + ;; (Pairof _ (Listof (List (Listof (∩ A OO)) ... A))) + ((inst append-inner-inner OO A ... A) + (kons nulls + (map (λ ([xᵢ : (Pairof Output + (List (Listof (∩ A OO)) ... A))]) + (cdr xᵢ)) + x)))) + res)))) + +;(:type mapf) +;(define (mapf vs procs) +; (error "NIY")) + +(define w1 + (unsafe-cast + (inst worklist + (I Any) (O Any) + (U (I Number) (O String)) + (U (I Float) (O Boolean))) + ;; cast to its own type, circumventing the fact that TR doesn't seem to apply + ;; intersections in this case. + (-> (List (Listof (Pairof 'I Number)) (Listof (Pairof 'I Flonum))) + (List + (-> (Pairof 'I Number) + (List + (Pairof 'O String) + (Listof (Pairof 'I Number)) + (Listof (Pairof 'I Flonum)))) + (-> (Pairof 'I Flonum) + (List + (Pairof 'O Boolean) + (Listof (Pairof 'I Number)) + (Listof (Pairof 'I Flonum))))) + (List (Listof (Pairof 'O String)) (Listof (Pairof 'O Boolean)))))) + + +(λ () + (w1 + '(() ()) + (list (λ ([x : (I Number)]) + (list (o (number->string (i-v x))) '() '())) + (λ ([x : (I Float)]) + (list (o (positive? (i-v x))) '() '()))))) diff --git a/info.rkt b/info.rkt new file mode 100644 index 0000000..d248d8e --- /dev/null +++ b/info.rkt @@ -0,0 +1,10 @@ +#lang info +(define collection "typed-worklist") +(define deps '("base" + "rackunit-lib")) +(define build-deps '("scribble-lib" + "racket-doc")) +(define scribblings '(("scribblings/typed-worklist.scrbl" ()))) +(define pkg-desc "A Typed/Racket implementation of Kildall's worklist algorithm, with multiple worklists of different types.") +(define version "0.1") +(define pkg-authors '("Georges Dupéron")) diff --git a/main.rkt b/main.rkt new file mode 100644 index 0000000..7bc35af --- /dev/null +++ b/main.rkt @@ -0,0 +1 @@ +#lang racket/base diff --git a/scribblings/typed-worklist.scrbl b/scribblings/typed-worklist.scrbl new file mode 100644 index 0000000..8d8cb72 --- /dev/null +++ b/scribblings/typed-worklist.scrbl @@ -0,0 +1,9 @@ +#lang scribble/manual +@(require (for-label typed-worklist + racket/base)) + +@title{typed-worklist} +@author[@author+email["Georges Dupéron" "georges.duperon@gmail.com"]] + +@defmodule[typed-worklist] +