summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/Monad/Local.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/Monad/Local.hs')
-rw-r--r--src/full/Agda/TypeChecking/Monad/Local.hs40
1 files changed, 40 insertions, 0 deletions
diff --git a/src/full/Agda/TypeChecking/Monad/Local.hs b/src/full/Agda/TypeChecking/Monad/Local.hs
new file mode 100644
index 0000000..b47b9ba
--- /dev/null
+++ b/src/full/Agda/TypeChecking/Monad/Local.hs
@@ -0,0 +1,40 @@
+{-# LANGUAGE CPP #-}
+module Agda.TypeChecking.Monad.Local where
+
+import Control.Applicative
+import Control.Monad
+import Data.Monoid
+
+import Agda.Syntax.Internal
+import Agda.TypeChecking.Substitute
+import Agda.TypeChecking.Monad.Base
+import Agda.TypeChecking.Monad.Context
+import Agda.TypeChecking.Monad.Env
+import Agda.TypeChecking.Monad.Options
+import Agda.TypeChecking.Free
+import {-# SOURCE #-} Agda.TypeChecking.Monad.Signature (inFreshModuleIfFreeParams, lookupSection)
+
+import Agda.Utils.Size
+import Agda.Utils.Impossible
+#include "undefined.h"
+
+-- | Precondition: must not be called if the module parameter of the current
+-- module have been refined or (touched at all).
+makeLocal :: Free' a All => a -> TCM (Local a)
+makeLocal x | closed x = return $ Global x
+ | otherwise = inFreshModuleIfFreeParams $ do
+ m <- currentModule
+ return (Local m x)
+
+makeGlobal :: Free' a All => a -> TCM (Local a)
+makeGlobal x | closed x = return $ Global x
+ | otherwise = __IMPOSSIBLE__
+
+getLocal :: Subst Term a => Local a -> TCM (Maybe a)
+getLocal (Global x) = return (Just x)
+getLocal l@(Local m x) = do
+ m' <- currentModule
+ if m' == m || isSubModuleOf m' m
+ then Just . (`applySubst` x) <$> getModuleParameterSub m
+ else return Nothing
+