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 | %runElab (deriveFromDhall Record `{ Category })
170 | %runElab (deriveFromDhall Record `{ Config })
171 |
172 | public export
173 | data Backend = LaTeX | HTML | Markdown | Literate
174 |
175 | export
176 | defaultConfig : Backend -> Config
177 | defaultConfig LaTeX = defaultLatexConfig
178 | defaultConfig HTML = defaultHTMLConfig
179 | defaultConfig Markdown = defaultHTMLConfig
180 | defaultConfig Literate = defaultLatexConfig
181 |
182 | export
183 | getConfiguration : Backend -> (configFile : Maybe String) -> IO Config
184 | getConfiguration backend Nothing = pure $ defaultConfig backend
185 | getConfiguration backend (Just filename) = do
186 |   Right fileContent <- readFile filename
187 |   | Left err => putStrLn "Error reading file: \{show err}"
188 |              >> exitFailure
189 |   Right config <- liftIOEither (deriveFromDhallString {ty = Config} fileContent)
190 |   | Left err => do putStrLn  """
191 |                      Error while parsing configuration file \{filename}:
192 |                      \{show err}
193 |                      Using default configuration instead.
194 |                      """
195 |                    pure $ defaultConfig backend
196 |
197 |   pure config
198 |
199 |
200 | public export
201 | record Driver where
202 |   constructor MkDriver
203 |   line        : ((width, lineNumber : Nat) -> String, String)
204 |   escape      : Char -> List Char
205 |   annotate    : Maybe Decoration -> String -> String
206 |   standalone  : (String, String)
207 |   inlineMacro : (String -> String, String)
208 |   blockMacro  : (String -> String, String)
209 |
210 | export
211 | initExec : (backend : Backend) -> (moutput : Maybe String) -> IO ()
212 | initExec backend moutput = do
213 |   Right file <- maybe (pure $ Right stdout) (flip openFile WriteTruncate) moutput
214 |   | Left err => do putStrLn """
215 |                             Error while opening configuration file \{fromMaybe "stdout" moutput}:
216 |                             \{show err}
217 |                             """
218 |                    exitFailure
219 |   Right () <- fPutStrLn file $ (defaultConfig backend).toString
220 |   | Left err => do putStrLn """
221 |                             Error while writing preamble file \{fromMaybe "stdout" moutput}:
222 |                             \{show err}
223 |                             """
224 |                    exitFailure
225 |   closeFile file
226 |