{- generated by Isabelle -}
{- Title: Tools/Haskell/Library.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
Basic library of Isabelle idioms.
See also "$ISABELLE_HOME/src/Pure/General/basics.ML", "$ISABELLE_HOME/src/Pure/library.ML".
-}
module Isabelle.Library (
(|>), (|->), (#>), (#->),
the, the_default,
fold, fold_rev, single, map_index, get_index,
quote, trim_line, clean_name)
where
import Data.Maybe
{- functions -}
(|>) :: a -> (a -> b) -> b
x |> f = f x
(|->) :: (a, b) -> (a -> b -> c) -> c
(x, y) |-> f = f x y
(#>) :: (a -> b) -> (b -> c) -> a -> c
(f #> g) x = x |> f |> g
(#->) :: (a -> (c, b)) -> (c -> b -> d) -> a -> d
(f #-> g) x = x |> f |-> g
{- options -}
the :: Maybe a -> a
the (Just x) = x
the Nothing = error "the Nothing"
the_default :: a -> Maybe a -> a
the_default x Nothing = x
the_default _ (Just y) = y
{- lists -}
fold :: (a -> b -> b) -> [a] -> b -> b
fold _ [] y = y
fold f (x : xs) y = fold f xs (f x y)
fold_rev :: (a -> b -> b) -> [a] -> b -> b
fold_rev _ [] y = y
fold_rev f (x : xs) y = f x (fold_rev f xs y)
single :: a -> [a]
single x = [x]
map_index :: ((Int, a) -> b) -> [a] -> [b]
map_index f = map_aux 0
where
map_aux _ [] = []
map_aux i (x : xs) = f (i, x) : map_aux (i + 1) xs
get_index :: (a -> Maybe b) -> [a] -> Maybe (Int, b)
get_index f = get_aux 0
where
get_aux _ [] = Nothing
get_aux i (x : xs) =
case f x of
Nothing -> get_aux (i + 1) xs
Just y -> Just (i, y)
{- strings -}
quote :: String -> String
quote s = "\"" ++ s ++ "\""
trim_line :: String -> String
trim_line line =
case reverse line of
'\n' : '\r' : rest -> reverse rest
'\n' : rest -> reverse rest
_ -> line
clean_name :: String -> String
clean_name = reverse #> dropWhile (== '_') #> reverse