--- a/NEWS Wed Nov 26 15:44:32 2014 +0100
+++ b/NEWS Wed Nov 26 16:55:43 2014 +0100
@@ -220,8 +220,9 @@
* Tactical PARALLEL_ALLGOALS is the most common way to refer to
PARALLEL_GOALS.
-* Basic combinators map, fold, fold_map, split_list are available as
-parameterized antiquotations, e.g. @{map 4} for lists of quadruples.
+* Basic combinators map, fold, fold_map, split_list, apply are
+available as parameterized antiquotations, e.g. @{map 4} for lists of
+quadruples.
*** System ***
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Nov 26 15:44:32 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Nov 26 16:55:43 2014 +0100
@@ -6,10 +6,6 @@
signature PREDICATE_COMPILE_AUX =
sig
- (* general functions *)
- val apfst3 : ('a -> 'd) -> 'a * 'b * 'c -> 'd * 'b * 'c
- val apsnd3 : ('b -> 'd) -> 'a * 'b * 'c -> 'a * 'd * 'c
- val aptrd3 : ('c -> 'd) -> 'a * 'b * 'c -> 'a * 'b * 'd
val find_indices : ('a -> bool) -> 'a list -> int list
(* mode *)
datatype mode = Bool | Input | Output | Pair of mode * mode | Fun of mode * mode
@@ -172,10 +168,6 @@
(* general functions *)
-fun apfst3 f (x, y, z) = (f x, y, z)
-fun apsnd3 f (x, y, z) = (x, f y, z)
-fun aptrd3 f (x, y, z) = (x, y, f z)
-
fun comb_option f (SOME x1, SOME x2) = SOME (f (x1, x2))
| comb_option f (NONE, SOME x2) = SOME x2
| comb_option f (SOME x1, NONE) = SOME x1
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Wed Nov 26 15:44:32 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Wed Nov 26 16:55:43 2014 +0100
@@ -49,17 +49,18 @@
fun mk_data (c, k, s) = {ignore_consts = c, keep_functions = k, processed_specs = s}
fun map_data f {ignore_consts = c, keep_functions = k, processed_specs = s} = mk_data (f (c, k, s))
-fun ignore_consts cs = Data.map (map_data (apfst3 (fold (fn c => Symtab.insert (op =) (c, ())) cs)))
+fun ignore_consts cs =
+ Data.map (map_data (@{apply 3(1)} (fold (fn c => Symtab.insert (op =) (c, ())) cs)))
-fun keep_functions cs = Data.map (map_data (apsnd3 (fold (fn c => Symtab.insert (op =) (c, ())) cs)))
+fun keep_functions cs =
+ Data.map (map_data (@{apply 3(2)} (fold (fn c => Symtab.insert (op =) (c, ())) cs)))
fun keep_function thy = Symtab.defined (#keep_functions (Data.get thy))
fun processed_specs thy = Symtab.lookup (#processed_specs (Data.get thy))
fun store_processed_specs (constname, specs) =
- Data.map (map_data (aptrd3 (Symtab.update_new (constname, specs))))
-(* *)
+ Data.map (map_data (@{apply 3(3)} (Symtab.update_new (constname, specs))))
fun defining_term_of_introrule_term t =
--- a/src/Pure/ML/ml_antiquotations.ML Wed Nov 26 15:44:32 2014 +0100
+++ b/src/Pure/ML/ml_antiquotations.ML Wed Nov 26 16:55:43 2014 +0100
@@ -226,7 +226,21 @@
\ | split_list" ^ tuple_cons n ^ " =\n\
\ let val" ^ tuple_vars "xs" n ^ " = split_list xs\n\
\ in " ^ cons_tuple n ^ "end\n\
- \ in split_list list end")))
+ \ in split_list list end")) #>
+ ML_Antiquotation.value @{binding apply}
+ (Scan.lift (parameter -- Scan.option (Args.parens (Parse.position Parse.nat))) >>
+ (fn (n, opt_index) =>
+ let
+ val cond =
+ (case opt_index of
+ NONE => K true
+ | SOME (index, index_pos) =>
+ if 1 <= index andalso index <= n then equal (string_of_int index)
+ else error ("Bad index: " ^ string_of_int index ^ Position.here index_pos));
+ in
+ "fn f => fn " ^ tuple_vars "x" n ^ " => " ^
+ tuple (map (fn a => (if cond a then "f x" else "x") ^ a) (indices n))
+ end)));
end;
--- a/src/Tools/induct.ML Wed Nov 26 15:44:32 2014 +0100
+++ b/src/Tools/induct.ML Wed Nov 26 16:55:43 2014 +0100
@@ -300,17 +300,12 @@
Thm.declaration_attribute (fn th => Data.map (which (pairself (fn rs =>
fold Item_Net.remove (filter_rules rs th) rs))));
-fun map1 f (x, y, z, s) = (f x, y, z, s);
-fun map2 f (x, y, z, s) = (x, f y, z, s);
-fun map3 f (x, y, z, s) = (x, y, f z, s);
-fun map4 f (x, y, z, s) = (x, y, z, f s);
-
-fun add_casesT rule x = map1 (apfst (Item_Net.update rule)) x;
-fun add_casesP rule x = map1 (apsnd (Item_Net.update rule)) x;
-fun add_inductT rule x = map2 (apfst (Item_Net.update rule)) x;
-fun add_inductP rule x = map2 (apsnd (Item_Net.update rule)) x;
-fun add_coinductT rule x = map3 (apfst (Item_Net.update rule)) x;
-fun add_coinductP rule x = map3 (apsnd (Item_Net.update rule)) x;
+fun add_casesT rule x = @{apply 4(1)} (apfst (Item_Net.update rule)) x;
+fun add_casesP rule x = @{apply 4(1)} (apsnd (Item_Net.update rule)) x;
+fun add_inductT rule x = @{apply 4(2)} (apfst (Item_Net.update rule)) x;
+fun add_inductP rule x = @{apply 4(2)} (apsnd (Item_Net.update rule)) x;
+fun add_coinductT rule x = @{apply 4(3)} (apfst (Item_Net.update rule)) x;
+fun add_coinductP rule x = @{apply 4(3)} (apsnd (Item_Net.update rule)) x;
val consumes0 = Rule_Cases.default_consumes 0;
val consumes1 = Rule_Cases.default_consumes 1;
@@ -319,18 +314,18 @@
val cases_type = mk_att add_casesT consumes0;
val cases_pred = mk_att add_casesP consumes1;
-val cases_del = del_att map1;
+val cases_del = del_att @{apply 4(1)};
val induct_type = mk_att add_inductT consumes0;
val induct_pred = mk_att add_inductP consumes1;
-val induct_del = del_att map2;
+val induct_del = del_att @{apply 4(2)};
val coinduct_type = mk_att add_coinductT consumes0;
val coinduct_pred = mk_att add_coinductP consumes1;
-val coinduct_del = del_att map3;
+val coinduct_del = del_att @{apply 4(3)};
fun map_simpset f context =
- context |> (Data.map o map4 o Simplifier.simpset_map (Context.proof_of context)) f;
+ context |> (Data.map o @{apply 4(4)} o Simplifier.simpset_map (Context.proof_of context)) f;
fun induct_simp f =
Thm.declaration_attribute (fn thm => map_simpset (fn ctxt => f (ctxt, [thm])));