merged
authorwenzelm
Sat Nov 03 20:24:56 2018 +0100 (6 months ago)
changeset 69229043cbeb0b1cf
parent 69221 21ee588bac7d
parent 69228 f4263f7ec9a4
child 69230 07fc77bf5eb6
merged
     1.1 --- a/src/Pure/General/file.ML	Thu Nov 01 18:19:33 2018 +0000
     1.2 +++ b/src/Pure/General/file.ML	Sat Nov 03 20:24:56 2018 +0100
     1.3 @@ -9,6 +9,7 @@
     1.4    val standard_path: Path.T -> string
     1.5    val platform_path: Path.T -> string
     1.6    val bash_path: Path.T -> string
     1.7 +  val bash_paths: Path.T list -> string
     1.8    val full_path: Path.T -> Path.T -> Path.T
     1.9    val tmp_path: Path.T -> Path.T
    1.10    val exists: Path.T -> bool
    1.11 @@ -29,6 +30,7 @@
    1.12    val read: Path.T -> string
    1.13    val write: Path.T -> string -> unit
    1.14    val append: Path.T -> string -> unit
    1.15 +  val generate: Path.T -> string -> unit
    1.16    val output: BinIO.outstream -> string -> unit
    1.17    val write_list: Path.T -> string list -> unit
    1.18    val append_list: Path.T -> string list -> unit
    1.19 @@ -45,7 +47,7 @@
    1.20  val platform_path = ML_System.platform_path o standard_path;
    1.21  
    1.22  val bash_path = Bash_Syntax.string o standard_path;
    1.23 -
    1.24 +val bash_paths = Bash_Syntax.strings o map standard_path;
    1.25  
    1.26  (* full_path *)
    1.27  
    1.28 @@ -154,6 +156,7 @@
    1.29  
    1.30  fun write path txt = write_list path [txt];
    1.31  fun append path txt = append_list path [txt];
    1.32 +fun generate path txt = if try read path = SOME txt then () else write path txt;
    1.33  
    1.34  fun write_buffer path buf = open_output (Buffer.output buf) path;
    1.35  
     2.1 --- a/src/Pure/PIDE/xml.ML	Thu Nov 01 18:19:33 2018 +0000
     2.2 +++ b/src/Pure/PIDE/xml.ML	Sat Nov 03 20:24:56 2018 +0100
     2.3 @@ -93,7 +93,7 @@
     2.4    | unwrap_elem _ = NONE;
     2.5  
     2.6  
     2.7 -(* text context *)
     2.8 +(* text content *)
     2.9  
    2.10  fun add_content tree =
    2.11    (case unwrap_elem tree of
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Tools/Haskell/Buffer.hs	Sat Nov 03 20:24:56 2018 +0100
     3.3 @@ -0,0 +1,23 @@
     3.4 +{- generated by Isabelle -}
     3.5 +
     3.6 +{-  Title:      Tools/Haskell/Buffer.hs
     3.7 +    Author:     Makarius
     3.8 +    LICENSE:    BSD 3-clause (Isabelle)
     3.9 +
    3.10 +Efficient text buffers.
    3.11 +-}
    3.12 +
    3.13 +module Isabelle.Buffer (T, empty, add, content)
    3.14 +where
    3.15 +
    3.16 +newtype T = Buffer [String]
    3.17 +
    3.18 +empty :: T
    3.19 +empty = Buffer []
    3.20 +
    3.21 +add :: String -> T -> T
    3.22 +add "" buf = buf
    3.23 +add x (Buffer xs) = Buffer (x : xs)
    3.24 +
    3.25 +content :: T -> String
    3.26 +content (Buffer xs) = concat (reverse xs)
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Tools/Haskell/Build.thy	Sat Nov 03 20:24:56 2018 +0100
     4.3 @@ -0,0 +1,24 @@
     4.4 +(*  Title:      Tools/Haskell/Build.thy
     4.5 +    Author:     Makarius
     4.6 +*)
     4.7 +
     4.8 +section \<open>Build Isabelle/Haskell modules\<close>
     4.9 +
    4.10 +theory Build imports Haskell
    4.11 +begin
    4.12 +
    4.13 +ML_command \<open>
    4.14 +  Isabelle_System.with_tmp_dir "ghc" (fn dir =>
    4.15 +    let
    4.16 +      val (out, rc) =
    4.17 +        Isabelle_System.bash_output
    4.18 +         (cat_lines
    4.19 +           ["set -e",
    4.20 +            "cd " ^ File.bash_path dir,
    4.21 +            "cp " ^ File.bash_paths Haskell.source_modules ^ " .",
    4.22 +            "\"$ISABELLE_GHC\" " ^ File.bash_paths (map Path.base Haskell.source_modules)]);
    4.23 +    in if rc = 0 then writeln out else error out end
    4.24 +  )
    4.25 +\<close>
    4.26 +
    4.27 +end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Tools/Haskell/Haskell.thy	Sat Nov 03 20:24:56 2018 +0100
     5.3 @@ -0,0 +1,372 @@
     5.4 +(*  Title:      Tools/Haskell/Haskell.thy
     5.5 +    Author:     Makarius
     5.6 +
     5.7 +Support for Isabelle tools in Haskell.
     5.8 +*)
     5.9 +
    5.10 +theory Haskell
    5.11 +  imports Pure
    5.12 +  keywords "generate_haskell_file" "export_haskell_file" :: thy_decl
    5.13 +begin
    5.14 +
    5.15 +ML_file "haskell.ML"
    5.16 +
    5.17 +
    5.18 +section \<open>Commands\<close>
    5.19 +
    5.20 +ML \<open>
    5.21 +  Outer_Syntax.command \<^command_keyword>\<open>generate_haskell_file\<close> "generate Haskell file"
    5.22 +    (Parse.position Parse.path -- (\<^keyword>\<open>=\<close> |-- Parse.input Parse.embedded)
    5.23 +      >> Haskell.generate_file_cmd);
    5.24 +
    5.25 +  Outer_Syntax.command \<^command_keyword>\<open>export_haskell_file\<close> "export Haskell file"
    5.26 +    (Parse.name -- (\<^keyword>\<open>=\<close> |-- Parse.input Parse.embedded)
    5.27 +      >> Haskell.export_file_cmd);
    5.28 +\<close>
    5.29 +
    5.30 +
    5.31 +section \<open>Source modules\<close>
    5.32 +
    5.33 +generate_haskell_file Library.hs = \<open>
    5.34 +{-  Title:      Tools/Haskell/Library.hs
    5.35 +    Author:     Makarius
    5.36 +    LICENSE:    BSD 3-clause (Isabelle)
    5.37 +
    5.38 +Basic library of Isabelle idioms.
    5.39 +-}
    5.40 +
    5.41 +module Isabelle.Library
    5.42 +  ((|>), (|->), (#>), (#->), fold, fold_rev, single, quote, trim_line)
    5.43 +where
    5.44 +
    5.45 +{- functions -}
    5.46 +
    5.47 +(|>) :: a -> (a -> b) -> b
    5.48 +x |> f = f x
    5.49 +
    5.50 +(|->) :: (a, b) -> (a -> b -> c) -> c
    5.51 +(x, y) |-> f = f x y
    5.52 +
    5.53 +(#>) :: (a -> b) -> (b -> c) -> a -> c
    5.54 +(f #> g) x = x |> f |> g
    5.55 +
    5.56 +(#->) :: (a -> (c, b)) -> (c -> b -> d) -> a -> d
    5.57 +(f #-> g) x  = x |> f |-> g
    5.58 +
    5.59 +
    5.60 +{- lists -}
    5.61 +
    5.62 +fold :: (a -> b -> b) -> [a] -> b -> b
    5.63 +fold _ [] y = y
    5.64 +fold f (x : xs) y = fold f xs (f x y)
    5.65 +
    5.66 +fold_rev :: (a -> b -> b) -> [a] -> b -> b
    5.67 +fold_rev _ [] y = y
    5.68 +fold_rev f (x : xs) y = f x (fold_rev f xs y)
    5.69 +
    5.70 +single :: a -> [a]
    5.71 +single x = [x]
    5.72 +
    5.73 +
    5.74 +{- strings -}
    5.75 +
    5.76 +quote :: String -> String
    5.77 +quote s = "\"" ++ s ++ "\""
    5.78 +
    5.79 +trim_line :: String -> String
    5.80 +trim_line line =
    5.81 +  case reverse line of
    5.82 +    '\n' : '\r' : rest -> reverse rest
    5.83 +    '\n' : rest -> reverse rest
    5.84 +    _ -> line
    5.85 +\<close>
    5.86 +
    5.87 +generate_haskell_file Buffer.hs = \<open>
    5.88 +{-  Title:      Tools/Haskell/Buffer.hs
    5.89 +    Author:     Makarius
    5.90 +    LICENSE:    BSD 3-clause (Isabelle)
    5.91 +
    5.92 +Efficient text buffers.
    5.93 +-}
    5.94 +
    5.95 +module Isabelle.Buffer (T, empty, add, content)
    5.96 +where
    5.97 +
    5.98 +newtype T = Buffer [String]
    5.99 +
   5.100 +empty :: T
   5.101 +empty = Buffer []
   5.102 +
   5.103 +add :: String -> T -> T
   5.104 +add "" buf = buf
   5.105 +add x (Buffer xs) = Buffer (x : xs)
   5.106 +
   5.107 +content :: T -> String
   5.108 +content (Buffer xs) = concat (reverse xs)
   5.109 +\<close>
   5.110 +
   5.111 +generate_haskell_file Properties.hs = \<open>
   5.112 +{-  Title:      Tools/Haskell/Properties.hs
   5.113 +    Author:     Makarius
   5.114 +    LICENSE:    BSD 3-clause (Isabelle)
   5.115 +
   5.116 +Property lists.
   5.117 +-}
   5.118 +
   5.119 +module Isabelle.Properties (Entry, T, defined, get, put, remove)
   5.120 +where
   5.121 +
   5.122 +import qualified Data.List as List
   5.123 +
   5.124 +
   5.125 +type Entry = (String, String)
   5.126 +type T = [Entry]
   5.127 +
   5.128 +defined :: T -> String -> Bool
   5.129 +defined props name = any (\(a, _) -> a == name) props
   5.130 +
   5.131 +get :: T -> String -> Maybe String
   5.132 +get props name = List.lookup name props
   5.133 +
   5.134 +put :: Entry -> T -> T
   5.135 +put entry props = entry : remove (fst entry) props
   5.136 +
   5.137 +remove :: String -> T -> T
   5.138 +remove name props =
   5.139 +  if defined props name then filter (\(a, _) -> a /= name) props
   5.140 +  else props
   5.141 +\<close>
   5.142 +
   5.143 +generate_haskell_file Markup.hs = \<open>
   5.144 +{-  Title:      Haskell/Tools/Markup.hs
   5.145 +    Author:     Makarius
   5.146 +    LICENSE:    BSD 3-clause (Isabelle)
   5.147 +
   5.148 +Quasi-abstract markup elements.
   5.149 +-}
   5.150 +
   5.151 +module Isabelle.Markup (T, empty, is_empty, Output, no_output)
   5.152 +where
   5.153 +
   5.154 +import qualified Isabelle.Properties as Properties
   5.155 +
   5.156 +
   5.157 +type T = (String, Properties.T)
   5.158 +
   5.159 +empty :: T
   5.160 +empty = ("", [])
   5.161 +
   5.162 +is_empty :: T -> Bool
   5.163 +is_empty ("", _) = True
   5.164 +is_empty _ = False
   5.165 +
   5.166 +
   5.167 +type Output = (String, String)
   5.168 +
   5.169 +no_output :: Output
   5.170 +no_output = ("", "")
   5.171 +\<close>
   5.172 +
   5.173 +generate_haskell_file XML.hs = \<open>
   5.174 +{-  Title:      Tools/Haskell/XML.hs
   5.175 +    Author:     Makarius
   5.176 +    LICENSE:    BSD 3-clause (Isabelle)
   5.177 +
   5.178 +Untyped XML trees and representation of ML values.
   5.179 +-}
   5.180 +
   5.181 +module Isabelle.XML (Attributes, Body, Tree(..), wrap_elem, unwrap_elem, content_of)
   5.182 +where
   5.183 +
   5.184 +import qualified Data.List as List
   5.185 +
   5.186 +import Isabelle.Library
   5.187 +import qualified Isabelle.Properties as Properties
   5.188 +import qualified Isabelle.Markup as Markup
   5.189 +import qualified Isabelle.Buffer as Buffer
   5.190 +
   5.191 +
   5.192 +{- types -}
   5.193 +
   5.194 +type Attributes = Properties.T
   5.195 +type Body = [Tree]
   5.196 +data Tree = Elem Markup.T Body | Text String
   5.197 +
   5.198 +
   5.199 +{- wrapped elements -}
   5.200 +
   5.201 +xml_elemN = "xml_elem";
   5.202 +xml_nameN = "xml_name";
   5.203 +xml_bodyN = "xml_body";
   5.204 +
   5.205 +wrap_elem (((a, atts), body1), body2) =
   5.206 +  Elem (xml_elemN, (xml_nameN, a) : atts) (Elem (xml_bodyN, []) body1 : body2)
   5.207 +
   5.208 +unwrap_elem (Elem (name, (n, a) : atts) (Elem (name', atts') body1 : body2)) =
   5.209 +  if name == xml_elemN && n == xml_nameN && name' == xml_bodyN && null atts'
   5.210 +  then Just (((a, atts), body1), body2) else Nothing
   5.211 +unwrap_elem _ = Nothing
   5.212 +
   5.213 +
   5.214 +{- text content -}
   5.215 +
   5.216 +add_content tree =
   5.217 +  case unwrap_elem tree of
   5.218 +    Just (_, ts) -> fold add_content ts
   5.219 +    Nothing ->
   5.220 +      case tree of
   5.221 +        Elem _ ts -> fold add_content ts
   5.222 +        Text s -> Buffer.add s
   5.223 +
   5.224 +content_of body = Buffer.empty |> fold add_content body |> Buffer.content
   5.225 +
   5.226 +
   5.227 +{- string representation -}
   5.228 +
   5.229 +encode '<' = "&lt;"
   5.230 +encode '>' = "&gt;"
   5.231 +encode '&' = "&amp;"
   5.232 +encode '\'' = "&apos;"
   5.233 +encode '\"' = "&quot;"
   5.234 +encode c = [c]
   5.235 +
   5.236 +instance Show Tree where
   5.237 +  show tree =
   5.238 +    Buffer.empty |> show_tree tree |> Buffer.content
   5.239 +    where
   5.240 +      show_tree (Elem (name, atts) []) =
   5.241 +        Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add "/>"
   5.242 +      show_tree (Elem (name, atts) ts) =
   5.243 +        Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add ">" #>
   5.244 +        fold show_tree ts #>
   5.245 +        Buffer.add "</" #> Buffer.add name #> Buffer.add ">"
   5.246 +      show_tree (Text s) = Buffer.add (show_text s)
   5.247 +
   5.248 +      show_elem name atts =
   5.249 +        unwords (name : map (\(a, x) -> a ++ "=\"" ++ show_text x ++ "\"") atts)
   5.250 +
   5.251 +      show_text = concatMap encode
   5.252 +\<close>
   5.253 +
   5.254 +generate_haskell_file YXML.hs = \<open>
   5.255 +{-  Title:      Tools/Haskell/YXML.hs
   5.256 +    Author:     Makarius
   5.257 +    LICENSE:    BSD 3-clause (Isabelle)
   5.258 +
   5.259 +Efficient text representation of XML trees.  Suitable for direct
   5.260 +inlining into plain text.
   5.261 +-}
   5.262 +
   5.263 +module Isabelle.YXML (charX, charY, strX, strY, detect,
   5.264 +  buffer_body, buffer, string_of_body, string_of, parse_body, parse)
   5.265 +where
   5.266 +
   5.267 +import qualified Data.Char as Char
   5.268 +import qualified Data.List as List
   5.269 +
   5.270 +import Isabelle.Library
   5.271 +import qualified Isabelle.Markup as Markup
   5.272 +import qualified Isabelle.XML as XML
   5.273 +import qualified Isabelle.Buffer as Buffer
   5.274 +
   5.275 +
   5.276 +{- markers -}
   5.277 +
   5.278 +charX, charY :: Char
   5.279 +charX = Char.chr 5
   5.280 +charY = Char.chr 6
   5.281 +
   5.282 +strX, strY, strXY, strXYX :: String
   5.283 +strX = [charX]
   5.284 +strY = [charY]
   5.285 +strXY = strX ++ strY
   5.286 +strXYX = strXY ++ strX
   5.287 +
   5.288 +detect :: String -> Bool
   5.289 +detect = any (\c -> c == charX || c == charY)
   5.290 +
   5.291 +
   5.292 +{- output -}
   5.293 +
   5.294 +buffer_attrib (a, x) =
   5.295 +  Buffer.add strY #> Buffer.add a #> Buffer.add "=" #> Buffer.add x
   5.296 +
   5.297 +buffer_body :: XML.Body -> Buffer.T -> Buffer.T
   5.298 +buffer_body = fold buffer
   5.299 +
   5.300 +buffer :: XML.Tree -> Buffer.T -> Buffer.T
   5.301 +buffer (XML.Elem (name, atts) ts) =
   5.302 +  Buffer.add strXY #> Buffer.add name #> fold buffer_attrib atts #> Buffer.add strX #>
   5.303 +  buffer_body ts #>
   5.304 +  Buffer.add strXYX
   5.305 +buffer (XML.Text s) = Buffer.add s
   5.306 +
   5.307 +string_of_body :: XML.Body -> String
   5.308 +string_of_body body = Buffer.empty |> buffer_body body |> Buffer.content
   5.309 +
   5.310 +string_of :: XML.Tree -> String
   5.311 +string_of = string_of_body . single
   5.312 +
   5.313 +
   5.314 +{- parse -}
   5.315 +
   5.316 +-- split: fields or non-empty tokens
   5.317 +
   5.318 +split :: Bool -> Char -> String -> [String]
   5.319 +split _ _ [] = []
   5.320 +split fields sep str = splitting str
   5.321 +  where
   5.322 +    splitting rest =
   5.323 +      case span (/= sep) rest of
   5.324 +        (_, []) -> cons rest []
   5.325 +        (prfx, _ : rest') -> cons prfx (splitting rest')
   5.326 +    cons item = if fields || not (null item) then (:) item else id
   5.327 +
   5.328 +
   5.329 +-- structural errors
   5.330 +
   5.331 +err msg = error ("Malformed YXML: " ++ msg)
   5.332 +err_attribute = err "bad attribute"
   5.333 +err_element = err "bad element"
   5.334 +err_unbalanced "" = err "unbalanced element"
   5.335 +err_unbalanced name = err ("unbalanced element " ++ quote name)
   5.336 +
   5.337 +
   5.338 +-- stack operations
   5.339 +
   5.340 +add x ((elem, body) : pending) = (elem, x : body) : pending
   5.341 +
   5.342 +push "" _ _ = err_element
   5.343 +push name atts pending = ((name, atts), []) : pending
   5.344 +
   5.345 +pop ((("", _), _) : _) = err_unbalanced ""
   5.346 +pop ((markup, body) : pending) = add (XML.Elem markup (reverse body)) pending
   5.347 +
   5.348 +
   5.349 +-- parsing
   5.350 +
   5.351 +parse_attrib s =
   5.352 +  case List.elemIndex '=' s of
   5.353 +    Just i | i > 0 -> (take i s, drop (i + 1) s)
   5.354 +    _ -> err_attribute
   5.355 +
   5.356 +parse_chunk ["", ""] = pop
   5.357 +parse_chunk ("" : name : atts) = push name (map parse_attrib atts)
   5.358 +parse_chunk txts = fold (add . XML.Text) txts
   5.359 +
   5.360 +parse_body :: String -> XML.Body
   5.361 +parse_body source =
   5.362 +  case fold parse_chunk chunks [(("", []), [])] of
   5.363 +    [(("", _), result)] -> reverse result
   5.364 +    ((name, _), _) : _ -> err_unbalanced name
   5.365 +  where chunks = split False charX source |> map (split True charY)
   5.366 +
   5.367 +parse :: String -> XML.Tree
   5.368 +parse source =
   5.369 +  case parse_body source of
   5.370 +    [result] -> result
   5.371 +    [] -> XML.Text ""
   5.372 +    _ -> err "multiple results"
   5.373 +\<close>
   5.374 +
   5.375 +end
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Tools/Haskell/Library.hs	Sat Nov 03 20:24:56 2018 +0100
     6.3 @@ -0,0 +1,53 @@
     6.4 +{- generated by Isabelle -}
     6.5 +
     6.6 +{-  Title:      Tools/Haskell/Library.hs
     6.7 +    Author:     Makarius
     6.8 +    LICENSE:    BSD 3-clause (Isabelle)
     6.9 +
    6.10 +Basic library of Isabelle idioms.
    6.11 +-}
    6.12 +
    6.13 +module Isabelle.Library
    6.14 +  ((|>), (|->), (#>), (#->), fold, fold_rev, single, quote, trim_line)
    6.15 +where
    6.16 +
    6.17 +{- functions -}
    6.18 +
    6.19 +(|>) :: a -> (a -> b) -> b
    6.20 +x |> f = f x
    6.21 +
    6.22 +(|->) :: (a, b) -> (a -> b -> c) -> c
    6.23 +(x, y) |-> f = f x y
    6.24 +
    6.25 +(#>) :: (a -> b) -> (b -> c) -> a -> c
    6.26 +(f #> g) x = x |> f |> g
    6.27 +
    6.28 +(#->) :: (a -> (c, b)) -> (c -> b -> d) -> a -> d
    6.29 +(f #-> g) x  = x |> f |-> g
    6.30 +
    6.31 +
    6.32 +{- lists -}
    6.33 +
    6.34 +fold :: (a -> b -> b) -> [a] -> b -> b
    6.35 +fold _ [] y = y
    6.36 +fold f (x : xs) y = fold f xs (f x y)
    6.37 +
    6.38 +fold_rev :: (a -> b -> b) -> [a] -> b -> b
    6.39 +fold_rev _ [] y = y
    6.40 +fold_rev f (x : xs) y = f x (fold_rev f xs y)
    6.41 +
    6.42 +single :: a -> [a]
    6.43 +single x = [x]
    6.44 +
    6.45 +
    6.46 +{- strings -}
    6.47 +
    6.48 +quote :: String -> String
    6.49 +quote s = "\"" ++ s ++ "\""
    6.50 +
    6.51 +trim_line :: String -> String
    6.52 +trim_line line =
    6.53 +  case reverse line of
    6.54 +    '\n' : '\r' : rest -> reverse rest
    6.55 +    '\n' : rest -> reverse rest
    6.56 +    _ -> line
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Tools/Haskell/Markup.hs	Sat Nov 03 20:24:56 2018 +0100
     7.3 @@ -0,0 +1,29 @@
     7.4 +{- generated by Isabelle -}
     7.5 +
     7.6 +{-  Title:      Haskell/Tools/Markup.hs
     7.7 +    Author:     Makarius
     7.8 +    LICENSE:    BSD 3-clause (Isabelle)
     7.9 +
    7.10 +Quasi-abstract markup elements.
    7.11 +-}
    7.12 +
    7.13 +module Isabelle.Markup (T, empty, is_empty, Output, no_output)
    7.14 +where
    7.15 +
    7.16 +import qualified Isabelle.Properties as Properties
    7.17 +
    7.18 +
    7.19 +type T = (String, Properties.T)
    7.20 +
    7.21 +empty :: T
    7.22 +empty = ("", [])
    7.23 +
    7.24 +is_empty :: T -> Bool
    7.25 +is_empty ("", _) = True
    7.26 +is_empty _ = False
    7.27 +
    7.28 +
    7.29 +type Output = (String, String)
    7.30 +
    7.31 +no_output :: Output
    7.32 +no_output = ("", "")
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/Tools/Haskell/Properties.hs	Sat Nov 03 20:24:56 2018 +0100
     8.3 @@ -0,0 +1,31 @@
     8.4 +{- generated by Isabelle -}
     8.5 +
     8.6 +{-  Title:      Tools/Haskell/Properties.hs
     8.7 +    Author:     Makarius
     8.8 +    LICENSE:    BSD 3-clause (Isabelle)
     8.9 +
    8.10 +Property lists.
    8.11 +-}
    8.12 +
    8.13 +module Isabelle.Properties (Entry, T, defined, get, put, remove)
    8.14 +where
    8.15 +
    8.16 +import qualified Data.List as List
    8.17 +
    8.18 +
    8.19 +type Entry = (String, String)
    8.20 +type T = [Entry]
    8.21 +
    8.22 +defined :: T -> String -> Bool
    8.23 +defined props name = any (\(a, _) -> a == name) props
    8.24 +
    8.25 +get :: T -> String -> Maybe String
    8.26 +get props name = List.lookup name props
    8.27 +
    8.28 +put :: Entry -> T -> T
    8.29 +put entry props = entry : remove (fst entry) props
    8.30 +
    8.31 +remove :: String -> T -> T
    8.32 +remove name props =
    8.33 +  if defined props name then filter (\(a, _) -> a /= name) props
    8.34 +  else props
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/Tools/Haskell/XML.hs	Sat Nov 03 20:24:56 2018 +0100
     9.3 @@ -0,0 +1,80 @@
     9.4 +{- generated by Isabelle -}
     9.5 +
     9.6 +{-  Title:      Tools/Haskell/XML.hs
     9.7 +    Author:     Makarius
     9.8 +    LICENSE:    BSD 3-clause (Isabelle)
     9.9 +
    9.10 +Untyped XML trees and representation of ML values.
    9.11 +-}
    9.12 +
    9.13 +module Isabelle.XML (Attributes, Body, Tree(..), wrap_elem, unwrap_elem, content_of)
    9.14 +where
    9.15 +
    9.16 +import qualified Data.List as List
    9.17 +
    9.18 +import Isabelle.Library
    9.19 +import qualified Isabelle.Properties as Properties
    9.20 +import qualified Isabelle.Markup as Markup
    9.21 +import qualified Isabelle.Buffer as Buffer
    9.22 +
    9.23 +
    9.24 +{- types -}
    9.25 +
    9.26 +type Attributes = Properties.T
    9.27 +type Body = [Tree]
    9.28 +data Tree = Elem Markup.T Body | Text String
    9.29 +
    9.30 +
    9.31 +{- wrapped elements -}
    9.32 +
    9.33 +xml_elemN = "xml_elem";
    9.34 +xml_nameN = "xml_name";
    9.35 +xml_bodyN = "xml_body";
    9.36 +
    9.37 +wrap_elem (((a, atts), body1), body2) =
    9.38 +  Elem (xml_elemN, (xml_nameN, a) : atts) (Elem (xml_bodyN, []) body1 : body2)
    9.39 +
    9.40 +unwrap_elem (Elem (name, (n, a) : atts) (Elem (name', atts') body1 : body2)) =
    9.41 +  if name == xml_elemN && n == xml_nameN && name' == xml_bodyN && null atts'
    9.42 +  then Just (((a, atts), body1), body2) else Nothing
    9.43 +unwrap_elem _ = Nothing
    9.44 +
    9.45 +
    9.46 +{- text content -}
    9.47 +
    9.48 +add_content tree =
    9.49 +  case unwrap_elem tree of
    9.50 +    Just (_, ts) -> fold add_content ts
    9.51 +    Nothing ->
    9.52 +      case tree of
    9.53 +        Elem _ ts -> fold add_content ts
    9.54 +        Text s -> Buffer.add s
    9.55 +
    9.56 +content_of body = Buffer.empty |> fold add_content body |> Buffer.content
    9.57 +
    9.58 +
    9.59 +{- string representation -}
    9.60 +
    9.61 +encode '<' = "&lt;"
    9.62 +encode '>' = "&gt;"
    9.63 +encode '&' = "&amp;"
    9.64 +encode '\'' = "&apos;"
    9.65 +encode '\"' = "&quot;"
    9.66 +encode c = [c]
    9.67 +
    9.68 +instance Show Tree where
    9.69 +  show tree =
    9.70 +    Buffer.empty |> show_tree tree |> Buffer.content
    9.71 +    where
    9.72 +      show_tree (Elem (name, atts) []) =
    9.73 +        Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add "/>"
    9.74 +      show_tree (Elem (name, atts) ts) =
    9.75 +        Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add ">" #>
    9.76 +        fold show_tree ts #>
    9.77 +        Buffer.add "</" #> Buffer.add name #> Buffer.add ">"
    9.78 +      show_tree (Text s) = Buffer.add (show_text s)
    9.79 +
    9.80 +      show_elem name atts =
    9.81 +        unwords (name : map (\(a, x) -> a ++ "=\"" ++ show_text x ++ "\"") atts)
    9.82 +
    9.83 +      show_text = concatMap encode
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/Tools/Haskell/YXML.hs	Sat Nov 03 20:24:56 2018 +0100
    10.3 @@ -0,0 +1,120 @@
    10.4 +{- generated by Isabelle -}
    10.5 +
    10.6 +{-  Title:      Tools/Haskell/YXML.hs
    10.7 +    Author:     Makarius
    10.8 +    LICENSE:    BSD 3-clause (Isabelle)
    10.9 +
   10.10 +Efficient text representation of XML trees.  Suitable for direct
   10.11 +inlining into plain text.
   10.12 +-}
   10.13 +
   10.14 +module Isabelle.YXML (charX, charY, strX, strY, detect,
   10.15 +  buffer_body, buffer, string_of_body, string_of, parse_body, parse)
   10.16 +where
   10.17 +
   10.18 +import qualified Data.Char as Char
   10.19 +import qualified Data.List as List
   10.20 +
   10.21 +import Isabelle.Library
   10.22 +import qualified Isabelle.Markup as Markup
   10.23 +import qualified Isabelle.XML as XML
   10.24 +import qualified Isabelle.Buffer as Buffer
   10.25 +
   10.26 +
   10.27 +{- markers -}
   10.28 +
   10.29 +charX, charY :: Char
   10.30 +charX = Char.chr 5
   10.31 +charY = Char.chr 6
   10.32 +
   10.33 +strX, strY, strXY, strXYX :: String
   10.34 +strX = [charX]
   10.35 +strY = [charY]
   10.36 +strXY = strX ++ strY
   10.37 +strXYX = strXY ++ strX
   10.38 +
   10.39 +detect :: String -> Bool
   10.40 +detect = any (\c -> c == charX || c == charY)
   10.41 +
   10.42 +
   10.43 +{- output -}
   10.44 +
   10.45 +buffer_attrib (a, x) =
   10.46 +  Buffer.add strY #> Buffer.add a #> Buffer.add "=" #> Buffer.add x
   10.47 +
   10.48 +buffer_body :: XML.Body -> Buffer.T -> Buffer.T
   10.49 +buffer_body = fold buffer
   10.50 +
   10.51 +buffer :: XML.Tree -> Buffer.T -> Buffer.T
   10.52 +buffer (XML.Elem (name, atts) ts) =
   10.53 +  Buffer.add strXY #> Buffer.add name #> fold buffer_attrib atts #> Buffer.add strX #>
   10.54 +  buffer_body ts #>
   10.55 +  Buffer.add strXYX
   10.56 +buffer (XML.Text s) = Buffer.add s
   10.57 +
   10.58 +string_of_body :: XML.Body -> String
   10.59 +string_of_body body = Buffer.empty |> buffer_body body |> Buffer.content
   10.60 +
   10.61 +string_of :: XML.Tree -> String
   10.62 +string_of = string_of_body . single
   10.63 +
   10.64 +
   10.65 +{- parse -}
   10.66 +
   10.67 +-- split: fields or non-empty tokens
   10.68 +
   10.69 +split :: Bool -> Char -> String -> [String]
   10.70 +split _ _ [] = []
   10.71 +split fields sep str = splitting str
   10.72 +  where
   10.73 +    splitting rest =
   10.74 +      case span (/= sep) rest of
   10.75 +        (_, []) -> cons rest []
   10.76 +        (prfx, _ : rest') -> cons prfx (splitting rest')
   10.77 +    cons item = if fields || not (null item) then (:) item else id
   10.78 +
   10.79 +
   10.80 +-- structural errors
   10.81 +
   10.82 +err msg = error ("Malformed YXML: " ++ msg)
   10.83 +err_attribute = err "bad attribute"
   10.84 +err_element = err "bad element"
   10.85 +err_unbalanced "" = err "unbalanced element"
   10.86 +err_unbalanced name = err ("unbalanced element " ++ quote name)
   10.87 +
   10.88 +
   10.89 +-- stack operations
   10.90 +
   10.91 +add x ((elem, body) : pending) = (elem, x : body) : pending
   10.92 +
   10.93 +push "" _ _ = err_element
   10.94 +push name atts pending = ((name, atts), []) : pending
   10.95 +
   10.96 +pop ((("", _), _) : _) = err_unbalanced ""
   10.97 +pop ((markup, body) : pending) = add (XML.Elem markup (reverse body)) pending
   10.98 +
   10.99 +
  10.100 +-- parsing
  10.101 +
  10.102 +parse_attrib s =
  10.103 +  case List.elemIndex '=' s of
  10.104 +    Just i | i > 0 -> (take i s, drop (i + 1) s)
  10.105 +    _ -> err_attribute
  10.106 +
  10.107 +parse_chunk ["", ""] = pop
  10.108 +parse_chunk ("" : name : atts) = push name (map parse_attrib atts)
  10.109 +parse_chunk txts = fold (add . XML.Text) txts
  10.110 +
  10.111 +parse_body :: String -> XML.Body
  10.112 +parse_body source =
  10.113 +  case fold parse_chunk chunks [(("", []), [])] of
  10.114 +    [(("", _), result)] -> reverse result
  10.115 +    ((name, _), _) : _ -> err_unbalanced name
  10.116 +  where chunks = split False charX source |> map (split True charY)
  10.117 +
  10.118 +parse :: String -> XML.Tree
  10.119 +parse source =
  10.120 +  case parse_body source of
  10.121 +    [result] -> result
  10.122 +    [] -> XML.Text ""
  10.123 +    _ -> err "multiple results"
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/Tools/Haskell/haskell.ML	Sat Nov 03 20:24:56 2018 +0100
    11.3 @@ -0,0 +1,56 @@
    11.4 +(*  Title:      Tools/Haskell/haskell.ml
    11.5 +    Author:     Makarius
    11.6 +
    11.7 +Support for Isabelle tools in Haskell.
    11.8 +*)
    11.9 +
   11.10 +signature HASKELL =
   11.11 +sig
   11.12 +  val generate_file_cmd: (string * Position.T) * Input.source ->
   11.13 +    Toplevel.transition -> Toplevel.transition
   11.14 +  val export_file_cmd: string * Input.source ->
   11.15 +    Toplevel.transition -> Toplevel.transition
   11.16 +  val source_modules: Path.T list
   11.17 +end;
   11.18 +
   11.19 +structure Haskell: HASKELL =
   11.20 +struct
   11.21 +
   11.22 +(* commands *)
   11.23 +
   11.24 +val header = "{- generated by Isabelle -}\n";
   11.25 +
   11.26 +fun generate_file_cmd (file, source) =
   11.27 +  Toplevel.keep (fn state =>
   11.28 +    let
   11.29 +      val ctxt = Toplevel.context_of state;
   11.30 +      val thy = Toplevel.theory_of state;
   11.31 +
   11.32 +      val path = Resources.check_path ctxt (Resources.master_directory thy) file;
   11.33 +      val text = header ^ GHC.read_source ctxt source;
   11.34 +      val _ = Isabelle_System.mkdirs (Path.dir (Path.expand path));
   11.35 +      val _ = File.generate path text;
   11.36 +    in () end);
   11.37 +
   11.38 +fun export_file_cmd (name, source) =
   11.39 +  Toplevel.keep (fn state =>
   11.40 +    let
   11.41 +      val ctxt = Toplevel.context_of state;
   11.42 +      val thy = Toplevel.theory_of state;
   11.43 +
   11.44 +      val text = header ^ GHC.read_source ctxt source;
   11.45 +      val _ = Export.export thy name [text];
   11.46 +    in () end);
   11.47 +
   11.48 +
   11.49 +(* source modules *)
   11.50 +
   11.51 +val source_modules =
   11.52 + [\<^file>\<open>~~/src/Tools/Haskell/Library.hs\<close>,
   11.53 +  \<^file>\<open>~~/src/Tools/Haskell/Buffer.hs\<close>,
   11.54 +  \<^file>\<open>~~/src/Tools/Haskell/Properties.hs\<close>,
   11.55 +  \<^file>\<open>~~/src/Tools/Haskell/Markup.hs\<close>,
   11.56 +  \<^file>\<open>~~/src/Tools/Haskell/XML.hs\<close>,
   11.57 +  \<^file>\<open>~~/src/Tools/Haskell/YXML.hs\<close>];
   11.58 +
   11.59 +end;
    12.1 --- a/src/Tools/ROOT	Thu Nov 01 18:19:33 2018 +0000
    12.2 +++ b/src/Tools/ROOT	Sat Nov 03 20:24:56 2018 +0100
    12.3 @@ -8,3 +8,9 @@
    12.4  session SML in SML = Pure +
    12.5    theories
    12.6      Examples
    12.7 +
    12.8 +session Haskell in Haskell = Pure +
    12.9 +  theories
   12.10 +    Haskell
   12.11 +  theories [condition = ISABELLE_GHC]
   12.12 +    Build