69233
|
1 |
{- generated by Isabelle -}
|
|
2 |
|
|
3 |
{- Title: Haskell/Tools/Value.hs
|
|
4 |
Author: Makarius
|
|
5 |
LICENSE: BSD 3-clause (Isabelle)
|
|
6 |
|
|
7 |
Plain values, represented as string.
|
|
8 |
-}
|
|
9 |
|
|
10 |
module Isabelle.Value
|
|
11 |
(print_bool, parse_bool, print_int, parse_int, print_real, parse_real)
|
|
12 |
where
|
|
13 |
|
|
14 |
import Data.Maybe
|
|
15 |
import qualified Data.List as List
|
|
16 |
import qualified Text.Read as Read
|
|
17 |
|
|
18 |
|
|
19 |
{- bool -}
|
|
20 |
|
|
21 |
print_bool :: Bool -> String
|
|
22 |
print_bool True = "true"
|
|
23 |
print_bool False = "false"
|
|
24 |
|
|
25 |
parse_bool :: String -> Maybe Bool
|
|
26 |
parse_bool "true" = Just True
|
|
27 |
parse_bool "false" = Just False
|
|
28 |
parse_bool _ = Nothing
|
|
29 |
|
|
30 |
|
|
31 |
{- int -}
|
|
32 |
|
|
33 |
print_int :: Int -> String
|
|
34 |
print_int = show
|
|
35 |
|
|
36 |
parse_int :: String -> Maybe Int
|
|
37 |
parse_int = Read.readMaybe
|
|
38 |
|
|
39 |
|
|
40 |
{- real -}
|
|
41 |
|
|
42 |
print_real :: Double -> String
|
|
43 |
print_real x =
|
|
44 |
let s = show x in
|
|
45 |
case span (/= '.') s of
|
|
46 |
(a, '.' : b) | List.all (== '0') b -> a
|
|
47 |
_ -> s
|
|
48 |
|
|
49 |
parse_real :: String -> Maybe Double
|
|
50 |
parse_real = Read.readMaybe
|