summaryrefslogtreecommitdiff
path: root/src/full/Agda/Syntax/Common.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Syntax/Common.hs')
-rw-r--r--src/full/Agda/Syntax/Common.hs128
1 files changed, 98 insertions, 30 deletions
diff --git a/src/full/Agda/Syntax/Common.hs b/src/full/Agda/Syntax/Common.hs
index 381b300..32c4420 100644
--- a/src/full/Agda/Syntax/Common.hs
+++ b/src/full/Agda/Syntax/Common.hs
@@ -1,11 +1,10 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE DeriveFoldable #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE DeriveTraversable #-}
-{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE DeriveFoldable #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE TypeSynonymInstances #-}
{-| Some common syntactic entities are defined in this module.
-}
@@ -17,16 +16,16 @@ import Data.ByteString.Char8 (ByteString)
import qualified Data.ByteString.Char8 as ByteString
import Data.Foldable
import Data.Hashable
+import Data.Monoid
import Data.Traversable
import Data.Typeable (Typeable)
-import Test.QuickCheck
+import Test.QuickCheck hiding (Small)
import Agda.Syntax.Position
import Agda.Utils.Functor
import Agda.Utils.Pretty
-import Agda.Utils.Size
#include "undefined.h"
import Agda.Utils.Impossible
@@ -73,9 +72,39 @@ instance CoArbitrary Induction where
data Hiding = Hidden | Instance | NotHidden
deriving (Typeable, Show, Eq, Ord)
+-- | 'Hiding' is an idempotent partial monoid, with unit 'NotHidden'.
+-- 'Instance' and 'NotHidden' are incompatible.
+instance Monoid Hiding where
+ mempty = NotHidden
+ mappend NotHidden h = h
+ mappend h NotHidden = h
+ mappend Hidden Hidden = Hidden
+ mappend Instance Instance = Instance
+ mappend _ _ = __IMPOSSIBLE__
+
instance KillRange Hiding where
killRange = id
+-- | Decorating something with 'Hiding' information.
+data WithHiding a = WithHiding Hiding a
+ deriving (Typeable, Eq, Ord, Show, Functor, Foldable, Traversable)
+
+instance Decoration WithHiding where
+ traverseF f (WithHiding h a) = WithHiding h <$> f a
+
+instance Applicative WithHiding where
+ pure = WithHiding mempty
+ WithHiding h f <*> WithHiding h' a = WithHiding (mappend h h') (f a)
+
+instance HasRange a => HasRange (WithHiding a) where
+ getRange = getRange . dget
+
+instance SetRange a => SetRange (WithHiding a) where
+ setRange = fmap . setRange
+
+instance KillRange a => KillRange (WithHiding a) where
+ killRange = fmap killRange
+
-- | A lens to access the 'Hiding' attribute in data structures.
-- Minimal implementation: @getHiding@ and one of @setHiding@ or @mapHiding@.
class LensHiding a where
@@ -93,6 +122,15 @@ instance LensHiding Hiding where
setHiding = const
mapHiding = id
+instance LensHiding (WithHiding a) where
+ getHiding (WithHiding h _) = h
+ setHiding h (WithHiding _ a) = WithHiding h a
+ mapHiding f (WithHiding h a) = WithHiding (f h) a
+
+-- | Monoidal composition of 'Hiding' information in some data.
+mergeHiding :: LensHiding a => WithHiding a -> a
+mergeHiding (WithHiding h a) = mapHiding (mappend h) a
+
-- | @isHidden@ does not apply to 'Instance', only to 'Hidden'.
isHidden :: LensHiding a => a -> Bool
isHidden a = getHiding a == Hidden
@@ -119,27 +157,55 @@ makeInstance = setHiding Instance
-- * Relevance
---------------------------------------------------------------------------
+-- | An constructor argument is big if the sort of its type is bigger than
+-- the sort of the data type. Only parameters (and maybe forced arguments)
+-- are allowed to be big.
+-- @
+-- List : Set -> Set
+-- nil : (A : Set) -> List A
+-- @
+-- @A@ is big in constructor @nil@ as the sort @Set1@ of its type @Set@
+-- is bigger than the sort @Set@ of the data type @List@.
+data Big = Big | Small
+ deriving (Typeable, Show, Eq, Enum, Bounded)
+
+instance Ord Big where
+ Big <= Small = False
+ _ <= _ = True
+
-- | A function argument can be relevant or irrelevant.
--- See 'Agda.TypeChecking.Irrelevance'.
+-- See "Agda.TypeChecking.Irrelevance".
data Relevance
= Relevant -- ^ The argument is (possibly) relevant at compile-time.
| NonStrict -- ^ The argument may never flow into evaluation position.
-- Therefore, it is irrelevant at run-time.
-- It is treated relevantly during equality checking.
| Irrelevant -- ^ The argument is irrelevant at compile- and runtime.
- | Forced -- ^ The argument can be skipped during equality checking
+ | Forced Big -- ^ The argument can be skipped during equality checking
-- because its value is already determined by the type.
+ -- If a constructor argument is big, it has to be regarded
+ -- absent, otherwise we get into paradoxes.
| UnusedArg -- ^ The polarity checker has determined that this argument
-- is unused in the definition. It can be skipped during
-- equality checking but should be mined for solutions
-- of meta-variables with relevance 'UnusedArg'
- deriving (Typeable, Show, Eq, Enum, Bounded)
+ deriving (Typeable, Show, Eq)
+
+allRelevances :: [Relevance]
+allRelevances =
+ [ Relevant
+ , NonStrict
+ , Irrelevant
+ , Forced Small
+ , Forced Big
+ , UnusedArg
+ ]
instance KillRange Relevance where
killRange rel = rel -- no range to kill
instance Arbitrary Relevance where
- arbitrary = elements [minBound..maxBound]
+ arbitrary = elements allRelevances
instance Ord Relevance where
(<=) = moreRelevant
@@ -186,8 +252,8 @@ moreRelevant r r' =
(UnusedArg, _) -> True
(_, UnusedArg) -> False
-- third bottom
- (Forced, _) -> True
- (_, Forced) -> False
+ (Forced{}, _) -> True
+ (_, Forced{}) -> False
-- remaining case
(NonStrict,NonStrict) -> True
@@ -206,7 +272,7 @@ data ArgInfo c = ArgInfo
instance KillRange c => KillRange (ArgInfo c) where
killRange (ArgInfo h r cs) = killRange3 ArgInfo h r cs
-{- FAILED to define a less for ArgInfo, since it is parametrized by c
+{- FAILED to define a lens for ArgInfo, since it is parametrized by c
can't instantiate the following to f c = Arg c e
since Haskell does not have lambda abstraction
@@ -270,12 +336,12 @@ instance Decoration (Arg c) where
instance HasRange a => HasRange (Arg c a) where
getRange = getRange . unArg
+instance SetRange a => SetRange (Arg c a) where
+ setRange r = fmap $ setRange r
+
instance (KillRange c, KillRange a) => KillRange (Arg c a) where
killRange (Arg info a) = killRange2 Arg info a
-instance Sized a => Sized (Arg c a) where
- size = size . unArg
-
instance (Eq a, Eq c) => Eq (Arg c a) where
Arg (ArgInfo h1 _ cs1) x1 == Arg (ArgInfo h2 _ cs2) x2 = (h1, cs1, x1) == (h2, cs2, x2)
@@ -285,11 +351,13 @@ instance (Show a, Show c) => Show (Arg c a) where
showH Hidden s = "{" ++ s ++ "}"
showH NotHidden s = "(" ++ s ++ ")"
showH Instance s = "{{" ++ s ++ "}}"
- showR Irrelevant s = "." ++ s
- showR NonStrict s = "?" ++ s
- showR Forced s = "!" ++ s
- showR UnusedArg s = "k" ++ s -- constant
- showR Relevant s = "r" ++ s -- Andreas: I want to see it explicitly
+ showR r s = case r of
+ Irrelevant -> "." ++ s
+ NonStrict -> "?" ++ s
+ Forced Big -> "!b" ++ s
+ Forced Small -> "!" ++ s
+ UnusedArg -> "k" ++ s -- constant
+ Relevant -> "r" ++ s -- Andreas: I want to see it explicitly
showC cs s = show cs ++ s
instance LensHiding (Arg c e) where
@@ -392,9 +460,6 @@ instance HasRange a => HasRange (Dom c a) where
instance (KillRange c, KillRange a) => KillRange (Dom c a) where
killRange (Dom info a) = killRange2 Dom info a
-instance Sized a => Sized (Dom c a) where
- size = size . unDom
-
instance (Show a, Show c) => Show (Dom c a) where
show = show . argFromDom
@@ -447,12 +512,12 @@ instance Decoration (Named name) where
instance HasRange a => HasRange (Named name a) where
getRange = getRange . namedThing
+instance SetRange a => SetRange (Named name a) where
+ setRange r = fmap $ setRange r
+
instance (KillRange name, KillRange a) => KillRange (Named name a) where
killRange (Named n a) = Named (killRange n) (killRange a)
-instance Sized a => Sized (Named name a) where
- size = size . namedThing
-
instance Show a => Show (Named_ a) where
show (Named Nothing x) = show x
show (Named (Just n) x) = rawNameToString (rangedThing n) ++ " = " ++ show x
@@ -555,6 +620,9 @@ type Arity = Nat
data NameId = NameId Integer Integer
deriving (Eq, Ord, Typeable)
+instance KillRange NameId where
+ killRange = id
+
instance Show NameId where
show (NameId x i) = show x ++ "@" ++ show i