0 | module Idris.Doc.Keywords
2 | import Decidable.Equality
3 | import Parser.Lexer.Source
4 | import Data.List.Quantifiers
7 | import Idris.Doc.Annotations
10 | import Libraries.Data.List.Quantifiers.Extra
13 | private infix 10 ::=
15 | data DocFor : String -> Type where
16 | (::=) : (0 str : String) -> (doc : Doc IdrisDocAnn) -> DocFor str
18 | doc : DocFor _ -> Doc IdrisDocAnn
21 | fixity : Doc IdrisDocAnn
23 | header "Fixity declarations" :: ""
26 | Operators can be assigned a priority level and associativity. During parsing
27 | operators with a higher priority will collect their arguments first and the
28 | declared associativity will inform how subterms are grouped.
30 | For instance the expression `a + b * c * d + e` is parsed as
31 | `(a + ((b * c) * d)) + e` because:
32 | `(+)` is at level 8 and associates to the left
33 | `(*)` is at level 9 and associates to the left
36 | recordtypes : Doc IdrisDocAnn
37 | recordtypes = vcat $
38 | header "Record types" :: ""
41 | Records are data types with a single constructor. Each of the constructor's
42 | argument is given a name and the corresponding projections and record update
43 | functions are automatically generated.
44 | For instance, we can define a type of pairs of natural numbers
55 | and we can then immediately use all of `fst`, `snd`, `{ fst := ?h1 }`,
56 | or `{ snd $= ?h2 }` to respectively project values out of a record,
57 | replace values, or update them.
61 | datatypes : Doc IdrisDocAnn
63 | header "(Co)Data types" :: ""
66 | Keyword to introduce a (co)inductive type definition.
67 | You can either use a BNF-style definition for simple types
71 | data List a = Nil | (::) a (List a)
75 | or a GADT-style definition for indexed types
79 | data Vect : Nat -> Type -> Type where
81 | (::) : a -> Vect n a -> Vect (S n) a
85 | Coinductive data is introduced using the same syntax except
86 | that the type of potentially infinite subterms is wrapped in
87 | an `Inf` type constructor.
90 | totality : Doc IdrisDocAnn
92 | header "Totality" :: ""
95 | Definitions can be individually declared `total`, `covering`, or `partial`.
96 | It is also possible to set the default totality flag for definitions in a
97 | module by using the `%default` pragma.
100 | * `total` offers the highest guarantees. Definitions using this flag are
102 | 1. their patterns are covering all possible cases;
103 | 2. they are either obviously terminating (for recursive functions)
104 | or productive (for corecursive functions);
105 | 3. all the auxiliary functions used are total themselves.
108 | * `covering` is the default level of guarantees. It only enforces that
109 | pattern matchings are exhaustive.
112 | * `partial` is the absence of any totality requirement: as long as the
113 | definition typechecks, it is accepted. It is possible to call a partial
114 | function from a total one by using the `assert_total` escape hatch.
117 | visibility : Doc IdrisDocAnn
118 | visibility = vcat $
119 | header "Visibility" :: ""
120 | :: map (indent 2) [
122 | Programmers can decide which parts of a module they expose to the outside
126 | * `public export` ensures that both the declaration and the definition
127 | are accessible from the outside of the module. This means the function
128 | will be able to reduce in types.
131 | * `export` means that only the declaration will be made available to the
132 | outside world. Users will be able to call the function but its internals
133 | will not be exposed because it will not reduce in types.
136 | * `private` means that neither the declaration nor the definition will be
137 | exported. This is the default and is the ideal setting for auxiliary
141 | If a forward-declaration for a definition exists, they cannot declare
142 | incompatible visibility modifiers - they either have to match up or at most
143 | one of the two can declare visibility.
146 | ifthenelse : Doc IdrisDocAnn
147 | ifthenelse = vcat $
148 | header "Boolean conditional" :: ""
149 | :: map (indent 2) [
151 | The `if ... then ... else ...` construct is dependently typed. This means
152 | that if you are branching over a variable, the branches will have refined
153 | types where that variable has been replaced by either `True` or `False`.
154 | For instance, in the following incomplete program
158 | notInvolutive : (b : Bool) -> not (not b) === b
159 | notInvolutive b = if b then ?holeTrue else ?holeFalse
163 | the two holes have respective types `True === True` and `False === False`.
166 | If you do not need the added power granted by dependently typed branches,
167 | consider using the simpler `ifThenElse` function defined in `Prelude`.
170 | impossibility : Doc IdrisDocAnn
171 | impossibility = vcat $
172 | header "Impossible branches" :: ""
173 | :: map (indent 2) [
175 | The `impossible` keyword can be used to dismiss a clause involving an
176 | argument with an uninhabited type. For instance an assumption stating
177 | that 0 is equal to 1:
181 | zeroIsNotOne : 0 === 1 -> Void
182 | zeroIsNotOne eq impossible
186 | caseof : Doc IdrisDocAnn
188 | header "Case block" :: ""
189 | :: map (indent 2) [
191 | The `case ... of ...` construct is dependently typed. This means that if you
192 | are branching over a variable, the branches will have refined types where
193 | that variable has been replaced by the appropriate pattern.
194 | For instance, in the following program
198 | assoc : (ma, mb, mc : Maybe a) ->
199 | ((ma <|> mb) <|> mc) === (ma <|> (mb <|> mc))
200 | assoc ma mb mc = case ma of
206 | the branches typecheck because in their respective types `ma` has been replaced
207 | either by `Nothing` or `Just a` and that was enough for them to compute to
208 | `(mb <|> mc) === (mb <|> mc)` and `Just a === Just a` respectively. Both of
209 | which can be discharged using `Refl`.
212 | importing : Doc IdrisDocAnn
214 | header "Importing" :: ""
215 | :: map (indent 2) [
217 | Importing a module brings the definition it exports into scope.
218 | Combined with `public` it also re-exports these definitions.
221 | forallquantifier : Doc IdrisDocAnn
222 | forallquantifier = vcat $
223 | header "Forall quantifier" :: ""
224 | :: map (indent 2) [
226 | `forall` quantification is syntactic sugar for implicit runtime-irrelevant
227 | universal quantification. That is to say that `forall x, y, z. ...`
228 | desugars to `{0 x, y, z : _} -> ...`.
231 | implicitarg : Doc IdrisDocAnn
232 | implicitarg = vcat $
233 | header "Implicit arguments" :: ""
234 | :: map (indent 2) [
236 | Implicit arguments can be solved using various strategies. By default
237 | they will be filled in using unification but programmers can use various
238 | keywords to change that.
241 | * `auto` will use the same mechanism as interface resolution to build the
242 | argument. Users can add new hints to the database by adding a `%hint`
243 | pragma to their declarations. By default all data constructors are hints.
244 | For instance, the following function
246 | f : (n : Nat) -> {auto _ : n === Z} -> Nat
249 | will only accept arguments that can be automatically proven to be equal
253 | * `default` takes a value of the appropriate type and if no argument is
254 | explicitly passed at a call site, will use that default value.
255 | For instance, the following function
257 | f : {default 0 n : Nat} -> Nat
260 | will return `0` if no argument is passed and its argument otherwise.
263 | unusedKeyword : Doc IdrisDocAnn
264 | unusedKeyword = "Currently unused keyword"
266 | interfacemechanism : Doc IdrisDocAnn
267 | interfacemechanism = vcat $
268 | header "Interfaces" :: ""
269 | :: map (indent 2) [
271 | Interfaces offer ad-hoc polymorphism. Programmers can declare new
272 | interfaces offering a set of methods (some of which may have default
273 | implementations in terms of the interface's other methods) and write
274 | programs generic over all types implementing the interface.
277 | In the following example we define a `Fail` interface that allows
278 | users to abort in case a computation is doomed to fail. We implement
279 | the `whenJust` construct using this interface and show a couple of
284 | interface Fail (0 a : Type) where
287 | whenJust : Fail ret => Maybe a -> (a -> ret) -> ret
288 | whenJust (Just v) k = k v
289 | whenJust Nothing _ = fail
291 | implementation Fail Bool where
294 | Fail (Maybe a) where
299 | As you can see the `implementation` keyword is optional. Note that the
300 | proof search machinery powering interface resolution works best if your
301 | implementations are for specific type constructors (here `Bool` and `Maybe`).
304 | doblock : Doc IdrisDocAnn
306 | header "Do block" :: ""
307 | :: map (indent 2) [
309 | Do blocks are a popular way to structure (among other things) effectful code.
310 | They are desugared using `(>>=)` and `(>>)` respectively depending on whether
311 | the result of a subcomputation is bound. Let bindings and local definitions
312 | can be used (omitting `in` because the layout is already controlled by the
313 | `do`-based indentation) and desugared to the corresponding `let` constructs.
315 | For instance the following block
322 | is equivalent to the expression `e1 >>= \ x => e2 >> let y = e3 in e4`.
325 | By default `(>>=)` and `(>>)` are then selected using the usual type
326 | directed disambiguation mechanisms. Users who want to bypass this implicit
327 | disambiguation step can use a qualified `do`: by writing `M.do` they ensure
328 | Idris will explicitly use `M.(>>=)` and `M.(>>)` during elaboration.
331 | whereblock : Doc IdrisDocAnn
332 | whereblock = vcat $
333 | header "Where block" :: ""
334 | :: map (indent 2) [
335 | header "NB:" <++> """
336 | `where` is used as a layout keyword in `data`, `record`, `interface`,
337 | and `implementation` blocks. This documentation snippet focuses instead
338 | on the `where` blocks introducing local definitions.
341 | A `where` block allows the introduction of local auxiliary definitions
342 | that are parametrised over the variables bound on the left hand side of
343 | the parent clause (cf. the doc for `parameters`).
347 | parametersblock : Doc IdrisDocAnn
348 | parametersblock = vcat $
349 | header "Parameters block" :: ""
350 | :: map (indent 2) [
352 | Definitions that share a common parameter can be grouped in a parameters
353 | block to avoid having to explicitly pass it around. Outside of the block
354 | all the definitions will take additional arguments corresponding to the
355 | parameters. For instance the functions in the following block all use a
356 | default value `dflt`
360 | parameters (dflt : a)
368 | last (_ :: xs) = last xs
373 | and their respective types outside of the parameters block are
374 | `head : a -> List a -> a` and `last : a -> List a -> a`.
377 | failblock : Doc IdrisDocAnn
379 | header "Fail block" :: ""
380 | :: map (indent 2) [
382 | Fail blocks let users check that some code parses but is rejected during elaboration.
383 | In the following example, we make sure that Idris rejects a proof that the character
384 | 'a' is equal to 'b' by throwing an error when unifying them.
388 | failing "When unifying"
389 | noteq : 'a' === 'b'
394 | If the (optional) string attached to a failing block does not appear in the error raised,
395 | or if no error is raised then the failing block is itself failing and thus leads to an error.
396 | This lets users document the kind of error the block is meant to document.
400 | mutualblock : Doc IdrisDocAnn
401 | mutualblock = vcat $
402 | header "Mutual block" :: ""
403 | :: map (indent 2) [
405 | Mutual blocks allow users to have inter-dependent declarations. For instance
406 | we can define the `odd` and `even` checks in terms of each other like so:
420 | Internally this is implemented in terms of the more fundamental
421 | forward-declaration feature: all the mutual declarations come first and then
422 | their definitions. In other words, the earlier example using a `mutual` block
423 | is equivalent to the following
436 | namespaceblock : Doc IdrisDocAnn
437 | namespaceblock = vcat $
438 | header "Namespace block" :: ""
439 | :: map (indent 2) [
441 | Attempting to declare two functions with the same name in a given module
442 | will lead to a scope error. Putting each one in a different `namespace`
443 | block can help bypass this issue by ensuring that they are assigned distinct
444 | fully qualified names. For instance
456 | declares a module `M` containing two values `M.Zero.val` and `M.One.val`.
457 | You can use `export` or `public export` to control whether a function
458 | declared in a namespace is available outside of it.
460 | autobindDoc : Doc IdrisDocAnn
464 | `autobind` is a modifier for operator precedence and fixity declaration.
465 | It tells the parser that this operator behaves like a binding operator,
466 | allowing you to give a name to the left-hand-side of the operator and
467 | use it on the right-hand-side.
469 | `autobind` differs from `typebind` in the syntax it allows and the way
470 | it desugars. Delcaring an operator as `autobind infixr 0 =|>` allows
471 | you to use it with the syntax `(x := e) =|> f x`, `(x : t := e) =|> f x`.
474 | You will need to use `autobind` instead of `typebind` whenever the
475 | type of the lambda of the function called by the operator has a type
476 | that is not equal to the argument given on the left side of the operator.
478 | `autobind` only applies to `infixr` operators and cannot be used as
481 | `autobind` operators are desugared as a lambda:
482 | `(x := expr) =|> fn x` -> `(expr =|> (\x : ? => fn x))`
483 | `(x : ty := expr) =|> fn x` -> `(expr =|> (\x : ty => fn x))`
485 | typebindDoc : Doc IdrisDocAnn
489 | `typebind` is a modifier for operator precedence and fixity declaration.
490 | It tells the parser that this operator behaves like a binding operator,
491 | allowing you to give a name to the left-hand-side of the operator and
492 | use it on the right-hand-side.
494 | A typical example of a typebind operator is `(**)` the type constructor
495 | for dependent pairs. It is used like this: `(x : Nat) ** Vect x String`
497 | If you declare a new operator to be typebind you can use it the same
500 | Start by defining `typebind infixr 0 =@`, and then you can use it
501 | like so: `(n : Nat) =@ f n`
503 | `typebind` only applies to `infixr` operators and cannot be used as
506 | `typebind` operators are desugared as a lambda:
507 | `(x : ty) =@ fn x` -> `ty =@ (\x : ty =@ fn x)`
510 | rewriteeq : Doc IdrisDocAnn
512 | header "Rewrite" :: ""
513 | :: map (indent 2) [
515 | Users can deploy an equality proof to adjust a type by replacing the value
516 | on the left hand side of the equality by that on the right hand side.
517 | For instance, if we know that the types `a` and `b` are propositionally
518 | equal, we can return a value of type `a` as if it had type `b`:
520 | transport : a === b -> a -> b
521 | transport eq x = rewrite sym eq in x
525 | withabstraction : Doc IdrisDocAnn
526 | withabstraction = vcat $
527 | header "With abstraction" :: ""
528 | :: map (indent 2) [
530 | We often need to match on the result of an intermediate computation.
531 | When this intermediate computation additionally appears in the type of the
532 | function being defined, the `with` construct allows us to capture these
533 | occurrences so that the observations made in the patterns will be reflected
535 | If we additionally need to remember that the link between the patterns and
536 | the intermediate computation we can use the `proof` keyword to retain an
539 | In the following example we want to implement a `filter` function that not
540 | only returns values that satisfy the input predicate but also proofs that
541 | they do. The `with (p x)` construct introduces a value of type `Bool`
542 | obtained by testing `x` with `p`. The additional `proof eq` part records in
543 | `eq` an equality proof stating that the `True`/`False` patterns in the further
544 | clauses are equal to the result of evaluating `p x`. This is the reason why
545 | we can successfully form `(x ** eq)` in the `True` branch.
547 | filter : (p : a -> Bool) -> List a -> List (x : a ** p x === True)
549 | filter p (x :: xs) with (p x) proof eq
550 | _ | True = (x ** eq) :: filter p xs
551 | _ | False = filter p xs
555 | letbinding : Doc IdrisDocAnn
556 | letbinding = vcat $
557 | header "Let binding" :: ""
558 | :: map (indent 2) [
560 | The `let` keyword is used for both local definitions and let bindings.
561 | Local definitions are just like top-level definitions except that they are
562 | defined in whatever extended context is available at the definition site.
564 | Let bindings can be used to bind the result of intermediate computations.
565 | They do not necessitate but can have a type annotation. They will not unfold
566 | in the type of subsequent terms so may not be appropriate in all cases.
568 | For instance, in the following definition the let-bound value `square`
569 | ensures that `n * n` is only computed once:
571 | power4 : Nat -> Nat
572 | power4 n = let square := n * n in square * square
575 | It is also possible to pattern-match on the result of the intermediate
576 | computation. The main pattern is written in place of the variable and
577 | an alternative list of clauses can be given using the `|` separator.
578 | For instance, we can shortcut the `square * square` computation in case
579 | the returned value is 0 like so:
581 | power4 : Nat -> Nat
582 | power4 n = let square@(S _) := n * n
588 | keywordsDoc : All DocFor Source.keywords
590 | "data" ::= datatypes
591 | :: "module" ::= "Keyword to start a module definition"
592 | :: "where" ::= whereblock
593 | :: "let" ::= letbinding
594 | :: "in" ::= "Used by `let` and `rewrite`. See either of them for more details."
595 | :: "do" ::= doblock
596 | :: "record" ::= recordtypes
597 | :: "auto" ::= implicitarg
598 | :: "default" ::= implicitarg
599 | :: "implicit" ::= unusedKeyword
600 | :: "failing" ::= failblock
601 | :: "mutual" ::= mutualblock
602 | :: "namespace" ::= namespaceblock
603 | :: "parameters" ::= parametersblock
604 | :: "with" ::= withabstraction
605 | :: "proof" ::= withabstraction
606 | :: "impossible" ::= impossibility
607 | :: "case" ::= caseof
609 | :: "if" ::= ifthenelse
610 | :: "then" ::= ifthenelse
611 | :: "else" ::= ifthenelse
612 | :: "forall" ::= forallquantifier
613 | :: "rewrite" ::= rewriteeq
614 | :: "typebind" ::= autobindDoc
615 | :: "autobind" ::= autobindDoc
617 | :: "interface" ::= interfacemechanism
618 | :: "implementation" ::= interfacemechanism
619 | :: "open" ::= unusedKeyword
620 | :: "import" ::= importing
621 | :: "public" ::= visibility
622 | :: "export" ::= visibility
623 | :: "private" ::= visibility
624 | :: "infixl" ::= fixity
625 | :: "infixr" ::= fixity
626 | :: "infix" ::= fixity
627 | :: "prefix" ::= fixity
628 | :: "total" ::= totality
629 | :: "partial" ::= totality
630 | :: "covering" ::= totality
634 | getDocsForKeyword : String -> Doc IdrisDocAnn
635 | getDocsForKeyword k
636 | = maybe (annotate (Syntax Keyword) $
pretty0 k) doc
637 | $
lookup k keywordsDoc
640 | unusedSymbol : Doc IdrisDocAnn
641 | unusedSymbol = "Currently unused symbol"
643 | lambdaAbstraction : Doc IdrisDocAnn
644 | lambdaAbstraction = """
645 | An anonymous function is introduced using a lambda `\\` and binds a
646 | comma-separated list of either variable names or irrefutable patterns
647 | before returning a right hand side using `=>`.
649 | For instance we can implement `transport` like so:
651 | transport : a === b -> a -> b
652 | transport = \\ Refl, v => v
656 | fatArrow : Doc IdrisDocAnn
659 | Used for an interface constraint in a type signature or as part of a
660 | lambda abstraction or case block.
662 | 1. Interface constraint
665 | `a => b` corresponds to `{auto _ : a} -> b`
668 | 2. Lambda abstraction
670 | , indent 2 lambdaAbstraction
676 | bang : Doc IdrisDocAnn
678 | Directive to lift the following effectful expression to the nearest enclosing
679 | (potentially implicit) `do` block. In the following definition for instance
682 | anyM : Monad m => (a -> m Bool) -> List a -> m (Maybe a)
683 | anyM p [] = pure Nothing
684 | anyM p (x :: xs) = if !(p x) then pure (Just x) else anyM p xs
687 | the expression `if !(p x) then pure (Just x) else anyM p xs` is equivalent to
688 | the following `do` block:
692 | if b then pure (Just x) else anyM p xs
696 | asPattern : Doc IdrisDocAnn
698 | An as pattern `@` can be used to both pattern match on a variable
699 | and retain a name for the compound expression. E.g. instead of writing
701 | last : List a -> Maybe a
704 | last (x :: y :: ys) = last (y :: ys)
707 | where, in the last clasue, we take `y :: ys` apart on the left hand side
708 | before reconstructing it on the right hand side, we can write:
711 | last (x :: xs@(_ :: _)) = last xs
715 | tupleSyntax : Doc IdrisDocAnn
716 | tupleSyntax = "Used to build dependent pairs together with parentheses"
718 | rangeSyntax : Doc IdrisDocAnn
720 | The ellipsis `..` can be used to generate lists or streams of values for
721 | types that implement the `Range` interface.
723 | Lists can be generated using an initial value, an (optional) second value
724 | and a final one. For instance, we can generate lists of integers like so:
725 | 1. `[1..5]` evaluates to `[1,2,3,4,5]`
726 | 2. `[1,3..5]` evaluates to `[1, 3, 5]`
728 | Streams can be generated using an initial value and an optional second value.
729 | For instance the following streams of integers:
730 | 1. `[1..]` for all positive integers
731 | 2. `[1,3..]` for all positive odds
734 | recordUpdate : Doc IdrisDocAnn
735 | recordUpdate = vcat $
header "Record updates" :: ""
736 | :: map (indent 2) [
738 | If a record `r` has a field `n` of type `Nat`, it is possible to either
740 | 1. overwrite the current value with `0` by using the assignment symbol `:=`
741 | like so: `{ n := 0 } r`
743 | 2. modify the current value by adding `2` by using the modification symbol `$=`
744 | like so: `{ n $= (2 +) } r`.
746 | Multiple updates can be combined in a single update by grouping a comma-separated
747 | list of assignments and/or modifications like so: `{ a := Z, b $= S } r`.
751 | symbolsDoc : All DocFor (Source.symbols ++ Source.reservedInfixSymbols)
756 | An implicit value either solved by unification or bound
757 | as a pattern or type variable.
760 | :: "%" ::= "Start of a pragma"
761 | :: "\\" ::= lambdaAbstraction
763 | Type declaration, for instance `id : a -> a`
764 | declares a new toplevel definition `id` of type `a -> a`.
766 | :: "=" ::= "Definition or equality type"
767 | :: ":=" ::= "Let binding or record assignment"
768 | :: "$=" ::= recordUpdate
769 | :: "|" ::= "Additional patterns showing up in a `with` clause"
770 | :: "|||" ::= "Document string attached to the following definition"
771 | :: "<-" ::= "Bind in a do block"
772 | :: "->" ::= "Function type"
773 | :: "=>" ::= fatArrow
774 | :: "?" ::= "An implicit value solved by unification."
776 | :: "&" ::= unusedSymbol
777 | :: "**" ::= tupleSyntax
778 | :: ".." ::= rangeSyntax
780 | :: "@" ::= asPattern
784 | getDocsForSymbol : String -> Doc IdrisDocAnn
786 | = maybe (annotate (Syntax Keyword) $
pretty0 k) doc
787 | $
lookup k symbolsDoc