		Search-engine friendly clone of the ACL2 documentation.

Lifting

Lift-expression

Shallowly embedded semantics of expressions.

Signature
(lift-expression expr prime state) → term
Arguments: expr — Guard (expressionp expr).; prime — Guard (symbolp prime).

Besides the expression, this function also takes as argument a variable (symbol) to use as the prime. This is needed because we generate terms involving prime field operations, which all take a prime as argument; the prime is also used to reduce integer constants.

A constant is mapped to itself, reduced modulo the prime.

A variable is mapped to a symbol, according to lift-var-name.

Additions and multiplications are mapped to calls of the corresponding prime field operations applied to the terms obtained by translating the argument expressions.

Definitions and Theorems

Function: lift-expression

(defun lift-expression (expr prime state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (expressionp expr)
                             (symbolp prime))))
 (let ((__function__ 'lift-expression))
  (declare (ignorable __function__))
  (expression-case
      expr
      :const (cons 'mod
                   (cons expr.value (cons prime 'nil)))
      :var (lift-var-name expr.name state)
      :add (cons 'add
                 (cons (lift-expression expr.arg1 prime state)
                       (cons (lift-expression expr.arg2 prime state)
                             (cons prime 'nil))))
      :mul (cons 'mul
                 (cons (lift-expression expr.arg1 prime state)
                       (cons (lift-expression expr.arg2 prime state)
                             (cons prime 'nil)))))))