src/HOL/Tools/code_evaluation.ML
author haftmann
Thu May 26 15:27:50 2016 +0200 (2016-05-26)
changeset 63157 65a81a4ef7f8
parent 63064 2f18172214c8
child 63161 2660ba498798
permissions -rw-r--r--
clarified naming conventions and code for code evaluation sandwiches
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@55757
     9
  val dynamic_value: Proof.context -> term -> term option
haftmann@55757
    10
  val dynamic_value_strict: Proof.context -> term -> term
haftmann@55757
    11
  val dynamic_value_exn: Proof.context -> term -> term Exn.result
haftmann@56973
    12
  val static_value: { ctxt: Proof.context, consts: string list, Ts: typ list }
haftmann@56973
    13
    -> Proof.context -> term -> term option
haftmann@56973
    14
  val static_value_strict: { ctxt: Proof.context, consts: string list, Ts: typ list }
haftmann@56973
    15
    -> Proof.context -> term -> term
haftmann@56973
    16
  val static_value_exn: { ctxt: Proof.context, consts: string list, Ts: typ list }
haftmann@56973
    17
    -> Proof.context -> term -> term Exn.result
haftmann@55757
    18
  val dynamic_conv: Proof.context -> conv
haftmann@56973
    19
  val static_conv: { ctxt: Proof.context, consts: string list, Ts: typ list }
haftmann@56973
    20
    -> Proof.context -> conv
haftmann@39564
    21
  val put_term: (unit -> term) -> Proof.context -> Proof.context
haftmann@39564
    22
  val tracing: string -> 'a -> 'a
haftmann@39564
    23
end;
haftmann@39564
    24
haftmann@39564
    25
structure Code_Evaluation : CODE_EVALUATION =
haftmann@39564
    26
struct
haftmann@39564
    27
haftmann@39564
    28
(** term_of instances **)
haftmann@39564
    29
haftmann@39564
    30
(* formal definition *)
haftmann@39564
    31
haftmann@39564
    32
fun add_term_of tyco raw_vs thy =
haftmann@39564
    33
  let
haftmann@39564
    34
    val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs;
haftmann@39564
    35
    val ty = Type (tyco, map TFree vs);
haftmann@39564
    36
    val lhs = Const (@{const_name term_of}, ty --> @{typ term})
haftmann@39564
    37
      $ Free ("x", ty);
haftmann@39564
    38
    val rhs = @{term "undefined :: term"};
haftmann@39564
    39
    val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
haftmann@39564
    40
    fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst
haftmann@39564
    41
      o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv";
haftmann@39564
    42
  in
haftmann@39564
    43
    thy
haftmann@39564
    44
    |> Class.instantiation ([tyco], vs, @{sort term_of})
haftmann@39564
    45
    |> `(fn lthy => Syntax.check_term lthy eq)
wenzelm@63064
    46
    |-> (fn eq => Specification.definition NONE [] ((Binding.name (triv_name_of eq), []), eq))
haftmann@39564
    47
    |> snd
wenzelm@59498
    48
    |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
haftmann@39564
    49
  end;
haftmann@39564
    50
haftmann@61667
    51
fun ensure_term_of (tyco, (vs, _)) thy =
haftmann@39564
    52
  let
wenzelm@48272
    53
    val need_inst = not (Sorts.has_instance (Sign.classes_of thy) tyco @{sort term_of})
wenzelm@48272
    54
      andalso Sorts.has_instance (Sign.classes_of thy) tyco @{sort typerep};
haftmann@61667
    55
  in if need_inst then add_term_of tyco vs thy else thy end;
haftmann@61667
    56
haftmann@61667
    57
fun for_term_of_instance tyco vs f thy =
haftmann@61667
    58
  let
haftmann@61667
    59
    val algebra = Sign.classes_of thy;
haftmann@61667
    60
  in
haftmann@61667
    61
    case try (Sorts.mg_domain algebra tyco) @{sort term_of} of
haftmann@61667
    62
      NONE => thy
haftmann@61667
    63
    | SOME sorts => f tyco (map2 (fn (v, sort) => fn sort' =>
haftmann@61667
    64
        (v, Sorts.inter_sort algebra (sort, sort'))) vs sorts) thy
haftmann@61667
    65
  end;
haftmann@39564
    66
haftmann@39564
    67
haftmann@39564
    68
(* code equations for datatypes *)
haftmann@39564
    69
haftmann@40726
    70
fun mk_term_of_eq thy ty (c, (_, tys)) =
haftmann@39564
    71
  let
haftmann@39564
    72
    val t = list_comb (Const (c, tys ---> ty),
wenzelm@43329
    73
      map Free (Name.invent_names Name.context "a" tys));
haftmann@39564
    74
    val (arg, rhs) =
wenzelm@59621
    75
      apply2 (Thm.global_cterm_of thy o Logic.unvarify_types_global o Logic.varify_global)
wenzelm@45344
    76
        (t,
wenzelm@45344
    77
          map_aterms (fn t as Free (_, ty) => HOLogic.mk_term_of ty t | t => t)
wenzelm@45344
    78
            (HOLogic.reflect_term t));
wenzelm@59621
    79
    val cty = Thm.global_ctyp_of thy ty;
haftmann@39564
    80
  in
haftmann@39564
    81
    @{thm term_of_anything}
wenzelm@60801
    82
    |> Thm.instantiate' [SOME cty] [SOME arg, SOME rhs]
haftmann@39564
    83
    |> Thm.varifyT_global
haftmann@39564
    84
  end;
haftmann@39564
    85
haftmann@61667
    86
fun add_term_of_code tyco vs raw_cs thy =
haftmann@39564
    87
  let
haftmann@39564
    88
    val ty = Type (tyco, map TFree vs);
haftmann@40726
    89
    val cs = (map o apsnd o apsnd o map o map_atyps)
haftmann@39564
    90
      (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
wenzelm@51685
    91
    val const = Axclass.param_of_inst thy (@{const_name term_of}, tyco);
haftmann@39565
    92
    val eqs = map (mk_term_of_eq thy ty) cs;
haftmann@39564
    93
 in
haftmann@39564
    94
    thy
haftmann@39564
    95
    |> Code.del_eqns const
haftmann@39564
    96
    |> fold Code.add_eqn eqs
haftmann@39564
    97
  end;
haftmann@39564
    98
haftmann@61667
    99
fun ensure_term_of_code (tyco, (vs, cs)) =
haftmann@61667
   100
  for_term_of_instance tyco vs (fn tyco => fn vs => add_term_of_code tyco vs cs);
haftmann@39564
   101
haftmann@39564
   102
haftmann@39564
   103
(* code equations for abstypes *)
haftmann@39564
   104
haftmann@39565
   105
fun mk_abs_term_of_eq thy ty abs ty_rep proj =
haftmann@39564
   106
  let
haftmann@39564
   107
    val arg = Var (("x", 0), ty);
haftmann@39564
   108
    val rhs = Abs ("y", @{typ term}, HOLogic.reflect_term (Const (abs, ty_rep --> ty) $ Bound 0)) $
haftmann@39564
   109
      (HOLogic.mk_term_of ty_rep (Const (proj, ty --> ty_rep) $ arg))
wenzelm@59621
   110
      |> Thm.global_cterm_of thy;
wenzelm@59621
   111
    val cty = Thm.global_ctyp_of thy ty;
haftmann@39564
   112
  in
haftmann@39564
   113
    @{thm term_of_anything}
wenzelm@60801
   114
    |> Thm.instantiate' [SOME cty] [SOME (Thm.global_cterm_of thy arg), SOME rhs]
haftmann@39564
   115
    |> Thm.varifyT_global
haftmann@39564
   116
  end;
haftmann@39564
   117
haftmann@61667
   118
fun add_abs_term_of_code tyco vs abs raw_ty_rep proj thy =
haftmann@39564
   119
  let
haftmann@39564
   120
    val ty = Type (tyco, map TFree vs);
haftmann@39564
   121
    val ty_rep = map_atyps
haftmann@39564
   122
      (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_ty_rep;
wenzelm@51685
   123
    val const = Axclass.param_of_inst thy (@{const_name term_of}, tyco);
haftmann@39565
   124
    val eq = mk_abs_term_of_eq thy ty abs ty_rep proj;
haftmann@39564
   125
 in
haftmann@39564
   126
    thy
haftmann@39564
   127
    |> Code.del_eqns const
haftmann@39564
   128
    |> Code.add_eqn eq
haftmann@39564
   129
  end;
haftmann@39564
   130
haftmann@61667
   131
fun ensure_abs_term_of_code (tyco, (vs, ((abs, (_, ty)), (proj, _)))) =
haftmann@61667
   132
  for_term_of_instance tyco vs
haftmann@61667
   133
    (fn tyco => fn vs => add_abs_term_of_code tyco vs abs ty proj);
haftmann@39564
   134
haftmann@39564
   135
haftmann@56926
   136
(* setup *)
haftmann@56926
   137
haftmann@59323
   138
val _ = Theory.setup
haftmann@56926
   139
  (Code.datatype_interpretation ensure_term_of
haftmann@56926
   140
  #> Code.abstype_interpretation ensure_term_of
haftmann@56926
   141
  #> Code.datatype_interpretation ensure_term_of_code
haftmann@59323
   142
  #> Code.abstype_interpretation ensure_abs_term_of_code);
haftmann@56926
   143
haftmann@56926
   144
haftmann@39564
   145
(** termifying syntax **)
haftmann@39564
   146
haftmann@39564
   147
fun map_default f xs =
haftmann@39564
   148
  let val ys = map f xs
haftmann@39564
   149
  in if exists is_some ys
haftmann@39564
   150
    then SOME (map2 the_default xs ys)
haftmann@39564
   151
    else NONE
haftmann@39564
   152
  end;
haftmann@39564
   153
haftmann@39565
   154
fun subst_termify_app (Const (@{const_name termify}, _), [t]) =
haftmann@39564
   155
      if not (Term.has_abs t)
haftmann@39564
   156
      then if fold_aterms (fn Const _ => I | _ => K false) t true
haftmann@39564
   157
        then SOME (HOLogic.reflect_term t)
haftmann@51714
   158
        else error "Cannot termify expression containing variable"
haftmann@39564
   159
      else error "Cannot termify expression containing abstraction"
haftmann@39564
   160
  | subst_termify_app (t, ts) = case map_default subst_termify ts
haftmann@39564
   161
     of SOME ts' => SOME (list_comb (t, ts'))
haftmann@39564
   162
      | NONE => NONE
haftmann@39564
   163
and subst_termify (Abs (v, T, t)) = (case subst_termify t
haftmann@39564
   164
     of SOME t' => SOME (Abs (v, T, t'))
haftmann@39564
   165
      | NONE => NONE)
haftmann@39564
   166
  | subst_termify t = subst_termify_app (strip_comb t) 
haftmann@39564
   167
wenzelm@62952
   168
fun check_termify ts = the_default ts (map_default subst_termify ts);
haftmann@39564
   169
wenzelm@62952
   170
val _ = Context.>> (Syntax_Phases.term_check 0 "termify" (K check_termify));
haftmann@56926
   171
haftmann@39564
   172
haftmann@39564
   173
(** evaluation **)
haftmann@39564
   174
wenzelm@41472
   175
structure Evaluation = Proof_Data
wenzelm@41472
   176
(
haftmann@39564
   177
  type T = unit -> term
wenzelm@59153
   178
  val empty: T = fn () => raise Fail "Evaluation"
wenzelm@59153
   179
  fun init _ = empty
haftmann@39564
   180
);
haftmann@39564
   181
val put_term = Evaluation.put;
haftmann@39565
   182
val cookie = (Evaluation.get, put_term, "Code_Evaluation.put_term");
haftmann@39565
   183
haftmann@39565
   184
fun mk_term_of t = HOLogic.mk_term_of (fastype_of t) t;
haftmann@39565
   185
wenzelm@51685
   186
fun term_of_const_for thy = Axclass.unoverload_const thy o dest_Const o HOLogic.term_of_const;
haftmann@39565
   187
haftmann@63157
   188
fun gen_dynamic_value computation ctxt t =
haftmann@63157
   189
  computation cookie ctxt NONE I (mk_term_of t) [];
haftmann@39565
   190
haftmann@39565
   191
val dynamic_value = gen_dynamic_value Code_Runtime.dynamic_value;
haftmann@39565
   192
val dynamic_value_strict = gen_dynamic_value Code_Runtime.dynamic_value_strict;
haftmann@39565
   193
val dynamic_value_exn = gen_dynamic_value Code_Runtime.dynamic_value_exn;
haftmann@39565
   194
haftmann@63157
   195
fun gen_static_value computation { ctxt, consts, Ts } =
haftmann@55757
   196
  let
haftmann@63157
   197
    val computation' = computation cookie
haftmann@56973
   198
      { ctxt = ctxt, target = NONE, lift_postproc = I, consts =
haftmann@56973
   199
        union (op =) (map (term_of_const_for (Proof_Context.theory_of ctxt)) Ts) consts }
haftmann@63157
   200
  in fn ctxt' => computation' ctxt' o mk_term_of end;
haftmann@39565
   201
haftmann@39565
   202
val static_value = gen_static_value Code_Runtime.static_value;
haftmann@39565
   203
val static_value_strict = gen_static_value Code_Runtime.static_value_strict;
haftmann@39565
   204
val static_value_exn = gen_static_value Code_Runtime.static_value_exn;
haftmann@39565
   205
haftmann@55757
   206
fun certify_eval ctxt value conv ct =
haftmann@39567
   207
  let
haftmann@39567
   208
    val t = Thm.term_of ct;
haftmann@39567
   209
    val T = fastype_of t;
wenzelm@59617
   210
    val mk_eq =
wenzelm@59621
   211
      Thm.mk_binop (Thm.cterm_of ctxt (Const (@{const_name Pure.eq}, T --> T --> propT)));
haftmann@55757
   212
  in case value ctxt t
haftmann@39567
   213
   of NONE => Thm.reflexive ct
wenzelm@59621
   214
    | SOME t' => conv ctxt (mk_eq ct (Thm.cterm_of ctxt t')) RS @{thm eq_eq_TrueD}
haftmann@39567
   215
        handle THM _ =>
haftmann@55757
   216
          error ("Failed to certify evaluation result of " ^ Syntax.string_of_term ctxt t)
haftmann@39567
   217
  end;
haftmann@39567
   218
haftmann@55757
   219
fun dynamic_conv ctxt = certify_eval ctxt dynamic_value
haftmann@55757
   220
  Code_Runtime.dynamic_holds_conv;
haftmann@39567
   221
haftmann@56973
   222
fun static_conv { ctxt, consts, Ts }  =
haftmann@39567
   223
  let
wenzelm@56245
   224
    val eqs = @{const_name Pure.eq} :: @{const_name HOL.eq} ::
haftmann@55757
   225
      map (fn T => Axclass.unoverload_const (Proof_Context.theory_of ctxt)
wenzelm@56245
   226
        (@{const_name HOL.equal}, T)) Ts; (*assumes particular code equations for Pure.eq etc.*)
haftmann@56973
   227
    val value = static_value { ctxt = ctxt, consts = consts, Ts = Ts };
haftmann@56973
   228
    val holds = Code_Runtime.static_holds_conv { ctxt = ctxt, consts = union (op =) eqs consts };
haftmann@39567
   229
  in
haftmann@55757
   230
    fn ctxt' => certify_eval ctxt' value holds
haftmann@39567
   231
  end;
haftmann@39567
   232
haftmann@39565
   233
haftmann@39565
   234
(** diagnostic **)
haftmann@39564
   235
haftmann@39564
   236
fun tracing s x = (Output.tracing s; x);
haftmann@39564
   237
haftmann@39564
   238
end;