{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Agda.TypeChecking.Serialise.Instances.Common (SerialisedRange(..)) where
import Prelude hiding (mapM)
import Control.Monad.Reader hiding (mapM)
import Control.Monad.State.Strict (gets, modify)
import Control.Exception
import Data.Array.IArray
import Data.Word
import qualified Data.ByteString.Lazy as L
import qualified Data.Foldable as Fold
import Data.Hashable
import qualified Data.HashTable.IO as H
import Data.Int (Int32)
import Data.Maybe
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.IntSet as IntSet
import Data.IntSet (IntSet)
import qualified Data.Set as Set
import Data.Sequence (Seq)
import qualified Data.Sequence as Seq
import Data.Traversable ( mapM )
import Data.Void
import Agda.Syntax.Common
import Agda.Syntax.Concrete.Name as C
import qualified Agda.Syntax.Concrete as C
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Position as P
import Agda.Syntax.Fixity
import Agda.Syntax.Notation
import Agda.Syntax.Literal
import Agda.Interaction.FindFile
import Agda.TypeChecking.Serialise.Base
import Agda.Utils.BiMap (BiMap)
import qualified Agda.Utils.BiMap as BiMap
import Agda.Utils.HashMap (HashMap)
import qualified Agda.Utils.HashMap as HMap
import Agda.Utils.FileName
import Agda.Utils.Maybe
import Agda.Utils.NonemptyList
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Trie (Trie(..))
import qualified Agda.Utils.Trie as Trie
import Agda.Utils.Except
import Agda.Utils.Empty (Empty)
import qualified Agda.Utils.Empty as Empty
#include "undefined.h"
import Agda.Utils.Impossible
instance {-# OVERLAPPING #-} EmbPrj String where
icod_ = icodeString
value i = (! i) `fmap` gets stringE
instance EmbPrj L.ByteString where
icod_ = icodeX bstringD bstringC
value i = (! i) `fmap` gets bstringE
instance EmbPrj Integer where
icod_ = icodeInteger
value i = (! i) `fmap` gets integerE
instance EmbPrj Word64 where
icod_ i = icodeN' (undefined :: Int32 -> Int32 -> Int32) (int32 q) (int32 r)
where (q, r) = quotRem i (2^32)
int32 :: Word64 -> Int32
int32 = fromIntegral
value = vcase valu where
valu [a, b] = return $ n * mod (fromIntegral a) n + mod (fromIntegral b) n
valu _ = malformed
n = 2^32
instance EmbPrj Int32 where
icod_ i = return i
value i = return i
instance EmbPrj Int where
icod_ i = return (fromIntegral i)
value i = return (fromIntegral i)
instance EmbPrj Char where
icod_ c = return (fromIntegral $ fromEnum c)
value i = return (toEnum $ fromInteger $ toInteger i)
instance EmbPrj Double where
icod_ = icodeDouble
value i = (! i) `fmap` gets doubleE
instance EmbPrj Void where
icod_ = absurd
value = vcase valu where valu _ = malformed
instance EmbPrj () where
icod_ () = icodeN' ()
value = vcase valu where
valu [] = valuN ()
valu _ = malformed
instance (EmbPrj a, EmbPrj b) => EmbPrj (a, b) where
icod_ (a, b) = icodeN' (,) a b
value = valueN (,)
instance (EmbPrj a, EmbPrj b, EmbPrj c) => EmbPrj (a, b, c) where
icod_ (a, b, c) = icodeN' (,,) a b c
value = valueN (,,)
instance (EmbPrj a, EmbPrj b) => EmbPrj (Either a b) where
icod_ (Left x) = icodeN 0 Left x
icod_ (Right x) = icodeN 1 Right x
value = vcase valu where
valu [0, x] = valuN Left x
valu [1, x] = valuN Right x
valu _ = malformed
instance EmbPrj a => EmbPrj (Maybe a) where
icod_ Nothing = icodeN' Nothing
icod_ (Just x) = icodeN' Just x
value = vcase valu where
valu [] = valuN Nothing
valu [x] = valuN Just x
valu _ = malformed
instance EmbPrj a => EmbPrj (Strict.Maybe a) where
icod_ m = icode (Strict.toLazy m)
value m = Strict.toStrict `fmap` value m
instance EmbPrj Bool where
icod_ True = icodeN' True
icod_ False = icodeN 0 False
value = vcase valu where
valu [] = valuN True
valu [0] = valuN False
valu _ = malformed
instance EmbPrj DataOrRecord where
icod_ IsData = icodeN' IsData
icod_ IsRecord = icodeN 0 IsRecord
value = vcase $ \case
[] -> valuN IsData
[0] -> valuN IsRecord
_ -> malformed
instance EmbPrj AbsolutePath where
icod_ file = do
d <- asks absPathD
liftIO $ flip fromMaybeM (H.lookup d file) $ do
putStrLn $ unlines $
[ "Panic while serializing absolute path: " ++ show file
, "The path could not be found in the dictionary:"
]
putStrLn . show =<< H.toList d
__IMPOSSIBLE__
value m = do
m :: TopLevelModuleName
<- value m
mf <- gets modFile
incs <- gets includes
(r, mf) <- liftIO $ findFile'' incs m mf
modify $ \s -> s { modFile = mf }
case r of
Left err -> throwError $ findErrorToTypeError m err
Right f -> return f
instance EmbPrj a => EmbPrj (Position' a) where
icod_ (P.Pn file pos line col) = icodeN' P.Pn file pos line col
value = valueN P.Pn
instance EmbPrj TopLevelModuleName where
icod_ (TopLevelModuleName a b) = icodeN' TopLevelModuleName a b
value = valueN TopLevelModuleName
instance {-# OVERLAPPABLE #-} EmbPrj a => EmbPrj [a] where
icod_ xs = icodeNode =<< mapM icode xs
value = vcase (mapM value)
instance EmbPrj a => EmbPrj (NonemptyList a) where
icod_ = icod_ . toList
value = listCaseNe malformed return <=< value
instance (Ord a, Ord b, EmbPrj a, EmbPrj b) => EmbPrj (BiMap a b) where
icod_ m = icode (BiMap.toList m)
value m = BiMap.fromList <$> value m
instance (Ord a, EmbPrj a, EmbPrj b) => EmbPrj (Map a b) where
icod_ m = icode (Map.toList m)
value m = Map.fromList `fmap` value m
instance (Ord a, EmbPrj a) => EmbPrj (Set a) where
icod_ s = icode (Set.toList s)
value s = Set.fromList `fmap` value s
instance EmbPrj IntSet where
icod_ s = icode (IntSet.toList s)
value s = IntSet.fromList <$> value s
instance (Ord a, EmbPrj a, EmbPrj b) => EmbPrj (Trie a b) where
icod_ (Trie a b)= icodeN' Trie a b
value = valueN Trie
instance EmbPrj a => EmbPrj (Seq a) where
icod_ s = icode (Fold.toList s)
value s = Seq.fromList `fmap` value s
instance EmbPrj a => EmbPrj (P.Interval' a) where
icod_ (P.Interval p q) = icodeN' P.Interval p q
value = valueN P.Interval
instance EmbPrj Range where
icod_ _ = icodeN' ()
value _ = return noRange
newtype SerialisedRange = SerialisedRange { underlyingRange :: Range }
instance EmbPrj SerialisedRange where
icod_ (SerialisedRange r) =
icodeN' (undefined :: SrcFile -> [IntervalWithoutFile] -> SerialisedRange)
(P.rangeFile r) (P.rangeIntervals r)
value = vcase valu where
valu [a, b] = SerialisedRange <$> valuN P.intervalsToRange a b
valu _ = malformed
instance EmbPrj C.Name where
icod_ (C.NoName a b) = icodeN 0 C.NoName a b
icod_ (C.Name r xs) = icodeN' C.Name r xs
value = vcase valu where
valu [0, a, b] = valuN C.NoName a b
valu [r, xs] = valuN C.Name r xs
valu _ = malformed
instance EmbPrj NamePart where
icod_ Hole = icodeN' Hole
icod_ (Id a) = icodeN' Id a
value = vcase valu where
valu [] = valuN Hole
valu [a] = valuN Id a
valu _ = malformed
instance EmbPrj C.QName where
icod_ (Qual a b) = icodeN' Qual a b
icod_ (C.QName a ) = icodeN' C.QName a
value = vcase valu where
valu [a, b] = valuN Qual a b
valu [a] = valuN C.QName a
valu _ = malformed
instance EmbPrj Agda.Syntax.Fixity.Associativity where
icod_ LeftAssoc = icodeN' LeftAssoc
icod_ RightAssoc = icodeN 1 RightAssoc
icod_ NonAssoc = icodeN 2 NonAssoc
value = vcase valu where
valu [] = valuN LeftAssoc
valu [1] = valuN RightAssoc
valu [2] = valuN NonAssoc
valu _ = malformed
instance EmbPrj Agda.Syntax.Fixity.PrecedenceLevel where
icod_ Unrelated = icodeN' Unrelated
icod_ (Related a) = icodeN' Related a
value = vcase valu where
valu [] = valuN Unrelated
valu [a] = valuN Related a
valu _ = malformed
instance EmbPrj Agda.Syntax.Fixity.Fixity where
icod_ (Fixity a b c) = icodeN' Fixity a b c
value = valueN Fixity
instance EmbPrj Agda.Syntax.Fixity.Fixity' where
icod_ (Fixity' a b r) = icodeN' (\ a b -> Fixity' a b r) a b
value = valueN (\ f n -> Fixity' f n noRange)
instance EmbPrj GenPart where
icod_ (BindHole a) = icodeN 0 BindHole a
icod_ (NormalHole a) = icodeN 1 NormalHole a
icod_ (WildHole a) = icodeN 2 WildHole a
icod_ (IdPart a) = icodeN' IdPart a
value = vcase valu where
valu [0, a] = valuN BindHole a
valu [1, a] = valuN NormalHole a
valu [2, a] = valuN WildHole a
valu [a] = valuN IdPart a
valu _ = malformed
instance EmbPrj MetaId where
icod_ (MetaId n) = icod_ n
value i = MetaId <$> value i
instance EmbPrj A.QName where
icod_ n@(A.QName a b) = icodeMemo qnameD qnameC (qnameId n) $ icodeN' A.QName a b
value = valueN A.QName
instance EmbPrj A.AmbiguousQName where
icod_ (A.AmbQ a) = icode a
value n = A.AmbQ `fmap` value n
instance EmbPrj A.ModuleName where
icod_ (A.MName a) = icode a
value n = A.MName `fmap` value n
instance EmbPrj A.Name where
icod_ (A.Name a b c d) = icodeMemo nameD nameC a $
icodeN' (\ a b -> A.Name a b . underlyingRange) a b (SerialisedRange c) d
value = valueN (\a b c -> A.Name a b (underlyingRange c))
instance EmbPrj a => EmbPrj (C.FieldAssignment' a) where
icod_ (C.FieldAssignment a b) = icodeN' C.FieldAssignment a b
value = valueN C.FieldAssignment
instance (EmbPrj s, EmbPrj t) => EmbPrj (Named s t) where
icod_ (Named a b) = icodeN' Named a b
value = valueN Named
instance EmbPrj a => EmbPrj (Ranged a) where
icod_ (Ranged r x) = icodeN' Ranged r x
value = valueN Ranged
instance EmbPrj ArgInfo where
icod_ (ArgInfo h r o fv) = icodeN' ArgInfo h r o fv
value = valueN ArgInfo
instance EmbPrj NameId where
icod_ (NameId a b) = icodeN' NameId a b
value = valueN NameId
instance (Eq k, Hashable k, EmbPrj k, EmbPrj v) => EmbPrj (HashMap k v) where
icod_ m = icode (HMap.toList m)
value m = HMap.fromList `fmap` value m
instance EmbPrj a => EmbPrj (WithHiding a) where
icod_ (WithHiding a b) = icodeN' WithHiding a b
value = valueN WithHiding
instance EmbPrj a => EmbPrj (Arg a) where
icod_ (Arg i e) = icodeN' Arg i e
value = valueN Arg
instance EmbPrj a => EmbPrj (Dom a) where
icod_ (Dom i e) = icodeN' Dom i e
value = valueN Dom
instance EmbPrj HasEta where
icod_ YesEta = icodeN' YesEta
icod_ NoEta = icodeN 1 NoEta
value = vcase valu where
valu [] = valuN YesEta
valu [1] = valuN NoEta
valu _ = malformed
instance EmbPrj Induction where
icod_ Inductive = icodeN' Inductive
icod_ CoInductive = icodeN 1 CoInductive
value = vcase valu where
valu [] = valuN Inductive
valu [1] = valuN CoInductive
valu _ = malformed
instance EmbPrj Hiding where
icod_ Hidden = return 0
icod_ NotHidden = return 1
icod_ (Instance NoOverlap) = return 2
icod_ (Instance YesOverlap) = return 3
value 0 = return Hidden
value 1 = return NotHidden
value 2 = return (Instance NoOverlap)
value 3 = return (Instance YesOverlap)
value _ = malformed
instance EmbPrj Quantity where
icod_ Quantity0 = return 0
icod_ Quantityω = return 1
value 0 = return Quantity0
value 1 = return Quantityω
value _ = malformed
instance EmbPrj Modality where
icod_ (Modality a b) = icodeN' Modality a b
value = vcase $ \case
[a, b] -> valuN Modality a b
_ -> malformed
instance EmbPrj Relevance where
icod_ Relevant = return 0
icod_ Irrelevant = return 1
icod_ NonStrict = return 2
value 0 = return Relevant
value 1 = return Irrelevant
value 2 = return NonStrict
value _ = malformed
instance EmbPrj Origin where
icod_ UserWritten = return 0
icod_ Inserted = return 1
icod_ Reflected = return 2
icod_ CaseSplit = return 3
value 0 = return UserWritten
value 1 = return Inserted
value 2 = return Reflected
value 3 = return CaseSplit
value _ = malformed
instance EmbPrj FreeVariables where
icod_ UnknownFVs = icodeN' UnknownFVs
icod_ (KnownFVs a) = icodeN' KnownFVs a
value = vcase valu where
valu [] = valuN UnknownFVs
valu [a] = valuN KnownFVs a
valu _ = malformed
instance EmbPrj ConOrigin where
icod_ ConOSystem = return 0
icod_ ConOCon = return 1
icod_ ConORec = return 2
icod_ ConOSplit = return 3
value 0 = return ConOSystem
value 1 = return ConOCon
value 2 = return ConORec
value 3 = return ConOSplit
value _ = malformed
instance EmbPrj ProjOrigin where
icod_ ProjPrefix = return 0
icod_ ProjPostfix = return 1
icod_ ProjSystem = return 2
value 0 = return ProjPrefix
value 1 = return ProjPostfix
value 2 = return ProjSystem
value _ = malformed
instance EmbPrj Agda.Syntax.Literal.Literal where
icod_ (LitNat a b) = icodeN' LitNat a b
icod_ (LitFloat a b) = icodeN 1 LitFloat a b
icod_ (LitString a b) = icodeN 2 LitString a b
icod_ (LitChar a b) = icodeN 3 LitChar a b
icod_ (LitQName a b) = icodeN 5 LitQName a b
icod_ (LitMeta a b c) = icodeN 6 LitMeta a b c
icod_ (LitWord64 a b) = icodeN 7 LitWord64 a b
value = vcase valu where
valu [a, b] = valuN LitNat a b
valu [1, a, b] = valuN LitFloat a b
valu [2, a, b] = valuN LitString a b
valu [3, a, b] = valuN LitChar a b
valu [5, a, b] = valuN LitQName a b
valu [6, a, b, c] = valuN LitMeta a b c
valu [7, a, b] = valuN LitWord64 a b
valu _ = malformed
instance EmbPrj IsAbstract where
icod_ AbstractDef = icodeN 0 AbstractDef
icod_ ConcreteDef = icodeN' ConcreteDef
value = vcase valu where
valu [0] = valuN AbstractDef
valu [] = valuN ConcreteDef
valu _ = malformed
instance EmbPrj Delayed where
icod_ Delayed = icodeN 0 Delayed
icod_ NotDelayed = icodeN' NotDelayed
value = vcase valu where
valu [0] = valuN Delayed
valu [] = valuN NotDelayed
valu _ = malformed
instance EmbPrj Impossible where
icod_ (Impossible a b) = icodeN 0 Impossible a b
icod_ (Unreachable a b) = icodeN 1 Unreachable a b
value = vcase valu where
valu [0, a, b] = valuN Impossible a b
valu [1, a, b] = valuN Unreachable a b
valu _ = malformed
instance EmbPrj Empty where
icod_ a = icod_ =<< lift (Empty.toImpossible a)
value = fmap throwImpossible . value