author | wenzelm |
Thu, 15 Oct 2009 23:28:10 +0200 | |
changeset 32952 | aeb1e44fbc19 |
parent 32950 | 5d5e123443b3 |
child 33149 | 2c8f1c450b47 |
permissions | -rw-r--r-- |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
1 |
(* Author: Lukas Bulwahn, TU Muenchen |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
2 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
3 |
Preprocessing functions to predicates |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
4 |
*) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
5 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
6 |
signature PREDICATE_COMPILE_FUN = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
7 |
sig |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
8 |
val define_predicates : (string * thm list) list -> theory -> theory |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
9 |
val rewrite_intro : theory -> thm -> thm list |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
10 |
val setup_oracle : theory -> theory |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
11 |
end; |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
12 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
13 |
structure Predicate_Compile_Fun : PREDICATE_COMPILE_FUN = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
14 |
struct |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
15 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
16 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
17 |
(* Oracle for preprocessing *) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
18 |
|
32740 | 19 |
val (oracle : (string * (cterm -> thm)) option Unsynchronized.ref) = Unsynchronized.ref NONE; |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
20 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
21 |
fun the_oracle () = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
22 |
case !oracle of |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
23 |
NONE => error "Oracle is not setup" |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
24 |
| SOME (_, oracle) => oracle |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
25 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
26 |
val setup_oracle = Thm.add_oracle (Binding.name "pred_compile_preprocessing", I) #-> |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
27 |
(fn ora => fn thy => let val _ = (oracle := SOME ora) in thy end) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
28 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
29 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
30 |
fun is_funtype (Type ("fun", [_, _])) = true |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
31 |
| is_funtype _ = false; |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
32 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
33 |
fun is_Type (Type _) = true |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
34 |
| is_Type _ = false |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
35 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
36 |
(* returns true if t is an application of an datatype constructor *) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
37 |
(* which then consequently would be splitted *) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
38 |
(* else false *) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
39 |
(* |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
40 |
fun is_constructor thy t = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
41 |
if (is_Type (fastype_of t)) then |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
42 |
(case DatatypePackage.get_datatype thy ((fst o dest_Type o fastype_of) t) of |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
43 |
NONE => false |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
44 |
| SOME info => (let |
32952 | 45 |
val constr_consts = maps (fn (_, (_, _, constrs)) => map fst constrs) (#descr info) |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
46 |
val (c, _) = strip_comb t |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
47 |
in (case c of |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
48 |
Const (name, _) => name mem_string constr_consts |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
49 |
| _ => false) end)) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
50 |
else false |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
51 |
*) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
52 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
53 |
(* must be exported in code.ML *) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
54 |
fun is_constr thy = is_some o Code.get_datatype_of_constr thy; |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
55 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
56 |
(* Table from constant name (string) to term of inductive predicate *) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
57 |
structure Pred_Compile_Preproc = TheoryDataFun |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
58 |
( |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
59 |
type T = string Symtab.table; |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
60 |
val empty = Symtab.empty; |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
61 |
val copy = I; |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
62 |
val extend = I; |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
63 |
fun merge _ = Symtab.merge (op =); |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
64 |
) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
65 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
66 |
fun defined thy = Symtab.defined (Pred_Compile_Preproc.get thy) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
67 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
68 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
69 |
fun transform_ho_typ (T as Type ("fun", _)) = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
70 |
let |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
71 |
val (Ts, T') = strip_type T |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
72 |
in if T' = @{typ "bool"} then T else (Ts @ [T']) ---> HOLogic.boolT end |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
73 |
| transform_ho_typ t = t |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
74 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
75 |
fun transform_ho_arg arg = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
76 |
case (fastype_of arg) of |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
77 |
(T as Type ("fun", _)) => |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
78 |
(case arg of |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
79 |
Free (name, _) => Free (name, transform_ho_typ T) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
80 |
| _ => error "I am surprised") |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
81 |
| _ => arg |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
82 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
83 |
fun pred_type T = |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
84 |
let |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
85 |
val (Ts, T') = strip_type T |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
86 |
val Ts' = map transform_ho_typ Ts |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
87 |
in |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
88 |
(Ts' @ [T']) ---> HOLogic.boolT |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
89 |
end; |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
90 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
91 |
(* FIXME: create new predicate name -- does not avoid nameclashing *) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
92 |
fun pred_of f = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
93 |
let |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
94 |
val (name, T) = dest_Const f |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
95 |
in |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
96 |
if (body_type T = @{typ bool}) then |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
97 |
(Free (Long_Name.base_name name ^ "P", T)) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
98 |
else |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
99 |
(Free (Long_Name.base_name name ^ "P", pred_type T)) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
100 |
end |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
101 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
102 |
fun mk_param lookup_pred (t as Free (v, _)) = lookup_pred t |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
103 |
| mk_param lookup_pred t = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
104 |
let |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
105 |
val (vs, body) = strip_abs t |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
106 |
val names = Term.add_free_names body [] |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
107 |
val vs_names = Name.variant_list names (map fst vs) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
108 |
val vs' = map2 (curry Free) vs_names (map snd vs) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
109 |
val body' = subst_bounds (rev vs', body) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
110 |
val (f, args) = strip_comb body' |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
111 |
val resname = Name.variant (vs_names @ names) "res" |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
112 |
val resvar = Free (resname, body_type (fastype_of body')) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
113 |
val P = lookup_pred f |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
114 |
val pred_body = list_comb (P, args @ [resvar]) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
115 |
val param = fold_rev lambda (vs' @ [resvar]) pred_body |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
116 |
in param end; |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
117 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
118 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
119 |
(* creates the list of premises for every intro rule *) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
120 |
(* theory -> term -> (string list, term list list) *) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
121 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
122 |
fun dest_code_eqn eqn = let |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
123 |
val (lhs, rhs) = Logic.dest_equals (Logic.unvarify (Thm.prop_of eqn)) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
124 |
val (func, args) = strip_comb lhs |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
125 |
in ((func, args), rhs) end; |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
126 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
127 |
fun string_of_typ T = Syntax.string_of_typ_global @{theory} T |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
128 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
129 |
fun string_of_term t = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
130 |
case t of |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
131 |
Const (c, T) => "Const (" ^ c ^ ", " ^ string_of_typ T ^ ")" |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
132 |
| Free (c, T) => "Free (" ^ c ^ ", " ^ string_of_typ T ^ ")" |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
133 |
| Var ((c, i), T) => "Var ((" ^ c ^ ", " ^ string_of_int i ^ "), " ^ string_of_typ T ^ ")" |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
134 |
| Bound i => "Bound " ^ string_of_int i |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
135 |
| Abs (x, T, t) => "Abs (" ^ x ^ ", " ^ string_of_typ T ^ ", " ^ string_of_term t ^ ")" |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
136 |
| t1 $ t2 => "(" ^ string_of_term t1 ^ ") $ (" ^ string_of_term t2 ^ ")" |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
137 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
138 |
fun ind_package_get_nparams thy name = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
139 |
case try (Inductive.the_inductive (ProofContext.init thy)) name of |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
140 |
SOME (_, result) => length (Inductive.params_of (#raw_induct result)) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
141 |
| NONE => error ("No such predicate: " ^ quote name) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
142 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
143 |
(* TODO: does not work with higher order functions yet *) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
144 |
fun mk_rewr_eq (func, pred) = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
145 |
let |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
146 |
val (argTs, resT) = (strip_type (fastype_of func)) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
147 |
val nctxt = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
148 |
Name.make_context (Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) (func $ pred) []) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
149 |
val (argnames, nctxt') = Name.variants (replicate (length argTs) "a") nctxt |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
150 |
val ([resname], nctxt'') = Name.variants ["r"] nctxt' |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
151 |
val args = map Free (argnames ~~ argTs) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
152 |
val res = Free (resname, resT) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
153 |
in Logic.mk_equals |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
154 |
(HOLogic.mk_eq (res, list_comb (func, args)), list_comb (pred, args @ [res])) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
155 |
end; |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
156 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
157 |
fun has_split_rule_cname @{const_name "nat_case"} = true |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
158 |
| has_split_rule_cname @{const_name "list_case"} = true |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
159 |
| has_split_rule_cname _ = false |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
160 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
161 |
fun has_split_rule_term thy (Const (@{const_name "nat_case"}, _)) = true |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
162 |
| has_split_rule_term thy (Const (@{const_name "list_case"}, _)) = true |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
163 |
| has_split_rule_term thy _ = false |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
164 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
165 |
fun has_split_rule_term' thy (Const (@{const_name "If"}, _)) = true |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
166 |
| has_split_rule_term' thy (Const (@{const_name "Let"}, _)) = true |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
167 |
| has_split_rule_term' thy c = has_split_rule_term thy c |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
168 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
169 |
fun prepare_split_thm ctxt split_thm = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
170 |
(split_thm RS @{thm iffD2}) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
171 |
|> LocalDefs.unfold ctxt [@{thm atomize_conjL[symmetric]}, |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
172 |
@{thm atomize_all[symmetric]}, @{thm atomize_imp[symmetric]}] |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
173 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
174 |
fun find_split_thm thy (Const (name, typ)) = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
175 |
let |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
176 |
fun split_name str = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
177 |
case first_field "." str |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
178 |
of (SOME (field, rest)) => field :: split_name rest |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
179 |
| NONE => [str] |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
180 |
val splitted_name = split_name name |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
181 |
in |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
182 |
if length splitted_name > 0 andalso |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
183 |
String.isSuffix "_case" (List.last splitted_name) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
184 |
then |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
185 |
(List.take (splitted_name, length splitted_name - 1)) @ ["split"] |
32952 | 186 |
|> space_implode "." |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
187 |
|> PureThy.get_thm thy |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
188 |
|> SOME |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
189 |
handle ERROR msg => NONE |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
190 |
else NONE |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
191 |
end |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
192 |
| find_split_thm _ _ = NONE |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
193 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
194 |
fun find_split_thm' thy (Const (@{const_name "If"}, _)) = SOME @{thm split_if} |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
195 |
| find_split_thm' thy (Const (@{const_name "Let"}, _)) = SOME @{thm refl} (* TODO *) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
196 |
| find_split_thm' thy c = find_split_thm thy c |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
197 |
|
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
198 |
fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
199 |
|
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
200 |
fun folds_map f xs y = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
201 |
let |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
202 |
fun folds_map' acc [] y = [(rev acc, y)] |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
203 |
| folds_map' acc (x :: xs) y = |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
204 |
maps (fn (x, y) => folds_map' (x :: acc) xs y) (f x y) |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
205 |
in |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
206 |
folds_map' [] xs y |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
207 |
end; |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
208 |
|
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
209 |
fun mk_prems thy (lookup_pred, get_nparams) t (names, prems) = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
210 |
let |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
211 |
fun mk_prems' (t as Const (name, T)) (names, prems) = |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
212 |
if is_constr thy name orelse (is_none (try lookup_pred t)) then |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
213 |
[(t ,(names, prems))] |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
214 |
else [(lookup_pred t, (names, prems))] |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
215 |
| mk_prems' (t as Free (f, T)) (names, prems) = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
216 |
[(lookup_pred t, (names, prems))] |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
217 |
| mk_prems' t (names, prems) = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
218 |
if Predicate_Compile_Aux.is_constrt thy t then |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
219 |
[(t, (names, prems))] |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
220 |
else |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
221 |
if has_split_rule_term' thy (fst (strip_comb t)) then |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
222 |
let |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
223 |
val (f, args) = strip_comb t |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
224 |
val split_thm = prepare_split_thm (ProofContext.init thy) (the (find_split_thm' thy f)) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
225 |
(* TODO: contextify things - this line is to unvarify the split_thm *) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
226 |
(*val ((_, [isplit_thm]), _) = Variable.import true [split_thm] (ProofContext.init thy)*) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
227 |
val (assms, concl) = Logic.strip_horn (Thm.prop_of split_thm) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
228 |
val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
229 |
val subst = Pattern.match thy (split_t, t) (Vartab.empty, Vartab.empty) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
230 |
val (_, split_args) = strip_comb split_t |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
231 |
val match = split_args ~~ args |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
232 |
fun mk_prems_of_assm assm = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
233 |
let |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
234 |
val (vTs, assm') = strip_all (Envir.beta_norm (Envir.subst_term subst assm)) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
235 |
val var_names = Name.variant_list names (map fst vTs) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
236 |
val vars = map Free (var_names ~~ (map snd vTs)) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
237 |
val (prems', pre_res) = Logic.strip_horn (subst_bounds (rev vars, assm')) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
238 |
val (_, [inner_t]) = strip_comb (HOLogic.dest_Trueprop pre_res) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
239 |
in |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
240 |
mk_prems' inner_t (var_names @ names, prems' @ prems) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
241 |
end |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
242 |
in |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
243 |
maps mk_prems_of_assm assms |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
244 |
end |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
245 |
else |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
246 |
let |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
247 |
val (f, args) = strip_comb t |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
248 |
val resname = Name.variant names "res" |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
249 |
val resvar = Free (resname, body_type (fastype_of t)) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
250 |
val names' = resname :: names |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
251 |
fun mk_prems'' (t as Const (c, _)) = |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
252 |
if is_constr thy c orelse (is_none (try lookup_pred t)) then |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
253 |
folds_map mk_prems' args (names', prems) |> |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
254 |
map |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
255 |
(fn (argvs, (names'', prems')) => |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
256 |
let |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
257 |
val prem = HOLogic.mk_Trueprop (HOLogic.mk_eq (resvar, list_comb (f, argvs))) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
258 |
in (names'', prem :: prems') end) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
259 |
else |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
260 |
let |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
261 |
val pred = lookup_pred t |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
262 |
val nparams = get_nparams pred |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
263 |
val (params, args) = chop nparams args |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
264 |
val _ = tracing ("mk_prems'': " ^ (Syntax.string_of_term_global thy t) ^ " has " ^ string_of_int nparams ^ " parameters.") |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
265 |
val params' = map (mk_param lookup_pred) params |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
266 |
in |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
267 |
folds_map mk_prems' args (names', prems) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
268 |
|> map (fn (argvs, (names'', prems')) => |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
269 |
let |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
270 |
val prem = HOLogic.mk_Trueprop (list_comb (pred, params' @ argvs @ [resvar])) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
271 |
in (names'', prem :: prems') end) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
272 |
end |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
273 |
| mk_prems'' (t as Free (_, _)) = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
274 |
let |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
275 |
(* higher order argument call *) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
276 |
val pred = lookup_pred t |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
277 |
in |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
278 |
folds_map mk_prems' args (resname :: names, prems) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
279 |
|> map (fn (argvs, (names', prems')) => |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
280 |
let |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
281 |
val prem = HOLogic.mk_Trueprop (list_comb (pred, argvs @ [resvar])) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
282 |
in (names', prem :: prems') end) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
283 |
end |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
284 |
| mk_prems'' t = error ("Invalid term: " ^ Syntax.string_of_term_global thy t) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
285 |
in |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
286 |
map (pair resvar) (mk_prems'' f) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
287 |
end |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
288 |
in |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
289 |
mk_prems' t (names, prems) |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
290 |
end; |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
291 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
292 |
(* assumption: mutual recursive predicates all have the same parameters. *) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
293 |
fun define_predicates specs thy = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
294 |
if forall (fn (const, _) => member (op =) (Symtab.keys (Pred_Compile_Preproc.get thy)) const) specs then |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
295 |
thy |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
296 |
else |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
297 |
let |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
298 |
val consts = map fst specs |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
299 |
val eqns = maps snd specs |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
300 |
(*val eqns = maps (Predicate_Compile_Preproc_Data.get_specification thy) consts*) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
301 |
(* create prednames *) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
302 |
val ((funs, argss), rhss) = map_split dest_code_eqn eqns |>> split_list |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
303 |
val argss' = map (map transform_ho_arg) argss |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
304 |
val pnames = map dest_Free (distinct (op =) (maps (filter (is_funtype o fastype_of)) argss')) |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
305 |
val preds = map pred_of funs |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
306 |
val prednames = map (fst o dest_Free) preds |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
307 |
val funnames = map (fst o dest_Const) funs |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
308 |
val fun_pred_names = (funnames ~~ prednames) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
309 |
(* mapping from term (Free or Const) to term *) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
310 |
fun lookup_pred (Const (@{const_name Cons}, T)) = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
311 |
Const ("Preprocessing.ConsP", pred_type T) (* FIXME: temporary - Cons lookup *) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
312 |
| lookup_pred (Const (name, T)) = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
313 |
(case (Symtab.lookup (Pred_Compile_Preproc.get thy) name) of |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
314 |
SOME c => Const (c, pred_type T) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
315 |
| NONE => |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
316 |
(case AList.lookup op = fun_pred_names name of |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
317 |
SOME f => Free (f, pred_type T) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
318 |
| NONE => Const (name, T))) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
319 |
| lookup_pred (Free (name, T)) = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
320 |
if member op = (map fst pnames) name then |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
321 |
Free (name, transform_ho_typ T) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
322 |
else |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
323 |
Free (name, T) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
324 |
| lookup_pred t = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
325 |
error ("lookup function is not defined for " ^ Syntax.string_of_term_global thy t) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
326 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
327 |
(* mapping from term (predicate term, not function term!) to int *) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
328 |
fun get_nparams (Const (name, _)) = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
329 |
the_default 0 (try (ind_package_get_nparams thy) name) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
330 |
| get_nparams (Free (name, _)) = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
331 |
(if member op = prednames name then |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
332 |
length pnames |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
333 |
else 0) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
334 |
| get_nparams t = error ("No parameters for " ^ (Syntax.string_of_term_global thy t)) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
335 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
336 |
(* create intro rules *) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
337 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
338 |
fun mk_intros ((func, pred), (args, rhs)) = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
339 |
if (body_type (fastype_of func) = @{typ bool}) then |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
340 |
(*TODO: preprocess predicate definition of rhs *) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
341 |
[Logic.list_implies ([HOLogic.mk_Trueprop rhs], HOLogic.mk_Trueprop (list_comb (pred, args)))] |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
342 |
else |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
343 |
let |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
344 |
val names = Term.add_free_names rhs [] |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
345 |
in mk_prems thy (lookup_pred, get_nparams) rhs (names, []) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
346 |
|> map (fn (resultt, (names', prems)) => |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
347 |
Logic.list_implies (prems, HOLogic.mk_Trueprop (list_comb (pred, args @ [resultt])))) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
348 |
end |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
349 |
fun mk_rewr_thm (func, pred) = @{thm refl} |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
350 |
in |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
351 |
case try (maps mk_intros) ((funs ~~ preds) ~~ (argss' ~~ rhss)) of |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
352 |
NONE => thy |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
353 |
| SOME intr_ts => let |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
354 |
val _ = map (tracing o (Syntax.string_of_term_global thy)) intr_ts |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
355 |
in |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
356 |
if is_some (try (map (cterm_of thy)) intr_ts) then |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
357 |
let |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
358 |
val (ind_result, thy') = |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
359 |
Inductive.add_inductive_global (serial_string ()) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
360 |
{quiet_mode = false, verbose = false, kind = Thm.internalK, |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
361 |
alt_name = Binding.empty, coind = false, no_elim = false, |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
362 |
no_ind = false, skip_mono = false, fork_mono = false} |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
363 |
(map (fn (s, T) => ((Binding.name s, T), NoSyn)) (distinct (op =) (map dest_Free preds))) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
364 |
pnames |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
365 |
(map (fn x => (Attrib.empty_binding, x)) intr_ts) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
366 |
[] thy |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
367 |
val prednames = map (fst o dest_Const) (#preds ind_result) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
368 |
(* val rewr_thms = map mk_rewr_eq ((distinct (op =) funs) ~~ (#preds ind_result)) *) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
369 |
(* add constants to my table *) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
370 |
in Pred_Compile_Preproc.map (fold Symtab.update_new (consts ~~ prednames)) thy' end |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
371 |
else |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
372 |
thy |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
373 |
end |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
374 |
end |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
375 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
376 |
(* preprocessing intro rules - uses oracle *) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
377 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
378 |
(* theory -> thm -> thm *) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
379 |
fun rewrite_intro thy intro = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
380 |
let |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
381 |
fun lookup_pred (Const (name, T)) = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
382 |
(case (Symtab.lookup (Pred_Compile_Preproc.get thy) name) of |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
383 |
SOME c => Const (c, pred_type T) |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
384 |
| NONE => error ("Function " ^ name ^ " is not inductified")) |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
385 |
| lookup_pred (Free (name, T)) = Free (name, T) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
386 |
| lookup_pred _ = error "lookup function is not defined!" |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
387 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
388 |
fun get_nparams (Const (name, _)) = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
389 |
the_default 0 (try (ind_package_get_nparams thy) name) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
390 |
| get_nparams (Free _) = 0 |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
391 |
| get_nparams t = error ("No parameters for " ^ (Syntax.string_of_term_global thy t)) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
392 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
393 |
val intro_t = (Logic.unvarify o prop_of) intro |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
394 |
val _ = tracing (Syntax.string_of_term_global thy intro_t) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
395 |
val (prems, concl) = Logic.strip_horn intro_t |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
396 |
val frees = map fst (Term.add_frees intro_t []) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
397 |
fun rewrite prem names = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
398 |
let |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
399 |
val t = (HOLogic.dest_Trueprop prem) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
400 |
val (lit, mk_lit) = case try HOLogic.dest_not t of |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
401 |
SOME t => (t, HOLogic.mk_not) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
402 |
| NONE => (t, I) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
403 |
val (P, args) = (strip_comb lit) |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
404 |
in |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
405 |
folds_map ( |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
406 |
fn t => if (is_funtype (fastype_of t)) then (fn x => [(t, x)]) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
407 |
else mk_prems thy (lookup_pred, get_nparams) t) args (names, []) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
408 |
|> map (fn (resargs, (names', prems')) => |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
409 |
let |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32668
diff
changeset
|
410 |
val prem' = HOLogic.mk_Trueprop (mk_lit (list_comb (P, resargs))) |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
411 |
in (prem'::prems', names') end) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
412 |
end |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
413 |
val intro_ts' = folds_map rewrite prems frees |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
414 |
|> maps (fn (prems', frees') => |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
415 |
rewrite concl frees' |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
416 |
|> map (fn (concl'::conclprems, _) => |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
417 |
Logic.list_implies ((flat prems') @ conclprems, concl'))) |
32950 | 418 |
val _ = tracing ("intro_ts': " ^ |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
419 |
commas (map (Syntax.string_of_term_global thy) intro_ts')) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
420 |
in |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
421 |
map (Drule.standard o the_oracle () o cterm_of thy) intro_ts' |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
422 |
end; |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
423 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
424 |
end; |