src/Tools/Haskell/Haskell.thy
changeset 69233 560263485988
parent 69228 f4263f7ec9a4
child 69234 2dec32c7313f
     1.1 --- a/src/Tools/Haskell/Haskell.thy	Sun Nov 04 12:07:24 2018 +0100
     1.2 +++ b/src/Tools/Haskell/Haskell.thy	Sun Nov 04 15:28:51 2018 +0100
     1.3 @@ -81,6 +81,57 @@
     1.4      _ -> line
     1.5  \<close>
     1.6  
     1.7 +generate_haskell_file Value.hs = \<open>
     1.8 +{-  Title:      Haskell/Tools/Value.hs
     1.9 +    Author:     Makarius
    1.10 +    LICENSE:    BSD 3-clause (Isabelle)
    1.11 +
    1.12 +Plain values, represented as string.
    1.13 +-}
    1.14 +
    1.15 +module Isabelle.Value
    1.16 +  (print_bool, parse_bool, print_int, parse_int, print_real, parse_real)
    1.17 +where
    1.18 +
    1.19 +import Data.Maybe
    1.20 +import qualified Data.List as List
    1.21 +import qualified Text.Read as Read
    1.22 +
    1.23 +
    1.24 +{- bool -}
    1.25 +
    1.26 +print_bool :: Bool -> String
    1.27 +print_bool True = "true"
    1.28 +print_bool False = "false"
    1.29 +
    1.30 +parse_bool :: String -> Maybe Bool
    1.31 +parse_bool "true" = Just True
    1.32 +parse_bool "false" = Just False
    1.33 +parse_bool _ = Nothing
    1.34 +
    1.35 +
    1.36 +{- int -}
    1.37 +
    1.38 +print_int :: Int -> String
    1.39 +print_int = show
    1.40 +
    1.41 +parse_int :: String -> Maybe Int
    1.42 +parse_int = Read.readMaybe
    1.43 +
    1.44 +
    1.45 +{- real -}
    1.46 +
    1.47 +print_real :: Double -> String
    1.48 +print_real x =
    1.49 +  let s = show x in
    1.50 +    case span (/= '.') s of
    1.51 +      (a, '.' : b) | List.all (== '0') b -> a
    1.52 +      _ -> s
    1.53 +
    1.54 +parse_real :: String -> Maybe Double
    1.55 +parse_real = Read.readMaybe
    1.56 +\<close>
    1.57 +
    1.58  generate_haskell_file Buffer.hs = \<open>
    1.59  {-  Title:      Tools/Haskell/Buffer.hs
    1.60      Author:     Makarius