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