summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/Serialise/Instances/Common.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/Serialise/Instances/Common.hs')
-rw-r--r--src/full/Agda/TypeChecking/Serialise/Instances/Common.hs60
1 files changed, 39 insertions, 21 deletions
diff --git a/src/full/Agda/TypeChecking/Serialise/Instances/Common.hs b/src/full/Agda/TypeChecking/Serialise/Instances/Common.hs
index 0922ce2..ae6c373 100644
--- a/src/full/Agda/TypeChecking/Serialise/Instances/Common.hs
+++ b/src/full/Agda/TypeChecking/Serialise/Instances/Common.hs
@@ -1,16 +1,10 @@
{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE ExistentialQuantification #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ScopedTypeVariables #-}
-#if __GLASGOW_HASKELL__ >= 710
-{-# LANGUAGE FlexibleContexts #-}
-#endif
-
#if __GLASGOW_HASKELL__ <= 708
-{-# LANGUAGE OverlappingInstances #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE OverlappingInstances #-}
#endif
{-# OPTIONS_GHC -fno-warn-orphans #-}
@@ -35,7 +29,9 @@ import Data.Set (Set)
import qualified Data.Set as Set
import Data.Sequence (Seq)
import qualified Data.Sequence as Seq
+#if __GLASGOW_HASKELL__ <= 708
import Data.Typeable (Typeable)
+#endif
import Data.Void
import Agda.Syntax.Common
@@ -236,7 +232,9 @@ instance EmbPrj Range where
-- | Ranges that should be serialised properly.
newtype SerialisedRange = SerialisedRange { underlyingRange :: Range }
+#if __GLASGOW_HASKELL__ <= 708
deriving (Typeable)
+#endif
instance EmbPrj SerialisedRange where
icod_ (SerialisedRange r) =
@@ -301,11 +299,11 @@ instance EmbPrj Agda.Syntax.Fixity.Fixity where
valu _ = malformed
instance EmbPrj Agda.Syntax.Fixity.Fixity' where
- icod_ (Fixity' a b) = icode2' a b
+ icod_ (Fixity' a b _) = icode2' a b -- discard theNameRange
value = vcase valu where
- valu [a,b] = valu2 Fixity' a b
- valu _ = malformed
+ valu [a, b] = valu2 (\ f n -> Fixity' f n noRange) a b
+ valu _ = malformed
instance EmbPrj GenPart where
icod_ (BindHole a) = icode1 0 a
@@ -370,11 +368,11 @@ instance EmbPrj a => EmbPrj (Ranged a) where
valu _ = malformed
instance EmbPrj ArgInfo where
- icod_ (ArgInfo h r) = icode2' h r
+ icod_ (ArgInfo h r o v) = icode4' h r o v
value = vcase valu where
- valu [h, r] = valu2 ArgInfo h r
- valu _ = malformed
+ valu [h, r, o, v] = valu4 ArgInfo h r o v
+ valu _ = malformed
instance EmbPrj NameId where
icod_ (NameId a b) = icode2' a b
@@ -443,14 +441,34 @@ instance EmbPrj Relevance where
value 5 = return UnusedArg
value _ = malformed
-instance EmbPrj ConPOrigin where
- icod_ ConPImplicit = return 0
- icod_ ConPCon = return 1
- icod_ ConPRec = return 2
+instance EmbPrj Origin where
+ icod_ UserWritten = return 0
+ icod_ Inserted = return 1
+ icod_ Reflected = return 2
+
+ value 0 = return UserWritten
+ value 1 = return Inserted
+ value 2 = return Reflected
+ value _ = malformed
+
+instance EmbPrj ConOrigin where
+ icod_ ConOSystem = return 0
+ icod_ ConOCon = return 1
+ icod_ ConORec = return 2
+
+ value 0 = return ConOSystem
+ value 1 = return ConOCon
+ value 2 = return ConORec
+ value _ = malformed
+
+instance EmbPrj ProjOrigin where
+ icod_ ProjPrefix = return 0
+ icod_ ProjPostfix = return 1
+ icod_ ProjSystem = return 2
- value 0 = return ConPImplicit
- value 1 = return ConPCon
- value 2 = return ConPRec
+ value 0 = return ProjPrefix
+ value 1 = return ProjPostfix
+ value 2 = return ProjSystem
value _ = malformed
instance EmbPrj Agda.Syntax.Literal.Literal where