support for Isabelle tools in Haskell;
authorwenzelm
Sat Nov 03 19:33:15 2018 +0100 (6 months ago)
changeset 69225bf2fecda8383
parent 69224 fe9d746b273e
child 69226 68f5dc2275ac
support for Isabelle tools in Haskell;
src/Tools/Haskell/Buffer.hs
src/Tools/Haskell/Build.thy
src/Tools/Haskell/Haskell.thy
src/Tools/Haskell/Library.hs
src/Tools/Haskell/Markup.hs
src/Tools/Haskell/Properties.hs
src/Tools/Haskell/XML.hs
src/Tools/Haskell/YXML.hs
src/Tools/Haskell/haskell.ML
src/Tools/ROOT
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/Haskell/Buffer.hs	Sat Nov 03 19:33:15 2018 +0100
     1.3 @@ -0,0 +1,22 @@
     1.4 +{- GENERATED by Isabelle! -}
     1.5 +{-  Title:      Tools/Haskell/Buffer.hs
     1.6 +    Author:     Makarius
     1.7 +    LICENSE:    BSD 3-clause (Isabelle)
     1.8 +
     1.9 +Efficient text buffers.
    1.10 +-}
    1.11 +
    1.12 +module Isabelle.Buffer (T, empty, add, content)
    1.13 +where
    1.14 +
    1.15 +newtype T = Buffer [String]
    1.16 +
    1.17 +empty :: T
    1.18 +empty = Buffer []
    1.19 +
    1.20 +add :: String -> T -> T
    1.21 +add "" buf = buf
    1.22 +add x (Buffer xs) = Buffer (x : xs)
    1.23 +
    1.24 +content :: T -> String
    1.25 +content (Buffer xs) = concat (reverse xs)
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Tools/Haskell/Build.thy	Sat Nov 03 19:33:15 2018 +0100
     2.3 @@ -0,0 +1,24 @@
     2.4 +(*  Title:      Tools/Haskell/Build.thy
     2.5 +    Author:     Makarius
     2.6 +*)
     2.7 +
     2.8 +section \<open>Build Isabelle/Haskell modules\<close>
     2.9 +
    2.10 +theory Build imports Haskell
    2.11 +begin
    2.12 +
    2.13 +ML_command \<open>
    2.14 +  Isabelle_System.with_tmp_dir "ghc" (fn dir =>
    2.15 +    let
    2.16 +      val (out, rc) =
    2.17 +        Isabelle_System.bash_output
    2.18 +         (cat_lines
    2.19 +           ["set -e",
    2.20 +            "cd " ^ File.bash_path dir,
    2.21 +            "cp " ^ File.bash_paths Haskell.source_modules ^ " .",
    2.22 +            "\"$ISABELLE_GHC\" " ^ File.bash_paths (map Path.base Haskell.source_modules)]);
    2.23 +    in if rc = 0 then writeln out else error out end
    2.24 +  )
    2.25 +\<close>
    2.26 +
    2.27 +end
     3.1 --- a/src/Tools/Haskell/Haskell.thy	Sat Nov 03 19:31:50 2018 +0100
     3.2 +++ b/src/Tools/Haskell/Haskell.thy	Sat Nov 03 19:33:15 2018 +0100
     3.3 @@ -1,42 +1,373 @@
     3.4  (*  Title:      Tools/Haskell/Haskell.thy
     3.5      Author:     Makarius
     3.6 +
     3.7 +Support for Isabelle tools in Haskell.
     3.8  *)
     3.9  
    3.10 -section \<open>Support for Isabelle tool development in Haskell\<close>
    3.11 -
    3.12  theory Haskell
    3.13    imports Pure
    3.14    keywords "generate_haskell_file" "export_haskell_file" :: thy_decl
    3.15  begin
    3.16  
    3.17 +ML_file "haskell.ML"
    3.18 +
    3.19 +
    3.20 +section \<open>Commands\<close>
    3.21 +
    3.22  ML \<open>
    3.23    Outer_Syntax.command \<^command_keyword>\<open>generate_haskell_file\<close> "generate Haskell file"
    3.24 -    (Parse.position Parse.path -- (\<^keyword>\<open>=\<close> |-- Parse.input Parse.embedded) >>
    3.25 -      (fn (file, source) =>
    3.26 -        Toplevel.keep (fn state =>
    3.27 -          let
    3.28 -            val ctxt = Toplevel.context_of state;
    3.29 -            val thy = Toplevel.theory_of state;
    3.30 +    (Parse.position Parse.path -- (\<^keyword>\<open>=\<close> |-- Parse.input Parse.embedded)
    3.31 +      >> Haskell.generate_file_cmd);
    3.32 +
    3.33 +  Outer_Syntax.command \<^command_keyword>\<open>export_haskell_file\<close> "export Haskell file"
    3.34 +    (Parse.name -- (\<^keyword>\<open>=\<close> |-- Parse.input Parse.embedded)
    3.35 +      >> Haskell.export_file_cmd);
    3.36 +\<close>
    3.37 +
    3.38 +
    3.39 +section \<open>Source modules\<close>
    3.40 +
    3.41 +generate_haskell_file Library.hs =
    3.42 +\<open>{-  Title:      Tools/Haskell/Library.hs
    3.43 +    Author:     Makarius
    3.44 +    LICENSE:    BSD 3-clause (Isabelle)
    3.45 +
    3.46 +Basic library of Isabelle idioms.
    3.47 +-}
    3.48 +
    3.49 +module Isabelle.Library
    3.50 +  ((|>), (|->), (#>), (#->), fold, fold_rev, single, quote, trim_line)
    3.51 +where
    3.52 +
    3.53 +{- functions -}
    3.54 +
    3.55 +(|>) :: a -> (a -> b) -> b
    3.56 +x |> f = f x
    3.57 +
    3.58 +(|->) :: (a, b) -> (a -> b -> c) -> c
    3.59 +(x, y) |-> f = f x y
    3.60 +
    3.61 +(#>) :: (a -> b) -> (b -> c) -> a -> c
    3.62 +(f #> g) x = x |> f |> g
    3.63 +
    3.64 +(#->) :: (a -> (c, b)) -> (c -> b -> d) -> a -> d
    3.65 +(f #-> g) x  = x |> f |-> g
    3.66 +
    3.67 +
    3.68 +{- lists -}
    3.69 +
    3.70 +fold :: (a -> b -> b) -> [a] -> b -> b
    3.71 +fold _ [] y = y
    3.72 +fold f (x : xs) y = fold f xs (f x y)
    3.73 +
    3.74 +fold_rev :: (a -> b -> b) -> [a] -> b -> b
    3.75 +fold_rev _ [] y = y
    3.76 +fold_rev f (x : xs) y = f x (fold_rev f xs y)
    3.77 +
    3.78 +single :: a -> [a]
    3.79 +single x = [x]
    3.80 +
    3.81 +
    3.82 +{- strings -}
    3.83 +
    3.84 +quote :: String -> String
    3.85 +quote s = "\"" ++ s ++ "\""
    3.86 +
    3.87 +trim_line :: String -> String
    3.88 +trim_line line =
    3.89 +  case reverse line of
    3.90 +    '\n' : '\r' : rest -> reverse rest
    3.91 +    '\n' : rest -> reverse rest
    3.92 +    _ -> line
    3.93 +\<close>
    3.94 +
    3.95 +generate_haskell_file Buffer.hs =
    3.96 +\<open>{-  Title:      Tools/Haskell/Buffer.hs
    3.97 +    Author:     Makarius
    3.98 +    LICENSE:    BSD 3-clause (Isabelle)
    3.99 +
   3.100 +Efficient text buffers.
   3.101 +-}
   3.102  
   3.103 -            val path = Resources.check_path ctxt (Resources.master_directory thy) file;
   3.104 -            val text = GHC.read_source ctxt source;
   3.105 -            val _ = Isabelle_System.mkdirs (Path.dir (Path.expand path));
   3.106 -            val _ = if try File.read path = SOME text then () else File.write path text;
   3.107 -          in () end)));
   3.108 +module Isabelle.Buffer (T, empty, add, content)
   3.109 +where
   3.110 +
   3.111 +newtype T = Buffer [String]
   3.112 +
   3.113 +empty :: T
   3.114 +empty = Buffer []
   3.115 +
   3.116 +add :: String -> T -> T
   3.117 +add "" buf = buf
   3.118 +add x (Buffer xs) = Buffer (x : xs)
   3.119 +
   3.120 +content :: T -> String
   3.121 +content (Buffer xs) = concat (reverse xs)
   3.122 +\<close>
   3.123 +
   3.124 +generate_haskell_file Properties.hs =
   3.125 +\<open>{-  Title:      Tools/Haskell/Properties.hs
   3.126 +    Author:     Makarius
   3.127 +    LICENSE:    BSD 3-clause (Isabelle)
   3.128 +
   3.129 +Property lists.
   3.130 +-}
   3.131 +
   3.132 +module Isabelle.Properties (Entry, T, defined, get, put, remove)
   3.133 +where
   3.134 +
   3.135 +import qualified Data.List as List
   3.136 +
   3.137 +
   3.138 +type Entry = (String, String)
   3.139 +type T = [Entry]
   3.140 +
   3.141 +defined :: T -> String -> Bool
   3.142 +defined props name = any (\(a, _) -> a == name) props
   3.143 +
   3.144 +get :: T -> String -> Maybe String
   3.145 +get props name = List.lookup name props
   3.146 +
   3.147 +put :: Entry -> T -> T
   3.148 +put entry props = entry : remove (fst entry) props
   3.149 +
   3.150 +remove :: String -> T -> T
   3.151 +remove name props =
   3.152 +  if defined props name then filter (\(a, _) -> a /= name) props
   3.153 +  else props
   3.154 +\<close>
   3.155 +
   3.156 +generate_haskell_file Markup.hs =
   3.157 +\<open>{-  Title:      Haskell/Tools/Markup.hs
   3.158 +    Author:     Makarius
   3.159 +    LICENSE:    BSD 3-clause (Isabelle)
   3.160 +
   3.161 +Quasi-abstract markup elements.
   3.162 +-}
   3.163 +
   3.164 +module Isabelle.Markup (T, empty, is_empty, Output, no_output)
   3.165 +where
   3.166 +
   3.167 +import qualified Isabelle.Properties as Properties
   3.168 +
   3.169 +
   3.170 +type T = (String, Properties.T)
   3.171 +
   3.172 +empty :: T
   3.173 +empty = ("", [])
   3.174 +
   3.175 +is_empty :: T -> Bool
   3.176 +is_empty ("", _) = True
   3.177 +is_empty _ = False
   3.178 +
   3.179 +
   3.180 +type Output = (String, String)
   3.181 +
   3.182 +no_output :: Output
   3.183 +no_output = ("", "")
   3.184  \<close>
   3.185  
   3.186 -ML \<open>
   3.187 -  Outer_Syntax.command \<^command_keyword>\<open>export_haskell_file\<close> "export Haskell file"
   3.188 -    (Parse.name -- (\<^keyword>\<open>=\<close> |-- Parse.input Parse.embedded) >>
   3.189 -      (fn (name, source) =>
   3.190 -        Toplevel.keep (fn state =>
   3.191 -          let
   3.192 -            val ctxt = Toplevel.context_of state;
   3.193 -            val thy = Toplevel.theory_of state;
   3.194 +generate_haskell_file XML.hs =
   3.195 +\<open>{-  Title:      Tools/Haskell/XML.hs
   3.196 +    Author:     Makarius
   3.197 +    LICENSE:    BSD 3-clause (Isabelle)
   3.198 +
   3.199 +Untyped XML trees and representation of ML values.
   3.200 +-}
   3.201 +
   3.202 +module Isabelle.XML (Attributes, Body, Tree(..), wrap_elem, unwrap_elem, content_of)
   3.203 +where
   3.204 +
   3.205 +import qualified Data.List as List
   3.206 +
   3.207 +import Isabelle.Library
   3.208 +import qualified Isabelle.Properties as Properties
   3.209 +import qualified Isabelle.Markup as Markup
   3.210 +import qualified Isabelle.Buffer as Buffer
   3.211 +
   3.212 +
   3.213 +{- types -}
   3.214 +
   3.215 +type Attributes = Properties.T
   3.216 +type Body = [Tree]
   3.217 +data Tree = Elem Markup.T Body | Text String
   3.218 +
   3.219 +
   3.220 +{- wrapped elements -}
   3.221 +
   3.222 +xml_elemN = "xml_elem";
   3.223 +xml_nameN = "xml_name";
   3.224 +xml_bodyN = "xml_body";
   3.225 +
   3.226 +wrap_elem (((a, atts), body1), body2) =
   3.227 +  Elem (xml_elemN, (xml_nameN, a) : atts) (Elem (xml_bodyN, []) body1 : body2)
   3.228 +
   3.229 +unwrap_elem (Elem (name, (n, a) : atts) (Elem (name', atts') body1 : body2)) =
   3.230 +  if name == xml_elemN && n == xml_nameN && name' == xml_bodyN && null atts'
   3.231 +  then Just (((a, atts), body1), body2) else Nothing
   3.232 +unwrap_elem _ = Nothing
   3.233 +
   3.234 +
   3.235 +{- text content -}
   3.236 +
   3.237 +add_content tree =
   3.238 +  case unwrap_elem tree of
   3.239 +    Just (_, ts) -> fold add_content ts
   3.240 +    Nothing ->
   3.241 +      case tree of
   3.242 +        Elem _ ts -> fold add_content ts
   3.243 +        Text s -> Buffer.add s
   3.244 +
   3.245 +content_of body = Buffer.empty |> fold add_content body |> Buffer.content
   3.246 +
   3.247 +
   3.248 +{- string representation -}
   3.249 +
   3.250 +encode '<' = "&lt;"
   3.251 +encode '>' = "&gt;"
   3.252 +encode '&' = "&amp;"
   3.253 +encode '\'' = "&apos;"
   3.254 +encode '\"' = "&quot;"
   3.255 +encode c = [c]
   3.256 +
   3.257 +instance Show Tree where
   3.258 +  show tree =
   3.259 +    Buffer.empty |> show_tree tree |> Buffer.content
   3.260 +    where
   3.261 +      show_tree (Elem (name, atts) []) =
   3.262 +        Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add "/>"
   3.263 +      show_tree (Elem (name, atts) ts) =
   3.264 +        Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add ">" #>
   3.265 +        fold show_tree ts #>
   3.266 +        Buffer.add "</" #> Buffer.add name #> Buffer.add ">"
   3.267 +      show_tree (Text s) = Buffer.add (show_text s)
   3.268 +
   3.269 +      show_elem name atts =
   3.270 +        unwords (name : map (\(a, x) -> a ++ "=\"" ++ show_text x ++ "\"") atts)
   3.271 +
   3.272 +      show_text = concatMap encode
   3.273 +\<close>
   3.274 +
   3.275 +generate_haskell_file YXML.hs =
   3.276 +\<open>{-  Title:      Tools/Haskell/YXML.hs
   3.277 +    Author:     Makarius
   3.278 +    LICENSE:    BSD 3-clause (Isabelle)
   3.279 +
   3.280 +Efficient text representation of XML trees.  Suitable for direct
   3.281 +inlining into plain text.
   3.282 +-}
   3.283 +
   3.284 +
   3.285 +module Isabelle.YXML (charX, charY, strX, strY, detect,
   3.286 +  buffer_body, buffer, string_of_body, string_of, parse_body, parse)
   3.287 +where
   3.288 +
   3.289 +import qualified Data.Char as Char
   3.290 +import qualified Data.List as List
   3.291  
   3.292 -            val text = GHC.read_source ctxt source;
   3.293 -            val _ = Export.export thy name [text];
   3.294 -          in () end)));
   3.295 +import Isabelle.Library
   3.296 +import qualified Isabelle.Markup as Markup
   3.297 +import qualified Isabelle.XML as XML
   3.298 +import qualified Isabelle.Buffer as Buffer
   3.299 +
   3.300 +
   3.301 +{- markers -}
   3.302 +
   3.303 +charX, charY :: Char
   3.304 +charX = Char.chr 5
   3.305 +charY = Char.chr 6
   3.306 +
   3.307 +strX, strY, strXY, strXYX :: String
   3.308 +strX = [charX]
   3.309 +strY = [charY]
   3.310 +strXY = strX ++ strY
   3.311 +strXYX = strXY ++ strX
   3.312 +
   3.313 +detect :: String -> Bool
   3.314 +detect = any (\c -> c == charX || c == charY)
   3.315 +
   3.316 +
   3.317 +{- output -}
   3.318 +
   3.319 +buffer_attrib (a, x) =
   3.320 +  Buffer.add strY #> Buffer.add a #> Buffer.add "=" #> Buffer.add x
   3.321 +
   3.322 +buffer_body :: XML.Body -> Buffer.T -> Buffer.T
   3.323 +buffer_body = fold buffer
   3.324 +
   3.325 +buffer :: XML.Tree -> Buffer.T -> Buffer.T
   3.326 +buffer (XML.Elem (name, atts) ts) =
   3.327 +  Buffer.add strXY #> Buffer.add name #> fold buffer_attrib atts #> Buffer.add strX #>
   3.328 +  buffer_body ts #>
   3.329 +  Buffer.add strXYX
   3.330 +buffer (XML.Text s) = Buffer.add s
   3.331 +
   3.332 +string_of_body :: XML.Body -> String
   3.333 +string_of_body body = Buffer.empty |> buffer_body body |> Buffer.content
   3.334 +
   3.335 +string_of :: XML.Tree -> String
   3.336 +string_of = string_of_body . single
   3.337 +
   3.338 +
   3.339 +{- parse -}
   3.340 +
   3.341 +-- split: fields or non-empty tokens
   3.342 +
   3.343 +split :: Bool -> Char -> String -> [String]
   3.344 +split _ _ [] = []
   3.345 +split fields sep str = splitting str
   3.346 +  where
   3.347 +    splitting rest =
   3.348 +      case span (/= sep) rest of
   3.349 +        (_, []) -> cons rest []
   3.350 +        (prfx, _ : rest') -> cons prfx (splitting rest')
   3.351 +    cons item = if fields || not (null item) then (:) item else id
   3.352 +
   3.353 +
   3.354 +-- structural errors
   3.355 +
   3.356 +err msg = error ("Malformed YXML: " ++ msg)
   3.357 +err_attribute = err "bad attribute"
   3.358 +err_element = err "bad element"
   3.359 +err_unbalanced "" = err "unbalanced element"
   3.360 +err_unbalanced name = err ("unbalanced element " ++ quote name)
   3.361 +
   3.362 +
   3.363 +-- stack operations
   3.364 +
   3.365 +add x ((elem, body) : pending) = (elem, x : body) : pending
   3.366 +
   3.367 +push "" _ _ = err_element
   3.368 +push name atts pending = ((name, atts), []) : pending
   3.369 +
   3.370 +pop ((("", _), _) : _) = err_unbalanced ""
   3.371 +pop ((markup, body) : pending) = add (XML.Elem markup (reverse body)) pending
   3.372 +
   3.373 +
   3.374 +-- parsing
   3.375 +
   3.376 +parse_attrib s =
   3.377 +  case List.elemIndex '=' s of
   3.378 +    Just i | i > 0 -> (take i s, drop (i + 1) s)
   3.379 +    _ -> err_attribute
   3.380 +
   3.381 +parse_chunk ["", ""] = pop
   3.382 +parse_chunk ("" : name : atts) = push name (map parse_attrib atts)
   3.383 +parse_chunk txts = fold (add . XML.Text) txts
   3.384 +
   3.385 +parse_body :: String -> XML.Body
   3.386 +parse_body source =
   3.387 +  case fold parse_chunk chunks [(("", []), [])] of
   3.388 +    [(("", _), result)] -> reverse result
   3.389 +    ((name, _), _) : _ -> err_unbalanced name
   3.390 +  where chunks = split False charX source |> map (split True charY)
   3.391 +
   3.392 +parse :: String -> XML.Tree
   3.393 +parse source =
   3.394 +  case parse_body source of
   3.395 +    [result] -> result
   3.396 +    [] -> XML.Text ""
   3.397 +    _ -> err "multiple results"
   3.398  \<close>
   3.399  
   3.400  end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Tools/Haskell/Library.hs	Sat Nov 03 19:33:15 2018 +0100
     4.3 @@ -0,0 +1,52 @@
     4.4 +{- GENERATED by Isabelle! -}
     4.5 +{-  Title:      Tools/Haskell/Library.hs
     4.6 +    Author:     Makarius
     4.7 +    LICENSE:    BSD 3-clause (Isabelle)
     4.8 +
     4.9 +Basic library of Isabelle idioms.
    4.10 +-}
    4.11 +
    4.12 +module Isabelle.Library
    4.13 +  ((|>), (|->), (#>), (#->), fold, fold_rev, single, quote, trim_line)
    4.14 +where
    4.15 +
    4.16 +{- functions -}
    4.17 +
    4.18 +(|>) :: a -> (a -> b) -> b
    4.19 +x |> f = f x
    4.20 +
    4.21 +(|->) :: (a, b) -> (a -> b -> c) -> c
    4.22 +(x, y) |-> f = f x y
    4.23 +
    4.24 +(#>) :: (a -> b) -> (b -> c) -> a -> c
    4.25 +(f #> g) x = x |> f |> g
    4.26 +
    4.27 +(#->) :: (a -> (c, b)) -> (c -> b -> d) -> a -> d
    4.28 +(f #-> g) x  = x |> f |-> g
    4.29 +
    4.30 +
    4.31 +{- lists -}
    4.32 +
    4.33 +fold :: (a -> b -> b) -> [a] -> b -> b
    4.34 +fold _ [] y = y
    4.35 +fold f (x : xs) y = fold f xs (f x y)
    4.36 +
    4.37 +fold_rev :: (a -> b -> b) -> [a] -> b -> b
    4.38 +fold_rev _ [] y = y
    4.39 +fold_rev f (x : xs) y = f x (fold_rev f xs y)
    4.40 +
    4.41 +single :: a -> [a]
    4.42 +single x = [x]
    4.43 +
    4.44 +
    4.45 +{- strings -}
    4.46 +
    4.47 +quote :: String -> String
    4.48 +quote s = "\"" ++ s ++ "\""
    4.49 +
    4.50 +trim_line :: String -> String
    4.51 +trim_line line =
    4.52 +  case reverse line of
    4.53 +    '\n' : '\r' : rest -> reverse rest
    4.54 +    '\n' : rest -> reverse rest
    4.55 +    _ -> line
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Tools/Haskell/Markup.hs	Sat Nov 03 19:33:15 2018 +0100
     5.3 @@ -0,0 +1,28 @@
     5.4 +{- GENERATED by Isabelle! -}
     5.5 +{-  Title:      Haskell/Tools/Markup.hs
     5.6 +    Author:     Makarius
     5.7 +    LICENSE:    BSD 3-clause (Isabelle)
     5.8 +
     5.9 +Quasi-abstract markup elements.
    5.10 +-}
    5.11 +
    5.12 +module Isabelle.Markup (T, empty, is_empty, Output, no_output)
    5.13 +where
    5.14 +
    5.15 +import qualified Isabelle.Properties as Properties
    5.16 +
    5.17 +
    5.18 +type T = (String, Properties.T)
    5.19 +
    5.20 +empty :: T
    5.21 +empty = ("", [])
    5.22 +
    5.23 +is_empty :: T -> Bool
    5.24 +is_empty ("", _) = True
    5.25 +is_empty _ = False
    5.26 +
    5.27 +
    5.28 +type Output = (String, String)
    5.29 +
    5.30 +no_output :: Output
    5.31 +no_output = ("", "")
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Tools/Haskell/Properties.hs	Sat Nov 03 19:33:15 2018 +0100
     6.3 @@ -0,0 +1,30 @@
     6.4 +{- GENERATED by Isabelle! -}
     6.5 +{-  Title:      Tools/Haskell/Properties.hs
     6.6 +    Author:     Makarius
     6.7 +    LICENSE:    BSD 3-clause (Isabelle)
     6.8 +
     6.9 +Property lists.
    6.10 +-}
    6.11 +
    6.12 +module Isabelle.Properties (Entry, T, defined, get, put, remove)
    6.13 +where
    6.14 +
    6.15 +import qualified Data.List as List
    6.16 +
    6.17 +
    6.18 +type Entry = (String, String)
    6.19 +type T = [Entry]
    6.20 +
    6.21 +defined :: T -> String -> Bool
    6.22 +defined props name = any (\(a, _) -> a == name) props
    6.23 +
    6.24 +get :: T -> String -> Maybe String
    6.25 +get props name = List.lookup name props
    6.26 +
    6.27 +put :: Entry -> T -> T
    6.28 +put entry props = entry : remove (fst entry) props
    6.29 +
    6.30 +remove :: String -> T -> T
    6.31 +remove name props =
    6.32 +  if defined props name then filter (\(a, _) -> a /= name) props
    6.33 +  else props
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Tools/Haskell/XML.hs	Sat Nov 03 19:33:15 2018 +0100
     7.3 @@ -0,0 +1,79 @@
     7.4 +{- GENERATED by Isabelle! -}
     7.5 +{-  Title:      Tools/Haskell/XML.hs
     7.6 +    Author:     Makarius
     7.7 +    LICENSE:    BSD 3-clause (Isabelle)
     7.8 +
     7.9 +Untyped XML trees and representation of ML values.
    7.10 +-}
    7.11 +
    7.12 +module Isabelle.XML (Attributes, Body, Tree(..), wrap_elem, unwrap_elem, content_of)
    7.13 +where
    7.14 +
    7.15 +import qualified Data.List as List
    7.16 +
    7.17 +import Isabelle.Library
    7.18 +import qualified Isabelle.Properties as Properties
    7.19 +import qualified Isabelle.Markup as Markup
    7.20 +import qualified Isabelle.Buffer as Buffer
    7.21 +
    7.22 +
    7.23 +{- types -}
    7.24 +
    7.25 +type Attributes = Properties.T
    7.26 +type Body = [Tree]
    7.27 +data Tree = Elem Markup.T Body | Text String
    7.28 +
    7.29 +
    7.30 +{- wrapped elements -}
    7.31 +
    7.32 +xml_elemN = "xml_elem";
    7.33 +xml_nameN = "xml_name";
    7.34 +xml_bodyN = "xml_body";
    7.35 +
    7.36 +wrap_elem (((a, atts), body1), body2) =
    7.37 +  Elem (xml_elemN, (xml_nameN, a) : atts) (Elem (xml_bodyN, []) body1 : body2)
    7.38 +
    7.39 +unwrap_elem (Elem (name, (n, a) : atts) (Elem (name', atts') body1 : body2)) =
    7.40 +  if name == xml_elemN && n == xml_nameN && name' == xml_bodyN && null atts'
    7.41 +  then Just (((a, atts), body1), body2) else Nothing
    7.42 +unwrap_elem _ = Nothing
    7.43 +
    7.44 +
    7.45 +{- text content -}
    7.46 +
    7.47 +add_content tree =
    7.48 +  case unwrap_elem tree of
    7.49 +    Just (_, ts) -> fold add_content ts
    7.50 +    Nothing ->
    7.51 +      case tree of
    7.52 +        Elem _ ts -> fold add_content ts
    7.53 +        Text s -> Buffer.add s
    7.54 +
    7.55 +content_of body = Buffer.empty |> fold add_content body |> Buffer.content
    7.56 +
    7.57 +
    7.58 +{- string representation -}
    7.59 +
    7.60 +encode '<' = "&lt;"
    7.61 +encode '>' = "&gt;"
    7.62 +encode '&' = "&amp;"
    7.63 +encode '\'' = "&apos;"
    7.64 +encode '\"' = "&quot;"
    7.65 +encode c = [c]
    7.66 +
    7.67 +instance Show Tree where
    7.68 +  show tree =
    7.69 +    Buffer.empty |> show_tree tree |> Buffer.content
    7.70 +    where
    7.71 +      show_tree (Elem (name, atts) []) =
    7.72 +        Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add "/>"
    7.73 +      show_tree (Elem (name, atts) ts) =
    7.74 +        Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add ">" #>
    7.75 +        fold show_tree ts #>
    7.76 +        Buffer.add "</" #> Buffer.add name #> Buffer.add ">"
    7.77 +      show_tree (Text s) = Buffer.add (show_text s)
    7.78 +
    7.79 +      show_elem name atts =
    7.80 +        unwords (name : map (\(a, x) -> a ++ "=\"" ++ show_text x ++ "\"") atts)
    7.81 +
    7.82 +      show_text = concatMap encode
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/Tools/Haskell/YXML.hs	Sat Nov 03 19:33:15 2018 +0100
     8.3 @@ -0,0 +1,120 @@
     8.4 +{- GENERATED by Isabelle! -}
     8.5 +{-  Title:      Tools/Haskell/YXML.hs
     8.6 +    Author:     Makarius
     8.7 +    LICENSE:    BSD 3-clause (Isabelle)
     8.8 +
     8.9 +Efficient text representation of XML trees.  Suitable for direct
    8.10 +inlining into plain text.
    8.11 +-}
    8.12 +
    8.13 +
    8.14 +module Isabelle.YXML (charX, charY, strX, strY, detect,
    8.15 +  buffer_body, buffer, string_of_body, string_of, parse_body, parse)
    8.16 +where
    8.17 +
    8.18 +import qualified Data.Char as Char
    8.19 +import qualified Data.List as List
    8.20 +
    8.21 +import Isabelle.Library
    8.22 +import qualified Isabelle.Markup as Markup
    8.23 +import qualified Isabelle.XML as XML
    8.24 +import qualified Isabelle.Buffer as Buffer
    8.25 +
    8.26 +
    8.27 +{- markers -}
    8.28 +
    8.29 +charX, charY :: Char
    8.30 +charX = Char.chr 5
    8.31 +charY = Char.chr 6
    8.32 +
    8.33 +strX, strY, strXY, strXYX :: String
    8.34 +strX = [charX]
    8.35 +strY = [charY]
    8.36 +strXY = strX ++ strY
    8.37 +strXYX = strXY ++ strX
    8.38 +
    8.39 +detect :: String -> Bool
    8.40 +detect = any (\c -> c == charX || c == charY)
    8.41 +
    8.42 +
    8.43 +{- output -}
    8.44 +
    8.45 +buffer_attrib (a, x) =
    8.46 +  Buffer.add strY #> Buffer.add a #> Buffer.add "=" #> Buffer.add x
    8.47 +
    8.48 +buffer_body :: XML.Body -> Buffer.T -> Buffer.T
    8.49 +buffer_body = fold buffer
    8.50 +
    8.51 +buffer :: XML.Tree -> Buffer.T -> Buffer.T
    8.52 +buffer (XML.Elem (name, atts) ts) =
    8.53 +  Buffer.add strXY #> Buffer.add name #> fold buffer_attrib atts #> Buffer.add strX #>
    8.54 +  buffer_body ts #>
    8.55 +  Buffer.add strXYX
    8.56 +buffer (XML.Text s) = Buffer.add s
    8.57 +
    8.58 +string_of_body :: XML.Body -> String
    8.59 +string_of_body body = Buffer.empty |> buffer_body body |> Buffer.content
    8.60 +
    8.61 +string_of :: XML.Tree -> String
    8.62 +string_of = string_of_body . single
    8.63 +
    8.64 +
    8.65 +{- parse -}
    8.66 +
    8.67 +-- split: fields or non-empty tokens
    8.68 +
    8.69 +split :: Bool -> Char -> String -> [String]
    8.70 +split _ _ [] = []
    8.71 +split fields sep str = splitting str
    8.72 +  where
    8.73 +    splitting rest =
    8.74 +      case span (/= sep) rest of
    8.75 +        (_, []) -> cons rest []
    8.76 +        (prfx, _ : rest') -> cons prfx (splitting rest')
    8.77 +    cons item = if fields || not (null item) then (:) item else id
    8.78 +
    8.79 +
    8.80 +-- structural errors
    8.81 +
    8.82 +err msg = error ("Malformed YXML: " ++ msg)
    8.83 +err_attribute = err "bad attribute"
    8.84 +err_element = err "bad element"
    8.85 +err_unbalanced "" = err "unbalanced element"
    8.86 +err_unbalanced name = err ("unbalanced element " ++ quote name)
    8.87 +
    8.88 +
    8.89 +-- stack operations
    8.90 +
    8.91 +add x ((elem, body) : pending) = (elem, x : body) : pending
    8.92 +
    8.93 +push "" _ _ = err_element
    8.94 +push name atts pending = ((name, atts), []) : pending
    8.95 +
    8.96 +pop ((("", _), _) : _) = err_unbalanced ""
    8.97 +pop ((markup, body) : pending) = add (XML.Elem markup (reverse body)) pending
    8.98 +
    8.99 +
   8.100 +-- parsing
   8.101 +
   8.102 +parse_attrib s =
   8.103 +  case List.elemIndex '=' s of
   8.104 +    Just i | i > 0 -> (take i s, drop (i + 1) s)
   8.105 +    _ -> err_attribute
   8.106 +
   8.107 +parse_chunk ["", ""] = pop
   8.108 +parse_chunk ("" : name : atts) = push name (map parse_attrib atts)
   8.109 +parse_chunk txts = fold (add . XML.Text) txts
   8.110 +
   8.111 +parse_body :: String -> XML.Body
   8.112 +parse_body source =
   8.113 +  case fold parse_chunk chunks [(("", []), [])] of
   8.114 +    [(("", _), result)] -> reverse result
   8.115 +    ((name, _), _) : _ -> err_unbalanced name
   8.116 +  where chunks = split False charX source |> map (split True charY)
   8.117 +
   8.118 +parse :: String -> XML.Tree
   8.119 +parse source =
   8.120 +  case parse_body source of
   8.121 +    [result] -> result
   8.122 +    [] -> XML.Text ""
   8.123 +    _ -> err "multiple results"
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/Tools/Haskell/haskell.ML	Sat Nov 03 19:33:15 2018 +0100
     9.3 @@ -0,0 +1,56 @@
     9.4 +(*  Title:      Tools/Haskell/haskell.ml
     9.5 +    Author:     Makarius
     9.6 +
     9.7 +Support for Isabelle tools in Haskell.
     9.8 +*)
     9.9 +
    9.10 +signature HASKELL =
    9.11 +sig
    9.12 +  val generate_file_cmd: (string * Position.T) * Input.source ->
    9.13 +    Toplevel.transition -> Toplevel.transition
    9.14 +  val export_file_cmd: string * Input.source ->
    9.15 +    Toplevel.transition -> Toplevel.transition
    9.16 +  val source_modules: Path.T list
    9.17 +end;
    9.18 +
    9.19 +structure Haskell: HASKELL =
    9.20 +struct
    9.21 +
    9.22 +(* commands *)
    9.23 +
    9.24 +val header = "{- GENERATED by Isabelle! -}\n";
    9.25 +
    9.26 +fun generate_file_cmd (file, source) =
    9.27 +  Toplevel.keep (fn state =>
    9.28 +    let
    9.29 +      val ctxt = Toplevel.context_of state;
    9.30 +      val thy = Toplevel.theory_of state;
    9.31 +
    9.32 +      val path = Resources.check_path ctxt (Resources.master_directory thy) file;
    9.33 +      val text = header ^ GHC.read_source ctxt source;
    9.34 +      val _ = Isabelle_System.mkdirs (Path.dir (Path.expand path));
    9.35 +      val _ = File.generate path text;
    9.36 +    in () end);
    9.37 +
    9.38 +fun export_file_cmd (name, source) =
    9.39 +  Toplevel.keep (fn state =>
    9.40 +    let
    9.41 +      val ctxt = Toplevel.context_of state;
    9.42 +      val thy = Toplevel.theory_of state;
    9.43 +
    9.44 +      val text = header ^ GHC.read_source ctxt source;
    9.45 +      val _ = Export.export thy name [text];
    9.46 +    in () end);
    9.47 +
    9.48 +
    9.49 +(* source modules *)
    9.50 +
    9.51 +val source_modules =
    9.52 + [\<^file>\<open>~~/src/Tools/Haskell/Library.hs\<close>,
    9.53 +  \<^file>\<open>~~/src/Tools/Haskell/Buffer.hs\<close>,
    9.54 +  \<^file>\<open>~~/src/Tools/Haskell/Properties.hs\<close>,
    9.55 +  \<^file>\<open>~~/src/Tools/Haskell/Markup.hs\<close>,
    9.56 +  \<^file>\<open>~~/src/Tools/Haskell/XML.hs\<close>,
    9.57 +  \<^file>\<open>~~/src/Tools/Haskell/YXML.hs\<close>];
    9.58 +
    9.59 +end;
    10.1 --- a/src/Tools/ROOT	Sat Nov 03 19:31:50 2018 +0100
    10.2 +++ b/src/Tools/ROOT	Sat Nov 03 19:33:15 2018 +0100
    10.3 @@ -12,3 +12,5 @@
    10.4  session Haskell in Haskell = Pure +
    10.5    theories
    10.6      Haskell
    10.7 +  theories [condition = ISABELLE_GHC]
    10.8 +    Build