Aelve Codesearch

grep over package repositories
Please provide a string to search for.
3+ characters are required.
Index updated about a month ago

total matches: more than 1000

Agda-2.6.0.1
30 matches
src/full/Agda/Syntax/Common.hs

instance Monoid Overlappable where
  mempty  = NoOverlap
  mappend = (<>)

instance Monoid Hiding where
  mempty = NotHidden
  mappend = (<>)

instance KillRange Hiding where
  killRange = id

instance NFData Overlappable where

            
src/full/Agda/Syntax/Common.hs

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

            
src/full/Agda/Syntax/Common.hs
  getRange = getRange . dget

instance SetRange a => SetRange (WithHiding a) where
  setRange = fmap . setRange

instance KillRange a => KillRange (WithHiding a) where
  killRange = fmap killRange

instance NFData a => NFData (WithHiding a) where
  rnf (WithHiding _ a) = rnf a

-- | A lens to access the 'Hiding' attribute in data structures.

            
src/full/Agda/Syntax/Common.hs
  rnf (WithHiding _ a) = rnf a

-- | A lens to access the 'Hiding' attribute in data structures.
--   Minimal implementation: @getHiding@ and one of @setHiding@ or @mapHiding@.
class LensHiding a where

  getHiding :: a -> Hiding

  setHiding :: Hiding -> a -> a

            
src/full/Agda/Syntax/Common.hs
  getHiding :: a -> Hiding

  setHiding :: Hiding -> a -> a
  setHiding h = mapHiding (const h)

  mapHiding :: (Hiding -> Hiding) -> a -> a
  mapHiding f a = setHiding (f $ getHiding a) a

instance LensHiding Hiding where
  getHiding = id
  setHiding = const
  mapHiding = id

            
src/full/Agda/Syntax/Common.hs
instance LensHiding Hiding where
  getHiding = id
  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

            
src/full/Agda/Syntax/Common.hs
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

-- | 'NotHidden' arguments are @visible@.
visible :: LensHiding a => a -> Bool
visible a = getHiding a == NotHidden


            
src/full/Agda/Syntax/Common.hs
-- | Pointwise unit.
instance Monoid Modality where
  mempty = Modality mempty mempty
  mappend = (<>)

-- | Dominance ordering.
instance PartialOrd Modality where
  comparable (Modality r q) (Modality r' q') = comparable (r, q) (r', q')


            
src/full/Agda/Syntax/Common.hs
--   This function is e.g. used to update the modality information
--   on pattern variables @a@ after a match against something of modality @q@.
applyModality :: LensModality a => Modality -> a -> a
applyModality m = mapModality (m `composeModality`)

-- | @inverseComposeModality r x@ returns the least modality @y@
--   such that forall @x@, @y@ we have
--   @x \`moreUsableModality\` (r \`composeModality\` y)@
--   iff

            
src/full/Agda/Syntax/Common.hs
-- | Left division by a 'Modality'.
--   Used e.g. to modify context when going into a @m@ argument.
inverseApplyModality :: LensModality a => Modality -> a -> a
inverseApplyModality m = mapModality (m `inverseComposeModality`)


-- boilerplate instances

instance KillRange Modality where

            
src/full/Agda/Syntax/Common.hs
  getModality :: a -> Modality

  setModality :: Modality -> a -> a
  setModality = mapModality . const

  mapModality :: (Modality -> Modality) -> a -> a
  mapModality f a = setModality (f $ getModality a) a

instance LensModality Modality where
  getModality = id
  setModality = const
  mapModality = id

            
src/full/Agda/Syntax/Common.hs
instance LensModality Modality where
  getModality = id
  setModality = const
  mapModality = id

instance LensRelevance Modality where
  getRelevance = modRelevance
  setRelevance h m = m { modRelevance = h }
  mapRelevance f m = m { modRelevance = f (modRelevance m) }

            
src/full/Agda/Syntax/Common.hs
instance LensRelevance Modality where
  getRelevance = modRelevance
  setRelevance h m = m { modRelevance = h }
  mapRelevance f m = m { modRelevance = f (modRelevance m) }

instance LensQuantity Modality where
  getQuantity = modQuantity
  setQuantity h m = m { modQuantity = h }
  mapQuantity f m = m { modQuantity = f (modQuantity m) }

            
src/full/Agda/Syntax/Common.hs
instance LensQuantity Modality where
  getQuantity = modQuantity
  setQuantity h m = m { modQuantity = h }
  mapQuantity f m = m { modQuantity = f (modQuantity m) }

-- default accessors for Relevance

getRelevanceMod :: LensModality a => LensGet Relevance a
getRelevanceMod = getRelevance . getModality

            
src/full/Agda/Syntax/Common.hs
getRelevanceMod = getRelevance . getModality

setRelevanceMod :: LensModality a => LensSet Relevance a
setRelevanceMod = mapModality . setRelevance

mapRelevanceMod :: LensModality a => LensMap Relevance a
mapRelevanceMod = mapModality . mapRelevance

-- default accessors for Quantity

getQuantityMod :: LensModality a => LensGet Quantity a
getQuantityMod = getQuantity . getModality

            
src/full/Agda/Syntax/Common.hs
getQuantityMod = getQuantity . getModality

setQuantityMod :: LensModality a => LensSet Quantity a
setQuantityMod = mapModality . setQuantity

mapQuantityMod :: LensModality a => LensMap Quantity a
mapQuantityMod = mapModality . mapQuantity

---------------------------------------------------------------------------
-- * Quantities
---------------------------------------------------------------------------


            
src/full/Agda/Syntax/Common.hs
    -- Mostly TODO (needs postponable constraints between quantities to compute uses).
  | Quantityω  -- ^ Unrestricted use @ℕ@.
  deriving (Data, Show, Generic, Eq, Enum, Bounded, Ord)
    -- @Ord@ instance in case @Quantity@ is used in keys for maps etc.

defaultQuantity :: Quantity
defaultQuantity = Quantityω

-- | Composition of quantities (multiplication).

            
src/full/Agda/Syntax/Common.hs
--   Otherwise, 1 is the unit.
instance Monoid Quantity where
  mempty  = Quantity1
  mappend = (<>)

-- | Note that the order is @ω ≤ 0,1@, more options is smaller.
instance PartialOrd Quantity where
  comparable = curry $ \case
    (q, q') | q == q' -> POEQ

            
src/full/Agda/Syntax/Common.hs
--   This function is e.g. used to update the quantity information
--   on pattern variables @a@ after a match against something of quantity @q@.
applyQuantity :: LensQuantity a => Quantity -> a -> a
applyQuantity q = mapQuantity (q `composeQuantity`)

-- | @inverseComposeQuantity r x@ returns the least quantity @y@
--   such that forall @x@, @y@ we have
--   @x \`moreQuantity\` (r \`composeQuantity\` y)@
--   iff

            
src/full/Agda/Syntax/Common.hs
-- | Left division by a 'Quantity'.
--   Used e.g. to modify context when going into a @q@ argument.
inverseApplyQuantity :: LensQuantity a => Quantity -> a -> a
inverseApplyQuantity q = mapQuantity (q `inverseComposeQuantity`)


-- boilerplate instances

class LensQuantity a where

            
src/full/Agda/Syntax/Common.hs
  getQuantity :: a -> Quantity

  setQuantity :: Quantity -> a -> a
  setQuantity = mapQuantity . const

  mapQuantity :: (Quantity -> Quantity) -> a -> a
  mapQuantity f a = setQuantity (f $ getQuantity a) a

instance LensQuantity Quantity where
  getQuantity = id
  setQuantity = const
  mapQuantity = id

            
src/full/Agda/Syntax/Common.hs
instance LensQuantity Quantity where
  getQuantity = id
  setQuantity = const
  mapQuantity = id

instance KillRange Quantity where
  killRange = id

instance NFData Quantity where

            
src/full/Agda/Syntax/Common.hs
  rnf Irrelevant = ()

-- | A lens to access the 'Relevance' attribute in data structures.
--   Minimal implementation: @getRelevance@ and one of @setRelevance@ or @mapRelevance@.
class LensRelevance a where

  getRelevance :: a -> Relevance

  setRelevance :: Relevance -> a -> a

            
src/full/Agda/Syntax/Common.hs
  getRelevance :: a -> Relevance

  setRelevance :: Relevance -> a -> a
  setRelevance h = mapRelevance (const h)

  mapRelevance :: (Relevance -> Relevance) -> a -> a
  mapRelevance f a = setRelevance (f $ getRelevance a) a

instance LensRelevance Relevance where
  getRelevance = id
  setRelevance = const
  mapRelevance = id

            
src/full/Agda/Syntax/Common.hs
instance LensRelevance Relevance where
  getRelevance = id
  setRelevance = const
  mapRelevance = id

isRelevant :: LensRelevance a => a -> Bool
isRelevant a = getRelevance a == Relevant

isIrrelevant :: LensRelevance a => a -> Bool

            
src/full/Agda/Syntax/Common.hs
--   This function is e.g. used to update the relevance information
--   on pattern variables @a@ after a match against something @rel@.
applyRelevance :: LensRelevance a => Relevance -> a -> a
applyRelevance rel = mapRelevance (rel `composeRelevance`)

-- | @inverseComposeRelevance r x@ returns the most irrelevant @y@
--   such that forall @x@, @y@ we have
--   @x \`moreRelevant\` (r \`composeRelevance\` y)@
--   iff

            
src/full/Agda/Syntax/Common.hs
-- | Left division by a 'Relevance'.
--   Used e.g. to modify context when going into a @rel@ argument.
inverseApplyRelevance :: LensRelevance a => Relevance -> a -> a
inverseApplyRelevance rel = mapRelevance (rel `inverseComposeRelevance`)

-- | 'Relevance' forms a semigroup under composition.
instance Semigroup Relevance where
  (<>) = composeRelevance


            
src/full/Agda/Syntax/Common.hs
-- | 'Relevant' is the unit.
instance Monoid Relevance where
  mempty  = Relevant
  mappend = (<>)

instance POSemigroup Relevance where
instance POMonoid Relevance where

instance LeftClosedPOMonoid Relevance where

            
src/full/Agda/Syntax/Common.hs
  getRange = getRange . dget

instance SetRange a => SetRange (WithOrigin a) where
  setRange = fmap . setRange

instance KillRange a => KillRange (WithOrigin a) where
  killRange = fmap killRange

instance NFData a => NFData (WithOrigin a) where
  rnf (WithOrigin _ a) = rnf a

-- | A lens to access the 'Origin' attribute in data structures.

            
src/full/Agda/Syntax/Common.hs
  rnf (WithOrigin _ a) = rnf a

-- | A lens to access the 'Origin' attribute in data structures.
--   Minimal implementation: @getOrigin@ and one of @setOrigin@ or @mapOrigin@.

class LensOrigin a where

  getOrigin :: a -> Origin