summaryrefslogtreecommitdiff
path: root/src/full/Agda/Syntax/Internal
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Syntax/Internal')
-rw-r--r--src/full/Agda/Syntax/Internal/Defs.hs8
-rw-r--r--src/full/Agda/Syntax/Internal/Generic.hs11
-rw-r--r--src/full/Agda/Syntax/Internal/Pattern.hs30
3 files changed, 30 insertions, 19 deletions
diff --git a/src/full/Agda/Syntax/Internal/Defs.hs b/src/full/Agda/Syntax/Internal/Defs.hs
index dd4fc38..a79b7be 100644
--- a/src/full/Agda/Syntax/Internal/Defs.hs
+++ b/src/full/Agda/Syntax/Internal/Defs.hs
@@ -1,6 +1,5 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleInstances #-}
-- | Extract used definitions from terms.
module Agda.Syntax.Internal.Defs where
@@ -82,6 +81,7 @@ instance GetDefs Sort where
Type l -> getDefs l
Prop -> return ()
Inf -> return ()
+ SizeUniv -> return ()
DLub s s' -> getDefs s >> getDefs s'
instance GetDefs Level where
@@ -95,7 +95,7 @@ instance GetDefs LevelAtom where
getDefs a = case a of
MetaLevel x vs -> getDefs x >> getDefs vs
BlockedLevel _ v -> getDefs v
- NeutralLevel v -> getDefs v
+ NeutralLevel _ v -> getDefs v
UnreducedLevel v -> getDefs v
-- collection instances
diff --git a/src/full/Agda/Syntax/Internal/Generic.hs b/src/full/Agda/Syntax/Internal/Generic.hs
index 9da57c2..d0e9552 100644
--- a/src/full/Agda/Syntax/Internal/Generic.hs
+++ b/src/full/Agda/Syntax/Internal/Generic.hs
@@ -1,6 +1,5 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleInstances #-}
module Agda.Syntax.Internal.Generic where
@@ -160,17 +159,17 @@ instance TermLike PlusLevel where
instance TermLike LevelAtom where
traverseTerm f l = case l of
MetaLevel m vs -> MetaLevel m $ traverseTerm f vs
- NeutralLevel v -> NeutralLevel $ traverseTerm f v
+ NeutralLevel r v -> NeutralLevel r $ traverseTerm f v
BlockedLevel m v -> BlockedLevel m $ traverseTerm f v
UnreducedLevel v -> UnreducedLevel $ traverseTerm f v
traverseTermM f l = case l of
MetaLevel m vs -> MetaLevel m <$> traverseTermM f vs
- NeutralLevel v -> NeutralLevel <$> traverseTermM f v
+ NeutralLevel r v -> NeutralLevel r <$> traverseTermM f v
BlockedLevel m v -> BlockedLevel m <$> traverseTermM f v
UnreducedLevel v -> UnreducedLevel <$> traverseTermM f v
foldTerm f l = case l of
MetaLevel m vs -> foldTerm f vs
- NeutralLevel v -> foldTerm f v
+ NeutralLevel _ v -> foldTerm f v
BlockedLevel _ v -> foldTerm f v
UnreducedLevel v -> foldTerm f v
diff --git a/src/full/Agda/Syntax/Internal/Pattern.hs b/src/full/Agda/Syntax/Internal/Pattern.hs
index 7f9ca74..78da0c4 100644
--- a/src/full/Agda/Syntax/Internal/Pattern.hs
+++ b/src/full/Agda/Syntax/Internal/Pattern.hs
@@ -1,12 +1,14 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE OverlappingInstances #-}
-{-# LANGUAGE TupleSections #-}
-{-# LANGUAGE TypeSynonymInstances #-}
-{-# LANGUAGE UndecidableInstances #-} -- because of func. deps.
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE UndecidableInstances #-} -- because of func. deps.
+
+#if __GLASGOW_HASKELL__ <= 708
+{-# LANGUAGE OverlappingInstances #-}
+#endif
module Agda.Syntax.Internal.Pattern where
@@ -49,7 +51,12 @@ class FunArity a where
funArity :: a -> Int
-- | Get the number of initial 'Apply' patterns.
+
+#if __GLASGOW_HASKELL__ >= 710
+instance {-# OVERLAPPABLE #-} IsProjP p => FunArity [p] where
+#else
instance IsProjP p => FunArity [p] where
+#endif
funArity = length . takeWhile (isNothing . isProjP)
-- | Get the number of initial 'Apply' patterns in a clause.
@@ -57,7 +64,11 @@ instance FunArity Clause where
funArity = funArity . clausePats
-- | Get the number of common initial 'Apply' patterns in a list of clauses.
+#if __GLASGOW_HASKELL__ >= 710
+instance {-# OVERLAPPING #-} FunArity [Clause] where
+#else
instance FunArity [Clause] where
+#endif
funArity [] = 0
funArity cls = minimum $ map funArity cls
@@ -90,7 +101,8 @@ instance LabelPatVars (Pattern' x) (Pattern' (i,x)) i where
where next = do (x:xs) <- get; put xs; return x
-- | Augment pattern variables with their de Bruijn index.
-{-# SPECIALIZE numberPatVars :: Permutation -> [NamedArg (Pattern' x)] -> [(NamedArg (Pattern' (Int, x)))] #-}
+{-# SPECIALIZE numberPatVars :: Permutation -> [NamedArg (Pattern' x)] -> [NamedArg (Pattern' (Int, x))] #-}
+{-# SPECIALIZE numberPatVars :: Permutation -> [NamedArg Pattern] -> [NamedArg DeBruijnPattern] #-}
numberPatVars :: LabelPatVars a b Int => Permutation -> a -> b
numberPatVars perm ps = evalState (labelPatVars ps) $
permute (invertP __IMPOSSIBLE__ perm) $ downFrom $ size perm