src/Tools/Haskell/Value.hs
author wenzelm
Sat, 10 Nov 2018 17:12:09 +0100
changeset 69280 e1d01b351724
parent 69233 560263485988
permissions -rw-r--r--
more formal references;
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.
69280
e1d01b351724 more formal references;
wenzelm
parents: 69233
diff changeset
     8
e1d01b351724 more formal references;
wenzelm
parents: 69233
diff changeset
     9
See also "$ISABELLE_HOME/src/Pure/General/value.ML".
69233
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    10
-}
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    11
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    12
module Isabelle.Value
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    13
  (print_bool, parse_bool, print_int, parse_int, print_real, parse_real)
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    14
where
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    15
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    16
import Data.Maybe
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    17
import qualified Data.List as List
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    18
import qualified Text.Read as Read
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    19
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
{- bool -}
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    22
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    23
print_bool :: Bool -> String
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    24
print_bool True = "true"
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    25
print_bool False = "false"
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    26
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    27
parse_bool :: String -> Maybe Bool
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    28
parse_bool "true" = Just True
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    29
parse_bool "false" = Just False
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    30
parse_bool _ = Nothing
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    31
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
{- int -}
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    34
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    35
print_int :: Int -> String
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    36
print_int = show
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    37
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    38
parse_int :: String -> Maybe Int
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    39
parse_int = Read.readMaybe
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    40
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
{- real -}
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    43
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    44
print_real :: Double -> String
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    45
print_real x =
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    46
  let s = show x in
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    47
    case span (/= '.') s of
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    48
      (a, '.' : b) | List.all (== '0') b -> a
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    49
      _ -> s
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    50
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    51
parse_real :: String -> Maybe Double
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents:
diff changeset
    52
parse_real = Read.readMaybe