equal
deleted
inserted
replaced
6 |
6 |
7 theory Haskell |
7 theory Haskell |
8 imports Pure |
8 imports Pure |
9 begin |
9 begin |
10 |
10 |
11 generate_file "Library.hs" = \<open> |
11 generate_file "Isabelle/Library.hs" = \<open> |
12 {- Title: Tools/Haskell/Library.hs |
12 {- Title: Tools/Haskell/Library.hs |
13 Author: Makarius |
13 Author: Makarius |
14 LICENSE: BSD 3-clause (Isabelle) |
14 LICENSE: BSD 3-clause (Isabelle) |
15 |
15 |
16 Basic library of Isabelle idioms. |
16 Basic library of Isabelle idioms. |
100 |
100 |
101 clean_name :: String -> String |
101 clean_name :: String -> String |
102 clean_name = reverse #> dropWhile (== '_') #> reverse |
102 clean_name = reverse #> dropWhile (== '_') #> reverse |
103 \<close> |
103 \<close> |
104 |
104 |
105 generate_file "Value.hs" = \<open> |
105 generate_file "Isabelle/Value.hs" = \<open> |
106 {- Title: Haskell/Tools/Value.hs |
106 {- Title: Haskell/Tools/Value.hs |
107 Author: Makarius |
107 Author: Makarius |
108 LICENSE: BSD 3-clause (Isabelle) |
108 LICENSE: BSD 3-clause (Isabelle) |
109 |
109 |
110 Plain values, represented as string. |
110 Plain values, represented as string. |
153 |
153 |
154 parse_real :: String -> Maybe Double |
154 parse_real :: String -> Maybe Double |
155 parse_real = Read.readMaybe |
155 parse_real = Read.readMaybe |
156 \<close> |
156 \<close> |
157 |
157 |
158 generate_file "Buffer.hs" = \<open> |
158 generate_file "Isabelle/Buffer.hs" = \<open> |
159 {- Title: Tools/Haskell/Buffer.hs |
159 {- Title: Tools/Haskell/Buffer.hs |
160 Author: Makarius |
160 Author: Makarius |
161 LICENSE: BSD 3-clause (Isabelle) |
161 LICENSE: BSD 3-clause (Isabelle) |
162 |
162 |
163 Efficient text buffers. |
163 Efficient text buffers. |
179 |
179 |
180 content :: T -> String |
180 content :: T -> String |
181 content (Buffer xs) = concat (reverse xs) |
181 content (Buffer xs) = concat (reverse xs) |
182 \<close> |
182 \<close> |
183 |
183 |
184 generate_file "Properties.hs" = \<open> |
184 generate_file "Isabelle/Properties.hs" = \<open> |
185 {- Title: Tools/Haskell/Properties.hs |
185 {- Title: Tools/Haskell/Properties.hs |
186 Author: Makarius |
186 Author: Makarius |
187 LICENSE: BSD 3-clause (Isabelle) |
187 LICENSE: BSD 3-clause (Isabelle) |
188 |
188 |
189 Property lists. |
189 Property lists. |
213 remove name props = |
213 remove name props = |
214 if defined props name then filter (\(a, _) -> a /= name) props |
214 if defined props name then filter (\(a, _) -> a /= name) props |
215 else props |
215 else props |
216 \<close> |
216 \<close> |
217 |
217 |
218 generate_file "Markup.hs" = \<open> |
218 generate_file "Isabelle/Markup.hs" = \<open> |
219 {- Title: Haskell/Tools/Markup.hs |
219 {- Title: Haskell/Tools/Markup.hs |
220 Author: Makarius |
220 Author: Makarius |
221 LICENSE: BSD 3-clause (Isabelle) |
221 LICENSE: BSD 3-clause (Isabelle) |
222 |
222 |
223 Quasi-abstract markup elements. |
223 Quasi-abstract markup elements. |
583 |
583 |
584 no_output :: Output |
584 no_output :: Output |
585 no_output = ("", "") |
585 no_output = ("", "") |
586 \<close> |
586 \<close> |
587 |
587 |
588 generate_file "Completion.hs" = \<open> |
588 generate_file "Isabelle/Completion.hs" = \<open> |
589 {- Title: Tools/Haskell/Completion.hs |
589 {- Title: Tools/Haskell/Completion.hs |
590 Author: Makarius |
590 Author: Makarius |
591 LICENSE: BSD 3-clause (Isabelle) |
591 LICENSE: BSD 3-clause (Isabelle) |
592 |
592 |
593 Completion of names. |
593 Completion of names. |
644 make_report :: Int -> (String, Properties.T) -> ((String -> Bool) -> [Name]) -> String |
644 make_report :: Int -> (String, Properties.T) -> ((String -> Bool) -> [Name]) -> String |
645 make_report limit name_props make_names = |
645 make_report limit name_props make_names = |
646 markup_report [make limit name_props make_names] |
646 markup_report [make limit name_props make_names] |
647 \<close> |
647 \<close> |
648 |
648 |
649 generate_file "File.hs" = \<open> |
649 generate_file "Isabelle/File.hs" = \<open> |
650 {- Title: Tools/Haskell/File.hs |
650 {- Title: Tools/Haskell/File.hs |
651 Author: Makarius |
651 Author: Makarius |
652 LICENSE: BSD 3-clause (Isabelle) |
652 LICENSE: BSD 3-clause (Isabelle) |
653 |
653 |
654 File-system operations. |
654 File-system operations. |
679 append :: IO.FilePath -> String -> IO () |
679 append :: IO.FilePath -> String -> IO () |
680 append path s = |
680 append path s = |
681 IO.withFile path IO.AppendMode (\h -> do setup h; IO.hPutStr h s) |
681 IO.withFile path IO.AppendMode (\h -> do setup h; IO.hPutStr h s) |
682 \<close> |
682 \<close> |
683 |
683 |
684 generate_file "XML.hs" = \<open> |
684 generate_file "Isabelle/XML.hs" = \<open> |
685 {- Title: Tools/Haskell/XML.hs |
685 {- Title: Tools/Haskell/XML.hs |
686 Author: Makarius |
686 Author: Makarius |
687 LICENSE: BSD 3-clause (Isabelle) |
687 LICENSE: BSD 3-clause (Isabelle) |
688 |
688 |
689 Untyped XML trees and representation of ML values. |
689 Untyped XML trees and representation of ML values. |
758 unwords (name : map (\(a, x) -> a ++ "=\"" ++ show_text x ++ "\"") atts) |
758 unwords (name : map (\(a, x) -> a ++ "=\"" ++ show_text x ++ "\"") atts) |
759 |
759 |
760 show_text = concatMap encode |
760 show_text = concatMap encode |
761 \<close> |
761 \<close> |
762 |
762 |
763 generate_file "XML/Encode.hs" = \<open> |
763 generate_file "Isabelle/XML/Encode.hs" = \<open> |
764 {- Title: Tools/Haskell/XML/Encode.hs |
764 {- Title: Tools/Haskell/XML/Encode.hs |
765 Author: Makarius |
765 Author: Makarius |
766 LICENSE: BSD 3-clause (Isabelle) |
766 LICENSE: BSD 3-clause (Isabelle) |
767 |
767 |
768 XML as data representation language. |
768 XML as data representation language. |
844 |
844 |
845 variant :: [V a] -> T a |
845 variant :: [V a] -> T a |
846 variant fs x = [tagged (the (get_index (\f -> f x) fs))] |
846 variant fs x = [tagged (the (get_index (\f -> f x) fs))] |
847 \<close> |
847 \<close> |
848 |
848 |
849 generate_file "XML/Decode.hs" = \<open> |
849 generate_file "Isabelle/XML/Decode.hs" = \<open> |
850 {- Title: Tools/Haskell/XML/Decode.hs |
850 {- Title: Tools/Haskell/XML/Decode.hs |
851 Author: Makarius |
851 Author: Makarius |
852 LICENSE: BSD 3-clause (Isabelle) |
852 LICENSE: BSD 3-clause (Isabelle) |
853 |
853 |
854 XML as data representation language. |
854 XML as data representation language. |
955 variant fs [t] = (fs !! tag) (xs, ts) |
955 variant fs [t] = (fs !! tag) (xs, ts) |
956 where (tag, (xs, ts)) = tagged t |
956 where (tag, (xs, ts)) = tagged t |
957 variant _ _ = err_body |
957 variant _ _ = err_body |
958 \<close> |
958 \<close> |
959 |
959 |
960 generate_file "YXML.hs" = \<open> |
960 generate_file "Isabelle/YXML.hs" = \<open> |
961 {- Title: Tools/Haskell/YXML.hs |
961 {- Title: Tools/Haskell/YXML.hs |
962 Author: Makarius |
962 Author: Makarius |
963 LICENSE: BSD 3-clause (Isabelle) |
963 LICENSE: BSD 3-clause (Isabelle) |
964 |
964 |
965 Efficient text representation of XML trees. Suitable for direct |
965 Efficient text representation of XML trees. Suitable for direct |
1083 [result] -> result |
1083 [result] -> result |
1084 [] -> XML.Text "" |
1084 [] -> XML.Text "" |
1085 _ -> err "multiple results" |
1085 _ -> err "multiple results" |
1086 \<close> |
1086 \<close> |
1087 |
1087 |
1088 generate_file "Pretty.hs" = \<open> |
1088 generate_file "Isabelle/Pretty.hs" = \<open> |
1089 {- Title: Tools/Haskell/Pretty.hs |
1089 {- Title: Tools/Haskell/Pretty.hs |
1090 Author: Makarius |
1090 Author: Makarius |
1091 LICENSE: BSD 3-clause (Isabelle) |
1091 LICENSE: BSD 3-clause (Isabelle) |
1092 |
1092 |
1093 Generic pretty printing module. |
1093 Generic pretty printing module. |
1237 |
1237 |
1238 big_list :: String -> [T] -> T |
1238 big_list :: String -> [T] -> T |
1239 big_list name prts = block (fbreaks (str name : prts)) |
1239 big_list name prts = block (fbreaks (str name : prts)) |
1240 \<close> |
1240 \<close> |
1241 |
1241 |
1242 generate_file "Term.hs" = \<open> |
1242 generate_file "Isabelle/Term.hs" = \<open> |
1243 {- Title: Tools/Haskell/Term.hs |
1243 {- Title: Tools/Haskell/Term.hs |
1244 Author: Makarius |
1244 Author: Makarius |
1245 LICENSE: BSD 3-clause (Isabelle) |
1245 LICENSE: BSD 3-clause (Isabelle) |
1246 |
1246 |
1247 Lambda terms, types, sorts. |
1247 Lambda terms, types, sorts. |
1284 | Abs (String, Typ, Term) |
1284 | Abs (String, Typ, Term) |
1285 | App (Term, Term) |
1285 | App (Term, Term) |
1286 deriving Show |
1286 deriving Show |
1287 \<close> |
1287 \<close> |
1288 |
1288 |
1289 generate_file "Term_XML/Encode.hs" = \<open> |
1289 generate_file "Isabelle/Term_XML/Encode.hs" = \<open> |
1290 {- Title: Tools/Haskell/Term_XML/Encode.hs |
1290 {- Title: Tools/Haskell/Term_XML/Encode.hs |
1291 Author: Makarius |
1291 Author: Makarius |
1292 LICENSE: BSD 3-clause (Isabelle) |
1292 LICENSE: BSD 3-clause (Isabelle) |
1293 |
1293 |
1294 XML data representation of lambda terms. |
1294 XML data representation of lambda terms. |
1326 \case { Bound a -> Just ([int_atom a], []); _ -> Nothing }, |
1326 \case { Bound a -> Just ([int_atom a], []); _ -> Nothing }, |
1327 \case { Abs (a, b, c) -> Just ([a], pair typ term (b, c)); _ -> Nothing }, |
1327 \case { Abs (a, b, c) -> Just ([a], pair typ term (b, c)); _ -> Nothing }, |
1328 \case { App a -> Just ([], pair term term a); _ -> Nothing }] |
1328 \case { App a -> Just ([], pair term term a); _ -> Nothing }] |
1329 \<close> |
1329 \<close> |
1330 |
1330 |
1331 generate_file "Term_XML/Decode.hs" = \<open> |
1331 generate_file "Isabelle/Term_XML/Decode.hs" = \<open> |
1332 {- Title: Tools/Haskell/Term_XML/Decode.hs |
1332 {- Title: Tools/Haskell/Term_XML/Decode.hs |
1333 Author: Makarius |
1333 Author: Makarius |
1334 LICENSE: BSD 3-clause (Isabelle) |
1334 LICENSE: BSD 3-clause (Isabelle) |
1335 |
1335 |
1336 XML data representation of lambda terms. |
1336 XML data representation of lambda terms. |