explicit context for Codegen.eval_term etc.;
authorwenzelm
Wed Apr 20 14:33:33 2011 +0200 (2011-04-20)
changeset 424267ec150fcf3dc
parent 42425 2aa907d5ee4f
child 42427 5611f178a747
explicit context for Codegen.eval_term etc.;
src/HOL/HOL.thy
src/HOL/Library/reflection.ML
src/Pure/codegen.ML
     1.1 --- a/src/HOL/HOL.thy	Wed Apr 20 13:54:07 2011 +0200
     1.2 +++ b/src/HOL/HOL.thy	Wed Apr 20 14:33:33 2011 +0200
     1.3 @@ -1969,20 +1969,22 @@
     1.4  subsubsection {* Evaluation and normalization by evaluation *}
     1.5  
     1.6  setup {*
     1.7 -  Value.add_evaluator ("SML", Codegen.eval_term o Proof_Context.theory_of)  (* FIXME proper context!? *)
     1.8 +  Value.add_evaluator ("SML", Codegen.eval_term)
     1.9  *}
    1.10  
    1.11  ML {*
    1.12  fun gen_eval_method conv ctxt = SIMPLE_METHOD'
    1.13 -  (CONVERSION (Conv.params_conv (~1) (K (Conv.concl_conv (~1) (conv (Proof_Context.theory_of ctxt)))) ctxt)
    1.14 +  (CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 (conv ctxt))) ctxt)
    1.15      THEN' rtac TrueI)
    1.16  *}
    1.17  
    1.18 -method_setup eval = {* Scan.succeed (gen_eval_method Code_Runtime.dynamic_holds_conv) *}
    1.19 -  "solve goal by evaluation"
    1.20 +method_setup eval = {*
    1.21 +  Scan.succeed (gen_eval_method (Code_Runtime.dynamic_holds_conv o Proof_Context.theory_of))
    1.22 +*} "solve goal by evaluation"
    1.23  
    1.24 -method_setup evaluation = {* Scan.succeed (gen_eval_method (K Codegen.evaluation_conv)) *}
    1.25 -  "solve goal by evaluation"
    1.26 +method_setup evaluation = {*
    1.27 +  Scan.succeed (gen_eval_method Codegen.evaluation_conv)
    1.28 +*} "solve goal by evaluation"
    1.29  
    1.30  method_setup normalization = {*
    1.31    Scan.succeed (fn ctxt => SIMPLE_METHOD'
     2.1 --- a/src/HOL/Library/reflection.ML	Wed Apr 20 13:54:07 2011 +0200
     2.2 +++ b/src/HOL/Library/reflection.ML	Wed Apr 20 14:33:33 2011 +0200
     2.3 @@ -312,7 +312,7 @@
     2.4      val th = genreflect ctxt conv corr_thms raw_eqs t RS ssubst
     2.5    in rtac th i THEN TRY (rtac TrueI i) end);  (* FIXME THEN_ALL_NEW !? *)
     2.6  
     2.7 -fun reflection_tac ctxt = gen_reflection_tac ctxt Codegen.evaluation_conv;
     2.8 +fun reflection_tac ctxt = gen_reflection_tac ctxt (Codegen.evaluation_conv ctxt);
     2.9    (*FIXME why Codegen.evaluation_conv?  very specific...*)
    2.10  
    2.11  end
     3.1 --- a/src/Pure/codegen.ML	Wed Apr 20 13:54:07 2011 +0200
     3.2 +++ b/src/Pure/codegen.ML	Wed Apr 20 14:33:33 2011 +0200
     3.3 @@ -77,8 +77,8 @@
     3.4    val test_fn: (int -> term list option) Unsynchronized.ref  (* FIXME *)
     3.5    val test_term: Proof.context -> term -> int -> term list option
     3.6    val eval_result: (unit -> term) Unsynchronized.ref  (* FIXME *)
     3.7 -  val eval_term: theory -> term -> term
     3.8 -  val evaluation_conv: cterm -> thm
     3.9 +  val eval_term: Proof.context -> term -> term
    3.10 +  val evaluation_conv: Proof.context -> conv
    3.11    val parse_mixfix: (string -> 'a) -> string -> 'a mixfix list
    3.12    val quotes_of: 'a mixfix list -> 'a list
    3.13    val num_args_of: 'a mixfix list -> int
    3.14 @@ -903,11 +903,11 @@
    3.15  
    3.16  val eval_result = Unsynchronized.ref (fn () => Bound 0);
    3.17  
    3.18 -fun eval_term thy t =
    3.19 +fun eval_term ctxt t =
    3.20    let
    3.21 -    val ctxt = Proof_Context.init_global thy;  (* FIXME *)
    3.22      val e =
    3.23        let
    3.24 +        val thy = Proof_Context.theory_of ctxt;
    3.25          val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
    3.26            error "Term to be evaluated contains type variables";
    3.27          val _ = (null (Term.add_vars t []) andalso null (Term.add_frees t [])) orelse
    3.28 @@ -930,12 +930,18 @@
    3.29        end
    3.30    in e () end;
    3.31  
    3.32 -val (_, evaluation_conv) = Context.>>> (Context.map_theory_result
    3.33 -  (Thm.add_oracle (Binding.name "evaluation", fn ct =>
    3.34 +val (_, evaluation_oracle) = Context.>>> (Context.map_theory_result
    3.35 +  (Thm.add_oracle (Binding.name "evaluation", fn (ctxt, ct) =>
    3.36      let
    3.37 -      val thy = Thm.theory_of_cterm ct;
    3.38 +      val thy = Proof_Context.theory_of ctxt;
    3.39        val t = Thm.term_of ct;
    3.40 -    in Thm.cterm_of thy (Logic.mk_equals (t, eval_term thy t)) end)));
    3.41 +    in
    3.42 +      if Theory.subthy (Thm.theory_of_cterm ct, thy) then
    3.43 +        Thm.cterm_of thy (Logic.mk_equals (t, eval_term ctxt t))
    3.44 +      else raise CTERM ("evaluation_oracle: bad theory", [ct])
    3.45 +    end)));
    3.46 +
    3.47 +fun evaluation_conv ctxt ct = evaluation_oracle (ctxt, ct);
    3.48  
    3.49  
    3.50  (**** Interface ****)