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