author  wenzelm 
Sat, 09 Dec 2006 18:05:41 +0100  
changeset 21722  25239591e732 
parent 21704  f4fe6e5a3ee6 
child 21741  5f3d62008bb5 
permissions  rwrr 
19  1 
(* Title: Pure/sign.ML 
0  2 
ID: $Id$ 
251  3 
Author: Lawrence C Paulson and Markus Wenzel 
0  4 

16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

5 
Logical signature content: naming conventions, concrete syntax, type 
18062  6 
signature, polymorphic constants. 
0  7 
*) 
8 

16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

9 
signature SIGN_THEORY = 
3791
c5db2c87a646
now supports qualified names (intern vs. extern) !!!
wenzelm
parents:
3552
diff
changeset

10 
sig 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

11 
val add_defsort: string > theory > theory 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

12 
val add_defsort_i: sort > theory > theory 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

13 
val add_types: (bstring * int * mixfix) list > theory > theory 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

14 
val add_typedecls: (bstring * string list * mixfix) list > theory > theory 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

15 
val add_nonterminals: bstring list > theory > theory 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

16 
val add_tyabbrs: (bstring * string list * string * mixfix) list > theory > theory 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

17 
val add_tyabbrs_i: (bstring * string list * typ * mixfix) list > theory > theory 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

18 
val add_syntax: (bstring * string * mixfix) list > theory > theory 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

19 
val add_syntax_i: (bstring * typ * mixfix) list > theory > theory 
20784  20 
val add_modesyntax: Syntax.mode > (bstring * string * mixfix) list > theory > theory 
21 
val add_modesyntax_i: Syntax.mode > (bstring * typ * mixfix) list > theory > theory 

22 
val del_modesyntax: Syntax.mode > (bstring * string * mixfix) list > theory > theory 

23 
val del_modesyntax_i: Syntax.mode > (bstring * typ * mixfix) list > theory > theory 

16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

24 
val add_consts: (bstring * string * mixfix) list > theory > theory 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

25 
val add_consts_i: (bstring * typ * mixfix) list > theory > theory 
19099
100bf66d7e85
add_const_constraint(_i): demand TFrees instead of TVars, optional type (i.e. may delete constraints);
wenzelm
parents:
19054
diff
changeset

26 
val add_const_constraint: xstring * string option > theory > theory 
100bf66d7e85
add_const_constraint(_i): demand TFrees instead of TVars, optional type (i.e. may delete constraints);
wenzelm
parents:
19054
diff
changeset

27 
val add_const_constraint_i: string * typ option > theory > theory 
19513
77ff7cd602d7
removed add_classes/classrel/arities (superceded by AxClass.axiomatize_class/classrel/arity);
wenzelm
parents:
19482
diff
changeset

28 
val primitive_class: string * class list > theory > theory 
77ff7cd602d7
removed add_classes/classrel/arities (superceded by AxClass.axiomatize_class/classrel/arity);
wenzelm
parents:
19482
diff
changeset

29 
val primitive_classrel: class * class > theory > theory 
77ff7cd602d7
removed add_classes/classrel/arities (superceded by AxClass.axiomatize_class/classrel/arity);
wenzelm
parents:
19482
diff
changeset

30 
val primitive_arity: arity > theory > theory 
1501  31 
val add_trfuns: 
4344  32 
(string * (ast list > ast)) list * 
33 
(string * (term list > term)) list * 

34 
(string * (term list > term)) list * 

16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

35 
(string * (ast list > ast)) list > theory > theory 
2385  36 
val add_trfunsT: 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

37 
(string * (bool > typ > term list > term)) list > theory > theory 
14645  38 
val add_advanced_trfuns: 
18857  39 
(string * (Context.generic > ast list > ast)) list * 
40 
(string * (Context.generic > term list > term)) list * 

41 
(string * (Context.generic > term list > term)) list * 

42 
(string * (Context.generic > ast list > ast)) list > theory > theory 

14645  43 
val add_advanced_trfunsT: 
18857  44 
(string * (Context.generic > bool > typ > term list > term)) list > theory > theory 
2693  45 
val add_tokentrfuns: 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

46 
(string * string * (string > string * real)) list > theory > theory 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

47 
val add_mode_tokentrfuns: string > (string * (string > string * real)) list 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

48 
> theory > theory 
17102
a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

49 
val parse_ast_translation: bool * string > theory > theory 
a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

50 
val parse_translation: bool * string > theory > theory 
a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

51 
val print_translation: bool * string > theory > theory 
a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

52 
val typed_print_translation: bool * string > theory > theory 
a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

53 
val print_ast_translation: bool * string > theory > theory 
a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

54 
val token_translation: string > theory > theory 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

55 
val add_trrules: (xstring * string) Syntax.trrule list > theory > theory 
19258
ada9977f1e98
declared_const: check for type constraint only, i.e. admit abbreviations as well;
wenzelm
parents:
19250
diff
changeset

56 
val del_trrules: (xstring * string) Syntax.trrule list > theory > theory 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

57 
val add_trrules_i: ast Syntax.trrule list > theory > theory 
19258
ada9977f1e98
declared_const: check for type constraint only, i.e. admit abbreviations as well;
wenzelm
parents:
19250
diff
changeset

58 
val del_trrules_i: ast Syntax.trrule list > theory > theory 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

59 
val add_path: string > theory > theory 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

60 
val parent_path: theory > theory 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

61 
val root_path: theory > theory 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

62 
val absolute_path: theory > theory 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

63 
val local_path: theory > theory 
19013  64 
val no_base_names: theory > theory 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

65 
val qualified_names: theory > theory 
19054
af7cc6063285
replaced qualified_force_prefix to sticky_prefix;
wenzelm
parents:
19013
diff
changeset

66 
val sticky_prefix: string > theory > theory 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

67 
val set_policy: (string > bstring > string) * (string list > string list list) > 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

68 
theory > theory 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

69 
val restore_naming: theory > theory > theory 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

70 
val hide_classes: bool > xstring list > theory > theory 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

71 
val hide_classes_i: bool > string list > theory > theory 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

72 
val hide_types: bool > xstring list > theory > theory 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

73 
val hide_types_i: bool > string list > theory > theory 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

74 
val hide_consts: bool > xstring list > theory > theory 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

75 
val hide_consts_i: bool > string list > theory > theory 
17343  76 
val hide_names: bool > string * xstring list > theory > theory 
77 
val hide_names_i: bool > string * string list > theory > theory 

16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

78 
end 
0  79 

16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

80 
signature SIGN = 
5642  81 
sig 
16536  82 
val init_data: theory > theory 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

83 
val rep_sg: theory > 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

84 
{naming: NameSpace.naming, 
16597
5a5229a55964
eliminated separate syn type  advanced trfuns already part of Syntax.syntax;
wenzelm
parents:
16536
diff
changeset

85 
syn: Syntax.syntax, 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

86 
tsig: Type.tsig, 
18062  87 
consts: Consts.T} 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

88 
val naming_of: theory > NameSpace.naming 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

89 
val base_name: string > bstring 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

90 
val full_name: theory > bstring > string 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

91 
val full_name_path: theory > string > bstring > string 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

92 
val declare_name: theory > string > NameSpace.T > NameSpace.T 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

93 
val syn_of: theory > Syntax.syntax 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

94 
val tsig_of: theory > Type.tsig 
19642  95 
val classes_of: theory > Sorts.algebra 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

96 
val classes: theory > class list 
19407  97 
val super_classes: theory > class > class list 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

98 
val defaultS: theory > sort 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

99 
val subsort: theory > sort * sort > bool 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

100 
val of_sort: theory > typ * sort > bool 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

101 
val witness_sorts: theory > sort list > sort list > (typ * sort) list 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

102 
val universal_witness: theory > (typ * sort) option 
16655  103 
val all_sorts_nonempty: theory > bool 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

104 
val typ_instance: theory > typ * typ > bool 
19427  105 
val typ_equiv: theory > typ * typ > bool 
16941
0bda949449ee
added add_const_constraint(_i), const_constraint;
wenzelm
parents:
16894
diff
changeset

106 
val typ_match: theory > typ * typ > Type.tyenv > Type.tyenv 
0bda949449ee
added add_const_constraint(_i), const_constraint;
wenzelm
parents:
16894
diff
changeset

107 
val typ_unify: theory > typ * typ > Type.tyenv * int > Type.tyenv * int 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

108 
val is_logtype: theory > string > bool 
18967  109 
val consts_of: theory > Consts.T 
16941
0bda949449ee
added add_const_constraint(_i), const_constraint;
wenzelm
parents:
16894
diff
changeset

110 
val const_constraint: theory > string > typ option 
17037  111 
val the_const_constraint: theory > string > typ 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

112 
val const_type: theory > string > typ option 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

113 
val the_const_type: theory > string > typ 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

114 
val declared_tyname: theory > string > bool 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

115 
val declared_const: theory > string > bool 
18062  116 
val const_monomorphic: theory > string > bool 
21183  117 
val const_syntax_name: theory > string > string 
18146  118 
val const_typargs: theory > string * typ > typ list 
18164  119 
val const_instance: theory > string * typ list > typ 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

120 
val class_space: theory > NameSpace.T 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

121 
val type_space: theory > NameSpace.T 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

122 
val const_space: theory > NameSpace.T 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

123 
val intern_class: theory > xstring > string 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

124 
val extern_class: theory > string > xstring 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

125 
val intern_type: theory > xstring > string 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

126 
val extern_type: theory > string > xstring 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

127 
val intern_const: theory > xstring > string 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

128 
val extern_const: theory > string > xstring 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

129 
val intern_sort: theory > sort > sort 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

130 
val extern_sort: theory > sort > sort 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

131 
val intern_typ: theory > typ > typ 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

132 
val extern_typ: theory > typ > typ 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

133 
val intern_term: theory > term > term 
18994  134 
val extern_term: (string > xstring) > theory > term > term 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

135 
val intern_tycons: theory > typ > typ 
19366
a2040baa9444
pretty_term': early vs. late externing (support authentic syntax);
wenzelm
parents:
19289
diff
changeset

136 
val pretty_term': Context.generic > Syntax.syntax > (string > xstring) > term > Pretty.T 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

137 
val pretty_term: theory > term > Pretty.T 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

138 
val pretty_typ: theory > typ > Pretty.T 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

139 
val pretty_sort: theory > sort > Pretty.T 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

140 
val pretty_classrel: theory > class list > Pretty.T 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

141 
val pretty_arity: theory > arity > Pretty.T 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

142 
val string_of_term: theory > term > string 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

143 
val string_of_typ: theory > typ > string 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

144 
val string_of_sort: theory > sort > string 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

145 
val string_of_classrel: theory > class list > string 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

146 
val string_of_arity: theory > arity > string 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

147 
val pp: theory > Pretty.pp 
19462  148 
val arity_number: theory > string > int 
149 
val arity_sorts: theory > string > sort > sort list 

16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

150 
val certify_class: theory > class > class 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

151 
val certify_sort: theory > sort > sort 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

152 
val certify_typ: theory > typ > typ 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

153 
val certify_typ_syntax: theory > typ > typ 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

154 
val certify_typ_abbrev: theory > typ > typ 
19366
a2040baa9444
pretty_term': early vs. late externing (support authentic syntax);
wenzelm
parents:
19289
diff
changeset

155 
val certify': bool > bool > Pretty.pp > Consts.T > theory > term > term * typ * int 
18967  156 
val certify_term: theory > term > term * typ * int 
157 
val certify_prop: theory > term > term * typ * int 

16494  158 
val cert_term: theory > term > term 
159 
val cert_prop: theory > term > term 

18941  160 
val no_vars: Pretty.pp > term > term 
161 
val cert_def: Pretty.pp > term > (string * typ) * term 

19244
1d7e51d9828b
added read_class, read/cert_classrel/arity (from axclass.ML);
wenzelm
parents:
19099
diff
changeset

162 
val read_class: theory > xstring > class 
18857  163 
val read_sort': Syntax.syntax > Context.generic > string > sort 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

164 
val read_sort: theory > string > sort 
19244
1d7e51d9828b
added read_class, read/cert_classrel/arity (from axclass.ML);
wenzelm
parents:
19099
diff
changeset

165 
val read_arity: theory > xstring * string list * string > arity 
1d7e51d9828b
added read_class, read/cert_classrel/arity (from axclass.ML);
wenzelm
parents:
19099
diff
changeset

166 
val cert_arity: theory > arity > arity 
18857  167 
val read_typ': Syntax.syntax > Context.generic > 
168 
(indexname > sort option) > string > typ 

169 
val read_typ_syntax': Syntax.syntax > Context.generic > 

170 
(indexname > sort option) > string > typ 

171 
val read_typ_abbrev': Syntax.syntax > Context.generic > 

172 
(indexname > sort option) > string > typ 

16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

173 
val read_typ: theory * (indexname > sort option) > string > typ 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

174 
val read_typ_syntax: theory * (indexname > sort option) > string > typ 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

175 
val read_typ_abbrev: theory * (indexname > sort option) > string > typ 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

176 
val read_tyname: theory > string > typ 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

177 
val read_const: theory > string > term 
18967  178 
val infer_types_simult: Pretty.pp > theory > Consts.T > (indexname > typ option) > 
20155  179 
(indexname > sort option) > Name.context > bool 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

180 
> (term list * typ) list > term list * (indexname * typ) list 
18967  181 
val infer_types: Pretty.pp > theory > Consts.T > (indexname > typ option) > 
20155  182 
(indexname > sort option) > Name.context > bool 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

183 
> term list * typ > term * (indexname * typ) list 
18967  184 
val read_def_terms': Pretty.pp > (string > bool) > Syntax.syntax > Consts.T > 
185 
Context.generic > (indexname > typ option) * (indexname > sort option) > 

20155  186 
Name.context > bool > (string * typ) list > term list * (indexname * typ) list 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

187 
val read_def_terms: 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

188 
theory * (indexname > typ option) * (indexname > sort option) > 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

189 
string list > bool > (string * typ) list > term list * (indexname * typ) list 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

190 
val simple_read_term: theory > typ > string > term 
16494  191 
val read_term: theory > string > term 
192 
val read_prop: theory > string > term 

19679
ae4c1e2742c1
consts: replaced early'' flag by inverted authentic'';
wenzelm
parents:
19673
diff
changeset

193 
val add_consts_authentic: (bstring * typ * mixfix) list > theory > theory 
21206
2af4c7b3f7ef
replaced const_syntax by notation, which operates on terms;
wenzelm
parents:
21183
diff
changeset

194 
val add_notation: Syntax.mode > (term * mixfix) list > theory > theory 
21704  195 
val add_abbrev: string > bstring * term > theory > ((string * typ) * term) * theory 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

196 
include SIGN_THEORY 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

197 
end 
5642  198 

16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

199 
structure Sign: SIGN = 
143  200 
struct 
0  201 

402  202 

16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

203 
(** datatype sign **) 
16337  204 

16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

205 
datatype sign = Sign of 
18062  206 
{naming: NameSpace.naming, (*common naming conventions*) 
207 
syn: Syntax.syntax, (*concrete syntax for terms, types, sorts*) 

208 
tsig: Type.tsig, (*ordersorted signature of types*) 

209 
consts: Consts.T}; (*polymorphic constants*) 

16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

210 

1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

211 
fun make_sign (naming, syn, tsig, consts) = 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

212 
Sign {naming = naming, syn = syn, tsig = tsig, consts = consts}; 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

213 

1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

214 
structure SignData = TheoryDataFun 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

215 
(struct 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

216 
val name = "Pure/sign"; 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

217 
type T = sign; 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

218 
val copy = I; 
17405  219 
fun extend (Sign {syn, tsig, consts, ...}) = 
220 
make_sign (NameSpace.default_naming, syn, tsig, consts); 

16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

221 

18062  222 
val empty = 
18714  223 
make_sign (NameSpace.default_naming, Syntax.basic_syn, Type.empty_tsig, Consts.empty); 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

224 

1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

225 
fun merge pp (sign1, sign2) = 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

226 
let 
18062  227 
val Sign {naming = _, syn = syn1, tsig = tsig1, consts = consts1} = sign1; 
228 
val Sign {naming = _, syn = syn2, tsig = tsig2, consts = consts2} = sign2; 

16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

229 

1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

230 
val naming = NameSpace.default_naming; 
16597
5a5229a55964
eliminated separate syn type  advanced trfuns already part of Syntax.syntax;
wenzelm
parents:
16536
diff
changeset

231 
val syn = Syntax.merge_syntaxes syn1 syn2; 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

232 
val tsig = Type.merge_tsigs pp (tsig1, tsig2); 
18062  233 
val consts = Consts.merge (consts1, consts2); 
234 
in make_sign (naming, syn, tsig, consts) end; 

16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

235 

1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

236 
fun print _ _ = (); 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

237 
end); 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

238 

16536  239 
val init_data = SignData.init; 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

240 

1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

241 
fun rep_sg thy = SignData.get thy > (fn Sign args => args); 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

242 

1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

243 
fun map_sign f = SignData.map (fn Sign {naming, syn, tsig, consts} => 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

244 
make_sign (f (naming, syn, tsig, consts))); 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

245 

1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

246 
fun map_naming f = map_sign (fn (naming, syn, tsig, consts) => (f naming, syn, tsig, consts)); 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

247 
fun map_syn f = map_sign (fn (naming, syn, tsig, consts) => (naming, f syn, tsig, consts)); 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

248 
fun map_tsig f = map_sign (fn (naming, syn, tsig, consts) => (naming, syn, f tsig, consts)); 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

249 
fun map_consts f = map_sign (fn (naming, syn, tsig, consts) => (naming, syn, tsig, f consts)); 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

250 

16337  251 

252 
(* naming *) 

253 

16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

254 
val naming_of = #naming o rep_sg; 
16337  255 
val base_name = NameSpace.base; 
256 
val full_name = NameSpace.full o naming_of; 

16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

257 
fun full_name_path thy elems = NameSpace.full (NameSpace.add_path elems (naming_of thy)); 
16337  258 
val declare_name = NameSpace.declare o naming_of; 
14645  259 

260 

261 
(* syntax *) 

262 

16597
5a5229a55964
eliminated separate syn type  advanced trfuns already part of Syntax.syntax;
wenzelm
parents:
16536
diff
changeset

263 
val syn_of = #syn o rep_sg; 
14645  264 

0  265 

16337  266 
(* type signature *) 
267 

268 
val tsig_of = #tsig o rep_sg; 

19642  269 
val classes_of = #2 o #classes o Type.rep_tsig o tsig_of; 
270 
val classes = Sorts.classes o classes_of; 

271 
val super_classes = Sorts.super_classes o classes_of; 

4844  272 
val defaultS = Type.defaultS o tsig_of; 
4568  273 
val subsort = Type.subsort o tsig_of; 
7640  274 
val of_sort = Type.of_sort o tsig_of; 
275 
val witness_sorts = Type.witness_sorts o tsig_of; 

14784
e65d77313a94
xxx_typ_raw replace xxx_typ_no_norm forms; prevent duplicate consts declarations in merge; misc cleanup;
wenzelm
parents:
14700
diff
changeset

276 
val universal_witness = Type.universal_witness o tsig_of; 
16655  277 
val all_sorts_nonempty = is_some o universal_witness; 
14784
e65d77313a94
xxx_typ_raw replace xxx_typ_no_norm forms; prevent duplicate consts declarations in merge; misc cleanup;
wenzelm
parents:
14700
diff
changeset

278 
val typ_instance = Type.typ_instance o tsig_of; 
19427  279 
fun typ_equiv thy (T, U) = typ_instance thy (T, U) andalso typ_instance thy (U, T); 
16941
0bda949449ee
added add_const_constraint(_i), const_constraint;
wenzelm
parents:
16894
diff
changeset

280 
val typ_match = Type.typ_match o tsig_of; 
0bda949449ee
added add_const_constraint(_i), const_constraint;
wenzelm
parents:
16894
diff
changeset

281 
val typ_unify = Type.unify o tsig_of; 
20664  282 
val is_logtype = member (op =) o Type.logical_types o tsig_of; 
4256  283 

284 

18062  285 
(* polymorphic constants *) 
16941
0bda949449ee
added add_const_constraint(_i), const_constraint;
wenzelm
parents:
16894
diff
changeset

286 

18062  287 
val consts_of = #consts o rep_sg; 
21722  288 
val the_const_constraint = Consts.the_constraint o consts_of; 
18062  289 
val const_constraint = try o the_const_constraint; 
21722  290 
val the_const_type = Consts.the_declaration o consts_of; 
18062  291 
val const_type = try o the_const_type; 
21722  292 
val const_monomorphic = Consts.is_monomorphic o consts_of; 
21183  293 
val const_syntax_name = Consts.syntax_name o consts_of; 
18062  294 
val const_typargs = Consts.typargs o consts_of; 
18164  295 
val const_instance = Consts.instance o consts_of; 
4256  296 

16894  297 
val declared_tyname = Symtab.defined o #2 o #types o Type.rep_tsig o tsig_of; 
19258
ada9977f1e98
declared_const: check for type constraint only, i.e. admit abbreviations as well;
wenzelm
parents:
19250
diff
changeset

298 
val declared_const = is_some oo const_constraint; 
620  299 

402  300 

0  301 

16337  302 
(** intern / extern names **) 
303 

16368
a06868ebeb0f
discontinued named name spaces (classK, typeK, constK);
wenzelm
parents:
16354
diff
changeset

304 
val class_space = #1 o #classes o Type.rep_tsig o tsig_of; 
a06868ebeb0f
discontinued named name spaces (classK, typeK, constK);
wenzelm
parents:
16354
diff
changeset

305 
val type_space = #1 o #types o Type.rep_tsig o tsig_of; 
18967  306 
val const_space = Consts.space_of o consts_of; 
14645  307 

16368
a06868ebeb0f
discontinued named name spaces (classK, typeK, constK);
wenzelm
parents:
16354
diff
changeset

308 
val intern_class = NameSpace.intern o class_space; 
a06868ebeb0f
discontinued named name spaces (classK, typeK, constK);
wenzelm
parents:
16354
diff
changeset

309 
val extern_class = NameSpace.extern o class_space; 
a06868ebeb0f
discontinued named name spaces (classK, typeK, constK);
wenzelm
parents:
16354
diff
changeset

310 
val intern_type = NameSpace.intern o type_space; 
a06868ebeb0f
discontinued named name spaces (classK, typeK, constK);
wenzelm
parents:
16354
diff
changeset

311 
val extern_type = NameSpace.extern o type_space; 
a06868ebeb0f
discontinued named name spaces (classK, typeK, constK);
wenzelm
parents:
16354
diff
changeset

312 
val intern_const = NameSpace.intern o const_space; 
a06868ebeb0f
discontinued named name spaces (classK, typeK, constK);
wenzelm
parents:
16354
diff
changeset

313 
val extern_const = NameSpace.extern o const_space; 
16337  314 

315 
val intern_sort = map o intern_class; 

316 
val extern_sort = map o extern_class; 

317 

318 
local 

14645  319 

18892  320 
fun map_typ f g (Type (c, Ts)) = Type (g c, map (map_typ f g) Ts) 
321 
 map_typ f _ (TFree (x, S)) = TFree (x, map f S) 

322 
 map_typ f _ (TVar (xi, S)) = TVar (xi, map f S); 

323 

324 
fun map_term f g h (Const (c, T)) = Const (h c, map_typ f g T) 

325 
 map_term f g _ (Free (x, T)) = Free (x, map_typ f g T) 

326 
 map_term f g _ (Var (xi, T)) = Var (xi, map_typ f g T) 

327 
 map_term _ _ _ (t as Bound _) = t 

328 
 map_term f g h (Abs (x, T, t)) = Abs (x, map_typ f g T, map_term f g h t) 

329 
 map_term f g h (t $ u) = map_term f g h t $ map_term f g h u; 

330 

18994  331 
val add_classesT = Term.fold_atyps 
332 
(fn TFree (_, S) => fold (insert (op =)) S 

333 
 TVar (_, S) => fold (insert (op =)) S 

334 
 _ => I); 

335 

336 
fun add_tyconsT (Type (c, Ts)) = insert (op =) c #> fold add_tyconsT Ts 

337 
 add_tyconsT _ = I; 

338 

339 
val add_consts = Term.fold_aterms (fn Const (c, _) => insert (op =) c  _ => I); 

340 

16337  341 
fun mapping add_names f t = 
342 
let 

20664  343 
fun f' (x: string) = let val y = f x in if x = y then NONE else SOME (x, y) end; 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19462
diff
changeset

344 
val tab = map_filter f' (add_names t []); 
18941  345 
fun get x = the_default x (AList.lookup (op =) tab x); 
16337  346 
in get end; 
347 

16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

348 
fun typ_mapping f g thy T = 
18892  349 
T > map_typ 
18994  350 
(mapping add_classesT (f thy) T) 
351 
(mapping add_tyconsT (g thy) T); 

14645  352 

16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

353 
fun term_mapping f g h thy t = 
18892  354 
t > map_term 
18994  355 
(mapping (Term.fold_types add_classesT) (f thy) t) 
356 
(mapping (Term.fold_types add_tyconsT) (g thy) t) 

357 
(mapping add_consts (h thy) t); 

16337  358 

359 
in 

14645  360 

16368
a06868ebeb0f
discontinued named name spaces (classK, typeK, constK);
wenzelm
parents:
16354
diff
changeset

361 
val intern_typ = typ_mapping intern_class intern_type; 
a06868ebeb0f
discontinued named name spaces (classK, typeK, constK);
wenzelm
parents:
16354
diff
changeset

362 
val extern_typ = typ_mapping extern_class extern_type; 
a06868ebeb0f
discontinued named name spaces (classK, typeK, constK);
wenzelm
parents:
16354
diff
changeset

363 
val intern_term = term_mapping intern_class intern_type intern_const; 
18994  364 
fun extern_term h = term_mapping extern_class extern_type (K h); 
16368
a06868ebeb0f
discontinued named name spaces (classK, typeK, constK);
wenzelm
parents:
16354
diff
changeset

365 
val intern_tycons = typ_mapping (K I) intern_type; 
16337  366 

367 
end; 

14645  368 

369 

370 

4249  371 
(** pretty printing of terms, types etc. **) 
3937  372 

19366
a2040baa9444
pretty_term': early vs. late externing (support authentic syntax);
wenzelm
parents:
19289
diff
changeset

373 
fun pretty_term' context syn ext t = 
18994  374 
let val curried = Context.exists_name Context.CPureN (Context.theory_of context) 
19366
a2040baa9444
pretty_term': early vs. late externing (support authentic syntax);
wenzelm
parents:
19289
diff
changeset

375 
in Syntax.pretty_term ext context syn curried t end; 
18857  376 

18994  377 
fun pretty_term thy t = 
19366
a2040baa9444
pretty_term': early vs. late externing (support authentic syntax);
wenzelm
parents:
19289
diff
changeset

378 
pretty_term' (Context.Theory thy) (syn_of thy) (Consts.extern (consts_of thy)) 
a2040baa9444
pretty_term': early vs. late externing (support authentic syntax);
wenzelm
parents:
19289
diff
changeset

379 
(extern_term (Consts.extern_early (consts_of thy)) thy t); 
18857  380 

381 
fun pretty_typ thy T = Syntax.pretty_typ (Context.Theory thy) (syn_of thy) (extern_typ thy T); 

382 
fun pretty_sort thy S = Syntax.pretty_sort (Context.Theory thy) (syn_of thy) (extern_sort thy S); 

3937  383 

19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19462
diff
changeset

384 
fun pretty_classrel thy cs = Pretty.block (flat 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

385 
(separate [Pretty.str " <", Pretty.brk 1] (map (single o pretty_sort thy o single) cs))); 
3937  386 

16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

387 
fun pretty_arity thy (a, Ss, S) = 
3937  388 
let 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

389 
val a' = extern_type thy a; 
3937  390 
val dom = 
391 
if null Ss then [] 

16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

392 
else [Pretty.list "(" ")" (map (pretty_sort thy) Ss), Pretty.brk 1]; 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

393 
in Pretty.block ([Pretty.str (a' ^ " ::"), Pretty.brk 1] @ dom @ [pretty_sort thy S]) end; 
3937  394 

14828  395 
val string_of_term = Pretty.string_of oo pretty_term; 
396 
val string_of_typ = Pretty.string_of oo pretty_typ; 

397 
val string_of_sort = Pretty.string_of oo pretty_sort; 

398 
val string_of_classrel = Pretty.string_of oo pretty_classrel; 

399 
val string_of_arity = Pretty.string_of oo pretty_arity; 

3937  400 

16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

401 
fun pp thy = Pretty.pp (pretty_term thy, pretty_typ thy, pretty_sort thy, 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

402 
pretty_classrel thy, pretty_arity thy); 
14828  403 

3937  404 

405 

16337  406 
(** certify entities **) (*exception TYPE*) 
8898  407 

16337  408 
(* certify wrt. type signature *) 
8898  409 

19462  410 
val arity_number = Type.arity_number o tsig_of; 
411 
fun arity_sorts thy = Type.arity_sorts (pp thy) (tsig_of thy); 

412 

16723  413 
fun certify cert = cert o tsig_of o Context.check_thy; 
562  414 

16337  415 
val certify_class = certify Type.cert_class; 
416 
val certify_sort = certify Type.cert_sort; 

417 
val certify_typ = certify Type.cert_typ; 

418 
val certify_typ_syntax = certify Type.cert_typ_syntax; 

419 
val certify_typ_abbrev = certify Type.cert_typ_abbrev; 

10443
0a68dc9edba5
added certify_tycon, certify_tyabbr, certify_const;
wenzelm
parents:
10404
diff
changeset

420 

4961
27f559b54c57
certify_term: type_check replaces Term.type_of, providing sensible
wenzelm
parents:
4951
diff
changeset

421 

18967  422 
(* certify term/prop *) 
4961
27f559b54c57
certify_term: type_check replaces Term.type_of, providing sensible
wenzelm
parents:
4951
diff
changeset

423 

14987  424 
local 
1494
22f67e796445
added nodup_Vars check in cterm_of. Prevents same var with distinct types.
nipkow
parents:
1460
diff
changeset

425 

16337  426 
fun type_check pp tm = 
4961
27f559b54c57
certify_term: type_check replaces Term.type_of, providing sensible
wenzelm
parents:
4951
diff
changeset

427 
let 
27f559b54c57
certify_term: type_check replaces Term.type_of, providing sensible
wenzelm
parents:
4951
diff
changeset

428 
fun err_appl why bs t T u U = 
27f559b54c57
certify_term: type_check replaces Term.type_of, providing sensible
wenzelm
parents:
4951
diff
changeset

429 
let 
10404  430 
val xs = map Free bs; (*we do not rename here*) 
4961
27f559b54c57
certify_term: type_check replaces Term.type_of, providing sensible
wenzelm
parents:
4951
diff
changeset

431 
val t' = subst_bounds (xs, t); 
27f559b54c57
certify_term: type_check replaces Term.type_of, providing sensible
wenzelm
parents:
4951
diff
changeset

432 
val u' = subst_bounds (xs, u); 
16337  433 
val msg = cat_lines 
14828  434 
(TypeInfer.appl_error (Syntax.pp_show_brackets pp) why t' T u' U); 
16337  435 
in raise TYPE (msg, [T, U], [t', u']) end; 
4961
27f559b54c57
certify_term: type_check replaces Term.type_of, providing sensible
wenzelm
parents:
4951
diff
changeset

436 

27f559b54c57
certify_term: type_check replaces Term.type_of, providing sensible
wenzelm
parents:
4951
diff
changeset

437 
fun typ_of (_, Const (_, T)) = T 
27f559b54c57
certify_term: type_check replaces Term.type_of, providing sensible
wenzelm
parents:
4951
diff
changeset

438 
 typ_of (_, Free (_, T)) = T 
27f559b54c57
certify_term: type_check replaces Term.type_of, providing sensible
wenzelm
parents:
4951
diff
changeset

439 
 typ_of (_, Var (_, T)) = T 
15570  440 
 typ_of (bs, Bound i) = snd (List.nth (bs, i) handle Subscript => 
4961
27f559b54c57
certify_term: type_check replaces Term.type_of, providing sensible
wenzelm
parents:
4951
diff
changeset

441 
raise TYPE ("Loose bound variable: B." ^ string_of_int i, [], [Bound i])) 
27f559b54c57
certify_term: type_check replaces Term.type_of, providing sensible
wenzelm
parents:
4951
diff
changeset

442 
 typ_of (bs, Abs (x, T, body)) = T > typ_of ((x, T) :: bs, body) 
27f559b54c57
certify_term: type_check replaces Term.type_of, providing sensible
wenzelm
parents:
4951
diff
changeset

443 
 typ_of (bs, t $ u) = 
27f559b54c57
certify_term: type_check replaces Term.type_of, providing sensible
wenzelm
parents:
4951
diff
changeset

444 
let val T = typ_of (bs, t) and U = typ_of (bs, u) in 
27f559b54c57
certify_term: type_check replaces Term.type_of, providing sensible
wenzelm
parents:
4951
diff
changeset

445 
(case T of 
27f559b54c57
certify_term: type_check replaces Term.type_of, providing sensible
wenzelm
parents:
4951
diff
changeset

446 
Type ("fun", [T1, T2]) => 
14828  447 
if T1 = U then T2 else err_appl "Incompatible operand type" bs t T u U 
448 
 _ => err_appl "Operator not of function type" bs t T u U) 

4961
27f559b54c57
certify_term: type_check replaces Term.type_of, providing sensible
wenzelm
parents:
4951
diff
changeset

449 
end; 
18967  450 
in typ_of ([], tm) end; 
4961
27f559b54c57
certify_term: type_check replaces Term.type_of, providing sensible
wenzelm
parents:
4951
diff
changeset

451 

18967  452 
fun err msg = raise TYPE (msg, [], []); 
453 

454 
fun check_vars (t $ u) = (check_vars t; check_vars u) 

455 
 check_vars (Abs (_, _, t)) = check_vars t 

456 
 check_vars (Var (xi as (_, i), _)) = 

457 
if i < 0 then err ("Malformed variable: " ^ quote (Term.string_of_vname xi)) else () 

458 
 check_vars _ = (); 

0  459 

14987  460 
in 
461 

19366
a2040baa9444
pretty_term': early vs. late externing (support authentic syntax);
wenzelm
parents:
19289
diff
changeset

462 
fun certify' normalize prop pp consts thy tm = 
251  463 
let 
16723  464 
val _ = Context.check_thy thy; 
18967  465 
val _ = check_vars tm; 
20548
8ef25fe585a8
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
wenzelm
parents:
20330
diff
changeset

466 
val tm' = Term.map_types (certify_typ thy) tm; 
18967  467 
val T = type_check pp tm'; 
468 
val _ = if prop andalso T <> propT then err "Term not of type prop" else (); 

19366
a2040baa9444
pretty_term': early vs. late externing (support authentic syntax);
wenzelm
parents:
19289
diff
changeset

469 
val tm'' = Consts.certify pp (tsig_of thy) consts tm'; 
18967  470 
val tm'' = if normalize then tm'' else tm'; 
471 
in (if tm = tm'' then tm else tm'', T, Term.maxidx_of_term tm'') end; 

169  472 

19366
a2040baa9444
pretty_term': early vs. late externing (support authentic syntax);
wenzelm
parents:
19289
diff
changeset

473 
fun certify_term thy = certify' true false (pp thy) (consts_of thy) thy; 
a2040baa9444
pretty_term': early vs. late externing (support authentic syntax);
wenzelm
parents:
19289
diff
changeset

474 
fun certify_prop thy = certify' true true (pp thy) (consts_of thy) thy; 
18967  475 

19366
a2040baa9444
pretty_term': early vs. late externing (support authentic syntax);
wenzelm
parents:
19289
diff
changeset

476 
fun cert_term_abbrev thy = #1 o certify' false false (pp thy) (consts_of thy) thy; 
18967  477 
val cert_term = #1 oo certify_term; 
478 
val cert_prop = #1 oo certify_prop; 

251  479 

14987  480 
end; 
481 

251  482 

18941  483 
(* specifications *) 
484 

485 
fun no_vars pp tm = 

20330  486 
(case (Term.add_vars tm [], Term.add_tvars tm []) of 
18941  487 
([], []) => tm 
20330  488 
 (vars, tvars) => error (Pretty.string_of (Pretty.block (Pretty.breaks 
18941  489 
(Pretty.str "Illegal schematic variable(s) in term:" :: 
20330  490 
map (Pretty.term pp o Var) vars @ map (Pretty.typ pp o TVar) tvars))))); 
18941  491 

492 
fun cert_def pp tm = 

493 
let val ((lhs, rhs), _) = tm 

494 
> no_vars pp 

495 
> Logic.strip_imp_concl 

496 
> Logic.dest_def pp Term.is_Const (K false) (K false) 

497 
in (Term.dest_Const (Term.head_of lhs), rhs) end 

498 
handle TERM (msg, _) => error msg; 

499 

500 

16337  501 

16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

502 
(** read and certify entities **) (*exception ERROR*) 
16337  503 

19244
1d7e51d9828b
added read_class, read/cert_classrel/arity (from axclass.ML);
wenzelm
parents:
19099
diff
changeset

504 
(* classes and sorts *) 
1d7e51d9828b
added read_class, read/cert_classrel/arity (from axclass.ML);
wenzelm
parents:
19099
diff
changeset

505 

19427  506 
fun read_class thy c = certify_class thy (intern_class thy c) 
507 
handle TYPE (msg, _, _) => error msg; 

16337  508 

18857  509 
fun read_sort' syn context str = 
16337  510 
let 
18857  511 
val thy = Context.theory_of context; 
16723  512 
val _ = Context.check_thy thy; 
18857  513 
val S = intern_sort thy (Syntax.read_sort context syn str); 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

514 
in certify_sort thy S handle TYPE (msg, _, _) => error msg end; 
16337  515 

18857  516 
fun read_sort thy str = read_sort' (syn_of thy) (Context.Theory thy) str; 
16337  517 

518 

19244
1d7e51d9828b
added read_class, read/cert_classrel/arity (from axclass.ML);
wenzelm
parents:
19099
diff
changeset

519 
(* type arities *) 
1d7e51d9828b
added read_class, read/cert_classrel/arity (from axclass.ML);
wenzelm
parents:
19099
diff
changeset

520 

1d7e51d9828b
added read_class, read/cert_classrel/arity (from axclass.ML);
wenzelm
parents:
19099
diff
changeset

521 
fun prep_arity prep_tycon prep_sort thy (t, Ss, S) = 
1d7e51d9828b
added read_class, read/cert_classrel/arity (from axclass.ML);
wenzelm
parents:
19099
diff
changeset

522 
let val arity = (prep_tycon thy t, map (prep_sort thy) Ss, prep_sort thy S) 
19513
77ff7cd602d7
removed add_classes/classrel/arities (superceded by AxClass.axiomatize_class/classrel/arity);
wenzelm
parents:
19482
diff
changeset

523 
in Type.add_arity (pp thy) arity (tsig_of thy); arity end; 
19244
1d7e51d9828b
added read_class, read/cert_classrel/arity (from axclass.ML);
wenzelm
parents:
19099
diff
changeset

524 

1d7e51d9828b
added read_class, read/cert_classrel/arity (from axclass.ML);
wenzelm
parents:
19099
diff
changeset

525 
val read_arity = prep_arity intern_type read_sort; 
1d7e51d9828b
added read_class, read/cert_classrel/arity (from axclass.ML);
wenzelm
parents:
19099
diff
changeset

526 
val cert_arity = prep_arity (K I) certify_sort; 
1d7e51d9828b
added read_class, read/cert_classrel/arity (from axclass.ML);
wenzelm
parents:
19099
diff
changeset

527 

1d7e51d9828b
added read_class, read/cert_classrel/arity (from axclass.ML);
wenzelm
parents:
19099
diff
changeset

528 

16337  529 
(* types *) 
530 

531 
local 

532 

18857  533 
fun gen_read_typ' cert syn context def_sort str = 
16337  534 
let 
18857  535 
val thy = Context.theory_of context; 
16723  536 
val _ = Context.check_thy thy; 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

537 
val get_sort = TypeInfer.get_sort (tsig_of thy) def_sort (intern_sort thy); 
18857  538 
val T = intern_tycons thy (Syntax.read_typ context syn get_sort (intern_sort thy) str); 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

539 
in cert thy T handle TYPE (msg, _, _) => error msg end 
18678  540 
handle ERROR msg => cat_error msg ("The error(s) above occurred in type " ^ quote str); 
16337  541 

16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

542 
fun gen_read_typ cert (thy, def_sort) str = 
18857  543 
gen_read_typ' cert (syn_of thy) (Context.Theory thy) def_sort str; 
16337  544 

545 
in 

546 

16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

547 
fun no_def_sort thy = (thy: theory, K NONE); 
16337  548 

16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

549 
val read_typ' = gen_read_typ' certify_typ; 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

550 
val read_typ_syntax' = gen_read_typ' certify_typ_syntax; 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

551 
val read_typ_abbrev' = gen_read_typ' certify_typ_abbrev; 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

552 
val read_typ = gen_read_typ certify_typ; 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

553 
val read_typ_syntax = gen_read_typ certify_typ_syntax; 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

554 
val read_typ_abbrev = gen_read_typ certify_typ_abbrev; 
16337  555 

556 
end; 

557 

558 

16368
a06868ebeb0f
discontinued named name spaces (classK, typeK, constK);
wenzelm
parents:
16354
diff
changeset

559 
(* type and constant names *) 
15703  560 

16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

561 
fun read_tyname thy raw_c = 
19462  562 
let val c = intern_type thy raw_c 
563 
in Type (c, replicate (arity_number thy c) dummyT) end; 

15703  564 

18967  565 
val read_const = Consts.read_const o consts_of; 
15703  566 

567 

251  568 

583  569 
(** infer_types **) (*exception ERROR*) 
251  570 

2979  571 
(* 
16337  572 
def_type: partial map from indexnames to types (constrains Frees and Vars) 
573 
def_sort: partial map from indexnames to sorts (constrains TFrees and TVars) 

20155  574 
used: context of already used type variables 
2979  575 
freeze: if true then generated parameters are turned into TFrees, else TVars 
4249  576 

577 
termss: lists of alternative parses (only one combination should be typecorrect) 

578 
typs: expected types 

2979  579 
*) 
580 

18967  581 
fun infer_types_simult pp thy consts def_type def_sort used freeze args = 
251  582 
let 
18146  583 
val termss = fold_rev (multiply o fst) args [[]]; 
4249  584 
val typs = 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

585 
map (fn (_, T) => certify_typ thy T handle TYPE (msg, _, _) => error msg) args; 
169  586 

18678  587 
fun infer ts = Result (TypeInfer.infer_types (Syntax.pp_show_brackets pp) (tsig_of thy) 
21722  588 
(try (Consts.the_constraint consts)) def_type def_sort (Consts.intern consts) 
18967  589 
(intern_tycons thy) (intern_sort thy) used freeze typs ts) 
18678  590 
handle TYPE (msg, _, _) => Exn (ERROR msg); 
623  591 

4249  592 
val err_results = map infer termss; 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19462
diff
changeset

593 
val errs = map_filter (fn Exn (ERROR msg) => SOME msg  _ => NONE) err_results; 
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19462
diff
changeset

594 
val results = map_filter get_result err_results; 
4249  595 

14645  596 
val ambiguity = length termss; 
4249  597 
fun ambig_msg () = 
18678  598 
if ambiguity > 1 andalso ambiguity <= ! Syntax.ambiguity_level then 
599 
"Got more than one parse tree.\n\ 

600 
\Retry with smaller Syntax.ambiguity_level for more information." 

601 
else ""; 

4249  602 
in 
18678  603 
if null results then (cat_error (ambig_msg ()) (cat_lines errs)) 
4249  604 
else if length results = 1 then 
605 
(if ambiguity > ! Syntax.ambiguity_level then 

606 
warning "Fortunately, only one parse tree is type correct.\n\ 

607 
\You may still want to disambiguate your grammar or your input." 

608 
else (); hd results) 

18678  609 
else (cat_error (ambig_msg ()) ("More than one term is type correct:\n" ^ 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19462
diff
changeset

610 
cat_lines (map (Pretty.string_of_term pp) (maps fst results)))) 
4249  611 
end; 
623  612 

18967  613 
fun infer_types pp thy consts def_type def_sort used freeze tsT = 
614 
apfst hd (infer_types_simult pp thy consts def_type def_sort used freeze [tsT]); 

251  615 

616 

16494  617 
(* read_def_terms  read terms and infer types *) (*exception ERROR*) 
16337  618 

18967  619 
fun read_def_terms' pp is_logtype syn consts context (types, sorts) used freeze sTs = 
8607  620 
let 
18857  621 
val thy = Context.theory_of context; 
8607  622 
fun read (s, T) = 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

623 
let val T' = certify_typ thy T handle TYPE (msg, _, _) => error msg 
18857  624 
in (Syntax.read context is_logtype syn T' s, T') end; 
18967  625 
in infer_types_simult pp thy consts types sorts used freeze (map read sTs) end; 
8607  626 

20230
04cb2d917de5
read_def_cterms (legacy version): Consts.certify;
wenzelm
parents:
20211
diff
changeset

627 
fun read_def_terms (thy, types, sorts) used freeze sTs = 
04cb2d917de5
read_def_cterms (legacy version): Consts.certify;
wenzelm
parents:
20211
diff
changeset

628 
let 
04cb2d917de5
read_def_cterms (legacy version): Consts.certify;
wenzelm
parents:
20211
diff
changeset

629 
val pp = pp thy; 
04cb2d917de5
read_def_cterms (legacy version): Consts.certify;
wenzelm
parents:
20211
diff
changeset

630 
val consts = consts_of thy; 
04cb2d917de5
read_def_cterms (legacy version): Consts.certify;
wenzelm
parents:
20211
diff
changeset

631 
val cert_consts = Consts.certify pp (tsig_of thy) consts; 
04cb2d917de5
read_def_cterms (legacy version): Consts.certify;
wenzelm
parents:
20211
diff
changeset

632 
val (ts, inst) = 
04cb2d917de5
read_def_cterms (legacy version): Consts.certify;
wenzelm
parents:
20211
diff
changeset

633 
read_def_terms' pp (is_logtype thy) (syn_of thy) consts 
04cb2d917de5
read_def_cterms (legacy version): Consts.certify;
wenzelm
parents:
20211
diff
changeset

634 
(Context.Theory thy) (types, sorts) (Name.make_context used) freeze sTs; 
04cb2d917de5
read_def_cterms (legacy version): Consts.certify;
wenzelm
parents:
20211
diff
changeset

635 
in (map cert_consts ts, inst) end; 
12068
469f372d63db
added pretty_term', read_typ', read_typ_no_norm', read_def_terms'
wenzelm
parents:
11720
diff
changeset

636 

16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

637 
fun simple_read_term thy T s = 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

638 
let val ([t], _) = read_def_terms (thy, K NONE, K NONE) [] true [(s, T)] 
20230
04cb2d917de5
read_def_cterms (legacy version): Consts.certify;
wenzelm
parents:
20211
diff
changeset

639 
in t end handle ERROR msg => cat_error msg ("The error(s) above occurred for term " ^ s); 
8802  640 

16494  641 
fun read_term thy = simple_read_term thy TypeInfer.logicT; 
642 
fun read_prop thy = simple_read_term thy propT; 

643 

8607  644 

2979  645 

16337  646 
(** signature extension functions **) (*exception ERROR/TYPE*) 
386  647 

648 
(* add default sort *) 

649 

16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

650 
fun gen_add_defsort prep_sort s thy = 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

651 
thy > map_tsig (Type.set_defsort (prep_sort thy s)); 
8898  652 

16337  653 
val add_defsort = gen_add_defsort read_sort; 
654 
val add_defsort_i = gen_add_defsort certify_sort; 

386  655 

656 

657 
(* add type constructors *) 

658 

16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

659 
fun add_types types thy = thy > map_sign (fn (naming, syn, tsig, consts) => 
14856  660 
let 
16597
5a5229a55964
eliminated separate syn type  advanced trfuns already part of Syntax.syntax;
wenzelm
parents:
16536
diff
changeset

661 
val syn' = Syntax.extend_type_gram types syn; 
16368
a06868ebeb0f
discontinued named name spaces (classK, typeK, constK);
wenzelm
parents:
16354
diff
changeset

662 
val decls = map (fn (a, n, mx) => (Syntax.type_name a mx, n)) types; 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

663 
val tsig' = Type.add_types naming decls tsig; 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

664 
in (naming, syn', tsig', consts) end); 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

665 

1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

666 
fun add_typedecls decls thy = 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

667 
let 
20664  668 
fun type_of (a, vs: string list, mx) = 
18928
042608ffa2ec
subsituted gen_duplicates / has_duplicates for duplicates whenever appropriate
haftmann
parents:
18892
diff
changeset

669 
if not (has_duplicates (op =) vs) then (a, length vs, mx) 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

670 
else error ("Duplicate parameters in type declaration: " ^ quote a); 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

671 
in add_types (map type_of decls) thy end; 
16337  672 

673 

674 
(* add nonterminals *) 

675 

16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

676 
fun add_nonterminals ns thy = thy > map_sign (fn (naming, syn, tsig, consts) => 
16337  677 
let 
16597
5a5229a55964
eliminated separate syn type  advanced trfuns already part of Syntax.syntax;
wenzelm
parents:
16536
diff
changeset

678 
val syn' = Syntax.extend_consts ns syn; 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

679 
val tsig' = Type.add_nonterminals naming ns tsig; 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

680 
in (naming, syn', tsig', consts) end); 
386  681 

682 

683 
(* add type abbreviations *) 

684 

16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

685 
fun gen_add_tyabbr prep_typ (a, vs, rhs, mx) thy = 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

686 
thy > map_sign (fn (naming, syn, tsig, consts) => 
16337  687 
let 
16597
5a5229a55964
eliminated separate syn type  advanced trfuns already part of Syntax.syntax;
wenzelm
parents:
16536
diff
changeset

688 
val syn' = Syntax.extend_type_gram [(a, length vs, mx)] syn; 
16368
a06868ebeb0f
discontinued named name spaces (classK, typeK, constK);
wenzelm
parents:
16354
diff
changeset

689 
val a' = Syntax.type_name a mx; 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

690 
val abbr = (a', vs, prep_typ thy rhs) 
18678  691 
handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote a'); 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

692 
val tsig' = Type.add_abbrevs naming [abbr] tsig; 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

693 
in (naming, syn', tsig', consts) end); 
386  694 

16337  695 
val add_tyabbrs = fold (gen_add_tyabbr (read_typ_syntax o no_def_sort)); 
696 
val add_tyabbrs_i = fold (gen_add_tyabbr certify_typ_syntax); 

14784
e65d77313a94
xxx_typ_raw replace xxx_typ_no_norm forms; prevent duplicate consts declarations in merge; misc cleanup;
wenzelm
parents:
14700
diff
changeset

697 

e65d77313a94
xxx_typ_raw replace xxx_typ_no_norm forms; prevent duplicate consts declarations in merge; misc cleanup;
wenzelm
parents:
14700
diff
changeset

698 

16337  699 
(* modify syntax *) 
700 

20784  701 
fun gen_syntax change_gram prep_typ mode args thy = 
16337  702 
let 
18678  703 
fun prep (c, T, mx) = (c, prep_typ thy T, mx) handle ERROR msg => 
704 
cat_error msg ("in syntax declaration " ^ quote (Syntax.const_name c mx)); 

20784  705 
in thy > map_syn (change_gram (is_logtype thy) mode (map prep args)) end; 
16337  706 

707 
fun gen_add_syntax x = gen_syntax Syntax.extend_const_gram x; 

386  708 

16337  709 
val add_modesyntax = gen_add_syntax (read_typ_syntax o no_def_sort); 
710 
val add_modesyntax_i = gen_add_syntax certify_typ_syntax; 

16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

711 
val add_syntax = add_modesyntax Syntax.default_mode; 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

712 
val add_syntax_i = add_modesyntax_i Syntax.default_mode; 
16337  713 
val del_modesyntax = gen_syntax Syntax.remove_const_gram (read_typ_syntax o no_def_sort); 
714 
val del_modesyntax_i = gen_syntax Syntax.remove_const_gram certify_typ_syntax; 

3805  715 

21661
e070569dd638
add_notation: permissive about undeclared consts;
wenzelm
parents:
21269
diff
changeset

716 
fun const_syntax thy (Const (c, _), mx) = try (Consts.syntax (consts_of thy)) (c, mx) 
21206
2af4c7b3f7ef
replaced const_syntax by notation, which operates on terms;
wenzelm
parents:
21183
diff
changeset

717 
 const_syntax _ _ = NONE; 
2af4c7b3f7ef
replaced const_syntax by notation, which operates on terms;
wenzelm
parents:
21183
diff
changeset

718 

2af4c7b3f7ef
replaced const_syntax by notation, which operates on terms;
wenzelm
parents:
21183
diff
changeset

719 
fun add_notation mode args thy = 
2af4c7b3f7ef
replaced const_syntax by notation, which operates on terms;
wenzelm
parents:
21183
diff
changeset

720 
thy > add_modesyntax_i mode (map_filter (const_syntax thy) args); 
19658  721 

16337  722 

723 
(* add constants *) 

386  724 

17995  725 
local 
726 

19679
ae4c1e2742c1
consts: replaced early'' flag by inverted authentic'';
wenzelm
parents:
19673
diff
changeset

727 
fun gen_add_consts prep_typ authentic raw_args thy = 
386  728 
let 
19806  729 
val prepT = Compress.typ thy o Logic.varifyT o Type.no_tvars o Term.no_dummyT o prep_typ thy; 
19658  730 
fun prep (raw_c, raw_T, raw_mx) = 
731 
let 

732 
val (c, mx) = Syntax.const_mixfix raw_c raw_mx; 

19679
ae4c1e2742c1
consts: replaced early'' flag by inverted authentic'';
wenzelm
parents:
19673
diff
changeset

733 
val c' = if authentic then Syntax.constN ^ full_name thy c else c; 
19658  734 
val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg => 
735 
cat_error msg ("in declaration of constant " ^ quote c); 

19679
ae4c1e2742c1
consts: replaced early'' flag by inverted authentic'';
wenzelm
parents:
19673
diff
changeset

736 
in (((c, T), authentic), (c', T, mx)) end; 
16337  737 
val args = map prep raw_args; 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

738 
in 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

739 
thy 
19658  740 
> map_consts (fold (Consts.declare (naming_of thy) o #1) args) 
741 
> add_syntax_i (map #2 args) 

16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

742 
end; 
386  743 

17995  744 
in 
745 

19679
ae4c1e2742c1
consts: replaced early'' flag by inverted authentic'';
wenzelm
parents:
19673
diff
changeset

746 
val add_consts = gen_add_consts (read_typ o no_def_sort) false; 
ae4c1e2742c1
consts: replaced early'' flag by inverted authentic'';
wenzelm
parents:
19673
diff
changeset

747 
val add_consts_i = gen_add_consts certify_typ false; 
ae4c1e2742c1
consts: replaced early'' flag by inverted authentic'';
wenzelm
parents:
19673
diff
changeset

748 
val add_consts_authentic = gen_add_consts certify_typ true; 
386  749 

17995  750 
end; 
751 

386  752 

21696  753 
(* add abbreviations *) 
18941  754 

21704  755 
fun add_abbrev mode (c, raw_t) thy = 
18941  756 
let 
21681  757 
val prep_tm = Compress.term thy o Term.no_dummy_patterns o cert_term_abbrev thy; 
19806  758 
val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg  TERM (msg, _) => error msg) 
19366
a2040baa9444
pretty_term': early vs. late externing (support authentic syntax);
wenzelm
parents:
19289
diff
changeset

759 
handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c); 
21696  760 
val (res, consts') = consts_of thy 
21722  761 
> Consts.abbreviate (pp thy) (tsig_of thy) (naming_of thy) mode (c, t); 
21704  762 
in (res, thy > map_consts (K consts')) end; 
18941  763 

764 

16941
0bda949449ee
added add_const_constraint(_i), const_constraint;
wenzelm
parents:
16894
diff
changeset

765 
(* add constraints *) 
0bda949449ee
added add_const_constraint(_i), const_constraint;
wenzelm
parents:
16894
diff
changeset

766 

19099
100bf66d7e85
add_const_constraint(_i): demand TFrees instead of TVars, optional type (i.e. may delete constraints);
wenzelm
parents:
19054
diff
changeset

767 
fun gen_add_constraint int_const prep_typ (raw_c, opt_T) thy = 
16941
0bda949449ee
added add_const_constraint(_i), const_constraint;
wenzelm
parents:
16894
diff
changeset

768 
let 
0bda949449ee
added add_const_constraint(_i), const_constraint;
wenzelm
parents:
16894
diff
changeset

769 
val c = int_const thy raw_c; 
19099
100bf66d7e85
add_const_constraint(_i): demand TFrees instead of TVars, optional type (i.e. may delete constraints);
wenzelm
parents:
19054
diff
changeset

770 
fun prepT raw_T = 
19806  771 
let val T = Logic.varifyT (Type.no_tvars (Term.no_dummyT (prep_typ thy raw_T))) 
19099
100bf66d7e85
add_const_constraint(_i): demand TFrees instead of TVars, optional type (i.e. may delete constraints);
wenzelm
parents:
19054
diff
changeset

772 
in cert_term thy (Const (c, T)); T end 
16941
0bda949449ee
added add_const_constraint(_i), const_constraint;
wenzelm
parents:
16894
diff
changeset

773 
handle TYPE (msg, _, _) => error msg; 
19099
100bf66d7e85
add_const_constraint(_i): demand TFrees instead of TVars, optional type (i.e. may delete constraints);
wenzelm
parents:
19054
diff
changeset

774 
in thy > map_consts (Consts.constrain (c, Option.map prepT opt_T)) end; 
16941
0bda949449ee
added add_const_constraint(_i), const_constraint;
wenzelm
parents:
16894
diff
changeset

775 

0bda949449ee
added add_const_constraint(_i), const_constraint;
wenzelm
parents:
16894
diff
changeset

776 
val add_const_constraint = gen_add_constraint intern_const (read_typ o no_def_sort); 
0bda949449ee
added add_const_constraint(_i), const_constraint;
wenzelm
parents:
16894
diff
changeset

777 
val add_const_constraint_i = gen_add_constraint (K I) certify_typ; 
0bda949449ee
added add_const_constraint(_i), const_constraint;
wenzelm
parents:
16894
diff
changeset

778 

0bda949449ee
added add_const_constraint(_i), const_constraint;
wenzelm
parents:
16894
diff
changeset

779 

19513
77ff7cd602d7
removed add_classes/classrel/arities (superceded by AxClass.axiomatize_class/classrel/arity);
wenzelm
parents:
19482
diff
changeset

780 
(* primitive classes and arities *) 
386  781 

19513
77ff7cd602d7
removed add_classes/classrel/arities (superceded by AxClass.axiomatize_class/classrel/arity);
wenzelm
parents:
19482
diff
changeset

782 
fun primitive_class (bclass, classes) thy = 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

783 
thy > map_sign (fn (naming, syn, tsig, consts) => 
16337  784 
let 
16597
5a5229a55964
eliminated separate syn type  advanced trfuns already part of Syntax.syntax;
wenzelm
parents:
16536
diff
changeset

785 
val syn' = Syntax.extend_consts [bclass] syn; 
19513
77ff7cd602d7
removed add_classes/classrel/arities (superceded by AxClass.axiomatize_class/classrel/arity);
wenzelm
parents:
19482
diff
changeset

786 
val tsig' = Type.add_class (pp thy) naming (bclass, classes) tsig; 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

787 
in (naming, syn', tsig', consts) end) 
19391  788 
> add_consts_i [(Logic.const_of_class bclass, Term.a_itselfT > propT, NoSyn)]; 
3791
c5db2c87a646
now supports qualified names (intern vs. extern) !!!
wenzelm
parents:
3552
diff
changeset

789 

19513
77ff7cd602d7
removed add_classes/classrel/arities (superceded by AxClass.axiomatize_class/classrel/arity);
wenzelm
parents:
19482
diff
changeset

790 
fun primitive_classrel arg thy = thy > map_tsig (Type.add_classrel (pp thy) arg); 
77ff7cd602d7
removed add_classes/classrel/arities (superceded by AxClass.axiomatize_class/classrel/arity);
wenzelm
parents:
19482
diff
changeset

791 
fun primitive_arity arg thy = thy > map_tsig (Type.add_arity (pp thy) arg); 
421  792 

793 

14645  794 
(* add translation functions *) 
795 

15746  796 
local 
797 

798 
fun mk trs = map Syntax.mk_trfun trs; 

799 

16597
5a5229a55964
eliminated separate syn type  advanced trfuns already part of Syntax.syntax;
wenzelm
parents:
16536
diff
changeset

800 
fun gen_add_trfuns ext non_typed (atrs, trs, tr's, atr's) = 
5a5229a55964
eliminated separate syn type  advanced trfuns already part of Syntax.syntax;
wenzelm
parents:
16536
diff
changeset

801 
map_syn (ext (mk atrs, mk trs, mk (map (apsnd non_typed) tr's), mk atr's)); 
14645  802 

16597
5a5229a55964
eliminated separate syn type  advanced trfuns already part of Syntax.syntax;
wenzelm
parents:
16536
diff
changeset

803 
fun gen_add_trfunsT ext tr's = map_syn (ext ([], [], mk tr's, [])); 
14645  804 

15746  805 
in 
806 

16597
5a5229a55964
eliminated separate syn type  advanced trfuns already part of Syntax.syntax;
wenzelm
parents:
16536
diff
changeset

807 
val add_trfuns = gen_add_trfuns Syntax.extend_trfuns Syntax.non_typed_tr'; 
5a5229a55964
eliminated separate syn type  advanced trfuns already part of Syntax.syntax;
wenzelm
parents:
16536
diff
changeset

808 
val add_trfunsT = gen_add_trfunsT Syntax.extend_trfuns; 
5a5229a55964
eliminated separate syn type  advanced trfuns already part of Syntax.syntax;
wenzelm
parents:
16536
diff
changeset

809 
val add_advanced_trfuns = gen_add_trfuns Syntax.extend_advanced_trfuns Syntax.non_typed_tr''; 
5a5229a55964
eliminated separate syn type  advanced trfuns already part of Syntax.syntax;
wenzelm
parents:
16536
diff
changeset

810 
val add_advanced_trfunsT = gen_add_trfunsT Syntax.extend_advanced_trfuns; 
14645  811 

15746  812 
end; 
813 

16597
5a5229a55964
eliminated separate syn type  advanced trfuns already part of Syntax.syntax;
wenzelm
parents:
16536
diff
changeset

814 
val add_tokentrfuns = map_syn o Syntax.extend_tokentrfuns; 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

815 
fun add_mode_tokentrfuns m = add_tokentrfuns o map (fn (s, f) => (m, s, f)); 
14645  816 

817 

17102
a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

818 
(* compile translation functions *) 
a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

819 

a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

820 
local 
a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

821 

a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

822 
fun advancedT false = "" 
18857  823 
 advancedT true = "Context.generic > "; 
17102
a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

824 

a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

825 
fun advancedN false = "" 
a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

826 
 advancedN true = "advanced_"; 
a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

827 

a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

828 
in 
a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

829 

a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

830 
fun parse_ast_translation (a, txt) = 
a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

831 
txt > Context.use_let ("val parse_ast_translation: (string * (" ^ advancedT a ^ 
a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

832 
"Syntax.ast list > Syntax.ast)) list") 
a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

833 
("Sign.add_" ^ advancedN a ^ "trfuns (parse_ast_translation, [], [], [])"); 
a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

834 

a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

835 
fun parse_translation (a, txt) = 
a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

836 
txt > Context.use_let ("val parse_translation: (string * (" ^ advancedT a ^ 
a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

837 
"term list > term)) list") 
a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

838 
("Sign.add_" ^ advancedN a ^ "trfuns ([], parse_translation, [], [])"); 
a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

839 

a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

840 
fun print_translation (a, txt) = 
a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

841 
txt > Context.use_let ("val print_translation: (string * (" ^ advancedT a ^ 
a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

842 
"term list > term)) list") 
a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

843 
("Sign.add_" ^ advancedN a ^ "trfuns ([], [], print_translation, [])"); 
a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

844 

a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

845 
fun print_ast_translation (a, txt) = 
a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

846 
txt > Context.use_let ("val print_ast_translation: (string * (" ^ advancedT a ^ 
a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

847 
"Syntax.ast list > Syntax.ast)) list") 
a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

848 
("Sign.add_" ^ advancedN a ^ "trfuns ([], [], [], print_ast_translation)"); 
a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

849 

a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

850 
fun typed_print_translation (a, txt) = 
a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

851 
txt > Context.use_let ("val typed_print_translation: (string * (" ^ advancedT a ^ 
a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

852 
"bool > typ > term list > term)) list") 
a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

853 
("Sign.add_" ^ advancedN a ^ "trfunsT typed_print_translation"); 
a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

854 

a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

855 
val token_translation = 
a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

856 
Context.use_let "val token_translation: (string * string * (string > string * real)) list" 
a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

857 
"Sign.add_tokentrfuns token_translation"; 
a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

858 

a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

859 
end; 
a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

860 

a83a80f1c8dd
added interfaces for compile translation functions (from Isar/isar_thy.ML);
wenzelm
parents:
17039
diff
changeset

861 

19258
ada9977f1e98
declared_const: check for type constraint only, i.e. admit abbreviations as well;
wenzelm
parents:
19250
diff
changeset

862 
(* translation rules *) 
4619  863 

19258
ada9977f1e98
declared_const: check for type constraint only, i.e. admit abbreviations as well;
wenzelm
parents:
19250
diff
changeset

864 
fun gen_trrules f args thy = thy > map_syn (fn syn => 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

865 
let val rules = map (Syntax.map_trrule (apfst (intern_type thy))) args 
19258
ada9977f1e98
declared_const: check for type constraint only, i.e. admit abbreviations as well;
wenzelm
parents:
19250
diff
changeset

866 
in f (Context.Theory thy) (is_logtype thy) syn rules syn end); 
8725  867 

19258
ada9977f1e98
declared_const: check for type constraint only, i.e. admit abbreviations as well;
wenzelm
parents:
19250
diff
changeset

868 
val add_trrules = gen_trrules Syntax.extend_trrules; 
ada9977f1e98
declared_const: check for type constraint only, i.e. admit abbreviations as well;
wenzelm
parents:
19250
diff
changeset

869 
val del_trrules = gen_trrules Syntax.remove_trrules; 
16597
5a5229a55964
eliminated separate syn type  advanced trfuns already part of Syntax.syntax;
wenzelm
parents:
16536
diff
changeset

870 
val add_trrules_i = map_syn o Syntax.extend_trrules_i; 
19258
ada9977f1e98
declared_const: check for type constraint only, i.e. admit abbreviations as well;
wenzelm
parents:
19250
diff
changeset

871 
val del_trrules_i = map_syn o Syntax.remove_trrules_i; 
386  872 

873 

16337  874 
(* modify naming *) 
6546  875 

19054
af7cc6063285
replaced qualified_force_prefix to sticky_prefix;
wenzelm
parents:
19013
diff
changeset

876 
val add_path = map_naming o NameSpace.add_path; 
af7cc6063285
replaced qualified_force_prefix to sticky_prefix;
wenzelm
parents:
19013
diff
changeset

877 
val no_base_names = map_naming NameSpace.no_base_names; 
af7cc6063285
replaced qualified_force_prefix to sticky_prefix;
wenzelm
parents:
19013
diff
changeset

878 
val qualified_names = map_naming NameSpace.qualified_names; 
af7cc6063285
replaced qualified_force_prefix to sticky_prefix;
wenzelm
parents:
19013
diff
changeset

879 
val sticky_prefix = map_naming o NameSpace.sticky_prefix; 
af7cc6063285
replaced qualified_force_prefix to sticky_prefix;
wenzelm
parents:
19013
diff
changeset

880 
val set_policy = map_naming o NameSpace.set_policy; 
af7cc6063285
replaced qualified_force_prefix to sticky_prefix;
wenzelm
parents:
19013
diff
changeset

881 
val restore_naming = map_naming o K o naming_of; 
6546  882 

19013  883 
val parent_path = add_path ".."; 
884 
val root_path = add_path "/"; 

885 
val absolute_path = add_path "//"; 

16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

886 

1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

887 
fun local_path thy = thy > root_path > add_path (Context.theory_name thy); 
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

888 

6546  889 

16337  890 
(* hide names *) 
386  891 

16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

892 
fun hide_classes b xs thy = thy > map_tsig (Type.hide_classes b (map (intern_class thy) xs)); 
16368
a06868ebeb0f
discontinued named name spaces (classK, typeK, constK);
wenzelm
parents:
16354
diff
changeset

893 
val hide_classes_i = map_tsig oo Type.hide_classes; 
16442
1171ecf7fb7e
obsolete type sg is now an alias for Context.theory;
wenzelm
parents:
16368
diff
changeset

894 
fun hide_types b xs thy = thy > map_tsig (Type.hide_types b (map (intern_type thy) xs)); 
16368
a06868ebeb0f
discontinued named name spaces (classK, typeK, constK);
wenzelm
parents:
16354
diff
changeset

895 
val hide_types_i = map_tsig oo Type.hide_types; 
18062  896 
fun hide_consts b xs thy = thy > map_consts (fold (Consts.hide b o intern_const thy) xs); 
897 
val hide_consts_i = map_consts oo (fold o Consts.hide); 

386  898 

17343  899 
local 
900 

901 
val kinds = 

902 
[("class", (intern_class, can o certify_class, hide_classes_i)), 

903 
("type", (intern_type, declared_tyname, hide_types_i)), 

904 
("const", (intern_const, declared_const, hide_consts_i))]; 

905 

906 
fun gen_hide int b (kind, xnames) thy = 

907 
(case AList.lookup (op =) kinds kind of 

908 
SOME (intern, check, hide) => 

909 
let 

910 
val names = if int then map (intern thy) xnames else xnames; 

911 
val bads = filter_out (check thy) names; 

912 
in 

913 
if null bads then hide b names thy 

914 
else error ("Attempt to hide undeclared item(s): " ^ commas_quote bads) 

915 
end 

916 
 NONE => error ("Bad name space specification: " ^ quote kind)); 

917 

918 
in 

919 

920 
val hide_names = gen_hide true; 

921 
val hide_names_i = gen_hide false; 

922 

0  923 
end; 
17343  924 

925 
end; 