// SPDX-License-Identifier: CC-BY-SA-4.0
= A2ML v0 Specification (Draft)
:toc:
:toclevels: 3
:icons: font

[IMPORTANT]
====
*FROZEN ARCHIVE — NOT NORMATIVE.* This is the original v0 draft, retained
for lineage only. The current normative specification is `../SPEC.adoc`
(v1.1.0). See `../VERSIONS.adoc` for the full lineage. Do not edit this
file except to correct transcription errors.
====

== Overview

A2ML has two layers:

* Surface syntax (lightweight markup)
* Typed core (Idris2 model with proof obligations)

The surface grammar is independent from Idris; Idris is the semantic core.
Multiple surface syntaxes may compile to the same typed core.

== Example Applications

A2ML is agnostic about delivery pipelines. Projects like
stateful-artefacts-for-gitforges are example applications that demonstrate
event-chain workflows (metadata updates -> attested compile -> rendered artifacts).
A2ML itself remains independent of that ecosystem and can be used in other
pipelines.

== Lexical Rules

* Line: a sequence of characters ending in LF or EOF
* Blank line: line containing only whitespace
* Identifier: `ID = [A-Za-z][A-Za-z0-9:_-]*`
* String: `"..."` or `'...'` with `\\` and escaped quote support

== Surface Grammar (EBNF)

[source]
----
Document     ::= Block*
Block        ::= Heading
              | DirectiveBlock
              | List
              | CodeBlock
              | Paragraph
              | Blank

Blank        ::= BlankLine+

Heading      ::= HeadingLine HeadingBody?
HeadingLine  ::= HeadingMarker SP TextLine
HeadingMarker::= "#" | "##" | "###" | "####" | "#####"
HeadingBody  ::= Block*         // until next same-or-higher heading or EOF

DirectiveBlock ::= "@" Name Attrs? ":" NL DirectiveBody "@end"
Name          ::= ID
Attrs         ::= "(" Attr ("," Attr)* ")"
Attr          ::= ID "=" (ID | STRING | Number)
Number        ::= "-"? [0-9]+ ("." [0-9]+)?

DirectiveBody ::= Block*         // nested blocks allowed

List         ::= ListItem (NL ListItem)*
ListItem     ::= ("-" | "*") SP Inline

CodeBlock    ::= FenceLang? NL RawLines FenceEnd
FenceLang    ::= "```" LangSpec?
LangSpec     ::= [A-Za-z0-9_+-]+
FenceEnd     ::= "```"

Paragraph    ::= Inline (NL Inline)*
Inline       ::= InlineAtom (SP InlineAtom)*
InlineAtom   ::= Emph | Strong | Link | Ref | Text

Emph         ::= "*" TextInline "*"
Strong       ::= "**" TextInline "**"
Link         ::= "[" TextInline "]" "(" URL ")"
Ref          ::= "@ref(" ID ")"

TextInline   ::= (TextChar | Escaped)+
TextChar     ::= any char except control, "*", "[", "]", "@", NL
Escaped      ::= "\\" any

TextLine     ::= (TextChar | Escaped)*

RawLines     ::= (RawLine NL)*
RawLine      ::= any char sequence (including punctuation)
URL          ::= [^ )\n]+
SP           ::= " "+
NL           ::= "\n"
----

== Core Directives (v0)

* `@abstract` (declares the abstract)
* `@refs` (declares references)
* `@fig` (figure block)
* `@table` (table block)
* `@requires` (structural dependencies)
* `@opaque` (byte-for-byte payload preservation)

== Inline Parsing (Prototype)

The v0 prototype supports inline emphasis, strong, and links:

* `*text*` -> emphasis
* `**text**` -> strong
* `[label](url)` -> link

See link:docs/INLINE-RULES.adoc[INLINE-RULES] for the prototype rules.

== Prototype Coverage Notes (Module 0)

The Module 0 prototype in `prototype/rescript/` is intentionally small:

* Directive headers MUST be on a single line and end with `:`.
* `@refs` content is parsed as one paragraph per non-blank line.
* `@opaque` content is treated as raw lines until `@end` and preserved verbatim.
* Heading bodies are not nested; headings are standalone blocks.
* Code fences are not implemented in the prototype.

== Semantics (Surface -> Typed Core)

1) Headings become `Section` nodes.
2) Directives map to typed core nodes with parameters.
3) References must resolve in checked/attested modes.
4) Opaque payloads are preserved byte-for-byte.
5) Attested mode enforces structural invariants (e.g., required sections).

== Modes

* Lax: best-effort parsing, warnings only.
* Checked: IDs required, references must resolve, no unknown directives.
* Attested: typed core + proof obligations must discharge.

== Profiles (Non-Executable)

Profiles are named validation bundles that add required sections, fields, and
structural rules on top of the base A2ML modes. Profiles do not grant execution
capabilities or side effects. They are strictly about validation and attestation.

* Profiles are optional and MUST be safe under Checked/Attested modes.
* A profile MUST NOT imply command execution, network access, or filesystem writes.
* Tools MAY expose profiles via flags (e.g., `--profile contractiles-v1`).
* If a profile is declared in a document, validators SHOULD enforce it.

This allows “active” or “attested” variants (often described as A2MLa) without
introducing a new executable file type. A2ML remains read-only; profiles only
increase validation strictness.

== Typed Core (Idris2 Outline)

[source]
----
data Doc : Type where
  MkDoc : Meta -> List Block -> Doc

data Block : Type where
  Section  : Sec -> Block
  Para     : List Inline -> Block
  List     : List (List Inline) -> Block
  Figure   : Fig -> Block
  Table    : Tbl -> Block
  Refs     : RefList -> Block
  Opaque   : OpaquePayload -> Block

data Sec : Type where
  MkSec : (id : Id) -> (title : Text) -> (reqs : List Req) -> (body : List Block) -> Sec

data Fig : Type where
  MkFig : (id : Id) -> (caption : Text) -> (ref : Maybe Id) -> Fig

data RefList : Type where
  MkRefs : List Ref -> RefList

data OpaquePayload : Type where
  MkOpaque : (id : Maybe Id) -> (lang : Maybe Lang) -> (bytes : ByteString) -> OpaquePayload
----

== Invariants (Attested Mode)

* Unique IDs across the document
* All references resolve to existing IDs
* Required sections present (policy-configurable)
* Optional rules (e.g., each figure must be referenced)

== Opaque Payloads (Non-Negotiable)

Opaque payloads MUST be preserved byte-for-byte in the typed core.
Renderers MAY transform only when the target format requires it, and must
report transformations.

== Non-Goals (v0)

* No semantic-web ontology requirements
* No runtime execution in documents
* No dependency on a single output format
