# HG changeset patch # User blanchet # Date 1282812142 -7200 # Node ID 3913f58d0fcc39c84694162b071c44e660ef4470 # Parent 14c1085dec028961f6a7bb4c595be63ddbaee0e6# Parent 6628adcae4a710ae19e8619ae9e319aae1c08748 merged diff -r 6628adcae4a7 -r 3913f58d0fcc src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Aug 26 10:42:06 2010 +0200 +++ b/src/HOL/IsaMakefile Thu Aug 26 10:42:22 2010 +0200 @@ -1321,7 +1321,8 @@ Predicate_Compile_Examples/ROOT.ML \ Predicate_Compile_Examples/Predicate_Compile_Examples.thy \ Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy \ - Predicate_Compile_Examples/Code_Prolog_Examples.thy + Predicate_Compile_Examples/Code_Prolog_Examples.thy \ + Predicate_Compile_Examples/Hotel_Example.thy @$(ISABELLE_TOOL) usedir $(OUT)/HOL Predicate_Compile_Examples diff -r 6628adcae4a7 -r 3913f58d0fcc src/HOL/Library/Code_Prolog.thy --- a/src/HOL/Library/Code_Prolog.thy Thu Aug 26 10:42:06 2010 +0200 +++ b/src/HOL/Library/Code_Prolog.thy Thu Aug 26 10:42:22 2010 +0200 @@ -9,5 +9,10 @@ uses "~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML" begin +section {* Setup for Numerals *} + +setup {* Predicate_Compile_Data.ignore_consts [@{const_name number_of}] *} +setup {* Predicate_Compile_Data.keep_functions [@{const_name number_of}] *} + end diff -r 6628adcae4a7 -r 3913f58d0fcc src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy --- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Thu Aug 26 10:42:06 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Thu Aug 26 10:42:22 2010 +0200 @@ -9,8 +9,6 @@ "append [] ys ys" | "append xs ys zs ==> append (x # xs) ys (x # zs)" -code_pred append . - values 3 "{(x, y, z). append x y z}" @@ -71,9 +69,7 @@ where "queen [1,2,3,4,5,6,7,8,9] ys ==> queen_9 ys" -code_pred queen_9 . - -values 150 "{ys. queen_9 ys}" +values 10 "{ys. queen_9 ys}" section {* Example symbolic derivation *} @@ -163,14 +159,35 @@ where "d (Mult (Mult (Mult (Mult (Mult (Mult (Mult (Mult (Mult x x) x) x) x) x) x) x) x) x) x e ==> times10 e" -code_pred ops8 . -code_pred divide10 . -code_pred log10 . -code_pred times10 . - values "{e. ops8 e}" values "{e. divide10 e}" values "{e. log10 e}" values "{e. times10 e}" +section {* Example negation *} + +datatype abc = A | B | C + +inductive notB :: "abc => bool" +where + "y \ B \ notB y" + +ML {* Code_Prolog.options := {ensure_groundness = true} *} + +values 2 "{y. notB y}" + +inductive notAB :: "abc * abc \ bool" +where + "y \ A \ z \ B \ notAB (y, z)" + +values 5 "{y. notAB y}" + +section {* Example prolog conform variable names *} + +inductive equals :: "abc => abc => bool" +where + "equals y' y'" +ML {* set Code_Prolog.trace *} +values 1 "{(y, z). equals y z}" + end diff -r 6628adcae4a7 -r 3913f58d0fcc src/HOL/Predicate_Compile_Examples/Hotel_Example.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Thu Aug 26 10:42:22 2010 +0200 @@ -0,0 +1,101 @@ +theory Hotel_Example +imports Predicate_Compile_Alternative_Defs Code_Prolog +begin + +datatype guest = Guest0 | Guest1 +datatype key = Key0 | Key1 | Key2 | Key3 +datatype room = Room0 + +types card = "key * key" + +datatype event = + Check_in guest room card | Enter guest room card | Exit guest room + +definition initk :: "room \ key" + where "initk = (%r. Key0)" + +declare initk_def[code_pred_def, code] + +primrec owns :: "event list \ room \ guest option" +where + "owns [] r = None" +| "owns (e#s) r = (case e of + Check_in g r' c \ if r' = r then Some g else owns s r | + Enter g r' c \ owns s r | + Exit g r' \ owns s r)" + +primrec currk :: "event list \ room \ key" +where + "currk [] r = initk r" +| "currk (e#s) r = (let k = currk s r in + case e of Check_in g r' (k1, k2) \ if r' = r then k2 else k + | Enter g r' c \ k + | Exit g r \ k)" + +primrec issued :: "event list \ key set" +where + "issued [] = range initk" +| "issued (e#s) = issued s \ + (case e of Check_in g r (k1, k2) \ {k2} | Enter g r c \ {} | Exit g r \ {})" + +primrec cards :: "event list \ guest \ card set" +where + "cards [] g = {}" +| "cards (e#s) g = (let C = cards s g in + case e of Check_in g' r c \ if g' = g then insert c C + else C + | Enter g r c \ C + | Exit g r \ C)" + +primrec roomk :: "event list \ room \ key" +where + "roomk [] r = initk r" +| "roomk (e#s) r = (let k = roomk s r in + case e of Check_in g r' c \ k + | Enter g r' (x,y) \ if r' = r (*& x = k*) then y else k + | Exit g r \ k)" + +primrec isin :: "event list \ room \ guest set" +where + "isin [] r = {}" +| "isin (e#s) r = (let G = isin s r in + case e of Check_in g r c \ G + | Enter g r' c \ if r' = r then {g} \ G else G + | Exit g r' \ if r'=r then G - {g} else G)" + +primrec hotel :: "event list \ bool" +where + "hotel [] = True" +| "hotel (e # s) = (hotel s & (case e of + Check_in g r (k,k') \ k = currk s r \ k' \ issued s | + Enter g r (k,k') \ (k,k') : cards s g & (roomk s r : {k, k'}) | + Exit g r \ g : isin s r))" + +lemma issued_nil: "issued [] = {Key0}" +by (auto simp add: initk_def) + +lemmas issued_simps[code, code_pred_def] = issued_nil issued.simps(2) + +declare Let_def[code_pred_inline] + +lemma [code_pred_inline]: "insert == (%y A x. y = x | A x)" +by (auto simp add: insert_iff[unfolded mem_def] expand_fun_eq intro!: eq_reflection) + +lemma [code_pred_inline]: "(op -) == (%A B x. A x \ \ B x)" +by (auto simp add: Diff_iff[unfolded mem_def] expand_fun_eq intro!: eq_reflection) + +ML {* Code_Prolog.options := {ensure_groundness = true} *} + +values 40 "{s. hotel s}" + + +setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *} +ML {* set Code_Prolog.trace *} + +lemma "\ hotel s; g \ isin s r \ \ 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 6628adcae4a7 -r 3913f58d0fcc src/HOL/Predicate_Compile_Examples/ROOT.ML --- a/src/HOL/Predicate_Compile_Examples/ROOT.ML Thu Aug 26 10:42:06 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML Thu Aug 26 10:42:22 2010 +0200 @@ -1,2 +1,2 @@ use_thys ["Predicate_Compile_Examples", "Predicate_Compile_Quickcheck_Examples", "Specialisation_Examples"]; -if getenv "PROLOG_HOME" = "" then () else use_thys ["Code_Prolog_Examples"]; +if getenv "PROLOG_HOME" = "" then () else use_thys ["Code_Prolog_Examples", "Hotel_Example"]; diff -r 6628adcae4a7 -r 3913f58d0fcc src/HOL/Tools/Predicate_Compile/code_prolog.ML --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Aug 26 10:42:06 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Aug 26 10:42:22 2010 +0200 @@ -6,22 +6,28 @@ signature CODE_PROLOG = sig + type code_options = {ensure_groundness : bool} + val options : code_options ref + datatype arith_op = Plus | Minus datatype prol_term = Var of string | Cons of string | AppF of string * prol_term list | Number of int | ArithOp of arith_op * prol_term list; datatype prem = Conj of prem list | Rel of string * prol_term list | NotRel of string * prol_term list | Eq of prol_term * prol_term | NotEq of prol_term * prol_term - | ArithEq of prol_term * prol_term | NotArithEq of prol_term * prol_term; - + | ArithEq of prol_term * prol_term | NotArithEq of prol_term * prol_term + | Ground of string * typ; + type clause = ((string * prol_term list) * prem); type logic_program = clause list; type constant_table = (string * string) list - - val generate : Proof.context -> string list -> (logic_program * constant_table) + + val generate : code_options -> Proof.context -> string -> (logic_program * constant_table) 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; @@ -33,6 +39,13 @@ val trace = Unsynchronized.ref false fun tracing s = if !trace then Output.tracing s else () + +(* code generation options *) + +type code_options = {ensure_groundness : bool} + +val options = Unsynchronized.ref {ensure_groundness = false}; + (* general string functions *) val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode; @@ -45,6 +58,21 @@ datatype prol_term = Var of string | Cons of string | AppF of string * prol_term list | Number of int | ArithOp of arith_op * prol_term list; +fun dest_Var (Var v) = v + +fun add_vars (Var v) = insert (op =) v + | add_vars (ArithOp (_, ts)) = fold add_vars ts + | add_vars (AppF (_, ts)) = fold add_vars ts + | add_vars _ = I + +fun map_vars f (Var v) = Var (f v) + | map_vars f (ArithOp (opr, ts)) = ArithOp (opr, map (map_vars f) ts) + | map_vars f (AppF (fs, ts)) = AppF (fs, map (map_vars f) ts) + | map_vars f t = t + +fun maybe_AppF (c, []) = Cons c + | maybe_AppF (c, xs) = AppF (c, xs) + fun is_Var (Var _) = true | is_Var _ = false @@ -61,10 +89,29 @@ datatype prem = Conj of prem list | Rel of string * prol_term list | NotRel of string * prol_term list | Eq of prol_term * prol_term | NotEq of prol_term * prol_term - | ArithEq of prol_term * prol_term | NotArithEq of prol_term * prol_term; - + | ArithEq of prol_term * prol_term | NotArithEq of prol_term * prol_term + | Ground of string * typ; + fun dest_Rel (Rel (c, ts)) = (c, ts) - + +fun map_term_prem f (Conj prems) = Conj (map (map_term_prem f) prems) + | map_term_prem f (Rel (r, ts)) = Rel (r, map f ts) + | map_term_prem f (NotRel (r, ts)) = NotRel (r, map f ts) + | map_term_prem f (Eq (l, r)) = Eq (f l, f r) + | map_term_prem f (NotEq (l, r)) = NotEq (f l, f r) + | map_term_prem f (ArithEq (l, r)) = ArithEq (f l, f r) + | map_term_prem f (NotArithEq (l, r)) = NotArithEq (f l, f r) + | map_term_prem f (Ground (v, T)) = Ground (dest_Var (f (Var v)), T) + +fun fold_prem_terms f (Conj prems) = fold (fold_prem_terms f) prems + | fold_prem_terms f (Rel (_, ts)) = fold f ts + | fold_prem_terms f (NotRel (_, ts)) = fold f ts + | fold_prem_terms f (Eq (l, r)) = f l #> f r + | fold_prem_terms f (NotEq (l, r)) = f l #> f r + | fold_prem_terms f (ArithEq (l, r)) = f l #> f r + | fold_prem_terms f (NotArithEq (l, r)) = f l #> f r + | fold_prem_terms f (Ground (v, T)) = f (Var v) + type clause = ((string * prol_term list) * prem); type logic_program = clause list; @@ -96,16 +143,23 @@ case inv_lookup (op =) constant_table c of SOME c' => c' | NONE => error ("No constant corresponding to " ^ c) - + (** translation of terms, literals, premises, and clauses **) fun translate_arith_const @{const_name "Groups.plus_class.plus"} = SOME Plus | translate_arith_const @{const_name "Groups.minus_class.minus"} = SOME Minus | translate_arith_const _ = NONE +fun mk_nat_term constant_table n = + let + val zero = translate_const constant_table @{const_name "Groups.zero_class.zero"} + val Suc = translate_const constant_table @{const_name "Suc"} + in funpow n (fn t => AppF (Suc, [t])) (Cons zero) end + fun translate_term ctxt constant_table t = case try HOLogic.dest_number t of SOME (@{typ "int"}, n) => Number n + | SOME (@{typ "nat"}, n) => mk_nat_term constant_table n | NONE => (case strip_comb t of (Free (v, T), []) => Var v @@ -124,7 +178,7 @@ val l' = translate_term ctxt constant_table l val r' = translate_term ctxt constant_table r in - (if is_Var l' andalso is_arith_term r' then ArithEq else Eq) (l', r') + (if is_Var l' andalso is_arith_term r' andalso not (is_Var r') then ArithEq else Eq) (l', r') end | (Const (c, _), args) => Rel (translate_const constant_table c, map (translate_term ctxt constant_table) args) @@ -134,11 +188,16 @@ | NegRel_of (Eq eq) = NotEq eq | NegRel_of (ArithEq eq) = NotArithEq eq -fun translate_prem ctxt constant_table t = +fun mk_groundness_prems t = map Ground (Term.add_frees t []) + +fun translate_prem options ctxt constant_table t = case try HOLogic.dest_not t of - SOME t => NegRel_of (translate_literal ctxt constant_table t) + SOME t => + if #ensure_groundness options then + Conj (mk_groundness_prems t @ [NegRel_of (translate_literal ctxt constant_table t)]) + else + NegRel_of (translate_literal ctxt constant_table t) | NONE => translate_literal ctxt constant_table t - fun imp_prems_conv cv ct = case Thm.term_of ct of @@ -156,64 +215,165 @@ (Trueprop_conv (Conv.try_conv (Conv.rewr_conv @{thm Predicate.eq_is_eq})))) (Thm.transfer thy rule) -fun translate_intros ctxt gr const constant_table = +fun translate_intros options ctxt gr const constant_table = let val intros = map (preprocess_intro (ProofContext.theory_of ctxt)) (Graph.get_node gr const) val (intros', ctxt') = Variable.import_terms true (map prop_of intros) ctxt val constant_table' = declare_consts (fold Term.add_const_names intros' []) constant_table + |> declare_consts [@{const_name "Groups.zero_class.zero"}, @{const_name "Suc"}] fun translate_intro intro = let val head = HOLogic.dest_Trueprop (Logic.strip_imp_concl intro) - val prems = map HOLogic.dest_Trueprop (Logic.strip_imp_prems intro) - val prems' = Conj (map (translate_prem ctxt' constant_table') prems) + val prems = map HOLogic.dest_Trueprop (Logic.strip_imp_prems intro) + val prems' = Conj (map (translate_prem options ctxt' constant_table') prems) val clause = (dest_Rel (translate_literal ctxt' constant_table' head), prems') in clause end in (map translate_intro intros', constant_table') end -fun generate ctxt const = - let - fun strong_conn_of gr keys = - Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr) - val gr = Predicate_Compile_Core.intros_graph_of ctxt - val scc = strong_conn_of gr const - val constant_table = mk_constant_table (flat scc) +val preprocess_options = Predicate_Compile_Aux.Options { + expected_modes = NONE, + proposed_modes = NONE, + proposed_names = [], + show_steps = false, + show_intermediate_results = false, + show_proof_trace = false, + show_modes = false, + show_mode_inference = false, + show_compilation = false, + show_caught_failures = false, + skip_proof = true, + no_topmost_reordering = false, + function_flattening = true, + specialise = false, + fail_safe_function_flattening = false, + no_higher_order_predicate = [], + inductify = false, + detect_switches = true, + compilation = Predicate_Compile_Aux.Pred +} + +fun depending_preds_of (key, intros) = + fold Term.add_const_names (map Thm.prop_of intros) [] + +fun add_edges edges_of key G = + let + fun extend' key (G, visited) = + case try (Graph.get_node G) key of + SOME v => + let + val new_edges = filter (fn k => is_some (try (Graph.get_node G) k)) (edges_of (key, v)) + val (G', visited') = fold extend' + (subtract (op =) (key :: visited) new_edges) (G, key :: visited) + in + (fold (Graph.add_edge o (pair key)) new_edges G', visited') + end + | NONE => (G, visited) in - apfst flat (fold_map (translate_intros ctxt gr) (flat scc) constant_table) + fst (extend' key (G, [])) end -(* transform logic program *) +fun generate options ctxt const = + let + fun strong_conn_of gr keys = + Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr) + val gr = Predicate_Compile_Core.intros_graph_of ctxt + val gr' = add_edges depending_preds_of const gr + val scc = strong_conn_of gr' [const] + val constant_table = mk_constant_table (flat scc) + in + apfst flat (fold_map (translate_intros options ctxt gr) (flat scc) constant_table) + end + +(* add implementation for ground predicates *) -(** ensure groundness of terms before negation **) +fun add_ground_typ (Conj prems) = fold add_ground_typ prems + | add_ground_typ (Ground (_, T)) = insert (op =) T + | add_ground_typ _ = I + +fun mk_relname (Type (Tcon, Targs)) = + first_lower (Long_Name.base_name Tcon) ^ space_implode "_" (map mk_relname Targs) + | mk_relname _ = raise Fail "unexpected type" -fun add_vars (Var x) vs = insert (op =) x vs - | add_vars (Cons c) vs = vs - | add_vars (AppF (f, args)) vs = fold add_vars args vs +(* This is copied from "pat_completeness.ML" *) +fun inst_constrs_of thy (T as Type (name, _)) = + map (fn (Cn,CT) => + Envir.subst_term_types (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT))) + (the (Datatype.get_constrs thy name)) + | inst_constrs_of thy T = raise TYPE ("inst_constrs_of", [T], []) + +fun mk_ground_impl ctxt (T as Type (Tcon, Targs)) (seen, constant_table) = + if member (op =) seen T then ([], (seen, constant_table)) + else + let + val rel_name = mk_relname T + fun mk_impl (Const (constr_name, T)) (seen, constant_table) = + let + val constant_table' = declare_consts [constr_name] constant_table + val (rec_clauses, (seen', constant_table'')) = + fold_map (mk_ground_impl ctxt) (binder_types T) (seen, constant_table') + val vars = map (fn i => Var ("x" ^ string_of_int i)) (1 upto (length (binder_types T))) + fun mk_prem v T = Rel (mk_relname T, [v]) + val clause = + ((rel_name, [maybe_AppF (translate_const constant_table'' constr_name, vars)]), + Conj (map2 mk_prem vars (binder_types T))) + in + (clause :: flat rec_clauses, (seen', constant_table'')) + end + val constrs = inst_constrs_of (ProofContext.theory_of ctxt) T + in apfst flat (fold_map mk_impl constrs (T :: seen, constant_table)) end + | mk_ground_impl ctxt T (seen, constant_table) = + raise Fail ("unexpected type :" ^ Syntax.string_of_typ ctxt T) -fun string_of_typ (Type (s, Ts)) = Long_Name.base_name s - -fun mk_groundness_prems ts = +fun replace_ground (Conj prems) = Conj (map replace_ground prems) + | replace_ground (Ground (x, T)) = + Rel (mk_relname T, [Var x]) + | replace_ground p = p + +fun add_ground_predicates ctxt (p, constant_table) = let - val vars = fold add_vars ts [] - fun mk_ground v = - Rel ("ground", [Var v]) + val ground_typs = fold (add_ground_typ o snd) p [] + val (grs, (_, constant_table')) = fold_map (mk_ground_impl ctxt) ground_typs ([], constant_table) + val p' = map (apsnd replace_ground) p in - map mk_ground vars + ((flat grs) @ p', constant_table') end + +(* rename variables to prolog-friendly names *) + +fun rename_vars_term renaming = map_vars (fn v => the (AList.lookup (op =) renaming v)) + +fun rename_vars_prem renaming = map_term_prem (rename_vars_term renaming) + +fun dest_Char (Symbol.Char c) = c + +fun is_prolog_conform v = + forall (fn s => Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s) (Symbol.explode v) -fun ensure_groundness_prem (NotRel (c, ts)) = Conj (mk_groundness_prems ts @ [NotRel (c, ts)]) - | ensure_groundness_prem (NotEq (l, r)) = Conj (mk_groundness_prems [l, r] @ [NotEq (l, r)]) - | ensure_groundness_prem (Conj ps) = Conj (map ensure_groundness_prem ps) - | ensure_groundness_prem p = p +fun mk_conform avoid v = + let + val v' = space_implode "" (map (dest_Char o Symbol.decode) + (filter (fn s => Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s) + (Symbol.explode v))) + val v' = if v' = "" then "var" else v' + in Name.variant avoid (first_upper v') end + +fun mk_renaming v renaming = + (v, mk_conform (map snd renaming) v) :: renaming -fun ensure_groundness_before_negation p = - map (apsnd ensure_groundness_prem) p - +fun rename_vars_clause ((rel, args), prem) = + let + val vars = fold_prem_terms add_vars prem (fold add_vars args []) + val renaming = fold mk_renaming vars [] + in ((rel, map (rename_vars_term renaming) args), rename_vars_prem renaming prem) end + +val rename_vars_program = map rename_vars_clause + (* code printer *) fun write_arith_op Plus = "+" | write_arith_op Minus = "-" -fun write_term (Var v) = first_upper v +fun write_term (Var v) = v | write_term (Cons c) = c | write_term (AppF (f, args)) = f ^ "(" ^ space_implode ", " (map write_term args) ^ ")" | write_term (ArithOp (oper, [a1, a2])) = write_term a1 ^ " " ^ write_arith_op oper ^ " " ^ write_term a2 @@ -254,7 +414,9 @@ val prelude = "#!/usr/bin/swipl -q -t main -f\n\n" ^ ":- use_module(library('dialect/ciao/aggregates')).\n" ^ - ":- style_check(-singleton).\n\n" ^ + ":- style_check(-singleton).\n" ^ + ":- style_check(-discontiguous).\n" ^ + ":- style_check(-atom).\n\n" ^ "main :- catch(eval, E, (print_message(error, E), fail)), halt.\n" ^ "main :- halt(1).\n" @@ -263,7 +425,7 @@ Scan.many1 Symbol.is_ascii_digit val scan_atom = - Scan.many1 (fn s => Symbol.is_ascii_lower s orelse Symbol.is_ascii_quasi s) + Scan.many1 (fn s => Symbol.is_ascii_lower s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s) val scan_var = Scan.many1 @@ -312,8 +474,12 @@ fun run p query_rel vnames nsols = let val cmd = Path.named_root - val query = case nsols of NONE => query_first | SOME n => query_firstn n - val prog = prelude ^ query query_rel vnames ^ write_program p + val query = case nsols of NONE => query_first | SOME n => query_firstn n + val p' = rename_vars_program p + val _ = tracing "Renaming variable names..." + val renaming = fold mk_renaming vnames [] + val vnames' = map (fn v => the (AList.lookup (op =) renaming v)) vnames + val prog = prelude ^ query query_rel vnames' ^ write_program p' val _ = tracing ("Generated prolog program:\n" ^ prog) val prolog_file = File.tmp_path (Path.basic "prolog_file") val _ = File.write prolog_file prog @@ -345,6 +511,7 @@ fun values ctxt soln t_compr = let + val options = !options val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term ctxt t_compr); val (body, Ts, fp) = HOLogic.strip_psplits split; @@ -360,8 +527,15 @@ case try (map (fst o dest_Free)) all_args of SOME vs => vs | NONE => error ("Not only free variables in " ^ commas (map (Syntax.string_of_term ctxt) all_args)) + val _ = tracing "Preprocessing specification..." + val T = Sign.the_const_type (ProofContext.theory_of ctxt) name + val t = Const (name, T) + val ctxt' = ProofContext.theory (Context.copy_thy) ctxt + val thy' = Predicate_Compile.preprocess preprocess_options t (ProofContext.theory_of ctxt') + val ctxt'' = ProofContext.init_global thy' val _ = tracing "Generating prolog program..." - val (p, constant_table) = generate ctxt [name] + val (p, constant_table) = generate options ctxt'' name + |> (if #ensure_groundness options then add_ground_predicates ctxt'' else I) val _ = tracing "Running prolog program..." val tss = run p (translate_const constant_table name) (map first_upper vnames) soln val _ = tracing "Restoring terms..." @@ -379,17 +553,18 @@ mk_set_compr (t :: in_insert) ts xs else let - val uu as (uuN, uuT) = singleton (Variable.variant_frees ctxt [t]) ("uu", fastype_of t) + val uu as (uuN, uuT) = singleton (Variable.variant_frees ctxt'' [t]) ("uu", fastype_of t) val set_compr = HOLogic.mk_Collect (uuN, uuT, fold (fn (s, T) => fn t => HOLogic.mk_exists (s, T, t)) frees (HOLogic.mk_conj (HOLogic.mk_eq (Free uu, t), @{term "True"}))) in - set_compr :: (if null in_insert then xs else (fold mk_insert in_insert empty) :: xs) + mk_set_compr [] ts + (set_compr :: (if null in_insert then xs else (fold mk_insert in_insert empty) :: xs)) end end in foldl1 (HOLogic.mk_binop @{const_name sup}) (mk_set_compr [] - (map (fn ts => HOLogic.mk_tuple (map (restore_term ctxt constant_table) (ts ~~ Ts))) tss) []) + (map (fn ts => HOLogic.mk_tuple (map (restore_term ctxt'' constant_table) (ts ~~ Ts))) tss) []) end fun values_cmd print_modes soln raw_t state = @@ -416,4 +591,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 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; diff -r 6628adcae4a7 -r 3913f58d0fcc src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Thu Aug 26 10:42:06 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Thu Aug 26 10:42:22 2010 +0200 @@ -275,7 +275,6 @@ else let val specs = get_specification options thy t - (*|> Predicate_Compile_Set.unfold_set_notation*) (*val _ = print_specification options thy constname specs*) val us = defiants_of specs in