src/HOL/Code_Evaluation.thy
author wenzelm
Mon, 05 Sep 2016 23:11:00 +0200
changeset 63806 c54a53ef1873
parent 63161 2660ba498798
child 66013 03002d10bf1d
permissions -rw-r--r--
clarified modules;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32657
5f13912245ff Code_Eval(uation)
haftmann
parents: 32371
diff changeset
     1
(*  Title:      HOL/Code_Evaluation.thy
28228
7ebe8dc06cbb evaluation using code generator
haftmann
parents:
diff changeset
     2
    Author:     Florian Haftmann, TU Muenchen
7ebe8dc06cbb evaluation using code generator
haftmann
parents:
diff changeset
     3
*)
7ebe8dc06cbb evaluation using code generator
haftmann
parents:
diff changeset
     4
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59484
diff changeset
     5
section \<open>Term evaluation using the generic code generator\<close>
28228
7ebe8dc06cbb evaluation using code generator
haftmann
parents:
diff changeset
     6
32657
5f13912245ff Code_Eval(uation)
haftmann
parents: 32371
diff changeset
     7
theory Code_Evaluation
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 51112
diff changeset
     8
imports Typerep Limited_Sequence
56925
601edd9a6859 degeneralized value command into HOL
haftmann
parents: 56241
diff changeset
     9
keywords "value" :: diag
28228
7ebe8dc06cbb evaluation using code generator
haftmann
parents:
diff changeset
    10
begin
7ebe8dc06cbb evaluation using code generator
haftmann
parents:
diff changeset
    11
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59484
diff changeset
    12
subsection \<open>Term representation\<close>
28228
7ebe8dc06cbb evaluation using code generator
haftmann
parents:
diff changeset
    13
61799
4cf66f21b764 isabelle update_cartouches -c -t;
wenzelm
parents: 61076
diff changeset
    14
subsubsection \<open>Terms and class \<open>term_of\<close>\<close>
28228
7ebe8dc06cbb evaluation using code generator
haftmann
parents:
diff changeset
    15
58350
919149921e46 added 'extraction' plugins -- this might help 'HOL-Proofs'
blanchet
parents: 58334
diff changeset
    16
datatype (plugins only: code extraction) "term" = dummy_term
28228
7ebe8dc06cbb evaluation using code generator
haftmann
parents:
diff changeset
    17
31205
98370b26c2ce String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents: 31203
diff changeset
    18
definition Const :: "String.literal \<Rightarrow> typerep \<Rightarrow> term" where
28228
7ebe8dc06cbb evaluation using code generator
haftmann
parents:
diff changeset
    19
  "Const _ _ = dummy_term"
7ebe8dc06cbb evaluation using code generator
haftmann
parents:
diff changeset
    20
28661
a287d0e8aa9d slightly tuned
haftmann
parents: 28562
diff changeset
    21
definition App :: "term \<Rightarrow> term \<Rightarrow> term" where
28228
7ebe8dc06cbb evaluation using code generator
haftmann
parents:
diff changeset
    22
  "App _ _ = dummy_term"
7ebe8dc06cbb evaluation using code generator
haftmann
parents:
diff changeset
    23
40638
6b137c96df07 adding dummy definition for Code_Evaluation.Abs and hiding constants App less strict
bulwahn
parents: 39567
diff changeset
    24
definition Abs :: "String.literal \<Rightarrow> typerep \<Rightarrow> term \<Rightarrow> term" where
6b137c96df07 adding dummy definition for Code_Evaluation.Abs and hiding constants App less strict
bulwahn
parents: 39567
diff changeset
    25
  "Abs _ _ _ = dummy_term"
6b137c96df07 adding dummy definition for Code_Evaluation.Abs and hiding constants App less strict
bulwahn
parents: 39567
diff changeset
    26
42979
5b9e16259341 extending terms of Code_Evaluation by Free to allow partial terms
bulwahn
parents: 40884
diff changeset
    27
definition Free :: "String.literal \<Rightarrow> typerep \<Rightarrow> term" where
5b9e16259341 extending terms of Code_Evaluation by Free to allow partial terms
bulwahn
parents: 40884
diff changeset
    28
  "Free _ _ = dummy_term"
5b9e16259341 extending terms of Code_Evaluation by Free to allow partial terms
bulwahn
parents: 40884
diff changeset
    29
5b9e16259341 extending terms of Code_Evaluation by Free to allow partial terms
bulwahn
parents: 40884
diff changeset
    30
code_datatype Const App Abs Free
28228
7ebe8dc06cbb evaluation using code generator
haftmann
parents:
diff changeset
    31
28335
25326092cf9a renamed rtype to typerep
haftmann
parents: 28313
diff changeset
    32
class term_of = typerep +
31031
cbec39ebf8f2 class typerep inherits from type
haftmann
parents: 30970
diff changeset
    33
  fixes term_of :: "'a \<Rightarrow> term"
28228
7ebe8dc06cbb evaluation using code generator
haftmann
parents:
diff changeset
    34
7ebe8dc06cbb evaluation using code generator
haftmann
parents:
diff changeset
    35
lemma term_of_anything: "term_of x \<equiv> t"
7ebe8dc06cbb evaluation using code generator
haftmann
parents:
diff changeset
    36
  by (rule eq_reflection) (cases "term_of x", cases t, simp)
7ebe8dc06cbb evaluation using code generator
haftmann
parents:
diff changeset
    37
31191
7733125bac3c tuned term input syntax
haftmann
parents: 31178
diff changeset
    38
definition valapp :: "('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)
31178
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
    39
  \<Rightarrow> 'a \<times> (unit \<Rightarrow> term) \<Rightarrow> 'b \<times> (unit \<Rightarrow> term)" where
31191
7733125bac3c tuned term input syntax
haftmann
parents: 31178
diff changeset
    40
  "valapp f x = (fst f (fst x), \<lambda>u. App (snd f ()) (snd x ()))"
31178
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
    41
32069
6d28bbd33e2c prefer code_inline over code_unfold; use code_unfold_post where appropriate
haftmann
parents: 31998
diff changeset
    42
lemma valapp_code [code, code_unfold]:
31191
7733125bac3c tuned term input syntax
haftmann
parents: 31178
diff changeset
    43
  "valapp (f, tf) (x, tx) = (f x, \<lambda>u. App (tf ()) (tx ()))"
7733125bac3c tuned term input syntax
haftmann
parents: 31178
diff changeset
    44
  by (simp only: valapp_def fst_conv snd_conv)
31178
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
    45
28228
7ebe8dc06cbb evaluation using code generator
haftmann
parents:
diff changeset
    46
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59484
diff changeset
    47
subsubsection \<open>Syntax\<close>
31178
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
    48
31191
7733125bac3c tuned term input syntax
haftmann
parents: 31178
diff changeset
    49
definition termify :: "'a \<Rightarrow> term" where
7733125bac3c tuned term input syntax
haftmann
parents: 31178
diff changeset
    50
  [code del]: "termify x = dummy_term"
7733125bac3c tuned term input syntax
haftmann
parents: 31178
diff changeset
    51
7733125bac3c tuned term input syntax
haftmann
parents: 31178
diff changeset
    52
abbreviation valtermify :: "'a \<Rightarrow> 'a \<times> (unit \<Rightarrow> term)" where
7733125bac3c tuned term input syntax
haftmann
parents: 31178
diff changeset
    53
  "valtermify x \<equiv> (x, \<lambda>u. termify x)"
31178
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
    54
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
    55
locale term_syntax
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
    56
begin
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
    57
31191
7733125bac3c tuned term input syntax
haftmann
parents: 31178
diff changeset
    58
notation App (infixl "<\<cdot>>" 70)
7733125bac3c tuned term input syntax
haftmann
parents: 31178
diff changeset
    59
  and valapp (infixl "{\<cdot>}" 70)
31178
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
    60
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
    61
end
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
    62
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
    63
interpretation term_syntax .
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
    64
31191
7733125bac3c tuned term input syntax
haftmann
parents: 31178
diff changeset
    65
no_notation App (infixl "<\<cdot>>" 70)
7733125bac3c tuned term input syntax
haftmann
parents: 31178
diff changeset
    66
  and valapp (infixl "{\<cdot>}" 70)
7733125bac3c tuned term input syntax
haftmann
parents: 31178
diff changeset
    67
7733125bac3c tuned term input syntax
haftmann
parents: 31178
diff changeset
    68
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59484
diff changeset
    69
subsection \<open>Tools setup and evaluation\<close>
39564
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    70
63161
2660ba498798 delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents: 62958
diff changeset
    71
context
2660ba498798 delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents: 62958
diff changeset
    72
begin
2660ba498798 delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents: 62958
diff changeset
    73
2660ba498798 delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents: 62958
diff changeset
    74
qualified definition TERM_OF :: "'a::term_of itself"
2660ba498798 delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents: 62958
diff changeset
    75
where
2660ba498798 delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents: 62958
diff changeset
    76
  "TERM_OF = snd (Code_Evaluation.term_of :: 'a \<Rightarrow> _, TYPE('a))"
2660ba498798 delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents: 62958
diff changeset
    77
2660ba498798 delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents: 62958
diff changeset
    78
qualified definition TERM_OF_EQUAL :: "'a::term_of itself"
2660ba498798 delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents: 62958
diff changeset
    79
where
2660ba498798 delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents: 62958
diff changeset
    80
  "TERM_OF_EQUAL = snd (\<lambda>(a::'a). (Code_Evaluation.term_of a, HOL.eq a), TYPE('a))"
2660ba498798 delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents: 62958
diff changeset
    81
2660ba498798 delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents: 62958
diff changeset
    82
end
2660ba498798 delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents: 62958
diff changeset
    83
39567
5ee997fbe5cc dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents: 39564
diff changeset
    84
lemma eq_eq_TrueD:
62958
b41c1cb5e251 Type_Infer.object_logic controls improvement of type inference result;
wenzelm
parents: 62597
diff changeset
    85
  fixes x y :: "'a::{}"
39567
5ee997fbe5cc dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents: 39564
diff changeset
    86
  assumes "(x \<equiv> y) \<equiv> Trueprop True"
5ee997fbe5cc dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents: 39564
diff changeset
    87
  shows "x \<equiv> y"
5ee997fbe5cc dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents: 39564
diff changeset
    88
  using assms by simp
5ee997fbe5cc dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents: 39564
diff changeset
    89
56928
1e50fddbe1f5 dropped term_of obfuscation -- not really required;
haftmann
parents: 56927
diff changeset
    90
code_printing
1e50fddbe1f5 dropped term_of obfuscation -- not really required;
haftmann
parents: 56927
diff changeset
    91
  type_constructor "term" \<rightharpoonup> (Eval) "Term.term"
1e50fddbe1f5 dropped term_of obfuscation -- not really required;
haftmann
parents: 56927
diff changeset
    92
| constant Const \<rightharpoonup> (Eval) "Term.Const/ ((_), (_))"
1e50fddbe1f5 dropped term_of obfuscation -- not really required;
haftmann
parents: 56927
diff changeset
    93
| constant App \<rightharpoonup> (Eval) "Term.$/ ((_), (_))"
1e50fddbe1f5 dropped term_of obfuscation -- not really required;
haftmann
parents: 56927
diff changeset
    94
| constant Abs \<rightharpoonup> (Eval) "Term.Abs/ ((_), (_), (_))"
1e50fddbe1f5 dropped term_of obfuscation -- not really required;
haftmann
parents: 56927
diff changeset
    95
| constant Free \<rightharpoonup> (Eval) "Term.Free/ ((_), (_))"
1e50fddbe1f5 dropped term_of obfuscation -- not really required;
haftmann
parents: 56927
diff changeset
    96
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47108
diff changeset
    97
ML_file "Tools/code_evaluation.ML"
39564
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    98
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    99
code_reserved Eval Code_Evaluation
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   100
63806
c54a53ef1873 clarified modules;
wenzelm
parents: 63161
diff changeset
   101
ML_file "~~/src/HOL/Tools/value_command.ML"
56928
1e50fddbe1f5 dropped term_of obfuscation -- not really required;
haftmann
parents: 56927
diff changeset
   102
39564
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   103
61799
4cf66f21b764 isabelle update_cartouches -c -t;
wenzelm
parents: 61076
diff changeset
   104
subsection \<open>\<open>term_of\<close> instances\<close>
39564
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   105
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   106
instantiation "fun" :: (typerep, typerep) term_of
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   107
begin
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   108
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   109
definition
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60758
diff changeset
   110
  "term_of (f :: 'a \<Rightarrow> 'b) =
56241
029246729dc0 more qualified names;
wenzelm
parents: 55642
diff changeset
   111
    Const (STR ''Pure.dummy_pattern'')
029246729dc0 more qualified names;
wenzelm
parents: 55642
diff changeset
   112
      (Typerep.Typerep (STR ''fun'') [Typerep.typerep TYPE('a), Typerep.typerep TYPE('b)])"
39564
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   113
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   114
instance ..
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   115
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   116
end
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   117
58334
7553a1bcecb7 disable datatype 'plugins' for internal types
blanchet
parents: 58310
diff changeset
   118
declare [[code drop: rec_term case_term "HOL.equal :: term \<Rightarrow> _"
56926
aaea99edc040 modernized setups
haftmann
parents: 56925
diff changeset
   119
  "term_of :: typerep \<Rightarrow> _" "term_of :: term \<Rightarrow> _" "term_of :: String.literal \<Rightarrow> _"
aaea99edc040 modernized setups
haftmann
parents: 56925
diff changeset
   120
  "term_of :: _ Predicate.pred \<Rightarrow> term" "term_of :: _ Predicate.seq \<Rightarrow> term"]]
39564
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   121
62597
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61799
diff changeset
   122
definition case_char :: "'a \<Rightarrow> (num \<Rightarrow> 'a) \<Rightarrow> char \<Rightarrow> 'a"
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61799
diff changeset
   123
  where "case_char f g c = (if c = 0 then f else g (num_of_nat (nat_of_char c)))"
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61799
diff changeset
   124
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61799
diff changeset
   125
lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_num_def, code]:
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61799
diff changeset
   126
  "term_of =
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61799
diff changeset
   127
    case_char (Const (STR ''Groups.zero_class.zero'') (TYPEREP(char)))
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61799
diff changeset
   128
    (\<lambda>k. App (Const (STR ''String.Char'') (TYPEREP(num \<Rightarrow> char))) (term_of k))"
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61799
diff changeset
   129
  by (rule ext) (rule term_of_anything [THEN meta_eq_to_obj_eq])
39564
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   130
59484
a130ae7a9398 slightly more standard code setup for String.literal, with explicit special case in predicate compiler
haftmann
parents: 58889
diff changeset
   131
lemma term_of_string [code]:
a130ae7a9398 slightly more standard code setup for String.literal, with explicit special case in predicate compiler
haftmann
parents: 58889
diff changeset
   132
   "term_of s = App (Const (STR ''STR'')
a130ae7a9398 slightly more standard code setup for String.literal, with explicit special case in predicate compiler
haftmann
parents: 58889
diff changeset
   133
     (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''list'') [Typerep.Typerep (STR ''char'') []],
a130ae7a9398 slightly more standard code setup for String.literal, with explicit special case in predicate compiler
haftmann
parents: 58889
diff changeset
   134
       Typerep.Typerep (STR ''String.literal'') []])) (term_of (String.explode s))"
a130ae7a9398 slightly more standard code setup for String.literal, with explicit special case in predicate compiler
haftmann
parents: 58889
diff changeset
   135
  by (subst term_of_anything) rule 
a130ae7a9398 slightly more standard code setup for String.literal, with explicit special case in predicate compiler
haftmann
parents: 58889
diff changeset
   136
  
52435
6646bb548c6b migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents: 52286
diff changeset
   137
code_printing
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60758
diff changeset
   138
  constant "term_of :: integer \<Rightarrow> term" \<rightharpoonup> (Eval) "HOLogic.mk'_number/ HOLogic.code'_integerT"
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60758
diff changeset
   139
| constant "term_of :: String.literal \<Rightarrow> term" \<rightharpoonup> (Eval) "HOLogic.mk'_literal"
39564
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   140
58036
f23045003476 add code equation for term_of on integer
Andreas Lochbihler
parents: 56928
diff changeset
   141
declare [[code drop: "term_of :: integer \<Rightarrow> _"]]
f23045003476 add code equation for term_of on integer
Andreas Lochbihler
parents: 56928
diff changeset
   142
f23045003476 add code equation for term_of on integer
Andreas Lochbihler
parents: 56928
diff changeset
   143
lemma term_of_integer [unfolded typerep_fun_def typerep_num_def typerep_integer_def, code]:
58038
f8e6197668c9 correct code equation for term_of on integer
Andreas Lochbihler
parents: 58036
diff changeset
   144
  "term_of (i :: integer) =
f8e6197668c9 correct code equation for term_of on integer
Andreas Lochbihler
parents: 58036
diff changeset
   145
  (if i > 0 then 
f8e6197668c9 correct code equation for term_of on integer
Andreas Lochbihler
parents: 58036
diff changeset
   146
     App (Const (STR ''Num.numeral_class.numeral'') (TYPEREP(num \<Rightarrow> integer)))
f8e6197668c9 correct code equation for term_of on integer
Andreas Lochbihler
parents: 58036
diff changeset
   147
      (term_of (num_of_integer i))
f8e6197668c9 correct code equation for term_of on integer
Andreas Lochbihler
parents: 58036
diff changeset
   148
   else if i = 0 then Const (STR ''Groups.zero_class.zero'') TYPEREP(integer)
f8e6197668c9 correct code equation for term_of on integer
Andreas Lochbihler
parents: 58036
diff changeset
   149
   else
f8e6197668c9 correct code equation for term_of on integer
Andreas Lochbihler
parents: 58036
diff changeset
   150
     App (Const (STR ''Groups.uminus_class.uminus'') TYPEREP(integer \<Rightarrow> integer))
f8e6197668c9 correct code equation for term_of on integer
Andreas Lochbihler
parents: 58036
diff changeset
   151
       (term_of (- i)))"
62597
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61799
diff changeset
   152
  by (rule term_of_anything [THEN meta_eq_to_obj_eq])
58036
f23045003476 add code equation for term_of on integer
Andreas Lochbihler
parents: 56928
diff changeset
   153
39564
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   154
code_reserved Eval HOLogic
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   155
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   156
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59484
diff changeset
   157
subsection \<open>Generic reification\<close>
31178
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
   158
56928
1e50fddbe1f5 dropped term_of obfuscation -- not really required;
haftmann
parents: 56927
diff changeset
   159
ML_file "~~/src/HOL/Tools/reification.ML"
31178
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
   160
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
   161
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59484
diff changeset
   162
subsection \<open>Diagnostic\<close>
39387
6608c4838ff9 replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
haftmann
parents: 39274
diff changeset
   163
6608c4838ff9 replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
haftmann
parents: 39274
diff changeset
   164
definition tracing :: "String.literal \<Rightarrow> 'a \<Rightarrow> 'a" where
6608c4838ff9 replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
haftmann
parents: 39274
diff changeset
   165
  [code del]: "tracing s x = x"
6608c4838ff9 replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
haftmann
parents: 39274
diff changeset
   166
52435
6646bb548c6b migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents: 52286
diff changeset
   167
code_printing
6646bb548c6b migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents: 52286
diff changeset
   168
  constant "tracing :: String.literal => 'a => 'a" \<rightharpoonup> (Eval) "Code'_Evaluation.tracing"
33473
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 32740
diff changeset
   169
31178
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
   170
40638
6b137c96df07 adding dummy definition for Code_Evaluation.Abs and hiding constants App less strict
bulwahn
parents: 39567
diff changeset
   171
hide_const dummy_term valapp
51144
0ede9e2266a8 less customary term_of conversions;
haftmann
parents: 51143
diff changeset
   172
hide_const (open) Const App Abs Free termify valtermify term_of tracing
28228
7ebe8dc06cbb evaluation using code generator
haftmann
parents:
diff changeset
   173
7ebe8dc06cbb evaluation using code generator
haftmann
parents:
diff changeset
   174
end
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   175