more general command 'generate_file' for registered file types, notably Haskell;
discontinued 'generate_haskell_file', 'export_haskell_file';
eliminated generated sources: compile files in tmp dir;
--- a/NEWS Fri Nov 30 23:30:42 2018 +0100
+++ b/NEWS Fri Nov 30 23:43:10 2018 +0100
@@ -119,24 +119,27 @@
potentially with variations on ML syntax (existing ML_Env.SML_operations
observes the official standard).
-* GHC.read_source reads Haskell source text with antiquotations (only
-the control-cartouche form). The default "cartouche" antiquotation
-evaluates an ML expression of type string and inlines the result as
-Haskell string literal. This allows to refer to Isabelle items robustly,
-e.g. via Isabelle/ML antiquotations or library operations. For example:
-
-ML_command \<open>
- GHC.read_source \<^context> \<open>
+* ML antiquotation @{master_dir} refers to the master directory of the
+underlying theory, i.e. the directory of the theory file.
+
+* Command 'generate_file' allows to produce sources for other languages,
+with antiquotations in the Isabelle context (only the control-cartouche
+form). The default "cartouche" antiquotation evaluates an ML expression
+of type string and inlines the result as a string literal of the target
+language. For example, this works for Haskell as follows:
+
+ generate_file "Pure.hs" = \<open>
+ module Isabelle.Pure where
allConst, impConst, eqConst :: String
allConst = \<open>\<^const_name>\<open>Pure.all\<close>\<close>
impConst = \<open>\<^const_name>\<open>Pure.imp\<close>\<close>
eqConst = \<open>\<^const_name>\<open>Pure.eq\<close>\<close>
\<close>
- |> writeln
-\<close>
-
-* ML antiquotation @{master_dir} refers to the master directory of the
-underlying theory, i.e. the directory of the theory file.
+
+The ML function Generate_File.generate writes all generated files from a
+given theory to the file-system, e.g. a temporary directory where some
+external compiler is applied.
+
*** System ***
--- a/src/Pure/General/path.ML Fri Nov 30 23:30:42 2018 +0100
+++ b/src/Pure/General/path.ML Fri Nov 30 23:43:10 2018 +0100
@@ -15,6 +15,7 @@
val parent: T
val basic: string -> T
val variable: string -> T
+ val has_parent: T -> bool
val is_absolute: T -> bool
val is_basic: T -> bool
val starts_basic: T -> bool
@@ -88,6 +89,8 @@
fun variable s = Path [variable_elem s];
val parent = Path [Parent];
+fun has_parent (Path xs) = exists (fn Parent => true | _ => false) xs;
+
fun is_absolute (Path xs) =
(case try List.last xs of
SOME (Root _) => true
--- a/src/Pure/PIDE/markup.ML Fri Nov 30 23:30:42 2018 +0100
+++ b/src/Pure/PIDE/markup.ML Fri Nov 30 23:43:10 2018 +0100
@@ -31,7 +31,6 @@
val language_prop: bool -> T
val language_ML: bool -> T
val language_SML: bool -> T
- val language_haskell: bool -> T
val language_document: bool -> T
val language_antiquotation: T
val language_text: bool -> T
@@ -116,8 +115,9 @@
val ML_breakpointN: string val ML_breakpoint: int -> T
val antiquotedN: string val antiquoted: T
val antiquoteN: string val antiquote: T
+ val file_typeN: string
+ val antiquotationN: string
val ML_antiquotationN: string
- val haskell_antiquotationN: string
val document_antiquotationN: string
val document_antiquotation_optionN: string
val paragraphN: string val paragraph: T
@@ -306,7 +306,6 @@
val language_prop = language' {name = "prop", symbols = true, antiquotes = false};
val language_ML = language' {name = "ML", symbols = false, antiquotes = true};
val language_SML = language' {name = "SML", symbols = false, antiquotes = false};
-val language_haskell = language' {name = "Haskell", symbols = false, antiquotes = true};
val language_document = language' {name = "document", symbols = false, antiquotes = true};
val language_antiquotation =
language {name = "antiquotation", symbols = true, antiquotes = false, delimited = true};
@@ -476,8 +475,9 @@
val (antiquotedN, antiquoted) = markup_elem "antiquoted";
val (antiquoteN, antiquote) = markup_elem "antiquote";
+val file_typeN = "file_type";
+val antiquotationN = "antiquotation";
val ML_antiquotationN = "ML_antiquotation";
-val haskell_antiquotationN = "Haskell_antiquotation";
val document_antiquotationN = "document_antiquotation";
val document_antiquotation_optionN = "document_antiquotation_option";
--- a/src/Pure/Pure.thy Fri Nov 30 23:30:42 2018 +0100
+++ b/src/Pure/Pure.thy Fri Nov 30 23:43:10 2018 +0100
@@ -21,6 +21,7 @@
"no_notation" "axiomatization" "alias" "type_alias" "lemmas" "declare"
"hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
and "external_file" "bibtex_file" :: thy_load
+ and "generate_file" :: thy_decl
and "ML_file" "ML_file_debug" "ML_file_no_debug" :: thy_load % "ML"
and "SML_file" "SML_file_debug" "SML_file_no_debug" :: thy_load % "ML"
and "SML_import" "SML_export" "ML_export" :: thy_decl % "ML"
@@ -117,6 +118,13 @@
val ([{lines, pos, ...}], thy') = files thy;
val _ = Bibtex.check_database_output pos (cat_lines lines);
in thy' end)));
+
+ val _ =
+ Outer_Syntax.local_theory \<^command_keyword>\<open>generate_file\<close>
+ "generate source file, with antiquotations"
+ (Parse.position Parse.path -- (\<^keyword>\<open>=\<close> |-- Parse.input Parse.embedded)
+ >> Generate_File.generate_file_cmd);
+
in end\<close>
--- a/src/Pure/ROOT.ML Fri Nov 30 23:30:42 2018 +0100
+++ b/src/Pure/ROOT.ML Fri Nov 30 23:43:10 2018 +0100
@@ -347,3 +347,4 @@
ML_file "Tools/named_theorems.ML";
ML_file "Tools/jedit.ML";
ML_file "Tools/ghc.ML";
+ML_file "Tools/generate_file.ML"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/generate_file.ML Fri Nov 30 23:43:10 2018 +0100
@@ -0,0 +1,218 @@
+(* Title: Pure/Tools/generate_file.ML
+ Author: Makarius
+
+Generate source files for other languages (with antiquotations, without Isabelle symbols).
+*)
+
+signature GENERATE_FILE =
+sig
+ type file_type =
+ {name: string, ext: string, make_comment: string -> string, make_string: string -> string}
+ val file_type:
+ binding -> {ext: string, make_comment: string -> string, make_string: string -> string} ->
+ theory -> theory
+ val antiquotation: binding -> 'a Token.context_parser ->
+ ({context: Proof.context, source: Token.src, file_type: file_type, argument: 'a} -> string) ->
+ theory -> theory
+ val set_string: string -> Proof.context -> Proof.context
+ val generate_file_cmd: (string * Position.T) * Input.source -> local_theory -> local_theory
+ val generate: theory -> Path.T -> Path.T list
+end;
+
+structure Generate_File: GENERATE_FILE =
+struct
+
+(** context data **)
+
+type file_type =
+ {name: string, ext: string, make_comment: string -> string, make_string: string -> string};
+
+type antiquotation = Token.src -> Proof.context -> file_type -> string;
+
+structure Data = Theory_Data
+(
+ type T =
+ file_type Name_Space.table * (*file types*)
+ antiquotation Name_Space.table * (*antiquotations*)
+ (Path.T * (Position.T * string)) list; (*generated files for current theory*)
+ val empty =
+ (Name_Space.empty_table Markup.file_typeN,
+ Name_Space.empty_table Markup.antiquotationN,
+ []);
+ val extend = @{apply 3(3)} (K []);
+ fun merge ((types1, antiqs1, _), (types2, antiqs2, _)) =
+ (Name_Space.merge_tables (types1, types2),
+ Name_Space.merge_tables (antiqs1, antiqs2),
+ []);
+);
+
+val get_files = rev o #3 o Data.get;
+
+fun add_files (path, (pos, text)) =
+ (Data.map o @{apply 3(3)}) (fn files =>
+ (case AList.lookup (op =) files path of
+ SOME (pos', _) =>
+ error ("Duplicate generated file " ^ Path.print path ^ Position.here_list [pos, pos'])
+ | NONE => (path, (pos, text)) :: files));
+
+
+(* file types *)
+
+fun the_file_type thy ext =
+ if ext = "" then error "Bad file extension"
+ else
+ (#1 (Data.get thy), NONE) |-> Name_Space.fold_table
+ (fn (_, file_type) => fn res =>
+ if #ext file_type = ext then SOME file_type else res)
+ |> (fn SOME file_type => file_type
+ | NONE => error ("Unknown file type for extension " ^ quote ext));
+
+fun file_type binding {ext, make_comment, make_string} thy =
+ let
+ val name = Binding.name_of binding;
+ val pos = Binding.pos_of binding;
+ val file_type = {name = name, ext = ext, make_comment = make_comment, make_string = make_string};
+
+ val table = #1 (Data.get thy);
+ val space = Name_Space.space_of_table table;
+ val context = Context.Theory thy |> Name_Space.map_naming (K Name_Space.global_naming);
+ val (_, data') = table |> Name_Space.define context true (Binding.make (name, pos), file_type);
+
+ val _ =
+ (case try (#name o the_file_type thy) ext of
+ NONE => ()
+ | SOME name' =>
+ error ("Extension " ^ quote ext ^ " already registered for file type " ^
+ quote (Markup.markup (Name_Space.markup space name') name') ^ Position.here pos));
+ in thy |> (Data.map o @{apply 3(1)}) (K data') end;
+
+
+(* antiquotations *)
+
+val get_antiquotations = #2 o Data.get o Proof_Context.theory_of;
+
+fun antiquotation name scan body thy =
+ let
+ fun ant src ctxt file_type : string =
+ let val (x, ctxt') = Token.syntax scan src ctxt
+ in body {context = ctxt', source = src, file_type = file_type, argument = x} end;
+ in
+ thy
+ |> (Data.map o @{apply 3(2)}) (Name_Space.define (Context.Theory thy) true (name, ant) #> #2)
+ end;
+
+val scan_antiq =
+ Antiquote.scan_control >> Antiquote.Control ||
+ Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (Antiquote.Text o Symbol_Pos.symbol);
+
+fun read_source ctxt (file_type: file_type) source =
+ let
+ val _ =
+ Context_Position.report ctxt (Input.pos_of source)
+ (Markup.language
+ {name = #name file_type, symbols = false, antiquotes = true,
+ delimited = Input.is_delimited source});
+
+ val (input, _) =
+ Input.source_explode source
+ |> Scan.error (Scan.finite Symbol_Pos.stopper (Scan.repeat scan_antiq));
+
+ val _ = Context_Position.reports ctxt (Antiquote.antiq_reports input);
+
+ fun expand antiq =
+ (case antiq of
+ Antiquote.Text s => s
+ | Antiquote.Control {name, body, ...} =>
+ let
+ val src = Token.make_src name (if null body then [] else [Token.read_cartouche body]);
+ val (src', ant) = Token.check_src ctxt get_antiquotations src;
+ in ant src' ctxt file_type end
+ | Antiquote.Antiq antiq => error ("Bad antiquotation " ^ Position.here (#1 (#range antiq))));
+ in implode (map expand input) end;
+
+
+(* generate files *)
+
+fun generate_file_cmd ((file, pos), source) lthy =
+ let
+ val thy = Proof_Context.theory_of lthy;
+
+ val path = Path.expand (Path.explode file);
+ fun err_path msg = error (msg ^ ": " ^ Path.print path ^ Position.here pos);
+ val _ =
+ if Path.is_absolute path then err_path "Illegal absolute path"
+ else if Path.has_parent path then err_path "Illegal parent path"
+ else ();
+
+ val file_type =
+ the_file_type thy (#2 (Path.split_ext path))
+ handle ERROR msg => error (msg ^ Position.here pos);
+
+ val header = #make_comment file_type " generated by Isabelle ";
+ val text = header ^ "\n" ^ read_source lthy file_type source;
+ in lthy |> (Local_Theory.background_theory o add_files) (path, (pos, text)) end;
+
+fun generate thy dir =
+ thy |> get_files |> List.map (fn (path, (_, text)) =>
+ let
+ val path' = Path.expand (Path.append dir path);
+ val _ = Isabelle_System.mkdirs (Path.dir path');
+ val _ = File.generate path' text;
+ in path end);
+
+
+
+(** concrete file types **)
+
+val _ =
+ Theory.setup
+ (file_type \<^binding>\<open>Haskell\<close>
+ {ext = "hs",
+ make_comment = enclose "{-" "-}",
+ make_string = GHC.print_string});
+
+
+
+(** concrete antiquotations **)
+
+(* ML expression as string literal *)
+
+structure Local_Data = Proof_Data
+(
+ type T = string option;
+ fun init _ = NONE;
+);
+
+val set_string = Local_Data.put o SOME;
+
+fun the_string ctxt =
+ (case Local_Data.get ctxt of
+ SOME s => s
+ | NONE => raise Fail "No result string");
+
+val _ =
+ Theory.setup
+ (antiquotation \<^binding>\<open>cartouche\<close> (Scan.lift Args.cartouche_input)
+ (fn {context = ctxt, file_type, argument, ...} =>
+ ctxt |> Context.proof_map
+ (ML_Context.expression (Input.pos_of argument)
+ (ML_Lex.read "Theory.local_setup (Generate_File.set_string (" @
+ ML_Lex.read_source argument @ ML_Lex.read "))"))
+ |> the_string |> #make_string file_type));
+
+
+(* file-system paths *)
+
+fun path_antiquotation binding check =
+ antiquotation binding
+ (Args.context -- Scan.lift (Parse.position Parse.path) >>
+ (fn (ctxt, (name, pos)) => (check ctxt Path.current (name, pos) |> Path.implode)))
+ (fn {file_type, argument, ...} => #make_string file_type argument);
+
+val _ =
+ Theory.setup
+ (path_antiquotation \<^binding>\<open>path\<close> Resources.check_path #>
+ path_antiquotation \<^binding>\<open>file\<close> Resources.check_file #>
+ path_antiquotation \<^binding>\<open>dir\<close> Resources.check_dir);
+
+end;
--- a/src/Pure/Tools/ghc.ML Fri Nov 30 23:30:42 2018 +0100
+++ b/src/Pure/Tools/ghc.ML Fri Nov 30 23:43:10 2018 +0100
@@ -9,10 +9,6 @@
val print_codepoint: UTF8.codepoint -> string
val print_symbol: Symbol.symbol -> string
val print_string: string -> string
- val antiquotation: binding -> 'a Token.context_parser ->
- ({context: Proof.context, source: Token.src, argument: 'a} -> string) -> theory -> theory
- val read_source: Proof.context -> Input.source -> string
- val set_result: string -> Proof.context -> Proof.context
end;
structure GHC: GHC =
@@ -46,89 +42,4 @@
val print_string = quote o implode o map print_symbol o Symbol.explode;
-
-(** antiquotations **)
-
-(* theory data *)
-
-structure Antiqs = Theory_Data
-(
- type T = (Token.src -> Proof.context -> string) Name_Space.table;
- val empty : T = Name_Space.empty_table Markup.haskell_antiquotationN;
- val extend = I;
- fun merge tabs : T = Name_Space.merge_tables tabs;
-);
-
-val get_antiquotations = Antiqs.get o Proof_Context.theory_of;
-
-fun antiquotation name scan body thy =
- let
- fun antiq src ctxt =
- let val (x, ctxt') = Token.syntax scan src ctxt
- in body {context = ctxt', source = src, argument = x} end;
- in thy |> Antiqs.map (Name_Space.define (Context.Theory thy) true (name, antiq) #> #2) end;
-
-
-(* read source and expand antiquotations *)
-
-val scan_antiq =
- Antiquote.scan_control >> Antiquote.Control ||
- Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (Antiquote.Text o Symbol_Pos.symbol);
-
-fun read_source ctxt source =
- let
- val _ =
- Context_Position.report ctxt (Input.pos_of source)
- (Markup.language_haskell (Input.is_delimited source));
-
- val (input, _) =
- Input.source_explode source
- |> Scan.error (Scan.finite Symbol_Pos.stopper (Scan.repeat scan_antiq));
-
- val _ = Context_Position.reports ctxt (Antiquote.antiq_reports input);
-
- fun expand antiq =
- (case antiq of
- Antiquote.Text s => s
- | Antiquote.Control {name, body, ...} =>
- let
- val src = Token.make_src name (if null body then [] else [Token.read_cartouche body]);
- val (src', f) = Token.check_src ctxt get_antiquotations src;
- in f src' ctxt end
- | Antiquote.Antiq antiq => error ("Bad antiquotation " ^ Position.here (#1 (#range antiq))));
- in implode (map expand input) end;
-
-
-(* concrete antiquotation: ML expression as Haskell string literal *)
-
-structure Local_Data = Proof_Data
-(
- type T = string option;
- fun init _ = NONE;
-);
-
-val set_result = Local_Data.put o SOME;
-
-fun the_result ctxt =
- (case Local_Data.get ctxt of
- SOME s => s
- | NONE => raise Fail "No result");
-
-fun path_antiq check =
- Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, (name, pos)) =>
- (check ctxt Path.current (name, pos) |> Path.implode |> print_string));
-
-val _ =
- Theory.setup
- (antiquotation \<^binding>\<open>cartouche\<close> (Scan.lift Args.cartouche_input)
- (fn {context = ctxt, argument, ...} =>
- ctxt |> Context.proof_map
- (ML_Context.expression (Input.pos_of argument)
- (ML_Lex.read "Theory.local_setup (GHC.set_result (" @
- ML_Lex.read_source argument @ ML_Lex.read "))"))
- |> the_result |> print_string) #>
- antiquotation \<^binding>\<open>path\<close> (path_antiq Resources.check_path) #argument #>
- antiquotation \<^binding>\<open>file\<close> (path_antiq Resources.check_file) #argument #>
- antiquotation \<^binding>\<open>dir\<close> (path_antiq Resources.check_dir) #argument);
-
end;
--- a/src/Tools/Haskell/Buffer.hs Fri Nov 30 23:30:42 2018 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-{- generated by Isabelle -}
-
-{- Title: Tools/Haskell/Buffer.hs
- Author: Makarius
- LICENSE: BSD 3-clause (Isabelle)
-
-Efficient text buffers.
-
-See also "$ISABELLE_HOME/src/Pure/General/buffer.ML".
--}
-
-module Isabelle.Buffer (T, empty, add, content)
-where
-
-newtype T = Buffer [String]
-
-empty :: T
-empty = Buffer []
-
-add :: String -> T -> T
-add "" buf = buf
-add x (Buffer xs) = Buffer (x : xs)
-
-content :: T -> String
-content (Buffer xs) = concat (reverse xs)
--- a/src/Tools/Haskell/Completion.hs Fri Nov 30 23:30:42 2018 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,60 +0,0 @@
-{- generated by Isabelle -}
-
-{- Title: Tools/Haskell/Completion.hs
- Author: Makarius
- LICENSE: BSD 3-clause (Isabelle)
-
-Completion of names.
-
-See also "$ISABELLE_HOME/src/Pure/General/completion.ML".
--}
-
-module Isabelle.Completion (
- Name, T, names, none, make, markup_element, markup_report, make_report
- ) where
-
-import qualified Data.List as List
-
-import Isabelle.Library
-import qualified Isabelle.Properties as Properties
-import qualified Isabelle.Markup as Markup
-import qualified Isabelle.XML.Encode as Encode
-import qualified Isabelle.XML as XML
-import qualified Isabelle.YXML as YXML
-
-
-type Name = (String, (String, String)) -- external name, kind, internal name
-data T = Completion Properties.T Int [Name] -- position, total length, names
-
-names :: Int -> Properties.T -> [Name] -> T
-names limit props names = Completion props (length names) (take limit names)
-
-none :: T
-none = names 0 [] []
-
-make :: Int -> (String, Properties.T) -> ((String -> Bool) -> [Name]) -> T
-make limit (name, props) make_names =
- if name /= "" && name /= "_"
- then names limit props (make_names $ List.isPrefixOf $ clean_name name)
- else none
-
-markup_element :: T -> (Markup.T, XML.Body)
-markup_element (Completion props total names) =
- if not (null names) then
- let
- markup = Markup.properties props Markup.completion
- body =
- Encode.pair Encode.int
- (Encode.list (Encode.pair Encode.string (Encode.pair Encode.string Encode.string)))
- (total, names)
- in (markup, body)
- else (Markup.empty, [])
-
-markup_report :: [T] -> String
-markup_report [] = ""
-markup_report elems =
- YXML.string_of $ XML.Elem (Markup.report, map (XML.Elem . markup_element) elems)
-
-make_report :: Int -> (String, Properties.T) -> ((String -> Bool) -> [Name]) -> String
-make_report limit name_props make_names =
- markup_report [make limit name_props make_names]
--- a/src/Tools/Haskell/File.hs Fri Nov 30 23:30:42 2018 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,34 +0,0 @@
-{- generated by Isabelle -}
-
-{- Title: Tools/Haskell/File.hs
- Author: Makarius
- LICENSE: BSD 3-clause (Isabelle)
-
-File-system operations.
-
-See also "$ISABELLE_HOME/src/Pure/General/file.ML".
--}
-
-module Isabelle.File (setup, read, write, append) where
-
-import Prelude hiding (read)
-import System.IO (IO)
-import qualified System.IO as IO
-
-setup :: IO.Handle -> IO ()
-setup h = do
- IO.hSetEncoding h IO.utf8
- IO.hSetNewlineMode h IO.noNewlineTranslation
-
-read :: IO.FilePath -> IO String
-read path =
- IO.withFile path IO.ReadMode (\h ->
- do setup h; IO.hGetContents h >>= \s -> length s `seq` return s)
-
-write :: IO.FilePath -> String -> IO ()
-write path s =
- IO.withFile path IO.WriteMode (\h -> do setup h; IO.hPutStr h s)
-
-append :: IO.FilePath -> String -> IO ()
-append path s =
- IO.withFile path IO.AppendMode (\h -> do setup h; IO.hPutStr h s)
--- a/src/Tools/Haskell/Haskell.thy Fri Nov 30 23:30:42 2018 +0100
+++ b/src/Tools/Haskell/Haskell.thy Fri Nov 30 23:43:10 2018 +0100
@@ -6,28 +6,9 @@
theory Haskell
imports Pure
- keywords "generate_haskell_file" "export_haskell_file" :: thy_decl
begin
-ML_file "haskell.ML"
-
-
-section \<open>Commands\<close>
-
-ML \<open>
- Outer_Syntax.command \<^command_keyword>\<open>generate_haskell_file\<close> "generate Haskell file"
- (Parse.position Parse.path -- (\<^keyword>\<open>=\<close> |-- Parse.input Parse.embedded)
- >> Haskell.generate_file_cmd);
-
- Outer_Syntax.command \<^command_keyword>\<open>export_haskell_file\<close> "export Haskell file"
- (Parse.name -- (\<^keyword>\<open>=\<close> |-- Parse.input Parse.embedded)
- >> Haskell.export_file_cmd);
-\<close>
-
-
-section \<open>Source modules\<close>
-
-generate_haskell_file "Library.hs" = \<open>
+generate_file "Library.hs" = \<open>
{- Title: Tools/Haskell/Library.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
@@ -121,7 +102,7 @@
clean_name = reverse #> dropWhile (== '_') #> reverse
\<close>
-generate_haskell_file "Value.hs" = \<open>
+generate_file "Value.hs" = \<open>
{- Title: Haskell/Tools/Value.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
@@ -174,7 +155,7 @@
parse_real = Read.readMaybe
\<close>
-generate_haskell_file "Buffer.hs" = \<open>
+generate_file "Buffer.hs" = \<open>
{- Title: Tools/Haskell/Buffer.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
@@ -200,7 +181,7 @@
content (Buffer xs) = concat (reverse xs)
\<close>
-generate_haskell_file "Properties.hs" = \<open>
+generate_file "Properties.hs" = \<open>
{- Title: Tools/Haskell/Properties.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
@@ -234,7 +215,7 @@
else props
\<close>
-generate_haskell_file "Markup.hs" = \<open>
+generate_file "Markup.hs" = \<open>
{- Title: Haskell/Tools/Markup.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
@@ -604,7 +585,7 @@
no_output = ("", "")
\<close>
-generate_haskell_file "Completion.hs" = \<open>
+generate_file "Completion.hs" = \<open>
{- Title: Tools/Haskell/Completion.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
@@ -665,7 +646,7 @@
markup_report [make limit name_props make_names]
\<close>
-generate_haskell_file "File.hs" = \<open>
+generate_file "File.hs" = \<open>
{- Title: Tools/Haskell/File.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
@@ -700,7 +681,7 @@
IO.withFile path IO.AppendMode (\h -> do setup h; IO.hPutStr h s)
\<close>
-generate_haskell_file "XML.hs" = \<open>
+generate_file "XML.hs" = \<open>
{- Title: Tools/Haskell/XML.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
@@ -779,7 +760,7 @@
show_text = concatMap encode
\<close>
-generate_haskell_file "XML/Encode.hs" = \<open>
+generate_file "XML/Encode.hs" = \<open>
{- Title: Tools/Haskell/XML/Encode.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
@@ -865,7 +846,7 @@
variant fs x = [tagged (the (get_index (\f -> f x) fs))]
\<close>
-generate_haskell_file "XML/Decode.hs" = \<open>
+generate_file "XML/Decode.hs" = \<open>
{- Title: Tools/Haskell/XML/Decode.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
@@ -976,7 +957,7 @@
variant _ _ = err_body
\<close>
-generate_haskell_file "YXML.hs" = \<open>
+generate_file "YXML.hs" = \<open>
{- Title: Tools/Haskell/YXML.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
@@ -1104,7 +1085,7 @@
_ -> err "multiple results"
\<close>
-generate_haskell_file "Pretty.hs" = \<open>
+generate_file "Pretty.hs" = \<open>
{- Title: Tools/Haskell/Pretty.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
@@ -1258,7 +1239,7 @@
big_list name prts = block (fbreaks (str name : prts))
\<close>
-generate_haskell_file "Term.hs" = \<open>
+generate_file "Term.hs" = \<open>
{- Title: Tools/Haskell/Term.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
@@ -1305,7 +1286,7 @@
deriving Show
\<close>
-generate_haskell_file "Term_XML/Encode.hs" = \<open>
+generate_file "Term_XML/Encode.hs" = \<open>
{- Title: Tools/Haskell/Term_XML/Encode.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
@@ -1347,7 +1328,7 @@
\case { App a -> Just ([], pair term term a); _ -> Nothing }]
\<close>
-generate_haskell_file "Term_XML/Decode.hs" = \<open>
+generate_file "Term_XML/Decode.hs" = \<open>
{- Title: Tools/Haskell/Term_XML/Decode.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
--- a/src/Tools/Haskell/Library.hs Fri Nov 30 23:30:42 2018 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,93 +0,0 @@
-{- generated by Isabelle -}
-
-{- Title: Tools/Haskell/Library.hs
- Author: Makarius
- LICENSE: BSD 3-clause (Isabelle)
-
-Basic library of Isabelle idioms.
-
-See also "$ISABELLE_HOME/src/Pure/General/basics.ML", "$ISABELLE_HOME/src/Pure/library.ML".
--}
-
-module Isabelle.Library (
- (|>), (|->), (#>), (#->),
-
- the, the_default,
-
- fold, fold_rev, single, map_index, get_index,
-
- quote, trim_line, clean_name)
-where
-
-import Data.Maybe
-
-
-{- functions -}
-
-(|>) :: a -> (a -> b) -> b
-x |> f = f x
-
-(|->) :: (a, b) -> (a -> b -> c) -> c
-(x, y) |-> f = f x y
-
-(#>) :: (a -> b) -> (b -> c) -> a -> c
-(f #> g) x = x |> f |> g
-
-(#->) :: (a -> (c, b)) -> (c -> b -> d) -> a -> d
-(f #-> g) x = x |> f |-> g
-
-
-{- options -}
-
-the :: Maybe a -> a
-the (Just x) = x
-the Nothing = error "the Nothing"
-
-the_default :: a -> Maybe a -> a
-the_default x Nothing = x
-the_default _ (Just y) = y
-
-
-{- lists -}
-
-fold :: (a -> b -> b) -> [a] -> b -> b
-fold _ [] y = y
-fold f (x : xs) y = fold f xs (f x y)
-
-fold_rev :: (a -> b -> b) -> [a] -> b -> b
-fold_rev _ [] y = y
-fold_rev f (x : xs) y = f x (fold_rev f xs y)
-
-single :: a -> [a]
-single x = [x]
-
-map_index :: ((Int, a) -> b) -> [a] -> [b]
-map_index f = map_aux 0
- where
- map_aux _ [] = []
- map_aux i (x : xs) = f (i, x) : map_aux (i + 1) xs
-
-get_index :: (a -> Maybe b) -> [a] -> Maybe (Int, b)
-get_index f = get_aux 0
- where
- get_aux _ [] = Nothing
- get_aux i (x : xs) =
- case f x of
- Nothing -> get_aux (i + 1) xs
- Just y -> Just (i, y)
-
-
-{- strings -}
-
-quote :: String -> String
-quote s = "\"" ++ s ++ "\""
-
-trim_line :: String -> String
-trim_line line =
- case reverse line of
- '\n' : '\r' : rest -> reverse rest
- '\n' : rest -> reverse rest
- _ -> line
-
-clean_name :: String -> String
-clean_name = reverse #> dropWhile (== '_') #> reverse
--- a/src/Tools/Haskell/Markup.hs Fri Nov 30 23:30:42 2018 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,369 +0,0 @@
-{- generated by Isabelle -}
-
-{- Title: Haskell/Tools/Markup.hs
- Author: Makarius
- LICENSE: BSD 3-clause (Isabelle)
-
-Quasi-abstract markup elements.
-
-See also "$ISABELLE_HOME/src/Pure/PIDE/markup.ML".
--}
-
-module Isabelle.Markup (
- T, empty, is_empty, properties,
-
- nameN, name, xnameN, xname, kindN,
-
- bindingN, binding, entityN, entity, defN, refN,
-
- completionN, completion, no_completionN, no_completion,
-
- lineN, end_lineN, offsetN, end_offsetN, fileN, idN, positionN, position,
-
- expressionN, expression,
-
- citationN, citation,
-
- pathN, urlN, docN,
-
- markupN, consistentN, unbreakableN, indentN, widthN,
- blockN, block, breakN, break, fbreakN, fbreak, itemN, item,
-
- wordsN, words, no_wordsN, no_words,
-
- tfreeN, tfree, tvarN, tvar, freeN, free, skolemN, skolem, boundN, bound, varN, var,
- numeralN, numeral, literalN, literal, delimiterN, delimiter, inner_stringN, inner_string,
- inner_cartoucheN, inner_cartouche,
- token_rangeN, token_range,
- sortingN, sorting, typingN, typing, class_parameterN, class_parameter,
-
- antiquotedN, antiquoted, antiquoteN, antiquote,
-
- paragraphN, paragraph, text_foldN, text_fold,
-
- keyword1N, keyword1, keyword2N, keyword2, keyword3N, keyword3, quasi_keywordN, quasi_keyword,
- improperN, improper, operatorN, operator, stringN, string, alt_stringN, alt_string,
- verbatimN, verbatim, cartoucheN, cartouche, commentN, comment, comment1N, comment1,
- comment2N, comment2, comment3N, comment3,
-
- writelnN, writeln, stateN, state, informationN, information, tracingN, tracing,
- warningN, warning, legacyN, legacy, errorN, error, reportN, report, no_reportN, no_report,
-
- intensifyN, intensify,
- Output, no_output)
-where
-
-import Prelude hiding (words, error, break)
-
-import Isabelle.Library
-import qualified Isabelle.Properties as Properties
-import qualified Isabelle.Value as Value
-
-
-{- basic markup -}
-
-type T = (String, Properties.T)
-
-empty :: T
-empty = ("", [])
-
-is_empty :: T -> Bool
-is_empty ("", _) = True
-is_empty _ = False
-
-properties :: Properties.T -> T -> T
-properties more_props (elem, props) =
- (elem, fold_rev Properties.put more_props props)
-
-markup_elem name = (name, (name, []) :: T)
-markup_string name prop = (name, \s -> (name, [(prop, s)]) :: T)
-
-
-{- misc properties -}
-
-nameN :: String
-nameN = "name"
-
-name :: String -> T -> T
-name a = properties [(nameN, a)]
-
-xnameN :: String
-xnameN = "xname"
-
-xname :: String -> T -> T
-xname a = properties [(xnameN, a)]
-
-kindN :: String
-kindN = "kind"
-
-
-{- formal entities -}
-
-bindingN :: String; binding :: T
-(bindingN, binding) = markup_elem "binding"
-
-entityN :: String; entity :: String -> String -> T
-entityN = "entity"
-entity kind name =
- (entityN,
- (if null name then [] else [(nameN, name)]) ++ (if null kind then [] else [(kindN, kind)]))
-
-defN :: String
-defN = "def"
-
-refN :: String
-refN = "ref"
-
-
-{- completion -}
-
-completionN :: String; completion :: T
-(completionN, completion) = markup_elem "completion"
-
-no_completionN :: String; no_completion :: T
-(no_completionN, no_completion) = markup_elem "no_completion"
-
-
-{- position -}
-
-lineN, end_lineN :: String
-lineN = "line"
-end_lineN = "end_line"
-
-offsetN, end_offsetN :: String
-offsetN = "offset"
-end_offsetN = "end_offset"
-
-fileN, idN :: String
-fileN = "file"
-idN = "id"
-
-positionN :: String; position :: T
-(positionN, position) = markup_elem "position"
-
-
-{- expression -}
-
-expressionN :: String
-expressionN = "expression"
-
-expression :: String -> T
-expression kind = (expressionN, if kind == "" then [] else [(kindN, kind)])
-
-
-{- citation -}
-
-citationN :: String; citation :: String -> T
-(citationN, citation) = markup_string "citation" nameN
-
-
-{- external resources -}
-
-pathN :: String; path :: String -> T
-(pathN, path) = markup_string "path" nameN
-
-urlN :: String; url :: String -> T
-(urlN, url) = markup_string "url" nameN
-
-docN :: String; doc :: String -> T
-(docN, doc) = markup_string "doc" nameN
-
-
-{- pretty printing -}
-
-markupN, consistentN, unbreakableN, indentN :: String
-markupN = "markup";
-consistentN = "consistent";
-unbreakableN = "unbreakable";
-indentN = "indent";
-
-widthN :: String
-widthN = "width"
-
-blockN :: String
-blockN = "block"
-block :: Bool -> Int -> T
-block c i =
- (blockN,
- (if c then [(consistentN, Value.print_bool c)] else []) ++
- (if i /= 0 then [(indentN, Value.print_int i)] else []))
-
-breakN :: String
-breakN = "break"
-break :: Int -> Int -> T
-break w i =
- (breakN,
- (if w /= 0 then [(widthN, Value.print_int w)] else []) ++
- (if i /= 0 then [(indentN, Value.print_int i)] else []))
-
-fbreakN :: String; fbreak :: T
-(fbreakN, fbreak) = markup_elem "fbreak"
-
-itemN :: String; item :: T
-(itemN, item) = markup_elem "item"
-
-
-{- text properties -}
-
-wordsN :: String; words :: T
-(wordsN, words) = markup_elem "words"
-
-no_wordsN :: String; no_words :: T
-(no_wordsN, no_words) = markup_elem "no_words"
-
-
-{- inner syntax -}
-
-tfreeN :: String; tfree :: T
-(tfreeN, tfree) = markup_elem "tfree"
-
-tvarN :: String; tvar :: T
-(tvarN, tvar) = markup_elem "tvar"
-
-freeN :: String; free :: T
-(freeN, free) = markup_elem "free"
-
-skolemN :: String; skolem :: T
-(skolemN, skolem) = markup_elem "skolem"
-
-boundN :: String; bound :: T
-(boundN, bound) = markup_elem "bound"
-
-varN :: String; var :: T
-(varN, var) = markup_elem "var"
-
-numeralN :: String; numeral :: T
-(numeralN, numeral) = markup_elem "numeral"
-
-literalN :: String; literal :: T
-(literalN, literal) = markup_elem "literal"
-
-delimiterN :: String; delimiter :: T
-(delimiterN, delimiter) = markup_elem "delimiter"
-
-inner_stringN :: String; inner_string :: T
-(inner_stringN, inner_string) = markup_elem "inner_string"
-
-inner_cartoucheN :: String; inner_cartouche :: T
-(inner_cartoucheN, inner_cartouche) = markup_elem "inner_cartouche"
-
-
-token_rangeN :: String; token_range :: T
-(token_rangeN, token_range) = markup_elem "token_range"
-
-
-sortingN :: String; sorting :: T
-(sortingN, sorting) = markup_elem "sorting"
-
-typingN :: String; typing :: T
-(typingN, typing) = markup_elem "typing"
-
-class_parameterN :: String; class_parameter :: T
-(class_parameterN, class_parameter) = markup_elem "class_parameter"
-
-
-{- antiquotations -}
-
-antiquotedN :: String; antiquoted :: T
-(antiquotedN, antiquoted) = markup_elem "antiquoted"
-
-antiquoteN :: String; antiquote :: T
-(antiquoteN, antiquote) = markup_elem "antiquote"
-
-
-{- text structure -}
-
-paragraphN :: String; paragraph :: T
-(paragraphN, paragraph) = markup_elem "paragraph"
-
-text_foldN :: String; text_fold :: T
-(text_foldN, text_fold) = markup_elem "text_fold"
-
-
-{- outer syntax -}
-
-keyword1N :: String; keyword1 :: T
-(keyword1N, keyword1) = markup_elem "keyword1"
-
-keyword2N :: String; keyword2 :: T
-(keyword2N, keyword2) = markup_elem "keyword2"
-
-keyword3N :: String; keyword3 :: T
-(keyword3N, keyword3) = markup_elem "keyword3"
-
-quasi_keywordN :: String; quasi_keyword :: T
-(quasi_keywordN, quasi_keyword) = markup_elem "quasi_keyword"
-
-improperN :: String; improper :: T
-(improperN, improper) = markup_elem "improper"
-
-operatorN :: String; operator :: T
-(operatorN, operator) = markup_elem "operator"
-
-stringN :: String; string :: T
-(stringN, string) = markup_elem "string"
-
-alt_stringN :: String; alt_string :: T
-(alt_stringN, alt_string) = markup_elem "alt_string"
-
-verbatimN :: String; verbatim :: T
-(verbatimN, verbatim) = markup_elem "verbatim"
-
-cartoucheN :: String; cartouche :: T
-(cartoucheN, cartouche) = markup_elem "cartouche"
-
-commentN :: String; comment :: T
-(commentN, comment) = markup_elem "comment"
-
-
-{- comments -}
-
-comment1N :: String; comment1 :: T
-(comment1N, comment1) = markup_elem "comment1"
-
-comment2N :: String; comment2 :: T
-(comment2N, comment2) = markup_elem "comment2"
-
-comment3N :: String; comment3 :: T
-(comment3N, comment3) = markup_elem "comment3"
-
-
-{- messages -}
-
-writelnN :: String; writeln :: T
-(writelnN, writeln) = markup_elem "writeln"
-
-stateN :: String; state :: T
-(stateN, state) = markup_elem "state"
-
-informationN :: String; information :: T
-(informationN, information) = markup_elem "information"
-
-tracingN :: String; tracing :: T
-(tracingN, tracing) = markup_elem "tracing"
-
-warningN :: String; warning :: T
-(warningN, warning) = markup_elem "warning"
-
-legacyN :: String; legacy :: T
-(legacyN, legacy) = markup_elem "legacy"
-
-errorN :: String; error :: T
-(errorN, error) = markup_elem "error"
-
-reportN :: String; report :: T
-(reportN, report) = markup_elem "report"
-
-no_reportN :: String; no_report :: T
-(no_reportN, no_report) = markup_elem "no_report"
-
-intensifyN :: String; intensify :: T
-(intensifyN, intensify) = markup_elem "intensify"
-
-
-{- output -}
-
-type Output = (String, String)
-
-no_output :: Output
-no_output = ("", "")
--- a/src/Tools/Haskell/Pretty.hs Fri Nov 30 23:30:42 2018 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,153 +0,0 @@
-{- generated by Isabelle -}
-
-{- Title: Tools/Haskell/Pretty.hs
- Author: Makarius
- LICENSE: BSD 3-clause (Isabelle)
-
-Generic pretty printing module.
-
-See also "$ISABELLE_HOME/src/Pure/General/pretty.ML".
--}
-
-module Isabelle.Pretty (
- T, symbolic, formatted, unformatted,
-
- str, brk_indent, brk, fbrk, breaks, fbreaks, blk, block, strs, markup, mark, mark_str, marks_str,
- item, text_fold, keyword1, keyword2, text, paragraph, para, quote, cartouche, separate,
- commas, enclose, enum, list, str_list, big_list)
-where
-
-import Isabelle.Library hiding (quote)
-import qualified Data.List as List
-import qualified Isabelle.Buffer as Buffer
-import qualified Isabelle.Markup as Markup
-import qualified Isabelle.XML as XML
-import qualified Isabelle.YXML as YXML
-
-
-data T =
- Block Markup.T Bool Int [T]
- | Break Int Int
- | Str String
-
-
-{- output -}
-
-output_spaces n = replicate n ' '
-
-symbolic_text "" = []
-symbolic_text s = [XML.Text s]
-
-symbolic_markup markup body =
- if Markup.is_empty markup then body
- else [XML.Elem (markup, body)]
-
-symbolic :: T -> XML.Body
-symbolic (Block markup consistent indent prts) =
- concatMap symbolic prts
- |> symbolic_markup block_markup
- |> symbolic_markup markup
- where block_markup = if null prts then Markup.empty else Markup.block consistent indent
-symbolic (Break wd ind) = [XML.Elem (Markup.break wd ind, symbolic_text (output_spaces wd))]
-symbolic (Str s) = symbolic_text s
-
-formatted :: T -> String
-formatted = YXML.string_of_body . symbolic
-
-unformatted :: T -> String
-unformatted prt = Buffer.empty |> out prt |> Buffer.content
- where
- out (Block markup _ _ prts) =
- let (bg, en) = YXML.output_markup markup
- in Buffer.add bg #> fold out prts #> Buffer.add en
- out (Break _ wd) = Buffer.add (output_spaces wd)
- out (Str s) = Buffer.add s
-
-
-{- derived operations to create formatting expressions -}
-
-force_nat n | n < 0 = 0
-force_nat n = n
-
-str :: String -> T
-str = Str
-
-brk_indent :: Int -> Int -> T
-brk_indent wd ind = Break (force_nat wd) ind
-
-brk :: Int -> T
-brk wd = brk_indent wd 0
-
-fbrk :: T
-fbrk = str "\n"
-
-breaks, fbreaks :: [T] -> [T]
-breaks = List.intersperse (brk 1)
-fbreaks = List.intersperse fbrk
-
-blk :: (Int, [T]) -> T
-blk (indent, es) = Block Markup.empty False (force_nat indent) es
-
-block :: [T] -> T
-block prts = blk (2, prts)
-
-strs :: [String] -> T
-strs = block . breaks . map str
-
-markup :: Markup.T -> [T] -> T
-markup m = Block m False 0
-
-mark :: Markup.T -> T -> T
-mark m prt = if m == Markup.empty then prt else markup m [prt]
-
-mark_str :: (Markup.T, String) -> T
-mark_str (m, s) = mark m (str s)
-
-marks_str :: ([Markup.T], String) -> T
-marks_str (ms, s) = fold_rev mark ms (str s)
-
-item :: [T] -> T
-item = markup Markup.item
-
-text_fold :: [T] -> T
-text_fold = markup Markup.text_fold
-
-keyword1, keyword2 :: String -> T
-keyword1 name = mark_str (Markup.keyword1, name)
-keyword2 name = mark_str (Markup.keyword2, name)
-
-text :: String -> [T]
-text = breaks . map str . words
-
-paragraph :: [T] -> T
-paragraph = markup Markup.paragraph
-
-para :: String -> T
-para = paragraph . text
-
-quote :: T -> T
-quote prt = blk (1, [str "\"", prt, str "\""])
-
-cartouche :: T -> T
-cartouche prt = blk (1, [str "\92<open>", prt, str "\92<close>"])
-
-separate :: String -> [T] -> [T]
-separate sep = List.intercalate [str sep, brk 1] . map single
-
-commas :: [T] -> [T]
-commas = separate ","
-
-enclose :: String -> String -> [T] -> T
-enclose lpar rpar prts = block (str lpar : prts ++ [str rpar])
-
-enum :: String -> String -> String -> [T] -> T
-enum sep lpar rpar = enclose lpar rpar . separate sep
-
-list :: String -> String -> [T] -> T
-list = enum ","
-
-str_list :: String -> String -> [String] -> T
-str_list lpar rpar = list lpar rpar . map str
-
-big_list :: String -> [T] -> T
-big_list name prts = block (fbreaks (str name : prts))
--- a/src/Tools/Haskell/Properties.hs Fri Nov 30 23:30:42 2018 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-{- generated by Isabelle -}
-
-{- Title: Tools/Haskell/Properties.hs
- Author: Makarius
- LICENSE: BSD 3-clause (Isabelle)
-
-Property lists.
-
-See also "$ISABELLE_HOME/src/Pure/General/properties.ML".
--}
-
-module Isabelle.Properties (Entry, T, defined, get, put, remove)
-where
-
-import qualified Data.List as List
-
-
-type Entry = (String, String)
-type T = [Entry]
-
-defined :: T -> String -> Bool
-defined props name = any (\(a, _) -> a == name) props
-
-get :: T -> String -> Maybe String
-get props name = List.lookup name props
-
-put :: Entry -> T -> T
-put entry props = entry : remove (fst entry) props
-
-remove :: String -> T -> T
-remove name props =
- if defined props name then filter (\(a, _) -> a /= name) props
- else props
--- a/src/Tools/Haskell/Term.hs Fri Nov 30 23:30:42 2018 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,46 +0,0 @@
-{- generated by Isabelle -}
-
-{- Title: Tools/Haskell/Term.hs
- Author: Makarius
- LICENSE: BSD 3-clause (Isabelle)
-
-Lambda terms, types, sorts.
-
-See also "$ISABELLE_HOME/src/Pure/term.scala".
--}
-
-module Isabelle.Term (
- Indexname,
-
- Sort, dummyS,
-
- Typ(..), dummyT, Term(..))
-where
-
-type Indexname = (String, Int)
-
-
-type Sort = [String]
-
-dummyS :: Sort
-dummyS = [""]
-
-
-data Typ =
- Type (String, [Typ])
- | TFree (String, Sort)
- | TVar (Indexname, Sort)
- deriving Show
-
-dummyT :: Typ
-dummyT = Type ("dummy", [])
-
-
-data Term =
- Const (String, Typ)
- | Free (String, Typ)
- | Var (Indexname, Typ)
- | Bound Int
- | Abs (String, Typ, Term)
- | App (Term, Term)
- deriving Show
--- a/src/Tools/Haskell/Term_XML/Decode.hs Fri Nov 30 23:30:42 2018 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-{- generated by Isabelle -}
-
-{- Title: Tools/Haskell/Term_XML/Decode.hs
- Author: Makarius
- LICENSE: BSD 3-clause (Isabelle)
-
-XML data representation of lambda terms.
-
-See also "$ISABELLE_HOME/src/Pure/term_xml.ML".
--}
-
-module Isabelle.Term_XML.Decode (sort, typ, term)
-where
-
-import Isabelle.Library
-import qualified Isabelle.XML as XML
-import Isabelle.XML.Decode
-import Isabelle.Term
-
-
-sort :: T Sort
-sort = list string
-
-typ :: T Typ
-typ ty =
- ty |> variant
- [\([a], b) -> Type (a, list typ b),
- \([a], b) -> TFree (a, sort b),
- \([a, b], c) -> TVar ((a, int_atom b), sort c)]
-
-term :: T Term
-term t =
- t |> variant
- [\([a], b) -> Const (a, typ b),
- \([a], b) -> Free (a, typ b),
- \([a, b], c) -> Var ((a, int_atom b), typ c),
- \([a], []) -> Bound (int_atom a),
- \([a], b) -> let (c, d) = pair typ term b in Abs (a, c, d),
- \([], a) -> App (pair term term a)]
--- a/src/Tools/Haskell/Term_XML/Encode.hs Fri Nov 30 23:30:42 2018 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +0,0 @@
-{- generated by Isabelle -}
-
-{- Title: Tools/Haskell/Term_XML/Encode.hs
- Author: Makarius
- LICENSE: BSD 3-clause (Isabelle)
-
-XML data representation of lambda terms.
-
-See also "$ISABELLE_HOME/src/Pure/term_xml.ML".
--}
-
-{-# LANGUAGE LambdaCase #-}
-
-module Isabelle.Term_XML.Encode (sort, typ, term)
-where
-
-import Isabelle.Library
-import qualified Isabelle.XML as XML
-import Isabelle.XML.Encode
-import Isabelle.Term
-
-
-sort :: T Sort
-sort = list string
-
-typ :: T Typ
-typ ty =
- ty |> variant
- [\case { Type (a, b) -> Just ([a], list typ b); _ -> Nothing },
- \case { TFree (a, b) -> Just ([a], sort b); _ -> Nothing },
- \case { TVar ((a, b), c) -> Just ([a, int_atom b], sort c); _ -> Nothing }]
-
-term :: T Term
-term t =
- t |> variant
- [\case { Const (a, b) -> Just ([a], typ b); _ -> Nothing },
- \case { Free (a, b) -> Just ([a], typ b); _ -> Nothing },
- \case { Var ((a, b), c) -> Just ([a, int_atom b], typ c); _ -> Nothing },
- \case { Bound a -> Just ([int_atom a], []); _ -> Nothing },
- \case { Abs (a, b, c) -> Just ([a], pair typ term (b, c)); _ -> Nothing },
- \case { App a -> Just ([], pair term term a); _ -> Nothing }]
--- a/src/Tools/Haskell/Test.thy Fri Nov 30 23:30:42 2018 +0100
+++ b/src/Tools/Haskell/Test.thy Fri Nov 30 23:43:10 2018 +0100
@@ -10,13 +10,13 @@
ML \<open>
Isabelle_System.with_tmp_dir "ghc" (fn dir =>
let
- val _ = Haskell.install_sources dir;
+ val files = Generate_File.generate \<^theory>\<open>Haskell\<close> dir;
val (out, rc) =
Isabelle_System.bash_output
(cat_lines
["set -e",
"cd " ^ File.bash_path dir,
- "\"$ISABELLE_GHC\" " ^ File.bash_paths Haskell.sources]);
+ "\"$ISABELLE_GHC\" " ^ File.bash_paths files]);
in if rc = 0 then writeln out else error out end)
\<close>
--- a/src/Tools/Haskell/Value.hs Fri Nov 30 23:30:42 2018 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,52 +0,0 @@
-{- generated by Isabelle -}
-
-{- Title: Haskell/Tools/Value.hs
- Author: Makarius
- LICENSE: BSD 3-clause (Isabelle)
-
-Plain values, represented as string.
-
-See also "$ISABELLE_HOME/src/Pure/General/value.ML".
--}
-
-module Isabelle.Value
- (print_bool, parse_bool, print_int, parse_int, print_real, parse_real)
-where
-
-import Data.Maybe
-import qualified Data.List as List
-import qualified Text.Read as Read
-
-
-{- bool -}
-
-print_bool :: Bool -> String
-print_bool True = "true"
-print_bool False = "false"
-
-parse_bool :: String -> Maybe Bool
-parse_bool "true" = Just True
-parse_bool "false" = Just False
-parse_bool _ = Nothing
-
-
-{- int -}
-
-print_int :: Int -> String
-print_int = show
-
-parse_int :: String -> Maybe Int
-parse_int = Read.readMaybe
-
-
-{- real -}
-
-print_real :: Double -> String
-print_real x =
- let s = show x in
- case span (/= '.') s of
- (a, '.' : b) | List.all (== '0') b -> a
- _ -> s
-
-parse_real :: String -> Maybe Double
-parse_real = Read.readMaybe
--- a/src/Tools/Haskell/XML.hs Fri Nov 30 23:30:42 2018 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,78 +0,0 @@
-{- generated by Isabelle -}
-
-{- Title: Tools/Haskell/XML.hs
- Author: Makarius
- LICENSE: BSD 3-clause (Isabelle)
-
-Untyped XML trees and representation of ML values.
-
-See also "$ISABELLE_HOME/src/Pure/PIDE/xml.ML".
--}
-
-module Isabelle.XML (Attributes, Body, Tree(..), wrap_elem, unwrap_elem, content_of)
-where
-
-import qualified Data.List as List
-
-import Isabelle.Library
-import qualified Isabelle.Properties as Properties
-import qualified Isabelle.Markup as Markup
-import qualified Isabelle.Buffer as Buffer
-
-
-{- types -}
-
-type Attributes = Properties.T
-type Body = [Tree]
-data Tree = Elem (Markup.T, Body) | Text String
-
-
-{- wrapped elements -}
-
-wrap_elem (((a, atts), body1), body2) =
- Elem (("xml_elem", ("xml_name", a) : atts), Elem (("xml_body", []), body1) : body2)
-
-unwrap_elem
- (Elem (("xml_elem", ("xml_name", a) : atts), Elem (("xml_body", []), body1) : body2)) =
- Just (((a, atts), body1), body2)
-unwrap_elem _ = Nothing
-
-
-{- text content -}
-
-add_content tree =
- case unwrap_elem tree of
- Just (_, ts) -> fold add_content ts
- Nothing ->
- case tree of
- Elem (_, ts) -> fold add_content ts
- Text s -> Buffer.add s
-
-content_of body = Buffer.empty |> fold add_content body |> Buffer.content
-
-
-{- string representation -}
-
-encode '<' = "<"
-encode '>' = ">"
-encode '&' = "&"
-encode '\'' = "'"
-encode '\"' = """
-encode c = [c]
-
-instance Show Tree where
- show tree =
- Buffer.empty |> show_tree tree |> Buffer.content
- where
- show_tree (Elem ((name, atts), [])) =
- Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add "/>"
- show_tree (Elem ((name, atts), ts)) =
- Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add ">" #>
- fold show_tree ts #>
- Buffer.add "</" #> Buffer.add name #> Buffer.add ">"
- show_tree (Text s) = Buffer.add (show_text s)
-
- show_elem name atts =
- unwords (name : map (\(a, x) -> a ++ "=\"" ++ show_text x ++ "\"") atts)
-
- show_text = concatMap encode
--- a/src/Tools/Haskell/XML/Decode.hs Fri Nov 30 23:30:42 2018 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,110 +0,0 @@
-{- generated by Isabelle -}
-
-{- Title: Tools/Haskell/XML/Decode.hs
- Author: Makarius
- LICENSE: BSD 3-clause (Isabelle)
-
-XML as data representation language.
-
-See also "$ISABELLE_HOME/src/Pure/PIDE/xml.ML".
--}
-
-module Isabelle.XML.Decode (
- A, T, V,
-
- int_atom, bool_atom, unit_atom,
-
- tree, properties, string, init, bool, unit, pair, triple, list, variant
-)
-where
-
-import Data.List ((!!))
-
-import Isabelle.Library
-import qualified Isabelle.Value as Value
-import qualified Isabelle.Properties as Properties
-import qualified Isabelle.XML as XML
-
-
-type A a = String -> a
-type T a = XML.Body -> a
-type V a = ([String], XML.Body) -> a
-
-err_atom = error "Malformed XML atom"
-err_body = error "Malformed XML body"
-
-
-{- atomic values -}
-
-int_atom :: A Int
-int_atom s =
- case Value.parse_int s of
- Just i -> i
- Nothing -> err_atom
-
-bool_atom :: A Bool
-bool_atom "0" = False
-bool_atom "1" = True
-bool_atom _ = err_atom
-
-unit_atom :: A ()
-unit_atom "" = ()
-unit_atom _ = err_atom
-
-
-{- structural nodes -}
-
-node (XML.Elem ((":", []), ts)) = ts
-node _ = err_body
-
-vector atts =
- map_index (\(i, (a, x)) -> if int_atom a == i then x else err_atom) atts
-
-tagged (XML.Elem ((name, atts), ts)) = (int_atom name, (vector atts, ts))
-tagged _ = err_body
-
-
-{- representation of standard types -}
-
-tree :: T XML.Tree
-tree [t] = t
-tree _ = err_body
-
-properties :: T Properties.T
-properties [XML.Elem ((":", props), [])] = props
-properties _ = err_body
-
-string :: T String
-string [] = ""
-string [XML.Text s] = s
-string _ = err_body
-
-int :: T Int
-int = int_atom . string
-
-bool :: T Bool
-bool = bool_atom . string
-
-unit :: T ()
-unit = unit_atom . string
-
-pair :: T a -> T b -> T (a, b)
-pair f g [t1, t2] = (f (node t1), g (node t2))
-pair _ _ _ = err_body
-
-triple :: T a -> T b -> T c -> T (a, b, c)
-triple f g h [t1, t2, t3] = (f (node t1), g (node t2), h (node t3))
-triple _ _ _ _ = err_body
-
-list :: T a -> T [a]
-list f ts = map (f . node) ts
-
-option :: T a -> T (Maybe a)
-option _ [] = Nothing
-option f [t] = Just (f (node t))
-option _ _ = err_body
-
-variant :: [V a] -> T a
-variant fs [t] = (fs !! tag) (xs, ts)
- where (tag, (xs, ts)) = tagged t
-variant _ _ = err_body
--- a/src/Tools/Haskell/XML/Encode.hs Fri Nov 30 23:30:42 2018 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,85 +0,0 @@
-{- generated by Isabelle -}
-
-{- Title: Tools/Haskell/XML/Encode.hs
- Author: Makarius
- LICENSE: BSD 3-clause (Isabelle)
-
-XML as data representation language.
-
-See also "$ISABELLE_HOME/src/Pure/PIDE/xml.ML".
--}
-
-module Isabelle.XML.Encode (
- A, T, V,
-
- int_atom, bool_atom, unit_atom,
-
- tree, properties, string, int, bool, unit, pair, triple, list, variant
-)
-where
-
-import Isabelle.Library
-import qualified Isabelle.Value as Value
-import qualified Isabelle.Properties as Properties
-import qualified Isabelle.XML as XML
-
-
-type A a = a -> String
-type T a = a -> XML.Body
-type V a = a -> Maybe ([String], XML.Body)
-
-
--- atomic values
-
-int_atom :: A Int
-int_atom = Value.print_int
-
-bool_atom :: A Bool
-bool_atom False = "0"
-bool_atom True = "1"
-
-unit_atom :: A ()
-unit_atom () = ""
-
-
--- structural nodes
-
-node ts = XML.Elem ((":", []), ts)
-
-vector = map_index (\(i, x) -> (int_atom i, x))
-
-tagged (tag, (xs, ts)) = XML.Elem ((int_atom tag, vector xs), ts)
-
-
--- representation of standard types
-
-tree :: T XML.Tree
-tree t = [t]
-
-properties :: T Properties.T
-properties props = [XML.Elem ((":", props), [])]
-
-string :: T String
-string "" = []
-string s = [XML.Text s]
-
-int :: T Int
-int = string . int_atom
-
-bool :: T Bool
-bool = string . bool_atom
-
-unit :: T ()
-unit = string . unit_atom
-
-pair :: T a -> T b -> T (a, b)
-pair f g (x, y) = [node (f x), node (g y)]
-
-triple :: T a -> T b -> T c -> T (a, b, c)
-triple f g h (x, y, z) = [node (f x), node (g y), node (h z)]
-
-list :: T a -> T [a]
-list f xs = map (node . f) xs
-
-variant :: [V a] -> T a
-variant fs x = [tagged (the (get_index (\f -> f x) fs))]
--- a/src/Tools/Haskell/YXML.hs Fri Nov 30 23:30:42 2018 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,127 +0,0 @@
-{- generated by Isabelle -}
-
-{- Title: Tools/Haskell/YXML.hs
- Author: Makarius
- LICENSE: BSD 3-clause (Isabelle)
-
-Efficient text representation of XML trees. Suitable for direct
-inlining into plain text.
-
-See also "$ISABELLE_HOME/src/Pure/PIDE/yxml.ML".
--}
-
-module Isabelle.YXML (charX, charY, strX, strY, detect, output_markup,
- buffer_body, buffer, string_of_body, string_of, parse_body, parse)
-where
-
-import qualified Data.Char as Char
-import qualified Data.List as List
-
-import Isabelle.Library
-import qualified Isabelle.Markup as Markup
-import qualified Isabelle.XML as XML
-import qualified Isabelle.Buffer as Buffer
-
-
-{- markers -}
-
-charX, charY :: Char
-charX = Char.chr 5
-charY = Char.chr 6
-
-strX, strY, strXY, strXYX :: String
-strX = [charX]
-strY = [charY]
-strXY = strX ++ strY
-strXYX = strXY ++ strX
-
-detect :: String -> Bool
-detect = any (\c -> c == charX || c == charY)
-
-
-{- output -}
-
-output_markup :: Markup.T -> Markup.Output
-output_markup markup@(name, atts) =
- if Markup.is_empty markup then Markup.no_output
- else (strXY ++ name ++ concatMap (\(a, x) -> strY ++ a ++ "=" ++ x) atts ++ strX, strXYX)
-
-buffer_attrib (a, x) =
- Buffer.add strY #> Buffer.add a #> Buffer.add "=" #> Buffer.add x
-
-buffer_body :: XML.Body -> Buffer.T -> Buffer.T
-buffer_body = fold buffer
-
-buffer :: XML.Tree -> Buffer.T -> Buffer.T
-buffer (XML.Elem ((name, atts), ts)) =
- Buffer.add strXY #> Buffer.add name #> fold buffer_attrib atts #> Buffer.add strX #>
- buffer_body ts #>
- Buffer.add strXYX
-buffer (XML.Text s) = Buffer.add s
-
-string_of_body :: XML.Body -> String
-string_of_body body = Buffer.empty |> buffer_body body |> Buffer.content
-
-string_of :: XML.Tree -> String
-string_of = string_of_body . single
-
-
-{- parse -}
-
--- split: fields or non-empty tokens
-
-split :: Bool -> Char -> String -> [String]
-split _ _ [] = []
-split fields sep str = splitting str
- where
- splitting rest =
- case span (/= sep) rest of
- (_, []) -> cons rest []
- (prfx, _ : rest') -> cons prfx (splitting rest')
- cons item = if fields || not (null item) then (:) item else id
-
-
--- structural errors
-
-err msg = error ("Malformed YXML: " ++ msg)
-err_attribute = err "bad attribute"
-err_element = err "bad element"
-err_unbalanced "" = err "unbalanced element"
-err_unbalanced name = err ("unbalanced element " ++ quote name)
-
-
--- stack operations
-
-add x ((elem, body) : pending) = (elem, x : body) : pending
-
-push "" _ _ = err_element
-push name atts pending = ((name, atts), []) : pending
-
-pop ((("", _), _) : _) = err_unbalanced ""
-pop ((markup, body) : pending) = add (XML.Elem (markup, reverse body)) pending
-
-
--- parsing
-
-parse_attrib s =
- case List.elemIndex '=' s of
- Just i | i > 0 -> (take i s, drop (i + 1) s)
- _ -> err_attribute
-
-parse_chunk ["", ""] = pop
-parse_chunk ("" : name : atts) = push name (map parse_attrib atts)
-parse_chunk txts = fold (add . XML.Text) txts
-
-parse_body :: String -> XML.Body
-parse_body source =
- case fold parse_chunk chunks [(("", []), [])] of
- [(("", _), result)] -> reverse result
- ((name, _), _) : _ -> err_unbalanced name
- where chunks = split False charX source |> map (split True charY)
-
-parse :: String -> XML.Tree
-parse source =
- case parse_body source of
- [result] -> result
- [] -> XML.Text ""
- _ -> err "multiple results"
--- a/src/Tools/Haskell/haskell.ML Fri Nov 30 23:30:42 2018 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,69 +0,0 @@
-(* Title: Tools/Haskell/haskell.ml
- Author: Makarius
-
-Support for Isabelle tools in Haskell.
-*)
-
-signature HASKELL =
-sig
- val generate_file_cmd: (string * Position.T) * Input.source ->
- Toplevel.transition -> Toplevel.transition
- val export_file_cmd: string * Input.source ->
- Toplevel.transition -> Toplevel.transition
- val sources: Path.T list
- val install_sources: Path.T -> unit
-end;
-
-structure Haskell: HASKELL =
-struct
-
-(* commands *)
-
-val header = "{- generated by Isabelle -}\n";
-
-fun generate_file_cmd (file, source) =
- Toplevel.keep (fn state =>
- let
- val ctxt = Toplevel.context_of state;
- val thy = Toplevel.theory_of state;
-
- val path = Resources.check_path ctxt (Resources.master_directory thy) file;
- val text = header ^ GHC.read_source ctxt source;
- val _ = Isabelle_System.mkdirs (Path.dir (Path.expand path));
- val _ = File.generate path text;
- in () end);
-
-fun export_file_cmd (name, source) =
- Toplevel.keep (fn state =>
- let
- val ctxt = Toplevel.context_of state;
- val thy = Toplevel.theory_of state;
-
- val text = header ^ GHC.read_source ctxt source;
- val _ = Export.export thy name [text];
- in () end);
-
-
-(* sources *)
-
-val sources =
- [\<^path>\<open>Library.hs\<close>,
- \<^path>\<open>Value.hs\<close>,
- \<^path>\<open>Buffer.hs\<close>,
- \<^path>\<open>Properties.hs\<close>,
- \<^path>\<open>Markup.hs\<close>,
- \<^path>\<open>Completion.hs\<close>,
- \<^path>\<open>File.hs\<close>,
- \<^path>\<open>XML.hs\<close>,
- \<^path>\<open>XML/Encode.hs\<close>,
- \<^path>\<open>XML/Decode.hs\<close>,
- \<^path>\<open>YXML.hs\<close>,
- \<^path>\<open>Pretty.hs\<close>,
- \<^path>\<open>Term.hs\<close>,
- \<^path>\<open>Term_XML/Encode.hs\<close>,
- \<^path>\<open>Term_XML/Decode.hs\<close>];
-
-fun install_sources dir =
- sources |> List.app (fn path => Isabelle_System.copy_file_base (\<^master_dir>, path) dir);
-
-end;