/usr/share/acl2-7.2dfsg/books/misc/hons-help2.lisp is in acl2-books-source 7.2dfsg-3.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
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 | ; Copyright (C) 2013, Regents of the University of Texas
; Written by Bob Boyer and Warren A. Hunt, Jr. (some years before that)
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
; Abbreviations from Bob Boyer and Warren Hunt for hons.
(in-package "ACL2")
(include-book "hons-help")
(defmacro def-macro-alias (mac fn arity-or-args)
(let ((args (if (integerp arity-or-args)
(make-var-lst 'x arity-or-args)
arity-or-args)))
`(progn (defmacro ,mac ,args
(list (quote ,fn) ,@(remove1-eq '&optional args)))
; Could call add-binop for arity 2. Or better yet, modify ACL2 so
; that untranslate is sensitive to something like the
; macro-aliases-table.
(add-macro-alias ,mac ,fn))))
; Primitives:
(def-macro-alias hqual hons-equal 2)
(def-macro-alias hopy hons-copy 1)
(def-macro-alias assoc-hqual hons-assoc-equal 2)
(def-macro-alias het hons-get (x a))
(def-macro-alias hut hons-acons 3)
(def-macro-alias hshrink-alist hons-shrink-alist 2)
; From hons-help.lisp:
(defmacro hist (&rest x)
`(hons-list ,@x))
(defmacro hist* (&rest x)
`(hons-list* ,@x))
;; [Jared]: Removed these
;; (def-macro-alias hen1 hons-len1 2)
;; (def-macro-alias hen hons-len 1)
;; (def-macro-alias hetprop hons-getprop 3)
;; (def-macro-alias hutprop hons-putprop 4)
;; (def-macro-alias hmerge-sort hons-merge-sort 2)
;; (def-macro-alias hhshrink-alist hons-shrink-alist! 2)
;; (def-macro-alias hopy-r hons-copy-r 1)
;; (def-macro-alias hopy-list-r hons-copy-list-r 1)
;; (def-macro-alias member-hqual hons-member-equal 2)
;; (def-macro-alias binary-hppend hons-binary-append 2)
;; (def-macro-alias hunion hons-union 2)
;; (def-macro-alias heverse hons-reverse 1)
;; (def-macro-alias hut-list hons-put-list 3)
;; (def-macro-alias hintersection hons-intersection 2)
;; (def-macro-alias revhppend hons-revappend 2)
;; (defmacro hppend (&rest args) `(hons-append ,@args))
;; (def-macro-alias hhut hons-acons! 3)
|