Sig
Specify type signatures for polymorphic functions
Examples:
(sig nthcdr (nat (listof :a)) => (listof :a))
(sig binary-append ((listof :a) (listof :a)) => (listof :a))
(sig nth (nat (listof :a)) => :a
:satisfies (< x1 (len x2)))
;; xi corresponds to the ith type appearing in the sig form. For example,
;; x1 corresponds to nat and x2 to (listof :a)
General Form:
(sig fun-name arg-types => return-type
[:satisfies hyp]
[:hints hints]
[:gen-rule-classes rule-classes]
[:rule-classes rule-classes]
[:verbose t])
where arg-types is a list of defdata type expressions
and return-type is a defdata type expression with the
added capability of referring to type variables, which in our
syntax are represented using keyword symbols :a, :b, :c, ....
Note: sig is currently limited to only 12 type variables.
Check :pe *allowed-type-vars* to view them. We have never encountered
type signatures with more than 3 type variables, so we hope that this is
not a limitation in practice. There are several other limitations
we impose on sig. If you would like more comprehensive
support, contact Pete and Harsh.
The following keyword arguments are supported by the sig macro:
- :satisfies -- specify additional dependent type hypotheses.
- :hints -- ACL2::hints option to the generic type signature.
- :gen-rule-classes -- ACL2::rule-classes option to the generic type signature.
- :rule-classes -- ACL2::rule-classes option to the generated theorems.
- :verbose -- for debugging.
