src/HOL/Library/Eval.thy
author haftmann
Tue Sep 18 07:46:00 2007 +0200 (2007-09-18)
changeset 24626 85eceef2edc7
parent 24621 97d403d9ab54
child 24659 6b7ac2a43df8
permissions -rw-r--r--
introduced generic concepts for theory interpretators
haftmann@22525
     1
(*  Title:      HOL/Library/Eval.thy
haftmann@22525
     2
    ID:         $Id$
haftmann@22525
     3
    Author:     Florian Haftmann, TU Muenchen
haftmann@22525
     4
*)
haftmann@22525
     5
haftmann@22525
     6
header {* A simple term evaluation mechanism *}
haftmann@22525
     7
haftmann@22525
     8
theory Eval
haftmann@24280
     9
imports Main Pure_term
haftmann@22525
    10
begin
haftmann@22525
    11
haftmann@22527
    12
subsection {* @{text typ_of} class *}
haftmann@22525
    13
haftmann@23062
    14
class typ_of =
haftmann@23062
    15
  fixes typ_of :: "'a\<Colon>{} itself \<Rightarrow> typ"
haftmann@22525
    16
haftmann@22525
    17
ML {*
haftmann@22525
    18
structure TypOf =
haftmann@22525
    19
struct
haftmann@22525
    20
haftmann@22525
    21
val class_typ_of = Sign.intern_class @{theory} "typ_of";
haftmann@22525
    22
haftmann@22525
    23
fun term_typ_of_type ty =
haftmann@22525
    24
  Const (@{const_name typ_of}, Term.itselfT ty --> @{typ typ})
haftmann@22525
    25
    $ Logic.mk_type ty;
haftmann@22525
    26
haftmann@22525
    27
fun mk_typ_of_def ty =
haftmann@22525
    28
  let
haftmann@22525
    29
    val lhs = Const (@{const_name typ_of}, Term.itselfT ty --> @{typ typ})
haftmann@22525
    30
      $ Free ("x", Term.itselfT ty)
haftmann@22525
    31
    val rhs = Pure_term.mk_typ (fn v => term_typ_of_type (TFree v)) ty
haftmann@22525
    32
  in Logic.mk_equals (lhs, rhs) end;
haftmann@22525
    33
haftmann@22525
    34
end;
haftmann@22525
    35
*}
haftmann@22525
    36
haftmann@24587
    37
instance "prop" :: typ_of
haftmann@24587
    38
  "typ_of T \<equiv> STR ''prop'' {\<struct>} []" ..
haftmann@24587
    39
haftmann@23062
    40
instance itself :: (typ_of) typ_of
haftmann@23062
    41
  "typ_of T \<equiv> STR ''itself'' {\<struct>} [typ_of TYPE('a\<Colon>typ_of)]" ..
haftmann@23062
    42
haftmann@24587
    43
instance set :: (typ_of) typ_of
haftmann@24587
    44
  "typ_of T \<equiv> STR ''set'' {\<struct>} [typ_of TYPE('a\<Colon>typ_of)]" ..
haftmann@23062
    45
haftmann@23020
    46
instance int :: typ_of
haftmann@23020
    47
  "typ_of T \<equiv> STR ''IntDef.int'' {\<struct>} []" ..
haftmann@23020
    48
haftmann@22525
    49
setup {*
haftmann@22525
    50
let
haftmann@22525
    51
  fun mk arities _ thy =
haftmann@22525
    52
    (maps (fn (tyco, asorts, _) => [(("", []), TypOf.mk_typ_of_def
haftmann@22525
    53
      (Type (tyco,
haftmann@22525
    54
        map TFree (Name.names Name.context "'a" asorts))))]) arities, thy);
haftmann@22525
    55
  fun hook specs =
haftmann@24219
    56
    DatatypeCodegen.prove_codetypes_arities (Class.intro_classes_tac [])
haftmann@22525
    57
      (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
haftmann@24621
    58
      [TypOf.class_typ_of] mk ((K o K) (fold Code.add_default_func))
haftmann@24626
    59
in DatatypeCodegen.add_codetypes_hook hook end
haftmann@22525
    60
*}
haftmann@22525
    61
haftmann@22525
    62
haftmann@22527
    63
subsection {* @{text term_of} class *}
haftmann@22525
    64
haftmann@22525
    65
class term_of = typ_of +
haftmann@23062
    66
  constrains typ_of :: "'a\<Colon>{} itself \<Rightarrow> typ"
haftmann@22525
    67
  fixes term_of :: "'a \<Rightarrow> term"
haftmann@22525
    68
haftmann@22525
    69
ML {*
haftmann@22525
    70
structure TermOf =
haftmann@22525
    71
struct
haftmann@22525
    72
haftmann@22525
    73
local
haftmann@22525
    74
  fun term_term_of ty =
haftmann@22525
    75
    Const (@{const_name term_of}, ty --> @{typ term});
haftmann@22525
    76
in
haftmann@22525
    77
  val class_term_of = Sign.intern_class @{theory} "term_of";
haftmann@22525
    78
  fun mk_terms_of_defs vs (tyco, cs) =
haftmann@22525
    79
    let
haftmann@22525
    80
      val dty = Type (tyco, map TFree vs);
haftmann@22525
    81
      fun mk_eq c =
haftmann@22525
    82
        let
haftmann@22525
    83
          val lhs : term = term_term_of dty $ c;
haftmann@22525
    84
          val rhs : term = Pure_term.mk_term
haftmann@22525
    85
            (fn (v, ty) => term_term_of ty $ Free (v, ty))
haftmann@22525
    86
            (Pure_term.mk_typ (fn (v, sort) => TypOf.term_typ_of_type (TFree (v, sort)))) c
haftmann@22525
    87
        in
haftmann@22525
    88
          HOLogic.mk_eq (lhs, rhs)
haftmann@22525
    89
        end;
haftmann@22525
    90
    in map mk_eq cs end;
haftmann@22525
    91
  fun mk_term_of t =
haftmann@22525
    92
    term_term_of (Term.fastype_of t) $ t;
haftmann@22525
    93
end;
haftmann@22525
    94
haftmann@22525
    95
end;
haftmann@22525
    96
*}
haftmann@22525
    97
haftmann@22525
    98
setup {*
haftmann@22525
    99
let
haftmann@22525
   100
  fun thy_note ((name, atts), thms) =
haftmann@22525
   101
    PureThy.add_thmss [((name, thms), atts)] #-> (fn [thms] => pair (name, thms));
haftmann@22525
   102
  fun thy_def ((name, atts), t) =
haftmann@22525
   103
    PureThy.add_defs_i false [((name, t), atts)] #-> (fn [thm] => pair (name, thm));
haftmann@24423
   104
  fun mk arities css _ thy =
haftmann@22525
   105
    let
haftmann@22525
   106
      val (_, asorts, _) :: _ = arities;
haftmann@22525
   107
      val vs = Name.names Name.context "'a" asorts;
haftmann@22525
   108
      val defs = map (TermOf.mk_terms_of_defs vs) css;
haftmann@22525
   109
      val defs' = (map (pair ("", []) o ObjectLogic.ensure_propT thy) o flat) defs;
haftmann@22525
   110
    in
haftmann@22525
   111
      thy
haftmann@22525
   112
      |> PrimrecPackage.gen_primrec thy_note thy_def "" defs'
haftmann@22525
   113
      |> snd
haftmann@22525
   114
    end;
haftmann@22525
   115
  fun hook specs =
haftmann@22525
   116
    if (fst o hd) specs = (fst o dest_Type) @{typ typ} then I
haftmann@22525
   117
    else
haftmann@24219
   118
      DatatypeCodegen.prove_codetypes_arities (Class.intro_classes_tac [])
haftmann@22525
   119
      (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
haftmann@22525
   120
      [TermOf.class_term_of] ((K o K o pair) []) mk
haftmann@24626
   121
in DatatypeCodegen.add_codetypes_hook hook end
haftmann@22525
   122
*}
haftmann@22525
   123
haftmann@23062
   124
abbreviation
haftmann@23062
   125
  intT :: "typ"
haftmann@23062
   126
where
haftmann@23062
   127
  "intT \<equiv> STR ''IntDef.int'' {\<struct>} []"
haftmann@23062
   128
haftmann@23133
   129
abbreviation
haftmann@23133
   130
  bitT :: "typ"
haftmann@23133
   131
where
haftmann@23133
   132
  "bitT \<equiv> STR ''Numeral.bit'' {\<struct>} []"
haftmann@23133
   133
haftmann@23062
   134
function
haftmann@23062
   135
  mk_int :: "int \<Rightarrow> term"
haftmann@23062
   136
where
haftmann@23062
   137
  "mk_int k = (if k = 0 then STR ''Numeral.Pls'' \<Colon>\<subseteq> intT
haftmann@23062
   138
    else if k = -1 then STR ''Numeral.Min'' \<Colon>\<subseteq> intT
haftmann@23062
   139
    else let (l, m) = divAlg (k, 2)
haftmann@23133
   140
  in STR ''Numeral.Bit'' \<Colon>\<subseteq> intT \<rightarrow> bitT \<rightarrow> intT \<bullet> mk_int l \<bullet>
haftmann@23133
   141
    (if m = 0 then STR ''Numeral.bit.B0'' \<Colon>\<subseteq> bitT else STR ''Numeral.bit.B1'' \<Colon>\<subseteq> bitT))"
haftmann@23062
   142
by pat_completeness auto
haftmann@23062
   143
termination by (relation "measure (nat o abs)") (auto simp add: divAlg_mod_div)
haftmann@23062
   144
haftmann@23062
   145
instance int :: term_of
haftmann@23133
   146
  "term_of k \<equiv> STR ''Numeral.number_class.number_of'' \<Colon>\<subseteq> intT \<rightarrow> intT \<bullet> mk_int k" ..
haftmann@23062
   147
haftmann@23062
   148
haftmann@22804
   149
text {* Adaption for @{typ ml_string}s *}
haftmann@22525
   150
haftmann@22845
   151
lemmas [code func, code func del] = term_of_ml_string_def
haftmann@22525
   152
haftmann@22525
   153
haftmann@22525
   154
subsection {* Evaluation infrastructure *}
haftmann@22525
   155
haftmann@22525
   156
ML {*
haftmann@22525
   157
signature EVAL =
haftmann@22525
   158
sig
haftmann@24587
   159
  val eval_ref: (unit -> term) option ref
haftmann@24280
   160
  val eval_conv: cterm -> thm
haftmann@24280
   161
  val eval_print: (cterm -> thm) -> Proof.context -> term -> unit
haftmann@24280
   162
  val eval_print_cmd: (cterm -> thm) -> string -> Toplevel.state -> unit
haftmann@22525
   163
end;
haftmann@22525
   164
haftmann@24280
   165
structure Eval =
haftmann@22525
   166
struct
haftmann@22525
   167
haftmann@24587
   168
val eval_ref = ref (NONE : (unit -> term) option);
haftmann@22525
   169
haftmann@24280
   170
end;
haftmann@24280
   171
*}
haftmann@24280
   172
haftmann@24381
   173
oracle eval_oracle ("term * CodeThingol.code * (CodeThingol.typscheme * CodeThingol.iterm) * cterm") =
haftmann@24381
   174
{* fn thy => fn (t0, code, ((vs, ty), t), ct) => 
haftmann@24280
   175
let
haftmann@24280
   176
  val _ = (Term.map_types o Term.map_atyps) (fn _ =>
haftmann@24280
   177
    error ("Term " ^ Sign.string_of_term thy t0 ^ " contains polymorphic type"))
haftmann@24280
   178
    t0;
haftmann@24621
   179
in
haftmann@24621
   180
  Logic.mk_equals (t0,
haftmann@24621
   181
    CodePackage.eval_invoke thy ("Eval.eval_ref", Eval.eval_ref) code (t, ty) [])
haftmann@24621
   182
end;
haftmann@24280
   183
*}
haftmann@24280
   184
haftmann@24280
   185
ML {*
haftmann@24280
   186
structure Eval : EVAL =
haftmann@24280
   187
struct
haftmann@24280
   188
haftmann@24280
   189
open Eval;
haftmann@24280
   190
haftmann@24381
   191
fun eval_invoke thy t0 code vs_ty_t _ ct = eval_oracle thy (t0, code, vs_ty_t, ct);
haftmann@22525
   192
haftmann@24280
   193
fun eval_conv ct =
haftmann@24280
   194
  let
haftmann@24280
   195
    val thy = Thm.theory_of_cterm ct;
haftmann@24280
   196
    val ct' = (Thm.cterm_of thy o TermOf.mk_term_of o Thm.term_of) ct;
haftmann@24280
   197
  in
haftmann@24280
   198
    CodePackage.eval_term thy
haftmann@24280
   199
      (eval_invoke thy (Thm.term_of ct)) ct'
haftmann@24280
   200
  end;
haftmann@24280
   201
haftmann@24280
   202
fun eval_print conv ctxt t =
haftmann@24280
   203
  let
haftmann@24280
   204
    val thy = ProofContext.theory_of ctxt;
haftmann@24280
   205
    val ct = Thm.cterm_of thy t;
haftmann@24280
   206
    val (_, t') = (Logic.dest_equals o Thm.prop_of o conv) ct;
haftmann@24280
   207
    val ty = Term.type_of t';
haftmann@24280
   208
    val p = 
haftmann@24280
   209
      Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t'), Pretty.fbrk,
haftmann@24280
   210
        Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt ty)];
haftmann@24280
   211
  in Pretty.writeln p end;
haftmann@24280
   212
haftmann@24280
   213
fun eval_print_cmd conv raw_t state =
haftmann@22525
   214
  let
haftmann@22804
   215
    val ctxt = Toplevel.context_of state;
wenzelm@24508
   216
    val t = Syntax.read_term ctxt raw_t;
haftmann@22804
   217
    val thy = ProofContext.theory_of ctxt;
haftmann@24280
   218
    val ct = Thm.cterm_of thy t;
haftmann@24280
   219
    val (_, t') = (Logic.dest_equals o Thm.prop_of o conv) ct;
haftmann@24280
   220
    val ty = Term.type_of t';
haftmann@24280
   221
    val p = 
haftmann@24280
   222
      Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t'), Pretty.fbrk,
haftmann@24280
   223
        Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt ty)];
haftmann@24280
   224
  in Pretty.writeln p end;
haftmann@22525
   225
haftmann@22525
   226
end;
haftmann@22525
   227
*}
haftmann@22525
   228
haftmann@22804
   229
ML {*
haftmann@22804
   230
val valueP =
haftmann@22804
   231
  OuterSyntax.improper_command "value" "read, evaluate and print term" OuterKeyword.diag
haftmann@24587
   232
    (OuterParse.term
haftmann@24587
   233
      >> (fn t => Toplevel.no_timing o Toplevel.keep
haftmann@24587
   234
           (Eval.eval_print_cmd (fn ct => case try Eval.eval_conv ct
haftmann@24587
   235
     of SOME thm => thm
haftmann@24587
   236
      | NONE => Codegen.evaluation_conv ct) t)));
haftmann@22804
   237
haftmann@22804
   238
val _ = OuterSyntax.add_parsers [valueP];
haftmann@22804
   239
*}
haftmann@22804
   240
wenzelm@22665
   241
end