src/HOL/Tools/code_evaluation.ML
author haftmann
Wed Dec 08 13:34:50 2010 +0100 (2010-12-08)
changeset 41075 4bed56dc95fb
parent 40726 16dcfedc4eb7
child 41184 5c6f44d22f51
permissions -rw-r--r--
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
haftmann@39564
     1
(*  Title:      HOL/Tools/code_evaluation.ML
haftmann@39564
     2
    Author:     Florian Haftmann, TU Muenchen
haftmann@39564
     3
haftmann@39564
     4
Evaluation and reconstruction of terms in ML.
haftmann@39564
     5
*)
haftmann@39564
     6
haftmann@39564
     7
signature CODE_EVALUATION =
haftmann@39564
     8
sig
haftmann@39565
     9
  val dynamic_value: theory -> term -> term option
haftmann@39564
    10
  val dynamic_value_strict: theory -> term -> term
haftmann@39565
    11
  val dynamic_value_exn: theory -> term -> term Exn.result
haftmann@39565
    12
  val static_value: theory -> string list -> typ list -> term -> term option
haftmann@39565
    13
  val static_value_strict: theory -> string list -> typ list -> term -> term
haftmann@39565
    14
  val static_value_exn: theory -> string list -> typ list -> term -> term Exn.result
haftmann@39567
    15
  val dynamic_eval_conv: conv
haftmann@39567
    16
  val static_eval_conv: theory -> string list -> typ list -> conv
haftmann@39564
    17
  val put_term: (unit -> term) -> Proof.context -> Proof.context
haftmann@39564
    18
  val tracing: string -> 'a -> 'a
haftmann@39564
    19
  val setup: theory -> theory
haftmann@39564
    20
end;
haftmann@39564
    21
haftmann@39564
    22
structure Code_Evaluation : CODE_EVALUATION =
haftmann@39564
    23
struct
haftmann@39564
    24
haftmann@39564
    25
(** term_of instances **)
haftmann@39564
    26
haftmann@39564
    27
(* formal definition *)
haftmann@39564
    28
haftmann@39564
    29
fun add_term_of tyco raw_vs thy =
haftmann@39564
    30
  let
haftmann@39564
    31
    val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs;
haftmann@39564
    32
    val ty = Type (tyco, map TFree vs);
haftmann@39564
    33
    val lhs = Const (@{const_name term_of}, ty --> @{typ term})
haftmann@39564
    34
      $ Free ("x", ty);
haftmann@39564
    35
    val rhs = @{term "undefined :: term"};
haftmann@39564
    36
    val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
haftmann@39564
    37
    fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst
haftmann@39564
    38
      o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv";
haftmann@39564
    39
  in
haftmann@39564
    40
    thy
haftmann@39564
    41
    |> Class.instantiation ([tyco], vs, @{sort term_of})
haftmann@39564
    42
    |> `(fn lthy => Syntax.check_term lthy eq)
haftmann@39564
    43
    |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq)))
haftmann@39564
    44
    |> snd
haftmann@39564
    45
    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
haftmann@39564
    46
  end;
haftmann@39564
    47
haftmann@39564
    48
fun ensure_term_of (tyco, (raw_vs, _)) thy =
haftmann@39564
    49
  let
haftmann@39564
    50
    val need_inst = not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of})
haftmann@39564
    51
      andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep};
haftmann@39564
    52
  in if need_inst then add_term_of tyco raw_vs thy else thy end;
haftmann@39564
    53
haftmann@39564
    54
haftmann@39564
    55
(* code equations for datatypes *)
haftmann@39564
    56
haftmann@40726
    57
fun mk_term_of_eq thy ty (c, (_, tys)) =
haftmann@39564
    58
  let
haftmann@39564
    59
    val t = list_comb (Const (c, tys ---> ty),
haftmann@39564
    60
      map Free (Name.names Name.context "a" tys));
haftmann@39564
    61
    val (arg, rhs) =
haftmann@39564
    62
      pairself (Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global)
haftmann@39565
    63
        (t, (map_aterms (fn t as Free (_, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t)
haftmann@39564
    64
    val cty = Thm.ctyp_of thy ty;
haftmann@39564
    65
  in
haftmann@39564
    66
    @{thm term_of_anything}
haftmann@39564
    67
    |> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs]
haftmann@39564
    68
    |> Thm.varifyT_global
haftmann@39564
    69
  end;
haftmann@39564
    70
haftmann@39564
    71
fun add_term_of_code tyco raw_vs raw_cs thy =
haftmann@39564
    72
  let
haftmann@39564
    73
    val algebra = Sign.classes_of thy;
haftmann@39564
    74
    val vs = map (fn (v, sort) =>
haftmann@39564
    75
      (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs;
haftmann@39564
    76
    val ty = Type (tyco, map TFree vs);
haftmann@40726
    77
    val cs = (map o apsnd o apsnd o map o map_atyps)
haftmann@39564
    78
      (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
haftmann@39564
    79
    val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
haftmann@39565
    80
    val eqs = map (mk_term_of_eq thy ty) cs;
haftmann@39564
    81
 in
haftmann@39564
    82
    thy
haftmann@39564
    83
    |> Code.del_eqns const
haftmann@39564
    84
    |> fold Code.add_eqn eqs
haftmann@39564
    85
  end;
haftmann@39564
    86
haftmann@39564
    87
fun ensure_term_of_code (tyco, (raw_vs, cs)) thy =
haftmann@39564
    88
  let
haftmann@39564
    89
    val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
haftmann@39564
    90
  in if has_inst then add_term_of_code tyco raw_vs cs thy else thy end;
haftmann@39564
    91
haftmann@39564
    92
haftmann@39564
    93
(* code equations for abstypes *)
haftmann@39564
    94
haftmann@39565
    95
fun mk_abs_term_of_eq thy ty abs ty_rep proj =
haftmann@39564
    96
  let
haftmann@39564
    97
    val arg = Var (("x", 0), ty);
haftmann@39564
    98
    val rhs = Abs ("y", @{typ term}, HOLogic.reflect_term (Const (abs, ty_rep --> ty) $ Bound 0)) $
haftmann@39564
    99
      (HOLogic.mk_term_of ty_rep (Const (proj, ty --> ty_rep) $ arg))
haftmann@39564
   100
      |> Thm.cterm_of thy;
haftmann@39564
   101
    val cty = Thm.ctyp_of thy ty;
haftmann@39564
   102
  in
haftmann@39564
   103
    @{thm term_of_anything}
haftmann@39564
   104
    |> Drule.instantiate' [SOME cty] [SOME (Thm.cterm_of thy arg), SOME rhs]
haftmann@39564
   105
    |> Thm.varifyT_global
haftmann@39564
   106
  end;
haftmann@39564
   107
haftmann@39564
   108
fun add_abs_term_of_code tyco raw_vs abs raw_ty_rep proj thy =
haftmann@39564
   109
  let
haftmann@39564
   110
    val algebra = Sign.classes_of thy;
haftmann@39564
   111
    val vs = map (fn (v, sort) =>
haftmann@39564
   112
      (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs;
haftmann@39564
   113
    val ty = Type (tyco, map TFree vs);
haftmann@39564
   114
    val ty_rep = map_atyps
haftmann@39564
   115
      (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_ty_rep;
haftmann@39564
   116
    val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
haftmann@39565
   117
    val eq = mk_abs_term_of_eq thy ty abs ty_rep proj;
haftmann@39564
   118
 in
haftmann@39564
   119
    thy
haftmann@39564
   120
    |> Code.del_eqns const
haftmann@39564
   121
    |> Code.add_eqn eq
haftmann@39564
   122
  end;
haftmann@39564
   123
haftmann@40726
   124
fun ensure_abs_term_of_code (tyco, (raw_vs, ((abs, (_, ty)), (proj, _)))) thy =
haftmann@39564
   125
  let
haftmann@39564
   126
    val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
haftmann@39564
   127
  in if has_inst then add_abs_term_of_code tyco raw_vs abs ty proj thy else thy end;
haftmann@39564
   128
haftmann@39564
   129
haftmann@39564
   130
(** termifying syntax **)
haftmann@39564
   131
haftmann@39564
   132
fun map_default f xs =
haftmann@39564
   133
  let val ys = map f xs
haftmann@39564
   134
  in if exists is_some ys
haftmann@39564
   135
    then SOME (map2 the_default xs ys)
haftmann@39564
   136
    else NONE
haftmann@39564
   137
  end;
haftmann@39564
   138
haftmann@39565
   139
fun subst_termify_app (Const (@{const_name termify}, _), [t]) =
haftmann@39564
   140
      if not (Term.has_abs t)
haftmann@39564
   141
      then if fold_aterms (fn Const _ => I | _ => K false) t true
haftmann@39564
   142
        then SOME (HOLogic.reflect_term t)
haftmann@39564
   143
        else error "Cannot termify expression containing variables"
haftmann@39564
   144
      else error "Cannot termify expression containing abstraction"
haftmann@39564
   145
  | subst_termify_app (t, ts) = case map_default subst_termify ts
haftmann@39564
   146
     of SOME ts' => SOME (list_comb (t, ts'))
haftmann@39564
   147
      | NONE => NONE
haftmann@39564
   148
and subst_termify (Abs (v, T, t)) = (case subst_termify t
haftmann@39564
   149
     of SOME t' => SOME (Abs (v, T, t'))
haftmann@39564
   150
      | NONE => NONE)
haftmann@39564
   151
  | subst_termify t = subst_termify_app (strip_comb t) 
haftmann@39564
   152
haftmann@39564
   153
fun check_termify ts ctxt = map_default subst_termify ts
haftmann@39564
   154
  |> Option.map (rpair ctxt)
haftmann@39564
   155
haftmann@39564
   156
haftmann@39564
   157
(** evaluation **)
haftmann@39564
   158
haftmann@39564
   159
structure Evaluation = Proof_Data (
haftmann@39564
   160
  type T = unit -> term
haftmann@39564
   161
  fun init _ () = error "Evaluation"
haftmann@39564
   162
);
haftmann@39564
   163
val put_term = Evaluation.put;
haftmann@39565
   164
val cookie = (Evaluation.get, put_term, "Code_Evaluation.put_term");
haftmann@39565
   165
haftmann@39565
   166
fun mk_term_of t = HOLogic.mk_term_of (fastype_of t) t;
haftmann@39565
   167
haftmann@39565
   168
fun term_of_const_for thy = AxClass.unoverload_const thy o dest_Const o HOLogic.term_of_const;
haftmann@39565
   169
haftmann@39565
   170
fun gen_dynamic_value dynamic_value thy t =
haftmann@39565
   171
  dynamic_value cookie thy NONE I (mk_term_of t) [];
haftmann@39565
   172
haftmann@39565
   173
val dynamic_value = gen_dynamic_value Code_Runtime.dynamic_value;
haftmann@39565
   174
val dynamic_value_strict = gen_dynamic_value Code_Runtime.dynamic_value_strict;
haftmann@39565
   175
val dynamic_value_exn = gen_dynamic_value Code_Runtime.dynamic_value_exn;
haftmann@39565
   176
haftmann@39565
   177
fun gen_static_value static_value thy consts Ts =
haftmann@39565
   178
  static_value cookie thy NONE I (union (op =) (map (term_of_const_for thy) Ts) consts)
haftmann@39565
   179
  o mk_term_of;
haftmann@39565
   180
haftmann@39565
   181
val static_value = gen_static_value Code_Runtime.static_value;
haftmann@39565
   182
val static_value_strict = gen_static_value Code_Runtime.static_value_strict;
haftmann@39565
   183
val static_value_exn = gen_static_value Code_Runtime.static_value_exn;
haftmann@39565
   184
haftmann@39567
   185
fun certify_eval thy value conv ct =
haftmann@39567
   186
  let
haftmann@39567
   187
    val t = Thm.term_of ct;
haftmann@39567
   188
    val T = fastype_of t;
haftmann@39567
   189
    val mk_eq = Thm.mk_binop (Thm.cterm_of thy (Const ("==", T --> T --> propT)));
haftmann@39567
   190
  in case value t
haftmann@39567
   191
   of NONE => Thm.reflexive ct
haftmann@39567
   192
    | SOME t' => conv (mk_eq ct (Thm.cterm_of thy t')) RS @{thm eq_eq_TrueD}
haftmann@39567
   193
        handle THM _ =>
haftmann@39567
   194
          error ("Failed to certify evaluation result of " ^ Syntax.string_of_term_global thy t)
haftmann@39567
   195
  end;
haftmann@39567
   196
haftmann@39567
   197
val dynamic_eval_conv = Conv.tap_thy
haftmann@39567
   198
  (fn thy => certify_eval thy (dynamic_value thy) Code_Runtime.dynamic_holds_conv);
haftmann@39567
   199
haftmann@39567
   200
fun static_eval_conv thy consts Ts =
haftmann@39567
   201
  let
haftmann@39567
   202
    val eqs = "==" :: @{const_name HOL.eq} ::
haftmann@39567
   203
      map (fn T => AxClass.unoverload_const thy (@{const_name HOL.equal}, T)) Ts;
haftmann@39567
   204
        (*assumes particular code equations for "==" etc.*)
haftmann@39567
   205
  in
haftmann@39567
   206
    certify_eval thy (static_value thy consts Ts)
haftmann@39567
   207
      (Code_Runtime.static_holds_conv thy (union (op =) eqs consts))
haftmann@39567
   208
  end;
haftmann@39567
   209
haftmann@39565
   210
haftmann@39565
   211
(** diagnostic **)
haftmann@39564
   212
haftmann@39564
   213
fun tracing s x = (Output.tracing s; x);
haftmann@39564
   214
haftmann@39564
   215
haftmann@39564
   216
(** setup **)
haftmann@39564
   217
haftmann@39564
   218
val setup =
haftmann@39564
   219
  Code.datatype_interpretation ensure_term_of
haftmann@39564
   220
  #> Code.abstype_interpretation ensure_term_of
haftmann@39564
   221
  #> Code.datatype_interpretation ensure_term_of_code
haftmann@39564
   222
  #> Code.abstype_interpretation ensure_abs_term_of_code
haftmann@39564
   223
  #> Context.theory_map (Syntax.add_term_check 0 "termify" check_termify)
haftmann@39564
   224
  #> Value.add_evaluator ("code", dynamic_value_strict o ProofContext.theory_of);
haftmann@39564
   225
haftmann@39564
   226
end;