Lift
Macro to lift a deeply embedded PFCS definition
to a shallowly embedded PFCS definition
with a theorem relating the two.
The required argument must be a ground form
that evaluates to a PFCS definition.
The form is evaluated and the resulting definition is processed.
The pred keyword argument, if present,
must be a symbol to use as
the name of the predicate the constitutes
the generated shallowly embedded PFCS definition.
If omitted, the default is nil,
which means that the predicate name is determined
according to the same mapping as for PFCS variables.
This input is quoted (not evaluated) for processing.
The prime keyword argument, if present,
must be a symbol to use as
the prime that parameterizes the PFCS semantics.
It is p by default.
This is quoted (not evaluated) for processing.
Macro: lift
(defmacro lift (def &key pred (prime 'p))
(cons 'make-event
(cons (cons 'lift-fn
(cons def
(cons (cons 'quote (cons pred 'nil))
(cons (cons 'quote (cons prime 'nil))
'(state)))))
'nil)))
