# HG changeset patch
# User wenzelm
# Date 1541341731 -3600
# Node ID 5602634859882b3b15248e182aab28ae7e052491
# Parent  2b913054a9cf447afc55d60db304829d210727ac
ported from src/Pure/General/value.ML;

diff -r 2b913054a9cf -r 560263485988 src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Sun Nov 04 12:07:24 2018 +0100
+++ b/src/Tools/Haskell/Haskell.thy	Sun Nov 04 15:28:51 2018 +0100
@@ -81,6 +81,57 @@
     _ -> line
 \<close>
 
+generate_haskell_file Value.hs = \<open>
+{-  Title:      Haskell/Tools/Value.hs
+    Author:     Makarius
+    LICENSE:    BSD 3-clause (Isabelle)
+
+Plain values, represented as string.
+-}
+
+module Isabelle.Value
+  (print_bool, parse_bool, print_int, parse_int, print_real, parse_real)
+where
+
+import Data.Maybe
+import qualified Data.List as List
+import qualified Text.Read as Read
+
+
+{- bool -}
+
+print_bool :: Bool -> String
+print_bool True = "true"
+print_bool False = "false"
+
+parse_bool :: String -> Maybe Bool
+parse_bool "true" = Just True
+parse_bool "false" = Just False
+parse_bool _ = Nothing
+
+
+{- int -}
+
+print_int :: Int -> String
+print_int = show
+
+parse_int :: String -> Maybe Int
+parse_int = Read.readMaybe
+
+
+{- real -}
+
+print_real :: Double -> String
+print_real x =
+  let s = show x in
+    case span (/= '.') s of
+      (a, '.' : b) | List.all (== '0') b -> a
+      _ -> s
+
+parse_real :: String -> Maybe Double
+parse_real = Read.readMaybe
+\<close>
+
 generate_haskell_file Buffer.hs = \<open>
 {-  Title:      Tools/Haskell/Buffer.hs
     Author:     Makarius
diff -r 2b913054a9cf -r 560263485988 src/Tools/Haskell/Value.hs
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Haskell/Value.hs	Sun Nov 04 15:28:51 2018 +0100
@@ -0,0 +1,50 @@
+{- generated by Isabelle -}
+
+{-  Title:      Haskell/Tools/Value.hs
+    Author:     Makarius
+    LICENSE:    BSD 3-clause (Isabelle)
+
+Plain values, represented as string.
+-}
+
+module Isabelle.Value
+  (print_bool, parse_bool, print_int, parse_int, print_real, parse_real)
+where
+
+import Data.Maybe
+import qualified Data.List as List
+import qualified Text.Read as Read
+
+
+{- bool -}
+
+print_bool :: Bool -> String
+print_bool True = "true"
+print_bool False = "false"
+
+parse_bool :: String -> Maybe Bool
+parse_bool "true" = Just True
+parse_bool "false" = Just False
+parse_bool _ = Nothing
+
+
+{- int -}
+
+print_int :: Int -> String
+print_int = show
+
+parse_int :: String -> Maybe Int
+parse_int = Read.readMaybe
+
+
+{- real -}
+
+print_real :: Double -> String
+print_real x =
+  let s = show x in
+    case span (/= '.') s of
+      (a, '.' : b) | List.all (== '0') b -> a
+      _ -> s
+
+parse_real :: String -> Maybe Double
+parse_real = Read.readMaybe
diff -r 2b913054a9cf -r 560263485988 src/Tools/Haskell/haskell.ML
--- a/src/Tools/Haskell/haskell.ML	Sun Nov 04 12:07:24 2018 +0100
+++ b/src/Tools/Haskell/haskell.ML	Sun Nov 04 15:28:51 2018 +0100
@@ -47,6 +47,7 @@
 
 val source_modules =
  [\<^file>\<open>~~/src/Tools/Haskell/Library.hs\<close>,
+  \<^file>\<open>~~/src/Tools/Haskell/Value.hs\<close>,
   \<^file>\<open>~~/src/Tools/Haskell/Buffer.hs\<close>,
   \<^file>\<open>~~/src/Tools/Haskell/Properties.hs\<close>,
   \<^file>\<open>~~/src/Tools/Haskell/Markup.hs\<close>,