src/Tools/Haskell/Haskell.thy
changeset 69234 2dec32c7313f
parent 69233 560263485988
child 69236 a75aab6d785b
     1.1 --- a/src/Tools/Haskell/Haskell.thy	Sun Nov 04 15:28:51 2018 +0100
     1.2 +++ b/src/Tools/Haskell/Haskell.thy	Sun Nov 04 17:19:56 2018 +0100
     1.3 @@ -36,9 +36,12 @@
     1.4  -}
     1.5  
     1.6  module Isabelle.Library
     1.7 -  ((|>), (|->), (#>), (#->), fold, fold_rev, single, quote, trim_line)
     1.8 +  ((|>), (|->), (#>), (#->), the_default, fold, fold_rev, single, quote, trim_line)
     1.9  where
    1.10  
    1.11 +import Data.Maybe
    1.12 +
    1.13 +
    1.14  {- functions -}
    1.15  
    1.16  (|>) :: a -> (a -> b) -> b
    1.17 @@ -54,6 +57,13 @@
    1.18  (f #-> g) x  = x |> f |-> g
    1.19  
    1.20  
    1.21 +{- options -}
    1.22 +
    1.23 +the_default :: a -> Maybe a -> a
    1.24 +the_default x Nothing = x
    1.25 +the_default _ (Just y) = y
    1.26 +
    1.27 +
    1.28  {- lists -}
    1.29  
    1.30  fold :: (a -> b -> b) -> [a] -> b -> b
    1.31 @@ -196,12 +206,44 @@
    1.32  Quasi-abstract markup elements.
    1.33  -}
    1.34  
    1.35 -module Isabelle.Markup (T, empty, is_empty, Output, no_output)
    1.36 +module Isabelle.Markup (
    1.37 +  T, empty, is_empty, properties,
    1.38 +
    1.39 +  nameN, name, xnameN, xname, kindN,
    1.40 +
    1.41 +  lineN, end_lineN, offsetN, end_offsetN, fileN, idN, positionN, position,
    1.42 +
    1.43 +  wordsN, words, no_wordsN, no_words,
    1.44 +
    1.45 +  tfreeN, tfree, tvarN, tvar, freeN, free, skolemN, skolem, boundN, bound, varN, var,
    1.46 +  numeralN, numeral, literalN, literal, delimiterN, delimiter, inner_stringN, inner_string,
    1.47 +  inner_cartoucheN, inner_cartouche, inner_commentN, inner_comment,
    1.48 +  token_rangeN, token_range,
    1.49 +  sortingN, sorting, typingN, typing, class_parameterN, class_parameter,
    1.50 +
    1.51 +  antiquotedN, antiquoted, antiquoteN, antiquote,
    1.52 +
    1.53 +  paragraphN, paragraph, text_foldN, text_fold,
    1.54 +
    1.55 +  keyword1N, keyword1, keyword2N, keyword2, keyword3N, keyword3, quasi_keywordN, quasi_keyword,
    1.56 +  improperN, improper, operatorN, operator, stringN, string, alt_stringN, alt_string,
    1.57 +  verbatimN, verbatim, cartoucheN, cartouche, commentN, comment,
    1.58 +
    1.59 +  writelnN, writeln, stateN, state, informationN, information, tracingN, tracing,
    1.60 +  warningN, warning, legacyN, legacy, errorN, error, reportN, report, no_reportN, no_report,
    1.61 +
    1.62 +  intensifyN, intensify,
    1.63 +  Output, no_output)
    1.64  where
    1.65  
    1.66 +import Prelude hiding (words, error)
    1.67 +
    1.68 +import Isabelle.Library
    1.69  import qualified Isabelle.Properties as Properties
    1.70  
    1.71  
    1.72 +{- basic markup -}
    1.73 +
    1.74  type T = (String, Properties.T)
    1.75  
    1.76  empty :: T
    1.77 @@ -211,6 +253,199 @@
    1.78  is_empty ("", _) = True
    1.79  is_empty _ = False
    1.80  
    1.81 +properties :: Properties.T -> T -> T
    1.82 +properties more_props (elem, props) =
    1.83 +  (elem, fold_rev Properties.put more_props props)
    1.84 +
    1.85 +markup_elem name = (name, (name, []) :: T)
    1.86 +
    1.87 +
    1.88 +{- misc properties -}
    1.89 +
    1.90 +nameN :: String
    1.91 +nameN = \<open>Markup.nameN\<close>
    1.92 +
    1.93 +name :: String -> T -> T
    1.94 +name a = properties [(nameN, a)]
    1.95 +
    1.96 +xnameN :: String
    1.97 +xnameN = \<open>Markup.xnameN\<close>
    1.98 +
    1.99 +xname :: String -> T -> T
   1.100 +xname a = properties [(xnameN, a)]
   1.101 +
   1.102 +kindN :: String
   1.103 +kindN = \<open>Markup.kindN\<close>
   1.104 +
   1.105 +
   1.106 +{- position -}
   1.107 +
   1.108 +lineN, end_lineN :: String
   1.109 +lineN = \<open>Markup.lineN\<close>
   1.110 +end_lineN = \<open>Markup.end_lineN\<close>
   1.111 +
   1.112 +offsetN, end_offsetN :: String
   1.113 +offsetN = \<open>Markup.offsetN\<close>
   1.114 +end_offsetN = \<open>Markup.end_offsetN\<close>
   1.115 +
   1.116 +fileN, idN :: String
   1.117 +fileN = \<open>Markup.fileN\<close>
   1.118 +idN = \<open>Markup.idN\<close>
   1.119 +
   1.120 +positionN :: String; position :: T
   1.121 +(positionN, position) = markup_elem \<open>Markup.positionN\<close>
   1.122 +
   1.123 +
   1.124 +{- text properties -}
   1.125 +
   1.126 +wordsN :: String; words :: T
   1.127 +(wordsN, words) = markup_elem \<open>Markup.wordsN\<close>
   1.128 +
   1.129 +no_wordsN :: String; no_words :: T
   1.130 +(no_wordsN, no_words) = markup_elem \<open>Markup.no_wordsN\<close>
   1.131 +
   1.132 +
   1.133 +{- inner syntax -}
   1.134 +
   1.135 +tfreeN :: String; tfree :: T
   1.136 +(tfreeN, tfree) = markup_elem \<open>Markup.tfreeN\<close>
   1.137 +
   1.138 +tvarN :: String; tvar :: T
   1.139 +(tvarN, tvar) = markup_elem \<open>Markup.tvarN\<close>
   1.140 +
   1.141 +freeN :: String; free :: T
   1.142 +(freeN, free) = markup_elem \<open>Markup.freeN\<close>
   1.143 +
   1.144 +skolemN :: String; skolem :: T
   1.145 +(skolemN, skolem) = markup_elem \<open>Markup.skolemN\<close>
   1.146 +
   1.147 +boundN :: String; bound :: T
   1.148 +(boundN, bound) = markup_elem \<open>Markup.boundN\<close>
   1.149 +
   1.150 +varN :: String; var :: T
   1.151 +(varN, var) = markup_elem \<open>Markup.varN\<close>
   1.152 +
   1.153 +numeralN :: String; numeral :: T
   1.154 +(numeralN, numeral) = markup_elem \<open>Markup.numeralN\<close>
   1.155 +
   1.156 +literalN :: String; literal :: T
   1.157 +(literalN, literal) = markup_elem \<open>Markup.literalN\<close>
   1.158 +
   1.159 +delimiterN :: String; delimiter :: T
   1.160 +(delimiterN, delimiter) = markup_elem \<open>Markup.delimiterN\<close>
   1.161 +
   1.162 +inner_stringN :: String; inner_string :: T
   1.163 +(inner_stringN, inner_string) = markup_elem \<open>Markup.inner_stringN\<close>
   1.164 +
   1.165 +inner_cartoucheN :: String; inner_cartouche :: T
   1.166 +(inner_cartoucheN, inner_cartouche) = markup_elem \<open>Markup.inner_cartoucheN\<close>
   1.167 +
   1.168 +inner_commentN :: String; inner_comment :: T
   1.169 +(inner_commentN, inner_comment) = markup_elem \<open>Markup.inner_commentN\<close>
   1.170 +
   1.171 +
   1.172 +token_rangeN :: String; token_range :: T
   1.173 +(token_rangeN, token_range) = markup_elem \<open>Markup.token_rangeN\<close>
   1.174 +
   1.175 +
   1.176 +sortingN :: String; sorting :: T
   1.177 +(sortingN, sorting) = markup_elem \<open>Markup.sortingN\<close>
   1.178 +
   1.179 +typingN :: String; typing :: T
   1.180 +(typingN, typing) = markup_elem \<open>Markup.typingN\<close>
   1.181 +
   1.182 +class_parameterN :: String; class_parameter :: T
   1.183 +(class_parameterN, class_parameter) = markup_elem \<open>Markup.class_parameterN\<close>
   1.184 +
   1.185 +
   1.186 +{- antiquotations -}
   1.187 +
   1.188 +antiquotedN :: String; antiquoted :: T
   1.189 +(antiquotedN, antiquoted) = markup_elem \<open>Markup.antiquotedN\<close>
   1.190 +
   1.191 +antiquoteN :: String; antiquote :: T
   1.192 +(antiquoteN, antiquote) = markup_elem \<open>Markup.antiquoteN\<close>
   1.193 +
   1.194 +
   1.195 +{- text structure -}
   1.196 +
   1.197 +paragraphN :: String; paragraph :: T
   1.198 +(paragraphN, paragraph) = markup_elem \<open>Markup.paragraphN\<close>
   1.199 +
   1.200 +text_foldN :: String; text_fold :: T
   1.201 +(text_foldN, text_fold) = markup_elem \<open>Markup.text_foldN\<close>
   1.202 +
   1.203 +
   1.204 +{- outer syntax -}
   1.205 +
   1.206 +keyword1N :: String; keyword1 :: T
   1.207 +(keyword1N, keyword1) = markup_elem \<open>Markup.keyword1N\<close>
   1.208 +
   1.209 +keyword2N :: String; keyword2 :: T
   1.210 +(keyword2N, keyword2) = markup_elem \<open>Markup.keyword2N\<close>
   1.211 +
   1.212 +keyword3N :: String; keyword3 :: T
   1.213 +(keyword3N, keyword3) = markup_elem \<open>Markup.keyword3N\<close>
   1.214 +
   1.215 +quasi_keywordN :: String; quasi_keyword :: T
   1.216 +(quasi_keywordN, quasi_keyword) = markup_elem \<open>Markup.quasi_keywordN\<close>
   1.217 +
   1.218 +improperN :: String; improper :: T
   1.219 +(improperN, improper) = markup_elem \<open>Markup.improperN\<close>
   1.220 +
   1.221 +operatorN :: String; operator :: T
   1.222 +(operatorN, operator) = markup_elem \<open>Markup.operatorN\<close>
   1.223 +
   1.224 +stringN :: String; string :: T
   1.225 +(stringN, string) = markup_elem \<open>Markup.stringN\<close>
   1.226 +
   1.227 +alt_stringN :: String; alt_string :: T
   1.228 +(alt_stringN, alt_string) = markup_elem \<open>Markup.alt_stringN\<close>
   1.229 +
   1.230 +verbatimN :: String; verbatim :: T
   1.231 +(verbatimN, verbatim) = markup_elem \<open>Markup.verbatimN\<close>
   1.232 +
   1.233 +cartoucheN :: String; cartouche :: T
   1.234 +(cartoucheN, cartouche) = markup_elem \<open>Markup.cartoucheN\<close>
   1.235 +
   1.236 +commentN :: String; comment :: T
   1.237 +(commentN, comment) = markup_elem \<open>Markup.commentN\<close>
   1.238 +
   1.239 +
   1.240 +{- messages -}
   1.241 +
   1.242 +writelnN :: String; writeln :: T
   1.243 +(writelnN, writeln) = markup_elem \<open>Markup.writelnN\<close>
   1.244 +
   1.245 +stateN :: String; state :: T
   1.246 +(stateN, state) = markup_elem \<open>Markup.stateN\<close>
   1.247 +
   1.248 +informationN :: String; information :: T
   1.249 +(informationN, information) = markup_elem \<open>Markup.informationN\<close>
   1.250 +
   1.251 +tracingN :: String; tracing :: T
   1.252 +(tracingN, tracing) = markup_elem \<open>Markup.tracingN\<close>
   1.253 +
   1.254 +warningN :: String; warning :: T
   1.255 +(warningN, warning) = markup_elem \<open>Markup.warningN\<close>
   1.256 +
   1.257 +legacyN :: String; legacy :: T
   1.258 +(legacyN, legacy) = markup_elem \<open>Markup.legacyN\<close>
   1.259 +
   1.260 +errorN :: String; error :: T
   1.261 +(errorN, error) = markup_elem \<open>Markup.errorN\<close>
   1.262 +
   1.263 +reportN :: String; report :: T
   1.264 +(reportN, report) = markup_elem \<open>Markup.reportN\<close>
   1.265 +
   1.266 +no_reportN :: String; no_report :: T
   1.267 +(no_reportN, no_report) = markup_elem \<open>Markup.no_reportN\<close>
   1.268 +
   1.269 +intensifyN :: String; intensify :: T
   1.270 +(intensifyN, intensify) = markup_elem \<open>Markup.intensifyN\<close>
   1.271 +
   1.272 +
   1.273 +{- output -}
   1.274  
   1.275  type Output = (String, String)
   1.276  
   1.277 @@ -246,9 +481,9 @@
   1.278  
   1.279  {- wrapped elements -}
   1.280  
   1.281 -xml_elemN = "xml_elem";
   1.282 -xml_nameN = "xml_name";
   1.283 -xml_bodyN = "xml_body";
   1.284 +xml_elemN = \<open>XML.xml_elemN\<close>
   1.285 +xml_nameN = \<open>XML.xml_nameN\<close>
   1.286 +xml_bodyN = \<open>XML.xml_bodyN\<close>
   1.287  
   1.288  wrap_elem (((a, atts), body1), body2) =
   1.289    Elem (xml_elemN, (xml_nameN, a) : atts) (Elem (xml_bodyN, []) body1 : body2)