added ML antiquotation @{apply n} or @{apply n(k)};
authorwenzelm
Wed Nov 26 16:55:43 2014 +0100 (2014-11-26)
changeset 590575b649fb2f2e1
parent 59056 cbe9563c03d1
child 59058 a78612c67ec0
added ML antiquotation @{apply n} or @{apply n(k)};
NEWS
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
src/Pure/ML/ml_antiquotations.ML
src/Tools/induct.ML
     1.1 --- a/NEWS	Wed Nov 26 15:44:32 2014 +0100
     1.2 +++ b/NEWS	Wed Nov 26 16:55:43 2014 +0100
     1.3 @@ -220,8 +220,9 @@
     1.4  * Tactical PARALLEL_ALLGOALS is the most common way to refer to
     1.5  PARALLEL_GOALS.
     1.6  
     1.7 -* Basic combinators map, fold, fold_map, split_list are available as
     1.8 -parameterized antiquotations, e.g. @{map 4} for lists of quadruples.
     1.9 +* Basic combinators map, fold, fold_map, split_list, apply are
    1.10 +available as parameterized antiquotations, e.g. @{map 4} for lists of
    1.11 +quadruples.
    1.12  
    1.13  
    1.14  *** System ***
     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Nov 26 15:44:32 2014 +0100
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Nov 26 16:55:43 2014 +0100
     2.3 @@ -6,10 +6,6 @@
     2.4  
     2.5  signature PREDICATE_COMPILE_AUX =
     2.6  sig
     2.7 -  (* general functions *)
     2.8 -  val apfst3 : ('a -> 'd) -> 'a * 'b * 'c -> 'd * 'b * 'c
     2.9 -  val apsnd3 : ('b -> 'd) -> 'a * 'b * 'c -> 'a * 'd * 'c
    2.10 -  val aptrd3 : ('c -> 'd) -> 'a * 'b * 'c -> 'a * 'b * 'd
    2.11    val find_indices : ('a -> bool) -> 'a list -> int list
    2.12    (* mode *)
    2.13    datatype mode = Bool | Input | Output | Pair of mode * mode | Fun of mode * mode
    2.14 @@ -172,10 +168,6 @@
    2.15  
    2.16  (* general functions *)
    2.17  
    2.18 -fun apfst3 f (x, y, z) = (f x, y, z)
    2.19 -fun apsnd3 f (x, y, z) = (x, f y, z)
    2.20 -fun aptrd3 f (x, y, z) = (x, y, f z)
    2.21 -
    2.22  fun comb_option f (SOME x1, SOME x2) = SOME (f (x1, x2))
    2.23    | comb_option f (NONE, SOME x2) = SOME x2
    2.24    | comb_option f (SOME x1, NONE) = SOME x1
     3.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Wed Nov 26 15:44:32 2014 +0100
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Wed Nov 26 16:55:43 2014 +0100
     3.3 @@ -49,17 +49,18 @@
     3.4  fun mk_data (c, k, s) = {ignore_consts = c, keep_functions = k, processed_specs = s}
     3.5  fun map_data f {ignore_consts = c, keep_functions = k, processed_specs = s} = mk_data (f (c, k, s))
     3.6  
     3.7 -fun ignore_consts cs = Data.map (map_data (apfst3 (fold (fn c => Symtab.insert (op =) (c, ())) cs)))
     3.8 +fun ignore_consts cs =
     3.9 +  Data.map (map_data (@{apply 3(1)} (fold (fn c => Symtab.insert (op =) (c, ())) cs)))
    3.10  
    3.11 -fun keep_functions cs = Data.map (map_data (apsnd3 (fold (fn c => Symtab.insert (op =) (c, ())) cs)))
    3.12 +fun keep_functions cs =
    3.13 +  Data.map (map_data (@{apply 3(2)} (fold (fn c => Symtab.insert (op =) (c, ())) cs)))
    3.14  
    3.15  fun keep_function thy = Symtab.defined (#keep_functions (Data.get thy))
    3.16  
    3.17  fun processed_specs thy = Symtab.lookup (#processed_specs (Data.get thy))
    3.18  
    3.19  fun store_processed_specs (constname, specs) =
    3.20 -  Data.map (map_data (aptrd3 (Symtab.update_new (constname, specs))))
    3.21 -(* *)
    3.22 +  Data.map (map_data (@{apply 3(3)} (Symtab.update_new (constname, specs))))
    3.23  
    3.24  
    3.25  fun defining_term_of_introrule_term t =
     4.1 --- a/src/Pure/ML/ml_antiquotations.ML	Wed Nov 26 15:44:32 2014 +0100
     4.2 +++ b/src/Pure/ML/ml_antiquotations.ML	Wed Nov 26 16:55:43 2014 +0100
     4.3 @@ -226,7 +226,21 @@
     4.4        \      | split_list" ^ tuple_cons n ^ " =\n\
     4.5        \          let val" ^ tuple_vars "xs" n ^ " = split_list xs\n\
     4.6        \          in " ^ cons_tuple n ^ "end\n\
     4.7 -      \  in split_list list end")))
     4.8 +      \  in split_list list end")) #>
     4.9 +  ML_Antiquotation.value @{binding apply}
    4.10 +    (Scan.lift (parameter -- Scan.option (Args.parens (Parse.position Parse.nat))) >>
    4.11 +      (fn (n, opt_index) =>
    4.12 +        let
    4.13 +          val cond =
    4.14 +            (case opt_index of
    4.15 +              NONE => K true
    4.16 +            | SOME (index, index_pos) =>
    4.17 +                if 1 <= index andalso index <= n then equal (string_of_int index)
    4.18 +                else error ("Bad index: " ^ string_of_int index ^ Position.here index_pos));
    4.19 +        in
    4.20 +          "fn f => fn " ^ tuple_vars "x" n ^ " => " ^
    4.21 +            tuple (map (fn a => (if cond a then "f x" else "x") ^ a) (indices n))
    4.22 +        end)));
    4.23  
    4.24  end;
    4.25  
     5.1 --- a/src/Tools/induct.ML	Wed Nov 26 15:44:32 2014 +0100
     5.2 +++ b/src/Tools/induct.ML	Wed Nov 26 16:55:43 2014 +0100
     5.3 @@ -300,17 +300,12 @@
     5.4    Thm.declaration_attribute (fn th => Data.map (which (pairself (fn rs =>
     5.5      fold Item_Net.remove (filter_rules rs th) rs))));
     5.6  
     5.7 -fun map1 f (x, y, z, s) = (f x, y, z, s);
     5.8 -fun map2 f (x, y, z, s) = (x, f y, z, s);
     5.9 -fun map3 f (x, y, z, s) = (x, y, f z, s);
    5.10 -fun map4 f (x, y, z, s) = (x, y, z, f s);
    5.11 -
    5.12 -fun add_casesT rule x = map1 (apfst (Item_Net.update rule)) x;
    5.13 -fun add_casesP rule x = map1 (apsnd (Item_Net.update rule)) x;
    5.14 -fun add_inductT rule x = map2 (apfst (Item_Net.update rule)) x;
    5.15 -fun add_inductP rule x = map2 (apsnd (Item_Net.update rule)) x;
    5.16 -fun add_coinductT rule x = map3 (apfst (Item_Net.update rule)) x;
    5.17 -fun add_coinductP rule x = map3 (apsnd (Item_Net.update rule)) x;
    5.18 +fun add_casesT rule x = @{apply 4(1)} (apfst (Item_Net.update rule)) x;
    5.19 +fun add_casesP rule x = @{apply 4(1)} (apsnd (Item_Net.update rule)) x;
    5.20 +fun add_inductT rule x = @{apply 4(2)} (apfst (Item_Net.update rule)) x;
    5.21 +fun add_inductP rule x = @{apply 4(2)} (apsnd (Item_Net.update rule)) x;
    5.22 +fun add_coinductT rule x = @{apply 4(3)} (apfst (Item_Net.update rule)) x;
    5.23 +fun add_coinductP rule x = @{apply 4(3)} (apsnd (Item_Net.update rule)) x;
    5.24  
    5.25  val consumes0 = Rule_Cases.default_consumes 0;
    5.26  val consumes1 = Rule_Cases.default_consumes 1;
    5.27 @@ -319,18 +314,18 @@
    5.28  
    5.29  val cases_type = mk_att add_casesT consumes0;
    5.30  val cases_pred = mk_att add_casesP consumes1;
    5.31 -val cases_del = del_att map1;
    5.32 +val cases_del = del_att @{apply 4(1)};
    5.33  
    5.34  val induct_type = mk_att add_inductT consumes0;
    5.35  val induct_pred = mk_att add_inductP consumes1;
    5.36 -val induct_del = del_att map2;
    5.37 +val induct_del = del_att @{apply 4(2)};
    5.38  
    5.39  val coinduct_type = mk_att add_coinductT consumes0;
    5.40  val coinduct_pred = mk_att add_coinductP consumes1;
    5.41 -val coinduct_del = del_att map3;
    5.42 +val coinduct_del = del_att @{apply 4(3)};
    5.43  
    5.44  fun map_simpset f context =
    5.45 -  context |> (Data.map o map4 o Simplifier.simpset_map (Context.proof_of context)) f;
    5.46 +  context |> (Data.map o @{apply 4(4)} o Simplifier.simpset_map (Context.proof_of context)) f;
    5.47  
    5.48  fun induct_simp f =
    5.49    Thm.declaration_attribute (fn thm => map_simpset (fn ctxt => f (ctxt, [thm])));