summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/Serialise.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/Serialise.hs')
-rw-r--r--src/full/Agda/TypeChecking/Serialise.hs185
1 files changed, 115 insertions, 70 deletions
diff --git a/src/full/Agda/TypeChecking/Serialise.hs b/src/full/Agda/TypeChecking/Serialise.hs
index ed6cd48..b9300be 100644
--- a/src/full/Agda/TypeChecking/Serialise.hs
+++ b/src/full/Agda/TypeChecking/Serialise.hs
@@ -1,9 +1,15 @@
-{-# LANGUAGE CPP #-}
+{-# LANGUAGE CPP #-}
{-# LANGUAGE ExistentialQuantification #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE OverlappingInstances #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+#if __GLASGOW_HASKELL__ >= 710
+{-# LANGUAGE FlexibleContexts #-}
+#endif
+
+#if __GLASGOW_HASKELL__ <= 708
+{-# LANGUAGE OverlappingInstances #-}
+#endif
-- Andreas, Makoto, Francesco 2014-10-15 AIM XX:
-- -O2 does not have any noticable effect on runtime
@@ -48,7 +54,7 @@ import qualified Data.Binary.Get as B
import qualified Data.Binary.Put as B
import qualified Data.List as List
import Data.Function
-import Data.Typeable
+import Data.Typeable ( cast, Typeable, typeOf, TypeRep )
import qualified Codec.Compression.GZip as G
import qualified Agda.Compiler.Epic.Interface as Epic
@@ -70,7 +76,6 @@ import qualified Agda.Interaction.Highlighting.Precise as HP
import Agda.Interaction.FindFile
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
-import Agda.TypeChecking.Monad.Benchmark (billSub, billTo)
import Agda.TypeChecking.Monad
import Agda.TypeChecking.CompiledClause
@@ -110,7 +115,7 @@ returnForcedByteString bs = return $! bs
-- 32-bit machines). Word64 does not have these problems.
currentInterfaceVersion :: Word64
-currentInterfaceVersion = 20141018 * 10 + 0
+currentInterfaceVersion = 20150511 * 10 + 0
-- | Constructor tag (maybe omitted) and argument indices.
@@ -269,19 +274,19 @@ encode a = do
liftIO $ H.toList stats
modifyStatistics $ Map.union stats
-- Encode hashmaps and root, and compress.
- bits1 <- billSub [ Bench.Serialization, Bench.BinaryEncode ] $
+ bits1 <- Bench.billTo [ Bench.Serialization, Bench.BinaryEncode ] $
returnForcedByteString $ B.encode (root, nL, sL, iL, dL)
let compressParams = G.defaultCompressParams
{ G.compressLevel = G.bestSpeed
, G.compressStrategy = G.huffmanOnlyStrategy
}
- cbits <- billSub [ Bench.Serialization, Bench.Compress ] $
+ cbits <- Bench.billTo [ Bench.Serialization, Bench.Compress ] $
returnForcedByteString $ G.compressWith compressParams bits1
let x = B.encode currentInterfaceVersion `L.append` cbits
return x
where
l h = List.map fst . List.sortBy (compare `on` snd) <$> H.toList h
- benchSort = billTo [Bench.Serialization, Bench.Sort] . liftIO
+ benchSort = Bench.billTo [Bench.Serialization, Bench.Sort] . liftIO
statistics :: String -> IORef FreshAndReuse -> TCM ()
statistics kind ioref = do
FreshAndReuse fresh reused <- liftIO $ readIORef ioref
@@ -402,7 +407,11 @@ decodeHashes s
decodeFile :: FilePath -> TCM (Maybe Interface)
decodeFile f = decodeInterface =<< liftIO (L.readFile f)
+#if __GLASGOW_HASKELL__ >= 710
+instance {-# OVERLAPPING #-} EmbPrj String where
+#else
instance EmbPrj String where
+#endif
icod_ = icodeString
value i = (! i) `fmap` gets stringE
@@ -493,9 +502,13 @@ instance EmbPrj TopLevelModuleName where
value = vcase valu where valu [a] = valu1 TopLevelModuleName a
valu _ = malformed
+#if __GLASGOW_HASKELL__ >= 710
+instance {-# OVERLAPPABLE #-} EmbPrj a => EmbPrj [a] where
+#else
instance EmbPrj a => EmbPrj [a] where
+#endif
icod_ xs = icodeN =<< mapM icode xs
- value = vcase (mapM value)
+ value = vcase (mapM value)
-- icode [] = icode0'
-- icode (x : xs) = icode2' x xs
-- value = vcase valu where valu [] = valu0 []
@@ -612,13 +625,18 @@ instance EmbPrj KindOfName where
valu [4] = valu0 QuotableName
valu _ = malformed
+instance EmbPrj Agda.Syntax.Fixity.Associativity where
+ icod_ LeftAssoc = icode0'
+ icod_ RightAssoc = icode0 1
+ icod_ NonAssoc = icode0 2
+ value = vcase valu where valu [] = valu0 LeftAssoc
+ valu [1] = valu0 RightAssoc
+ valu [2] = valu0 NonAssoc
+ valu _ = malformed
+
instance EmbPrj Agda.Syntax.Fixity.Fixity where
- icod_ (LeftAssoc a b) = icode2 0 a b
- icod_ (RightAssoc a b) = icode2 1 a b
- icod_ (NonAssoc a b) = icode2' a b
- value = vcase valu where valu [0, a, b] = valu2 LeftAssoc a b
- valu [1, a, b] = valu2 RightAssoc a b
- valu [a, b] = valu2 NonAssoc a b
+ icod_ (Fixity a b c) = icode3' a b c
+ value = vcase valu where valu [a, b, c] = valu3 Fixity a b c
valu _ = malformed
instance EmbPrj Agda.Syntax.Fixity.Fixity' where
@@ -846,6 +864,11 @@ instance EmbPrj a => EmbPrj (Elim' a) where
valu [0, a] = valu1 Proj a
valu _ = malformed
+instance EmbPrj a => EmbPrj (WithHiding a) where
+ icod_ (WithHiding a b) = icode2' a b
+ value = vcase valu where valu [a, b] = valu2 WithHiding a b
+ valu _ = malformed
+
instance (EmbPrj a, EmbPrj c) => EmbPrj (Agda.Syntax.Common.Arg c a) where
icod_ (Arg i e) = icode2' i e
value = vcase valu where valu [i, e] = valu2 Arg i e
@@ -875,12 +898,14 @@ instance EmbPrj Agda.Syntax.Common.Hiding where
instance EmbPrj Agda.Syntax.Common.Relevance where
icod_ Relevant = icode0'
icod_ Irrelevant = icode0 1
- icod_ Forced = icode0 2
+ icod_ (Forced Small) = icode0 2
+ icod_ (Forced Big) = icode0 5
icod_ NonStrict = icode0 3
icod_ UnusedArg = icode0 4
value = vcase valu where valu [] = valu0 Relevant
valu [1] = valu0 Irrelevant
- valu [2] = valu0 Forced
+ valu [2] = valu0 (Forced Small)
+ valu [5] = valu0 (Forced Big)
valu [3] = valu0 NonStrict
valu [4] = valu0 UnusedArg
valu _ = malformed
@@ -955,21 +980,26 @@ instance EmbPrj PlusLevel where
valu _ = malformed
instance EmbPrj LevelAtom where
- icod_ (NeutralLevel a) = icode1' a
+ icod_ (NeutralLevel _ a) = icode1' a
icod_ (UnreducedLevel a) = icode1 1 a
icod_ MetaLevel{} = __IMPOSSIBLE__
icod_ BlockedLevel{} = __IMPOSSIBLE__
- value = vcase valu where valu [a] = valu1 NeutralLevel a
- valu [1, a] = valu1 UnreducedLevel a
- valu _ = malformed
+ value = vcase valu where
+ valu [a] = valu1 UnreducedLevel a -- we forget that we are a NeutralLevel,
+ -- since we do not want do (de)serialize
+ -- the reason for neutrality
+ valu [1, a] = valu1 UnreducedLevel a
+ valu _ = malformed
instance EmbPrj I.Sort where
icod_ (Type a ) = icode1' a
icod_ Prop = icode1 1 ()
+ icod_ SizeUniv = icode1 3 ()
icod_ Inf = icode1 4 ()
icod_ (DLub a b) = __IMPOSSIBLE__
value = vcase valu where valu [a] = valu1 Type a
valu [1, _] = valu0 Prop
+ valu [3, _] = valu0 SizeUniv
valu [4, _] = valu0 Inf
valu _ = malformed
@@ -1022,6 +1052,17 @@ instance EmbPrj Definition where
value = vcase valu where valu [rel, a, b, c, d, e, f, g, h, i, j] = valu11 Defn rel a b c d e f g h i j
valu _ = malformed
+instance EmbPrj NLPat where
+ icod_ (PVar a) = icode1 0 a
+ icod_ (PWild) = icode0 1
+ icod_ (PDef a b) = icode2 2 a b
+ icod_ (PTerm a) = icode1 3 a
+ value = vcase valu where valu [0, a] = valu1 PVar a
+ valu [1] = valu0 PWild
+ valu [2, a, b] = valu2 PDef a b
+ valu [3, a] = valu1 PTerm a
+ valu _ = malformed
+
instance EmbPrj RewriteRule where
icod_ (RewriteRule a b c d e) = icode5' a b c d e
value = vcase valu where valu [a, b, c, d, e] = valu5 RewriteRule a b c d e
@@ -1215,6 +1256,11 @@ instance EmbPrj Delayed where
valu [] = valu0 NotDelayed
valu _ = malformed
+instance EmbPrj I.ConPatternInfo where
+ icod_ (ConPatternInfo a b) = icode2' a b
+ value = vcase valu where valu [a, b] = valu2 ConPatternInfo a b
+ valu _ = malformed
+
instance EmbPrj I.Pattern where
icod_ (VarP a ) = icode1' a
icod_ (ConP a b c) = icode3' a b c
@@ -1329,7 +1375,6 @@ instance EmbPrj Precedence where
valu [8] = valu0 WithArgCtx
valu [9] = valu0 DotPatternCtx
valu _ = malformed
-
instance EmbPrj ScopeInfo where
icod_ (ScopeInfo a b c d) = icode4' a b c d
value = vcase valu where valu [a, b, c, d] = valu4 ScopeInfo a b c d
@@ -1414,15 +1459,15 @@ icodeX dict counter key = do
d <- asks dict
c <- asks counter
liftIO $ do
- mi <- H.lookup d key
- case mi of
- Just i -> do
- modifyIORef' c $ over lensReuse (+1)
- return i
- Nothing -> do
- fresh <- (^.lensFresh) <$> do readModifyIORef' c $ over lensFresh (+1)
- H.insert d key fresh
- return fresh
+ mi <- H.lookup d key
+ case mi of
+ Just i -> do
+ modifyIORef' c $ over lensReuse (+1)
+ return i
+ Nothing -> do
+ fresh <- (^.lensFresh) <$> do readModifyIORef' c $ over lensFresh (+1)
+ H.insert d key fresh
+ return fresh
-- Instead of inlining icodeX, we manually specialize it to
-- its four uses: Integer, String, Double, Node.
@@ -1433,60 +1478,60 @@ icodeInteger key = do
d <- asks integerD
c <- asks integerC
liftIO $ do
- mi <- H.lookup d key
- case mi of
- Just i -> do
- modifyIORef' c $ over lensReuse (+1)
- return i
- Nothing -> do
- fresh <- (^.lensFresh) <$> do readModifyIORef' c $ over lensFresh (+1)
- H.insert d key fresh
- return fresh
+ mi <- H.lookup d key
+ case mi of
+ Just i -> do
+ modifyIORef' c $ over lensReuse (+1)
+ return i
+ Nothing -> do
+ fresh <- (^.lensFresh) <$> do readModifyIORef' c $ over lensFresh (+1)
+ H.insert d key fresh
+ return fresh
icodeDouble :: Double -> S Int32
icodeDouble key = do
d <- asks doubleD
c <- asks doubleC
liftIO $ do
- mi <- H.lookup d key
- case mi of
- Just i -> do
- modifyIORef' c $ over lensReuse (+1)
- return i
- Nothing -> do
- fresh <- (^.lensFresh) <$> do readModifyIORef' c $ over lensFresh (+1)
- H.insert d key fresh
- return fresh
+ mi <- H.lookup d key
+ case mi of
+ Just i -> do
+ modifyIORef' c $ over lensReuse (+1)
+ return i
+ Nothing -> do
+ fresh <- (^.lensFresh) <$> do readModifyIORef' c $ over lensFresh (+1)
+ H.insert d key fresh
+ return fresh
icodeString :: String -> S Int32
icodeString key = do
d <- asks stringD
c <- asks stringC
liftIO $ do
- mi <- H.lookup d key
- case mi of
- Just i -> do
- modifyIORef' c $ over lensReuse (+1)
- return i
- Nothing -> do
- fresh <- (^.lensFresh) <$> do readModifyIORef' c $ over lensFresh (+1)
- H.insert d key fresh
- return fresh
+ mi <- H.lookup d key
+ case mi of
+ Just i -> do
+ modifyIORef' c $ over lensReuse (+1)
+ return i
+ Nothing -> do
+ fresh <- (^.lensFresh) <$> do readModifyIORef' c $ over lensFresh (+1)
+ H.insert d key fresh
+ return fresh
icodeN :: Node -> S Int32
icodeN key = do
d <- asks nodeD
c <- asks nodeC
liftIO $ do
- mi <- H.lookup d key
- case mi of
- Just i -> do
- modifyIORef' c $ over lensReuse (+1)
- return i
- Nothing -> do
- fresh <- (^.lensFresh) <$> do readModifyIORef' c $ over lensFresh (+1)
- H.insert d key fresh
- return fresh
+ mi <- H.lookup d key
+ case mi of
+ Just i -> do
+ modifyIORef' c $ over lensReuse (+1)
+ return i
+ Nothing -> do
+ fresh <- (^.lensFresh) <$> do readModifyIORef' c $ over lensFresh (+1)
+ H.insert d key fresh
+ return fresh
-- icodeN :: [Int32] -> S Int32
-- icodeN = icodeX nodeD nodeC