From a3a528d254524bbdb36040b002ddabd7fbe85064 Mon Sep 17 00:00:00 2001
From: Gabriel <gabriel@motacilla.home>
Date: Fri, 15 Oct 2021 15:09:01 +0200
Subject: [PATCH] proof translation
---
exporter/tptp.lisp | 330 ------------------------------------------
proofs/proof-gen.lisp | 92 ++++++++++++
proofs/tptp.lisp | 323 +++++++++++++++++++++++++++++++++++++++++
pvs-load.lisp | 2 +
4 files changed, 417 insertions(+), 330 deletions(-)
delete mode 100644 exporter/tptp.lisp
create mode 100644 proofs/proof-gen.lisp
create mode 100644 proofs/tptp.lisp
diff --git a/exporter/tptp.lisp b/exporter/tptp.lisp
deleted file mode 100644
index 7cef180..0000000
--- a/exporter/tptp.lisp
+++ /dev/null
@@ -1,330 +0,0 @@
-(defvar *tptp-id-counter*)
-(defvar *tptp-ite-env*)
-
-(newcounter *tptp-id-counter*)
-
-(defparameter *metit-interpreted-names*
- '((FALSE (|booleans| . $false))
- (TRUE (|booleans| . $true))
- (IMPLIES (|booleans| . =>))
- (=> (|booleans| . =>))
- (AND (|booleans| . &))
- (& (|booleans| . &))
- (OR (|booleans| . \|))
- (NOT (|booleans| . ~))
- (IFF (|booleans| . <=>))
- (<=> (|booleans| . <=>))
- (= (|equalities| . =))
- (/= (|notequal| . /=))
- (< (|reals| . <))
- (<= (|reals| . <=))
- (> (|reals| . >))
- (>= (|reals| . >=))
- (+ (|number_fields| . +))
- (- (|number_fields| . -))
- (* (|number_fields| . *))
- (/ (|number_fields| . /))
- (^ (|exponentiation| . ^))
- (sin (|sincos_def| . sin) (|trig_basic| . sin))
- (cos (|sincos_def| . cos) (|trig_basic| . cos))
- (tan (|sincos_def| . tan) (|trig_basic| . tan))
- (pi (|atan| . pi) (|trig_basic| . pi))
- (e (|ln_exp| . "exp(1)"))
- (asin (|asin| . arcsin))
- (atan (|atan| . arctan))
- (acos (|acos| . arccos))
- (sqrt (|sqrt| . sqrt))
- (sq (|sq| . sq))
- (ln (|ln_exp| . ln))
- (exp (|ln_exp| . exp))
- (sinh (|hyperbolic| . sinh))
- (cosh (|hyperbolic| . cosh))
- (tanh (|hyperbolic| . tanh))
- (abs (|real_defs| . abs))
- (\#\# (|interval| . \#\#))
-))
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; Input is a name-expr and a list of bindings of the form
-;; (("Y" . Y2) ("X" . X1)). The bindings are set in translate-metit-bindings
-;; Since the metit-named bounded variables travel in the bindings list, when we get
-;; the named variable in an expression return the cdr that
-;; holds the variable name. Otherwise we have a constant symbol (such as pi) and call
-;; metit-interpretation.
-;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(defparameter tptp-escape nil)
-
-(defun downcase-tptp-id (id)
- (setq tptp-escape nil)
- (format nil "~{~a~}"
- (loop for char across (format nil "~a" id)
- collect
- (cond ((alpha-char-p char)
- (string (char-downcase char)))
- ((and (digit-char-p char) tptp-escape)
- (format nil "0")
- (format nil "~c" char)
- (setq tptp-escape nil))
- ((and (digit-char-p char) (not tptp-escape))
- (format nil "~c" char))
- ((equal char #\_)
- (setq tptp-escape t)
- (format nil "_"))
- (t
- (format nil "_~d_" (char-int char)))))))
-
-(defun upcase-tptp-id (id)
- (setq tptp-escape nil)
- (format nil "~{~a~}"
- (loop for char across (format nil "~a" id)
- collect
- (cond ((alpha-char-p char)
- (string-upcase (format nil "~c" char)))
- ((and (digit-char-p char) tptp-escape)
- (format nil "0")
- (format nil "~c" char)
- (setq tptp-escape nil))
- ((and (digit-char-p char) (not tptp-escape))
- (format nil "~c" char))
- ((equal char #\_)
- (setq tptp-escape t)
- (format nil "_"))
- (t
- (format nil "_~d_" (char-int char)))))))
-
-(defmethod translate-to-tptp* ((expr name-expr) env)
- (or (cond ((find (id expr) env)
- (format nil "~a" (upcase-tptp-id (id expr))))
- ;; ((is-const-decl-expr expr '("pi" "e"))
- ;; (metit-interpretation expr))
- ((assoc (id expr) *metit-interpreted-names*)
- (metit-interpretation expr))
- ;; ((is-variable-expr expr)
- ;; (cdr (assoc (id expr) bindings :test #'string=)))
- (t
- (downcase-tptp-id (format nil "~a" (id expr)))))
- (error "constant/variable ~a cannot be handled 1." expr)))
-
-;; (defmethod translate-to-tptp* ((expr fieldappl))
-;; (or (when (is-variable-expr expr)
-;; (cdr (assoc (format nil "~a" expr) bindings :test #'string=)))
-;; (error "field application ~a cannot be handled." expr)))
-
-;; (defmethod translate-to-tptp* ((expr projappl))
-;; (or (when (is-variable-expr expr)
-;; (cdr (assoc (format nil "~a" expr) bindings :test #'string=)))
-;; (error "projection ~a cannot be handled." expr)))
-
-(defmethod translate-to-tptp* ((expr decimal) env)
- (declare (ignore env))
- (format nil "(~a / ~a)" (args1 expr) (args2 expr)))
-
-(defmethod translate-to-tptp* ((expr rational-expr) env)
- (declare (ignore env))
- (if (number-expr? expr)
- (number expr)
- (let ((rat (number expr)))
- (format nil "(~a / ~a)" (numerator rat) (denominator rat)))))
-
-(defmethod translate-to-tptp* ((expr string-expr) env)
- (declare (ignore env))
- (error "string ~a cannot be handled" expr))
-
-;;
-;; The PVS variables are converted into a Tptp representation (uppercase) and are
-;; made distinct by appending *metit-id-counter*. This is required because a user
-;; might use both cases in a specification and we need to differentiate between x and X.
-;; In this case they would be converted to X1 and X2.
-;;
-
-(defun tptp-id-name ()
- (format nil "ite~a" (funcall *tptp-id-counter*)))
-
-;;
-;; (argument expr) return a tuple of the arguments of expr
-;; (args1 expr) (args2 expr) returns the first and second parts of the expr tuple
-;;
-
-(defun translate-to-tptp-list (exprs env)
- (cond ((null exprs)
- "")
- (t
- (format nil "~a"
- (translate-to-tptp-list* exprs env)))))
-
-(defun translate-to-tptp-list* (exprs env)
- (cond ((null (cdr exprs))
- (translate-to-tptp* (car exprs) env))
- (t
- (format nil "~a, ~a"
- (translate-to-tptp* (car exprs) env)
- (translate-to-tptp-list* (cdr exprs) env)))))
-
-(defmethod translate-to-tptp* ((expr tuple-expr) env)
- (translate-to-tptp-list (exprs expr) env))
-
-(defmethod translate-to-tptp* ((expr application) env)
- (with-slots (operator argument) expr
- (if (name-expr? operator)
- (let* ((op-id (metit-interpretation operator)))
- (case op-id
- (~ (format nil "(~~ ~a)" (translate-to-tptp* (argument expr) env)))
- ((<=>)
- (let ((arg1 (translate-to-tptp* (args1 expr) env))
- (arg2 (translate-to-tptp* (args2 expr) env)))
- (format nil "((~a => ~a) & (~a => ~a))" arg1 arg2 arg2 arg1)))
- (^
- (format nil "~a~a~a" (translate-to-tptp* (args1 expr) env)
- op-id (translate-to-tptp* (args2 expr) env)))
- ((sq)
- (format nil "~a^2" (translate-to-tptp* (argument expr) env)))
- ((sin cos tan sqrt tanh cosh sinh ln exp abs arctan)
- (format nil "~a(~a)" op-id (translate-to-tptp* (argument expr) env)))
- (-
- (if (unary-application? expr)
- (format nil "-~a" (translate-to-tptp* (argument expr) env))
- (format nil "(~a ~a ~a)"
- (translate-to-tptp* (args1 expr) env)
- op-id
- (translate-to-tptp* (args2 expr) env))))
- ((/=)
- (format nil "(~a < ~a | ~a > ~a)"
- (translate-to-tptp* (args1 expr) env)
- (translate-to-tptp* (args2 expr) env)
- (translate-to-tptp* (args1 expr) env)
- (translate-to-tptp* (args2 expr) env)))
- ((=)
- (if (and (type-name? (car (types (domain (type (operator expr))))))
- (or (eq (id (car (types (domain (type (operator expr)))))) 'bool)
- (eq (id (car (types (domain (type (operator expr)))))) 'boolean)))
- (format nil "(~a ~a ~a)"
- (translate-to-tptp* (args1 expr) env)
- '<=>
- (translate-to-tptp* (args2 expr) env))
- (format nil "(~a ~a ~a)"
- (translate-to-tptp* (args1 expr) env)
- op-id
- (translate-to-tptp* (args2 expr) env))))
- ((< <= > >= + * / => & \|)
- (format nil "(~a ~a ~a)"
- (translate-to-tptp* (args1 expr) env)
- op-id
- (translate-to-tptp* (args2 expr) env)))
- ((\#\#)
- (format nil "(~a <= ~a & ~a <= ~a)"
- (translate-to-tptp* (args1 (args2 expr)) env)
- (translate-to-tptp* (args1 expr) env)
- (translate-to-tptp* (args1 expr) env)
- (translate-to-tptp* (args2 (args2 expr)) env)))
- (t
- (cond ((eq (id operator) 'IF)
- (translate-to-tptp* (mk-if-expr (car (exprs (argument expr)))
- (cadr (exprs (argument expr)))
- (caddr (exprs (argument expr))))
- env))
- ((and (name-expr? (operator expr))
- (find (id (operator expr)) env))
- (format nil "app(~a)"
- (translate-to-tptp-list (list (operator expr) (argument expr)) env)))
- (t
- (format nil "~a(~a)"
- (translate-to-tptp* (operator expr) env)
- (translate-to-tptp* (argument expr) env))))
- ;; (error "expression ~a cannot be handled." expr)
- )))
- (error "expression ~a cannot be handled 2." operator))))
-
-;;
-;; translate-metit-bindings : Go through a list of bind declarations and create a
-;; bind list with their new metit names. tc-eq ensures we only have real variables.
-;;
-
-;; (defun translate-metit-bindings (bind-decls bindings accum)
-;; (cond ((consp bind-decls)
-;; (if (tc-eq (type (car bind-decls)) *real*)
-;; (let ((yname (metit-id-name (id (car bind-decls)))))
-;; (translate-metit-bindings (cdr bind-decls) ;;making bindings here
-;; (cons (cons (string (id (car bind-decls)))
-;; yname)
-;; )
-;; (cons yname accum)))
-;; (error "type of ~a must be real." (id (car bind-decls)))))
-;; (t (values bindings (nreverse accum)))))
-
-;;
-;; metit-interpretation : Translate pvs symbol to the Tptp representation. Ensures
-;; that the resolution (the real meaning of the symbol) is what we want. This is due
-;; to the massive overloading in PVS (anything can be overloaded).
-;; Answers the question: is + actually the + for the reals?
-;;
-
-(defun metit-interpretation (name-expr)
- (assert (name-expr? name-expr))
- (let* ((id-assoc (cdr (assoc (id name-expr) *metit-interpreted-names*)))
- (mod-assoc (cdr (assoc (id (module-instance
- (resolution name-expr)))
- id-assoc))))
- mod-assoc))
-
-(defmethod translate-to-tptp* ((expr binding-expr) env)
- (declare (ignore env))
- (error "expression ~a cannot be handled 3." expr))
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; lift-predicates-in-quantifier takes the constraints on the variables (p1 : posreal)
-;; and converts it into the proper logical form p1 > 0 & p1 >= 0 and returns
-;; a new expression with these propositional atoms in the antecedent
-;;
-;; The we recursively call translate-metit-bindings to build a cons list of bindvars
-;; ((p1 : real. P11))
-;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(defmethod translate-to-tptp* ((expr quant-expr) env)
- ;; (let ((new-expr (lift-predicates-in-quantifier expr (list *real*))))
- (with-slots
- (bindings expression) expr
- ;; (multiple-value-bind (newbindings bindvars)
- ;; (translate-metit-bindings expr-bindings bindings nil)
- (let ((yexpression (translate-to-tptp* expression (append (mapcar #'id bindings) env))))
- (cond ((forall-expr? expr)
- (format nil "(![~{~a~^, ~}]: ~a)" (mapcar #'upcase-tptp-id (mapcar #'id bindings))
- yexpression))
- ((exists-expr? expr)
- (format nil "(?[~{~a~^, ~}]: ~a)" (mapcar #'upcase-tptp-id (mapcar #'id bindings))
- yexpression)))))) ;;no else case
-
-(defmethod translate-to-tptp* ((expr if-expr) env)
- (if (and (type-name? (type expr))
- (or (eq (id (type expr)) 'bool)
- (eq (id (type expr)) 'boolean)))
- (let ((condexpr (translate-to-tptp* (nth 0 (arguments expr)) env)))
- (format nil "((~a => ~a) & ((~~ ~a) => ~a))"
- condexpr
- (translate-to-tptp* (nth 1 (arguments expr)) env)
- condexpr
- (translate-to-tptp* (nth 2 (arguments expr)) env)))
- (if (assoc expr *tptp-ite-env* :test #'tc-eq)
- (cdr (assoc expr *tptp-ite-env* :test #'tc-eq))
- (let ((newsym (tptp-id-name)))
- (setq *tptp-ite-env* (cons (cons expr newsym) *tptp-ite-env*))
- newsym))))
-
-(defmethod translate-to-tptp* :around (expr env)
- (declare (ignore expr env))
- ;; (format t "TEST: ~a~%~%" expr)
- (call-next-method))
-
-(defun translate-to-tptp (expr source)
- (setq *tptp-ite-env* nil)
- (if (or ;; (eq source 'decision-procedure)
- (eq source 'lift-if)
- (eq source 'typepred))
- (format nil "%fof(pvs2metit,conjecture, ~a)."
- (translate-to-tptp* expr nil))
- (format nil "fof(pvs2metit,conjecture, ~a)."
- (translate-to-tptp* expr nil))))
diff --git a/proofs/proof-gen.lisp b/proofs/proof-gen.lisp
new file mode 100644
index 0000000..341df92
--- /dev/null
+++ b/proofs/proof-gen.lisp
@@ -0,0 +1,92 @@
+(in-package :pvs)
+
+;;; JSON creation: output proofstates as json structures.
+
+;; 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)))
+ (unless (view sform)
+ (multiple-value-bind (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)))))))
+
+(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)))
+
+(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)))
+ (make-seqstruct
+ :antecedents (pvs2json-sforms (neg-s-forms seq) t par-sforms)
+ :succedents (pvs2json-sforms (pos-s-forms seq) nil par-sforms)
+ :hidden-antecedents (pvs2json-sforms hn-sforms t par-sforms)
+ :hidden-succedents (pvs2json-sforms hp-sforms nil par-sforms)
+ :info nil)))
+
+(defmethod pvs2json ((ps proofstate))
+ (with-slots (label comment current-goal (pps parent-proofstate)) ps
+ (let ((sequent (pvs2json-seq current-goal pps))
+ (prev-cmd (let ((wish-rule (wish-current-rule ps))
+ (parent-ps (parent-proofstate ps)))
+ (cond (wish-rule (format nil "~s" wish-rule))
+ (parent-ps (format nil "~s" (current-rule parent-ps)))
+ (t nil)))))
+ `(("label" . ,label)
+ ,@(when prev-cmd `(("prev-cmd" . ,prev-cmd)))
+ ("path" . ,(format nil "~{~a~^.~}" (path-from-top ps)))
+ ("sequent" . ,sequent)))))
+
+(setq *suppress-msg* t)
+(setq *suppress-printing* t)
+(setq *pvs-message-hook* nil)
+
+(defun rerun-prove (decl)
+ (if (and *noninteractive*
+ (integerp *pvs-verbose*)
+ (> *pvs-verbose* 2))
+ (let ((*suppress-printing* t) ;; <- printing supressed even when *noninteractive* and verbose
+ (*proving-tcc* t))
+ (prove-decl decl :strategy `(then (then (rerun) (postpone)) (quit))))
+ (let ((*suppress-printing* t)
+ (*printproofstate* nil)
+ (*proving-tcc* t))
+ (prove-decl decl :strategy `(then (then (rerun) (postpone)) (quit))))))
+
+(defun output-json-proofstate-to-stream (ps)
+ (let* ((json:*lisp-identifier-name-to-json* #'identity)
+ (ps-json (pvs:pvs2json ps)))
+ (format t "~&~a~%" (json:encode-json-to-string ps-json))
+ (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
new file mode 100644
index 0000000..ef1a8fb
--- /dev/null
+++ b/proofs/tptp.lisp
@@ -0,0 +1,323 @@
+;;;; Translate PVS formulae to TPTP.
+
+(in-package :pvs)
+
+(defvar *tptp-id-counter*)
+(defvar *tptp-ite-env*)
+
+(newcounter *tptp-id-counter*)
+
+(defparameter *metit-interpreted-names*
+ '((FALSE (|booleans| . $false))
+ (TRUE (|booleans| . $true))
+ (IMPLIES (|booleans| . =>))
+ (=> (|booleans| . =>))
+ (AND (|booleans| . &))
+ (& (|booleans| . &))
+ (OR (|booleans| . \|))
+ (NOT (|booleans| . ~))
+ (IFF (|booleans| . <=>))
+ (<=> (|booleans| . <=>))
+ (= (|equalities| . =))
+ (/= (|notequal| . /=))
+ (< (|reals| . <))
+ (<= (|reals| . <=))
+ (> (|reals| . >))
+ (>= (|reals| . >=))
+ (+ (|number_fields| . +))
+ (- (|number_fields| . -))
+ (* (|number_fields| . *))
+ (/ (|number_fields| . /))
+ (^ (|exponentiation| . ^))
+ (sin (|sincos_def| . sin) (|trig_basic| . sin))
+ (cos (|sincos_def| . cos) (|trig_basic| . cos))
+ (tan (|sincos_def| . tan) (|trig_basic| . tan))
+ (pi (|atan| . pi) (|trig_basic| . pi))
+ (e (|ln_exp| . "exp(1)"))
+ (asin (|asin| . arcsin))
+ (atan (|atan| . arctan))
+ (acos (|acos| . arccos))
+ (sqrt (|sqrt| . sqrt))
+ (sq (|sq| . sq))
+ (ln (|ln_exp| . ln))
+ (exp (|ln_exp| . exp))
+ (sinh (|hyperbolic| . sinh))
+ (cosh (|hyperbolic| . cosh))
+ (tanh (|hyperbolic| . tanh))
+ (abs (|real_defs| . abs))
+ (\#\# (|interval| . \#\#))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; Input is a name-expr and a list of bindings of the form
+;; (("Y" . Y2) ("X" . X1)). The bindings are set in translate-metit-bindings
+;; Since the metit-named bounded variables travel in the bindings list, when we get
+;; the named variable in an expression return the cdr that
+;; holds the variable name. Otherwise we have a constant symbol (such as pi) and call
+;; metit-interpretation.
+;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(defparameter tptp-escape nil)
+
+(defun downcase-tptp-id (id)
+ (setq tptp-escape nil)
+ (format nil "~{~a~}"
+ (loop for char across (format nil "~a" id)
+ collect
+ (cond ((alpha-char-p char)
+ (string (char-downcase char)))
+ ((and (digit-char-p char) tptp-escape)
+ (format nil "0")
+ (format nil "~c" char)
+ (setq tptp-escape nil))
+ ((and (digit-char-p char) (not tptp-escape))
+ (format nil "~c" char))
+ ((equal char #\_)
+ (setq tptp-escape t)
+ (format nil "_"))
+ (t
+ (format nil "_~d_" (char-int char)))))))
+
+(defun upcase-tptp-id (id)
+ (setq tptp-escape nil)
+ (format nil "~{~a~}"
+ (loop for char across (format nil "~a" id)
+ collect
+ (cond ((alpha-char-p char)
+ (string-upcase (format nil "~c" char)))
+ ((and (digit-char-p char) tptp-escape)
+ (format nil "0")
+ (format nil "~c" char)
+ (setq tptp-escape nil))
+ ((and (digit-char-p char) (not tptp-escape))
+ (format nil "~c" char))
+ ((equal char #\_)
+ (setq tptp-escape t)
+ (format nil "_"))
+ (t
+ (format nil "_~d_" (char-int char)))))))
+
+(defmethod translate-to-tptp* ((expr name-expr) env)
+ (or (cond ((find (id expr) env)
+ (format nil "~a" (upcase-tptp-id (id expr))))
+ ;; ((is-const-decl-expr expr '("pi" "e"))
+ ;; (metit-interpretation expr))
+ ((assoc (id expr) *metit-interpreted-names*)
+ (metit-interpretation expr))
+ ;; ((is-variable-expr expr)
+ ;; (cdr (assoc (id expr) bindings :test #'string=)))
+ (t
+ (downcase-tptp-id (format nil "~a" (id expr)))))
+ (error "constant/variable ~a cannot be handled 1." expr)))
+
+;; (defmethod translate-to-tptp* ((expr fieldappl))
+;; (or (when (is-variable-expr expr)
+;; (cdr (assoc (format nil "~a" expr) bindings :test #'string=)))
+;; (error "field application ~a cannot be handled." expr)))
+
+;; (defmethod translate-to-tptp* ((expr projappl))
+;; (or (when (is-variable-expr expr)
+;; (cdr (assoc (format nil "~a" expr) bindings :test #'string=)))
+;; (error "projection ~a cannot be handled." expr)))
+
+(defmethod translate-to-tptp* ((expr decimal) env)
+ (declare (ignore env))
+ (format nil "(~a / ~a)" (args1 expr) (args2 expr)))
+
+(defmethod translate-to-tptp* ((expr rational-expr) env)
+ (declare (ignore env))
+ (if (number-expr? expr)
+ (number expr)
+ (let ((rat (number expr)))
+ (format nil "(~a / ~a)" (numerator rat) (denominator rat)))))
+
+(defmethod translate-to-tptp* ((expr string-expr) env)
+ (declare (ignore env))
+ (error "string ~a cannot be handled" expr))
+
+;;
+;; The PVS variables are converted into a Tptp representation (uppercase) and are
+;; made distinct by appending *metit-id-counter*. This is required because a user
+;; might use both cases in a specification and we need to differentiate between x and X.
+;; In this case they would be converted to X1 and X2.
+;;
+
+(defun tptp-id-name ()
+ (format nil "ite~a" (funcall *tptp-id-counter*)))
+
+;;
+;; (argument expr) return a tuple of the arguments of expr
+;; (args1 expr) (args2 expr) returns the first and second parts of the expr tuple
+;;
+
+(defun translate-to-tptp-list (exprs env)
+ (cond ((null exprs)
+ "")
+ (t
+ (format nil "~a"
+ (translate-to-tptp-list* exprs env)))))
+
+(defun translate-to-tptp-list* (exprs env)
+ (cond ((null (cdr exprs))
+ (translate-to-tptp* (car exprs) env))
+ (t
+ (format nil "~a, ~a"
+ (translate-to-tptp* (car exprs) env)
+ (translate-to-tptp-list* (cdr exprs) env)))))
+
+(defmethod translate-to-tptp* ((expr tuple-expr) env)
+ (translate-to-tptp-list (exprs expr) env))
+
+(defmethod translate-to-tptp* ((expr application) env)
+ (with-slots (operator argument) expr
+ (if (name-expr? operator)
+ (let* ((op-id (metit-interpretation operator)))
+ (case op-id
+ (~ (format nil "(~~ ~a)" (translate-to-tptp* (argument expr) env)))
+ ((<=>)
+ (let ((arg1 (translate-to-tptp* (args1 expr) env))
+ (arg2 (translate-to-tptp* (args2 expr) env)))
+ (format nil "((~a => ~a) & (~a => ~a))" arg1 arg2 arg2 arg1)))
+ (^
+ (format nil "~a~a~a" (translate-to-tptp* (args1 expr) env)
+ op-id (translate-to-tptp* (args2 expr) env)))
+ ((sq)
+ (format nil "~a^2" (translate-to-tptp* (argument expr) env)))
+ ((sin cos tan sqrt tanh cosh sinh ln exp abs arctan)
+ (format nil "~a(~a)" op-id (translate-to-tptp* (argument expr) env)))
+ (-
+ (if (unary-application? expr)
+ (format nil "-~a" (translate-to-tptp* (argument expr) env))
+ (format nil "(~a ~a ~a)"
+ (translate-to-tptp* (args1 expr) env)
+ op-id
+ (translate-to-tptp* (args2 expr) env))))
+ ((/=)
+ (format nil "(~a < ~a | ~a > ~a)"
+ (translate-to-tptp* (args1 expr) env)
+ (translate-to-tptp* (args2 expr) env)
+ (translate-to-tptp* (args1 expr) env)
+ (translate-to-tptp* (args2 expr) env)))
+ ((=)
+ (if (and (type-name? (car (types (domain (type (operator expr))))))
+ (or (eq (id (car (types (domain (type (operator expr)))))) 'bool)
+ (eq (id (car (types (domain (type (operator expr)))))) 'boolean)))
+ (format nil "(~a ~a ~a)"
+ (translate-to-tptp* (args1 expr) env)
+ '<=>
+ (translate-to-tptp* (args2 expr) env))
+ (format nil "(~a ~a ~a)"
+ (translate-to-tptp* (args1 expr) env)
+ op-id
+ (translate-to-tptp* (args2 expr) env))))
+ ((< <= > >= + * / => & \|)
+ (format nil "(~a ~a ~a)"
+ (translate-to-tptp* (args1 expr) env)
+ op-id
+ (translate-to-tptp* (args2 expr) env)))
+ ((\#\#)
+ (format nil "(~a <= ~a & ~a <= ~a)"
+ (translate-to-tptp* (args1 (args2 expr)) env)
+ (translate-to-tptp* (args1 expr) env)
+ (translate-to-tptp* (args1 expr) env)
+ (translate-to-tptp* (args2 (args2 expr)) env)))
+ (t
+ (cond ((eq (id operator) 'IF)
+ (translate-to-tptp* (mk-if-expr (car (exprs (argument expr)))
+ (cadr (exprs (argument expr)))
+ (caddr (exprs (argument expr))))
+ env))
+ ((and (name-expr? (operator expr))
+ (find (id (operator expr)) env))
+ (format nil "app(~a)"
+ (translate-to-tptp-list (list (operator expr) (argument expr)) env)))
+ (t
+ (format nil "~a(~a)"
+ (translate-to-tptp* (operator expr) env)
+ (translate-to-tptp* (argument expr) env))))
+ ;; (error "expression ~a cannot be handled." expr)
+ )))
+ (error "expression ~a cannot be handled 2." operator))))
+
+;;
+;; translate-metit-bindings : Go through a list of bind declarations and create a
+;; bind list with their new metit names. tc-eq ensures we only have real variables.
+;;
+
+;; (defun translate-metit-bindings (bind-decls bindings accum)
+;; (cond ((consp bind-decls)
+;; (if (tc-eq (type (car bind-decls)) *real*)
+;; (let ((yname (metit-id-name (id (car bind-decls)))))
+;; (translate-metit-bindings (cdr bind-decls) ;;making bindings here
+;; (cons (cons (string (id (car bind-decls)))
+;; yname)
+;; )
+;; (cons yname accum)))
+;; (error "type of ~a must be real." (id (car bind-decls)))))
+;; (t (values bindings (nreverse accum)))))
+
+;;
+;; metit-interpretation : Translate pvs symbol to the Tptp representation. Ensures
+;; that the resolution (the real meaning of the symbol) is what we want. This is due
+;; to the massive overloading in PVS (anything can be overloaded).
+;; Answers the question: is + actually the + for the reals?
+;;
+
+(defun metit-interpretation (name-expr)
+ (assert (name-expr? name-expr))
+ (let* ((id-assoc (cdr (assoc (id name-expr) *metit-interpreted-names*)))
+ (mod-assoc (cdr (assoc (id (module-instance
+ (resolution name-expr)))
+ id-assoc))))
+ mod-assoc))
+
+(defmethod translate-to-tptp* ((expr binding-expr) env)
+ (declare (ignore env))
+ (error "expression ~a cannot be handled 3." expr))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; lift-predicates-in-quantifier takes the constraints on the variables (p1 : posreal)
+;; and converts it into the proper logical form p1 > 0 & p1 >= 0 and returns
+;; a new expression with these propositional atoms in the antecedent
+;;
+;; The we recursively call translate-metit-bindings to build a cons list of bindvars
+;; ((p1 : real. P11))
+;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(defmethod translate-to-tptp* ((expr quant-expr) env)
+ ;; (let ((new-expr (lift-predicates-in-quantifier expr (list *real*))))
+ (with-slots
+ (bindings expression) expr
+ ;; (multiple-value-bind (newbindings bindvars)
+ ;; (translate-metit-bindings expr-bindings bindings nil)
+ (let ((yexpression (translate-to-tptp* expression (append (mapcar #'id bindings) env))))
+ (cond ((forall-expr? expr)
+ (format nil "(![~{~a~^, ~}]: ~a)" (mapcar #'upcase-tptp-id (mapcar #'id bindings))
+ yexpression))
+ ((exists-expr? expr)
+ (format nil "(?[~{~a~^, ~}]: ~a)" (mapcar #'upcase-tptp-id (mapcar #'id bindings))
+ yexpression)))))) ;;no else case
+
+(defmethod translate-to-tptp* ((expr if-expr) env)
+ (if (and (type-name? (type expr))
+ (or (eq (id (type expr)) 'bool)
+ (eq (id (type expr)) 'boolean)))
+ (let ((condexpr (translate-to-tptp* (nth 0 (arguments expr)) env)))
+ (format nil "((~a => ~a) & ((~~ ~a) => ~a))"
+ condexpr
+ (translate-to-tptp* (nth 1 (arguments expr)) env)
+ condexpr
+ (translate-to-tptp* (nth 2 (arguments expr)) env)))
+ (if (assoc expr *tptp-ite-env* :test #'tc-eq)
+ (cdr (assoc expr *tptp-ite-env* :test #'tc-eq))
+ (let ((newsym (tptp-id-name)))
+ (setq *tptp-ite-env* (cons (cons expr newsym) *tptp-ite-env*))
+ newsym))))
+
+(defun translate-to-tptp (expr)
+ (setq *tptp-ite-env* nil)
+ (format nil "fof(pvs2dk, conjecture, ~a)."
+ (translate-to-tptp* expr nil)))
diff --git a/pvs-load.lisp b/pvs-load.lisp
index 467561d..397dce5 100644
--- a/pvs-load.lisp
+++ b/pvs-load.lisp
@@ -3,3 +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"))
+ (load (concatenate 'string *pvs-dedukti-path* "/proofs/" m ".lisp")))
--
GitLab