16 fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
16 fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
17 |
17 |
18 defs |
18 defs |
19 eq_def: "eq x y \<equiv> (x = y)" |
19 eq_def: "eq x y \<equiv> (x = y)" |
20 |
20 |
21 ML {* |
|
22 local |
|
23 val thy = the_context (); |
|
24 val const_eq = Sign.intern_const thy "eq"; |
|
25 val type_bool = Type (Sign.intern_type thy "bool", []); |
|
26 in |
|
27 val eq_def_sym = Thm.symmetric (thm "eq_def"); |
|
28 val class_eq = Sign.intern_class thy "eq"; |
|
29 end |
|
30 *} |
|
31 |
|
32 |
21 |
33 subsection {* bool type *} |
22 subsection {* bool type *} |
34 |
23 |
35 instance bool :: eq .. |
24 instance bool :: eq .. |
36 |
25 |
45 |
34 |
46 lemma [code func]: |
35 lemma [code func]: |
47 "eq p False = (\<not> p)" unfolding eq_def by auto |
36 "eq p False = (\<not> p)" unfolding eq_def by auto |
48 |
37 |
49 |
38 |
50 subsection {* preprocessor *} |
39 subsection {* code generator setup *} |
51 |
40 |
52 ML {* |
41 subsubsection {* preprocessor *} |
53 fun constrain_op_eq thy thms = |
|
54 let |
|
55 fun add_eq (Const ("op =", ty)) = |
|
56 fold (insert (eq_fst (op = : indexname * indexname -> bool))) |
|
57 (Term.add_tvarsT ty []) |
|
58 | add_eq _ = |
|
59 I |
|
60 val eqs = fold (fold_aterms add_eq o Thm.prop_of) thms []; |
|
61 val instT = map (fn (v_i, sort) => |
|
62 (Thm.ctyp_of thy (TVar (v_i, sort)), |
|
63 Thm.ctyp_of thy (TVar (v_i, Sorts.inter_sort (Sign.classes_of thy) (sort, [class_eq]))))) eqs; |
|
64 in |
|
65 thms |
|
66 |> map (Thm.instantiate (instT, [])) |
|
67 end; |
|
68 *} |
|
69 |
|
70 |
|
71 subsection {* codegenerator setup *} |
|
72 |
42 |
73 setup {* |
43 setup {* |
74 CodegenData.add_preproc constrain_op_eq |
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 |
75 *} |
57 *} |
76 |
58 |
77 declare eq_def [symmetric, code inline] |
59 declare eq_def [symmetric, code inline] |
78 |
60 |
79 code_constname |
61 code_constname |