69225
|
1 |
{- GENERATED by Isabelle! -}
|
69226
|
2 |
|
69225
|
3 |
{- Title: Tools/Haskell/Library.hs
|
|
4 |
Author: Makarius
|
|
5 |
LICENSE: BSD 3-clause (Isabelle)
|
|
6 |
|
|
7 |
Basic library of Isabelle idioms.
|
|
8 |
-}
|
|
9 |
|
|
10 |
module Isabelle.Library
|
|
11 |
((|>), (|->), (#>), (#->), fold, fold_rev, single, quote, trim_line)
|
|
12 |
where
|
|
13 |
|
|
14 |
{- functions -}
|
|
15 |
|
|
16 |
(|>) :: a -> (a -> b) -> b
|
|
17 |
x |> f = f x
|
|
18 |
|
|
19 |
(|->) :: (a, b) -> (a -> b -> c) -> c
|
|
20 |
(x, y) |-> f = f x y
|
|
21 |
|
|
22 |
(#>) :: (a -> b) -> (b -> c) -> a -> c
|
|
23 |
(f #> g) x = x |> f |> g
|
|
24 |
|
|
25 |
(#->) :: (a -> (c, b)) -> (c -> b -> d) -> a -> d
|
|
26 |
(f #-> g) x = x |> f |-> g
|
|
27 |
|
|
28 |
|
|
29 |
{- lists -}
|
|
30 |
|
|
31 |
fold :: (a -> b -> b) -> [a] -> b -> b
|
|
32 |
fold _ [] y = y
|
|
33 |
fold f (x : xs) y = fold f xs (f x y)
|
|
34 |
|
|
35 |
fold_rev :: (a -> b -> b) -> [a] -> b -> b
|
|
36 |
fold_rev _ [] y = y
|
|
37 |
fold_rev f (x : xs) y = f x (fold_rev f xs y)
|
|
38 |
|
|
39 |
single :: a -> [a]
|
|
40 |
single x = [x]
|
|
41 |
|
|
42 |
|
|
43 |
{- strings -}
|
|
44 |
|
|
45 |
quote :: String -> String
|
|
46 |
quote s = "\"" ++ s ++ "\""
|
|
47 |
|
|
48 |
trim_line :: String -> String
|
|
49 |
trim_line line =
|
|
50 |
case reverse line of
|
|
51 |
'\n' : '\r' : rest -> reverse rest
|
|
52 |
'\n' : rest -> reverse rest
|
|
53 |
_ -> line
|