Primitive-functions
A formalization of the ACL2 primitive functions.
The ACL2 primitive functionshave no definitions.
Their evaluation semantics is described in the ACL2 documentation.
In order to formalize the evaluation semantics of ACL2,
we need to formalize the evaluation semantics of the primitive functions.
We do so ``directly'' here,
i.e. not via execution steps through evaluation states
as we do for defined functions.
Since our formalization of the ACL2 primitive functions
is written in the ACL2 logical language,
we use the executable ACL2 primitive functions of the logical language
to formalize the ACL2 primitive functions of the ACL2 programming language.
However, note that the latter operate on our model of ACL2 values,
i.e. on the value fixtype,
while the former operate on ACL2 values directly.
So there is a necessary indirection there,
due to the meta level nature of our formalization.
The treatment of symbol values is also slightly different,
because, as noted in the documentation of symbol-value,
at the meta level we want to be able to talk about
all possible symbols for all possible known packages,
and not just the symbols for the packages that happen to be known
at the point in which we write this formalization.
Here we formalize the evaluation of the ACL2 primitive functions
in the logic, i.e. for all possible values, inside and outside the guards.
The treatment of values outside the guards
are according to the completion axioms shown in the documentation,
which amount to fixing the values to the required types.
Subtopics
- Eval-intern-in-package-of-symbol
- Evaluation semantics of intern-in-package-of-symbol.
- Eval-pkg-witness
- Evaluation semantics of pkg-witness.
- Eval-pkg-imports
- Evaluation semantics of pkg-imports.
- Primitive-function-namep
- Check if a symbol value is the name of a primitive function.
- Primitive-function-arity
- Arith of a primitive function.
- Eval-if
- Evaluation semantics of if.
- Eval-bad-atom<=
- Evaluation semantics of bad-atom<=.
- Eval-coerce
- Evaluation semantics of coerce.
- Eval-<
- Evaluation semantics of <.
- Eval-complex
- Evaluation semantics of complex.
- Eval-binary-+
- Evaluation semantics of binary-+.
- Eval-binary-*
- Evaluation semantics of binary-*.
- Eval-equal
- Evaluation semantics of equal.
- Eval-cons
- Evaluation semantics of cons.
- Eval-symbol-package-name
- Evaluation semantics of symbol-package-name.
- Eval-complex-rationalp
- Evaluation semantics of complex-rationalp.
- Eval-code-char
- Evaluation semantics of code-char.
- Eval-unary-/
- Evaluation semantics of unary-/.
- Eval-symbol-name
- Evaluation semantics of symbol-name.
- Eval-realpart
- Evaluation semantics of realpart.
- Eval-numerator
- Evaluation semantics of numerator.
- Eval-imagpart
- Evaluation semantics of imagpart.
- Eval-denominator
- Evaluation semantics of denominator.
- Eval-char-code
- Evaluation semantics of char-code.
- Eval-ACL2-numberp
- Evaluation semantics of ACL2-numberp.
- Eval-unary--
- Evaluation semantics of unary--.
- Eval-symbolp
- Evaluation semantics of symbolp.
- Eval-stringp
- Evaluation semantics of stringp.
- Eval-rationalp
- Evaluation semantics of rationalp.
- Eval-integerp
- Evaluation semantics of integerp.
- Eval-characterp
- Evaluation semantics of characterp.
- Eval-consp
- Evaluation semantics of consp.
- Eval-cdr
- Evaluation semantics of cdr.
- Eval-car
- Evaluation semantics of car.
