added get_simproc, @{simproc};
authorwenzelm
Mon Jan 29 19:58:14 2007 +0100 (2007-01-29)
changeset 2220433da3a55c00e
parent 22203 efc0cdc01307
child 22205 23bd1ed32ac0
added get_simproc, @{simproc};
src/Pure/simplifier.ML
     1.1 --- a/src/Pure/simplifier.ML	Sun Jan 28 23:29:17 2007 +0100
     1.2 +++ b/src/Pure/simplifier.ML	Mon Jan 29 19:58:14 2007 +0100
     1.3 @@ -69,6 +69,7 @@
     1.4    val simp_del: attribute
     1.5    val cong_add: attribute
     1.6    val cong_del: attribute
     1.7 +  val get_simproc: Proof.context -> xstring -> simproc
     1.8    val def_simproc: string -> string list -> (morphism -> simpset -> cterm -> thm option) ->
     1.9      local_theory -> local_theory
    1.10    val def_simproc_i: string -> term list -> (morphism -> simpset -> cterm -> thm option) ->
    1.11 @@ -171,6 +172,8 @@
    1.12  fun err_dup_simprocs ds =
    1.13    error ("Duplicate simproc(s): " ^ commas_quote ds);
    1.14  
    1.15 +(* data *)
    1.16 +
    1.17  structure Simprocs = GenericDataFun
    1.18  (
    1.19    val name = "Pure/simprocs";
    1.20 @@ -181,8 +184,27 @@
    1.21      handle Symtab.DUPS ds => err_dup_simprocs ds;
    1.22    fun print _ _ = ();
    1.23  );
    1.24 +val _ = Context.add_setup Simprocs.init;
    1.25  
    1.26 -val _ = Context.add_setup Simprocs.init;
    1.27 +
    1.28 +(* get simprocs *)
    1.29 +
    1.30 +fun get_simproc ctxt xname =
    1.31 +  let
    1.32 +    val (space, tab) = Simprocs.get (Context.Proof ctxt);
    1.33 +    val name = NameSpace.intern space xname;
    1.34 +  in
    1.35 +    (case Symtab.lookup tab name of
    1.36 +      SOME (proc, _) => proc
    1.37 +    | NONE => error ("Undefined simplification procedure: " ^ quote name))
    1.38 +  end;
    1.39 +
    1.40 +val _ = ML_Context.value_antiq "simproc" (Scan.lift Args.name >> (fn name =>
    1.41 +  ("simproc",
    1.42 +    "Simplifier.get_simproc (ML_Context.the_local_context ()) " ^ ML_Syntax.print_string name)));
    1.43 +
    1.44 +
    1.45 +(* define simprocs *)
    1.46  
    1.47  local
    1.48