0 | module Prelude.Interpolation
 1 |
 2 | import Builtin
 3 |
 4 | ||| Interpolated strings are of the form `"xxxx \{ expr } yyyy"`.
 5 | ||| In this example the string `"xxxx "` is concatenated with `expr` and
 6 | ||| `" yyyy"`, since `expr` is not necessarily a string, the generated
 7 | ||| code looks like this:
 8 | ||| ```
 9 | ||| concat [interpolate "xxxx ", interpolate expr, interpolate " yyyy"]
10 | ||| ```
11 | ||| This allows to customise the interpolation behaviour by providing
12 | ||| an instance of `Interpolation` for a type.
13 | public export
14 | interface Interpolation a where
15 |   constructor MkInterpolation
16 |   interpolate : a -> String
17 |
18 | ||| The interpolation instance for Strings is the identity
19 | export
20 | Interpolation String where
21 |   interpolate x = x
22 |
23 | export
24 | Interpolation Void where
25 |   interpolate _ impossible
26 |