← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to src/full/Agda/TypeChecking/Monad/State.hs

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/full/Agda/TypeChecking/Monad/State.hs
 
1
-- | Lenses for 'TCState' and more.
1
2
 
2
3
module Agda.TypeChecking.Monad.State where
3
4
 
4
5
import Control.Applicative
 
6
import qualified Control.Exception as E
5
7
import Control.Monad.State
6
8
import Data.Set (Set)
7
9
import Data.Map as Map
8
10
import qualified Data.Set as Set
9
11
 
 
12
-- import {-# SOURCE #-} Agda.Interaction.Response
 
13
import Agda.Interaction.Response
 
14
  (InteractionOutputCallback, Response)
 
15
 
10
16
import Agda.Syntax.Common
11
17
import Agda.Syntax.Scope.Base
12
18
import qualified Agda.Syntax.Concrete.Name as C
14
20
import Agda.Syntax.Abstract.Name
15
21
 
16
22
import Agda.TypeChecking.Monad.Base
 
23
import Agda.TypeChecking.Monad.Base.Benchmark
 
24
import {-# SOURCE #-} Agda.TypeChecking.Monad.Options
17
25
 
18
26
import Agda.Utils.Hash
 
27
import Agda.Utils.Monad (bracket_)
 
28
import Agda.Utils.Pretty
19
29
 
20
30
-- | Resets the non-persistent part of the type checking state.
21
31
 
22
32
resetState :: TCM ()
23
33
resetState = do
24
 
    pers <- stPersistent <$> get
 
34
    pers <- gets stPersistent
25
35
    put $ initState { stPersistent = pers }
26
36
 
27
37
-- | Resets all of the type checking state.
 
38
--
 
39
--   Keep only 'Benchmark' information.
28
40
 
29
41
resetAllState :: TCM ()
30
 
resetAllState = put initState
31
 
 
32
 
setScope :: ScopeInfo -> TCM ()
33
 
setScope scope = modify $ \s -> s { stScope = scope }
 
42
resetAllState = do
 
43
    b <- getBenchmark
 
44
    put $ updatePersistentState (\ s -> s { stBenchmark = b }) initState
 
45
-- resetAllState = put initState
 
46
 
 
47
-- | Restore 'TCState' after performing subcomputation.
 
48
--
 
49
--   In contrast to 'Agda.Utils.Monad.localState', the 'Benchmark'
 
50
--   info from the subcomputation is saved.
 
51
localTCState :: TCM a -> TCM a
 
52
localTCState = bracket_ get $ \ s -> do
 
53
   b <- getBenchmark
 
54
   put s
 
55
   modifyBenchmark $ const b
 
56
 
 
57
---------------------------------------------------------------------------
 
58
-- * Lens for persistent state
 
59
---------------------------------------------------------------------------
 
60
 
 
61
updatePersistentState :: (PersistentTCState -> PersistentTCState) -> (TCState -> TCState)
 
62
updatePersistentState f s = s { stPersistent = f (stPersistent s) }
 
63
 
 
64
modifyPersistentState :: (PersistentTCState -> PersistentTCState) -> TCM ()
 
65
modifyPersistentState = modify . updatePersistentState
 
66
 
 
67
---------------------------------------------------------------------------
 
68
-- * Scope
 
69
---------------------------------------------------------------------------
34
70
 
35
71
-- | Get the current scope.
36
72
getScope :: TCM ScopeInfo
37
73
getScope = gets stScope
38
74
 
39
 
getPatternSyns :: TCM PatternSynDefns
40
 
getPatternSyns = gets stPatternSyns
41
 
 
42
 
setPatternSyns :: PatternSynDefns -> TCM ()
43
 
setPatternSyns m = modify $ \s -> s { stPatternSyns = m }
44
 
 
45
 
modifyPatternSyns :: (PatternSynDefns -> PatternSynDefns) -> TCM ()
46
 
modifyPatternSyns f = do
47
 
  s <- getPatternSyns
48
 
  setPatternSyns $ f s
49
 
 
50
 
getPatternSynImports :: TCM PatternSynDefns
51
 
getPatternSynImports = gets stPatternSynImports
52
 
 
53
 
lookupPatternSyn :: QName -> TCM PatternSynDefn
54
 
lookupPatternSyn x = do
55
 
    s <- getPatternSyns
56
 
    case Map.lookup x s of
57
 
        Just d  -> return d
58
 
        Nothing -> do
59
 
            si <- getPatternSynImports
60
 
            case Map.lookup x si of
61
 
                Just d  -> return d
62
 
                Nothing -> typeError $ NotInScope [qnameToConcrete x]
63
 
 
64
 
setExtLambdaTele :: Map QName (Int , Int) -> TCM ()
65
 
setExtLambdaTele tele = modify $ \s -> s { stExtLambdaTele = tele }
66
 
 
67
 
getExtLambdaTele :: TCM (Map QName (Int , Int))
68
 
getExtLambdaTele = gets stExtLambdaTele
69
 
 
70
 
addExtLambdaTele :: QName -> (Int , Int) -> TCM ()
71
 
addExtLambdaTele id x = getExtLambdaTele >>= setExtLambdaTele . (insert id x)
 
75
-- | Set the current scope.
 
76
setScope :: ScopeInfo -> TCM ()
 
77
setScope scope = modifyScope (const scope)
72
78
 
73
79
-- | Modify the current scope.
74
80
modifyScope :: (ScopeInfo -> ScopeInfo) -> TCM ()
75
 
modifyScope f = do
76
 
  s <- getScope
77
 
  setScope $ f s
 
81
modifyScope f = modify $ \ s -> s { stScope = f (stScope s) }
78
82
 
79
83
-- | Run a computation in a local scope.
80
84
withScope :: ScopeInfo -> TCM a -> TCM (a, ScopeInfo)
101
102
  setScope scope
102
103
  return x
103
104
 
 
105
-- | Scope error.
 
106
notInScope :: C.QName -> TCM a
 
107
notInScope x = do
 
108
  printScope "unbound" 5 ""
 
109
  typeError $ NotInScope [x]
 
110
 
 
111
-- | Debug print the scope.
 
112
printScope :: String -> Int -> String -> TCM ()
 
113
printScope tag v s = verboseS ("scope." ++ tag) v $ do
 
114
  scope <- getScope
 
115
  reportSDoc ("scope." ++ tag) v $ return $ vcat [ text s, text $ show scope ]
 
116
 
 
117
---------------------------------------------------------------------------
 
118
-- * Top level module
 
119
---------------------------------------------------------------------------
 
120
 
104
121
-- | Set the top-level module. This affects the global module id of freshly
105
122
--   generated names.
106
123
 
111
128
setTopLevelModule x =
112
129
  modify $ \s -> s
113
130
    { stFreshThings = (stFreshThings s)
114
 
      { fName = NameId 0 $ hash (show x)
 
131
      { fName = NameId 0 $ hashString (show x)
115
132
      }
116
133
    }
117
134
 
125
142
  modify $ \s -> s { stFreshThings = (stFreshThings s) { fName = next } }
126
143
  return y
127
144
 
 
145
---------------------------------------------------------------------------
 
146
-- * Haskell imports
 
147
---------------------------------------------------------------------------
 
148
 
128
149
-- | Tell the compiler to import the given Haskell module.
129
150
addHaskellImport :: String -> TCM ()
130
151
addHaskellImport i =
133
154
-- | Get the Haskell imports.
134
155
getHaskellImports :: TCM (Set String)
135
156
getHaskellImports = gets stHaskellImports
 
157
 
 
158
---------------------------------------------------------------------------
 
159
-- * Interaction output callback
 
160
---------------------------------------------------------------------------
 
161
 
 
162
getInteractionOutputCallback :: TCM InteractionOutputCallback
 
163
getInteractionOutputCallback
 
164
  = gets $ stInteractionOutputCallback . stPersistent
 
165
 
 
166
appInteractionOutputCallback :: Response -> TCM ()
 
167
appInteractionOutputCallback r
 
168
  = getInteractionOutputCallback >>= \ cb -> cb r
 
169
 
 
170
setInteractionOutputCallback :: InteractionOutputCallback -> TCM ()
 
171
setInteractionOutputCallback cb
 
172
  = modifyPersistentState $ \ s -> s { stInteractionOutputCallback = cb }
 
173
 
 
174
---------------------------------------------------------------------------
 
175
-- * Pattern synonyms
 
176
---------------------------------------------------------------------------
 
177
 
 
178
getPatternSyns :: TCM PatternSynDefns
 
179
getPatternSyns = gets stPatternSyns
 
180
 
 
181
setPatternSyns :: PatternSynDefns -> TCM ()
 
182
setPatternSyns m = modifyPatternSyns (const m)
 
183
 
 
184
-- | Lens for 'stPatternSyns'.
 
185
modifyPatternSyns :: (PatternSynDefns -> PatternSynDefns) -> TCM ()
 
186
modifyPatternSyns f = modify $ \s -> s { stPatternSyns = f (stPatternSyns s) }
 
187
 
 
188
getPatternSynImports :: TCM PatternSynDefns
 
189
getPatternSynImports = gets stPatternSynImports
 
190
 
 
191
lookupPatternSyn :: QName -> TCM PatternSynDefn
 
192
lookupPatternSyn x = do
 
193
    s <- getPatternSyns
 
194
    case Map.lookup x s of
 
195
        Just d  -> return d
 
196
        Nothing -> do
 
197
            si <- getPatternSynImports
 
198
            case Map.lookup x si of
 
199
                Just d  -> return d
 
200
                Nothing -> notInScope $ qnameToConcrete x
 
201
 
 
202
---------------------------------------------------------------------------
 
203
-- * Benchmark
 
204
---------------------------------------------------------------------------
 
205
 
 
206
-- | Lens getter for 'Benchmark' from 'TCState'.
 
207
theBenchmark :: TCState -> Benchmark
 
208
theBenchmark = stBenchmark . stPersistent
 
209
 
 
210
-- | Lens map for 'Benchmark'.
 
211
updateBenchmark :: (Benchmark -> Benchmark) -> TCState -> TCState
 
212
updateBenchmark f = updatePersistentState $ \ s -> s { stBenchmark = f (stBenchmark s) }
 
213
 
 
214
-- | Lens getter for 'Benchmark' from 'TCM'.
 
215
getBenchmark :: TCM Benchmark
 
216
getBenchmark = gets $ theBenchmark
 
217
 
 
218
-- | Lens modify for 'Benchmark'.
 
219
modifyBenchmark :: (Benchmark -> Benchmark) -> TCM ()
 
220
modifyBenchmark = modify . updateBenchmark
 
221
 
 
222
-- | Run a fresh instance of the TCM (with initial state).
 
223
--   'Benchmark' info is preserved.
 
224
freshTCM :: TCM a -> TCM (Either TCErr a)
 
225
freshTCM m = do
 
226
  -- Prepare an initial state with current benchmark info.
 
227
  b <- getBenchmark
 
228
  let s = updateBenchmark (const b) initState
 
229
  -- Run subcomputation in initial state.
 
230
  -- If we encounter an exception, we lose the state and the
 
231
  -- benchmark info.
 
232
  -- We could retrieve i from a type error, which carries the state,
 
233
  -- but we do not care for benchmarking in the presence of errors.
 
234
  r <- liftIO $ (Right <$> runTCM initEnv s m) `E.catch` (return . Left)
 
235
  case r of
 
236
    Left err     -> return $ Left err
 
237
    Right (a, s) -> do
 
238
      -- Keep only the benchmark info from the final state of the subcomp.
 
239
      modifyBenchmark $ const $ theBenchmark s
 
240
      return $ Right a