| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Util
- (▪) :: forall a b. (BShow a, BShow b) => a -> b -> String
- class BShow a where
- printInd :: Show a => Int -> a -> IO ()
- putStrLnInd :: Int -> String -> IO ()
- unique :: Ord a => [a] -> [a]
- swapPrefix :: Eq a => [a] -> [a] -> [a] -> [a]
- agdafy :: String -> String
- stdout2file :: Maybe FilePath -> IO ()
- checkIdScope :: Int -> String -> Set (Int, String) -> Bool
Spaced concatenation
(▪) :: forall a b. (BShow a, BShow b) => a -> b -> String infixr 4
'"foo" ▪ "bar"' = '"foo bar"'. Its main use is to simplify the concatenation of printable types separated by spaces.
class BShow a where
Printing with indentation
putStrLnInd :: Int -> String -> IO ()
printInd i str, prints a with str level of indentation i.
List manipulation
Arguments
| :: Eq a | |
| => [a] | Current prefix |
| -> [a] | Replacement |
| -> [a] | List to be replaced |
| -> [a] | Resulting list |
swapPrefix a b str, replaces prefix a in str with b
checking that a is a prefix of str.
Others
Metis
identifiers usually contain _ characters which are invalid in
Agda, agdafy
replaces normalize_0_0 with normalize-0-0. This is
mostly used inside the
Happy
parser every time an AtomicWord is created.
stdout2file :: Maybe FilePath -> IO ()
Redirect all stdout output into a file or do nothing (in case of
Nothing)
checkIdScope :: Int -> String -> Set (Int, String) -> Bool
checkIdScope i t s check if any name in s has a more
general scope than t with level i