Merge pull request #3148 from dunhamsteve/doc-pragma

[ doc ] Add missing pragmas to documentation

docs/source/backends/backend-cookbook.rst

@@ -182,6 +182,8 @@ custom back-end and diverging from the Idris representation is not a good idea.
 The best approach here is to build a conversion layer between the string
 representation of the custom back-end and the runtime.
 
+.. _sect-world:
+
 **World**
 
 In pure functional programming, causality needs to be represented whenever we

docs/source/ffi/ffi.rst

@@ -1,3 +1,5 @@
+.. _ffi-overview:
+
 ************
 FFI Overview
 ************

docs/source/implementation/overview.rst

@@ -253,6 +253,8 @@ Once we know what the bound implicits need to be, we bind them in
 gets turned into a local binding (either Pi or Pat as appropriate, or PLet for
 @-patterns).
 
+.. _unbound-implicits:
+
 Unbound Implicits
 -----------------
 

docs/source/reference/debugging.rst

@@ -10,6 +10,7 @@ The compiler has the ``--timing`` flag to dump timing information collected duri
 The output documents, in reverse chronological order, the cumulative time taken for the operation (and sub operations) to complete.
 Sub levels are indicated by successive repetitions of ``+``.
 
+.. _sect-logging:
 
 Logging
 =======

docs/source/reference/pragmas.rst

@@ -14,17 +14,127 @@ small niche of pragmas apply directly to one or more arguments instead of the co
     This page is a work in progress. If you know about a pragma that is not described yet, please consider
     submitting a pull request!
 
+Global pragmas
+====================
+
+``%language``
+--------------------
+
+Enable language extensions.  Currently, the only extension is ``ElabReflection``.
+
+.. code-block:: idris
+
+   %language ElabReflection
+
+``%default``
+--------------------
+
+Set the default totality requirement for functions, which can be one of ``total``,
+``covering``, or ``partial``.  The value is initially set to ``covering`` unless the ``--total``
+command line switch is used, which sets it to ``total``.
 
 ``%builtin``
-====================
+--------------------
 
 The ``%builtin Natural`` pragma converts recursive/unary representations of natural numbers
 into primitive ``Integer`` representations.
 
 This pragma is explained in detail on its own page. For more, see :ref:`builtins`.
 
+
+``%name``
+--------------------
+
+Give the compiler some suggested names to use for a particular type when it is asked to generate names for values.
+You can specify any number of suggested names; they will be used in-order when more than one is needed for a single
+definition.
+
+.. code-block:: idris
+
+   data Foo = X | Y
+
+   %name Foo foo,bar
+
+
+``%ambiguity_depth``
+--------------------
+
+Set how deep nested ambiguous names can be before Idris gives up. The default is 3, increashing this
+will effect compiler performance. For more details, see :ref:`ambiguous-name-resolution`.
+
+``%auto_implicit_depth``
+------------------------
+
+Set the search depth for ``auto`` implicits. The default value is 50.
+
+``%logging``
+--------------------
+
+ Change the logging level.  See :ref:`sect-logging` for details.
+
+ .. code-block:: idris
+
+    %logging 1
+    %logging "elab" 5
+
+
+``%prefix_record_projections``
+------------------------------
+
+Configure whether projection functions without a leading period are generated for records. It defaults
+to ``on``.  See :ref:`record-elaboration` for more details.
+
+.. code-block:
+   %prefix_record_projections on
+
+``%transform``
+--------------------
+
+Replace a function at runtime with another implementation. It allows us to
+functions that are appropriate for type checking and have an efficient version at runtime. For example:
+
+.. code-block:: idris
+
+    plus : Nat -> Nat -> Nat
+    plus Z y = y
+    plus (S x) y = S $ plus x y
+
+    %transform "plus" plus j k = integerToNat (natToInteger j + natToInteger j)
+
+``%unbound_implicits``
+----------------------
+
+Configure whether implicit bindings are automatically added to function types for unbound
+lowercase names. It is on by default. See :ref:`unbound-implicits` for more details.
+
+``%auto_lazy``
+--------------------
+
+Configure whether the compiler automatically adds ``delay`` and ``force`` when
+necessary.  It defaults to ``on``.
+
+
+``%search_timeout``
+--------------------
+
+Set the expression search timeout in milliseconds.  The default is 1000.
+
+.. code-block:: idris
+
+   %search_timeout 1000
+
+
+``%nf_metavar_threshold``
+-------------------------
+
+Set the maximum number of stuck applications allowed while unifying a meta. The
+default value is 25.
+
+Pragmas on declarations
+=======================
+
 ``%deprecate``
-====================
+--------------------
 
 Mark the following definition as deprecated. Whenever the function is used, Idris will show a deprecation
 warning.
@@ -61,10 +171,10 @@ deprecated function call and that documentation will be displayed alongside the
      Please use the @altFoo@ function from now on.
 
 ``%inline``
-====================
+--------------------
 
 Instruct the compiler to inline the following definition when it is applied. It is generally best to let the
-compiler and the backend you are using optimize code based on its predetermined rules, but if you want to
+compiler and the backend you are using optimise code based on its predetermined rules, but if you want to
 force a function to be inlined when it is called, this pragma will force it.
 
 .. code-block:: idris
@@ -74,10 +184,10 @@ force a function to be inlined when it is called, this pragma will force it.
    foo x = x ++ "!"
 
 ``%noinline``
-====================
+--------------------
 
 Instruct the compiler _not_ to inline the following definition when it is applied. It is generally best to let the
-compiler and the backend you are using optimize code based on its predetermined rules, but if you want to
+compiler and the backend you are using optimise code based on its predetermined rules, but if you want to
 force a function to never be inlined when it is called, this pragma will force it.
 
 .. code-block:: idris
@@ -86,21 +196,13 @@ force a function to never be inlined when it is called, this pragma will force i
    foo : String -> String
    foo x = x ++ "!"
 
-``%name``
-====================
+``%tcinline``
+--------------------
 
-Give the compiler some suggested names to use for a particular type when it is asked to generate names for values.
-You can specify any number of suggested names; they will be used in-order when more than one is needed for a single
-definition.
-
-.. code-block:: idris
-
-   data Foo = X | Y
-
-   %name Foo foo,bar
+Instruct the compiler to inline the function during totality checking.
 
 ``%hide``
-====================
+--------------------
 
 Hide a definition from imports. This is particularly useful when you are re-definiing functions or types from
 a module but still need to import it.
@@ -124,3 +226,249 @@ You can also hide fixity declarations if you need to redefine your own.
    %hide Prelude.Ops.infixl.(+)
 
    infixr 5 +
+
+
+``%unhide``
+--------------------
+
+The ``%unhide`` pragma unhides a definition that was previously hidden with ``%hide``.
+
+
+``%unsafe``
+--------------------
+
+Mark a function like ``believe_me`` as being unsafe. The function will be semantically
+highlighted in a different color to draw the user's attention to its use.
+
+
+``%spec``
+--------------------
+
+Specialise a function according to a list of arguments.
+
+.. code-block:: idris
+
+   %spec a
+   identity : List a -> List a
+   identity [] = []
+   identity (x :: xs) = x :: identity xs
+
+
+``%foreign``
+--------------------
+
+Declare a foreign function.  It is followed by an indented block of expressions
+that evaluate to strings. See :ref:`ffi-overview` for more details.
+
+``%export``
+--------------------
+
+Export an Idris function to the underlying host language. The the name for each backend is
+given in an indented block of string expressions, similar to ``%foreign``.  Currently this
+pragma is only supported by the javascript backend.
+
+.. code-block:: idris
+
+   %export "javascript:addNat"
+   addNat : Nat -> Nat -> Nat
+   addNat a b = a + b
+
+
+``%nomangle``
+--------------------
+
+This pragma is deprecated.  Instead use ``%export`` to expose functions to the backend.
+
+
+``%hint``
+--------------------
+
+Mark a function to be used for ``auto`` search (see :ref:`auto-implicits` and
+:ref:`auto-implicit-arguments` for more).  Hints are used internally for instance
+resolution and non-named instances are automatically tagged with ``%hint``.
+
+
+``%defaulthint``
+--------------------
+
+Mark a hint to be tried when no other hints match.
+
+``%globalhint``
+--------------------
+
+A global hint is like a ``%hint``, but it is always tried, while ``%hint`` is only tried if the return
+type matches.
+
+``%extern``
+--------------------
+
+Declare a function to be externally implemented, but relies on codegen
+to fill in the function rather than specifying the name. The function name must be explicitly
+handled in the codegen. It is used for functions like ``prim__newIORef`` in the prelude.
+
+
+``%macro``
+--------------------
+
+Mark a function that returns the ``Elab`` monad as a macro. When the function is used in
+an expression, it will be run at compile time and the invocation will be replaced by the
+result of the elaboration.
+
+``%start``
+--------------------
+
+The ``%start`` pragma is not implemented.
+
+``%allow_overloads``
+--------------------
+
+This pragma is no longer used by the compiler.
+
+Internal
+========
+
+These pragmas are used in the prelude, but aren't typically used in user programs.
+
+
+``%rewrite``
+--------------------
+
+Specify the `Equal` type and rewrite function used by rewrite statements.
+
+.. code-block:: idris
+
+   %rewrite Equal rewrite__impl
+
+``%pair``
+--------------------
+
+This directive is used in the prelude to tell auto implicit search what to use to look inside pairs.
+
+.. code-block:: idris
+
+   %pair Pair fst snd
+
+``%integerLit``
+--------------------
+
+Define the function used to interpret literal integers. In the prelude, it is set
+to ``fromInteger``, so a literal ``2`` is elaborated to ``fromInteger 2``.
+
+.. code-block:: idris
+
+   %integerLit fromInteger
+
+``%stringLit``
+--------------------
+
+Define the function used to interpret literal strings. In the prelude, it is set
+to ``fromString``, so a literal ``"idris"`` is elaborated to ``fromString "idris"``.
+
+.. code-block:: idris
+
+   %stringLit fromString
+
+
+``%charLit``
+--------------------
+
+Define the function used to interpret literal characters. In the prelude, it is set
+to ``fromChar``, so a literal ```x```` is elaborated to ``fromChar 'x'``.
+
+.. code-block:: idris
+
+   %charLit fromChar
+
+``%doubleLit``
+--------------------
+
+Define the function used to interpret literal numbers with a decimal in them. In the prelude, it is set
+to ``fromDouble``, so a literal ```2.0```` is elaborated to ``fromDouble 2.0``.
+
+.. code-block:: idris
+
+   %charLit fromDouble
+
+
+Reflection Literals
+===================
+
+
+``%TTImpLit``
+--------------------
+
+Allow quoted expressions to be cast to a user defined type.
+
+.. code-block:: idris
+
+   %TTImpLit fromTTImp
+
+   public export
+   data NatExpr : Type where
+        Plus : NatExpr -> NatExpr -> NatExpr
+        Mult : NatExpr -> NatExpr -> NatExpr
+        Val : Nat -> NatExpr
+        Var : String -> NatExpr
+
+   public export
+   natExpr : TTImp -> Elab NatExpr
+   natExpr `(~(l) + ~(r)) = [| Plus (natExpr l) (natExpr r) |]
+   natExpr `(~(l) * ~(r)) = [| Mult (natExpr l) (natExpr r) |]
+   natExpr `(fromInteger ~(IPrimVal _ (BI n))) = pure $ Val $ fromInteger n
+   natExpr (IVar _ (UN (Basic nm))) = pure $ Var nm
+   natExpr s = failAt (getFC s) "Invalid NatExpr"
+
+   %macro
+   fromTTImp : TTImp -> Elab NatExpr
+   fromTTImp = natExpr
+
+   export
+   natExprMacroTest : NatExpr
+   natExprMacroTest = `(1 + 2 + x)
+
+``%declsLit``
+--------------------
+
+Allow quoted declarations to be cast to user defined types.
+
+``%nameLit``
+--------------------
+
+Allow quoted names to be cast to user defined types.
+
+
+Expressions
+===========
+
+Pragmas that occur inside expressions.
+
+``%runElab``
+--------------------
+
+The ``%runElab`` pragma can be used at the top level or as an expression. It takes the an elaboration
+script as an argument which runs in the ``Elab`` monad, has access to Idris' type-checking machinery,
+and can generate code.
+
+``%search``
+--------------------
+
+Ask Idris to fill in the value with auto-implicit search. See :ref:`auto-implicits` for more details.
+
+``%World``
+--------------------
+
+The type of the world token used for IO.  For more information, see :ref:`World<sect-world>`.
+
+``%MkWorld``
+--------------------
+
+The world token used for IO.  For more information, see :ref:`World<sect-world>`.
+
+``%syntactic``
+--------------------
+
+The ``%syntactic`` pragma can appear after the ``with`` keyword.  It abstracts
+over the value syntactically, rather than by value, and can significantly speed
+up elaboration where large types are involved, at a cost of being less general.
+Try it if "with" is slow.
+

docs/source/reference/records.rst

@@ -50,6 +50,8 @@ Desugaring rules
 * ``(simpleExpr .field1 .field2 .field3)`` desugars to ``((.field .field2
   .field3) simpleExpr)``
 
+.. _record-elaboration:
+
 Record elaboration
 ------------------
 

docs/source/tutorial/miscellany.rst

@@ -20,6 +20,8 @@ omitted when they can be inferred by the type checker [#IdrisType]_, e.g.
 
     index : forall a, n . Fin n -> Vect n a -> a
 
+.. _auto-implicit-arguments:
+
 Auto implicit arguments
 -----------------------
 

docs/source/updates/updates.rst

@@ -245,6 +245,8 @@ in the prelude in:
 Smaller Changes
 ===============
 
+.. _ambiguous-name-resolution:
+
 Ambiguous Name Resolution
 -------------------------
 
@@ -360,6 +362,8 @@ below.
 Also, an alternative syntax ``let x := val in e`` is available.
 See Section :ref:`sect-let-bindings` for more info.
 
+.. _auto-implicits:
+
 ``auto``-implicits and Interfaces
 ---------------------------------