added def_simproc(_i) -- define named simprocs;
authorwenzelm
Sun Jan 28 23:29:15 2007 +0100 (2007-01-28)
changeset 222016fe46a7259ec
parent 22200 d4797b506752
child 22202 0544af1a5117
added def_simproc(_i) -- define named simprocs;
tuned;
src/Pure/simplifier.ML
     1.1 --- a/src/Pure/simplifier.ML	Sun Jan 28 23:29:14 2007 +0100
     1.2 +++ b/src/Pure/simplifier.ML	Sun Jan 28 23:29:15 2007 +0100
     1.3 @@ -69,6 +69,10 @@
     1.4    val simp_del: attribute
     1.5    val cong_add: attribute
     1.6    val cong_del: attribute
     1.7 +  val def_simproc: string -> string list -> (morphism -> simpset -> cterm -> thm option) ->
     1.8 +    local_theory -> local_theory
     1.9 +  val def_simproc_i: string -> term list -> (morphism -> simpset -> cterm -> thm option) ->
    1.10 +    local_theory -> local_theory
    1.11    val cong_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
    1.12    val simp_modifiers': (Args.T list -> (Method.modifier * Args.T list)) list
    1.13    val simp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
    1.14 @@ -142,11 +146,18 @@
    1.15    (Scan.succeed ("simpset", "Simplifier.local_simpset_of (ML_Context.the_local_context ())"));
    1.16  
    1.17  
    1.18 +(* generic simpsets *)
    1.19 +
    1.20 +fun get_ss (Context.Theory thy) = simpset_of thy
    1.21 +  | get_ss (Context.Proof ctxt) = local_simpset_of ctxt;
    1.22 +
    1.23 +fun map_ss f (Context.Theory thy) = (change_simpset_of thy f; Context.Theory thy)
    1.24 +  | map_ss f (Context.Proof ctxt) = Context.Proof (LocalSimpset.map f ctxt);
    1.25 +
    1.26 +
    1.27  (* attributes *)
    1.28  
    1.29 -fun attrib f = Thm.declaration_attribute (fn th =>
    1.30 -   fn Context.Theory thy => (change_simpset_of thy (fn ss => f (ss, [th])); Context.Theory thy)
    1.31 -    | Context.Proof ctxt => Context.Proof (LocalSimpset.map (fn ss => f (ss, [th])) ctxt));
    1.32 +fun attrib f = Thm.declaration_attribute (fn th => map_ss (fn ss => f (ss, [th])));
    1.33  
    1.34  val simp_add = attrib (op addsimps);
    1.35  val simp_del = attrib (op delsimps);
    1.36 @@ -155,6 +166,74 @@
    1.37  
    1.38  
    1.39  
    1.40 +(** named simprocs **)
    1.41 +
    1.42 +fun err_dup_simprocs ds =
    1.43 +  error ("Duplicate simproc(s): " ^ commas_quote ds);
    1.44 +
    1.45 +structure Simprocs = GenericDataFun
    1.46 +(
    1.47 +  val name = "Pure/simprocs";
    1.48 +  type T = (simproc * stamp) NameSpace.table;
    1.49 +  val empty = NameSpace.empty_table;
    1.50 +  val extend = I;
    1.51 +  fun merge _ simprocs = NameSpace.merge_tables (eq_snd (op =)) simprocs
    1.52 +    handle Symtab.DUPS ds => err_dup_simprocs ds;
    1.53 +  fun print _ _ = ();
    1.54 +);
    1.55 +
    1.56 +val _ = Context.add_setup Simprocs.init;
    1.57 +
    1.58 +local
    1.59 +
    1.60 +(* FIXME *)
    1.61 +fun read_terms ctxt ts =
    1.62 +  #1 (ProofContext.read_termTs ctxt (K false) (K NONE) (K NONE) []
    1.63 +    (map (rpair TypeInfer.logicT) ts));
    1.64 +
    1.65 +(* FIXME *)
    1.66 +fun cert_terms ctxt ts = map (ProofContext.cert_term ctxt) ts;
    1.67 +
    1.68 +fun prep_pats prep ctxt raw_pats =
    1.69 +  let
    1.70 +    val pats = prep ctxt raw_pats;
    1.71 +    val ctxt' = ctxt
    1.72 +      |> fold Variable.declare_term pats
    1.73 +      |> fold Variable.auto_fixes pats;
    1.74 +  in Variable.export_terms ctxt' ctxt pats end;
    1.75 +
    1.76 +fun gen_simproc prep name raw_pats proc lthy =
    1.77 +  let
    1.78 +    val pats =
    1.79 +      prep_pats prep lthy raw_pats
    1.80 +      |> map (Morphism.term (LocalTheory.target_morphism lthy));
    1.81 +    val naming = LocalTheory.target_naming lthy;
    1.82 +  in
    1.83 +    lthy |> LocalTheory.declaration (fn phi => fn context =>
    1.84 +      let
    1.85 +        val cert = Thm.cterm_of (Context.theory_of context);
    1.86 +        val pats' = map (cert o Morphism.term phi) pats;
    1.87 +        val name' = Morphism.name phi name;
    1.88 +        val proc' = proc phi;
    1.89 +        val simproc = mk_simproc' (NameSpace.full naming name') pats' proc';
    1.90 +      in
    1.91 +        context
    1.92 +        |> Simprocs.map (fn simprocs =>
    1.93 +            NameSpace.extend_table naming (simprocs, [(name', (simproc, stamp ()))])
    1.94 +              handle Symtab.DUPS ds => err_dup_simprocs ds)
    1.95 +        |> map_ss (fn ss => ss addsimprocs [simproc])
    1.96 +      end)
    1.97 +  end;
    1.98 +
    1.99 +in
   1.100 +
   1.101 +val def_simproc = gen_simproc read_terms;
   1.102 +val def_simproc_i = gen_simproc cert_terms;
   1.103 +
   1.104 +end;
   1.105 +
   1.106 +
   1.107 +
   1.108  (** simplification tactics and rules **)
   1.109  
   1.110  fun solve_all_tac solvers ss =
   1.111 @@ -251,9 +330,6 @@
   1.112      Args.parens (Args.$$$ no_asm_useN) >> K full_simplify ||
   1.113      Scan.succeed asm_full_simplify) |> Scan.lift) x;
   1.114  
   1.115 -fun get_ss (Context.Theory thy) = simpset_of thy
   1.116 -  | get_ss (Context.Proof ctxt) = local_simpset_of ctxt;
   1.117 -
   1.118  in
   1.119  
   1.120  val simplified =