A Collection of Isabelle Programming Hacks
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
 
 
 

80 lines
3.1 KiB

  1. (***********************************************************************************
  2. * Copyright (c) Achim D. Brucker
  3. *
  4. * All rights reserved.
  5. *
  6. * Redistribution and use in source and binary forms, with or without
  7. * modification, are permitted provided that the following conditions are met:
  8. *
  9. * * Redistributions of source code must retain the above copyright notice, this
  10. *
  11. * * Redistributions in binary form must reproduce the above copyright notice,
  12. * this list of conditions and the following disclaimer in the documentation
  13. * and/or other materials provided with the distribution.
  14. *
  15. * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
  16. * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
  17. * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
  18. * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
  19. * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
  20. * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
  21. * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  22. * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
  23. * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
  24. * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
  25. *
  26. * SPDX-License-Identifier: BSD-2-Clause
  27. * Repository: https://git.logicalhacking.com/adbrucker/isabelle-hacks/
  28. * Dependencies: None
  29. ***********************************************************************************)
  30. chapter\<open>Code Reflection for \<close>
  31. theory
  32. "Code_Reflection"
  33. imports
  34. Main
  35. keywords
  36. "reflect_ML_exports" :: thy_decl
  37. begin
  38. subsection\<open>Reflecting exported SML code\<close>
  39. ML\<open>
  40. fun reflect_local_ML_exports args trans = let
  41. fun eval_ML_context ctxt = let
  42. fun is_sml_file f = String.isSuffix ".ML" (Path.implode (#path f))
  43. val files = (map (Generated_Files.check_files_in (Context.proof_of ctxt)) args)
  44. val ml_files = filter is_sml_file (map #1 (maps Generated_Files.get_files_in files))
  45. val ml_content = map (fn f => Syntax.read_input (#content f)) ml_files
  46. fun eval ml_content = fold (fn sml => (ML_Context.exec
  47. (fn () => ML_Context.eval_source ML_Compiler.flags sml)))
  48. ml_content
  49. in
  50. (eval ml_content #> Local_Theory.propagate_ml_env) ctxt
  51. end
  52. in
  53. Toplevel.generic_theory eval_ML_context trans
  54. end
  55. val files_in_theory =
  56. (Parse.underscore >> K [] || Scan.repeat1 Parse.path_binding) --
  57. Scan.option (\<^keyword>\<open>(\<close> |-- Parse.!!! (\<^keyword>\<open>in\<close>
  58. |-- Parse.theory_name --| \<^keyword>\<open>)\<close>));
  59. val _ =
  60. Outer_Syntax.command \<^command_keyword>\<open>reflect_ML_exports\<close>
  61. "evaluate generated Standard ML files"
  62. (Parse.and_list1 files_in_theory >> (fn args => reflect_local_ML_exports args));
  63. \<close>
  64. export_code Suc in SML module_name Natural
  65. reflect_ML_exports _
  66. ML\<open>
  67. open Natural
  68. \<close>
  69. end