/
InteractionTop.hs
1161 lines (999 loc) · 44.1 KB
/
InteractionTop.hs
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
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
{-# OPTIONS_GHC -fno-cse #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Agda.Interaction.InteractionTop
( module Agda.Interaction.InteractionTop
)
where
import Prelude hiding (null)
import Control.Concurrent
import Control.Concurrent.Async
import Control.Concurrent.STM.TChan
import Control.Concurrent.STM.TVar
import qualified Control.Exception as E
import Control.Monad.Identity
import Control.Monad.Reader
import Control.Monad.State hiding (state)
import Control.Monad.STM
import qualified Data.Char as Char
import Data.Function
import qualified Data.List as List
import qualified Data.Map as Map
import System.Directory
import System.FilePath
import Agda.TypeChecking.Monad as TM
hiding (initState, setCommandLineOptions)
import qualified Agda.TypeChecking.Monad as TM
import qualified Agda.TypeChecking.Pretty as TCP
import Agda.TypeChecking.Rules.Term (checkExpr, isType_)
import Agda.TypeChecking.Errors
import Agda.TypeChecking.Warnings (runPM)
import Agda.Syntax.Fixity
import Agda.Syntax.Position
import Agda.Syntax.Parser
import Agda.Syntax.Common
import Agda.Syntax.Concrete as C
import Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Pretty
import Agda.Syntax.Info (mkDefInfo)
import Agda.Syntax.Translation.ConcreteToAbstract
import Agda.Syntax.Translation.AbstractToConcrete hiding (withScope)
import Agda.Syntax.Scope.Base
import Agda.Interaction.Base
import Agda.Interaction.FindFile
import Agda.Interaction.Options
import Agda.Interaction.Options.Lenses as Lenses
import Agda.Interaction.MakeCase
import Agda.Interaction.SearchAbout
import Agda.Interaction.Response hiding (Function, ExtendedLambda)
import qualified Agda.Interaction.Response as R
import qualified Agda.Interaction.BasicOps as B
import Agda.Interaction.BasicOps hiding (whyInScope)
import Agda.Interaction.Highlighting.Precise hiding (Error, Postulate)
import qualified Agda.Interaction.Imports as Imp
import Agda.Interaction.Highlighting.Generate
import qualified Agda.Interaction.Highlighting.LaTeX as LaTeX
import Agda.Compiler.Common (IsMain (..))
import Agda.Compiler.Backend
import Agda.Auto.Auto as Auto
import Agda.Utils.Except
( ExceptT
, mkExceptT
, MonadError(catchError)
, runExceptT
)
import Agda.Utils.Either
import Agda.Utils.FileName
import Agda.Utils.Function
import Agda.Utils.Hash
import Agda.Utils.Lens
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Pretty
import Agda.Utils.String
import Agda.Utils.Time
import Agda.Utils.Tuple
import Agda.Utils.Impossible
------------------------------------------------------------------------
-- The CommandM monad
-- | Restore both 'TCState' and 'CommandState'.
localStateCommandM :: CommandM a -> CommandM a
localStateCommandM m = do
cSt <- get
tcSt <- getTC
x <- m
putTC tcSt
put cSt
return x
-- | Restore 'TCState', do not touch 'CommandState'.
liftLocalState :: TCM a -> CommandM a
liftLocalState = lift . localTCState
-- | Build an opposite action to 'lift' for state monads.
revLift
:: MonadState st m
=> (forall c . m c -> st -> k (c, st)) -- ^ run
-> (forall b . k b -> m b) -- ^ lift
-> (forall x . (m a -> k x) -> k x) -> m a -- ^ reverse lift in double negative position
revLift run lift' f = do
st <- get
(a, st') <- lift' $ f (`run` st)
put st'
return a
revLiftTC
:: MonadTCState m
=> (forall c . m c -> TCState -> k (c, TCState)) -- ^ run
-> (forall b . k b -> m b) -- ^ lift
-> (forall x . (m a -> k x) -> k x) -> m a -- ^ reverse lift in double negative position
revLiftTC run lift' f = do
st <- getTC
(a, st') <- lift' $ f (`run` st)
putTC st'
return a
-- | Opposite of 'liftIO' for 'CommandM'.
-- Use only if main errors are already catched.
commandMToIO :: (forall x . (CommandM a -> IO x) -> IO x) -> CommandM a
commandMToIO ci_i = revLift runStateT lift $ \ct -> revLiftTC runSafeTCM liftIO $ ci_i . (. ct)
-- | Lift a TCM action transformer to a CommandM action transformer.
liftCommandMT :: (forall x . TCM x -> TCM x) -> CommandM a -> CommandM a
liftCommandMT f m = revLift runStateT lift $ f . ($ m)
-- | Ditto, but restore state.
liftCommandMTLocalState :: (forall x . TCM x -> TCM x) -> CommandM a -> CommandM a
liftCommandMTLocalState f = liftCommandMT f . localStateCommandM
-- | Put a response by the callback function given by 'stInteractionOutputCallback'.
putResponse :: Response -> CommandM ()
putResponse = lift . appInteractionOutputCallback
-- | A Lens for 'theInteractionPoints'.
modifyTheInteractionPoints :: ([InteractionId] -> [InteractionId]) -> CommandM ()
modifyTheInteractionPoints f = modify $ \ s ->
s { theInteractionPoints = f (theInteractionPoints s) }
-- * Operations for manipulating 'oldInteractionScopes'.
-- | A Lens for 'oldInteractionScopes'.
modifyOldInteractionScopes :: (OldInteractionScopes -> OldInteractionScopes) -> CommandM ()
modifyOldInteractionScopes f = modify $ \ s ->
s { oldInteractionScopes = f $ oldInteractionScopes s }
insertOldInteractionScope :: InteractionId -> ScopeInfo -> CommandM ()
insertOldInteractionScope ii scope = do
lift $ reportSLn "interaction.scope" 20 $ "inserting old interaction scope " ++ show ii
modifyOldInteractionScopes $ Map.insert ii scope
removeOldInteractionScope :: InteractionId -> CommandM ()
removeOldInteractionScope ii = do
lift $ reportSLn "interaction.scope" 20 $ "removing old interaction scope " ++ show ii
modifyOldInteractionScopes $ Map.delete ii
getOldInteractionScope :: InteractionId -> CommandM ScopeInfo
getOldInteractionScope ii = do
ms <- gets $ Map.lookup ii . oldInteractionScopes
case ms of
Nothing -> fail $ "not an old interaction point: " ++ show ii
Just scope -> return scope
-- | Do setup and error handling for a command.
handleCommand_ :: CommandM () -> CommandM ()
handleCommand_ = handleCommand id (return ())
handleCommand :: (forall a. CommandM a -> CommandM a) -> CommandM () -> CommandM () -> CommandM ()
handleCommand wrap onFail cmd = handleNastyErrors $ wrap $ do
oldState <- getTC
-- -- Andreas, 2016-11-18 OLD CODE:
-- -- onFail and handleErr are executed in "new" command state (not TCState).
-- -- But it seems that if an exception is raised, it is identical to the old state,
-- -- see code for catchErr.
-- res <- (`catchErr` (return . Just)) $ Nothing <$ cmd
-- maybe (return ()) (\ e -> onFail >> handleErr e) res
-- Andreas, 2016-11-18 NEW CODE: execute onFail and handleErr in handler
-- which means (looking at catchErr) they run in state s rathern than s'.
-- Yet, it looks like s == s' in case the command failed.
cmd `catchErr` \ e -> do
onFail
handleErr e
-- Andreas, 2016-11-18, issue #2174
-- Reset TCState after error is handled, to get rid of metas created during failed command
lift $ do
newPersistentState <- useTC lensPersistentState
putTC oldState
lensPersistentState `setTCLens` newPersistentState
where
-- Preserves state so we can do unsolved meta highlighting
catchErr :: CommandM a -> (TCErr -> CommandM a) -> CommandM a
catchErr m h = do
s <- get
(x, s') <- lift $ do runStateT m s
`catchError_` \ e ->
runStateT (h e) s
put s'
return x
-- | Handle every possible kind of error (#637), except for
-- AsyncCancelled, which is used to abort Agda.
handleNastyErrors :: CommandM () -> CommandM ()
handleNastyErrors m = commandMToIO $ \ toIO -> do
let handle e =
Right <$>
(toIO $ handleErr $ Exception noRange $ text $ show e)
asyncHandler e@AsyncCancelled = return (Left e)
generalHandler (e :: E.SomeException) = handle e
r <- ((Right <$> toIO m) `E.catch` asyncHandler)
`E.catch` generalHandler
case r of
Right x -> return x
Left e -> E.throwIO e
-- | Displays an error and instructs Emacs to jump to the site of the
-- error. Because this function may switch the focus to another file
-- the status information is also updated.
handleErr e = do
unsolvedNotOK <- lift $ not . optAllowUnsolved <$> pragmaOptions
meta <- lift $ computeUnsolvedMetaWarnings
constr <- lift $ computeUnsolvedConstraints
err <- lift $ errorHighlighting e
modFile <- lift $ useTC stModuleToSource
method <- lift $ viewTC eHighlightingMethod
let info = compress $ mconcat $
-- Errors take precedence over unsolved things.
err : if unsolvedNotOK then [meta, constr] else []
-- TODO: make a better predicate for this
noError <- lift $ null <$> prettyError e
x <- lift $ optShowImplicit <$> useTC stPragmaOptions
unless noError $ mapM_ putResponse $
[ Resp_DisplayInfo $ Info_Error $ Info_GenericError e ] ++
tellEmacsToJumpToError (getRange e) ++
[ Resp_HighlightingInfo info KeepHighlighting
method modFile ] ++
[ Resp_Status $ Status { sChecked = False
, sShowImplicitArguments = x
} ]
-- | Run an 'IOTCM' value, catch the exceptions, emit output
--
-- If an error happens the state of 'CommandM' does not change,
-- but stPersistent may change (which contains successfully
-- loaded interfaces for example).
runInteraction :: IOTCM -> CommandM ()
runInteraction (IOTCM current highlighting highlightingMethod cmd) =
handleCommand inEmacs onFail $ do
currentAbs <- liftIO $ absolute current
-- Raises an error if the given file is not the one currently
-- loaded.
cf <- gets theCurrentFile
when (not (independent cmd) && Just currentAbs /= (fst <$> cf)) $
lift $ typeError $ GenericError "Error: First load the file."
withCurrentFile $ interpret cmd
cf' <- gets theCurrentFile
when (updateInteractionPointsAfter cmd
&&
Just currentAbs == (fst <$> cf')) $
putResponse . Resp_InteractionPoints =<< gets theInteractionPoints
where
inEmacs = liftCommandMT $ withEnv $ initEnv
{ envHighlightingLevel = highlighting
, envHighlightingMethod = highlightingMethod
}
-- If an independent command fails we should reset theCurrentFile (Issue853).
onFail | independent cmd = modify $ \ s -> s { theCurrentFile = Nothing }
| otherwise = return ()
------------------------------------------------------------------------
-- Command queues
-- | If the next command from the command queue is anything but an
-- actual command, then the command is returned.
--
-- If the command is an 'IOTCM' command, then the following happens:
-- The given computation is applied to the command and executed. If an
-- abort command is encountered (and acted upon), then the computation
-- is interrupted, the persistent state and all options are restored,
-- and some commands are sent to the frontend. If the computation was
-- not interrupted, then its result is returned.
-- TODO: It might be nice if some of the changes to the persistent
-- state inflicted by the interrupted computation were preserved.
maybeAbort :: (IOTCM -> CommandM a) -> CommandM (Command' (Maybe a))
maybeAbort m = do
commandState <- get
let q = commandQueue commandState
(n, cmd) <- liftIO $ atomically $ readTChan (commands q)
case cmd of
Done -> return Done
Error e -> return (Error e)
Command c -> do
tcState <- getTC
tcEnv <- askTC
result <- liftIO $ race
(runTCM tcEnv tcState $ runStateT (m c) commandState)
(waitForAbort n q)
case result of
Left ((x, commandState'), tcState') -> do
putTC tcState'
put commandState'
case c of
IOTCM _ _ _ Cmd_exit -> do
putResponse Resp_DoneExiting
return Done
_ -> return (Command (Just x))
Right a -> do
liftIO $ popAbortedCommands q a
putTC $ initState
{ stPersistentState = stPersistentState tcState
, stPreScopeState =
(stPreScopeState initState)
{ stPrePragmaOptions =
stPrePragmaOptions
(stPreScopeState tcState)
}
}
put $ (initCommandState (commandQueue commandState))
{ optionsOnReload = optionsOnReload commandState
}
putResponse Resp_DoneAborting
displayStatus
return (Command Nothing)
where
-- | Returns if the currently executing command should be aborted.
-- The "abort number" is returned.
waitForAbort
:: Integer
-- ^ The number of the currently executing command.
-> CommandQueue
-- ^ The command queue.
-> IO Integer
waitForAbort n q = do
atomically $ do
a <- readTVar (abort q)
case a of
Just a' | n <= a' -> return a'
_ -> retry
-- | Removes every command for which the command number is at most
-- the given number (the "abort number") from the command queue.
--
-- New commands could be added to the end of the queue while this
-- computation is running. This does not lead to a race condition,
-- because those commands have higher command numbers, so they will
-- not be removed.
popAbortedCommands :: CommandQueue -> Integer -> IO ()
popAbortedCommands q n = do
done <- atomically $ do
cmd <- tryReadTChan (commands q)
case cmd of
Nothing -> return True
Just c ->
if fst c <= n then
return False
else do
unGetTChan (commands q) c
return True
unless done $
popAbortedCommands q n
-- | Creates a command queue, and forks a thread that writes commands
-- to the queue. The queue is returned.
initialiseCommandQueue
:: IO Command
-- ^ Returns the next command.
-> IO CommandQueue
initialiseCommandQueue next = do
commands <- newTChanIO
abort <- newTVarIO Nothing
let -- Read commands. The argument is the number of the previous
-- command (other than abort commands) that was read, if any.
readCommands n = do
c <- next
case c of
Command (IOTCM _ _ _ Cmd_abort) -> do
atomically $ writeTVar abort (Just n)
readCommands n
_ -> do
n' <- return (succ n)
atomically $ writeTChan commands (n', c)
case c of
Done -> return ()
_ -> readCommands n'
_ <- forkIO (readCommands 0)
return (CommandQueue { .. })
---------------------------------------------------------
-- | Can the command run even if the relevant file has not been loaded
-- into the state?
independent :: Interaction -> Bool
independent (Cmd_load {}) = True
independent (Cmd_compile {}) = True
independent (Cmd_load_highlighting_info {}) = True
independent Cmd_tokenHighlighting {} = True
independent Cmd_show_version = True
independent _ = False
-- | Should 'Resp_InteractionPoints' be issued after the command has
-- run?
updateInteractionPointsAfter :: Interaction -> Bool
updateInteractionPointsAfter Cmd_load{} = True
updateInteractionPointsAfter Cmd_compile{} = True
updateInteractionPointsAfter Cmd_constraints{} = False
updateInteractionPointsAfter Cmd_metas{} = False
updateInteractionPointsAfter Cmd_show_module_contents_toplevel{} = False
updateInteractionPointsAfter Cmd_search_about_toplevel{} = False
updateInteractionPointsAfter Cmd_solveAll{} = True
updateInteractionPointsAfter Cmd_solveOne{} = True
updateInteractionPointsAfter Cmd_infer_toplevel{} = False
updateInteractionPointsAfter Cmd_compute_toplevel{} = False
updateInteractionPointsAfter Cmd_load_highlighting_info{} = False
updateInteractionPointsAfter Cmd_tokenHighlighting{} = False
updateInteractionPointsAfter Cmd_highlight{} = True
updateInteractionPointsAfter ShowImplicitArgs{} = False
updateInteractionPointsAfter ToggleImplicitArgs{} = False
updateInteractionPointsAfter Cmd_give{} = True
updateInteractionPointsAfter Cmd_refine{} = True
updateInteractionPointsAfter Cmd_intro{} = True
updateInteractionPointsAfter Cmd_refine_or_intro{} = True
updateInteractionPointsAfter Cmd_autoOne{} = True
updateInteractionPointsAfter Cmd_autoAll{} = True
updateInteractionPointsAfter Cmd_context{} = False
updateInteractionPointsAfter Cmd_helper_function{} = False
updateInteractionPointsAfter Cmd_infer{} = False
updateInteractionPointsAfter Cmd_goal_type{} = False
updateInteractionPointsAfter Cmd_elaborate_give{} = True
updateInteractionPointsAfter Cmd_goal_type_context{} = False
updateInteractionPointsAfter Cmd_goal_type_context_infer{} = False
updateInteractionPointsAfter Cmd_goal_type_context_check{} = False
updateInteractionPointsAfter Cmd_show_module_contents{} = False
updateInteractionPointsAfter Cmd_make_case{} = True
updateInteractionPointsAfter Cmd_compute{} = False
updateInteractionPointsAfter Cmd_why_in_scope{} = False
updateInteractionPointsAfter Cmd_why_in_scope_toplevel{} = False
updateInteractionPointsAfter Cmd_show_version{} = False
updateInteractionPointsAfter Cmd_abort{} = False
updateInteractionPointsAfter Cmd_exit{} = False
-- | Interpret an interaction
interpret :: Interaction -> CommandM ()
interpret (Cmd_load m argv) =
cmd_load' m argv True Imp.TypeCheck $ \_ -> interpret Cmd_metas
interpret (Cmd_compile backend file argv) =
cmd_load' file argv (backend `elem` [LaTeX, QuickLaTeX])
(if backend == QuickLaTeX
then Imp.ScopeCheck
else Imp.TypeCheck) $ \(i, mw) -> do
mw' <- lift $ Imp.applyFlagsToMaybeWarnings mw
case mw' of
Imp.NoWarnings -> do
lift $ case backend of
LaTeX -> LaTeX.generateLaTeX i
QuickLaTeX -> LaTeX.generateLaTeX i
OtherBackend "GHCNoMain" -> callBackend "GHC" NotMain i -- for backwards compatibility
OtherBackend b -> callBackend b IsMain i
display_info . Info_CompilationOk =<< lift getWarningsAndNonFatalErrors
Imp.SomeWarnings w -> display_info $ Info_Error $ Info_CompilationError w
interpret Cmd_constraints =
display_info . Info_Constraints =<< lift B.getConstraints
interpret Cmd_metas = do
ms <- lift B.getGoals
display_info . Info_AllGoalsWarnings ms =<< lift getWarningsAndNonFatalErrors
interpret (Cmd_show_module_contents_toplevel norm s) =
liftCommandMT B.atTopLevel $ showModuleContents norm noRange s
interpret (Cmd_search_about_toplevel norm s) =
liftCommandMT B.atTopLevel $ searchAbout norm noRange s
interpret (Cmd_solveAll norm) = solveInstantiatedGoals norm Nothing
interpret (Cmd_solveOne norm ii _ _) = solveInstantiatedGoals norm' (Just ii)
-- `solveOne` is called via `agda2-maybe-normalised` which does not use
-- AsIs < Simplified < Normalised but rather Simplified < Instantiated < Normalised
-- So we remap the Rewrite modifiers to match solveAll's behaviour.
-- NB: instantiate is called in getSolvedInteractionPoints no matter what.
where norm' = case norm of
Simplified -> AsIs
Instantiated -> Simplified
_ -> norm
interpret (Cmd_infer_toplevel norm s) = do
(time, expr) <- parseAndDoAtToplevel (B.typeInCurrent norm) s
state <- get
display_info $ Info_InferredType state time expr
interpret (Cmd_compute_toplevel cmode s) = do
(time, expr) <- parseAndDoAtToplevel action (computeWrapInput cmode s)
state <- get
display_info $ Info_NormalForm state cmode time expr
where
action = allowNonTerminatingReductions
. (if computeIgnoreAbstract cmode then ignoreAbstractMode else inConcreteMode)
. B.evalInCurrent
-- interpret (Cmd_compute_toplevel cmode s) =
-- parseAndDoAtToplevel action Info_NormalForm $ computeWrapInput cmode s
-- where
-- action = allowNonTerminatingReductions
-- . (if computeIgnoreAbstract cmode then ignoreAbstractMode else inConcreteMode)
-- . (B.showComputed cmode <=< B.evalInCurrent)
interpret (ShowImplicitArgs showImpl) = do
opts <- lift commandLineOptions
setCommandLineOpts $
opts { optPragmaOptions =
(optPragmaOptions opts) { optShowImplicit = showImpl } }
interpret ToggleImplicitArgs = do
opts <- lift commandLineOptions
let ps = optPragmaOptions opts
setCommandLineOpts $
opts { optPragmaOptions =
ps { optShowImplicit = not $ optShowImplicit ps } }
interpret (Cmd_load_highlighting_info source) = do
l <- asksTC envHighlightingLevel
when (l /= None) $ do
-- Make sure that the include directories have
-- been set.
setCommandLineOpts =<< lift commandLineOptions
resp <- lift $ liftIO . tellToUpdateHighlighting =<< do
ex <- liftIO $ doesFileExist source
absSource <- liftIO $ SourceFile <$> absolute source
case ex of
False -> return Nothing
True -> (do
si <- Imp.sourceInfo absSource
let m = Imp.siModuleName si
checkModuleName m absSource Nothing
mmi <- getVisitedModule m
case mmi of
Nothing -> return Nothing
Just mi ->
if hashText (Imp.siSource si) ==
iSourceHash (miInterface mi)
then do
modFile <- useTC stModuleToSource
method <- viewTC eHighlightingMethod
return $ Just (iHighlighting $ miInterface mi, method, modFile)
else
return Nothing)
`catchError`
\_ -> return Nothing
mapM_ putResponse resp
interpret (Cmd_tokenHighlighting source remove) = do
info <- do l <- asksTC envHighlightingLevel
if l == None
then return Nothing
else do
source' <- liftIO (absolute source)
lift $ (Just <$> generateTokenInfo source')
`catchError` \_ ->
return Nothing
`finally`
case remove of
Remove -> liftIO $ removeFile source
Keep -> return ()
case info of
Just info' -> lift $ printHighlightingInfo RemoveHighlighting info'
Nothing -> return ()
interpret (Cmd_highlight ii rng s) = do
l <- asksTC envHighlightingLevel
when (l /= None) $ do
scope <- getOldInteractionScope ii
removeOldInteractionScope ii
handle $ do
parsed <- try (Info_HighlightingParseError ii) $
B.parseExpr rng s
expr <- try (Info_HighlightingScopeCheckError ii) $
concreteToAbstract scope parsed
lift $ printHighlightingInfo KeepHighlighting =<<
generateTokenInfoFromString rng s
lift $ highlightExpr expr
where
handle :: ExceptT Info_Error TCM () -> CommandM ()
handle m = do
res <- lift $ runExceptT m
case res of
Left err -> display_info $ Info_Error err
Right _ -> return ()
try :: Info_Error -> TCM a -> ExceptT Info_Error TCM a
try err m = mkExceptT $ do
(mapLeft (const err) <$> freshTCM m) `catchError` \ _ -> return (Left err)
-- freshTCM to avoid scope checking creating new interaction points
interpret (Cmd_give force ii rng s) = give_gen force ii rng s Give
interpret (Cmd_refine ii rng s) = give_gen WithoutForce ii rng s Refine
interpret (Cmd_intro pmLambda ii rng _) = do
ss <- lift $ B.introTactic pmLambda ii
liftCommandMT (B.withInteractionId ii) $ case ss of
[] -> do
display_info $ Info_Intro_NotFound
[s] -> give_gen WithoutForce ii rng s Intro
_:_:_ -> do
display_info $ Info_Intro_ConstructorUnknown ss
interpret (Cmd_refine_or_intro pmLambda ii r s) = interpret $
let s' = trim s
in (if null s' then Cmd_intro pmLambda else Cmd_refine) ii r s'
interpret (Cmd_autoOne ii rng hint) = do
-- Andreas, 2014-07-05 Issue 1226:
-- Save the state to have access to even those interaction ids
-- that Auto solves (since Auto gives the solution right away).
st <- getTC
(time , res) <- maybeTimed $ Auto.auto ii rng hint
case autoProgress res of
Solutions sols -> do
lift $ reportSLn "auto" 10 $ "Auto produced the following solutions " ++ show sols
forM_ sols $ \(ii', sol) -> do
-- Andreas, 2014-07-05 Issue 1226:
-- For highlighting, Resp_GiveAction needs to access
-- the @oldInteractionScope@s of the interaction points solved by Auto.
-- We dig them out from the state before Auto was invoked.
insertOldInteractionScope ii' =<< liftLocalState (putTC st >> getInteractionScope ii')
-- Andreas, 2014-07-07: NOT TRUE:
-- -- Andreas, 2014-07-05: The following should be obsolete,
-- -- as Auto has removed the interaction points already:
-- modifyTheInteractionPoints $ filter (/= ii)
putResponse $ Resp_GiveAction ii' $ Give_String sol
-- Andreas, 2014-07-07: Remove the interaction points in one go.
modifyTheInteractionPoints (List.\\ (map fst sols))
case autoMessage res of
Nothing -> interpret Cmd_metas
Just msg -> display_info $ Info_Auto msg
FunClauses cs -> do
case autoMessage res of
Nothing -> return ()
Just msg -> display_info $ Info_Auto msg
putResponse $ Resp_MakeCase ii R.Function cs
Refinement s -> give_gen WithoutForce ii rng s Refine
maybe (return ()) (display_info . Info_Time) time
interpret Cmd_autoAll = do
iis <- getInteractionPoints
unless (null iis) $ do
let time = 1000 `div` length iis
st <- getTC
solved <- forM iis $ \ ii -> do
rng <- getInteractionRange ii
res <- Auto.auto ii rng ("-t " ++ show time ++ "ms")
case autoProgress res of
Solutions sols -> forM sols $ \ (jj, s) -> do
oldInteractionScope <- liftLocalState (putTC st >> getInteractionScope jj)
insertOldInteractionScope jj oldInteractionScope
putResponse $ Resp_GiveAction ii $ Give_String s
return jj
_ -> return []
modifyTheInteractionPoints (List.\\ concat solved)
interpret (Cmd_context norm ii _ _) =
display_info . Info_Context ii =<< liftLocalState (getResponseContext norm ii)
interpret (Cmd_helper_function norm ii rng s) = do
-- Create type of application of new helper function that would solve the goal.
helperType <- liftLocalState $ B.withInteractionId ii $ inTopContext $ B.metaHelperType norm ii rng s
display_info $ Info_GoalSpecific ii (Goal_HelperFunction helperType)
interpret (Cmd_infer norm ii rng s) = do
expr <- liftLocalState $ B.withInteractionId ii $ B.typeInMeta ii norm =<< B.parseExprIn ii rng s
display_info $ Info_GoalSpecific ii (Goal_InferredType expr)
interpret (Cmd_goal_type norm ii _ _) =
display_info $ Info_GoalSpecific ii (Goal_CurrentGoal norm)
interpret (Cmd_elaborate_give norm ii rng s) = do
have <- liftLocalState $ B.withInteractionId ii $ do
expr <- B.parseExprIn ii rng s
goal <- B.typeOfMeta AsIs ii
term <- case goal of
OfType _ ty -> checkExpr expr =<< isType_ ty
_ -> __IMPOSSIBLE__
nf <- normalForm norm term
txt <- localTC (\ e -> e { envPrintMetasBare = True }) (TCP.prettyTCM nf)
return $ show txt
give_gen WithoutForce ii rng have ElaborateGive
interpret (Cmd_goal_type_context norm ii rng s) =
cmd_goal_type_context_and GoalOnly norm ii rng s
interpret (Cmd_goal_type_context_infer norm ii rng s) = do
-- In case of the empty expression to type, don't fail with
-- a stupid parse error, but just fall back to
-- Cmd_goal_type_context.
aux <- if all Char.isSpace s
then return GoalOnly
else do
typ <- liftLocalState
$ B.withInteractionId ii
$ B.typeInMeta ii norm =<< B.parseExprIn ii rng s
return (GoalAndHave typ)
cmd_goal_type_context_and aux norm ii rng s
interpret (Cmd_goal_type_context_check norm ii rng s) = do
term <- liftLocalState $ B.withInteractionId ii $ do
expr <- B.parseExprIn ii rng s
goal <- B.typeOfMeta AsIs ii
term <- case goal of
OfType _ ty -> checkExpr expr =<< isType_ ty
_ -> __IMPOSSIBLE__
normalForm norm term
cmd_goal_type_context_and (GoalAndElaboration term) norm ii rng s
interpret (Cmd_show_module_contents norm ii rng s) =
liftCommandMT (B.withInteractionId ii) $ showModuleContents norm rng s
interpret (Cmd_why_in_scope_toplevel s) =
liftCommandMT B.atTopLevel $ whyInScope s
interpret (Cmd_why_in_scope ii _range s) =
liftCommandMT (B.withInteractionId ii) $ whyInScope s
interpret (Cmd_make_case ii rng s) = do
(f, casectxt, cs) <- lift $ makeCase ii rng s
liftCommandMT (B.withInteractionId ii) $ do
tel <- lift $ lookupSection (qnameModule f) -- don't shadow the names in this telescope
unicode <- getsTC $ optUseUnicode . getPragmaOptions
pcs :: [Doc] <- lift $ inTopContext $ addContext tel $ mapM prettyA cs
let pcs' :: [String] = List.map (extlam_dropName unicode casectxt . decorate) pcs
lift $ reportSDoc "interaction.case" 60 $ TCP.vcat
[ "InteractionTop.Cmd_make_case"
, TCP.nest 2 $ TCP.vcat
[ "cs = " TCP.<+> TCP.vcat (map prettyA cs)
, "pcs = " TCP.<+> TCP.vcat (map return pcs)
, "pcs' = " TCP.<+> TCP.vcat (map TCP.text pcs')
]
]
lift $ reportSDoc "interaction.case" 90 $ TCP.vcat
[ "InteractionTop.Cmd_make_case"
, TCP.nest 2 $ TCP.vcat
[ "cs = " TCP.<+> TCP.text (show cs)
]
]
putResponse $ Resp_MakeCase ii (makeCaseVariant casectxt) pcs'
where
decorate = renderStyle (style { mode = OneLineMode })
makeCaseVariant :: CaseContext -> MakeCaseVariant
makeCaseVariant Nothing = R.Function
makeCaseVariant Just{} = R.ExtendedLambda
-- very dirty hack, string manipulation by dropping the function name
-- and replacing the last " = " with " -> ". It's important not to replace
-- the equal sign in named implicit with an arrow!
extlam_dropName :: Bool -> CaseContext -> String -> String
extlam_dropName _ Nothing x = x
extlam_dropName unicode Just{} x
= unwords $ reverse $ replEquals $ reverse $ drop 1 $ words x
where
replEquals ("=" : ws)
| unicode = "→" : ws
| otherwise = "->" : ws
replEquals (w : ws) = w : replEquals ws
replEquals [] = []
interpret (Cmd_compute cmode ii rng s) = do
expr <- liftLocalState $ do
e <- B.parseExprIn ii rng (computeWrapInput cmode s)
B.withInteractionId ii $ applyWhen (computeIgnoreAbstract cmode) ignoreAbstractMode $ B.evalInCurrent e
display_info $ Info_GoalSpecific ii (Goal_NormalForm cmode expr)
interpret Cmd_show_version = display_info Info_Version
interpret Cmd_abort = return ()
interpret Cmd_exit = return ()
-- | Solved goals already instantiated internally
-- The second argument potentially limits it to one specific goal.
solveInstantiatedGoals :: Rewrite -> Maybe InteractionId -> CommandM ()
solveInstantiatedGoals norm mii = do
-- Andreas, 2016-10-23 issue #2280: throw away meta elims.
out <- lift $ localTC (\ e -> e { envPrintMetasBare = True }) $ do
sip <- B.getSolvedInteractionPoints False norm
-- only solve metas which have a proper instantiation, i.e., not another meta
let sip' = maybe id (\ ii -> filter ((ii ==) . fst3)) mii sip
mapM prt sip'
putResponse $ Resp_SolveAll out
where
prt (i, m, e) = do
mi <- getMetaInfo <$> lookupMeta m
e' <- withMetaInfo mi $ abstractToConcreteCtx TopCtx e
return (i, e')
-- | @cmd_load' file argv unsolvedOk cmd@
-- loads the module in file @file@,
-- using @argv@ as the command-line options.
--
-- If type checking completes without any exceptions having been
-- encountered then the command @cmd r@ is executed, where @r@ is the
-- result of 'Imp.typeCheckMain'.
cmd_load' :: FilePath -> [String]
-> Bool -- ^ Allow unsolved meta-variables?
-> Imp.Mode -- ^ Full type-checking, or only
-- scope-checking?
-> ((Interface, Imp.MaybeWarnings) -> CommandM ())
-> CommandM ()
cmd_load' file argv unsolvedOK mode cmd = do
f <- liftIO $ SourceFile <$> absolute file
ex <- liftIO $ doesFileExist $ filePath (srcFilePath f)
unless ex $ typeError $ GenericError $
"The file " ++ file ++ " was not found."
-- Forget the previous "current file" and interaction points.
modify $ \ st -> st { theInteractionPoints = []
, theCurrentFile = Nothing
}
t <- liftIO $ getModificationTime file
-- Parse the file.
si <- lift (Imp.sourceInfo f)
-- All options are reset when a file is reloaded, including the
-- choice of whether or not to display implicit arguments.
opts0 <- gets optionsOnReload
backends <- useTC stBackends
z <- liftIO $ runOptM $ parseBackendOptions backends argv opts0
case z of
Left err -> lift $ typeError $ GenericError err
Right (_, opts) -> do
let update o = o { optAllowUnsolved = unsolvedOK && optAllowUnsolved o}
root = projectRoot (srcFilePath f) (Imp.siModuleName si)
lift $ TM.setCommandLineOptions' root $ mapPragmaOptions update opts
displayStatus
-- Reset the state, preserving options and decoded modules. Note
-- that if the include directories have changed, then the decoded
-- modules are reset when cmd_load' is run by ioTCM.
lift resetState
-- Clear the info buffer to make room for information about which
-- module is currently being type-checked.
putResponse Resp_ClearRunningInfo
-- Remove any prior syntax highlighting.
putResponse (Resp_ClearHighlighting NotOnlyTokenBased)
ok <- lift $ Imp.typeCheckMain f mode si
-- The module type checked. If the file was not changed while the
-- type checker was running then the interaction points and the
-- "current file" are stored.
t' <- liftIO $ getModificationTime file
when (t == t') $ do
is <- lift $ sortInteractionPoints =<< getInteractionPoints
modify $ \st -> st { theInteractionPoints = is
, theCurrentFile = Just (srcFilePath f, t)
}
cmd ok
-- | Set 'envCurrentPath' to 'theCurrentFile', if any.
withCurrentFile :: CommandM a -> CommandM a
withCurrentFile m = do
mfile <- fmap fst <$> gets theCurrentFile
localTC (\ e -> e { envCurrentPath = mfile }) m
data GiveRefine = Give | Refine | Intro | ElaborateGive
deriving (Eq, Show)
-- | A "give"-like action (give, refine, etc).
--
-- @give_gen force ii rng s give_ref mk_newtxt@
-- acts on interaction point @ii@
-- occupying range @rng@,
-- placing the new content given by string @s@,
-- and replacing @ii@ by the newly created interaction points
-- in the state if safety checks pass (unless @force@ is applied).
give_gen
:: UseForce -- ^ Should safety checks be skipped?
-> InteractionId
-> Range
-> String
-> GiveRefine
-> CommandM ()
give_gen force ii rng s0 giveRefine = do
let s = trim s0
lift $ reportSLn "interaction.give" 20 $ "give_gen " ++ s
-- Andreas, 2015-02-26 if string is empty do nothing rather
-- than giving a parse error.
unless (null s) $ do
let give_ref =
case giveRefine of
Give -> B.give
Refine -> B.refine
Intro -> B.refine
ElaborateGive -> B.give
-- save scope of the interaction point (for printing the given expr. later)
scope <- lift $ getInteractionScope ii
-- parse string and "give", obtaining an abstract expression
-- and newly created interaction points
(time, (ae, ae0, iis)) <- maybeTimed $ lift $ do
mis <- getInteractionPoints
reportSLn "interaction.give" 30 $ "interaction points before = " ++ show mis
given <- B.parseExprIn ii rng s
ae <- give_ref force ii Nothing given
mis' <- getInteractionPoints
reportSLn "interaction.give" 30 $ "interaction points after = " ++ show mis'
return (ae, given, mis' List.\\ mis)
-- favonia: backup the old scope for highlighting
insertOldInteractionScope ii scope
-- sort the new interaction points and put them into the state
-- in replacement of the old interaction point
iis' <- lift $ sortInteractionPoints iis
modifyTheInteractionPoints $ replace ii iis'
-- print abstract expr
ce <- lift $ abstractToConcreteScope scope ae
lift $ reportS "interaction.give" 30
[ "ce = " ++ show ce
, "scopePrecedence = " ++ show (scope ^. scopePrecedence)
]
-- if the command was @Give@, use the literal user input;
-- Andreas, 2014-01-15, see issue 1020:
-- Refine could solve a goal by introducing the sole constructor
-- without arguments. Then there are no interaction metas, but
-- we still cannot just `give' the user string (which may be empty).
-- WRONG: also, if no interaction metas were created by @Refine@
-- WRONG: let literally = (giveRefine == Give || null iis) && rng /= noRange
-- Ulf, 2015-03-30, if we're doing intro we can't do literal give since
-- there is nothing in the hole (issue 1892).
let literally = giveRefine /= Intro && giveRefine /= ElaborateGive && ae == ae0 && rng /= noRange
-- Ulf, 2014-01-24: This works for give since we're highlighting the string
-- that's already in the buffer. Doing it before the give action means that
-- the highlighting is moved together with the text when the hole goes away.
-- To make it work for refine we'd have to adjust the ranges.
when literally $ lift $ do
l <- asksTC envHighlightingLevel
when (l /= None) $ do
printHighlightingInfo KeepHighlighting =<<
generateTokenInfoFromString rng s
highlightExpr ae
putResponse $ Resp_GiveAction ii $ mkNewTxt literally ce
lift $ reportSLn "interaction.give" 30 $ "putResponse GiveAction passed"
-- display new goal set (if not measuring time)
maybe (interpret Cmd_metas) (display_info . Info_Time) time
lift $ reportSLn "interaction.give" 30 $ "interpret Cmd_metas passed"
where
-- Substitutes xs for x in ys.
replace x xs ys = concatMap (\ y -> if y == x then xs else [y]) ys