dynamic and static value computation; built-in evaluation of propositions
authorhaftmann
Thu Sep 16 16:51:34 2010 +0200 (2010-09-16)
changeset 3947333638f4883ac
parent 39472 1cf49add5b40
child 39474 1986f18c4940
dynamic and static value computation; built-in evaluation of propositions
src/Tools/Code/code_runtime.ML
     1.1 --- a/src/Tools/Code/code_runtime.ML	Thu Sep 16 16:51:33 2010 +0200
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Thu Sep 16 16:51:34 2010 +0200
     1.3 @@ -7,41 +7,139 @@
     1.4  signature CODE_RUNTIME =
     1.5  sig
     1.6    val target: string
     1.7 -  val value: string option
     1.8 -    -> (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string
     1.9 -    -> ((term -> term) -> 'a -> 'a) -> theory -> term -> string list -> 'a
    1.10 +  type 'a cookie = (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string
    1.11 +  val dynamic_value: 'a cookie -> theory -> string option
    1.12 +    -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a option
    1.13 +  val dynamic_value_strict: 'a cookie -> theory -> string option
    1.14 +    -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a
    1.15 +  val dynamic_value_exn: 'a cookie -> theory -> string option
    1.16 +    -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a Exn.result
    1.17 +  val static_value: 'a cookie -> theory -> string option
    1.18 +    -> ((term -> term) -> 'a -> 'a) -> string list -> term -> 'a option
    1.19 +  val static_value_strict: 'a cookie -> theory -> string option
    1.20 +    -> ((term -> term) -> 'a -> 'a) -> string list -> term -> 'a
    1.21 +  val static_value_exn: 'a cookie -> theory -> string option
    1.22 +    -> ((term -> term) -> 'a -> 'a) -> string list -> term -> 'a Exn.result
    1.23 +  val dynamic_holds_conv: conv
    1.24 +  val static_holds_conv: theory -> string list -> conv
    1.25    val code_reflect: (string * string list) list -> string list -> string -> string option
    1.26      -> theory -> theory
    1.27 -  val setup: theory -> theory
    1.28 +  datatype truth = Holds
    1.29 +  val put_truth: (unit -> truth) -> Proof.context -> Proof.context
    1.30  end;
    1.31  
    1.32  structure Code_Runtime : CODE_RUNTIME =
    1.33  struct
    1.34  
    1.35 +open Basic_Code_Thingol;
    1.36 +
    1.37  (** evaluation **)
    1.38  
    1.39 +(* technical prerequisites *)
    1.40 +
    1.41 +val this = "Code_Runtime";
    1.42 +val s_truth = Long_Name.append this "truth";
    1.43 +val s_Holds = Long_Name.append this "Holds";
    1.44 +
    1.45  val target = "Eval";
    1.46  
    1.47 -val truth_struct = "Code_Truth";
    1.48 +datatype truth = Holds;
    1.49  
    1.50 -fun value some_target cookie postproc thy t args =
    1.51 +val _ = Context.>> (Context.map_theory
    1.52 +  (Code_Target.extend_target (target, (Code_ML.target_SML, K I))
    1.53 +  #> Code_Target.add_tyco_syntax target @{type_name prop} (SOME (0, (K o K o K) (Code_Printer.str s_truth)))
    1.54 +  #> Code_Target.add_const_syntax target @{const_name Code_Generator.holds} (SOME (Code_Printer.plain_const_syntax s_Holds))
    1.55 +  #> Code_Target.add_reserved target this
    1.56 +  #> fold (Code_Target.add_reserved target) ["oo", "ooo", "oooo", "upto", "downto", "orf", "andf"])); (*avoid further pervasive infix names*)
    1.57 +
    1.58 +
    1.59 +(* evaluation into target language values *)
    1.60 +
    1.61 +type 'a cookie = (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string;
    1.62 +
    1.63 +fun base_evaluator cookie thy some_target naming program ((_, (vs, ty)), t) deps args =
    1.64    let
    1.65      val ctxt = ProofContext.init_global thy;
    1.66 -    fun evaluator naming program ((_, (_, ty)), t) deps =
    1.67 -      let
    1.68 -        val _ = if Code_Thingol.contains_dictvar t then
    1.69 -          error "Term to be evaluated contains free dictionaries" else ();
    1.70 -        val value_name = "Value.VALUE.value"
    1.71 -        val program' = program
    1.72 -          |> Graph.new_node (value_name,
    1.73 -              Code_Thingol.Fun (Term.dummy_patternN, ((([], ty), [(([], t), (NONE, true))]), NONE)))
    1.74 -          |> fold (curry Graph.add_edge value_name) deps;
    1.75 -        val (program_code, [SOME value_name']) = Code_Target.produce_code_for thy
    1.76 -          (the_default target some_target) NONE "Code" [] naming program' [value_name];
    1.77 -        val value_code = space_implode " "
    1.78 -          (value_name' :: map (enclose "(" ")") args);
    1.79 -      in ML_Context.value ctxt cookie (program_code, value_code) end;
    1.80 -  in Code_Thingol.dynamic_eval_value thy postproc evaluator t end;
    1.81 +    val _ = if Code_Thingol.contains_dictvar t then
    1.82 +      error "Term to be evaluated contains free dictionaries" else ();
    1.83 +    val v' = Name.variant (map fst vs) "a";
    1.84 +    val vs' = (v', []) :: vs
    1.85 +    val ty' = Code_Thingol.fun_tyco `%% [ITyVar v', ty];
    1.86 +    val value_name = "Value.value.value"
    1.87 +    val program' = program
    1.88 +      |> Graph.new_node (value_name,
    1.89 +          Code_Thingol.Fun (Term.dummy_patternN, (((vs', ty'), [(([IVar NONE], t), (NONE, true))]), NONE)))
    1.90 +      |> fold (curry Graph.add_edge value_name) deps;
    1.91 +    val (program_code, [SOME value_name']) = Code_Target.produce_code_for thy
    1.92 +      (the_default target some_target) NONE "Code" [] naming program' [value_name];
    1.93 +    val value_code = space_implode " "
    1.94 +      (value_name' :: "()" :: map (enclose "(" ")") args);
    1.95 +  in Exn.capture (ML_Context.value ctxt cookie) (program_code, value_code) end;
    1.96 +
    1.97 +fun partiality_as_none e = SOME (Exn.release e)
    1.98 +  handle General.Match => NONE
    1.99 +    | General.Bind => NONE
   1.100 +    | General.Fail _ => NONE;
   1.101 +
   1.102 +fun dynamic_value_exn cookie thy some_target postproc t args =
   1.103 +  let
   1.104 +    fun evaluator naming program expr deps =
   1.105 +      base_evaluator cookie thy some_target naming program expr deps args;
   1.106 +  in Code_Thingol.dynamic_eval_value thy (Exn.map_result o postproc) evaluator t end;
   1.107 +
   1.108 +fun dynamic_value_strict cookie thy some_target postproc t args =
   1.109 +  Exn.release (dynamic_value_exn cookie thy some_target postproc t args);
   1.110 +
   1.111 +fun dynamic_value cookie thy some_target postproc t args =
   1.112 +  partiality_as_none (dynamic_value_exn cookie thy some_target postproc t args);
   1.113 +
   1.114 +fun static_value_exn cookie thy some_target postproc consts =
   1.115 +  let
   1.116 +    fun evaluator naming program thy expr deps =
   1.117 +      base_evaluator cookie thy some_target naming program expr deps [];
   1.118 +  in Code_Thingol.static_eval_value thy (Exn.map_result o postproc) consts evaluator end;
   1.119 +
   1.120 +fun static_value_strict cookie thy some_target postproc consts t =
   1.121 +  Exn.release (static_value_exn cookie thy some_target postproc consts t);
   1.122 +
   1.123 +fun static_value cookie thy some_target postproc consts t =
   1.124 +  partiality_as_none (static_value_exn cookie thy some_target postproc consts t);
   1.125 +
   1.126 +
   1.127 +(* evaluation for truth or nothing *)
   1.128 +
   1.129 +structure Truth_Result = Proof_Data (
   1.130 +  type T = unit -> truth
   1.131 +  fun init _ () = error "Truth_Result"
   1.132 +);
   1.133 +val put_truth = Truth_Result.put;
   1.134 +val truth_cookie = (Truth_Result.get, put_truth, Long_Name.append this "put_truth");
   1.135 +
   1.136 +fun check_holds thy naming program expr deps ct =
   1.137 +  let
   1.138 +    val t = Thm.term_of ct;
   1.139 +    val _ = if fastype_of t <> propT
   1.140 +      then error ("Not a proposition: " ^ Syntax.string_of_term_global thy t)
   1.141 +      else ();
   1.142 +    val iff = Thm.cterm_of thy (Term.Const ("==", propT --> propT --> propT));
   1.143 +    val result = case partiality_as_none (base_evaluator truth_cookie thy NONE naming program expr deps [])
   1.144 +     of SOME Holds => true
   1.145 +      | _ => false;
   1.146 +  in
   1.147 +    Thm.mk_binop iff ct (if result then @{cprop "PROP Code_Generator.holds"} else ct)
   1.148 +  end;
   1.149 +
   1.150 +val (_, raw_check_holds_oracle) = Context.>>> (Context.map_theory_result
   1.151 +  (Thm.add_oracle (Binding.name "holds_by_evaluation",
   1.152 +  fn (thy, naming, program, expr, deps, ct) => check_holds thy naming program expr deps ct)));
   1.153 +
   1.154 +fun check_holds_oracle thy naming program expr deps ct =
   1.155 +  raw_check_holds_oracle (thy, naming, program, expr, deps, ct);
   1.156 +
   1.157 +val dynamic_holds_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_eval_conv thy (check_holds_oracle thy));
   1.158 +
   1.159 +fun static_holds_conv thy consts = Code_Thingol.static_eval_conv thy consts
   1.160 +  (fn naming => fn program => fn thy => check_holds_oracle thy naming program);
   1.161  
   1.162  
   1.163  (** instrumentalization **)
   1.164 @@ -221,6 +319,4 @@
   1.165  
   1.166  end; (*local*)
   1.167  
   1.168 -val setup = Code_Target.extend_target (target, (Code_ML.target_SML, K I));
   1.169 -
   1.170  end; (*struct*)