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
|
#|$ACL2s-Preamble$;
(include-book ;; Newline to fool ACL2/cert.pl dependency scanner
"portcullis")
(begin-book t :ttags :all);$ACL2s-Preamble$|#
(in-package "ACL2S")
(include-book "definec" :ttags :all)
(defmacro defintrange1 (name min max)
(declare (xargs :guard (symbolp name)))
`(make-event
(b* ((pkg (current-package state))
(M (defdata::type-metadata-table (w state)))
(A (defdata::type-alias-table (w state)))
(th1 (make-sym ',name 'thm1 pkg))
(th2 (make-sym ',name 'thm2 pkg))
(th3 (make-sym ',name 'thm3 pkg))
(namep (make-symbl `(,',name p) pkg))
(type (cond ((equal ,min 0) 'acl2s::nat)
((< 0 ,min) 'acl2s::pos)
((<= ,max 0) 'acl2s::neg)
(t 'acl2s::integer)))
(pred (make-symbl `(,type p) pkg))
(rng `(and (,pred a)
(<= ,,min a)
(< a ,,max)))
(type-of-type (type-of-type ',name M A))
(alias? (not (equal type-of-type ',name))))
(value
(if alias?
'(value-triple :invisible)
`(progn
(defdata-subtype ,',name ,type :strictp t)
(defthm ,th1
(implies (,namep a) ,rng)
:rule-classes ((:forward-chaining)))
(defthm ,th2
(implies ,rng (,namep a))
:rule-classes ((:rewrite :backchain-limit-lst 1)))
(defthm ,th3
(equal (,namep a) ,rng)
:rule-classes :compound-recognizer)
(in-theory (disable ,namep))))))))
(defmacro defintrange (name min max)
"Define a datatype that includes all integers [min..max), i.e., >= min and < max"
(declare (xargs :guard (symbolp name)))
`(progn (defdata ,name (range integer (,min <= _ < ,max)))
(defintrange1 ,name ,min ,max)))
#|
(defmacro defintrange (name min max)
"Define a datatype that includes all integers [min..max), i.e., >= min and < max"
(declare (xargs :guard (symbolp name)))
`(make-event
(b* ((pkg (current-package state))
(th1 (make-sym ',name 'thm1 pkg))
(th2 (make-sym ',name 'thm2 pkg))
(th3 (make-sym ',name 'thm3 pkg))
(namep (make-symbl `(,',name p) pkg))
(type (cond ((equal ,min 0) 'acl2s::nat)
((< 0 ,min) 'acl2s::pos)
((<= ,max 0) 'acl2s::neg)
(t 'acl2s::integer)))
(pred (make-symbl `(,type p) pkg))
(rng `(and (,pred a)
(<= ,,min a)
(< a ,,max))))
`(progn
(defdata ,',name (range integer (,,min <= _ < ,,max)))
(defdata-subtype ,',name ,type :strictp t)
(defthm ,th1
(implies (,namep a) ,rng)
:rule-classes ((:forward-chaining)))
(defthm ,th2
(implies ,rng (,namep a))
:rule-classes ((:rewrite :backchain-limit-lst 1)))
(defthm ,th3
(equal (,namep a) ,rng)
:rule-classes :compound-recognizer)
(in-theory (disable ,namep))))))
|#
(defmacro defnatrange (name max)
"Define a datatype that includes all nats < max"
(declare (xargs :guard (symbolp name)))
`(defintrange ,name 0 ,max))
#|
:trans1 (defintrange foo1 0 1)
:trans1 (defintrange foo2 0 100)
:trans1 (defintrange foo3 2 100)
:trans1 (defintrange foo4 -100 0)
:trans1 (defintrange foo5 -2 100)
:trans1 (defintrange foo5 -2 (expt 2 10))
(defintrange foo1 0 1)
(defintrange foo2 0 100)
(defintrange foo3 2 100)
(defintrange foo4 -100 0)
(defintrange foo5 -2 100)
(defintrange foo5 -2 (expt 2 10))
|#
|
