1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
|
; C Library
;
; Copyright (C) 2022 Kestrel Institute (http://www.kestrel.edu)
; Copyright (C) 2022 Kestrel Technology LLC (http://kestreltechnology.com)
;
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
;
; Author: Alessandro Coglio (coglio@kestrel.edu)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(in-package "C")
(include-book "kestrel/std/util/defmacro-plus" :dir :system)
(include-book "xdoc/constructors" :dir :system)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defmacro+ pack (&rest args)
:parents (c)
:short "Build a symbol in the C package from a list of atoms."
:long
(xdoc::topstring
(xdoc::p
"This is a concise wrapper of the built-in @(tsee packn-pos),
specialized for the C package.
This macro takes any number of arguments,
which are evaluated and put into a list passed to @(tsee packn-pos);
thus, the arguments must be all atoms."))
`(packn-pos (list ,@args) (pkg-witness "C")))
|
