author | paulson |
Wed, 09 Oct 1996 13:32:33 +0200 | |
changeset 2073 | fb0655539d05 |
parent 1726 | cbea219f5e5a |
child 2562 | d571d6660240 |
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 |
|
1726 | 14 |
fun claset_of tname = |
15 |
case get_thydata tname "claset" of |
|
16 |
None => empty_cs |
|
17 |
| Some (CS_DATA cs) => cs; |
|
18 |
||
1668 | 19 |
|
20 |
(** Information about datatypes **) |
|
21 |
||
22 |
(* Retrieve information for a specific datatype *) |
|
23 |
fun datatype_info thy tname = |
|
24 |
case get_thydata (thyname_of_sign (sign_of thy)) "datatypes" of |
|
25 |
None => None |
|
26 |
| Some (DT_DATA ds) => assoc (ds, tname); |
|
27 |
||
28 |
fun match_info thy tname = |
|
29 |
case datatype_info thy tname of |
|
30 |
Some {case_const, constructors, ...} => |
|
31 |
{case_const=case_const, constructors=constructors} |
|
32 |
| None => error ("No datatype \"" ^ tname ^ "\" defined in this theory."); |
|
33 |
||
34 |
fun induct_info thy tname = |
|
35 |
case datatype_info thy tname of |
|
36 |
Some {constructors, nchotomy, ...} => |
|
37 |
{constructors=constructors, nchotomy=nchotomy} |
|
38 |
| None => error ("No datatype \"" ^ tname ^ "\" defined in this theory."); |
|
39 |
||
40 |
||
41 |
(* Retrieve information for all datatypes defined in a theory and its |
|
42 |
ancestors *) |
|
43 |
fun extract_info thy = |
|
44 |
let val (congs, rewrites) = |
|
45 |
case get_thydata (thyname_of_sign (sign_of thy)) "datatypes" of |
|
46 |
None => ([], []) |
|
47 |
| Some (DT_DATA ds) => |
|
48 |
let val info = map snd ds |
|
49 |
in (map #case_cong info, flat (map #case_rewrites info)) end; |
|
50 |
in {case_congs = congs, case_rewrites = rewrites} end; |