adapting Quickcheck_Narrowing: adding setup for characters; correcting import statement
authorbulwahn
Thu, 09 Jun 2011 08:32:18 +0200
changeset 43312 7a31f9064f99
parent 43311 1efdcb579b6c
child 43313 d3c34987863b
adapting Quickcheck_Narrowing: adding setup for characters; correcting import statement
src/HOL/Quickcheck_Narrowing.thy
--- a/src/HOL/Quickcheck_Narrowing.thy	Thu Jun 09 08:32:16 2011 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy	Thu Jun 09 08:32:18 2011 +0200
@@ -3,7 +3,7 @@
 header {* Counterexample generator preforming narrowing-based testing *}
 
 theory Quickcheck_Narrowing
-imports Main "~~/src/HOL/Library/Code_Char"
+imports Quickcheck_Exhaustive
 uses
   ("~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs")
   ("~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs")
@@ -26,6 +26,20 @@
 
 code_reserved Haskell_Quickcheck Typerep
 
+code_type char
+  (Haskell_Quickcheck "Char")
+
+setup {*
+  fold String_Code.add_literal_char ["Haskell_Quickcheck"] 
+  #> String_Code.add_literal_list_string "Haskell_Quickcheck"
+*}
+
+code_instance char :: equal
+  (Haskell_Quickcheck -)
+
+code_const "HOL.equal \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
+  (Haskell_Quickcheck infix 4 "==")
+
 subsubsection {* Type @{text "code_int"} for Haskell_Quickcheck's Int type *}
 
 typedef (open) code_int = "UNIV \<Colon> int set"