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
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
|
; XDOC Documentation System for ACL2
;
; Copyright (C) 2022 Kestrel Institute (http://www.kestrel.edu)
;
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
;
; Author: Alessandro Coglio (coglio@kestrel.edu)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(in-package "ACL2")
(include-book "defxdoc-plus")
(include-book "std/testing/assert-equal" :dir :system)
(include-book "std/testing/must-eval-to-t" :dir :system)
(include-book "std/testing/must-fail" :dir :system)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; This is just to ensure the correctness of the implementation of DEFXDOC+,
; which picks all the arguments of DEFXDOC from the DEFXDOC+ call
; and passes them to the call of DEFXDOC generated by DEFXDOC+.
; If the arguments of DEFXDOC change,
; the following test will fail,
; prompting the adaptation of DEFXDOC+ to the change.
(assert-equal (macro-args 'defxdoc (w state))
'(xdoc::name
&key
xdoc::parents
xdoc::short
xdoc::long
xdoc::pkg
xdoc::no-override))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(must-eval-to-t
(mv-let (erp form state)
(trans1 '(defxdoc+ topic
:parents (parent1 parent2)
:short "short"
:long "long"
:pkg "ACL2"
:no-override t))
(declare (ignore erp))
(value (equal form
'(progn
(defxdoc topic
:parents (parent1 parent2)
:short "short"
:long "long"
:pkg "ACL2"
:no-override t))))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(must-eval-to-t
(mv-let (erp form state)
(trans1 '(defxdoc+ topic
:parents (parent1 parent2)
:short "short"
:long "long"
:pkg "ACL2"
:no-override t
:order-subtopics t))
(declare (ignore erp))
(value (equal form
'(progn
(defxdoc topic
:parents (parent1 parent2)
:short "short"
:long "long"
:pkg "ACL2"
:no-override t)
(xdoc::order-subtopics topic nil t))))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(must-eval-to-t
(mv-let (erp form state)
(trans1 '(defxdoc+ topic
:parents (parent1 parent2)
:short "short"
:long "long"
:pkg "ACL2"
:no-override t
:default-parent t))
(declare (ignore erp))
(value (equal form
'(progn
(defxdoc topic
:parents (parent1 parent2)
:short "short"
:long "long"
:pkg "ACL2"
:no-override t)
(local (set-default-parents topic)))))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(must-eval-to-t
(mv-let (erp form state)
(trans1 '(defxdoc+ topic
:parents (parent1 parent2)
:short "short"
:long "long"
:pkg "ACL2"
:no-override t
:order-subtopics t
:default-parent t))
(declare (ignore erp))
(value (equal form
'(progn
(defxdoc topic
:parents (parent1 parent2)
:short "short"
:long "long"
:pkg "ACL2"
:no-override t)
(xdoc::order-subtopics topic nil t)
(local (set-default-parents topic)))))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(must-fail ; malformed keyed options
(defxdoc+ topic 88))
(must-fail ; malforemed keyed options
(defxdoc+ topic :malformed))
(must-fail ; malformed keyed options
(defxdoc+ topic :short))
(must-fail ; unrecognized keyed options
(defxdoc+ topic :unknown "a"))
(must-fail ; unrecognized keyed options
(defxdoc+ topic :parents ("legit") :shorter #\c :longer 'doc))
|
