support for Isabelle tool development in Haskell;
authorwenzelm
Thu Nov 01 13:53:29 2018 +0100 (7 months ago)
changeset 692228365124a86ae
parent 69219 d4cec24a1d87
child 69223 44d68a00917c
support for Isabelle tool development in Haskell;
src/Tools/Haskell/Haskell.thy
src/Tools/ROOT
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/Haskell/Haskell.thy	Thu Nov 01 13:53:29 2018 +0100
     1.3 @@ -0,0 +1,42 @@
     1.4 +(*  Title:      Tools/Haskell/Haskell.thy
     1.5 +    Author:     Makarius
     1.6 +*)
     1.7 +
     1.8 +section \<open>Support for Isabelle tool development in Haskell\<close>
     1.9 +
    1.10 +theory Haskell
    1.11 +  imports Pure
    1.12 +  keywords "generate_haskell_file" "export_haskell_file" :: thy_decl
    1.13 +begin
    1.14 +
    1.15 +ML \<open>
    1.16 +  Outer_Syntax.command \<^command_keyword>\<open>generate_haskell_file\<close> "generate Haskell file"
    1.17 +    (Parse.position Parse.path -- (\<^keyword>\<open>=\<close> |-- Parse.input Parse.embedded) >>
    1.18 +      (fn (file, source) =>
    1.19 +        Toplevel.keep (fn state =>
    1.20 +          let
    1.21 +            val ctxt = Toplevel.context_of state;
    1.22 +            val thy = Toplevel.theory_of state;
    1.23 +
    1.24 +            val path = Resources.check_path ctxt (Resources.master_directory thy) file;
    1.25 +            val text = GHC.read_source ctxt source;
    1.26 +            val _ = Isabelle_System.mkdirs (Path.dir (Path.expand path));
    1.27 +            val _ = if try File.read path = SOME text then () else File.write path text;
    1.28 +          in () end)));
    1.29 +\<close>
    1.30 +
    1.31 +ML \<open>
    1.32 +  Outer_Syntax.command \<^command_keyword>\<open>export_haskell_file\<close> "export Haskell file"
    1.33 +    (Parse.name -- (\<^keyword>\<open>=\<close> |-- Parse.input Parse.embedded) >>
    1.34 +      (fn (name, source) =>
    1.35 +        Toplevel.keep (fn state =>
    1.36 +          let
    1.37 +            val ctxt = Toplevel.context_of state;
    1.38 +            val thy = Toplevel.theory_of state;
    1.39 +
    1.40 +            val text = GHC.read_source ctxt source;
    1.41 +            val _ = Export.export thy name [text];
    1.42 +          in () end)));
    1.43 +\<close>
    1.44 +
    1.45 +end
     2.1 --- a/src/Tools/ROOT	Thu Nov 01 12:23:54 2018 +0100
     2.2 +++ b/src/Tools/ROOT	Thu Nov 01 13:53:29 2018 +0100
     2.3 @@ -8,3 +8,7 @@
     2.4  session SML in SML = Pure +
     2.5    theories
     2.6      Examples
     2.7 +
     2.8 +session Haskell in Haskell = Pure +
     2.9 +  theories
    2.10 +    Haskell