dropped term_of obfuscation -- not really required;
authorhaftmann
Fri May 09 08:13:37 2014 +0200 (2014-05-09)
changeset 569281e50fddbe1f5
parent 56927 4044a7d1720f
child 56929 40213e24c8c4
dropped term_of obfuscation -- not really required;
tuned theory structure
src/HOL/Code_Evaluation.thy
     1.1 --- a/src/HOL/Code_Evaluation.thy	Fri May 09 08:13:37 2014 +0200
     1.2 +++ b/src/HOL/Code_Evaluation.thy	Fri May 09 08:13:37 2014 +0200
     1.3 @@ -73,10 +73,19 @@
     1.4    shows "x \<equiv> y"
     1.5    using assms by simp
     1.6  
     1.7 +code_printing
     1.8 +  type_constructor "term" \<rightharpoonup> (Eval) "Term.term"
     1.9 +| constant Const \<rightharpoonup> (Eval) "Term.Const/ ((_), (_))"
    1.10 +| constant App \<rightharpoonup> (Eval) "Term.$/ ((_), (_))"
    1.11 +| constant Abs \<rightharpoonup> (Eval) "Term.Abs/ ((_), (_), (_))"
    1.12 +| constant Free \<rightharpoonup> (Eval) "Term.Free/ ((_), (_))"
    1.13 +
    1.14  ML_file "Tools/code_evaluation.ML"
    1.15  
    1.16  code_reserved Eval Code_Evaluation
    1.17  
    1.18 +ML_file "~~/src/HOL/Tools/value.ML"
    1.19 +
    1.20  
    1.21  subsection {* @{text term_of} instances *}
    1.22  
    1.23 @@ -104,9 +113,6 @@
    1.24  
    1.25  end
    1.26  
    1.27 -
    1.28 -subsubsection {* Code generator setup *}
    1.29 -
    1.30  declare [[code drop: rec_term case_term size_term "size :: term \<Rightarrow> _" "HOL.equal :: term \<Rightarrow> _"
    1.31    "term_of :: typerep \<Rightarrow> _" "term_of :: term \<Rightarrow> _" "term_of :: String.literal \<Rightarrow> _"
    1.32    "term_of :: _ Predicate.pred \<Rightarrow> term" "term_of :: _ Predicate.seq \<Rightarrow> term"]]
    1.33 @@ -119,30 +125,15 @@
    1.34    by (subst term_of_anything) rule 
    1.35  
    1.36  code_printing
    1.37 -  type_constructor "term" \<rightharpoonup> (Eval) "Term.term"
    1.38 -| constant Const \<rightharpoonup> (Eval) "Term.Const/ ((_), (_))"
    1.39 -| constant App \<rightharpoonup> (Eval) "Term.$/ ((_), (_))"
    1.40 -| constant Abs \<rightharpoonup> (Eval) "Term.Abs/ ((_), (_), (_))"
    1.41 -| constant Free \<rightharpoonup> (Eval) "Term.Free/ ((_), (_))"
    1.42 -| constant "term_of \<Colon> integer \<Rightarrow> term" \<rightharpoonup> (Eval) "HOLogic.mk'_number/ HOLogic.code'_integerT"
    1.43 +  constant "term_of \<Colon> integer \<Rightarrow> term" \<rightharpoonup> (Eval) "HOLogic.mk'_number/ HOLogic.code'_integerT"
    1.44  | constant "term_of \<Colon> String.literal \<Rightarrow> term" \<rightharpoonup> (Eval) "HOLogic.mk'_literal"
    1.45  
    1.46  code_reserved Eval HOLogic
    1.47  
    1.48  
    1.49 -subsubsection {* Obfuscation *}
    1.50 +subsection {* Generic reification *}
    1.51  
    1.52 -print_translation {*
    1.53 -  let
    1.54 -    val term = Const ("<TERM>", dummyT);
    1.55 -    fun tr1' _ [_, _] = term;
    1.56 -    fun tr2' _ [] = term;
    1.57 -  in
    1.58 -   [(@{const_syntax Const}, tr1'),
    1.59 -    (@{const_syntax App}, tr1'),
    1.60 -    (@{const_syntax dummy_term}, tr2')]
    1.61 -  end
    1.62 -*}
    1.63 +ML_file "~~/src/HOL/Tools/reification.ML"
    1.64  
    1.65  
    1.66  subsection {* Diagnostic *}
    1.67 @@ -154,16 +145,6 @@
    1.68    constant "tracing :: String.literal => 'a => 'a" \<rightharpoonup> (Eval) "Code'_Evaluation.tracing"
    1.69  
    1.70  
    1.71 -subsection {* Interactive evaluation *}
    1.72 -
    1.73 -ML_file "~~/src/HOL/Tools/value.ML"
    1.74 -
    1.75 -
    1.76 -subsection {* Generic reification *}
    1.77 -
    1.78 -ML_file "~~/src/HOL/Tools/reification.ML"
    1.79 -
    1.80 -
    1.81  hide_const dummy_term valapp
    1.82  hide_const (open) Const App Abs Free termify valtermify term_of tracing
    1.83