|
|
|---|
|
|
|
|---|
Shallowly embedded semantics of expressions.
(sesem-expression expr prime state) → term
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 name-to-symbol.
Additions and multiplications are mapped to calls of the corresponding prime field operations applied to the terms obtained by translating the argument expressions.
Function:
(defun sesem-expression (expr prime state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (expressionp expr) (symbolp prime)))) (let ((__function__ 'sesem-expression)) (declare (ignorable __function__)) (expression-case expr :const (cons 'mod (cons expr.value (cons prime 'nil))) :var (name-to-symbol expr.name state) :add (cons 'add (cons (sesem-expression expr.arg1 prime state) (cons (sesem-expression expr.arg2 prime state) (cons prime 'nil)))) :mul (cons 'mul (cons (sesem-expression expr.arg1 prime state) (cons (sesem-expression expr.arg2 prime state) (cons prime 'nil)))))))