;-*- Mode: lisp -*-
;; pvs-attachments
;; Predefined semantic attachments
;; Release : PVSio-2.d (11/09/05)

(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))

(defattach 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))))))))))

(attachments stdio

(defattach 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))))))))
)

(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)

(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))

)

(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 T according to the S"
  (cond ((stringp e) (format nil s e))
	((typep e 'array)
	 (apply #'format (append (list nil s)
				 (reduce #'cons e :initial-value nil :from-end t))))
	(t (format nil s e))))
)

(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))
)

(attachments stdpvs

(defattach typeof(e)
  "Returns the string value of the type of E"
  (let* ((the-type (pc-parse *the-pvs-type* 'type-expr))
	 (domain   (domain the-type)))
    (format nil "~a" (or (print-type domain) 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-type (pc-parse *the-pvs-type* 'type-expr))
	 (domain   (domain the-type)))
    (format nil "~a" (cl2pvs e (pc-typecheck domain)))))
)

(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*)

)

(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 (sys:getenv name) default))

)
	     
