0 | module Idris.Doc.Brackets
 1 |
 2 | import Data.String
 3 |
 4 | import Idris.Doc.Annotations
 5 | import Idris.Syntax
 6 | import Idris.Pretty
 7 |
 8 | export
 9 | getDocsForBracket : BracketType -> Doc IdrisDocAnn
10 | getDocsForBracket IdiomBrackets = vcat $
11 |     header "Idiom brackets" :: ""
12 |     :: map (indent 2) [
13 |     """
14 |     Idiom brackets allow for easier application of `Applicative`s
15 |
16 |     Adding two `Maybe Int`s can be written using `<*>` and `pure`
17 |
18 |     ```idris
19 |     addMaybe : Maybe Int -> Maybe Int -> Maybe Int
20 |     addMaybe x y = pure (+) <*> x <*> y
21 |     ```
22 |
23 |     This can be expressed more concisely as:
24 |
25 |     ```idris
26 |     addMaybe : Maybe Int -> Maybe Int -> Maybe Int
27 |     addMaybe x y= [| x + y |]
28 |     ```
29 |     """]
30 | getDocsForBracket NameQuote = vcat $
31 |     header "Name quotes" :: ""
32 |     :: map (indent 2) [
33 |     """
34 |     Name quotes convert a raw name into a representation of a name.
35 |     This allows elaborator scripts to refer to names the user provides.
36 |
37 |     ```idris
38 |     import Language.Reflection
39 |     %language ElabReflection
40 |
41 |     nameOfMaybe : Name
42 |     nameOfMaybe = `{Maybe}
43 |     ```
44 |
45 |     Names can be qualified, however no disambiguation of names occurs when
46 |     quoting them, so if you need a disambiguated name consider using
47 |     `Language.Reflection.getType`.
48 |     """]
49 | getDocsForBracket TermQuote = vcat $
50 |     header "Term quotes" :: ""
51 |     :: map (indent 2) [
52 |     """
53 |     These allow an expression to be interpreted as a syntax tree rather than
54 |     an actual expression, so it can be processed by an elaborator script
55 |     for compile time codegen or meta-programming.
56 |
57 |     ```idris
58 |     import Language.Reflection
59 |     %language ElabReflection
60 |
61 |     helloWorld : TTImp
62 |     helloWorld = `(putStrLn "hello world")
63 |     ```
64 |     """]
65 | getDocsForBracket DeclQuote = vcat $
66 |     header "Declaration quotes" :: ""
67 |     :: map (indent 2) [
68 |     """
69 |     Declarations quotes allow multiple declaration
70 |     (e.g. type declarations or function definitions) to be quoted
71 |
72 |     These can then be passed to a elaborator script for compile time
73 |     codegen or meta-programming.
74 |
75 |     ```idris
76 |     import Language.Reflection
77 |     %language ElabReflection
78 |
79 |     myProgram : List Decl
80 |     myProgram = `[
81 |         data Bool = False | True
82 |
83 |         main : IO ()
84 |         main = putStrLn "hello world"
85 |     ]
86 |     ```
87 |
88 |     In this example, `main : IO ()` and
89 |     `main = putStrLn "hello world"` are different `Decl`s
90 |     """]
91 |