4 |
4 |
5 The abstract type "sg" of signatures. |
5 The abstract type "sg" of signatures. |
6 *) |
6 *) |
7 |
7 |
8 signature SIGN = |
8 signature SIGN = |
9 sig |
9 sig |
10 structure Symtab: SYMTAB |
10 type sg |
11 structure Syntax: SYNTAX |
11 val rep_sg: sg -> {tsig: Type.type_sig, |
12 structure Type: TYPE |
12 const_tab: typ Symtab.table, |
13 sharing Symtab = Type.Symtab |
13 syn: Syntax.syntax, |
14 local open Type Syntax in |
14 stamps: string ref list} |
15 type sg |
15 val subsig: sg * sg -> bool |
16 val rep_sg: sg -> |
16 val eq_sg: sg * sg -> bool |
17 {tsig: type_sig, |
17 val same_sg: sg * sg -> bool |
18 const_tab: typ Symtab.table, |
18 val is_draft: sg -> bool |
19 syn: syntax, |
19 val const_type: sg -> string -> typ option |
20 stamps: string ref list} |
20 val classes: sg -> class list |
21 val subsig: sg * sg -> bool |
21 val subsort: sg -> sort * sort -> bool |
22 val eq_sg: sg * sg -> bool |
22 val nodup_Vars: term -> unit |
23 val same_sg: sg * sg -> bool |
23 val norm_sort: sg -> sort -> sort |
24 val is_draft: sg -> bool |
24 val nonempty_sort: sg -> sort list -> sort -> bool |
25 val const_type: sg -> string -> typ option |
25 val print_sg: sg -> unit |
26 val classes: sg -> class list |
26 val pretty_sg: sg -> Pretty.T |
27 val subsort: sg -> sort * sort -> bool |
27 val pprint_sg: sg -> pprint_args -> unit |
28 val nodup_Vars: term -> unit |
28 val pretty_term: sg -> term -> Pretty.T |
29 val norm_sort: sg -> sort -> sort |
29 val pretty_typ: sg -> typ -> Pretty.T |
30 val nonempty_sort: sg -> sort list -> sort -> bool |
30 val pretty_sort: sort -> Pretty.T |
31 val print_sg: sg -> unit |
31 val string_of_term: sg -> term -> string |
32 val pretty_sg: sg -> Pretty.T |
32 val string_of_typ: sg -> typ -> string |
33 val pprint_sg: sg -> pprint_args -> unit |
33 val pprint_term: sg -> term -> pprint_args -> unit |
34 val pretty_term: sg -> term -> Pretty.T |
34 val pprint_typ: sg -> typ -> pprint_args -> unit |
35 val pretty_typ: sg -> typ -> Pretty.T |
35 val certify_typ: sg -> typ -> typ |
36 val pretty_sort: sort -> Pretty.T |
36 val certify_term: sg -> term -> term * typ * int |
37 val string_of_term: sg -> term -> string |
37 val read_typ: sg * (indexname -> sort option) -> string -> typ |
38 val string_of_typ: sg -> typ -> string |
38 val exn_type_msg: sg -> string * typ list * term list -> string |
39 val pprint_term: sg -> term -> pprint_args -> unit |
39 val infer_types: sg -> (indexname -> typ option) -> |
40 val pprint_typ: sg -> typ -> pprint_args -> unit |
40 (indexname -> sort option) -> string list -> bool |
41 val certify_typ: sg -> typ -> typ |
41 -> term list * typ -> int * term * (indexname * typ) list |
42 val certify_term: sg -> term -> term * typ * int |
42 val add_classes: (class * class list) list -> sg -> sg |
43 val read_typ: sg * (indexname -> sort option) -> string -> typ |
43 val add_classrel: (class * class) list -> sg -> sg |
44 val exn_type_msg: sg -> string * typ list * term list -> string |
44 val add_defsort: sort -> sg -> sg |
45 val infer_types: sg -> (indexname -> typ option) -> |
45 val add_types: (string * int * mixfix) list -> sg -> sg |
46 (indexname -> sort option) -> string list -> bool |
46 val add_tyabbrs: (string * string list * string * mixfix) list -> sg -> sg |
47 -> term list * typ -> int * term * (indexname * typ) list |
47 val add_tyabbrs_i: (string * string list * typ * mixfix) list -> sg -> sg |
48 val add_classes: (class * class list) list -> sg -> sg |
48 val add_arities: (string * sort list * sort) list -> sg -> sg |
49 val add_classrel: (class * class) list -> sg -> sg |
49 val add_consts: (string * string * mixfix) list -> sg -> sg |
50 val add_defsort: sort -> sg -> sg |
50 val add_consts_i: (string * typ * mixfix) list -> sg -> sg |
51 val add_types: (string * int * mixfix) list -> sg -> sg |
51 val add_syntax: (string * string * mixfix) list -> sg -> sg |
52 val add_tyabbrs: (string * string list * string * mixfix) list -> sg -> sg |
52 val add_syntax_i: (string * typ * mixfix) list -> sg -> sg |
53 val add_tyabbrs_i: (string * string list * typ * mixfix) list -> sg -> sg |
53 val add_trfuns: |
54 val add_arities: (string * sort list * sort) list -> sg -> sg |
54 (string * (ast list -> ast)) list * |
55 val add_consts: (string * string * mixfix) list -> sg -> sg |
55 (string * (term list -> term)) list * |
56 val add_consts_i: (string * typ * mixfix) list -> sg -> sg |
56 (string * (term list -> term)) list * |
57 val add_syntax: (string * string * mixfix) list -> sg -> sg |
57 (string * (ast list -> ast)) list -> sg -> sg |
58 val add_syntax_i: (string * typ * mixfix) list -> sg -> sg |
58 val add_trrules: (string * string) trrule list -> sg -> sg |
59 val add_trfuns: |
59 val add_trrules_i: ast trrule list -> sg -> sg |
60 (string * (ast list -> ast)) list * |
60 val add_name: string -> sg -> sg |
61 (string * (term list -> term)) list * |
61 val make_draft: sg -> sg |
62 (string * (term list -> term)) list * |
62 val merge: sg * sg -> sg |
63 (string * (ast list -> ast)) list -> sg -> sg |
63 val proto_pure: sg |
64 val add_trrules: (string * string) trrule list -> sg -> sg |
64 val pure: sg |
65 val add_trrules_i: ast trrule list -> sg -> sg |
65 val cpure: sg |
66 val add_name: string -> sg -> sg |
66 val const_of_class: class -> string |
67 val make_draft: sg -> sg |
67 val class_of_const: string -> class |
68 val merge: sg * sg -> sg |
68 end; |
69 val proto_pure: sg |
69 |
70 val pure: sg |
70 structure Sign : SIGN = |
71 val cpure: sg |
|
72 val const_of_class: class -> string |
|
73 val class_of_const: string -> class |
|
74 end |
|
75 end; |
|
76 |
|
77 functor SignFun(structure Syntax: SYNTAX and Type: TYPE): SIGN = |
|
78 struct |
71 struct |
79 |
72 |
80 structure Symtab = Type.Symtab; |
73 local open Type Syntax in |
81 structure Syntax = Syntax; |
|
82 structure BasicSyntax: BASIC_SYNTAX = Syntax; |
|
83 structure Pretty = Syntax.Pretty; |
|
84 structure Type = Type; |
|
85 open BasicSyntax Type; |
|
86 |
|
87 |
74 |
88 (** datatype sg **) |
75 (** datatype sg **) |
89 |
76 |
90 (*the "ref" in stamps ensures that no two signatures are identical -- it is |
77 (*the "ref" in stamps ensures that no two signatures are identical -- it is |
91 impossible to forge a signature*) |
78 impossible to forge a signature*) |
92 |
79 |
93 datatype sg = |
80 datatype sg = |
94 Sg of { |
81 Sg of { |
95 tsig: type_sig, (*order-sorted signature of types*) |
82 tsig: Type.type_sig, (*order-sorted signature of types*) |
96 const_tab: typ Symtab.table, (*types of constants*) |
83 const_tab: typ Symtab.table, (*types of constants*) |
97 syn: Syntax.syntax, (*syntax for parsing and printing*) |
84 syn: Syntax.syntax, (*syntax for parsing and printing*) |
98 stamps: string ref list}; (*unique theory indentifier*) |
85 stamps: string ref list}; (*unique theory indentifier*) |
99 |
86 |
100 fun rep_sg (Sg args) = args; |
87 fun rep_sg (Sg args) = args; |