src/Tools/Code/code_runtime.ML
changeset 63157 65a81a4ef7f8
parent 63156 3cb84e4469a7
child 63159 84c6dd947b75
     1.1 --- a/src/Tools/Code/code_runtime.ML	Thu May 26 15:27:50 2016 +0200
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Thu May 26 15:27:50 2016 +0200
     1.3 @@ -53,7 +53,7 @@
     1.4  
     1.5  open Basic_Code_Symbol;
     1.6  
     1.7 -(** evaluation **)
     1.8 +(** computation **)
     1.9  
    1.10  (* technical prerequisites *)
    1.11  
    1.12 @@ -90,29 +90,25 @@
    1.13        prelude ^ "\nval _ = Context.put_generic_context (SOME (Context.map_proof (" ^
    1.14        put_ml ^ " (fn () => " ^ value ^ ")) (Context.the_generic_context ())))";
    1.15      val ctxt' = ctxt
    1.16 -      |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
    1.17 +      |> put (fn () => error ("Bad computation for " ^ quote put_ml))
    1.18        |> Context.proof_map (exec ctxt false code);
    1.19    in get ctxt' () end;
    1.20  
    1.21  
    1.22 -(* evaluation into target language values *)
    1.23 +(* computation as evaluation into ML language values *)
    1.24  
    1.25  type 'a cookie = (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string;
    1.26  
    1.27  fun reject_vars ctxt t =
    1.28    ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t);
    1.29  
    1.30 -fun obtain_evaluator ctxt some_target program consts =
    1.31 +fun build_computation_text ctxt some_target program consts =
    1.32 +  Code_Target.computation_text ctxt (the_default target some_target) program consts false
    1.33 +  #>> (fn ml_modules => space_implode "\n\n" (map snd ml_modules));
    1.34 +
    1.35 +fun run_computation_text cookie ctxt comp vs_t args =
    1.36    let
    1.37 -    val evaluator' = Code_Target.evaluator ctxt (the_default target some_target) program consts false;
    1.38 -  in
    1.39 -    evaluator'
    1.40 -    #> apfst (fn ml_modules => space_implode "\n\n" (map snd ml_modules))
    1.41 -  end;
    1.42 -
    1.43 -fun evaluation cookie ctxt evaluator vs_t args =
    1.44 -  let
    1.45 -    val (program_code, value_name) = evaluator vs_t;
    1.46 +    val (program_code, value_name) = comp vs_t;
    1.47      val value_code = space_implode " "
    1.48        (value_name :: "()" :: map (enclose "(" ")") args);
    1.49    in Exn.interruptible_capture (value ctxt cookie) (program_code, value_code) end;
    1.50 @@ -128,9 +124,9 @@
    1.51      val _ = if Config.get ctxt trace
    1.52        then tracing ("Evaluation of term " ^ quote (Syntax.string_of_term ctxt t))
    1.53        else ()
    1.54 -    fun evaluator program _ vs_ty_t deps =
    1.55 -      evaluation cookie ctxt (obtain_evaluator ctxt some_target program deps) vs_ty_t args;
    1.56 -  in Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t end;
    1.57 +    fun comp program _ vs_ty_t deps =
    1.58 +      run_computation_text cookie ctxt (build_computation_text ctxt some_target program deps) vs_ty_t args;
    1.59 +  in Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) comp t end;
    1.60  
    1.61  fun dynamic_value_strict cookie ctxt some_target postproc t args =
    1.62    Exn.release (dynamic_value_exn cookie ctxt some_target postproc t args);
    1.63 @@ -138,18 +134,17 @@
    1.64  fun dynamic_value cookie ctxt some_target postproc t args =
    1.65    partiality_as_none (dynamic_value_exn cookie ctxt some_target postproc t args);
    1.66  
    1.67 -fun static_evaluator cookie ctxt some_target { program, deps } =
    1.68 -  let
    1.69 -    val evaluator = obtain_evaluator ctxt some_target program (map Constant deps);
    1.70 -    val evaluation' = evaluation cookie ctxt evaluator;
    1.71 -  in fn _ => fn _ => fn vs_ty_t => fn _ => evaluation' vs_ty_t [] end;
    1.72 -
    1.73  fun static_value_exn cookie { ctxt, target, lift_postproc, consts } =
    1.74    let
    1.75 -    val evaluator = Code_Thingol.static_value { ctxt = ctxt,
    1.76 +    fun computation' { program, deps } =
    1.77 +      let
    1.78 +        val computation'' = run_computation_text cookie ctxt
    1.79 +          (build_computation_text ctxt target program (map Constant deps));
    1.80 +      in fn _ => fn _ => fn vs_ty_t => fn _ => computation'' vs_ty_t [] end;
    1.81 +    val computation = Code_Thingol.static_value { ctxt = ctxt,
    1.82        lift_postproc = Exn.map_res o lift_postproc, consts = consts }
    1.83 -      (static_evaluator cookie ctxt target);
    1.84 -  in fn ctxt' => evaluator ctxt' o reject_vars ctxt' end;
    1.85 +      computation';
    1.86 +  in fn ctxt' => computation ctxt' o reject_vars ctxt' end;
    1.87  
    1.88  fun static_value_strict cookie = Exn.release ooo static_value_exn cookie;
    1.89  
    1.90 @@ -178,7 +173,7 @@
    1.91        then error ("Not a proposition: " ^ Syntax.string_of_term ctxt t)
    1.92        else ();
    1.93      val iff = Thm.cterm_of ctxt (Term.Const (@{const_name Pure.eq}, propT --> propT --> propT));
    1.94 -    val result = case partiality_as_none (evaluation truth_cookie ctxt evaluator vs_t [])
    1.95 +    val result = case partiality_as_none (run_computation_text truth_cookie ctxt evaluator vs_t [])
    1.96       of SOME Holds => true
    1.97        | _ => false;
    1.98    in
    1.99 @@ -196,12 +191,12 @@
   1.100  
   1.101  fun dynamic_holds_conv ctxt = Code_Thingol.dynamic_conv ctxt
   1.102    (fn program => fn vs_t => fn deps =>
   1.103 -    check_holds_oracle ctxt (obtain_evaluator ctxt NONE program deps) vs_t)
   1.104 +    check_holds_oracle ctxt (build_computation_text ctxt NONE program deps) vs_t)
   1.105        o reject_vars ctxt;
   1.106  
   1.107  fun static_holds_conv (ctxt_consts as { ctxt, ... }) =
   1.108    Code_Thingol.static_conv_thingol ctxt_consts (fn { program, deps } => fn ctxt' => fn vs_t =>
   1.109 -    K (check_holds_oracle ctxt' (obtain_evaluator ctxt NONE program (map Constant deps)) vs_t o reject_vars ctxt'));
   1.110 +    K (check_holds_oracle ctxt' (build_computation_text ctxt NONE program (map Constant deps)) vs_t o reject_vars ctxt'));
   1.111  
   1.112  end; (*local*)
   1.113