• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
      • Io
      • Defttag
      • Sys-call
      • Save-exec
      • Quicklisp
      • Std/io
      • Oslib
      • Bridge
      • Clex
        • Example-lexer
        • Sin
          • Strin-p
            • Strin
            • Make-strin
            • Strin-left
            • Change-strin
            • Strin-get-file
            • Strin-get-col
            • Strin-nthcdr
            • Strin-get-line
            • Strin-cdr
            • Strin-find
            • Honsed-strin
            • Make-honsed-strin
            • Strin-matches-p
            • Strin-imatches-p
            • Strin-firstn
            • Strin-count-charset
            • Empty-strin
            • Strin-nth
            • Strin-len
            • Strin-endp
            • Strin-car
            • Strin->chars
            • Strin->line
            • Strin->col
            • Strin->file
          • Sin$c
        • Matching-functions
        • Def-sin-progress
      • Tshell
      • Unsound-eval
      • Hacker
      • ACL2s-interface
      • Startup-banner
      • Command-line
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Sin

Strin-p

Logical representation of the current state of a string input stream.

(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 with strin->chars.
        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 more efficient.

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.

Subtopics

Strin
Raw constructor for strin-p structures.
Make-strin
Constructor macro for strin-p structures.
Strin-left
Remaining characters in a strin-p.
Change-strin
A copying macro that lets you create new strin-p structures, based on existing structures.
Strin-get-file
Simple wrapper that fixes the filename number to a string.
Strin-get-col
Wrapper for strin->col that fixes the column number to a natp.
Strin-nthcdr
Advance the input stream by n characters.
Strin-get-line
Wrapper for strin->line that fixes the line number to a posp.
Strin-cdr
Advance the input stream by 1 character.
Strin-find
Find the first occurrence of the string literal in the input stream, and return its position.
Honsed-strin
Raw constructor for honsed strin-p structures.
Make-honsed-strin
Constructor macro for honsed strin-p structures.
Strin-matches-p
See if some string literal occurs (case sensitively) at the start of the input stream.
Strin-imatches-p
See if some string literal occurs (case insensitively) at the start of the input stream.
Strin-firstn
Extract the first n characters as a string.
Strin-count-charset
Count how many characters at the start of the input stream are members of some particular character set.
Empty-strin
Create an empty strin-p structure.
Strin-nth
Peek at the nth character in the input stream.
Strin-len
How many characters are left in the input stream?
Strin-endp
Are we at the end of the input stream?
Strin-car
Peek at the first character in the input stream.
Strin->chars
Access the chars field of a strin-p structure.
Strin->line
Access the line field of a strin-p structure.
Strin->col
Access the col field of a strin-p structure.
Strin->file
Access the file field of a strin-p structure.