author | blanchet |
Fri, 04 Dec 2015 14:15:16 +0100 | |
changeset 61782 | 7d754aca6a75 |
parent 59143 | 15c342a9a8e0 |
child 67149 | e61557884799 |
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 |
59143
15c342a9a8e0
correctly apply type substitution before checking for function types
blanchet
parents:
59142
diff
changeset
|
30 |
val selss = map (map (Ctr_Sugar.mk_disc_or_sel Ts)) selss0 |
15c342a9a8e0
correctly apply type substitution before checking for function types
blanchet
parents:
59142
diff
changeset
|
31 |
val ctrs = map (Ctr_Sugar.mk_ctr Ts) ctrs0 |
15c342a9a8e0
correctly apply type substitution before checking for function types
blanchet
parents:
59142
diff
changeset
|
32 |
|
15c342a9a8e0
correctly apply type substitution before checking for function types
blanchet
parents:
59142
diff
changeset
|
33 |
fun mk_constr ctr sels = |
15c342a9a8e0
correctly apply type substitution before checking for function types
blanchet
parents:
59142
diff
changeset
|
34 |
mk_selectors T (binder_types (fastype_of ctr)) sels #>> pair ctr |
58362
cf32eb8001b8
register Isabelle selectors as SMT selectors when possible
blanchet
parents:
58361
diff
changeset
|
35 |
|
59143
15c342a9a8e0
correctly apply type substitution before checking for function types
blanchet
parents:
59142
diff
changeset
|
36 |
val selss' = |
15c342a9a8e0
correctly apply type substitution before checking for function types
blanchet
parents:
59142
diff
changeset
|
37 |
(if has_duplicates (op aconv) (flat selss) orelse |
15c342a9a8e0
correctly apply type substitution before checking for function types
blanchet
parents:
59142
diff
changeset
|
38 |
exists (exists (can (dest_funT o range_type o fastype_of))) selss then |
15c342a9a8e0
correctly apply type substitution before checking for function types
blanchet
parents:
59142
diff
changeset
|
39 |
[] |
15c342a9a8e0
correctly apply type substitution before checking for function types
blanchet
parents:
59142
diff
changeset
|
40 |
else |
15c342a9a8e0
correctly apply type substitution before checking for function types
blanchet
parents:
59142
diff
changeset
|
41 |
selss) |
15c342a9a8e0
correctly apply type substitution before checking for function types
blanchet
parents:
59142
diff
changeset
|
42 |
|> Ctr_Sugar_Util.pad_list [] (length ctrs) |
57226 | 43 |
in |
59143
15c342a9a8e0
correctly apply type substitution before checking for function types
blanchet
parents:
59142
diff
changeset
|
44 |
@{fold_map 2} mk_constr ctrs selss' ctxt |
57226 | 45 |
|>> (pair T #> single) |
46 |
end |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
47 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
48 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
49 |
(* typedef declarations *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
50 |
|
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
|
51 |
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
|
52 |
: 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
|
53 |
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
|
54 |
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
|
55 |
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
|
56 |
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
|
57 |
|
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
|
58 |
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
|
59 |
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
|
60 |
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
|
61 |
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
|
62 |
[] |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
63 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
64 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
65 |
(* collection of declarations *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
66 |
|
58427
cc1bab5558b0
gracefully handle types like 'enat' whose coinductive view is registered using 'free_constructors'
blanchet
parents:
58364
diff
changeset
|
67 |
val extN = "_ext" (* cf. "HOL/Tools/typedef.ML" *) |
58361 | 68 |
|
58429
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58428
diff
changeset
|
69 |
fun get_decls fps T n Ts ctxt = |
58361 | 70 |
let |
58427
cc1bab5558b0
gracefully handle types like 'enat' whose coinductive view is registered using 'free_constructors'
blanchet
parents:
58364
diff
changeset
|
71 |
fun maybe_typedef () = |
57226 | 72 |
(case Typedef.get_info ctxt n of |
73 |
[] => ([], ctxt) |
|
58429
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58428
diff
changeset
|
74 |
| info :: _ => (map (pair (hd fps)) (get_typedef_decl info T Ts), ctxt)) |
58361 | 75 |
in |
58427
cc1bab5558b0
gracefully handle types like 'enat' whose coinductive view is registered using 'free_constructors'
blanchet
parents:
58364
diff
changeset
|
76 |
(case BNF_FP_Def_Sugar.fp_sugar_of ctxt n of |
58460 | 77 |
SOME {fp, fp_res = {Ts = fp_Ts, ...}, fp_ctr_sugar = {ctr_sugar, ...}, ...} => |
58429
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58428
diff
changeset
|
78 |
if member (op =) fps fp then |
58428
e4e34dfc3e68
rule out nested (co)recursion for SMT (co)datatypes
blanchet
parents:
58427
diff
changeset
|
79 |
let |
e4e34dfc3e68
rule out nested (co)recursion for SMT (co)datatypes
blanchet
parents:
58427
diff
changeset
|
80 |
val ns = map (fst o dest_Type) fp_Ts |
e4e34dfc3e68
rule out nested (co)recursion for SMT (co)datatypes
blanchet
parents:
58427
diff
changeset
|
81 |
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
|
82 |
val Xs = map #X mutual_fp_sugars |
58460 | 83 |
val ctrXs_Tsss = map (#ctrXs_Tss o #fp_ctr_sugar) mutual_fp_sugars |
58428
e4e34dfc3e68
rule out nested (co)recursion for SMT (co)datatypes
blanchet
parents:
58427
diff
changeset
|
84 |
|
58430 | 85 |
(* Datatypes nested through datatypes and codatatypes nested through codatatypes are |
86 |
allowed. So are mutually (co)recursive (co)datatypes. *) |
|
87 |
fun is_same_fp s = |
|
88 |
(case BNF_FP_Def_Sugar.fp_sugar_of ctxt s of |
|
89 |
SOME {fp = fp', ...} => fp' = fp |
|
90 |
| NONE => false) |
|
91 |
fun is_homogenously_nested_co_recursive (Type (s, Ts)) = |
|
92 |
forall (if is_same_fp s then is_homogenously_nested_co_recursive |
|
93 |
else not o BNF_FP_Rec_Sugar_Util.exists_subtype_in Xs) Ts |
|
94 |
| is_homogenously_nested_co_recursive _ = true |
|
59020
a86683d6c97e
work around bug in CVC4, with boolean arguments to (co)datatypes
blanchet
parents:
58634
diff
changeset
|
95 |
|
a86683d6c97e
work around bug in CVC4, with boolean arguments to (co)datatypes
blanchet
parents:
58634
diff
changeset
|
96 |
val Type (_, As) :: _ = fp_Ts |
a86683d6c97e
work around bug in CVC4, with boolean arguments to (co)datatypes
blanchet
parents:
58634
diff
changeset
|
97 |
val substAs = Term.typ_subst_atomic (As ~~ Ts); |
58428
e4e34dfc3e68
rule out nested (co)recursion for SMT (co)datatypes
blanchet
parents:
58427
diff
changeset
|
98 |
in |
59020
a86683d6c97e
work around bug in CVC4, with boolean arguments to (co)datatypes
blanchet
parents:
58634
diff
changeset
|
99 |
(* TODO/FIXME: The "bool" check is there to work around a CVC4 bug |
a86683d6c97e
work around bug in CVC4, with boolean arguments to (co)datatypes
blanchet
parents:
58634
diff
changeset
|
100 |
(http://church.cims.nyu.edu/bugzilla3/show_bug.cgi?id=597). It should be removed once |
a86683d6c97e
work around bug in CVC4, with boolean arguments to (co)datatypes
blanchet
parents:
58634
diff
changeset
|
101 |
the bug is fixed. *) |
a86683d6c97e
work around bug in CVC4, with boolean arguments to (co)datatypes
blanchet
parents:
58634
diff
changeset
|
102 |
if forall (forall (forall (is_homogenously_nested_co_recursive))) ctrXs_Tsss andalso |
a86683d6c97e
work around bug in CVC4, with boolean arguments to (co)datatypes
blanchet
parents:
58634
diff
changeset
|
103 |
forall (forall (forall (curry (op <>) @{typ bool}))) |
a86683d6c97e
work around bug in CVC4, with boolean arguments to (co)datatypes
blanchet
parents:
58634
diff
changeset
|
104 |
(map (map (map substAs)) ctrXs_Tsss) then |
58430 | 105 |
get_ctr_sugar_decl ctr_sugar T Ts ctxt |>> map (pair fp) |
106 |
else |
|
107 |
maybe_typedef () |
|
58428
e4e34dfc3e68
rule out nested (co)recursion for SMT (co)datatypes
blanchet
parents:
58427
diff
changeset
|
108 |
end |
e4e34dfc3e68
rule out nested (co)recursion for SMT (co)datatypes
blanchet
parents:
58427
diff
changeset
|
109 |
else |
e4e34dfc3e68
rule out nested (co)recursion for SMT (co)datatypes
blanchet
parents:
58427
diff
changeset
|
110 |
([], ctxt) |
58427
cc1bab5558b0
gracefully handle types like 'enat' whose coinductive view is registered using 'free_constructors'
blanchet
parents:
58364
diff
changeset
|
111 |
| NONE => |
58429
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58428
diff
changeset
|
112 |
if String.isSuffix extN n then |
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58428
diff
changeset
|
113 |
(* for records (FIXME: hack) *) |
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58428
diff
changeset
|
114 |
(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
|
115 |
SOME ctr_sugar => |
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58428
diff
changeset
|
116 |
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
|
117 |
| NONE => maybe_typedef ()) |
58427
cc1bab5558b0
gracefully handle types like 'enat' whose coinductive view is registered using 'free_constructors'
blanchet
parents:
58364
diff
changeset
|
118 |
else |
58429
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58428
diff
changeset
|
119 |
maybe_typedef ()) |
58361 | 120 |
end |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
121 |
|
58429
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58428
diff
changeset
|
122 |
fun add_decls fps T (declss, ctxt) = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
123 |
let |
58429
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58428
diff
changeset
|
124 |
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
|
125 |
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
|
126 |
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
|
127 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
128 |
fun add (TFree _) = I |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
129 |
| add (TVar _) = I |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
130 |
| add (T as Type (@{type_name fun}, _)) = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
131 |
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
|
132 |
| add @{typ bool} = I |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
133 |
| 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
|
134 |
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
|
135 |
(dss, ctxt1) |
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58428
diff
changeset
|
136 |
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
|
137 |
(dss, ctxt1) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
138 |
else |
58429
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58428
diff
changeset
|
139 |
(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
|
140 |
([], _) => (dss, ctxt1) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
141 |
| (ds, ctxt2) => |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
142 |
let |
58429
0b94858325a5
interleave (co)datatypes in the right order w.r.t. dependencies
blanchet
parents:
58428
diff
changeset
|
143 |
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
|
144 |
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
|
145 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
146 |
fun ins [] = [(Us, ds)] |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
147 |
| ins ((Uds as (Us', _)) :: Udss) = |
58364 | 148 |
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
|
149 |
in fold add Us (ins dss, ctxt2) end)) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
150 |
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
|
151 |
|
57229 | 152 |
end; |