From 6d370b65e8cca8a488b7c9140c0ecad668a5de56 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Mon, 18 Nov 2002 23:07:36 +0000 Subject: Fixup code to interpret default values. --- generic/pg-pgip.el | 127 ++++++++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 112 insertions(+), 15 deletions(-) (limited to 'generic/pg-pgip.el') diff --git a/generic/pg-pgip.el b/generic/pg-pgip.el index 42060e13..8224f937 100644 --- a/generic/pg-pgip.el +++ b/generic/pg-pgip.el @@ -50,7 +50,8 @@ ;; ((eq elt 'prefval) - ) + (pg-pgip-prefval attrs (car-safe body))) + ;; ((eq elt 'idtable) ) @@ -93,10 +94,15 @@ ))) -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; -;; name +;; name ;; +;; Proof assistant advises PG that it has a preference value named name, +;; category k, class c, with default value d, type t. +;; +;; PGIP FIXME: do we need a operation? (defun pg-pgip-haspref (attrs name) "Issue a defpacustom from a element with attributes ATTRS, name NAME." @@ -104,10 +110,10 @@ (pg-pgip-error "pg-pgip-haspref: missing NAME in NAME.")) (let* ((type (pg-pgip-get-type attrs)) - (default (or (pg-pgip-get-attr "haspref" 'default attrs t) - ;; If no default is supplied, make one - ;; [NB: boolean default is nil anyway] - (pg-pgip-default-for type))) + (defattr (pg-pgip-get-attr "haspref" 'default attrs t)) + (default (if defattr + (pg-pgip-interpret-value defattr type) + (pg-pgip-default-for type))) (kind (intern (or (pg-pgip-get-attr "haspref" 'kind attrs t) @@ -130,6 +136,28 @@ :type (quote ,type) :setting ,setting))))) +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; value +;; +;; Proof assistant advises that preference n has been updated. +;; +;; Protocol is that sent on a PGIP channel is assumed to +;; succeed, so is not required to be acknowledged with a +;; message from prover. But no harm will result if it is --- and that +;; might be appropriate if some canonicalisation occurs. + +; in progress +;(defun pg-pgip-prefval (attrs value) +; "Process a element, by setting interface's copy of preference." +; (let* +; ((name (pg-pgip-get-attr "haspref" 'name attrs t)) +; (type ( + + + + + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -156,14 +184,20 @@ (t "%s"))) (defun pg-pgip-get-type (attrs) - "Extract and check type value from ATTRS. Normalize to custom format." + "Extract and check type value from ATTRS. Return type in internal (custom) format." (let ((rawtype (pg-pgip-get-attr "haspref" 'type attrs))) + (pg-pgip-pgiptype rawtype))) + + +(defun pg-pgip-pgiptype (rawtype) + "Return internal (custom format) representation for element." (cond - ((string-match "choice(\\(.*\\))" rawtype) + ((string-match "choice\(\\(.*\\)\)" rawtype) (let* ((choiceslist (match-string 1 rawtype)) + ;; FIXME: nested choices not supported yet (choices (split-string choiceslist "[ \f\t\n\r\v]*,[ \f\t\n\r\v]*"))) - (list 'choice choices))) + (list 'choice (mapcar 'pg-pgip-pgiptype choices)))) ((equal rawtype "boolean") 'boolean) ((equal rawtype "int") @@ -173,7 +207,65 @@ ((equal rawtype "string") 'string) (t - (error "pg-pgip-get-type: unrecognized type %s" rawtype))))) + (error "pg-pgip-pgiptype: unrecognized type %s" rawtype)))) + + +;; Converting PGIP representations to elisp representations. This is +;; the inverse of proof-assistant-format translations in proof-menu.el, +;; although we fix PGIP value syntax. + +(defun pg-pgip-interpret-bool (value) + (cond + ((string-equal value "true") t) + ((string-equal value "false") nil) + ;; Non-boolean value: return false, give debug message. + (t (progn + (proof-debug "pg-pgip-interpret-bool: received non-bool value %s" value) + nil)))) + +(defun pg-pgip-interpret-int (value) + ;; FIXME: string-to-int returns zero for non int string, + ;; should have better validation here. + (string-to-int value)) + +(defun pg-pgip-interpret-string (value) + value) + +(defun pg-pgip-interpret-choice (choices value) + ;; Untagged union types: test for each type in turn. + ;; FIXME: nested unions not supported here. + (cond + ((and + (memq 'boolean choices) + (or (string-equal value "true") (string-equal value "false"))) + (pg-pgip-interpret-value value 'boolean)) + ((and + (memq 'integer (cdr type)) + (string-match "[0-9]+$" value)) + (pg-pgip-interpret-value value 'integer)) + ((memq 'string (cdr type)) + ;; FIXME: No special syntax for string inside PGIP yet, should be? + (pg-pgip-interpret-value value 'string)) + (t + (pg-pgip-error "pg-pgip-interpret-choice: mismatching value %s for choices %s" + value choices)))) + +(defun pg-pgip-interpret-value (value type) + (cond + ((eq type 'boolean) + (pg-pgip-interpret-bool value)) + ((eq type 'integer) + (pg-pgip-interpret-int value)) + ((eq type 'string) + (pg-pgip-interpret-string value)) + ((and (consp type) (eq (car type) 'choice)) + (pg-pgip-interpret-choice (cdr type) value)) + (t + (pg-pgip-error "pg-pgip-interpret-value: unkown type %s" type)))) + +;;(defun pg-pgip-interpret-choice (value) +;; FIXME: Choice should be tagged. Syntax is (value) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -197,10 +289,15 @@ ;; Function to interface PGIP commands sent to prover. ;; (defun pg-prover-interpret-pgip-command (pgip) - (if proof-shell-issue-pgip-cmd - (format proof-shell-issue-pgip-cmd pgip) - "")) ;; Empty setting: might be better to send a comment - ;; for debugging purposes. + (cond + ((stringp proof-shell-issue-pgip-cmd) + (format proof-shell-issue-pgip-cmd pgip)) + ((functionp proof-shell-issue-pgip-cmd) + (funcall proof-shell-issue-pgip-cmd pgip)) + (t + ;; FIXME: Empty setting: might be better to send a comment + ""))) + -- cgit v1.2.3