1 (* Title: HOL/Library/Eval.thy
3 Author: Florian Haftmann, TU Muenchen
6 header {* A simple term evaluation mechanism *}
12 subsection {* @{text typ_of} class *}
15 fixes typ_of :: "'a\<Colon>{} itself \<Rightarrow> typ"
21 val class_typ_of = Sign.intern_class @{theory} "typ_of";
23 fun term_typ_of_type ty =
24 Const (@{const_name typ_of}, Term.itselfT ty --> @{typ typ})
27 fun mk_typ_of_def ty =
29 val lhs = Const (@{const_name typ_of}, Term.itselfT ty --> @{typ typ})
30 $ Free ("x", Term.itselfT ty)
31 val rhs = Pure_term.mk_typ (fn v => term_typ_of_type (TFree v)) ty
32 in Logic.mk_equals (lhs, rhs) end;
37 instance "prop" :: typ_of
38 "typ_of T \<equiv> STR ''prop'' {\<struct>} []" ..
40 instance itself :: (typ_of) typ_of
41 "typ_of T \<equiv> STR ''itself'' {\<struct>} [typ_of TYPE('a\<Colon>typ_of)]" ..
43 instance set :: (typ_of) typ_of
44 "typ_of T \<equiv> STR ''set'' {\<struct>} [typ_of TYPE('a\<Colon>typ_of)]" ..
46 instance int :: typ_of
47 "typ_of T \<equiv> STR ''IntDef.int'' {\<struct>} []" ..
51 fun mk arities _ thy =
52 (maps (fn (tyco, asorts, _) => [(("", []), TypOf.mk_typ_of_def
54 map TFree (Name.names Name.context "'a" asorts))))]) arities, thy);
56 DatatypeCodegen.prove_codetypes_arities (Class.intro_classes_tac [])
57 (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
58 [TypOf.class_typ_of] mk ((K o K) (fold Code.add_default_func))
59 in DatatypeCodegen.add_codetypes_hook hook end
63 subsection {* @{text term_of} class *}
65 class term_of = typ_of +
66 constrains typ_of :: "'a\<Colon>{} itself \<Rightarrow> typ"
67 fixes term_of :: "'a \<Rightarrow> term"
75 Const (@{const_name term_of}, ty --> @{typ term});
77 val class_term_of = Sign.intern_class @{theory} "term_of";
78 fun mk_terms_of_defs vs (tyco, cs) =
80 val dty = Type (tyco, map TFree vs);
83 val lhs : term = term_term_of dty $ c;
84 val rhs : term = Pure_term.mk_term
85 (fn (v, ty) => term_term_of ty $ Free (v, ty))
86 (Pure_term.mk_typ (fn (v, sort) => TypOf.term_typ_of_type (TFree (v, sort)))) c
88 HOLogic.mk_eq (lhs, rhs)
92 term_term_of (Term.fastype_of t) $ t;
100 fun thy_note ((name, atts), thms) =
101 PureThy.add_thmss [((name, thms), atts)] #-> (fn [thms] => pair (name, thms));
102 fun thy_def ((name, atts), t) =
103 PureThy.add_defs_i false [((name, t), atts)] #-> (fn [thm] => pair (name, thm));
104 fun mk arities css _ thy =
106 val (_, asorts, _) :: _ = arities;
107 val vs = Name.names Name.context "'a" asorts;
108 val defs = map (TermOf.mk_terms_of_defs vs) css;
109 val defs' = (map (pair ("", []) o ObjectLogic.ensure_propT thy) o flat) defs;
112 |> PrimrecPackage.gen_primrec thy_note thy_def "" defs'
116 if null specs orelse (fst o hd) specs = (fst o dest_Type) @{typ typ} then I
118 DatatypeCodegen.prove_codetypes_arities (Class.intro_classes_tac [])
119 (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
120 [TermOf.class_term_of] ((K o K o pair) []) mk
121 in DatatypeCodegen.add_codetypes_hook hook end
127 "intT \<equiv> STR ''IntDef.int'' {\<struct>} []"
132 "bitT \<equiv> STR ''Numeral.bit'' {\<struct>} []"
135 mk_int :: "int \<Rightarrow> term"
137 "mk_int k = (if k = 0 then STR ''Numeral.Pls'' \<Colon>\<subseteq> intT
138 else if k = -1 then STR ''Numeral.Min'' \<Colon>\<subseteq> intT
139 else let (l, m) = divAlg (k, 2)
140 in STR ''Numeral.Bit'' \<Colon>\<subseteq> intT \<rightarrow> bitT \<rightarrow> intT \<bullet> mk_int l \<bullet>
141 (if m = 0 then STR ''Numeral.bit.B0'' \<Colon>\<subseteq> bitT else STR ''Numeral.bit.B1'' \<Colon>\<subseteq> bitT))"
142 by pat_completeness auto
143 termination by (relation "measure (nat o abs)") (auto simp add: divAlg_mod_div)
145 instance int :: term_of
146 "term_of k \<equiv> STR ''Numeral.number_class.number_of'' \<Colon>\<subseteq> intT \<rightarrow> intT \<bullet> mk_int k" ..
149 text {* Adaption for @{typ ml_string}s *}
151 lemmas [code func, code func del] = term_of_ml_string_def
154 subsection {* Evaluation infrastructure *}
159 val eval_ref: (unit -> term) option ref
160 val eval_term: theory -> term -> term
161 val evaluate: Proof.context -> term -> unit
162 val evaluate': string -> Proof.context -> term -> unit
163 val evaluate_cmd: string option -> Toplevel.state -> unit
169 val eval_ref = ref (NONE : (unit -> term) option);
171 fun eval_invoke thy code ((_, ty), t) deps _ =
172 CodePackage.eval_invoke thy ("Eval.eval_ref", eval_ref) code (t, ty) [];
176 #> CodePackage.eval_term thy (eval_invoke thy)
177 #> Code.postprocess_term thy;
181 ("SML", Codegen.eval_term),
182 ("normal_form", Nbe.norm_term)
185 fun gen_evaluate evaluators ctxt t =
187 val thy = ProofContext.theory_of ctxt;
188 val (evls, evl) = split_last evaluators;
189 val t' = case get_first (fn f => try (f thy) t) evls
192 val ty' = Term.type_of t';
193 val p = Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t'),
194 Pretty.fbrk, Pretty.str "::", Pretty.brk 1,
195 Pretty.quote (ProofContext.pretty_typ ctxt ty')];
196 in Pretty.writeln p end;
198 val evaluate = gen_evaluate (map snd evaluators);
200 fun evaluate' name = gen_evaluate
201 [(the o AList.lookup (op =) evaluators) name];
203 fun evaluate_cmd some_name raw_t state =
205 val ctxt = Toplevel.context_of state;
206 val t = Syntax.read_term ctxt raw_t;
208 of NONE => evaluate ctxt t
209 | SOME name => evaluate' name ctxt t
216 OuterSyntax.improper_command "value" "read, evaluate and print term" OuterKeyword.diag
217 (Scan.option (OuterParse.$$$ "(" |-- OuterParse.name --| OuterParse.$$$ ")")
219 >> (fn (some_name, t) => Toplevel.no_timing o Toplevel.keep
220 (Eval.evaluate_cmd some_name t)));