typed-racket/typed-racket-lib/typed-racket/static-contracts
Ben Greenman 137c138b2e static-contracts: fix list-length/sc
- Change `list-length/sc` to be a contract for lists
- Add tests to check sc-generated contracts against values
2017-09-19 00:13:00 -04:00
..
combinators static-contracts: fix list-length/sc 2017-09-19 00:13:00 -04:00
combinators.rkt Remove extra directories. 2014-12-02 00:53:36 -05:00
constraints.rkt add refinement types, linear expr objs, and ineq props (#510) 2017-03-27 14:32:29 -04:00
equations.rkt remove interning for most Reps in TR 2016-12-16 15:18:50 -05:00
instantiate.rkt less dynamic dispatch in contract gen 2016-10-31 12:53:48 -04:00
kinds.rkt fix contract provide ordering bug 2016-10-23 19:50:24 -04:00
optimize.rkt add types for Immutable-HashTable, Mutable-HashTable, Weak-HashTable (#559) 2017-06-26 18:00:19 -04:00
parametric-check.rkt remove interning for most Reps in TR 2016-12-16 15:18:50 -05:00
README Remove extra directories. 2014-12-02 00:53:36 -05:00
structures.rkt less dynamic dispatch in contract gen 2016-10-31 12:53:48 -04:00
terminal.rkt Remove extra directories. 2014-12-02 00:53:36 -05:00

Static Contracts:
-----------------

Purpose:
Static contracts are a data structure that correspond to a regular contract.
The two differences are that a static contract corresponds to a contract at a lower phase,
and that they are designed to support introspection and manipulation.

Operations:

various constructors : * -> static-contract?
Construct a static contract corresponding to a regular contract.

optimize : static-contract? [#:trusted-positive boolean? #:trusted-negative boolean?] -> static-contract?
Changes a static contract into another one that is cheaper to check. It also removes contracts
protecting a trusted side.

instantiate : static-contract? (-> A) [kind/c] -> (or/c syntax? A)
Turns a static contract into syntax that when evaluated is the corresponding contract.
The failure continuation is invoked if the translation fails to produce a contract of the right kind.

Internal Implementation Details:

A static contract is one of three things:

recursive-sc:
  This introduces bindings for recursive contracts.
recursive-sc-use:
  This is a reference to a previously introduced recursive contract.
other:
  This is a combinator or terminal contract.

These support a couple of different operations:

sc-map: Calls a function on each sub static contract, and builds up a new static contract
sc-traverse: Calls a function on each sub static contract
sc-terminal-kind: Tells whether a static contract has no subparts and has a known contract kind

These are not applicable to recursive contract; instantaite uses them in its implementation, and
directly deals with the recursive casses.

sc->contract: Turns a static contract into syntax
sc->constraints: Turns a static contract into constraints about the contract kind