--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Examples/Functions.thy Wed Aug 25 22:17:38 2021 +0200
@@ -0,0 +1,519 @@
+(* Title: HOL/ex/Functions.thy
+ Author: Alexander Krauss, TU Muenchen
+*)
+
+section \<open>Examples of function definitions\<close>
+
+theory Functions
+imports Main "HOL-Library.Monad_Syntax"
+begin
+
+subsection \<open>Very basic\<close>
+
+fun fib :: "nat \<Rightarrow> nat"
+where
+ "fib 0 = 1"
+| "fib (Suc 0) = 1"
+| "fib (Suc (Suc n)) = fib n + fib (Suc n)"
+
+text \<open>Partial simp and induction rules:\<close>
+thm fib.psimps
+thm fib.pinduct
+
+text \<open>There is also a cases rule to distinguish cases along the definition:\<close>
+thm fib.cases
+
+
+text \<open>Total simp and induction rules:\<close>
+thm fib.simps
+thm fib.induct
+
+text \<open>Elimination rules:\<close>
+thm fib.elims
+
+
+subsection \<open>Currying\<close>
+
+fun add
+where
+ "add 0 y = y"
+| "add (Suc x) y = Suc (add x y)"
+
+thm add.simps
+thm add.induct \<comment> \<open>Note the curried induction predicate\<close>
+
+
+subsection \<open>Nested recursion\<close>
+
+function nz
+where
+ "nz 0 = 0"
+| "nz (Suc x) = nz (nz x)"
+by pat_completeness auto
+
+lemma nz_is_zero: \<comment> \<open>A lemma we need to prove termination\<close>
+ assumes trm: "nz_dom x"
+ shows "nz x = 0"
+using trm
+by induct (auto simp: nz.psimps)
+
+termination nz
+ by (relation "less_than") (auto simp:nz_is_zero)
+
+thm nz.simps
+thm nz.induct
+
+
+subsubsection \<open>Here comes McCarthy's 91-function\<close>
+
+function f91 :: "nat \<Rightarrow> nat"
+where
+ "f91 n = (if 100 < n then n - 10 else f91 (f91 (n + 11)))"
+by pat_completeness auto
+
+text \<open>Prove a lemma before attempting a termination proof:\<close>
+lemma f91_estimate:
+ assumes trm: "f91_dom n"
+ shows "n < f91 n + 11"
+using trm by induct (auto simp: f91.psimps)
+
+termination
+proof
+ let ?R = "measure (\<lambda>x. 101 - x)"
+ show "wf ?R" ..
+
+ fix n :: nat
+ assume "\<not> 100 < n" \<comment> \<open>Inner call\<close>
+ then show "(n + 11, n) \<in> ?R" by simp
+
+ assume inner_trm: "f91_dom (n + 11)" \<comment> \<open>Outer call\<close>
+ with f91_estimate have "n + 11 < f91 (n + 11) + 11" .
+ with \<open>\<not> 100 < n\<close> show "(f91 (n + 11), n) \<in> ?R" by simp
+qed
+
+text \<open>Now trivial (even though it does not belong here):\<close>
+lemma "f91 n = (if 100 < n then n - 10 else 91)"
+ by (induct n rule: f91.induct) auto
+
+
+subsubsection \<open>Here comes Takeuchi's function\<close>
+
+definition tak_m1 where "tak_m1 = (\<lambda>(x,y,z). if x \<le> y then 0 else 1)"
+definition tak_m2 where "tak_m2 = (\<lambda>(x,y,z). nat (Max {x, y, z} - Min {x, y, z}))"
+definition tak_m3 where "tak_m3 = (\<lambda>(x,y,z). nat (x - Min {x, y, z}))"
+
+function tak :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int" where
+ "tak x y z = (if x \<le> y then y else tak (tak (x-1) y z) (tak (y-1) z x) (tak (z-1) x y))"
+ by auto
+
+lemma tak_pcorrect:
+ "tak_dom (x, y, z) \<Longrightarrow> tak x y z = (if x \<le> y then y else if y \<le> z then z else x)"
+ by (induction x y z rule: tak.pinduct) (auto simp: tak.psimps)
+
+termination
+ by (relation "tak_m1 <*mlex*> tak_m2 <*mlex*> tak_m3 <*mlex*> {}")
+ (auto simp: mlex_iff wf_mlex tak_pcorrect tak_m1_def tak_m2_def tak_m3_def min_def max_def)
+
+theorem tak_correct: "tak x y z = (if x \<le> y then y else if y \<le> z then z else x)"
+ by (induction x y z rule: tak.induct) auto
+
+
+subsection \<open>More general patterns\<close>
+
+subsubsection \<open>Overlapping patterns\<close>
+
+text \<open>
+ Currently, patterns must always be compatible with each other, since
+ no automatic splitting takes place. But the following definition of
+ GCD is OK, although patterns overlap:
+\<close>
+
+fun gcd2 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+where
+ "gcd2 x 0 = x"
+| "gcd2 0 y = y"
+| "gcd2 (Suc x) (Suc y) = (if x < y then gcd2 (Suc x) (y - x)
+ else gcd2 (x - y) (Suc y))"
+
+thm gcd2.simps
+thm gcd2.induct
+
+
+subsubsection \<open>Guards\<close>
+
+text \<open>We can reformulate the above example using guarded patterns:\<close>
+
+function gcd3 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+where
+ "gcd3 x 0 = x"
+| "gcd3 0 y = y"
+| "gcd3 (Suc x) (Suc y) = gcd3 (Suc x) (y - x)" if "x < y"
+| "gcd3 (Suc x) (Suc y) = gcd3 (x - y) (Suc y)" if "\<not> x < y"
+ apply (case_tac x, case_tac a, auto)
+ apply (case_tac ba, auto)
+ done
+termination by lexicographic_order
+
+thm gcd3.simps
+thm gcd3.induct
+
+
+text \<open>General patterns allow even strange definitions:\<close>
+
+function ev :: "nat \<Rightarrow> bool"
+where
+ "ev (2 * n) = True"
+| "ev (2 * n + 1) = False"
+proof - \<comment> \<open>completeness is more difficult here \dots\<close>
+ fix P :: bool
+ fix x :: nat
+ assume c1: "\<And>n. x = 2 * n \<Longrightarrow> P"
+ and c2: "\<And>n. x = 2 * n + 1 \<Longrightarrow> P"
+ have divmod: "x = 2 * (x div 2) + (x mod 2)" by auto
+ show P
+ proof (cases "x mod 2 = 0")
+ case True
+ with divmod have "x = 2 * (x div 2)" by simp
+ with c1 show "P" .
+ next
+ case False
+ then have "x mod 2 = 1" by simp
+ with divmod have "x = 2 * (x div 2) + 1" by simp
+ with c2 show "P" .
+ qed
+qed presburger+ \<comment> \<open>solve compatibility with presburger\<close>
+termination by lexicographic_order
+
+thm ev.simps
+thm ev.induct
+thm ev.cases
+
+
+subsection \<open>Mutual Recursion\<close>
+
+fun evn od :: "nat \<Rightarrow> bool"
+where
+ "evn 0 = True"
+| "od 0 = False"
+| "evn (Suc n) = od n"
+| "od (Suc n) = evn n"
+
+thm evn.simps
+thm od.simps
+
+thm evn_od.induct
+thm evn_od.termination
+
+thm evn.elims
+thm od.elims
+
+
+subsection \<open>Definitions in local contexts\<close>
+
+locale my_monoid =
+ fixes opr :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
+ and un :: "'a"
+ assumes assoc: "opr (opr x y) z = opr x (opr y z)"
+ and lunit: "opr un x = x"
+ and runit: "opr x un = x"
+begin
+
+fun foldR :: "'a list \<Rightarrow> 'a"
+where
+ "foldR [] = un"
+| "foldR (x # xs) = opr x (foldR xs)"
+
+fun foldL :: "'a list \<Rightarrow> 'a"
+where
+ "foldL [] = un"
+| "foldL [x] = x"
+| "foldL (x # y # ys) = foldL (opr x y # ys)"
+
+thm foldL.simps
+
+lemma foldR_foldL: "foldR xs = foldL xs"
+ by (induct xs rule: foldL.induct) (auto simp:lunit runit assoc)
+
+thm foldR_foldL
+
+end
+
+thm my_monoid.foldL.simps
+thm my_monoid.foldR_foldL
+
+
+subsection \<open>\<open>fun_cases\<close>\<close>
+
+subsubsection \<open>Predecessor\<close>
+
+fun pred :: "nat \<Rightarrow> nat"
+where
+ "pred 0 = 0"
+| "pred (Suc n) = n"
+
+thm pred.elims
+
+lemma
+ assumes "pred x = y"
+ obtains "x = 0" "y = 0" | "n" where "x = Suc n" "y = n"
+ by (fact pred.elims[OF assms])
+
+
+text \<open>If the predecessor of a number is 0, that number must be 0 or 1.\<close>
+
+fun_cases pred0E[elim]: "pred n = 0"
+
+lemma "pred n = 0 \<Longrightarrow> n = 0 \<or> n = Suc 0"
+ by (erule pred0E) metis+
+
+text \<open>
+ Other expressions on the right-hand side also work, but whether the
+ generated rule is useful depends on how well the simplifier can
+ simplify it. This example works well:
+\<close>
+
+fun_cases pred42E[elim]: "pred n = 42"
+
+lemma "pred n = 42 \<Longrightarrow> n = 43"
+ by (erule pred42E)
+
+
+subsubsection \<open>List to option\<close>
+
+fun list_to_option :: "'a list \<Rightarrow> 'a option"
+where
+ "list_to_option [x] = Some x"
+| "list_to_option _ = None"
+
+fun_cases list_to_option_NoneE: "list_to_option xs = None"
+ and list_to_option_SomeE: "list_to_option xs = Some x"
+
+lemma "list_to_option xs = Some y \<Longrightarrow> xs = [y]"
+ by (erule list_to_option_SomeE)
+
+
+subsubsection \<open>Boolean Functions\<close>
+
+fun xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
+where
+ "xor False False = False"
+| "xor True True = False"
+| "xor _ _ = True"
+
+thm xor.elims
+
+text \<open>
+ \<open>fun_cases\<close> does not only recognise function equations, but also works with
+ functions that return a boolean, e.g.:
+\<close>
+
+fun_cases xor_TrueE: "xor a b" and xor_FalseE: "\<not>xor a b"
+print_theorems
+
+
+subsubsection \<open>Many parameters\<close>
+
+fun sum4 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+ where "sum4 a b c d = a + b + c + d"
+
+fun_cases sum40E: "sum4 a b c d = 0"
+
+lemma "sum4 a b c d = 0 \<Longrightarrow> a = 0"
+ by (erule sum40E)
+
+
+subsection \<open>Partial Function Definitions\<close>
+
+text \<open>Partial functions in the option monad:\<close>
+
+partial_function (option)
+ collatz :: "nat \<Rightarrow> nat list option"
+where
+ "collatz n =
+ (if n \<le> 1 then Some [n]
+ else if even n
+ then do { ns \<leftarrow> collatz (n div 2); Some (n # ns) }
+ else do { ns \<leftarrow> collatz (3 * n + 1); Some (n # ns)})"
+
+declare collatz.simps[code]
+value "collatz 23"
+
+
+text \<open>Tail-recursive functions:\<close>
+
+partial_function (tailrec) fixpoint :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
+where
+ "fixpoint f x = (if f x = x then x else fixpoint f (f x))"
+
+
+subsection \<open>Regression tests\<close>
+
+text \<open>
+ The following examples mainly serve as tests for the
+ function package.
+\<close>
+
+fun listlen :: "'a list \<Rightarrow> nat"
+where
+ "listlen [] = 0"
+| "listlen (x#xs) = Suc (listlen xs)"
+
+
+subsubsection \<open>Context recursion\<close>
+
+fun f :: "nat \<Rightarrow> nat"
+where
+ zero: "f 0 = 0"
+| succ: "f (Suc n) = (if f n = 0 then 0 else f n)"
+
+
+subsubsection \<open>A combination of context and nested recursion\<close>
+
+function h :: "nat \<Rightarrow> nat"
+where
+ "h 0 = 0"
+| "h (Suc n) = (if h n = 0 then h (h n) else h n)"
+by pat_completeness auto
+
+
+subsubsection \<open>Context, but no recursive call\<close>
+
+fun i :: "nat \<Rightarrow> nat"
+where
+ "i 0 = 0"
+| "i (Suc n) = (if n = 0 then 0 else i n)"
+
+
+subsubsection \<open>Tupled nested recursion\<close>
+
+fun fa :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+where
+ "fa 0 y = 0"
+| "fa (Suc n) y = (if fa n y = 0 then 0 else fa n y)"
+
+
+subsubsection \<open>Let\<close>
+
+fun j :: "nat \<Rightarrow> nat"
+where
+ "j 0 = 0"
+| "j (Suc n) = (let u = n in Suc (j u))"
+
+
+text \<open>There were some problems with fresh names \dots\<close>
+function k :: "nat \<Rightarrow> nat"
+where
+ "k x = (let a = x; b = x in k x)"
+ by pat_completeness auto
+
+
+function f2 :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
+where
+ "f2 p = (let (x,y) = p in f2 (y,x))"
+ by pat_completeness auto
+
+
+subsubsection \<open>Abbreviations\<close>
+
+fun f3 :: "'a set \<Rightarrow> bool"
+where
+ "f3 x = finite x"
+
+
+subsubsection \<open>Simple Higher-Order Recursion\<close>
+
+datatype 'a tree = Leaf 'a | Branch "'a tree list"
+
+fun treemap :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a tree \<Rightarrow> 'a tree"
+where
+ "treemap fn (Leaf n) = (Leaf (fn n))"
+| "treemap fn (Branch l) = (Branch (map (treemap fn) l))"
+
+fun tinc :: "nat tree \<Rightarrow> nat tree"
+where
+ "tinc (Leaf n) = Leaf (Suc n)"
+| "tinc (Branch l) = Branch (map tinc l)"
+
+fun testcase :: "'a tree \<Rightarrow> 'a list"
+where
+ "testcase (Leaf a) = [a]"
+| "testcase (Branch x) =
+ (let xs = concat (map testcase x);
+ ys = concat (map testcase x) in
+ xs @ ys)"
+
+
+subsubsection \<open>Pattern matching on records\<close>
+
+record point =
+ Xcoord :: int
+ Ycoord :: int
+
+function swp :: "point \<Rightarrow> point"
+where
+ "swp \<lparr> Xcoord = x, Ycoord = y \<rparr> = \<lparr> Xcoord = y, Ycoord = x \<rparr>"
+proof -
+ fix P x
+ assume "\<And>xa y. x = \<lparr>Xcoord = xa, Ycoord = y\<rparr> \<Longrightarrow> P"
+ then show P by (cases x)
+qed auto
+termination by rule auto
+
+
+subsubsection \<open>The diagonal function\<close>
+
+fun diag :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> nat"
+where
+ "diag x True False = 1"
+| "diag False y True = 2"
+| "diag True False z = 3"
+| "diag True True True = 4"
+| "diag False False False = 5"
+
+
+subsubsection \<open>Many equations (quadratic blowup)\<close>
+
+datatype DT =
+ A | B | C | D | E | F | G | H | I | J | K | L | M | N | P
+| Q | R | S | T | U | V
+
+fun big :: "DT \<Rightarrow> nat"
+where
+ "big A = 0"
+| "big B = 0"
+| "big C = 0"
+| "big D = 0"
+| "big E = 0"
+| "big F = 0"
+| "big G = 0"
+| "big H = 0"
+| "big I = 0"
+| "big J = 0"
+| "big K = 0"
+| "big L = 0"
+| "big M = 0"
+| "big N = 0"
+| "big P = 0"
+| "big Q = 0"
+| "big R = 0"
+| "big S = 0"
+| "big T = 0"
+| "big U = 0"
+| "big V = 0"
+
+
+subsubsection \<open>Automatic pattern splitting\<close>
+
+fun f4 :: "nat \<Rightarrow> nat \<Rightarrow> bool"
+where
+ "f4 0 0 = True"
+| "f4 _ _ = False"
+
+
+subsubsection \<open>Polymorphic partial-function\<close>
+
+partial_function (option) f5 :: "'a list \<Rightarrow> 'a option"
+where
+ "f5 x = f5 x"
+
+end
--- a/src/HOL/ROOT Wed Aug 25 22:16:27 2021 +0200
+++ b/src/HOL/ROOT Wed Aug 25 22:17:38 2021 +0200
@@ -28,6 +28,7 @@
Coherent
Commands
Drinker
+ Functions
Groebner_Examples
Iff_Oracle
Induction_Schema
@@ -665,7 +666,6 @@
Eval_Examples
Executable_Relation
Execute_Choice
- Functions
Function_Growth
Gauge_Integration
Guess
--- a/src/HOL/ex/Functions.thy Wed Aug 25 22:16:27 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,519 +0,0 @@
-(* Title: HOL/ex/Functions.thy
- Author: Alexander Krauss, TU Muenchen
-*)
-
-section \<open>Examples of function definitions\<close>
-
-theory Functions
-imports Main "HOL-Library.Monad_Syntax"
-begin
-
-subsection \<open>Very basic\<close>
-
-fun fib :: "nat \<Rightarrow> nat"
-where
- "fib 0 = 1"
-| "fib (Suc 0) = 1"
-| "fib (Suc (Suc n)) = fib n + fib (Suc n)"
-
-text \<open>Partial simp and induction rules:\<close>
-thm fib.psimps
-thm fib.pinduct
-
-text \<open>There is also a cases rule to distinguish cases along the definition:\<close>
-thm fib.cases
-
-
-text \<open>Total simp and induction rules:\<close>
-thm fib.simps
-thm fib.induct
-
-text \<open>Elimination rules:\<close>
-thm fib.elims
-
-
-subsection \<open>Currying\<close>
-
-fun add
-where
- "add 0 y = y"
-| "add (Suc x) y = Suc (add x y)"
-
-thm add.simps
-thm add.induct \<comment> \<open>Note the curried induction predicate\<close>
-
-
-subsection \<open>Nested recursion\<close>
-
-function nz
-where
- "nz 0 = 0"
-| "nz (Suc x) = nz (nz x)"
-by pat_completeness auto
-
-lemma nz_is_zero: \<comment> \<open>A lemma we need to prove termination\<close>
- assumes trm: "nz_dom x"
- shows "nz x = 0"
-using trm
-by induct (auto simp: nz.psimps)
-
-termination nz
- by (relation "less_than") (auto simp:nz_is_zero)
-
-thm nz.simps
-thm nz.induct
-
-
-subsubsection \<open>Here comes McCarthy's 91-function\<close>
-
-function f91 :: "nat \<Rightarrow> nat"
-where
- "f91 n = (if 100 < n then n - 10 else f91 (f91 (n + 11)))"
-by pat_completeness auto
-
-text \<open>Prove a lemma before attempting a termination proof:\<close>
-lemma f91_estimate:
- assumes trm: "f91_dom n"
- shows "n < f91 n + 11"
-using trm by induct (auto simp: f91.psimps)
-
-termination
-proof
- let ?R = "measure (\<lambda>x. 101 - x)"
- show "wf ?R" ..
-
- fix n :: nat
- assume "\<not> 100 < n" \<comment> \<open>Inner call\<close>
- then show "(n + 11, n) \<in> ?R" by simp
-
- assume inner_trm: "f91_dom (n + 11)" \<comment> \<open>Outer call\<close>
- with f91_estimate have "n + 11 < f91 (n + 11) + 11" .
- with \<open>\<not> 100 < n\<close> show "(f91 (n + 11), n) \<in> ?R" by simp
-qed
-
-text \<open>Now trivial (even though it does not belong here):\<close>
-lemma "f91 n = (if 100 < n then n - 10 else 91)"
- by (induct n rule: f91.induct) auto
-
-
-subsubsection \<open>Here comes Takeuchi's function\<close>
-
-definition tak_m1 where "tak_m1 = (\<lambda>(x,y,z). if x \<le> y then 0 else 1)"
-definition tak_m2 where "tak_m2 = (\<lambda>(x,y,z). nat (Max {x, y, z} - Min {x, y, z}))"
-definition tak_m3 where "tak_m3 = (\<lambda>(x,y,z). nat (x - Min {x, y, z}))"
-
-function tak :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int" where
- "tak x y z = (if x \<le> y then y else tak (tak (x-1) y z) (tak (y-1) z x) (tak (z-1) x y))"
- by auto
-
-lemma tak_pcorrect:
- "tak_dom (x, y, z) \<Longrightarrow> tak x y z = (if x \<le> y then y else if y \<le> z then z else x)"
- by (induction x y z rule: tak.pinduct) (auto simp: tak.psimps)
-
-termination
- by (relation "tak_m1 <*mlex*> tak_m2 <*mlex*> tak_m3 <*mlex*> {}")
- (auto simp: mlex_iff wf_mlex tak_pcorrect tak_m1_def tak_m2_def tak_m3_def min_def max_def)
-
-theorem tak_correct: "tak x y z = (if x \<le> y then y else if y \<le> z then z else x)"
- by (induction x y z rule: tak.induct) auto
-
-
-subsection \<open>More general patterns\<close>
-
-subsubsection \<open>Overlapping patterns\<close>
-
-text \<open>
- Currently, patterns must always be compatible with each other, since
- no automatic splitting takes place. But the following definition of
- GCD is OK, although patterns overlap:
-\<close>
-
-fun gcd2 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-where
- "gcd2 x 0 = x"
-| "gcd2 0 y = y"
-| "gcd2 (Suc x) (Suc y) = (if x < y then gcd2 (Suc x) (y - x)
- else gcd2 (x - y) (Suc y))"
-
-thm gcd2.simps
-thm gcd2.induct
-
-
-subsubsection \<open>Guards\<close>
-
-text \<open>We can reformulate the above example using guarded patterns:\<close>
-
-function gcd3 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-where
- "gcd3 x 0 = x"
-| "gcd3 0 y = y"
-| "gcd3 (Suc x) (Suc y) = gcd3 (Suc x) (y - x)" if "x < y"
-| "gcd3 (Suc x) (Suc y) = gcd3 (x - y) (Suc y)" if "\<not> x < y"
- apply (case_tac x, case_tac a, auto)
- apply (case_tac ba, auto)
- done
-termination by lexicographic_order
-
-thm gcd3.simps
-thm gcd3.induct
-
-
-text \<open>General patterns allow even strange definitions:\<close>
-
-function ev :: "nat \<Rightarrow> bool"
-where
- "ev (2 * n) = True"
-| "ev (2 * n + 1) = False"
-proof - \<comment> \<open>completeness is more difficult here \dots\<close>
- fix P :: bool
- fix x :: nat
- assume c1: "\<And>n. x = 2 * n \<Longrightarrow> P"
- and c2: "\<And>n. x = 2 * n + 1 \<Longrightarrow> P"
- have divmod: "x = 2 * (x div 2) + (x mod 2)" by auto
- show P
- proof (cases "x mod 2 = 0")
- case True
- with divmod have "x = 2 * (x div 2)" by simp
- with c1 show "P" .
- next
- case False
- then have "x mod 2 = 1" by simp
- with divmod have "x = 2 * (x div 2) + 1" by simp
- with c2 show "P" .
- qed
-qed presburger+ \<comment> \<open>solve compatibility with presburger\<close>
-termination by lexicographic_order
-
-thm ev.simps
-thm ev.induct
-thm ev.cases
-
-
-subsection \<open>Mutual Recursion\<close>
-
-fun evn od :: "nat \<Rightarrow> bool"
-where
- "evn 0 = True"
-| "od 0 = False"
-| "evn (Suc n) = od n"
-| "od (Suc n) = evn n"
-
-thm evn.simps
-thm od.simps
-
-thm evn_od.induct
-thm evn_od.termination
-
-thm evn.elims
-thm od.elims
-
-
-subsection \<open>Definitions in local contexts\<close>
-
-locale my_monoid =
- fixes opr :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
- and un :: "'a"
- assumes assoc: "opr (opr x y) z = opr x (opr y z)"
- and lunit: "opr un x = x"
- and runit: "opr x un = x"
-begin
-
-fun foldR :: "'a list \<Rightarrow> 'a"
-where
- "foldR [] = un"
-| "foldR (x # xs) = opr x (foldR xs)"
-
-fun foldL :: "'a list \<Rightarrow> 'a"
-where
- "foldL [] = un"
-| "foldL [x] = x"
-| "foldL (x # y # ys) = foldL (opr x y # ys)"
-
-thm foldL.simps
-
-lemma foldR_foldL: "foldR xs = foldL xs"
- by (induct xs rule: foldL.induct) (auto simp:lunit runit assoc)
-
-thm foldR_foldL
-
-end
-
-thm my_monoid.foldL.simps
-thm my_monoid.foldR_foldL
-
-
-subsection \<open>\<open>fun_cases\<close>\<close>
-
-subsubsection \<open>Predecessor\<close>
-
-fun pred :: "nat \<Rightarrow> nat"
-where
- "pred 0 = 0"
-| "pred (Suc n) = n"
-
-thm pred.elims
-
-lemma
- assumes "pred x = y"
- obtains "x = 0" "y = 0" | "n" where "x = Suc n" "y = n"
- by (fact pred.elims[OF assms])
-
-
-text \<open>If the predecessor of a number is 0, that number must be 0 or 1.\<close>
-
-fun_cases pred0E[elim]: "pred n = 0"
-
-lemma "pred n = 0 \<Longrightarrow> n = 0 \<or> n = Suc 0"
- by (erule pred0E) metis+
-
-text \<open>
- Other expressions on the right-hand side also work, but whether the
- generated rule is useful depends on how well the simplifier can
- simplify it. This example works well:
-\<close>
-
-fun_cases pred42E[elim]: "pred n = 42"
-
-lemma "pred n = 42 \<Longrightarrow> n = 43"
- by (erule pred42E)
-
-
-subsubsection \<open>List to option\<close>
-
-fun list_to_option :: "'a list \<Rightarrow> 'a option"
-where
- "list_to_option [x] = Some x"
-| "list_to_option _ = None"
-
-fun_cases list_to_option_NoneE: "list_to_option xs = None"
- and list_to_option_SomeE: "list_to_option xs = Some x"
-
-lemma "list_to_option xs = Some y \<Longrightarrow> xs = [y]"
- by (erule list_to_option_SomeE)
-
-
-subsubsection \<open>Boolean Functions\<close>
-
-fun xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
-where
- "xor False False = False"
-| "xor True True = False"
-| "xor _ _ = True"
-
-thm xor.elims
-
-text \<open>
- \<open>fun_cases\<close> does not only recognise function equations, but also works with
- functions that return a boolean, e.g.:
-\<close>
-
-fun_cases xor_TrueE: "xor a b" and xor_FalseE: "\<not>xor a b"
-print_theorems
-
-
-subsubsection \<open>Many parameters\<close>
-
-fun sum4 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
- where "sum4 a b c d = a + b + c + d"
-
-fun_cases sum40E: "sum4 a b c d = 0"
-
-lemma "sum4 a b c d = 0 \<Longrightarrow> a = 0"
- by (erule sum40E)
-
-
-subsection \<open>Partial Function Definitions\<close>
-
-text \<open>Partial functions in the option monad:\<close>
-
-partial_function (option)
- collatz :: "nat \<Rightarrow> nat list option"
-where
- "collatz n =
- (if n \<le> 1 then Some [n]
- else if even n
- then do { ns \<leftarrow> collatz (n div 2); Some (n # ns) }
- else do { ns \<leftarrow> collatz (3 * n + 1); Some (n # ns)})"
-
-declare collatz.simps[code]
-value "collatz 23"
-
-
-text \<open>Tail-recursive functions:\<close>
-
-partial_function (tailrec) fixpoint :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
-where
- "fixpoint f x = (if f x = x then x else fixpoint f (f x))"
-
-
-subsection \<open>Regression tests\<close>
-
-text \<open>
- The following examples mainly serve as tests for the
- function package.
-\<close>
-
-fun listlen :: "'a list \<Rightarrow> nat"
-where
- "listlen [] = 0"
-| "listlen (x#xs) = Suc (listlen xs)"
-
-
-subsubsection \<open>Context recursion\<close>
-
-fun f :: "nat \<Rightarrow> nat"
-where
- zero: "f 0 = 0"
-| succ: "f (Suc n) = (if f n = 0 then 0 else f n)"
-
-
-subsubsection \<open>A combination of context and nested recursion\<close>
-
-function h :: "nat \<Rightarrow> nat"
-where
- "h 0 = 0"
-| "h (Suc n) = (if h n = 0 then h (h n) else h n)"
-by pat_completeness auto
-
-
-subsubsection \<open>Context, but no recursive call\<close>
-
-fun i :: "nat \<Rightarrow> nat"
-where
- "i 0 = 0"
-| "i (Suc n) = (if n = 0 then 0 else i n)"
-
-
-subsubsection \<open>Tupled nested recursion\<close>
-
-fun fa :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-where
- "fa 0 y = 0"
-| "fa (Suc n) y = (if fa n y = 0 then 0 else fa n y)"
-
-
-subsubsection \<open>Let\<close>
-
-fun j :: "nat \<Rightarrow> nat"
-where
- "j 0 = 0"
-| "j (Suc n) = (let u = n in Suc (j u))"
-
-
-text \<open>There were some problems with fresh names \dots\<close>
-function k :: "nat \<Rightarrow> nat"
-where
- "k x = (let a = x; b = x in k x)"
- by pat_completeness auto
-
-
-function f2 :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
-where
- "f2 p = (let (x,y) = p in f2 (y,x))"
- by pat_completeness auto
-
-
-subsubsection \<open>Abbreviations\<close>
-
-fun f3 :: "'a set \<Rightarrow> bool"
-where
- "f3 x = finite x"
-
-
-subsubsection \<open>Simple Higher-Order Recursion\<close>
-
-datatype 'a tree = Leaf 'a | Branch "'a tree list"
-
-fun treemap :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a tree \<Rightarrow> 'a tree"
-where
- "treemap fn (Leaf n) = (Leaf (fn n))"
-| "treemap fn (Branch l) = (Branch (map (treemap fn) l))"
-
-fun tinc :: "nat tree \<Rightarrow> nat tree"
-where
- "tinc (Leaf n) = Leaf (Suc n)"
-| "tinc (Branch l) = Branch (map tinc l)"
-
-fun testcase :: "'a tree \<Rightarrow> 'a list"
-where
- "testcase (Leaf a) = [a]"
-| "testcase (Branch x) =
- (let xs = concat (map testcase x);
- ys = concat (map testcase x) in
- xs @ ys)"
-
-
-subsubsection \<open>Pattern matching on records\<close>
-
-record point =
- Xcoord :: int
- Ycoord :: int
-
-function swp :: "point \<Rightarrow> point"
-where
- "swp \<lparr> Xcoord = x, Ycoord = y \<rparr> = \<lparr> Xcoord = y, Ycoord = x \<rparr>"
-proof -
- fix P x
- assume "\<And>xa y. x = \<lparr>Xcoord = xa, Ycoord = y\<rparr> \<Longrightarrow> P"
- then show P by (cases x)
-qed auto
-termination by rule auto
-
-
-subsubsection \<open>The diagonal function\<close>
-
-fun diag :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> nat"
-where
- "diag x True False = 1"
-| "diag False y True = 2"
-| "diag True False z = 3"
-| "diag True True True = 4"
-| "diag False False False = 5"
-
-
-subsubsection \<open>Many equations (quadratic blowup)\<close>
-
-datatype DT =
- A | B | C | D | E | F | G | H | I | J | K | L | M | N | P
-| Q | R | S | T | U | V
-
-fun big :: "DT \<Rightarrow> nat"
-where
- "big A = 0"
-| "big B = 0"
-| "big C = 0"
-| "big D = 0"
-| "big E = 0"
-| "big F = 0"
-| "big G = 0"
-| "big H = 0"
-| "big I = 0"
-| "big J = 0"
-| "big K = 0"
-| "big L = 0"
-| "big M = 0"
-| "big N = 0"
-| "big P = 0"
-| "big Q = 0"
-| "big R = 0"
-| "big S = 0"
-| "big T = 0"
-| "big U = 0"
-| "big V = 0"
-
-
-subsubsection \<open>Automatic pattern splitting\<close>
-
-fun f4 :: "nat \<Rightarrow> nat \<Rightarrow> bool"
-where
- "f4 0 0 = True"
-| "f4 _ _ = False"
-
-
-subsubsection \<open>Polymorphic partial-function\<close>
-
-partial_function (option) f5 :: "'a list \<Rightarrow> 'a option"
-where
- "f5 x = f5 x"
-
-end
--- a/src/Tools/ROOT Wed Aug 25 22:16:27 2021 +0200
+++ b/src/Tools/ROOT Wed Aug 25 22:17:38 2021 +0200
@@ -4,6 +4,11 @@
theories
Code_Generator
+session Spec_Check in Spec_Check = Pure +
+ theories
+ Spec_Check
+ Examples
+
session SML in SML = Pure +
theories
Examples
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/Examples.thy Wed Aug 25 22:17:38 2021 +0200
@@ -0,0 +1,83 @@
+theory Examples
+imports Spec_Check
+begin
+
+section \<open>List examples\<close>
+
+ML_command \<open>
+check_property "ALL xs. rev xs = xs";
+\<close>
+
+ML_command \<open>
+check_property "ALL xs. rev (rev xs) = xs";
+\<close>
+
+
+section \<open>AList Specification\<close>
+
+ML_command \<open>
+(* map_entry applies the function to the element *)
+check_property "ALL k f xs. AList.lookup (op =) (AList.map_entry (op =) k f xs) k = Option.map f (AList.lookup (op =) xs k)";
+\<close>
+
+ML_command \<open>
+(* update always results in an entry *)
+check_property "ALL k v xs. AList.defined (op =) (AList.update (op =) (k, v) xs) k";
+\<close>
+
+ML_command \<open>
+(* update always writes the value *)
+check_property "ALL k v xs. AList.lookup (op =) (AList.update (op =) (k, v) xs) k = SOME v";
+\<close>
+
+ML_command \<open>
+(* default always results in an entry *)
+check_property "ALL k v xs. AList.defined (op =) (AList.default (op =) (k, v) xs) k";
+\<close>
+
+ML_command \<open>
+(* delete always removes the entry *)
+check_property "ALL k xs. not (AList.defined (op =) (AList.delete (op =) k xs) k)";
+\<close>
+
+ML_command \<open>
+(* default writes the entry iff it didn't exist *)
+check_property "ALL k v xs. (AList.lookup (op =) (AList.default (op =) (k, v) xs) k = (if AList.defined (op =) xs k then AList.lookup (op =) xs k else SOME v))";
+\<close>
+
+section \<open>Examples on Types and Terms\<close>
+
+ML_command \<open>
+check_property "ALL f g t. map_types (g o f) t = (map_types f o map_types g) t";
+\<close>
+
+ML_command \<open>
+check_property "ALL f g t. map_types (f o g) t = (map_types f o map_types g) t";
+\<close>
+
+
+text \<open>One would think this holds:\<close>
+
+ML_command \<open>
+check_property "ALL t ts. strip_comb (list_comb (t, ts)) = (t, ts)"
+\<close>
+
+text \<open>But it only holds with this precondition:\<close>
+
+ML_command \<open>
+check_property "ALL t ts. case t of _ $ _ => true | _ => strip_comb (list_comb (t, ts)) = (t, ts)"
+\<close>
+
+section \<open>Some surprises\<close>
+
+ML_command \<open>
+check_property "ALL Ts t. type_of1 (Ts, t) = fastype_of1 (Ts, t)"
+\<close>
+
+
+ML_command \<open>
+val thy = \<^theory>;
+check_property "ALL t u. if Pattern.matches thy (t, u) then Term.could_unify (t, u) else true"
+\<close>
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/README Wed Aug 25 22:17:38 2021 +0200
@@ -0,0 +1,47 @@
+This is a Quickcheck tool for Isabelle/ML.
+
+Authors
+
+ Lukas Bulwahn
+ Nicolai Schaffroth
+
+Quick Usage
+
+ - Import Spec_Check.thy in your development
+ - Look at examples in Examples.thy
+ - write specifications with the ML invocation
+ check_property "ALL x. P x"
+
+Notes
+
+Our specification-based testing tool originated from Christopher League's
+QCheck tool for SML (cf. https://github.com/league/qcheck). As Isabelle
+provides a rich and uniform ML platform (called Isabelle/ML), this
+testing tools is very different than the one for a typical ML developer.
+
+1. Isabelle/ML provides common data structures, which we can use in the
+tool's implementation for storing data and printing output.
+
+2. The implementation in Isabelle that will be checked with this tool
+commonly use Isabelle/ML's int type (which corresponds ML's IntInf.int),
+but they do not use other integer types in ML, such as ML's Int.int,
+Word.word and others.
+
+3. As Isabelle can run heavily in parallel, we avoid reference types.
+
+4. Isabelle has special naming conventions and documentation of source
+code is only minimal to avoid parroting.
+
+Next steps:
+ - Remove all references and store the neccessary random seed in the
+ Isabelle's context.
+ - Simplify some existing random generators.
+ The original ones from Christopher League are so complicated to
+ support many integer types uniformly.
+
+License
+
+ The source code originated from Christopher League's QCheck, which is
+ licensed under the 2-clause BSD license. The current source code is
+ licensed under the compatible 3-clause BSD license of Isabelle.
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/Spec_Check.thy Wed Aug 25 22:17:38 2021 +0200
@@ -0,0 +1,13 @@
+theory Spec_Check
+imports Pure
+begin
+
+ML_file \<open>random.ML\<close>
+ML_file \<open>property.ML\<close>
+ML_file \<open>base_generator.ML\<close>
+ML_file \<open>generator.ML\<close>
+ML_file \<open>gen_construction.ML\<close>
+ML_file \<open>spec_check.ML\<close>
+ML_file \<open>output_style.ML\<close>
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/base_generator.ML Wed Aug 25 22:17:38 2021 +0200
@@ -0,0 +1,201 @@
+(* Title: Tools/Spec_Check/base_generator.ML
+ Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
+ Author: Christopher League
+
+Basic random generators.
+*)
+
+signature BASE_GENERATOR =
+sig
+
+type rand
+type 'a gen = rand -> 'a * rand
+type ('a, 'b) co = 'a -> 'b gen -> 'b gen
+
+val new : unit -> rand
+val range : int * int -> rand -> int * rand
+type ('a, 'b) reader = 'b -> ('a * 'b) option
+
+val lift : 'a -> 'a gen
+val select : 'a vector -> 'a gen
+val choose : 'a gen vector -> 'a gen
+val choose' : (int * 'a gen) vector -> 'a gen
+val selectL : 'a list -> 'a gen
+val chooseL : 'a gen list -> 'a gen
+val chooseL' : (int * 'a gen) list -> 'a gen
+val filter : ('a -> bool) -> 'a gen -> 'a gen
+
+val zip : ('a gen * 'b gen) -> ('a * 'b) gen
+val zip3 : ('a gen * 'b gen * 'c gen) -> ('a * 'b * 'c) gen
+val zip4 : ('a gen * 'b gen * 'c gen * 'd gen) -> ('a * 'b * 'c * 'd) gen
+val map : ('a -> 'b) -> 'a gen -> 'b gen
+val map2 : ('a * 'b -> 'c) -> ('a gen * 'b gen) -> 'c gen
+val map3 : ('a * 'b * 'c -> 'd) -> ('a gen * 'b gen * 'c gen) -> 'd gen
+val map4 : ('a * 'b * 'c * 'd -> 'e) -> ('a gen * 'b gen * 'c gen * 'd gen) -> 'e gen
+
+val flip : bool gen
+val flip' : int * int -> bool gen
+
+val list : bool gen -> 'a gen -> 'a list gen
+val option : bool gen -> 'a gen -> 'a option gen
+val vector : (int * (int -> 'a) -> 'b) -> int gen * 'a gen -> 'b gen
+
+val variant : (int, 'b) co
+val arrow : ('a, 'b) co * 'b gen -> ('a -> 'b) gen
+val cobool : (bool, 'b) co
+val colist : ('a, 'b) co -> ('a list, 'b) co
+val coopt : ('a, 'b) co -> ('a option, 'b) co
+
+type stream
+val start : rand -> stream
+val limit : int -> 'a gen -> ('a, stream) reader
+
+end
+
+structure Base_Generator : BASE_GENERATOR =
+struct
+
+(* random number engine *)
+
+type rand = real
+
+val a = 16807.0
+val m = 2147483647.0
+
+fun nextrand seed =
+ let
+ val t = a * seed
+ in
+ t - m * real (floor (t / m))
+ end
+
+val new = nextrand o Time.toReal o Time.now
+
+fun range (min, max) =
+ if min > max then raise Domain (* TODO: raise its own error *)
+ else fn r => (min + (floor (real (max - min + 1) * r / m)), nextrand r)
+
+fun split r =
+ let
+ val r = r / a
+ val r0 = real (floor r)
+ val r1 = r - r0
+ in
+ (nextrand r0, nextrand r1)
+ end
+
+(* generators *)
+
+type 'a gen = rand -> 'a * rand
+type ('a, 'b) reader = 'b -> ('a * 'b) option
+
+fun lift obj r = (obj, r)
+
+local (* Isabelle does not use vectors? *)
+ fun explode ((freq, gen), acc) =
+ List.tabulate (freq, fn _ => gen) @ acc
+in
+ fun choose v r =
+ let val (i, r) = range(0, Vector.length v - 1) r
+ in Vector.sub (v, i) r end
+ fun choose' v = choose (Vector.fromList (Vector.foldr explode [] v))
+ fun select v = choose (Vector.map lift v)
+end
+
+fun chooseL l = choose (Vector.fromList l)
+fun chooseL' l = choose' (Vector.fromList l)
+fun selectL l = select (Vector.fromList l)
+
+fun zip (g1, g2) = g1 #-> (fn x1 => g2 #-> (fn x2 => pair (x1, x2)))
+
+fun zip3 (g1, g2, g3) =
+ zip (g1, zip (g2, g3)) #-> (fn (x1, (x2, x3)) => pair (x1, x2, x3))
+
+fun zip4 (g1, g2, g3, g4) =
+ zip (zip (g1, g2), zip (g3, g4)) #-> (fn ((x1, x2), (x3, x4)) => pair (x1, x2, x3, x4))
+
+fun map f g = apfst f o g
+
+fun map2 f = map f o zip
+fun map3 f = map f o zip3
+fun map4 f = map f o zip4
+
+fun filter p gen r =
+ let
+ fun loop (x, r) = if p x then (x, r) else loop (gen r)
+ in
+ loop (gen r)
+ end
+
+val flip = selectL [true, false]
+fun flip' (p, q) = chooseL' [(p, lift true), (q, lift false)]
+
+fun list flip g r =
+ case flip r of
+ (true, r) => ([], r)
+ | (false, r) =>
+ let
+ val (x,r) = g r
+ val (xs,r) = list flip g r
+ in (x::xs, r) end
+
+fun option flip g r =
+ case flip r of
+ (true, r) => (NONE, r)
+ | (false, r) => map SOME g r
+
+fun vector tabulate (int, elem) r =
+ let
+ val (n, r) = int r
+ val p = Unsynchronized.ref r
+ fun g _ =
+ let
+ val (x,r) = elem(!p)
+ in x before p := r end
+ in
+ (tabulate(n, g), !p)
+ end
+
+type stream = rand Unsynchronized.ref * int
+
+fun start r = (Unsynchronized.ref r, 0)
+
+fun limit max gen =
+ let
+ fun next (p, i) =
+ if i >= max then NONE
+ else
+ let val (x, r) = gen(!p)
+ in SOME(x, (p, i+1)) before p := r end
+ in
+ next
+ end
+
+type ('a, 'b) co = 'a -> 'b gen -> 'b gen
+
+fun variant v g r =
+ let
+ fun nth (i, r) =
+ let val (r1, r2) = split r
+ in if i = 0 then r1 else nth (i-1, r2) end
+ in
+ g (nth (v, r))
+ end
+
+fun arrow (cogen, gen) r =
+ let
+ val (r1, r2) = split r
+ fun g x = fst (cogen x gen r1)
+ in (g, r2) end
+
+fun cobool false = variant 0
+ | cobool true = variant 1
+
+fun colist _ [] = variant 0
+ | colist co (x::xs) = variant 1 o co x o colist co xs
+
+fun coopt _ NONE = variant 0
+ | coopt co (SOME x) = variant 1 o co x
+
+end
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/gen_construction.ML Wed Aug 25 22:17:38 2021 +0200
@@ -0,0 +1,179 @@
+(* Title: Tools/Spec_Check/gen_construction.ML
+ Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
+ Author: Christopher League
+
+Constructing generators and pretty printing function for complex types.
+*)
+
+signature GEN_CONSTRUCTION =
+sig
+ val register : string * (string * string) -> theory -> theory
+ type mltype
+ val parse_pred : string -> string * mltype
+ val build_check : Proof.context -> string -> mltype * string -> string
+ (*val safe_check : string -> mltype * string -> string*)
+ val string_of_bool : bool -> string
+ val string_of_ref : ('a -> string) -> 'a Unsynchronized.ref -> string
+end;
+
+structure Gen_Construction : GEN_CONSTRUCTION =
+struct
+
+(* Parsing ML types *)
+
+datatype mltype = Var | Con of string * mltype list | Tuple of mltype list;
+
+(*Split string into tokens for parsing*)
+fun split s =
+ let
+ fun split_symbol #"(" = "( "
+ | split_symbol #")" = " )"
+ | split_symbol #"," = " ,"
+ | split_symbol #":" = " :"
+ | split_symbol c = Char.toString c
+ fun is_space c = c = #" "
+ in String.tokens is_space (String.translate split_symbol s) end;
+
+(*Accept anything that is not a recognized symbol*)
+val scan_name = Scan.one (fn s => not (String.isSubstring s "(),*->;"));
+
+(*Turn a type list into a nested Con*)
+fun make_con [] = raise Empty
+ | make_con [c] = c
+ | make_con (Con (s, _) :: cl) = Con (s, [make_con cl]);
+
+(*Parse a type*)
+fun parse_type s = (parse_fun || parse_tuple || parse_type_single) s
+
+and parse_type_arg s = (parse_tuple || parse_type_single) s
+
+and parse_type_single s = (parse_con || parse_type_basic) s
+
+and parse_type_basic s = (parse_var || $$ "(" |-- parse_type --| $$ ")") s
+
+and parse_list s =
+ ($$ "(" |-- parse_type -- Scan.repeat1 ($$ "," |-- parse_type) --| $$ ")" >> op::) s
+
+and parse_var s = (Scan.one (String.isPrefix "'") >> (fn _ => Var)) s
+
+and parse_con s = ((parse_con_nest
+ || parse_type_basic -- parse_con_nest >> (fn (b, Con (t, _) :: tl) => Con (t, [b]) :: tl)
+ || parse_list -- parse_con_nest >> (fn (l, Con (t, _) :: tl) => Con (t, l) :: tl))
+ >> (make_con o rev)) s
+
+and parse_con_nest s = Scan.unless parse_var (Scan.repeat1 (scan_name >> (fn t => Con (t, [])))) s
+
+and parse_fun s = (parse_type_arg -- $$ "->" -- parse_type >> (fn ((a, f), r) => Con (f, [a, r]))) s
+
+and parse_tuple s = (parse_type_single -- Scan.repeat1 ($$ "*" |-- parse_type_single)
+ >> (fn (t, tl) => Tuple (t :: tl))) s;
+
+(*Parse entire type + name*)
+fun parse_function s =
+ let
+ val p = $$ "val" |-- scan_name --| ($$ "=" -- $$ "fn" -- $$ ":")
+ val (name, ty) = p (split s)
+ val stop = Scan.stopper (fn _ => ";") (fn s => s = ";");
+ val (typ, _) = Scan.finite stop parse_type ty
+ in (name, typ) end;
+
+(*Create desired output*)
+fun parse_pred s =
+ let
+ val (name, Con ("->", t :: _)) = parse_function s
+ in (name, t) end;
+
+(* Construct Generators and Pretty Printers *)
+
+(*copied from smt_config.ML *)
+fun string_of_bool b = if b then "true" else "false"
+
+fun string_of_ref f r = f (!r) ^ " ref";
+
+val initial_content = Symtab.make
+ [("bool", ("Generator.flip", "Gen_Construction.string_of_bool")),
+ ("option", ("Generator.option (Generator.flip' (1, 3))", "ML_Syntax.print_option")),
+ ("list", ("Generator.list (Generator.flip' (1, 3))", "ML_Syntax.print_list")),
+ ("unit", ("gen_unit", "fn () => \"()\"")),
+ ("int", ("Generator.int", "string_of_int")),
+ ("real", ("Generator.real", "string_of_real")),
+ ("char", ("Generator.char", "fn c => \"#'\" ^ (Char.toString c) ^ \"'\"")),
+ ("string", ("Generator.string (Generator.range (0, 100), Generator.char)", "ML_Syntax.print_string")),
+ ("->", ("Generator.function_lazy", "fn (_, _) => fn _ => \"fn\"")),
+ ("typ", ("Generator.typ 10", "ML_Syntax.print_typ")),
+ ("term", ("Generator.term 10", "ML_Syntax.print_term"))]
+
+structure Data = Theory_Data
+(
+ type T = (string * string) Symtab.table
+ val empty = initial_content
+ val extend = I
+ fun merge data : T = Symtab.merge (K true) data
+)
+
+fun data_of ctxt tycon =
+ (case Symtab.lookup (Data.get (Proof_Context.theory_of ctxt)) tycon of
+ SOME data => data
+ | NONE => error ("No generator and printer defined for ML type constructor " ^ quote tycon))
+
+val generator_of = fst oo data_of
+val printer_of = snd oo data_of
+
+fun register (ty, data) = Data.map (Symtab.update (ty, data))
+
+(*
+fun remove_gen ty = gen_table := AList.delete (op =) ty (!gen_table);
+*)
+
+fun combine dict [] = dict
+ | combine dict dicts = enclose "(" ")" dict ^ " " ^ enclose "(" ")" (commas dicts)
+
+fun compose_generator _ Var = "Generator.int"
+ | compose_generator ctxt (Con (s, types)) =
+ combine (generator_of ctxt s) (map (compose_generator ctxt) types)
+ | compose_generator ctxt (Tuple t) =
+ let
+ fun tuple_body t = space_implode ""
+ (map (fn (ty, n) => "val (x" ^ string_of_int n ^ ", r" ^ string_of_int n ^ ") = " ^
+ compose_generator ctxt ty ^ " r" ^ string_of_int (n - 1) ^ " ") (t ~~ (1 upto (length t))))
+ fun tuple_ret a = commas (map (fn n => "x" ^ string_of_int n) (1 upto a))
+ in
+ "fn r0 => let " ^ tuple_body t ^
+ "in ((" ^ tuple_ret (length t) ^ "), r" ^ string_of_int (length t) ^ ") end"
+ end;
+
+fun compose_printer _ Var = "Int.toString"
+ | compose_printer ctxt (Con (s, types)) =
+ combine (printer_of ctxt s) (map (compose_printer ctxt) types)
+ | compose_printer ctxt (Tuple t) =
+ let
+ fun tuple_head a = commas (map (fn n => "x" ^ string_of_int n) (1 upto a))
+ fun tuple_body t = space_implode " ^ \", \" ^ "
+ (map (fn (ty, n) => "(" ^ compose_printer ctxt ty ^ ") x" ^ string_of_int n)
+ (t ~~ (1 upto (length t))))
+ in "fn (" ^ tuple_head (length t) ^ ") => \"(\" ^ " ^ tuple_body t ^ " ^ \")\"" end;
+
+(*produce compilable string*)
+fun build_check ctxt name (ty, spec) =
+ "Spec_Check.checkGen (Context.the_local_context ()) ("
+ ^ compose_generator ctxt ty ^ ", SOME (" ^ compose_printer ctxt ty ^ ")) (\""
+ ^ name ^ "\", Property.pred (" ^ spec ^ "));";
+
+(*produce compilable string - non-eqtype functions*)
+(*
+fun safe_check name (ty, spec) =
+ let
+ val default =
+ (case AList.lookup (op =) (!gen_table) "->" of
+ NONE => ("gen_function_rand", "fn (_, _) => fn _ => \"fn\"")
+ | SOME entry => entry)
+ in
+ (gen_table :=
+ AList.update (op =) ("->", ("gen_function_safe", "fn (_, _) => fn _ => \"fn\"")) (!gen_table);
+ build_check name (ty, spec) before
+ gen_table := AList.update (op =) ("->", default) (!gen_table))
+ end;
+*)
+
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/generator.ML Wed Aug 25 22:17:38 2021 +0200
@@ -0,0 +1,235 @@
+(* Title: Tools/Spec_Check/generator.ML
+ Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
+ Author: Christopher League
+
+Random generators for Isabelle/ML's types.
+*)
+
+signature GENERATOR = sig
+ include BASE_GENERATOR
+ (* text generators *)
+ val char : char gen
+ val charRange : char * char -> char gen
+ val charFrom : string -> char gen
+ val charByType : (char -> bool) -> char gen
+ val string : (int gen * char gen) -> string gen
+ val substring : string gen -> substring gen
+ val cochar : (char, 'b) co
+ val costring : (string, 'b) co
+ val cosubstring : (substring, 'b) co
+ (* integer generators *)
+ val int : int gen
+ val int_pos : int gen
+ val int_neg : int gen
+ val int_nonpos : int gen
+ val int_nonneg : int gen
+ val coint : (int, 'b) co
+ (* real generators *)
+ val real : real gen
+ val real_frac : real gen
+ val real_pos : real gen
+ val real_neg : real gen
+ val real_nonpos : real gen
+ val real_nonneg : real gen
+ val real_finite : real gen
+ (* function generators *)
+ val function_const : 'c * 'b gen -> ('a -> 'b) gen
+ val function_strict : int -> ''a gen * 'b gen -> (''a -> 'b) gen
+ val function_lazy : ''a gen * 'b gen -> (''a -> 'b) gen
+ val unit : unit gen
+ val ref' : 'a gen -> 'a Unsynchronized.ref gen
+ (* more generators *)
+ val term : int -> term gen
+ val typ : int -> typ gen
+
+ val stream : stream
+end
+
+structure Generator : GENERATOR =
+struct
+
+open Base_Generator
+
+val stream = start (new())
+
+type 'a gen = rand -> 'a * rand
+type ('a, 'b) co = 'a -> 'b gen -> 'b gen
+
+(* text *)
+
+type char = Char.char
+type string = String.string
+type substring = Substring.substring
+
+
+val char = map Char.chr (range (0, Char.maxOrd))
+fun charRange (lo, hi) = map Char.chr (range (Char.ord lo, Char.ord hi))
+
+fun charFrom s =
+ choose (Vector.tabulate (String.size s, fn i => lift (String.sub (s, i))))
+
+fun charByType p = filter p char
+
+val string = vector CharVector.tabulate
+
+fun substring gen r =
+ let
+ val (s, r') = gen r
+ val (i, r'') = range (0, String.size s) r'
+ val (j, r''') = range (0, String.size s - i) r''
+ in
+ (Substring.substring (s, i, j), r''')
+ end
+
+fun cochar c =
+ if Char.ord c = 0 then variant 0
+ else variant 1 o cochar (Char.chr (Char.ord c div 2))
+
+fun cosubstring s = Substring.foldr (fn (c,v) => cochar c o v) (variant 0) s
+
+fun costring s = cosubstring (Substring.full s)
+
+(* integers *)
+val digit = charRange (#"0", #"9")
+val nonzero = string (lift 1, charRange (#"1", #"9"))
+fun digits' n = string (range (0, n-1), digit)
+fun digits n = map2 op^ (nonzero, digits' n)
+
+val maxDigits = 64
+val ratio = 49
+
+fun pos_or_neg f r =
+ let
+ val (s, r') = digits maxDigits r
+ in (f (the (Int.fromString s)), r') end
+
+val int_pos = pos_or_neg I
+val int_neg = pos_or_neg Int.~
+val zero = lift 0
+
+val int_nonneg = chooseL' [(1, zero), (ratio, int_pos)]
+val int_nonpos = chooseL' [(1, zero), (ratio, int_neg)]
+val int = chooseL [int_nonneg, int_nonpos]
+
+fun coint n =
+ if n = 0 then variant 0
+ else if n < 0 then variant 1 o coint (~ n)
+ else variant 2 o coint (n div 2)
+
+(* reals *)
+val digits = string (range(1, Real.precision), charRange(#"0", #"9"))
+
+fun real_frac r =
+ let val (s, r') = digits r
+ in (the (Real.fromString s), r') end
+
+val {exp=minExp,...} = Real.toManExp Real.minPos
+val {exp=maxExp,...} = Real.toManExp Real.posInf
+
+val ratio = 99
+
+fun mk r =
+ let
+ val (a, r') = digits r
+ val (b, r'') = digits r'
+ val (e, r''') = range (minExp div 4, maxExp div 4) r''
+ val x = String.concat [a, ".", b, "E", Int.toString e]
+ in
+ (the (Real.fromString x), r''')
+ end
+
+val real_pos = chooseL' (List.map ((pair 1) o lift)
+ [Real.posInf, Real.maxFinite, Real.minPos, Real.minNormalPos] @ [(ratio, mk)])
+
+val real_neg = map Real.~ real_pos
+
+val real_zero = Real.fromInt 0
+val real_nonneg = chooseL' [(1, lift real_zero), (ratio, real_pos)]
+val real_nonpos = chooseL' [(1, lift real_zero), (ratio, real_neg)]
+
+val real = chooseL [real_nonneg, real_nonpos]
+
+val real_finite = filter Real.isFinite real
+
+(*alternate list generator - uses an integer generator to determine list length*)
+fun list' int gen = vector List.tabulate (int, gen);
+
+(* more function generators *)
+
+fun function_const (_, gen2) r =
+ let
+ val (v, r') = gen2 r
+ in (fn _ => v, r') end;
+
+fun function_strict size (gen1, gen2) r =
+ let
+ val (def, r') = gen2 r
+ val (table, r'') = list' (fn s => (size, s)) (zip (gen1, gen2)) r'
+ in (fn v1 => the_default def (AList.lookup (op =) table v1), r'') end;
+
+fun function_lazy (gen1, gen2) r =
+ let
+ val (initial1, r') = gen1 r
+ val (initial2, internal) = gen2 r'
+ val seed = Unsynchronized.ref internal
+ val table = Unsynchronized.ref [(initial1, initial2)]
+ fun new_entry k =
+ let
+ val (new_val, new_seed) = gen2 (!seed)
+ val _ = seed := new_seed
+ val _ = table := AList.update (op =) (k, new_val) (!table)
+ in new_val end
+ in
+ (fn v1 =>
+ case AList.lookup (op =) (!table) v1 of
+ NONE => new_entry v1
+ | SOME v2 => v2, r')
+ end;
+
+(* unit *)
+
+fun unit r = ((), r);
+
+(* references *)
+
+fun ref' gen r =
+ let val (value, r') = gen r
+ in (Unsynchronized.ref value, r') end;
+
+(* types and terms *)
+
+val sort_string = selectL ["sort1", "sort2", "sort3"];
+val type_string = selectL ["TCon1", "TCon2", "TCon3"];
+val tvar_string = selectL ["a", "b", "c"];
+
+val const_string = selectL ["c1", "c2", "c3"];
+val var_string = selectL ["x", "y", "z"];
+val index = selectL [0, 1, 2, 3];
+val bound_index = selectL [0, 1, 2, 3];
+
+val sort = list (flip' (1, 2)) sort_string;
+
+fun typ n =
+ let
+ fun type' m = map Type (zip (type_string, list (flip' (1, 3)) (typ m)))
+ val tfree = map TFree (zip (tvar_string, sort))
+ val tvar = map TVar (zip (zip (tvar_string, index), sort))
+ in
+ if n = 0 then chooseL [tfree, tvar]
+ else chooseL [type' (n div 2), tfree, tvar]
+ end;
+
+fun term n =
+ let
+ val const = map Const (zip (const_string, typ 10))
+ val free = map Free (zip (var_string, typ 10))
+ val var = map Var (zip (zip (var_string, index), typ 10))
+ val bound = map Bound bound_index
+ fun abs m = map Abs (zip3 (var_string, typ 10, term m))
+ fun app m = map (op $) (zip (term m, term m))
+ in
+ if n = 0 then chooseL [const, free, var, bound]
+ else chooseL [const, free, var, bound, abs (n - 1), app (n div 2)]
+ end;
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/output_style.ML Wed Aug 25 22:17:38 2021 +0200
@@ -0,0 +1,113 @@
+(* Title: Tools/Spec_Check/output_style.ML
+ Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
+ Author: Christopher League
+
+Output styles for presenting Spec_Check's results.
+*)
+
+structure Output_Style : sig end =
+struct
+
+(* perl style *)
+
+val perl_style =
+ Spec_Check.register_style "Perl"
+ (fn ctxt => fn tag =>
+ let
+ val target = Config.get ctxt Spec_Check.gen_target
+ val namew = Config.get ctxt Spec_Check.column_width
+ val sort_examples = Config.get ctxt Spec_Check.sort_examples
+ val show_stats = Config.get ctxt Spec_Check.show_stats
+ val limit = Config.get ctxt Spec_Check.examples
+
+ val resultw = 8
+ val countw = 20
+ val allw = namew + resultw + countw + 2
+
+ val maybe_sort = if sort_examples then sort (int_ord o apply2 size) else I
+
+ fun result ({count = 0, ...}, _) _ = "dubious"
+ | result (_ : Property.stats, badobjs) false = if null badobjs then "ok" else "FAILED"
+ | result ({count, tags}, badobjs) true =
+ if not (null badobjs) then "FAILED"
+ else if AList.defined (op =) tags "__GEN" andalso count < target then "dubious"
+ else "ok"
+
+ fun ratio (0, _) = "(0/0 passed)"
+ | ratio (count, 0) = "(" ^ string_of_int count ^ " passed)"
+ | ratio (count, n) =
+ "(" ^ string_of_int (count - n) ^ "/" ^ string_of_int count ^ " passed)"
+
+ fun update (stats, badobjs) donep =
+ "\r" ^ StringCvt.padRight #"." namew tag ^ "." ^
+ StringCvt.padRight #" " resultw (result (stats, badobjs) donep) ^
+ StringCvt.padRight #" " countw (ratio (#count stats, length badobjs))
+
+ fun status (_, result, (stats, badobjs)) =
+ if Property.failure result then warning (update (stats, badobjs) false) else ()
+
+ fun prtag count (tag, n) first =
+ if String.isPrefix "__" tag then ("", first)
+ else
+ let
+ val ratio = round ((real n / real count) * 100.0)
+ in
+ (((if first then "" else StringCvt.padRight #" " allw "\n") ^
+ StringCvt.padLeft #" " 3 (string_of_int ratio) ^ "% " ^ tag),
+ false)
+ end
+
+ fun prtags ({count, tags} : Property.stats) =
+ if show_stats then cat_lines (fst (fold_map (prtag count) tags true)) else ""
+
+ fun err badobjs =
+ let
+ fun iter [] _ = ()
+ | iter (e :: es) k =
+ (warning (StringCvt.padLeft #" " namew (if k > 0 then "" else "counter-examples") ^
+ StringCvt.padRight #" " resultw (if k > 0 then "" else ":") ^ e);
+ iter es (k + 1))
+ in
+ iter (maybe_sort (take limit (map_filter I badobjs))) 0
+ end
+
+ fun finish (stats, badobjs) =
+ if null badobjs then writeln (update (stats, badobjs) true ^ prtags stats)
+ else (warning (update (stats, badobjs) true); err badobjs)
+ in
+ {status = status, finish = finish}
+ end)
+
+val _ = Theory.setup perl_style;
+
+
+(* CM style: meshes with CM output; highlighted in sml-mode *)
+
+val cm_style =
+ Spec_Check.register_style "CM"
+ (fn ctxt => fn tag =>
+ let
+ fun pad wd = StringCvt.padLeft #"0" wd o Int.toString
+ val gen_target = Config.get ctxt Spec_Check.gen_target
+ val _ = writeln ("[testing " ^ tag ^ "... ")
+ fun finish ({count, ...} : Property.stats, badobjs) =
+ (case (count, badobjs) of
+ (0, []) => warning ("no valid cases generated]")
+ | (n, []) => writeln (
+ if n >= gen_target then "ok]"
+ else "ok on " ^ string_of_int n ^ "; " ^ string_of_int gen_target ^ " required]")
+ | (_, es) =>
+ let
+ val wd = size (string_of_int (length es))
+ fun each (NONE, _) = ()
+ | each (SOME e, i) = warning (tag ^ ":" ^ pad wd i ^ ".0 Error: " ^ e)
+ in
+ (warning "FAILED]"; map each (es ~~ (1 upto (length es))); ())
+ end)
+ in
+ {status = K (), finish = finish}
+ end)
+
+val _ = Theory.setup cm_style;
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/property.ML Wed Aug 25 22:17:38 2021 +0200
@@ -0,0 +1,77 @@
+(* Title: Tools/Spec_Check/property.ML
+ Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
+ Author: Christopher League
+
+Conditional properties that can track argument distribution.
+*)
+
+signature PROPERTY =
+sig
+
+type 'a pred = 'a -> bool
+type 'a prop
+val pred : 'a pred -> 'a prop
+val pred2 : ('a * 'b) pred -> 'b -> 'a prop
+val implies : 'a pred * 'a prop -> 'a prop
+val ==> : 'a pred * 'a pred -> 'a prop
+val trivial : 'a pred -> 'a prop -> 'a prop
+val classify : 'a pred -> string -> 'a prop -> 'a prop
+val classify' : ('a -> string option) -> 'a prop -> 'a prop
+
+(*Results*)
+type result = bool option
+type stats = { tags : (string * int) list, count : int }
+val test : 'a prop -> 'a * stats -> result * stats
+val stats : stats
+val success : result pred
+val failure : result pred
+
+end
+
+structure Property : PROPERTY =
+struct
+
+type result = bool option
+type stats = { tags : (string * int) list, count : int }
+type 'a pred = 'a -> bool
+type 'a prop = 'a * stats -> result * stats
+
+fun success (SOME true) = true
+ | success _ = false
+
+fun failure (SOME false) = true
+ | failure _ = false
+
+fun apply f x = (case try f x of NONE => SOME false | some => some)
+fun pred f (x,s) = (apply f x, s)
+fun pred2 f z = pred (fn x => f (x, z))
+
+fun implies (cond, p) (x,s) = if cond x then p (x, s) else (NONE, s)
+
+fun ==> (p1, p2) = implies (p1, pred p2)
+
+fun wrap trans p (x,s) =
+ let val (result,s) = p (x,s)
+ in (result, trans (x, result, s)) end
+
+fun classify' f =
+ wrap (fn (x, result, {tags, count}) =>
+ { tags =
+ if is_some result then
+ (case f x of
+ NONE => tags
+ | SOME tag => AList.map_default (op =) (tag, 0) (fn c => c + 1) tags)
+ else tags,
+ count = count })
+
+fun classify p tag = classify' (fn x => if p x then SOME tag else NONE)
+
+fun trivial cond = classify cond "trivial"
+
+fun test p =
+ wrap (fn (_, result, {tags, count}) =>
+ { tags = tags, count = if is_some result then count + 1 else count }) p
+
+val stats = { tags = [], count = 0 }
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/random.ML Wed Aug 25 22:17:38 2021 +0200
@@ -0,0 +1,46 @@
+(* Title: Tools/Spec_Check/random.ML
+ Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
+ Author: Christopher League
+
+Random number engine.
+*)
+
+signature RANDOM =
+sig
+ type rand
+ val new : unit -> rand
+ val range : int * int -> rand -> int * rand
+ val split : rand -> rand * rand
+end
+
+structure Random : RANDOM =
+struct
+
+type rand = real
+
+val a = 16807.0
+val m = 2147483647.0
+
+fun nextrand seed =
+ let
+ val t = a * seed
+ in
+ t - m * real(floor(t/m))
+ end
+
+val new = nextrand o Time.toReal o Time.now
+
+fun range (min, max) =
+ if min > max then raise Domain (* TODO: raise its own error *)
+ else fn r => (min + (floor(real(max-min+1) * r / m)), nextrand r)
+
+fun split r =
+ let
+ val r = r / a
+ val r0 = real(floor r)
+ val r1 = r - r0
+ in
+ (nextrand r0, nextrand r1)
+ end
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/spec_check.ML Wed Aug 25 22:17:38 2021 +0200
@@ -0,0 +1,196 @@
+(* Title: Tools/Spec_Check/spec_check.ML
+ Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
+ Author: Christopher League
+
+Specification-based testing of ML programs with random values.
+*)
+
+signature SPEC_CHECK =
+sig
+ val gen_target : int Config.T
+ val gen_max : int Config.T
+ val examples : int Config.T
+ val sort_examples : bool Config.T
+ val show_stats : bool Config.T
+ val column_width : int Config.T
+ val style : string Config.T
+
+ type output_style = Proof.context -> string ->
+ {status : string option * Property.result * (Property.stats * string option list) -> unit,
+ finish: Property.stats * string option list -> unit}
+
+ val register_style : string -> output_style -> theory -> theory
+
+ val checkGen : Proof.context ->
+ 'a Generator.gen * ('a -> string) option -> string * 'a Property.prop -> unit
+
+ val check_property : Proof.context -> string -> unit
+end;
+
+structure Spec_Check : SPEC_CHECK =
+struct
+
+(* configurations *)
+
+val gen_target = Attrib.setup_config_int \<^binding>\<open>spec_check_gen_target\<close> (K 100)
+val gen_max = Attrib.setup_config_int \<^binding>\<open>spec_check_gen_max\<close> (K 400)
+val examples = Attrib.setup_config_int \<^binding>\<open>spec_check_examples\<close> (K 5)
+
+val sort_examples = Attrib.setup_config_bool \<^binding>\<open>spec_check_sort_examples\<close> (K true)
+val show_stats = Attrib.setup_config_bool \<^binding>\<open>spec_check_show_stats\<close> (K true)
+val column_width = Attrib.setup_config_int \<^binding>\<open>spec_check_column_width\<close> (K 22)
+val style = Attrib.setup_config_string \<^binding>\<open>spec_check_style\<close> (K "Perl")
+
+type ('a, 'b) reader = 'b -> ('a * 'b) option
+type 'a rep = ('a -> string) option
+
+type output_style = Proof.context -> string ->
+ {status: string option * Property.result * (Property.stats * string option list) -> unit,
+ finish: Property.stats * string option list -> unit}
+
+fun limit ctxt gen = Generator.limit (Config.get ctxt gen_max) gen
+
+structure Style = Theory_Data
+(
+ type T = output_style Symtab.table
+ val empty = Symtab.empty
+ val extend = I
+ fun merge data : T = Symtab.merge (K true) data
+)
+
+fun get_style ctxt =
+ let val name = Config.get ctxt style in
+ (case Symtab.lookup (Style.get (Proof_Context.theory_of ctxt)) name of
+ SOME style => style ctxt
+ | NONE => error ("No style called " ^ quote name ^ " found"))
+ end
+
+fun register_style name style = Style.map (Symtab.update (name, style))
+
+
+(* testing functions *)
+
+fun cpsCheck ctxt s0 shrink (next, show) (tag, prop) =
+ let
+ val apply_show = case show of NONE => (fn _ => NONE) | SOME f => SOME o f
+
+ val {status, finish} = get_style ctxt tag
+ fun status' (obj, result, (stats, badobjs)) =
+ let
+ val badobjs' = if Property.failure result then obj :: badobjs else badobjs
+ val _ = status (apply_show obj, result, (stats, map apply_show badobjs'))
+ in badobjs' end
+
+ fun try_shrink (obj, result, stats') (stats, badobjs) =
+ let
+ fun is_failure s =
+ let val (result, stats') = Property.test prop (s, stats)
+ in if Property.failure result then SOME (s, result, stats') else NONE end
+ in
+ case get_first is_failure (shrink obj) of
+ SOME (obj, result, stats') => try_shrink (obj, result, stats') (stats, badobjs)
+ | NONE => status' (obj, result, (stats', badobjs))
+ end
+
+ fun iter (NONE, (stats, badobjs)) = finish (stats, map apply_show badobjs)
+ | iter (SOME (obj, stream), (stats, badobjs)) =
+ if #count stats >= Config.get ctxt gen_target then
+ finish (stats, map apply_show badobjs)
+ else
+ let
+ val (result, stats') = Property.test prop (obj, stats)
+ val badobjs' = if Property.failure result then
+ try_shrink (obj, result, stats') (stats, badobjs)
+ else
+ status' (obj, result, (stats', badobjs))
+ in iter (next stream, (stats', badobjs')) end
+ in
+ fn stream => iter (next stream, (s0, []))
+ end
+
+fun check' ctxt s0 = cpsCheck ctxt s0 (fn _ => [])
+fun check ctxt = check' ctxt Property.stats
+fun checks ctxt = cpsCheck ctxt Property.stats
+
+fun checkGen ctxt (gen, show) (tag, prop) =
+ check' ctxt {count = 0, tags = [("__GEN", 0)]}
+ (limit ctxt gen, show) (tag, prop) Generator.stream
+
+fun checkGenShrink ctxt shrink (gen, show) (tag, prop) =
+ cpsCheck ctxt {count=0, tags=[("__GEN", 0)]} shrink
+ (limit ctxt gen, show) (tag, prop) Generator.stream
+
+fun checkOne ctxt show (tag, prop) obj =
+ check ctxt (List.getItem, show) (tag, prop) [obj]
+
+(*call the compiler and pass resulting type string to the parser*)
+fun determine_type ctxt s =
+ let
+ val return = Unsynchronized.ref "return"
+ val context : ML_Compiler0.context =
+ {name_space = #name_space ML_Env.context,
+ print_depth = SOME 1000000,
+ here = #here ML_Env.context,
+ print = fn r => return := r,
+ error = #error ML_Env.context}
+ val _ =
+ Context.setmp_generic_context (SOME (Context.Proof ctxt))
+ (fn () =>
+ ML_Compiler0.ML context
+ {line = 0, file = "generated code", verbose = true, debug = false} s) ()
+ in
+ Gen_Construction.parse_pred (! return)
+ end;
+
+(*call the compiler and run the test*)
+fun run_test ctxt s =
+ Context.setmp_generic_context (SOME (Context.Proof ctxt))
+ (fn () =>
+ ML_Compiler0.ML ML_Env.context
+ {line = 0, file = "generated code", verbose = false, debug = false} s) ();
+
+(*split input into tokens*)
+fun input_split s =
+ let
+ fun dot c = c = #"."
+ fun space c = c = #" "
+ val (head, code) = Substring.splitl (not o dot) (Substring.full s)
+ in
+ (String.tokens space (Substring.string head),
+ Substring.string (Substring.dropl dot code))
+ end;
+
+(*create the function from the input*)
+fun make_fun s =
+ let
+ val scan_param = Scan.one (fn s => s <> ";")
+ fun parameters s = Scan.repeat1 scan_param s
+ val p = $$ "ALL" |-- parameters
+ val (split, code) = input_split s
+ val stop = Scan.stopper (fn _ => ";") (fn s => s = ";");
+ val (params, _) = Scan.finite stop p split
+ in "fn (" ^ commas params ^ ") => " ^ code end;
+
+(*read input and perform the test*)
+fun gen_check_property check ctxt s =
+ let
+ val func = make_fun s
+ val (_, ty) = determine_type ctxt func
+ in run_test ctxt (check ctxt "Check" (ty, func)) end;
+
+val check_property = gen_check_property Gen_Construction.build_check
+(*val check_property_safe = gen_check_property Gen_Construction.safe_check*)
+
+(*perform test for specification function*)
+fun gen_check_property_f check ctxt s =
+ let
+ val (name, ty) = determine_type ctxt s
+ in run_test ctxt (check ctxt name (ty, s)) end;
+
+val check_property_f = gen_check_property_f Gen_Construction.build_check
+(*val check_property_safe_f_ = gen_check_property_f Gen_Construction.safe_check*)
+
+end;
+
+fun check_property s = Spec_Check.check_property (Context.the_local_context ()) s;
+