Agda: Core Syntax Documentation

[pnlph]

I am having trouble finding in the documentation an unitary description of the core syntax of Agda. I found these by now:

• the Core language in readthedocs, self-labeled as stub, where a Term is defined in Agda
• an old Core Syntax in the wiki about the grammar of terms explained in another way
• the Syntax Overview in the wiki that explains in plain english the three key components of the syntax (expressions, declarations and pragmas) and the three levels of interpretation (concrete, abstract and internal) but in the Syntax folder seems to be many more levels of interpretation

Am i missing something? Is this explained somewhere else?

[jespercockx]

Concrete, Abstract, and Internal syntax are the three main forms of syntax that are used internally. Aside from those we also have the 'nice' Concrete syntax (a somewhat cleaned-up version of concrete syntax), Reflected syntax (used for reflection), and Treeless syntax (final stage of syntax before being handed off to one of the backends). The pipeline is as follows:

*.agda file 
   ==[ parser (Lexer.x + Parser.y) ]==> 
Concrete syntax 
   ==[ nicifier (Syntax.Concrete.Definitions) ]==> 
'Nice' concrete syntax 
   ==[ scope checking (Syntax.Translation.ConcreteToAbstract) ]==>
Abstract syntax
   ==[ type checking (TypeChecking.Rules.*) ]==>
Internal syntax
   ==[ Agda.Compiler.ToTreeless ]==>
Treeless syntax
   ==[ different backends (Compiler.MAlonzo.*, Compiler.JS.*, ...) ]==>
Executable

The core language in the stub on ReadTheDocs corresponds to the Haskell datatype used for the Internal syntax.

I don't think most of this is really officially documented, PRs for the documentation are always welcome.

[banacorn]

It's nice to know about the existence of these syntax.