author | bulwahn |
Mon, 22 Mar 2010 08:30:13 +0100 | |
changeset 35878 | 74a74828d682 |
parent 35877 | 295e1af6c8dc |
child 36029 | a790b94e090c |
permissions | -rw-r--r-- |
33265 | 1 |
(* Title: HOL/Tools/Predicate_Compile/predicate_compile_fun.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 |
Preprocessing functions to predicates. |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
5 |
*) |
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_FUN = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
8 |
sig |
33630
68e058d061f5
removed unnecessary oracle in the predicate compiler
bulwahn
parents:
33522
diff
changeset
|
9 |
val define_predicates : (string * thm list) list -> theory -> (string * thm list) list * theory |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
10 |
val rewrite_intro : theory -> thm -> thm list |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
11 |
val pred_of_function : theory -> string -> string option |
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:
35021
diff
changeset
|
12 |
val add_function_predicate_translation : (term * term) -> theory -> theory |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
13 |
end; |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
14 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
15 |
structure Predicate_Compile_Fun : PREDICATE_COMPILE_FUN = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
16 |
struct |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
17 |
|
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset
|
18 |
open Predicate_Compile_Aux; |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
19 |
|
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:
35021
diff
changeset
|
20 |
(* Table from function to inductive predicate *) |
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:
35021
diff
changeset
|
21 |
structure Fun_Pred = Theory_Data |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
22 |
( |
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:
35021
diff
changeset
|
23 |
type T = (term * term) Item_Net.T; |
35411 | 24 |
val empty = Item_Net.init ((op aconv o pairself fst) : (term * term) * (term * term) -> bool) |
25 |
(single o fst); |
|
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
26 |
val extend = I; |
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:
35021
diff
changeset
|
27 |
val merge = Item_Net.merge; |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
28 |
) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
29 |
|
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:
35021
diff
changeset
|
30 |
fun lookup thy net 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:
35021
diff
changeset
|
31 |
case Item_Net.retrieve net t of |
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:
35021
diff
changeset
|
32 |
[] => NONE |
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:
35021
diff
changeset
|
33 |
| [(f, p)] => |
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:
35021
diff
changeset
|
34 |
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:
35021
diff
changeset
|
35 |
val subst = Pattern.match thy (f, t) (Vartab.empty, Vartab.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:
35021
diff
changeset
|
36 |
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:
35021
diff
changeset
|
37 |
SOME (Envir.subst_term subst p) |
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:
35021
diff
changeset
|
38 |
end |
35875 | 39 |
| _ => NONE |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
40 |
|
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:
35021
diff
changeset
|
41 |
fun pred_of_function thy name = |
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:
35021
diff
changeset
|
42 |
case Item_Net.retrieve (Fun_Pred.get thy) (Const (name, Term.dummyT)) of |
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:
35021
diff
changeset
|
43 |
[] => NONE |
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:
35021
diff
changeset
|
44 |
| [(f, p)] => SOME (fst (dest_Const p)) |
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:
35021
diff
changeset
|
45 |
| _ => error ("Multiple matches possible for lookup of constant " ^ name) |
33250
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:
35021
diff
changeset
|
47 |
fun defined_const thy name = is_some (pred_of_function thy name) |
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:
35021
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:
35021
diff
changeset
|
49 |
fun add_function_predicate_translation (f, p) = |
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:
35021
diff
changeset
|
50 |
Fun_Pred.map (Item_Net.update (f, p)) |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
51 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
52 |
fun transform_ho_typ (T as Type ("fun", _)) = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
53 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
54 |
val (Ts, T') = strip_type T |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
55 |
in if T' = @{typ "bool"} then T else (Ts @ [T']) ---> HOLogic.boolT end |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
56 |
| transform_ho_typ t = t |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
57 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
58 |
fun transform_ho_arg arg = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
59 |
case (fastype_of arg) of |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
60 |
(T as Type ("fun", _)) => |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
61 |
(case arg of |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
62 |
Free (name, _) => Free (name, transform_ho_typ T) |
35878 | 63 |
| _ => raise Fail "A non-variable term at a higher-order position") |
64 |
| _ => arg |
|
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
65 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
66 |
fun pred_type T = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
67 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
68 |
val (Ts, T') = strip_type T |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
69 |
val Ts' = map transform_ho_typ Ts |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
70 |
in |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
71 |
(Ts' @ [T']) ---> HOLogic.boolT |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
72 |
end; |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
73 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
74 |
(* FIXME: create new predicate name -- does not avoid nameclashing *) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
75 |
fun pred_of f = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
76 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
77 |
val (name, T) = dest_Const f |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
78 |
in |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
79 |
if (body_type T = @{typ bool}) then |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
80 |
(Free (Long_Name.base_name name ^ "P", T)) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
81 |
else |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
82 |
(Free (Long_Name.base_name name ^ "P", pred_type T)) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
83 |
end |
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 |
(* creates the list of premises for every intro rule *) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
86 |
(* theory -> term -> (string list, term list list) *) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
87 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
88 |
fun dest_code_eqn eqn = let |
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35411
diff
changeset
|
89 |
val (lhs, rhs) = Logic.dest_equals (Logic.unvarify_global (Thm.prop_of eqn)) |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
90 |
val (func, args) = strip_comb lhs |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
91 |
in ((func, args), rhs) end; |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
92 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
93 |
(* TODO: does not work with higher order functions yet *) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
94 |
fun mk_rewr_eq (func, pred) = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
95 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
96 |
val (argTs, resT) = (strip_type (fastype_of func)) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
97 |
val nctxt = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
98 |
Name.make_context (Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) (func $ pred) []) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
99 |
val (argnames, nctxt') = Name.variants (replicate (length argTs) "a") nctxt |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
100 |
val ([resname], nctxt'') = Name.variants ["r"] nctxt' |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
101 |
val args = map Free (argnames ~~ argTs) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
102 |
val res = Free (resname, resT) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
103 |
in Logic.mk_equals |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
104 |
(HOLogic.mk_eq (res, list_comb (func, args)), list_comb (pred, args @ [res])) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
105 |
end; |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
106 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
107 |
fun folds_map f xs y = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
108 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
109 |
fun folds_map' acc [] y = [(rev acc, y)] |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
110 |
| folds_map' acc (x :: xs) y = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
111 |
maps (fn (x, y) => folds_map' (x :: acc) xs y) (f x y) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
112 |
in |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
113 |
folds_map' [] xs y |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
114 |
end; |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
115 |
|
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:
35021
diff
changeset
|
116 |
fun keep_functions 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:
35021
diff
changeset
|
117 |
case try dest_Const (fst (strip_comb t)) of |
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:
35021
diff
changeset
|
118 |
SOME (c, _) => Predicate_Compile_Data.keep_function 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:
35021
diff
changeset
|
119 |
| _ => false |
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:
35021
diff
changeset
|
120 |
|
35875 | 121 |
fun flatten thy lookup_pred t (names, prems) = |
122 |
let |
|
123 |
fun lift t (names, prems) = |
|
124 |
case lookup_pred (Envir.eta_contract t) of |
|
125 |
SOME pred => [(pred, (names, prems))] |
|
126 |
| NONE => |
|
127 |
let |
|
128 |
val (vars, body) = strip_abs t |
|
129 |
val _ = assert (fastype_of body = body_type (fastype_of body)) |
|
130 |
val absnames = Name.variant_list names (map fst vars) |
|
131 |
val frees = map2 (curry Free) absnames (map snd vars) |
|
132 |
val body' = subst_bounds (rev frees, body) |
|
133 |
val resname = Name.variant (absnames @ names) "res" |
|
134 |
val resvar = Free (resname, fastype_of body) |
|
135 |
val t = flatten' body' ([], []) |
|
136 |
|> map (fn (res, (inner_names, inner_prems)) => |
|
137 |
let |
|
138 |
fun mk_exists (x, T) t = HOLogic.mk_exists (x, T, t) |
|
139 |
val vTs = |
|
140 |
fold Term.add_frees inner_prems [] |
|
141 |
|> filter (fn (x, T) => member (op =) inner_names x) |
|
142 |
val t = |
|
143 |
fold mk_exists vTs |
|
144 |
(foldr1 HOLogic.mk_conj (HOLogic.mk_eq (res, resvar) :: |
|
145 |
map HOLogic.dest_Trueprop inner_prems)) |
|
146 |
in |
|
147 |
t |
|
148 |
end) |
|
149 |
|> foldr1 HOLogic.mk_disj |
|
150 |
|> fold lambda (resvar :: rev frees) |
|
151 |
in |
|
152 |
[(t, (names, prems))] |
|
153 |
end |
|
154 |
and flatten_or_lift (t, T) (names, prems) = |
|
155 |
if fastype_of t = T then |
|
156 |
flatten' t (names, prems) |
|
157 |
else |
|
158 |
(* note pred_type might be to general! *) |
|
159 |
if (pred_type (fastype_of t) = T) then |
|
160 |
lift t (names, prems) |
|
161 |
else |
|
162 |
error ("unexpected input for flatten or lift" ^ Syntax.string_of_term_global thy t ^ |
|
163 |
", " ^ Syntax.string_of_typ_global thy T) |
|
164 |
and flatten' (t as Const (name, T)) (names, prems) = [(t, (names, prems))] |
|
165 |
| flatten' (t as Free (f, T)) (names, prems) = [(t, (names, prems))] |
|
166 |
| flatten' (t as Abs _) (names, prems) = [(t, (names, prems))] |
|
167 |
| flatten' (t as _ $ _) (names, prems) = |
|
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:
35021
diff
changeset
|
168 |
if Predicate_Compile_Aux.is_constrt thy t orelse keep_functions thy t then |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
169 |
[(t, (names, prems))] |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
170 |
else |
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:
35021
diff
changeset
|
171 |
case (fst (strip_comb t)) of |
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:
35021
diff
changeset
|
172 |
Const (@{const_name "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:
35021
diff
changeset
|
173 |
(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:
35021
diff
changeset
|
174 |
val (_, [B, x, y]) = strip_comb 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:
35021
diff
changeset
|
175 |
in |
35875 | 176 |
flatten' B (names, prems) |
177 |
|> maps (fn (B', (names, prems)) => |
|
178 |
(flatten' x (names, prems) |
|
179 |
|> map (fn (res, (names, prems)) => (res, (names, (HOLogic.mk_Trueprop B') :: prems)))) |
|
180 |
@ (flatten' y (names, prems) |
|
181 |
|> map (fn (res, (names, prems)) => |
|
182 |
(* in general unsound! *) |
|
183 |
(res, (names, (HOLogic.mk_Trueprop (HOLogic.mk_not B')) :: prems))))) |
|
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:
35021
diff
changeset
|
184 |
end) |
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:
35021
diff
changeset
|
185 |
| Const (@{const_name "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:
35021
diff
changeset
|
186 |
(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:
35021
diff
changeset
|
187 |
val (_, [f, g]) = strip_comb 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:
35021
diff
changeset
|
188 |
in |
35874
bcfa6b4b21c6
renaming mk_prems to flatten in the function flattening
bulwahn
parents:
35873
diff
changeset
|
189 |
flatten' f (names, prems) |
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:
35021
diff
changeset
|
190 |
|> maps (fn (res, (names, prems)) => |
35874
bcfa6b4b21c6
renaming mk_prems to flatten in the function flattening
bulwahn
parents:
35873
diff
changeset
|
191 |
flatten' (betapply (g, res)) (names, prems)) |
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:
35021
diff
changeset
|
192 |
end) |
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:
35021
diff
changeset
|
193 |
| Const (@{const_name "split"}, _) => |
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:
35021
diff
changeset
|
194 |
(let |
35877
295e1af6c8dc
generalized split transformation in the function flattening
bulwahn
parents:
35876
diff
changeset
|
195 |
val (_, g :: res :: args) = strip_comb 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:
35021
diff
changeset
|
196 |
val [res1, res2] = Name.variant_list names ["res1", "res2"] |
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:
35021
diff
changeset
|
197 |
val (T1, T2) = HOLogic.dest_prodT (fastype_of res) |
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:
35021
diff
changeset
|
198 |
val (resv1, resv2) = (Free (res1, T1), Free (res2, T2)) |
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:
35021
diff
changeset
|
199 |
in |
35877
295e1af6c8dc
generalized split transformation in the function flattening
bulwahn
parents:
35876
diff
changeset
|
200 |
flatten' (betapplys (g, (resv1 :: resv2 :: args))) |
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:
35021
diff
changeset
|
201 |
(res1 :: res2 :: names, |
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:
35021
diff
changeset
|
202 |
HOLogic.mk_Trueprop (HOLogic.mk_eq (res, HOLogic.mk_prod (resv1, resv2))) :: prems) |
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:
35021
diff
changeset
|
203 |
end) |
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:
35021
diff
changeset
|
204 |
| _ => |
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:
35021
diff
changeset
|
205 |
if has_split_thm thy (fst (strip_comb t)) then |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
206 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
207 |
val (f, args) = strip_comb t |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
208 |
val split_thm = prepare_split_thm (ProofContext.init thy) (the (find_split_thm' thy f)) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
209 |
val (assms, concl) = Logic.strip_horn (Thm.prop_of split_thm) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
210 |
val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
211 |
val subst = Pattern.match thy (split_t, t) (Vartab.empty, Vartab.empty) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
212 |
val (_, split_args) = strip_comb split_t |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
213 |
val match = split_args ~~ args |
35874
bcfa6b4b21c6
renaming mk_prems to flatten in the function flattening
bulwahn
parents:
35873
diff
changeset
|
214 |
fun flatten_of_assm assm = |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
215 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
216 |
val (vTs, assm') = strip_all (Envir.beta_norm (Envir.subst_term subst assm)) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
217 |
val var_names = Name.variant_list names (map fst vTs) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
218 |
val vars = map Free (var_names ~~ (map snd vTs)) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
219 |
val (prems', pre_res) = Logic.strip_horn (subst_bounds (rev vars, assm')) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
220 |
val (_, [inner_t]) = strip_comb (HOLogic.dest_Trueprop pre_res) |
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:
35021
diff
changeset
|
221 |
val (lhss : term list, rhss) = |
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:
35021
diff
changeset
|
222 |
split_list (map (HOLogic.dest_eq o HOLogic.dest_Trueprop) prems') |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
223 |
in |
35874
bcfa6b4b21c6
renaming mk_prems to flatten in the function flattening
bulwahn
parents:
35873
diff
changeset
|
224 |
folds_map flatten' lhss (var_names @ names, prems) |
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:
35021
diff
changeset
|
225 |
|> map (fn (ress, (names, prems)) => |
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:
35021
diff
changeset
|
226 |
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:
35021
diff
changeset
|
227 |
val prems' = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (ress ~~ rhss) |
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:
35021
diff
changeset
|
228 |
in (names, prems' @ prems) end) |
35874
bcfa6b4b21c6
renaming mk_prems to flatten in the function flattening
bulwahn
parents:
35873
diff
changeset
|
229 |
|> maps (flatten' inner_t) |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
230 |
end |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
231 |
in |
35874
bcfa6b4b21c6
renaming mk_prems to flatten in the function flattening
bulwahn
parents:
35873
diff
changeset
|
232 |
maps flatten_of_assm assms |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
233 |
end |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
234 |
else |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
235 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
236 |
val (f, args) = strip_comb 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:
35021
diff
changeset
|
237 |
val args = map (Pattern.eta_long []) args |
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:
35021
diff
changeset
|
238 |
val _ = assert (fastype_of t = body_type (fastype_of t)) |
35875 | 239 |
val f' = lookup_pred f |
240 |
val Ts = case f' of |
|
35873 | 241 |
SOME pred => (fst (split_last (binder_types (fastype_of pred)))) |
35875 | 242 |
| NONE => binder_types (fastype_of f) |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
243 |
in |
35875 | 244 |
folds_map flatten_or_lift (args ~~ Ts) (names, prems) |> |
245 |
(case f' of |
|
246 |
NONE => |
|
247 |
map (fn (argvs, (names', prems')) => (list_comb (f, argvs), (names', prems'))) |
|
248 |
| SOME pred => |
|
249 |
map (fn (argvs, (names', prems')) => |
|
250 |
let |
|
251 |
fun lift_arg T t = |
|
252 |
if (fastype_of t) = T then t |
|
253 |
else |
|
254 |
let |
|
255 |
val _ = assert (T = |
|
256 |
(binder_types (fastype_of t) @ [@{typ bool}] ---> @{typ bool})) |
|
257 |
fun mk_if T (b, t, e) = |
|
258 |
Const (@{const_name If}, @{typ bool} --> T --> T --> T) $ b $ t $ e |
|
259 |
val Ts = binder_types (fastype_of t) |
|
35878 | 260 |
in |
35875 | 261 |
list_abs (map (pair "x") Ts @ [("b", @{typ bool})], |
262 |
mk_if @{typ bool} (list_comb (t, map Bound (length Ts downto 1)), |
|
263 |
HOLogic.mk_eq (@{term True}, Bound 0), |
|
264 |
HOLogic.mk_eq (@{term False}, Bound 0))) |
|
265 |
end |
|
266 |
val argvs' = map2 lift_arg Ts argvs |
|
267 |
val resname = Name.variant names' "res" |
|
268 |
val resvar = Free (resname, body_type (fastype_of t)) |
|
269 |
val prem = HOLogic.mk_Trueprop (list_comb (pred, argvs' @ [resvar])) |
|
270 |
in (resvar, (resname :: names', prem :: prems')) end)) |
|
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
271 |
end |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
272 |
in |
35875 | 273 |
map (apfst Envir.eta_contract) (flatten' (Pattern.eta_long [] t) (names, prems)) |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
274 |
end; |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
275 |
|
35878 | 276 |
(* assumption: mutual recursive predicates all have the same parameters. *) |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
277 |
fun define_predicates specs thy = |
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:
35021
diff
changeset
|
278 |
if forall (fn (const, _) => defined_const thy const) specs then |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
279 |
([], thy) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
280 |
else |
35876
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
281 |
let |
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
282 |
val consts = map fst specs |
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
283 |
val eqns = maps snd specs |
35878 | 284 |
(* create prednames *) |
35876
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
285 |
val ((funs, argss), rhss) = map_split dest_code_eqn eqns |>> split_list |
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
286 |
val argss' = map (map transform_ho_arg) argss |
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
287 |
fun is_lifted (t1, t2) = (fastype_of t2 = pred_type (fastype_of t1)) |
35878 | 288 |
(* FIXME: higher order arguments also occur in tuples! *) |
35876
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
289 |
val lifted_args = distinct (op =) (filter is_lifted (flat argss ~~ flat argss')) |
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
290 |
val preds = map pred_of funs |
35878 | 291 |
(* mapping from term (Free or Const) to term *) |
35876
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
292 |
val net = fold Item_Net.update |
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
293 |
((funs ~~ preds) @ lifted_args) |
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
294 |
(Fun_Pred.get thy) |
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
295 |
fun lookup_pred t = lookup thy net t |
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
296 |
(* create intro rules *) |
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
297 |
fun mk_intros ((func, pred), (args, rhs)) = |
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
298 |
if (body_type (fastype_of func) = @{typ bool}) then |
35878 | 299 |
(* TODO: preprocess predicate definition of rhs *) |
35876
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
300 |
[Logic.list_implies ([HOLogic.mk_Trueprop rhs], HOLogic.mk_Trueprop (list_comb (pred, args)))] |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
301 |
else |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
302 |
let |
35876
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
303 |
val names = Term.add_free_names rhs [] |
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
304 |
in flatten thy lookup_pred rhs (names, []) |
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
305 |
|> map (fn (resultt, (names', prems)) => |
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
306 |
Logic.list_implies (prems, HOLogic.mk_Trueprop (list_comb (pred, args @ [resultt])))) |
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
307 |
end |
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
308 |
fun mk_rewr_thm (func, pred) = @{thm refl} |
35878 | 309 |
val intr_ts = maps mk_intros ((funs ~~ preds) ~~ (argss' ~~ rhss)) |
310 |
val (ind_result, thy') = |
|
311 |
thy |
|
312 |
|> Sign.map_naming Name_Space.conceal |
|
313 |
|> Inductive.add_inductive_global |
|
314 |
{quiet_mode = false, verbose = false, alt_name = Binding.empty, coind = false, |
|
315 |
no_elim = false, no_ind = false, skip_mono = false, fork_mono = false} |
|
316 |
(map (fn (s, T) => |
|
317 |
((Binding.name s, T), NoSyn)) (distinct (op =) (map dest_Free preds))) |
|
318 |
(map (dest_Free o snd) lifted_args) |
|
319 |
(map (fn x => (Attrib.empty_binding, x)) intr_ts) |
|
320 |
[] |
|
321 |
||> Sign.restore_naming thy |
|
322 |
val prednames = map (fst o dest_Const) (#preds ind_result) |
|
323 |
(* add constants to my table *) |
|
324 |
val specs = map (fn predname => (predname, filter (Predicate_Compile_Aux.is_intro predname) |
|
325 |
(#intrs ind_result))) prednames |
|
326 |
val thy'' = Fun_Pred.map |
|
327 |
(fold Item_Net.update (map (apfst Logic.varify_global) |
|
328 |
(distinct (op =) funs ~~ (#preds ind_result)))) thy' |
|
35876
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
329 |
in |
35878 | 330 |
(specs, thy'') |
35876
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
331 |
end |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
332 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
333 |
fun rewrite_intro thy intro = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
334 |
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:
35021
diff
changeset
|
335 |
(*val _ = tracing ("Rewriting intro with registered mapping for: " ^ |
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:
35021
diff
changeset
|
336 |
commas (Symtab.keys (Pred_Compile_Preproc.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:
35021
diff
changeset
|
337 |
fun lookup_pred t = lookup thy (Fun_Pred.get thy) t |
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35411
diff
changeset
|
338 |
val intro_t = Logic.unvarify_global (prop_of intro) |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
339 |
val (prems, concl) = Logic.strip_horn intro_t |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
340 |
val frees = map fst (Term.add_frees intro_t []) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
341 |
fun rewrite prem names = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
342 |
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:
35021
diff
changeset
|
343 |
(*val _ = tracing ("Rewriting premise " ^ Syntax.string_of_term_global thy prem ^ "...")*) |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
344 |
val t = (HOLogic.dest_Trueprop prem) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
345 |
val (lit, mk_lit) = case try HOLogic.dest_not t of |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
346 |
SOME t => (t, HOLogic.mk_not) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
347 |
| NONE => (t, I) |
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:
35021
diff
changeset
|
348 |
val (P, args) = (strip_comb lit) |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
349 |
in |
35874
bcfa6b4b21c6
renaming mk_prems to flatten in the function flattening
bulwahn
parents:
35873
diff
changeset
|
350 |
folds_map (flatten thy lookup_pred) args (names, []) |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
351 |
|> map (fn (resargs, (names', prems')) => |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
352 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
353 |
val prem' = HOLogic.mk_Trueprop (mk_lit (list_comb (P, resargs))) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
354 |
in (prem'::prems', names') end) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
355 |
end |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
356 |
val intro_ts' = folds_map rewrite prems frees |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
357 |
|> maps (fn (prems', frees') => |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
358 |
rewrite concl frees' |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
359 |
|> map (fn (concl'::conclprems, _) => |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
360 |
Logic.list_implies ((flat prems') @ conclprems, concl'))) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
361 |
in |
35021
c839a4c670c6
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
34954
diff
changeset
|
362 |
map (Drule.export_without_context o Skip_Proof.make_thm thy) intro_ts' |
33630
68e058d061f5
removed unnecessary oracle in the predicate compiler
bulwahn
parents:
33522
diff
changeset
|
363 |
end |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
364 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
365 |
end; |