author | clasohm |
Fri, 19 Apr 1996 11:33:24 +0200 | |
changeset 1668 | 8ead1fe65aad |
parent 1657 | a7a6c3fb3cdd |
child 1726 | cbea219f5e5a |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: HOL/thy_data.ML |
1455
52a0271621f3
changed the way simpsets and information about datatypes are stored
clasohm
parents:
diff
changeset
|
2 |
ID: $Id$ |
1465 | 3 |
Author: Carsten Clasohm |
1455
52a0271621f3
changed the way simpsets and information about datatypes are stored
clasohm
parents:
diff
changeset
|
4 |
Copyright 1995 TU Muenchen |
52a0271621f3
changed the way simpsets and information about datatypes are stored
clasohm
parents:
diff
changeset
|
5 |
|
52a0271621f3
changed the way simpsets and information about datatypes are stored
clasohm
parents:
diff
changeset
|
6 |
Definitions that have to be reread after init_thy_reader has been invoked |
52a0271621f3
changed the way simpsets and information about datatypes are stored
clasohm
parents:
diff
changeset
|
7 |
*) |
52a0271621f3
changed the way simpsets and information about datatypes are stored
clasohm
parents:
diff
changeset
|
8 |
|
52a0271621f3
changed the way simpsets and information about datatypes are stored
clasohm
parents:
diff
changeset
|
9 |
fun simpset_of tname = |
1657
a7a6c3fb3cdd
changed first parameter of add_thydata and get_thydata
clasohm
parents:
1465
diff
changeset
|
10 |
case get_thydata tname "simpset" of |
1455
52a0271621f3
changed the way simpsets and information about datatypes are stored
clasohm
parents:
diff
changeset
|
11 |
None => empty_ss |
52a0271621f3
changed the way simpsets and information about datatypes are stored
clasohm
parents:
diff
changeset
|
12 |
| Some (SS_DATA ss) => ss; |
52a0271621f3
changed the way simpsets and information about datatypes are stored
clasohm
parents:
diff
changeset
|
13 |
|
1668 | 14 |
|
15 |
(** Information about datatypes **) |
|
16 |
||
17 |
(* Retrieve information for a specific datatype *) |
|
18 |
fun datatype_info thy tname = |
|
19 |
case get_thydata (thyname_of_sign (sign_of thy)) "datatypes" of |
|
20 |
None => None |
|
21 |
| Some (DT_DATA ds) => assoc (ds, tname); |
|
22 |
||
23 |
fun match_info thy tname = |
|
24 |
case datatype_info thy tname of |
|
25 |
Some {case_const, constructors, ...} => |
|
26 |
{case_const=case_const, constructors=constructors} |
|
27 |
| None => error ("No datatype \"" ^ tname ^ "\" defined in this theory."); |
|
28 |
||
29 |
fun induct_info thy tname = |
|
30 |
case datatype_info thy tname of |
|
31 |
Some {constructors, nchotomy, ...} => |
|
32 |
{constructors=constructors, nchotomy=nchotomy} |
|
33 |
| None => error ("No datatype \"" ^ tname ^ "\" defined in this theory."); |
|
34 |
||
35 |
||
36 |
(* Retrieve information for all datatypes defined in a theory and its |
|
37 |
ancestors *) |
|
38 |
fun extract_info thy = |
|
39 |
let val (congs, rewrites) = |
|
40 |
case get_thydata (thyname_of_sign (sign_of thy)) "datatypes" of |
|
41 |
None => ([], []) |
|
42 |
| Some (DT_DATA ds) => |
|
43 |
let val info = map snd ds |
|
44 |
in (map #case_cong info, flat (map #case_rewrites info)) end; |
|
45 |
in {case_congs = congs, case_rewrites = rewrites} end; |