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 \ 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: haftmann@28228: code_datatype Const App 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@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 \ 'a \ '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 \ 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\term) t2 \ eq_class.eq t1 t2" .. haftmann@28228: haftmann@28562: lemma [code, code del]: "(term_of \ typerep \ term) = term_of" .. haftmann@28562: lemma [code, code del]: "(term_of \ term \ term) = term_of" .. haftmann@31205: lemma [code, code del]: "(term_of \ String.literal \ term) = term_of" .. haftmann@30427: lemma [code, code del]: haftmann@32657: "(Code_Evaluation.term_of \ 'a::{type, term_of} Predicate.pred \ Code_Evaluation.term) = Code_Evaluation.term_of" .. haftmann@30427: lemma [code, code del]: haftmann@32657: "(Code_Evaluation.term_of \ 'a::{type, term_of} Predicate.seq \ 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 \ nibble \ 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 \ String.literal \ 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 \ 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: 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 "<\>" 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@31191: subsection {* Numeric types *} haftmann@31191: haftmann@31191: definition term_of_num :: "'a\{semiring_div} \ 'a\{semiring_div} \ term" where haftmann@31191: "term_of_num two = (\_. 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 <\> term_of_num two (k div two) haftmann@31191: else termify Int.Bit1 <\> 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 \ nat) <\> 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 \ int) <\> term_of_num (2::int) k haftmann@31191: else termify (uminus :: int \ int) <\> (termify (number_of :: int \ int) <\> 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 \ code_numeral) <\> 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 ("", 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