equal
deleted
inserted
replaced
5 definitions and simple sub-structural overloading. |
5 definitions and simple sub-structural overloading. |
6 *) |
6 *) |
7 |
7 |
8 signature DEFS = |
8 signature DEFS = |
9 sig |
9 sig |
10 datatype item_kind = Constant | Type |
10 datatype item_kind = Const | Type |
11 type item = item_kind * string |
11 type item = item_kind * string |
12 val item_ord: item * item -> order |
12 val item_ord: item * item -> order |
13 type entry = item * typ list |
13 type entry = item * typ list |
14 val pretty_args: Proof.context -> typ list -> Pretty.T list |
14 val pretty_args: Proof.context -> typ list -> Pretty.T list |
15 val plain_args: typ list -> bool |
15 val plain_args: typ list -> bool |
33 structure Defs: DEFS = |
33 structure Defs: DEFS = |
34 struct |
34 struct |
35 |
35 |
36 (* specification items *) |
36 (* specification items *) |
37 |
37 |
38 datatype item_kind = Constant | Type; |
38 datatype item_kind = Const | Type; |
39 type item = item_kind * string; |
39 type item = item_kind * string; |
40 |
40 |
41 fun item_kind_ord (Constant, Type) = LESS |
41 fun item_kind_ord (Const, Type) = LESS |
42 | item_kind_ord (Type, Constant) = GREATER |
42 | item_kind_ord (Type, Const) = GREATER |
43 | item_kind_ord _ = EQUAL; |
43 | item_kind_ord _ = EQUAL; |
44 |
44 |
45 val item_ord = prod_ord item_kind_ord string_ord; |
45 val item_ord = prod_ord item_kind_ord string_ord; |
46 val fast_item_ord = prod_ord item_kind_ord fast_string_ord; |
46 val fast_item_ord = prod_ord item_kind_ord fast_string_ord; |
47 |
47 |
48 fun print_item (k, s) = if k = Constant then s else "type " ^ s; |
48 fun print_item (k, s) = if k = Const then s else "type " ^ s; |
49 |
49 |
50 structure Itemtab = Table(type key = item val ord = fast_item_ord); |
50 structure Itemtab = Table(type key = item val ord = fast_item_ord); |
51 |
51 |
52 |
52 |
53 (* type arguments *) |
53 (* type arguments *) |