src/HOL/Code_Evaluation.thy
author haftmann
Fri, 09 May 2014 08:13:37 +0200
changeset 56928 1e50fddbe1f5
parent 56927 4044a7d1720f
child 58036 f23045003476
permissions -rw-r--r--
dropped term_of obfuscation -- not really required; tuned theory structure
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
7ebe8dc06cbb evaluation using code generator
haftmann
parents:
diff changeset
     5
header {* Term evaluation using the generic code generator *}
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
7ebe8dc06cbb evaluation using code generator
haftmann
parents:
diff changeset
    12
subsection {* Term representation *}
7ebe8dc06cbb evaluation using code generator
haftmann
parents:
diff changeset
    13
7ebe8dc06cbb evaluation using code generator
haftmann
parents:
diff changeset
    14
subsubsection {* Terms and class @{text term_of} *}
7ebe8dc06cbb evaluation using code generator
haftmann
parents:
diff changeset
    15
7ebe8dc06cbb evaluation using code generator
haftmann
parents:
diff changeset
    16
datatype "term" = dummy_term
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
31178
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
    47
subsubsection {* Syntax *}
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
39564
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    69
subsection {* Tools setup and evaluation *}
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    70
39567
5ee997fbe5cc dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents: 39564
diff changeset
    71
lemma eq_eq_TrueD:
5ee997fbe5cc dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents: 39564
diff changeset
    72
  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
    73
  shows "x \<equiv> y"
5ee997fbe5cc dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents: 39564
diff changeset
    74
  using assms by simp
5ee997fbe5cc dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents: 39564
diff changeset
    75
56928
1e50fddbe1f5 dropped term_of obfuscation -- not really required;
haftmann
parents: 56927
diff changeset
    76
code_printing
1e50fddbe1f5 dropped term_of obfuscation -- not really required;
haftmann
parents: 56927
diff changeset
    77
  type_constructor "term" \<rightharpoonup> (Eval) "Term.term"
1e50fddbe1f5 dropped term_of obfuscation -- not really required;
haftmann
parents: 56927
diff changeset
    78
| constant Const \<rightharpoonup> (Eval) "Term.Const/ ((_), (_))"
1e50fddbe1f5 dropped term_of obfuscation -- not really required;
haftmann
parents: 56927
diff changeset
    79
| constant App \<rightharpoonup> (Eval) "Term.$/ ((_), (_))"
1e50fddbe1f5 dropped term_of obfuscation -- not really required;
haftmann
parents: 56927
diff changeset
    80
| constant Abs \<rightharpoonup> (Eval) "Term.Abs/ ((_), (_), (_))"
1e50fddbe1f5 dropped term_of obfuscation -- not really required;
haftmann
parents: 56927
diff changeset
    81
| constant Free \<rightharpoonup> (Eval) "Term.Free/ ((_), (_))"
1e50fddbe1f5 dropped term_of obfuscation -- not really required;
haftmann
parents: 56927
diff changeset
    82
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47108
diff changeset
    83
ML_file "Tools/code_evaluation.ML"
39564
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    84
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    85
code_reserved Eval Code_Evaluation
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    86
56928
1e50fddbe1f5 dropped term_of obfuscation -- not really required;
haftmann
parents: 56927
diff changeset
    87
ML_file "~~/src/HOL/Tools/value.ML"
1e50fddbe1f5 dropped term_of obfuscation -- not really required;
haftmann
parents: 56927
diff changeset
    88
39564
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    89
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    90
subsection {* @{text term_of} instances *}
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    91
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    92
instantiation "fun" :: (typerep, typerep) term_of
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    93
begin
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    94
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    95
definition
56241
029246729dc0 more qualified names;
wenzelm
parents: 55642
diff changeset
    96
  "term_of (f \<Colon> 'a \<Rightarrow> 'b) =
029246729dc0 more qualified names;
wenzelm
parents: 55642
diff changeset
    97
    Const (STR ''Pure.dummy_pattern'')
029246729dc0 more qualified names;
wenzelm
parents: 55642
diff changeset
    98
      (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
    99
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   100
instance ..
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   101
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   102
end
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   103
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   104
instantiation String.literal :: term_of
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   105
begin
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   106
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   107
definition
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   108
  "term_of s = App (Const (STR ''STR'')
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   109
    (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''list'') [Typerep.Typerep (STR ''char'') []],
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   110
      Typerep.Typerep (STR ''String.literal'') []])) (term_of (String.explode s))"
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   111
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   112
instance ..
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
end
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   115
56926
aaea99edc040 modernized setups
haftmann
parents: 56925
diff changeset
   116
declare [[code drop: rec_term case_term size_term "size :: term \<Rightarrow> _" "HOL.equal :: term \<Rightarrow> _"
aaea99edc040 modernized setups
haftmann
parents: 56925
diff changeset
   117
  "term_of :: typerep \<Rightarrow> _" "term_of :: term \<Rightarrow> _" "term_of :: String.literal \<Rightarrow> _"
aaea99edc040 modernized setups
haftmann
parents: 56925
diff changeset
   118
  "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
   119
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   120
lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]:
51160
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 51144
diff changeset
   121
  "Code_Evaluation.term_of c = (case c of Char x y \<Rightarrow>
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 51144
diff changeset
   122
   Code_Evaluation.App (Code_Evaluation.App
39564
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   123
    (Code_Evaluation.Const (STR ''String.char.Char'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
51160
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 51144
diff changeset
   124
      (Code_Evaluation.term_of x)) (Code_Evaluation.term_of y))"
39564
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   125
  by (subst term_of_anything) rule 
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   126
52435
6646bb548c6b migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents: 52286
diff changeset
   127
code_printing
56928
1e50fddbe1f5 dropped term_of obfuscation -- not really required;
haftmann
parents: 56927
diff changeset
   128
  constant "term_of \<Colon> integer \<Rightarrow> term" \<rightharpoonup> (Eval) "HOLogic.mk'_number/ HOLogic.code'_integerT"
52435
6646bb548c6b migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents: 52286
diff changeset
   129
| constant "term_of \<Colon> String.literal \<Rightarrow> term" \<rightharpoonup> (Eval) "HOLogic.mk'_literal"
39564
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   130
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   131
code_reserved Eval HOLogic
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   132
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   133
56928
1e50fddbe1f5 dropped term_of obfuscation -- not really required;
haftmann
parents: 56927
diff changeset
   134
subsection {* Generic reification *}
31178
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
   135
56928
1e50fddbe1f5 dropped term_of obfuscation -- not really required;
haftmann
parents: 56927
diff changeset
   136
ML_file "~~/src/HOL/Tools/reification.ML"
31178
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
   137
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
   138
39564
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   139
subsection {* Diagnostic *}
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
   140
6608c4838ff9 replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
haftmann
parents: 39274
diff changeset
   141
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
   142
  [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
   143
52435
6646bb548c6b migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents: 52286
diff changeset
   144
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
   145
  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
   146
31178
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
   147
40638
6b137c96df07 adding dummy definition for Code_Evaluation.Abs and hiding constants App less strict
bulwahn
parents: 39567
diff changeset
   148
hide_const dummy_term valapp
51144
0ede9e2266a8 less customary term_of conversions;
haftmann
parents: 51143
diff changeset
   149
hide_const (open) Const App Abs Free termify valtermify term_of tracing
28228
7ebe8dc06cbb evaluation using code generator
haftmann
parents:
diff changeset
   150
7ebe8dc06cbb evaluation using code generator
haftmann
parents:
diff changeset
   151
end
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   152