author | haftmann |
Sun, 02 Jul 2017 20:13:38 +0200 | |
changeset 66251 | cd935b7cb3fb |
parent 65062 | dc746d43f40e |
child 66310 | e8d2862ec203 |
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 |
|
39564 | 12 |
val put_term: (unit -> term) -> Proof.context -> Proof.context |
13 |
val tracing: string -> 'a -> 'a |
|
14 |
end; |
|
15 |
||
16 |
structure Code_Evaluation : CODE_EVALUATION = |
|
17 |
struct |
|
18 |
||
19 |
(** term_of instances **) |
|
20 |
||
21 |
(* formal definition *) |
|
22 |
||
23 |
fun add_term_of tyco raw_vs thy = |
|
24 |
let |
|
25 |
val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs; |
|
26 |
val ty = Type (tyco, map TFree vs); |
|
27 |
val lhs = Const (@{const_name term_of}, ty --> @{typ term}) |
|
28 |
$ Free ("x", ty); |
|
29 |
val rhs = @{term "undefined :: term"}; |
|
30 |
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); |
|
31 |
fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst |
|
32 |
o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv"; |
|
33 |
in |
|
34 |
thy |
|
35 |
|> Class.instantiation ([tyco], vs, @{sort term_of}) |
|
36 |
|> `(fn lthy => Syntax.check_term lthy eq) |
|
63180 | 37 |
|-> (fn eq => Specification.definition NONE [] [] ((Binding.name (triv_name_of eq), []), eq)) |
39564 | 38 |
|> snd |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59323
diff
changeset
|
39 |
|> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt []) |
39564 | 40 |
end; |
41 |
||
61667
4b53042d7a40
explicit computation of sort arguments for code equations makes less assumption about sort arguments of underlying type class instances
haftmann
parents:
60801
diff
changeset
|
42 |
fun ensure_term_of (tyco, (vs, _)) thy = |
39564 | 43 |
let |
48272 | 44 |
val need_inst = not (Sorts.has_instance (Sign.classes_of thy) tyco @{sort term_of}) |
45 |
andalso Sorts.has_instance (Sign.classes_of thy) tyco @{sort typerep}; |
|
61667
4b53042d7a40
explicit computation of sort arguments for code equations makes less assumption about sort arguments of underlying type class instances
haftmann
parents:
60801
diff
changeset
|
46 |
in if need_inst then add_term_of tyco vs thy else thy end; |
4b53042d7a40
explicit computation of sort arguments for code equations makes less assumption about sort arguments of underlying type class instances
haftmann
parents:
60801
diff
changeset
|
47 |
|
4b53042d7a40
explicit computation of sort arguments for code equations makes less assumption about sort arguments of underlying type class instances
haftmann
parents:
60801
diff
changeset
|
48 |
fun for_term_of_instance tyco vs f thy = |
4b53042d7a40
explicit computation of sort arguments for code equations makes less assumption about sort arguments of underlying type class instances
haftmann
parents:
60801
diff
changeset
|
49 |
let |
4b53042d7a40
explicit computation of sort arguments for code equations makes less assumption about sort arguments of underlying type class instances
haftmann
parents:
60801
diff
changeset
|
50 |
val algebra = Sign.classes_of thy; |
4b53042d7a40
explicit computation of sort arguments for code equations makes less assumption about sort arguments of underlying type class instances
haftmann
parents:
60801
diff
changeset
|
51 |
in |
4b53042d7a40
explicit computation of sort arguments for code equations makes less assumption about sort arguments of underlying type class instances
haftmann
parents:
60801
diff
changeset
|
52 |
case try (Sorts.mg_domain algebra tyco) @{sort term_of} of |
4b53042d7a40
explicit computation of sort arguments for code equations makes less assumption about sort arguments of underlying type class instances
haftmann
parents:
60801
diff
changeset
|
53 |
NONE => thy |
4b53042d7a40
explicit computation of sort arguments for code equations makes less assumption about sort arguments of underlying type class instances
haftmann
parents:
60801
diff
changeset
|
54 |
| SOME sorts => f tyco (map2 (fn (v, sort) => fn sort' => |
4b53042d7a40
explicit computation of sort arguments for code equations makes less assumption about sort arguments of underlying type class instances
haftmann
parents:
60801
diff
changeset
|
55 |
(v, Sorts.inter_sort algebra (sort, sort'))) vs sorts) thy |
4b53042d7a40
explicit computation of sort arguments for code equations makes less assumption about sort arguments of underlying type class instances
haftmann
parents:
60801
diff
changeset
|
56 |
end; |
39564 | 57 |
|
58 |
||
59 |
(* code equations for datatypes *) |
|
60 |
||
40726
16dcfedc4eb7
keep type variable arguments of datatype constructors in bookkeeping
haftmann
parents:
39567
diff
changeset
|
61 |
fun mk_term_of_eq thy ty (c, (_, tys)) = |
39564 | 62 |
let |
63 |
val t = list_comb (Const (c, tys ---> ty), |
|
43329
84472e198515
tuned signature: Name.invent and Name.invent_names;
wenzelm
parents:
42402
diff
changeset
|
64 |
map Free (Name.invent_names Name.context "a" tys)); |
39564 | 65 |
val (arg, rhs) = |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59617
diff
changeset
|
66 |
apply2 (Thm.global_cterm_of thy o Logic.unvarify_types_global o Logic.varify_global) |
45344
e209da839ff4
added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
wenzelm
parents:
43329
diff
changeset
|
67 |
(t, |
e209da839ff4
added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
wenzelm
parents:
43329
diff
changeset
|
68 |
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
|
69 |
(HOLogic.reflect_term t)); |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59617
diff
changeset
|
70 |
val cty = Thm.global_ctyp_of thy ty; |
39564 | 71 |
in |
72 |
@{thm term_of_anything} |
|
60801 | 73 |
|> Thm.instantiate' [SOME cty] [SOME arg, SOME rhs] |
39564 | 74 |
|> Thm.varifyT_global |
75 |
end; |
|
76 |
||
61667
4b53042d7a40
explicit computation of sort arguments for code equations makes less assumption about sort arguments of underlying type class instances
haftmann
parents:
60801
diff
changeset
|
77 |
fun add_term_of_code tyco vs raw_cs thy = |
39564 | 78 |
let |
79 |
val ty = Type (tyco, map TFree vs); |
|
40726
16dcfedc4eb7
keep type variable arguments of datatype constructors in bookkeeping
haftmann
parents:
39567
diff
changeset
|
80 |
val cs = (map o apsnd o apsnd o map o map_atyps) |
39564 | 81 |
(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
|
82 |
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
|
83 |
val eqs = map (mk_term_of_eq thy ty) cs; |
39564 | 84 |
in |
85 |
thy |
|
66251
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
65062
diff
changeset
|
86 |
|> Code.declare_default_eqns_global (map (rpair true) eqs) |
39564 | 87 |
end; |
88 |
||
61667
4b53042d7a40
explicit computation of sort arguments for code equations makes less assumption about sort arguments of underlying type class instances
haftmann
parents:
60801
diff
changeset
|
89 |
fun ensure_term_of_code (tyco, (vs, cs)) = |
4b53042d7a40
explicit computation of sort arguments for code equations makes less assumption about sort arguments of underlying type class instances
haftmann
parents:
60801
diff
changeset
|
90 |
for_term_of_instance tyco vs (fn tyco => fn vs => add_term_of_code tyco vs cs); |
39564 | 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)) |
|
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59617
diff
changeset
|
100 |
|> Thm.global_cterm_of thy; |
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59617
diff
changeset
|
101 |
val cty = Thm.global_ctyp_of thy ty; |
39564 | 102 |
in |
103 |
@{thm term_of_anything} |
|
60801 | 104 |
|> Thm.instantiate' [SOME cty] [SOME (Thm.global_cterm_of thy arg), SOME rhs] |
39564 | 105 |
|> Thm.varifyT_global |
106 |
end; |
|
107 |
||
61667
4b53042d7a40
explicit computation of sort arguments for code equations makes less assumption about sort arguments of underlying type class instances
haftmann
parents:
60801
diff
changeset
|
108 |
fun add_abs_term_of_code tyco vs abs raw_ty_rep proj thy = |
39564 | 109 |
let |
110 |
val ty = Type (tyco, map TFree vs); |
|
111 |
val ty_rep = map_atyps |
|
112 |
(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
|
113 |
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
|
114 |
val eq = mk_abs_term_of_eq thy ty abs ty_rep proj; |
39564 | 115 |
in |
116 |
thy |
|
66251
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
65062
diff
changeset
|
117 |
|> Code.declare_default_eqns_global [(eq, true)] |
39564 | 118 |
end; |
119 |
||
61667
4b53042d7a40
explicit computation of sort arguments for code equations makes less assumption about sort arguments of underlying type class instances
haftmann
parents:
60801
diff
changeset
|
120 |
fun ensure_abs_term_of_code (tyco, (vs, ((abs, (_, ty)), (proj, _)))) = |
4b53042d7a40
explicit computation of sort arguments for code equations makes less assumption about sort arguments of underlying type class instances
haftmann
parents:
60801
diff
changeset
|
121 |
for_term_of_instance tyco vs |
4b53042d7a40
explicit computation of sort arguments for code equations makes less assumption about sort arguments of underlying type class instances
haftmann
parents:
60801
diff
changeset
|
122 |
(fn tyco => fn vs => add_abs_term_of_code tyco vs abs ty proj); |
39564 | 123 |
|
124 |
||
56926 | 125 |
(* setup *) |
126 |
||
59323 | 127 |
val _ = Theory.setup |
56926 | 128 |
(Code.datatype_interpretation ensure_term_of |
129 |
#> Code.abstype_interpretation ensure_term_of |
|
130 |
#> Code.datatype_interpretation ensure_term_of_code |
|
59323 | 131 |
#> Code.abstype_interpretation ensure_abs_term_of_code); |
56926 | 132 |
|
133 |
||
39564 | 134 |
(** termifying syntax **) |
135 |
||
136 |
fun map_default f xs = |
|
137 |
let val ys = map f xs |
|
138 |
in if exists is_some ys |
|
139 |
then SOME (map2 the_default xs ys) |
|
140 |
else NONE |
|
141 |
end; |
|
142 |
||
39565
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
143 |
fun subst_termify_app (Const (@{const_name termify}, _), [t]) = |
63619 | 144 |
if not (Term.exists_subterm (fn Abs _ => true | _ => false) t) |
39564 | 145 |
then if fold_aterms (fn Const _ => I | _ => K false) t true |
146 |
then SOME (HOLogic.reflect_term t) |
|
51714 | 147 |
else error "Cannot termify expression containing variable" |
39564 | 148 |
else error "Cannot termify expression containing abstraction" |
149 |
| subst_termify_app (t, ts) = case map_default subst_termify ts |
|
150 |
of SOME ts' => SOME (list_comb (t, ts')) |
|
151 |
| NONE => NONE |
|
152 |
and subst_termify (Abs (v, T, t)) = (case subst_termify t |
|
153 |
of SOME t' => SOME (Abs (v, T, t')) |
|
154 |
| NONE => NONE) |
|
155 |
| subst_termify t = subst_termify_app (strip_comb t) |
|
156 |
||
62952 | 157 |
fun check_termify ts = the_default ts (map_default subst_termify ts); |
39564 | 158 |
|
62952 | 159 |
val _ = Context.>> (Syntax_Phases.term_check 0 "termify" (K check_termify)); |
56926 | 160 |
|
39564 | 161 |
|
162 |
(** evaluation **) |
|
163 |
||
41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41247
diff
changeset
|
164 |
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
|
165 |
( |
39564 | 166 |
type T = unit -> term |
59153 | 167 |
val empty: T = fn () => raise Fail "Evaluation" |
168 |
fun init _ = empty |
|
39564 | 169 |
); |
170 |
val put_term = Evaluation.put; |
|
39565
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
171 |
val cookie = (Evaluation.get, put_term, "Code_Evaluation.put_term"); |
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
172 |
|
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
173 |
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
|
174 |
|
63157
65a81a4ef7f8
clarified naming conventions and code for code evaluation sandwiches
haftmann
parents:
63064
diff
changeset
|
175 |
fun gen_dynamic_value computation ctxt t = |
65a81a4ef7f8
clarified naming conventions and code for code evaluation sandwiches
haftmann
parents:
63064
diff
changeset
|
176 |
computation cookie ctxt NONE I (mk_term_of t) []; |
39565
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
177 |
|
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
178 |
val dynamic_value = gen_dynamic_value Code_Runtime.dynamic_value; |
f4f87c6e2fad
full palette of dynamic/static value(_strict/exn)
haftmann
parents:
39564
diff
changeset
|
179 |
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
|
180 |
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
|
181 |
|
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 |
(** diagnostic **) |
39564 | 184 |
|
185 |
fun tracing s x = (Output.tracing s; x); |
|
186 |
||
187 |
end; |