src/Tools/Haskell/Value.hs
author wenzelm
Sun, 04 Nov 2018 15:28:51 +0100
changeset 69233 560263485988
child 69280 e1d01b351724
permissions -rw-r--r--
ported from src/Pure/General/value.ML;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
69233
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
     1
{- generated by Isabelle -}
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
     2
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
     3
{-  Title:      Haskell/Tools/Value.hs
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
     4
    Author:     Makarius
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
     5
    LICENSE:    BSD 3-clause (Isabelle)
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
     6
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
     7
Plain values, represented as string.
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
     8
-}
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
     9
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    10
module Isabelle.Value
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    11
  (print_bool, parse_bool, print_int, parse_int, print_real, parse_real)
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    12
where
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    13
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    14
import Data.Maybe
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    15
import qualified Data.List as List
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    16
import qualified Text.Read as Read
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    17
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    18
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    19
{- bool -}
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    20
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    21
print_bool :: Bool -> String
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    22
print_bool True = "true"
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    23
print_bool False = "false"
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    24
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    25
parse_bool :: String -> Maybe Bool
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    26
parse_bool "true" = Just True
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    27
parse_bool "false" = Just False
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    28
parse_bool _ = Nothing
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    29
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    30
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    31
{- int -}
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    32
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    33
print_int :: Int -> String
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    34
print_int = show
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    35
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    36
parse_int :: String -> Maybe Int
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    37
parse_int = Read.readMaybe
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    38
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    39
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    40
{- real -}
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    41
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    42
print_real :: Double -> String
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    43
print_real x =
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    44
  let s = show x in
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    45
    case span (/= '.') s of
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    46
      (a, '.' : b) | List.all (== '0') b -> a
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    47
      _ -> s
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    48
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    49
parse_real :: String -> Maybe Double
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    50
parse_real = Read.readMaybe