author | wenzelm |
Mon, 03 May 2010 14:25:56 +0200 | |
changeset 36610 | bafd82950e24 |
parent 36246 | 43fecedff8cf |
child 37007 | 116670499530 |
permissions | -rw-r--r-- |
36032
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
2 |
Author: Lukas Bulwahn, TU Muenchen |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
3 |
|
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
4 |
Deriving specialised predicates and their intro rules |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
5 |
*) |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
6 |
|
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
7 |
signature PREDICATE_COMPILE_SPECIALISATION = |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
8 |
sig |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
9 |
val find_specialisations : string list -> (string * thm list) list -> theory -> (string * thm list) list * theory |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
10 |
end; |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
11 |
|
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
12 |
structure Predicate_Compile_Specialisation : PREDICATE_COMPILE_SPECIALISATION = |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
13 |
struct |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
14 |
|
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
15 |
open Predicate_Compile_Aux; |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
16 |
|
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
17 |
(* table of specialisations *) |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
18 |
structure Specialisations = Theory_Data |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
19 |
( |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
20 |
type T = (term * term) Item_Net.T; |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
21 |
val empty = Item_Net.init ((op aconv o pairself fst) : (term * term) * (term * term) -> bool) |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
22 |
(single o fst); |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
23 |
val extend = I; |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
24 |
val merge = Item_Net.merge; |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
25 |
) |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
26 |
|
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
27 |
fun specialisation_of thy atom = |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
28 |
Item_Net.retrieve (Specialisations.get thy) atom |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
29 |
|
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
30 |
fun print_specialisations thy = |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
31 |
tracing (cat_lines (map (fn (t, spec_t) => |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
32 |
Syntax.string_of_term_global thy t ^ " ~~~> " ^ Syntax.string_of_term_global thy spec_t) |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
33 |
(Item_Net.content (Specialisations.get thy)))) |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
34 |
|
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
35 |
fun import (pred, intros) args ctxt = |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
36 |
let |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
37 |
val thy = ProofContext.theory_of ctxt |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
38 |
val ((Tinst, intros'), ctxt') = Variable.importT intros ctxt |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
39 |
val pred' = fst (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl (prop_of (hd intros'))))) |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
40 |
val Ts = binder_types (fastype_of pred') |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
41 |
val argTs = map fastype_of args |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
42 |
val Tsubst = Type.raw_matches (argTs, Ts) Vartab.empty |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
43 |
val args' = map (Envir.subst_term_types Tsubst) args |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
44 |
in |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
45 |
(((pred', intros'), args'), ctxt') |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
46 |
end |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
47 |
|
36036
ea7d0df15be0
no specialisation for patterns with only tuples in the predicate compiler
bulwahn
parents:
36032
diff
changeset
|
48 |
(* patterns only constructed of variables and pairs/tuples are trivial constructor terms*) |
ea7d0df15be0
no specialisation for patterns with only tuples in the predicate compiler
bulwahn
parents:
36032
diff
changeset
|
49 |
fun is_nontrivial_constrt thy t = |
ea7d0df15be0
no specialisation for patterns with only tuples in the predicate compiler
bulwahn
parents:
36032
diff
changeset
|
50 |
let |
ea7d0df15be0
no specialisation for patterns with only tuples in the predicate compiler
bulwahn
parents:
36032
diff
changeset
|
51 |
val cnstrs = flat (maps |
ea7d0df15be0
no specialisation for patterns with only tuples in the predicate compiler
bulwahn
parents:
36032
diff
changeset
|
52 |
(map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd) |
ea7d0df15be0
no specialisation for patterns with only tuples in the predicate compiler
bulwahn
parents:
36032
diff
changeset
|
53 |
(Symtab.dest (Datatype.get_all thy))); |
ea7d0df15be0
no specialisation for patterns with only tuples in the predicate compiler
bulwahn
parents:
36032
diff
changeset
|
54 |
fun check t = (case strip_comb t of |
ea7d0df15be0
no specialisation for patterns with only tuples in the predicate compiler
bulwahn
parents:
36032
diff
changeset
|
55 |
(Var _, []) => (true, true) |
ea7d0df15be0
no specialisation for patterns with only tuples in the predicate compiler
bulwahn
parents:
36032
diff
changeset
|
56 |
| (Free _, []) => (true, true) |
ea7d0df15be0
no specialisation for patterns with only tuples in the predicate compiler
bulwahn
parents:
36032
diff
changeset
|
57 |
| (Const (@{const_name Pair}, _), ts) => |
ea7d0df15be0
no specialisation for patterns with only tuples in the predicate compiler
bulwahn
parents:
36032
diff
changeset
|
58 |
pairself (forall I) (split_list (map check ts)) |
ea7d0df15be0
no specialisation for patterns with only tuples in the predicate compiler
bulwahn
parents:
36032
diff
changeset
|
59 |
| (Const (s, T), ts) => (case (AList.lookup (op =) cnstrs s, body_type T) of |
ea7d0df15be0
no specialisation for patterns with only tuples in the predicate compiler
bulwahn
parents:
36032
diff
changeset
|
60 |
(SOME (i, Tname), Type (Tname', _)) => (false, |
ea7d0df15be0
no specialisation for patterns with only tuples in the predicate compiler
bulwahn
parents:
36032
diff
changeset
|
61 |
length ts = i andalso Tname = Tname' andalso forall (snd o check) ts) |
ea7d0df15be0
no specialisation for patterns with only tuples in the predicate compiler
bulwahn
parents:
36032
diff
changeset
|
62 |
| _ => (false, false)) |
ea7d0df15be0
no specialisation for patterns with only tuples in the predicate compiler
bulwahn
parents:
36032
diff
changeset
|
63 |
| _ => (false, false)) |
ea7d0df15be0
no specialisation for patterns with only tuples in the predicate compiler
bulwahn
parents:
36032
diff
changeset
|
64 |
in check t = (false, true) end; |
36032
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
65 |
|
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
66 |
fun specialise_intros black_list (pred, intros) pats thy = |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
67 |
let |
36610
bafd82950e24
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
wenzelm
parents:
36246
diff
changeset
|
68 |
val ctxt = ProofContext.init_global thy |
36032
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
69 |
val maxidx = fold (Term.maxidx_term o prop_of) intros ~1 |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
70 |
val pats = map (Logic.incr_indexes ([], maxidx + 1)) pats |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
71 |
val (((pred, intros), pats), ctxt') = import (pred, intros) pats ctxt |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
72 |
val intros_t = map prop_of intros |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
73 |
val result_pats = map Var (fold_rev Term.add_vars pats []) |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
74 |
fun mk_fresh_name names = |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
75 |
let |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
76 |
val name = |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
77 |
Name.variant names ("specialised_" ^ Long_Name.base_name (fst (dest_Const pred))) |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
78 |
val bname = Sign.full_bname thy name |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
79 |
in |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
80 |
if Sign.declared_const thy bname then |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
81 |
mk_fresh_name (name :: names) |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
82 |
else |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
83 |
bname |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
84 |
end |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
85 |
val constname = mk_fresh_name [] |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
86 |
val constT = map fastype_of result_pats ---> @{typ bool} |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
87 |
val specialised_const = Const (constname, constT) |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
88 |
val specialisation = |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
89 |
[(HOLogic.mk_Trueprop (list_comb (pred, pats)), |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
90 |
HOLogic.mk_Trueprop (list_comb (specialised_const, result_pats)))] |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
91 |
fun specialise_intro intro = |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
92 |
(let |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
93 |
val (prems, concl) = Logic.strip_horn (prop_of intro) |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
94 |
val env = Pattern.unify thy |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
95 |
(HOLogic.mk_Trueprop (list_comb (pred, pats)), concl) (Envir.empty 0) |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
96 |
val prems = map (Envir.norm_term env) prems |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
97 |
val args = map (Envir.norm_term env) result_pats |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
98 |
val concl = HOLogic.mk_Trueprop (list_comb (specialised_const, args)) |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
99 |
val intro = Logic.list_implies (prems, concl) |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
100 |
in |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
101 |
SOME intro |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
102 |
end handle Pattern.Unif => NONE) |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
103 |
val specialised_intros_t = map_filter I (map specialise_intro intros) |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
104 |
val thy' = Sign.add_consts_i [(Binding.name (Long_Name.base_name constname), constT, NoSyn)] thy |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
105 |
val specialised_intros = map (Skip_Proof.make_thm thy') specialised_intros_t |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
106 |
val exported_intros = Variable.exportT ctxt' ctxt specialised_intros |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
107 |
val [t, specialised_t] = Variable.exportT_terms ctxt' ctxt |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
108 |
[list_comb (pred, pats), list_comb (specialised_const, result_pats)] |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
109 |
val thy'' = Specialisations.map (Item_Net.update (t, specialised_t)) thy' |
36246
43fecedff8cf
added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
bulwahn
parents:
36052
diff
changeset
|
110 |
val optimised_intros = |
43fecedff8cf
added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
bulwahn
parents:
36052
diff
changeset
|
111 |
map_filter (Predicate_Compile_Aux.peephole_optimisation thy'') exported_intros |
43fecedff8cf
added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
bulwahn
parents:
36052
diff
changeset
|
112 |
val ([spec], thy''') = find_specialisations black_list [(constname, optimised_intros)] thy'' |
36032
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
113 |
val thy'''' = Predicate_Compile_Core.register_intros spec thy''' |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
114 |
in |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
115 |
thy'''' |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
116 |
end |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
117 |
|
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
118 |
and find_specialisations black_list specs thy = |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
119 |
let |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
120 |
val add_vars = fold_aterms (fn Var v => cons v | _ => I); |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
121 |
fun fresh_free T free_names = |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
122 |
let |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
123 |
val free_name = Name.variant free_names "x" |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
124 |
in |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
125 |
(Free (free_name, T), free_name :: free_names) |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
126 |
end |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
127 |
fun replace_term_and_restrict thy T t Tts free_names = |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
128 |
let |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
129 |
val (free, free_names') = fresh_free T free_names |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
130 |
val Tts' = map (apsnd (Pattern.rewrite_term thy [(t, free)] [])) Tts |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
131 |
val (ts', free_names'') = restrict_pattern' thy Tts' free_names' |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
132 |
in |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
133 |
(free :: ts', free_names'') |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
134 |
end |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
135 |
and restrict_pattern' thy [] free_names = ([], free_names) |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
136 |
| restrict_pattern' thy ((T, Free (x, _)) :: Tts) free_names = |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
137 |
let |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
138 |
val (ts', free_names') = restrict_pattern' thy Tts free_names |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
139 |
in |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
140 |
(Free (x, T) :: ts', free_names') |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
141 |
end |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
142 |
| restrict_pattern' thy ((T as TFree _, t) :: Tts) free_names = |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
143 |
replace_term_and_restrict thy T t Tts free_names |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
144 |
| restrict_pattern' thy ((T as Type (Tcon, Ts), t) :: Tts) free_names = |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
145 |
case Datatype_Data.get_constrs thy Tcon of |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
146 |
NONE => replace_term_and_restrict thy T t Tts free_names |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
147 |
| SOME constrs => (case strip_comb t of |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
148 |
(Const (s, _), ats) => (case AList.lookup (op =) constrs s of |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
149 |
SOME constr_T => |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
150 |
let |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
151 |
val (Ts', T') = strip_type constr_T |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
152 |
val Tsubst = Type.raw_match (T', T) Vartab.empty |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
153 |
val Ts = map (Envir.subst_type Tsubst) Ts' |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
154 |
val (bts', free_names') = restrict_pattern' thy ((Ts ~~ ats) @ Tts) free_names |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
155 |
val (ats', ts') = chop (length ats) bts' |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
156 |
in |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
157 |
(list_comb (Const (s, map fastype_of ats' ---> T), ats') :: ts', free_names') |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
158 |
end |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
159 |
| NONE => replace_term_and_restrict thy T t Tts free_names)) |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
160 |
fun restrict_pattern thy Ts args = |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
161 |
let |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
162 |
val args = map Logic.unvarify_global args |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
163 |
val Ts = map Logic.unvarifyT_global Ts |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
164 |
val free_names = fold Term.add_free_names args [] |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
165 |
val (pat, _) = restrict_pattern' thy (Ts ~~ args) free_names |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
166 |
in map Logic.varify_global pat end |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
167 |
fun detect' atom thy = |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
168 |
case strip_comb atom of |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
169 |
(pred as Const (pred_name, _), args) => |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
170 |
let |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
171 |
val Ts = binder_types (Sign.the_const_type thy pred_name) |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
172 |
val vnames = map fst (fold Term.add_var_names args []) |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
173 |
val pats = restrict_pattern thy Ts args |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
174 |
in |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
175 |
if (exists (is_nontrivial_constrt thy) pats) |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
176 |
orelse (has_duplicates (op =) (fold add_vars pats [])) then |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
177 |
let |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
178 |
val thy' = |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
179 |
case specialisation_of thy atom of |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
180 |
[] => |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
181 |
if member (op =) ((map fst specs) @ black_list) pred_name then |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
182 |
thy |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
183 |
else |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
184 |
(case try (Predicate_Compile_Core.intros_of thy) pred_name of |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
185 |
NONE => thy |
36052
c240b2a5df90
no specialisation for predicates without introduction rules in the predicate compiler
bulwahn
parents:
36036
diff
changeset
|
186 |
| SOME [] => thy |
36032
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
187 |
| SOME intros => |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
188 |
specialise_intros ((map fst specs) @ (pred_name :: black_list)) |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
189 |
(pred, intros) pats thy) |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
190 |
| (t, specialised_t) :: _ => thy |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
191 |
val atom' = |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
192 |
case specialisation_of thy' atom of |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
193 |
[] => atom |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
194 |
| (t, specialised_t) :: _ => |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
195 |
let |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
196 |
val subst = Pattern.match thy' (t, atom) (Vartab.empty, Vartab.empty) |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
197 |
in Envir.subst_term subst specialised_t end handle Pattern.MATCH => atom |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
198 |
(*FIXME: this exception could be caught earlier in specialisation_of *) |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
199 |
in |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
200 |
(atom', thy') |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
201 |
end |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
202 |
else (atom, thy) |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
203 |
end |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
204 |
| _ => (atom, thy) |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
205 |
fun specialise' (constname, intros) thy = |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
206 |
let |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
207 |
(* FIXME: only necessary because of sloppy Logic.unvarify in restrict_pattern *) |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
208 |
val intros = Drule.zero_var_indexes_list intros |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
209 |
val (intros_t', thy') = (fold_map o fold_map_atoms) detect' (map prop_of intros) thy |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
210 |
in |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
211 |
((constname, map (Skip_Proof.make_thm thy') intros_t'), thy') |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
212 |
end |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
213 |
in |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
214 |
fold_map specialise' specs thy |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
215 |
end |
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
216 |
|
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
diff
changeset
|
217 |
end; |