haftmann@32657: (* Title: HOL/Code_Evaluation.thy haftmann@28228: Author: Florian Haftmann, TU Muenchen haftmann@28228: *) haftmann@28228: haftmann@28228: header {* Term evaluation using the generic code generator *} haftmann@28228: haftmann@32657: theory Code_Evaluation haftmann@51126: imports Typerep Limited_Sequence haftmann@28228: begin haftmann@28228: haftmann@28228: subsection {* Term representation *} haftmann@28228: haftmann@28228: subsubsection {* Terms and class @{text term_of} *} haftmann@28228: haftmann@28228: datatype "term" = dummy_term haftmann@28228: haftmann@31205: definition Const :: "String.literal \ typerep \ term" where haftmann@28228: "Const _ _ = dummy_term" haftmann@28228: haftmann@28661: definition App :: "term \ term \ term" where haftmann@28228: "App _ _ = dummy_term" haftmann@28228: bulwahn@40638: definition Abs :: "String.literal \ typerep \ term \ term" where bulwahn@40638: "Abs _ _ _ = dummy_term" bulwahn@40638: bulwahn@42979: definition Free :: "String.literal \ typerep \ term" where bulwahn@42979: "Free _ _ = dummy_term" bulwahn@42979: bulwahn@42979: code_datatype Const App Abs Free haftmann@28228: haftmann@28335: class term_of = typerep + haftmann@31031: fixes term_of :: "'a \ term" haftmann@28228: haftmann@28228: lemma term_of_anything: "term_of x \ t" haftmann@28228: by (rule eq_reflection) (cases "term_of x", cases t, simp) haftmann@28228: haftmann@31191: definition valapp :: "('a \ 'b) \ (unit \ term) haftmann@31178: \ 'a \ (unit \ term) \ 'b \ (unit \ term)" where haftmann@31191: "valapp f x = (fst f (fst x), \u. App (snd f ()) (snd x ()))" haftmann@31178: haftmann@32069: lemma valapp_code [code, code_unfold]: haftmann@31191: "valapp (f, tf) (x, tx) = (f x, \u. App (tf ()) (tx ()))" haftmann@31191: by (simp only: valapp_def fst_conv snd_conv) haftmann@31178: haftmann@28228: haftmann@31178: subsubsection {* Syntax *} haftmann@31178: haftmann@31191: definition termify :: "'a \ term" where haftmann@31191: [code del]: "termify x = dummy_term" haftmann@31191: haftmann@31191: abbreviation valtermify :: "'a \ 'a \ (unit \ term)" where haftmann@31191: "valtermify x \ (x, \u. termify x)" haftmann@31178: haftmann@31178: locale term_syntax haftmann@31178: begin haftmann@31178: haftmann@31191: notation App (infixl "<\>" 70) haftmann@31191: and valapp (infixl "{\}" 70) haftmann@31178: haftmann@31178: end haftmann@31178: haftmann@31178: interpretation term_syntax . haftmann@31178: haftmann@31191: no_notation App (infixl "<\>" 70) haftmann@31191: and valapp (infixl "{\}" 70) haftmann@31191: haftmann@31191: haftmann@39564: subsection {* Tools setup and evaluation *} haftmann@39564: haftmann@39567: lemma eq_eq_TrueD: haftmann@39567: assumes "(x \ y) \ Trueprop True" haftmann@39567: shows "x \ y" haftmann@39567: using assms by simp haftmann@39567: wenzelm@48891: ML_file "Tools/code_evaluation.ML" haftmann@39564: haftmann@39564: code_reserved Eval Code_Evaluation haftmann@39564: haftmann@39564: setup {* Code_Evaluation.setup *} haftmann@39564: haftmann@39564: haftmann@39564: subsection {* @{text term_of} instances *} haftmann@39564: haftmann@39564: instantiation "fun" :: (typerep, typerep) term_of haftmann@39564: begin haftmann@39564: haftmann@39564: definition haftmann@39564: "term_of (f \ 'a \ 'b) = Const (STR ''dummy_pattern'') (Typerep.Typerep (STR ''fun'') haftmann@39564: [Typerep.typerep TYPE('a), Typerep.typerep TYPE('b)])" haftmann@39564: haftmann@39564: instance .. haftmann@39564: haftmann@39564: end haftmann@39564: haftmann@39564: instantiation String.literal :: term_of haftmann@39564: begin haftmann@39564: haftmann@39564: definition haftmann@39564: "term_of s = App (Const (STR ''STR'') haftmann@39564: (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''list'') [Typerep.Typerep (STR ''char'') []], haftmann@39564: Typerep.Typerep (STR ''String.literal'') []])) (term_of (String.explode s))" haftmann@39564: haftmann@39564: instance .. haftmann@39564: haftmann@39564: end haftmann@39564: haftmann@39564: haftmann@39564: subsubsection {* Code generator setup *} haftmann@39564: haftmann@39564: lemmas [code del] = term.recs term.cases term.size haftmann@39564: lemma [code, code del]: "HOL.equal (t1\term) t2 \ HOL.equal t1 t2" .. haftmann@39564: haftmann@39564: lemma [code, code del]: "(term_of \ typerep \ term) = term_of" .. haftmann@39564: lemma [code, code del]: "(term_of \ term \ term) = term_of" .. haftmann@39564: lemma [code, code del]: "(term_of \ String.literal \ term) = term_of" .. haftmann@39564: lemma [code, code del]: "(Code_Evaluation.term_of \ 'a::{type, term_of} Predicate.pred \ Code_Evaluation.term) haftmann@39564: = Code_Evaluation.term_of" .. haftmann@39564: lemma [code, code del]: "(Code_Evaluation.term_of \ 'a::{type, term_of} Predicate.seq \ Code_Evaluation.term) haftmann@39564: = Code_Evaluation.term_of" .. haftmann@39564: haftmann@39564: lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]: haftmann@51160: "Code_Evaluation.term_of c = (case c of Char x y \ haftmann@51160: Code_Evaluation.App (Code_Evaluation.App haftmann@39564: (Code_Evaluation.Const (STR ''String.char.Char'') (TYPEREP(nibble \ nibble \ char))) haftmann@51160: (Code_Evaluation.term_of x)) (Code_Evaluation.term_of y))" haftmann@39564: by (subst term_of_anything) rule haftmann@39564: haftmann@52435: code_printing haftmann@52435: type_constructor "term" \ (Eval) "Term.term" haftmann@52435: | constant Const \ (Eval) "Term.Const/ ((_), (_))" haftmann@52435: | constant App \ (Eval) "Term.$/ ((_), (_))" haftmann@52435: | constant Abs \ (Eval) "Term.Abs/ ((_), (_), (_))" haftmann@52435: | constant Free \ (Eval) "Term.Free/ ((_), (_))" haftmann@52435: | constant "term_of \ integer \ term" \ (Eval) "HOLogic.mk'_number/ HOLogic.code'_integerT" haftmann@52435: | constant "term_of \ String.literal \ term" \ (Eval) "HOLogic.mk'_literal" haftmann@39564: haftmann@39564: code_reserved Eval HOLogic haftmann@39564: haftmann@39564: haftmann@39564: subsubsection {* Obfuscation *} haftmann@31178: haftmann@31178: print_translation {* wenzelm@52143: let wenzelm@52143: val term = Const ("", dummyT); wenzelm@52143: fun tr1' _ [_, _] = term; wenzelm@52143: fun tr2' _ [] = term; wenzelm@52143: in wenzelm@52143: [(@{const_syntax Const}, tr1'), haftmann@31178: (@{const_syntax App}, tr1'), haftmann@31178: (@{const_syntax dummy_term}, tr2')] wenzelm@52143: end haftmann@31178: *} haftmann@31178: haftmann@31178: haftmann@39564: subsection {* Diagnostic *} haftmann@39387: haftmann@39387: definition tracing :: "String.literal \ 'a \ 'a" where haftmann@39387: [code del]: "tracing s x = x" haftmann@39387: haftmann@52435: code_printing haftmann@52435: constant "tracing :: String.literal => 'a => 'a" \ (Eval) "Code'_Evaluation.tracing" bulwahn@33473: haftmann@31178: haftmann@52286: subsection {* Generic reification *} haftmann@52286: haftmann@52286: ML_file "~~/src/HOL/Tools/reification.ML" haftmann@52286: haftmann@52286: bulwahn@40638: hide_const dummy_term valapp haftmann@51144: hide_const (open) Const App Abs Free termify valtermify term_of tracing haftmann@28228: haftmann@28228: end haftmann@51143: