From f71b8c7ed40ad53434d5ae9e5de4f6f5ad0b078b Mon Sep 17 00:00:00 2001
From: hondet <gabrielhondet@gmail.com>
Date: Tue, 19 Oct 2021 12:51:23 +0200
Subject: [PATCH] use functions rather than macros
---
tools/load-personoj.lisp | 11 ++++-------
tools/load-pvs.lisp | 21 +++++++++------------
2 files changed, 13 insertions(+), 19 deletions(-)
diff --git a/tools/load-personoj.lisp b/tools/load-personoj.lisp
index 6e91d84..b0e571c 100644
--- a/tools/load-personoj.lisp
+++ b/tools/load-personoj.lisp
@@ -1,14 +1,11 @@
-;;;; Call (load-personoj) from ~/.pvs.lisp to load Personoj automatically into
-;;;; PVS
-
-(defmacro load-personoj (&optional pth)
+(defun load-personoj (&optional pth)
"Load Personoj specification exporter and proof exporter. If given, PTH is the
path to the root of the repository. Otherwise, the root is taken from the
environment variable PERSONOJ"
(let ((pth (cond
- (pth pth)
+ (pth (uiop:ensure-pathname pth))
((uiop:getenvp "PERSONOJPATH")
(uiop:getenv-pathname "PERSONOJPATH" :ensure-directory t))
(t (error "Cannot load personoj: PERSONOJPATH not set.")))))
- `(uiop:with-current-directory (,pth)
- (load "load.lisp"))))
+ (uiop:with-current-directory (pth)
+ (load "load.lisp"))))
diff --git a/tools/load-pvs.lisp b/tools/load-pvs.lisp
index f8dfe47..483d9b4 100644
--- a/tools/load-pvs.lisp
+++ b/tools/load-pvs.lisp
@@ -1,15 +1,12 @@
-;;; Place the following definitions into "~/.sbclrc" to be able to load PVS into
-;;; any sbcl session.
-(defmacro load-pvs (&optional pvspath)
+(defun load-pvs (&optional pvspath)
"Load PVS into the current lisp environment. Argument PVSPATH is the filespec
to the sources of PVS. If not provided, it is fetched from the environment
variables PVSPATH."
- (let (($pvspath (gensym)))
- `(let ((,$pvspath
- (cond
- (,pvspath ,pvspath)
- ((uiop:getenvp "PVSPATH") (uiop:getenv-pathname "PVSPATH"))
- (t (error "Cannot load PVS: PVSPATH not set.")))))
- (uiop:with-current-directory (,$pvspath)
- (load "pvs.system")
- (uiop:symbol-call :make "OPERATE-ON-SYSTEM" :pvs :load)))))
+ (let ((pvspath
+ (cond
+ (pvspath (uiop:ensure-pathname pvspath))
+ ((uiop:getenvp "PVSPATH") (uiop:getenv-pathname "PVSPATH"))
+ (t (error "Cannot load PVS: PVSPATH not set.")))))
+ (uiop:with-current-directory (pvspath)
+ (load "pvs.system")
+ (uiop:symbol-call :make "OPERATE-ON-SYSTEM" :pvs :load))))
--
GitLab