more Haskell operations;
authorwenzelm
Tue Nov 06 14:53:56 2018 +0100 (6 months ago)
changeset 692489f21381600e3
parent 69247 fc24fe912258
child 69249 27423819534c
more Haskell operations;
src/Tools/Haskell/Haskell.thy
src/Tools/Haskell/Markup.hs
src/Tools/Haskell/Pretty.hs
src/Tools/Haskell/YXML.hs
src/Tools/Haskell/haskell.ML
     1.1 --- a/src/Tools/Haskell/Haskell.thy	Tue Nov 06 14:30:53 2018 +0100
     1.2 +++ b/src/Tools/Haskell/Haskell.thy	Tue Nov 06 14:53:56 2018 +0100
     1.3 @@ -238,6 +238,9 @@
     1.4  
     1.5    lineN, end_lineN, offsetN, end_offsetN, fileN, idN, positionN, position,
     1.6  
     1.7 +  markupN, consistentN, unbreakableN, indentN, widthN,
     1.8 +  blockN, block, breakN, break, fbreakN, fbreak, itemN, item,
     1.9 +
    1.10    wordsN, words, no_wordsN, no_words,
    1.11  
    1.12    tfreeN, tfree, tvarN, tvar, freeN, free, skolemN, skolem, boundN, bound, varN, var,
    1.13 @@ -261,10 +264,11 @@
    1.14    Output, no_output)
    1.15  where
    1.16  
    1.17 -import Prelude hiding (words, error)
    1.18 +import Prelude hiding (words, error, break)
    1.19  
    1.20  import Isabelle.Library
    1.21  import qualified Isabelle.Properties as Properties
    1.22 +import qualified Isabelle.Value as Value
    1.23  
    1.24  
    1.25  {- basic markup -}
    1.26 @@ -321,6 +325,40 @@
    1.27  (positionN, position) = markup_elem \<open>Markup.positionN\<close>
    1.28  
    1.29  
    1.30 +{- pretty printing -}
    1.31 +
    1.32 +markupN, consistentN, unbreakableN, indentN :: String
    1.33 +markupN = \<open>Markup.markupN\<close>;
    1.34 +consistentN = \<open>Markup.consistentN\<close>;
    1.35 +unbreakableN = \<open>Markup.unbreakableN\<close>;
    1.36 +indentN = \<open>Markup.indentN\<close>;
    1.37 +
    1.38 +widthN :: String
    1.39 +widthN = \<open>Markup.widthN\<close>
    1.40 +
    1.41 +blockN :: String
    1.42 +blockN = \<open>Markup.blockN\<close>
    1.43 +block :: Bool -> Int -> T
    1.44 +block c i =
    1.45 +  (blockN,
    1.46 +    (if c then [(consistentN, Value.print_bool c)] else []) ++
    1.47 +    (if i /= 0 then [(indentN, Value.print_int i)] else []))
    1.48 +
    1.49 +breakN :: String
    1.50 +breakN = \<open>Markup.breakN\<close>
    1.51 +break :: Int -> Int -> T
    1.52 +break w i =
    1.53 +  (breakN,
    1.54 +    (if w /= 0 then [(widthN, Value.print_int w)] else []) ++
    1.55 +    (if i /= 0 then [(indentN, Value.print_int i)] else []))
    1.56 +
    1.57 +fbreakN :: String; fbreak :: T
    1.58 +(fbreakN, fbreak) = markup_elem \<open>Markup.fbreakN\<close>
    1.59 +
    1.60 +itemN :: String; item :: T
    1.61 +(itemN, item) = markup_elem \<open>Markup.itemN\<close>
    1.62 +
    1.63 +
    1.64  {- text properties -}
    1.65  
    1.66  wordsN :: String; words :: T
    1.67 @@ -748,6 +786,158 @@
    1.68  variant _ _ = err_body
    1.69  \<close>
    1.70  
    1.71 +generate_haskell_file "Pretty.hs" = \<open>
    1.72 +{-  Title:      Tools/Haskell/Pretty.hs
    1.73 +    Author:     Makarius
    1.74 +    LICENSE:    BSD 3-clause (Isabelle)
    1.75 +
    1.76 +Generic pretty printing module.
    1.77 +-}
    1.78 +
    1.79 +module Isabelle.Pretty (
    1.80 +  T, symbolic, formatted, unformatted,
    1.81 +
    1.82 +  str, brk_indent, brk, fbrk, breaks, fbreaks, blk, block, strs, markup, mark, mark_str, marks_str,
    1.83 +  item, text_fold, keyword1, keyword2, text, paragraph, para, quote, cartouche, separate,
    1.84 +  commas, enclose, enum, list, str_list, big_list)
    1.85 +where
    1.86 +
    1.87 +import Isabelle.Library hiding (quote)
    1.88 +import qualified Data.List as List
    1.89 +import qualified Isabelle.Buffer as Buffer
    1.90 +import qualified Isabelle.Markup as Markup
    1.91 +import qualified Isabelle.XML as XML
    1.92 +import qualified Isabelle.YXML as YXML
    1.93 +
    1.94 +
    1.95 +data T =
    1.96 +    Block Markup.T Bool Int [T]
    1.97 +  | Break Int Int
    1.98 +  | Str String
    1.99 +
   1.100 +
   1.101 +{- output -}
   1.102 +
   1.103 +output_spaces n = replicate n ' '
   1.104 +
   1.105 +symbolic_text "" = []
   1.106 +symbolic_text s = [XML.Text s]
   1.107 +
   1.108 +symbolic_markup markup body =
   1.109 +  if Markup.is_empty markup then body
   1.110 +  else [XML.Elem markup body]
   1.111 +
   1.112 +symbolic :: T -> XML.Body
   1.113 +symbolic (Block markup consistent indent prts) =
   1.114 +  concatMap symbolic prts
   1.115 +  |> symbolic_markup block_markup
   1.116 +  |> symbolic_markup markup
   1.117 +  where block_markup = if null prts then Markup.empty else Markup.block consistent indent
   1.118 +symbolic (Break wd ind) = [XML.Elem (Markup.break wd ind) (symbolic_text (output_spaces wd))]
   1.119 +symbolic (Str s) = symbolic_text s
   1.120 +
   1.121 +formatted :: T -> String
   1.122 +formatted = YXML.string_of_body . symbolic
   1.123 +
   1.124 +unformatted :: T -> String
   1.125 +unformatted prt = Buffer.empty |> out prt |> Buffer.content
   1.126 +  where
   1.127 +    out (Block markup _ _ prts) =
   1.128 +      let (bg, en) = YXML.output_markup markup
   1.129 +      in Buffer.add bg #> fold out prts #> Buffer.add en
   1.130 +    out (Break _ wd) = Buffer.add (output_spaces wd)
   1.131 +    out (Str s) = Buffer.add s
   1.132 +
   1.133 +
   1.134 +{- derived operations to create formatting expressions -}
   1.135 +
   1.136 +force_nat n | n < 0 = 0
   1.137 +force_nat n = n
   1.138 +
   1.139 +str :: String -> T
   1.140 +str = Str
   1.141 +
   1.142 +brk_indent :: Int -> Int -> T
   1.143 +brk_indent wd ind = Break (force_nat wd) ind
   1.144 +
   1.145 +brk :: Int -> T
   1.146 +brk wd = brk_indent wd 0
   1.147 +
   1.148 +fbrk :: T
   1.149 +fbrk = str "\n"
   1.150 +
   1.151 +breaks, fbreaks :: [T] -> [T]
   1.152 +breaks = List.intersperse (brk 1)
   1.153 +fbreaks = List.intersperse fbrk
   1.154 +
   1.155 +blk :: (Int, [T]) -> T
   1.156 +blk (indent, es) = Block Markup.empty False (force_nat indent) es
   1.157 +
   1.158 +block :: [T] -> T
   1.159 +block prts = blk (2, prts)
   1.160 +
   1.161 +strs :: [String] -> T
   1.162 +strs = block . breaks . map str
   1.163 +
   1.164 +markup :: Markup.T -> [T] -> T
   1.165 +markup m = Block m False 0
   1.166 +
   1.167 +mark :: Markup.T -> T -> T
   1.168 +mark m prt = if m == Markup.empty then prt else markup m [prt]
   1.169 +
   1.170 +mark_str :: (Markup.T, String) -> T
   1.171 +mark_str (m, s) = mark m (str s)
   1.172 +
   1.173 +marks_str :: ([Markup.T], String) -> T
   1.174 +marks_str (ms, s) = fold_rev mark ms (str s)
   1.175 +
   1.176 +item :: [T] -> T
   1.177 +item = markup Markup.item
   1.178 +
   1.179 +text_fold :: [T] -> T
   1.180 +text_fold = markup Markup.text_fold
   1.181 +
   1.182 +keyword1, keyword2 :: String -> T
   1.183 +keyword1 name = mark_str (Markup.keyword1, name)
   1.184 +keyword2 name = mark_str (Markup.keyword2, name)
   1.185 +
   1.186 +text :: String -> [T]
   1.187 +text = breaks . map str . words
   1.188 +
   1.189 +paragraph :: [T] -> T
   1.190 +paragraph = markup Markup.paragraph
   1.191 +
   1.192 +para :: String -> T
   1.193 +para = paragraph . text
   1.194 +
   1.195 +quote :: T -> T
   1.196 +quote prt = blk (1, [str "\"", prt, str "\""])
   1.197 +
   1.198 +cartouche :: T -> T
   1.199 +cartouche prt = blk (1, [str "\92<open>", prt, str "\92<close>"])
   1.200 +
   1.201 +separate :: String -> [T] -> [T]
   1.202 +separate sep = List.intercalate [str sep, brk 1] . map single
   1.203 +
   1.204 +commas :: [T] -> [T]
   1.205 +commas = separate ","
   1.206 +
   1.207 +enclose :: String -> String -> [T] -> T
   1.208 +enclose lpar rpar prts = block (str lpar : prts ++ [str rpar])
   1.209 +
   1.210 +enum :: String -> String -> String -> [T] -> T
   1.211 +enum sep lpar rpar = enclose lpar rpar . separate sep
   1.212 +
   1.213 +list :: String -> String -> [T] -> T
   1.214 +list = enum ","
   1.215 +
   1.216 +str_list :: String -> String -> [String] -> T
   1.217 +str_list lpar rpar = list lpar rpar . map str
   1.218 +
   1.219 +big_list :: String -> [T] -> T
   1.220 +big_list name prts = block (fbreaks (str name : prts))
   1.221 +\<close>
   1.222 +
   1.223  generate_haskell_file "YXML.hs" = \<open>
   1.224  {-  Title:      Tools/Haskell/YXML.hs
   1.225      Author:     Makarius
   1.226 @@ -757,7 +947,7 @@
   1.227  inlining into plain text.
   1.228  -}
   1.229  
   1.230 -module Isabelle.YXML (charX, charY, strX, strY, detect,
   1.231 +module Isabelle.YXML (charX, charY, strX, strY, detect, output_markup,
   1.232    buffer_body, buffer, string_of_body, string_of, parse_body, parse)
   1.233  where
   1.234  
   1.235 @@ -788,6 +978,11 @@
   1.236  
   1.237  {- output -}
   1.238  
   1.239 +output_markup :: Markup.T -> Markup.Output
   1.240 +output_markup markup@(name, atts) =
   1.241 +  if Markup.is_empty markup then Markup.no_output
   1.242 +  else (strXY ++ name ++ concatMap (\(a, x) -> strY ++ a ++ "=" ++ x) atts ++ strX, strXYX)
   1.243 +
   1.244  buffer_attrib (a, x) =
   1.245    Buffer.add strY #> Buffer.add a #> Buffer.add "=" #> Buffer.add x
   1.246  
     2.1 --- a/src/Tools/Haskell/Markup.hs	Tue Nov 06 14:30:53 2018 +0100
     2.2 +++ b/src/Tools/Haskell/Markup.hs	Tue Nov 06 14:53:56 2018 +0100
     2.3 @@ -14,6 +14,9 @@
     2.4  
     2.5    lineN, end_lineN, offsetN, end_offsetN, fileN, idN, positionN, position,
     2.6  
     2.7 +  markupN, consistentN, unbreakableN, indentN, widthN,
     2.8 +  blockN, block, breakN, break, fbreakN, fbreak, itemN, item,
     2.9 +
    2.10    wordsN, words, no_wordsN, no_words,
    2.11  
    2.12    tfreeN, tfree, tvarN, tvar, freeN, free, skolemN, skolem, boundN, bound, varN, var,
    2.13 @@ -37,10 +40,11 @@
    2.14    Output, no_output)
    2.15  where
    2.16  
    2.17 -import Prelude hiding (words, error)
    2.18 +import Prelude hiding (words, error, break)
    2.19  
    2.20  import Isabelle.Library
    2.21  import qualified Isabelle.Properties as Properties
    2.22 +import qualified Isabelle.Value as Value
    2.23  
    2.24  
    2.25  {- basic markup -}
    2.26 @@ -97,6 +101,40 @@
    2.27  (positionN, position) = markup_elem "position"
    2.28  
    2.29  
    2.30 +{- pretty printing -}
    2.31 +
    2.32 +markupN, consistentN, unbreakableN, indentN :: String
    2.33 +markupN = "markup";
    2.34 +consistentN = "consistent";
    2.35 +unbreakableN = "unbreakable";
    2.36 +indentN = "indent";
    2.37 +
    2.38 +widthN :: String
    2.39 +widthN = "width"
    2.40 +
    2.41 +blockN :: String
    2.42 +blockN = "block"
    2.43 +block :: Bool -> Int -> T
    2.44 +block c i =
    2.45 +  (blockN,
    2.46 +    (if c then [(consistentN, Value.print_bool c)] else []) ++
    2.47 +    (if i /= 0 then [(indentN, Value.print_int i)] else []))
    2.48 +
    2.49 +breakN :: String
    2.50 +breakN = "break"
    2.51 +break :: Int -> Int -> T
    2.52 +break w i =
    2.53 +  (breakN,
    2.54 +    (if w /= 0 then [(widthN, Value.print_int w)] else []) ++
    2.55 +    (if i /= 0 then [(indentN, Value.print_int i)] else []))
    2.56 +
    2.57 +fbreakN :: String; fbreak :: T
    2.58 +(fbreakN, fbreak) = markup_elem "fbreak"
    2.59 +
    2.60 +itemN :: String; item :: T
    2.61 +(itemN, item) = markup_elem "item"
    2.62 +
    2.63 +
    2.64  {- text properties -}
    2.65  
    2.66  wordsN :: String; words :: T
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Tools/Haskell/Pretty.hs	Tue Nov 06 14:53:56 2018 +0100
     3.3 @@ -0,0 +1,151 @@
     3.4 +{- generated by Isabelle -}
     3.5 +
     3.6 +{-  Title:      Tools/Haskell/Pretty.hs
     3.7 +    Author:     Makarius
     3.8 +    LICENSE:    BSD 3-clause (Isabelle)
     3.9 +
    3.10 +Generic pretty printing module.
    3.11 +-}
    3.12 +
    3.13 +module Isabelle.Pretty (
    3.14 +  T, symbolic, formatted, unformatted,
    3.15 +
    3.16 +  str, brk_indent, brk, fbrk, breaks, fbreaks, blk, block, strs, markup, mark, mark_str, marks_str,
    3.17 +  item, text_fold, keyword1, keyword2, text, paragraph, para, quote, cartouche, separate,
    3.18 +  commas, enclose, enum, list, str_list, big_list)
    3.19 +where
    3.20 +
    3.21 +import Isabelle.Library hiding (quote)
    3.22 +import qualified Data.List as List
    3.23 +import qualified Isabelle.Buffer as Buffer
    3.24 +import qualified Isabelle.Markup as Markup
    3.25 +import qualified Isabelle.XML as XML
    3.26 +import qualified Isabelle.YXML as YXML
    3.27 +
    3.28 +
    3.29 +data T =
    3.30 +    Block Markup.T Bool Int [T]
    3.31 +  | Break Int Int
    3.32 +  | Str String
    3.33 +
    3.34 +
    3.35 +{- output -}
    3.36 +
    3.37 +output_spaces n = replicate n ' '
    3.38 +
    3.39 +symbolic_text "" = []
    3.40 +symbolic_text s = [XML.Text s]
    3.41 +
    3.42 +symbolic_markup markup body =
    3.43 +  if Markup.is_empty markup then body
    3.44 +  else [XML.Elem markup body]
    3.45 +
    3.46 +symbolic :: T -> XML.Body
    3.47 +symbolic (Block markup consistent indent prts) =
    3.48 +  concatMap symbolic prts
    3.49 +  |> symbolic_markup block_markup
    3.50 +  |> symbolic_markup markup
    3.51 +  where block_markup = if null prts then Markup.empty else Markup.block consistent indent
    3.52 +symbolic (Break wd ind) = [XML.Elem (Markup.break wd ind) (symbolic_text (output_spaces wd))]
    3.53 +symbolic (Str s) = symbolic_text s
    3.54 +
    3.55 +formatted :: T -> String
    3.56 +formatted = YXML.string_of_body . symbolic
    3.57 +
    3.58 +unformatted :: T -> String
    3.59 +unformatted prt = Buffer.empty |> out prt |> Buffer.content
    3.60 +  where
    3.61 +    out (Block markup _ _ prts) =
    3.62 +      let (bg, en) = YXML.output_markup markup
    3.63 +      in Buffer.add bg #> fold out prts #> Buffer.add en
    3.64 +    out (Break _ wd) = Buffer.add (output_spaces wd)
    3.65 +    out (Str s) = Buffer.add s
    3.66 +
    3.67 +
    3.68 +{- derived operations to create formatting expressions -}
    3.69 +
    3.70 +force_nat n | n < 0 = 0
    3.71 +force_nat n = n
    3.72 +
    3.73 +str :: String -> T
    3.74 +str = Str
    3.75 +
    3.76 +brk_indent :: Int -> Int -> T
    3.77 +brk_indent wd ind = Break (force_nat wd) ind
    3.78 +
    3.79 +brk :: Int -> T
    3.80 +brk wd = brk_indent wd 0
    3.81 +
    3.82 +fbrk :: T
    3.83 +fbrk = str "\n"
    3.84 +
    3.85 +breaks, fbreaks :: [T] -> [T]
    3.86 +breaks = List.intersperse (brk 1)
    3.87 +fbreaks = List.intersperse fbrk
    3.88 +
    3.89 +blk :: (Int, [T]) -> T
    3.90 +blk (indent, es) = Block Markup.empty False (force_nat indent) es
    3.91 +
    3.92 +block :: [T] -> T
    3.93 +block prts = blk (2, prts)
    3.94 +
    3.95 +strs :: [String] -> T
    3.96 +strs = block . breaks . map str
    3.97 +
    3.98 +markup :: Markup.T -> [T] -> T
    3.99 +markup m = Block m False 0
   3.100 +
   3.101 +mark :: Markup.T -> T -> T
   3.102 +mark m prt = if m == Markup.empty then prt else markup m [prt]
   3.103 +
   3.104 +mark_str :: (Markup.T, String) -> T
   3.105 +mark_str (m, s) = mark m (str s)
   3.106 +
   3.107 +marks_str :: ([Markup.T], String) -> T
   3.108 +marks_str (ms, s) = fold_rev mark ms (str s)
   3.109 +
   3.110 +item :: [T] -> T
   3.111 +item = markup Markup.item
   3.112 +
   3.113 +text_fold :: [T] -> T
   3.114 +text_fold = markup Markup.text_fold
   3.115 +
   3.116 +keyword1, keyword2 :: String -> T
   3.117 +keyword1 name = mark_str (Markup.keyword1, name)
   3.118 +keyword2 name = mark_str (Markup.keyword2, name)
   3.119 +
   3.120 +text :: String -> [T]
   3.121 +text = breaks . map str . words
   3.122 +
   3.123 +paragraph :: [T] -> T
   3.124 +paragraph = markup Markup.paragraph
   3.125 +
   3.126 +para :: String -> T
   3.127 +para = paragraph . text
   3.128 +
   3.129 +quote :: T -> T
   3.130 +quote prt = blk (1, [str "\"", prt, str "\""])
   3.131 +
   3.132 +cartouche :: T -> T
   3.133 +cartouche prt = blk (1, [str "\92<open>", prt, str "\92<close>"])
   3.134 +
   3.135 +separate :: String -> [T] -> [T]
   3.136 +separate sep = List.intercalate [str sep, brk 1] . map single
   3.137 +
   3.138 +commas :: [T] -> [T]
   3.139 +commas = separate ","
   3.140 +
   3.141 +enclose :: String -> String -> [T] -> T
   3.142 +enclose lpar rpar prts = block (str lpar : prts ++ [str rpar])
   3.143 +
   3.144 +enum :: String -> String -> String -> [T] -> T
   3.145 +enum sep lpar rpar = enclose lpar rpar . separate sep
   3.146 +
   3.147 +list :: String -> String -> [T] -> T
   3.148 +list = enum ","
   3.149 +
   3.150 +str_list :: String -> String -> [String] -> T
   3.151 +str_list lpar rpar = list lpar rpar . map str
   3.152 +
   3.153 +big_list :: String -> [T] -> T
   3.154 +big_list name prts = block (fbreaks (str name : prts))
     4.1 --- a/src/Tools/Haskell/YXML.hs	Tue Nov 06 14:30:53 2018 +0100
     4.2 +++ b/src/Tools/Haskell/YXML.hs	Tue Nov 06 14:53:56 2018 +0100
     4.3 @@ -8,7 +8,7 @@
     4.4  inlining into plain text.
     4.5  -}
     4.6  
     4.7 -module Isabelle.YXML (charX, charY, strX, strY, detect,
     4.8 +module Isabelle.YXML (charX, charY, strX, strY, detect, output_markup,
     4.9    buffer_body, buffer, string_of_body, string_of, parse_body, parse)
    4.10  where
    4.11  
    4.12 @@ -39,6 +39,11 @@
    4.13  
    4.14  {- output -}
    4.15  
    4.16 +output_markup :: Markup.T -> Markup.Output
    4.17 +output_markup markup@(name, atts) =
    4.18 +  if Markup.is_empty markup then Markup.no_output
    4.19 +  else (strXY ++ name ++ concatMap (\(a, x) -> strY ++ a ++ "=" ++ x) atts ++ strX, strXYX)
    4.20 +
    4.21  buffer_attrib (a, x) =
    4.22    Buffer.add strY #> Buffer.add a #> Buffer.add "=" #> Buffer.add x
    4.23  
     5.1 --- a/src/Tools/Haskell/haskell.ML	Tue Nov 06 14:30:53 2018 +0100
     5.2 +++ b/src/Tools/Haskell/haskell.ML	Tue Nov 06 14:53:56 2018 +0100
     5.3 @@ -56,6 +56,7 @@
     5.4    \<^path>\<open>XML/Encode.hs\<close>,
     5.5    \<^path>\<open>XML/Decode.hs\<close>,
     5.6    \<^path>\<open>YXML.hs\<close>,
     5.7 +  \<^path>\<open>Pretty.hs\<close>,
     5.8    \<^path>\<open>Term.hs\<close>,
     5.9    \<^path>\<open>Term_XML/Encode.hs\<close>,
    5.10    \<^path>\<open>Term_XML/Decode.hs\<close>];