28228

1 
(* Title: HOL/Code_Eval.thy


2 
ID: $Id$


3 
Author: Florian Haftmann, TU Muenchen


4 
*)


5 


6 
header {* Term evaluation using the generic code generator *}


7 


8 
theory Code_Eval

28313

9 
imports Plain "~~/src/HOL/Library/RType"

28228

10 
begin


11 


12 
subsection {* Term representation *}


13 


14 
subsubsection {* Terms and class @{text term_of} *}


15 


16 
datatype "term" = dummy_term


17 


18 
definition

28335

19 
Const :: "message_string \<Rightarrow> typerep \<Rightarrow> term"

28228

20 
where


21 
"Const _ _ = dummy_term"


22 


23 
definition


24 
App :: "term \<Rightarrow> term \<Rightarrow> term"


25 
where


26 
"App _ _ = dummy_term"


27 


28 
code_datatype Const App


29 

28335

30 
class term_of = typerep +

28228

31 
fixes term_of :: "'a \<Rightarrow> term"


32 


33 
lemma term_of_anything: "term_of x \<equiv> t"


34 
by (rule eq_reflection) (cases "term_of x", cases t, simp)


35 


36 
ML {*


37 
structure Eval =


38 
struct


39 


40 
fun mk_term f g (Const (c, ty)) =


41 
@{term Const} $ Message_String.mk c $ g ty


42 
 mk_term f g (t1 $ t2) =


43 
@{term App} $ mk_term f g t1 $ mk_term f g t2


44 
 mk_term f g (Free v) = f v


45 
 mk_term f g (Bound i) = Bound i


46 
 mk_term f g (Abs (v, _, t)) = Abs (v, @{typ term}, mk_term f g t);


47 


48 
fun mk_term_of ty t = Const (@{const_name term_of}, ty > @{typ term}) $ t;


49 


50 
end;


51 
*}


52 


53 


54 
subsubsection {* @{text term_of} instances *}


55 


56 
setup {*


57 
let


58 
fun add_term_of_def ty vs tyco thy =


59 
let


60 
val lhs = Const (@{const_name term_of}, ty > @{typ term})


61 
$ Free ("x", ty);


62 
val rhs = @{term "undefined \<Colon> term"};


63 
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));

28243

64 
fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst


65 
o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv";

28228

66 
in


67 
thy


68 
> TheoryTarget.instantiation ([tyco], vs, @{sort term_of})


69 
> `(fn lthy => Syntax.check_term lthy eq)

28243

70 
> (fn eq => Specification.definition (NONE, ((Name.binding (triv_name_of eq), []), eq)))

28228

71 
> snd


72 
> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))


73 
> LocalTheory.exit


74 
> ProofContext.theory_of


75 
end;


76 
fun interpretator (tyco, (raw_vs, _)) thy =


77 
let


78 
val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};


79 
val constrain_sort =


80 
curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of};


81 
val vs = (map o apsnd) constrain_sort raw_vs;


82 
val ty = Type (tyco, map TFree vs);


83 
in


84 
thy

28335

85 
> Typerep.perhaps_add_def tyco

28228

86 
> not has_inst ? add_term_of_def ty vs tyco


87 
end;


88 
in


89 
Code.type_interpretation interpretator


90 
end


91 
*}


92 


93 
setup {*


94 
let


95 
fun mk_term_of_eq ty vs tyco (c, tys) =


96 
let


97 
val t = list_comb (Const (c, tys > ty),


98 
map Free (Name.names Name.context "a" tys));


99 
in (map_aterms (fn Free (v, ty) => Var ((v, 0), ty)  t => t) t, Eval.mk_term


100 
(fn (v, ty) => Eval.mk_term_of ty (Var ((v, 0), ty)))

28335

101 
(Typerep.mk (fn (v, sort) => Typerep.typerep (TFree (v, sort)))) t)

28228

102 
end;


103 
fun prove_term_of_eq ty eq thy =


104 
let


105 
val cty = Thm.ctyp_of thy ty;


106 
val (arg, rhs) = pairself (Thm.cterm_of thy) eq;


107 
val thm = @{thm term_of_anything}


108 
> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs]


109 
> Thm.varifyT;


110 
in


111 
thy


112 
> Code.add_func thm


113 
end;


114 
fun interpretator (tyco, (raw_vs, raw_cs)) thy =


115 
let


116 
val constrain_sort =


117 
curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of};


118 
val vs = (map o apsnd) constrain_sort raw_vs;


119 
val cs = (map o apsnd o map o map_atyps)


120 
(fn TFree (v, sort) => TFree (v, constrain_sort sort)) raw_cs;


121 
val ty = Type (tyco, map TFree vs);


122 
val eqs = map (mk_term_of_eq ty vs tyco) cs;


123 
val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);


124 
in


125 
thy


126 
> Code.del_funcs const


127 
> fold (prove_term_of_eq ty) eqs


128 
end;


129 
in


130 
Code.type_interpretation interpretator


131 
end


132 
*}


133 


134 


135 
subsubsection {* Code generator setup *}


136 


137 
lemmas [code func del] = term.recs term.cases term.size


138 
lemma [code func, code func del]: "(t1\<Colon>term) = t2 \<longleftrightarrow> t1 = t2" ..


139 

28335

140 
lemma [code func, code func del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..

28228

141 
lemma [code func, code func del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..


142 
lemma [code func, code func del]: "(term_of \<Colon> message_string \<Rightarrow> term) = term_of" ..


143 

28335

144 
lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code func]: "Code_Eval.term_of c =

28243

145 
(let (n, m) = nibble_pair_of_char c

28335

146 
in Code_Eval.App (Code_Eval.App (Code_Eval.Const (STR ''Pair'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))

28243

147 
(Code_Eval.term_of n)) (Code_Eval.term_of m))"


148 
by (subst term_of_anything) rule


149 

28228

150 
code_type "term"


151 
(SML "Term.term")


152 


153 
code_const Const and App


154 
(SML "Term.Const/ (_, _)" and "Term.$/ (_, _)")


155 


156 
code_const "term_of \<Colon> message_string \<Rightarrow> term"


157 
(SML "Message'_String.mk")


158 


159 


160 
subsection {* Evaluation setup *}


161 


162 
ML {*


163 
signature EVAL =


164 
sig


165 
val mk_term: ((string * typ) > term) > (typ > term) > term > term


166 
val eval_ref: (unit > term) option ref


167 
val eval_term: theory > term > term


168 
end;


169 


170 
structure Eval : EVAL =


171 
struct


172 


173 
open Eval;


174 


175 
val eval_ref = ref (NONE : (unit > term) option);


176 


177 
fun eval_term thy t =


178 
t


179 
> Eval.mk_term_of (fastype_of t)


180 
> (fn t => Code_ML.eval_term ("Eval.eval_ref", eval_ref) thy t [])


181 
> Code.postprocess_term thy;


182 


183 
end;


184 
*}


185 


186 
setup {*


187 
Value.add_evaluator ("code", Eval.eval_term o ProofContext.theory_of)


188 
*}


189 

28243

190 


191 
subsubsection {* Syntax *}


192 


193 
print_translation {*


194 
let


195 
val term = Const ("<TERM>", dummyT);


196 
fun tr1' [_, _] = term;


197 
fun tr2' [] = term;


198 
in


199 
[(@{const_syntax Const}, tr1'),


200 
(@{const_syntax App}, tr1'),


201 
(@{const_syntax dummy_term}, tr2')]

28228

202 
end

28243

203 
*}


204 


205 
hide const dummy_term


206 
hide (open) const Const App


207 
hide (open) const term_of


208 


209 
end
