author | hoelzl |
Wed, 23 Feb 2011 11:33:45 +0100 | |
changeset 41830 | 719b0a517c33 |
parent 41472 | f6ab14e61604 |
child 42361 | 23f352990944 |
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 |
|
39565
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
9 |
val dynamic_value: theory -> term -> term option |
39564 | 10 |
val dynamic_value_strict: theory -> term -> term |
39565
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
11 |
val dynamic_value_exn: theory -> term -> term Exn.result |
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
12 |
val static_value: theory -> string list -> typ list -> term -> term option |
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
13 |
val static_value_strict: theory -> string list -> typ list -> term -> term |
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
14 |
val static_value_exn: theory -> string list -> typ list -> term -> term Exn.result |
41247 | 15 |
val dynamic_conv: theory -> conv |
41184 | 16 |
val static_conv: theory -> string list -> typ list -> 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 |
|
50 |
val need_inst = not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of}) |
|
51 |
andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep}; |
|
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), |
|
60 |
map Free (Name.names Name.context "a" tys)); |
|
61 |
val (arg, rhs) = |
|
62 |
pairself (Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global) |
|
39565
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
63 |
(t, (map_aterms (fn t as Free (_, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t) |
39564 | 64 |
val cty = Thm.ctyp_of thy ty; |
65 |
in |
|
66 |
@{thm term_of_anything} |
|
67 |
|> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs] |
|
68 |
|> Thm.varifyT_global |
|
69 |
end; |
|
70 |
||
71 |
fun add_term_of_code tyco raw_vs raw_cs thy = |
|
72 |
let |
|
73 |
val algebra = Sign.classes_of thy; |
|
74 |
val vs = map (fn (v, sort) => |
|
75 |
(v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs; |
|
76 |
val ty = Type (tyco, map TFree vs); |
|
40726
16dcfedc4eb7
keep type variable arguments of datatype constructors in bookkeeping
haftmann
parents:
39567
diff
changeset
|
77 |
val cs = (map o apsnd o apsnd o map o map_atyps) |
39564 | 78 |
(fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs; |
79 |
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
|
80 |
val eqs = map (mk_term_of_eq thy ty) cs; |
39564 | 81 |
in |
82 |
thy |
|
83 |
|> Code.del_eqns const |
|
84 |
|> fold Code.add_eqn eqs |
|
85 |
end; |
|
86 |
||
87 |
fun ensure_term_of_code (tyco, (raw_vs, cs)) thy = |
|
88 |
let |
|
89 |
val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of}; |
|
90 |
in if has_inst then add_term_of_code tyco raw_vs cs thy else thy end; |
|
91 |
||
92 |
||
93 |
(* code equations for abstypes *) |
|
94 |
||
39565
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
95 |
fun mk_abs_term_of_eq thy ty abs ty_rep proj = |
39564 | 96 |
let |
97 |
val arg = Var (("x", 0), ty); |
|
98 |
val rhs = Abs ("y", @{typ term}, HOLogic.reflect_term (Const (abs, ty_rep --> ty) $ Bound 0)) $ |
|
99 |
(HOLogic.mk_term_of ty_rep (Const (proj, ty --> ty_rep) $ arg)) |
|
100 |
|> Thm.cterm_of thy; |
|
101 |
val cty = Thm.ctyp_of thy ty; |
|
102 |
in |
|
103 |
@{thm term_of_anything} |
|
104 |
|> Drule.instantiate' [SOME cty] [SOME (Thm.cterm_of thy arg), SOME rhs] |
|
105 |
|> Thm.varifyT_global |
|
106 |
end; |
|
107 |
||
108 |
fun add_abs_term_of_code tyco raw_vs abs raw_ty_rep proj thy = |
|
109 |
let |
|
110 |
val algebra = Sign.classes_of thy; |
|
111 |
val vs = map (fn (v, sort) => |
|
112 |
(v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs; |
|
113 |
val ty = Type (tyco, map TFree vs); |
|
114 |
val ty_rep = map_atyps |
|
115 |
(fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_ty_rep; |
|
116 |
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
|
117 |
val eq = mk_abs_term_of_eq thy ty abs ty_rep proj; |
39564 | 118 |
in |
119 |
thy |
|
120 |
|> Code.del_eqns const |
|
121 |
|> Code.add_eqn eq |
|
122 |
end; |
|
123 |
||
40726
16dcfedc4eb7
keep type variable arguments of datatype constructors in bookkeeping
haftmann
parents:
39567
diff
changeset
|
124 |
fun ensure_abs_term_of_code (tyco, (raw_vs, ((abs, (_, ty)), (proj, _)))) thy = |
39564 | 125 |
let |
126 |
val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of}; |
|
127 |
in if has_inst then add_abs_term_of_code tyco raw_vs abs ty proj thy else thy end; |
|
128 |
||
129 |
||
130 |
(** termifying syntax **) |
|
131 |
||
132 |
fun map_default f xs = |
|
133 |
let val ys = map f xs |
|
134 |
in if exists is_some ys |
|
135 |
then SOME (map2 the_default xs ys) |
|
136 |
else NONE |
|
137 |
end; |
|
138 |
||
39565
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
139 |
fun subst_termify_app (Const (@{const_name termify}, _), [t]) = |
39564 | 140 |
if not (Term.has_abs t) |
141 |
then if fold_aterms (fn Const _ => I | _ => K false) t true |
|
142 |
then SOME (HOLogic.reflect_term t) |
|
143 |
else error "Cannot termify expression containing variables" |
|
144 |
else error "Cannot termify expression containing abstraction" |
|
145 |
| subst_termify_app (t, ts) = case map_default subst_termify ts |
|
146 |
of SOME ts' => SOME (list_comb (t, ts')) |
|
147 |
| NONE => NONE |
|
148 |
and subst_termify (Abs (v, T, t)) = (case subst_termify t |
|
149 |
of SOME t' => SOME (Abs (v, T, t')) |
|
150 |
| NONE => NONE) |
|
151 |
| subst_termify t = subst_termify_app (strip_comb t) |
|
152 |
||
153 |
fun check_termify ts ctxt = map_default subst_termify ts |
|
154 |
|> Option.map (rpair ctxt) |
|
155 |
||
156 |
||
157 |
(** evaluation **) |
|
158 |
||
41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41247
diff
changeset
|
159 |
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
|
160 |
( |
39564 | 161 |
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
|
162 |
(* FIXME avoid user error with non-user text *) |
39564 | 163 |
fun init _ () = error "Evaluation" |
164 |
); |
|
165 |
val put_term = Evaluation.put; |
|
39565
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
166 |
val cookie = (Evaluation.get, put_term, "Code_Evaluation.put_term"); |
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
167 |
|
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
168 |
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
|
169 |
|
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
170 |
fun term_of_const_for thy = AxClass.unoverload_const thy o dest_Const o HOLogic.term_of_const; |
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
171 |
|
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
172 |
fun gen_dynamic_value dynamic_value thy t = |
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
173 |
dynamic_value cookie thy NONE I (mk_term_of t) []; |
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
174 |
|
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
175 |
val dynamic_value = gen_dynamic_value Code_Runtime.dynamic_value; |
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
176 |
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
|
177 |
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
|
178 |
|
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
179 |
fun gen_static_value static_value thy consts Ts = |
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
180 |
static_value cookie thy NONE I (union (op =) (map (term_of_const_for thy) Ts) consts) |
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
181 |
o mk_term_of; |
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
182 |
|
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
183 |
val static_value = gen_static_value Code_Runtime.static_value; |
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
184 |
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
|
185 |
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
|
186 |
|
39567
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39565
diff
changeset
|
187 |
fun certify_eval thy value conv ct = |
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39565
diff
changeset
|
188 |
let |
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39565
diff
changeset
|
189 |
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
|
190 |
val T = fastype_of t; |
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39565
diff
changeset
|
191 |
val mk_eq = Thm.mk_binop (Thm.cterm_of thy (Const ("==", T --> T --> propT))); |
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39565
diff
changeset
|
192 |
in case value t |
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39565
diff
changeset
|
193 |
of NONE => Thm.reflexive ct |
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39565
diff
changeset
|
194 |
| SOME t' => conv (mk_eq ct (Thm.cterm_of thy t')) RS @{thm eq_eq_TrueD} |
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39565
diff
changeset
|
195 |
handle THM _ => |
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39565
diff
changeset
|
196 |
error ("Failed to certify evaluation result of " ^ Syntax.string_of_term_global thy t) |
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39565
diff
changeset
|
197 |
end; |
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39565
diff
changeset
|
198 |
|
41247 | 199 |
fun dynamic_conv thy = certify_eval thy (dynamic_value thy) |
200 |
(Code_Runtime.dynamic_holds_conv thy); |
|
39567
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39565
diff
changeset
|
201 |
|
41184 | 202 |
fun static_conv thy consts Ts = |
39567
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39565
diff
changeset
|
203 |
let |
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39565
diff
changeset
|
204 |
val eqs = "==" :: @{const_name HOL.eq} :: |
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39565
diff
changeset
|
205 |
map (fn T => AxClass.unoverload_const thy (@{const_name HOL.equal}, T)) Ts; |
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39565
diff
changeset
|
206 |
(*assumes particular code equations for "==" etc.*) |
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39565
diff
changeset
|
207 |
in |
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39565
diff
changeset
|
208 |
certify_eval thy (static_value thy consts Ts) |
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39565
diff
changeset
|
209 |
(Code_Runtime.static_holds_conv thy (union (op =) eqs consts)) |
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39565
diff
changeset
|
210 |
end; |
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39565
diff
changeset
|
211 |
|
39565
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
212 |
|
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
213 |
(** diagnostic **) |
39564 | 214 |
|
215 |
fun tracing s x = (Output.tracing s; x); |
|
216 |
||
217 |
||
218 |
(** setup **) |
|
219 |
||
220 |
val setup = |
|
221 |
Code.datatype_interpretation ensure_term_of |
|
222 |
#> Code.abstype_interpretation ensure_term_of |
|
223 |
#> Code.datatype_interpretation ensure_term_of_code |
|
224 |
#> Code.abstype_interpretation ensure_abs_term_of_code |
|
225 |
#> Context.theory_map (Syntax.add_term_check 0 "termify" check_termify) |
|
226 |
#> Value.add_evaluator ("code", dynamic_value_strict o ProofContext.theory_of); |
|
227 |
||
228 |
end; |