author | blanchet |
Wed, 24 Sep 2014 15:46:40 +0200 | |
changeset 58430 | 73df5884edcf |
parent 58429 | 0b94858325a5 |
child 58460 | a88eb33058f7 |
permissions | -rw-r--r-- |
58061 | 1 |
(* Title: HOL/Tools/SMT/smt_datatypes.ML |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
2 |
Author: Sascha Boehme, TU Muenchen |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
3 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
4 |
Collector functions for common type declarations and their representation |
58361 | 5 |
as (co)algebraic datatypes. |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
6 |
*) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
7 |
|
58061 | 8 |
signature SMT_DATATYPES = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
9 |
sig |
58429
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58428
diff
changeset
|
10 |
val add_decls: BNF_Util.fp_kind list -> typ -> |
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58428
diff
changeset
|
11 |
(BNF_Util.fp_kind * (typ * (term * term list) list)) list list * Proof.context -> |
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58428
diff
changeset
|
12 |
(BNF_Util.fp_kind * (typ * (term * term list) list)) list list * Proof.context |
57229 | 13 |
end; |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
14 |
|
58061 | 15 |
structure SMT_Datatypes: SMT_DATATYPES = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
16 |
struct |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
17 |
|
58362
cf32eb8001b8
register Isabelle selectors as SMT selectors when possible
blanchet
parents:
58361
diff
changeset
|
18 |
fun mk_selectors T Ts sels = |
cf32eb8001b8
register Isabelle selectors as SMT selectors when possible
blanchet
parents:
58361
diff
changeset
|
19 |
if null sels then |
cf32eb8001b8
register Isabelle selectors as SMT selectors when possible
blanchet
parents:
58361
diff
changeset
|
20 |
Variable.variant_fixes (replicate (length Ts) "select") |
cf32eb8001b8
register Isabelle selectors as SMT selectors when possible
blanchet
parents:
58361
diff
changeset
|
21 |
#>> map2 (fn U => fn n => Free (n, T --> U)) Ts |
cf32eb8001b8
register Isabelle selectors as SMT selectors when possible
blanchet
parents:
58361
diff
changeset
|
22 |
else |
cf32eb8001b8
register Isabelle selectors as SMT selectors when possible
blanchet
parents:
58361
diff
changeset
|
23 |
pair sels |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
24 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
25 |
|
57226 | 26 |
(* free constructor type declarations *) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
27 |
|
58362
cf32eb8001b8
register Isabelle selectors as SMT selectors when possible
blanchet
parents:
58361
diff
changeset
|
28 |
fun get_ctr_sugar_decl ({ctrs = ctrs0, selss = selss0, ...} : Ctr_Sugar.ctr_sugar) T Ts ctxt = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
29 |
let |
58362
cf32eb8001b8
register Isabelle selectors as SMT selectors when possible
blanchet
parents:
58361
diff
changeset
|
30 |
fun mk_constr ctr0 sels0 = |
cf32eb8001b8
register Isabelle selectors as SMT selectors when possible
blanchet
parents:
58361
diff
changeset
|
31 |
let |
cf32eb8001b8
register Isabelle selectors as SMT selectors when possible
blanchet
parents:
58361
diff
changeset
|
32 |
val sels = map (Ctr_Sugar.mk_disc_or_sel Ts) sels0 |
cf32eb8001b8
register Isabelle selectors as SMT selectors when possible
blanchet
parents:
58361
diff
changeset
|
33 |
val ctr = Ctr_Sugar.mk_ctr Ts ctr0 |
cf32eb8001b8
register Isabelle selectors as SMT selectors when possible
blanchet
parents:
58361
diff
changeset
|
34 |
val binder_Ts = binder_types (fastype_of ctr) |
cf32eb8001b8
register Isabelle selectors as SMT selectors when possible
blanchet
parents:
58361
diff
changeset
|
35 |
in |
cf32eb8001b8
register Isabelle selectors as SMT selectors when possible
blanchet
parents:
58361
diff
changeset
|
36 |
mk_selectors T binder_Ts sels #>> pair ctr |
57226 | 37 |
end |
58362
cf32eb8001b8
register Isabelle selectors as SMT selectors when possible
blanchet
parents:
58361
diff
changeset
|
38 |
|
cf32eb8001b8
register Isabelle selectors as SMT selectors when possible
blanchet
parents:
58361
diff
changeset
|
39 |
val selss = if has_duplicates (op aconv) (flat selss0) then [] else selss0 |
57226 | 40 |
in |
58362
cf32eb8001b8
register Isabelle selectors as SMT selectors when possible
blanchet
parents:
58361
diff
changeset
|
41 |
Ctr_Sugar_Util.fold_map2 mk_constr ctrs0 (Ctr_Sugar_Util.pad_list [] (length ctrs0) selss) ctxt |
57226 | 42 |
|>> (pair T #> single) |
43 |
end |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
44 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
45 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
46 |
(* typedef declarations *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
47 |
|
57213
9daec42f6784
fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
blanchet
parents:
56078
diff
changeset
|
48 |
fun get_typedef_decl (({Abs_name, Rep_name, abs_type, rep_type, ...}, {Abs_inverse, ...}) |
9daec42f6784
fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
blanchet
parents:
56078
diff
changeset
|
49 |
: Typedef.info) T Ts = |
9daec42f6784
fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
blanchet
parents:
56078
diff
changeset
|
50 |
if can (curry (op RS) @{thm UNIV_I}) Abs_inverse then |
9daec42f6784
fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
blanchet
parents:
56078
diff
changeset
|
51 |
let |
9daec42f6784
fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
blanchet
parents:
56078
diff
changeset
|
52 |
val env = snd (Term.dest_Type abs_type) ~~ Ts |
9daec42f6784
fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
blanchet
parents:
56078
diff
changeset
|
53 |
val instT = Term.map_atyps (perhaps (AList.lookup (op =) env)) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
54 |
|
57213
9daec42f6784
fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
blanchet
parents:
56078
diff
changeset
|
55 |
val constr = Const (Abs_name, instT (rep_type --> abs_type)) |
9daec42f6784
fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
blanchet
parents:
56078
diff
changeset
|
56 |
val select = Const (Rep_name, instT (abs_type --> rep_type)) |
9daec42f6784
fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
blanchet
parents:
56078
diff
changeset
|
57 |
in [(T, [(constr, [select])])] end |
9daec42f6784
fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
blanchet
parents:
56078
diff
changeset
|
58 |
else |
9daec42f6784
fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
blanchet
parents:
56078
diff
changeset
|
59 |
[] |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
60 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
61 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
62 |
(* collection of declarations *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
63 |
|
58427
cc1bab5558b0
gracefully handle types like 'enat' whose coinductive view is registered using 'free_constructors'
blanchet
parents:
58364
diff
changeset
|
64 |
val extN = "_ext" (* cf. "HOL/Tools/typedef.ML" *) |
58361 | 65 |
|
58429
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58428
diff
changeset
|
66 |
fun get_decls fps T n Ts ctxt = |
58361 | 67 |
let |
58427
cc1bab5558b0
gracefully handle types like 'enat' whose coinductive view is registered using 'free_constructors'
blanchet
parents:
58364
diff
changeset
|
68 |
fun maybe_typedef () = |
57226 | 69 |
(case Typedef.get_info ctxt n of |
70 |
[] => ([], ctxt) |
|
58429
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58428
diff
changeset
|
71 |
| info :: _ => (map (pair (hd fps)) (get_typedef_decl info T Ts), ctxt)) |
58361 | 72 |
in |
58427
cc1bab5558b0
gracefully handle types like 'enat' whose coinductive view is registered using 'free_constructors'
blanchet
parents:
58364
diff
changeset
|
73 |
(case BNF_FP_Def_Sugar.fp_sugar_of ctxt n of |
58429
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58428
diff
changeset
|
74 |
SOME {fp, fp_res = {Ts = fp_Ts, ...}, ctr_sugar, ...} => |
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58428
diff
changeset
|
75 |
if member (op =) fps fp then |
58428
e4e34dfc3e68
rule out nested (co)recursion for SMT (co)datatypes
blanchet
parents:
58427
diff
changeset
|
76 |
let |
e4e34dfc3e68
rule out nested (co)recursion for SMT (co)datatypes
blanchet
parents:
58427
diff
changeset
|
77 |
val ns = map (fst o dest_Type) fp_Ts |
e4e34dfc3e68
rule out nested (co)recursion for SMT (co)datatypes
blanchet
parents:
58427
diff
changeset
|
78 |
val mutual_fp_sugars = map_filter (BNF_FP_Def_Sugar.fp_sugar_of ctxt) ns |
e4e34dfc3e68
rule out nested (co)recursion for SMT (co)datatypes
blanchet
parents:
58427
diff
changeset
|
79 |
val Xs = map #X mutual_fp_sugars |
e4e34dfc3e68
rule out nested (co)recursion for SMT (co)datatypes
blanchet
parents:
58427
diff
changeset
|
80 |
val ctrXs_Tsss = map #ctrXs_Tss mutual_fp_sugars |
e4e34dfc3e68
rule out nested (co)recursion for SMT (co)datatypes
blanchet
parents:
58427
diff
changeset
|
81 |
|
58430 | 82 |
(* Datatypes nested through datatypes and codatatypes nested through codatatypes are |
83 |
allowed. So are mutually (co)recursive (co)datatypes. *) |
|
84 |
fun is_same_fp s = |
|
85 |
(case BNF_FP_Def_Sugar.fp_sugar_of ctxt s of |
|
86 |
SOME {fp = fp', ...} => fp' = fp |
|
87 |
| NONE => false) |
|
88 |
fun is_homogenously_nested_co_recursive (Type (s, Ts)) = |
|
89 |
forall (if is_same_fp s then is_homogenously_nested_co_recursive |
|
90 |
else not o BNF_FP_Rec_Sugar_Util.exists_subtype_in Xs) Ts |
|
91 |
| is_homogenously_nested_co_recursive _ = true |
|
58428
e4e34dfc3e68
rule out nested (co)recursion for SMT (co)datatypes
blanchet
parents:
58427
diff
changeset
|
92 |
in |
58430 | 93 |
if forall (forall (forall is_homogenously_nested_co_recursive)) ctrXs_Tsss then |
94 |
get_ctr_sugar_decl ctr_sugar T Ts ctxt |>> map (pair fp) |
|
95 |
else |
|
96 |
maybe_typedef () |
|
58428
e4e34dfc3e68
rule out nested (co)recursion for SMT (co)datatypes
blanchet
parents:
58427
diff
changeset
|
97 |
end |
e4e34dfc3e68
rule out nested (co)recursion for SMT (co)datatypes
blanchet
parents:
58427
diff
changeset
|
98 |
else |
e4e34dfc3e68
rule out nested (co)recursion for SMT (co)datatypes
blanchet
parents:
58427
diff
changeset
|
99 |
([], ctxt) |
58427
cc1bab5558b0
gracefully handle types like 'enat' whose coinductive view is registered using 'free_constructors'
blanchet
parents:
58364
diff
changeset
|
100 |
| NONE => |
58429
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58428
diff
changeset
|
101 |
if String.isSuffix extN n then |
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58428
diff
changeset
|
102 |
(* for records (FIXME: hack) *) |
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58428
diff
changeset
|
103 |
(case Ctr_Sugar.ctr_sugar_of ctxt n of |
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58428
diff
changeset
|
104 |
SOME ctr_sugar => |
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58428
diff
changeset
|
105 |
get_ctr_sugar_decl ctr_sugar T Ts ctxt |>> map (pair (hd fps)) |
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58428
diff
changeset
|
106 |
| NONE => maybe_typedef ()) |
58427
cc1bab5558b0
gracefully handle types like 'enat' whose coinductive view is registered using 'free_constructors'
blanchet
parents:
58364
diff
changeset
|
107 |
else |
58429
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58428
diff
changeset
|
108 |
maybe_typedef ()) |
58361 | 109 |
end |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
110 |
|
58429
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58428
diff
changeset
|
111 |
fun add_decls fps T (declss, ctxt) = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
112 |
let |
58429
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58428
diff
changeset
|
113 |
fun declared T = exists (exists (equal T o fst o snd)) |
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58428
diff
changeset
|
114 |
fun declared' T = exists (exists (equal T o fst o snd) o snd) |
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58428
diff
changeset
|
115 |
fun depends ds = exists (member (op =) (map (fst o snd) ds)) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
116 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
117 |
fun add (TFree _) = I |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
118 |
| add (TVar _) = I |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
119 |
| add (T as Type (@{type_name fun}, _)) = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
120 |
fold add (Term.body_type T :: Term.binder_types T) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
121 |
| add @{typ bool} = I |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
122 |
| add (T as Type (n, Ts)) = (fn (dss, ctxt1) => |
58429
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58428
diff
changeset
|
123 |
if declared T declss orelse declared' T dss then |
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58428
diff
changeset
|
124 |
(dss, ctxt1) |
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58428
diff
changeset
|
125 |
else if SMT_Builtin.is_builtin_typ_ext ctxt1 T then |
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58428
diff
changeset
|
126 |
(dss, ctxt1) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
127 |
else |
58429
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58428
diff
changeset
|
128 |
(case get_decls fps T n Ts ctxt1 of |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
129 |
([], _) => (dss, ctxt1) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
130 |
| (ds, ctxt2) => |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
131 |
let |
58429
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58428
diff
changeset
|
132 |
val constrTs = maps (map (snd o Term.dest_Const o fst) o snd o snd) ds |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
133 |
val Us = fold (union (op =) o Term.binder_types) constrTs [] |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
134 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
135 |
fun ins [] = [(Us, ds)] |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
136 |
| ins ((Uds as (Us', _)) :: Udss) = |
58364 | 137 |
if depends ds Us' then (Us, ds) :: Uds :: Udss else Uds :: ins Udss |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
138 |
in fold add Us (ins dss, ctxt2) end)) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
139 |
in add T ([], ctxt) |>> append declss o map snd end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
140 |
|
57229 | 141 |
end; |