1 {- generated by Isabelle -} |
|
2 |
|
3 {- Title: Tools/Haskell/Library.hs |
|
4 Author: Makarius |
|
5 LICENSE: BSD 3-clause (Isabelle) |
|
6 |
|
7 Basic library of Isabelle idioms. |
|
8 |
|
9 See also "$ISABELLE_HOME/src/Pure/General/basics.ML", "$ISABELLE_HOME/src/Pure/library.ML". |
|
10 -} |
|
11 |
|
12 module Isabelle.Library ( |
|
13 (|>), (|->), (#>), (#->), |
|
14 |
|
15 the, the_default, |
|
16 |
|
17 fold, fold_rev, single, map_index, get_index, |
|
18 |
|
19 quote, trim_line, clean_name) |
|
20 where |
|
21 |
|
22 import Data.Maybe |
|
23 |
|
24 |
|
25 {- functions -} |
|
26 |
|
27 (|>) :: a -> (a -> b) -> b |
|
28 x |> f = f x |
|
29 |
|
30 (|->) :: (a, b) -> (a -> b -> c) -> c |
|
31 (x, y) |-> f = f x y |
|
32 |
|
33 (#>) :: (a -> b) -> (b -> c) -> a -> c |
|
34 (f #> g) x = x |> f |> g |
|
35 |
|
36 (#->) :: (a -> (c, b)) -> (c -> b -> d) -> a -> d |
|
37 (f #-> g) x = x |> f |-> g |
|
38 |
|
39 |
|
40 {- options -} |
|
41 |
|
42 the :: Maybe a -> a |
|
43 the (Just x) = x |
|
44 the Nothing = error "the Nothing" |
|
45 |
|
46 the_default :: a -> Maybe a -> a |
|
47 the_default x Nothing = x |
|
48 the_default _ (Just y) = y |
|
49 |
|
50 |
|
51 {- lists -} |
|
52 |
|
53 fold :: (a -> b -> b) -> [a] -> b -> b |
|
54 fold _ [] y = y |
|
55 fold f (x : xs) y = fold f xs (f x y) |
|
56 |
|
57 fold_rev :: (a -> b -> b) -> [a] -> b -> b |
|
58 fold_rev _ [] y = y |
|
59 fold_rev f (x : xs) y = f x (fold_rev f xs y) |
|
60 |
|
61 single :: a -> [a] |
|
62 single x = [x] |
|
63 |
|
64 map_index :: ((Int, a) -> b) -> [a] -> [b] |
|
65 map_index f = map_aux 0 |
|
66 where |
|
67 map_aux _ [] = [] |
|
68 map_aux i (x : xs) = f (i, x) : map_aux (i + 1) xs |
|
69 |
|
70 get_index :: (a -> Maybe b) -> [a] -> Maybe (Int, b) |
|
71 get_index f = get_aux 0 |
|
72 where |
|
73 get_aux _ [] = Nothing |
|
74 get_aux i (x : xs) = |
|
75 case f x of |
|
76 Nothing -> get_aux (i + 1) xs |
|
77 Just y -> Just (i, y) |
|
78 |
|
79 |
|
80 {- strings -} |
|
81 |
|
82 quote :: String -> String |
|
83 quote s = "\"" ++ s ++ "\"" |
|
84 |
|
85 trim_line :: String -> String |
|
86 trim_line line = |
|
87 case reverse line of |
|
88 '\n' : '\r' : rest -> reverse rest |
|
89 '\n' : rest -> reverse rest |
|
90 _ -> line |
|
91 |
|
92 clean_name :: String -> String |
|
93 clean_name = reverse #> dropWhile (== '_') #> reverse |
|