src/Tools/Haskell/Library.hs
author wenzelm
Sat, 03 Nov 2018 20:00:45 +0100
changeset 69226 68f5dc2275ac
parent 69225 bf2fecda8383
child 69227 71b48b749836
permissions -rw-r--r--
tuned whitespace;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
     1
{- GENERATED by Isabelle! -}
69226
68f5dc2275ac tuned whitespace;
wenzelm
parents: 69225
diff changeset
     2
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
     3
{-  Title:      Tools/Haskell/Library.hs
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
     4
    Author:     Makarius
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
     5
    LICENSE:    BSD 3-clause (Isabelle)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
     6
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
     7
Basic library of Isabelle idioms.
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
     8
-}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
     9
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    10
module Isabelle.Library
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    11
  ((|>), (|->), (#>), (#->), fold, fold_rev, single, quote, trim_line)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    12
where
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    13
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    14
{- functions -}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    15
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    16
(|>) :: a -> (a -> b) -> b
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    17
x |> f = f x
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    18
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    19
(|->) :: (a, b) -> (a -> b -> c) -> c
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    20
(x, y) |-> f = f x y
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    21
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    22
(#>) :: (a -> b) -> (b -> c) -> a -> c
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    23
(f #> g) x = x |> f |> g
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    24
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    25
(#->) :: (a -> (c, b)) -> (c -> b -> d) -> a -> d
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    26
(f #-> g) x  = x |> f |-> g
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    27
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    28
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    29
{- lists -}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    30
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    31
fold :: (a -> b -> b) -> [a] -> b -> b
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    32
fold _ [] y = y
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    33
fold f (x : xs) y = fold f xs (f x y)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    34
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    35
fold_rev :: (a -> b -> b) -> [a] -> b -> b
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    36
fold_rev _ [] y = y
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    37
fold_rev f (x : xs) y = f x (fold_rev f xs y)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    38
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    39
single :: a -> [a]
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    40
single x = [x]
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    41
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    42
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    43
{- strings -}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    44
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    45
quote :: String -> String
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    46
quote s = "\"" ++ s ++ "\""
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    47
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    48
trim_line :: String -> String
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    49
trim_line line =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    50
  case reverse line of
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    51
    '\n' : '\r' : rest -> reverse rest
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    52
    '\n' : rest -> reverse rest
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    53
    _ -> line