From 4efdc47f116aab7fbde2059f60967e59b2178ee9 Mon Sep 17 00:00:00 2001
From: Gabriel <gabriel@motacilla.home>
Date: Mon, 18 Oct 2021 13:30:16 +0200
Subject: [PATCH] printing derivation as tptp
---
proofs/{proof-gen.lisp => proof-json.lisp} | 46 +++++++---------------
proofs/tptp.lisp | 43 ++++++++++++++++++--
pvs-load.lisp | 2 +-
3 files changed, 55 insertions(+), 36 deletions(-)
rename proofs/{proof-gen.lisp => proof-json.lisp} (70%)
diff --git a/proofs/proof-gen.lisp b/proofs/proof-json.lisp
similarity index 70%
rename from proofs/proof-gen.lisp
rename to proofs/proof-json.lisp
index 341df92..7af60e7 100644
--- a/proofs/proof-gen.lisp
+++ b/proofs/proof-json.lisp
@@ -1,34 +1,34 @@
-(in-package :pvs)
-
;;; JSON creation: output proofstates as json structures.
+(in-package :pvs)
+
;; Note that this has the side effect of setting the view of the sform,
;; Which is a cons of the string and its view (computed lazily).
(defun pvs2json-sform (sform fnum par-sforms)
(let* ((nf (formula sform))
- (frm (if (negation? nf) (args1 nf) nf)))
+ (frm (if (negation? nf) (args1 nf) nf)))
(unless (view sform)
(multiple-value-bind (frmstr frmview)
- (pp-with-view frm *proofstate-indent* *proofstate-width*)
- (setf (view sform) (list frmstr frmview))))
+ (pp-with-view frm *proofstate-indent* *proofstate-width*)
+ (setf (view sform) (list frmstr frmview))))
(let ((names-info (names-info-proof-formula sform)))
`(("labels" . ,(cons fnum (label sform)))
- ("changed" . ,(if (memq sform par-sforms) "false" "true"))
- ("formula" . ,(car (view sform)))))))
+ ("changed" . ,(if (memq sform par-sforms) "false" "true"))
+ ("formula" . ,(car (view sform)))))))
(defun pvs2json-sforms (sforms neg? par-sforms)
(let ((c 0))
(mapcar #'(lambda (sf)
- (let* ((fnum (if neg? (- (incf c)) (incf c))))
- (pvs2json-sform sf fnum par-sforms)))
- sforms)))
+ (let* ((fnum (if neg? (- (incf c)) (incf c))))
+ (pvs2json-sform sf fnum par-sforms)))
+ sforms)))
(defmethod pvs2json-seq (seq parent-ps)
(let* ((par-sforms (when parent-ps
- (s-forms (current-goal parent-ps))))
- (hidden-s-forms (hidden-s-forms seq))
- (hn-sforms (neg-s-forms* hidden-s-forms))
- (hp-sforms (pos-s-forms* hidden-s-forms)))
+ (s-forms (current-goal parent-ps))))
+ (hidden-s-forms (hidden-s-forms seq))
+ (hn-sforms (neg-s-forms* hidden-s-forms))
+ (hp-sforms (pos-s-forms* hidden-s-forms)))
(make-seqstruct
:antecedents (pvs2json-sforms (neg-s-forms seq) t par-sforms)
:succedents (pvs2json-sforms (pos-s-forms seq) nil par-sforms)
@@ -72,21 +72,3 @@
(setq *prover-commentary* nil)))
(pushnew 'output-json-proofstate-to-stream *proofstate-hooks*)
-
-;;; TPTP export: transform sequents into TPTP clauses
-
-(defgeneric pvs->tptp (thing)
- (:documentation "Translate a THING to TPTP"))
-
-(defmethod pvs->tptp ((sform s-formula))
- (translate-to-tptp (formula sform)))
-
-(defmethod pvs->tptp ((seq sequent))
- (mapcan #'pvs->tptp (neg-s-forms seq))
- (mapcan #'pvs->tptp (pos-s-forms seq)))
-
-(defun output-tptp-proofstate-to-stream (ps)
- (let ((ps-tptp (pvs->tptp (current-goal ps))))
- (format t "~%~a~%" ps-tptp)))
-
-(pushnew 'output-tptp-proofstate-to-stream *proofstate-hooks*)
diff --git a/proofs/tptp.lisp b/proofs/tptp.lisp
index ef1a8fb..a79660b 100644
--- a/proofs/tptp.lisp
+++ b/proofs/tptp.lisp
@@ -317,7 +317,44 @@
(setq *tptp-ite-env* (cons (cons expr newsym) *tptp-ite-env*))
newsym))))
-(defun translate-to-tptp (expr)
+;;; Interface with PVS
+
+(defun translate-to-tptp (name expr &optional (role "plain") source)
+ "Transform expression EXPR to a TPTP expression as a string."
(setq *tptp-ite-env* nil)
- (format nil "fof(pvs2dk, conjecture, ~a)."
- (translate-to-tptp* expr nil)))
+ (let ((expr (translate-to-tptp* expr nil)))
+ (if source
+ (format nil "fof(~a, ~a, ~a, ~a)." name role expr source)
+ (format nil "fof(~a, ~a, ~a)." name role expr))))
+
+(defun pp-path (stream ps &optional colon-p at-sign-p)
+ (declare (ignore colon-p at-sign-p))
+ (let ((pth (path-from-top ps)))
+ (if (endp pth)
+ (princ "root" stream)
+ (format stream "~{~a~^.~}" pth))))
+
+(defgeneric pvs->tptp (thing)
+ (:documentation "Translate a THING to TPTP"))
+
+;; (neg-s-forms seq) to get the antecedents
+;; (pos-s-forms seq) to get the succedents
+
+(defmethod pvs->tptp ((ps proofstate))
+ (with-slots ((goal current-goal) (lab label) (pps parent-proofstate)) ps
+ (let* ((name (format nil "'~a ~/pvs:pp-path/'" lab ps))
+ (forms (mapcar #'formula (s-forms goal)))
+ (formula (make!-disjunction* forms))
+ (role (if pps "plain" "conjecture"))
+ (source (if pps
+ (let ((*pp-no-newlines?* t)
+ (*pp-compact* t))
+ (mkstr (current-rule pps)))
+ "file")))
+ (translate-to-tptp name formula "plain" source))))
+
+(defun output-tptp-proofstate-to-stream (ps)
+ (let ((ps-tptp (pvs->tptp ps)))
+ (format t "~%~a~%" ps-tptp)))
+
+(pushnew 'output-tptp-proofstate-to-stream *proofstate-hooks*)
diff --git a/pvs-load.lisp b/pvs-load.lisp
index 397dce5..bdb1982 100644
--- a/pvs-load.lisp
+++ b/pvs-load.lisp
@@ -3,5 +3,5 @@
(defparameter *pvs-dedukti-path* "PVSDKPATH")
(dolist (m '("utils" "packages" "dklog" "dk-sig" "dk-recursive" "pp-dk3" "pvs"))
(load (concatenate 'string *pvs-dedukti-path* "/exporter/" m ".lisp")))
-(dolist (m '("tptp" "proof-gen"))
+(dolist (m '("tptp" "proof-json"))
(load (concatenate 'string *pvs-dedukti-path* "/proofs/" m ".lisp")))
--
GitLab