src/Tools/Code/code_runtime.ML
changeset 41347 064133cb4ef6
parent 41343 71f4f15258a5
child 41348 692c3fbde3c9
     1.1 --- a/src/Tools/Code/code_runtime.ML	Tue Dec 21 09:18:29 2010 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Tue Dec 21 09:18:29 2010 +0100
     1.3 @@ -86,25 +86,15 @@
     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_serializer thy some_target = Code_Target.produce_code_for thy
     1.8 -  (the_default target some_target) NONE "Code" [];
     1.9 +fun obtain_evaluator thy some_target naming program deps =
    1.10 +  Code_Target.evaluator thy (the_default target some_target) naming program deps;
    1.11  
    1.12 -fun base_evaluator cookie serializer (naming : Code_Thingol.naming) thy program ((vs, ty), t) deps args =
    1.13 +fun evaluation cookie thy evaluator vs_t args =
    1.14    let
    1.15      val ctxt = ProofContext.init_global thy;
    1.16 -    val _ = if Code_Thingol.contains_dict_var t then
    1.17 -      error "Term to be evaluated contains free dictionaries" else ();
    1.18 -    val v' = Name.variant (map fst vs) "a";
    1.19 -    val vs' = (v', []) :: vs;
    1.20 -    val ty' = Code_Thingol.fun_tyco `%% [ITyVar v', ty];
    1.21 -    val value_name = "Value.value.value"
    1.22 -    val program' = program
    1.23 -      |> Graph.new_node (value_name,
    1.24 -          Code_Thingol.Fun (Term.dummy_patternN, (((vs', ty'), [(([IVar NONE], t), (NONE, true))]), NONE)))
    1.25 -      |> fold (curry Graph.add_edge value_name) deps;
    1.26 -    val (program_code, [SOME value_name']) = serializer naming program' [value_name];
    1.27 +    val (program_code, value_name) = evaluator vs_t;
    1.28      val value_code = space_implode " "
    1.29 -      (value_name' :: "()" :: map (enclose "(" ")") args);
    1.30 +      (value_name :: "()" :: map (enclose "(" ")") args);
    1.31    in Exn.interruptible_capture (value ctxt cookie) (program_code, value_code) end;
    1.32  
    1.33  fun partiality_as_none e = SOME (Exn.release e)
    1.34 @@ -119,7 +109,7 @@
    1.35        then tracing ("Evaluation of term " ^ quote (Syntax.string_of_term_global thy t))
    1.36        else ()
    1.37      fun evaluator naming program ((_, vs_ty), t) deps =
    1.38 -      base_evaluator cookie (obtain_serializer thy some_target) naming thy program (vs_ty, t) deps args;
    1.39 +      evaluation cookie thy (obtain_evaluator thy some_target naming program deps) (vs_ty, t) args;
    1.40    in Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t end;
    1.41  
    1.42  fun dynamic_value_strict cookie thy some_target postproc t args =
    1.43 @@ -128,18 +118,20 @@
    1.44  fun dynamic_value cookie thy some_target postproc t args =
    1.45    partiality_as_none (dynamic_value_exn cookie thy some_target postproc t args);
    1.46  
    1.47 -fun static_value_exn cookie thy some_target postproc consts =
    1.48 +fun static_evaluator cookie thy some_target naming program consts' =
    1.49    let
    1.50 -    val serializer = obtain_serializer thy some_target;
    1.51 -    fun evaluator naming program thy ((_, vs_ty), t) deps =
    1.52 -      base_evaluator cookie serializer naming thy program (vs_ty, t) deps [];
    1.53 -  in Code_Thingol.static_value thy (Exn.map_result o postproc) consts evaluator o reject_vars thy end;
    1.54 +    val evaluator = obtain_evaluator thy some_target naming program consts'
    1.55 +  in fn ((_, vs_ty), t) => fn _ => evaluation cookie thy evaluator (vs_ty, t) [] end;
    1.56  
    1.57 -fun static_value_strict cookie thy some_target postproc consts t =
    1.58 -  Exn.release (static_value_exn cookie thy some_target postproc consts t);
    1.59 +fun static_value_exn cookie thy some_target postproc consts =
    1.60 +  Code_Thingol.static_value thy (Exn.map_result o postproc) consts
    1.61 +    (static_evaluator cookie thy some_target) o reject_vars thy;
    1.62  
    1.63 -fun static_value cookie thy some_target postproc consts t =
    1.64 -  partiality_as_none (static_value_exn cookie thy some_target postproc consts t);
    1.65 +fun static_value_strict cookie thy some_target postproc consts =
    1.66 +  Exn.release o static_value_exn cookie thy some_target postproc consts;
    1.67 +
    1.68 +fun static_value cookie thy some_target postproc consts =
    1.69 +  partiality_as_none o static_value_exn cookie thy some_target postproc consts;
    1.70  
    1.71  
    1.72  (* evaluation for truth or nothing *)
    1.73 @@ -154,14 +146,15 @@
    1.74  
    1.75  val reject_vars = fn thy => tap (reject_vars thy o Thm.term_of);
    1.76  
    1.77 -fun check_holds serializer naming thy program vs_t deps ct =
    1.78 +fun check_holds some_target naming thy program vs_t deps ct =
    1.79    let
    1.80      val t = Thm.term_of ct;
    1.81      val _ = if fastype_of t <> propT
    1.82        then error ("Not a proposition: " ^ Syntax.string_of_term_global thy t)
    1.83        else ();
    1.84      val iff = Thm.cterm_of thy (Term.Const ("==", propT --> propT --> propT));
    1.85 -    val result = case partiality_as_none (base_evaluator truth_cookie serializer naming thy program vs_t deps [])
    1.86 +    val result = case partiality_as_none
    1.87 +      (evaluation truth_cookie thy (obtain_evaluator thy some_target naming program deps) vs_t [])
    1.88       of SOME Holds => true
    1.89        | _ => false;
    1.90    in
    1.91 @@ -176,17 +169,13 @@
    1.92    raw_check_holds_oracle (serializer, naming, thy, program, (vs_ty, t), deps, ct);
    1.93  
    1.94  fun dynamic_holds_conv thy = Code_Thingol.dynamic_conv thy
    1.95 -    (fn naming => check_holds_oracle (obtain_serializer thy NONE) naming thy)
    1.96 +    (fn naming => check_holds_oracle NONE naming thy)
    1.97    o reject_vars thy;
    1.98  
    1.99  fun static_holds_conv thy consts =
   1.100 -  let
   1.101 -    val serializer = obtain_serializer thy NONE;
   1.102 -  in
   1.103 -    Code_Thingol.static_conv thy consts
   1.104 -      (fn naming => fn program => fn thy => check_holds_oracle serializer naming thy program)
   1.105 -    o reject_vars thy
   1.106 -  end;
   1.107 +  Code_Thingol.static_conv thy consts
   1.108 +    (fn naming => fn program => fn consts' => check_holds_oracle NONE naming thy program)
   1.109 +    o reject_vars thy;
   1.110  
   1.111  
   1.112  (** instrumentalization **)