This file is indexed.

/usr/share/hol88-2.02.19940316/lisp/f-macro.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
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;                             HOL 88 Version 2.0                          ;;;
;;;                                                                         ;;;
;;;   FILE NAME:        f-macro.l                                           ;;;
;;;                                                                         ;;;
;;;   DESCRIPTION:      Macros for the LCF system                           ;;;
;;;                                                                         ;;;
;;;   USES FILES:       f-franz.l (or f-cl.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")
   (macros t))


;;; expand a function call
;;;  (function f)    --->    (f arg1 ... argn)
;;;  others           --->    (funcall fun arg1 ... argn)

(defun call-fun (fun args)
   (cond
      ((or (atom fun) (not (member (car fun) '(function quote))))
         `(funcall ,fun ,@args))
      (t `(,(cadr fun) ,@args))))


;;; Print a constant string, computing length at compile-time
;;; for this use flatc rather than flatsize2, 
;;; since flatc is standard Franz while flatsize2 is flatc with a bug fixed
;;; the flatc bug concerns bignums, which do not concern this macro

(defmacro ptoken (str)
   `(pstringlen ',str ,(flatc str)))

(defmacro failwith (tok)
   `(throw-from evaluation ,tok))

(defmacro msg-failwith (tok . msgs)
   ;; fail with appended error message
   `(throw-from evaluation (concat ,tok " -- " . ,msgs)))

(defmacro cond-failwith (tok . code)
   ;; fail if any of the error messages are not nil
   `(let ((msg (or . ,code)))
      (cond
         (msg (throw-from evaluation (concat ,tok " -- " msg))))))

(defmacro failtrap (failfun . trycode)
   ;; ML failure trapping :  trycode ?\tok failfun
   (let ((x (gensym)))
      `((lambda (,x)
            (cond
               ((atom ,x) ,(call-fun failfun (list x)))
               (t (car ,x))))
         (catch-throw evaluation (list (progn . ,trycode))))))

(defmacro errortrap (errorfun . trycode)
   ;; Lisp error trapping 
   (let ((x (gensym)))
      `((lambda (,x)
            (cond ((atom ,x) ,(call-fun errorfun (list x)))
               (t (car ,x))))
         (errset (progn . ,trycode)))))


;;; Apply the function to successive list elements and return the first
;;; non-nil value. If none, return nil

(defmacro exists (fun . lists)
   (let ((vars (mapcar #'(lambda (ignore) (gensym)) lists)))
      (let
         ((inits (mapcar #'(lambda (v l) `(,v ,l (cdr ,v))) vars lists))
            (args (mapcar #'(lambda (v) `(car ,v)) vars)))
         `(do ,inits ((null ,(car vars)) nil)
            (cond (,(call-fun fun args) (return (list ,@args))))))))


(defmacro forall (fun . lists)
   (let ((vars (mapcar #'(lambda (ignore) (gensym)) lists)))
      (let
         ((inits (mapcar #'(lambda (v l) `(,v ,l (cdr ,v))) vars lists))
            (args (mapcar #'(lambda (v) `(car ,v)) vars)))
         `(do ,inits ((null ,(car vars)) t)
            (cond (,(call-fun fun args)) ((return nil)))))))


(defmacro dml (ml-fn n lisp-fn mty)
   `(eval-when (load)
      (declare-ml-fun (quote ,ml-fn) (quote ,n) (quote ,lisp-fn)
         (quote ,mty))))

(defmacro dmlc (id exp mty)
   `(eval-when (load)
      (declare-ml-const (quote ,id) (quote ,exp) (quote ,mty))))