← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/data-structures/memories/private.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/data-structures/memories/private.lisp
42
42
; of other libraries.
43
43
 
44
44
(in-package "MEM")
45
 
(include-book "../doc-section")
46
 
 
47
 
(defdoc private
48
 
  ":Doc-Section acl2::data-structures
49
 
  redundantly define, then serverely restrict the usage of some function~/
50
 
  ~bv[]
51
 
  Example:
52
 
     (private foo (x y) 
53
 
        (if (atom x) 
 
45
(include-book "xdoc/top" :dir :system)
 
46
 
 
47
(defxdoc private
 
48
  :parents (memory)
 
49
  :short "Redundantly define, then serverely restrict the usage of some function."
 
50
  :long "<p>Example:</p>
 
51
 
 
52
@({
 
53
     (private foo (x y)
 
54
        (if (atom x)
54
55
            ...))
55
 
  ~ev[]
56
 
  ~c[private] is a macro which may be useful for authors of libraries, or
57
 
  to users who want to enforce severe discipline upon themselves.~/
58
 
 
59
 
  The macro is similar to defund (~l[defund]) in that it first introduces
60
 
  a defun and then immediately disables its definition.  However, ~c[private]
61
 
  goes further -- it also disables the resulting type-prescription rule and 
62
 
  sets up theory invariants that prohibit the user from ever enabling the 
63
 
  definition or the type prescription.
64
 
 
65
 
  Why would we want such a thing?  A nice way to develop libraries is to use
66
 
  redundant definitions (~l[set-enforce-redundancy]) in an interface file, 
67
 
  so that users never even see the local lemmas and so forth that you used
68
 
  to get the proofs to go through.  This gives you the freedom to change 
69
 
  and remove those definitions at will.
70
 
 
71
 
  Unfortunately, you cannot do the same for functions, because ACL2 needs
72
 
  the functions available in the interface book if they are ever used.  With
73
 
  ~c[private], you can identify functions that you want to keep control over
74
 
  and that the user should either (1) not be using at all, or (2) only be
75
 
  reasoning about using the theorems your have provided.
76
 
 
77
 
  To use private, simply copy your ~c[(defun foo ...)] form into your interface
78
 
  file, then replace ~c[defun] with ~c[private].")
 
56
})
 
57
 
 
58
<p>@('private') is a macro which may be useful for authors of libraries, or to
 
59
users who want to enforce severe discipline upon themselves.</p>
 
60
 
 
61
<p>The macro is similar to @(see defund) in that it first introduces a defun
 
62
and then immediately disables its definition.  However, @('private') goes
 
63
further: it also disables the resulting type-prescription rule and sets up
 
64
@(see theory-invariant)s that prohibit the user from ever enabling the
 
65
definition or the type prescription.</p>
 
66
 
 
67
<p>Why would we want such a thing?  A nice way to develop libraries is to use
 
68
@(see redundant-events) in an interface file, so that users never even see the
 
69
local lemmas and so forth that you used to get the proofs to go through.  This
 
70
gives you the freedom to change and remove those definitions at will.</p>
 
71
 
 
72
<p>Unfortunately, you cannot do the same for functions, because ACL2 needs the
 
73
functions available in the interface book if they are ever used.  With
 
74
@('private'), you can identify functions that you want to keep control over and
 
75
that the user should either (1) not be using at all, or (2) only be reasoning
 
76
about using the theorems your have provided.</p>
 
77
 
 
78
<p>To use private, simply copy your @('(defun foo ...)') form into your
 
79
interface file, then replace @('defun') with @('private').</p>")
79
80
 
80
81
(defmacro private (&rest def)
81
82
  (declare (xargs :guard (and (true-listp def)
82
83
                              (symbolp (car def))
83
84
                              (symbol-listp (cadr def)))))
84
 
  `(progn 
 
85
  `(progn
85
86
 
86
87
     ;; First introduce the function itself
87
88
     (defun ,@def)
88
89
 
89
90
     ;; Now disable the :definition and :type-prescription rules
90
 
     (with-output :off summary 
 
91
     (with-output :off summary
91
92
                  (in-theory (disable (:definition ,(car def))
92
93
                                      (:type-prescription ,(car def)))))
93
94
 
94
95
     ;; Now create a theory invariant named foo-is-private, which will cause an
95
96
     ;; error if the user ever tries to enable these rules
96
97
     (with-output :off summary
97
 
                  (theory-invariant 
 
98
                  (theory-invariant
98
99
                   (and (not (active-runep '(:definition ,(car def))))
99
100
                        (not (active-runep '(:type-prescription ,(car def)))))
100
101
                   :key ,(intern-in-package-of-symbol