266 lines
9.8 KiB
Plaintext
266 lines
9.8 KiB
Plaintext
(***********************************************************************************
|
|
* 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
|