1.1 --- a/src/HOL/Code_Generator.thy	Fri Jan 19 22:08:05 2007 +0100
     1.2 +++ b/src/HOL/Code_Generator.thy	Fri Jan 19 22:08:06 2007 +0100
     1.3 @@ -61,21 +61,14 @@
     1.4  
     1.5  text {* Evaluation *}
     1.6  
     1.7 -setup {*
     1.8 +method_setup evaluation = {*
     1.9  let
    1.10  
    1.11 -val TrueI = thm "TrueI"
    1.12  fun evaluation_tac i = Tactical.PRIMITIVE (Drule.fconv_rule
    1.13    (Drule.goals_conv (equal i) Codegen.evaluation_conv));
    1.14 -val evaluation_meth =
    1.15 -  Method.no_args (Method.SIMPLE_METHOD' (evaluation_tac THEN' rtac TrueI));
    1.16  
    1.17 -in
    1.18 -
    1.19 -Method.add_method ("evaluation", evaluation_meth, "solve goal by evaluation")
    1.20 -
    1.21 -end;
    1.22 -*}
    1.23 +in Method.no_args (Method.SIMPLE_METHOD' (evaluation_tac THEN' rtac TrueI)) end
    1.24 +*} "solve goal by evaluation"
    1.25  
    1.26  
    1.27  subsection {* Generic code generator setup *}
    1.28 @@ -163,17 +156,14 @@
    1.29  text {* itself as a code generator datatype *}
    1.30  
    1.31  setup {*
    1.32 -let fun add_itself thy =
    1.33    let
    1.34      val v = ("'a", []);
    1.35      val t = Logic.mk_type (TFree v);
    1.36      val Const (c, ty) = t;
    1.37      val (_, Type (dtco, _)) = strip_type ty;
    1.38    in
    1.39 -    thy
    1.40 -    |> CodegenData.add_datatype (dtco, (([v], [(c, [])]), CodegenData.lazy (fn () => [])))
    1.41 +    CodegenData.add_datatype (dtco, (([v], [(c, [])]), CodegenData.lazy (fn () => [])))
    1.42    end
    1.43 -in add_itself end;
    1.44  *} 
    1.45  
    1.46  
    1.47 @@ -194,15 +184,11 @@
    1.48  subsection {* Evaluation oracle *}
    1.49  
    1.50  ML {*
    1.51 -signature HOL_EVAL =
    1.52 +structure HOL_Eval:
    1.53  sig
    1.54    val reff: bool option ref
    1.55    val prop: theory -> term -> term
    1.56 -  val tac: int -> tactic
    1.57 -  val method: Method.src -> Proof.context -> Method.method
    1.58 -end;
    1.59 -
    1.60 -structure HOL_Eval =
    1.61 +end =
    1.62  struct
    1.63  
    1.64  val reff : bool option ref = ref NONE;
    1.65 @@ -213,54 +199,39 @@
    1.66      then HOLogic.true_const
    1.67      else HOLogic.false_const
    1.68  
    1.69 -fun mk_eq thy t =
    1.70 -  Logic.mk_equals (t, prop thy t)
    1.71 -
    1.72 -end;
    1.73 +end
    1.74  *}
    1.75  
    1.76 -setup {*
    1.77 -  PureThy.add_oracle ("invoke", "term", "HOL_Eval.mk_eq")
    1.78 +oracle eval_oracle ("term") = {*
    1.79 +  fn thy => fn t => Logic.mk_equals (t, HOL_Eval.prop thy t)
    1.80  *}
    1.81  
    1.82 -ML {*
    1.83 -structure HOL_Eval : HOL_EVAL =
    1.84 -struct
    1.85 -
    1.86 -open HOL_Eval;
    1.87 +method_setup eval = {*
    1.88 +let
    1.89  
    1.90  fun conv ct =
    1.91 -  let
    1.92 -    val {thy, t, ...} = rep_cterm ct;
    1.93 -  in invoke thy t end;
    1.94 +  let val {thy, t, ...} = rep_cterm ct
    1.95 +  in eval_oracle thy t end;
    1.96  
    1.97 -fun tac i = Tactical.PRIMITIVE (Drule.fconv_rule
    1.98 +fun eval_tac i = Tactical.PRIMITIVE (Drule.fconv_rule
    1.99    (Drule.goals_conv (equal i) (HOLogic.Trueprop_conv conv)));
   1.100  
   1.101 -val method =
   1.102 -  Method.no_args (Method.SIMPLE_METHOD' (tac THEN' rtac TrueI));
   1.103 -
   1.104 -end;
   1.105 -*}
   1.106 -
   1.107 -setup {*
   1.108 -  Method.add_method ("eval", HOL_Eval.method, "solve goal by evaluation")
   1.109 -*}
   1.110 +in Method.no_args (Method.SIMPLE_METHOD' (eval_tac THEN' rtac TrueI)) end
   1.111 +*} "solve goal by evaluation"
   1.112  
   1.113  
   1.114  subsection {* Normalization by evaluation *}
   1.115  
   1.116 -setup {*
   1.117 +method_setup normalization = {*
   1.118  let
   1.119    fun normalization_tac i = Tactical.PRIMITIVE (Drule.fconv_rule
   1.120      (Drule.goals_conv (equal i) (HOLogic.Trueprop_conv
   1.121        NBE.normalization_conv)));
   1.122 -  val normalization_meth =
   1.123 -    Method.no_args (Method.SIMPLE_METHOD' (normalization_tac THEN' resolve_tac [TrueI, refl]));
   1.124  in
   1.125 -  Method.add_method ("normalization", normalization_meth, "solve goal by normalization")
   1.126 -end;
   1.127 -*}
   1.128 +  Method.no_args (Method.SIMPLE_METHOD' (normalization_tac THEN' resolve_tac [TrueI, refl]))
   1.129 +end
   1.130 +*} "solve goal by normalization"
   1.131 +
   1.132  
   1.133  text {* lazy @{const If} *}
   1.134  
   1.135 @@ -280,4 +251,4 @@
   1.136  
   1.137  hide (open) const if_delayed
   1.138  
   1.139 -end
   1.140 \ No newline at end of file
   1.141 +end