# HG changeset patch # User haftmann # Date 1284652276 -7200 # Node ID fd1032c23cdfff714328e7686e05cb50bfd37bfc # Parent d7caf48c46769d67b9e1bb7fd2511ca7a2680d0e# Parent 8bc560df99eacf5eb94667c8fb324f9c51b886bd merged diff -r 8bc560df99ea -r fd1032c23cdf etc/components --- a/etc/components Thu Sep 16 16:51:44 2010 +0200 +++ b/etc/components Thu Sep 16 17:51:16 2010 +0200 @@ -17,3 +17,4 @@ src/HOL/Mirabelle src/HOL/Library/Sum_Of_Squares src/HOL/Tools/SMT +src/HOL/Tools/Predicate_Compile diff -r 8bc560df99ea -r fd1032c23cdf src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy --- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Thu Sep 16 16:51:44 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Thu Sep 16 17:51:16 2010 +0200 @@ -15,12 +15,12 @@ limited_types = [], limited_predicates = [], replacing = [], - manual_reorder = [], - timeout = Time.fromSeconds 10, - prolog_system = Code_Prolog.SWI_PROLOG}) *} + manual_reorder = []}) *} values "{(x, y, z). append x y z}" +values 4 "{(z, x, y). append x y ((1::nat) # (2 # (3 # z)))}" + values 3 "{(x, y, z). append x y z}" setup {* Code_Prolog.map_code_options (K @@ -28,9 +28,7 @@ limited_types = [], limited_predicates = [], replacing = [], - manual_reorder = [], - timeout = Time.fromSeconds 10, - prolog_system = Code_Prolog.YAP}) *} + manual_reorder = []}) *} values "{(x, y, z). append x y z}" @@ -39,9 +37,7 @@ limited_types = [], limited_predicates = [], replacing = [], - manual_reorder = [], - timeout = Time.fromSeconds 10, - prolog_system = Code_Prolog.SWI_PROLOG}) *} + manual_reorder = []}) *} section {* Example queens *} @@ -209,9 +205,7 @@ limited_types = [], limited_predicates = [], replacing = [], - manual_reorder = [], - timeout = Time.fromSeconds 10, - prolog_system = Code_Prolog.SWI_PROLOG}) *} + manual_reorder = []}) *} values 2 "{y. notB y}" diff -r 8bc560df99ea -r fd1032c23cdf src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy --- a/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy Thu Sep 16 16:51:44 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy Thu Sep 16 17:51:16 2010 +0200 @@ -19,7 +19,7 @@ declare size_list_def[symmetric, code_pred_inline] -setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *} +setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *} datatype alphabet = a | b @@ -61,9 +61,7 @@ limited_types = [], limited_predicates = [(["s1", "a1", "b1"], 2)], replacing = [(("s1", "limited_s1"), "quickcheck")], - manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])], - timeout = Time.fromSeconds 10, - prolog_system = Code_Prolog.SWI_PROLOG}) *} + manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *} theorem S\<^isub>1_sound: @@ -86,9 +84,7 @@ limited_types = [], limited_predicates = [(["s2", "a2", "b2"], 3)], replacing = [(("s2", "limited_s2"), "quickcheck")], - manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])], - timeout = Time.fromSeconds 10, - prolog_system = Code_Prolog.SWI_PROLOG}) *} + manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *} theorem S\<^isub>2_sound: @@ -110,9 +106,7 @@ limited_types = [], limited_predicates = [(["s3", "a3", "b3"], 6)], replacing = [(("s3", "limited_s3"), "quickcheck")], - manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])], - timeout = Time.fromSeconds 10, - prolog_system = Code_Prolog.SWI_PROLOG}) *} + manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *} lemma S\<^isub>3_sound: "w \ S\<^isub>3 \ length [x \ w. x = a] = length [x \ w. x = b]" @@ -152,9 +146,7 @@ limited_types = [], limited_predicates = [(["s4", "a4", "b4"], 6)], replacing = [(("s4", "limited_s4"), "quickcheck")], - manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])], - timeout = Time.fromSeconds 10, - prolog_system = Code_Prolog.SWI_PROLOG}) *} + manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *} theorem S\<^isub>4_sound: diff -r 8bc560df99ea -r fd1032c23cdf src/HOL/Predicate_Compile_Examples/Hotel_Example.thy --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Thu Sep 16 16:51:44 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Thu Sep 16 17:51:16 2010 +0200 @@ -89,14 +89,12 @@ limited_types = [], limited_predicates = [], replacing = [], - manual_reorder = [], - timeout = Time.fromSeconds 10, - prolog_system = Code_Prolog.SWI_PROLOG}) *} + manual_reorder = []}) *} values 40 "{s. hotel s}" -setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *} +setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *} lemma "\ hotel s; g \ isin s r \ \ owns s r = Some g" quickcheck[generator = code, iterations = 100000, report] @@ -119,9 +117,7 @@ limited_types = [], limited_predicates = [(["hotel"], 5)], replacing = [(("hotel", "limited_hotel"), "quickcheck")], - manual_reorder = [], - timeout = Time.fromSeconds 10, - prolog_system = Code_Prolog.SWI_PROLOG}) *} + manual_reorder = []}) *} lemma "hotel s ==> feels_safe s r ==> g \ isin s r ==> owns s r = Some g" diff -r 8bc560df99ea -r fd1032c23cdf src/HOL/Predicate_Compile_Examples/Lambda_Example.thy --- a/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy Thu Sep 16 16:51:44 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy Thu Sep 16 17:51:16 2010 +0200 @@ -79,7 +79,7 @@ section {* Manual setup to find counterexample *} -setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *} +setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *} setup {* Code_Prolog.map_code_options (K { ensure_groundness = true, @@ -87,9 +87,7 @@ limited_predicates = [(["typing"], 2), (["nthel1"], 2)], replacing = [(("typing", "limited_typing"), "quickcheck"), (("nthel1", "limited_nthel1"), "lim_typing")], - manual_reorder = [], - timeout = Time.fromSeconds 10, - prolog_system = Code_Prolog.SWI_PROLOG}) *} + manual_reorder = []}) *} lemma "\ \ t : U \ t \\<^sub>\ t' \ \ \ t' : U" diff -r 8bc560df99ea -r fd1032c23cdf src/HOL/Predicate_Compile_Examples/List_Examples.thy --- a/src/HOL/Predicate_Compile_Examples/List_Examples.thy Thu Sep 16 16:51:44 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/List_Examples.thy Thu Sep 16 17:51:16 2010 +0200 @@ -2,7 +2,7 @@ imports Main "Predicate_Compile_Quickcheck" "Code_Prolog" begin -setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *} +setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *} setup {* Code_Prolog.map_code_options (K {ensure_groundness = true, @@ -12,9 +12,7 @@ [(("appendP", "limited_appendP"), "quickcheck"), (("revP", "limited_revP"), "quickcheck"), (("appendP", "limited_appendP"), "lim_revP")], - manual_reorder = [], - timeout = Time.fromSeconds 10, - prolog_system = Code_Prolog.SWI_PROLOG}) *} + manual_reorder = []}) *} lemma "(xs :: nat list) = ys @ ys --> rev xs = xs" quickcheck[generator = code, iterations = 200000, expect = counterexample] diff -r 8bc560df99ea -r fd1032c23cdf src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Thu Sep 16 16:51:44 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Thu Sep 16 17:51:16 2010 +0200 @@ -1310,6 +1310,10 @@ values "{xs::int list. test_append (replicate 1000 1) (replicate 1000 2) xs}" values "{xs::int list. test_append (replicate 2000 1) (replicate 2000 2) xs}" +text {* Redeclaring append.equation as code equation *} + +declare appendP.equation[code] + subsection {* Function with tuples *} fun append' @@ -1580,6 +1584,56 @@ thm big_step.equation +section {* General Context Free Grammars *} +text {* a contribution by Aditi Barthwal *} + +datatype ('nts,'ts) symbol = NTS 'nts + | TS 'ts + + +datatype ('nts,'ts) rule = rule 'nts "('nts,'ts) symbol list" + +types ('nts,'ts) grammar = "('nts,'ts) rule set * 'nts" + +fun rules :: "('nts,'ts) grammar => ('nts,'ts) rule set" +where + "rules (r, s) = r" + +definition derives +where +"derives g = { (lsl,rsl). \s1 s2 lhs rhs. + (s1 @ [NTS lhs] @ s2 = lsl) \ + (s1 @ rhs @ s2) = rsl \ + (rule lhs rhs) \ fst g }" + +abbreviation "example_grammar == +({ rule ''S'' [NTS ''A'', NTS ''B''], + rule ''S'' [TS ''a''], + rule ''A'' [TS ''b'']}, ''S'')" + + +code_pred [inductify,skip_proof] derives . + +thm derives.equation + +definition "test = { rhs. derives example_grammar ([NTS ''S''], rhs) }" + +code_pred (modes: o \ bool) [inductify, show_modes, show_intermediate_results, skip_proof] test . +thm test.equation + +values "{rhs. test rhs}" + +declare rtrancl.intros(1)[code_pred_def] converse_rtrancl_into_rtrancl[code_pred_def] + +code_pred [inductify] rtrancl . + +definition "test2 = { rhs. ([NTS ''S''],rhs) \ (derives example_grammar)^* }" + +code_pred [inductify, skip_proof] test2 . + +values "{rhs. test2 rhs}" + + section {* Examples for detecting switches *} inductive detect_switches1 where diff -r 8bc560df99ea -r fd1032c23cdf src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy --- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Thu Sep 16 16:51:44 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Thu Sep 16 17:51:16 2010 +0200 @@ -96,7 +96,7 @@ oops -setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *} +setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *} setup {* Code_Prolog.map_code_options (K {ensure_groundness = true, @@ -108,9 +108,7 @@ (("subP", "limited_subP"), "repIntP"), (("repIntPa", "limited_repIntPa"), "repIntP"), (("accepts", "limited_accepts"), "quickcheck")], - manual_reorder = [], - timeout = Time.fromSeconds 10, - prolog_system = Code_Prolog.SWI_PROLOG}) *} + manual_reorder = []}) *} text {* Finding the counterexample still seems out of reach for the prolog-style generation. *} diff -r 8bc560df99ea -r fd1032c23cdf src/HOL/Tools/Predicate_Compile/code_prolog.ML --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Sep 16 16:51:44 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Sep 16 17:51:16 2010 +0200 @@ -12,12 +12,13 @@ limited_types : (typ * int) list, limited_predicates : (string list * int) list, replacing : ((string * string) * string) list, - manual_reorder : ((string * int) * int list) list, - timeout : Time.time, - prolog_system : prolog_system} + manual_reorder : ((string * int) * int list) list} + val set_ensure_groundness : code_options -> code_options + val map_limit_predicates : ((string list * int) list -> (string list * int) list) + -> code_options -> code_options val code_options_of : theory -> code_options val map_code_options : (code_options -> code_options) -> theory -> theory - + 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; @@ -30,12 +31,13 @@ type clause = ((string * prol_term list) * prem); type logic_program = clause list; type constant_table = (string * string) list - - val generate : bool -> Proof.context -> string -> (logic_program * constant_table) + + val generate : Predicate_Compile_Aux.mode option * bool -> + Proof.context -> string -> (logic_program * constant_table) val write_program : logic_program -> string - val run : (Time.time * prolog_system) -> 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 run : (Time.time * prolog_system) -> logic_program -> (string * prol_term list) -> string list -> int option -> prol_term list list + + val quickcheck : Proof.context -> term -> int -> term list option * (bool list * bool) val trace : bool Unsynchronized.ref @@ -53,44 +55,70 @@ (* code generation options *) -datatype prolog_system = SWI_PROLOG | YAP type code_options = {ensure_groundness : bool, limited_types : (typ * int) list, limited_predicates : (string list * int) list, replacing : ((string * string) * string) list, - manual_reorder : ((string * int) * int list) list, - timeout : Time.time, - prolog_system : prolog_system} + manual_reorder : ((string * int) * int list) list} + +fun set_ensure_groundness {ensure_groundness, limited_types, limited_predicates, + replacing, manual_reorder} = + {ensure_groundness = true, limited_types = limited_types, + limited_predicates = limited_predicates, replacing = replacing, + manual_reorder = manual_reorder} + +fun map_limit_predicates f {ensure_groundness, limited_types, limited_predicates, + replacing, manual_reorder} = + {ensure_groundness = ensure_groundness, limited_types = limited_types, + limited_predicates = f limited_predicates, replacing = replacing, + manual_reorder = manual_reorder} + structure Options = Theory_Data ( type T = code_options val empty = {ensure_groundness = false, - limited_types = [], limited_predicates = [], replacing = [], manual_reorder = [], - timeout = Time.fromSeconds 10, prolog_system = SWI_PROLOG} + limited_types = [], limited_predicates = [], replacing = [], manual_reorder = []} val extend = I; fun merge ({ensure_groundness = ensure_groundness1, limited_types = limited_types1, limited_predicates = limited_predicates1, replacing = replacing1, - manual_reorder = manual_reorder1, timeout = timeout1, prolog_system = prolog_system1}, + manual_reorder = manual_reorder1}, {ensure_groundness = ensure_groundness2, limited_types = limited_types2, limited_predicates = limited_predicates2, replacing = replacing2, - manual_reorder = manual_reorder2, timeout = timeout2, prolog_system = prolog_system2}) = + manual_reorder = manual_reorder2}) = {ensure_groundness = ensure_groundness1 orelse ensure_groundness2, limited_types = AList.merge (op =) (K true) (limited_types1, limited_types2), limited_predicates = AList.merge (op =) (K true) (limited_predicates1, limited_predicates2), manual_reorder = AList.merge (op =) (K true) (manual_reorder1, manual_reorder2), - replacing = Library.merge (op =) (replacing1, replacing2), - timeout = timeout1, - prolog_system = prolog_system1}; + replacing = Library.merge (op =) (replacing1, replacing2)}; ); val code_options_of = Options.get val map_code_options = Options.map +(* system configuration *) + +datatype prolog_system = SWI_PROLOG | YAP + +fun string_of_system SWI_PROLOG = "swiprolog" + | string_of_system YAP = "yap" + +type system_configuration = {timeout : Time.time, prolog_system : prolog_system} + +structure System_Config = Generic_Data +( + type T = system_configuration + val empty = {timeout = Time.fromSeconds 10, prolog_system = SWI_PROLOG} + val extend = I; + fun merge ({timeout = timeout1, prolog_system = prolog_system1}, + {timeout = timeout2, prolog_system = prolog_system2}) = + {timeout = timeout1, prolog_system = prolog_system1} +) + (* general string functions *) val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode; @@ -176,7 +204,6 @@ type constant_table = (string * string) list -(* assuming no clashing *) fun declare_consts consts constant_table = let fun update' c table = @@ -281,7 +308,6 @@ 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) @@ -316,18 +342,153 @@ tracing (cat_lines (map (fn const => "Constant " ^ const ^ "has intros:\n" ^ cat_lines (map (Display.string_of_thm ctxt) (Graph.get_node gr const))) consts)) - -fun generate ensure_groundness ctxt const = + +(* translation of moded predicates *) + +(** generating graph of moded predicates **) + +(* could be moved to Predicate_Compile_Core *) +fun requires_modes polarity cls = + let + fun req_mode_of pol (t, derivation) = + (case fst (strip_comb t) of + Const (c, _) => SOME (c, (pol, Predicate_Compile_Core.head_mode_of derivation)) + | _ => NONE) + fun req (Predicate_Compile_Aux.Prem t, derivation) = req_mode_of polarity (t, derivation) + | req (Predicate_Compile_Aux.Negprem t, derivation) = req_mode_of (not polarity) (t, derivation) + | req _ = NONE + in + maps (fn (_, prems) => map_filter req prems) cls + end + +structure Mode_Graph = Graph(type key = string * (bool * Predicate_Compile_Aux.mode) + val ord = prod_ord fast_string_ord (prod_ord bool_ord Predicate_Compile_Aux.mode_ord)); + +fun mk_moded_clauses_graph ctxt scc gr = + let + val options = Predicate_Compile_Aux.default_options + val mode_analysis_options = + {use_random = true, reorder_premises = true, infer_pos_and_neg_modes = true} + fun infer prednames (gr, (pos_modes, neg_modes, random)) = + let + val (lookup_modes, lookup_neg_modes, needs_random) = + ((fn s => the (AList.lookup (op =) pos_modes s)), + (fn s => the (AList.lookup (op =) neg_modes s)), + (fn s => member (op =) (the (AList.lookup (op =) random s)))) + val (preds, all_vs, param_vs, all_modes, clauses) = + Predicate_Compile_Core.prepare_intrs options ctxt prednames + (maps (Predicate_Compile_Core.intros_of ctxt) prednames) + val ((moded_clauses, random'), _) = + Predicate_Compile_Core.infer_modes mode_analysis_options options + (lookup_modes, lookup_neg_modes, needs_random) ctxt preds all_modes param_vs clauses + val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses + val pos_modes' = map (apsnd (map_filter (fn (true, m) => SOME m | _ => NONE))) modes + val neg_modes' = map (apsnd (map_filter (fn (false, m) => SOME m | _ => NONE))) modes + val _ = tracing ("Inferred modes:\n" ^ + cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map + (fn (p, m) => Predicate_Compile_Aux.string_of_mode m ^ (if p then "pos" else "neg")) ms)) modes)) + val gr' = gr + |> fold (fn (p, mps) => fold (fn (mode, cls) => + Mode_Graph.new_node ((p, mode), cls)) mps) + moded_clauses + |> fold (fn (p, mps) => fold (fn (mode, cls) => fold (fn req => + Mode_Graph.add_edge ((p, mode), req)) (requires_modes (fst mode) cls)) mps) + moded_clauses + in + (gr', (AList.merge (op =) (op =) (pos_modes, pos_modes'), + AList.merge (op =) (op =) (neg_modes, neg_modes'), + AList.merge (op =) (op =) (random, random'))) + end + in + fst (fold infer (rev scc) (Mode_Graph.empty, ([], [], []))) + end + +fun declare_moded_predicate moded_preds table = + let + fun update' (p as (pred, (pol, mode))) table = + if AList.defined (op =) table p then table else + let + val name = Long_Name.base_name pred ^ (if pol then "p" else "n") + ^ Predicate_Compile_Aux.ascii_string_of_mode mode + val p' = mk_conform first_lower "pred" (map snd table) name + in + AList.update (op =) (p, p') table + end + in + fold update' moded_preds table + end + +fun mk_program ctxt moded_gr moded_preds (prog, (moded_pred_table, constant_table)) = + let + val moded_pred_table' = declare_moded_predicate moded_preds moded_pred_table + fun mk_literal pol derivation constant_table' t = + let + val (p, args) = strip_comb t + val mode = Predicate_Compile_Core.head_mode_of derivation + val name = fst (dest_Const p) + + val p' = the (AList.lookup (op =) moded_pred_table' (name, (pol, mode))) + val args' = map (translate_term ctxt constant_table') args + in + Rel (p', args') + end + fun mk_prem pol (indprem, derivation) constant_table = + case indprem of + Predicate_Compile_Aux.Generator (s, T) => (Ground (s, T), constant_table) + | _ => + declare_consts (Term.add_const_names (Predicate_Compile_Aux.dest_indprem indprem) []) constant_table + |> (fn constant_table' => + (case indprem of Predicate_Compile_Aux.Negprem t => + NegRel_of (mk_literal (not pol) derivation constant_table' t) + | _ => + mk_literal pol derivation constant_table' (Predicate_Compile_Aux.dest_indprem indprem), constant_table')) + fun mk_clause pred_name pol (ts, prems) (prog, constant_table) = + let + val constant_table' = declare_consts (fold Term.add_const_names ts []) constant_table + val args = map (translate_term ctxt constant_table') ts + val (prems', constant_table'') = fold_map (mk_prem pol) prems constant_table' + in + (((pred_name, args), Conj prems') :: prog, constant_table'') + end + fun mk_clauses (pred, mode as (pol, _)) = + let + val clauses = Mode_Graph.get_node moded_gr (pred, mode) + val pred_name = the (AList.lookup (op =) moded_pred_table' (pred, mode)) + in + fold (mk_clause pred_name pol) clauses + end + in + apsnd (pair moded_pred_table') (fold mk_clauses moded_preds (prog, constant_table)) + end + +fun generate (use_modes, ensure_groundness) 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 _ = print_intros ctxt gr (flat scc) - val constant_table = declare_consts (flat scc) [] + val initial_constant_table = + declare_consts [@{const_name "Groups.zero_class.zero"}, @{const_name "Suc"}] [] in - apfst flat (fold_map (translate_intros ensure_groundness ctxt gr) (flat scc) constant_table) + case use_modes of + SOME mode => + let + val moded_gr = mk_moded_clauses_graph ctxt scc gr + val moded_gr' = Mode_Graph.subgraph + (member (op =) (Mode_Graph.all_succs moded_gr [(const, (true, mode))])) moded_gr + val scc = Mode_Graph.strong_conn moded_gr' + in + apfst rev (apsnd snd + (fold (mk_program ctxt moded_gr') (rev scc) ([], ([], initial_constant_table)))) + end + | NONE => + let + val _ = print_intros ctxt gr (flat scc) + val constant_table = declare_consts (flat scc) initial_constant_table + in + apfst flat (fold_map (translate_intros ensure_groundness ctxt gr) (flat scc) constant_table) + end end (* implementation for fully enumerating predicates and @@ -480,6 +641,7 @@ in fst (fold_map reorder' p []) end + (* rename variables to prolog-friendly names *) fun rename_vars_term renaming = map_vars (fn v => the (AList.lookup (op =) renaming v)) @@ -521,6 +683,7 @@ | write_prem (NotEq (l, r)) = write_term l ^ " \\= " ^ write_term r | write_prem (ArithEq (l, r)) = write_term l ^ " is " ^ write_term r | write_prem (NotArithEq (l, r)) = write_term l ^ " =\\= " ^ write_term r + | write_prem _ = raise Fail "Not a valid prolog premise" fun write_clause (head, prem) = write_rel head ^ (if prem = Conj [] then "." else " :- " ^ write_prem prem ^ ".") @@ -532,14 +695,14 @@ (** query and prelude for swi-prolog **) -fun swi_prolog_query_first rel vnames = - "eval :- once(" ^ rel ^ "(" ^ space_implode ", " vnames ^ ")),\n" ^ +fun swi_prolog_query_first (rel, args) vnames = + "eval :- once(" ^ rel ^ "(" ^ space_implode ", " (map write_term args) ^ ")),\n" ^ "writef('" ^ space_implode ";" (map (fn v => v ^ " = %w") vnames) ^ "\\n', [" ^ space_implode ", " vnames ^ "]).\n" -fun swi_prolog_query_firstn n rel vnames = +fun swi_prolog_query_firstn n (rel, args) vnames = "eval :- findnsols(" ^ string_of_int n ^ ", (" ^ space_implode ", " vnames ^ "), " ^ - rel ^ "(" ^ space_implode ", " vnames ^ "), Sols), writelist(Sols).\n" ^ + rel ^ "(" ^ space_implode ", " (map write_term args) ^ "), Sols), writelist(Sols).\n" ^ "writelist([]).\n" ^ "writelist([(" ^ space_implode ", " vnames ^ ")|T]) :- " ^ "writef('" ^ space_implode ";" (map (fn v => v ^ " = %w") vnames) ^ @@ -556,8 +719,8 @@ (** query and prelude for yap **) -fun yap_query_first rel vnames = - "eval :- once(" ^ rel ^ "(" ^ space_implode ", " vnames ^ ")),\n" ^ +fun yap_query_first (rel, args) vnames = + "eval :- once(" ^ rel ^ "(" ^ space_implode ", " (map write_term args) ^ ")),\n" ^ "format('" ^ space_implode ";" (map (fn v => v ^ " = ~w") vnames) ^ "\\n', [" ^ space_implode ", " vnames ^ "]).\n" @@ -580,9 +743,16 @@ fun invoke system file_name = let + val env_var = + (case system of SWI_PROLOG => "EXEC_SWIPL"| YAP => "EXEC_YAP") + val prog = getenv env_var val cmd = - case system of SWI_PROLOG => "/usr/local/bin/swipl -f " | YAP => "/usr/local/bin/yap -L " - in fst (bash_output (cmd ^ file_name)) end + case system of SWI_PROLOG => prog ^ " -f " | YAP => prog ^ " -L " + in + if prog = "" then + (warning (env_var ^ " not set; could not execute code for " ^ string_of_system system); "") + else fst (bash_output (cmd ^ file_name)) + end (* parsing prolog solution *) @@ -637,13 +807,14 @@ (* calling external interpreter and getting results *) -fun run (timeout, system) p query_rel vnames nsols = +fun run (timeout, system) p (query_rel, args) vnames nsols = let val p' = rename_vars_program p val _ = tracing "Renaming variable names..." - val renaming = fold mk_renaming vnames [] + val renaming = fold mk_renaming (fold add_vars args vnames) [] val vnames' = map (fn v => the (AList.lookup (op =) renaming v)) vnames - val prog = prelude system ^ query system nsols query_rel vnames' ^ write_program p' + val args' = map (rename_vars_term renaming) args + val prog = prelude system ^ query system nsols (query_rel, args') vnames' ^ write_program p' val _ = tracing ("Generated prolog program:\n" ^ prog) val solution = TimeLimit.timeLimit timeout (fn prog => Cache_IO.with_tmp_file "prolog_file" (fn prolog_file => (File.write prolog_file prog; invoke system (Path.implode prolog_file)))) prog @@ -672,6 +843,17 @@ map (restore_term ctxt constant_table) (args ~~ argsT')) end + +(* restore numerals in natural numbers *) + +fun restore_nat_numerals t = + if fastype_of t = @{typ nat} andalso is_some (try HOLogic.dest_nat t) then + HOLogic.mk_number @{typ nat} (HOLogic.dest_nat t) + else + (case t of + t1 $ t2 => restore_nat_numerals t1 $ restore_nat_numerals t2 + | t => t) + (* values command *) val preprocess_options = Predicate_Compile_Aux.Options { @@ -711,10 +893,6 @@ case strip_comb body of (Const (name, T), all_args) => (Const (name, T), all_args) | (head, _) => error ("Not a constant: " ^ Syntax.string_of_term ctxt head) - val vnames = - 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) @@ -723,16 +901,19 @@ |> Predicate_Compile.preprocess preprocess_options t val ctxt' = ProofContext.init_global thy' val _ = tracing "Generating prolog program..." - val (p, constant_table) = generate (#ensure_groundness options) ctxt' name + val (p, constant_table) = generate (NONE, #ensure_groundness options) ctxt' name (* FIXME *) |> (if #ensure_groundness options then add_ground_predicates ctxt' (#limited_types options) else I) |> add_limited_predicates (#limited_predicates options) |> apfst (fold replace (#replacing options)) |> apfst (reorder_manually (#manual_reorder options)) + val constant_table' = declare_consts (fold Term.add_const_names all_args []) constant_table + val args' = map (translate_term ctxt constant_table') all_args val _ = tracing "Running prolog program..." - val tss = run (#timeout options, #prolog_system options) - p (translate_const constant_table name) (map first_upper vnames) soln + val system_config = System_Config.get (Context.Proof ctxt) + val tss = run (#timeout system_config, #prolog_system system_config) + p (translate_const constant_table' name, args') output_names soln val _ = tracing "Restoring terms..." val empty = Const("Orderings.bot_class.bot", fastype_of t_compr) fun mk_insert x S = @@ -759,7 +940,8 @@ 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_nat_numerals o restore_term ctxt' constant_table) (ts ~~ Ts))) tss) []) end fun values_cmd print_modes soln raw_t state = @@ -798,7 +980,7 @@ fun strip_horn A = (strip_imp_prems A, strip_imp_concl A); -fun quickcheck ctxt report t size = +fun quickcheck ctxt t size = let val options = code_options_of (ProofContext.theory_of ctxt) val thy = Theory.copy (ProofContext.theory_of ctxt) @@ -821,14 +1003,15 @@ 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 true ctxt' full_constname + val (p, constant_table) = generate (NONE, true) ctxt' full_constname |> add_ground_predicates ctxt' (#limited_types options) |> add_limited_predicates (#limited_predicates options) |> apfst (fold replace (#replacing options)) |> apfst (reorder_manually (#manual_reorder options)) val _ = tracing "Running prolog program..." - val tss = run (#timeout options, #prolog_system options) - p (translate_const constant_table full_constname) (map fst vs') (SOME 1) + val system_config = System_Config.get (Context.Proof ctxt) + val tss = run (#timeout system_config, #prolog_system system_config) + p (translate_const constant_table full_constname, map (Var o fst) vs') (map fst vs') (SOME 1) val _ = tracing "Restoring terms..." val res = case tss of diff -r 8bc560df99ea -r fd1032c23cdf src/HOL/Tools/Predicate_Compile/etc/settings --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Predicate_Compile/etc/settings Thu Sep 16 17:51:16 2010 +0200 @@ -0,0 +1,13 @@ + +EXEC_SWIPL=$(choosefrom \ + "$ISABELLE_HOME/contrib/swipl/bin/swipl" \ + "$ISABELLE_HOME/contrib_devel/swipl/bin/swipl" \ + "$ISABELLE_HOME/../swipl" \ + $(type -p swipl) \ + "") + +EXEC_YAP=$(choosefrom \ + "$ISABELLE_HOME/contrib/yap" \ + "$ISABELLE_HOME/../yap" \ + $(type -p yap) \ + "") diff -r 8bc560df99ea -r fd1032c23cdf src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Sep 16 16:51:44 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Sep 16 17:51:16 2010 +0200 @@ -71,6 +71,7 @@ type mode_analysis_options = {use_random : bool, reorder_premises : bool, infer_pos_and_neg_modes : bool} datatype mode_derivation = Mode_App of mode_derivation * mode_derivation | Context of mode | Mode_Pair of mode_derivation * mode_derivation | Term of mode + val head_mode_of : mode_derivation -> mode type moded_clause = term list * (Predicate_Compile_Aux.indprem * mode_derivation) list type 'a pred_mode_table = (string * ((bool * mode) * 'a) list) list diff -r 8bc560df99ea -r fd1032c23cdf src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Thu Sep 16 16:51:44 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Thu Sep 16 17:51:16 2010 +0200 @@ -333,11 +333,20 @@ ((full_constname, [definition])::new_defs, thy')) end | replace_abs_arg arg (new_defs, thy) = - if (is_predT (fastype_of arg)) then + if is_some (try HOLogic.dest_prodT (fastype_of arg)) then + (case try HOLogic.dest_prod arg of + SOME (t1, t2) => + (new_defs, thy) + |> process constname t1 + ||>> process constname t2 + |>> HOLogic.mk_prod + | NONE => (warning ("Replacing higher order arguments " ^ + "is not applied in an undestructable product type"); (arg, (new_defs, thy)))) + else if (is_predT (fastype_of arg)) then process constname arg (new_defs, thy) else (arg, (new_defs, thy)) - + val (args', (new_defs', thy')) = fold_map replace_abs_arg (map Envir.beta_eta_contract args) (new_defs, thy) in