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