Logical representation of the current state of a string input
(strin-p x) is a defaggregate of the following fields.
- chars — Remaining characters in the input stream. Note that you should
typically access these with strin-left, instead of directly
Invariant (character-listp chars).
- line — Current line number, starts at 1.
Invariant (posp line).
- col — Current column number.
Invariant (natp col).
- file — A name describing where these characters are being read from,
typically the name of some file.
Invariant (stringp file).
Source link: strin-p
A strin-p structure is intended as a logical fiction to
explain the behavior of the sin ("string input") stobj.
You should not typically create or operate on strin-p structures.
Doing so would create a lot of garbage, and the sin stobj is generally
We generally think of the line, col, and file fields as a sort of debugging
convenience that, while practically very useful, are not necessarily anything
we want to reason about.
Accordingly, we generally leave all strin-p operations disabled, but
prove some property about their chars.
- Raw constructor for strin-p structures.
- Constructor macro for strin-p structures.
- Remaining characters in a strin-p.
- A copying macro that lets you create new strin-p structures, based on existing structures.
- Simple wrapper that fixes the filename number to a string.
- Wrapper for strin->col that fixes the column number to a natp.
- Advance the input stream by n characters.
- Wrapper for strin->line that fixes the line number to a posp.
- Advance the input stream by 1 character.
- Find the first occurrence of the string literal in the input stream,
and return its position.
- Raw constructor for honsed strin-p structures.
- Constructor macro for honsed strin-p structures.
- See if some string literal occurs (case sensitively) at the start of
the input stream.
- See if some string literal occurs (case insensitively) at the start
of the input stream.
- Extract the first n characters as a string.
- Count how many characters at the start of the input stream are
members of some particular character set.
- Create an empty strin-p structure.
- Peek at the nth character in the input stream.
- How many characters are left in the input stream?
- Are we at the end of the input stream?
- Peek at the first character in the input stream.
- Access the chars field of a strin-p structure.
- Access the line field of a strin-p structure.
- Access the col field of a strin-p structure.
- Access the file field of a strin-p structure.