Add a bunch of documentation to static contracts.

original commit: 93488e49b44f51188c2f54b939ddc8379f14e285
This commit is contained in:
Eric Dobson 2013-12-14 18:30:02 -08:00
parent 37ec886258
commit 9b858ddfd0
18 changed files with 125 additions and 5 deletions

View File

@ -3,7 +3,7 @@ Static Contracts:
Purpose:
Static contracts are a data structure that correspond to a regular contract.
The twe differences are that a static contract corresponds to a contract at a lower phase,
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:

View File

@ -1,5 +1,7 @@
#lang racket/base
;; Reprovides everything from all the files in the combinators directory.
(require (for-syntax racket/base racket/runtime-path))
(begin-for-syntax

View File

@ -1,5 +1,9 @@
#lang racket/base
;; Static contract for any/c.
;; Allows optimizations as many combinators can be simplified if their arguments are any/sc
;; Ex: (listof/sc any/sc) => list?/sc
(require "../structures.rkt" "../constraints.rkt"
racket/match
(except-in racket/contract recursive-contract)

View File

@ -1,5 +1,8 @@
#lang racket/base
;; Static contract for case->.
;; Like case-> doesn't support keyword arguments.
(require "../structures.rkt" "../constraints.rkt"
racket/list racket/match
unstable/contract

View File

@ -1,5 +1,8 @@
#lang racket/base
;; Static contracts for control contracts.
;; Currently only supports prompt tags.
(require "../structures.rkt" "../constraints.rkt"
racket/list racket/match
unstable/contract

View File

@ -1,4 +1,9 @@
#lang racket/base
;; Static contracts for common data types.
;; These are used during optimizations as simplifications.
;; Ex: (listof/sc any/sc) => list?/sc
(require "simple.rkt"
(for-template racket/base racket/set racket/promise))
(provide (all-defined-out))

View File

@ -1,5 +1,7 @@
#lang racket/base
;; Static contract for ->.
;; Supports the whole range of possible options that -> does.
(require "../structures.rkt" "../constraints.rkt"
racket/list racket/match
@ -119,7 +121,7 @@
(map (lambda (arg) (f arg 'covariant))
range-args)
empty)))
(function-combinator new-args indices mand-kws opt-kws))

View File

@ -1,5 +1,8 @@
#lang racket/base
;; Static contracts for class constructs.
;; Currently supports object/c and class/c.
(require "../structures.rkt" "../constraints.rkt"
racket/list racket/match
unstable/contract

View File

@ -1,5 +1,7 @@
#lang racket/base
;; Static contract for parametric->/c.
(require "../structures.rkt" "../constraints.rkt"
racket/list racket/match
unstable/contract

View File

@ -1,5 +1,8 @@
#lang racket/base
;; Static contracts that are terminal and have no sub parts.
;; Ex: (flat/sc #'number?)
(require
"../kinds.rkt"
"../structures.rkt"

View File

@ -1,5 +1,7 @@
#lang racket/base
;; Static contract for struct/c.
(require "../structures.rkt" "../constraints.rkt"
racket/list racket/match
unstable/contract

View File

@ -1,4 +1,8 @@
#lang racket/base
;; Static contracts for structural contracts.
;; Ex: list/sc, vectorof/sc
(require "../structures.rkt"
"../constraints.rkt"
racket/list racket/match

View File

@ -1,5 +1,40 @@
#lang racket/base
;; Manages the restrictions on what kind of contract is viable.
;; Some combinators cannot support arbitrary contracts. Ex: hash/c needs a flat contract on the key.
;; This module provides the functions for manipulating a set of such constraints.
;;
;; Constructors:
;; simple-contract-restrict: kind? -> contract-restrict?
;; This means that the generated contract will be contract of the supplied kind.
;;
;; variable-contract-restrict: identifier? -> contract-restrict?
;; This means that the generated contract will be of the same kind as the recursive contract
;; referenced by the variable.
;;
;; merge-restricts: kind? contract-restrict? ... -> contract-restrict?
;; merge-restricts*: kind? (listof contracct-restrict?) -> contract-restrict?
;; This means that the generated contract will be the max of kind and all of the other contract
;; restricts.
;;
;; add-constraint: contract-restrict? kind? -> contract-restrict
;; This means the kind of the generated contract can not be greater than the supplied kind.
;;
;; close-loop: (lisotf identifier?) (listof contract-restrict?) contract-restrict? -> contract-restrict?
;; This takes a bunch of recursive contract identifiers, their corresponding contract-restricts,
;; the contract restrict for a body and constructs the appropriate constract restrict.
;;
;; Other:
;; validate-constraints: contract-restrict? -> void?
;; This takes a contract-restrict and raises an exception if it has any violated constraints.
;;
;; contract-restrict-recursive-values: contract-restrict? -> (dict/c identifier? kind?)
;; Provides the kinds of all of the internal recursive contracts that are a part of the
;; contract-restrict.
;;
;;
;;
(require
racket/match
racket/list

View File

@ -1,5 +1,13 @@
#lang racket
;; Manages a set of mutually recursive equations, and provids functionality for finding a fix point.
;; An equation set has two components
;; 1. a mapping of variables to initial values.
;; 2. a mapping of variables to thunks that compute new values.
;;
;; Variables are an opaque structure, which support accessing their current value.
(provide
make-equation-set
add-variable!
@ -23,12 +31,14 @@
(hash-set! (equation-set-initial-values eqs) a-var initial-value)
a-var)
; add-equation! (equation-set? var? (-> value?))
; add-equation!: (equation-set? var? (-> value?) -> void?)
(define (add-equation! eqs var thunk)
(hash-set! (equation-set-equations eqs) var thunk))
(define current-variable-values (make-parameter (hash)))
;; resolve-equations (equation-set? -> (hash/c var? value?))
;; Produces a mapping of variables to values such that every equation holds.
(define (resolve-equations eqs)
(define values (hash-copy (equation-set-initial-values eqs)))
(parameterize ((current-variable-values values))

View File

@ -1,5 +1,7 @@
#lang racket/base
;; Provides functionality to take a static contract and turn it into a regular contract.
(require
racket/function
racket/match
@ -16,12 +18,14 @@
(c:contract-out
[instantiate ((static-contract? (c:-> c:none/c)) (contract-kind?) . c:->* . syntax?)]))
;; Providing these so that tests can work directly with them.
(module* internals #f
(provide compute-constraints
compute-recursive-kinds
instantiate/inner))
;; kind is the greatest kind of contract that is supported, if a greater kind would be produced the
;; fail procedure is called.
(define (instantiate sc fail [kind 'impersonator])
(with-handlers [(exn:fail:constraint-failure? (lambda (exn) (fail)))]
(instantiate/inner sc

View File

@ -1,5 +1,10 @@
#lang racket/base
;; Functions for the different kinds of contracts, which are represented by the symbols:
;; 'flat, 'chaperone, and 'impersonator
;;
;; There is an ordering with 'flat < 'chaperone < 'impersonator.
(require racket/match racket/contract)
(provide
@ -23,6 +28,7 @@
[('impersonator (or 'flat 'chaperone)) #f]
[('impersonator 'impersonator) #t]))
;; Computes the maximum over the supplied kinds.
(define combine-kinds
(case-lambda
((v) v)

View File

@ -1,5 +1,8 @@
#lang racket/base
;; Functionalityt otoptimize a static contract to provide faster checking.
;; Also supports droping one side's obligations.
(require "combinators.rkt"
"structures.rkt"
racket/set
@ -7,6 +10,8 @@
(except-in racket/contract recursive-contract)
racket/match)
(provide
(contract-out
[optimize (static-contract? (or/c 'covariant 'contravariant 'invariant ) . -> . static-contract?)]))
@ -51,6 +56,9 @@
[(contravariant) (invert-variance var2)]
[(invariant) 'invariant]))
;; If the variance is 'covariant, drops the parts ensuring that server behaves
;; If the variance is 'contrvariant, drops the parts ensuring that client behaves
;; If the variance is 'invariant, only optimizes the contract.
(define (optimize sc variance)
(define (single-step sc variance)
(define ((maybe/co reduce) sc)

View File

@ -1,5 +1,7 @@
#lang racket/base
;; Internal structures for representing a static contract.
(require racket/match racket/list racket/generic
(except-in racket/contract recursive-contract)
"kinds.rkt" "constraints.rkt")
@ -85,16 +87,33 @@
v))
v)))
;; Functionality that all static contracts should support
(define-generics sc
;; sc-map: static-contract? (static-contract? variance/c -> static-contract?) -> static-contract?
;; Takes a static contract and returns a similar one.
;; Each sub part should be replaced with the value of calling the supplied function on it. The
;; variance argument should be how the sub part relates to the static contract.
[sc-map sc f]
;; sc->contract: static-contract? (static-contract? -> contract?) -> contract?
;; Takes a static contract and returns the corresponding contract.
;; The function argument should be used for sub parts of the static contract.
[sc->contract sc f]
;; sc->constraints: static-contract? (static-contract? -> constraint-set?) -> constraint-set?
;; Takes a static contract and computes the constraint set for a static contract.
;; The function argument should be used for sub parts of the static contract.
[sc->constraints sc f])
;; Super struct of static contracts
(struct static-contract ()
#:transparent
#:property prop:custom-print-quotable 'never)
;; Represents a recursive contract.
;; In each value and the body, each name is bound to a the corresponding value contract.
;; - names : (listof identifier?)
;; - values : (listof static-contract?)
;; - body : static-contract?
;; names and value must have the same length.
(struct recursive-contract static-contract (names values body)
#:transparent
#:methods gen:sc
@ -104,6 +123,8 @@
(recursive-contract names (map (λ (v) (f v 'covariant)) values) (f body 'covariant))]))]
#:methods gen:custom-write [(define write-proc recursive-contract-write-proc)])
;; A use of a contract bound by recursive-contract
;; - name : identifier?
(struct recursive-contract-use static-contract (name)
#:transparent
#:methods gen:sc
@ -112,6 +133,9 @@
(define (sc->constraints v f) (variable-contract-restrict (recursive-contract-use-name v)))]
#:methods gen:custom-write [(define write-proc recursive-contract-use-write-proc)])
;; Super struct of static contract combinators.
;; Provides printing functionality.
;; - args : (listof static-contract?)
(struct combinator static-contract (args)
#:transparent
#:property prop:combinator-name "combinator/sc"