@@ -4,6 +4,89 @@ Syntax Guide
44
55Examples are mostly adapted from the Idris tutorial.
66
7+Source File Structure
8+---------------------
9+
10+Source files consist of:
11+
12+1. An optional :ref:`syntax-module-headers`.
13+2. Zero or more :ref:`syntax-imports`.
14+3. Zero or more declarations, e.g. :ref:`syntax-variables`,
15+ :ref:`syntax-data-types`, etc.
16+
17+For example:
18+
19+.. code:: idris
20+
21+ module MyModule -- module header
22+
23+ import Data.Vect -- an import
24+
25+ %default total -- a directive
26+
27+ foo : Nat -- a declaration
28+ foo = 5
29+
30+.. _syntax-module-headers:
31+
32+Module Header
33+~~~~~~~~~~~~~
34+
35+A file can start with a module header, introduced by the ``module`` keyword:
36+
37+.. code-block:: idris
38+
39+ module Semantics
40+
41+Module names can be hierarchical, with parts separated by ``.``:
42+
43+.. code-block:: idris
44+
45+ module Semantics.Transform
46+
47+Each file can define only a single module, which includes everything defined in
48+that file.
49+
50+Like with declarations, a :ref:`docstring <syntax-comments>` can be used to
51+provide documentation for a module:
52+
53+.. code-block:: idris
54+
55+ ||| Implementation of predicate transformer semantics.
56+ module Semantics.Transform
57+
58+.. _syntax-imports:
59+
60+Imports
61+~~~~~~~
62+
63+An ``import`` makes the names in another module available for use by the current
64+module:
65+
66+.. code-block:: idris
67+
68+ import Data.Vect
69+
70+All the declarations in an imported module are available for use in the file.
71+In a case where a name is ambiguous --- e.g. because it is imported from
72+multiple modules, or appears in multiple visible namespaces --- the ambiguity can be resolved using :ref:`syntax-qualified-names`. (Often, the compiler can
73+resolve the ambiguity for you, using the types involved.)
74+
75+Imported modules can be given aliases to make qualified names more compact:
76+
77+.. code-block:: idris
78+
79+ import Data.Vect as V
80+
81+Note that names made visible by import are not, by default, re-exported to
82+users of the module being written. This can be done using ``import public``:
83+
84+.. code-block:: idris
85+
86+ import public Data.Vect
87+
88+.. _syntax-variables:
89+
790Variables
891---------
992
@@ -43,6 +126,8 @@ a more interesting example:
43126 MyListType : Type
44127 MyListType = List Int
45128
129+.. _syntax-data-types:
130+
46131Data types
47132~~~~~~~~~~
48133
@@ -246,6 +331,36 @@ Options
246331Misc
247332----
248333
334+.. _syntax-qualified-names:
335+
336+Qualified Names
337+~~~~~~~~~~~~~~~
338+
339+If multiple declarations with the same name are visible, using the name can
340+result in an ambiguous situation. The compiler will attempt to resolve the
341+ambiguity using the types involved. If it's unable --- for example, because
342+the declarations with the same name also have the same type signatures --- the
343+situation can be cleared up using a *qualified name*.
344+
345+A qualified name has the symbol's namespace prefixed, separated by a ``.``:
346+
347+.. code-block:: idris
348+
349+ Data.Vect.length
350+
351+This would specifically reference a ``length`` declaration from ``Data.Vect``.
352+
353+Qualified names can be written using two different shorthands:
354+
355+1. Names in modules that are :ref:`imported <syntax-imports>` using an alias
356+ can be qualified by the alias.
357+
358+2. The name can be qualified by the *shortest unique suffix* of the
359+ namespace in question. For example, the ``length`` case above can likely
360+ be shortened to ``Vect.length``.
361+
362+.. _syntax-comments:
363+
249364Comments
250365~~~~~~~~
251366
@@ -264,6 +379,8 @@ Multi line String literals
264379 this is a
265380 string literal"""
266381
382+.. _syntax-directives:
383+
267384Directives
268385----------
269386