/usr/share/hol88-2.02.19940316/lisp/genmacs.l is in hol88-source 2.02.19940316-28.
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 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 | ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; HOL 88 Version 2.0 ;;;
;;; ;;;
;;; FILE NAME: genmacs.l ;;;
;;; ;;;
;;; DESCRIPTION: General-purpose macros ;;;
;;; ;;;
;;; USES FILES: f-franz.l (or f-cl.l), f-macro.l, f-ol-rec.l ;;;
;;; ;;;
;;; University of Cambridge ;;;
;;; Hardware Verification Group ;;;
;;; Computer Laboratory ;;;
;;; New Museums Site ;;;
;;; Pembroke Street ;;;
;;; Cambridge CB2 3QG ;;;
;;; England ;;;
;;; ;;;
;;; COPYRIGHT: University of Edinburgh ;;;
;;; COPYRIGHT: University of Cambridge ;;;
;;; COPYRIGHT: INRIA ;;;
;;; ;;;
;;; REVISION HISTORY: (none) ;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(eval-when (compile)
#+franz (include "lisp/f-franz")
(include "lisp/f-macro")
(include "lisp/f-ol-rec")
(macros t)
(special %show-types %empty-set))
(defmacro get-term-list (tm) `(cadr ,tm))
(defmacro make-prep-term (class term-list type)
`(cons ,class (cons ,term-list ,type)))
(defmacro atom-to-num (a)
;; (atom-to-num |n1n2...|) gives the number n1n2...
#+franz `(readlist (explodec ,a))
#-franz `(parse-integer (string ,a) :junk-allowed t))
(defmacro is-num-atom (a)
;; is-num-atom tests whether an atom is an atomified number
`(numberp (atom-to-num ,a)))
(defmacro null-ol-list (tm)
`(and (is-const ,tm) (eq (get-const-name ,tm) 'NIL)))
(defmacro hd-ol-list (tm)
`(get-rand (get-rator ,tm)))
(defmacro tl-ol-list (tm)
`(get-rand ,tm))
(defmacro get-ol-list-type (tm)
`(first (get-type-args (get-type ,tm))))
(defmacro null-ol-set (tm)
`(and (is-const ,tm) (eq (get-const-name ,tm) %empty-set)))
(defmacro hd-ol-set (tm)
`(get-rand (get-rator ,tm)))
(defmacro tl-ol-set (tm)
`(get-rand ,tm))
(defmacro get-ol-set-type (tm)
`(first (get-type-args (get-type ,tm))))
(defmacro is-pair (tm)
`(and (is-comb ,tm)
(is-comb (get-rator ,tm))
(is-const (get-rator (get-rator ,tm)))
(eq (get-const-name (get-rator (get-rator ,tm))) '|,|)))
(defmacro is-triple (tm) `(and (is-pair ,tm) (is-pair (get-snd ,tm))))
(defmacro get-fst (tm) `(get-rand (get-rator ,tm)))
(defmacro get-snd (tm) `(get-rand ,tm))
(defmacro get-thrd (tm) `(get-snd (get-snd ,tm)))
|