From a03c3bf376f34c13ebc48022e72bd49194eac452 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Tue, 21 Nov 2023 20:20:14 -0800 Subject: [PATCH 1/2] [ doc ] Add missing pragmas to documentation --- docs/source/backends/backend-cookbook.rst | 2 + docs/source/ffi/ffi.rst | 2 + docs/source/implementation/overview.rst | 2 + docs/source/reference/debugging.rst | 1 + docs/source/reference/pragmas.rst | 382 +++++++++++++++++++++- docs/source/reference/records.rst | 2 + docs/source/updates/updates.rst | 4 + 7 files changed, 377 insertions(+), 18 deletions(-) diff --git a/docs/source/backends/backend-cookbook.rst b/docs/source/backends/backend-cookbook.rst index d8d50c29a..c20f9c8bb 100644 --- a/docs/source/backends/backend-cookbook.rst +++ b/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 diff --git a/docs/source/ffi/ffi.rst b/docs/source/ffi/ffi.rst index 8e43374c4..3ba431c47 100644 --- a/docs/source/ffi/ffi.rst +++ b/docs/source/ffi/ffi.rst @@ -1,3 +1,5 @@ +.. _ffi-overview: + ************ FFI Overview ************ diff --git a/docs/source/implementation/overview.rst b/docs/source/implementation/overview.rst index 194b8ca1a..fcc93cc92 100644 --- a/docs/source/implementation/overview.rst +++ b/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 ----------------- diff --git a/docs/source/reference/debugging.rst b/docs/source/reference/debugging.rst index f3622c8ab..e2a617ed3 100644 --- a/docs/source/reference/debugging.rst +++ b/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 ======= diff --git a/docs/source/reference/pragmas.rst b/docs/source/reference/pragmas.rst index c568490d1..fba8d6443 100644 --- a/docs/source/reference/pragmas.rst +++ b/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. The initial value is `covering`, which +required case statements to cover, but does not require totality. The other options are +`total` and `partial`. ``%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,247 @@ 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` for more). + + +``%defaulthint`` +-------------------- + +Mark a default for functions like ``fromString`` in cases where the compiler cannot +determine which type the user wants. + +``%globalhint`` +-------------------- + +This pragma is similar to ``%defaulthint``. + +``%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`. + +``%MkWorld`` +-------------------- + +The world token used for IO. For more information, see :ref:`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. + diff --git a/docs/source/reference/records.rst b/docs/source/reference/records.rst index 85cf07446..e0be6c5aa 100644 --- a/docs/source/reference/records.rst +++ b/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 ------------------ diff --git a/docs/source/updates/updates.rst b/docs/source/updates/updates.rst index e8b36661a..e8a872025 100644 --- a/docs/source/updates/updates.rst +++ b/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 --------------------------------- From 60ec783483beb738e7f6f7b23b435e345d8fd94a Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Thu, 23 Nov 2023 14:28:15 -0800 Subject: [PATCH 2/2] [ doc ] updates to hint documentation. --- docs/source/reference/pragmas.rst | 16 +++++++++------- docs/source/tutorial/miscellany.rst | 2 ++ 2 files changed, 11 insertions(+), 7 deletions(-) diff --git a/docs/source/reference/pragmas.rst b/docs/source/reference/pragmas.rst index fba8d6443..cd50d6902 100644 --- a/docs/source/reference/pragmas.rst +++ b/docs/source/reference/pragmas.rst @@ -29,9 +29,9 @@ Enable language extensions. Currently, the only extension is ``ElabReflection`` ``%default`` -------------------- -Set the default totality requirement for functions. The initial value is `covering`, which -required case statements to cover, but does not require totality. The other options are -`total` and `partial`. +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`` -------------------- @@ -283,19 +283,21 @@ This pragma is deprecated. Instead use ``%export`` to expose functions to the b ``%hint`` -------------------- -Mark a function to be used for ``auto`` search (see :ref:`auto-implicits` for more). +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 default for functions like ``fromString`` in cases where the compiler cannot -determine which type the user wants. +Mark a hint to be tried when no other hints match. ``%globalhint`` -------------------- -This pragma is similar to ``%defaulthint``. +A global hint is like a ``%hint``, but it is always tried, while ``%hint`` is only tried if the return +type matches. ``%extern`` -------------------- diff --git a/docs/source/tutorial/miscellany.rst b/docs/source/tutorial/miscellany.rst index c0f45d67f..a87972d43 100644 --- a/docs/source/tutorial/miscellany.rst +++ b/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 -----------------------