author | boehmes |
Mon, 03 Jan 2011 16:22:08 +0100 | |
changeset 41426 | 09615ed31f04 |
child 42361 | 23f352990944 |
permissions | -rw-r--r-- |
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/SMT/smt_datatypes.ML |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
2 |
Author: Sascha Boehme, TU Muenchen |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
3 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
4 |
Collector functions for common type declarations and their representation |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
5 |
as algebraic datatypes. |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
6 |
*) |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
7 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
8 |
signature SMT_DATATYPES = |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
9 |
sig |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
10 |
val add_decls: typ -> |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
11 |
(typ * (term * term list) list) list list * Proof.context -> |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
12 |
(typ * (term * term list) list) list list * Proof.context |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
13 |
end |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
14 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
15 |
structure SMT_Datatypes: SMT_DATATYPES = |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
16 |
struct |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
17 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
18 |
val lhs_head_of = Term.head_of o fst o Logic.dest_equals o Thm.prop_of |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
19 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
20 |
fun mk_selectors T Ts ctxt = |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
21 |
let |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
22 |
val (sels, ctxt') = |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
23 |
Variable.variant_fixes (replicate (length Ts) "select") ctxt |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
24 |
in (map2 (fn n => fn U => Free (n, T --> U)) sels Ts, ctxt') end |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
25 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
26 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
27 |
(* datatype declarations *) |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
28 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
29 |
fun get_datatype_decl ({descr, ...} : Datatype.info) n Ts ctxt = |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
30 |
let |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
31 |
fun get_vars (_, (m, vs, _)) = if m = n then SOME vs else NONE |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
32 |
val vars = the (get_first get_vars descr) ~~ Ts |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
33 |
val lookup_var = the o AList.lookup (op =) vars |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
34 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
35 |
val dTs = map (apsnd (fn (m, vs, _) => Type (m, map lookup_var vs))) descr |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
36 |
val lookup_typ = the o AList.lookup (op =) dTs |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
37 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
38 |
fun typ_of (dt as Datatype.DtTFree _) = lookup_var dt |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
39 |
| typ_of (Datatype.DtType (n, dts)) = Type (n, map typ_of dts) |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
40 |
| typ_of (Datatype.DtRec i) = lookup_typ i |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
41 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
42 |
fun mk_constr T (m, dts) ctxt = |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
43 |
let |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
44 |
val Ts = map typ_of dts |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
45 |
val constr = Const (m, Ts ---> T) |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
46 |
val (selects, ctxt') = mk_selectors T Ts ctxt |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
47 |
in ((constr, selects), ctxt') end |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
48 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
49 |
fun mk_decl (i, (_, _, constrs)) ctxt = |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
50 |
let |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
51 |
val T = lookup_typ i |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
52 |
val (css, ctxt') = fold_map (mk_constr T) constrs ctxt |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
53 |
in ((T, css), ctxt') end |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
54 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
55 |
in fold_map mk_decl descr ctxt end |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
56 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
57 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
58 |
(* record declarations *) |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
59 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
60 |
val record_name_of = Long_Name.implode o fst o split_last o Long_Name.explode |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
61 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
62 |
fun get_record_decl ({ext_def, ...} : Record.info) T ctxt = |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
63 |
let |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
64 |
val (con, _) = Term.dest_Const (lhs_head_of ext_def) |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
65 |
val (fields, more) = Record.get_extT_fields (ProofContext.theory_of ctxt) T |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
66 |
val fieldTs = map snd fields @ [snd more] |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
67 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
68 |
val constr = Const (con, fieldTs ---> T) |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
69 |
val (selects, ctxt') = mk_selectors T fieldTs ctxt |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
70 |
in ((T, [(constr, selects)]), ctxt') end |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
71 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
72 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
73 |
(* typedef declarations *) |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
74 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
75 |
fun get_typedef_decl (info : Typedef.info) T Ts = |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
76 |
let |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
77 |
val ({Abs_name, Rep_name, abs_type, rep_type, ...}, _) = info |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
78 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
79 |
val env = snd (Term.dest_Type abs_type) ~~ Ts |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
80 |
val instT = Term.map_atyps (perhaps (AList.lookup (op =) env)) |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
81 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
82 |
val constr = Const (Abs_name, instT (rep_type --> abs_type)) |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
83 |
val select = Const (Rep_name, instT (abs_type --> rep_type)) |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
84 |
in (T, [(constr, [select])]) end |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
85 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
86 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
87 |
(* collection of declarations *) |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
88 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
89 |
fun declared declss T = exists (exists (equal T o fst)) declss |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
90 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
91 |
fun get_decls T n Ts ctxt = |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
92 |
let val thy = ProofContext.theory_of ctxt |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
93 |
in |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
94 |
(case Datatype.get_info thy n of |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
95 |
SOME info => get_datatype_decl info n Ts ctxt |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
96 |
| NONE => |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
97 |
(case Record.get_info thy (record_name_of n) of |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
98 |
SOME info => get_record_decl info T ctxt |>> single |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
99 |
| NONE => |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
100 |
(case Typedef.get_info ctxt n of |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
101 |
[] => ([], ctxt) |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
102 |
| info :: _ => ([get_typedef_decl info T Ts], ctxt)))) |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
103 |
end |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
104 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
105 |
fun add_decls T (declss, ctxt) = |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
106 |
let |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
107 |
fun add (TFree _) = I |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
108 |
| add (TVar _) = I |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
109 |
| add (T as Type (@{type_name fun}, _)) = |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
110 |
fold add (Term.body_type T :: Term.binder_types T) |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
111 |
| add @{typ bool} = I |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
112 |
| add (T as Type (n, Ts)) = (fn (dss, ctxt1) => |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
113 |
if declared declss T orelse declared dss T then (dss, ctxt1) |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
114 |
else if SMT_Builtin.is_builtin_typ_ext ctxt1 T then (dss, ctxt1) |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
115 |
else |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
116 |
(case get_decls T n Ts ctxt1 of |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
117 |
([], _) => (dss, ctxt1) |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
118 |
| (ds, ctxt2) => |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
119 |
let |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
120 |
val constrTs = |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
121 |
maps (map (snd o Term.dest_Const o fst) o snd) ds |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
122 |
val Us = fold (union (op =) o Term.binder_types) constrTs [] |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
123 |
in fold add Us (ds :: dss, ctxt2) end)) |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
124 |
in add T ([], ctxt) |>> append declss end |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
125 |
|
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
diff
changeset
|
126 |
end |