# HG changeset patch # User wenzelm # Date 1543617790 -3600 # Node ID 4c9b4e2c54600d9c5153c91003c3f0b92c952324 # Parent 87644f76c9977131a7ecd2dc6a8fd3be74eee8be 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; diff -r 87644f76c997 -r 4c9b4e2c5460 NEWS --- 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 \ - GHC.read_source \<^context> \ +* 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" = \ + module Isabelle.Pure where allConst, impConst, eqConst :: String allConst = \\<^const_name>\Pure.all\\ impConst = \\<^const_name>\Pure.imp\\ eqConst = \\<^const_name>\Pure.eq\\ \ - |> writeln -\ - -* 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 *** diff -r 87644f76c997 -r 4c9b4e2c5460 src/Pure/General/path.ML --- 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 diff -r 87644f76c997 -r 4c9b4e2c5460 src/Pure/PIDE/markup.ML --- 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"; diff -r 87644f76c997 -r 4c9b4e2c5460 src/Pure/Pure.thy --- 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>\generate_file\ + "generate source file, with antiquotations" + (Parse.position Parse.path -- (\<^keyword>\=\ |-- Parse.input Parse.embedded) + >> Generate_File.generate_file_cmd); + in end\ diff -r 87644f76c997 -r 4c9b4e2c5460 src/Pure/ROOT.ML --- 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" diff -r 87644f76c997 -r 4c9b4e2c5460 src/Pure/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>\Haskell\ + {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>\cartouche\ (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>\path\ Resources.check_path #> + path_antiquotation \<^binding>\file\ Resources.check_file #> + path_antiquotation \<^binding>\dir\ Resources.check_dir); + +end; diff -r 87644f76c997 -r 4c9b4e2c5460 src/Pure/Tools/ghc.ML --- 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>\cartouche\ (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>\path\ (path_antiq Resources.check_path) #argument #> - antiquotation \<^binding>\file\ (path_antiq Resources.check_file) #argument #> - antiquotation \<^binding>\dir\ (path_antiq Resources.check_dir) #argument); - end; diff -r 87644f76c997 -r 4c9b4e2c5460 src/Tools/Haskell/Buffer.hs --- 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) diff -r 87644f76c997 -r 4c9b4e2c5460 src/Tools/Haskell/Completion.hs --- 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] diff -r 87644f76c997 -r 4c9b4e2c5460 src/Tools/Haskell/File.hs --- 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) diff -r 87644f76c997 -r 4c9b4e2c5460 src/Tools/Haskell/Haskell.thy --- 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 \Commands\ - -ML \ - Outer_Syntax.command \<^command_keyword>\generate_haskell_file\ "generate Haskell file" - (Parse.position Parse.path -- (\<^keyword>\=\ |-- Parse.input Parse.embedded) - >> Haskell.generate_file_cmd); - - Outer_Syntax.command \<^command_keyword>\export_haskell_file\ "export Haskell file" - (Parse.name -- (\<^keyword>\=\ |-- Parse.input Parse.embedded) - >> Haskell.export_file_cmd); -\ - - -section \Source modules\ - -generate_haskell_file "Library.hs" = \ +generate_file "Library.hs" = \ {- Title: Tools/Haskell/Library.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) @@ -121,7 +102,7 @@ clean_name = reverse #> dropWhile (== '_') #> reverse \ -generate_haskell_file "Value.hs" = \ +generate_file "Value.hs" = \ {- Title: Haskell/Tools/Value.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) @@ -174,7 +155,7 @@ parse_real = Read.readMaybe \ -generate_haskell_file "Buffer.hs" = \ +generate_file "Buffer.hs" = \ {- Title: Tools/Haskell/Buffer.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) @@ -200,7 +181,7 @@ content (Buffer xs) = concat (reverse xs) \ -generate_haskell_file "Properties.hs" = \ +generate_file "Properties.hs" = \ {- Title: Tools/Haskell/Properties.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) @@ -234,7 +215,7 @@ else props \ -generate_haskell_file "Markup.hs" = \ +generate_file "Markup.hs" = \ {- Title: Haskell/Tools/Markup.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) @@ -604,7 +585,7 @@ no_output = ("", "") \ -generate_haskell_file "Completion.hs" = \ +generate_file "Completion.hs" = \ {- Title: Tools/Haskell/Completion.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) @@ -665,7 +646,7 @@ markup_report [make limit name_props make_names] \ -generate_haskell_file "File.hs" = \ +generate_file "File.hs" = \ {- 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) \ -generate_haskell_file "XML.hs" = \ +generate_file "XML.hs" = \ {- Title: Tools/Haskell/XML.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) @@ -779,7 +760,7 @@ show_text = concatMap encode \ -generate_haskell_file "XML/Encode.hs" = \ +generate_file "XML/Encode.hs" = \ {- 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))] \ -generate_haskell_file "XML/Decode.hs" = \ +generate_file "XML/Decode.hs" = \ {- Title: Tools/Haskell/XML/Decode.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) @@ -976,7 +957,7 @@ variant _ _ = err_body \ -generate_haskell_file "YXML.hs" = \ +generate_file "YXML.hs" = \ {- Title: Tools/Haskell/YXML.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) @@ -1104,7 +1085,7 @@ _ -> err "multiple results" \ -generate_haskell_file "Pretty.hs" = \ +generate_file "Pretty.hs" = \ {- 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)) \ -generate_haskell_file "Term.hs" = \ +generate_file "Term.hs" = \ {- Title: Tools/Haskell/Term.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) @@ -1305,7 +1286,7 @@ deriving Show \ -generate_haskell_file "Term_XML/Encode.hs" = \ +generate_file "Term_XML/Encode.hs" = \ {- 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 }] \ -generate_haskell_file "Term_XML/Decode.hs" = \ +generate_file "Term_XML/Decode.hs" = \ {- Title: Tools/Haskell/Term_XML/Decode.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) diff -r 87644f76c997 -r 4c9b4e2c5460 src/Tools/Haskell/Library.hs --- 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 diff -r 87644f76c997 -r 4c9b4e2c5460 src/Tools/Haskell/Markup.hs --- 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 = ("", "") diff -r 87644f76c997 -r 4c9b4e2c5460 src/Tools/Haskell/Pretty.hs --- 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", prt, str "\92"]) - -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)) diff -r 87644f76c997 -r 4c9b4e2c5460 src/Tools/Haskell/Properties.hs --- 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 diff -r 87644f76c997 -r 4c9b4e2c5460 src/Tools/Haskell/Term.hs --- 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 diff -r 87644f76c997 -r 4c9b4e2c5460 src/Tools/Haskell/Term_XML/Decode.hs --- 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)] diff -r 87644f76c997 -r 4c9b4e2c5460 src/Tools/Haskell/Term_XML/Encode.hs --- 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 }] diff -r 87644f76c997 -r 4c9b4e2c5460 src/Tools/Haskell/Test.thy --- 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 \ Isabelle_System.with_tmp_dir "ghc" (fn dir => let - val _ = Haskell.install_sources dir; + val files = Generate_File.generate \<^theory>\Haskell\ 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) \ diff -r 87644f76c997 -r 4c9b4e2c5460 src/Tools/Haskell/Value.hs --- 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 diff -r 87644f76c997 -r 4c9b4e2c5460 src/Tools/Haskell/XML.hs --- 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 diff -r 87644f76c997 -r 4c9b4e2c5460 src/Tools/Haskell/XML/Decode.hs --- 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 diff -r 87644f76c997 -r 4c9b4e2c5460 src/Tools/Haskell/XML/Encode.hs --- 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))] diff -r 87644f76c997 -r 4c9b4e2c5460 src/Tools/Haskell/YXML.hs --- 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" diff -r 87644f76c997 -r 4c9b4e2c5460 src/Tools/Haskell/haskell.ML --- 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>\Library.hs\, - \<^path>\Value.hs\, - \<^path>\Buffer.hs\, - \<^path>\Properties.hs\, - \<^path>\Markup.hs\, - \<^path>\Completion.hs\, - \<^path>\File.hs\, - \<^path>\XML.hs\, - \<^path>\XML/Encode.hs\, - \<^path>\XML/Decode.hs\, - \<^path>\YXML.hs\, - \<^path>\Pretty.hs\, - \<^path>\Term.hs\, - \<^path>\Term_XML/Encode.hs\, - \<^path>\Term_XML/Decode.hs\]; - -fun install_sources dir = - sources |> List.app (fn path => Isabelle_System.copy_file_base (\<^master_dir>, path) dir); - -end;