author | wenzelm |
Tue, 25 Sep 2012 15:40:41 +0200 | |
changeset 49561 | 26fc70e983c2 |
parent 47108 | 2a1953f0d20d |
child 50056 | 72efd6b4038d |
permissions | -rw-r--r-- |
33265 | 1 |
(* Title: HOL/Tools/Predicate_Compile/predicate_compile_data.ML |
2 |
Author: Lukas Bulwahn, TU Muenchen |
|
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
3 |
|
33265 | 4 |
Book-keeping datastructure for the predicate compiler. |
5 |
*) |
|
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
6 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
7 |
signature PREDICATE_COMPILE_DATA = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
8 |
sig |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
9 |
val ignore_consts : string list -> theory -> theory |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
10 |
val keep_functions : string list -> theory -> theory |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
11 |
val keep_function : theory -> string -> bool |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
12 |
val processed_specs : theory -> string -> (string * thm list) list option |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
13 |
val store_processed_specs : (string * (string * thm list) list) -> theory -> theory |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
14 |
|
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
15 |
val get_specification : Predicate_Compile_Aux.options -> theory -> term -> thm list |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
16 |
val obtain_specification_graph : |
35404 | 17 |
Predicate_Compile_Aux.options -> theory -> term -> thm list Term_Graph.T |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
18 |
|
35404 | 19 |
val present_graph : thm list Term_Graph.T -> unit |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
20 |
val normalize_equation : theory -> thm -> thm |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
21 |
end; |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
22 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
23 |
structure Predicate_Compile_Data : PREDICATE_COMPILE_DATA = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
24 |
struct |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
25 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
26 |
open Predicate_Compile_Aux; |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
27 |
|
33522 | 28 |
structure Data = Theory_Data |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
29 |
( |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
30 |
type T = |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
31 |
{ignore_consts : unit Symtab.table, |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
32 |
keep_functions : unit Symtab.table, |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
33 |
processed_specs : ((string * thm list) list) Symtab.table}; |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
34 |
val empty = |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
35 |
{ignore_consts = Symtab.empty, |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
36 |
keep_functions = Symtab.empty, |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
37 |
processed_specs = Symtab.empty}; |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
38 |
val extend = I; |
33522 | 39 |
fun merge |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
40 |
({ignore_consts = c1, keep_functions = k1, processed_specs = s1}, |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
41 |
{ignore_consts = c2, keep_functions = k2, processed_specs = s2}) = |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
42 |
{ignore_consts = Symtab.merge (K true) (c1, c2), |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
43 |
keep_functions = Symtab.merge (K true) (k1, k2), |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
44 |
processed_specs = Symtab.merge (K true) (s1, s2)} |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
45 |
); |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
46 |
|
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
47 |
|
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
48 |
|
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
49 |
fun mk_data (c, k, s) = {ignore_consts = c, keep_functions = k, processed_specs = s} |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
50 |
fun map_data f {ignore_consts = c, keep_functions = k, processed_specs = s} = mk_data (f (c, k, s)) |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
51 |
|
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
52 |
fun ignore_consts cs = Data.map (map_data (apfst3 (fold (fn c => Symtab.insert (op =) (c, ())) cs))) |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
53 |
|
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
54 |
fun keep_functions cs = Data.map (map_data (apsnd3 (fold (fn c => Symtab.insert (op =) (c, ())) cs))) |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
55 |
|
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
56 |
fun keep_function thy = Symtab.defined (#keep_functions (Data.get thy)) |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
57 |
|
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
58 |
fun processed_specs thy = Symtab.lookup (#processed_specs (Data.get thy)) |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
59 |
|
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
60 |
fun store_processed_specs (constname, specs) = |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
61 |
Data.map (map_data (aptrd3 (Symtab.update_new (constname, specs)))) |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
62 |
(* *) |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
63 |
|
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
64 |
|
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
65 |
fun defining_term_of_introrule_term t = |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
66 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
67 |
val _ $ u = Logic.strip_imp_concl t |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
68 |
in fst (strip_comb u) end |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
69 |
(* |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
70 |
in case pred of |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
71 |
Const (c, T) => c |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
72 |
| _ => raise TERM ("defining_const_of_introrule_term failed: Not a constant", [t]) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
73 |
end |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
74 |
*) |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
75 |
val defining_term_of_introrule = defining_term_of_introrule_term o prop_of |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
76 |
|
40142
128f8a1611e6
relaxing the filtering condition for getting specifications from Spec_Rules
bulwahn
parents:
40053
diff
changeset
|
77 |
fun defining_const_of_introrule th = |
128f8a1611e6
relaxing the filtering condition for getting specifications from Spec_Rules
bulwahn
parents:
40053
diff
changeset
|
78 |
case defining_term_of_introrule th |
128f8a1611e6
relaxing the filtering condition for getting specifications from Spec_Rules
bulwahn
parents:
40053
diff
changeset
|
79 |
of Const (c, _) => c |
128f8a1611e6
relaxing the filtering condition for getting specifications from Spec_Rules
bulwahn
parents:
40053
diff
changeset
|
80 |
| _ => raise TERM ("defining_const_of_introrule failed: Not a constant", [prop_of th]) |
128f8a1611e6
relaxing the filtering condition for getting specifications from Spec_Rules
bulwahn
parents:
40053
diff
changeset
|
81 |
|
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
82 |
(*TODO*) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
83 |
fun is_introlike_term t = true |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
84 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
85 |
val is_introlike = is_introlike_term o prop_of |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
86 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
87 |
fun check_equation_format_term (t as (Const ("==", _) $ u $ v)) = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
88 |
(case strip_comb u of |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
89 |
(Const (c, T), args) => |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
90 |
if (length (binder_types T) = length args) then |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
91 |
true |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
92 |
else |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
93 |
raise TERM ("check_equation_format_term failed: Number of arguments mismatch", [t]) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
94 |
| _ => raise TERM ("check_equation_format_term failed: Not a constant", [t])) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
95 |
| check_equation_format_term t = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
96 |
raise TERM ("check_equation_format_term failed: Not an equation", [t]) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
97 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
98 |
val check_equation_format = check_equation_format_term o prop_of |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
99 |
|
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
100 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
101 |
fun defining_term_of_equation_term (t as (Const ("==", _) $ u $ v)) = fst (strip_comb u) |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
102 |
| defining_term_of_equation_term t = |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
103 |
raise TERM ("defining_const_of_equation_term failed: Not an equation", [t]) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
104 |
|
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
105 |
val defining_term_of_equation = defining_term_of_equation_term o prop_of |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
106 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
107 |
fun defining_const_of_equation th = |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
108 |
case defining_term_of_equation th |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
109 |
of Const (c, _) => c |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
110 |
| _ => raise TERM ("defining_const_of_equation failed: Not a constant", [prop_of th]) |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
111 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
112 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
113 |
|
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
114 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
115 |
(* Normalizing equations *) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
116 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
117 |
fun mk_meta_equation th = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
118 |
case prop_of th of |
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38795
diff
changeset
|
119 |
Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => th RS @{thm eq_reflection} |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
120 |
| _ => th |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
121 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
122 |
val meta_fun_cong = @{lemma "f == g ==> f x == g x" by simp} |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
123 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
124 |
fun full_fun_cong_expand th = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
125 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
126 |
val (f, args) = strip_comb (fst (Logic.dest_equals (prop_of th))) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
127 |
val i = length (binder_types (fastype_of f)) - length args |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
128 |
in funpow i (fn th => th RS meta_fun_cong) th end; |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
129 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
130 |
fun declare_names s xs ctxt = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
131 |
let |
43329
84472e198515
tuned signature: Name.invent and Name.invent_names;
wenzelm
parents:
43277
diff
changeset
|
132 |
val res = Name.invent_names ctxt s xs |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
133 |
in (res, fold Name.declare (map fst res) ctxt) end |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
134 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
135 |
fun split_all_pairs thy th = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
136 |
let |
42361 | 137 |
val ctxt = Proof_Context.init_global thy |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
138 |
val ((_, [th']), ctxt') = Variable.import true [th] ctxt |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
139 |
val t = prop_of th' |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
140 |
val frees = Term.add_frees t [] |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
141 |
val freenames = Term.add_free_names t [] |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
142 |
val nctxt = Name.make_context freenames |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
143 |
fun mk_tuple_rewrites (x, T) nctxt = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
144 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
145 |
val Ts = HOLogic.flatten_tupleT T |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
146 |
val (xTs, nctxt') = declare_names x Ts nctxt |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
147 |
val paths = HOLogic.flat_tupleT_paths T |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
148 |
in ((Free (x, T), HOLogic.mk_ptuple paths T (map Free xTs)), nctxt') end |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
149 |
val (rewr, _) = fold_map mk_tuple_rewrites frees nctxt |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
150 |
val t' = Pattern.rewrite_term thy rewr [] t |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
151 |
val tac = Skip_Proof.cheat_tac thy |
33441
99a5f22a967d
eliminated funny record patterns and made SML/NJ happy;
wenzelm
parents:
33404
diff
changeset
|
152 |
val th'' = Goal.prove ctxt (Term.add_free_names t' []) [] t' (fn _ => tac) |
35624 | 153 |
val th''' = Local_Defs.unfold ctxt [@{thm split_conv}, @{thm fst_conv}, @{thm snd_conv}] th'' |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
154 |
in |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
155 |
th''' |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
156 |
end; |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
157 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
158 |
|
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
159 |
fun inline_equations thy th = |
33404 | 160 |
let |
42361 | 161 |
val inline_defs = Predicate_Compile_Inline_Defs.get (Proof_Context.init_global thy) |
33404 | 162 |
val th' = (Simplifier.full_simplify (HOL_basic_ss addsimps inline_defs)) th |
163 |
(*val _ = print_step options |
|
164 |
("Inlining " ^ (Syntax.string_of_term_global thy (prop_of th)) |
|
165 |
^ "with " ^ (commas (map ((Syntax.string_of_term_global thy) o prop_of) inline_defs)) |
|
166 |
^" to " ^ (Syntax.string_of_term_global thy (prop_of th')))*) |
|
167 |
in |
|
168 |
th' |
|
169 |
end |
|
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
170 |
|
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
171 |
fun normalize_equation thy th = |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
172 |
mk_meta_equation th |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
173 |
|> full_fun_cong_expand |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
174 |
|> split_all_pairs thy |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
175 |
|> tap check_equation_format |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
176 |
|> inline_equations thy |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
177 |
|
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
178 |
fun normalize_intros thy th = |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
179 |
split_all_pairs thy th |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
180 |
|> inline_equations thy |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
181 |
|
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
182 |
fun normalize thy th = |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
183 |
if is_equationlike th then |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
184 |
normalize_equation thy th |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
185 |
else |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
186 |
normalize_intros thy th |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
187 |
|
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
188 |
fun get_specification options thy t = |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
189 |
let |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
190 |
(*val (c, T) = dest_Const t |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
191 |
val t = Const (AxClass.unoverload_const thy (c, T), T)*) |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
192 |
val _ = if show_steps options then |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
193 |
tracing ("getting specification of " ^ Syntax.string_of_term_global thy t ^ |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
194 |
" with type " ^ Syntax.string_of_typ_global thy (fastype_of t)) |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
195 |
else () |
42361 | 196 |
val ctxt = Proof_Context.init_global thy |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
197 |
fun filtering th = |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
198 |
if is_equationlike th andalso |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
199 |
defining_const_of_equation (normalize_equation thy th) = fst (dest_Const t) then |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
200 |
SOME (normalize_equation thy th) |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
201 |
else |
40142
128f8a1611e6
relaxing the filtering condition for getting specifications from Spec_Rules
bulwahn
parents:
40053
diff
changeset
|
202 |
if is_introlike th andalso defining_const_of_introrule th = fst (dest_Const t) then |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
203 |
SOME th |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
204 |
else |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
205 |
NONE |
35758
c029f85d3879
adopting predicate compiler to changes in Spec_Rules; removed dependency to Nitpick_Intros
bulwahn
parents:
35624
diff
changeset
|
206 |
fun filter_defs ths = map_filter filtering (map (normalize thy o Thm.transfer thy) ths) |
c029f85d3879
adopting predicate compiler to changes in Spec_Rules; removed dependency to Nitpick_Intros
bulwahn
parents:
35624
diff
changeset
|
207 |
val spec = case filter_defs (Predicate_Compile_Alternative_Defs.get ctxt) of |
c029f85d3879
adopting predicate compiler to changes in Spec_Rules; removed dependency to Nitpick_Intros
bulwahn
parents:
35624
diff
changeset
|
208 |
[] => (case Spec_Rules.retrieve ctxt t of |
c029f85d3879
adopting predicate compiler to changes in Spec_Rules; removed dependency to Nitpick_Intros
bulwahn
parents:
35624
diff
changeset
|
209 |
[] => error ("No specification for " ^ (Syntax.string_of_term_global thy t)) |
c029f85d3879
adopting predicate compiler to changes in Spec_Rules; removed dependency to Nitpick_Intros
bulwahn
parents:
35624
diff
changeset
|
210 |
| ((_, (_, ths)) :: _) => filter_defs ths) |
c029f85d3879
adopting predicate compiler to changes in Spec_Rules; removed dependency to Nitpick_Intros
bulwahn
parents:
35624
diff
changeset
|
211 |
| ths => rev ths |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
212 |
val _ = |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
213 |
if show_intermediate_results options then |
43277 | 214 |
tracing ("Specification for " ^ (Syntax.string_of_term_global thy t) ^ ":\n" ^ |
40142
128f8a1611e6
relaxing the filtering condition for getting specifications from Spec_Rules
bulwahn
parents:
40053
diff
changeset
|
215 |
commas (map (Display.string_of_thm_global thy) spec)) |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
216 |
else () |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
217 |
in |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
218 |
spec |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
219 |
end |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
220 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
221 |
val logic_operator_names = |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
222 |
[@{const_name "=="}, |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
223 |
@{const_name "==>"}, |
38558 | 224 |
@{const_name Trueprop}, |
225 |
@{const_name Not}, |
|
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38795
diff
changeset
|
226 |
@{const_name HOL.eq}, |
38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38731
diff
changeset
|
227 |
@{const_name HOL.implies}, |
38558 | 228 |
@{const_name All}, |
229 |
@{const_name Ex}, |
|
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset
|
230 |
@{const_name HOL.conj}, |
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset
|
231 |
@{const_name HOL.disj}] |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
232 |
|
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
233 |
fun special_cases (c, T) = member (op =) [ |
34974
18b41bba42b5
new theory Algebras.thy for generic algebraic structures
haftmann
parents:
34954
diff
changeset
|
234 |
@{const_name Product_Type.Unity}, |
18b41bba42b5
new theory Algebras.thy for generic algebraic structures
haftmann
parents:
34954
diff
changeset
|
235 |
@{const_name False}, |
18b41bba42b5
new theory Algebras.thy for generic algebraic structures
haftmann
parents:
34954
diff
changeset
|
236 |
@{const_name Suc}, @{const_name Nat.zero_nat_inst.zero_nat}, |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
237 |
@{const_name Nat.one_nat_inst.one_nat}, |
35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
34974
diff
changeset
|
238 |
@{const_name Orderings.less}, @{const_name Orderings.less_eq}, |
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
239 |
@{const_name Groups.zero}, |
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
240 |
@{const_name Groups.one}, @{const_name Groups.plus}, |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
241 |
@{const_name Nat.ord_nat_inst.less_eq_nat}, |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
242 |
@{const_name Nat.ord_nat_inst.less_nat}, |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44338
diff
changeset
|
243 |
(* FIXME |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
244 |
@{const_name number_nat_inst.number_of_nat}, |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44338
diff
changeset
|
245 |
*) |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44338
diff
changeset
|
246 |
@{const_name Num.Bit0}, |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44338
diff
changeset
|
247 |
@{const_name Num.Bit1}, |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44338
diff
changeset
|
248 |
@{const_name Num.One}, |
34974
18b41bba42b5
new theory Algebras.thy for generic algebraic structures
haftmann
parents:
34954
diff
changeset
|
249 |
@{const_name Int.zero_int_inst.zero_int}, |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
250 |
@{const_name List.filter}, |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
251 |
@{const_name HOL.If}, |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
252 |
@{const_name Groups.minus} |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
253 |
] c |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
254 |
|
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
255 |
|
33252
8bd2eb003b8f
print retrieved specification when printing intermediate results
bulwahn
parents:
33250
diff
changeset
|
256 |
fun print_specification options thy constname specs = |
8bd2eb003b8f
print retrieved specification when printing intermediate results
bulwahn
parents:
33250
diff
changeset
|
257 |
if show_intermediate_results options then |
8bd2eb003b8f
print retrieved specification when printing intermediate results
bulwahn
parents:
33250
diff
changeset
|
258 |
tracing ("Specification of " ^ constname ^ ":\n" ^ |
8bd2eb003b8f
print retrieved specification when printing intermediate results
bulwahn
parents:
33250
diff
changeset
|
259 |
cat_lines (map (Display.string_of_thm_global thy) specs)) |
8bd2eb003b8f
print retrieved specification when printing intermediate results
bulwahn
parents:
33250
diff
changeset
|
260 |
else () |
8bd2eb003b8f
print retrieved specification when printing intermediate results
bulwahn
parents:
33250
diff
changeset
|
261 |
|
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
262 |
fun obtain_specification_graph options thy t = |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
263 |
let |
42361 | 264 |
val ctxt = Proof_Context.init_global thy |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
265 |
fun is_nondefining_const (c, T) = member (op =) logic_operator_names c |
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
38864
diff
changeset
|
266 |
fun has_code_pred_intros (c, T) = can (Core_Data.intros_of ctxt) c |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
267 |
fun case_consts (c, T) = is_some (Datatype.info_of_case thy c) |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
268 |
fun is_datatype_constructor (c, T) = is_some (Datatype.info_of_constr thy (c, T)) |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
269 |
fun defiants_of specs = |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
270 |
fold (Term.add_consts o prop_of) specs [] |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
271 |
|> filter_out is_datatype_constructor |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
272 |
|> filter_out is_nondefining_const |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
273 |
|> filter_out has_code_pred_intros |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
274 |
|> filter_out case_consts |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
275 |
|> filter_out special_cases |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
276 |
|> filter_out (fn (c, _) => Symtab.defined (#ignore_consts (Data.get thy)) c) |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
277 |
|> map (fn (c, _) => (c, Sign.the_const_constraint thy c)) |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
278 |
|> map Const |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
279 |
(* |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
280 |
|> filter is_defining_constname*) |
35405 | 281 |
fun extend t gr = |
282 |
if can (Term_Graph.get_node gr) t then gr |
|
283 |
else |
|
284 |
let |
|
285 |
val specs = get_specification options thy t |
|
286 |
(*val _ = print_specification options thy constname specs*) |
|
287 |
val us = defiants_of specs |
|
288 |
in |
|
289 |
gr |
|
290 |
|> Term_Graph.new_node (t, specs) |
|
291 |
|> fold extend us |
|
292 |
|> fold (fn u => Term_Graph.add_edge (t, u)) us |
|
293 |
end |
|
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
294 |
in |
35405 | 295 |
extend t Term_Graph.empty |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
296 |
end; |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
297 |
|
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
298 |
|
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
299 |
fun present_graph gr = |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
300 |
let |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
301 |
fun eq_cname (Const (c1, _), Const (c2, _)) = (c1 = c2) |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
302 |
fun string_of_const (Const (c, _)) = c |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
303 |
| string_of_const _ = error "string_of_const: unexpected term" |
35404 | 304 |
val constss = Term_Graph.strong_conn gr; |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
305 |
val mapping = Termtab.empty |> fold (fn consts => fold (fn const => |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
306 |
Termtab.update (const, consts)) consts) constss; |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
307 |
fun succs consts = consts |
44338
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
43329
diff
changeset
|
308 |
|> maps (Term_Graph.immediate_succs gr) |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
309 |
|> subtract eq_cname consts |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
310 |
|> map (the o Termtab.lookup mapping) |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
311 |
|> distinct (eq_list eq_cname); |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
312 |
val conn = [] |> fold (fn consts => cons (consts, succs consts)) constss; |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
313 |
|
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
314 |
fun namify consts = map string_of_const consts |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
315 |
|> commas; |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
316 |
val prgr = map (fn (consts, constss) => |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
317 |
{ name = namify consts, ID = namify consts, dir = "", unfold = true, |
49561 | 318 |
path = "", parents = map namify constss, content = [] }) conn; |
319 |
in Graph_Display.display_graph prgr end; |
|
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35267
diff
changeset
|
320 |
|
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33756
diff
changeset
|
321 |
|
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
322 |
end; |