Utilities
Generic utilities that are unrelated to Verilog processing, but which
are provided by the VL books.
Subtopics
- Name-database
- A general utility for generating fresh names.
- Vl-gc
- Maybe trigger a garbage collection.
- Make-lookup-alist
- Make a fast-alist for use with fast-memberp.
- Symbol-list-names
- (symbol-list-names x) maps symbol-name across a list.
- Html-encoding
- Routines to encode HTML entities such as < and & into
<, &, etc.
- Nats-from
- (nats-from a b) enumerates the naturals from [a, b).
- Redundant-mergesort
- Same as mergesort, but avoids re-sorting lists that are already
sorted.
- Longest-common-prefix
- (longest-common-prefix x y) returns the longest list, p, such
that p is a prefix of both x and y, in the sense of
prefixp.
- Vl-edition-p
- Editions of the Verilog or SystemVerilog standards that VL attempts
to implement.
- Nat-listp
- (nat-listp x) recognizes lists where every element satisfies natp.
- Vl-plural-p
- (vl-plural-p x) determines whether a description of a list should
be plural instead of singluar.
- Vl-remove-keys
- (vl-remove-keys keys x) removes all bindings for the given keys
from alist.
- Sum-nats
- Sum a list of natural numbers.
- Vl-maybe-nat-listp
- (vl-maybe-nat-listp x) recognizes lists where every element satisfies maybe-natp.
- Url-encoding
- Functions for % encoding strings for use in URLs, as described in RFC 3986.
- Fast-memberp
- Fast list membership using make-lookup-alist.
- Vl-string-keys-p
- Recognizer for alists whose keys are strings.
- Max-nats
- Maximum member in a list of naturals.
- Longest-common-prefix-list
- (longest-common-prefix-list x) returns the longest list, p,
such that p is a prefix of every list in x.
- Character-list-listp
- (character-list-listp x) recognizes lists where every element satisfies character-listp.
- Vl-string-list-values-p
- Recognizer for alists whose values are string lists.
- Vl-character-list-list-values-p
- Recognizer for alists whose values are strings.
- Remove-from-alist
- (remove-from-alist key alist) removes all bindings for key from
alist.
- Prefix-of-eachp
- (prefix-of-eachp p x) returns true exactly when p is a
prefix of every member of x.
- Vl-maybe-string-listp
- (vl-maybe-string-listp x) recognizes lists where every element satisfies maybe-stringp.
- Pos-listp
- (pos-listp x) recognizes lists where every element satisfies posp.
- Vl-string-values-p
- Recognizer for alists whose values are strings.
- String-list-listp
- (string-list-listp x) recognizes lists where every element satisfies string-listp.
- True-list-listp
- (true-list-listp x) recognizes lists where every element satisfies true-listp.
- Symbol-list-listp
- (symbol-list-listp x) recognizes lists where every element satisfies symbol-listp.
- Explode-list
- Coerce a list of strings into a character-list-listp.
- All-have-len
- (all-have-len x n) determines if every element of x has length
n.
- Min-nats
- Minimum member in a list of naturals.
- Debuggable-and
- Alternative to and that prints a message where it fails.
- Vl-starname
- (vl-starname name) is given a string, say "foo", and return a
symbol in the ACL2 package, e.g., ACL2::*foo*.
- Remove-equal-without-guard
- Same as remove-equal, but doesn't require true-listp.
- String-fix
- (string-fix x) is the identity function for strings.
- Longer-than-p
- (longer-than-p n x) determines if the list x is longer than
n.
- Clean-alist
- Anyp
- Recognizes any object.
- Or*
- or* is like or but is a (typically disabled) function.
- Fast-alist-free-each-alist-val
- Applies fast-alist-free to every value bound in the alist x.
- And*
- and* is like and but is a (typically disabled) function.
- Not*
- not* is like not but is not built-in to ACL2 and is
typically disabled.
- Free-list-of-fast-alists
- *nls*
- A string consisting of a newline character.
