src/Tools/Code/code_runtime.ML
changeset 39404 a8c337299bc1
parent 39401 887f4218a39a
child 39422 9019b6afaa4a
     1.1 --- a/src/Tools/Code/code_runtime.ML	Wed Sep 15 15:40:35 2010 +0200
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Wed Sep 15 15:40:36 2010 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  signature CODE_RUNTIME =
     1.5  sig
     1.6    val target: string
     1.7 -  val eval: string option
     1.8 +  val value: string option
     1.9      -> (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string
    1.10      -> ((term -> term) -> 'a -> 'a) -> theory -> term -> string list -> 'a
    1.11    val setup: theory -> theory
    1.12 @@ -16,10 +16,32 @@
    1.13  structure Code_Runtime : CODE_RUNTIME =
    1.14  struct
    1.15  
    1.16 -(** generic **)
    1.17 +(** evaluation **)
    1.18  
    1.19  val target = "Eval";
    1.20  
    1.21 +fun value some_target cookie postproc thy t args =
    1.22 +  let
    1.23 +    val ctxt = ProofContext.init_global thy;
    1.24 +    fun evaluator naming program ((_, (_, ty)), t) deps =
    1.25 +      let
    1.26 +        val _ = if Code_Thingol.contains_dictvar t then
    1.27 +          error "Term to be evaluated contains free dictionaries" else ();
    1.28 +        val value_name = "Value.VALUE.value"
    1.29 +        val program' = program
    1.30 +          |> Graph.new_node (value_name,
    1.31 +              Code_Thingol.Fun (Term.dummy_patternN, ((([], ty), [(([], t), (NONE, true))]), NONE)))
    1.32 +          |> fold (curry Graph.add_edge value_name) deps;
    1.33 +        val (program_code, [SOME value_name']) = Code_Target.produce_code_for thy
    1.34 +          (the_default target some_target) NONE "Code" [] naming program' [value_name];
    1.35 +        val value_code = space_implode " "
    1.36 +          (value_name' :: map (enclose "(" ")") args);
    1.37 +      in ML_Context.value ctxt cookie (program_code, value_code) end;
    1.38 +  in Code_Thingol.dynamic_eval_value thy postproc evaluator t end;
    1.39 +
    1.40 +
    1.41 +(** instrumentalization **)
    1.42 +
    1.43  fun evaluation_code thy module_name tycos consts =
    1.44    let
    1.45      val (consts', (naming, program)) = Code_Thingol.consts_program thy false consts;
    1.46 @@ -38,29 +60,7 @@
    1.47    in (ml_code, (tycos_map, consts_map)) end;
    1.48  
    1.49  
    1.50 -(** evaluation **)
    1.51 -
    1.52 -fun eval some_target cookie postproc thy t args =
    1.53 -  let
    1.54 -    val ctxt = ProofContext.init_global thy;
    1.55 -    fun evaluator naming program ((_, (_, ty)), t) deps =
    1.56 -      let
    1.57 -        val _ = if Code_Thingol.contains_dictvar t then
    1.58 -          error "Term to be evaluated contains free dictionaries" else ();
    1.59 -        val value_name = "Value.VALUE.value"
    1.60 -        val program' = program
    1.61 -          |> Graph.new_node (value_name,
    1.62 -              Code_Thingol.Fun (Term.dummy_patternN, ((([], ty), [(([], t), (NONE, true))]), NONE)))
    1.63 -          |> fold (curry Graph.add_edge value_name) deps;
    1.64 -        val (program_code, [SOME value_name']) = Code_Target.produce_code_for thy
    1.65 -          (the_default target some_target) NONE "Code" [] naming program' [value_name];
    1.66 -        val value_code = space_implode " "
    1.67 -          (value_name' :: map (enclose "(" ")") args);
    1.68 -      in ML_Context.value ctxt cookie (program_code, value_code) end;
    1.69 -  in Code_Thingol.dynamic_eval_value thy postproc evaluator t end;
    1.70 -
    1.71 -
    1.72 -(** instrumentalization by antiquotation **)
    1.73 +(* by antiquotation *)
    1.74  
    1.75  local
    1.76  
    1.77 @@ -110,7 +110,7 @@
    1.78  end; (*local*)
    1.79  
    1.80  
    1.81 -(** reflection support **)
    1.82 +(* reflection support *)
    1.83  
    1.84  fun check_datatype thy tyco consts =
    1.85    let