author | haftmann |
Fri, 09 May 2014 08:13:36 +0200 | |
changeset 56925 | 601edd9a6859 |
parent 56245 | 84fc7dfa3cd4 |
child 56926 | aaea99edc040 |
permissions | -rw-r--r-- |
39564 | 1 |
(* Title: HOL/Tools/code_evaluation.ML |
2 |
Author: Florian Haftmann, TU Muenchen |
|
3 |
||
4 |
Evaluation and reconstruction of terms in ML. |
|
5 |
*) |
|
6 |
||
7 |
signature CODE_EVALUATION = |
|
8 |
sig |
|
55757 | 9 |
val dynamic_value: Proof.context -> term -> term option |
10 |
val dynamic_value_strict: Proof.context -> term -> term |
|
11 |
val dynamic_value_exn: Proof.context -> term -> term Exn.result |
|
12 |
val static_value: Proof.context -> string list -> typ list -> Proof.context -> term -> term option |
|
13 |
val static_value_strict: Proof.context -> string list -> typ list -> Proof.context -> term -> term |
|
14 |
val static_value_exn: Proof.context -> string list -> typ list -> Proof.context -> term -> term Exn.result |
|
15 |
val dynamic_conv: Proof.context -> conv |
|
16 |
val static_conv: Proof.context -> string list -> typ list -> Proof.context -> conv |
|
39564 | 17 |
val put_term: (unit -> term) -> Proof.context -> Proof.context |
18 |
val tracing: string -> 'a -> 'a |
|
19 |
val setup: theory -> theory |
|
20 |
end; |
|
21 |
||
22 |
structure Code_Evaluation : CODE_EVALUATION = |
|
23 |
struct |
|
24 |
||
25 |
(** term_of instances **) |
|
26 |
||
27 |
(* formal definition *) |
|
28 |
||
29 |
fun add_term_of tyco raw_vs thy = |
|
30 |
let |
|
31 |
val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs; |
|
32 |
val ty = Type (tyco, map TFree vs); |
|
33 |
val lhs = Const (@{const_name term_of}, ty --> @{typ term}) |
|
34 |
$ Free ("x", ty); |
|
35 |
val rhs = @{term "undefined :: term"}; |
|
36 |
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); |
|
37 |
fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst |
|
38 |
o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv"; |
|
39 |
in |
|
40 |
thy |
|
41 |
|> Class.instantiation ([tyco], vs, @{sort term_of}) |
|
42 |
|> `(fn lthy => Syntax.check_term lthy eq) |
|
43 |
|-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq))) |
|
44 |
|> snd |
|
45 |
|> Class.prove_instantiation_exit (K (Class.intro_classes_tac [])) |
|
46 |
end; |
|
47 |
||
48 |
fun ensure_term_of (tyco, (raw_vs, _)) thy = |
|
49 |
let |
|
48272 | 50 |
val need_inst = not (Sorts.has_instance (Sign.classes_of thy) tyco @{sort term_of}) |
51 |
andalso Sorts.has_instance (Sign.classes_of thy) tyco @{sort typerep}; |
|
39564 | 52 |
in if need_inst then add_term_of tyco raw_vs thy else thy end; |
53 |
||
54 |
||
55 |
(* code equations for datatypes *) |
|
56 |
||
40726
16dcfedc4eb7
keep type variable arguments of datatype constructors in bookkeeping
haftmann
parents:
39567
diff
changeset
|
57 |
fun mk_term_of_eq thy ty (c, (_, tys)) = |
39564 | 58 |
let |
59 |
val t = list_comb (Const (c, tys ---> ty), |
|
43329
84472e198515
tuned signature: Name.invent and Name.invent_names;
wenzelm
parents:
42402
diff
changeset
|
60 |
map Free (Name.invent_names Name.context "a" tys)); |
39564 | 61 |
val (arg, rhs) = |
45344
e209da839ff4
added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
wenzelm
parents:
43329
diff
changeset
|
62 |
pairself (Thm.cterm_of thy o Logic.unvarify_types_global o Logic.varify_global) |
e209da839ff4
added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
wenzelm
parents:
43329
diff
changeset
|
63 |
(t, |
e209da839ff4
added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
wenzelm
parents:
43329
diff
changeset
|
64 |
map_aterms (fn t as Free (_, ty) => HOLogic.mk_term_of ty t | t => t) |
e209da839ff4
added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
wenzelm
parents:
43329
diff
changeset
|
65 |
(HOLogic.reflect_term t)); |
39564 | 66 |
val cty = Thm.ctyp_of thy ty; |
67 |
in |
|
68 |
@{thm term_of_anything} |
|
69 |
|> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs] |
|
70 |
|> Thm.varifyT_global |
|
71 |
end; |
|
72 |
||
73 |
fun add_term_of_code tyco raw_vs raw_cs thy = |
|
74 |
let |
|
75 |
val algebra = Sign.classes_of thy; |
|
76 |
val vs = map (fn (v, sort) => |
|
77 |
(v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs; |
|
78 |
val ty = Type (tyco, map TFree vs); |
|
40726
16dcfedc4eb7
keep type variable arguments of datatype constructors in bookkeeping
haftmann
parents:
39567
diff
changeset
|
79 |
val cs = (map o apsnd o apsnd o map o map_atyps) |
39564 | 80 |
(fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs; |
51685
385ef6706252
more standard module name Axclass (according to file name);
wenzelm
parents:
48272
diff
changeset
|
81 |
val const = Axclass.param_of_inst thy (@{const_name term_of}, tyco); |
39565
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
82 |
val eqs = map (mk_term_of_eq thy ty) cs; |
39564 | 83 |
in |
84 |
thy |
|
85 |
|> Code.del_eqns const |
|
86 |
|> fold Code.add_eqn eqs |
|
87 |
end; |
|
88 |
||
89 |
fun ensure_term_of_code (tyco, (raw_vs, cs)) thy = |
|
90 |
let |
|
48272 | 91 |
val has_inst = Sorts.has_instance (Sign.classes_of thy) tyco @{sort term_of}; |
39564 | 92 |
in if has_inst then add_term_of_code tyco raw_vs cs thy else thy end; |
93 |
||
94 |
||
95 |
(* code equations for abstypes *) |
|
96 |
||
39565
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
97 |
fun mk_abs_term_of_eq thy ty abs ty_rep proj = |
39564 | 98 |
let |
99 |
val arg = Var (("x", 0), ty); |
|
100 |
val rhs = Abs ("y", @{typ term}, HOLogic.reflect_term (Const (abs, ty_rep --> ty) $ Bound 0)) $ |
|
101 |
(HOLogic.mk_term_of ty_rep (Const (proj, ty --> ty_rep) $ arg)) |
|
102 |
|> Thm.cterm_of thy; |
|
103 |
val cty = Thm.ctyp_of thy ty; |
|
104 |
in |
|
105 |
@{thm term_of_anything} |
|
106 |
|> Drule.instantiate' [SOME cty] [SOME (Thm.cterm_of thy arg), SOME rhs] |
|
107 |
|> Thm.varifyT_global |
|
108 |
end; |
|
109 |
||
110 |
fun add_abs_term_of_code tyco raw_vs abs raw_ty_rep proj thy = |
|
111 |
let |
|
112 |
val algebra = Sign.classes_of thy; |
|
113 |
val vs = map (fn (v, sort) => |
|
114 |
(v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs; |
|
115 |
val ty = Type (tyco, map TFree vs); |
|
116 |
val ty_rep = map_atyps |
|
117 |
(fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_ty_rep; |
|
51685
385ef6706252
more standard module name Axclass (according to file name);
wenzelm
parents:
48272
diff
changeset
|
118 |
val const = Axclass.param_of_inst thy (@{const_name term_of}, tyco); |
39565
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
119 |
val eq = mk_abs_term_of_eq thy ty abs ty_rep proj; |
39564 | 120 |
in |
121 |
thy |
|
122 |
|> Code.del_eqns const |
|
123 |
|> Code.add_eqn eq |
|
124 |
end; |
|
125 |
||
40726
16dcfedc4eb7
keep type variable arguments of datatype constructors in bookkeeping
haftmann
parents:
39567
diff
changeset
|
126 |
fun ensure_abs_term_of_code (tyco, (raw_vs, ((abs, (_, ty)), (proj, _)))) thy = |
39564 | 127 |
let |
48272 | 128 |
val has_inst = Sorts.has_instance (Sign.classes_of thy) tyco @{sort term_of}; |
39564 | 129 |
in if has_inst then add_abs_term_of_code tyco raw_vs abs ty proj thy else thy end; |
130 |
||
131 |
||
132 |
(** termifying syntax **) |
|
133 |
||
134 |
fun map_default f xs = |
|
135 |
let val ys = map f xs |
|
136 |
in if exists is_some ys |
|
137 |
then SOME (map2 the_default xs ys) |
|
138 |
else NONE |
|
139 |
end; |
|
140 |
||
39565
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
141 |
fun subst_termify_app (Const (@{const_name termify}, _), [t]) = |
39564 | 142 |
if not (Term.has_abs t) |
143 |
then if fold_aterms (fn Const _ => I | _ => K false) t true |
|
144 |
then SOME (HOLogic.reflect_term t) |
|
51714 | 145 |
else error "Cannot termify expression containing variable" |
39564 | 146 |
else error "Cannot termify expression containing abstraction" |
147 |
| subst_termify_app (t, ts) = case map_default subst_termify ts |
|
148 |
of SOME ts' => SOME (list_comb (t, ts')) |
|
149 |
| NONE => NONE |
|
150 |
and subst_termify (Abs (v, T, t)) = (case subst_termify t |
|
151 |
of SOME t' => SOME (Abs (v, T, t')) |
|
152 |
| NONE => NONE) |
|
153 |
| subst_termify t = subst_termify_app (strip_comb t) |
|
154 |
||
42402
c7139609b67d
simplified check/uncheck interfaces: result comparison is hardwired by default;
wenzelm
parents:
42361
diff
changeset
|
155 |
fun check_termify ctxt ts = |
c7139609b67d
simplified check/uncheck interfaces: result comparison is hardwired by default;
wenzelm
parents:
42361
diff
changeset
|
156 |
the_default ts (map_default subst_termify ts); |
39564 | 157 |
|
158 |
||
159 |
(** evaluation **) |
|
160 |
||
41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41247
diff
changeset
|
161 |
structure Evaluation = Proof_Data |
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41247
diff
changeset
|
162 |
( |
39564 | 163 |
type T = unit -> term |
41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41247
diff
changeset
|
164 |
(* FIXME avoid user error with non-user text *) |
39564 | 165 |
fun init _ () = error "Evaluation" |
166 |
); |
|
167 |
val put_term = Evaluation.put; |
|
39565
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
168 |
val cookie = (Evaluation.get, put_term, "Code_Evaluation.put_term"); |
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
169 |
|
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
170 |
fun mk_term_of t = HOLogic.mk_term_of (fastype_of t) t; |
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
171 |
|
51685
385ef6706252
more standard module name Axclass (according to file name);
wenzelm
parents:
48272
diff
changeset
|
172 |
fun term_of_const_for thy = Axclass.unoverload_const thy o dest_Const o HOLogic.term_of_const; |
39565
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
173 |
|
55757 | 174 |
fun gen_dynamic_value dynamic_value ctxt t = |
175 |
dynamic_value cookie ctxt NONE I (mk_term_of t) []; |
|
39565
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
176 |
|
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
177 |
val dynamic_value = gen_dynamic_value Code_Runtime.dynamic_value; |
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
178 |
val dynamic_value_strict = gen_dynamic_value Code_Runtime.dynamic_value_strict; |
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
179 |
val dynamic_value_exn = gen_dynamic_value Code_Runtime.dynamic_value_exn; |
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
180 |
|
55757 | 181 |
fun gen_static_value static_value ctxt consts Ts = |
182 |
let |
|
183 |
val static_value' = static_value cookie ctxt NONE I |
|
184 |
(union (op =) (map (term_of_const_for (Proof_Context.theory_of ctxt)) Ts) consts) |
|
185 |
in fn ctxt' => fn t => static_value' ctxt' (mk_term_of t) end; |
|
39565
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
186 |
|
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
187 |
val static_value = gen_static_value Code_Runtime.static_value; |
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
188 |
val static_value_strict = gen_static_value Code_Runtime.static_value_strict; |
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
189 |
val static_value_exn = gen_static_value Code_Runtime.static_value_exn; |
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
190 |
|
55757 | 191 |
fun certify_eval ctxt value conv ct = |
39567
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39565
diff
changeset
|
192 |
let |
55757 | 193 |
val cert = Thm.cterm_of (Proof_Context.theory_of ctxt); |
39567
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39565
diff
changeset
|
194 |
val t = Thm.term_of ct; |
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39565
diff
changeset
|
195 |
val T = fastype_of t; |
56245 | 196 |
val mk_eq = Thm.mk_binop (cert (Const (@{const_name Pure.eq}, T --> T --> propT))); |
55757 | 197 |
in case value ctxt t |
39567
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39565
diff
changeset
|
198 |
of NONE => Thm.reflexive ct |
55757 | 199 |
| SOME t' => conv ctxt (mk_eq ct (cert t')) RS @{thm eq_eq_TrueD} |
39567
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39565
diff
changeset
|
200 |
handle THM _ => |
55757 | 201 |
error ("Failed to certify evaluation result of " ^ Syntax.string_of_term ctxt t) |
39567
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39565
diff
changeset
|
202 |
end; |
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39565
diff
changeset
|
203 |
|
55757 | 204 |
fun dynamic_conv ctxt = certify_eval ctxt dynamic_value |
205 |
Code_Runtime.dynamic_holds_conv; |
|
39567
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39565
diff
changeset
|
206 |
|
55757 | 207 |
fun static_conv ctxt consts Ts = |
39567
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39565
diff
changeset
|
208 |
let |
56245 | 209 |
val eqs = @{const_name Pure.eq} :: @{const_name HOL.eq} :: |
55757 | 210 |
map (fn T => Axclass.unoverload_const (Proof_Context.theory_of ctxt) |
56245 | 211 |
(@{const_name HOL.equal}, T)) Ts; (*assumes particular code equations for Pure.eq etc.*) |
55757 | 212 |
val value = static_value ctxt consts Ts; |
213 |
val holds = Code_Runtime.static_holds_conv ctxt (union (op =) eqs consts); |
|
39567
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39565
diff
changeset
|
214 |
in |
55757 | 215 |
fn ctxt' => certify_eval ctxt' value holds |
39567
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39565
diff
changeset
|
216 |
end; |
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39565
diff
changeset
|
217 |
|
39565
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
218 |
|
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
219 |
(** diagnostic **) |
39564 | 220 |
|
221 |
fun tracing s x = (Output.tracing s; x); |
|
222 |
||
223 |
||
224 |
(** setup **) |
|
225 |
||
226 |
val setup = |
|
227 |
Code.datatype_interpretation ensure_term_of |
|
228 |
#> Code.abstype_interpretation ensure_term_of |
|
229 |
#> Code.datatype_interpretation ensure_term_of_code |
|
230 |
#> Code.abstype_interpretation ensure_abs_term_of_code |
|
56925 | 231 |
#> Context.theory_map (Syntax_Phases.term_check 0 "termify" check_termify); |
39564 | 232 |
|
233 |
end; |