summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/Monad/State.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/Monad/State.hs')
-rw-r--r--src/full/Agda/TypeChecking/Monad/State.hs47
1 files changed, 28 insertions, 19 deletions
diff --git a/src/full/Agda/TypeChecking/Monad/State.hs b/src/full/Agda/TypeChecking/Monad/State.hs
index d1ce131..c58c835 100644
--- a/src/full/Agda/TypeChecking/Monad/State.hs
+++ b/src/full/Agda/TypeChecking/Monad/State.hs
@@ -1,4 +1,5 @@
{-# LANGUAGE CPP #-}
+{-# LANGUAGE BangPatterns #-}
-- | Lenses for 'TCState' and more.
@@ -10,7 +11,8 @@ import qualified Control.Exception as E
import Control.Monad.State (put, get, gets, modify)
import Control.Monad.Trans (liftIO)
-import Data.Map as Map
+import Data.Map (Map)
+import qualified Data.Map as Map
import Data.Monoid
import Data.Set (Set)
import qualified Data.Set as Set
@@ -31,6 +33,7 @@ import Agda.Syntax.Internal
import Agda.TypeChecking.Monad.Base
import {-# SOURCE #-} Agda.TypeChecking.Monad.Options
import Agda.TypeChecking.Positivity.Occurrence
+import Agda.TypeChecking.CompiledClause
import Agda.Utils.Hash
import qualified Agda.Utils.HashMap as HMap
@@ -176,9 +179,6 @@ modifyImportedSignature f = stImports %= f
getSignature :: TCM Signature
getSignature = use stSignature
-getImportedSignature :: TCM Signature
-getImportedSignature = use stImports
-
-- | Update a possibly imported definition. Warning: changes made to imported
-- definitions (during type checking) will not persist outside the current
-- module. This function is currently used to update the compiled
@@ -190,9 +190,6 @@ modifyGlobalDefinition q f = modifySignature (updateDefinition q f) >>
setSignature :: Signature -> TCM ()
setSignature sig = modifySignature $ const sig
-setImportedSignature :: Signature -> TCM ()
-setImportedSignature sig = stImports .= sig
-
-- | Run some computation in a different signature, restore original signature.
withSignature :: Signature -> TCM a -> TCM a
withSignature sig m = do
@@ -203,14 +200,17 @@ withSignature sig m = do
return r
-- ** Modifiers for rewrite rules
-addRewriteRulesFor :: QName -> RewriteRules -> Signature -> Signature
-addRewriteRulesFor f rews =
+addRewriteRulesFor :: QName -> RewriteRules -> [QName] -> Signature -> Signature
+addRewriteRulesFor f rews matchables =
(over sigRewriteRules $ HMap.insertWith mappend f rews)
. (updateDefinition f $ updateTheDef setNotInjective)
+ . (foldr (.) id $ map (\g -> updateDefinition g setMatchable) matchables)
where
setNotInjective def@Function{} = def { funInv = NotInjective }
setNotInjective def = def
+ setMatchable def = def { defMatchable = True }
+
-- ** Modifiers for parts of the signature
lookupDefinition :: QName -> Signature -> Maybe Definition
@@ -241,6 +241,10 @@ updateFunClauses :: ([Clause] -> [Clause]) -> (Defn -> Defn)
updateFunClauses f def@Function{ funClauses = cs} = def { funClauses = f cs }
updateFunClauses f _ = __IMPOSSIBLE__
+updateCompiledClauses :: (Maybe CompiledClauses -> Maybe CompiledClauses) -> (Defn -> Defn)
+updateCompiledClauses f def@Function{ funCompiled = cc} = def { funCompiled = f cc }
+updateCompiledClauses f _ = __IMPOSSIBLE__
+
---------------------------------------------------------------------------
-- * Top level module
---------------------------------------------------------------------------
@@ -380,11 +384,12 @@ freshTCM m = do
---------------------------------------------------------------------------
-- | Look through the signature and reconstruct the instance table.
-addSignatureInstances :: Signature -> TCM ()
-addSignatureInstances sig = do
- let itable = Map.fromListWith (++)
- [ (c, [i]) | (i, Defn{ defInstance = Just c }) <- HMap.toList $ sig ^. sigDefinitions ]
- modifyInstanceDefs $ first $ Map.unionWith (++) itable
+addImportedInstances :: Signature -> TCM ()
+addImportedInstances sig = do
+ let itable = Map.fromListWith Set.union
+ [ (c, Set.singleton i)
+ | (i, Defn{ defInstance = Just c }) <- HMap.toList $ sig ^. sigDefinitions ]
+ stImportedInstanceDefs %= Map.unionWith Set.union itable
-- | Lens for 'stInstanceDefs'.
updateInstanceDefs :: (TempInstanceTable -> TempInstanceTable) -> (TCState -> TCState)
@@ -394,20 +399,24 @@ modifyInstanceDefs :: (TempInstanceTable -> TempInstanceTable) -> TCM ()
modifyInstanceDefs = modify . updateInstanceDefs
getAllInstanceDefs :: TCM TempInstanceTable
-getAllInstanceDefs = use stInstanceDefs
+getAllInstanceDefs = do
+ (table,xs) <- use stInstanceDefs
+ itable <- use stImportedInstanceDefs
+ let !table' = Map.unionWith Set.union itable table
+ return (table', xs)
-getAnonInstanceDefs :: TCM [QName]
+getAnonInstanceDefs :: TCM (Set QName)
getAnonInstanceDefs = snd <$> getAllInstanceDefs
-- | Remove all instances whose type is still unresolved.
clearAnonInstanceDefs :: TCM ()
-clearAnonInstanceDefs = modifyInstanceDefs $ mapSnd $ const []
+clearAnonInstanceDefs = modifyInstanceDefs $ mapSnd $ const Set.empty
-- | Add an instance whose type is still unresolved.
addUnknownInstance :: QName -> TCM ()
addUnknownInstance x = do
reportSLn "tc.decl.instance" 10 $ "adding definition " ++ show x ++ " to the instance table (the type is not yet known)"
- modifyInstanceDefs $ mapSnd (x:)
+ modifyInstanceDefs $ mapSnd $ Set.insert x
-- | Add instance to some ``class''.
addNamedInstance
@@ -419,4 +428,4 @@ addNamedInstance x n = do
-- Mark x as instance for n.
modifySignature $ updateDefinition x $ \ d -> d { defInstance = Just n }
-- Add x to n's instances.
- modifyInstanceDefs $ mapFst $ Map.insertWith (++) n [x]
+ modifyInstanceDefs $ mapFst $ Map.insertWith Set.union n $ Set.singleton x