1(* Title: HOL/Code_Evaluation.thy 2 Author: Florian Haftmann, TU Muenchen 3*) 4 5section \<open>Term evaluation using the generic code generator\<close> 6 7theory Code_Evaluation 8imports Typerep Limited_Sequence 9keywords "value" :: diag 10begin 11 12subsection \<open>Term representation\<close> 13 14subsubsection \<open>Terms and class \<open>term_of\<close>\<close> 15 16datatype (plugins only: extraction) "term" = dummy_term 17 18definition Const :: "String.literal \<Rightarrow> typerep \<Rightarrow> term" where 19 "Const _ _ = dummy_term" 20 21definition App :: "term \<Rightarrow> term \<Rightarrow> term" where 22 "App _ _ = dummy_term" 23 24definition Abs :: "String.literal \<Rightarrow> typerep \<Rightarrow> term \<Rightarrow> term" where 25 "Abs _ _ _ = dummy_term" 26 27definition Free :: "String.literal \<Rightarrow> typerep \<Rightarrow> term" where 28 "Free _ _ = dummy_term" 29 30code_datatype Const App Abs Free 31 32class term_of = typerep + 33 fixes term_of :: "'a \<Rightarrow> term" 34 35lemma term_of_anything: "term_of x \<equiv> t" 36 by (rule eq_reflection) (cases "term_of x", cases t, simp) 37 38definition valapp :: "('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term) 39 \<Rightarrow> 'a \<times> (unit \<Rightarrow> term) \<Rightarrow> 'b \<times> (unit \<Rightarrow> term)" where 40 "valapp f x = (fst f (fst x), \<lambda>u. App (snd f ()) (snd x ()))" 41 42lemma valapp_code [code, code_unfold]: 43 "valapp (f, tf) (x, tx) = (f x, \<lambda>u. App (tf ()) (tx ()))" 44 by (simp only: valapp_def fst_conv snd_conv) 45 46 47subsubsection \<open>Syntax\<close> 48 49definition termify :: "'a \<Rightarrow> term" where 50 [code del]: "termify x = dummy_term" 51 52abbreviation valtermify :: "'a \<Rightarrow> 'a \<times> (unit \<Rightarrow> term)" where 53 "valtermify x \<equiv> (x, \<lambda>u. termify x)" 54 55locale term_syntax 56begin 57 58notation App (infixl "<\<cdot>>" 70) 59 and valapp (infixl "{\<cdot>}" 70) 60 61end 62 63interpretation term_syntax . 64 65no_notation App (infixl "<\<cdot>>" 70) 66 and valapp (infixl "{\<cdot>}" 70) 67 68 69subsection \<open>Tools setup and evaluation\<close> 70 71context 72begin 73 74qualified definition TERM_OF :: "'a::term_of itself" 75where 76 "TERM_OF = snd (Code_Evaluation.term_of :: 'a \<Rightarrow> _, TYPE('a))" 77 78qualified definition TERM_OF_EQUAL :: "'a::term_of itself" 79where 80 "TERM_OF_EQUAL = snd (\<lambda>(a::'a). (Code_Evaluation.term_of a, HOL.eq a), TYPE('a))" 81 82end 83 84lemma eq_eq_TrueD: 85 fixes x y :: "'a::{}" 86 assumes "(x \<equiv> y) \<equiv> Trueprop True" 87 shows "x \<equiv> y" 88 using assms by simp 89 90code_printing 91 type_constructor "term" \<rightharpoonup> (Eval) "Term.term" 92| constant Const \<rightharpoonup> (Eval) "Term.Const/ ((_), (_))" 93| constant App \<rightharpoonup> (Eval) "Term.$/ ((_), (_))" 94| constant Abs \<rightharpoonup> (Eval) "Term.Abs/ ((_), (_), (_))" 95| constant Free \<rightharpoonup> (Eval) "Term.Free/ ((_), (_))" 96 97ML_file "Tools/code_evaluation.ML" 98 99code_reserved Eval Code_Evaluation 100 101ML_file "~~/src/HOL/Tools/value_command.ML" 102 103 104subsection \<open>Dedicated \<open>term_of\<close> instances\<close> 105 106instantiation "fun" :: (typerep, typerep) term_of 107begin 108 109definition 110 "term_of (f :: 'a \<Rightarrow> 'b) = 111 Const (STR ''Pure.dummy_pattern'') 112 (Typerep.Typerep (STR ''fun'') [Typerep.typerep TYPE('a), Typerep.typerep TYPE('b)])" 113 114instance .. 115 116end 117 118declare [[code drop: rec_term case_term 119 "term_of :: typerep \<Rightarrow> _" "term_of :: term \<Rightarrow> _" "term_of :: String.literal \<Rightarrow> _" 120 "term_of :: _ Predicate.pred \<Rightarrow> term" "term_of :: _ Predicate.seq \<Rightarrow> term"]] 121 122code_printing 123 constant "term_of :: integer \<Rightarrow> term" \<rightharpoonup> (Eval) "HOLogic.mk'_number/ HOLogic.code'_integerT" 124| constant "term_of :: String.literal \<Rightarrow> term" \<rightharpoonup> (Eval) "HOLogic.mk'_literal" 125 126declare [[code drop: "term_of :: integer \<Rightarrow> _"]] 127 128lemma term_of_integer [unfolded typerep_fun_def typerep_num_def typerep_integer_def, code]: 129 "term_of (i :: integer) = 130 (if i > 0 then 131 App (Const (STR ''Num.numeral_class.numeral'') (TYPEREP(num \<Rightarrow> integer))) 132 (term_of (num_of_integer i)) 133 else if i = 0 then Const (STR ''Groups.zero_class.zero'') TYPEREP(integer) 134 else 135 App (Const (STR ''Groups.uminus_class.uminus'') TYPEREP(integer \<Rightarrow> integer)) 136 (term_of (- i)))" 137 by (rule term_of_anything [THEN meta_eq_to_obj_eq]) 138 139code_reserved Eval HOLogic 140 141 142subsection \<open>Generic reification\<close> 143 144ML_file "~~/src/HOL/Tools/reification.ML" 145 146 147subsection \<open>Diagnostic\<close> 148 149definition tracing :: "String.literal \<Rightarrow> 'a \<Rightarrow> 'a" where 150 [code del]: "tracing s x = x" 151 152code_printing 153 constant "tracing :: String.literal => 'a => 'a" \<rightharpoonup> (Eval) "Code'_Evaluation.tracing" 154 155 156hide_const dummy_term valapp 157hide_const (open) Const App Abs Free termify valtermify term_of tracing 158 159end 160