@@ -4,6 +4,89 @@ Syntax Guide
5Examples are mostly adapted from the Idris tutorial.
5Examples are mostly adapted from the Idris tutorial.
10+Source files consist of:
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.
21+ module MyModule -- module header
23+ import Data.Vect -- an import
25+ %default total -- a directive
27+ foo : Nat -- a declaration
30+.. _syntax-module-headers:
35+A file can start with a module header, introduced by the ``module`` keyword:
41+Module names can be hierarchical, with parts separated by ``.``:
45+ module Semantics.Transform
47+Each file can define only a single module, which includes everything defined in
50+Like with declarations, a :ref:`docstring <syntax-comments>` can be used to
51+provide documentation for a module:
55+ ||| Implementation of predicate transformer semantics.
56+ module Semantics.Transform
63+An ``import`` makes the names in another module available for use by the current
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.)
75+Imported modules can be given aliases to make qualified names more compact:
79+ import Data.Vect as V
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``:
86+ import public Data.Vect
@@ -43,6 +126,8 @@ a more interesting example:
43 MyListType : Type
126 MyListType : Type
44 MyListType = List Int
127 MyListType = List Int
129+.. _syntax-data-types:
46Data types
131Data types
47~~~~~~~~~~
132~~~~~~~~~~
@@ -246,6 +331,36 @@ Options
334+.. _syntax-qualified-names:
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*.
345+A qualified name has the symbol's namespace prefixed, separated by a ``.``:
347+.. code-block:: idris
351+This would specifically reference a ``length`` declaration from ``Data.Vect``.
353+Qualified names can be written using two different shorthands:
355+1. Names in modules that are :ref:`imported <syntax-imports>` using an alias
356+ can be qualified by the alias.
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``.
@@ -264,6 +379,8 @@ Multi line String literals
264 this is a
379 this is a
265 string literal"""
380 string literal"""
382+.. _syntax-directives:
267Directives
384Directives
268----------
385----------