Defpreprocess-map-fn
- Signature
(defpreprocess-map-fn const-name filename
path drop-shared show-warnings state)
→
(mv erp event state)- Arguments
- const-name — Guard (symbolp const-name).
- filename — Guard (stringp filename).
- path — Guard (stringp path).
- drop-shared — Guard (booleanp drop-shared).
- show-warnings — Guard (booleanp show-warnings).
Definitions and Theorems
Function: defpreprocess-map-fn
(defun defpreprocess-map-fn
(const-name filename
path drop-shared show-warnings state)
(declare (xargs :stobjs (state)))
(declare (xargs :guard (and (symbolp const-name)
(stringp filename)
(stringp path)
(booleanp drop-shared)
(booleanp show-warnings))))
(b* (((mv erp map warnings state)
(preprocess-map-from-comp-file
filename path
drop-shared show-warnings nil state))
(- (if show-warnings (show-warnings warnings)
nil))
((when erp) (mv erp nil state)))
(value (cons 'defconst
(cons const-name
(cons (cons 'quote (cons map 'nil))
'nil))))))
