evaluator separating static and dynamic operations
authorhaftmann
Tue Dec 21 09:29:33 2010 +0100 (2010-12-21)
changeset 413490e2a3f22f018
parent 41348 692c3fbde3c9
child 41350 ce825d32b450
evaluator separating static and dynamic operations
src/Tools/Code/code_runtime.ML
     1.1 --- a/src/Tools/Code/code_runtime.ML	Tue Dec 21 09:19:37 2010 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Tue Dec 21 09:29:33 2010 +0100
     1.3 @@ -86,8 +86,7 @@
     1.4      val ctxt = ProofContext.init_global thy;
     1.5    in ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t) end;
     1.6  
     1.7 -fun obtain_evaluator thy some_target naming program deps =
     1.8 -  Code_Target.evaluator thy (the_default target some_target) naming program deps;
     1.9 +fun obtain_evaluator thy some_target = Code_Target.evaluator thy (the_default target some_target);
    1.10  
    1.11  fun evaluation cookie thy evaluator vs_t args =
    1.12    let
    1.13 @@ -146,15 +145,16 @@
    1.14  
    1.15  val reject_vars = fn thy => tap (reject_vars thy o Thm.term_of);
    1.16  
    1.17 -fun check_holds some_target naming thy program vs_t deps ct =
    1.18 +local
    1.19 +
    1.20 +fun check_holds thy evaluator vs_t deps ct =
    1.21    let
    1.22      val t = Thm.term_of ct;
    1.23      val _ = if fastype_of t <> propT
    1.24        then error ("Not a proposition: " ^ Syntax.string_of_term_global thy t)
    1.25        else ();
    1.26      val iff = Thm.cterm_of thy (Term.Const ("==", propT --> propT --> propT));
    1.27 -    val result = case partiality_as_none
    1.28 -      (evaluation truth_cookie thy (obtain_evaluator thy some_target naming program deps) vs_t [])
    1.29 +    val result = case partiality_as_none (evaluation truth_cookie thy evaluator vs_t [])
    1.30       of SOME Holds => true
    1.31        | _ => false;
    1.32    in
    1.33 @@ -163,19 +163,24 @@
    1.34  
    1.35  val (_, raw_check_holds_oracle) = Context.>>> (Context.map_theory_result
    1.36    (Thm.add_oracle (Binding.name "holds_by_evaluation",
    1.37 -  fn (some_target, naming, thy, program, vs_t, deps, ct) => check_holds some_target naming thy program vs_t deps ct)));
    1.38 +  fn (thy, evaluator, vs_t, deps, ct) => check_holds thy evaluator vs_t deps ct)));
    1.39  
    1.40 -fun check_holds_oracle some_target naming thy program ((_, vs_ty), t) deps ct =
    1.41 -  raw_check_holds_oracle (some_target, naming, thy, program, (vs_ty, t), deps, ct);
    1.42 +fun check_holds_oracle thy evaluator ((_, vs_ty), t) deps ct =
    1.43 +  raw_check_holds_oracle (thy, evaluator, (vs_ty, t), deps, ct);
    1.44 +
    1.45 +in
    1.46  
    1.47  fun dynamic_holds_conv thy = Code_Thingol.dynamic_conv thy
    1.48 -    (fn naming => check_holds_oracle NONE naming thy)
    1.49 -  o reject_vars thy;
    1.50 +  (fn naming => fn program => fn vs_t => fn deps =>
    1.51 +    check_holds_oracle thy (obtain_evaluator thy NONE naming program deps) vs_t deps)
    1.52 +      o reject_vars thy;
    1.53  
    1.54 -fun static_holds_conv thy consts =
    1.55 -  Code_Thingol.static_conv thy consts
    1.56 -    (fn naming => fn program => fn consts' => check_holds_oracle NONE naming thy program)
    1.57 -    o reject_vars thy;
    1.58 +fun static_holds_conv thy consts = Code_Thingol.static_conv thy consts
    1.59 +  (fn naming => fn program => fn consts' =>
    1.60 +    check_holds_oracle thy (obtain_evaluator thy NONE naming program consts'))
    1.61 +      o reject_vars thy;
    1.62 +
    1.63 +end; (*local*)
    1.64  
    1.65  
    1.66  (** instrumentalization **)