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 | public export
136 | record Session where
137 |   constructor MkSessionOpts
138 |   noprelude : Bool
139 |   totalReq : TotalReq
140 |   nobanner : Bool
141 |   findipkg : Bool
142 |   codegen : CG
143 |   directives : List String
144 |   searchTimeout : Integer -- maximum number of milliseconds to run
145 |                           -- expression/program search
146 |   ignoreMissingPkg : Bool -- fail silently on missing packages. This is because
147 |           -- while we're bootstrapping, we find modules by a different route
148 |           -- but we still want to have the dependencies listed properly
149 |
150 |   -- Troubleshooting
151 |   logEnabled : Bool -- do we check logging flags at all? This is 'False' until
152 |                     -- any logging is enabled.
153 |   logLevel : LogLevels
154 |   logTimings : Maybe Nat -- log level, higher means more details
155 |   debugElabCheck : Bool -- do conversion check to verify results of elaborator
156 |   dumpcases : Maybe String -- file to output compiled case trees
157 |   dumplifted : Maybe String -- file to output lambda lifted definitions
158 |   dumpanf : Maybe String -- file to output ANF definitions
159 |   dumpvmcode : Maybe String -- file to output VM code definitions
160 |   profile : Bool -- generate profiling information, if supported
161 |   logErrorCount : Nat -- when parsing alternatives fails, how many errors
162 |                       -- should be shown.
163 |   noCSE : Bool -- disable common subexpression elimination
164 |
165 |   -- Warnings
166 |   warningsAsErrors : Bool
167 |   showShadowingWarning : Bool
168 |
169 |   -- Experimental
170 |   checkHashesInsteadOfModTime : Bool
171 |   incrementalCGs : List CG
172 |   wholeProgram : Bool
173 |      -- Use whole program compilation for executables, no matter what
174 |      -- incremental CGs are set (intended for overriding any environment
175 |      -- variables that set incremental compilation)
176 |   caseTreeHeuristics : Bool -- apply heuristics to pick matches for case tree building
177 |
178 | public export
179 | record PPrinter where
180 |   constructor MkPPOpts
181 |   showImplicits : Bool
182 |   showMachineNames : Bool
183 |   showFullEnv : Bool
184 |   fullNamespace : Bool
185 |
186 | public export
187 | record Options where
188 |   constructor MkOptions
189 |   dirs : Dirs
190 |   printing : PPrinter
191 |   session : Session
192 |   elabDirectives : ElabDirectives
193 |   pairnames : Maybe PairNames
194 |   rewritenames : Maybe RewriteNames
195 |   primnames : PrimNames
196 |   extensions : List LangExt
197 |   additionalCGs : List (String, CG)
198 |   hashFn : Maybe String
199 |   -- fullName and definition for %foreign_impl
200 |   foreignImpl : List (Name, String)
201 |
202 | export
203 | availableCGs : Options -> List (String, CG)
204 | availableCGs o
205 |     = [("chez", Chez),
206 |        ("chez-sep", ChezSep),
207 |        ("racket", Racket),
208 |        ("node", Node),
209 |        ("javascript", Javascript),
210 |        ("refc", RefC),
211 |        ("gambit", Gambit),
212 |        ("vmcode-interp", VMCodeInterp)] ++ additionalCGs o
213 |
214 | export
215 | getCG : Options -> String -> Maybe CG
216 | getCG o cg = lookup (toLower cg) (availableCGs o)
217 |
218 | defaultDirs : Dirs
219 | defaultDirs = MkDirs "." Nothing "build" "depends" Nothing
220 |                      "/usr/local" ["."] [] [] [] []
221 |
222 | defaultPPrint : PPrinter
223 | defaultPPrint = MkPPOpts
224 |     { showImplicits = False
225 |     , showMachineNames = False
226 |     , showFullEnv = True
227 |     , fullNamespace = False
228 |     }
229 |
230 | export
231 | docsPPrint : PPrinter
232 | docsPPrint = MkPPOpts
233 |     { showImplicits = False
234 |     , showMachineNames = True
235 |     , showFullEnv = False
236 |     , fullNamespace = False
237 |     }
238 |
239 | export
240 | defaultSession : Session
241 | defaultSession = MkSessionOpts False CoveringOnly False False Chez [] 1000 False False
242 |                                defaultLogLevel Nothing False Nothing Nothing
243 |                                Nothing Nothing False 1 False False True
244 |                                False [] False False
245 |
246 | export
247 | defaultElab : ElabDirectives
248 | defaultElab = MkElabDirectives True True CoveringOnly 3 50 25 5 True
249 |
250 | -- FIXME: This turns out not to be reliably portable, since different systems
251 | -- may have tools with the same name but different required arugments. We
252 | -- probably need another way (perhaps our own internal hash function, although
253 | -- that's not going to be as good as sha256).
254 | export
255 | defaultHashFn : Core (Maybe String)
256 | defaultHashFn
257 |     = do Nothing <- coreLift $ pathLookup ["sha256sum", "gsha256sum"]
258 |            | Just p => pure $ Just $ p ++ " --tag"
259 |          Nothing <- coreLift $ pathLookup ["sha256"]
260 |            | Just p => pure $ Just p
261 |          Nothing <- coreLift $ pathLookup ["openssl"]
262 |            | Just p => pure $ Just $ p ++ " sha256"
263 |          pure Nothing
264 |
265 | export
266 | defaults : Core Options
267 | defaults
268 |     = do -- hashFn <- defaultHashFn
269 |          -- Temporarily disabling the hash function until we have a more
270 |          -- portable way of working out what to call, and allowing a way for
271 |          -- it to fail gracefully.
272 |          pure $ MkOptions
273 |            defaultDirs defaultPPrint defaultSession defaultElab Nothing Nothing
274 |            (MkPrimNs Nothing Nothing Nothing Nothing Nothing Nothing Nothing) [] [] Nothing []
275 |
276 | -- Reset the options which are set by source files
277 | export
278 | clearNames : Options -> Options
279 | clearNames = { pairnames := Nothing,
280 |                rewritenames := Nothing,
281 |                primnames := MkPrimNs Nothing Nothing Nothing Nothing Nothing Nothing Nothing,
282 |                foreignImpl := [],
283 |                extensions := []
284 |              }
285 |
286 | export
287 | addForeignImpl : (fullName : Name) -> (def : String) -> Options -> Options
288 | addForeignImpl fullName def = { foreignImpl $= ((fullName, def) ::) }
289 |
290 | export
291 | setPair : (pairType : Name) -> (fstn : Name) -> (sndn : Name) ->
292 |           Options -> Options
293 | setPair ty f s = { pairnames := Just (MkPairNs ty f s) }
294 |
295 | export
296 | setRewrite : (eq : Name) -> (rwlemma : Name) -> Options -> Options
297 | setRewrite eq rw = { rewritenames := Just (MkRewriteNs eq rw) }
298 |
299 | export
300 | setFromInteger : Name -> Options -> Options
301 | setFromInteger n = { primnames->fromIntegerName := Just n }
302 |
303 | export
304 | setFromString : Name -> Options -> Options
305 | setFromString n = { primnames->fromStringName := Just n }
306 |
307 | export
308 | setFromChar : Name -> Options -> Options
309 | setFromChar n = { primnames->fromCharName := Just n }
310 |
311 | export
312 | setFromDouble : Name -> Options -> Options
313 | setFromDouble n = { primnames->fromDoubleName := Just n }
314 |
315 | export
316 | setFromTTImp : Name -> Options -> Options
317 | setFromTTImp n = { primnames->fromTTImpName := Just n }
318 |
319 | export
320 | setFromName : Name -> Options -> Options
321 | setFromName n = { primnames->fromNameName := Just n }
322 |
323 | export
324 | setFromDecls : Name -> Options -> Options
325 | setFromDecls n = { primnames->fromDeclsName := Just n }
326 |
327 | export
328 | setExtension : LangExt -> Options -> Options
329 | setExtension e = { extensions $= (e ::) }
330 |
331 | export
332 | isExtension : LangExt -> Options -> Bool
333 | isExtension e opts = e `elem` extensions opts
334 |
335 | export
336 | addCG : (String, CG) -> Options -> Options
337 | addCG cg = { additionalCGs $= (cg::) }
338 |