7.9

#### 4.4Uninterpreted 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)) > (asserts) ; so Rosette emits the corresponding assertion '((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)) #t (ite (= 0 (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: {[b boolean?] [(! b) real?]} > (~> real?) ~>: arity mismatch; the expected number of arguments does not match the given number expected: at least 2 given: 1 arguments...: real?

 procedure 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)