rocq/backend/IrText.v
A reader of IR text (src/ir_text.pl): a module written as Prolog clauses, one func/5, data/4, alias/3 or context/2 term per item, which the Prolog compiler reads with read_term/3. This reader gives the same term as read_ir_file/3 or gives nothing: it never reads a text differently from SWI-Prolog.
It reads what the printer of ir_text.pl writes and a little more: % and block comments, names, quoted atoms and double-quoted strings with their escapes, symbol atoms, decimal integers, compounds, proper lists, and one operator, an infix - between two terms (a phi's edges are written start-const(0)). It gives nothing for the rest of Prolog's syntax: variables, every other use of an operator, parentheses around a term, a bar in a list, floats, the other number forms, back-quoted strings, and any byte outside ASCII that is not inside quotes.
A term becomes a term as the backend's driver reads the terms Prolog prints: [ ] is TList[ ], the quoted atom '[]' is TAtom"[]", an atom's name is its UTF-8 bytes, and a double-quoted string is the list of its characters, each an atom of one character.
The text is the list of the file's bytes. Every loop over the text, the clauses, the arguments of a compound and the elements of a list is a tail call, so the extracted reader needs no more stack for 200,000 items than for one; the terms being read are kept in a list of frames, not in the calls.
Characters
The three definitions below are the ones to give an OCaml definition of when extracting: taking a character apart into its eight bits is slow there.
The code of the character c, 0 to 255.
The character whose code is n, for an n below 256.
The string of the characters cs, which are given last first, as a loop collects them.
The codes of the characters the reader names.
Numbers the reader counts with: the two bases of a numeric escape, one more than the most digits of one, what a letter's code is above its value as a digit, and the first bytes and the continuation bytes of UTF-8. Each is a definition of its own because the extracted code builds a number again each time it meets one written inside a function.
Whether n is from lo to hi, both included.
Whether the code n is layout: a space, a newline, a tab or a carriage return.
Whether the code n is a lowercase letter, which starts a name.
Whether the code n is a decimal digit.
Whether the code n may follow the first letter of a name: a letter, a digit or an underscore.
The codes of Prolog's symbol characters, #$&*+-/:<=>?@\^~, but for the full stop, which the reader takes only as a clause's end.
Whether the code n is a symbol character other than the full stop. A run of them is one atom, as + or =<.
Whether the code n may stand as itself in a comment or between quotes: a printing ASCII character.
Whether the text cs starts with the character of code n.
Layout and comments
Where the reader is while it skips layout: between tokens, in a % comment, in a block comment, or in a block comment just after a *.
| | | InLayout | ||
| | | InLine | ||
| | | InBlock | ||
| | | InStar |
The text cs from its first character that is neither layout nor in a comment, the reader being in the state s. Nothing for a block comment that does not end, for a block comment with a /* inside it (SWI-Prolog nests them), and for a character in a comment that is not ASCII printing or layout. A / that no * follows is not a comment and is left in the text.
Names and integers
The name whose characters after those in acc (last first) are the letters, digits and underscores at the front of cs, and the text after it.
The symbol atom whose characters after those in acc are the symbol characters at the front of cs, and the text after it. Nothing when the run has a / then a *, which SWI does not read as one atom. The run stops before a full stop, and the step after the atom refuses one there: inside brackets always, and outside them because a lone symbol atom is no item. So =.. is refused, though SWI reads it.
Ten, the base of an integer's digits. A definition of its own, so the extracted reader builds the number once.
The integer whose digits are those of z and then the decimal digits at the front of cs, and the text after them.
Quoted text
The escapes of one character after a backslash, each with the code it stands for: \a, \b, \f, \n, \r, \t, \v, and a backslash or a quote of any kind standing for itself.
The code the escape character of code n stands for in the table l, if it is there.
The value of the character of code n as a digit in the base base, 8 or 16, if it is one. A hexadecimal digit's letter may be of either case.
The number whose digits in the base base are those of z and then the digits at the front of cs, which a backslash must end, and the text after that backslash. fuel is one more than the most digits read: nothing for a longer number.
The numbers of UTF-8: where each longer form starts, and what its bytes add to their six bits. Definitions of their own, as ten.
The last character code, 0x10FFFF, and the first and the last surrogate, 0xD800 and 0xDFFF, which are no characters.
Whether z is a character code an escape may give: not above 0x10FFFF, and not a surrogate (0xD800 to 0xDFFF). Zero is one: \0\ is the NUL character.
The character whose code is z, for a z from 0 to 255.
The UTF-8 bytes of the character code z, last first, in front of acc.
The code that the escape at the front of cs stands for, cs being the text after a backslash, and the text after the escape. The escapes are those of escapes, \x with one to eight hexadecimal digits and a closing backslash, and one to eight octal digits with a closing backslash. Nothing for any other escape, and for a number that is not a character's code.
The same for a UTF-8 character whose first byte, of code n, is already in acc: the bytes that must follow it are read. Nothing for a first byte that starts no character, and for the forms UTF-8 forbids: a longer form than a code needs, a surrogate, and a code above 0x10FFFF. SWI reads such bytes as other characters than the ones the bytes spell.
The bytes of a quoted atom or a string, last first and in front of acc, and the text after its closing quote. cs is the text after the opening quote, whose code is q. A doubled quote is one quote, a backslash starts an escape (escape), and a character outside ASCII must be well-formed UTF-8. Nothing for text with no closing quote and for a control character, a newline included, written as itself. fuel is at least the length of cs.
Terms
A term the reader is inside of, with what it has read of it: a compound with its name and the arguments so far, a list with the elements so far (both last first), or an infix - with its left side.
What one step of the reader gives: a refusal, the end of the text, a whole clause and the text after its full stop, or the text, the frames and the mode to go on with.
| | | Fail | ||
| | | Done | ||
| | | Clause | t : term cs : listascii | |
| | | Next |
The step after the term v has been read, cs being the text after it and st the frames: as the right side of an infix - it makes that term, after which no second - may come.
The step after the name name: a compound's start when a ( follows it at once, else the atom. lhs is whether the atom may be the left side of an infix -.
The names SWI-Prolog has as prefix operators. table − x is to it table(-(x)), so such an atom is not taken as the left side of an infix -. The symbol atoms that are prefix operators (-, +, \) are refused there with every other symbol atom.
Whether v is an atom SWI has as a prefix operator.
Whether cs, the text after a - that follows a term, starts the right side of an infix - the reader takes: after layout and comments, a name, a quoted atom or a list. The character just after the - must not be a symbol character or a full stop, so the - is an atom of its own, nor a digit: a right side that is a number is refused.
Whether cs, the text after a full stop, makes that full stop a clause's end: the text ends there, or layout or a % follows.
The step from what follows the term v, cs being the text after it from its first character that is not layout: a comma puts v in the compound or list it is in, a closing bracket ends that, a full stop ends the clause, and a - starts the right side of an infix -. Anything else is refused, so a term never runs into the token after it.
Whether name is a name whose compounds SWI-Prolog writes in a form of their own: '[|]'(a, []) is to it the list a, and '{}'(a) is a. A quoted atom of such a name is refused where a ( follows it.
The step from the start of a term, cs being the text from its first character that is not layout: a name, a quoted atom, a string, an integer (a - just before a digit makes it negative), a symbol atom, !, ;, {}, or the [ of a list. With first a ] gives the empty list. At the end of the text the reader is done if it is inside no term. fuel is at least the length of cs. Any other character is refused: a capital letter or an underscore starts a variable.
Clauses
Whether t is the atom end_of_file, which ends the text where it is a clause, as the end of the file does.
The length of cs more than n. The standard library's length is not a tail call in the extracted code.
The clauses of the text cs, last first, or nothing.
The clauses of the text cs in order, up to its end or to a clause that is the atom end_of_file, as read_term/3 reads them one after another. Nothing when SWI-Prolog would not read the text, and for the syntax this reader does not take.
Whether t is a run(Fn, Args) clause, which is no item.
Whether t is an item of a module: a func/5, data/4, alias/3 or context/2 term.
The items among the clauses r, which are given last first, in order and in front of acc: a run/2 clause is left out. Nothing when a clause is neither, where read_ir_file/3 throws.
The module of the IR text cs, module(Items), as read_ir_file/3 gives it and nanofilread − terms prints it: every item in order, not validated. Nothing when Prolog would throw, and for the syntax this reader does not take.
A text in pieces
The list of a large file's bytes takes far more room than the file: 24 bytes a character in the extracted reader. So the driver gives the text a piece at a time, and the reader asks for the next piece when it has read the whole clauses of the ones it has.
A text in pieces: its end, or its next characters and the rest, which is made when asked for.
What reading the whole clauses of a piece gives: the clauses so far, last first, and either the end, at an end_of_file clause, or the text rest that is left, from the start of the first clause that is not whole.
The whole clauses at the front of the text start, which is not the text's end, in front of acc. The reader is at cs inside the frames st in the mode m, within the clause that starts at start. A clause is whole when a character follows its full stop: then no more text changes how it is read. A refusal, or the end of the characters, is not taken as such here, since more text may follow: the clause is left to be read again.
The module of the IR text p, as read_module gives it for the characters of p's pieces one after another. That the two agree is not proved; tests/read.sh holds this one to Prolog with pieces of one character and of seven, and the examples below cut a text at every place.
Examples
A run is left out, a comment is passed over, and a phi's edge is the one operator.
Proof 1 step Qed
An escape in a quoted atom is its character, in UTF-8.
Proof 1 step Qed
A variable, an operator other than the infix -, a clause that is no item and a text with no full stop are refused.
Proof 1 step Qed
A text read in pieces of every size from one character to forty is read as the whole text is: here two clauses with a comment, a quoted atom with a full stop in it and an end_of_file that hides a clause the reader would refuse.
Proof 2 steps Qed
A text that is refused is refused in pieces too.