src/Tools/Code/code_runtime.ML
changeset 39485 f7270a5e2550
parent 39482 1c37d19e3d58
child 39537 41afe7124aa6
     1.1 --- a/src/Tools/Code/code_runtime.ML	Fri Sep 17 09:21:49 2010 +0200
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Fri Sep 17 10:00:01 2010 +0200
     1.3 @@ -47,17 +47,23 @@
     1.4  
     1.5  val _ = Context.>> (Context.map_theory
     1.6    (Code_Target.extend_target (target, (Code_ML.target_SML, K I))
     1.7 -  #> Code_Target.add_tyco_syntax target @{type_name prop} (SOME (0, (K o K o K) (Code_Printer.str s_truth)))
     1.8 -  #> Code_Target.add_const_syntax target @{const_name Code_Generator.holds} (SOME (Code_Printer.plain_const_syntax s_Holds))
     1.9 +  #> Code_Target.add_tyco_syntax target @{type_name prop}
    1.10 +       (SOME (0, (K o K o K) (Code_Printer.str s_truth)))
    1.11 +  #> Code_Target.add_const_syntax target @{const_name Code_Generator.holds}
    1.12 +       (SOME (Code_Printer.plain_const_syntax s_Holds))
    1.13    #> Code_Target.add_reserved target this
    1.14 -  #> fold (Code_Target.add_reserved target) ["oo", "ooo", "oooo", "upto", "downto", "orf", "andf"])); (*avoid further pervasive infix names*)
    1.15 +  #> fold (Code_Target.add_reserved target) ["oo", "ooo", "oooo", "upto", "downto", "orf", "andf"]));
    1.16 +       (*avoid further pervasive infix names*)
    1.17  
    1.18  
    1.19  (* evaluation into target language values *)
    1.20  
    1.21  type 'a cookie = (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string;
    1.22  
    1.23 -fun base_evaluator cookie thy some_target naming program ((vs, ty), t) deps args =
    1.24 +fun obtain_serializer thy some_target = Code_Target.produce_code_for thy
    1.25 +  (the_default target some_target) NONE "Code" [];
    1.26 +
    1.27 +fun base_evaluator cookie serializer naming thy program ((vs, ty), t) deps args =
    1.28    let
    1.29      val ctxt = ProofContext.init_global thy;
    1.30      val _ = if Code_Thingol.contains_dictvar t then
    1.31 @@ -70,8 +76,7 @@
    1.32        |> Graph.new_node (value_name,
    1.33            Code_Thingol.Fun (Term.dummy_patternN, (((vs', ty'), [(([IVar NONE], t), (NONE, true))]), NONE)))
    1.34        |> fold (curry Graph.add_edge value_name) deps;
    1.35 -    val (program_code, [SOME value_name']) = Code_Target.produce_code_for thy
    1.36 -      (the_default target some_target) NONE "Code" [] naming program' [value_name];
    1.37 +    val (program_code, [SOME value_name']) = serializer naming program' [value_name];
    1.38      val value_code = space_implode " "
    1.39        (value_name' :: "()" :: map (enclose "(" ")") args);
    1.40    in Exn.capture (ML_Context.value ctxt cookie) (program_code, value_code) end;
    1.41 @@ -84,7 +89,7 @@
    1.42  fun dynamic_value_exn cookie thy some_target postproc t args =
    1.43    let
    1.44      fun evaluator naming program ((_, vs_ty), t) deps =
    1.45 -      base_evaluator cookie thy some_target naming program (vs_ty, t) deps args;
    1.46 +      base_evaluator cookie (obtain_serializer thy some_target) naming thy program (vs_ty, t) deps args;
    1.47    in Code_Thingol.dynamic_eval_value thy (Exn.map_result o postproc) evaluator t end;
    1.48  
    1.49  fun dynamic_value_strict cookie thy some_target postproc t args =
    1.50 @@ -95,8 +100,9 @@
    1.51  
    1.52  fun static_value_exn cookie thy some_target postproc consts =
    1.53    let
    1.54 +    val serializer = obtain_serializer thy some_target;
    1.55      fun evaluator naming program thy ((_, vs_ty), t) deps =
    1.56 -      base_evaluator cookie thy some_target naming program (vs_ty, t) deps [];
    1.57 +      base_evaluator cookie serializer naming thy program (vs_ty, t) deps [];
    1.58    in Code_Thingol.static_eval_value thy (Exn.map_result o postproc) consts evaluator end;
    1.59  
    1.60  fun static_value_strict cookie thy some_target postproc consts t =
    1.61 @@ -115,14 +121,14 @@
    1.62  val put_truth = Truth_Result.put;
    1.63  val truth_cookie = (Truth_Result.get, put_truth, Long_Name.append this "put_truth");
    1.64  
    1.65 -fun check_holds thy naming program vs_t deps ct =
    1.66 +fun check_holds serializer naming thy program vs_t deps ct =
    1.67    let
    1.68      val t = Thm.term_of ct;
    1.69      val _ = if fastype_of t <> propT
    1.70        then error ("Not a proposition: " ^ Syntax.string_of_term_global thy t)
    1.71        else ();
    1.72      val iff = Thm.cterm_of thy (Term.Const ("==", propT --> propT --> propT));
    1.73 -    val result = case partiality_as_none (base_evaluator truth_cookie thy NONE naming program vs_t deps [])
    1.74 +    val result = case partiality_as_none (base_evaluator truth_cookie serializer naming thy program vs_t deps [])
    1.75       of SOME Holds => true
    1.76        | _ => false;
    1.77    in
    1.78 @@ -131,15 +137,21 @@
    1.79  
    1.80  val (_, raw_check_holds_oracle) = Context.>>> (Context.map_theory_result
    1.81    (Thm.add_oracle (Binding.name "holds_by_evaluation",
    1.82 -  fn (thy, naming, program, vs_t, deps, ct) => check_holds thy naming program vs_t deps ct)));
    1.83 +  fn (serializer, naming, thy, program, vs_t, deps, ct) => check_holds serializer naming thy program vs_t deps ct)));
    1.84  
    1.85 -fun check_holds_oracle thy naming program ((_, vs_ty), t) deps ct =
    1.86 -  raw_check_holds_oracle (thy, naming, program, (vs_ty, t), deps, ct);
    1.87 +fun check_holds_oracle serializer naming thy program ((_, vs_ty), t) deps ct =
    1.88 +  raw_check_holds_oracle (serializer, naming, thy, program, (vs_ty, t), deps, ct);
    1.89 +
    1.90 +val dynamic_holds_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_eval_conv thy
    1.91 +  (fn naming => check_holds_oracle (obtain_serializer thy NONE) naming thy));
    1.92  
    1.93 -val dynamic_holds_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_eval_conv thy (check_holds_oracle thy));
    1.94 -
    1.95 -fun static_holds_conv thy consts = Code_Thingol.static_eval_conv thy consts
    1.96 -  (fn naming => fn program => fn thy => check_holds_oracle thy naming program);
    1.97 +fun static_holds_conv thy consts =
    1.98 +  let
    1.99 +    val serializer = obtain_serializer thy NONE;
   1.100 +  in
   1.101 +    Code_Thingol.static_eval_conv thy consts
   1.102 +      (fn naming => fn program => fn thy => check_holds_oracle serializer naming thy program)
   1.103 +  end;
   1.104  
   1.105  
   1.106  (** instrumentalization **)
   1.107 @@ -253,7 +265,7 @@
   1.108  fun add_eval_const (const, const') = Code_Target.add_const_syntax target
   1.109    const (SOME (Code_Printer.simple_const_syntax (0, (K o K o K) const')));
   1.110  
   1.111 -fun process (code_body, (tyco_map, (constr_map, const_map))) module_name NONE thy =
   1.112 +fun process_reflection (code_body, (tyco_map, (constr_map, const_map))) module_name NONE thy =
   1.113        thy
   1.114        |> Code_Target.add_reserved target module_name
   1.115        |> Context.theory_map
   1.116 @@ -261,7 +273,7 @@
   1.117        |> fold (add_eval_tyco o apsnd Code_Printer.str) tyco_map
   1.118        |> fold (add_eval_constr o apsnd Code_Printer.str) constr_map
   1.119        |> fold (add_eval_const o apsnd Code_Printer.str) const_map
   1.120 -  | process (code_body, _) _ (SOME file_name) thy =
   1.121 +  | process_reflection (code_body, _) _ (SOME file_name) thy =
   1.122        let
   1.123          val preamble =
   1.124            "(* Generated from " ^ Path.implode (Thy_Header.thy_path (Context.theory_name thy))
   1.125 @@ -283,7 +295,7 @@
   1.126        |> (apsnd o apsnd) (chop (length constrs));
   1.127    in
   1.128      thy
   1.129 -    |> process result module_name some_file
   1.130 +    |> process_reflection result module_name some_file
   1.131    end;
   1.132  
   1.133  val code_reflect = gen_code_reflect Code_Target.cert_tyco (K I);