Quelle patch-109.lisp Sprache: Lisp

;;
;; prelude-attachments.lisp
;; Release: PVSio-6.0.9 (3/14/14)
;;
;; Contact: Cesar Munoz (cesar.a.munoz@nasa.gov)
;; NASA Langley Research Center
;; http://shemesh.larc.nasa.gov/people/cam/PVSio
;;
;; Copyright (c) 2011-2012 United States Government as represented by
;; the National Aeronautics and Space Administration.  No copyright
;; is claimed in the United States under Title 17, U.S.Code. All Other
;; Rights Reserved.
;;
;; Semantic attachments for PVSio standard library
;;

(defun stdstr-attachments ()

(eval '(attachments |stdstr|

(defattach |charcode| (n)
  "Char whose code is N"
  (format nil "~a" (code-char n)))

(defattach |chartable| ()
  "Standard char table"
  (or
   (do ((i 0 (+ i 1)))
       ((>= i 128))
       (let ((c (code-char i)))
  (when (and (graphic-char-p c)
      (standard-char-p c))
    (format t "~3d : ~a " i c))))
   t))

(defattach |newline| ()
  "New line"
  (format nil "~a" #\Newline))

(defattach |tab| ()
  "Tabular"
  (format nil "~a" #\Tab))

(defattach |spaces| (n)
  "N spaces"
  (make-string n :initial-element #\Space))

(defattach |upcase| (s)
  "Converts string S to uppercase"
  (string-upcase s))

(defattach |downcase| (s)
  "Converts string S to downcase"
  (string-downcase s))

(defattach |capitalize| (s)
  "Capitalizes string S"
  (string-capitalize s))

(defattach |substr| (s i j)
  "Substring S[i..j] if i <= j, S[j..i] if j <= i, empty if indices are out of range"
  (cond ((and (<= 0 i) (<= i j) (< j (length s)))
  (subseq s i (+ j 1)))
((and (<= 0 j) (<= j i) (< i (length s)))
  (reverse (subseq s j (+ i 1)))  )
(t "")))

(defattach |strfind| (s1 s2)
  "Index of leftmost occurrence of S1 in S2, starting from 0, or -1 if none"
  (or (search s1 s2 :test #'char=) -1))

(defprimitive |concat| (s1 s2)
  "Concatenates S1 and S2"
  (format nil "~a~a" s1 s2))

(defattach |real2str| (r)
  "String representation of real R"
  (if (integerp r)
      (format nil "~d" r)
    (format nil "~f" (rationalize r))))

(defattach |str2real| (s)
  "Rational denoted by S"
  (let ((i (read-from-string s)))
    (if (numberp i) (rationalize i)
      (throw '|NotARealNumber|
      (pvs2cl_record (the string "NotARealNumber")
       (the string s))))))

(defattach |str2int| (s)
  "Integer denoted by S"
  (let ((i (read-from-string s)))
    (if (integerp i) i
      (throw '|NotAnInteger|
      (pvs2cl_record (the string "NotAnInteger")
       (the string s))))))

(defattach |number?| (s)
  "Tests if S denotes a number"
  (numberp (read-from-string s)))

(defattach |int?| (s)
  "Tests if S denotes an integer"
  (integerp (read-from-string s)))

(defattach |strcmp| (s1 s2 sensitive)
  "Returns 0 if s1 = s2, < 0 if s1 < s2, > 0 if s1 > s2. ~
   Comparison is case sensitive according to sensitive"
  (if sensitive
      (cond ((string= s1 s2) 0)
     ((string< s1 s2) -1)
     (t 1))
    (cond ((string-equal s1 s2) 0)
   ((string-lessp s1 s2) -1)
   (t 1))))

(defattach |strtrim| (s1 s2)
   "A substring of s2, with all the characters in s1 stripped of the beginning and end"
   (string-trim s1 s2))

(defattach |strtrim_left| (s1 s2)
   "A substring of s2, with all the characters in s1 stripped of the beginning"
   (string-left-trim s1 s2))

(defattach |strtrim_right| (s1 s2)
   "A substring of s2, with all the characters in s1 stripped of the end"
   (string-right-trim s1 s2))

(defattach |trim| (s)
   "A substring of s, with all the space characters stripped of the beginning and end"
   (string-trim '(#\Space #\Tab #\Newline) s))

(defattach |trim_left| (s)
   "A substring of s, with all the space characters stripped of the beginning"
   (string-left-trim '(#\Space #\Tab #\Newline) s))

(defattach |trim_right| (s)
   "A substring of s, with all the space characters stripped of the end"
   (string-right-trim '(#\Space #\Tab #\Newline) s))

(defattach |filename| (s)
  "Returns the name part of a file name"
  (file-namestring s))

(defattach |directory| (s)
  "Returns the directory part of a file name"
  (directory-namestring s))

)))

(defun prompt (s)
  (when (string/= s "")
    (format t "~a~%" s)
    (finish-output))
  (clear-input))

(defparameter *pvsio_length_str_stream* (make-hash-table))

(defun read-token (f s)
  (get-output-stream-string
   (let ((c (read-char f nil nil)))
     (when c
       (do* ((str   (make-string-output-stream))
      (start t))
    ((not c) str)
  (let ((p (when c (position c s)))
        (m (when c (member c '(#\Space #\Tab #\Newline)))))
    (cond ((and start p)(write-char c str)
    (return str))
   (p (unread-char c f)
      (return str))
   ((and start m) (setq c (read-char f nil nil)))
   (m (return str))
   (t (setq start nil)
      (write-char c str)
      (setq c (read-char f nil nil))))))))))

(defun stdio-attachments ()

(eval '(attachments stdio

(defprimitive |printstr| (s)
  "Prints lisp format of string S"
  (not (format t "~a" s)))

(defattach |query_token| (mssg s)
  "Queries a token separated by characters in S from standard input with prompt MSSG"
  (prompt mssg)
  (format nil "~a" (read-token *standard-input* s)))

(defattach |query_line| (mssg)
  "Queries a line from standard input with prompt MSSG"
  (prompt mssg)
  (format nil "~a" (read-line)))

(defattach |query_real| (mssg)
  "Queries a real number from standard input with prompt MSSG"
  (prompt mssg)
  (let ((i (read)))
    (if (numberp i) (rationalize i)
      (throw '|NotARealNumber|
      (pvs2cl_record (the string "NotARealNumber")
       (the string (format nil "~a" i)))))))

(defattach |query_int| (mssg)
  "Queries an integer from standard input with prompt MSSG"
  (prompt mssg)
  (let ((i (read)))
    (if (integerp i) i
      (throw '|NotAnInteger|
      (pvs2cl_record (the string "NotAnInteger")
       (the string (format nil "~a" i)))))))

(defattach |stdin| ()
  "Standard input stream"
  *standard-input*)

(defattach |stdout| ()
  "Standard output stream"
  *standard-output*)

(defattach |stderr| ()
  "Error output stream"
  *error-output*)

(defattach |fopenin_lisp| (s)
  "Opens file input stream named S"
  (let ((f (open s :direction :input :if-does-not-exist nil)))
    (or f (throw '|FileNotFound|
   (pvs2cl_record (the string "FileNotFound")
    (the string s))))))

(defattach |sopenin| (s)
  "Opens string S as an input stream"
  (let ((str (make-string-input-stream s)))
    (setf (gethash str *pvsio_length_str_stream*) (length s))
    str))

(defattach |fopenout_lisp| (s i)
  "Opens file output stream named S"
  (let ((f (cond ((= i 0) (open s :direction :output :if-exists nil))
   ((= i 1) (open s :direction :output :if-exists :supersede))
   ((= i 2) (open s :direction :output :if-exists :append))
   ((= i 3) (open s :direction :output :if-exists :overwrite))
   ((= i 4) (open s :direction :output :if-exists :rename)))))
    (or f (throw '|FileAlreadyExists|
   (pvs2cl_record (the string "FileAlreadyExists")
    (the string s))))))

(defattach |sopenout| (s)
  "Opens string output stream"
  (let ((f (make-string-output-stream)))
    (format f s)
    f))

(defattach |fclose| (f)
  "Closes stream F"
  (or (when (typep f 'file-stream)
(close f))
      t))

(defattach |fexists| (s)
  "Tests if file named S already exists"
  (and (probe-file s) t))

(defattach |fopen?| (f)
  "Tests if stream F is open"
  (open-stream-p f))

(defattach |strstream?| (f)
  "Tests if F is a string stream"
  (typep f 'string-stream))

(defattach |filestream?| (f)
  "Tests if F is a file stream"
  (typep f 'file-stream))

(defattach |finput?| (f)
  "Tests if F is an input string"
  (input-stream-p f))

(defattach |foutput?| (f)
  "Tests if F is an output string"
  (output-stream-p f))

(defattach |fname_lisp| (f)
  "Gets the name of a file stream"
  (namestring f))

(defattach |fgetstr_lisp| (f)
  "Gets string from string output stream F"
  (if (typep f 'string-stream)
      (get-output-stream-string f)
    ""))

(defattach |eof_lisp| (f)
  "Tests end of input stream F"
  (not (peek-char nil f nil nil)))

(defattach |flength_lisp| (f)
  "Length of stream F"
  (cond ((typep f 'file-stream) (file-length f))
((typep f 'string-stream)
  (nth-value 0 (gethash f *pvsio_length_str_stream*)))
(t 0)))

(defattach |fgetpos_lisp| (f)
  "Gets current position of file stream F"
  (if (typep f 'file-stream)
      (file-position f)
    0))

(defattach |fsetpos_lisp| (f n)
  "Set current position of file stream F"
  (when (typep f 'file-stream)
    (cond ((<= n 0) (file-position f :start))
   ((>= n (file-length f)) (file-position f :end))
   (t (file-position f n)))))

(defattach |fprint_lisp| (f s)
  "Prints S in stream F"
  (not (format f "~a" s)))

(defattach |fread_token_lisp| (f s)
  "Reads a token from stream F separated by characters in S"
  (format nil "~a" (read-token f s)))

(defattach |fread_line_lisp| (f)
  "Reads a line from stream F"
  (let ((s (read-line f nil nil)))
    (format nil "~a" s)))

(defattach |fread_real_lisp| (f)
  "Reads a real number from stream F"
  (let ((i (read f nil nil)))
    (when i
      (if (numberp i) (rationalize i)
(throw '|NotARealNumber|
        (pvs2cl_record (the string "NotARealNumber")
         (the string (format nil "~a" i))))))))

(defattach |fread_int_lisp| (f)
  "Reads an integer from stream F"
  (let ((i (read f nil nil)))
    (when i
      (if (integerp i) i
(throw '|NotAnInteger|
        (pvs2cl_record (the string "NotAnInteger")
         (the string (format nil "~a" i))))))))
)))

(defun stdmath-attachments ()

(eval '(attachments stdmath

(defattach |PI| ()
  "Number Pi"
  pi)

(defattach |SIN| (x)
  "Sine of X"
  (sin x))

(defattach |COS| (x)
  "Cosine of X"
  (cos x))

(defattach |EXP| (x)
  "Exponential of X"
  (exp x))

(defattach |RANDOM| ()
  "Real random number in the interval [0..1]"
  (random 1.0))

(defattach |NRANDOM| (x)
  "Natural random number in the interval [0..X)"
  (random x))

(defattach |sqrt_lisp| (x)
  "Square root of X"
   (sqrt x))

(defattach |log_lisp| (x)
  "Logarithm of X"
  (if (<= x 0) 0 (log x)))

(defattach |atan_lisp| (x y)
  "Arctangent of Y/X"
  (atan x y))

(defattach |asin_lisp| (x)
  "Arcsine of X"
  (asin x))

(defattach |acos_lisp| (x)
  "Arccosine of X"
  (acos x))

)))

(defstruct indent stack n prefix)

(defun stdindent-attachments ()

(eval '(attachments stdindent

(defattach |create_indent| (n s)
  "Creates an ident structure with indentation N and prefix S"
  (make-indent :stack nil :n n :prefix s))

(defattach |pop_indent| (i)
  "Pops one element of indent I"
  (or (setf (indent-stack i) (cdr (indent-stack i))) t))

(defattach |push_indent| (i n)
  "Pushes a N-indentation in indent I"
  (setf (indent-stack i)
(cons (+ n (pvsio_stdindent_top_indent_1 i))
       (indent-stack i))))

(defattach |top_indent| (i)
  "Top of I"
  (or (car (indent-stack i)) 0))

(defattach |get_indent| (i)
  "Gets current indentation value of indent I"
  (indent-n i))

(defattach |set_indent| (i n)
  "Sets a new indentation value to indent I"
  (setf (indent-n i) n))

(defattach |get_prefix| (i)
  "Gets prefix of indent I"
  (indent-prefix i))

(defattach |set_prefix| (i s)
  "Sets prefix S to indent I"
  (setf (indent-prefix i) s))

)))

(defun formatargs (e type)
  (cond ((or (stringp e) (numberp e)
      (and (atom e) (type-name? type) (equal (id type) '|Blisp|))) e)
((and (listp e)
       (type-name? type)
       (equal (id type) '|Slisp|))
  (let ((ntype (type-value (car (actuals type)))))
    (loop for ei in e
   collect (formatargs ei ntype))))
(t (cl2pvs e type))))

(defun stdprog-attachments ()

(eval '(attachments stdprog

(defattach |exit| ()
  "Exits the current evaluation and returns to the ground evaluator"
  (throw 'abort t))

(defattach |error| (mssg)
  "Signals the error message MSSG to the ground evaluator"
  (error "~a" mssg))

(defattach |new| ()
  "Creates a new mutable variable without any current value"
  (cons nil t))

(defattach |ref| (e)
  "Creates a mutable variable with a current value E"
  (list e))

(defattach |def| (v e)
  "Sets to E the value of a mutable variable V"
  (when (cdr v) (setf (cdr v) nil))
  (setf (car v) e))

(defattach |undef| (v)
  "Tests if a mutable variable V is undefined"
  (cdr v))

(defattach |val_lisp| (v)
  "Gets the current value of a mutable variable V"
  (car v))

(defattach |loop_lift| (f)
   "Applies F in an infinite loop"
   (catch '|*pvsio-loop*|
     (loop (pvs-funcall f 0))))

(defattach |return| (e)
  "Returns E from an infinite loop"
  (throw '|*pvsio-loop*| e))

(defattach |format| (s e)
   "Formats expression E using Common Lisp format string S"
   (let* ((the-type (pc-typecheck (cadr (types (domain *the-pvs-type*))))))
     (if (and (arrayp e)
       (tupletype? the-type))
  (let* ((the-types (types the-type))
  (l (loop for ei across e
    for ti in the-types
    collect (formatargs ei ti))))
    (apply #'format (cons nil (cons s l))))
       (apply #'format (cons nil (cons s (list (formatargs e the-type))))))))
)))

(defun stdcatch-attachments ()

(eval '(attachments stdcatch

(defattach |catch_lift| (tag f1 f2)
  "If F1 throws the exception e tagged tag, then evaluates F2(e). Otherwise, returns F1"
  (let ((e (catch (makesym tag) (cons '*pvsio-catch* (pvs-funcall f1 0)))))
    (if (and (consp e) (eq (car e) '*pvsio-catch*))
(cdr e)
      (pvs-funcall f2 e))))

(defattach |throw| (tag e)
  "Throws the exception E"
  (throw (makesym tag) e))
)))

(defun stdpvs-attachments ()

(eval '(attachments stdpvs

(defattach |typeof| (e)
  "Returns the string value of the type of E"
  (let* ((the-domain (domain *the-pvs-type*)))
    (format nil "~a" (or (print-type the-domain) the-domain))))

(defattach |str2pvs| (s)
  "Translates string S to PVS format"
  (eval (pvs2cl (pc-typecheck (pc-parse s 'expr)))))

(defattach |pvs2str_lisp| (e)
  "Translates PVS expresion E to a string"
  (let* ((the-domain (domain *the-pvs-type*)))
    (format nil "~a" (cl2pvs e (pc-typecheck the-domain)))))

(defattach |slisp| (l)
  "Returns a s-expression representing list l. To be used exclusively in format functions."
  l)

)))

(defun stdpvsio-attachments ()

(eval '(attachments stdpvsio

(defattach |help_pvs_attachment| (s)
  "Displays help for semantic attachment S"
  (or (help-pvs-attachment s) t))

(defattach |help_pvs_theory_attachments| (s)
  "Displays help for semantic attachments in theory S"
  (or (help-pvs-theory-attachments s) t))

(defattach |pvsio_version| ()
  "Shows current version of PVSio"
  *pvsio-version*)

(defattach |set_promptin| (s)
  "Change current PVSio input prompt to S"
  (when (setq *pvsio-promptin* s) t))

(defattach |set_promptout| (s)
  "Change current PVSio output prompt to S"
  (when (setq *pvsio-promptout* s) t))

)))

(defun stdsys-attachments ()

(eval '(attachments stdsys

(defattach |get_time| ()
  "Gets current system time"
  (multiple-value-bind (s mi h d mo y dow dst tz) (get-decoded-time)
    (the (simple-array *) (pvs2cl_record d dow dst h mi mo s tz y))))

(defattach |sleep| (n)
  "Sleeps n seconds"
  (or (sleep n) t))

(defattach |get_env| (name default)
  "Gets environment variable NAME. Returns DEFAULT if undefined"
  (or (environment-variable (string name)) default))

(defattach |blisp| (b)
  "Returns a Boolean lisp expression representing b. To be used exclusively in format functions."
  b)

)))

(defun initialize-prelude-attachments ()
  (stdstr-attachments)
  (stdio-attachments)
  (stdmath-attachments)
  (stdindent-attachments)
  (stdprog-attachments)
  (stdcatch-attachments)
  (stdpvs-attachments)
  (stdpvsio-attachments)
  (stdsys-attachments))

quality97%

¤ Dauer der Verarbeitung: 0.26 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.