# HG changeset patch
# User bulwahn
# Date 1282748391 -7200
# Node ID 4b8fd91ea59aae359dbbc1c3fa85f5836ddc8b5c
# Parent  3371dbc806ae23147e1dd26b21c398fc2ee4a9b6
added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system

diff -r 3371dbc806ae -r 4b8fd91ea59a src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Wed Aug 25 16:59:51 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Wed Aug 25 16:59:51 2010 +0200
@@ -89,5 +89,13 @@
 values 10 "{s. hotel s}"
 
 
+setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *}
+ML {* set Code_Prolog.trace *}
+
+lemma "\<lbrakk> hotel s; g \<in> isin s r \<rbrakk> \<Longrightarrow> owns s r = Some g"
+quickcheck[generator = code, iterations = 100000, report]
+quickcheck[generator = prolog, iterations = 1]
+oops
+
 
 end
\ No newline at end of file
diff -r 3371dbc806ae -r 4b8fd91ea59a src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Aug 25 16:59:51 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Aug 25 16:59:51 2010 +0200
@@ -26,6 +26,8 @@
   val write_program : logic_program -> string
   val run : logic_program -> string -> string list -> int option -> prol_term list list
 
+  val quickcheck : Proof.context -> bool -> term -> int -> term list option * (bool list * bool)
+
   val trace : bool Unsynchronized.ref
 end;
 
@@ -517,5 +519,51 @@
    >> (fn ((print_modes, soln), t) => Toplevel.keep
         (values_cmd print_modes soln t))); (*FIXME does not preserve the previous functionality*)
 
+(* quickcheck generator *)
+
+(* FIXME: large copy of Predicate_Compile_Quickcheck - refactor out commons *)
+
+fun strip_imp_prems (Const(@{const_name "op -->"}, _) $ A $ B) = A :: strip_imp_prems B
+  | strip_imp_prems _ = [];
+
+fun strip_imp_concl (Const(@{const_name "op -->"}, _) $ A $ B) = strip_imp_concl B
+  | strip_imp_concl A = A : term;
+
+fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
+
+fun quickcheck ctxt report t size =
+  let
+    val ctxt' = ProofContext.theory (Context.copy_thy) ctxt
+    val thy = (ProofContext.theory_of ctxt')
+    val (vs, t') = strip_abs t
+    val vs' = Variable.variant_frees ctxt' [] vs
+    val Ts = map snd vs'
+    val t'' = subst_bounds (map Free (rev vs'), t')
+    val (prems, concl) = strip_horn t''
+    val constname = "quickcheck"
+    val full_constname = Sign.full_bname thy constname
+    val constT = Ts ---> @{typ bool}
+    val thy1 = Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] thy
+    val const = Const (full_constname, constT)
+    val t = Logic.list_implies
+      (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]),
+       HOLogic.mk_Trueprop (list_comb (Const (full_constname, constT), map Free vs')))
+    val tac = fn _ => Skip_Proof.cheat_tac thy1
+    val intro = Goal.prove (ProofContext.init_global thy1) (map fst vs') [] t tac
+    val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1
+    val thy3 = Predicate_Compile.preprocess preprocess_options const thy2
+    val ctxt'' = ProofContext.init_global thy3
+    val _ = tracing "Generating prolog program..."
+    val (p, constant_table) = generate {ensure_groundness = true} ctxt'' full_constname
+      |> add_ground_predicates ctxt''
+    val _ = tracing "Running prolog program..."
+    val [ts] = run p (translate_const constant_table full_constname) (map (first_upper o fst) vs')
+      (SOME 1)
+    val _ = tracing "Restoring terms..."
+    val res = SOME (map (restore_term ctxt'' constant_table) (ts ~~ Ts))
+    val empty_report = ([], false)
+  in
+    (res, empty_report)
+  end; 
 
 end;