Parse a string into s-expressions, by using Common Lisp's read
under the hood. (requires a ttag)
(read-string str pkg &key (state 'state))
(mv errmsg objects state)
- str — The string to parse.
Guard (stringp str).
- pkg — The package in which to read the string, or NIL for the current-package.
Guard (or (null pkg) (stringp pkg)).
- errmsg — An error msg on failure, e.g., parse errors;
or nil on success.
- objects — The list of objects parsed from str.
- state — Type (state-p1 state), given (state-p1 state).
In the logic we just read the oracle to decide if parsing will
succeed or fail. So you can never prove any relationship between the input
str and the resulting s-expressions that you get out.
In the execution, we turn the string into a Common Lisp input stream and try
to parse it using read, so that full Common Lisp syntax is permitted. The
read is done in the current-package if the pkg argument is
nil; otherwise, the pkg argument should be a known package name and
the read is done in that package. If we are able to successfully parse objects
until EOF is reached, we return success and the list of objects we read.
Jared thinks this may be sound. (Matt K. has since added the pkg
argument but thinks this is still sound, because of the continued use of the
oracle.) See read-string-tests.lisp for some obvious attempts to cause
Definitions and Theorems
(defun read-string-fn (str pkg state)
(declare (xargs :stobjs (state)))
(declare (xargs :guard (and (stringp str)
(or (null pkg) (stringp pkg)))))
(declare (ignore pkg))
(declare (ignorable str))
(let ((__function__ 'read-string))
(declare (ignorable __function__))
(b* ((- (raise "Raw lisp definition not installed?"))
((mv err1 errmsg? state)
((mv err2 objects state)
((when (or err1 err2))
(mv (msg "Reading oracle failed.")
((when errmsg?) (mv errmsg? nil state)))
(mv nil objects state))))
(implies (state-p1 state)
(b* (((mv ?errmsg ?objects ?state)
(read-string-fn str pkg state)))