|
|
|---|
|
|
|
|---|
Abstract ACL2::stobj for a string input stream.
The
This abstraction is especially useful for writing lexers or parsers, which typically involve scanning through the string from the front, and breaking it apart into individual tokens. Practically speaking, any lexer or parser that will actually be used needs to be able to provide location information to help its user track down errors.
Logically, the
Definition:
(defabsstobj sin :foundation sin$c :recognizer (sinp :logic strin-p :exec sin$cp) :creator (create-sin :logic empty-strin :exec create-sin$c) :corr-fn sin$corr :exports ((sin-init :logic strin-init :exec sin$c-init :protect t) (sin-line :logic strin-get-line$inline :exec sin$c-get-line$inline) (sin-col :logic strin-get-col$inline :exec sin$c-get-col$inline) (sin-file :logic strin-get-file$inline :exec sin$c-get-file$inline) (sin-endp :logic strin-endp :exec sin$c-endp$inline) (sin-len :logic strin-len :exec sin$c-len$inline) (sin-car :logic strin-car :exec sin$c-car$inline) (sin-nth :logic strin-nth :exec sin$c-nth$inline) (sin-firstn :logic strin-firstn :exec sin$c-firstn) (sin-cdr :logic strin-cdr :exec sin$c-cdr :protect t) (sin-nthcdr :logic strin-nthcdr :exec sin$c-nthcdr :protect t) (sin-matches-p :logic strin-matches-p :exec sin$c-matches-p) (sin-imatches-p :logic strin-imatches-p :exec sin$c-imatches-p) (sin-count-charset :logic strin-count-charset :exec sin$c-count-charset) (sin-find :logic strin-find :exec sin$c-find)))