src/HOL/Code_Evaluation.thy
author haftmann
Thu, 02 Dec 2010 13:53:36 +0100
changeset 40883 b37dca06477f
parent 40638 6b137c96df07
child 40884 3113fd4810bd
permissions -rw-r--r--
separate term_of function for integers -- more canonical representation of negative integers
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
31205
98370b26c2ce String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents: 31203
diff changeset
     8
imports Plain Typerep Code_Numeral
39564
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
     9
uses ("Tools/code_evaluation.ML")
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
6b137c96df07 adding dummy definition for Code_Evaluation.Abs and hiding constants App less strict
bulwahn
parents: 39567
diff changeset
    27
code_datatype Const App Abs
28228
7ebe8dc06cbb evaluation using code generator
haftmann
parents:
diff changeset
    28
28335
25326092cf9a renamed rtype to typerep
haftmann
parents: 28313
diff changeset
    29
class term_of = typerep +
31031
cbec39ebf8f2 class typerep inherits from type
haftmann
parents: 30970
diff changeset
    30
  fixes term_of :: "'a \<Rightarrow> term"
28228
7ebe8dc06cbb evaluation using code generator
haftmann
parents:
diff changeset
    31
7ebe8dc06cbb evaluation using code generator
haftmann
parents:
diff changeset
    32
lemma term_of_anything: "term_of x \<equiv> t"
7ebe8dc06cbb evaluation using code generator
haftmann
parents:
diff changeset
    33
  by (rule eq_reflection) (cases "term_of x", cases t, simp)
7ebe8dc06cbb evaluation using code generator
haftmann
parents:
diff changeset
    34
31191
7733125bac3c tuned term input syntax
haftmann
parents: 31178
diff changeset
    35
definition valapp :: "('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)
31178
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
    36
  \<Rightarrow> 'a \<times> (unit \<Rightarrow> term) \<Rightarrow> 'b \<times> (unit \<Rightarrow> term)" where
31191
7733125bac3c tuned term input syntax
haftmann
parents: 31178
diff changeset
    37
  "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
    38
32069
6d28bbd33e2c prefer code_inline over code_unfold; use code_unfold_post where appropriate
haftmann
parents: 31998
diff changeset
    39
lemma valapp_code [code, code_unfold]:
31191
7733125bac3c tuned term input syntax
haftmann
parents: 31178
diff changeset
    40
  "valapp (f, tf) (x, tx) = (f x, \<lambda>u. App (tf ()) (tx ()))"
7733125bac3c tuned term input syntax
haftmann
parents: 31178
diff changeset
    41
  by (simp only: valapp_def fst_conv snd_conv)
31178
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
    42
28228
7ebe8dc06cbb evaluation using code generator
haftmann
parents:
diff changeset
    43
31178
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
    44
subsubsection {* Syntax *}
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
    45
31191
7733125bac3c tuned term input syntax
haftmann
parents: 31178
diff changeset
    46
definition termify :: "'a \<Rightarrow> term" where
7733125bac3c tuned term input syntax
haftmann
parents: 31178
diff changeset
    47
  [code del]: "termify x = dummy_term"
7733125bac3c tuned term input syntax
haftmann
parents: 31178
diff changeset
    48
7733125bac3c tuned term input syntax
haftmann
parents: 31178
diff changeset
    49
abbreviation valtermify :: "'a \<Rightarrow> 'a \<times> (unit \<Rightarrow> term)" where
7733125bac3c tuned term input syntax
haftmann
parents: 31178
diff changeset
    50
  "valtermify x \<equiv> (x, \<lambda>u. termify x)"
31178
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
    51
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
    52
locale term_syntax
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
    53
begin
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
    54
31191
7733125bac3c tuned term input syntax
haftmann
parents: 31178
diff changeset
    55
notation App (infixl "<\<cdot>>" 70)
7733125bac3c tuned term input syntax
haftmann
parents: 31178
diff changeset
    56
  and valapp (infixl "{\<cdot>}" 70)
31178
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
    57
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
    58
end
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
    59
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
    60
interpretation term_syntax .
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
    61
31191
7733125bac3c tuned term input syntax
haftmann
parents: 31178
diff changeset
    62
no_notation App (infixl "<\<cdot>>" 70)
7733125bac3c tuned term input syntax
haftmann
parents: 31178
diff changeset
    63
  and valapp (infixl "{\<cdot>}" 70)
7733125bac3c tuned term input syntax
haftmann
parents: 31178
diff changeset
    64
7733125bac3c tuned term input syntax
haftmann
parents: 31178
diff changeset
    65
39564
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    66
subsection {* Tools setup and evaluation *}
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    67
39567
5ee997fbe5cc dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents: 39564
diff changeset
    68
lemma eq_eq_TrueD:
5ee997fbe5cc dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents: 39564
diff changeset
    69
  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
    70
  shows "x \<equiv> y"
5ee997fbe5cc dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents: 39564
diff changeset
    71
  using assms by simp
5ee997fbe5cc dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents: 39564
diff changeset
    72
39564
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    73
use "Tools/code_evaluation.ML"
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    74
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    75
code_reserved Eval Code_Evaluation
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    76
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    77
setup {* Code_Evaluation.setup *}
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    78
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    79
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    80
subsection {* @{text term_of} instances *}
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    81
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    82
instantiation "fun" :: (typerep, typerep) term_of
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    83
begin
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
definition
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    86
  "term_of (f \<Colon> 'a \<Rightarrow> 'b) = Const (STR ''dummy_pattern'') (Typerep.Typerep (STR ''fun'')
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    87
     [Typerep.typerep TYPE('a), Typerep.typerep TYPE('b)])"
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    88
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    89
instance ..
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    90
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    91
end
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    92
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    93
instantiation String.literal :: term_of
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    94
begin
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    95
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    96
definition
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    97
  "term_of s = App (Const (STR ''STR'')
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    98
    (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''list'') [Typerep.Typerep (STR ''char'') []],
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
    99
      Typerep.Typerep (STR ''String.literal'') []])) (term_of (String.explode s))"
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   100
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   101
instance ..
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   102
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   103
end
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   104
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
subsubsection {* Code generator setup *}
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   107
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   108
lemmas [code del] = term.recs term.cases term.size
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   109
lemma [code, code del]: "HOL.equal (t1\<Colon>term) t2 \<longleftrightarrow> HOL.equal t1 t2" ..
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   110
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   111
lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   112
lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   113
lemma [code, code del]: "(term_of \<Colon> String.literal \<Rightarrow> term) = term_of" ..
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   114
lemma [code, code del]: "(Code_Evaluation.term_of \<Colon> 'a::{type, term_of} Predicate.pred \<Rightarrow> Code_Evaluation.term)
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   115
  = Code_Evaluation.term_of" ..
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   116
lemma [code, code del]: "(Code_Evaluation.term_of \<Colon> 'a::{type, term_of} Predicate.seq \<Rightarrow> Code_Evaluation.term)
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   117
  = Code_Evaluation.term_of" ..
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   118
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   119
lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]:
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   120
  "Code_Evaluation.term_of c =
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   121
    (let (n, m) = nibble_pair_of_char c
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   122
  in Code_Evaluation.App (Code_Evaluation.App
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)))
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   124
      (Code_Evaluation.term_of n)) (Code_Evaluation.term_of m))"
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
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   127
code_type "term"
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   128
  (Eval "Term.term")
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   129
40638
6b137c96df07 adding dummy definition for Code_Evaluation.Abs and hiding constants App less strict
bulwahn
parents: 39567
diff changeset
   130
code_const Const and App and Abs
6b137c96df07 adding dummy definition for Code_Evaluation.Abs and hiding constants App less strict
bulwahn
parents: 39567
diff changeset
   131
  (Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))" and "Term.Abs/ ((_), (_), (_))")
39564
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
code_const "term_of \<Colon> String.literal \<Rightarrow> term"
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   134
  (Eval "HOLogic.mk'_literal")
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   135
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   136
code_reserved Eval HOLogic
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   137
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   138
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   139
subsubsection {* Numeric types *}
31191
7733125bac3c tuned term input syntax
haftmann
parents: 31178
diff changeset
   140
40883
b37dca06477f separate term_of function for integers -- more canonical representation of negative integers
haftmann
parents: 40638
diff changeset
   141
definition term_of_num_semiring :: "'a\<Colon>semiring_div \<Rightarrow> 'a \<Rightarrow> term" where
b37dca06477f separate term_of function for integers -- more canonical representation of negative integers
haftmann
parents: 40638
diff changeset
   142
  "term_of_num_semiring two = (\<lambda>_. dummy_term)"
31191
7733125bac3c tuned term input syntax
haftmann
parents: 31178
diff changeset
   143
40883
b37dca06477f separate term_of function for integers -- more canonical representation of negative integers
haftmann
parents: 40638
diff changeset
   144
lemma (in term_syntax) term_of_num_semiring_code [code]:
b37dca06477f separate term_of function for integers -- more canonical representation of negative integers
haftmann
parents: 40638
diff changeset
   145
  "term_of_num_semiring two k = (if k = 0 then termify Int.Pls
31191
7733125bac3c tuned term input syntax
haftmann
parents: 31178
diff changeset
   146
    else (if k mod two = 0
40883
b37dca06477f separate term_of function for integers -- more canonical representation of negative integers
haftmann
parents: 40638
diff changeset
   147
      then termify Int.Bit0 <\<cdot>> term_of_num_semiring two (k div two)
b37dca06477f separate term_of function for integers -- more canonical representation of negative integers
haftmann
parents: 40638
diff changeset
   148
      else termify Int.Bit1 <\<cdot>> term_of_num_semiring two (k div two)))"
b37dca06477f separate term_of function for integers -- more canonical representation of negative integers
haftmann
parents: 40638
diff changeset
   149
  by (auto simp add: term_of_anything Const_def App_def term_of_num_semiring_def Let_def)
31191
7733125bac3c tuned term input syntax
haftmann
parents: 31178
diff changeset
   150
7733125bac3c tuned term input syntax
haftmann
parents: 31178
diff changeset
   151
lemma (in term_syntax) term_of_nat_code [code]:
40883
b37dca06477f separate term_of function for integers -- more canonical representation of negative integers
haftmann
parents: 40638
diff changeset
   152
  "term_of (n::nat) = termify (number_of :: int \<Rightarrow> nat) <\<cdot>> term_of_num_semiring (2::nat) n"
31191
7733125bac3c tuned term input syntax
haftmann
parents: 31178
diff changeset
   153
  by (simp only: term_of_anything)
7733125bac3c tuned term input syntax
haftmann
parents: 31178
diff changeset
   154
31205
98370b26c2ce String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents: 31203
diff changeset
   155
lemma (in term_syntax) term_of_code_numeral_code [code]:
98370b26c2ce String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents: 31203
diff changeset
   156
  "term_of (k::code_numeral) = termify (number_of :: int \<Rightarrow> code_numeral) <\<cdot>> term_of_num (2::code_numeral) k"
31203
5c8fb4fd67e0 moved Code_Index, Random and Quickcheck before Main
haftmann
parents: 31191
diff changeset
   157
  by (simp only: term_of_anything)
31191
7733125bac3c tuned term input syntax
haftmann
parents: 31178
diff changeset
   158
40883
b37dca06477f separate term_of function for integers -- more canonical representation of negative integers
haftmann
parents: 40638
diff changeset
   159
definition term_of_num_ring :: "'a\<Colon>ring_div \<Rightarrow> 'a \<Rightarrow> term" where
b37dca06477f separate term_of function for integers -- more canonical representation of negative integers
haftmann
parents: 40638
diff changeset
   160
  "term_of_num_ring two = (\<lambda>_. dummy_term)"
b37dca06477f separate term_of function for integers -- more canonical representation of negative integers
haftmann
parents: 40638
diff changeset
   161
b37dca06477f separate term_of function for integers -- more canonical representation of negative integers
haftmann
parents: 40638
diff changeset
   162
lemma (in term_syntax) term_of_num_ring_code [code]:
b37dca06477f separate term_of function for integers -- more canonical representation of negative integers
haftmann
parents: 40638
diff changeset
   163
  "term_of_num_ring two k = (if k = 0 then termify Int.Pls
b37dca06477f separate term_of function for integers -- more canonical representation of negative integers
haftmann
parents: 40638
diff changeset
   164
    else if k = -1 then termify Int.Min
b37dca06477f separate term_of function for integers -- more canonical representation of negative integers
haftmann
parents: 40638
diff changeset
   165
    else if k mod two = 0 then termify Int.Bit0 <\<cdot>> term_of_num_ring two (k div two)
b37dca06477f separate term_of function for integers -- more canonical representation of negative integers
haftmann
parents: 40638
diff changeset
   166
    else termify Int.Bit1 <\<cdot>> term_of_num_ring two (k div two))"
b37dca06477f separate term_of function for integers -- more canonical representation of negative integers
haftmann
parents: 40638
diff changeset
   167
  by (auto simp add: term_of_anything Const_def App_def term_of_num_ring_def Let_def)
b37dca06477f separate term_of function for integers -- more canonical representation of negative integers
haftmann
parents: 40638
diff changeset
   168
b37dca06477f separate term_of function for integers -- more canonical representation of negative integers
haftmann
parents: 40638
diff changeset
   169
lemma (in term_syntax) term_of_int_code [code]:
b37dca06477f separate term_of function for integers -- more canonical representation of negative integers
haftmann
parents: 40638
diff changeset
   170
  "term_of (k::int) = (if k = 0 then termify (0 :: int)
b37dca06477f separate term_of function for integers -- more canonical representation of negative integers
haftmann
parents: 40638
diff changeset
   171
    else termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num_ring (2::int) k)"
b37dca06477f separate term_of function for integers -- more canonical representation of negative integers
haftmann
parents: 40638
diff changeset
   172
  by (simp only: term_of_anything)
b37dca06477f separate term_of function for integers -- more canonical representation of negative integers
haftmann
parents: 40638
diff changeset
   173
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
   174
39564
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   175
subsubsection {* Obfuscation *}
31178
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
   176
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
   177
print_translation {*
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
   178
let
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
   179
  val term = Const ("<TERM>", dummyT);
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
   180
  fun tr1' [_, _] = term;
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
   181
  fun tr2' [] = term;
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
   182
in
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
   183
  [(@{const_syntax Const}, tr1'),
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
   184
    (@{const_syntax App}, tr1'),
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
   185
    (@{const_syntax dummy_term}, tr2')]
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
   186
end
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
   187
*}
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
   188
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
   189
39564
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39471
diff changeset
   190
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
   191
6608c4838ff9 replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
haftmann
parents: 39274
diff changeset
   192
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
   193
  [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
   194
33473
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 32740
diff changeset
   195
code_const "tracing :: String.literal => 'a => 'a"
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 32740
diff changeset
   196
  (Eval "Code'_Evaluation.tracing")
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 32740
diff changeset
   197
31178
27afaaa6547a syntax support for term expressions
haftmann
parents: 31144
diff changeset
   198
40638
6b137c96df07 adding dummy definition for Code_Evaluation.Abs and hiding constants App less strict
bulwahn
parents: 39567
diff changeset
   199
hide_const dummy_term valapp
40883
b37dca06477f separate term_of function for integers -- more canonical representation of negative integers
haftmann
parents: 40638
diff changeset
   200
hide_const (open) Const App Abs termify valtermify term_of term_of_num_semiring term_of_num_ring tracing
28228
7ebe8dc06cbb evaluation using code generator
haftmann
parents:
diff changeset
   201
7ebe8dc06cbb evaluation using code generator
haftmann
parents:
diff changeset
   202
end