author | haftmann |
Mon, 20 Sep 2010 15:25:32 +0200 | |
changeset 39565 | f4f87c6e2fad |
parent 39564 | acfd10e38e80 |
child 39567 | 5ee997fbe5cc |
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 |
39564 | 15 |
val put_term: (unit -> term) -> Proof.context -> Proof.context |
16 |
val tracing: string -> 'a -> 'a |
|
17 |
val setup: theory -> theory |
|
18 |
end; |
|
19 |
||
20 |
structure Code_Evaluation : CODE_EVALUATION = |
|
21 |
struct |
|
22 |
||
23 |
(** term_of instances **) |
|
24 |
||
25 |
(* formal definition *) |
|
26 |
||
27 |
fun add_term_of tyco raw_vs thy = |
|
28 |
let |
|
29 |
val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs; |
|
30 |
val ty = Type (tyco, map TFree vs); |
|
31 |
val lhs = Const (@{const_name term_of}, ty --> @{typ term}) |
|
32 |
$ Free ("x", ty); |
|
33 |
val rhs = @{term "undefined :: term"}; |
|
34 |
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); |
|
35 |
fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst |
|
36 |
o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv"; |
|
37 |
in |
|
38 |
thy |
|
39 |
|> Class.instantiation ([tyco], vs, @{sort term_of}) |
|
40 |
|> `(fn lthy => Syntax.check_term lthy eq) |
|
41 |
|-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq))) |
|
42 |
|> snd |
|
43 |
|> Class.prove_instantiation_exit (K (Class.intro_classes_tac [])) |
|
44 |
end; |
|
45 |
||
46 |
fun ensure_term_of (tyco, (raw_vs, _)) thy = |
|
47 |
let |
|
48 |
val need_inst = not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of}) |
|
49 |
andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep}; |
|
50 |
in if need_inst then add_term_of tyco raw_vs thy else thy end; |
|
51 |
||
52 |
||
53 |
(* code equations for datatypes *) |
|
54 |
||
39565
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
55 |
fun mk_term_of_eq thy ty (c, tys) = |
39564 | 56 |
let |
57 |
val t = list_comb (Const (c, tys ---> ty), |
|
58 |
map Free (Name.names Name.context "a" tys)); |
|
59 |
val (arg, rhs) = |
|
60 |
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
|
61 |
(t, (map_aterms (fn t as Free (_, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t) |
39564 | 62 |
val cty = Thm.ctyp_of thy ty; |
63 |
in |
|
64 |
@{thm term_of_anything} |
|
65 |
|> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs] |
|
66 |
|> Thm.varifyT_global |
|
67 |
end; |
|
68 |
||
69 |
fun add_term_of_code tyco raw_vs raw_cs thy = |
|
70 |
let |
|
71 |
val algebra = Sign.classes_of thy; |
|
72 |
val vs = map (fn (v, sort) => |
|
73 |
(v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs; |
|
74 |
val ty = Type (tyco, map TFree vs); |
|
75 |
val cs = (map o apsnd o map o map_atyps) |
|
76 |
(fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs; |
|
77 |
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
|
78 |
val eqs = map (mk_term_of_eq thy ty) cs; |
39564 | 79 |
in |
80 |
thy |
|
81 |
|> Code.del_eqns const |
|
82 |
|> fold Code.add_eqn eqs |
|
83 |
end; |
|
84 |
||
85 |
fun ensure_term_of_code (tyco, (raw_vs, cs)) thy = |
|
86 |
let |
|
87 |
val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of}; |
|
88 |
in if has_inst then add_term_of_code tyco raw_vs cs thy else thy end; |
|
89 |
||
90 |
||
91 |
(* code equations for abstypes *) |
|
92 |
||
39565
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
93 |
fun mk_abs_term_of_eq thy ty abs ty_rep proj = |
39564 | 94 |
let |
95 |
val arg = Var (("x", 0), ty); |
|
96 |
val rhs = Abs ("y", @{typ term}, HOLogic.reflect_term (Const (abs, ty_rep --> ty) $ Bound 0)) $ |
|
97 |
(HOLogic.mk_term_of ty_rep (Const (proj, ty --> ty_rep) $ arg)) |
|
98 |
|> Thm.cterm_of thy; |
|
99 |
val cty = Thm.ctyp_of thy ty; |
|
100 |
in |
|
101 |
@{thm term_of_anything} |
|
102 |
|> Drule.instantiate' [SOME cty] [SOME (Thm.cterm_of thy arg), SOME rhs] |
|
103 |
|> Thm.varifyT_global |
|
104 |
end; |
|
105 |
||
106 |
fun add_abs_term_of_code tyco raw_vs abs raw_ty_rep proj thy = |
|
107 |
let |
|
108 |
val algebra = Sign.classes_of thy; |
|
109 |
val vs = map (fn (v, sort) => |
|
110 |
(v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs; |
|
111 |
val ty = Type (tyco, map TFree vs); |
|
112 |
val ty_rep = map_atyps |
|
113 |
(fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_ty_rep; |
|
114 |
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
|
115 |
val eq = mk_abs_term_of_eq thy ty abs ty_rep proj; |
39564 | 116 |
in |
117 |
thy |
|
118 |
|> Code.del_eqns const |
|
119 |
|> Code.add_eqn eq |
|
120 |
end; |
|
121 |
||
122 |
fun ensure_abs_term_of_code (tyco, (raw_vs, ((abs, ty), (proj, _)))) thy = |
|
123 |
let |
|
124 |
val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of}; |
|
125 |
in if has_inst then add_abs_term_of_code tyco raw_vs abs ty proj thy else thy end; |
|
126 |
||
127 |
||
128 |
(** termifying syntax **) |
|
129 |
||
130 |
fun map_default f xs = |
|
131 |
let val ys = map f xs |
|
132 |
in if exists is_some ys |
|
133 |
then SOME (map2 the_default xs ys) |
|
134 |
else NONE |
|
135 |
end; |
|
136 |
||
39565
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
137 |
fun subst_termify_app (Const (@{const_name termify}, _), [t]) = |
39564 | 138 |
if not (Term.has_abs t) |
139 |
then if fold_aterms (fn Const _ => I | _ => K false) t true |
|
140 |
then SOME (HOLogic.reflect_term t) |
|
141 |
else error "Cannot termify expression containing variables" |
|
142 |
else error "Cannot termify expression containing abstraction" |
|
143 |
| subst_termify_app (t, ts) = case map_default subst_termify ts |
|
144 |
of SOME ts' => SOME (list_comb (t, ts')) |
|
145 |
| NONE => NONE |
|
146 |
and subst_termify (Abs (v, T, t)) = (case subst_termify t |
|
147 |
of SOME t' => SOME (Abs (v, T, t')) |
|
148 |
| NONE => NONE) |
|
149 |
| subst_termify t = subst_termify_app (strip_comb t) |
|
150 |
||
151 |
fun check_termify ts ctxt = map_default subst_termify ts |
|
152 |
|> Option.map (rpair ctxt) |
|
153 |
||
154 |
||
155 |
(** evaluation **) |
|
156 |
||
157 |
structure Evaluation = Proof_Data ( |
|
158 |
type T = unit -> term |
|
159 |
fun init _ () = error "Evaluation" |
|
160 |
); |
|
161 |
val put_term = Evaluation.put; |
|
39565
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
162 |
val cookie = (Evaluation.get, put_term, "Code_Evaluation.put_term"); |
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
163 |
|
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
164 |
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
|
165 |
|
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
166 |
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
|
167 |
|
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
168 |
fun gen_dynamic_value dynamic_value thy t = |
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
169 |
dynamic_value cookie thy NONE I (mk_term_of t) []; |
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
170 |
|
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
171 |
val dynamic_value = gen_dynamic_value Code_Runtime.dynamic_value; |
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
172 |
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
|
173 |
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
|
174 |
|
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
175 |
fun gen_static_value static_value thy consts Ts = |
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
176 |
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
|
177 |
o mk_term_of; |
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 |
val static_value = gen_static_value Code_Runtime.static_value; |
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
180 |
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
|
181 |
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
|
182 |
|
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
183 |
|
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
184 |
(** diagnostic **) |
39564 | 185 |
|
186 |
fun tracing s x = (Output.tracing s; x); |
|
187 |
||
188 |
||
189 |
(** setup **) |
|
190 |
||
191 |
val setup = |
|
192 |
Code.datatype_interpretation ensure_term_of |
|
193 |
#> Code.abstype_interpretation ensure_term_of |
|
194 |
#> Code.datatype_interpretation ensure_term_of_code |
|
195 |
#> Code.abstype_interpretation ensure_abs_term_of_code |
|
196 |
#> Context.theory_map (Syntax.add_term_check 0 "termify" check_termify) |
|
197 |
#> Value.add_evaluator ("code", dynamic_value_strict o ProofContext.theory_of); |
|
198 |
||
199 |
end; |