
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@31205: imports Plain Typerep Code_Numeral
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 \<Rightarrow> typerep \<Rightarrow> term" where
haftmann@28228:   "Const _ _ = dummy_term"
haftmann@28228: 
haftmann@28661: definition App :: "term \<Rightarrow> term \<Rightarrow> term" where
haftmann@28228:   "App _ _ = dummy_term"
haftmann@28228: 
haftmann@28228: code_datatype Const App
haftmann@28228: 
haftmann@28335: class term_of = typerep +
haftmann@31031:   fixes term_of :: "'a \<Rightarrow> term"
haftmann@28228: 
haftmann@28228: lemma term_of_anything: "term_of x \<equiv> t"
haftmann@28228:   by (rule eq_reflection) (cases "term_of x", cases t, simp)
haftmann@28228: 
haftmann@31191: definition valapp :: "('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)
haftmann@31178:   \<Rightarrow> 'a \<times> (unit \<Rightarrow> term) \<Rightarrow> 'b \<times> (unit \<Rightarrow> term)" where
haftmann@31191:   "valapp f x = (fst f (fst x), \<lambda>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, \<lambda>u. App (tf ()) (tx ()))"
haftmann@31191:   by (simp only: valapp_def fst_conv snd_conv)
haftmann@31178: 
haftmann@28228: 
haftmann@28228: subsubsection {* @{text term_of} instances *}
haftmann@28228: 
haftmann@32344: instantiation "fun" :: (typerep, typerep) term_of
haftmann@32344: begin
haftmann@32344: 
haftmann@32344: definition
haftmann@32344:   "term_of (f \<Colon> 'a \<Rightarrow> 'b) = Const (STR ''dummy_pattern'') (Typerep.Typerep (STR ''fun'')
haftmann@32344:      [Typerep.typerep TYPE('a), Typerep.typerep TYPE('b)])"
haftmann@32344: 
haftmann@32344: instance ..
haftmann@32344: 
haftmann@32344: end
haftmann@32344: 
haftmann@28228: setup {*
haftmann@28228: let
haftmann@31139:   fun add_term_of tyco raw_vs thy =
haftmann@28228:     let
haftmann@31139:       val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs;
haftmann@31139:       val ty = Type (tyco, map TFree vs);
haftmann@28228:       val lhs = Const (@{const_name term_of}, ty --> @{typ term})
haftmann@28228:         $ Free ("x", ty);
haftmann@28228:       val rhs = @{term "undefined \<Colon> term"};
haftmann@28228:       val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
haftmann@28243:       fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst
haftmann@28243:         o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv";
haftmann@28228:     in
haftmann@28228:       thy
wenzelm@33553:       |> Theory_Target.instantiation ([tyco], vs, @{sort term_of})
haftmann@28228:       |> `(fn lthy => Syntax.check_term lthy eq)
haftmann@28965:       |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq)))
haftmann@28228:       |> snd
haftmann@31139:       |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
haftmann@28228:     end;
haftmann@31139:   fun ensure_term_of (tyco, (raw_vs, _)) thy =
haftmann@31139:     let
haftmann@31139:       val need_inst = not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of})
haftmann@31139:         andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep};
haftmann@31205:     in if need_inst then add_term_of tyco raw_vs thy else thy end;
haftmann@28228: in
haftmann@35299:   Code.datatype_interpretation ensure_term_of
haftmann@35299:   #> Code.abstype_interpretation ensure_term_of
haftmann@28228: end
haftmann@28228: *}
haftmann@28228: 
haftmann@28228: setup {*
haftmann@28228: let
haftmann@31139:   fun mk_term_of_eq thy ty vs tyco (c, tys) =
haftmann@28228:     let
haftmann@28228:       val t = list_comb (Const (c, tys ---> ty),
haftmann@28228:         map Free (Name.names Name.context "a" tys));
wenzelm@35845:       val (arg, rhs) =
wenzelm@35845:         pairself (Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global)
wenzelm@35845:           (t, (map_aterms (fn t as Free (v, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t)
haftmann@31139:       val cty = Thm.ctyp_of thy ty;
haftmann@31139:     in
haftmann@31139:       @{thm term_of_anything}
haftmann@31139:       |> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs]
wenzelm@35845:       |> Thm.varifyT_global
haftmann@28228:     end;
haftmann@31139:   fun add_term_of_code tyco raw_vs raw_cs thy =
haftmann@28228:     let
haftmann@31746:       val algebra = Sign.classes_of thy;
haftmann@31746:       val vs = map (fn (v, sort) =>
haftmann@31746:         (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs;
haftmann@31139:       val ty = Type (tyco, map TFree vs);
haftmann@31139:       val cs = (map o apsnd o map o map_atyps)
haftmann@31139:         (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
haftmann@31139:       val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
haftmann@31139:       val eqs = map (mk_term_of_eq thy ty vs tyco) cs;
haftmann@31139:    in
haftmann@31139:       thy
haftmann@31139:       |> Code.del_eqns const
haftmann@31139:       |> fold Code.add_eqn eqs
haftmann@31139:     end;
haftmann@31139:   fun ensure_term_of_code (tyco, (raw_vs, cs)) thy =
haftmann@31139:     let
haftmann@31139:       val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
haftmann@31205:     in if has_inst then add_term_of_code tyco raw_vs cs thy else thy end;
haftmann@28228: in
haftmann@35299:   Code.datatype_interpretation ensure_term_of_code
haftmann@28228: end
haftmann@28228: *}
haftmann@28228: 
haftmann@35366: setup {*
haftmann@35366: let
haftmann@35366:   fun mk_term_of_eq thy ty vs tyco abs ty_rep proj =
haftmann@35366:     let
haftmann@35366:       val arg = Var (("x", 0), ty);
haftmann@35366:       val rhs = Abs ("y", @{typ term}, HOLogic.reflect_term (Const (abs, ty_rep --> ty) $ Bound 0)) $
haftmann@35366:         (HOLogic.mk_term_of ty_rep (Const (proj, ty --> ty_rep) $ arg))
haftmann@35366:         |> Thm.cterm_of thy;
haftmann@35366:       val cty = Thm.ctyp_of thy ty;
haftmann@35366:     in
haftmann@35366:       @{thm term_of_anything}
haftmann@35366:       |> Drule.instantiate' [SOME cty] [SOME (Thm.cterm_of thy arg), SOME rhs]
wenzelm@35845:       |> Thm.varifyT_global
haftmann@35366:     end;
haftmann@35366:   fun add_term_of_code tyco raw_vs abs raw_ty_rep proj thy =
haftmann@35366:     let
haftmann@35366:       val algebra = Sign.classes_of thy;
haftmann@35366:       val vs = map (fn (v, sort) =>
haftmann@35366:         (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs;
haftmann@35366:       val ty = Type (tyco, map TFree vs);
haftmann@35366:       val ty_rep = map_atyps
haftmann@35366:         (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_ty_rep;
haftmann@35366:       val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
haftmann@35366:       val eq = mk_term_of_eq thy ty vs tyco abs ty_rep proj;
haftmann@35366:    in
haftmann@35366:       thy
haftmann@35366:       |> Code.del_eqns const
haftmann@35366:       |> Code.add_eqn eq
haftmann@35366:     end;
haftmann@35366:   fun ensure_term_of_code (tyco, (raw_vs, ((abs, ty), (proj, _)))) thy =
haftmann@35366:     let
haftmann@35366:       val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
haftmann@35366:     in if has_inst then add_term_of_code tyco raw_vs abs ty proj thy else thy end;
haftmann@35366: in
haftmann@35366:   Code.abstype_interpretation ensure_term_of_code
haftmann@35366: end
haftmann@35366: *}
haftmann@35366: 
haftmann@28228: 
haftmann@28228: subsubsection {* Code generator setup *}
haftmann@28228: 
haftmann@28562: lemmas [code del] = term.recs term.cases term.size
haftmann@28562: lemma [code, code del]: "eq_class.eq (t1\<Colon>term) t2 \<longleftrightarrow> eq_class.eq t1 t2" ..
haftmann@28228: 
haftmann@28562: lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
haftmann@28562: lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
haftmann@31205: lemma [code, code del]: "(term_of \<Colon> String.literal \<Rightarrow> term) = term_of" ..
haftmann@30427: lemma [code, code del]:
haftmann@32657:   "(Code_Evaluation.term_of \<Colon> 'a::{type, term_of} Predicate.pred \<Rightarrow> Code_Evaluation.term) = Code_Evaluation.term_of" ..
haftmann@30427: lemma [code, code del]:
haftmann@32657:   "(Code_Evaluation.term_of \<Colon> 'a::{type, term_of} Predicate.seq \<Rightarrow> Code_Evaluation.term) = Code_Evaluation.term_of" ..
haftmann@28228: 
haftmann@32657: lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]: "Code_Evaluation.term_of c =
haftmann@28243:     (let (n, m) = nibble_pair_of_char c
haftmann@32657:   in Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.Const (STR ''String.char.Char'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
haftmann@32657:     (Code_Evaluation.term_of n)) (Code_Evaluation.term_of m))"
haftmann@28243:   by (subst term_of_anything) rule 
haftmann@28243: 
haftmann@28228: code_type "term"
haftmann@31031:   (Eval "Term.term")
haftmann@28228: 
haftmann@28228: code_const Const and App
haftmann@31594:   (Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))")
haftmann@28228: 
haftmann@31205: code_const "term_of \<Colon> String.literal \<Rightarrow> term"
haftmann@33632:   (Eval "HOLogic.mk'_literal")
haftmann@31048: 
haftmann@31048: code_reserved Eval HOLogic
haftmann@28228: 
haftmann@28228: 
haftmann@31178: subsubsection {* Syntax *}
haftmann@31178: 
haftmann@31191: definition termify :: "'a \<Rightarrow> term" where
haftmann@31191:   [code del]: "termify x = dummy_term"
haftmann@31191: 
haftmann@31191: abbreviation valtermify :: "'a \<Rightarrow> 'a \<times> (unit \<Rightarrow> term)" where
haftmann@31191:   "valtermify x \<equiv> (x, \<lambda>u. termify x)"
haftmann@31178: 
haftmann@31178: setup {*
haftmann@31178: let
haftmann@31178:   fun map_default f xs =
haftmann@31178:     let val ys = map f xs
haftmann@31178:     in if exists is_some ys
haftmann@31178:       then SOME (map2 the_default xs ys)
haftmann@31178:       else NONE
haftmann@31178:     end;
haftmann@31178:   fun subst_termify_app (Const (@{const_name termify}, T), [t]) =
haftmann@31178:         if not (Term.has_abs t)
haftmann@31178:         then if fold_aterms (fn Const _ => I | _ => K false) t true
haftmann@31191:           then SOME (HOLogic.reflect_term t)
haftmann@31178:           else error "Cannot termify expression containing variables"
haftmann@31178:         else error "Cannot termify expression containing abstraction"
haftmann@31178:     | subst_termify_app (t, ts) = case map_default subst_termify ts
haftmann@31178:        of SOME ts' => SOME (list_comb (t, ts'))
haftmann@31178:         | NONE => NONE
haftmann@31178:   and subst_termify (Abs (v, T, t)) = (case subst_termify t
haftmann@31178:        of SOME t' => SOME (Abs (v, T, t'))
haftmann@31178:         | NONE => NONE)
haftmann@31178:     | subst_termify t = subst_termify_app (strip_comb t) 
haftmann@31178:   fun check_termify ts ctxt = map_default subst_termify ts
haftmann@31178:     |> Option.map (rpair ctxt)
haftmann@31178: in
haftmann@31178:   Context.theory_map (Syntax.add_term_check 0 "termify" check_termify)
haftmann@31178: end;
haftmann@31178: *}
haftmann@31178: 
haftmann@31178: locale term_syntax
haftmann@31178: begin
haftmann@31178: 
haftmann@31191: notation App (infixl "<\<cdot>>" 70)
haftmann@31191:   and valapp (infixl "{\<cdot>}" 70)
haftmann@31178: 
haftmann@31178: end
haftmann@31178: 
haftmann@31178: interpretation term_syntax .
haftmann@31178: 
haftmann@31191: no_notation App (infixl "<\<cdot>>" 70)
haftmann@31191:   and valapp (infixl "{\<cdot>}" 70)
haftmann@31191: 
haftmann@31191: 
haftmann@31191: subsection {* Numeric types *}
haftmann@31191: 
haftmann@31191: definition term_of_num :: "'a\<Colon>{semiring_div} \<Rightarrow> 'a\<Colon>{semiring_div} \<Rightarrow> term" where
haftmann@31191:   "term_of_num two = (\<lambda>_. dummy_term)"
haftmann@31191: 
haftmann@31191: lemma (in term_syntax) term_of_num_code [code]:
haftmann@31191:   "term_of_num two k = (if k = 0 then termify Int.Pls
haftmann@31191:     else (if k mod two = 0
haftmann@31191:       then termify Int.Bit0 <\<cdot>> term_of_num two (k div two)
haftmann@31191:       else termify Int.Bit1 <\<cdot>> term_of_num two (k div two)))"
haftmann@31191:   by (auto simp add: term_of_anything Const_def App_def term_of_num_def Let_def)
haftmann@31191: 
haftmann@31191: lemma (in term_syntax) term_of_nat_code [code]:
haftmann@31191:   "term_of (n::nat) = termify (number_of :: int \<Rightarrow> nat) <\<cdot>> term_of_num (2::nat) n"
haftmann@31191:   by (simp only: term_of_anything)
haftmann@31191: 
haftmann@31191: lemma (in term_syntax) term_of_int_code [code]:
haftmann@31191:   "term_of (k::int) = (if k = 0 then termify (0 :: int)
haftmann@31191:     else if k > 0 then termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num (2::int) k
haftmann@31191:       else termify (uminus :: int \<Rightarrow> int) <\<cdot>> (termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num (2::int) (- k)))"
haftmann@31191:   by (simp only: term_of_anything)
haftmann@31191: 
haftmann@31205: lemma (in term_syntax) term_of_code_numeral_code [code]:
haftmann@31205:   "term_of (k::code_numeral) = termify (number_of :: int \<Rightarrow> code_numeral) <\<cdot>> term_of_num (2::code_numeral) k"
haftmann@31203:   by (simp only: term_of_anything)
haftmann@31191: 
haftmann@31191: subsection {* Obfuscate *}
haftmann@31178: 
haftmann@31178: print_translation {*
haftmann@31178: let
haftmann@31178:   val term = Const ("<TERM>", dummyT);
haftmann@31178:   fun tr1' [_, _] = term;
haftmann@31178:   fun tr2' [] = term;
haftmann@31178: in
haftmann@31178:   [(@{const_syntax Const}, tr1'),
haftmann@31178:     (@{const_syntax App}, tr1'),
haftmann@31178:     (@{const_syntax dummy_term}, tr2')]
haftmann@31178: end
haftmann@31178: *}
haftmann@31178: 
wenzelm@36176: hide_const dummy_term App valapp
wenzelm@36176: hide_const (open) Const termify valtermify term_of term_of_num
haftmann@31178: 
bulwahn@33473: subsection {* Tracing of generated and evaluated code *}
bulwahn@33473: 
bulwahn@33473: definition tracing :: "String.literal => 'a => 'a"
bulwahn@33473: where
bulwahn@33473:   [code del]: "tracing s x = x"
bulwahn@33473: 
bulwahn@33473: ML {*
bulwahn@33473: structure Code_Evaluation =
bulwahn@33473: struct
bulwahn@33473: 
bulwahn@33473: fun tracing s x = (Output.tracing s; x)
bulwahn@33473: 
bulwahn@33473: end
bulwahn@33473: *}
bulwahn@33473: 
bulwahn@33473: code_const "tracing :: String.literal => 'a => 'a"
bulwahn@33473:   (Eval "Code'_Evaluation.tracing")
bulwahn@33473: 
wenzelm@36176: hide_const (open) tracing
bulwahn@33473: code_reserved Eval Code_Evaluation
haftmann@31178: 
haftmann@28228: subsection {* Evaluation setup *}
haftmann@28228: 
haftmann@28228: ML {*
haftmann@28228: signature EVAL =
haftmann@28228: sig
wenzelm@32740:   val eval_ref: (unit -> term) option Unsynchronized.ref
haftmann@28228:   val eval_term: theory -> term -> term
haftmann@28228: end;
haftmann@28228: 
haftmann@28228: structure Eval : EVAL =
haftmann@28228: struct
haftmann@28228: 
wenzelm@32740: val eval_ref = Unsynchronized.ref (NONE : (unit -> term) option);
haftmann@28228: 
haftmann@28228: fun eval_term thy t =
haftmann@34028:   Code_Eval.eval NONE ("Eval.eval_ref", eval_ref) I thy (HOLogic.mk_term_of (fastype_of t) t) [];
haftmann@28228: 
haftmann@28228: end;
haftmann@28228: *}
haftmann@28228: 
haftmann@28228: setup {*
haftmann@28228:   Value.add_evaluator ("code", Eval.eval_term o ProofContext.theory_of)
haftmann@28228: *}
haftmann@28228: 
haftmann@28228: end




