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.
 
 
 

266 lines
9.8 KiB

  1. (***********************************************************************************
  2. * Copyright (c) 2018-2019 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. (***********************************************************************************
  31. # Changelog
  32. This comment documents all notable changes to this file in a format inspired by
  33. [Keep a Changelog](https://keepachangelog.com/en/1.0.0/), and this project adheres
  34. to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
  35. ## [Unreleased]
  36. ## [1.0.0] - 2018-06-16
  37. - Initial release
  38. ***********************************************************************************)
  39. chapter\<open>An Assertion Framework for Isabelle\<close>
  40. theory
  41. "Assert"
  42. imports
  43. Main
  44. keywords
  45. "assert"::thy_decl
  46. begin
  47. text\<open>This theory implements a simple @{emph \<open>assertion framework\<close>} for Isabelle:
  48. it introduces a new top level command @{bold \<open>assert\<close>} that allows for
  49. checking an assertion. The overall idea is very similar to the assert
  50. annotations that man unit test frameworks provide. New assertion
  51. types can be registered on the ML level of Isabelle.\<close>
  52. section\<open>The Core Assertion Framework\<close>
  53. ML\<open>
  54. signature ASSERT = sig
  55. datatype arg_class = optional | mandatory
  56. type arg_parseT = ((string * Position.T) * string)
  57. type arg_specT = (string * arg_class * string option)
  58. type checkT = theory -> arg_parseT list -> unit
  59. type assertionT = {
  60. name : string,
  61. description: string,
  62. assertion: checkT
  63. }
  64. val dispatch : string -> arg_parseT list -> theory -> theory
  65. val register : assertionT-> theory -> theory
  66. end
  67. structure Assert : ASSERT = struct
  68. datatype arg_class = optional | mandatory
  69. type arg_parseT = ((string * Position.T) * string)
  70. type arg_specT = (string * arg_class * string option)
  71. type checkT = theory -> arg_parseT list -> unit
  72. type assertionT = {
  73. name : string,
  74. description: string,
  75. assertion: checkT
  76. }
  77. type assert_tab = (assertionT) Symtab.table
  78. fun assertion_eq (a, a') = (#name a) = (#name a')
  79. fun merge_assert_tab (tab,tab') = Symtab.merge assertion_eq (tab,tab')
  80. structure Data = Generic_Data
  81. (
  82. type T = assert_tab
  83. val empty = Symtab.empty:assert_tab
  84. val extend = I
  85. fun merge(t1,t2) = merge_assert_tab (t1, t2)
  86. );
  87. fun register assertion thy =
  88. let
  89. val name = #name assertion
  90. fun reg tab = Symtab.update_new(name, assertion) tab
  91. in
  92. Context.theory_of ( (Data.map reg) (Context.Theory thy))
  93. handle Symtab.DUP _ => error("Assertion already defined: "^name)
  94. end
  95. fun dispatch assertion args thy =
  96. let
  97. val tab = (Data.get o Context.Theory) thy
  98. val _ = (case Symtab.lookup tab assertion of
  99. SOME a => (#assertion a) thy args
  100. | NONE => error ("No assertion registered: "^assertion))
  101. in
  102. thy
  103. end
  104. end
  105. \<close>
  106. ML\<open>
  107. val argP =
  108. Parse.position Parse.name
  109. -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.string) "";
  110. val argsP =
  111. (Parse.$$$ "["
  112. |-- (Parse.position Parse.name --
  113. (Scan.optional(Parse.$$$ "," |-- (Parse.enum "," argP))) []))
  114. --| Parse.$$$ "]"
  115. val _ = Outer_Syntax.command @{command_keyword "assert"}
  116. "theory assertion"
  117. (argsP >> (fn ((assert,_),args) =>
  118. (Toplevel.theory (Assert.dispatch assert args))));
  119. \<close>
  120. section\<open>Utilities for Writing And Registering Assertions on the ML Level\<close>
  121. ML\<open>
  122. signature ASSERT_UTIL = sig
  123. val get_mandatory_arg : (string * string) list -> string -> string
  124. val get_optional_arg : (string * string) list -> string -> string option
  125. val parse_args : Assert.arg_specT list -> Assert.arg_parseT list
  126. -> (string * string) list
  127. val str_of_thm : Proof.context -> thm -> string
  128. end
  129. structure Assert_Util : ASSERT_UTIL = struct
  130. fun clean_ws s =
  131. let
  132. fun ws (c1::c2::cs) = if c1 = #" " andalso c2 = #" "
  133. then ws (c2::cs)
  134. else c1::(ws (c2::cs))
  135. | ws [c] = [c]
  136. | ws [] = []
  137. in
  138. String.implode (ws (String.explode
  139. (String.map (fn c => if c = #"\n" then #" " else c) s)))
  140. end
  141. fun str_of_thm ctx thm = clean_ws (Print_Mode.setmp []
  142. (Thm.string_of_thm
  143. (ctx |> Config.put show_markup false
  144. |> Config.put show_question_marks false
  145. |> Config.put show_types true
  146. )
  147. ) thm)
  148. fun parse_args spec (((name,_),value)::args) =
  149. let
  150. val arg = case filter (fn (name',_,_) => (name' = name)) spec of
  151. [v] => v
  152. | [] => error ("Not a valid argument: "^name)
  153. | _ => error ("Argument given multiple times: "^name)
  154. val spec = filter (fn arg' => arg <> arg') spec
  155. in
  156. (name, value)::(parse_args spec args)
  157. end
  158. | parse_args spec [] =
  159. let
  160. val default_args = map (fn (n, _, v) => (n, the v))
  161. (filter (fn (_,_,value) => value <> NONE) spec)
  162. val missing_args = filter (fn (_,typ,value) => typ = Assert.mandatory
  163. andalso value = NONE) spec
  164. in
  165. if missing_args = []
  166. then default_args
  167. else
  168. error(List.foldl (fn (s,s') => (s ^"\n"^s')) ""
  169. (map (fn (n,_,_) => "Mandatory argument missing: "^n)
  170. missing_args))
  171. end
  172. fun get_mandatory_arg ((name', s)::vals) name =
  173. if name = name' then s
  174. else get_mandatory_arg vals name
  175. | get_mandatory_arg [] name = error ("Mandatory arg "^name^" not found.")
  176. fun get_optional_arg ((name',s)::vals) name =
  177. if name = name' then SOME s
  178. else get_optional_arg vals name
  179. | get_optional_arg [] _ = NONE
  180. end
  181. \<close>
  182. section\<open>Am Example\<close>
  183. ML\<open>
  184. signature STRING_OF_THM_CMP_ASSERT = sig
  185. val string_of_thm_equal : Assert.assertionT
  186. val string_of_thm_notequal : Assert.assertionT
  187. end
  188. structure String_of_thm_cmp_assert : STRING_OF_THM_CMP_ASSERT = struct
  189. fun assert_string_of_thm_cmp cmp ctx thm str =
  190. let
  191. val str' = Assert_Util.str_of_thm ctx thm
  192. in
  193. if not (cmp(str,str'))
  194. then error ("assert_string_of_thm_equal failed, got '"
  195. ^str'^"' expected '"^str^"'.")
  196. else ()
  197. end
  198. fun assert_string_of_thm_cmp_args cmp thy args =
  199. let
  200. val ctx = Toplevel.context_of(Toplevel.theory_toplevel thy)
  201. val spec = [("thm_def", Assert.mandatory, NONE),
  202. ("str", Assert.mandatory, NONE)]
  203. val vals = Assert_Util.parse_args spec args
  204. val thm_name = Assert_Util.get_mandatory_arg vals "thm_def"
  205. val thm_def = (Global_Theory.get_thm thy thm_name)
  206. val str = Assert_Util.get_mandatory_arg vals "str"
  207. in
  208. assert_string_of_thm_cmp cmp ctx thm_def str
  209. end
  210. val string_of_thm_equal = {
  211. name = "string_of_thm_equal",
  212. description = "Check that string representation (including types) "
  213. ^"matches given string.",
  214. assertion = (assert_string_of_thm_cmp_args (=))
  215. }
  216. val string_of_thm_notequal = {
  217. name = "string_of_thm_notequal",
  218. description = "Check that string representation (including types) "
  219. ^"does not match given string.",
  220. assertion = (assert_string_of_thm_cmp_args (<>))
  221. }
  222. end
  223. \<close>
  224. setup\<open>
  225. fn thy => thy
  226. |> (Assert.register String_of_thm_cmp_assert.string_of_thm_equal)
  227. |> (Assert.register String_of_thm_cmp_assert.string_of_thm_notequal)
  228. \<close>
  229. section\<open>Examples\<close>
  230. assert[string_of_thm_equal,
  231. thm_def="True_def", str="True \<equiv> (\<lambda>x::bool. x) = (\<lambda>x::bool. x)"]
  232. assert[string_of_thm_notequal,
  233. thm_def="True_def", str="False \<equiv> (\<lambda>x::bool. x) = (\<lambda>x::bool. x)"]
  234. end