src/HOL/Code_Eval.thy
author wenzelm
Mon Mar 16 18:24:30 2009 +0100 (2009-03-16)
changeset 30549 d2d7874648bd
parent 30427 dfd31c1db060
child 30947 dd551284a300
permissions -rw-r--r--
simplified method setup;
haftmann@28228
     1
(*  Title:      HOL/Code_Eval.thy
haftmann@28228
     2
    Author:     Florian Haftmann, TU Muenchen
haftmann@28228
     3
*)
haftmann@28228
     4
haftmann@28228
     5
header {* Term evaluation using the generic code generator *}
haftmann@28228
     6
haftmann@28228
     7
theory Code_Eval
haftmann@28952
     8
imports Plain Typerep
haftmann@28228
     9
begin
haftmann@28228
    10
haftmann@28228
    11
subsection {* Term representation *}
haftmann@28228
    12
haftmann@28228
    13
subsubsection {* Terms and class @{text term_of} *}
haftmann@28228
    14
haftmann@28228
    15
datatype "term" = dummy_term
haftmann@28228
    16
haftmann@28661
    17
definition Const :: "message_string \<Rightarrow> typerep \<Rightarrow> term" where
haftmann@28228
    18
  "Const _ _ = dummy_term"
haftmann@28228
    19
haftmann@28661
    20
definition App :: "term \<Rightarrow> term \<Rightarrow> term" where
haftmann@28228
    21
  "App _ _ = dummy_term"
haftmann@28228
    22
haftmann@28228
    23
code_datatype Const App
haftmann@28228
    24
haftmann@28335
    25
class term_of = typerep +
haftmann@29575
    26
  fixes term_of :: "'a::{} \<Rightarrow> term"
haftmann@28228
    27
haftmann@28228
    28
lemma term_of_anything: "term_of x \<equiv> t"
haftmann@28228
    29
  by (rule eq_reflection) (cases "term_of x", cases t, simp)
haftmann@28228
    30
haftmann@28228
    31
ML {*
haftmann@28228
    32
structure Eval =
haftmann@28228
    33
struct
haftmann@28228
    34
haftmann@28228
    35
fun mk_term f g (Const (c, ty)) =
haftmann@28228
    36
      @{term Const} $ Message_String.mk c $ g ty
haftmann@28228
    37
  | mk_term f g (t1 $ t2) =
haftmann@28228
    38
      @{term App} $ mk_term f g t1 $ mk_term f g t2
haftmann@28228
    39
  | mk_term f g (Free v) = f v
haftmann@28228
    40
  | mk_term f g (Bound i) = Bound i
haftmann@28228
    41
  | mk_term f g (Abs (v, _, t)) = Abs (v, @{typ term}, mk_term f g t);
haftmann@28228
    42
haftmann@28228
    43
fun mk_term_of ty t = Const (@{const_name term_of}, ty --> @{typ term}) $ t;
haftmann@28228
    44
haftmann@28228
    45
end;
haftmann@28228
    46
*}
haftmann@28228
    47
haftmann@28228
    48
haftmann@28228
    49
subsubsection {* @{text term_of} instances *}
haftmann@28228
    50
haftmann@28228
    51
setup {*
haftmann@28228
    52
let
haftmann@28228
    53
  fun add_term_of_def ty vs tyco thy =
haftmann@28228
    54
    let
haftmann@28228
    55
      val lhs = Const (@{const_name term_of}, ty --> @{typ term})
haftmann@28228
    56
        $ Free ("x", ty);
haftmann@28228
    57
      val rhs = @{term "undefined \<Colon> term"};
haftmann@28228
    58
      val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
haftmann@28243
    59
      fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst
haftmann@28243
    60
        o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv";
haftmann@28228
    61
    in
haftmann@28228
    62
      thy
haftmann@28228
    63
      |> TheoryTarget.instantiation ([tyco], vs, @{sort term_of})
haftmann@28228
    64
      |> `(fn lthy => Syntax.check_term lthy eq)
haftmann@28965
    65
      |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq)))
haftmann@28228
    66
      |> snd
haftmann@28228
    67
      |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
wenzelm@28394
    68
      |> LocalTheory.exit_global
haftmann@28228
    69
    end;
haftmann@28228
    70
  fun interpretator (tyco, (raw_vs, _)) thy =
haftmann@28228
    71
    let
haftmann@28228
    72
      val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
haftmann@28228
    73
      val constrain_sort =
haftmann@28228
    74
        curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of};
haftmann@28228
    75
      val vs = (map o apsnd) constrain_sort raw_vs;
haftmann@28228
    76
      val ty = Type (tyco, map TFree vs);
haftmann@28228
    77
    in
haftmann@28228
    78
      thy
haftmann@28335
    79
      |> Typerep.perhaps_add_def tyco
haftmann@28228
    80
      |> not has_inst ? add_term_of_def ty vs tyco
haftmann@28228
    81
    end;
haftmann@28228
    82
in
haftmann@28228
    83
  Code.type_interpretation interpretator
haftmann@28228
    84
end
haftmann@28228
    85
*}
haftmann@28228
    86
haftmann@28228
    87
setup {*
haftmann@28228
    88
let
haftmann@28228
    89
  fun mk_term_of_eq ty vs tyco (c, tys) =
haftmann@28228
    90
    let
haftmann@28228
    91
      val t = list_comb (Const (c, tys ---> ty),
haftmann@28228
    92
        map Free (Name.names Name.context "a" tys));
haftmann@28228
    93
    in (map_aterms (fn Free (v, ty) => Var ((v, 0), ty) | t => t) t, Eval.mk_term
haftmann@28228
    94
      (fn (v, ty) => Eval.mk_term_of ty (Var ((v, 0), ty)))
haftmann@28335
    95
      (Typerep.mk (fn (v, sort) => Typerep.typerep (TFree (v, sort)))) t)
haftmann@28228
    96
    end;
haftmann@28228
    97
  fun prove_term_of_eq ty eq thy =
haftmann@28228
    98
    let
haftmann@28228
    99
      val cty = Thm.ctyp_of thy ty;
haftmann@28228
   100
      val (arg, rhs) = pairself (Thm.cterm_of thy) eq;
haftmann@28228
   101
      val thm = @{thm term_of_anything}
haftmann@28228
   102
        |> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs]
haftmann@28228
   103
        |> Thm.varifyT;
haftmann@28228
   104
    in
haftmann@28228
   105
      thy
haftmann@28370
   106
      |> Code.add_eqn thm
haftmann@28228
   107
    end;
haftmann@28228
   108
  fun interpretator (tyco, (raw_vs, raw_cs)) thy =
haftmann@28228
   109
    let
haftmann@28228
   110
      val constrain_sort =
haftmann@28228
   111
        curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of};
haftmann@28228
   112
      val vs = (map o apsnd) constrain_sort raw_vs;
haftmann@28228
   113
      val cs = (map o apsnd o map o map_atyps)
haftmann@28228
   114
        (fn TFree (v, sort) => TFree (v, constrain_sort sort)) raw_cs;
haftmann@28228
   115
      val ty = Type (tyco, map TFree vs);
haftmann@28228
   116
      val eqs = map (mk_term_of_eq ty vs tyco) cs;
haftmann@28228
   117
      val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
haftmann@28228
   118
    in
haftmann@28228
   119
      thy
haftmann@28370
   120
      |> Code.del_eqns const
haftmann@28228
   121
      |> fold (prove_term_of_eq ty) eqs
haftmann@28228
   122
    end;
haftmann@28228
   123
in
haftmann@28228
   124
  Code.type_interpretation interpretator
haftmann@28228
   125
end
haftmann@28228
   126
*}
haftmann@28228
   127
haftmann@28228
   128
haftmann@28228
   129
subsubsection {* Code generator setup *}
haftmann@28228
   130
haftmann@28562
   131
lemmas [code del] = term.recs term.cases term.size
haftmann@28562
   132
lemma [code, code del]: "eq_class.eq (t1\<Colon>term) t2 \<longleftrightarrow> eq_class.eq t1 t2" ..
haftmann@28228
   133
haftmann@28562
   134
lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
haftmann@28562
   135
lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
haftmann@28562
   136
lemma [code, code del]: "(term_of \<Colon> message_string \<Rightarrow> term) = term_of" ..
haftmann@30427
   137
lemma [code, code del]:
haftmann@30427
   138
  "(Code_Eval.term_of \<Colon> 'a::{type, term_of} Predicate.pred \<Rightarrow> Code_Eval.term) = Code_Eval.term_of" ..
haftmann@30427
   139
lemma [code, code del]:
haftmann@30427
   140
  "(Code_Eval.term_of \<Colon> 'a::{type, term_of} Predicate.seq \<Rightarrow> Code_Eval.term) = Code_Eval.term_of" ..
haftmann@28228
   141
haftmann@28562
   142
lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]: "Code_Eval.term_of c =
haftmann@28243
   143
    (let (n, m) = nibble_pair_of_char c
haftmann@28335
   144
  in Code_Eval.App (Code_Eval.App (Code_Eval.Const (STR ''Pair'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
haftmann@28243
   145
    (Code_Eval.term_of n)) (Code_Eval.term_of m))"
haftmann@28243
   146
  by (subst term_of_anything) rule 
haftmann@28243
   147
haftmann@28228
   148
code_type "term"
haftmann@28228
   149
  (SML "Term.term")
haftmann@28228
   150
haftmann@28228
   151
code_const Const and App
haftmann@28228
   152
  (SML "Term.Const/ (_, _)" and "Term.$/ (_, _)")
haftmann@28228
   153
haftmann@28228
   154
code_const "term_of \<Colon> message_string \<Rightarrow> term"
haftmann@28228
   155
  (SML "Message'_String.mk")
haftmann@28228
   156
haftmann@28228
   157
haftmann@28228
   158
subsection {* Evaluation setup *}
haftmann@28228
   159
haftmann@28228
   160
ML {*
haftmann@28228
   161
signature EVAL =
haftmann@28228
   162
sig
haftmann@28228
   163
  val mk_term: ((string * typ) -> term) -> (typ -> term) -> term -> term
haftmann@28228
   164
  val eval_ref: (unit -> term) option ref
haftmann@28228
   165
  val eval_term: theory -> term -> term
haftmann@28228
   166
end;
haftmann@28228
   167
haftmann@28228
   168
structure Eval : EVAL =
haftmann@28228
   169
struct
haftmann@28228
   170
haftmann@28228
   171
open Eval;
haftmann@28228
   172
haftmann@28228
   173
val eval_ref = ref (NONE : (unit -> term) option);
haftmann@28228
   174
haftmann@28228
   175
fun eval_term thy t =
haftmann@28228
   176
  t 
haftmann@28228
   177
  |> Eval.mk_term_of (fastype_of t)
haftmann@28228
   178
  |> (fn t => Code_ML.eval_term ("Eval.eval_ref", eval_ref) thy t [])
haftmann@28228
   179
  |> Code.postprocess_term thy;
haftmann@28228
   180
haftmann@28228
   181
end;
haftmann@28228
   182
*}
haftmann@28228
   183
haftmann@28228
   184
setup {*
haftmann@28228
   185
  Value.add_evaluator ("code", Eval.eval_term o ProofContext.theory_of)
haftmann@28228
   186
*}
haftmann@28228
   187
haftmann@28243
   188
haftmann@28243
   189
subsubsection {* Syntax *}
haftmann@28243
   190
haftmann@28243
   191
print_translation {*
haftmann@28243
   192
let
haftmann@28243
   193
  val term = Const ("<TERM>", dummyT);
haftmann@28243
   194
  fun tr1' [_, _] = term;
haftmann@28243
   195
  fun tr2' [] = term;
haftmann@28243
   196
in
haftmann@28243
   197
  [(@{const_syntax Const}, tr1'),
haftmann@28243
   198
    (@{const_syntax App}, tr1'),
haftmann@28243
   199
    (@{const_syntax dummy_term}, tr2')]
haftmann@28228
   200
end
haftmann@28243
   201
*}
haftmann@28243
   202
haftmann@28243
   203
hide const dummy_term
haftmann@28243
   204
hide (open) const Const App
haftmann@28243
   205
hide (open) const term_of
haftmann@28243
   206
haftmann@28243
   207
end