module Core.Options import Core.Coreimport Core.Nameimport Core.TTimport Utils.Binary import System.Info public exportrecord Dirs where  constructor MkDirs  working_dir : String  source_dir : Maybe String -- source directory, relative to working directory  build_dir : String -- build directory, relative to working directory  exec_dir : String -- executable directory, relative to working directory  dir_prefix : String -- installation prefix, for finding data files (e.g. run time support)  extra_dirs : List String -- places to look for import files  lib_dirs : List String -- places to look for libraries (for code generation)  data_dirs : List String -- places to look for data file public exporttoString : Dirs -> StringtoString (MkDirs wdir sdir bdir edir dfix edirs ldirs ddirs) =  unlines [ "+ Working Directory   :: " ++ show wdir          , "+ Source Directory    :: " ++ show sdir          , "+ Build Directory     :: " ++ show bdir          , "+ Executable Directory     :: " ++ show edir          , "+ Installation Prefix :: " ++ show dfix          , "+ Extra Directories :: " ++ show edirs          , "+ CG Library Directories :: " ++ show ldirs          , "+ Data Directories :: " ++ show ddirs] public exportdata CG = Chez        | Racket        | Gambit exportEq CG where  Chez == Chez = True  Racket == Racket = True  Gambit == Gambit = True  _ == _ = False exportavailableCGs : List (String, CG)availableCGs    = [("chez", Chez),       ("racket", Racket),       ("gambit", Gambit)] exportgetCG : String -> Maybe CGgetCG cg = lookup (toLower cg) availableCGs -- Name options, to be saved in TTCpublic exportrecord PairNames where  constructor MkPairNs  pairType : Name  fstName : Name  sndName : Name public exportrecord RewriteNames where  constructor MkRewriteNs  equalType : Name  rewriteName : Name public exportrecord PrimNames where  constructor MkPrimNs  fromIntegerName : Maybe Name  fromStringName : Maybe Name  fromCharName : Maybe Name public exportdata LangExt = Borrowing -- not yet implemented exportEq LangExt where  Borrowing == Borrowing = True -- Other options relevant to the current session (so not to be saved in a TTC)public exportrecord ElabDirectives where  constructor MkElabDirectives  lazyActive : Bool  unboundImplicits : Bool  totality : TotalReq  ambigLimit : Nat  undottedRecordProjections : Bool public exportrecord Session where  constructor MkSessionOpts  noprelude : Bool  nobanner : Bool  findipkg : Bool  codegen : CG  logLevel : Nat  logTimings : Bool  debugElabCheck : Bool -- do conversion check to verify results of elaborator  dumpcases : Maybe String -- file to output compiled case trees  dumplifted : Maybe String -- file to output lambda lifted definitions  dumpanf : Maybe String -- file to output ANF definitions  dumpvmcode : Maybe String -- file to output VM code definitions public exportrecord PPrinter where  constructor MkPPOpts  showImplicits : Bool  showFullEnv : Bool  fullNamespace : Bool public exportrecord Options where  constructor MkOptions  dirs : Dirs  printing : PPrinter  session : Session  elabDirectives : ElabDirectives  pairnames : Maybe PairNames  rewritenames : Maybe RewriteNames  primnames : PrimNames  extensions : List LangExt isWindows : BoolisWindows = os `elem` ["windows", "mingw32", "cygwin32"] exportsep : Charsep = '/' exportdirSep : StringdirSep = cast sep exportpathSep : CharpathSep = if isWindows then ';' else ':' defaultDirs : DirsdefaultDirs = MkDirs "." Nothing "build"                      ("build" ++ dirSep ++ "exec")                      "/usr/local" ["."] [] [] defaultPPrint : PPrinterdefaultPPrint = MkPPOpts False True False defaultSession : SessiondefaultSession = MkSessionOpts False False False Chez 0 False False                               Nothing Nothing Nothing Nothing defaultElab : ElabDirectivesdefaultElab = MkElabDirectives True True PartialOK 3 True exportdefaults : Optionsdefaults = MkOptions defaultDirs defaultPPrint defaultSession                     defaultElab Nothing Nothing                     (MkPrimNs Nothing Nothing Nothing)                     [] -- Reset the options which are set by source filesexportclearNames : Options -> OptionsclearNames = record { pairnames = Nothing,                      rewritenames = Nothing,                      primnames = MkPrimNs Nothing Nothing Nothing,                      extensions = []                    } exportsetPair : (pairType : Name) -> (fstn : Name) -> (sndn : Name) ->          Options -> OptionssetPair ty f s = record { pairnames = Just (MkPairNs ty f s) } exportsetRewrite : (eq : Name) -> (rwlemma : Name) -> Options -> OptionssetRewrite eq rw = record { rewritenames = Just (MkRewriteNs eq rw) } exportsetFromInteger : Name -> Options -> OptionssetFromInteger n = record { primnames->fromIntegerName = Just n } exportsetFromString : Name -> Options -> OptionssetFromString n = record { primnames->fromStringName = Just n } exportsetFromChar : Name -> Options -> OptionssetFromChar n = record { primnames->fromCharName = Just n } exportsetExtension : LangExt -> Options -> OptionssetExtension e = record { extensions $= (e ::) } exportisExtension : LangExt -> Options -> BoolisExtension e opts = e `elem` extensions opts