0 | module Idris.REPL.Opts
  1 |
  2 | import Compiler.Common
  3 | import Idris.Syntax
  4 | import Parser.Unlit
  5 | import TTImp.TTImp
  6 |
  7 | import Libraries.Data.List.Extra
  8 | import Libraries.Data.Tap
  9 | import Data.String
 10 | import System.File
 11 |
 12 | %default total
 13 |
 14 | namespace VerbosityLvl
 15 |   public export
 16 |   data VerbosityLvl =
 17 |    ||| Suppress all message output to `stdout`.
 18 |    NoneLvl |
 19 |    ||| Keep only errors.
 20 |    ErrorLvl |
 21 |    ||| Keep everything.
 22 |    InfoLvl
 23 |
 24 | public export
 25 | data OutputMode
 26 |   = IDEMode Integer File File |
 27 |     ||| Given that we can divide elaboration messages into
 28 |     ||| two categories: informational message and error message,
 29 |     ||| `VerbosityLvl` applies a filter on the output,
 30 |     |||  suppressing writes to `stdout` if the level condition isn't met.
 31 |     REPL VerbosityLvl
 32 |
 33 | public export
 34 | record REPLOpts where
 35 |   constructor MkREPLOpts
 36 |   showTypes : Bool
 37 |   evalMode : REPLEval
 38 |   evalTiming : Bool
 39 |   mainfile : Maybe String
 40 |   literateStyle : Maybe LiterateStyle
 41 |   source : String
 42 |   editor : String
 43 |   errorLine : Maybe Int
 44 |   idemode : OutputMode
 45 |   currentElabSource : String
 46 |   psResult : Maybe (Name, Core (Search RawImp)) -- last proof search continuation (and name)
 47 |   gdResult : Maybe (Int, Core (Search (FC, List ImpClause))) -- last generate def continuation (and line number)
 48 |   evalResultName : Maybe Name
 49 |   -- TODO: Move extraCodegens from here, it doesn't belong, but there's nowhere
 50 |   -- better to stick it now.
 51 |   extraCodegens : List (String, Codegen)
 52 |   consoleWidth : Maybe Nat -- Nothing is auto
 53 |   color : Bool
 54 |   synHighlightOn : Bool
 55 |
 56 | litStyle : Maybe String -> Maybe LiterateStyle
 57 | litStyle = join . map isLitFile
 58 |
 59 | covering
 60 | export
 61 | defaultOpts : Maybe String -> OutputMode -> List (String, Codegen) -> REPLOpts
 62 | defaultOpts fname outmode cgs
 63 |     = MkREPLOpts
 64 |         { showTypes = False
 65 |         , evalMode = NormaliseAll
 66 |         , evalTiming = False
 67 |         , mainfile = fname
 68 |         , literateStyle = litStyle fname
 69 |         , source = ""
 70 |         , editor = "vim"
 71 |         , errorLine = Nothing
 72 |         , idemode = outmode
 73 |         , currentElabSource = ""
 74 |         , psResult = Nothing
 75 |         , gdResult = Nothing
 76 |         , evalResultName = Nothing
 77 |         , extraCodegens = cgs
 78 |         , consoleWidth = Nothing
 79 |         , color = True
 80 |         , synHighlightOn = True
 81 |         }
 82 |   where
 83 |     litStyle : Maybe String -> Maybe LiterateStyle
 84 |     litStyle Nothing = Nothing
 85 |     litStyle (Just fn) = isLitFile fn
 86 |
 87 | export
 88 | data ROpts : Type where
 89 |
 90 | export
 91 | withROpts : {auto o : Ref ROpts REPLOpts} -> Core a -> Core a
 92 | withROpts = wrapRef ROpts (\_ => pure ())
 93 |
 94 | export
 95 | setOutput : {auto o : Ref ROpts REPLOpts} ->
 96 |             OutputMode -> Core ()
 97 | setOutput m = update ROpts { idemode := m }
 98 |
 99 | export
100 | getOutput : {auto o : Ref ROpts REPLOpts} -> Core OutputMode
101 | getOutput = idemode <$> get ROpts
102 |
103 | export
104 | setMainFile : {auto o : Ref ROpts REPLOpts} ->
105 |               Maybe String -> Core ()
106 | setMainFile src = update ROpts { mainfile      := src,
107 |                                  literateStyle := litStyle src }
108 |
109 | covering
110 | export
111 | resetProofState : {auto o : Ref ROpts REPLOpts} -> Core ()
112 | resetProofState = update ROpts { psResult := Nothing,
113 |                                  gdResult := Nothing }
114 |
115 | export
116 | setSource : {auto o : Ref ROpts REPLOpts} ->
117 |             String -> Core ()
118 | setSource src = update ROpts { source := src }
119 |
120 | export
121 | getSource : {auto o : Ref ROpts REPLOpts} ->
122 |             Core String
123 | getSource = source <$> get ROpts
124 |
125 | export
126 | getSourceLine : {auto o : Ref ROpts REPLOpts} ->
127 |                 Int -> Core (Maybe String)
128 | getSourceLine l
129 |     = do src <- getSource
130 |          pure $ elemAt (lines src) (integerToNat (cast (l-1)))
131 |
132 | export
133 | getLitStyle : {auto o : Ref ROpts REPLOpts} ->
134 |               Core (Maybe LiterateStyle)
135 | getLitStyle = literateStyle <$> get ROpts
136 |
137 | export
138 | setCurrentElabSource : {auto o : Ref ROpts REPLOpts} ->
139 |                        String -> Core ()
140 | setCurrentElabSource src = update ROpts { currentElabSource := src }
141 |
142 | export
143 | getCurrentElabSource : {auto o : Ref ROpts REPLOpts} ->
144 |                        Core String
145 | getCurrentElabSource = currentElabSource <$> get ROpts
146 |
147 | addCodegen : {auto o : Ref ROpts REPLOpts} ->
148 |              String -> Codegen -> Core ()
149 | addCodegen s cg = update ROpts { extraCodegens $= ((s,cg)::) }
150 |
151 | export
152 | getCodegen : {auto o : Ref ROpts REPLOpts} ->
153 |              String -> Core (Maybe Codegen)
154 | getCodegen s = lookup s . extraCodegens <$> get ROpts
155 |
156 | export
157 | getConsoleWidth : {auto o : Ref ROpts REPLOpts} -> Core (Maybe Nat)
158 | getConsoleWidth = consoleWidth <$> get ROpts
159 |
160 | export
161 | setConsoleWidth : {auto o : Ref ROpts REPLOpts} -> Maybe Nat -> Core ()
162 | setConsoleWidth n = update ROpts { consoleWidth := n }
163 |
164 | export
165 | getColor : {auto o : Ref ROpts REPLOpts} -> Core Bool
166 | getColor = color <$> get ROpts
167 |
168 | export
169 | setColor : {auto o : Ref ROpts REPLOpts} -> Bool -> Core ()
170 | setColor b = update ROpts { color := b }
171 |
172 | export
173 | getSynHighlightOn : {auto o : Ref ROpts REPLOpts} -> Core Bool
174 | getSynHighlightOn = synHighlightOn <$> get ROpts
175 |
176 | export
177 | setSynHighlightOn : {auto o : Ref ROpts REPLOpts} -> Bool -> Core ()
178 | setSynHighlightOn b = update ROpts { synHighlightOn := b }
179 |
180 | export
181 | getEvalTiming : {auto o : Ref ROpts REPLOpts} -> Core Bool
182 | getEvalTiming = evalTiming <$> get ROpts
183 |
184 | export
185 | setEvalTiming : {auto o : Ref ROpts REPLOpts} -> Bool -> Core ()
186 | setEvalTiming b = update ROpts { evalTiming := b }
187 |