|
|
|---|
|
|
|
|---|
(deftrans-core name extra-args bodies) → *
Function:
(defun deftrans-core (name extra-args bodies) (declare (xargs :guard (and (symbolp name) (true-listp extra-args) (alistp bodies)))) (let ((__function__ 'deftrans-core)) (declare (ignorable __function__)) (b* ((names (deftrans-mk-names name)) (name-exprs/decls/stmts (acl2::packn-pos (list name '-exprs/decls/stmts) name)) (extra-args-names (deftrans-get-args extra-args))) (cons 'progn (cons (deftrans-defn-ident names bodies extra-args) (cons (deftrans-defn-ident-list names bodies extra-args extra-args-names) (cons (deftrans-defn-const names bodies extra-args) (cons (cons 'defines (cons name-exprs/decls/stmts (cons (deftrans-defn-expr names bodies extra-args extra-args-names) (cons (deftrans-defn-expr-list names bodies extra-args extra-args-names) (cons (deftrans-defn-expr-option names bodies extra-args extra-args-names) (cons (deftrans-defn-const-expr names bodies extra-args extra-args-names) (cons (deftrans-defn-const-expr-option names bodies extra-args extra-args-names) (cons (deftrans-defn-genassoc names bodies extra-args extra-args-names) (cons (deftrans-defn-genassoc-list names bodies extra-args extra-args-names) (cons (deftrans-defn-member-designor names bodies extra-args extra-args-names) (cons (deftrans-defn-type-spec names bodies extra-args extra-args-names) (cons (deftrans-defn-spec/qual names bodies extra-args extra-args-names) (cons (deftrans-defn-spec/qual-list names bodies extra-args extra-args-names) (cons (deftrans-defn-align-spec names bodies extra-args extra-args-names) (cons (deftrans-defn-decl-spec names bodies extra-args extra-args-names) (cons (deftrans-defn-decl-spec-list names bodies extra-args extra-args-names) (cons (deftrans-defn-initer names bodies extra-args extra-args-names) (cons (deftrans-defn-initer-option names bodies extra-args extra-args-names) (cons (deftrans-defn-desiniter names bodies extra-args extra-args-names) (cons (deftrans-defn-desiniter-list names bodies extra-args extra-args-names) (cons (deftrans-defn-designor names bodies extra-args extra-args-names) (cons (deftrans-defn-designor-list names bodies extra-args extra-args-names) (cons (deftrans-defn-declor names bodies extra-args extra-args-names) (cons (deftrans-defn-declor-option names bodies extra-args extra-args-names) (cons (deftrans-defn-dirdeclor names bodies extra-args extra-args-names) (cons (deftrans-defn-absdeclor names bodies extra-args extra-args-names) (cons (deftrans-defn-absdeclor-option names bodies extra-args extra-args-names) (cons (deftrans-defn-dirabsdeclor names bodies extra-args extra-args-names) (cons (deftrans-defn-dirabsdeclor-option names bodies extra-args extra-args-names) (cons (deftrans-defn-paramdecl names bodies extra-args extra-args-names) (cons (deftrans-defn-paramdecl-list names bodies extra-args extra-args-names) (cons (deftrans-defn-paramdeclor names bodies extra-args extra-args-names) (cons (deftrans-defn-tyname names bodies extra-args extra-args-names) (cons (deftrans-defn-strunispec names bodies extra-args extra-args-names) (cons (deftrans-defn-structdecl names bodies extra-args extra-args-names) (cons (deftrans-defn-structdecl-list names bodies extra-args extra-args-names) (cons (deftrans-defn-structdeclor names bodies extra-args extra-args-names) (cons (deftrans-defn-structdeclor-list names bodies extra-args extra-args-names) (cons (deftrans-defn-enumspec names bodies extra-args extra-args-names) (cons (deftrans-defn-enumer names bodies extra-args extra-args-names) (cons (deftrans-defn-enumer-list names bodies extra-args extra-args-names) (cons (deftrans-defn-statassert names bodies extra-args extra-args-names) (cons (deftrans-defn-initdeclor names bodies extra-args extra-args-names) (cons (deftrans-defn-initdeclor-list names bodies extra-args extra-args-names) (cons (deftrans-defn-decl names bodies extra-args extra-args-names) (cons (deftrans-defn-decl-list names bodies extra-args extra-args-names) (cons (deftrans-defn-label names bodies extra-args extra-args-names) (cons (deftrans-defn-stmt names bodies extra-args extra-args-names) (cons (deftrans-defn-block-item names bodies extra-args extra-args-names) (cons (deftrans-defn-block-item-list names bodies extra-args extra-args-names) (cons ':hints (cons '(("Goal" :in-theory '(deftrans-measure-theory))) (cons ':verify-guards (cons 'nil (cons '/// (cons (cons 'verify-guards (cons (cdr (assoc-eq 'expr names)) 'nil)) 'nil)))))))))))))))))))))))))))))))))))))))))))))))))))))))) (cons (deftrans-defn-fundef names bodies extra-args extra-args-names) (cons (deftrans-defn-extdecl names bodies extra-args extra-args-names) (cons (deftrans-defn-extdecl-list names bodies extra-args extra-args-names) (cons (deftrans-defn-transunit names bodies extra-args extra-args-names) (cons (cons 'define (cons (cdr (assoc-eq 'filepath-transunit-map names)) (cons (cons '(map filepath-transunit-mapp) extra-args) (cons ':returns (cons '(new-map filepath-transunit-mapp :hyp (filepath-transunit-mapp map)) (cons (cons 'b* (cons (cons '((when (omap::emptyp map)) nil) (cons '((mv path tunit) (omap::head map)) (cons (cons 'new-path (cons (cons 'deftrans-filepath (cons 'path (cons (symbol-name name) 'nil))) 'nil)) (cons (cons 'new-tunit (cons (cons (cdr (assoc-eq 'transunit names)) (cons 'tunit extra-args-names)) 'nil)) (cons (cons 'new-map (cons (cons (cdr (assoc-eq 'filepath-transunit-map names)) (cons '(omap::tail map) extra-args-names)) 'nil)) 'nil))))) '((omap::update new-path new-tunit new-map)))) '(:verify-guards :after-returns))))))) (cons (cons 'define (cons (cdr (assoc-eq 'transunit-ensemble names)) (cons (cons '(tunits transunit-ensemblep) extra-args) (cons ':returns (cons '(new-tunits transunit-ensemblep) (cons ':short (cons '"Transform a translation unit ensemble." (cons (cons 'b* (cons '(((transunit-ensemble tunits) tunits)) (cons (cons 'transunit-ensemble (cons (cons (cdr (assoc-eq 'filepath-transunit-map names)) (cons 'tunits.unwrap extra-args-names)) 'nil)) 'nil))) 'nil)))))))) 'nil))))))))))))))