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

AC-PPM-1.1.1
2 matches
Codec/PPM/Text.hs
stringPPM :: (Integer,Integer) -> [(Word8,Word8,Word8)] -> TXT.ByteString
stringPPM (sx,sy) ps =
  TXT.pack ("P3\n" ++ show sx ++ " " ++ show sy ++ "\n255\n") `TXT.append`
  TXT.unlines (map (\(r,g,b) -> TXT.pack $ unwords [show r, show g,show b]) ps)

{-|
  Convenience function: Generate PPM data and write it to the
  specified 'Handle'. The handle is not closed or flushed afterwards.
  This allows writing PPM data to network streams, etc. This function

            
Codec/PPM/Text.hs
  other PPM functions.
-}
fn_list :: ((Integer,Integer) -> (Word8,Word8,Word8)) -> (Integer, Integer) -> [(Word8,Word8,Word8)]
fn_list fn (sx, sy) = map fn [ (x,y) | y <- [0..sy-1], x <- [0..sx-1] ]

            
AMI-0.1
1 matches
Network/AMI.hs
    formatParams $ [("Action", name), ("ActionID", packID i)] ++ ps

formatParams :: Parameters -> B.ByteString
formatParams pairs = B.intercalate "\r\n" $ map one pairs
  where
    one (k,v) = k `B.append` ": " `B.append` v


            
Agda-2.6.0.1
27 matches
src/full/Agda/Interaction/Highlighting/JSON.hs
-- | Encode meta information into a JSON Value
showAspects
  :: ModuleToSource
     -- ^ Must contain a mapping for the definition site's module, if any.
  -> (Range, Aspects) -> Value
showAspects modFile (range, aspect) = object
  [ "range" .= [from range, to range]
  , "atoms" .= toAtoms aspect
  , "tokenBased" .= tokenBased aspect

            
src/full/Agda/Interaction/Highlighting/JSON.hs
  , "atoms" .= toAtoms aspect
  , "tokenBased" .= tokenBased aspect
  , "note" .= note aspect
  , "definitionSite" .= fmap defSite (definitionSite aspect)
  ]
  where
    defSite (DefinitionSite mdl position _ _) = object
      [ "filepath" .= filePath (Map.findWithDefault __IMPOSSIBLE__ mdl modFile)
      , "position" .= position

            
src/full/Agda/Interaction/Highlighting/JSON.hs
  -> RemoveTokenBasedHighlighting
  -> HighlightingMethod
  -> ModuleToSource
     -- ^ Must contain a mapping for every definition site's module.
  -> IO Value
jsonifyHighlightingInfo info remove method modFile =
  case chooseHighlightingMethod info method of
    Direct   -> direct
    Indirect -> indirect

            
src/full/Agda/Interaction/Highlighting/JSON.hs
      [ "remove" .= case remove of
          RemoveHighlighting -> True
          KeepHighlighting -> False
      , "payload" .= map (showAspects modFile) (ranges info)
      ]

    direct :: IO Value
    direct = return $ object
      [ "kind"   .= String "HighlightingInfo"

            
src/full/Agda/Interaction/JSONTop.hs
  ]
jsonifyResponse (Resp_SolveAll solutions) = return $ encode $ object
  [ "kind"          .= String "SolveAll"
  , "solutions"     .= map encodeSolution solutions
  ]
  where
    encodeSolution (i, expr) = object
      [ "interactionPoint"  .= i
      , "expression"        .= show expr

            
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