src/HOL/Library/Eval.thy
author haftmann
Tue Dec 18 14:37:00 2007 +0100 (2007-12-18)
changeset 25691 8f8d83af100a
parent 25666 f46ed5b333fd
child 25763 474f8ba9dfa9
permissions -rw-r--r--
switched from PreList to ATP_Linkup
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@25691
     9
imports ATP_Linkup 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@25536
    21
fun mk ty =
haftmann@22525
    22
  Const (@{const_name typ_of}, Term.itselfT ty --> @{typ typ})
haftmann@22525
    23
    $ Logic.mk_type ty;
haftmann@22525
    24
haftmann@25536
    25
end
haftmann@22525
    26
*}
haftmann@22525
    27
haftmann@22525
    28
setup {*
haftmann@22525
    29
let
haftmann@25536
    30
  fun define_typ_of ty lthy =
haftmann@25536
    31
    let
haftmann@25536
    32
      val lhs = Const (@{const_name typ_of}, Term.itselfT ty --> @{typ typ})
haftmann@25536
    33
        $ Free ("T", Term.itselfT ty);
haftmann@25536
    34
      val rhs = Pure_term.mk_typ (fn v => TypOf.mk (TFree v)) ty;
haftmann@25603
    35
      val eq = Syntax.check_term lthy (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)))
haftmann@25536
    36
    in lthy |> Specification.definition (NONE, (("", []), eq)) end;
haftmann@25536
    37
  fun interpretator tyco thy =
haftmann@25536
    38
    let
haftmann@25536
    39
      val sorts = replicate (Sign.arity_number thy tyco) @{sort typ_of};
haftmann@25536
    40
      val ty = Type (tyco, map TFree (Name.names Name.context "'a" sorts));
haftmann@25536
    41
    in
haftmann@25536
    42
      thy
haftmann@25569
    43
      |> TheoryTarget.instantiation ([tyco], sorts, @{sort typ_of})
haftmann@25569
    44
      |> define_typ_of ty
haftmann@25569
    45
      |> snd
haftmann@25569
    46
      |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
haftmann@25569
    47
      |> LocalTheory.exit
haftmann@25569
    48
      |> ProofContext.theory_of
haftmann@25536
    49
    end;
haftmann@25536
    50
in TypedefPackage.interpretation interpretator end
haftmann@22525
    51
*}
haftmann@22525
    52
haftmann@25536
    53
instantiation "prop" :: typ_of
haftmann@25536
    54
begin
haftmann@25536
    55
haftmann@25666
    56
definition 
haftmann@25666
    57
  "typ_of (T\<Colon>prop itself) = Type (STR ''prop'') []"
haftmann@25536
    58
haftmann@25536
    59
instance ..
haftmann@25536
    60
haftmann@25536
    61
end
haftmann@25536
    62
haftmann@25536
    63
instantiation itself :: (typ_of) typ_of
haftmann@25536
    64
begin
haftmann@25536
    65
haftmann@25536
    66
definition
haftmann@25666
    67
  "typ_of (T\<Colon>'a itself itself) = Type (STR ''itself'') [typ_of TYPE('a\<Colon>typ_of)]"
haftmann@25536
    68
haftmann@25536
    69
instance ..
haftmann@25536
    70
haftmann@25536
    71
end
haftmann@25536
    72
haftmann@25536
    73
instantiation set :: (typ_of) typ_of
haftmann@25536
    74
begin
haftmann@25536
    75
 
haftmann@25536
    76
definition
haftmann@25666
    77
  "typ_of (T\<Colon>'a set itself) = Type (STR ''set'') [typ_of TYPE('a\<Colon>typ_of)]"
haftmann@25536
    78
haftmann@25536
    79
instance ..
haftmann@25536
    80
haftmann@25536
    81
end
haftmann@25536
    82
haftmann@22525
    83
haftmann@22527
    84
subsection {* @{text term_of} class *}
haftmann@22525
    85
haftmann@22525
    86
class term_of = typ_of +
haftmann@23062
    87
  constrains typ_of :: "'a\<Colon>{} itself \<Rightarrow> typ"
haftmann@22525
    88
  fixes term_of :: "'a \<Rightarrow> term"
haftmann@22525
    89
haftmann@22525
    90
ML {*
haftmann@22525
    91
structure TermOf =
haftmann@22525
    92
struct
haftmann@22525
    93
haftmann@22525
    94
local
haftmann@22525
    95
  fun term_term_of ty =
haftmann@22525
    96
    Const (@{const_name term_of}, ty --> @{typ term});
haftmann@22525
    97
in
haftmann@22525
    98
  val class_term_of = Sign.intern_class @{theory} "term_of";
haftmann@22525
    99
  fun mk_terms_of_defs vs (tyco, cs) =
haftmann@22525
   100
    let
haftmann@22525
   101
      val dty = Type (tyco, map TFree vs);
haftmann@22525
   102
      fun mk_eq c =
haftmann@22525
   103
        let
haftmann@22525
   104
          val lhs : term = term_term_of dty $ c;
haftmann@22525
   105
          val rhs : term = Pure_term.mk_term
haftmann@22525
   106
            (fn (v, ty) => term_term_of ty $ Free (v, ty))
haftmann@25536
   107
            (Pure_term.mk_typ (fn (v, sort) => TypOf.mk (TFree (v, sort)))) c
haftmann@22525
   108
        in
haftmann@25559
   109
          HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
haftmann@22525
   110
        end;
haftmann@22525
   111
    in map mk_eq cs end;
haftmann@22525
   112
  fun mk_term_of t =
haftmann@22525
   113
    term_term_of (Term.fastype_of t) $ t;
haftmann@22525
   114
end;
haftmann@22525
   115
haftmann@22525
   116
end;
haftmann@22525
   117
*}
haftmann@22525
   118
haftmann@22525
   119
setup {*
haftmann@22525
   120
let
haftmann@22525
   121
  fun thy_note ((name, atts), thms) =
haftmann@22525
   122
    PureThy.add_thmss [((name, thms), atts)] #-> (fn [thms] => pair (name, thms));
haftmann@22525
   123
  fun thy_def ((name, atts), t) =
haftmann@22525
   124
    PureThy.add_defs_i false [((name, t), atts)] #-> (fn [thm] => pair (name, thm));
haftmann@25536
   125
  fun prep_dtyp thy vs tyco =
haftmann@25536
   126
    let
haftmann@25536
   127
      val (_, cs) = DatatypePackage.the_datatype_spec thy tyco;
haftmann@25536
   128
      val prep_typ = map_atyps (fn TFree (v, sort) =>
haftmann@25536
   129
        TFree (v, (the o AList.lookup (op =) vs) v));
haftmann@25536
   130
      fun prep_c (c, tys) = list_comb (Const (c, tys ---> Type (tyco, map TFree vs)),
haftmann@25536
   131
        map Free (Name.names Name.context "a" tys));
haftmann@25536
   132
    in (tyco, map (prep_c o (apsnd o map) prep_typ) cs) end;
haftmann@25536
   133
  fun prep thy tycos =
haftmann@22525
   134
    let
haftmann@25536
   135
      val inter_sort = curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of};
haftmann@25536
   136
      val tyco = hd tycos;
haftmann@25536
   137
      val (vs_proto, _) = DatatypePackage.the_datatype_spec thy tyco;
haftmann@25536
   138
      val all_typs = maps (maps snd o snd o DatatypePackage.the_datatype_spec thy) tycos;
haftmann@25536
   139
      fun add_tycos (Type (tyco, tys)) = insert (op =) tyco #>
haftmann@25536
   140
            fold add_tycos tys
haftmann@25536
   141
        | add_tycos _ = I;
haftmann@25536
   142
      val dep_tycos = [] |> fold add_tycos all_typs |> subtract (op =) tycos;
haftmann@25536
   143
      val sorts = map (inter_sort o snd) vs_proto;
haftmann@25536
   144
      val vs = map fst vs_proto ~~ sorts;
haftmann@25536
   145
      val css = map (prep_dtyp thy vs) tycos;
haftmann@22525
   146
      val defs = map (TermOf.mk_terms_of_defs vs) css;
haftmann@25536
   147
    in if forall (fn tyco => can (Sign.arity_sorts thy tyco) @{sort term_of}) dep_tycos
haftmann@25536
   148
        andalso not (tycos = [@{type_name typ}])
haftmann@25559
   149
      then SOME (sorts, defs)
haftmann@25536
   150
      else NONE
haftmann@22525
   151
    end;
haftmann@25559
   152
  fun prep' ctxt proto_eqs =
haftmann@25559
   153
    let
haftmann@25603
   154
      val eqs as eq :: _ = map (Syntax.check_term ctxt) proto_eqs;
haftmann@25559
   155
      val (Free (v, ty), _) =
haftmann@25559
   156
        (strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
haftmann@25559
   157
    in ((v, SOME ty, NoSyn), map (pair ("", [])) eqs) end;
haftmann@25559
   158
  fun primrec primrecs ctxt =
haftmann@25559
   159
    let
haftmann@25559
   160
      val (fixes, eqnss) = split_list (map (prep' ctxt) primrecs);
haftmann@25559
   161
    in PrimrecPackage.add_primrec fixes (flat eqnss) ctxt end;
haftmann@25536
   162
  fun interpretator tycos thy = case prep thy tycos
haftmann@25536
   163
   of SOME (sorts, defs) =>
haftmann@25536
   164
      thy
haftmann@25569
   165
      |> TheoryTarget.instantiation (tycos, sorts, @{sort term_of})
haftmann@25569
   166
      |> primrec defs
haftmann@25569
   167
      |> snd
haftmann@25569
   168
      |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
haftmann@25569
   169
      |> LocalTheory.exit
haftmann@25569
   170
      |> ProofContext.theory_of
haftmann@25536
   171
    | NONE => thy;
haftmann@25536
   172
  in DatatypePackage.interpretation interpretator end
haftmann@22525
   173
*}
haftmann@22525
   174
haftmann@25666
   175
abbreviation (in pure_term_syntax) (input)
haftmann@23062
   176
  intT :: "typ"
haftmann@23062
   177
where
haftmann@25666
   178
  "intT \<equiv> Type (STR ''IntDef.int'') []"
haftmann@23062
   179
haftmann@25666
   180
abbreviation (in pure_term_syntax) (input)
haftmann@23133
   181
  bitT :: "typ"
haftmann@23133
   182
where
haftmann@25666
   183
  "bitT \<equiv> Type (STR ''Numeral.bit'') []"
haftmann@23133
   184
haftmann@25666
   185
function (in pure_term_syntax)
haftmann@23062
   186
  mk_int :: "int \<Rightarrow> term"
haftmann@23062
   187
where
haftmann@23062
   188
  "mk_int k = (if k = 0 then STR ''Numeral.Pls'' \<Colon>\<subseteq> intT
haftmann@23062
   189
    else if k = -1 then STR ''Numeral.Min'' \<Colon>\<subseteq> intT
haftmann@23062
   190
    else let (l, m) = divAlg (k, 2)
haftmann@23133
   191
  in STR ''Numeral.Bit'' \<Colon>\<subseteq> intT \<rightarrow> bitT \<rightarrow> intT \<bullet> mk_int l \<bullet>
haftmann@23133
   192
    (if m = 0 then STR ''Numeral.bit.B0'' \<Colon>\<subseteq> bitT else STR ''Numeral.bit.B1'' \<Colon>\<subseteq> bitT))"
haftmann@23062
   193
by pat_completeness auto
haftmann@25666
   194
termination (in pure_term_syntax)
haftmann@25666
   195
by (relation "measure (nat o abs)") (auto simp add: divAlg_mod_div)
haftmann@25666
   196
haftmann@25666
   197
declare pure_term_syntax.mk_int.simps [code func]
haftmann@25666
   198
haftmann@25666
   199
definition (in pure_term_syntax)
haftmann@25666
   200
  "term_of_int_aux k = STR ''Numeral.number_class.number_of'' \<Colon>\<subseteq> intT \<rightarrow> intT \<bullet> mk_int k"
haftmann@25666
   201
haftmann@25666
   202
declare pure_term_syntax.term_of_int_aux_def [code func]
haftmann@23062
   203
haftmann@25569
   204
instantiation int :: term_of
haftmann@25569
   205
begin
haftmann@25569
   206
haftmann@25569
   207
definition
haftmann@25666
   208
  "term_of = pure_term_syntax.term_of_int_aux"
haftmann@25569
   209
haftmann@25569
   210
instance ..
haftmann@25569
   211
haftmann@25569
   212
end
haftmann@23062
   213
haftmann@23062
   214
haftmann@24994
   215
text {* Adaption for @{typ message_string}s *}
haftmann@22525
   216
haftmann@25569
   217
lemmas [code func del] = term_of_message_string.simps
haftmann@22525
   218
haftmann@22525
   219
haftmann@22525
   220
subsection {* Evaluation infrastructure *}
haftmann@22525
   221
haftmann@22525
   222
ML {*
haftmann@22525
   223
signature EVAL =
haftmann@22525
   224
sig
haftmann@24587
   225
  val eval_ref: (unit -> term) option ref
haftmann@24835
   226
  val eval_term: theory -> term -> term
haftmann@24835
   227
  val evaluate: Proof.context -> term -> unit
haftmann@24835
   228
  val evaluate': string -> Proof.context -> term -> unit
haftmann@24835
   229
  val evaluate_cmd: string option -> Toplevel.state -> unit
haftmann@22525
   230
end;
haftmann@22525
   231
haftmann@24280
   232
structure Eval =
haftmann@22525
   233
struct
haftmann@22525
   234
haftmann@24587
   235
val eval_ref = ref (NONE : (unit -> term) option);
haftmann@22525
   236
haftmann@24835
   237
fun eval_invoke thy code ((_, ty), t) deps _ =
haftmann@24916
   238
  CodeTarget.eval_invoke thy ("Eval.eval_ref", eval_ref) code (t, ty) [];
haftmann@24280
   239
haftmann@24835
   240
fun eval_term thy =
haftmann@24835
   241
  TermOf.mk_term_of
haftmann@24835
   242
  #> CodePackage.eval_term thy (eval_invoke thy)
haftmann@24835
   243
  #> Code.postprocess_term thy;
haftmann@24280
   244
haftmann@24835
   245
val evaluators = [
haftmann@24835
   246
  ("code", eval_term),
haftmann@24835
   247
  ("SML", Codegen.eval_term),
haftmann@24835
   248
  ("normal_form", Nbe.norm_term)
haftmann@24835
   249
];
haftmann@22525
   250
haftmann@24835
   251
fun gen_evaluate evaluators ctxt t =
haftmann@24280
   252
  let
haftmann@24280
   253
    val thy = ProofContext.theory_of ctxt;
haftmann@24835
   254
    val (evls, evl) = split_last evaluators;
haftmann@24835
   255
    val t' = case get_first (fn f => try (f thy) t) evls
haftmann@24835
   256
     of SOME t' => t'
haftmann@24835
   257
      | NONE => evl thy t;
haftmann@24835
   258
    val ty' = Term.type_of t';
wenzelm@24920
   259
    val p = Pretty.block [Pretty.quote (Syntax.pretty_term ctxt t'),
haftmann@24835
   260
      Pretty.fbrk, Pretty.str "::", Pretty.brk 1,
wenzelm@24920
   261
      Pretty.quote (Syntax.pretty_typ ctxt ty')];
haftmann@24280
   262
  in Pretty.writeln p end;
haftmann@24280
   263
haftmann@24835
   264
val evaluate = gen_evaluate (map snd evaluators);
haftmann@24835
   265
haftmann@24835
   266
fun evaluate' name = gen_evaluate
haftmann@24835
   267
  [(the o AList.lookup (op =) evaluators) name];
haftmann@24835
   268
haftmann@24835
   269
fun evaluate_cmd some_name raw_t state =
haftmann@22525
   270
  let
haftmann@22804
   271
    val ctxt = Toplevel.context_of state;
wenzelm@24508
   272
    val t = Syntax.read_term ctxt raw_t;
haftmann@24835
   273
  in case some_name
haftmann@24835
   274
   of NONE => evaluate ctxt t
haftmann@24835
   275
    | SOME name => evaluate' name ctxt t
haftmann@24835
   276
  end;
haftmann@22525
   277
haftmann@22525
   278
end;
haftmann@22525
   279
*}
haftmann@22525
   280
haftmann@22804
   281
ML {*
haftmann@22804
   282
  OuterSyntax.improper_command "value" "read, evaluate and print term" OuterKeyword.diag
haftmann@24835
   283
    (Scan.option (OuterParse.$$$ "(" |-- OuterParse.name --| OuterParse.$$$ ")")
haftmann@24835
   284
    -- OuterParse.term
haftmann@24835
   285
      >> (fn (some_name, t) => Toplevel.no_timing o Toplevel.keep
haftmann@24835
   286
           (Eval.evaluate_cmd some_name t)));
haftmann@22804
   287
*}
haftmann@22804
   288
wenzelm@22665
   289
end