src/HOL/Tools/code_evaluation.ML
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (23 months ago)
changeset 66695 91500c024c7f
parent 66330 dcb3e6bdc00a
child 67149 e61557884799
permissions -rw-r--r--
tuned;
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@39564
    12
  val put_term: (unit -> term) -> Proof.context -> Proof.context
haftmann@39564
    13
  val tracing: string -> 'a -> 'a
haftmann@39564
    14
end;
haftmann@39564
    15
haftmann@39564
    16
structure Code_Evaluation : CODE_EVALUATION =
haftmann@39564
    17
struct
haftmann@39564
    18
haftmann@39564
    19
(** term_of instances **)
haftmann@39564
    20
haftmann@39564
    21
(* formal definition *)
haftmann@39564
    22
haftmann@66330
    23
fun add_term_of_inst tyco thy =
haftmann@39564
    24
  let
haftmann@66330
    25
    val ((raw_vs, _), _) = Code.get_type thy tyco;
haftmann@39564
    26
    val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs;
haftmann@39564
    27
    val ty = Type (tyco, map TFree vs);
haftmann@39564
    28
    val lhs = Const (@{const_name term_of}, ty --> @{typ term})
haftmann@39564
    29
      $ Free ("x", ty);
haftmann@39564
    30
    val rhs = @{term "undefined :: term"};
haftmann@39564
    31
    val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
haftmann@39564
    32
    fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst
haftmann@39564
    33
      o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv";
haftmann@39564
    34
  in
haftmann@39564
    35
    thy
haftmann@39564
    36
    |> Class.instantiation ([tyco], vs, @{sort term_of})
haftmann@39564
    37
    |> `(fn lthy => Syntax.check_term lthy eq)
wenzelm@63180
    38
    |-> (fn eq => Specification.definition NONE [] [] ((Binding.name (triv_name_of eq), []), eq))
haftmann@39564
    39
    |> snd
wenzelm@59498
    40
    |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
haftmann@39564
    41
  end;
haftmann@39564
    42
haftmann@66330
    43
fun ensure_term_of_inst tyco thy =
haftmann@39564
    44
  let
wenzelm@48272
    45
    val need_inst = not (Sorts.has_instance (Sign.classes_of thy) tyco @{sort term_of})
wenzelm@48272
    46
      andalso Sorts.has_instance (Sign.classes_of thy) tyco @{sort typerep};
haftmann@66330
    47
  in if need_inst then add_term_of_inst tyco thy else thy end;
haftmann@61667
    48
haftmann@61667
    49
fun for_term_of_instance tyco vs f thy =
haftmann@61667
    50
  let
haftmann@61667
    51
    val algebra = Sign.classes_of thy;
haftmann@61667
    52
  in
haftmann@61667
    53
    case try (Sorts.mg_domain algebra tyco) @{sort term_of} of
haftmann@61667
    54
      NONE => thy
haftmann@61667
    55
    | SOME sorts => f tyco (map2 (fn (v, sort) => fn sort' =>
haftmann@61667
    56
        (v, Sorts.inter_sort algebra (sort, sort'))) vs sorts) thy
haftmann@61667
    57
  end;
haftmann@39564
    58
haftmann@39564
    59
haftmann@39564
    60
(* code equations for datatypes *)
haftmann@39564
    61
haftmann@40726
    62
fun mk_term_of_eq thy ty (c, (_, tys)) =
haftmann@39564
    63
  let
haftmann@39564
    64
    val t = list_comb (Const (c, tys ---> ty),
wenzelm@43329
    65
      map Free (Name.invent_names Name.context "a" tys));
haftmann@39564
    66
    val (arg, rhs) =
wenzelm@59621
    67
      apply2 (Thm.global_cterm_of thy o Logic.unvarify_types_global o Logic.varify_global)
wenzelm@45344
    68
        (t,
wenzelm@45344
    69
          map_aterms (fn t as Free (_, ty) => HOLogic.mk_term_of ty t | t => t)
wenzelm@45344
    70
            (HOLogic.reflect_term t));
wenzelm@59621
    71
    val cty = Thm.global_ctyp_of thy ty;
haftmann@39564
    72
  in
haftmann@39564
    73
    @{thm term_of_anything}
wenzelm@60801
    74
    |> Thm.instantiate' [SOME cty] [SOME arg, SOME rhs]
haftmann@39564
    75
    |> Thm.varifyT_global
haftmann@39564
    76
  end;
haftmann@39564
    77
haftmann@66330
    78
fun add_term_of_code_datatype tyco vs raw_cs thy =
haftmann@39564
    79
  let
haftmann@39564
    80
    val ty = Type (tyco, map TFree vs);
haftmann@40726
    81
    val cs = (map o apsnd o apsnd o map o map_atyps)
haftmann@39564
    82
      (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
haftmann@39565
    83
    val eqs = map (mk_term_of_eq thy ty) cs;
haftmann@39564
    84
 in
haftmann@39564
    85
    thy
haftmann@66251
    86
    |> Code.declare_default_eqns_global (map (rpair true) eqs)
haftmann@39564
    87
  end;
haftmann@39564
    88
haftmann@66330
    89
fun ensure_term_of_code_datatype (tyco, (vs, cs)) =
haftmann@66330
    90
  for_term_of_instance tyco vs (fn tyco => fn vs => add_term_of_code_datatype tyco vs cs);
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))
wenzelm@59621
   100
      |> Thm.global_cterm_of thy;
wenzelm@59621
   101
    val cty = Thm.global_ctyp_of thy ty;
haftmann@39564
   102
  in
haftmann@39564
   103
    @{thm term_of_anything}
wenzelm@60801
   104
    |> Thm.instantiate' [SOME cty] [SOME (Thm.global_cterm_of thy arg), SOME rhs]
haftmann@39564
   105
    |> Thm.varifyT_global
haftmann@39564
   106
  end;
haftmann@39564
   107
haftmann@66330
   108
fun add_term_of_code_abstype tyco vs abs raw_ty_rep projection thy =
haftmann@39564
   109
  let
haftmann@39564
   110
    val ty = Type (tyco, map TFree vs);
haftmann@39564
   111
    val ty_rep = map_atyps
haftmann@39564
   112
      (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_ty_rep;
haftmann@66330
   113
    val eq = mk_abs_term_of_eq thy ty abs ty_rep projection;
haftmann@39564
   114
 in
haftmann@39564
   115
    thy
haftmann@66251
   116
    |> Code.declare_default_eqns_global [(eq, true)]
haftmann@39564
   117
  end;
haftmann@39564
   118
haftmann@66330
   119
fun ensure_term_of_code_abstype (tyco, (vs, {abstractor = (abs, (_, ty)),
haftmann@66310
   120
    projection, ...})) =
haftmann@61667
   121
  for_term_of_instance tyco vs
haftmann@66330
   122
    (fn tyco => fn vs => add_term_of_code_abstype tyco vs abs ty projection);
haftmann@39564
   123
haftmann@39564
   124
haftmann@56926
   125
(* setup *)
haftmann@56926
   126
haftmann@59323
   127
val _ = Theory.setup
haftmann@66330
   128
  (Code.type_interpretation ensure_term_of_inst
haftmann@66330
   129
  #> Code.datatype_interpretation ensure_term_of_code_datatype
haftmann@66330
   130
  #> Code.abstype_interpretation ensure_term_of_code_abstype);
haftmann@56926
   131
haftmann@56926
   132
haftmann@39564
   133
(** termifying syntax **)
haftmann@39564
   134
haftmann@39564
   135
fun map_default f xs =
haftmann@39564
   136
  let val ys = map f xs
haftmann@39564
   137
  in if exists is_some ys
haftmann@39564
   138
    then SOME (map2 the_default xs ys)
haftmann@39564
   139
    else NONE
haftmann@39564
   140
  end;
haftmann@39564
   141
haftmann@39565
   142
fun subst_termify_app (Const (@{const_name termify}, _), [t]) =
wenzelm@63619
   143
      if not (Term.exists_subterm (fn Abs _ => true | _ => false) t)
haftmann@39564
   144
      then if fold_aterms (fn Const _ => I | _ => K false) t true
haftmann@39564
   145
        then SOME (HOLogic.reflect_term t)
haftmann@51714
   146
        else error "Cannot termify expression containing variable"
haftmann@39564
   147
      else error "Cannot termify expression containing abstraction"
haftmann@39564
   148
  | subst_termify_app (t, ts) = case map_default subst_termify ts
haftmann@39564
   149
     of SOME ts' => SOME (list_comb (t, ts'))
haftmann@39564
   150
      | NONE => NONE
haftmann@39564
   151
and subst_termify (Abs (v, T, t)) = (case subst_termify t
haftmann@39564
   152
     of SOME t' => SOME (Abs (v, T, t'))
haftmann@39564
   153
      | NONE => NONE)
haftmann@39564
   154
  | subst_termify t = subst_termify_app (strip_comb t) 
haftmann@39564
   155
wenzelm@62952
   156
fun check_termify ts = the_default ts (map_default subst_termify ts);
haftmann@39564
   157
wenzelm@62952
   158
val _ = Context.>> (Syntax_Phases.term_check 0 "termify" (K check_termify));
haftmann@56926
   159
haftmann@39564
   160
haftmann@39564
   161
(** evaluation **)
haftmann@39564
   162
wenzelm@41472
   163
structure Evaluation = Proof_Data
wenzelm@41472
   164
(
haftmann@39564
   165
  type T = unit -> term
wenzelm@59153
   166
  val empty: T = fn () => raise Fail "Evaluation"
wenzelm@59153
   167
  fun init _ = empty
haftmann@39564
   168
);
haftmann@39564
   169
val put_term = Evaluation.put;
haftmann@39565
   170
val cookie = (Evaluation.get, put_term, "Code_Evaluation.put_term");
haftmann@39565
   171
haftmann@39565
   172
fun mk_term_of t = HOLogic.mk_term_of (fastype_of t) t;
haftmann@39565
   173
haftmann@63157
   174
fun gen_dynamic_value computation ctxt t =
haftmann@63157
   175
  computation cookie ctxt NONE I (mk_term_of t) [];
haftmann@39565
   176
haftmann@39565
   177
val dynamic_value = gen_dynamic_value Code_Runtime.dynamic_value;
haftmann@39565
   178
val dynamic_value_strict = gen_dynamic_value Code_Runtime.dynamic_value_strict;
haftmann@39565
   179
val dynamic_value_exn = gen_dynamic_value Code_Runtime.dynamic_value_exn;
haftmann@39565
   180
haftmann@39565
   181
haftmann@39565
   182
(** diagnostic **)
haftmann@39564
   183
haftmann@39564
   184
fun tracing s x = (Output.tracing s; x);
haftmann@39564
   185
haftmann@39564
   186
end;