20598
|
1 |
(* ID: $Id$
|
|
2 |
Author: Florian Haftmann, TU Muenchen
|
|
3 |
*)
|
|
4 |
|
|
5 |
header {* Operational equality for code generation *}
|
|
6 |
|
|
7 |
theory OperationalEquality
|
|
8 |
imports HOL
|
|
9 |
begin
|
|
10 |
|
|
11 |
section {* Operational equality for code generation *}
|
|
12 |
|
|
13 |
subsection {* eq class *}
|
|
14 |
|
|
15 |
class eq =
|
|
16 |
fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
|
|
17 |
|
|
18 |
defs
|
|
19 |
eq_def: "eq x y \<equiv> (x = y)"
|
|
20 |
|
|
21 |
|
|
22 |
subsection {* bool type *}
|
|
23 |
|
|
24 |
instance bool :: eq ..
|
|
25 |
|
|
26 |
lemma [code func]:
|
|
27 |
"eq True p = p" unfolding eq_def by auto
|
|
28 |
|
|
29 |
lemma [code func]:
|
|
30 |
"eq False p = (\<not> p)" unfolding eq_def by auto
|
|
31 |
|
|
32 |
lemma [code func]:
|
|
33 |
"eq p True = p" unfolding eq_def by auto
|
|
34 |
|
|
35 |
lemma [code func]:
|
|
36 |
"eq p False = (\<not> p)" unfolding eq_def by auto
|
|
37 |
|
|
38 |
|
20835
|
39 |
subsection {* code generator setup *}
|
20598
|
40 |
|
20835
|
41 |
subsubsection {* preprocessor *}
|
20598
|
42 |
|
|
43 |
setup {*
|
20835
|
44 |
let
|
|
45 |
val class_eq = "OperationalEquality.eq";
|
|
46 |
fun constrain_op_eq thy ts =
|
|
47 |
let
|
|
48 |
fun add_eq (Const ("op =", ty)) =
|
|
49 |
fold (insert (eq_fst (op = : indexname * indexname -> bool)))
|
|
50 |
(Term.add_tvarsT ty [])
|
|
51 |
| add_eq _ =
|
|
52 |
I
|
|
53 |
val eqs = (fold o fold_aterms) add_eq ts [];
|
|
54 |
val inst = map (fn (v_i, _) => (v_i, [class_eq])) eqs;
|
|
55 |
in inst end;
|
|
56 |
in CodegenData.add_constrains constrain_op_eq end
|
20598
|
57 |
*}
|
|
58 |
|
|
59 |
declare eq_def [symmetric, code inline]
|
|
60 |
|
|
61 |
code_constname
|
|
62 |
"eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool" "HOL.eq_bool"
|
|
63 |
|
|
64 |
|
|
65 |
subsection {* haskell setup *}
|
|
66 |
|
|
67 |
code_class eq
|
|
68 |
(Haskell "Eq" where eq \<equiv> "(==)")
|
|
69 |
|
|
70 |
code_const eq
|
|
71 |
(Haskell infixl 4 "==")
|
|
72 |
|
|
73 |
code_instance bool :: eq
|
|
74 |
(Haskell -)
|
|
75 |
|
|
76 |
code_const "eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
|
|
77 |
(Haskell infixl 4 "==")
|
|
78 |
|
|
79 |
|
|
80 |
subsection {* nbe setup *}
|
|
81 |
|
|
82 |
lemma eq_refl: "eq x x"
|
|
83 |
unfolding eq_def ..
|
|
84 |
|
|
85 |
setup {*
|
|
86 |
let
|
|
87 |
|
|
88 |
val eq_refl = thm "eq_refl";
|
|
89 |
|
|
90 |
fun Trueprop_conv conv ct = (case term_of ct of
|
|
91 |
Const ("Trueprop", _) $ _ =>
|
|
92 |
let val (ct1, ct2) = Thm.dest_comb ct
|
|
93 |
in Thm.combination (Thm.reflexive ct1) (conv ct2) end
|
|
94 |
| _ => raise TERM ("Trueprop_conv", []));
|
|
95 |
|
|
96 |
fun normalization_tac i = Tactical.PRIMITIVE (Drule.fconv_rule
|
|
97 |
(Drule.goals_conv (equal i) (Trueprop_conv NBE.normalization_conv)));
|
|
98 |
|
|
99 |
val normalization_meth =
|
|
100 |
Method.no_args (Method.METHOD (fn _ => normalization_tac 1 THEN resolve_tac [TrueI, refl, eq_refl] 1));
|
|
101 |
|
|
102 |
in
|
|
103 |
|
|
104 |
Method.add_method ("normalization", normalization_meth, "solve goal by normalization")
|
|
105 |
|
|
106 |
end;
|
|
107 |
*}
|
|
108 |
|
|
109 |
|
|
110 |
hide (open) const eq
|
|
111 |
|
|
112 |
end |