added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
authorbulwahn
Wed Aug 25 16:59:51 2010 +0200 (2010-08-25)
changeset 387334b8fd91ea59a
parent 38732 3371dbc806ae
child 38734 e5508a74b11f
added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
src/HOL/Tools/Predicate_Compile/code_prolog.ML
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Wed Aug 25 16:59:51 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Wed Aug 25 16:59:51 2010 +0200
     1.3 @@ -89,5 +89,13 @@
     1.4  values 10 "{s. hotel s}"
     1.5  
     1.6  
     1.7 +setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *}
     1.8 +ML {* set Code_Prolog.trace *}
     1.9 +
    1.10 +lemma "\<lbrakk> hotel s; g \<in> isin s r \<rbrakk> \<Longrightarrow> owns s r = Some g"
    1.11 +quickcheck[generator = code, iterations = 100000, report]
    1.12 +quickcheck[generator = prolog, iterations = 1]
    1.13 +oops
    1.14 +
    1.15  
    1.16  end
    1.17 \ No newline at end of file
     2.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Aug 25 16:59:51 2010 +0200
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Aug 25 16:59:51 2010 +0200
     2.3 @@ -26,6 +26,8 @@
     2.4    val write_program : logic_program -> string
     2.5    val run : logic_program -> string -> string list -> int option -> prol_term list list
     2.6  
     2.7 +  val quickcheck : Proof.context -> bool -> term -> int -> term list option * (bool list * bool)
     2.8 +
     2.9    val trace : bool Unsynchronized.ref
    2.10  end;
    2.11  
    2.12 @@ -517,5 +519,51 @@
    2.13     >> (fn ((print_modes, soln), t) => Toplevel.keep
    2.14          (values_cmd print_modes soln t))); (*FIXME does not preserve the previous functionality*)
    2.15  
    2.16 +(* quickcheck generator *)
    2.17 +
    2.18 +(* FIXME: large copy of Predicate_Compile_Quickcheck - refactor out commons *)
    2.19 +
    2.20 +fun strip_imp_prems (Const(@{const_name "op -->"}, _) $ A $ B) = A :: strip_imp_prems B
    2.21 +  | strip_imp_prems _ = [];
    2.22 +
    2.23 +fun strip_imp_concl (Const(@{const_name "op -->"}, _) $ A $ B) = strip_imp_concl B
    2.24 +  | strip_imp_concl A = A : term;
    2.25 +
    2.26 +fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
    2.27 +
    2.28 +fun quickcheck ctxt report t size =
    2.29 +  let
    2.30 +    val ctxt' = ProofContext.theory (Context.copy_thy) ctxt
    2.31 +    val thy = (ProofContext.theory_of ctxt')
    2.32 +    val (vs, t') = strip_abs t
    2.33 +    val vs' = Variable.variant_frees ctxt' [] vs
    2.34 +    val Ts = map snd vs'
    2.35 +    val t'' = subst_bounds (map Free (rev vs'), t')
    2.36 +    val (prems, concl) = strip_horn t''
    2.37 +    val constname = "quickcheck"
    2.38 +    val full_constname = Sign.full_bname thy constname
    2.39 +    val constT = Ts ---> @{typ bool}
    2.40 +    val thy1 = Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] thy
    2.41 +    val const = Const (full_constname, constT)
    2.42 +    val t = Logic.list_implies
    2.43 +      (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]),
    2.44 +       HOLogic.mk_Trueprop (list_comb (Const (full_constname, constT), map Free vs')))
    2.45 +    val tac = fn _ => Skip_Proof.cheat_tac thy1
    2.46 +    val intro = Goal.prove (ProofContext.init_global thy1) (map fst vs') [] t tac
    2.47 +    val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1
    2.48 +    val thy3 = Predicate_Compile.preprocess preprocess_options const thy2
    2.49 +    val ctxt'' = ProofContext.init_global thy3
    2.50 +    val _ = tracing "Generating prolog program..."
    2.51 +    val (p, constant_table) = generate {ensure_groundness = true} ctxt'' full_constname
    2.52 +      |> add_ground_predicates ctxt''
    2.53 +    val _ = tracing "Running prolog program..."
    2.54 +    val [ts] = run p (translate_const constant_table full_constname) (map (first_upper o fst) vs')
    2.55 +      (SOME 1)
    2.56 +    val _ = tracing "Restoring terms..."
    2.57 +    val res = SOME (map (restore_term ctxt'' constant_table) (ts ~~ Ts))
    2.58 +    val empty_report = ([], false)
    2.59 +  in
    2.60 +    (res, empty_report)
    2.61 +  end; 
    2.62  
    2.63  end;