From 17d870abb0f5a6062cf157e284a22bc5fd321707 Mon Sep 17 00:00:00 2001
From: hondet <gabrielhondet@gmail.com>
Date: Thu, 14 Oct 2021 10:31:01 +0200
Subject: [PATCH] use pvs singleton?
---
exporter/pp-dk3.lisp | 10 +++++-----
exporter/utils.lisp | 8 +++-----
2 files changed, 8 insertions(+), 10 deletions(-)
diff --git a/exporter/pp-dk3.lisp b/exporter/pp-dk3.lisp
index 5e14025..73812c5 100644
--- a/exporter/pp-dk3.lisp
+++ b/exporter/pp-dk3.lisp
@@ -282,7 +282,7 @@ a function name from where the debug is called)."
(declaim (ftype (function (arg) (or type-expr dep-binding)) type-formal))
(defun type-formal (arg &optional (ctx *ctx*))
"Give the type of argument ARG."
- (if (single arg)
+ (if (singleton? arg)
(type-with-ctx (car arg) ctx)
(make-tupletype (mapcar (lambda (e) (type-with-ctx e ctx)) arg))))
@@ -292,8 +292,8 @@ a function name from where the debug is called)."
something) into a proper term."
(cond
((atom arg) arg)
- ((and (consp arg) (not (single arg))) (make!-tuple-expr arg))
- ((single arg) (car arg))
+ ((and (consp arg) (not (singleton? arg))) (make!-tuple-expr arg))
+ ((singleton? arg) (car arg))
(t (error "Ill-formed argument ~a" arg))))
(declaim (ftype (function (var-decl) *) handle-var-decl))
@@ -409,7 +409,7 @@ fmtypes. For any i, if the ith element of FORMALS is a list of length l, then
the ith element of FMTYPES is a tuple type of length l."
(if (endp formals)
(if (functionp ex) (funcall ex stream wrap) (pp-dk stream ex wrap))
- (if (single (car formals))
+ (if (singleton? (car formals))
(flet ((ppfm (s colon-p)
(pprint-formals ex (cdr formals) (cdr fmtypes) s)))
(assert (expr? (caar formals)))
@@ -855,7 +855,7 @@ name resolution"
to its first element."
(with-slots (bindings expression) ex
(if
- (single bindings)
+ (singleton? bindings)
;; If there is only one binding, it represents a variable
(pprint-abstraction expression bindings stream :wrap colon-p)
;; Otherwise, each variable of the binding is the component of a tuple
diff --git a/exporter/utils.lisp b/exporter/utils.lisp
index 497e5e0..ab4e784 100644
--- a/exporter/utils.lisp
+++ b/exporter/utils.lisp
@@ -1,15 +1,13 @@
(in-package :pvs)
-(export '(append1 single double mkstr symb lrec aif acond))
+(export '(append1 double mkstr symb lrec aif acond))
+(proclaim '(inline append1 double))
(defun append1 (lst obj)
(append lst (list obj)))
-(defun single (lst)
- (and (consp lst) (not (cdr lst))))
-
(defun double (lst)
- (and (consp lst) (single (cdr lst))))
+ (and (consp lst) (singleton? (cdr lst))))
(defun mkstr (&rest args)
(with-output-to-string (s)
--
GitLab