Network Working Group M. Petit-Huguenin Internet-Draft Impedance Mismatch LLC Intended status: Experimental 5 August 2024 Expires: 6 February 2025 Computerate Specification draft-petithuguenin-computerate-specification-03 Abstract This document specifies computerate specifications, which are the combination of a formal and an informal specification such as parts of the informal specification are generated from the formal specification. Status of This Memo This Internet-Draft is submitted in full conformance with the provisions of BCP 78 and BCP 79. Internet-Drafts are working documents of the Internet Engineering Task Force (IETF). Note that other groups may also distribute working documents as Internet-Drafts. The list of current Internet- Drafts is at https://datatracker.ietf.org/drafts/current/. Internet-Drafts are draft documents valid for a maximum of six months and may be updated, replaced, or obsoleted by other documents at any time. It is inappropriate to use Internet-Drafts as reference material or to cite them other than as "work in progress." This Internet-Draft will expire on 6 February 2025. Copyright Notice Copyright (c) 2024 IETF Trust and the persons identified as the document authors. All rights reserved. This document is subject to BCP 78 and the IETF Trust's Legal Provisions Relating to IETF Documents (https://trustee.ietf.org/ license-info) in effect on the date of publication of this document. Please review these documents carefully, as they describe your rights and restrictions with respect to this document. Code Components extracted from this document must include Revised BSD License text as described in Section 4.e of the Trust Legal Provisions and are provided without warranty as described in the Revised BSD License. Petit-Huguenin Expires 6 February 2025 [Page 1] Internet-Draft Computerate Specification August 2024 Table of Contents 1. Introduction . . . . . . . . . . . . . . . . . . . . . . . . 2 2. Terminology . . . . . . . . . . . . . . . . . . . . . . . . . 3 3. AsciiDoc . . . . . . . . . . . . . . . . . . . . . . . . . . 3 3.1. Literate Programming . . . . . . . . . . . . . . . . . . 4 3.2. Code Macros . . . . . . . . . . . . . . . . . . . . . . . 5 3.2.1. Inline Code Macro . . . . . . . . . . . . . . . . . . 5 3.2.2. Block Code Macro . . . . . . . . . . . . . . . . . . 6 3.3. IdrisDoc Generation . . . . . . . . . . . . . . . . . . . 6 4. Idris2 . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 4.1. "Asciidoc" Module . . . . . . . . . . . . . . . . . . . . 7 4.1.1. Content . . . . . . . . . . . . . . . . . . . . . . . 7 4.1.2. Block . . . . . . . . . . . . . . . . . . . . . . . . 8 4.1.3. Implementing Asciidoc . . . . . . . . . . . . . . . . 8 4.2. "Xml2rfc" Module . . . . . . . . . . . . . . . . . . . . 9 4.2.1. Content . . . . . . . . . . . . . . . . . . . . . . . 9 4.2.2. Block . . . . . . . . . . . . . . . . . . . . . . . . 10 4.2.3. Top-level Section . . . . . . . . . . . . . . . . . . 10 4.2.4. Document . . . . . . . . . . . . . . . . . . . . . . 10 5. Informative References . . . . . . . . . . . . . . . . . . . 10 Appendix A. Installation . . . . . . . . . . . . . . . . . . . . 11 Appendix B. Package asciidoc . . . . . . . . . . . . . . . . . . 12 B.1. Module Asciidoc . . . . . . . . . . . . . . . . . . . . . 12 B.2. Module Asciidoc.Xml2rfc . . . . . . . . . . . . . . . . . 19 Acknowledgements . . . . . . . . . . . . . . . . . . . . . . . . 25 Contributors . . . . . . . . . . . . . . . . . . . . . . . . . . 25 Changelog . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 Author's Address . . . . . . . . . . . . . . . . . . . . . . . . 26 1. Introduction An informal specification is any document that is the combination of text, diagrams, tables, lists, and examples and whose purpose is to describe an engineering system. An RFC is an example of informal specification when it describes network elements and the protocols that help these elements to interoperate. Informal specifications are nowadays written on a computer, which makes them easier to write but not easier to reason about their correctness. Computers can be used to model the engineering system that a specification is meant to describe, to verify that some properties hold for that model, and to automatically derive parts of the text, diagrams, list and examples that compose that specification. This could be done in an ad-hoc way by copying and pasting results from external software, but this adds the burden for the specification authors of having to keep the software model and the specification synchronized. Petit-Huguenin Expires 6 February 2025 [Page 2] Internet-Draft Computerate Specification August 2024 A well-known consequence is when an example in a specification does not match the text, most likely because one of the two was modified without verifying that the other was updated. To simplify the integration of code in a specification we introduce the concept of "Computerate Specifying", which is similar in appearance to literate programming [LitProg], but reversing the intent. Literate programming is about interspersing code with the elements of a document, with the intent of producing a piece of code that can then be executed. On the other hand computerate specifying is about interspersing a document with code, with the intent of producing a document that have some of its elements generated from the result of computations that uses that code. "Computerate Specifying" is a play on "Literate Computing", itself a play on "Structured Computing" (see [Knuth92] page 99). Note that "computerate" is a British English word. To keep on the joke, an informal specification could be said to be an incomputerate specification, "incomputerate" being an Australian English word. 2. Terminology AsciiDoc: The formal language in which the document part of a computerate specification is written. Asciidoc: An Idris2 package that is used to generate AsciiDoc fragments. Asciidoctor: An extensible processor for AsciiDoc document. 3. AsciiDoc There is a large variety of target formats in which a specification can be written (HTML, PDF, Word, Confluence), so we use [AsciiDoc] as a common format from which any of the target formats can be generated. AsciiDoc is a text format, making it easy to mix with code and to integrate with the tools that programmers are most familiar with. It has been chosen because it is derived from DocBook and because its main implementation, [Asciidoctor], can be easily extended and already have a large set of backends for various target formats: * the HTML5, DocBook5, and Manpage back-ends are built-in * the PDF, Epub3, Reveal.js (slides) and many others are distributed as add-ons * [Metanorma] distributes a set of back-end add-ons for the development of standard documents Petit-Huguenin Expires 6 February 2025 [Page 3] Internet-Draft Computerate Specification August 2024 * an alternate XML2RFC v3 [draft-petithuguenin-xml2rfc-asciidoc] backend add-on is also available * a Confluence backend add-on is under development. The AsciiDoc syntax is enriched with several extensions designed to support computerate specifications: * the support for literate programming, by commenting out any line that starts with the '>' character in the leftmost column * an inline macro that inserts the result of a computation as AsciiDoc formatted text * a block macro that inserts the result of a computation as AsciiDoc blocks. These syntax extensions, which are described in the following sections, are implemented in the "asciidoctor-idris2" add-on. 3.1. Literate Programming Idris2 shares with Haskell and other Haskell relatives built-in support for literate programming. We use the Bird mode which marks lines of code with a '>' symbol in the leftmost column. The literate programming rule that states that a block of code must always be separated from normal text by at least one blank line applies. The following example contains a block of two lines of Idris2 code: Some text > a : Int > a = 2 More text Note that the '>' symbol is also used by AsciiDoc as an alternate way of defining a blockquote which is consequently not available in a computerate specification. The normal syntax for blockquotes must be used instead. The code will not appear in the rendered document, but self-inclusion can be used to copy part of the code into the document, thus guaranteeing that this code is verified by the type-checker: Petit-Huguenin Expires 6 February 2025 [Page 4] Internet-Draft Computerate Specification August 2024 > -- tag::currying[] > total > currying : ((a, b) -> c) -> (a -> b -> c) > currying f = \x => \y => f (x, y) > -- end::currying[] .... include::myfile.lidr[tag=currying] .... Because Idris2 does not resolve forward references by default, self- inclusion can also be used to reorder paragraphs when the flow of explanations does not coincide with the flow of the code. Alternating paragraphs of text and code permits to keep both representations as close as possible and is an effective way to quickly discover that the code and the text are diverging. The convention is to insert the code beneath the text it is related to. To be treated as a literate programming file, the AsciiDoc document must use the suffix ".lidr". This generally means that a document will be split in multiple documents, some with the ".adoc" extension and some with the ".lidr" extension. These files are put back together by using, directly or indirectly, AsciiDoc "include" statements in the files. 3.2. Code Macros Using code macros in lieu of the equivalent constants in a document ensures that the text stays consistent during the development of the specification. The type of the code passed to the macro must implement the Asciidoc interface so it is converted into properly escaped Asciidoc. Section 4.1.3 explains how to implement the Asciidoc interface for user defined types. A code macro searches first for an Asciidoc implementation that has the same name than the back-end, then fallback to an unnamed implementation when a named implementation cannot be found. This permits to use all the extensions specific to a particular back-end. 3.2.1. Inline Code Macro The code:[] inline macro is used when the result is to be inserted as AsciiDoc inline text. Petit-Huguenin Expires 6 February 2025 [Page 5] Internet-Draft Computerate Specification August 2024 For instance the following excerpt taken from the computerate specification of [RFC8489]: > retrans' : Nat -> Int -> Maybe (List1 Int) > retrans' rc = fromList . take rc . scanl (+) 0 > . unfoldr (bimap id (*2) . dup) > retrans : Nat -> Int -> String > retrans rc = maybe "Error" > (foldr1By (\e, a => show e ++ " ms, " ++ a) > (\x => "and " ++ show x ++ "ms")) . retrans' rc > timeout : Nat -> Int -> Int -> String > timeout rc rto rm = maybe "Error" > (\e => show (last e + rm * rto)) (retrans' rc rto) > rc : Nat; rc = 7 > rto : Int; rto = 500 > rm : Int; rm = 16 For example, assuming an RTO of code:[rto]ms, requests would be sent at times code:[retrans rc rto]. If the client has not received a response after code:[timeout] ms, the client will consider the transaction to have timed out. is rendered as "For example, assuming an RTO of 500ms, requests would be sent at times 0 ms, 500 ms, 1500 ms, 3500 ms, 7500 ms, 15500 ms, and 31500ms. If the client has not received a response after 39500 ms, the client will consider the transaction to have timed out." 3.2.2. Block Code Macro The "code::[]" block macro (notice the double colon) is used to generate AsciiDoc blocks in a way similar to the inline code macro. 3.3. IdrisDoc Generation The API documentation (IdrisDoc) generator in Idris has been extended to generate AsciiDoc instead of HTML. An Asciidoctor include processor has been added to build and integrate that generated document as part of the document rendering. For instance, the following generates the IdrisDoc for the asciidoc.ipkg package and includes the output in the document: include::asciidoc.ipkg[leveloffset=+2] Petit-Huguenin Expires 6 February 2025 [Page 6] Internet-Draft Computerate Specification August 2024 The document is generated with the main section at level one so the "leveloffset" attribute is used to update the actual section level. 4. Idris2 The code in a computerate specification uses the programming language [Idris2] in literate programming [Knuth92] mode. Although most programming languages could have been used, Idris2 has been chosen for the following features: * purely functional * eager evaluation, with optional laziness * totality checking * dependent and linear type system. * reflection and meta-programming support * REPL. The most important of these features are totality checking and the dependent type system, which permit to ensure an high level of correctness to the code. Generating portions of a document from a programming language that lacks these features would only bring marginal improvements in the quality of a specification. The next sections describe an Idris2 package that can be used to simplify the generation of IdrisDoc. Appendix B lists the API for that same package. 4.1. "Asciidoc" Module The Asciidoc module provides a way to programmatically build an AsciiDoc fragment without having to worry about the particular formatting details. The elements of an AsciiDoc document are grouped in 4 categories: * Content * Block * Top-level section * Document 4.1.1. Content Content is the sum type of the possible parts that compose an AsciiDoc text: TextContent: Plain text. BreakContent: An hard line break. ItalicContent: Italicized text. Petit-Huguenin Expires 6 February 2025 [Page 7] Internet-Draft Computerate Specification August 2024 LinkContent: An hyperlink. IndexContent: A word that will be cross-referenced in the index. BoldContent: Bold text. SubscriptContent: Subscripted text. SuperscriptContent: Superscripted text. MonospaceContent: Monospaced text. CrossrefContent: A cross reference to another part of the whole document. PassContent: Text that is copied in the output document without further processing. OtherContent is used to extend the Content sum type with content that is specific to a backend. 4.1.2. Block Block is the sum type of the possible blocks that compose an AsciiDoc document: ParagraphBlock: A paragraph. LiteralBlock: A pretty-printed block of text. ImageBlock: An image. SourceBlock: A pretty-printed block of source code. SidebarBlock: Visually separated content. QuoteBlock: A prose excerpt, quote, or verse. DefinitionListBlock: An association list. OrderedListBlock: An ordered list. UnorderedListBlock: An unordered list. TableBlock: An table. IndexBlock: A word that will be cross-referenced in the index. PassBlock: Text that is copied in the output document without further processing. OtherBlock is used to extend the Block sum type with blocks that are specific to a backend. 4.1.3. Implementing Asciidoc User-defined Idris2 types can implement the Asciidoc interface to streamline their conversion into AsciiDoc, in a way that is similar to the use of the standard Show and Pretty interfaces. The Asciidoc interface defines two functions, contents and blocks which, after implementation, generates respectively a non-empty list of Content instances or a non-empty list of Block instances. The former is called when using an inline code macro, the latter when using a block code macro. Both functions are implemented by default so it is mandatory to implement only one of the two. Petit-Huguenin Expires 6 February 2025 [Page 8] Internet-Draft Computerate Specification August 2024 For example the following fragment defines how to render the result of a decision function in a specification: > Asciidoc (Dec a) where > contents (Yes prf) = singleton (TextContent "yes") > contents (No contra) = singleton (TextContent "no") Is 1 + 1 = 2? code:[decEq (1 + 1) 2]. + Is 1 + 1 = 3? code:[decEq (1 + 1) 3]. The Asciidoc interface can be implemented multiple times using named implementations. This is used to generate different content or block. The Asciidoc interface is implemented for the builtin types String, Char, Integer, Int, Int8, Int16, Int32, Int64, Bits8, Bits16, Bits32, Bits64, and Double. The "asciidoctor-idris2" must know if an implementation of the Asciidoc is available on a separate package. These package dependencies must be added to the document header attribute ":idris2-packages:", separated by spaces or a comma. The "contrib" and "asciidoc" packages are always added as dependencies, and so do not need to be listed in the ":idris2-packages:" attribute. Additional packages containing implementations of the Asciidoc interface that are useful when writing an Internet-Draft will be documented in separate documents. 4.2. "Xml2rfc" Module This module supplements the Asciidoc module with types that implement the AsciiDoc extensions specific to the "xml2rfc" Asciidoctor backend. 4.2.1. Content CrossrefXml2rfc extends the Crossref content with additional attributes LinkXml2rfc extends the Link content with additional attributes Bcp14 is an additional content. Comment is an additional content. Unicode is an additional content. Petit-Huguenin Expires 6 February 2025 [Page 9] Internet-Draft Computerate Specification August 2024 4.2.2. Block ParagraphXml2rfc extends the Paragraph block with additional attributes LiteralXml2rfc extends the Literal block with additional attributes ImageXml2rfc extends the Image block with additional attributes SourceXml2rfc extends the Source block with additional attributes Alt is an additional block. Figure is an additional block. DefinitionListXml2rfc extends the DefinitionList block with additional attributes OrderedListXml2rfc extends the OrderedList block with additional attributes UnorderedListXml2rfc extends the UnorderedList block with additional attributes 4.2.3. Top-level Section TopSection is the sum type of the possible top-level sections that compose an AsciiDoc document: Note is an additional top-level section. AbstracTopSection: An abstract section. NormalTopSection: A section. BibliographyTopSection: A bibliography. AppendixTopSection: An appendix . IndexTopSection: An index. 4.2.4. Document Document represents a complete AsciiDoc document. 5. Informative References [AsciiDoc] "AsciiDoc", Accessed 23 April 2021, 8 March 2021, . Petit-Huguenin Expires 6 February 2025 [Page 10] Internet-Draft Computerate Specification August 2024 [Asciidoctor] "Asciidoctor Documentation Home :: Asciidoctor Docs", Accessed 23 April 2021, . [draft-petithuguenin-xml2rfc-asciidoc] Petit-Huguenin, M., "Mappings Between XML2RFC v3 and AsciiDoc", Work in Progress, Internet-Draft, draft- petithuguenin-xml2rfc-asciidoc-05, 28 July 2024, . [Idris2] "Documentation for the Idris 2 Language — Idris2 0.0 documentation", Accessed 31 January 2023, . [Knuth92] Knuth, D. E., "Literate Programming", 1 January 1992. [LitProg] "Literate programming", Accessed 31 January 2023, 9 January 2023, . [Metanorma] Inc, R., "Metanorma", Accessed 23 April 2021, . [RFC8489] Petit-Huguenin, M., Salgueiro, G., Rosenberg, J., Wing, D., Mahy, R., and P. Matthews, "Session Traversal Utilities for NAT (STUN)", RFC 8489, DOI 10.17487/RFC8489, February 2020, . Appendix A. Installation A computerate specification can be converted into an informal specification with the "computerate" command that is distributed as a Docker image that can be built as follow: docker build git://shalmaneser.org/yathewEngod7#0.0 -t computerate An AsciiDoc file can then be converted with the following command: docker run --rm -v $(pwd):/workspace computerate Note that only the files in the repository and sub-repositories where the command is executed are visible to that command. That means that files or symbolic links to files outside that hierarchy cannot be used. On the other hand external directories mounted with the "-- bind" option can be used. Petit-Huguenin Expires 6 February 2025 [Page 11] Internet-Draft Computerate Specification August 2024 The "computerate" command is configured to include the following Asciidoctor add-ons: * asciidoctor-xml2rfc [draft-petithuguenin-xml2rfc-asciidoc] * asciidoctor-pdf * asciidoctor-revealjs * asciidoctor-epub3 * asciidoctor-idris2 [This document] * asciidoctor-diagram The following diagram generators are available for use by asciidoctor-diagram: * actdiag * blockdiag * graphviz * nwdiag * packetdiag * plantuml * rackdiag * seqdiag The following additional Idris2 packages are installed in the Docker image: * asciidoc [This document] Appendix B. Package asciidoc An Idris2 package to generate a document, an embeddable document, or an inline document in AsciiDoc. Version: 0.0 Author(s): Marc Petit-Huguenin License: AGPL-3.0-or-later Dependencies: contrib B.1. Module Asciidoc A module that defines types for the generic AsciiDoc syntax. data Align : Type Alignment. Left : Align Left alignment. Petit-Huguenin Expires 6 February 2025 [Page 12] Internet-Draft Computerate Specification August 2024 Center : Align Center alignment. Right : Align Right alignment. interface Asciidoc a Things that have an AsciiDoc representation. Implemented by String, Char, Integer, Int, Int8, Int16, Int32, Int64, Bits8, Bits16, Bits32, Bits64, Double, List1. contents : a -> List1 Content Converts a value into inline AsciiDoc. blocks : a -> List1 Block Converts a value into embedded AsciiDoc. data Block : Type Types of blocks. ParagraphBlock : Paragraph -> Block A block of text. LiteralBlock : Literal -> Block A pretty-printed block of text. ImageBlock : Image -> Block An image. SourceBlock : Source -> Block A pretty-printed block of source code. SidebarBlock : Sidebar -> Block Visually separated blocks. QuoteBlock : Quote -> Block A block of prose excerpt, quote or verse. DefinitionListBlock : DefinitionList -> Block An association list. OrderedListBlock : OrderedList -> Block An ordered list. UnorderedListBlock : UnorderedList -> Block An unordered list. Petit-Huguenin Expires 6 February 2025 [Page 13] Internet-Draft Computerate Specification August 2024 TableBlock : Table -> Block A table. IndexBlock : Index -> Block An entry in the index. PassBlock : Pass -> Block Text that is passed directly to the backend. NullBlock : Block OtherBlock : Renderer a => a -> Block Extended block. data Content : Type Types of inline content. TextContent : String -> Content Plain text content. BreakContent : Content An hard line break. ItalicContent : List Content -> Content Italicized content. LinkContent : Link -> Content An hyperlink. IndexContent : Index -> Content An entry in the index. BoldContent : List Content -> Content Bold content. SubscriptContent : List Content -> Content Subscript content. SuperscriptContent : List Content -> Content Superscript content. MonospaceContent : List Content -> Content Monospaced content. CrossrefContent : Crossref -> Content A cross-reference to another part of the document. Petit-Huguenin Expires 6 February 2025 [Page 14] Internet-Draft Computerate Specification August 2024 PassContent : String -> Content Text that is passed directly to the backend. OtherContent : Renderer a => a -> Content Extended content. record Crossref A cross-reference content. MkCrossref: (target : String) -> (content : List Content) -> Crossref target: An identifier for the target of the cross-reference. content: The text for the cross-reference. record DefinitionList A definitition list. MkDefinitionList: (id : Maybe String) -> (content : List1 (DefinitionTerm, Item)) -> DefinitionList id: Identifier. content: A non-empty list of definition term. record DefinitionTerm A definition term. MkDefinitionTerm: (id : Maybe String) -> (content : List Content) -> DefinitionTerm id: Identifier. content: List of content. record Image An image. MkImage: (align : Maybe Align) -> (alt : Maybe String) -> (id : Maybe String) -> (src : String) -> Image align: Alignment. alt: Alternate description. id: Identifier. src: SVG source. record Index Petit-Huguenin Expires 6 February 2025 [Page 15] Internet-Draft Computerate Specification August 2024 An index term content MkIndex: (item : String) -> (primary : Maybe ()) -> (subitem : Maybe String) -> Index item: The primary term. subitem: The secondary term. record Item A list or table cell. MkItem: (id : Maybe String) -> (ref : Maybe String) -> (align : Maybe Align) -> (colspan : Maybe Nat) -> (rowspan : Maybe Nat) -> (content : Either (List1 Block) (List Content)) -> Item id: Identifier. align: Alignment. content: Either a non-empty list of blocks or a list of content. record Link A link content. MkLink: (target : String) -> (content : String) -> Link target: A URL. content: The text for the link. record Literal Literal. MkLiteral: (id : Maybe String) -> (style : Maybe String) -> (content : Doc ()) -> Literal id: Identifier. style: Style. content: Pretty-printable content. data Marker : Type Unordered list label style. Circle : Marker Symbol. Petit-Huguenin Expires 6 February 2025 [Page 16] Internet-Draft Computerate Specification August 2024 NoBullet : Marker No symbol, but indented. Unstyled : Marker No symbol, but not indented. data NumberType : Type Ordered list label type. Lowercase : NumberType Lower case alphabetic. Uppercase : NumberType Upper case alphabetic. Decimal : NumberType Decimal numbers. LowercaseRoman : NumberType Lower case roman numeral. UppercaseRoman : NumberType Upper case roman numeral. record OrderedList An ordered list. MkOrderedList: (id : Maybe String) -> (group : Maybe String) -> (start : Maybe Nat) -> (type : Maybe NumberType) -> (content : List1 Item) -> OrderedList id: Identifier. group: Numbering group. start: Numbering start. type: Labels type. content: A non-empty list of items. record Paragraph A paragraph. MkParagraph: (id : Maybe String) -> (content : List Content) -> Paragraph id: Identifier. content: The list of content. record Pass Petit-Huguenin Expires 6 February 2025 [Page 17] Internet-Draft Computerate Specification August 2024 Passthrough. MkPass: (id : Maybe String) -> (content : String) -> Pass id: Identifier. content: Text passed through. record Quote A quote. MkQuote: (id : Maybe String) -> (cite : Maybe String) -> (quotedFrom : Maybe String) -> (content : Either (List1 Block) (List1 Content)) -> Quote id: Identifier. cite: Source of the citation. quotedFrom: Origin of the quote. content: Either a non-empty list of blocks or a non-empty list of content. record Row A table row. MkRow: (id : Maybe String) -> (content : List1 (Either Item Item)) -> Row id: Identifier. content: A non-empty list of items. record Sidebar A sidebar, MkSidebar: (id : Maybe String) -> (content : List Block) -> Sidebar id: Identifier. content: List of blocks. record Source MkSource: (id : Maybe String) -> (type : Maybe String) -> (content : Doc ()) -> Source record Table A table. Petit-Huguenin Expires 6 February 2025 [Page 18] Internet-Draft Computerate Specification August 2024 MkTable: (id : Maybe String) -> (title : Maybe (List Content)) -> (align : Maybe Align) -> (head : Maybe (List1 Row)) -> (body : List1 Row) -> (foot : Maybe (List1 Row)) -> Table id: Identifier. title: Title. align: Alignment. head: An non-empty list of rows for the header. body: An non-empty list of rows. foot: An non-empty list of rows for the footer. record UnorderedList An unordered list. MkUnorderedList: (id : Maybe String) -> (title : Maybe (List Content)) -> (marker : Marker) -> (content : List1 Item) -> UnorderedList id: Identifier. title: Title. marker: Type of symbol. content: A non-empty list of items. blocks' : {ty : Type} -> (v : ty) -> Name -> Elab (List1 Block) contents' : {ty : Type} -> (v : ty) -> Name -> Elab (List1 Content) renderBlocks : List1 Block -> String Converts a non-empty list of Block into an embeddable AsciiDoc fragment. renderContents : List1 Content -> String Converts a non-empty list of Content into an inline AsciiDoc fragment. B.2. Module Asciidoc.Xml2rfc A Module that defines types for the AsciiDoc extensions of the "xml2rfc" back-end. record Abstract MkAbstract: (id : Maybe String) -> (title : Maybe (List Content)) -> (blocks : List Block) -> Abstract record Alt Petit-Huguenin Expires 6 February 2025 [Page 19] Internet-Draft Computerate Specification August 2024 MkAlt: (id : Maybe String) -> (content : List1 Block) -> Alt record Appendix MkAppendix: (id : Maybe String) -> (title : Maybe (List Content)) -> (notNumbered : Maybe ()) -> (removeInRfc : Maybe ()) -> (toc : Maybe Bool) -> (blocks : List Block) -> (sections : List Section) -> Appendix record Bcp14 MkBcp14: (content : String) -> Bcp14 record Bibliography MkBibliography: (id : Maybe String) -> (title : Maybe (List Content)) -> (blocks : List Block) -> Bibliography data Category : Type Intended category. StdCategory : Category Standard category. BcpCategory : Category BCP category. ExpCategory : Category Experimental category. InfoCategory : Category Informational category. HistoricCategory : Category Historic category. record Comment MkComment: (id : Maybe String) -> (noDisplay : Maybe ()) -> (source : Maybe String) -> (content : List Content) -> Comment record CrossrefXml2rfc MkCrossrefXml2rfc: (target : String) -> (format : Maybe Format) -> (relative : Maybe String) -> (section : Maybe String) -> (sectionFormat : Maybe SectionFormat) -> (content : List Content) -> CrossrefXml2rfc Petit-Huguenin Expires 6 February 2025 [Page 20] Internet-Draft Computerate Specification August 2024 record DefinitionListXml2rfc MkDefinitionListXml2rfc: (id : Maybe String) -> (indent : Maybe Nat) -> (newline : Maybe ()) -> (compactSpacing : Maybe ()) -> (content : List1 (DefinitionTerm, Item)) -> DefinitionListXml2rfc record Document MkDocument: (title : String) -> (abbrev : Maybe String) -> (category : Category) -> (consensus : Maybe ()) -> (docName : Maybe String) -> (ipr : Maybe Ipr) -> (obsoletes : Maybe String) -> (sortRefs : Maybe ()) -> (submissionType : Maybe Submission) -> (noSymRefs : Maybe ()) -> (tocDepth : Maybe Nat) -> (noTocInclude : Maybe ()) -> (updates : Maybe String) -> (sections : List TopSection) -> Document record Figure MkFigure: (id : Maybe String) -> (name : List Content) -> (content : List1 Block) -> Figure data Format : Type Crossref format. Implements Show. TitleFormat : Format Title format. CounterFormat : Format Counter format. NoneFormat : Format No format. record ImageXml2rfc MkImageXml2rfc: (align : Maybe Align) -> (alt : Maybe String) -> (id : Maybe String) -> (src : String) -> (type : Maybe String) -> (top : Maybe ()) -> (bottom : Maybe ()) -> (content : String) -> ImageXml2rfc data Ipr : Type Intellectual Property Rights. Trust200902Ipr : Ipr Petit-Huguenin Expires 6 February 2025 [Page 21] Internet-Draft Computerate Specification August 2024 NoModificationTrust200902Ipr : Ipr NoDerivativesTrust200902Ipr : Ipr Pre5378Trust200902Ipr : Ipr Trust200811Ipr : Ipr NoModificationTrust200811Ipr : Ipr NoDerivativesTrust200811Ipr : Ipr Full3978Ipr : Ipr NoModification3978Ipr : Ipr NoDerivatives3978Ipr : Ipr Full3667Ipr : Ipr NoModification3667Ipr : Ipr NoDerivatives3667Ipr : Ipr Full2026Ipr : Ipr NoDerivativeWorks2026Ipr : Ipr None : Ipr record LinkXml2rfc MkLinkXml2rfc: (angleBrackets : Maybe ()) -> (target : String) -> (content : String) -> LinkXml2rfc record LiteralXml2rfc MkLiteralXml2rfc: (align : Maybe Align) -> (style : Maybe String) -> (alt : Maybe String) -> (id : Maybe String) -> (name : Maybe String) -> (type : Maybe String) -> (top : Maybe String) -> (bottom : Maybe String) -> (content : Doc ()) -> LiteralXml2rfc record Note MkNote: (id : Maybe String) -> (title : Maybe (List Content)) -> (blocks : List Block) -> Note Petit-Huguenin Expires 6 February 2025 [Page 22] Internet-Draft Computerate Specification August 2024 record OrderedListXml2rfc MkOrderedListXml2rfc: (id : Maybe String) -> (group : Maybe String) -> (indent : Maybe Nat) -> (compactSpacing : Maybe ()) -> (start : Maybe Nat) -> (type : Maybe (NumberType, Maybe (String, String))) -> (content : List1 Item) -> OrderedListXml2rfc record ParagraphXml2rfc MkParagraphXml2rfc: (id : Maybe String) -> (indent : Maybe Nat) -> (keepWithNext : Maybe ()) -> (keepWithPrevious : Maybe ()) -> (content : List Content) -> ParagraphXml2rfc record Section MkSection: (id : Maybe String) -> (title : Maybe (List Content)) -> (notNumbered : Maybe ()) -> (removeInRfc : Maybe ()) -> (toc : Maybe Bool) -> (blocks : List Block) -> (sections : List Section) -> Section data SectionFormat : Type External reference format. Implements Show. CommaSectionFormat : SectionFormat Comma as separator. ParensSectionFormat : SectionFormat Parentheses as separator. BareSectionFormat : SectionFormat Same link withing parentheses. record SourceXml2rfc MkSourceXml2rfc: (id : Maybe String) -> (markers : Maybe ()) -> (name : Maybe String) -> (type : Maybe String) -> (top : Maybe String) -> (bottom : Maybe String) -> (content : Doc ()) -> SourceXml2rfc data Submission : Type Intended stream. IetfSubmission : Submission IETF stream. Petit-Huguenin Expires 6 February 2025 [Page 23] Internet-Draft Computerate Specification August 2024 IabSubmission : Submission IAB stream. IrtfSubmission : Submission IRTF stream. IndependentSubmission : Submission Independent stream. EditorialSubmission : Submission Editorial stream. data TopSection : Type Types of top sections. AbstractTopSection : Abstract -> TopSection The abstract. NormalTopSection : Section -> TopSection A section. BibliographyTopSection : Bibliography -> TopSection A bibliography. AppendixTopSection : Appendix -> TopSection An appendix. IndexTopSection : TopSection The index. OtherTopSection : Renderer a => a -> TopSection Extended top-level section. record Unicode MkUnicode: (id : Maybe String) -> (ascii : Maybe String) -> (format : Maybe String) -> (content : String) -> Unicode record UnorderedListXml2rfc MkUnorderedListXml2rfc: (id : Maybe String) -> (title : Maybe (List Content)) -> (marker : Marker) -> (indent : Maybe Nat) -> (compactSpacing : Maybe ()) -> (content : List1 Item) -> UnorderedListXml2rfc renderDocument : (d : Document) -> String Converts a Document into an Asciidoc document. Petit-Huguenin Expires 6 February 2025 [Page 24] Internet-Draft Computerate Specification August 2024 d: the document. renderSection : Nat -> Section -> String Acknowledgements No technology that cannot explain its own results (LLM, AI/ML) have been involved in the creation of this document or its associated tooling. Contributors Stéphane Bryant Email: stephane.ml.bryant@gmail.com Stephane is a co-founder of the Nephelion project, project that started back in 2014 during a week-end visiting national parks in Utah. Computerate Specifying is the successor of this project, and it could not have been done without the frequent reviews and video calls with Stephane during these last 10 years. Changelog This section is to be removed before publishing as an RFC. Since draft-petithuguenin-computerate-specification-02: * Document: - Update Since draft-petithuguenin-computerate-specification-01: * Document: - Update Since draft-petithuguenin-computerate-specification-00: * Document: - Nits * Tooling: - Patched Idris2 with support for external IdrisDoc generation (docgen) extension. Since draft-petithuguenin-computerate-specifying-17: * Document: - Nits - Add explanations for IdrisDoc generation. - Add explanations for ":idris2-packages:" header attribute. * Tooling: Petit-Huguenin Expires 6 February 2025 [Page 25] Internet-Draft Computerate Specification August 2024 - Patched Idris2 with support for external IdrisDoc generation (docgen) extension. - Add Asciidoc docgen implementation. - Add support for including a ipkg file to generate and include the generated IdrisDoc as an AsciiDoc section. - The content of the ":idris2-packages:" header attribute is passed to the idris2 instance. Author's Address Marc Petit-Huguenin Impedance Mismatch LLC Email: marc@petit-huguenin.org Petit-Huguenin Expires 6 February 2025 [Page 26]