Trivial:   type-tailored library functions
1 What is Tailoring?
1.1 Examples of Tailoring
1.2 Technical Description
2 Using Tailorings
2.1 Built-in Tailorings
2.1.1 Definitions
define
let
let*
2.1.2 Format Strings
format
printf
2.1.3 Functions
curry
lambda
λ
2.1.4 Integer Arithmetic
+
-
*
/
quotient
add1
sub1
expt
2.1.5 List Operations
make-list
build-list
cons
car
cdr
list
length
list-ref
list-tail
append
reverse
map
sort
2.1.6 Regular Expressions
regexp
pregexp
byte-regexp
byte-pregexp
regexp-match
2.1.7 String Operations
string-length
string-ref
substring
string-append
bytes-length
bytes-ref
subbytes
bytes-append
2.1.8 Vector Operations
vector
make-vector
build-vector
vector-append
vector-ref
vector-length
vector-set!
vector-map
vector-map!
vector->list
vector->immutable-vector
vector-fill!
vector-take
vector-take-right
vector-drop
vector-drop-right
2.2 Typed /   Untyped Interaction
3 Defining new Tailorings
define-tailoring
3.1 Property Domains
make-property-domain
property-domain?
in-domain?
⊥?
⊤?
glb
glb*
⊓*
lub
lub*
⊔*
reduce
reduce*
3.1.1 Built-in Property Domains
arity-domain
format-string-domain
integer-domain
list-domain
regexp-group-domain
vector-domain
vector-domain->list-domain
list-domain->vector-domain
list-domain->integer-domain
vector-domain->integer-domain
integer-domain->list-domain
integer-domain->vector-domain
list-domain-append*
list-domain-cons
list-domain-car
list-domain-cdr
list-domain-length
list-domain-ref
list-domain-reverse
list-domain-set
list-domain-slice
vector-domain-append*
vector-domain-length
vector-domain-ref
vector-domain-set
vector-domain-slice
3.2 Tailoring Properties
φ
φ?
φ-init
φ-ref
φ-set
φ<=?
3.3 Miscellaneous
trivial-logger
7.1

Trivial: type-tailored library functions

 (require trivial) package: trivial

The trivial module exports tailored versions of standard library functions.

1 What is Tailoring?

A tailored function f+:
  • has the same specification and behavior as some library function f

  • but can catch runtime errors during expansion

  • and may typecheck a little smoother in Typed Racket.

1.1 Examples of Tailoring

For example, make a new Racket module with a malformed call to format:

#lang racket/base
 
(format "batman and ~a")

This file will compile no problem (raco make file.rkt), but will raise a runtime error (racket file.rkt). If you add the line (require trivial), the file no longer compiles, but instead gives a helpful error message.

Here’s another example. Save the following (correct) Racket module:

#lang racket/base
 
(define (get-sidekick str)
  (cond
   [(regexp-match #rx"^([a-z]+) and ([a-z]+)$" str)
    => caddr]
   [else "???"]))
 
(get-sidekick "batman and alfred")

It should compile and run, returning "alfred". Great. Now try converting it to Typed Racket:

#lang typed/racket/base
 
(define (get-sidekick (str : String)) : String
  (cond
   [(regexp-match #rx"^([a-z]+) and ([a-z]+)$" str)
    => caddr]
   [else "???"]))
 
(get-sidekick "batman and alfred")

The file doesn’t compile anymore. Adding (require trivial) to the top of the file removes the error.

1.2 Technical Description

A tailored function f+ is really a macro that examines its call site and attempts to combine knowledge about the behavior of f with static properties of its arguments. If all goes well, the tailoring will either (1) identify an error or (2) transform the call site into an equivalent—but more efficient or more Typed-Racket-friendly—call. Otherwise, the call to f+ behaves exactly as a call to f would.

In general, the static properties could be the result of any static analysis. But this library is limited to properties that other macros can establish through local analysis and propagate via syntax properties. See Defining new Tailorings for more details.

2 Using Tailorings

The following tailorings are all provided by the trivial module. Note that these tailorings have the same name as their Racket and Typed Racket equivalents to make this library a drop-in replacement for existing code.

The descriptions below assume familiarity with the Racket reference and describe only the new behavior of the tailored function or form. Click the name of any tailoring to see its definition in the Racket reference.

2.1 Built-in Tailorings

2.1.1 Definitions

 (require trivial/define) package: trivial

WARNING the static analysis implemented by trivial/define is unsound in the presence of set!. Do not set! in a module that uses trivial/define.

syntax

(define id expr)

syntax

(define (head args) expr)

Forces local expansion of expr and associates any inferred properties with id for the rest of expansion.

syntax

(let ([id val-expr] ...) body ...+)

syntax

(let* ([id val-expr] ...) body ...+)

Forces local expansion of each val-expr and associates any inferred properties with the respective id in the context of body ...+.

2.1.2 Format Strings

 (require trivial/format) package: trivial

procedure

(format form v ...)  string?

  form : string?
  v : any/c

procedure

(printf form v ...)  void?

  form : string?
  v : any/c
When the string form is available during expansion, checks the number of values v ... against the number of formatting escapes in form that require arguments. When used in a Typed Racket module, annotates each v with the type required by the corresponding formatting escape.

2.1.3 Functions

 (require trivial/function) package: trivial

syntax

(curry f)

This form does not have a Typed Racket equivalent.

When the arity of the procedure f is available during expansion, expands to a curried version of f. In other words, if f is a function of N arguments then (curry f) is a chain of N one-argument functions.

For example,

(curry (λ (x y z) (+ (* x y) z)))

behaves the same as:
(λ (x)
  (λ (y)
    (λ (z)
      (+ (* x y) z))))

syntax

(lambda (id ...) body)

syntax

(λ (id ...) body)

Expands to an anonymous function with known arity. Other tailorings can access this arity.

2.1.4 Integer Arithmetic

 (require trivial/integer) package: trivial

procedure

(+ n ...)  integer?

  n : integer?

procedure

(- n ...)  integer?

  n : integer?

procedure

(* n ...)  integer?

  n : integer?
Constant-folding arithmetic functions. When all arguments n ... have integer values available during expansion, expands to a constant integer (or bignum). When only some arguments have available values, reduces the expression accordingly.

procedure

(/ n ...)  real?

  n : integer?

procedure

(quotient n ...)  integer?

  n : integer?
Constant-folding division. Raises a syntax error "division by zero" when the final argument is zero? during expansion.

procedure

(add1 n)  integer?

  n : integer?

procedure

(sub1 n)  integer?

  n : integer?
Increment and decrement functions that propagate the value of their argument.

procedure

(expt n1 n2)  integer?

  n1 : integer?
  n2 : integer?
Constant-folding exponentiation. If the value of n1 is unknown, checks whether the value of n2 is zero? or a small constant. In the latter case, unfolds to repeated multiplication of n1.

2.1.5 List Operations

 (require trivial/list) package: trivial

procedure

(make-list k v)  list?

  k : exact-nonnegative-integer?
  v : any/c

procedure

(build-list k proc)  list?

  k : exact-nonnegative-integer?
  proc : (-> exact-nonnegative-integer? any/c)

procedure

(cons a d)  pair?

  a : any/c
  d : any/c

procedure

(car p)  any/c

  p : pair?

procedure

(cdr p)  any/c

  p : pair?

procedure

(list v ...)  list?

  v : any/c

procedure

(length lst)  exact-nonnegative-integer?

  lst : list?

procedure

(list-ref lst pos)  any/c

  lst : pair?
  pos : exact-nonnegative-integer?

procedure

(list-tail lst pos)  any/c

  lst : pair?
  pos : exact-nonnegative-integer?

procedure

(append lst ...)  list?

  lst : list?

procedure

(reverse lst)  list?

  lst : list?

procedure

(map proc lst ...)  list?

  proc : procedure?
  lst : list?

procedure

(sort lst less-than?)  list?

  lst : list?
  less-than? : (-> any/c any/c any/c)
Length-aware and content-aware list operations. Operations that build lists propagate the length of their arguments. Operations that access lists check for bounds errors and propagate information about cells within a list.

Higher-order list functions check the arity of their functional argument; in particular, map includes a static check that the arity of its first argument includes the number of lists supplied at the call-site.

These Typed Racket examples demonstrate terms that would not typecheck without the trivial library.

Examples:
> (ann (- (length '(1 2 3)) 3) Zero)

- : Integer [more precisely: Zero]

0

> (ann (list-ref (make-list 5 0) 2) Zero)

- : Integer [more precisely: Zero]

0

> (ann (list-ref (list-ref '((A)) 0) 0) 'A)

- : Symbol [more precisely: 'A]

'A

2.1.6 Regular Expressions

 (require trivial/regexp) package: trivial

procedure

(regexp str)  regexp?

  str : string?

procedure

(pregexp str)  pregexp?

  str : string?

procedure

(byte-regexp byt)  byte-regexp?

  byt : bytes?

procedure

(byte-pregexp byt)  byte-pregexp?

  byt : bytes?
Regexp constructors; when their argument value is known during expansion, these constructors record the number of groups specified by the argument.

procedure

(regexp-match pattern input)

  
(if (and (or (string? pattern) (regexp? pattern))
         (or (string? input) (path? input)))
  (or/c #f (cons/c string? (listof (or/c string? #f))))
  (or/c #f (cons/c bytes?  (listof (or/c bytes?  #f)))))
  pattern : (or/c string? bytes? regexp? byte-regexp?)
  input : (or/c string? bytes? path? input-port?)
When possible, the type of the result list (in the case of a successful match) matches the number of groups in pattern.

This example is adapted from scribble/html-render

Examples:
> (: parse-font-size : String -> (List String String (U #f String) String))
> (define (parse-font-size str)
    (or (regexp-match #rx"^([0-9]*\\.?([0-9]+)?)(em|ex|pt|%|)$" str)
        (error 'malformed-input)))

2.1.7 String Operations

 (require trivial/string) package: trivial

procedure

(string-length str)  exact-nonnegative-integer?

  str : string?

procedure

(string-ref str k)  char?

  str : string?
  k : exact-nonnegative-integer?

procedure

(substring str start [end])  string?

  str : string?
  start : exact-nonnegative-integer?
  end : exact-nonnegative-integer? = (string-length str)

procedure

(string-append str ...)  string?

  str : string?

procedure

(bytes-length bstr)  exact-nonnegative-integer?

  bstr : bytes?

procedure

(bytes-ref bstr k)  byte?

  bstr : bytes?
  k : exact-nonnegative-integer?

procedure

(subbytes bstr start [end])  bytes?

  bstr : bytes?
  start : exact-nonnegative-integer?
  end : exact-nonnegative-integer? = (bytes-length bstr)

procedure

(bytes-append bstr ...)  bytes?

  bstr : bytes?
String and byte string operations that track the value of their arguments.

Example:
> (regexp-match (string-append "(" "a*" ")") "aaa")

- : (U (List String String) False)

'("aaa" "aaa")

2.1.8 Vector Operations

 (require trivial/vector) package: trivial

procedure

(vector v ...)  vector?

  v : any/c

procedure

(make-vector k v)  vector?

  k : exact-nonnegative-integer?
  v : any/c

procedure

(build-vector k proc)  vector?

  k : exact-nonnegative-integer?
  proc : (-> exact-nonnegative-integer? any/c)

procedure

(vector-append vec ...)  vector?

  vec : vector?

procedure

(vector-ref vec pos)  any/c

  vec : vector?
  pos : exact-nonnegative-integer?

procedure

(vector-length vec)  exact-nonnegative-integer?

  vec : vector?

procedure

(vector-set! vec pos v)  vector?

  vec : vector?
  pos : exact-nonnegative-integer?
  v : any/c

procedure

(vector-map proc vec ...)  vector?

  proc : procedure?
  vec : vector?

procedure

(vector-map! proc vec ...)  void?

  proc : procedure?
  vec : vector?

procedure

(vector->list vec)  list?

  vec : vector?

procedure

(vector->immutable-vector vec)  vector?

  vec : vector?

procedure

(vector-fill! vec v)  void?

  vec : vector?
  v : any/c

procedure

(vector-take vec pos)  vector?

  vec : vector?
  pos : exact-nonnegative-integer?

procedure

(vector-take-right vec pos)  vector?

  vec : vector?
  pos : exact-nonnegative-integer?

procedure

(vector-drop vec pos)  vector?

  vec : vector?
  pos : exact-nonnegative-integer?

procedure

(vector-drop-right vec pos)  vector?

  vec : vector?
  pos : exact-nonnegative-integer?
Length-aware and content-aware vector operations.

2.2 Typed / Untyped Interaction

The macros provided by trivial and related submodules are all untyped, but should work with no problems in Typed Racket modules. Under the hood, these macros keep two copies of every tailored identifier and use syntax-local-typed-context? to choose the appropriate identifiers and whether to expand to type-annotated code.

3 Defining new Tailorings

 (require trivial/tailoring) package: trivial

The bindings documented in this section are not provided by the trivial module.

Defining a new tailoring is not easy, but you can technically do it without making a pull request to this library. There are three steps to making a tailoring:
  • identify a property of Racket expressions,

  • define when & how to infer this property from #%datum literals,

  • define a set of tailorings that infer, propagate, and use the property

For example, here is a tailoring for add1. If the value of its argument is known during expansion, it expands to an integer.

#lang racket/base
(require
  trivial/tailoring
  (for-syntax racket/base)
  (only-in racket/base [add1 λ-add1])
  (only-in typed/racket/base [add1 τ-add1]))
 
(define-tailoring (-add1 [e ~> e+ (φ [integer-domain  i])])
  #:with +add1 (τλ #'τ-add1 #'λ-add1)
  #:= (⊥? integer-domain i)
      (+add1 e+)
  #:+ #t
      '#,(+ i 1)
  #:φ (φ-set (φ-init) integer-domain (reduce integer-domain + i 1)))

Here how to read the un-hygienic define-tailoring form:
  • -add1 is a macro expecting one argument, named e. (If -add1 is called with zero or +2 arguments, it expands to Racket’s add1.)

  • Note: the key integer-domain describes the relationship between e and i. In short, if tailorings that interact with integer-domain are implemented correctly, then expanding e yields and expression e+ with value i associated with the key integer-domain if and only if all run-time values for e are integers with value i.

    -add1 expands its argument e to the term e+ and retrieves a dictionary φ of tailoring properties (see Tailoring Properties) associated with e+. It furthermore pattern-matches the dictionary φ to get the integer value i of the expression e+.

  • -add1 conditionally produces one of two syntax objects.
    • In the neutral case (#:=), when i is an indeterminate value, the result is a call to Racket’s (or Typed Racket’s) add1.

    • In the positive case (#:+), when i is known during expansion, the result is the integer (+ i 1)

  • Any syntax object produced by expanding a call to -add1 with one argument has a new dictionary of tailoring properties (#:φ). The dictionary has one key, integer-domain. The corresponding value is "the indeterminate integer" when the value of i is indeterminate and (+ i 1) otherwise.

Here is the general form of define-tailoring:

syntax

(define-tailoring (tailored-id arg-pattern ...)
  guard ...
  defn ...
  #:= test-expr template
  #:+ then-expr template
  #:- then-expr expr
  #:φ prop-expr)
 
arg-pattern = (e-id elab-> e+-id (φ-id [key-id map-> val-id] ...))
     
guard = #:with expr expr
  | #:when expr
  | #:fail-unless expr expr
     
defn = (define . expr)
     
test-expr = expr
     
prop-expr = expr
     
elab-> = ~>
  | 
     
map-> = ->
  | 
Defines a tailoring tailored-id.

The arg-pattern clauses describe the shape of arguments to tailored-id. These say: expand e-id to e+-id, retrieve the tailoring properties φ-id associated with e+-id, and finally retrieve the values val-id associated with the given key-id.

If an arg-pattern is followed by a literal ..., then the tailoring accepts any number of arguments and matches each against arg-pattern. See the example for map below.

The guard expressions are a subset of the guards recognized by syntax-parse. Guards are most useful for defining variables based on the context in which the macro is expanding; see for example the #:with guard in -add1.

The defn expressions introduce local bindings.

The reason for #:+ etc. is so that define-tailoring can (1) log 'info messages for successful (#:+) and unsuccessful (#:=) tailorings (2) wrap each template in a syntax/loc based on use-sites of the tailoring.

The #:=, #:+, and #:- clauses are a cond-like domain-specific language. Their order matters. The test-expr are typically expressions involving the val-id bound above. In general, the template forms describe how the tailoring produces code (see syntax for their grammar). But the specific meaning of each template should correspond to its keyword:
  • #:= test-expr template uses test-expr to check whether the tailoring does not have enough information to transform the program. The template should implement "the standard Racket behavior" for tailored-id.

  • #:+ test-expr template determines when the tailoring can transform the program. The template may use unsafe operations, additional type annotations, or partial evaluation.

  • #:- test-expr expr detects errors statically and invokes expr to raise an exception. This clause is optional; when omitted, raises an internal exn:fail? about the inexhaustive tailoring.

Finally, prop-expr describes the result with a new dictionary of tailoring properties.

Note if any val-id is bound to a "top element" of the domain key-id, then define-tailoring raises an error message. See Property Domains for further intuition.

These examples contain free variables, but should convey the main ideas of define-tailoring. See the library implementation for working versions.

Example: a vector-length that computes the length statically.
(define-tailoring (-vector-length [e ~> e+ (φ [vector-domain v])])
  #:with +vl (τλ #'τ-vector-length #'λ-vector-length)
  (define n (vector-domain-length v))
  #:= (⊥? V-dom v)
      (+vl e+)
  #:+ #t '#,n
  #:φ (φ-set (φ-init) integer-domain n))

Example: a vector-ref that checks for out-of-bounds references and replaces in-bounds references with unsafe accesses.
(define-tailoring (-vector-ref [e1 ~> e1+ (φ1 [vector-domain  v])]
                               [e2 ~> e2+ (φ2 [integer-domain  i])])
   #:with +vector-ref (τλ #'τ-vector-ref #'λ-vector-ref)
   #:with +unsafe-vector-ref (τλ #'τ-unsafe-vector-ref #'λ-unsafe-vector-ref)
   (define n (vector-domain-length v))
   #:= (or (⊥? vector-domain v) (⊥? integer-domain i))
       (+vector-ref e1+ e2+)
   #:+ (and (<= 0 i) (< i n))
       (+unsafe-vector-ref e1+ e2+)
   #:- #t
       (format-bounds-error #'e1+ i)
   #:φ (vector-domain-ref v i))

Example: a map that statically checks arity and propagates the length of the result.
(define-tailoring (-map [f ~> f+ (φ1 [A-dom a])]
                        [e* ~> e+* (φ* [L-dom l*])] ...)
  #:with +map (τλ #'τ-map #'λ-map)
  (define expected-arity (length l*))
  (define arity-ok? (or (⊥? A-dom a) (= (length a) expected-arity)))
  (define n* (map L->I l*))
  #:= (and (⊥? I-dom (⊓* I-dom n*)) arity-ok?)
      (+map f+ e+* ...)
  #:+ arity-ok?
      (+map f+ e+* ...)
  #:- #t
      (format-arity-error #'f+ expected-arity)
  #:φ (φ-set (φ-init) L-dom (I->L (⊓* I-dom n*))))

3.1 Property Domains

Every tailoring extracts and asserts properties about program expressions. For example, tailorings in trivial/vector assert properties about the size and contents of vector values. Tailorings in trivial/format assert properties about the formatting escapes in string values. The "properties of vectors" and "properties of format strings" are two examples of property domains.

A property domain is a lattice. In particular, each property domain D has:
  • A distinguished bottom element ( D).

    Interpretation: unknown property.

  • A (family of) top element(s) ( D message).

    Interpretation: contradictory property, because message.

  • A family of elements.

  • A partial order <=? relating elements to one another, and to the top and bottom element. For any element e and any string message, both (<=? ( D) e) and (<=? e ( D message)) hold.

syntax

(make-property-domain sym #:leq order clause ...)

 
  sym : symbol?
  order : (-> any/c any/c any/c)
Builds a new property domain from a symbol id, ordering relation order, and list of syntax-parse clauses. Specifically:
  • generates symbols to represent the top and bottom elements,

  • lifts order to account for these top and bottom elements,

  • creates a syntax-parser from clause ...,

  • registers the new syntax parser with trivial/define.

The default order does not relate any elements to one another. It is (λ (x y) #false).

Examples:
> (define integer-domain
    (make-property-domain Z #:leq <=
     [i:integer (syntax-e #'i)]))
> (define flat-integer-domain
    (make-property-domain flat-Z
     [i:integer (syntax-e #'i)]))

procedure

(property-domain? v)  boolean?

  v : any/c
Predicate for values returned by make-property-domain.

procedure

(in-domain? D)  (-> any/c boolean?)

  D : property-domain?
Predicate for values in a domain.

procedure

( D)  (in-domain? D)

  D : property-domain?
Return the bottom element of D.

procedure

( D str)  (in-domain? D)

  D : property-domain?
  str : string?
Return a top element of D, with the error message str. If a tailoring encounters this element, it uses str to explain an error to the programmer.

Examples:
> (define bad-rx "foo ( bar")
> (regexp-match bad-rx "any string")

~>: [1:0] Invalid regexp pattern (unmatched '(' at index 4)

in "foo ( bar"

procedure

(⊥? D v)  boolean?

  D : property-domain?
  v : any/c

procedure

(⊤? D v)  boolean?

  D : property-domain?
  v : any/c
Predicates for the bottom and top elements of the given domain.

procedure

(glb D v ...)  (in-domain? D)

  D : property-domain?
  v : (in-domain? D)

procedure

( D v ...)  (in-domain? D)

  D : property-domain?
  v : (in-domain? D)

procedure

(glb* D lst)  (in-domain? D)

  D : property-domain?
  lst : (listof (in-domain? D))

procedure

(⊓* D lst)  (in-domain? D)

  D : property-domain?
  lst : (listof (in-domain? D))
Greatest-lower-bound on the domain D. Assumes that none of its arguments are top elements.

Examples:
> (glb integer-domain 1 2 -3 0)

-3

> (⊥? integer-domain (glb integer-domain 1 2 ( integer-domain)))

#t

procedure

(lub D v ...)  (in-domain? D)

  D : property-domain?
  v : (in-domain? D)

procedure

( D v ...)  (in-domain? D)

  D : property-domain?
  v : (in-domain? D)

procedure

(lub* D lst)  (in-domain? D)

  D : property-domain?
  lst : (listof (in-domain? D))

procedure

(⊔* D lst)  (in-domain? D)

  D : property-domain?
  lst : (listof (in-domain? D))
Least-upper-bound on D. Assumes that none of its arguments are top elements.

Examples:
> (lub* integer-domain '(4 5 6))

6

> (lub integer-domain 1 2 ( integer-domain))

2

procedure

(reduce D f init v ...)  (in-domain? D)

  D : property-domain?
  f : (-> any/c any/c any/c)
  init : any/c
  v : (in-domain? D)

procedure

(reduce* D f init lst)  (in-domain? D)

  D : property-domain?
  f : (-> any/c any/c any/c)
  init : any/c
  lst : (listof (in-domain? D))
Combine the elements v ... (or list of elements lst) using the binary function f. reduce lifts the given function f to handle top and bottom elements in D.

Examples:
> (reduce integer-domain + 8 6 7 5 3 0 9)

38

> (reduce flat-integer-domain + 0 2 2)

4

3.1.1 Built-in Property Domains

The following property domains are provided by the trivial/tailoring module.

value

arity-domain : property-domain?

Flat lattice of formal parameters to a function.

For example, the arity of:

(λ (x y z) x)

is:

(x y z)

Similarly, the arity of:

(λ ([a : String] [b : Integer]) 42)

is:

([a : String] [b : Integer])

value

format-string-domain : property-domain?

Flat lattice of sequences of Typed Racket types; in particular, an element of format-string-domain satisfies the contract:
These represent the values that a format string expects, given its formatting escapes.

value

integer-domain : property-domain?

Totally-ordered lattice of integers, using <=.

value

list-domain : property-domain?

Pointwise-ordered lattice of lists of tailoring properties.

value

regexp-group-domain : property-domain?

Flat lattice of lists of booleans. The boolean value at position i determines whether the i-th group in the regular expression is guaranteed to capture a string. For example, the domain element:

(list #true #false)

describes regular expressions that capture two groups; the second group may fail to capture. One regular expression that is described by this domain element is:

#rx"(a*)(b)*"

value

vector-domain : property-domain?

Pointwise-ordered lattice of lists of tailoring properties.

The list-domain and vector-domain have additional operations. These are -propagating versions of their racket/list and racket/vector equivalents. (And there is probably a better or more-general way to lift these computations.)

procedure

(vector-domain->list-domain v)  (in-domain? list-domain)

  v : (in-domain? vector-domain)

procedure

(list-domain->vector-domain l)  (in-domain? vector-domain)

  l : (in-domain? list-domain)
Defines an isomorphism between the list and vector domains.

procedure

(list-domain->integer-domain l)  (in-domain? integer-domain)

  l : (in-domain? list-domain)

procedure

(vector-domain->integer-domain v)  (in-domain? integer-domain)

  v : (in-domain? vector-domain)
"Forgetful functors" that abstract a sequence with its length.

procedure

(integer-domain->list-domain i)  (in-domain? list-domain)

  i : (in-domain? integer-domain)

procedure

(integer-domain->vector-domain i)  (in-domain? vector-domain)

  i : (in-domain? integer-domain)
"Right adjoints" to the above; these convert an integer to a sequence of empty tailoring property maps.

procedure

(list-domain-append* lst*)  (in-domain? list-domain)

  lst* : (listof (in-domain? list-domain))

procedure

(list-domain-cons prop lst)  (in-domain? list-domain)

  prop : φ?
  lst : (in-domain? list-domain)

procedure

(list-domain-car lst)  φ?

  lst : (in-domain? list-domain)

procedure

(list-domain-cdr lst)  (in-domain? list-domain)

  lst : (in-domain? list-domain)

procedure

(list-domain-length lst)  (in-domain? integer-domain)

  lst : (in-domain? list-domain)

procedure

(list-domain-ref lst pos)  φ?

  lst : (in-domain? list-domain)
  pos : (in-domain? integer-domain)

procedure

(list-domain-reverse lst)  (in-domain? list-domain)

  lst : (in-domain? list-domain)

procedure

(list-domain-set lst pos prop)  (in-domain? list-domain)

  lst : (in-domain? list-domain)
  pos : (in-domain? integer-domain)
  prop : φ?

procedure

(list-domain-slice lst lo hi)  (in-domain? list-domain)

  lst : (in-domain? list-domain)
  lo : (in-domain? integer-domain)
  hi : (in-domain? integer-domain)
Extra functions on list domain elements.

procedure

(vector-domain-append* lst*)  (in-domain? vector-domain)

  lst* : (vectorof (in-domain? vector-domain))

procedure

(vector-domain-length lst)  (in-domain? integer-domain)

  lst : (in-domain? vector-domain)

procedure

(vector-domain-ref lst pos)  φ?

  lst : (in-domain? vector-domain)
  pos : (in-domain? integer-domain)

procedure

(vector-domain-set lst pos prop)  (in-domain? vector-domain)

  lst : (in-domain? vector-domain)
  pos : (in-domain? integer-domain)
  prop : φ?

procedure

(vector-domain-slice lst lo hi)  (in-domain? vector-domain)

  lst : (in-domain? vector-domain)
  lo : (in-domain? integer-domain)
  hi : (in-domain? integer-domain)
Extra functions on vector domain elements.

3.2 Tailoring Properties

Tailorings associate static properties to expressions using finite maps φ. Each map relates property domains to values in the domain (or the bottom element of the domain).

procedure

(φ stx)  φ?

  stx : syntax?
Get the tailoring properties associated with the syntax object stx.

procedure

(φ? v)  boolean?

  v : any/c
Predicate for tailoring property maps.

procedure

(φ-init)  φ?

Return an empty map.

procedure

(φ-ref prop D)  (in-domain? D)

  prop : φ?
  D : property-domain?
Return the value associated with domain D in the map prop.

procedure

(φ-set prop D v)  φ?

  prop : φ?
  D : property-domain?
  v : (in-domain? d)
Return a map like prop, but with v associated with the domain D.

procedure

(φ<=? p1 p2)  boolean?

  p1 : φ?
  p2 : φ?
Pointwise ordering on tailoring property maps. Returns true when p2 has bindings for every domain D bound in p1, and furthermore the value v1 associated with D in p1 is less than the value v2 associated with D in p2 (using the order from D).

3.3 Miscellaneous

value

trivial-logger : logger?

Logs events to the "ttt" topic.