| author | wenzelm |
| Wed, 25 Jun 2025 16:35:25 +0200 | |
| changeset 82768 | 8f866fd6fae1 |
| parent 82516 | 88f101c3cfe2 |
| permissions | -rw-r--r-- |
|
82516
88f101c3cfe2
official theory for using bit shift operations for ordinary arithmetic if feasible
haftmann
parents:
diff
changeset
|
1 |
(* Author: Florian Haftmann, TU Muenchen *) |
|
88f101c3cfe2
official theory for using bit shift operations for ordinary arithmetic if feasible
haftmann
parents:
diff
changeset
|
2 |
|
|
88f101c3cfe2
official theory for using bit shift operations for ordinary arithmetic if feasible
haftmann
parents:
diff
changeset
|
3 |
section \<open>Basic setup\<close> |
|
88f101c3cfe2
official theory for using bit shift operations for ordinary arithmetic if feasible
haftmann
parents:
diff
changeset
|
4 |
|
|
88f101c3cfe2
official theory for using bit shift operations for ordinary arithmetic if feasible
haftmann
parents:
diff
changeset
|
5 |
theory Basic_Setup |
|
88f101c3cfe2
official theory for using bit shift operations for ordinary arithmetic if feasible
haftmann
parents:
diff
changeset
|
6 |
imports |
|
88f101c3cfe2
official theory for using bit shift operations for ordinary arithmetic if feasible
haftmann
parents:
diff
changeset
|
7 |
Complex_Main |
|
88f101c3cfe2
official theory for using bit shift operations for ordinary arithmetic if feasible
haftmann
parents:
diff
changeset
|
8 |
begin |
|
88f101c3cfe2
official theory for using bit shift operations for ordinary arithmetic if feasible
haftmann
parents:
diff
changeset
|
9 |
|
|
88f101c3cfe2
official theory for using bit shift operations for ordinary arithmetic if feasible
haftmann
parents:
diff
changeset
|
10 |
text \<open>Drop technical stuff from \<^theory>\<open>HOL.Quickcheck_Narrowing\<close> which is tailored towards Haskell\<close> |
|
88f101c3cfe2
official theory for using bit shift operations for ordinary arithmetic if feasible
haftmann
parents:
diff
changeset
|
11 |
|
|
88f101c3cfe2
official theory for using bit shift operations for ordinary arithmetic if feasible
haftmann
parents:
diff
changeset
|
12 |
ML \<open> |
|
88f101c3cfe2
official theory for using bit shift operations for ordinary arithmetic if feasible
haftmann
parents:
diff
changeset
|
13 |
structure Codegenerator_Test = |
|
88f101c3cfe2
official theory for using bit shift operations for ordinary arithmetic if feasible
haftmann
parents:
diff
changeset
|
14 |
struct |
|
88f101c3cfe2
official theory for using bit shift operations for ordinary arithmetic if feasible
haftmann
parents:
diff
changeset
|
15 |
|
|
88f101c3cfe2
official theory for using bit shift operations for ordinary arithmetic if feasible
haftmann
parents:
diff
changeset
|
16 |
fun drop_partial_term_of thy = |
|
88f101c3cfe2
official theory for using bit shift operations for ordinary arithmetic if feasible
haftmann
parents:
diff
changeset
|
17 |
let |
|
88f101c3cfe2
official theory for using bit shift operations for ordinary arithmetic if feasible
haftmann
parents:
diff
changeset
|
18 |
val tycos = Sign.logical_types thy; |
|
88f101c3cfe2
official theory for using bit shift operations for ordinary arithmetic if feasible
haftmann
parents:
diff
changeset
|
19 |
val consts = map_filter (try (curry (Axclass.param_of_inst thy) |
|
88f101c3cfe2
official theory for using bit shift operations for ordinary arithmetic if feasible
haftmann
parents:
diff
changeset
|
20 |
\<^const_name>\<open>Quickcheck_Narrowing.partial_term_of\<close>)) tycos; |
|
88f101c3cfe2
official theory for using bit shift operations for ordinary arithmetic if feasible
haftmann
parents:
diff
changeset
|
21 |
in |
|
88f101c3cfe2
official theory for using bit shift operations for ordinary arithmetic if feasible
haftmann
parents:
diff
changeset
|
22 |
thy |
|
88f101c3cfe2
official theory for using bit shift operations for ordinary arithmetic if feasible
haftmann
parents:
diff
changeset
|
23 |
|> fold Code.declare_unimplemented_global consts |
|
88f101c3cfe2
official theory for using bit shift operations for ordinary arithmetic if feasible
haftmann
parents:
diff
changeset
|
24 |
end; |
|
88f101c3cfe2
official theory for using bit shift operations for ordinary arithmetic if feasible
haftmann
parents:
diff
changeset
|
25 |
|
|
88f101c3cfe2
official theory for using bit shift operations for ordinary arithmetic if feasible
haftmann
parents:
diff
changeset
|
26 |
end; |
|
88f101c3cfe2
official theory for using bit shift operations for ordinary arithmetic if feasible
haftmann
parents:
diff
changeset
|
27 |
\<close> |
|
88f101c3cfe2
official theory for using bit shift operations for ordinary arithmetic if feasible
haftmann
parents:
diff
changeset
|
28 |
|
|
88f101c3cfe2
official theory for using bit shift operations for ordinary arithmetic if feasible
haftmann
parents:
diff
changeset
|
29 |
text \<open>Avoid popular infix.\<close> |
|
88f101c3cfe2
official theory for using bit shift operations for ordinary arithmetic if feasible
haftmann
parents:
diff
changeset
|
30 |
|
|
88f101c3cfe2
official theory for using bit shift operations for ordinary arithmetic if feasible
haftmann
parents:
diff
changeset
|
31 |
code_reserved (SML) upto |
|
88f101c3cfe2
official theory for using bit shift operations for ordinary arithmetic if feasible
haftmann
parents:
diff
changeset
|
32 |
|
|
88f101c3cfe2
official theory for using bit shift operations for ordinary arithmetic if feasible
haftmann
parents:
diff
changeset
|
33 |
end |