0 | module Katla.Config
  1 |
  2 | import Idrall.API.V2
  3 | import Language.Reflection
  4 | import Collie
  5 | import System.File
  6 | import System.Path
  7 | import Data.Maybe
  8 | import Core.Metadata
  9 |
 10 | %language ElabReflection
 11 |
 12 | export
 13 | convert : Decoration -> String
 14 | convert Typ        = "IdrisType"
 15 | convert Function   = "IdrisFunction"
 16 | convert Data       = "IdrisData"
 17 | convert Keyword    = "IdrisKeyword"
 18 | convert Bound      = "IdrisBound"
 19 | convert Namespace  = "IdrisNamespace"
 20 | convert Postulate  = "IdrisPostulate"
 21 | convert Module     = "IdrisModule"
 22 | convert Comment    = "IdrisComment"
 23 |
 24 | public export
 25 | record Category where
 26 |   constructor MkCategory
 27 |   style : String
 28 |   colour : String
 29 |
 30 | public export
 31 | record Config where
 32 |   constructor MkConfig
 33 |   font, space : String
 34 |   datacons : Category
 35 |   typecons : Category
 36 |   bound    : Category
 37 |   function : Category
 38 |   keyword  : Category
 39 |   comment  : Category
 40 |   hole     : Category
 41 |   namespce : Category
 42 |   postulte : Category
 43 |   aModule  : Category
 44 |
 45 | namespace Cat
 46 |   export
 47 |   (.toString) : Category -> (prefixString : String) ->
 48 |                 {default (length prefixString) prefixLength : Nat} -> String
 49 |   cat.toString prefixString =
 50 |     let initPadding = (prefixLength `minus` (length prefixString `minus` 2))
 51 |         restPadding = prefixLength + 2
 52 |     in """
 53 |     \{prefixString}\{replicate initPadding ' '  } = { style  = \{show cat.style }
 54 |     \{indent restPadding "   "}, colour = \{show cat.colour}}
 55 |     """
 56 |
 57 | export
 58 | (.toString) : Config -> String
 59 | conf.toString = """
 60 | { font  = \{show conf.font}
 61 | , space = \{show conf.space}
 62 | \{conf.datacons.toString ", datacons" {prefixLength = length "datacons"}}
 63 | \{conf.typecons.toString ", typecons" {prefixLength = length "datacons"}}
 64 | \{conf.bound   .toString ", bound"    {prefixLength = length "datacons"}}
 65 | \{conf.function.toString ", function" {prefixLength = length "datacons"}}
 66 | \{conf.keyword .toString ", keyword"  {prefixLength = length "datacons"}}
 67 | \{conf.comment .toString ", comment"  {prefixLength = length "datacons"}}
 68 | \{conf.hole    .toString ", hole"     {prefixLength = length "datacons"}}
 69 | \{conf.namespce.toString ", namespce" {prefixLength = length "datacons"}}
 70 | \{conf.postulte.toString ", postulte" {prefixLength = length "datacons"}}
 71 | \{conf.aModule .toString ", aModule"  {prefixLength = length "datacons"}}
 72 | }
 73 | """
 74 |
 75 |
 76 | export
 77 | defaultHTMLConfig : Config
 78 | defaultHTMLConfig = MkConfig
 79 |   { font = #"\ttfamily"#
 80 |   , space = " "
 81 |   , datacons = MkCategory
 82 |     { style  = ""
 83 |     , colour = "darkred"
 84 |     }
 85 |   , typecons = MkCategory
 86 |     { style  = ""
 87 |     , colour = "blue"
 88 |     }
 89 |   , bound = MkCategory
 90 |     { style  = ""
 91 |     , colour = "black"
 92 |     }
 93 |   , function = MkCategory
 94 |     { style  = ""
 95 |     , colour = "darkgreen"
 96 |     }
 97 |   , keyword = MkCategory
 98 |     { style  = "text-decoration: underline;"
 99 |     , colour = ""
100 |     }
101 |   , comment = MkCategory
102 |     { style  = ""
103 |     , colour = "#b22222"
104 |     }
105 |   , hole = MkCategory
106 |     { style  = "font-weight: bold;"
107 |     , colour = "yellow"
108 |     }
109 |   , namespce = MkCategory
110 |     { style = "font-style: italic;"
111 |     , colour = "black"
112 |     }
113 |   , postulte = MkCategory
114 |     { style = "font-weight: bold;"
115 |     , colour = "red"
116 |     }
117 |   , aModule  = MkCategory
118 |     { style = "font-style: italic;"
119 |     , colour = "black"
120 |     }
121 |   }
122 |
123 | export
124 | defaultLatexConfig : Config
125 | defaultLatexConfig = MkConfig
126 |   { font = #"\ttfamily"#
127 |   , space = #" "#
128 |   , datacons = MkCategory
129 |     { style  = ""
130 |     , colour = "IndianRed1"
131 |     }
132 |   , typecons = MkCategory
133 |     { style  = ""
134 |     , colour = "DeepSkyBlue3"
135 |     }
136 |   , bound = MkCategory
137 |     { style  = ""
138 |     , colour = "DarkOrchid3"
139 |     }
140 |   , function = MkCategory
141 |     { style  = ""
142 |     , colour = "Chartreuse4"
143 |     }
144 |   , keyword = MkCategory
145 |     { style  = #"\bfseries"#
146 |     , colour = "black"
147 |     }
148 |   , comment = MkCategory
149 |     { style  = #"\itshape"#
150 |     , colour = "Ivory3"
151 |     }
152 |   , hole = MkCategory
153 |     { style  = #"\bfseries"#
154 |     , colour = "yellow"
155 |     }
156 |   , namespce = MkCategory
157 |     { style = #"\itshape"#
158 |     , colour = "black"
159 |     }
160 |   , postulte = MkCategory
161 |     { style = #"\bfseries"#
162 |     , colour = "DarkOrchid3"
163 |     }
164 |   , aModule  = MkCategory
165 |     { style = #"\itshape"#
166 |     , colour = "black"
167 |     }
168 |   }
169 |
170 | export
171 | defaultTypstConfig : Config
172 | defaultTypstConfig = MkConfig
173 |   { font = #"Liberation Mono"#
174 |   , space = #" "#
175 |   , datacons = MkCategory
176 |     { style  = #", "normal", "medium""#
177 |     , colour = "rgb(\"#ff6a6a\")"
178 |     }
179 |   , typecons = MkCategory
180 |     { style  = #", "normal", "medium""#
181 |     , colour = "rgb(\"#009acd\")"
182 |     }
183 |   , bound = MkCategory
184 |     { style  = #", "normal", "medium""#
185 |     , colour = "rgb(\"#9a32cd\")"
186 |     }
187 |   , function = MkCategory
188 |     { style  = #", "normal", "medium""#
189 |     , colour = "rgb(\"#458b00\")"
190 |     }
191 |   , keyword = MkCategory
192 |     { style  = #", "normal", "bold""#
193 |     , colour = "color.black"
194 |     }
195 |   , comment = MkCategory
196 |     { style  = #", "italic", "medium""#
197 |     , colour = "rgb(\"#cdcdc1\")"
198 |     }
199 |   , hole = MkCategory
200 |     { style  = #", "normal", "bold""#
201 |     , colour = "color.yellow"
202 |     }
203 |   , namespce = MkCategory
204 |     { style = #", "italic", "medium""#
205 |     , colour = "color.black"
206 |     }
207 |   , postulte = MkCategory
208 |     { style = #", "normal", "bold""#
209 |     , colour = "rgb(\"#9a32cd\")"
210 |     }
211 |   , aModule  = MkCategory
212 |     { style = #", "italic", "medium""#
213 |     , colour = "color.black"
214 |     }
215 |   }
216 | %runElab (deriveFromDhall Record `{ Category })
217 | %runElab (deriveFromDhall Record `{ Config })
218 |
219 | public export
220 | data Backend = LaTeX | Typst | HTML | Markdown | Literate
221 |
222 | export
223 | defaultConfig : Backend -> Config
224 | defaultConfig LaTeX = defaultLatexConfig
225 | defaultConfig Typst = defaultTypstConfig
226 | defaultConfig HTML = defaultHTMLConfig
227 | defaultConfig Markdown = defaultHTMLConfig
228 | defaultConfig Literate = defaultLatexConfig
229 |
230 | export
231 | getConfiguration : Backend -> (configFile : Maybe String) -> IO Config
232 | getConfiguration backend Nothing = pure $ defaultConfig backend
233 | getConfiguration backend (Just filename) = do
234 |   Right fileContent <- readFile filename
235 |   | Left err => putStrLn "Error reading file: \{show err}"
236 |              >> exitFailure
237 |   Right config <- liftIOEither (deriveFromDhallString {ty = Config} fileContent)
238 |   | Left err => do putStrLn  """
239 |                      Error while parsing configuration file \{filename}:
240 |                      \{show err}
241 |                      Using default configuration instead.
242 |                      """
243 |                    pure $ defaultConfig backend
244 |
245 |   pure config
246 |
247 |
248 | public export
249 | record Driver where
250 |   constructor MkDriver
251 |   line        : ((width, lineNumber : Nat) -> String, String)
252 |   escape      : Char -> List Char
253 |   annotate    : Maybe Decoration -> String -> String
254 |   standalone  : (String, String)
255 |   inlineMacro : (String -> String, String)
256 |   blockMacro  : (String -> String, String)
257 |
258 | export
259 | initExec : (backend : Backend) -> (moutput : Maybe String) -> IO ()
260 | initExec backend moutput = do
261 |   Right file <- maybe (pure $ Right stdout) (flip openFile WriteTruncate) moutput
262 |   | Left err => do putStrLn """
263 |                             Error while opening configuration file \{fromMaybe "stdout" moutput}:
264 |                             \{show err}
265 |                             """
266 |                    exitFailure
267 |   Right () <- fPutStrLn file $ (defaultConfig backend).toString
268 |   | Left err => do putStrLn """
269 |                             Error while writing preamble file \{fromMaybe "stdout" moutput}:
270 |                             \{show err}
271 |                             """
272 |                    exitFailure
273 |   closeFile file
274 |