--- a/etc/components Thu Sep 16 17:31:51 2010 +0200
+++ b/etc/components Thu Sep 16 17:52:00 2010 +0200
@@ -17,3 +17,4 @@
src/HOL/Mirabelle
src/HOL/Library/Sum_Of_Squares
src/HOL/Tools/SMT
+src/HOL/Tools/Predicate_Compile
--- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Thu Sep 16 17:31:51 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Thu Sep 16 17:52:00 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}"
--- a/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy Thu Sep 16 17:31:51 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy Thu Sep 16 17:52:00 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 \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> 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:
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Thu Sep 16 17:31:51 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Thu Sep 16 17:52:00 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 "\<lbrakk> hotel s; g \<in> isin s r \<rbrakk> \<Longrightarrow> 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 \<in> isin s r ==> owns s r = Some g"
--- a/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy Thu Sep 16 17:31:51 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy Thu Sep 16 17:52:00 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
"\<Gamma> \<turnstile> t : U \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> \<Gamma> \<turnstile> t' : U"
--- a/src/HOL/Predicate_Compile_Examples/List_Examples.thy Thu Sep 16 17:31:51 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/List_Examples.thy Thu Sep 16 17:52:00 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]
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Thu Sep 16 17:31:51 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Thu Sep 16 17:52:00 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). \<exists>s1 s2 lhs rhs.
+ (s1 @ [NTS lhs] @ s2 = lsl) \<and>
+ (s1 @ rhs @ s2) = rsl \<and>
+ (rule lhs rhs) \<in> 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 \<Rightarrow> 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) \<in> (derives example_grammar)^* }"
+
+code_pred [inductify, skip_proof] test2 .
+
+values "{rhs. test2 rhs}"
+
+
section {* Examples for detecting switches *}
inductive detect_switches1 where
--- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Thu Sep 16 17:31:51 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Thu Sep 16 17:52:00 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. *}
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Sep 16 17:31:51 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Sep 16 17:52:00 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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Predicate_Compile/etc/settings Thu Sep 16 17:52:00 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) \
+ "")
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Sep 16 17:31:51 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Sep 16 17:52:00 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
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Thu Sep 16 17:31:51 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Thu Sep 16 17:52:00 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