0 | module Core.Options
  1 |
  2 | import Core.Core
  3 | import public Core.Options.Log
  4 | import Core.TT
  5 |
  6 | import Libraries.Utils.Path
  7 | import Idris.Syntax.Pragmas
  8 |
  9 | import Data.List
 10 | import Data.Maybe
 11 | import Data.String
 12 |
 13 | %default total
 14 |
 15 | public export
 16 | record Dirs where
 17 |   constructor MkDirs
 18 |   working_dir : String
 19 |   source_dir : Maybe String -- source directory, relative to working directory
 20 |   build_dir : String -- build directory, relative to working directory
 21 |   depends_dir : String -- local dependencies directory, relative to working directory
 22 |   output_dir : Maybe String -- output directory, relative to working directory
 23 |   prefix_dir : String -- installation prefix, for finding data files (e.g. run time support)
 24 |   extra_dirs : List String -- places to look for import files
 25 |   package_search_paths : List Path -- paths at which to look for packages
 26 |   package_dirs : List String -- places where specific needed packages at required versions are located
 27 |   lib_dirs : List String -- places to look for libraries (for code generation)
 28 |   data_dirs : List String -- places to look for data file
 29 |
 30 | export
 31 | execBuildDir : Dirs -> String
 32 | execBuildDir d = build_dir d </> "exec"
 33 |
 34 | export
 35 | outputDirWithDefault : Dirs -> String
 36 | outputDirWithDefault d = fromMaybe (build_dir d </> "exec") (output_dir d)
 37 |
 38 | public export
 39 | toString : Dirs -> String
 40 | toString d@(MkDirs wdir sdir bdir ldir odir dfix edirs ppaths pdirs ldirs ddirs) = """
 41 |   + Working Directory      :: \{ show wdir }
 42 |   + Source Directory       :: \{ show sdir }
 43 |   + Build Directory        :: \{ show bdir }
 44 |   + Local Depend Directory :: \{ show ldir }
 45 |   + Output Directory       :: \{ show $ outputDirWithDefault d }
 46 |   + Installation Prefix    :: \{ show dfix }
 47 |   + Extra Directories      :: \{ show edirs }
 48 |   + Package Search Paths   :: \{ show ppaths }
 49 |   + Package Directories    :: \{ show pdirs }
 50 |   + CG Library Directories :: \{ show ldirs }
 51 |   + Data Directories       :: \{ show ddirs }
 52 |   """
 53 |
 54 | public export
 55 | data CG = Chez
 56 |         | ChezSep
 57 |         | Racket
 58 |         | Gambit
 59 |         | Node
 60 |         | Javascript
 61 |         | RefC
 62 |         | VMCodeInterp
 63 |         | Other String
 64 |
 65 | export
 66 | Eq CG where
 67 |   Chez == Chez = True
 68 |   ChezSep == ChezSep = True
 69 |   Racket == Racket = True
 70 |   Gambit == Gambit = True
 71 |   Node == Node = True
 72 |   Javascript == Javascript = True
 73 |   RefC == RefC = True
 74 |   VMCodeInterp == VMCodeInterp = True
 75 |   Other s == Other t = s == t
 76 |   _ == _ = False
 77 |
 78 | export
 79 | Show CG where
 80 |   show Chez = "chez"
 81 |   show ChezSep = "chez-sep"
 82 |   show Racket = "racket"
 83 |   show Gambit = "gambit"
 84 |   show Node = "node"
 85 |   show Javascript = "javascript"
 86 |   show RefC = "refc"
 87 |   show VMCodeInterp = "vmcode-interp"
 88 |   show (Other s) = s
 89 |
 90 | public export
 91 | record PairNames where
 92 |   constructor MkPairNs
 93 |   pairType : Name
 94 |   fstName : Name
 95 |   sndName : Name
 96 |
 97 | public export
 98 | record RewriteNames where
 99 |   constructor MkRewriteNs
100 |   equalType : Name
101 |   rewriteName : Name
102 |
103 | public export
104 | record PrimNames where
105 |   constructor MkPrimNs
106 |   fromIntegerName : Maybe Name
107 |   fromStringName : Maybe Name
108 |   fromCharName : Maybe Name
109 |   fromDoubleName : Maybe Name
110 |   fromTTImpName : Maybe Name
111 |   fromNameName : Maybe Name
112 |   fromDeclsName : Maybe Name
113 |
114 | export
115 | primNamesToList : PrimNames -> List Name
116 | primNamesToList (MkPrimNs i s c d t n dl) = catMaybes [i,s,c,d,t,n,dl]
117 |
118 | -- Other options relevant to the current session (so not to be saved in a TTC)
119 | public export
120 | record ElabDirectives where
121 |   constructor MkElabDirectives
122 |   lazyActive : Bool
123 |   unboundImplicits : Bool
124 |   totality : TotalReq
125 |   ambigLimit : Nat
126 |   autoImplicitLimit : Nat
127 |   nfThreshold : Nat
128 |   totalLimit : Nat
129 |   --
130 |   -- produce traditional (prefix) record projections,
131 |   -- in addition to postfix (dot) projections
132 |   -- default: yes
133 |   prefixRecordProjections : Bool
134 |
135 | ||| Options relevant after running a typechecking session
136 | public export
137 | record PostSession where
138 |   constructor MkPostSession
139 |   checkOnly : Bool
140 |   outputFile : Maybe String
141 |   execExpr : List String
142 |   runRepl : Maybe String
143 |
144 | export
145 | defaultPost : PostSession
146 | defaultPost = MkPostSession
147 |   { checkOnly = False
148 |   , outputFile = Nothing
149 |   , execExpr = []
150 |   , runRepl = Nothing
151 |   }
152 |
153 | -- tag for PostSession
154 | export
155 | data PostS : Type where
156 |
157 | public export
158 | record Session where
159 |   constructor MkSessionOpts
160 |   noprelude : Bool
161 |   totalReq : TotalReq
162 |   nobanner : Bool
163 |   findipkg : Bool
164 |   codegen : CG
165 |   directives : List String
166 |   searchTimeout : Integer -- maximum number of milliseconds to run
167 |                           -- expression/program search
168 |   ignoreMissingPkg : Bool -- fail silently on missing packages. This is because
169 |           -- while we're bootstrapping, we find modules by a different route
170 |           -- but we still want to have the dependencies listed properly
171 |
172 |   -- Troubleshooting
173 |   logEnabled : Bool -- do we check logging flags at all? This is 'False' until
174 |                     -- any logging is enabled.
175 |   logLevel : LogLevels
176 |   logTimings : Maybe Nat -- log level, higher means more details
177 |   debugElabCheck : Bool -- do conversion check to verify results of elaborator
178 |   dumpcases : Maybe String -- file to output compiled case trees
179 |   dumplifted : Maybe String -- file to output lambda lifted definitions
180 |   dumpanf : Maybe String -- file to output ANF definitions
181 |   dumpvmcode : Maybe String -- file to output VM code definitions
182 |   profile : Bool -- generate profiling information, if supported
183 |   logErrorCount : Nat -- when parsing alternatives fails, how many errors
184 |                       -- should be shown.
185 |   noCSE : Bool -- disable common subexpression elimination
186 |
187 |   -- Warnings
188 |   warningsAsErrors : Bool
189 |   showShadowingWarning : Bool
190 |
191 |   -- Experimental
192 |   checkHashesInsteadOfModTime : Bool
193 |   incrementalCGs : List CG
194 |   wholeProgram : Bool
195 |      -- Use whole program compilation for executables, no matter what
196 |      -- incremental CGs are set (intended for overriding any environment
197 |      -- variables that set incremental compilation)
198 |   caseTreeHeuristics : Bool -- apply heuristics to pick matches for case tree building
199 |
200 | public export
201 | record PPrinter where
202 |   constructor MkPPOpts
203 |   showImplicits : Bool
204 |   showMachineNames : Bool
205 |   showFullEnv : Bool
206 |   fullNamespace : Bool
207 |
208 | public export
209 | record Options where
210 |   constructor MkOptions
211 |   dirs : Dirs
212 |   printing : PPrinter
213 |   session : Session
214 |   elabDirectives : ElabDirectives
215 |   pairnames : Maybe PairNames
216 |   rewritenames : Maybe RewriteNames
217 |   primnames : PrimNames
218 |   extensions : List LangExt
219 |   additionalCGs : List (String, CG)
220 |   hashFn : Maybe String
221 |   -- fullName and definition for %foreign_impl
222 |   foreignImpl : List (Name, String)
223 |
224 | export
225 | availableCGs : Options -> List (String, CG)
226 | availableCGs o
227 |     = [("chez", Chez),
228 |        ("chez-sep", ChezSep),
229 |        ("racket", Racket),
230 |        ("node", Node),
231 |        ("javascript", Javascript),
232 |        ("refc", RefC),
233 |        ("gambit", Gambit),
234 |        ("vmcode-interp", VMCodeInterp)] ++ additionalCGs o
235 |
236 | export
237 | getCG : Options -> String -> Maybe CG
238 | getCG o cg = lookup (toLower cg) (availableCGs o)
239 |
240 | defaultDirs : Dirs
241 | defaultDirs = MkDirs "." Nothing "build" "depends" Nothing
242 |                      "/usr/local" ["."] [] [] [] []
243 |
244 | defaultPPrint : PPrinter
245 | defaultPPrint = MkPPOpts
246 |     { showImplicits = False
247 |     , showMachineNames = False
248 |     , showFullEnv = True
249 |     , fullNamespace = False
250 |     }
251 |
252 | export
253 | docsPPrint : PPrinter
254 | docsPPrint = MkPPOpts
255 |     { showImplicits = False
256 |     , showMachineNames = True
257 |     , showFullEnv = False
258 |     , fullNamespace = False
259 |     }
260 |
261 | export
262 | defaultSession : Session
263 | defaultSession = MkSessionOpts False CoveringOnly False False Chez [] 1000 False False
264 |                                defaultLogLevel Nothing False Nothing Nothing
265 |                                Nothing Nothing False 1 False False True
266 |                                False [] False False
267 |
268 | export
269 | defaultElab : ElabDirectives
270 | defaultElab = MkElabDirectives True True CoveringOnly 3 50 25 5 True
271 |
272 | -- FIXME: This turns out not to be reliably portable, since different systems
273 | -- may have tools with the same name but different required arugments. We
274 | -- probably need another way (perhaps our own internal hash function, although
275 | -- that's not going to be as good as sha256).
276 | export
277 | defaultHashFn : Core (Maybe String)
278 | defaultHashFn
279 |     = do Nothing <- coreLift $ pathLookup ["sha256sum", "gsha256sum"]
280 |            | Just p => pure $ Just $ p ++ " --tag"
281 |          Nothing <- coreLift $ pathLookup ["sha256"]
282 |            | Just p => pure $ Just p
283 |          Nothing <- coreLift $ pathLookup ["openssl"]
284 |            | Just p => pure $ Just $ p ++ " sha256"
285 |          pure Nothing
286 |
287 | export
288 | defaults : Core Options
289 | defaults
290 |     = do -- hashFn <- defaultHashFn
291 |          -- Temporarily disabling the hash function until we have a more
292 |          -- portable way of working out what to call, and allowing a way for
293 |          -- it to fail gracefully.
294 |          pure $ MkOptions
295 |            defaultDirs defaultPPrint defaultSession defaultElab Nothing Nothing
296 |            (MkPrimNs Nothing Nothing Nothing Nothing Nothing Nothing Nothing) [] [] Nothing []
297 |
298 | -- Reset the options which are set by source files
299 | export
300 | clearNames : Options -> Options
301 | clearNames = { pairnames := Nothing,
302 |                rewritenames := Nothing,
303 |                primnames := MkPrimNs Nothing Nothing Nothing Nothing Nothing Nothing Nothing,
304 |                foreignImpl := [],
305 |                extensions := []
306 |              }
307 |
308 | export
309 | addForeignImpl : (fullName : Name) -> (def : String) -> Options -> Options
310 | addForeignImpl fullName def = { foreignImpl $= ((fullName, def) ::) }
311 |
312 | export
313 | setPair : (pairType : Name) -> (fstn : Name) -> (sndn : Name) ->
314 |           Options -> Options
315 | setPair ty f s = { pairnames := Just (MkPairNs ty f s) }
316 |
317 | export
318 | setRewrite : (eq : Name) -> (rwlemma : Name) -> Options -> Options
319 | setRewrite eq rw = { rewritenames := Just (MkRewriteNs eq rw) }
320 |
321 | export
322 | setFromInteger : Name -> Options -> Options
323 | setFromInteger n = { primnames->fromIntegerName := Just n }
324 |
325 | export
326 | setFromString : Name -> Options -> Options
327 | setFromString n = { primnames->fromStringName := Just n }
328 |
329 | export
330 | setFromChar : Name -> Options -> Options
331 | setFromChar n = { primnames->fromCharName := Just n }
332 |
333 | export
334 | setFromDouble : Name -> Options -> Options
335 | setFromDouble n = { primnames->fromDoubleName := Just n }
336 |
337 | export
338 | setFromTTImp : Name -> Options -> Options
339 | setFromTTImp n = { primnames->fromTTImpName := Just n }
340 |
341 | export
342 | setFromName : Name -> Options -> Options
343 | setFromName n = { primnames->fromNameName := Just n }
344 |
345 | export
346 | setFromDecls : Name -> Options -> Options
347 | setFromDecls n = { primnames->fromDeclsName := Just n }
348 |
349 | export
350 | setExtension : LangExt -> Options -> Options
351 | setExtension e = { extensions $= (e ::) }
352 |
353 | export
354 | isExtension : LangExt -> Options -> Bool
355 | isExtension e opts = e `elem` extensions opts
356 |
357 | export
358 | addCG : (String, CG) -> Options -> Options
359 | addCG cg = { additionalCGs $= (cg::) }
360 |