|
- (***********************************************************************************
- * Copyright (c) 2018-2019 Achim D. Brucker
- *
- * All rights reserved.
- *
- * Redistribution and use in source and binary forms, with or without
- * modification, are permitted provided that the following conditions are met:
- *
- * * Redistributions of source code must retain the above copyright notice, this
- *
- * * Redistributions in binary form must reproduce the above copyright notice,
- * this list of conditions and the following disclaimer in the documentation
- * and/or other materials provided with the distribution.
- *
- * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
- * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
- * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
- * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
- * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
- * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
- * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
- * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
- * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
- * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
- *
- * SPDX-License-Identifier: BSD-2-Clause
- * Repository: https://git.logicalhacking.com/adbrucker/isabelle-hacks/
- * Dependencies: None
- ***********************************************************************************)
-
- (***********************************************************************************
-
- # Changelog
-
- This comment documents all notable changes to this file in a format inspired by
- [Keep a Changelog](https://keepachangelog.com/en/1.0.0/), and this project adheres
- to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
-
- ## [Unreleased]
-
- ## [1.0.0] - 2018-06-16
- - Initial release
-
- ***********************************************************************************)
-
- chapter\<open>An Assertion Framework for Isabelle\<close>
- theory
- "Assert"
- imports
- Main
- keywords
- "assert"::thy_decl
- begin
- text\<open>This theory implements a simple @{emph \<open>assertion framework\<close>} for Isabelle:
- it introduces a new top level command @{bold \<open>assert\<close>} that allows for
- checking an assertion. The overall idea is very similar to the assert
- annotations that man unit test frameworks provide. New assertion
- types can be registered on the ML level of Isabelle.\<close>
-
- section\<open>The Core Assertion Framework\<close>
-
- ML\<open>
- signature ASSERT = sig
- datatype arg_class = optional | mandatory
- type arg_parseT = ((string * Position.T) * string)
- type arg_specT = (string * arg_class * string option)
- type checkT = theory -> arg_parseT list -> unit
- type assertionT = {
- name : string,
- description: string,
- assertion: checkT
- }
- val dispatch : string -> arg_parseT list -> theory -> theory
- val register : assertionT-> theory -> theory
- end
-
- structure Assert : ASSERT = struct
- datatype arg_class = optional | mandatory
- type arg_parseT = ((string * Position.T) * string)
- type arg_specT = (string * arg_class * string option)
- type checkT = theory -> arg_parseT list -> unit
- type assertionT = {
- name : string,
- description: string,
- assertion: checkT
- }
- type assert_tab = (assertionT) Symtab.table
-
- fun assertion_eq (a, a') = (#name a) = (#name a')
-
- fun merge_assert_tab (tab,tab') = Symtab.merge assertion_eq (tab,tab')
-
- structure Data = Generic_Data
- (
- type T = assert_tab
- val empty = Symtab.empty:assert_tab
- val extend = I
- fun merge(t1,t2) = merge_assert_tab (t1, t2)
- );
-
- fun register assertion thy =
- let
- val name = #name assertion
- fun reg tab = Symtab.update_new(name, assertion) tab
- in
- Context.theory_of ( (Data.map reg) (Context.Theory thy))
- handle Symtab.DUP _ => error("Assertion already defined: "^name)
- end
-
- fun dispatch assertion args thy =
- let
- val tab = (Data.get o Context.Theory) thy
- val _ = (case Symtab.lookup tab assertion of
- SOME a => (#assertion a) thy args
- | NONE => error ("No assertion registered: "^assertion))
- in
- thy
- end
- end
- \<close>
-
- ML\<open>
- val argP =
- Parse.position Parse.name
- -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.string) "";
-
- val argsP =
- (Parse.$$$ "["
- |-- (Parse.position Parse.name --
- (Scan.optional(Parse.$$$ "," |-- (Parse.enum "," argP))) []))
- --| Parse.$$$ "]"
-
- val _ = Outer_Syntax.command @{command_keyword "assert"}
- "theory assertion"
- (argsP >> (fn ((assert,_),args) =>
- (Toplevel.theory (Assert.dispatch assert args))));
- \<close>
-
- section\<open>Utilities for Writing And Registering Assertions on the ML Level\<close>
- ML\<open>
- signature ASSERT_UTIL = sig
- val get_mandatory_arg : (string * string) list -> string -> string
- val get_optional_arg : (string * string) list -> string -> string option
- val parse_args : Assert.arg_specT list -> Assert.arg_parseT list
- -> (string * string) list
- val str_of_thm : Proof.context -> thm -> string
- end
-
- structure Assert_Util : ASSERT_UTIL = struct
- fun clean_ws s =
- let
- fun ws (c1::c2::cs) = if c1 = #" " andalso c2 = #" "
- then ws (c2::cs)
- else c1::(ws (c2::cs))
- | ws [c] = [c]
- | ws [] = []
- in
- String.implode (ws (String.explode
- (String.map (fn c => if c = #"\n" then #" " else c) s)))
- end
-
- fun str_of_thm ctx thm = clean_ws (Print_Mode.setmp []
- (Thm.string_of_thm
- (ctx |> Config.put show_markup false
- |> Config.put show_question_marks false
- |> Config.put show_types true
- )
- ) thm)
- fun parse_args spec (((name,_),value)::args) =
- let
- val arg = case filter (fn (name',_,_) => (name' = name)) spec of
- [v] => v
- | [] => error ("Not a valid argument: "^name)
- | _ => error ("Argument given multiple times: "^name)
- val spec = filter (fn arg' => arg <> arg') spec
- in
- (name, value)::(parse_args spec args)
- end
- | parse_args spec [] =
- let
- val default_args = map (fn (n, _, v) => (n, the v))
- (filter (fn (_,_,value) => value <> NONE) spec)
- val missing_args = filter (fn (_,typ,value) => typ = Assert.mandatory
- andalso value = NONE) spec
- in
- if missing_args = []
- then default_args
- else
- error(List.foldl (fn (s,s') => (s ^"\n"^s')) ""
- (map (fn (n,_,_) => "Mandatory argument missing: "^n)
- missing_args))
- end
- fun get_mandatory_arg ((name', s)::vals) name =
- if name = name' then s
- else get_mandatory_arg vals name
- | get_mandatory_arg [] name = error ("Mandatory arg "^name^" not found.")
- fun get_optional_arg ((name',s)::vals) name =
- if name = name' then SOME s
- else get_optional_arg vals name
- | get_optional_arg [] _ = NONE
-
- end
- \<close>
-
- section\<open>Am Example\<close>
-
- ML\<open>
- signature STRING_OF_THM_CMP_ASSERT = sig
- val string_of_thm_equal : Assert.assertionT
- val string_of_thm_notequal : Assert.assertionT
- end
-
- structure String_of_thm_cmp_assert : STRING_OF_THM_CMP_ASSERT = struct
- fun assert_string_of_thm_cmp cmp ctx thm str =
- let
- val str' = Assert_Util.str_of_thm ctx thm
- in
- if not (cmp(str,str'))
- then error ("assert_string_of_thm_equal failed, got '"
- ^str'^"' expected '"^str^"'.")
- else ()
- end
-
- fun assert_string_of_thm_cmp_args cmp thy args =
- let
- val ctx = Toplevel.context_of(Toplevel.theory_toplevel thy)
- val spec = [("thm_def", Assert.mandatory, NONE),
- ("str", Assert.mandatory, NONE)]
- val vals = Assert_Util.parse_args spec args
- val thm_name = Assert_Util.get_mandatory_arg vals "thm_def"
- val thm_def = (Global_Theory.get_thm thy thm_name)
- val str = Assert_Util.get_mandatory_arg vals "str"
- in
- assert_string_of_thm_cmp cmp ctx thm_def str
- end
-
- val string_of_thm_equal = {
- name = "string_of_thm_equal",
- description = "Check that string representation (including types) "
- ^"matches given string.",
- assertion = (assert_string_of_thm_cmp_args (=))
- }
-
- val string_of_thm_notequal = {
- name = "string_of_thm_notequal",
- description = "Check that string representation (including types) "
- ^"does not match given string.",
- assertion = (assert_string_of_thm_cmp_args (<>))
- }
- end
- \<close>
-
- setup\<open>
- fn thy => thy
- |> (Assert.register String_of_thm_cmp_assert.string_of_thm_equal)
- |> (Assert.register String_of_thm_cmp_assert.string_of_thm_notequal)
- \<close>
-
- section\<open>Examples\<close>
-
- assert[string_of_thm_equal,
- thm_def="True_def", str="True \<equiv> (\<lambda>x::bool. x) = (\<lambda>x::bool. x)"]
- assert[string_of_thm_notequal,
- thm_def="True_def", str="False \<equiv> (\<lambda>x::bool. x) = (\<lambda>x::bool. x)"]
- end
|