src/Tools/Code/code_thingol.ML
changeset 63157 65a81a4ef7f8
parent 63156 3cb84e4469a7
child 63159 84c6dd947b75
     1.1 --- a/src/Tools/Code/code_thingol.ML	Thu May 26 15:27:50 2016 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Thu May 26 15:27:50 2016 +0200
     1.3 @@ -839,49 +839,59 @@
     1.4      #> term_value
     1.5    end;
     1.6  
     1.7 -fun dynamic_evaluator ctxt evaluator algebra eqngr t =
     1.8 +fun dynamic_evaluation eval ctxt algebra eqngr t =
     1.9    let
    1.10      val ((program, (vs_ty_t', deps)), _) =
    1.11 -      invoke_generation false (Proof_Context.theory_of ctxt) (algebra, eqngr) ensure_value t;
    1.12 -  in evaluator program t vs_ty_t' deps end;
    1.13 +      invoke_generation false (Proof_Context.theory_of ctxt)
    1.14 +        (algebra, eqngr) ensure_value t;
    1.15 +  in eval program t vs_ty_t' deps end;
    1.16  
    1.17  fun dynamic_conv ctxt conv =
    1.18 -  Code_Preproc.dynamic_conv ctxt (dynamic_evaluator ctxt (fn program => fn _ => conv program));
    1.19 -
    1.20 -fun dynamic_value ctxt postproc evaluator =
    1.21 -  Code_Preproc.dynamic_value ctxt postproc (dynamic_evaluator ctxt evaluator);
    1.22 +  Code_Preproc.dynamic_conv ctxt
    1.23 +    (dynamic_evaluation (fn program => fn _ => conv program) ctxt);
    1.24  
    1.25 -fun static_subevaluator ctxt subevaluator algebra eqngr program t =
    1.26 -  let
    1.27 -    val ((_, ((vs_ty', t'), deps)), _) =
    1.28 -      ensure_value ctxt algebra eqngr t ([], program);
    1.29 -  in subevaluator ctxt t (vs_ty', t') deps end;
    1.30 +fun dynamic_value ctxt postproc comp =
    1.31 +  Code_Preproc.dynamic_value ctxt postproc
    1.32 +    (dynamic_evaluation comp ctxt);
    1.33  
    1.34 -fun static_evaluator_thingol ctxt evaluator consts { algebra, eqngr } =
    1.35 +fun static_evaluation ctxt consts algebra eqngr static_eval =
    1.36    let
    1.37      fun generate_consts ctxt algebra eqngr =
    1.38        fold_map (ensure_const ctxt algebra eqngr false);
    1.39      val (deps, program) =
    1.40 -      invoke_generation true (Proof_Context.theory_of ctxt) (algebra, eqngr) generate_consts consts;
    1.41 -    val subevaluator = evaluator { program = program, deps = deps };
    1.42 -  in fn ctxt' => static_subevaluator ctxt' subevaluator algebra eqngr program end;
    1.43 +      invoke_generation true (Proof_Context.theory_of ctxt)
    1.44 +        (algebra, eqngr) generate_consts consts;
    1.45 +  in static_eval { program = program, deps = deps } end;
    1.46  
    1.47 -fun static_evaluator_isa ctxt evaluator consts { algebra, eqngr } =
    1.48 +fun static_evaluation_thingol ctxt consts algebra eqngr static_eval =
    1.49    let
    1.50 -    fun generate_consts ctxt algebra eqngr =
    1.51 -      fold_map (ensure_const ctxt algebra eqngr false);
    1.52 -    val (_, program) =
    1.53 -      invoke_generation true (Proof_Context.theory_of ctxt) (algebra, eqngr) generate_consts consts;
    1.54 -  in evaluator (program: program) end;
    1.55 +    fun evaluation' program dynamic_eval ctxt t =
    1.56 +      let
    1.57 +        val ((_, ((vs_ty', t'), deps)), _) =
    1.58 +          ensure_value ctxt algebra eqngr t ([], program);
    1.59 +      in dynamic_eval ctxt t (vs_ty', t') deps end;
    1.60 +    fun evaluation static_eval { program, deps } =
    1.61 +      evaluation' program (static_eval { program = program, deps = deps });
    1.62 +  in
    1.63 +    static_evaluation ctxt consts algebra eqngr
    1.64 +      (evaluation static_eval)
    1.65 +  end;
    1.66 +
    1.67 +fun static_evaluation_isa ctxt consts algebra eqngr static_eval =
    1.68 +  static_evaluation ctxt consts algebra eqngr
    1.69 +    (fn { program, ... } => static_eval (program: program));
    1.70  
    1.71  fun static_conv_thingol (ctxt_consts as { ctxt, consts }) conv =
    1.72 -  Code_Preproc.static_conv ctxt_consts (static_evaluator_thingol ctxt (K oo conv) consts);
    1.73 +  Code_Preproc.static_conv ctxt_consts (fn { algebra, eqngr } =>
    1.74 +    static_evaluation_thingol ctxt consts algebra eqngr (K oo conv));
    1.75  
    1.76  fun static_conv_isa (ctxt_consts as { ctxt, consts }) conv =
    1.77 -  Code_Preproc.static_conv ctxt_consts (static_evaluator_isa ctxt conv consts);
    1.78 +  Code_Preproc.static_conv ctxt_consts (fn { algebra, eqngr } =>
    1.79 +    static_evaluation_isa ctxt consts algebra eqngr conv);
    1.80  
    1.81 -fun static_value (ctxt_postproc_consts as { ctxt, consts, ... }) evaluator =
    1.82 -  Code_Preproc.static_value ctxt_postproc_consts (static_evaluator_thingol ctxt evaluator consts);
    1.83 +fun static_value (ctxt_postproc_consts as { ctxt, consts, ... }) comp =
    1.84 +  Code_Preproc.static_value ctxt_postproc_consts (fn { algebra, eqngr } =>
    1.85 +    static_evaluation_thingol ctxt consts algebra eqngr comp);
    1.86  
    1.87  
    1.88  (** constant expressions **)