33 subsection {* preprocessor *} |
33 subsection {* preprocessor *} |
34 |
34 |
35 ML {* |
35 ML {* |
36 fun constrain_op_eq thy thms = |
36 fun constrain_op_eq thy thms = |
37 let |
37 let |
38 fun dest_eq (Const ("op =", ty)) = |
38 fun add_eq (Const ("op =", ty)) = |
39 (SOME o hd o fst o strip_type) ty |
39 fold (insert (eq_fst (op = : indexname * indexname -> bool))) |
40 | dest_eq _ = NONE |
40 (Term.add_tvarsT ty []) |
41 fun eqs_of t = |
41 | add_eq _ = |
42 fold_aterms (fn t => case dest_eq t |
42 I |
43 of SOME (TVar v_sort) => cons v_sort |
43 val eqs = fold (fold_aterms add_eq o Thm.prop_of) thms []; |
44 | _ => I) t []; |
|
45 val eqs = maps (eqs_of o Thm.prop_of) thms; |
|
46 val instT = map (fn (v_i, sort) => |
44 val instT = map (fn (v_i, sort) => |
47 (Thm.ctyp_of thy (TVar (v_i, sort)), |
45 (Thm.ctyp_of thy (TVar (v_i, sort)), |
48 Thm.ctyp_of thy (TVar (v_i, Sorts.inter_sort (Sign.classes_of thy) (sort, [class_eq]))))) eqs; |
46 Thm.ctyp_of thy (TVar (v_i, Sorts.inter_sort (Sign.classes_of thy) (sort, [class_eq]))))) eqs; |
49 in |
47 in |
50 thms |
48 thms |
80 |
78 |
81 subsection {* extractor *} |
79 subsection {* extractor *} |
82 |
80 |
83 setup {* |
81 setup {* |
84 let |
82 let |
|
83 val lift_not_thm = thm "HOL.Eq_FalseI"; |
|
84 val lift_thm = thm "HOL.eq_reflection"; |
|
85 val eq_def_thm = Thm.symmetric (thm "eq_def"); |
85 fun get_eq_thms thy tyco = case DatatypePackage.get_datatype thy tyco |
86 fun get_eq_thms thy tyco = case DatatypePackage.get_datatype thy tyco |
86 of SOME _ => DatatypeCodegen.get_eq thy tyco |
87 of SOME _ => DatatypeCodegen.get_eq thy tyco |
87 | NONE => case TypedefCodegen.get_triv_typedef thy tyco |
88 | NONE => case TypedefCodegen.get_triv_typedef thy tyco |
88 of SOME (_ ,(_, thm)) => [thm] |
89 of SOME (_ ,(_, thm)) => [thm] |
89 | NONE => []; |
90 | NONE => []; |
90 fun get_eq_thms_eq thy ("OperationalEquality.eq", ty) = (case strip_type ty |
91 fun get_eq_thms_eq thy ("CodeOperationalEquality.eq", ty) = (case strip_type ty |
91 of (Type (tyco, _) :: _, _) => |
92 of (Type (tyco, _) :: _, _) => |
92 get_eq_thms thy tyco |
93 get_eq_thms thy tyco |
|
94 |> map (perhaps (try (fn thm => lift_not_thm OF [thm]))) |
|
95 |> map (perhaps (try (fn thm => lift_thm OF [thm]))) |
|
96 (*|> tap (writeln o cat_lines o map string_of_thm)*) |
|
97 |> constrain_op_eq thy |
|
98 (*|> tap (writeln o cat_lines o map string_of_thm)*) |
|
99 |> map (Tactic.rewrite_rule [eq_def_thm]) |
|
100 (*|> tap (writeln o cat_lines o map string_of_thm)*) |
93 | _ => []) |
101 | _ => []) |
94 | get_eq_thms_eq _ _ = []; |
102 | get_eq_thms_eq _ _ = []; |
95 in |
103 in |
96 CodegenTheorems.add_fun_extr get_eq_thms_eq |
104 CodegenTheorems.add_fun_extr get_eq_thms_eq |
97 end |
105 end |
136 (eq :: list) haskell |
144 (eq :: list) haskell |
137 (eq :: char) haskell |
145 (eq :: char) haskell |
138 (eq :: int) haskell |
146 (eq :: int) haskell |
139 |
147 |
140 code_constapp |
148 code_constapp |
141 "eq" |
|
142 haskell (infixl 4 "==") |
|
143 "eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool" |
149 "eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool" |
144 haskell (infixl 4 "==") |
150 haskell (infixl 4 "==") |
145 "eq \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool" |
151 "eq \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool" |
146 haskell (infixl 4 "==") |
152 haskell (infixl 4 "==") |
147 "eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool" |
153 "eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool" |
152 haskell (infixl 4 "==") |
158 haskell (infixl 4 "==") |
153 "eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool" |
159 "eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool" |
154 haskell (infixl 4 "==") |
160 haskell (infixl 4 "==") |
155 "eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool" |
161 "eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool" |
156 haskell (infixl 4 "==") |
162 haskell (infixl 4 "==") |
|
163 "eq" |
|
164 haskell (infixl 4 "==") |
157 |
165 |
158 end |
166 end |