|
1 (* Title: HOL/Library/Old_SMT/smt_datatypes.ML |
|
2 Author: Sascha Boehme, TU Muenchen |
|
3 |
|
4 Collector functions for common type declarations and their representation |
|
5 as algebraic datatypes. |
|
6 *) |
|
7 |
|
8 signature SMT_DATATYPES = |
|
9 sig |
|
10 val add_decls: typ -> |
|
11 (typ * (term * term list) list) list list * Proof.context -> |
|
12 (typ * (term * term list) list) list list * Proof.context |
|
13 end |
|
14 |
|
15 structure SMT_Datatypes: SMT_DATATYPES = |
|
16 struct |
|
17 |
|
18 fun mk_selectors T Ts = |
|
19 Variable.variant_fixes (replicate (length Ts) "select") |
|
20 #>> map2 (fn U => fn n => Free (n, T --> U)) Ts |
|
21 |
|
22 |
|
23 (* free constructor type declarations *) |
|
24 |
|
25 fun get_ctr_sugar_decl ({ctrs, ...} : Ctr_Sugar.ctr_sugar) T Ts ctxt = |
|
26 let |
|
27 fun mk_constr ctr0 = |
|
28 let val ctr = Ctr_Sugar.mk_ctr Ts ctr0 in |
|
29 mk_selectors T (binder_types (fastype_of ctr)) #>> pair ctr |
|
30 end |
|
31 in |
|
32 fold_map mk_constr ctrs ctxt |
|
33 |>> (pair T #> single) |
|
34 end |
|
35 |
|
36 |
|
37 (* typedef declarations *) |
|
38 |
|
39 fun get_typedef_decl (({Abs_name, Rep_name, abs_type, rep_type, ...}, {Abs_inverse, ...}) |
|
40 : Typedef.info) T Ts = |
|
41 if can (curry (op RS) @{thm UNIV_I}) Abs_inverse then |
|
42 let |
|
43 val env = snd (Term.dest_Type abs_type) ~~ Ts |
|
44 val instT = Term.map_atyps (perhaps (AList.lookup (op =) env)) |
|
45 |
|
46 val constr = Const (Abs_name, instT (rep_type --> abs_type)) |
|
47 val select = Const (Rep_name, instT (abs_type --> rep_type)) |
|
48 in [(T, [(constr, [select])])] end |
|
49 else |
|
50 [] |
|
51 |
|
52 |
|
53 (* collection of declarations *) |
|
54 |
|
55 fun declared declss T = exists (exists (equal T o fst)) declss |
|
56 fun declared' dss T = exists (exists (equal T o fst) o snd) dss |
|
57 |
|
58 fun get_decls T n Ts ctxt = |
|
59 (case Ctr_Sugar.ctr_sugar_of ctxt n of |
|
60 SOME ctr_sugar => get_ctr_sugar_decl ctr_sugar T Ts ctxt |
|
61 | NONE => |
|
62 (case Typedef.get_info ctxt n of |
|
63 [] => ([], ctxt) |
|
64 | info :: _ => (get_typedef_decl info T Ts, ctxt))) |
|
65 |
|
66 fun add_decls T (declss, ctxt) = |
|
67 let |
|
68 fun depends Ts ds = exists (member (op =) (map fst ds)) Ts |
|
69 |
|
70 fun add (TFree _) = I |
|
71 | add (TVar _) = I |
|
72 | add (T as Type (@{type_name fun}, _)) = |
|
73 fold add (Term.body_type T :: Term.binder_types T) |
|
74 | add @{typ bool} = I |
|
75 | add (T as Type (n, Ts)) = (fn (dss, ctxt1) => |
|
76 if declared declss T orelse declared' dss T then (dss, ctxt1) |
|
77 else if SMT_Builtin.is_builtin_typ_ext ctxt1 T then (dss, ctxt1) |
|
78 else |
|
79 (case get_decls T n Ts ctxt1 of |
|
80 ([], _) => (dss, ctxt1) |
|
81 | (ds, ctxt2) => |
|
82 let |
|
83 val constrTs = |
|
84 maps (map (snd o Term.dest_Const o fst) o snd) ds |
|
85 val Us = fold (union (op =) o Term.binder_types) constrTs [] |
|
86 |
|
87 fun ins [] = [(Us, ds)] |
|
88 | ins ((Uds as (Us', _)) :: Udss) = |
|
89 if depends Us' ds then (Us, ds) :: Uds :: Udss |
|
90 else Uds :: ins Udss |
|
91 in fold add Us (ins dss, ctxt2) end)) |
|
92 in add T ([], ctxt) |>> append declss o map snd end |
|
93 |
|
94 end |