--- a/doc-src/TutorialI/Datatype/Nested.thy Fri Oct 01 15:45:56 2010 +0200
+++ b/doc-src/TutorialI/Datatype/Nested.thy Fri Oct 01 16:13:28 2010 +0200
@@ -111,14 +111,13 @@
(* Exercise 2: *)
-consts trev :: "('v,'f) term \<Rightarrow> ('v,'f) term"
- trevs:: "('v,'f) term list \<Rightarrow> ('v,'f) term list"
-primrec
-"trev (Var v) = Var v"
-"trev (App f ts) = App f (trevs ts)"
-
-"trevs [] = []"
-"trevs (t#ts) = (trevs ts) @ [(trev t)]"
+primrec trev :: "('v,'f) term \<Rightarrow> ('v,'f) term"
+ and trevs:: "('v,'f) term list \<Rightarrow> ('v,'f) term list"
+where
+ "trev (Var v) = Var v"
+| "trev (App f ts) = App f (trevs ts)"
+| "trevs [] = []"
+| "trevs (t#ts) = (trevs ts) @ [(trev t)]"
lemma [simp]: "\<forall> ys. trevs (xs @ ys) = (trevs ys) @ (trevs xs)"
apply (induct_tac xs, auto)
--- a/doc-src/TutorialI/Inductive/Advanced.thy Fri Oct 01 15:45:56 2010 +0200
+++ b/doc-src/TutorialI/Inductive/Advanced.thy Fri Oct 01 16:13:28 2010 +0200
@@ -1,4 +1,3 @@
-(* ID: $Id$ *)
(*<*)theory Advanced imports Even uses "../../antiquote_setup.ML" begin(*>*)
text {*
@@ -360,11 +359,12 @@
(*<*)
text{*the following declaration isn't actually used*}
-consts integer_arity :: "integer_op \<Rightarrow> nat"
primrec
-"integer_arity (Number n) = 0"
-"integer_arity UnaryMinus = 1"
-"integer_arity Plus = 2"
+ integer_arity :: "integer_op \<Rightarrow> nat"
+where
+ "integer_arity (Number n) = 0"
+| "integer_arity UnaryMinus = 1"
+| "integer_arity Plus = 2"
text{* the rest isn't used: too complicated. OK for an exercise though.*}
--- a/doc-src/TutorialI/Protocol/Event.thy Fri Oct 01 15:45:56 2010 +0200
+++ b/doc-src/TutorialI/Protocol/Event.thy Fri Oct 01 16:13:28 2010 +0200
@@ -23,24 +23,15 @@
consts
bad :: "agent set" -- {* compromised agents *}
- knows :: "agent => event list => msg set"
text{*The constant "spies" is retained for compatibility's sake*}
-abbreviation (input)
- spies :: "event list => msg set" where
- "spies == knows Spy"
-
-text{*Spy has access to his own key for spoof messages, but Server is secure*}
-specification (bad)
- Spy_in_bad [iff]: "Spy \<in> bad"
- Server_not_bad [iff]: "Server \<notin> bad"
- by (rule exI [of _ "{Spy}"], simp)
-
primrec
+ knows :: "agent => event list => msg set"
+where
knows_Nil: "knows A [] = initState A"
- knows_Cons:
+| knows_Cons:
"knows A (ev # evs) =
(if A = Spy then
(case ev of
@@ -57,20 +48,29 @@
| Notes A' X =>
if A'=A then insert X (knows A evs) else knows A evs))"
+abbreviation (input)
+ spies :: "event list => msg set" where
+ "spies == knows Spy"
+
+text{*Spy has access to his own key for spoof messages, but Server is secure*}
+specification (bad)
+ Spy_in_bad [iff]: "Spy \<in> bad"
+ Server_not_bad [iff]: "Server \<notin> bad"
+ by (rule exI [of _ "{Spy}"], simp)
+
(*
Case A=Spy on the Gets event
enforces the fact that if a message is received then it must have been sent,
therefore the oops case must use Notes
*)
-consts
+primrec
(*Set of items that might be visible to somebody:
complement of the set of fresh items*)
used :: "event list => msg set"
-
-primrec
+where
used_Nil: "used [] = (UN B. parts (initState B))"
- used_Cons: "used (ev # evs) =
+| used_Cons: "used (ev # evs) =
(case ev of
Says A B X => parts {X} \<union> used evs
| Gets A X => used evs
--- a/doc-src/TutorialI/Protocol/Public.thy Fri Oct 01 15:45:56 2010 +0200
+++ b/doc-src/TutorialI/Protocol/Public.thy Fri Oct 01 16:13:28 2010 +0200
@@ -22,14 +22,19 @@
abbreviation priK :: "agent \<Rightarrow> key"
where "priK x \<equiv> invKey(pubK x)"
(*<*)
-primrec
+overloading initState \<equiv> initState
+begin
+
+primrec initState where
(*Agents know their private key and all public keys*)
initState_Server: "initState Server =
insert (Key (priK Server)) (Key ` range pubK)"
- initState_Friend: "initState (Friend i) =
+| initState_Friend: "initState (Friend i) =
insert (Key (priK (Friend i))) (Key ` range pubK)"
- initState_Spy: "initState Spy =
+| initState_Spy: "initState Spy =
(Key`invKey`pubK`bad) Un (Key ` range pubK)"
+
+end
(*>*)
text {*
--- a/doc-src/TutorialI/Sets/Examples.thy Fri Oct 01 15:45:56 2010 +0200
+++ b/doc-src/TutorialI/Sets/Examples.thy Fri Oct 01 16:13:28 2010 +0200
@@ -95,8 +95,8 @@
text{*
set extensionality
-@{thm[display] set_ext[no_vars]}
-\rulename{set_ext}
+@{thm[display] set_eqI[no_vars]}
+\rulename{set_eqI}
@{thm[display] equalityI[no_vars]}
\rulename{equalityI}
--- a/doc-src/TutorialI/Sets/Functions.thy Fri Oct 01 15:45:56 2010 +0200
+++ b/doc-src/TutorialI/Sets/Functions.thy Fri Oct 01 16:13:28 2010 +0200
@@ -66,20 +66,18 @@
\rulename{o_inv_distrib}
*}
-
-
text{*
small sample proof
@{thm[display] ext[no_vars]}
\rulename{ext}
-@{thm[display] expand_fun_eq[no_vars]}
-\rulename{expand_fun_eq}
+@{thm[display] fun_eq_iff[no_vars]}
+\rulename{fun_eq_iff}
*}
lemma "inj f \<Longrightarrow> (f o g = f o h) = (g = h)";
- apply (simp add: expand_fun_eq inj_on_def)
+ apply (simp add: fun_eq_iff inj_on_def)
apply (auto)
done
--- a/src/HOL/Code_Numeral.thy Fri Oct 01 15:45:56 2010 +0200
+++ b/src/HOL/Code_Numeral.thy Fri Oct 01 16:13:28 2010 +0200
@@ -340,7 +340,7 @@
(OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)")
(Haskell "divMod")
(Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))")
- (Eval "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
+ (Eval "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (Integer.div'_mod n m))")
code_const "HOL.equal \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
(SML "!((_ : Int.int) = _)")
--- a/src/HOL/Library/More_List.thy Fri Oct 01 15:45:56 2010 +0200
+++ b/src/HOL/Library/More_List.thy Fri Oct 01 16:13:28 2010 +0200
@@ -100,8 +100,6 @@
"fold plus xs = plus (listsum (rev xs))"
by (induct xs) (simp_all add: add.assoc)
-declare listsum_foldl [code del]
-
lemma (in monoid_add) listsum_conv_fold [code]:
"listsum xs = fold (\<lambda>x y. y + x) xs 0"
by (auto simp add: listsum_foldl foldl_fold fun_eq_iff)
--- a/src/HOL/Nat.thy Fri Oct 01 15:45:56 2010 +0200
+++ b/src/HOL/Nat.thy Fri Oct 01 16:13:28 2010 +0200
@@ -149,11 +149,10 @@
primrec minus_nat
where
- diff_0: "m - 0 = (m\<Colon>nat)"
- | diff_Suc: "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
+ diff_0 [code]: "m - 0 = (m\<Colon>nat)"
+| diff_Suc: "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
declare diff_Suc [simp del]
-declare diff_0 [code]
lemma diff_0_eq_0 [simp, code]: "0 - n = (0::nat)"
by (induct n) (simp_all add: diff_Suc)
--- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Fri Oct 01 15:45:56 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Fri Oct 01 16:13:28 2010 +0200
@@ -12,6 +12,7 @@
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = false,
+ limit_globally = NONE,
limited_types = [],
limited_predicates = [],
replacing = [],
@@ -25,6 +26,7 @@
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = false,
+ limit_globally = NONE,
limited_types = [],
limited_predicates = [],
replacing = [],
@@ -34,6 +36,7 @@
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = false,
+ limit_globally = NONE,
limited_types = [],
limited_predicates = [],
replacing = [],
@@ -202,6 +205,7 @@
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = true,
+ limit_globally = NONE,
limited_types = [],
limited_predicates = [],
replacing = [],
--- a/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy Fri Oct 01 15:45:56 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy Fri Oct 01 16:13:28 2010 +0200
@@ -58,6 +58,7 @@
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = true,
+ limit_globally = NONE,
limited_types = [],
limited_predicates = [(["s1", "a1", "b1"], 2)],
replacing = [(("s1", "limited_s1"), "quickcheck")],
@@ -81,6 +82,7 @@
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = true,
+ limit_globally = NONE,
limited_types = [],
limited_predicates = [(["s2", "a2", "b2"], 3)],
replacing = [(("s2", "limited_s2"), "quickcheck")],
@@ -103,6 +105,7 @@
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = true,
+ limit_globally = NONE,
limited_types = [],
limited_predicates = [(["s3", "a3", "b3"], 6)],
replacing = [(("s3", "limited_s3"), "quickcheck")],
@@ -117,6 +120,7 @@
(*
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = true,
+ limit_globally = NONE,
limited_types = [],
limited_predicates = [],
replacing = [],
@@ -143,6 +147,7 @@
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = true,
+ limit_globally = NONE,
limited_types = [],
limited_predicates = [(["s4", "a4", "b4"], 6)],
replacing = [(("s4", "limited_s4"), "quickcheck")],
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Fri Oct 01 15:45:56 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Fri Oct 01 16:13:28 2010 +0200
@@ -86,6 +86,7 @@
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = true,
+ limit_globally = NONE,
limited_types = [],
limited_predicates = [],
replacing = [],
@@ -97,7 +98,7 @@
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]
+(*quickcheck[generator = code, iterations = 100000, report]*)
quickcheck[generator = prolog, iterations = 1, expect = counterexample]
oops
@@ -112,8 +113,24 @@
s = s\<^isub>3 @ [Enter g r c] @ s\<^isub>2 @ [Check_in g r c'] @ s\<^isub>1 \<and>
no_Check_in (s\<^isub>3 @ s\<^isub>2) r \<and> isin (s\<^isub>2 @ [Check_in g r c] @ s\<^isub>1) r = {})"
+section {* Manual setup to find the counterexample *}
+
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = true,
+ limit_globally = NONE,
+ limited_types = [],
+ limited_predicates = [(["hotel"], 4)],
+ replacing = [(("hotel", "limited_hotel"), "quickcheck")],
+ manual_reorder = []}) *}
+
+lemma
+ "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
+quickcheck[generator = prolog, iterations = 1, expect = no_counterexample]
+oops
+
+setup {* Code_Prolog.map_code_options (K
+ {ensure_groundness = true,
+ limit_globally = NONE,
limited_types = [],
limited_predicates = [(["hotel"], 5)],
replacing = [(("hotel", "limited_hotel"), "quickcheck")],
@@ -124,4 +141,75 @@
quickcheck[generator = prolog, iterations = 1, expect = counterexample]
oops
+section {* Simulating a global depth limit manually by limiting all predicates *}
+
+setup {*
+ Code_Prolog.map_code_options (K
+ {ensure_groundness = true,
+ limit_globally = NONE,
+ limited_types = [],
+ limited_predicates = [(["feelssafe", "feelssafeaux", "noCheckin", "noCheckinaux", "appendP", "ownsP", "hotel", "hotelaux", "hotelauxaux", "roomkP", "issued", "currkP", "initkP",
+ "cards", "cardsauxauxaux", "cardsauxaux", "cardsaux", "isin", "isinauxauxa", "isinauxauxaux", "isinauxaux", "isinaux", "set"], 12)],
+ replacing = [(("hotel", "limited_hotel"), "quickcheck"), (("feelssafe", "limited_feelssafe"), "quickcheck"), (("isin", "limited_isin"), "quickcheck")],
+ manual_reorder = []})
+*}
+
+lemma
+ "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
+quickcheck[generator = prolog, iterations = 1, expect = no_counterexample]
+oops
+
+
+setup {*
+ Code_Prolog.map_code_options (K
+ {ensure_groundness = true,
+ limit_globally = NONE,
+ limited_types = [],
+ limited_predicates = [(["feelssafe", "feelssafeaux", "noCheckin", "noCheckinaux", "appendP", "ownsP", "hotel", "hotelaux", "hotelauxaux", "roomkP", "issued", "currkP", "initkP",
+ "cards", "cardsauxauxaux", "cardsauxaux", "cardsaux", "isin", "isinauxauxa", "isinauxauxaux", "isinauxaux", "isinaux", "set"], 13)],
+ replacing = [(("hotel", "limited_hotel"), "quickcheck"), (("feelssafe", "limited_feelssafe"), "quickcheck"), (("isin", "limited_isin"), "quickcheck")],
+ manual_reorder = []})
+*}
+
+lemma
+ "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
+quickcheck[generator = prolog, iterations = 1, expect = counterexample]
+oops
+
+section {* Using a global limit for limiting the execution *}
+
+text {* A global depth limit of 13 does not suffice to find the counterexample. *}
+
+setup {*
+ Code_Prolog.map_code_options (K
+ {ensure_groundness = true,
+ limit_globally = SOME 13,
+ limited_types = [],
+ limited_predicates = [],
+ replacing = [],
+ manual_reorder = []})
+*}
+
+lemma
+ "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
+quickcheck[generator = prolog, iterations = 1, expect = no_counterexample]
+oops
+
+text {* But a global depth limit of 14 does. *}
+
+setup {*
+ Code_Prolog.map_code_options (K
+ {ensure_groundness = true,
+ limit_globally = SOME 14,
+ limited_types = [],
+ limited_predicates = [],
+ replacing = [],
+ manual_reorder = []})
+*}
+
+lemma
+ "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
+quickcheck[generator = prolog, iterations = 1, expect = counterexample]
+oops
+
end
\ No newline at end of file
--- a/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy Fri Oct 01 15:45:56 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy Fri Oct 01 16:13:28 2010 +0200
@@ -83,6 +83,7 @@
setup {* Code_Prolog.map_code_options (K
{ ensure_groundness = true,
+ limit_globally = NONE,
limited_types = [(@{typ nat}, 1), (@{typ "type"}, 1), (@{typ dB}, 1), (@{typ "type list"}, 1)],
limited_predicates = [(["typing"], 2), (["nthel1"], 2)],
replacing = [(("typing", "limited_typing"), "quickcheck"),
--- a/src/HOL/Predicate_Compile_Examples/List_Examples.thy Fri Oct 01 15:45:56 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/List_Examples.thy Fri Oct 01 16:13:28 2010 +0200
@@ -6,6 +6,7 @@
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = true,
+ limit_globally = NONE,
limited_types = [(@{typ nat}, 2), (@{typ "nat list"}, 4)],
limited_predicates = [(["appendP"], 4), (["revP"], 4)],
replacing =
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Fri Oct 01 15:45:56 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Fri Oct 01 16:13:28 2010 +0200
@@ -1538,5 +1538,11 @@
code_pred implies_itself .
+text {* Case expressions *}
+
+definition
+ "map_pairs xs ys = (map (%((a, b), c). (a, b, c)) xs = ys)"
+
+code_pred [inductify] map_pairs .
end
--- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Fri Oct 01 15:45:56 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Fri Oct 01 16:13:28 2010 +0200
@@ -100,6 +100,7 @@
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = true,
+ limit_globally = NONE,
limited_types = [(@{typ Sym}, 0), (@{typ "Sym list"}, 2), (@{typ RE}, 6)],
limited_predicates = [(["repIntPa"], 2), (["repP"], 2), (["subP"], 0),
(["accepts", "acceptsaux", "seqSplit", "seqSplita", "seqSplitaux", "seqSplitb"], 25)],
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Oct 01 15:45:56 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Oct 01 16:13:28 2010 +0200
@@ -9,6 +9,7 @@
datatype prolog_system = SWI_PROLOG | YAP
type code_options =
{ensure_groundness : bool,
+ limit_globally : int option,
limited_types : (typ * int) list,
limited_predicates : (string list * int) list,
replacing : ((string * string) * string) list,
@@ -58,38 +59,45 @@
type code_options =
{ensure_groundness : bool,
+ limit_globally : int option,
limited_types : (typ * int) list,
limited_predicates : (string list * int) list,
replacing : ((string * string) * string) list,
manual_reorder : ((string * int) * int list) list}
-fun set_ensure_groundness {ensure_groundness, limited_types, limited_predicates,
+fun set_ensure_groundness {ensure_groundness, limit_globally, limited_types, limited_predicates,
replacing, manual_reorder} =
- {ensure_groundness = true, limited_types = limited_types,
+ {ensure_groundness = true, limit_globally = limit_globally, 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,
+fun map_limit_predicates f {ensure_groundness, limit_globally, limited_types, limited_predicates,
replacing, manual_reorder} =
- {ensure_groundness = ensure_groundness, limited_types = limited_types,
+ {ensure_groundness = ensure_groundness, limit_globally = limit_globally, limited_types = limited_types,
limited_predicates = f limited_predicates, replacing = replacing,
manual_reorder = manual_reorder}
-
+
+fun merge_global_limit (NONE, NONE) = NONE
+ | merge_global_limit (NONE, SOME n) = SOME n
+ | merge_global_limit (SOME n, NONE) = SOME n
+ | merge_global_limit (SOME n, SOME m) = SOME (Int.max (n, m))
+
structure Options = Theory_Data
(
type T = code_options
- val empty = {ensure_groundness = false,
+ val empty = {ensure_groundness = false, limit_globally = NONE,
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},
- {ensure_groundness = ensure_groundness2, limited_types = limited_types2,
- limited_predicates = limited_predicates2, replacing = replacing2,
- manual_reorder = manual_reorder2}) =
+ ({ensure_groundness = ensure_groundness1, limit_globally = limit_globally1,
+ limited_types = limited_types1, limited_predicates = limited_predicates1,
+ replacing = replacing1, manual_reorder = manual_reorder1},
+ {ensure_groundness = ensure_groundness2, limit_globally = limit_globally2,
+ limited_types = limited_types2, limited_predicates = limited_predicates2,
+ replacing = replacing2, manual_reorder = manual_reorder2}) =
{ensure_groundness = ensure_groundness1 orelse ensure_groundness2,
+ limit_globally = merge_global_limit (limit_globally1, limit_globally2),
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),
@@ -188,7 +196,7 @@
type clause = ((string * prol_term list) * prem);
type logic_program = clause list;
-
+
(* translation from introduction rules to internal representation *)
fun mk_conform f empty avoid name =
@@ -591,13 +599,14 @@
((mk_lim_rel_name rel_name, (Var "Lim") :: ts), prem)
end
-fun add_limited_predicates limited_predicates =
+fun nat_term_of n = funpow n (fn t => AppF ("suc", [t])) (Cons "zero")
+
+fun add_limited_predicates limited_predicates (p, constant_table) =
let
- fun add (rel_names, limit) (p, constant_table) =
+ fun add (rel_names, limit) p =
let
val clauses = filter (fn ((rel, _), _) => member (op =) rel_names rel) p
val clauses' = map (mk_depth_limited rel_names) clauses
- fun nat_term_of n = funpow n (fn t => AppF ("suc", [t])) (Cons "zero")
fun mk_entry_clause rel_name =
let
val nargs = length (snd (fst
@@ -606,9 +615,9 @@
in
(("limited_" ^ rel_name, vars), Rel ("lim_" ^ rel_name, nat_term_of limit :: vars))
end
- in (p @ (map mk_entry_clause rel_names) @ clauses', constant_table) end
+ in (p @ (map mk_entry_clause rel_names) @ clauses') end
in
- fold add limited_predicates
+ (fold add limited_predicates p, constant_table)
end
@@ -663,10 +672,29 @@
val rename_vars_program = map rename_vars_clause
+(* limit computation globally by some threshold *)
+
+fun limit_globally ctxt limit const_name (p, constant_table) =
+ let
+ val rel_names = fold (fn ((r, _), _) => insert (op =) r) p []
+ val p' = map (mk_depth_limited rel_names) p
+ val rel_name = translate_const constant_table const_name
+ val nargs = length (snd (fst
+ (the (find_first (fn ((rel, _), _) => rel = rel_name) p))))
+ val vars = map (fn i => Var ("x" ^ string_of_int i)) (1 upto nargs)
+ val entry_clause = ((rel_name, vars), Rel ("lim_" ^ rel_name, nat_term_of limit :: vars))
+ val p'' = filter_out (fn ((rel, _), _) => rel = rel_name) p
+ in
+ (entry_clause :: p' @ p'', constant_table)
+ end
+
(* post processing of generated prolog program *)
-fun post_process ctxt options (p, constant_table) =
+fun post_process ctxt options const_name (p, constant_table) =
(p, constant_table)
+ |> (case #limit_globally options of
+ SOME limit => limit_globally ctxt limit const_name
+ | NONE => I)
|> (if #ensure_groundness options then
add_ground_predicates ctxt (#limited_types options)
else I)
@@ -915,7 +943,7 @@
val ctxt' = ProofContext.init_global thy'
val _ = tracing "Generating prolog program..."
val (p, constant_table) = generate (NONE, #ensure_groundness options) ctxt' name (* FIXME *)
- |> post_process ctxt' options
+ |> post_process ctxt' options name
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..."
@@ -991,7 +1019,7 @@
val ctxt' = ProofContext.init_global thy3
val _ = tracing "Generating prolog program..."
val (p, constant_table) = generate (NONE, true) ctxt' full_constname
- |> post_process ctxt' (set_ensure_groundness options)
+ |> post_process ctxt' (set_ensure_groundness options) full_constname
val _ = tracing "Running prolog program..."
val system_config = System_Config.get (Context.Proof ctxt)
val tss = run (#timeout system_config, #prolog_system system_config)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Oct 01 15:45:56 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Oct 01 16:13:28 2010 +0200
@@ -147,6 +147,7 @@
(* simple transformations *)
val split_conjuncts_in_assms : Proof.context -> thm -> thm
val expand_tuples : theory -> thm -> thm
+ val case_betapply : theory -> term -> term
val eta_contract_ho_arguments : theory -> thm -> thm
val remove_equalities : theory -> thm -> thm
val remove_pointless_clauses : thm -> thm list
@@ -859,6 +860,85 @@
intro'''''
end
+(** making case distributivity rules **)
+(*** this should be part of the datatype package ***)
+
+fun datatype_names_of_case_name thy case_name =
+ map (#1 o #2) (#descr (the (Datatype_Data.info_of_case thy case_name)))
+
+fun make_case_distribs new_type_names descr sorts thy =
+ let
+ val case_combs = Datatype_Prop.make_case_combs new_type_names descr sorts thy "f";
+ fun make comb =
+ let
+ val Type ("fun", [T, T']) = fastype_of comb;
+ val (Const (case_name, _), fs) = strip_comb comb
+ val used = Term.add_tfree_names comb []
+ val U = TFree (Name.variant used "'t", HOLogic.typeS)
+ val x = Free ("x", T)
+ val f = Free ("f", T' --> U)
+ fun apply_f f' =
+ let
+ val Ts = binder_types (fastype_of f')
+ val bs = map Bound ((length Ts - 1) downto 0)
+ in
+ fold (curry absdummy) (rev Ts) (f $ (list_comb (f', bs)))
+ end
+ val fs' = map apply_f fs
+ val case_c' = Const (case_name, (map fastype_of fs') @ [T] ---> U)
+ in
+ HOLogic.mk_eq (f $ (comb $ x), list_comb (case_c', fs') $ x)
+ end
+ in
+ map make case_combs
+ end
+
+fun case_rewrites thy Tcon =
+ let
+ val info = Datatype.the_info thy Tcon
+ val descr = #descr info
+ val sorts = #sorts info
+ val typ_names = the_default [Tcon] (#alt_names info)
+ in
+ map (Drule.export_without_context o Skip_Proof.make_thm thy o HOLogic.mk_Trueprop)
+ (make_case_distribs typ_names [descr] sorts thy)
+ end
+
+fun instantiated_case_rewrites thy Tcon =
+ let
+ val rew_ths = case_rewrites thy Tcon
+ val ctxt = ProofContext.init_global thy
+ fun instantiate th =
+ let
+ val f = (fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th))))))
+ val Type ("fun", [uninst_T, uninst_T']) = fastype_of f
+ val ([tname, tname', uname, yname], ctxt') = Variable.add_fixes ["'t", "'t'", "'u", "y"] ctxt
+ val T = TFree (tname, HOLogic.typeS)
+ val T' = TFree (tname', HOLogic.typeS)
+ val U = TFree (uname, HOLogic.typeS)
+ val y = Free (yname, U)
+ val f' = absdummy (U --> T', Bound 0 $ y)
+ val th' = Thm.certify_instantiate
+ ([(dest_TVar uninst_T, U --> T'), (dest_TVar uninst_T', T')],
+ [((fst (dest_Var f), (U --> T') --> T'), f')]) th
+ val [th'] = Variable.export ctxt' ctxt [th']
+ in
+ th'
+ end
+ in
+ map instantiate rew_ths
+ end
+
+fun case_betapply thy t =
+ let
+ val case_name = fst (dest_Const (fst (strip_comb t)))
+ val Tcons = datatype_names_of_case_name thy case_name
+ val ths = maps (instantiated_case_rewrites thy) Tcons
+ in
+ MetaSimplifier.rewrite_term thy
+ (map (fn th => th RS @{thm eq_reflection}) ths) [] t
+ end
+
(*** conversions ***)
fun imp_prems_conv cv ct =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Fri Oct 01 15:45:56 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Fri Oct 01 16:13:28 2010 +0200
@@ -185,10 +185,9 @@
val (f, args) = strip_comb t
val split_thm = prepare_split_thm (ProofContext.init_global thy) raw_split_thm
val (assms, concl) = Logic.strip_horn (prop_of split_thm)
- val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl)
- val subst = Pattern.match thy (split_t, t) (Vartab.empty, Vartab.empty)
- val (_, split_args) = strip_comb split_t
- val match = split_args ~~ args
+ val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl)
+ val t' = case_betapply thy t
+ val subst = Pattern.match thy (split_t, t') (Vartab.empty, Vartab.empty)
fun flatten_of_assm assm =
let
val (vTs, assm') = strip_all (Envir.beta_norm (Envir.subst_term subst assm))
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Fri Oct 01 15:45:56 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Fri Oct 01 16:13:28 2010 +0200
@@ -19,73 +19,6 @@
open Predicate_Compile_Aux
-
-fun datatype_names_of_case_name thy case_name =
- map (#1 o #2) (#descr (the (Datatype_Data.info_of_case thy case_name)))
-
-fun make_case_distribs new_type_names descr sorts thy =
- let
- val case_combs = Datatype_Prop.make_case_combs new_type_names descr sorts thy "f";
- fun make comb =
- let
- val Type ("fun", [T, T']) = fastype_of comb;
- val (Const (case_name, _), fs) = strip_comb comb
- val used = Term.add_tfree_names comb []
- val U = TFree (Name.variant used "'t", HOLogic.typeS)
- val x = Free ("x", T)
- val f = Free ("f", T' --> U)
- fun apply_f f' =
- let
- val Ts = binder_types (fastype_of f')
- val bs = map Bound ((length Ts - 1) downto 0)
- in
- fold (curry absdummy) (rev Ts) (f $ (list_comb (f', bs)))
- end
- val fs' = map apply_f fs
- val case_c' = Const (case_name, (map fastype_of fs') @ [T] ---> U)
- in
- HOLogic.mk_eq (f $ (comb $ x), list_comb (case_c', fs') $ x)
- end
- in
- map make case_combs
- end
-
-fun case_rewrites thy Tcon =
- let
- val info = Datatype.the_info thy Tcon
- val descr = #descr info
- val sorts = #sorts info
- val typ_names = the_default [Tcon] (#alt_names info)
- in
- map (Drule.export_without_context o Skip_Proof.make_thm thy o HOLogic.mk_Trueprop)
- (make_case_distribs typ_names [descr] sorts thy)
- end
-
-fun instantiated_case_rewrites thy Tcon =
- let
- val rew_ths = case_rewrites thy Tcon
- val ctxt = ProofContext.init_global thy
- fun instantiate th =
- let
- val f = (fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th))))))
- val Type ("fun", [uninst_T, uninst_T']) = fastype_of f
- val ([tname, tname', uname, yname], ctxt') = Variable.add_fixes ["'t", "'t'", "'u", "y"] ctxt
- val T = TFree (tname, HOLogic.typeS)
- val T' = TFree (tname', HOLogic.typeS)
- val U = TFree (uname, HOLogic.typeS)
- val y = Free (yname, U)
- val f' = absdummy (U --> T', Bound 0 $ y)
- val th' = Thm.certify_instantiate
- ([(dest_TVar uninst_T, U --> T'), (dest_TVar uninst_T', T')],
- [((fst (dest_Var f), (U --> T') --> T'), f')]) th
- val [th'] = Variable.export ctxt' ctxt [th']
- in
- th'
- end
- in
- map instantiate rew_ths
- end
-
fun is_compound ((Const (@{const_name Not}, _)) $ t) =
error "is_compound: Negation should not occur; preprocessing is defect"
| is_compound ((Const (@{const_name Ex}, _)) $ _) = true
@@ -99,17 +32,13 @@
NONE => NONE
| SOME raw_split_thm =>
let
- val case_name = fst (dest_Const (fst (strip_comb atom)))
val split_thm = prepare_split_thm (ProofContext.init_global thy) raw_split_thm
(* TODO: contextify things - this line is to unvarify the split_thm *)
(*val ((_, [isplit_thm]), _) =
Variable.import true [split_thm] (ProofContext.init_global thy)*)
val (assms, concl) = Logic.strip_horn (prop_of split_thm)
val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl)
- val Tcons = datatype_names_of_case_name thy case_name
- val ths = maps (instantiated_case_rewrites thy) Tcons
- val atom' = MetaSimplifier.rewrite_term thy
- (map (fn th => th RS @{thm eq_reflection}) ths) [] atom
+ val atom' = case_betapply thy atom
val subst = Pattern.match thy (split_t, atom') (Vartab.empty, Vartab.empty)
val names' = Term.add_free_names atom' names
fun mk_subst_rhs assm =
--- a/src/HOL/Tools/SMT/cvc3_solver.ML Fri Oct 01 15:45:56 2010 +0200
+++ b/src/HOL/Tools/SMT/cvc3_solver.ML Fri Oct 01 16:13:28 2010 +0200
@@ -27,7 +27,7 @@
let
val empty_line = (fn "" => true | _ => false)
val split_first = (fn [] => ("", []) | l :: ls => (l, ls))
- val (l, _) = split_first (dropwhile empty_line output)
+ val (l, _) = split_first (snd (chop_while empty_line output))
in
if is_unsat l then @{cprop False}
else if is_sat l then raise_cex true
--- a/src/HOL/Tools/SMT/smt_solver.ML Fri Oct 01 15:45:56 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML Fri Oct 01 16:13:28 2010 +0200
@@ -160,7 +160,7 @@
val (res, err) = with_timeout ctxt (run ctxt cmd args) input
val _ = trace_msg ctxt (pretty "SMT solver:") err
- val ls = rev (dropwhile (equal "") (rev res))
+ val ls = rev (snd (chop_while (equal "") (rev res)))
val _ = trace_msg ctxt (pretty "SMT result:") ls
in ls end
--- a/src/HOL/Tools/SMT/yices_solver.ML Fri Oct 01 15:45:56 2010 +0200
+++ b/src/HOL/Tools/SMT/yices_solver.ML Fri Oct 01 16:13:28 2010 +0200
@@ -23,7 +23,7 @@
let
val empty_line = (fn "" => true | _ => false)
val split_first = (fn [] => ("", []) | l :: ls => (l, ls))
- val (l, _) = split_first (dropwhile empty_line output)
+ val (l, _) = split_first (snd (chop_while empty_line output))
in
if String.isPrefix "unsat" l then @{cprop False}
else if String.isPrefix "sat" l then raise_cex true
--- a/src/HOL/Tools/refute.ML Fri Oct 01 15:45:56 2010 +0200
+++ b/src/HOL/Tools/refute.ML Fri Oct 01 16:13:28 2010 +0200
@@ -2772,8 +2772,8 @@
(* go back up the stack until we find a level where we can go *)
(* to the next sibling node *)
let
- val offsets' = dropwhile
- (fn off' => off' mod size_elem = size_elem - 1) offsets
+ val offsets' = snd (chop_while
+ (fn off' => off' mod size_elem = size_elem - 1) offsets)
in
case offsets' of
[] =>
--- a/src/HOLCF/Cfun.thy Fri Oct 01 15:45:56 2010 +0200
+++ b/src/HOLCF/Cfun.thy Fri Oct 01 16:13:28 2010 +0200
@@ -373,13 +373,7 @@
fixes f :: "'a::cpo \<Rightarrow> 'b::cpo \<Rightarrow> 'c::cpo"
assumes f: "cont (\<lambda>p. f (fst p) (snd p))"
shows "cont (\<lambda>x. \<Lambda> y. f x y)"
-proof (rule cont2cont_LAM)
- fix x :: 'a show "cont (\<lambda>y. f x y)"
- using f by (rule cont_fst_snd_D2)
-next
- fix y :: 'b show "cont (\<lambda>x. f x y)"
- using f by (rule cont_fst_snd_D1)
-qed
+using assms by (simp add: cont2cont_LAM prod_cont_iff)
lemma cont2cont_LAM_discrete [simp, cont2cont]:
"(\<And>y::'a::discrete_cpo. cont (\<lambda>x. f x y)) \<Longrightarrow> cont (\<lambda>x. \<Lambda> y. f x y)"
--- a/src/HOLCF/Fixrec.thy Fri Oct 01 15:45:56 2010 +0200
+++ b/src/HOLCF/Fixrec.thy Fri Oct 01 16:13:28 2010 +0200
@@ -118,9 +118,9 @@
"match_UU = strictify\<cdot>(\<Lambda> x k. fail)"
definition
- match_cpair :: "'a::cpo \<times> 'b::cpo \<rightarrow> ('a \<rightarrow> 'b \<rightarrow> 'c match) \<rightarrow> 'c match"
+ match_Pair :: "'a::cpo \<times> 'b::cpo \<rightarrow> ('a \<rightarrow> 'b \<rightarrow> 'c match) \<rightarrow> 'c match"
where
- "match_cpair = (\<Lambda> x k. csplit\<cdot>k\<cdot>x)"
+ "match_Pair = (\<Lambda> x k. csplit\<cdot>k\<cdot>x)"
definition
match_spair :: "'a \<otimes> 'b \<rightarrow> ('a \<rightarrow> 'b \<rightarrow> 'c match) \<rightarrow> 'c match"
@@ -162,9 +162,9 @@
"x \<noteq> \<bottom> \<Longrightarrow> match_UU\<cdot>x\<cdot>k = fail"
by (simp_all add: match_UU_def)
-lemma match_cpair_simps [simp]:
- "match_cpair\<cdot>(x, y)\<cdot>k = k\<cdot>x\<cdot>y"
-by (simp_all add: match_cpair_def)
+lemma match_Pair_simps [simp]:
+ "match_Pair\<cdot>(x, y)\<cdot>k = k\<cdot>x\<cdot>y"
+by (simp_all add: match_Pair_def)
lemma match_spair_simps [simp]:
"\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> match_spair\<cdot>(:x, y:)\<cdot>k = k\<cdot>x\<cdot>y"
@@ -248,7 +248,7 @@
(@{const_name sinl}, @{const_name match_sinl}),
(@{const_name sinr}, @{const_name match_sinr}),
(@{const_name spair}, @{const_name match_spair}),
- (@{const_name Pair}, @{const_name match_cpair}),
+ (@{const_name Pair}, @{const_name match_Pair}),
(@{const_name ONE}, @{const_name match_ONE}),
(@{const_name TT}, @{const_name match_TT}),
(@{const_name FF}, @{const_name match_FF}),
--- a/src/HOLCF/Library/List_Cpo.thy Fri Oct 01 15:45:56 2010 +0200
+++ b/src/HOLCF/Library/List_Cpo.thy Fri Oct 01 16:13:28 2010 +0200
@@ -185,14 +185,7 @@
assumes g: "cont (\<lambda>x. g x)"
assumes h: "cont (\<lambda>p. h (fst p) (fst (snd p)) (snd (snd p)))"
shows "cont (\<lambda>x. case f x of [] \<Rightarrow> g x | y # ys \<Rightarrow> h x y ys)"
-proof -
- have "\<And>y ys. cont (\<lambda>x. h x (fst (y, ys)) (snd (y, ys)))"
- by (rule h [THEN cont_fst_snd_D1])
- hence h1: "\<And>y ys. cont (\<lambda>x. h x y ys)" by simp
- note h2 = h [THEN cont_fst_snd_D2, THEN cont_fst_snd_D1]
- note h3 = h [THEN cont_fst_snd_D2, THEN cont_fst_snd_D2]
- from f g h1 h2 h3 show ?thesis by (rule cont2cont_list_case)
-qed
+using assms by (simp add: cont2cont_list_case prod_cont_iff)
text {* The simple version (due to Joachim Breitner) is needed if the
element type of the list is not a cpo. *}
--- a/src/HOLCF/Library/Sum_Cpo.thy Fri Oct 01 15:45:56 2010 +0200
+++ b/src/HOLCF/Library/Sum_Cpo.thy Fri Oct 01 16:13:28 2010 +0200
@@ -173,17 +173,7 @@
assumes g: "cont (\<lambda>p. g (fst p) (snd p))"
assumes h: "cont (\<lambda>x. h x)"
shows "cont (\<lambda>x. case h x of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b)"
-proof -
- note f1 = f [THEN cont_fst_snd_D1]
- note f2 = f [THEN cont_fst_snd_D2]
- note g1 = g [THEN cont_fst_snd_D1]
- note g2 = g [THEN cont_fst_snd_D2]
- show ?thesis
- apply (rule cont_apply [OF h])
- apply (rule cont_sum_case2 [OF f2 g2])
- apply (rule cont_sum_case1 [OF f1 g1])
- done
-qed
+using assms by (simp add: cont2cont_sum_case prod_cont_iff)
subsection {* Compactness and chain-finiteness *}
--- a/src/HOLCF/Product_Cpo.thy Fri Oct 01 15:45:56 2010 +0200
+++ b/src/HOLCF/Product_Cpo.thy Fri Oct 01 16:13:28 2010 +0200
@@ -234,7 +234,7 @@
lemmas cont2cont_snd [simp, cont2cont] = cont_compose [OF cont_snd]
-lemma cont2cont_split:
+lemma cont2cont_prod_case:
assumes f1: "\<And>a b. cont (\<lambda>x. f x a b)"
assumes f2: "\<And>x b. cont (\<lambda>a. f x a b)"
assumes f3: "\<And>x a. cont (\<lambda>b. f x a b)"
@@ -248,6 +248,25 @@
apply (rule f1)
done
+lemma prod_contI:
+ assumes f1: "\<And>y. cont (\<lambda>x. f (x, y))"
+ assumes f2: "\<And>x. cont (\<lambda>y. f (x, y))"
+ shows "cont f"
+proof -
+ have "cont (\<lambda>(x, y). f (x, y))"
+ by (intro cont2cont_prod_case f1 f2 cont2cont)
+ thus "cont f"
+ by (simp only: split_eta)
+qed
+
+lemma prod_cont_iff:
+ "cont f \<longleftrightarrow> (\<forall>y. cont (\<lambda>x. f (x, y))) \<and> (\<forall>x. cont (\<lambda>y. f (x, y)))"
+apply safe
+apply (erule cont_compose [OF _ cont_pair1])
+apply (erule cont_compose [OF _ cont_pair2])
+apply (simp only: prod_contI)
+done
+
lemma cont_fst_snd_D1:
"cont (\<lambda>p. f (fst p) (snd p)) \<Longrightarrow> cont (\<lambda>x. f x y)"
by (drule cont_compose [OF _ cont_pair1], simp)
@@ -256,23 +275,11 @@
"cont (\<lambda>p. f (fst p) (snd p)) \<Longrightarrow> cont (\<lambda>y. f x y)"
by (drule cont_compose [OF _ cont_pair2], simp)
-lemma cont2cont_split' [simp, cont2cont]:
+lemma cont2cont_prod_case' [simp, cont2cont]:
assumes f: "cont (\<lambda>p. f (fst p) (fst (snd p)) (snd (snd p)))"
assumes g: "cont (\<lambda>x. g x)"
- shows "cont (\<lambda>x. split (f x) (g x))"
-proof -
- note f1 = f [THEN cont_fst_snd_D1]
- note f2 = f [THEN cont_fst_snd_D2, THEN cont_fst_snd_D1]
- note f3 = f [THEN cont_fst_snd_D2, THEN cont_fst_snd_D2]
- show ?thesis
- unfolding split_def
- apply (rule cont_apply [OF g])
- apply (rule cont_apply [OF cont_fst f2])
- apply (rule cont_apply [OF cont_snd f3])
- apply (rule cont_const)
- apply (rule f1)
- done
-qed
+ shows "cont (\<lambda>x. prod_case (f x) (g x))"
+using assms by (simp add: cont2cont_prod_case prod_cont_iff)
text {* The simple version (due to Joachim Breitner) is needed if
either element type of the pair is not a cpo. *}
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Oct 01 15:45:56 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Oct 01 16:13:28 2010 +0200
@@ -36,7 +36,7 @@
val beta_rules =
@{thms beta_cfun cont_id cont_const cont2cont_Rep_CFun cont2cont_LAM'} @
- @{thms cont2cont_fst cont2cont_snd cont2cont_Pair cont2cont_split'};
+ @{thms cont2cont_fst cont2cont_snd cont2cont_Pair cont2cont_prod_case'};
val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules);
--- a/src/HOLCF/Tools/fixrec.ML Fri Oct 01 15:45:56 2010 +0200
+++ b/src/HOLCF/Tools/fixrec.ML Fri Oct 01 16:13:28 2010 +0200
@@ -10,8 +10,6 @@
-> (Attrib.binding * term) list -> local_theory -> local_theory
val add_fixrec_cmd: bool -> (binding * string option * mixfix) list
-> (Attrib.binding * string) list -> local_theory -> local_theory
- val add_fixpat: Thm.binding * term list -> theory -> theory
- val add_fixpat_cmd: Attrib.binding * string list -> theory -> theory
val add_matchers: (string * string) list -> theory -> theory
val fixrec_simp_tac: Proof.context -> int -> tactic
val setup: theory -> theory
@@ -218,43 +216,43 @@
taken (t, [])
end;
-(* builds a monadic term for matching a constructor pattern *)
-fun pre_build match_name pat rhs vs taken =
- case pat of
- Const(@{const_name Rep_CFun},_)$f$(v as Free(n,T)) =>
- pre_build match_name f rhs (v::vs) taken
- | Const(@{const_name Rep_CFun},_)$f$x =>
- let val (rhs', v, taken') = pre_build match_name x rhs [] taken;
- in pre_build match_name f rhs' (v::vs) taken' end
- | f$(v as Free(n,T)) =>
- pre_build match_name f rhs (v::vs) taken
- | f$x =>
- let val (rhs', v, taken') = pre_build match_name x rhs [] taken;
- in pre_build match_name f rhs' (v::vs) taken' end
- | Const(c,T) =>
- let
- val n = Name.variant taken "v";
- fun result_type (Type(@{type_name cfun},[_,T])) (x::xs) = result_type T xs
- | result_type (Type (@{type_name "fun"},[_,T])) (x::xs) = result_type T xs
- | result_type T _ = T;
- val v = Free(n, result_type T vs);
- val m = Const(match_name c, matcherT (T, fastype_of rhs));
- val k = big_lambdas vs rhs;
- in
- (m`v`k, v, n::taken)
- end
- | Free(n,_) => fixrec_err ("expected constructor, found free variable " ^ quote n)
- | _ => fixrec_err "pre_build: invalid pattern";
+(* builds a monadic term for matching a pattern *)
+(* returns (rhs, free variable, used varnames) *)
+fun compile_pat match_name pat rhs taken =
+ let
+ fun comp_pat p rhs taken =
+ if is_Free p then (rhs, p, taken)
+ else comp_con (fastype_of p) p rhs [] taken
+ (* compiles a monadic term for a constructor pattern *)
+ and comp_con T p rhs vs taken =
+ case p of
+ Const(@{const_name Rep_CFun},_) $ f $ x =>
+ let val (rhs', v, taken') = comp_pat x rhs taken
+ in comp_con T f rhs' (v::vs) taken' end
+ | f $ x =>
+ let val (rhs', v, taken') = comp_pat x rhs taken
+ in comp_con T f rhs' (v::vs) taken' end
+ | Const (c, cT) =>
+ let
+ val n = Name.variant taken "v"
+ val v = Free(n, T)
+ val m = Const(match_name c, matcherT (cT, fastype_of rhs))
+ val k = big_lambdas vs rhs
+ in
+ (m`v`k, v, n::taken)
+ end
+ | _ => raise TERM ("fixrec: invalid pattern ", [p])
+ in
+ comp_pat pat rhs taken
+ end;
(* builds a monadic term for matching a function definition pattern *)
(* returns (name, arity, matcher) *)
-fun building match_name pat rhs vs taken =
+fun compile_lhs match_name pat rhs vs taken =
case pat of
- Const(@{const_name Rep_CFun}, _)$f$(v as Free(n,T)) =>
- building match_name f rhs (v::vs) taken
- | Const(@{const_name Rep_CFun}, _)$f$x =>
- let val (rhs', v, taken') = pre_build match_name x rhs [] taken;
- in building match_name f rhs' (v::vs) taken' end
+ Const(@{const_name Rep_CFun}, _) $ f $ x =>
+ let val (rhs', v, taken') = compile_pat match_name x rhs taken;
+ in compile_lhs match_name f rhs' (v::vs) taken' end
| Free(_,_) => ((pat, length vs), big_lambdas vs rhs)
| Const(_,_) => ((pat, length vs), big_lambdas vs rhs)
| _ => fixrec_err ("function is not declared as constant in theory: "
@@ -263,11 +261,11 @@
fun strip_alls t =
if Logic.is_all t then strip_alls (snd (Logic.dest_all t)) else t;
-fun match_eq match_name eq =
+fun compile_eq match_name eq =
let
val (lhs,rhs) = dest_eqs (Logic.strip_imp_concl (strip_alls eq));
in
- building match_name lhs (mk_succeed rhs) [] (taken_names eq)
+ compile_lhs match_name lhs (mk_succeed rhs) [] (taken_names eq)
end;
(* returns the sum (using +++) of the terms in ms *)
@@ -290,10 +288,10 @@
end;
(* this is the pattern-matching compiler function *)
-fun compile_pats match_name eqs =
+fun compile_eqs match_name eqs =
let
val ((names, arities), mats) =
- apfst ListPair.unzip (ListPair.unzip (map (match_eq match_name) eqs));
+ apfst ListPair.unzip (ListPair.unzip (map (compile_eq match_name) eqs));
val cname =
case distinct (op =) names of
[n] => n
@@ -379,7 +377,7 @@
case Symtab.lookup matcher_tab c of SOME m => m
| NONE => fixrec_err ("unknown pattern constructor: " ^ c);
- val matches = map (compile_pats match_name) (map (map snd) blocks);
+ val matches = map (compile_eqs match_name) (map (map snd) blocks);
val spec' = map (pair Attrib.empty_binding) matches;
val (lthy, cnames, fixdef_thms, unfold_thms) =
add_fixdefs fixes spec' lthy;
@@ -409,34 +407,6 @@
end; (* local *)
-(*************************************************************************)
-(******************************** Fixpat *********************************)
-(*************************************************************************)
-
-fun fix_pat thy t =
- let
- val T = fastype_of t;
- val eq = mk_trp (HOLogic.eq_const T $ t $ Var (("x",0),T));
- val cname = case chead_of t of Const(c,_) => c | _ =>
- fixrec_err "function is not declared as constant in theory";
- val unfold_thm = Global_Theory.get_thm thy (cname^".unfold");
- val simp = Goal.prove_global thy [] [] eq
- (fn _ => EVERY [stac unfold_thm 1, simp_tac (global_simpset_of thy) 1]);
- in simp end;
-
-fun gen_add_fixpat prep_term prep_attrib ((name, srcs), strings) thy =
- let
- val _ = legacy_feature "Old 'fixpat' command -- use \"fixrec_simp\" method instead";
- val atts = map (prep_attrib thy) srcs;
- val ts = map (prep_term thy) strings;
- val simps = map (fix_pat thy) ts;
- in
- (snd o Global_Theory.add_thmss [((name, simps), atts)]) thy
- end;
-
-val add_fixpat = gen_add_fixpat Sign.cert_term (K I);
-val add_fixpat_cmd = gen_add_fixpat Syntax.read_term_global Attrib.attribute;
-
(*************************************************************************)
(******************************** Parsers ********************************)
@@ -447,10 +417,6 @@
((Parse.opt_keyword "permissive" >> not) -- Parse.fixes -- Parse_Spec.where_alt_specs
>> (fn ((strict, fixes), specs) => add_fixrec_cmd strict fixes specs));
-val _ =
- Outer_Syntax.command "fixpat" "define rewrites for fixrec functions" Keyword.thy_decl
- (Parse_Spec.specs >> (Toplevel.theory o add_fixpat_cmd));
-
val setup =
Method.setup @{binding fixrec_simp}
(Scan.succeed (SIMPLE_METHOD' o fixrec_simp_tac))
--- a/src/Pure/Isar/code.ML Fri Oct 01 15:45:56 2010 +0200
+++ b/src/Pure/Isar/code.ML Fri Oct 01 16:13:28 2010 +0200
@@ -1049,12 +1049,17 @@
val c = const_eqn thy thm;
fun update_subsume thy (thm, proper) eqns =
let
- val args_of = snd o strip_comb o map_types Type.strip_sorts
- o fst o Logic.dest_equals o Thm.plain_prop_of;
+ val args_of = snd o chop_while is_Var o rev o snd o strip_comb
+ o map_types Type.strip_sorts o fst o Logic.dest_equals o Thm.plain_prop_of;
val args = args_of thm;
val incr_idx = Logic.incr_indexes ([], Thm.maxidx_of thm + 1);
- fun matches_args args' = length args <= length args' andalso
- Pattern.matchess thy (args, (map incr_idx o take (length args)) args');
+ fun matches_args args' =
+ let
+ val k = length args' - length args
+ in if k >= 0
+ then Pattern.matchess thy (args, (map incr_idx o drop k) args')
+ else false
+ end;
fun drop (thm', proper') = if (proper orelse not proper')
andalso matches_args (args_of thm') then
(warning ("Code generator: dropping subsumed code equation\n" ^
@@ -1066,7 +1071,8 @@
fun add_eqn' true (Default (eqns, _)) =
Default (natural_order (Theory.check_thy thy) ((thm, proper) :: eqns))
(*this restores the natural order and drops syntactic redundancies*)
- | add_eqn' _ (Eqns eqns) = Eqns (update_subsume thy (thm, proper) eqns)
+ | add_eqn' true fun_spec = fun_spec
+ | add_eqn' false (Eqns eqns) = Eqns (update_subsume thy (thm, proper) eqns)
| add_eqn' false _ = Eqns [(thm, proper)];
in change_fun_spec false c (add_eqn' default) thy end;
--- a/src/Pure/ML/ml_context.ML Fri Oct 01 15:45:56 2010 +0200
+++ b/src/Pure/ML/ml_context.ML Fri Oct 01 16:13:28 2010 +0200
@@ -217,12 +217,13 @@
fun value ctxt (get, put, put_ml) (prelude, value) =
let
- val read = ML_Lex.read Position.none;
- val ants = read prelude @ read ("val _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
+ val code = (prelude
+ ^ "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
^ " (fn () => " ^ value ^ ")) (ML_Context.the_generic_context ())))");
val ctxt' = ctxt
|> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
- |> Context.proof_map (exec (fn () => eval false Position.none ants));
+ |> Context.proof_map (exec
+ (fn () => Secure.use_text ML_Env.local_context (0, "value") false code));
in get ctxt' () end;
end;
--- a/src/Pure/library.ML Fri Oct 01 15:45:56 2010 +0200
+++ b/src/Pure/library.ML Fri Oct 01 16:13:28 2010 +0200
@@ -83,7 +83,7 @@
val take: int -> 'a list -> 'a list
val drop: int -> 'a list -> 'a list
val chop: int -> 'a list -> 'a list * 'a list
- val dropwhile: ('a -> bool) -> 'a list -> 'a list
+ val chop_while: ('a -> bool) -> 'a list -> 'a list * 'a list
val nth: 'a list -> int -> 'a
val nth_map: int -> ('a -> 'a) -> 'a list -> 'a list
val nth_drop: int -> 'a list -> 'a list
@@ -421,8 +421,9 @@
| chop _ [] = ([], [])
| chop n (x :: xs) = chop (n - 1) xs |>> cons x;
-fun dropwhile P [] = []
- | dropwhile P (ys as x::xs) = if P x then dropwhile P xs else ys;
+fun chop_while P [] = ([], [])
+ | chop_while P (ys as x :: xs) =
+ if P x then chop_while P xs |>> cons x else ([], ys);
(*return nth element of a list, where 0 designates the first element;
raise Subscript if list too short*)
--- a/src/Tools/Code/code_runtime.ML Fri Oct 01 15:45:56 2010 +0200
+++ b/src/Tools/Code/code_runtime.ML Fri Oct 01 16:13:28 2010 +0200
@@ -26,6 +26,7 @@
-> theory -> theory
datatype truth = Holds
val put_truth: (unit -> truth) -> Proof.context -> Proof.context
+ val polyml_as_definition: (binding * typ) list -> Path.T list -> theory -> theory
end;
structure Code_Runtime : CODE_RUNTIME =
@@ -341,4 +342,93 @@
end; (*local*)
+
+(** using external SML files as substitute for proper definitions -- only for polyml! **)
+
+local
+
+structure Loaded_Values = Theory_Data(
+ type T = string list
+ val empty = []
+ val merge = merge (op =)
+ val extend = I
+);
+
+fun notify_val (string, value) =
+ let
+ val _ = #enterVal ML_Env.name_space (string, value);
+ val _ = Context.>> ((Context.map_theory o Loaded_Values.map) (insert (op =) string));
+ in () end;
+
+fun abort _ = error "Only value bindings allowed.";
+
+val notifying_context : use_context =
+ {tune_source = #tune_source ML_Env.local_context,
+ name_space =
+ {lookupVal = #lookupVal ML_Env.name_space,
+ lookupType = #lookupType ML_Env.name_space,
+ lookupFix = #lookupFix ML_Env.name_space,
+ lookupStruct = #lookupStruct ML_Env.name_space,
+ lookupSig = #lookupSig ML_Env.name_space,
+ lookupFunct = #lookupFunct ML_Env.name_space,
+ enterVal = notify_val,
+ enterType = abort,
+ enterFix = abort,
+ enterStruct = abort,
+ enterSig = abort,
+ enterFunct = abort,
+ allVal = #allVal ML_Env.name_space,
+ allType = #allType ML_Env.name_space,
+ allFix = #allFix ML_Env.name_space,
+ allStruct = #allStruct ML_Env.name_space,
+ allSig = #allSig ML_Env.name_space,
+ allFunct = #allFunct ML_Env.name_space},
+ str_of_pos = #str_of_pos ML_Env.local_context,
+ print = #print ML_Env.local_context,
+ error = #error ML_Env.local_context};
+
+in
+
+fun use_file filepath thy =
+ let
+ val thy' = Loaded_Values.put [] thy;
+ val _ = Context.set_thread_data ((SOME o Context.Theory) thy');
+ val _ = Secure.use_text notifying_context
+ (0, Path.implode filepath) false (File.read filepath);
+ val thy'' = (Context.the_theory o the) (Context.thread_data ())
+ val names = Loaded_Values.get thy''
+ in (names, thy'') end;
+
+end;
+
+fun add_definiendum (ml_name, (b, T)) thy =
+ thy
+ |> Code_Target.add_reserved target ml_name
+ |> Specification.axiomatization [(b, SOME T, NoSyn)] []
+ |-> (fn ([Const (const, _)], _) =>
+ Code_Target.add_const_syntax target const
+ (SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name))));
+
+fun process_file filepath (definienda, thy) =
+ let
+ val (ml_names, thy') = use_file filepath thy;
+ val superfluous = subtract (fn ((name1, _), name2) => name1 = name2) definienda ml_names;
+ val _ = if null superfluous then ()
+ else error ("Value binding(s) " ^ commas_quote superfluous
+ ^ " found in external file " ^ quote (Path.implode filepath)
+ ^ " not present among the given contants binding(s).");
+ val these_definienda = AList.make (the o AList.lookup (op =) definienda) ml_names;
+ val thy'' = fold add_definiendum these_definienda thy';
+ val definienda' = fold (AList.delete (op =)) ml_names definienda;
+ in (definienda', thy'') end;
+
+fun polyml_as_definition bTs filepaths thy =
+ let
+ val definienda = map (fn bT => ((Binding.name_of o fst) bT, bT)) bTs;
+ val (remaining, thy') = fold process_file filepaths (definienda, thy);
+ val _ = if null remaining then ()
+ else error ("Constant binding(s) " ^ commas_quote (map fst remaining)
+ ^ " not present in external file(s).");
+ in thy' end;
+
end; (*struct*)
--- a/src/Tools/Code/code_target.ML Fri Oct 01 15:45:56 2010 +0200
+++ b/src/Tools/Code/code_target.ML Fri Oct 01 16:13:28 2010 +0200
@@ -244,12 +244,10 @@
fun the_literals thy = #literals o the_fundamental thy;
-local
-
-fun activate_target thy target =
+fun collapse_hierarchy thy =
let
- val ((targets, abortable), default_width) = Targets.get thy;
- fun collapse_hierarchy target =
+ val ((targets, _), _) = Targets.get thy;
+ fun collapse target =
let
val data = case Symtab.lookup targets target
of SOME data => data
@@ -257,10 +255,17 @@
in case the_description data
of Fundamental _ => (K I, data)
| Extension (super, modify) => let
- val (modify', data') = collapse_hierarchy super
+ val (modify', data') = collapse super
in (fn naming => modify' naming #> modify naming, merge_target false target (data', data)) end
end;
- val (modify, data) = collapse_hierarchy target;
+ in collapse end;
+
+local
+
+fun activate_target thy target =
+ let
+ val ((targets, abortable), default_width) = Targets.get thy;
+ val (modify, data) = collapse_hierarchy thy target;
in (default_width, abortable, data, modify) end;
fun activate_syntax lookup_name src_tab = Symtab.empty
@@ -537,12 +542,16 @@
then error ("Too many arguments in syntax for constant " ^ quote c)
else syn);
-fun add_reserved target =
+fun add_reserved target sym thy =
let
- fun add sym syms = if member (op =) syms sym
+ val (_, data) = collapse_hierarchy thy target;
+ val _ = if member (op =) (the_reserved data) sym
then error ("Reserved symbol " ^ quote sym ^ " already declared")
- else insert (op =) sym syms
- in map_reserved target o add end;
+ else ();
+ in
+ thy
+ |> map_reserved target (insert (op =) sym)
+ end;
fun gen_add_include read_const target args thy =
let