On this page:
~>
function?
fv?
8.12

4.4 Uninterpreted Functions🔗ℹ

In Rosette, functions are special kinds of procedures that are pure (have no side effects) and total (defined on every input value). A function type is recognized by the function? predicate, and all function types are solvable. The type of a function specifies the function’s domain and range, which are given as solvable? non-function? types. A value of a function type is recognized by the fv? (function value) predicate. Because function types are solvable, they can be used in the define-symbolic[*] form to introduce a symbolic function constant. These symbolic function constants are technically uninterpreted functionsthey have no fixed meaning. Their meaning (or interpretation) is determined by the underlying solver as the result of a solver-aided query.

Examples:
> (current-bitwidth #f)
; An uninterpreted function from integers to booleans:
> (define-symbolic f (~> integer? boolean?))
> (f 1)     ; No built-in interpretation for 1.

(app f 1)

> (define-symbolic x real?)
> (f x)     ; This typechecks when x is an integer,

(app f (real->integer x))

> (vc)      ; so Rosette emits the corresponding assertion.

(vc #t (int? x))

> (define sol (solve (assert (not (equal? (f x) (f 1))))))
> (define g (evaluate f sol)) ; An interpretation of f.
> g

(fv integer?~>boolean?)

> (evaluate x sol)

0

> (fv? f)   ; f is a function value,

#t

> (fv? g)   ; and so is g.

#t

> (g 2)     ; We can apply g to concrete values

#t

> (g x)     ; and to symbolic values.

(ite (= 1 (real->integer x)) #f #t)

procedure

(~> d ...+ r)  function?

  d : (and/c solvable? (not/c function?))
  r : (and/c solvable? (not/c function?))
Returns a type predicate for recognizing functions that take as input values of types d...+ and produce values of type r. The domain and range arguments must be concrete solvable? types that are not themselves functions. Note that ~> expects at least one domain type to be given, disallowing zero-argument functions.

Examples:
> (define t (~> integer? real? boolean? (bitvector 4)))
> t

integer?~>real?~>boolean?~>(bitvector 4)

> (~> t integer?)

function: expected a list of primitive solvable types

  domain: '(integer?~>real?~>boolean?~>(bitvector 4))

> (define-symbolic b boolean?)
> (~> integer? (if b boolean? real?))

function: expected a primitive solvable type

  range: (union [b boolean?] [(! b) real?])

> (~> real?)

~>: arity mismatch;

 the expected number of arguments does not match the given

number

  expected: at least 2

  given: 1

procedure

(function? v)  boolean?

  v : any/c
Returns true if v is a concrete type predicate that recognizes function values.

Examples:
> (define t0? (~> integer? real? boolean? (bitvector 4)))
> (define t1? (~> integer? real?))
> (function? t0?)

#t

> (function? t1?)

#t

> (define-symbolic b boolean?)
> (function? (if b t0? t1?)) ; Not a concrete type.

#f

> (function? integer?)       ; Not a function type.

#f

> (function? 3)              ; Not a type.

#f

procedure

(fv? v)  boolean?

  v : any/c
Returns true if v is a concrete or symbolic function value.

Examples:
> (define-symbolic f (~> boolean? boolean?))
> (fv? f)

#t

> (fv? (lambda (x) x))

#f

> (define-symbolic b boolean?)
> (fv? (if b f 1))

b

> (define sol
    (solve
     (begin
       (assert (not (f #t)))
       (assert (f #f)))))
> (define g (evaluate f sol))
> g ; g implements logical negation.

(fv boolean?~>boolean?)

> (fv? g)

#t

; Verify that g implements logical negation:
> (verify (assert (equal? (g b) (not b))))

(unsat)