author  wenzelm 
Mon, 05 May 2014 15:17:07 +0200  
changeset 56864  0446c7ac2e32 
parent 56438  7f6b2634d853 
child 56867  224109105008 
permissions  rwrr 
5819  1 
(* Title: Pure/Isar/proof_context.ML 
2 
Author: Markus Wenzel, TU Muenchen 

3 

19001  4 
The key concept of Isar proof contexts: elevates primitive local 
5 
reasoning Gamma  phi to a structured concept, with generic context 

20234
7e0693474bcd
added legacy_pretty_thm (with fallback on ProtoPure.thy);
wenzelm
parents:
20209
diff
changeset

6 
elements. See also structure Variable and Assumption. 
5819  7 
*) 
8 

9 
signature PROOF_CONTEXT = 

10 
sig 

20310  11 
val theory_of: Proof.context > theory 
36610
bafd82950e24
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
wenzelm
parents:
36542
diff
changeset

12 
val init_global: theory > Proof.context 
51686  13 
val get_global: theory > string > Proof.context 
24388
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

14 
type mode 
24501  15 
val mode_default: mode 
16 
val mode_stmt: mode 

17 
val mode_pattern: mode 

18 
val mode_schematic: mode 

19 
val mode_abbrev: mode 

24388
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

20 
val set_mode: mode > Proof.context > Proof.context 
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

21 
val get_mode: Proof.context > mode 
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

22 
val restore_mode: Proof.context > Proof.context > Proof.context 
27286  23 
val abbrev_mode: Proof.context > bool 
21667
ce813b82c88b
add_notation: permissive about undeclared consts;
wenzelm
parents:
21648
diff
changeset

24 
val set_stmt: bool > Proof.context > Proof.context 
42241
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
42224
diff
changeset

25 
val syntax_of: Proof.context > Local_Syntax.T 
35111  26 
val syn_of: Proof.context > Syntax.syntax 
35669
a91c7ed801b8
added ProofContext.tsig_of  proforma version for local name space only, not logical content;
wenzelm
parents:
35616
diff
changeset

27 
val tsig_of: Proof.context > Type.tsig 
36451  28 
val set_defsort: sort > Proof.context > Proof.context 
35680  29 
val default_sort: Proof.context > indexname > sort 
20310  30 
val consts_of: Proof.context > Consts.T 
20784  31 
val set_syntax_mode: Syntax.mode > Proof.context > Proof.context 
20310  32 
val restore_syntax_mode: Proof.context > Proof.context > Proof.context 
47005
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset

33 
val map_naming: (Name_Space.naming > Name_Space.naming) > Proof.context > Proof.context 
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset

34 
val naming_of: Proof.context > Name_Space.naming 
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset

35 
val restore_naming: Proof.context > Proof.context > Proof.context 
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset

36 
val full_name: Proof.context > binding > string 
42359  37 
val class_space: Proof.context > Name_Space.T 
38 
val type_space: Proof.context > Name_Space.T 

39 
val const_space: Proof.context > Name_Space.T 

40 
val intern_class: Proof.context > xstring > string 

41 
val intern_type: Proof.context > xstring > string 

42 
val intern_const: Proof.context > xstring > string 

43 
val extern_class: Proof.context > string > xstring 

55304  44 
val markup_class: Proof.context > string > string 
45 
val pretty_class: Proof.context > string > Pretty.T 

42359  46 
val extern_type: Proof.context > string > xstring 
55304  47 
val markup_type: Proof.context > string > string 
48 
val pretty_type: Proof.context > string > Pretty.T 

42359  49 
val extern_const: Proof.context > string > xstring 
55304  50 
val markup_const: Proof.context > string > string 
51 
val pretty_const: Proof.context > string > Pretty.T 

20310  52 
val transfer: theory > Proof.context > Proof.context 
38756
d07959fabde6
renamed ProofContext.theory(_result) to ProofContext.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in userspace tools;
wenzelm
parents:
38328
diff
changeset

53 
val background_theory: (theory > theory) > Proof.context > Proof.context 
d07959fabde6
renamed ProofContext.theory(_result) to ProofContext.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in userspace tools;
wenzelm
parents:
38328
diff
changeset

54 
val background_theory_result: (theory > 'a * theory) > Proof.context > 'a * Proof.context 
56141
c06202417c4a
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
wenzelm
parents:
56140
diff
changeset

55 
val facts_of: Proof.context > Facts.T 
c06202417c4a
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
wenzelm
parents:
56140
diff
changeset

56 
val facts_of_fact: Proof.context > string > Facts.T 
c06202417c4a
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
wenzelm
parents:
56140
diff
changeset

57 
val markup_extern_fact: Proof.context > string > Markup.T * xstring 
21728  58 
val pretty_term_abbrev: Proof.context > term > Pretty.T 
20310  59 
val pretty_fact: Proof.context > string * thm list > Pretty.T 
55922
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55843
diff
changeset

60 
val check_class: Proof.context > xstring * Position.T > class * Position.report list 
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55843
diff
changeset

61 
val read_class: Proof.context > string > class 
20310  62 
val read_typ: Proof.context > string > typ 
63 
val read_typ_syntax: Proof.context > string > typ 

64 
val read_typ_abbrev: Proof.context > string > typ 

65 
val cert_typ: Proof.context > typ > typ 

66 
val cert_typ_syntax: Proof.context > typ > typ 

67 
val cert_typ_abbrev: Proof.context > typ > typ 

36505
79c1d2bbe5a9
ProofContext.read_const: allow for type constraint (for fixed variable);
wenzelm
parents:
36503
diff
changeset

68 
val infer_type: Proof.context > string * typ > typ 
28082
37350f301128
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
28017
diff
changeset

69 
val inferred_param: string > Proof.context > typ * Proof.context 
25328  70 
val inferred_fixes: Proof.context > (string * typ) list * Proof.context 
56002  71 
val check_type_name: {proper: bool, strict: bool} > Proof.context > 
55922
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55843
diff
changeset

72 
xstring * Position.T > typ * Position.report list 
56002  73 
val read_type_name: {proper: bool, strict: bool} > Proof.context > string > typ 
55956
94d384d621b0
reject internal term names outright, and complete consts instead;
wenzelm
parents:
55955
diff
changeset

74 
val consts_completion_message: Proof.context > xstring * Position.T list > string 
56002  75 
val check_const: {proper: bool, strict: bool} > Proof.context > 
55959
c3b458435f4f
more decisive commitment to get_free vs. the_const;
wenzelm
parents:
55956
diff
changeset

76 
xstring * Position.T list > term * Position.report list 
56002  77 
val read_const: {proper: bool, strict: bool} > Proof.context > string > term 
46922
3717f3878714
source positions for locale and class expressions;
wenzelm
parents:
46849
diff
changeset

78 
val read_arity: Proof.context > xstring * string list * string > arity 
3717f3878714
source positions for locale and class expressions;
wenzelm
parents:
46849
diff
changeset

79 
val cert_arity: Proof.context > arity > arity 
27259  80 
val allow_dummies: Proof.context > Proof.context 
56333
38f1422ef473
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents:
56294
diff
changeset

81 
val prepare_sortsT: Proof.context > typ list > string list * typ list 
38f1422ef473
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents:
56294
diff
changeset

82 
val prepare_sorts: Proof.context > term list > string list * term list 
36152  83 
val check_tfree: Proof.context > string * sort > string * sort 
24684  84 
val read_term_pattern: Proof.context > string > term 
85 
val read_term_schematic: Proof.context > string > term 

86 
val read_term_abbrev: Proof.context > string > term 

40879
ca132ef44944
configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
wenzelm
parents:
39557
diff
changeset

87 
val show_abbrevs_raw: Config.raw 
ca132ef44944
configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
wenzelm
parents:
39557
diff
changeset

88 
val show_abbrevs: bool Config.T 
25345
dd5b851f8ef0
renamed ProofContext.read_const' to ProofContext.read_const_proper;
wenzelm
parents:
25332
diff
changeset

89 
val expand_abbrevs: Proof.context > term > term 
20310  90 
val cert_term: Proof.context > term > term 
91 
val cert_prop: Proof.context > term > term 

35616
b342390d296f
provide ProofContext.def_type depending on "pattern" mode;
wenzelm
parents:
35429
diff
changeset

92 
val def_type: Proof.context > indexname > typ option 
45429  93 
val standard_typ_check: Proof.context > typ list > typ list 
94 
val standard_term_check_finish: Proof.context > term list > term list 

95 
val standard_term_uncheck: Proof.context > term list > term list 

20310  96 
val goal_export: Proof.context > Proof.context > thm list > thm list 
97 
val export: Proof.context > Proof.context > thm list > thm list 

21531  98 
val export_morphism: Proof.context > Proof.context > morphism 
28396  99 
val norm_export_morphism: Proof.context > Proof.context > morphism 
30757
2d2076300185
replaced add_binds(_i) by bind_terms  internal version only;
wenzelm
parents:
30723
diff
changeset

100 
val bind_terms: (indexname * term option) list > Proof.context > Proof.context 
20310  101 
val auto_bind_goal: term list > Proof.context > Proof.context 
102 
val auto_bind_facts: term list > Proof.context > Proof.context 

103 
val match_bind: bool > (string list * string) list > Proof.context > term list * Proof.context 

104 
val match_bind_i: bool > (term list * term) list > Proof.context > term list * Proof.context 

45327  105 
val read_propp: (string * string list) list list > Proof.context > 
106 
(term * term list) list list * Proof.context 

107 
val cert_propp: (term * term list) list list > Proof.context > 

108 
(term * term list) list list * Proof.context 

109 
val read_propp_schematic: (string * string list) list list > Proof.context > 

110 
(term * term list) list list * Proof.context 

111 
val cert_propp_schematic: (term * term list) list list > Proof.context > 

112 
(term * term list) list list * Proof.context 

113 
val bind_propp: (string * string list) list list > Proof.context > 

114 
(term list list * (Proof.context > Proof.context)) * Proof.context 

115 
val bind_propp_i: (term * term list) list list > Proof.context > 

116 
(term list list * (Proof.context > Proof.context)) * Proof.context 

117 
val bind_propp_schematic: (string * string list) list list > Proof.context > 

118 
(term list list * (Proof.context > Proof.context)) * Proof.context 

119 
val bind_propp_schematic_i: (term * term list) list list > Proof.context > 

120 
(term list list * (Proof.context > Proof.context)) * Proof.context 

54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54740
diff
changeset

121 
val fact_tac: Proof.context > thm list > int > tactic 
20310  122 
val some_fact_tac: Proof.context > int > tactic 
56140
ed92ce2ac88e
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
wenzelm
parents:
56139
diff
changeset

123 
val get_fact_generic: Context.generic > Facts.ref > thm list 
26346
17debd2fff8e
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset

124 
val get_fact: Proof.context > Facts.ref > thm list 
17debd2fff8e
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset

125 
val get_fact_single: Proof.context > Facts.ref > thm 
17debd2fff8e
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset

126 
val get_thms: Proof.context > xstring > thm list 
17debd2fff8e
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset

127 
val get_thm: Proof.context > xstring > thm 
30761
ac7570d80c3d
renamed ProofContext.note_thmss_i to ProofContext.note_thmss, eliminated obsolete external version;
wenzelm
parents:
30758
diff
changeset

128 
val note_thmss: string > (Thm.binding * (thm list * attribute list) list) list > 
30211  129 
Proof.context > (string * thm list) list * Proof.context 
28082
37350f301128
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
28017
diff
changeset

130 
val put_thms: bool > string * thm list option > Proof.context > Proof.context 
29581  131 
val read_vars: (binding * string option * mixfix) list > Proof.context > 
132 
(binding * typ option * mixfix) list * Proof.context 

133 
val cert_vars: (binding * typ option * mixfix) list > Proof.context > 

134 
(binding * typ option * mixfix) list * Proof.context 

30763
6976521b4263
renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
wenzelm
parents:
30761
diff
changeset

135 
val add_fixes: (binding * typ option * mixfix) list > Proof.context > 
6976521b4263
renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
wenzelm
parents:
30761
diff
changeset

136 
string list * Proof.context 
20234
7e0693474bcd
added legacy_pretty_thm (with fallback on ProtoPure.thy);
wenzelm
parents:
20209
diff
changeset

137 
val add_assms: Assumption.export > 
30211  138 
(Thm.binding * (string * string list) list) list > 
28082
37350f301128
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
28017
diff
changeset

139 
Proof.context > (string * thm list) list * Proof.context 
20234
7e0693474bcd
added legacy_pretty_thm (with fallback on ProtoPure.thy);
wenzelm
parents:
20209
diff
changeset

140 
val add_assms_i: Assumption.export > 
30211  141 
(Thm.binding * (term * term list) list) list > 
28082
37350f301128
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
28017
diff
changeset

142 
Proof.context > (string * thm list) list * Proof.context 
53378
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

143 
val dest_cases: Proof.context > (string * (Rule_Cases.T * bool)) list 
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

144 
val update_cases: bool > (string * Rule_Cases.T option) list > Proof.context > Proof.context 
53380
08f3491c50bf
cases: formal binding of 'assumes', with position provided via invoke_case;
wenzelm
parents:
53378
diff
changeset

145 
val apply_case: Rule_Cases.T > Proof.context > (binding * term list) list * Proof.context 
53378
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

146 
val check_case: Proof.context > string * Position.T > binding option list > Rule_Cases.T 
35412
b8dead547d9e
more uniform treatment of syntax for types vs. consts;
wenzelm
parents:
35399
diff
changeset

147 
val type_notation: bool > Syntax.mode > (typ * mixfix) list > Proof.context > Proof.context 
24949  148 
val notation: bool > Syntax.mode > (term * mixfix) list > Proof.context > Proof.context 
47247  149 
val generic_type_notation: bool > Syntax.mode > (typ * mixfix) list > morphism > 
35412
b8dead547d9e
more uniform treatment of syntax for types vs. consts;
wenzelm
parents:
35399
diff
changeset

150 
Context.generic > Context.generic 
47247  151 
val generic_notation: bool > Syntax.mode > (term * mixfix) list > morphism > 
21744  152 
Context.generic > Context.generic 
35680  153 
val class_alias: binding > class > Proof.context > Proof.context 
154 
val type_alias: binding > string > Proof.context > Proof.context 

155 
val const_alias: binding > string > Proof.context > Proof.context 

24767  156 
val add_const_constraint: string * typ option > Proof.context > Proof.context 
33173
b8ca12f6681a
eliminated obsolete tags for types/consts  now handled via name space, in strongly typed fashion;
wenzelm
parents:
33165
diff
changeset

157 
val add_abbrev: string > binding * term > Proof.context > (term * term) * Proof.context 
25052  158 
val revert_abbrev: string > string > Proof.context > Proof.context 
47275  159 
val generic_add_abbrev: string > binding * term > Context.generic > 
160 
(term * term) * Context.generic 

161 
val generic_revert_abbrev: string > string > Context.generic > Context.generic 

20310  162 
val print_syntax: Proof.context > unit 
21728  163 
val print_abbrevs: Proof.context > unit 
20310  164 
val print_binds: Proof.context > unit 
56864  165 
val pretty_local_facts: Proof.context > bool > Pretty.T list 
56158
c2c6d560e7b2
more explicit treatment of verbose mode, which includes concealed entries;
wenzelm
parents:
56156
diff
changeset

166 
val print_local_facts: Proof.context > bool > unit 
20310  167 
val print_cases: Proof.context > unit 
42717
0bbb56867091
proper configuration options Proof_Context.debug and Proof_Context.verbose;
wenzelm
parents:
42502
diff
changeset

168 
val debug: bool Config.T 
0bbb56867091
proper configuration options Proof_Context.debug and Proof_Context.verbose;
wenzelm
parents:
42502
diff
changeset

169 
val verbose: bool Config.T 
20310  170 
val pretty_ctxt: Proof.context > Pretty.T list 
171 
val pretty_context: Proof.context > Pretty.T list 

5819  172 
end; 
173 

42360  174 
structure Proof_Context: PROOF_CONTEXT = 
5819  175 
struct 
176 

42363  177 
val theory_of = Proof_Context.theory_of; 
178 
val init_global = Proof_Context.init_global; 

51686  179 
val get_global = Proof_Context.get_global; 
42363  180 

12057  181 

7270  182 

24388
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

183 
(** inner syntax mode **) 
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

184 

cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

185 
datatype mode = 
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

186 
Mode of 
24486  187 
{stmt: bool, (*inner statement mode*) 
24388
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

188 
pattern: bool, (*pattern binding schematic variables*) 
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

189 
schematic: bool, (*term referencing loose schematic variables*) 
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

190 
abbrev: bool}; (*abbrev mode  no normalization*) 
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

191 

24486  192 
fun make_mode (stmt, pattern, schematic, abbrev) = 
193 
Mode {stmt = stmt, pattern = pattern, schematic = schematic, abbrev = abbrev}; 

24388
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

194 

24486  195 
val mode_default = make_mode (false, false, false, false); 
196 
val mode_stmt = make_mode (true, false, false, false); 

197 
val mode_pattern = make_mode (false, true, false, false); 

198 
val mode_schematic = make_mode (false, false, true, false); 

199 
val mode_abbrev = make_mode (false, false, false, true); 

24388
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

200 

cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

201 

5819  202 

16540  203 
(** Isar proof context information **) 
5819  204 

53378
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

205 
type cases = ((Rule_Cases.T * bool) * int) Name_Space.table; 
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

206 
val empty_cases: cases = Name_Space.empty_table Markup.caseN; 
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

207 

45650  208 
datatype data = 
209 
Data of 

36451  210 
{mode: mode, (*inner syntax mode*) 
211 
syntax: Local_Syntax.T, (*local syntax*) 

212 
tsig: Type.tsig * Type.tsig, (*local/global type signature  local name space / defsort only*) 

213 
consts: Consts.T * Consts.T, (*local/global consts  local name space / abbrevs only*) 

56141
c06202417c4a
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
wenzelm
parents:
56140
diff
changeset

214 
facts: Facts.T, (*local facts, based on initial global facts*) 
53378
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

215 
cases: cases}; (*named case contexts: case, is_proper, running index*) 
5819  216 

47005
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset

217 
fun make_data (mode, syntax, tsig, consts, facts, cases) = 
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset

218 
Data {mode = mode, syntax = syntax, tsig = tsig, consts = consts, facts = facts, cases = cases}; 
19079
9a7678a0736d
added put_thms_internal: local_naming, no fact index;
wenzelm
parents:
19062
diff
changeset

219 

37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37145
diff
changeset

220 
structure Data = Proof_Data 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

221 
( 
45650  222 
type T = data; 
16540  223 
fun init thy = 
56139
b7add947a6ef
more frugal recording of changes: join merely requires information from one side;
wenzelm
parents:
56062
diff
changeset

224 
make_data (mode_default, 
b7add947a6ef
more frugal recording of changes: join merely requires information from one side;
wenzelm
parents:
56062
diff
changeset

225 
Local_Syntax.init thy, 
b7add947a6ef
more frugal recording of changes: join merely requires information from one side;
wenzelm
parents:
56062
diff
changeset

226 
(Type.change_ignore (Sign.tsig_of thy), Sign.tsig_of thy), 
b7add947a6ef
more frugal recording of changes: join merely requires information from one side;
wenzelm
parents:
56062
diff
changeset

227 
(Consts.change_ignore (Sign.consts_of thy), Sign.consts_of thy), 
56140
ed92ce2ac88e
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
wenzelm
parents:
56139
diff
changeset

228 
Global_Theory.facts_of thy, 
56139
b7add947a6ef
more frugal recording of changes: join merely requires information from one side;
wenzelm
parents:
56062
diff
changeset

229 
empty_cases); 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

230 
); 
5819  231 

45650  232 
fun rep_data ctxt = Data.get ctxt > (fn Data rep => rep); 
5819  233 

45650  234 
fun map_data f = 
47005
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset

235 
Data.map (fn Data {mode, syntax, tsig, consts, facts, cases} => 
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset

236 
make_data (f (mode, syntax, tsig, consts, facts, cases))); 
24388
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

237 

47005
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset

238 
fun set_mode mode = map_data (fn (_, syntax, tsig, consts, facts, cases) => 
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset

239 
(mode, syntax, tsig, consts, facts, cases)); 
21443
cc5095d57da4
added stmt mode, which affects naming/indexing of local facts;
wenzelm
parents:
21370
diff
changeset

240 

24388
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

241 
fun map_mode f = 
47005
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset

242 
map_data (fn (Mode {stmt, pattern, schematic, abbrev}, syntax, tsig, consts, facts, cases) => 
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset

243 
(make_mode (f (stmt, pattern, schematic, abbrev)), syntax, tsig, consts, facts, cases)); 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

244 

19001  245 
fun map_syntax f = 
47005
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset

246 
map_data (fn (mode, syntax, tsig, consts, facts, cases) => 
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset

247 
(mode, f syntax, tsig, consts, facts, cases)); 
35669
a91c7ed801b8
added ProofContext.tsig_of  proforma version for local name space only, not logical content;
wenzelm
parents:
35616
diff
changeset

248 

36450  249 
fun map_tsig f = 
47005
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset

250 
map_data (fn (mode, syntax, tsig, consts, facts, cases) => 
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset

251 
(mode, syntax, f tsig, consts, facts, cases)); 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

252 

19001  253 
fun map_consts f = 
47005
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset

254 
map_data (fn (mode, syntax, tsig, consts, facts, cases) => 
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset

255 
(mode, syntax, tsig, f consts, facts, cases)); 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

256 

26284  257 
fun map_facts f = 
47005
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset

258 
map_data (fn (mode, syntax, tsig, consts, facts, cases) => 
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset

259 
(mode, syntax, tsig, consts, f facts, cases)); 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

260 

19001  261 
fun map_cases f = 
47005
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset

262 
map_data (fn (mode, syntax, tsig, consts, facts, cases) => 
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset

263 
(mode, syntax, tsig, consts, facts, f cases)); 
24388
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

264 

45650  265 
val get_mode = #mode o rep_data; 
28407  266 
val restore_mode = set_mode o get_mode; 
27286  267 
val abbrev_mode = get_mode #> (fn Mode {abbrev, ...} => abbrev); 
21443
cc5095d57da4
added stmt mode, which affects naming/indexing of local facts;
wenzelm
parents:
21370
diff
changeset

268 

24486  269 
fun set_stmt stmt = 
270 
map_mode (fn (_, pattern, schematic, abbrev) => (stmt, pattern, schematic, abbrev)); 

19001  271 

45650  272 
val syntax_of = #syntax o rep_data; 
33387  273 
val syn_of = Local_Syntax.syn_of o syntax_of; 
274 
val set_syntax_mode = map_syntax o Local_Syntax.set_mode; 

275 
val restore_syntax_mode = map_syntax o Local_Syntax.restore_mode o syntax_of; 

19001  276 

45650  277 
val tsig_of = #1 o #tsig o rep_data; 
36451  278 
val set_defsort = map_tsig o apfst o Type.set_defsort; 
35680  279 
fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt; 
35669
a91c7ed801b8
added ProofContext.tsig_of  proforma version for local name space only, not logical content;
wenzelm
parents:
35616
diff
changeset

280 

45650  281 
val consts_of = #1 o #consts o rep_data; 
282 
val cases_of = #cases o rep_data; 

5819  283 

284 

47005
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset

285 
(* naming *) 
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset

286 

421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset

287 
val naming_of = Name_Space.naming_of o Context.Proof; 
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset

288 
val map_naming = Context.proof_map o Name_Space.map_naming; 
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset

289 
val restore_naming = map_naming o K o naming_of; 
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset

290 

421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset

291 
val full_name = Name_Space.full_name o naming_of; 
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset

292 

421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset

293 

42359  294 
(* name spaces *) 
295 

296 
val class_space = Type.class_space o tsig_of; 

297 
val type_space = Type.type_space o tsig_of; 

298 
val const_space = Consts.space_of o consts_of; 

299 

300 
val intern_class = Name_Space.intern o class_space; 

301 
val intern_type = Name_Space.intern o type_space; 

302 
val intern_const = Name_Space.intern o const_space; 

303 

304 
fun extern_class ctxt = Name_Space.extern ctxt (class_space ctxt); 

305 
fun extern_type ctxt = Name_Space.extern ctxt (type_space ctxt); 

306 
fun extern_const ctxt = Name_Space.extern ctxt (const_space ctxt); 

307 

55304  308 
fun markup_class ctxt c = Name_Space.markup_extern ctxt (class_space ctxt) c > Markup.markup; 
309 
fun markup_type ctxt c = Name_Space.markup_extern ctxt (type_space ctxt) c > Markup.markup; 

310 
fun markup_const ctxt c = Name_Space.markup_extern ctxt (const_space ctxt) c > Markup.markup; 

311 

312 
fun pretty_class ctxt c = Name_Space.markup_extern ctxt (class_space ctxt) c > Pretty.mark_str; 

313 
fun pretty_type ctxt c = Name_Space.markup_extern ctxt (type_space ctxt) c > Pretty.mark_str; 

314 
fun pretty_const ctxt c = Name_Space.markup_extern ctxt (const_space ctxt) c > Pretty.mark_str; 

315 

42359  316 

20367  317 
(* theory transfer *) 
12093  318 

35669
a91c7ed801b8
added ProofContext.tsig_of  proforma version for local name space only, not logical content;
wenzelm
parents:
35616
diff
changeset

319 
fun transfer_syntax thy ctxt = ctxt > 
a91c7ed801b8
added ProofContext.tsig_of  proforma version for local name space only, not logical content;
wenzelm
parents:
35616
diff
changeset

320 
map_syntax (Local_Syntax.rebuild thy) > 
36450  321 
map_tsig (fn tsig as (local_tsig, global_tsig) => 
35669
a91c7ed801b8
added ProofContext.tsig_of  proforma version for local name space only, not logical content;
wenzelm
parents:
35616
diff
changeset

322 
let val thy_tsig = Sign.tsig_of thy in 
36450  323 
if Type.eq_tsig (thy_tsig, global_tsig) then tsig 
47005
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset

324 
else (Type.merge_tsig (Context.pretty ctxt) (local_tsig, thy_tsig), thy_tsig) 
35669
a91c7ed801b8
added ProofContext.tsig_of  proforma version for local name space only, not logical content;
wenzelm
parents:
35616
diff
changeset

325 
end) > 
30424
692279df7cc2
Consts.eq_const is back again (cf. 907da436f8a9)  required in ProofContext.transfer_syntax to prevent expensive merges of local_consts/global_consts;
wenzelm
parents:
30420
diff
changeset

326 
map_consts (fn consts as (local_consts, global_consts) => 
692279df7cc2
Consts.eq_const is back again (cf. 907da436f8a9)  required in ProofContext.transfer_syntax to prevent expensive merges of local_consts/global_consts;
wenzelm
parents:
30420
diff
changeset

327 
let val thy_consts = Sign.consts_of thy in 
692279df7cc2
Consts.eq_const is back again (cf. 907da436f8a9)  required in ProofContext.transfer_syntax to prevent expensive merges of local_consts/global_consts;
wenzelm
parents:
30420
diff
changeset

328 
if Consts.eq_consts (thy_consts, global_consts) then consts 
692279df7cc2
Consts.eq_const is back again (cf. 907da436f8a9)  required in ProofContext.transfer_syntax to prevent expensive merges of local_consts/global_consts;
wenzelm
parents:
30420
diff
changeset

329 
else (Consts.merge (local_consts, thy_consts), thy_consts) 
692279df7cc2
Consts.eq_const is back again (cf. 907da436f8a9)  required in ProofContext.transfer_syntax to prevent expensive merges of local_consts/global_consts;
wenzelm
parents:
30420
diff
changeset

330 
end); 
17072  331 

33031
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32966
diff
changeset

332 
fun transfer thy = Context.raw_transfer thy #> transfer_syntax thy; 
17072  333 

38756
d07959fabde6
renamed ProofContext.theory(_result) to ProofContext.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in userspace tools;
wenzelm
parents:
38328
diff
changeset

334 
fun background_theory f ctxt = transfer (f (theory_of ctxt)) ctxt; 
20367  335 

38756
d07959fabde6
renamed ProofContext.theory(_result) to ProofContext.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in userspace tools;
wenzelm
parents:
38328
diff
changeset

336 
fun background_theory_result f ctxt = 
20367  337 
let val (res, thy') = f (theory_of ctxt) 
338 
in (res, ctxt > transfer thy') end; 

19019  339 

12093  340 

56141
c06202417c4a
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
wenzelm
parents:
56140
diff
changeset

341 
(* hybrid facts *) 
c06202417c4a
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
wenzelm
parents:
56140
diff
changeset

342 

c06202417c4a
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
wenzelm
parents:
56140
diff
changeset

343 
val facts_of = #facts o rep_data; 
c06202417c4a
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
wenzelm
parents:
56140
diff
changeset

344 

c06202417c4a
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
wenzelm
parents:
56140
diff
changeset

345 
fun facts_of_fact ctxt name = 
c06202417c4a
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
wenzelm
parents:
56140
diff
changeset

346 
let 
c06202417c4a
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
wenzelm
parents:
56140
diff
changeset

347 
val local_facts = facts_of ctxt; 
c06202417c4a
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
wenzelm
parents:
56140
diff
changeset

348 
val global_facts = Global_Theory.facts_of (theory_of ctxt); 
c06202417c4a
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
wenzelm
parents:
56140
diff
changeset

349 
in 
56143
ed2b660a52a1
more accurate resolution of hybrid facts, which actually changes the sort order of results;
wenzelm
parents:
56141
diff
changeset

350 
if Facts.defined local_facts name 
56141
c06202417c4a
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
wenzelm
parents:
56140
diff
changeset

351 
then local_facts else global_facts 
c06202417c4a
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
wenzelm
parents:
56140
diff
changeset

352 
end; 
c06202417c4a
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
wenzelm
parents:
56140
diff
changeset

353 

c06202417c4a
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
wenzelm
parents:
56140
diff
changeset

354 
fun markup_extern_fact ctxt name = 
c06202417c4a
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
wenzelm
parents:
56140
diff
changeset

355 
Facts.markup_extern ctxt (facts_of_fact ctxt name) name; 
c06202417c4a
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
wenzelm
parents:
56140
diff
changeset

356 

c06202417c4a
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
wenzelm
parents:
56140
diff
changeset

357 

12093  358 

14828  359 
(** pretty printing **) 
360 

24922  361 
fun pretty_term_abbrev ctxt = Syntax.pretty_term (set_mode mode_abbrev ctxt); 
14828  362 

42378  363 
fun pretty_fact_name ctxt a = 
56141
c06202417c4a
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
wenzelm
parents:
56140
diff
changeset

364 
Pretty.block [Pretty.mark_str (markup_extern_fact ctxt a), Pretty.str ":"]; 
28209
02f3222a392d
pretty_fact: extern fact name wrt. the given context, assuming that is the proper one for presentation;
wenzelm
parents:
28087
diff
changeset

365 

51583  366 
fun pretty_fact ctxt = 
367 
let 

368 
val pretty_thm = Display.pretty_thm ctxt; 

51584  369 
val pretty_thms = map (Display.pretty_thm_item ctxt); 
51583  370 
in 
371 
fn ("", [th]) => pretty_thm th 

372 
 ("", ths) => Pretty.blk (0, Pretty.fbreaks (pretty_thms ths)) 

373 
 (a, [th]) => Pretty.block [pretty_fact_name ctxt a, Pretty.brk 1, pretty_thm th] 

374 
 (a, ths) => Pretty.block (Pretty.fbreaks (pretty_fact_name ctxt a :: pretty_thms ths)) 

375 
end; 

14828  376 

377 

378 

5819  379 
(** prepare types **) 
380 

35669
a91c7ed801b8
added ProofContext.tsig_of  proforma version for local name space only, not logical content;
wenzelm
parents:
35616
diff
changeset

381 
(* classes *) 
a91c7ed801b8
added ProofContext.tsig_of  proforma version for local name space only, not logical content;
wenzelm
parents:
35616
diff
changeset

382 

55922
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55843
diff
changeset

383 
fun check_class ctxt (xname, pos) = 
35669
a91c7ed801b8
added ProofContext.tsig_of  proforma version for local name space only, not logical content;
wenzelm
parents:
35616
diff
changeset

384 
let 
a91c7ed801b8
added ProofContext.tsig_of  proforma version for local name space only, not logical content;
wenzelm
parents:
35616
diff
changeset

385 
val tsig = tsig_of ctxt; 
55839
ee71b2687c4b
more markup for read_class: imitate Name_Space.check despite lack of Name_Space.table;
wenzelm
parents:
55829
diff
changeset

386 
val class_space = Type.class_space tsig; 
ee71b2687c4b
more markup for read_class: imitate Name_Space.check despite lack of Name_Space.table;
wenzelm
parents:
55829
diff
changeset

387 

56007  388 
val name = Type.cert_class tsig (Name_Space.intern class_space xname) 
55839
ee71b2687c4b
more markup for read_class: imitate Name_Space.check despite lack of Name_Space.table;
wenzelm
parents:
55829
diff
changeset

389 
handle TYPE (msg, _, _) => 
55840
2982d233d798
consider completion report as part of error message  less stateful, may get handled;
wenzelm
parents:
55839
diff
changeset

390 
error (msg ^ Position.here pos ^ 
55956
94d384d621b0
reject internal term names outright, and complete consts instead;
wenzelm
parents:
55955
diff
changeset

391 
Markup.markup_report (Completion.reported_text 
94d384d621b0
reject internal term names outright, and complete consts instead;
wenzelm
parents:
55955
diff
changeset

392 
(Name_Space.completion (Context.Proof ctxt) class_space (xname, pos)))); 
55922
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55843
diff
changeset

393 
val reports = 
55923  394 
if Context_Position.is_reported ctxt pos 
55922
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55843
diff
changeset

395 
then [(pos, Name_Space.markup class_space name)] else []; 
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55843
diff
changeset

396 
in (name, reports) end; 
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55843
diff
changeset

397 

710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55843
diff
changeset

398 
fun read_class ctxt text = 
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55843
diff
changeset

399 
let 
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55843
diff
changeset

400 
val (c, reports) = check_class ctxt (Symbol_Pos.source_content (Syntax.read_token text)); 
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55843
diff
changeset

401 
val _ = Position.reports reports; 
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55843
diff
changeset

402 
in c end; 
35669
a91c7ed801b8
added ProofContext.tsig_of  proforma version for local name space only, not logical content;
wenzelm
parents:
35616
diff
changeset

403 

a91c7ed801b8
added ProofContext.tsig_of  proforma version for local name space only, not logical content;
wenzelm
parents:
35616
diff
changeset

404 

a91c7ed801b8
added ProofContext.tsig_of  proforma version for local name space only, not logical content;
wenzelm
parents:
35616
diff
changeset

405 
(* types *) 
24277  406 

407 
fun read_typ_mode mode ctxt s = 

24486  408 
Syntax.read_typ (Type.set_mode mode ctxt) s; 
24277  409 

35669
a91c7ed801b8
added ProofContext.tsig_of  proforma version for local name space only, not logical content;
wenzelm
parents:
35616
diff
changeset

410 
val read_typ = read_typ_mode Type.mode_default; 
24277  411 
val read_typ_syntax = read_typ_mode Type.mode_syntax; 
412 
val read_typ_abbrev = read_typ_mode Type.mode_abbrev; 

413 

414 

415 
fun cert_typ_mode mode ctxt T = 

35669
a91c7ed801b8
added ProofContext.tsig_of  proforma version for local name space only, not logical content;
wenzelm
parents:
35616
diff
changeset

416 
Type.cert_typ_mode mode (tsig_of ctxt) T 
24277  417 
handle TYPE (msg, _, _) => error msg; 
418 

35669
a91c7ed801b8
added ProofContext.tsig_of  proforma version for local name space only, not logical content;
wenzelm
parents:
35616
diff
changeset

419 
val cert_typ = cert_typ_mode Type.mode_default; 
24277  420 
val cert_typ_syntax = cert_typ_mode Type.mode_syntax; 
421 
val cert_typ_abbrev = cert_typ_mode Type.mode_abbrev; 

422 

423 

24388
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

424 

5819  425 
(** prepare terms and propositions **) 
426 

25328  427 
(* inferred types of parameters *) 
428 

429 
fun infer_type ctxt x = 

36505
79c1d2bbe5a9
ProofContext.read_const: allow for type constraint (for fixed variable);
wenzelm
parents:
36503
diff
changeset

430 
Term.fastype_of (singleton (Syntax.check_terms (set_mode mode_schematic ctxt)) (Free x)); 
25328  431 

432 
fun inferred_param x ctxt = 

36505
79c1d2bbe5a9
ProofContext.read_const: allow for type constraint (for fixed variable);
wenzelm
parents:
36503
diff
changeset

433 
let val T = infer_type ctxt (x, dummyT) 
28082
37350f301128
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
28017
diff
changeset

434 
in (T, ctxt > Variable.declare_term (Free (x, T))) end; 
25328  435 

436 
fun inferred_fixes ctxt = 

28082
37350f301128
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
28017
diff
changeset

437 
let 
42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42469
diff
changeset

438 
val xs = map #2 (Variable.dest_fixes ctxt); 
28082
37350f301128
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
28017
diff
changeset

439 
val (Ts, ctxt') = fold_map inferred_param xs ctxt; 
37350f301128
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
28017
diff
changeset

440 
in (xs ~~ Ts, ctxt') end; 
25328  441 

442 

55842  443 
(* type names *) 
25328  444 

56002  445 
fun check_type_name {proper, strict} ctxt (c, pos) = 
55922
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55843
diff
changeset

446 
if Lexicon.is_tid c then 
56040  447 
if proper then error ("Not a type constructor: " ^ quote c ^ Position.here pos) 
55951
c07d184aebe9
tuned signature  more uniform check_type_name/read_type_name;
wenzelm
parents:
55950
diff
changeset

448 
else 
c07d184aebe9
tuned signature  more uniform check_type_name/read_type_name;
wenzelm
parents:
55950
diff
changeset

449 
let 
c07d184aebe9
tuned signature  more uniform check_type_name/read_type_name;
wenzelm
parents:
55950
diff
changeset

450 
val reports = 
c07d184aebe9
tuned signature  more uniform check_type_name/read_type_name;
wenzelm
parents:
55950
diff
changeset

451 
if Context_Position.is_reported ctxt pos 
c07d184aebe9
tuned signature  more uniform check_type_name/read_type_name;
wenzelm
parents:
55950
diff
changeset

452 
then [(pos, Markup.tfree)] else []; 
c07d184aebe9
tuned signature  more uniform check_type_name/read_type_name;
wenzelm
parents:
55950
diff
changeset

453 
in (TFree (c, default_sort ctxt (c, ~1)), reports) end 
55922
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55843
diff
changeset

454 
else 
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55843
diff
changeset

455 
let 
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55843
diff
changeset

456 
val ((d, reports), decl) = Type.check_decl (Context.Proof ctxt) (tsig_of ctxt) (c, pos); 
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55843
diff
changeset

457 
fun err () = error ("Bad type name: " ^ quote d ^ Position.here pos); 
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55843
diff
changeset

458 
val args = 
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55843
diff
changeset

459 
(case decl of 
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55843
diff
changeset

460 
Type.LogicalType n => n 
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55843
diff
changeset

461 
 Type.Abbreviation (vs, _, _) => if strict then err () else length vs 
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55843
diff
changeset

462 
 Type.Nonterminal => if strict then err () else 0); 
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55843
diff
changeset

463 
in (Type (d, replicate args dummyT), reports) end; 
25328  464 

55951
c07d184aebe9
tuned signature  more uniform check_type_name/read_type_name;
wenzelm
parents:
55950
diff
changeset

465 
fun read_type_name ctxt flags text = 
c07d184aebe9
tuned signature  more uniform check_type_name/read_type_name;
wenzelm
parents:
55950
diff
changeset

466 
let 
c07d184aebe9
tuned signature  more uniform check_type_name/read_type_name;
wenzelm
parents:
55950
diff
changeset

467 
val (T, reports) = 
c07d184aebe9
tuned signature  more uniform check_type_name/read_type_name;
wenzelm
parents:
55950
diff
changeset

468 
check_type_name ctxt flags (Symbol_Pos.source_content (Syntax.read_token text)); 
c07d184aebe9
tuned signature  more uniform check_type_name/read_type_name;
wenzelm
parents:
55950
diff
changeset

469 
val _ = Position.reports reports; 
c07d184aebe9
tuned signature  more uniform check_type_name/read_type_name;
wenzelm
parents:
55950
diff
changeset

470 
in T end; 
35669
a91c7ed801b8
added ProofContext.tsig_of  proforma version for local name space only, not logical content;
wenzelm
parents:
35616
diff
changeset

471 

a91c7ed801b8
added ProofContext.tsig_of  proforma version for local name space only, not logical content;
wenzelm
parents:
35616
diff
changeset

472 

55842  473 
(* constant names *) 
474 

55956
94d384d621b0
reject internal term names outright, and complete consts instead;
wenzelm
parents:
55955
diff
changeset

475 
fun consts_completion_message ctxt (c, ps) = 
94d384d621b0
reject internal term names outright, and complete consts instead;
wenzelm
parents:
55955
diff
changeset

476 
ps > map (fn pos => 
94d384d621b0
reject internal term names outright, and complete consts instead;
wenzelm
parents:
55955
diff
changeset

477 
Name_Space.completion (Context.Proof ctxt) (Consts.space_of (consts_of ctxt)) (c, pos) 
94d384d621b0
reject internal term names outright, and complete consts instead;
wenzelm
parents:
55955
diff
changeset

478 
> Completion.reported_text) 
94d384d621b0
reject internal term names outright, and complete consts instead;
wenzelm
parents:
55955
diff
changeset

479 
> implode 
94d384d621b0
reject internal term names outright, and complete consts instead;
wenzelm
parents:
55955
diff
changeset

480 
> Markup.markup_report; 
94d384d621b0
reject internal term names outright, and complete consts instead;
wenzelm
parents:
55955
diff
changeset

481 

56002  482 
fun check_const {proper, strict} ctxt (c, ps) = 
55842  483 
let 
55956
94d384d621b0
reject internal term names outright, and complete consts instead;
wenzelm
parents:
55955
diff
changeset

484 
val _ = 
55959
c3b458435f4f
more decisive commitment to get_free vs. the_const;
wenzelm
parents:
55956
diff
changeset

485 
Name.reject_internal (c, ps) handle ERROR msg => 
c3b458435f4f
more decisive commitment to get_free vs. the_const;
wenzelm
parents:
55956
diff
changeset

486 
error (msg ^ consts_completion_message ctxt (c, ps)); 
c3b458435f4f
more decisive commitment to get_free vs. the_const;
wenzelm
parents:
55956
diff
changeset

487 
fun err msg = error (msg ^ Position.here_list ps); 
55842  488 
val consts = consts_of ctxt; 
55954  489 
val fixed = if proper then NONE else Variable.lookup_fixed ctxt c; 
490 
val (t, reports) = 

491 
(case (fixed, Variable.lookup_const ctxt c) of 

492 
(SOME x, NONE) => 

55843
3fa61f39d1f2
prefer Name_Space.check with its builtin reports (including completion);
wenzelm
parents:
55842
diff
changeset

493 
let 
55959
c3b458435f4f
more decisive commitment to get_free vs. the_const;
wenzelm
parents:
55956
diff
changeset

494 
val reports = ps 
c3b458435f4f
more decisive commitment to get_free vs. the_const;
wenzelm
parents:
55956
diff
changeset

495 
> filter (Context_Position.is_reported ctxt) 
c3b458435f4f
more decisive commitment to get_free vs. the_const;
wenzelm
parents:
55956
diff
changeset

496 
> map (fn pos => 
c3b458435f4f
more decisive commitment to get_free vs. the_const;
wenzelm
parents:
55956
diff
changeset

497 
(pos, Markup.name x (if Name.is_skolem x then Markup.skolem else Markup.free))); 
55955
e8f1bf005661
eliminated odd type constraint for read_const (see also 79c1d2bbe5a9);
wenzelm
parents:
55954
diff
changeset

498 
in (Free (x, infer_type ctxt (x, dummyT)), reports) end 
55954  499 
 (_, SOME d) => 
500 
let 

501 
val T = Consts.type_scheme consts d handle TYPE (msg, _, _) => err msg; 

55959
c3b458435f4f
more decisive commitment to get_free vs. the_const;
wenzelm
parents:
55956
diff
changeset

502 
val reports = ps 
c3b458435f4f
more decisive commitment to get_free vs. the_const;
wenzelm
parents:
55956
diff
changeset

503 
> filter (Context_Position.is_reported ctxt) 
c3b458435f4f
more decisive commitment to get_free vs. the_const;
wenzelm
parents:
55956
diff
changeset

504 
> map (fn pos => (pos, Name_Space.markup (Consts.space_of consts) d)); 
55950
3bb5c7179234
clarified treatment of consts  prefer valueoriented reports;
wenzelm
parents:
55949
diff
changeset

505 
in (Const (d, T), reports) end 
55959
c3b458435f4f
more decisive commitment to get_free vs. the_const;
wenzelm
parents:
55956
diff
changeset

506 
 _ => Consts.check_const (Context.Proof ctxt) consts (c, ps)); 
55842  507 
val _ = 
55954  508 
(case (strict, t) of 
509 
(true, Const (d, _)) => 

510 
(ignore (Consts.the_const consts d) handle TYPE (msg, _, _) => err msg) 

511 
 _ => ()); 

55950
3bb5c7179234
clarified treatment of consts  prefer valueoriented reports;
wenzelm
parents:
55949
diff
changeset

512 
in (t, reports) end; 
55842  513 

55955
e8f1bf005661
eliminated odd type constraint for read_const (see also 79c1d2bbe5a9);
wenzelm
parents:
55954
diff
changeset

514 
fun read_const ctxt flags text = 
55950
3bb5c7179234
clarified treatment of consts  prefer valueoriented reports;
wenzelm
parents:
55949
diff
changeset

515 
let 
55959
c3b458435f4f
more decisive commitment to get_free vs. the_const;
wenzelm
parents:
55956
diff
changeset

516 
val (xname, pos) = Symbol_Pos.source_content (Syntax.read_token text); 
c3b458435f4f
more decisive commitment to get_free vs. the_const;
wenzelm
parents:
55956
diff
changeset

517 
val (t, reports) = check_const ctxt flags (xname, [pos]); 
55950
3bb5c7179234
clarified treatment of consts  prefer valueoriented reports;
wenzelm
parents:
55949
diff
changeset

518 
val _ = Position.reports reports; 
3bb5c7179234
clarified treatment of consts  prefer valueoriented reports;
wenzelm
parents:
55949
diff
changeset

519 
in t end; 
25328  520 

521 

46922
3717f3878714
source positions for locale and class expressions;
wenzelm
parents:
46849
diff
changeset

522 
(* type arities *) 
3717f3878714
source positions for locale and class expressions;
wenzelm
parents:
46849
diff
changeset

523 

3717f3878714
source positions for locale and class expressions;
wenzelm
parents:
46849
diff
changeset

524 
local 
3717f3878714
source positions for locale and class expressions;
wenzelm
parents:
46849
diff
changeset

525 

3717f3878714
source positions for locale and class expressions;
wenzelm
parents:
46849
diff
changeset

526 
fun prep_arity prep_tycon prep_sort ctxt (t, Ss, S) = 
3717f3878714
source positions for locale and class expressions;
wenzelm
parents:
46849
diff
changeset

527 
let val arity = (prep_tycon ctxt t, map (prep_sort ctxt) Ss, prep_sort ctxt S) 
47005
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset

528 
in Type.add_arity (Context.pretty ctxt) arity (tsig_of ctxt); arity end; 
46922
3717f3878714
source positions for locale and class expressions;
wenzelm
parents:
46849
diff
changeset

529 

3717f3878714
source positions for locale and class expressions;
wenzelm
parents:
46849
diff
changeset

530 
in 
3717f3878714
source positions for locale and class expressions;
wenzelm
parents:
46849
diff
changeset

531 

3717f3878714
source positions for locale and class expressions;
wenzelm
parents:
46849
diff
changeset

532 
val read_arity = 
56002  533 
prep_arity ((#1 o dest_Type) oo read_type_name {proper = true, strict = true}) Syntax.read_sort; 
47005
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset

534 

46922
3717f3878714
source positions for locale and class expressions;
wenzelm
parents:
46849
diff
changeset

535 
val cert_arity = prep_arity (K I) (Type.cert_sort o tsig_of); 
3717f3878714
source positions for locale and class expressions;
wenzelm
parents:
46849
diff
changeset

536 

3717f3878714
source positions for locale and class expressions;
wenzelm
parents:
46849
diff
changeset

537 
end; 
3717f3878714
source positions for locale and class expressions;
wenzelm
parents:
46849
diff
changeset

538 

3717f3878714
source positions for locale and class expressions;
wenzelm
parents:
46849
diff
changeset

539 

24684  540 
(* read_term *) 
541 

542 
fun read_term_mode mode ctxt = Syntax.read_term (set_mode mode ctxt); 

543 

544 
val read_term_pattern = read_term_mode mode_pattern; 

545 
val read_term_schematic = read_term_mode mode_schematic; 

546 
val read_term_abbrev = read_term_mode mode_abbrev; 

547 

548 

19001  549 
(* local abbreviations *) 
5819  550 

24501  551 
local 
552 

42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42381
diff
changeset

553 
fun certify_consts ctxt = Consts.certify (Context.pretty ctxt) (tsig_of ctxt) 
27286  554 
(not (abbrev_mode ctxt)) (consts_of ctxt); 
19001  555 

38979
60dbf0b3f6c7
prefer regular print functions over slightly lowlevel Term.string_of_vname;
wenzelm
parents:
38756
diff
changeset

556 
fun expand_binds ctxt = 
60dbf0b3f6c7
prefer regular print functions over slightly lowlevel Term.string_of_vname;
wenzelm
parents:
38756
diff
changeset

557 
let 
60dbf0b3f6c7
prefer regular print functions over slightly lowlevel Term.string_of_vname;
wenzelm
parents:
38756
diff
changeset

558 
val Mode {pattern, schematic, ...} = get_mode ctxt; 
5819  559 

38979
60dbf0b3f6c7
prefer regular print functions over slightly lowlevel Term.string_of_vname;
wenzelm
parents:
38756
diff
changeset

560 
fun reject_schematic (t as Var _) = 
60dbf0b3f6c7
prefer regular print functions over slightly lowlevel Term.string_of_vname;
wenzelm
parents:
38756
diff
changeset

561 
error ("Unbound schematic variable: " ^ Syntax.string_of_term ctxt t) 
60dbf0b3f6c7
prefer regular print functions over slightly lowlevel Term.string_of_vname;
wenzelm
parents:
38756
diff
changeset

562 
 reject_schematic (Abs (_, _, t)) = reject_schematic t 
60dbf0b3f6c7
prefer regular print functions over slightly lowlevel Term.string_of_vname;
wenzelm
parents:
38756
diff
changeset

563 
 reject_schematic (t $ u) = (reject_schematic t; reject_schematic u) 
60dbf0b3f6c7
prefer regular print functions over slightly lowlevel Term.string_of_vname;
wenzelm
parents:
38756
diff
changeset

564 
 reject_schematic _ = (); 
60dbf0b3f6c7
prefer regular print functions over slightly lowlevel Term.string_of_vname;
wenzelm
parents:
38756
diff
changeset

565 
in 
24495  566 
if pattern then I 
567 
else Variable.expand_binds ctxt #> (if schematic then I else tap reject_schematic) 

568 
end; 

5819  569 

24501  570 
in 
571 

572 
fun expand_abbrevs ctxt = certify_consts ctxt #> expand_binds ctxt; 

573 

574 
end; 

575 

56438  576 
val show_abbrevs_raw = Config.declare ("show_abbrevs", @{here}) (fn _ => Config.Bool true); 
40879
ca132ef44944
configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
wenzelm
parents:
39557
diff
changeset

577 
val show_abbrevs = Config.bool show_abbrevs_raw; 
5819  578 

24922  579 
fun contract_abbrevs ctxt t = 
580 
let 

581 
val thy = theory_of ctxt; 

582 
val consts = consts_of ctxt; 

583 
val Mode {abbrev, ...} = get_mode ctxt; 

30566
9643f54c4184
reverted abbreviations: improved performance via Item_Net.T;
wenzelm
parents:
30473
diff
changeset

584 
val retrieve = Consts.retrieve_abbrevs consts (print_mode_value () @ [""]); 
9643f54c4184
reverted abbreviations: improved performance via Item_Net.T;
wenzelm
parents:
30473
diff
changeset

585 
fun match_abbrev u = Option.map #1 (get_first (Pattern.match_rew thy u) (retrieve u)); 
24922  586 
in 
40879
ca132ef44944
configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
wenzelm
parents:
39557
diff
changeset

587 
if abbrev orelse not (Config.get ctxt show_abbrevs) orelse not (can Term.type_of t) then t 
35211
5d2fe4e09354
Use topdown rewriting to contract abbreviations.
berghofe
parents:
35141
diff
changeset

588 
else Pattern.rewrite_term_top thy [] [match_abbrev] t 
24922  589 
end; 
590 

591 

24518  592 
(* patterns *) 
593 

32003  594 
fun prepare_patternT ctxt T = 
595 
let 

596 
val Mode {pattern, schematic, ...} = get_mode ctxt; 

597 
val _ = 

598 
pattern orelse schematic orelse 

599 
T > Term.exists_subtype 

38979
60dbf0b3f6c7
prefer regular print functions over slightly lowlevel Term.string_of_vname;
wenzelm
parents:
38756
diff
changeset

600 
(fn T as TVar (xi, _) => 
37145
01aa36932739
renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
wenzelm
parents:
36610
diff
changeset

601 
not (Type_Infer.is_param xi) andalso 
38979
60dbf0b3f6c7
prefer regular print functions over slightly lowlevel Term.string_of_vname;
wenzelm
parents:
38756
diff
changeset

602 
error ("Illegal schematic type variable: " ^ Syntax.string_of_typ ctxt T) 
32003  603 
 _ => false) 
604 
in T end; 

24518  605 

22712  606 

24505  607 
local 
6550  608 

56438  609 
val dummies = 
610 
Config.bool (Config.declare ("Proof_Context.dummies", @{here}) (K (Config.Bool false))); 

27259  611 

612 
fun check_dummies ctxt t = 

39508
dfacdb01e1ec
simplified some internal flags using Config.T instead of fullblown Proof_Data;
wenzelm
parents:
39507
diff
changeset

613 
if Config.get ctxt dummies then t 
27259  614 
else Term.no_dummy_patterns t handle TERM _ => error "Illegal dummy pattern(s) in term"; 
615 

24767  616 
fun prepare_dummies ts = #1 (fold_map Term.replace_dummy_patterns ts 1); 
6762  617 

27259  618 
in 
6550  619 

39508
dfacdb01e1ec
simplified some internal flags using Config.T instead of fullblown Proof_Data;
wenzelm
parents:
39507
diff
changeset

620 
val allow_dummies = Config.put dummies true; 
24505  621 

24684  622 
fun prepare_patterns ctxt = 
24518  623 
let val Mode {pattern, ...} = get_mode ctxt in 
39296  624 
Type_Infer.fixate ctxt #> 
24767  625 
pattern ? Variable.polymorphic ctxt #> 
24684  626 
(map o Term.map_types) (prepare_patternT ctxt) #> 
27259  627 
(if pattern then prepare_dummies else map (check_dummies ctxt)) 
24505  628 
end; 
629 

630 
end; 

631 

6550  632 

42250
cc5ac538f991
eliminated odd objectoriented type_context/term_context;
wenzelm
parents:
42242
diff
changeset

633 
(* sort constraints *) 
27286  634 

49674
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

635 
local 
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

636 

dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

637 
fun prepare_sorts_env ctxt tys = 
27286  638 
let 
35669
a91c7ed801b8
added ProofContext.tsig_of  proforma version for local name space only, not logical content;
wenzelm
parents:
35616
diff
changeset

639 
val tsig = tsig_of ctxt; 
45453  640 
val defaultS = Type.defaultS tsig; 
27286  641 

53673
bcfd16f65014
treat all dummy type variables separately (in contrast to fca432074fb2);
wenzelm
parents:
53380
diff
changeset

642 
val dummy_var = ("'_dummy_", ~1); 
bcfd16f65014
treat all dummy type variables separately (in contrast to fca432074fb2);
wenzelm
parents:
53380
diff
changeset

643 

49685
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset

644 
fun constraint (xi, raw_S) env = 
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset

645 
let val (ps, S) = Term_Position.decode_positionS raw_S in 
53673
bcfd16f65014
treat all dummy type variables separately (in contrast to fca432074fb2);
wenzelm
parents:
53380
diff
changeset

646 
if xi = dummy_var orelse S = dummyS then env 
49685
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset

647 
else 
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset

648 
Vartab.insert (op =) (xi, Type.minimize_sort tsig S) env 
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset

649 
handle Vartab.DUP _ => 
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset

650 
error ("Inconsistent sort constraints for type variable " ^ 
49691  651 
quote (Term.string_of_vname' xi) ^ Position.here_list ps) 
49685
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset

652 
end; 
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset

653 

45453  654 
val env = 
655 
(fold o fold_atyps) 

656 
(fn TFree (x, S) => constraint ((x, ~1), S) 

657 
 TVar v => constraint v 

658 
 _ => I) tys Vartab.empty; 

36152  659 

53673
bcfd16f65014
treat all dummy type variables separately (in contrast to fca432074fb2);
wenzelm
parents:
53380
diff
changeset

660 
fun get_sort xi raw_S = 
bcfd16f65014
treat all dummy type variables separately (in contrast to fca432074fb2);
wenzelm
parents:
53380
diff
changeset

661 
if xi = dummy_var then 
bcfd16f65014
treat all dummy type variables separately (in contrast to fca432074fb2);
wenzelm
parents:
53380
diff
changeset

662 
Type.minimize_sort tsig (#2 (Term_Position.decode_positionS raw_S)) 
bcfd16f65014
treat all dummy type variables separately (in contrast to fca432074fb2);
wenzelm
parents:
53380
diff
changeset

663 
else 
bcfd16f65014
treat all dummy type variables separately (in contrast to fca432074fb2);
wenzelm
parents:
53380
diff
changeset

664 
(case (Vartab.lookup env xi, Variable.def_sort ctxt xi) of 
bcfd16f65014
treat all dummy type variables separately (in contrast to fca432074fb2);
wenzelm
parents:
53380
diff
changeset

665 
(NONE, NONE) => defaultS 
bcfd16f65014
treat all dummy type variables separately (in contrast to fca432074fb2);
wenzelm
parents:
53380
diff
changeset

666 
 (NONE, SOME S) => S 
bcfd16f65014
treat all dummy type variables separately (in contrast to fca432074fb2);
wenzelm
parents:
53380
diff
changeset

667 
 (SOME S, NONE) => S 
bcfd16f65014
treat all dummy type variables separately (in contrast to fca432074fb2);
wenzelm
parents:
53380
diff
changeset

668 
 (SOME S, SOME S') => 
bcfd16f65014
treat all dummy type variables separately (in contrast to fca432074fb2);
wenzelm
parents:
53380
diff
changeset

669 
if Type.eq_sort tsig (S, S') then S' 
bcfd16f65014
treat all dummy type variables separately (in contrast to fca432074fb2);
wenzelm
parents:
53380
diff
changeset

670 
else 
bcfd16f65014
treat all dummy type variables separately (in contrast to fca432074fb2);
wenzelm
parents:
53380
diff
changeset

671 
error ("Sort constraint " ^ Syntax.string_of_sort ctxt S ^ 
bcfd16f65014
treat all dummy type variables separately (in contrast to fca432074fb2);
wenzelm
parents:
53380
diff
changeset

672 
" inconsistent with default " ^ Syntax.string_of_sort ctxt S' ^ 
bcfd16f65014
treat all dummy type variables separately (in contrast to fca432074fb2);
wenzelm
parents:
53380
diff
changeset

673 
" for type variable " ^ quote (Term.string_of_vname' xi))); 
49674
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

674 

49685
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset

675 
fun add_report S pos reports = 
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset

676 
if Position.is_reported pos andalso not (AList.defined (op =) reports pos) then 
50201
c26369c9eda6
Isabellespecific implementation of quasiabstract markup elements  back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50126
diff
changeset

677 
(pos, Position.reported_text pos Markup.sorting (Syntax.string_of_sort ctxt S)) :: reports 
49685
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset

678 
else reports; 
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset

679 

49691  680 
fun get_sort_reports xi raw_S = 
681 
let 

682 
val ps = #1 (Term_Position.decode_positionS raw_S); 

53673
bcfd16f65014
treat all dummy type variables separately (in contrast to fca432074fb2);
wenzelm
parents:
53380
diff
changeset

683 
val S = get_sort xi raw_S handle ERROR msg => error (msg ^ Position.here_list ps); 
49691  684 
in fold (add_report S) ps end; 
49674
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

685 

dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

686 
val reports = 
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

687 
(fold o fold_atyps) 
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

688 
(fn T => 
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

689 
if Term_Position.is_positionT T then I 
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

690 
else 
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

691 
(case T of 
49691  692 
TFree (x, raw_S) => get_sort_reports (x, ~1) raw_S 
693 
 TVar (xi, raw_S) => get_sort_reports xi raw_S 

49674
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

694 
 _ => I)) tys []; 
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

695 

56333
38f1422ef473
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents:
56294
diff
changeset

696 
in (map #2 reports, get_sort) end; 
27286  697 

49674
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

698 
fun replace_sortsT get_sort = 
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

699 
map_atyps 
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

700 
(fn T => 
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

701 
if Term_Position.is_positionT T then T 
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

702 
else 
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

703 
(case T of 
53673
bcfd16f65014
treat all dummy type variables separately (in contrast to fca432074fb2);
wenzelm
parents:
53380
diff
changeset

704 
TFree (x, raw_S) => TFree (x, get_sort (x, ~1) raw_S) 
bcfd16f65014
treat all dummy type variables separately (in contrast to fca432074fb2);
wenzelm
parents:
53380
diff
changeset

705 
 TVar (xi, raw_S) => TVar (xi, get_sort xi raw_S) 
49674
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

706 
 _ => T)); 
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

707 

dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

708 
in 
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

709 

dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

710 
fun prepare_sortsT ctxt tys = 
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

711 
let val (sorting_report, get_sort) = prepare_sorts_env ctxt tys 
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

712 
in (sorting_report, map (replace_sortsT get_sort) tys) end; 
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

713 

dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

714 
fun prepare_sorts ctxt tms = 
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

715 
let 
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

716 
val tys = rev ((fold o fold_types) cons tms []); 
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

717 
val (sorting_report, get_sort) = prepare_sorts_env ctxt tys; 
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

718 
in (sorting_report, (map o map_types) (replace_sortsT get_sort) tms) end; 
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

719 

dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

720 
fun check_tfree ctxt v = 
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

721 
let 
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

722 
val (sorting_report, [TFree a]) = prepare_sortsT ctxt [TFree v]; 
56294
85911b8a6868
prefer Context_Position where a context is available;
wenzelm
parents:
56202
diff
changeset

723 
val _ = if Context_Position.is_visible ctxt then Output.report sorting_report else (); 
49674
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

724 
in a end; 
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

725 

dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

726 
end; 
36152  727 

5819  728 

729 
(* certify terms *) 

730 

10554  731 
local 
732 

24684  733 
fun gen_cert prop ctxt t = 
734 
t 

735 
> expand_abbrevs ctxt 

42383
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42381
diff
changeset

736 
> (fn t' => 
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42381
diff
changeset

737 
#1 (Sign.certify' prop (Context.pretty ctxt) false (consts_of ctxt) (theory_of ctxt) t') 
0ae4ad40d7b5
simplified pretty printing context, which is only required for certain kernel operations;
wenzelm
parents:
42381
diff
changeset

738 
handle TYPE (msg, _, _) => error msg  TERM (msg, _) => error msg); 
16501  739 

10554  740 
in 
8096  741 

24684  742 
val cert_term = gen_cert false; 
743 
val cert_prop = gen_cert true; 

10554  744 

745 
end; 

5819  746 

747 

42405
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
42402
diff
changeset

748 
(* check/uncheck *) 
22701  749 

35616
b342390d296f
provide ProofContext.def_type depending on "pattern" mode;
wenzelm
parents:
35429
diff
changeset

750 
fun def_type ctxt = 
b342390d296f
provide ProofContext.def_type depending on "pattern" mode;
wenzelm
parents:
35429
diff
changeset

751 
let val Mode {pattern, ...} = get_mode ctxt 
b342390d296f
provide ProofContext.def_type depending on "pattern" mode;
wenzelm
parents:
35429
diff
changeset

752 
in Variable.def_type ctxt pattern end; 
b342390d296f
provide ProofContext.def_type depending on "pattern" mode;
wenzelm
parents:
35429
diff
changeset

753 

24518  754 
fun standard_typ_check ctxt = 
45429  755 
map (cert_typ_mode (Type.get_mode ctxt) ctxt #> prepare_patternT ctxt); 
24922  756 

45429  757 
val standard_term_check_finish = prepare_patterns; 
24518  758 

45429  759 
fun standard_term_uncheck ctxt = map (contract_abbrevs ctxt); 
22701  760 

761 

9553  762 

21610  763 
(** export results **) 
21531  764 

20310  765 
fun common_export is_goal inner outer = 
766 
map (Assumption.export is_goal inner outer) #> 

767 
Variable.export inner outer; 

8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

768 

20310  769 
val goal_export = common_export true; 
770 
val export = common_export false; 

12704  771 

21531  772 
fun export_morphism inner outer = 
773 
Assumption.export_morphism inner outer $> 

774 
Variable.export_morphism inner outer; 

775 

28396  776 
fun norm_export_morphism inner outer = 
777 
export_morphism inner outer $> 

54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
54742
diff
changeset

778 
Morphism.thm_morphism "Proof_Context.norm_export" (Goal.norm_result outer); 
28396  779 

21531  780 

15758
07e382399a96
binds/thms: do not store options, but delete from table;
wenzelm
parents:
15750
diff
changeset

781 

30757
2d2076300185
replaced add_binds(_i) by bind_terms  internal version only;
wenzelm
parents:
30723
diff
changeset

782 
(** term bindings **) 
5819  783 

8096  784 
(* simult_matches *) 
785 

19867  786 
fun simult_matches ctxt (t, pats) = 
787 
(case Seq.pull (Unify.matchers (theory_of ctxt) (map (rpair t) pats)) of 

788 
NONE => error "Pattern match failed!" 

32032  789 
 SOME (env, _) => Vartab.fold (fn (v, (_, t)) => cons (v, t)) (Envir.term_env env) []); 
8096  790 

791 

30757
2d2076300185
replaced add_binds(_i) by bind_terms  internal version only;
wenzelm
parents:
30723
diff
changeset

792 
(* bind_terms *) 
7925  793 

30757
2d2076300185
replaced add_binds(_i) by bind_terms  internal version only;
wenzelm
parents:
30723
diff
changeset

794 
val bind_terms = fold (fn (xi, t) => fn ctxt => 
24511
69d270cc7e4f
removed obsolete read/cert variations (cf. Syntax.read/check);
wenzelm
parents:
24505
diff
changeset

795 
ctxt 
30757
2d2076300185
replaced add_binds(_i) by bind_terms  internal version only;
wenzelm
parents:
30723
diff
changeset

796 
> Variable.bind_term (xi, Option.map (cert_term (set_mode mode_default ctxt)) t)); 
5819  797 

30757
2d2076300185
replaced add_binds(_i) by bind_terms  internal version only;
wenzelm
parents:
30723
diff
changeset

798 

2d2076300185
replaced add_binds(_i) by bind_terms  internal version only;
wenzelm
parents:
30723
diff
changeset

799 
(* auto_bind *) 
10810  800 

20330  801 
fun drop_schematic (b as (xi, SOME t)) = if Term.exists_subterm is_Var t then (xi, NONE) else b 
10554  802 
 drop_schematic b = b; 
803 

30757
2d2076300185
replaced add_binds(_i) by bind_terms  internal version only;
wenzelm
parents:
30723
diff
changeset

804 
fun auto_bind f ts ctxt = ctxt > bind_terms (map drop_schematic (f (theory_of ctxt) ts)); 
8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

805 

33386  806 
val auto_bind_goal = auto_bind Auto_Bind.goal; 
807 
val auto_bind_facts = auto_bind Auto_Bind.facts; 

7925  808 

5819  809 

8096  810 
(* match_bind(_i) *) 
5819  811 

8096  812 
local 
813 

24684  814 
fun gen_bind prep_terms gen raw_binds ctxt = 
5819  815 
let 
24684  816 
fun prep_bind (raw_pats, t) ctxt1 = 
817 
let 

818 
val T = Term.fastype_of t; 

819 
val ctxt2 = Variable.declare_term t ctxt1; 

820 
val pats = prep_terms (set_mode mode_pattern ctxt2) T raw_pats; 

821 
val binds = simult_matches ctxt2 (t, pats); 

822 
in (binds, ctxt2) end; 

7670  823 

24686  824 
val ts = prep_terms ctxt dummyT (map snd raw_binds); 
825 
val (binds, ctxt') = apfst flat (fold_map prep_bind (map fst raw_binds ~~ ts) ctxt); 

8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

826 
val binds' = 
19916
3bbb9cc5d4f1
export: simultaneous facts, refer to Variable.export;
wenzelm
parents:
19897
diff
changeset

827 
if gen then map #1 binds ~~ Variable.exportT_terms ctxt' ctxt (map #2 binds) 
8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

828 
else binds; 
15531  829 
val binds'' = map (apsnd SOME) binds'; 
18310  830 
val ctxt'' = 
19897
fe661eb3b0e7
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19882
diff
changeset

831 
tap (Variable.warn_extra_tfrees ctxt) 
18310  832 
(if gen then 
30757
2d2076300185
replaced add_binds(_i) by bind_terms  internal version only;
wenzelm
parents:
30723
diff
changeset

833 
ctxt (*sic!*) > fold Variable.declare_term (map #2 binds') > bind_terms binds'' 
2d2076300185
replaced add_binds(_i) by bind_terms  internal version only;
wenzelm
parents:
30723
diff
changeset

834 
else ctxt' > bind_terms binds''); 
18310  835 
in (ts, ctxt'') end; 
8096  836 

837 
in 

5935  838 

24684  839 
fun read_terms ctxt T = 
39288  840 
map (Syntax.parse_term ctxt #> Type.constraint T) #> Syntax.check_terms ctxt; 
24684  841 

842 
val match_bind = gen_bind read_terms; 

843 
val match_bind_i = gen_bind (fn ctxt => fn _ => map (cert_term ctxt)); 

8096  844 

845 
end; 

5935  846 

847 

10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

848 
(* propositions with patterns *) 
5935  849 

10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

850 
local 
8096  851 

45327  852 
fun prep_propp mode prep_props args context = 
10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

853 
let 
19585  854 
fun prep (_, raw_pats) (ctxt, prop :: props) = 
24684  855 
let val ctxt' = Variable.declare_term prop ctxt 
856 
in ((prop, prep_props (set_mode mode_pattern ctxt') raw_pats), (ctxt', props)) end; 

857 

45327  858 
val (propp, (context', _)) = 
859 
(fold_map o fold_map) prep args 

860 
(context, prep_props (set_mode mode context) (maps (map fst) args)); 

861 
in (propp, context') end; 

5935  862 

45327  863 
fun gen_bind_propp mode parse_prop raw_args ctxt = 
8096  864 
let 
45327  865 
val (args, ctxt') = prep_propp mode parse_prop raw_args ctxt; 
19585  866 
val binds = flat (flat (map (map (simult_matches ctxt')) args)); 
10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

867 
val propss = map (map #1) args; 
45330
93b8e30a5d1f
more general Proof_Context.bind_propp, which allows outer parameters;
wenzelm
parents:
45327
diff
changeset

868 
fun gen_binds ctxt0 = ctxt0 
93b8e30a5d1f
more general Proof_Context.bind_propp, which allows outer parameters;
wenzelm
parents:
45327
diff
changeset

869 
> bind_terms (map #1 binds ~~ 
93b8e30a5d1f
more general Proof_Context.bind_propp, which allows outer parameters;
wenzelm
parents:
45327
diff
changeset

870 
map (SOME o Term.close_schematic_term) (Variable.export_terms ctxt' ctxt0 (map #2 binds))); 
45327  871 
in ((propss, gen_binds), ctxt' > bind_terms (map (apsnd SOME) binds)) end; 
8096  872 

10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

873 
in 
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

874 

24684  875 
val read_propp = prep_propp mode_default Syntax.read_props; 
876 
val cert_propp = prep_propp mode_default (map o cert_prop); 

877 
val read_propp_schematic = prep_propp mode_schematic Syntax.read_props; 

878 
val cert_propp_schematic = prep_propp mode_schematic (map o cert_prop); 

10554  879 

24684  880 
val bind_propp = gen_bind_propp mode_default Syntax.read_props; 
881 
val bind_propp_i = gen_bind_propp mode_default (map o cert_prop); 

882 
val bind_propp_schematic = gen_bind_propp mode_schematic Syntax.read_props; 

883 
val bind_propp_schematic_i = gen_bind_propp mode_schematic (map o cert_prop); 

6789  884 

10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

885 
end; 
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

886 

6789  887 

5819  888 

889 
(** theorems **) 

890 

18042  891 
(* fact_tac *) 
892 

52223
5bb6ae8acb87
tuned signature  more explicit flags for lowlevel Thm.bicompose;
wenzelm
parents:
52156
diff
changeset

893 
local 
5bb6ae8acb87
tuned signature  more explicit flags for lowlevel Thm.bicompose;
wenzelm
parents:
52156
diff
changeset

894 

5bb6ae8acb87
tuned signature  more explicit flags for lowlevel Thm.bicompose;
wenzelm
parents:
52156
diff
changeset

895 
fun comp_hhf_tac th i st = 
5bb6ae8acb87
tuned signature  more explicit flags for lowlevel Thm.bicompose;
wenzelm
parents:
52156
diff
changeset

896 
PRIMSEQ (Thm.bicompose {flatten = true, match = false, incremented = true} 
5bb6ae8acb87
tuned signature  more explicit flags for lowlevel Thm.bicompose;
wenzelm
parents:
52156
diff
changeset

897 
(false, Drule.lift_all (Thm.cprem_of st i) th, 0) i) st; 
5bb6ae8acb87
tuned signature  more explicit flags for lowlevel Thm.bicompose;
wenzelm
parents:
52156
diff
changeset

898 

27867  899 
fun comp_incr_tac [] _ = no_tac 
900 
 comp_incr_tac (th :: ths) i = 

52223
5bb6ae8acb87
tuned signature  more explicit flags for lowlevel Thm.bicompose;
wenzelm
parents:
52156
diff
changeset

901 
(fn st => comp_hhf_tac (Drule.incr_indexes st th) i st) APPEND comp_incr_tac ths i; 
5bb6ae8acb87
tuned signature  more explicit flags for lowlevel Thm.bicompose;
wenzelm
parents:
52156
diff
changeset

902 

5bb6ae8acb87
tuned signature  more explicit flags for lowlevel Thm.bicompose;
wenzelm
parents:
52156
diff
changeset

903 
in 
18042  904 

54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54740
diff
changeset

905 
fun fact_tac ctxt facts = Goal.norm_hhf_tac ctxt THEN' comp_incr_tac facts; 
18122  906 

27867  907 
fun potential_facts ctxt prop = 
908 
Facts.could_unify (facts_of ctxt) (Term.strip_all_body prop); 

909 

54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54740
diff
changeset

910 
fun some_fact_tac ctxt = SUBGOAL (fn (goal, i) => fact_tac ctxt (potential_facts ctxt goal) i); 
18042  911 

52223
5bb6ae8acb87
tuned signature  more explicit flags for lowlevel Thm.bicompose;
wenzelm
parents:
52156
diff
changeset

912 
end; 
5bb6ae8acb87
tuned signature  more explicit flags for lowlevel Thm.bicompose;
wenzelm
parents:
52156
diff
changeset

913 

18042  914 

56140
ed92ce2ac88e
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
wenzelm
parents:
56139
diff
changeset

915 
(* get facts *) 
5819  916 

26361  917 
local 
918 

56141
c06202417c4a
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
wenzelm
parents:
56140
diff
changeset

919 
fun retrieve_global context = 
c06202417c4a
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
wenzelm
parents:
56140
diff
changeset

920 
Facts.retrieve context (Global_Theory.facts_of (Context.theory_of context)); 
c06202417c4a
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
wenzelm
parents:
56140
diff
changeset

921 

56156
47015872e795
clarified retrieve_generic: local error takes precedence, which is relevant for completion;
wenzelm
parents:
56155
diff
changeset

922 
fun retrieve_generic (context as Context.Proof ctxt) arg = 
47015872e795
clarified retrieve_generic: local error takes precedence, which is relevant for completion;
wenzelm
parents:
56155
diff
changeset

923 
(Facts.retrieve context (facts_of ctxt) arg handle ERROR local_msg => 
47015872e795
clarified retrieve_generic: local error takes precedence, which is relevant for completion;
wenzelm
parents:
56155
diff
changeset

924 
(retrieve_global context arg handle ERROR _ => error local_msg)) 
56141
c06202417c4a
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
wenzelm
parents:
56140
diff
changeset

925 
 retrieve_generic context arg = retrieve_global context arg; 
c06202417c4a
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
wenzelm
parents:
56140
diff
changeset

926 

c06202417c4a
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
wenzelm
parents:
56140
diff
changeset

927 
fun retrieve pick context (Facts.Fact s) = 
16501  928 
let 
56140
ed92ce2ac88e
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
wenzelm
parents:
56139
diff
changeset

929 
val ctxt = Context.the_proof context; 
46849  930 
val pos = Syntax.read_token_pos s; 
42502  931 
val prop = 
932 
Syntax.read_prop (ctxt > set_mode mode_default > allow_dummies) s 

24511
69d270cc7e4f
removed obsolete read/cert variations (cf. Syntax.read/check);
wenzelm
parents:
24505
diff
changeset

933 
> singleton (Variable.polymorphic ctxt); 
48992  934 
fun err msg = error (msg ^ Position.here pos ^ ":\n" ^ Syntax.string_of_term ctxt prop); 
27867  935 

42502  936 
val (prop', _) = Term.replace_dummy_patterns prop (Variable.maxidx_of ctxt + 1); 
27867  937 
fun prove_fact th = 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54740
diff
changeset

938 
Goal.prove ctxt [] [] prop' (K (ALLGOALS (fact_tac ctxt [th]))); 
42502  939 
val results = map_filter (try prove_fact) (potential_facts ctxt prop'); 
56140
ed92ce2ac88e
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
wenzelm
parents:
56139
diff
changeset

940 
val thm = 
42502  941 
(case distinct Thm.eq_thm_prop results of 
56140
ed92ce2ac88e
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
wenzelm
parents:
56139
diff
changeset

942 
[thm] => thm 
42502  943 
 [] => err "Failed to retrieve literal fact" 
944 
 _ => err "Ambiguous specification of literal fact"); 

56140
ed92ce2ac88e
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
wenzelm
parents:
56139
diff
changeset

945 
in pick ("", Position.none) [thm] end 
56141
c06202417c4a
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
wenzelm
parents:
56140
diff
changeset

946 
 retrieve pick context (Facts.Named ((xname, pos), ivs)) = 
18042  947 
let 
56140
ed92ce2ac88e
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
wenzelm
parents:
56139
diff
changeset

948 
val thy = Context.theory_of context; 
ed92ce2ac88e
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
wenzelm
parents:
56139
diff
changeset

949 
val (name, thms) = 
ed92ce2ac88e
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
wenzelm
parents:
56139
diff
changeset

950 
(case xname of 
ed92ce2ac88e
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
wenzelm
parents:
56139
diff
changeset

951 
"" => (xname, [Thm.transfer thy Drule.dummy_thm]) 
ed92ce2ac88e
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
wenzelm
parents:
56139
diff
changeset

952 
 "_" => (xname, [Thm.transfer thy Drule.asm_rl]) 
56141
c06202417c4a
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
wenzelm
parents:
56140
diff
changeset

953 
 _ => retrieve_generic context (xname, pos)); 
56140
ed92ce2ac88e
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
wenzelm
parents:
56139
diff
changeset

954 
in pick (name, pos) (Facts.select (Facts.Named ((name, pos), ivs)) thms) end; 
5819  955 

26361  956 
in 
26346
17debd2fff8e
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset

957 

56141
c06202417c4a
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
wenzelm
parents:
56140
diff
changeset

958 
val get_fact_generic = retrieve (K I); 
c06202417c4a
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
wenzelm
parents:
56140
diff
changeset

959 
val get_fact = retrieve (K I) o Context.Proof; 
c06202417c4a
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
wenzelm
parents:
56140
diff
changeset

960 
val get_fact_single = retrieve Facts.the_single o Context.Proof; 
26346
17debd2fff8e
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset

961 

26361  962 
fun get_thms ctxt = get_fact ctxt o Facts.named; 
963 
fun get_thm ctxt = get_fact_single ctxt o Facts.named; 

964 

965 
end; 

5819  966 

967 

26284  968 
(* facts *) 
5819  969 

28082
37350f301128
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
28017
diff
changeset

970 
local 
37350f301128
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
28017
diff
changeset

971 

28965  972 
fun update_thms _ (b, NONE) ctxt = ctxt > map_facts (Facts.del (full_name ctxt b)) 
49747  973 
 update_thms flags (b, SOME ths) ctxt = ctxt > map_facts 
974 
(Facts.add_static (Context.Proof ctxt) flags (b, ths) #> snd); 

5819  975 

30761
ac7570d80c3d
renamed ProofContext.note_thmss_i to ProofContext.note_thmss, eliminated obsolete external version;
wenzelm
parents:
30758
diff
changeset

976 
in 
ac7570d80c3d
renamed ProofContext.note_thmss_i to ProofContext.note_thmss, eliminated obsolete external version;
wenzelm
parents:
30758
diff
changeset

977 

46775
6287653e63ec
canonical argument order for attribute application;
wenzelm
parents:
45666
diff
changeset

978 
fun note_thmss kind = fold_map (fn ((b, more_atts), raw_facts) => fn ctxt => 
5819  979 
let 
28965  980 
val name = full_name ctxt b; 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
39508
diff
changeset

981 
val facts = Global_Theory.name_thmss false name raw_facts; 
46775
6287653e63ec
canonical argument order for attribute application;
wenzelm
parents:
45666
diff
changeset

982 
fun app (ths, atts) = 
6287653e63ec
canonical argument order for attribute application;
wenzelm
parents:
45666
diff
changeset

983 
fold_map (Thm.proof_attributes (surround (Thm.kind kind) (atts @ more_atts))) ths; 
21443
cc5095d57da4
added stmt mode, which affects naming/indexing of local facts;
wenzelm
parents:
21370
diff
changeset

984 
val (res, ctxt') = fold_map app facts ctxt; 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
39508
diff
changeset

985 
val thms = Global_Theory.name_thms false false name (flat res); 
24388
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

986 
val Mode {stmt, ...} = get_mode ctxt; 
49747  987 
in ((name, thms), ctxt' > update_thms {strict = false, index = stmt} (b, SOME thms)) end); 
12711  988 

49747  989 
fun put_thms index thms ctxt = ctxt 
47005
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset

990 
> map_naming (K Name_Space.local_naming) 
33383  991 
> Context_Position.set_visible false 
49747  992 
> update_thms {strict = false, index = index} (apfst Binding.name thms) 
33383  993 
> Context_Position.restore_visible ctxt 
28417  994 
> restore_naming ctxt; 
28082
37350f301128
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
28017
diff
changeset

995 

12711  996 
end; 
9196  997 

5819  998 

999 

35680  1000 
(** basic logical entities **) 
17360
fa1f262dbc4e
added add_view, export_view (supercedes adhoc view arguments);
wenzelm
parents:
17221
diff
changeset

1001 

8096  1002 
(* variables *) 
1003 

19897
fe661eb3b0e7
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19882
diff
changeset

1004 
fun declare_var (x, opt_T, mx) ctxt = 
42287
d98eb048a2e4
discontinued special treatment of structure Mixfix;
wenzelm
parents:
42267
diff
changeset

1005 
let val T = (case opt_T of SOME T => T  NONE => Mixfix.mixfixT mx) 
20163  1006 
in ((x, T, mx), ctxt > Variable.declare_constraints (Free (x, T))) end; 
19897
fe661eb3b0e7
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19882
diff
changeset

1007 

10381  1008 
local 
1009 

25353
17f04d987f37
removed unused read_termTs_schematic, read/cert_vars_legacy, add_fixes_legacy;
wenzelm
parents:
25345
diff
changeset

1010 
fun prep_vars prep_typ internal = 
35129  1011 
fold_map (fn (b, raw_T, mx) => fn ctxt => 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1012 
let 
42494  1013 
val x = Variable.check_name b; 
55949  1014 
val check_name = if internal then Name.reject_skolem else Name.reject_internal; 
1015 
val _ = 

1016 
if can check_name (x, []) andalso Symbol_Pos.is_identifier x then () 

1017 
else error ("Bad name: " ^ Binding.print b); 

12504  1018 

18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1019 
fun cond_tvars T = 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1020 
if internal then T 
18678  1021 
else Type.no_tvars T handle TYPE (msg, _, _) => error msg; 
24277  1022 
val opt_T = Option.map (cond_tvars o cert_typ ctxt o prep_typ ctxt) raw_T; 
35129  1023 
val (_, ctxt') = ctxt > declare_var (x, opt_T, mx); 
1024 
in ((b, opt_T, mx), ctxt') end); 

8096  1025 

10381  1026 
in 
1027 

45427
fca432074fb2
sort assignment before simultaneous term_check, not isolated parse_term;
wenzelm
parents:
45330
diff
changeset

1028 
val read_vars = prep_vars Syntax.read_typ false; 
25353
17f04d987f37
removed unused read_termTs_schematic, read/cert_vars_legacy, add_fixes_legacy;
wenzelm
parents:
25345
diff
changeset

1029 
val cert_vars = prep_vars (K I) true; 
8096  1030 

10381  1031 
end; 
1032 

8096  1033 

21744  1034 
(* notation *) 
1035 

24949  1036 
local 
1037 

35429
afa8cf9e63d8
authentic syntax for classes and type constructors;
wenzelm
parents:
35412
diff
changeset

1038 
fun type_syntax (Type (c, args), mx) = 
42290
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42287
diff
changeset

1039 
SOME (Local_Syntax.Type, (Lexicon.mark_type c, Mixfix.make_type (length args), mx)) 
35412
b8dead547d9e
more uniform treatment of syntax for types vs. consts;
wenzelm
parents:
35399
diff
changeset

1040 
 type_syntax _ = NONE; 
b8dead547d9e
more uniform treatment of syntax for types vs. consts;
wenzelm
parents:
35399
diff
changeset

1041 

b8dead547d9e
more uniform treatment of syntax for types vs. consts;
wenzelm
parents:
35399
diff
changeset

1042 
fun const_syntax _ (Free (x, T), mx) = SOME (Local_Syntax.Fixed, (x, T, mx)) 
24949  1043 
 const_syntax ctxt (Const (c, _), mx) = 
35255  1044 
(case try (Consts.type_scheme (consts_of ctxt)) c of 
42290
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42287
diff
changeset

1045 
SOME T => SOME (Local_Syntax.Const, (Lexicon.mark_const c, T, mx)) 
35255  1046 
 NONE => NONE) 
24949  1047 
 const_syntax _ _ = NONE; 
1048 

35412
b8dead547d9e
more uniform treatment of syntax for types vs. consts;
wenzelm
parents:
35399
diff
changeset

1049 
fun gen_notation syntax add mode args ctxt = 
b8dead547d9e
more uniform treatment of syntax for types vs. consts;
wenzelm
parents:
35399
diff
changeset

1050 
ctxt > map_syntax 
b8dead547d9e
more uniform treatment of syntax for types vs. consts;
wenzelm
parents:
35399
diff
changeset

1051 
(Local_Syntax.update_modesyntax (theory_of ctxt) add mode (map_filter (syntax ctxt) args)); 
b8dead547d9e
more uniform treatment of syntax for types vs. consts;
wenzelm
parents:
35399
diff
changeset

1052 

24949  1053 
in 
21744  1054 

35412
b8dead547d9e
more uniform treatment of syntax for types vs. consts;
wenzelm
parents:
35399
diff
changeset

1055 
val type_notation = gen_notation (K type_syntax); 
b8dead547d9e
more uniform treatment of syntax for types vs. consts;
wenzelm
parents:
35399
diff
changeset

1056 
val notation = gen_notation const_syntax; 
b8dead547d9e
more uniform treatment of syntax for types vs. consts;
wenzelm
parents:
35399
diff
changeset

1057 

47247  1058 
fun generic_type_notation add mode args phi = 
35412
b8dead547d9e
more uniform treatment of syntax for types vs. consts;
wenzelm
parents:
35399
diff
changeset

1059 
let 
b8dead547d9e
more uniform treatment of syntax for types vs. consts;
wenzelm
parents:
35399
diff
changeset

1060 
val args' = args > map_filter (fn (T, mx) => 
b8dead547d9e
more uniform treatment of syntax for types vs. consts;
wenzelm
parents:
35399
diff
changeset

1061 
let 
b8dead547d9e
more uniform treatment of syntax for types vs. consts;
wenzelm
parents:
35399
diff
changeset

1062 
val T' = Morphism.typ phi T; 
b8dead547d9e
more uniform treatment of syntax for types vs. consts;
wenzelm
parents:
35399
diff
changeset

1063 
val similar = (case (T, T') of (Type (c, _), Type (c', _)) => c = c'  _ => false); 
b8dead547d9e
more uniform treatment of syntax for types vs. consts;
wenzelm
parents:
35399
diff
changeset

1064 
in if similar then SOME (T', mx) else NONE end); 
b8dead547d9e
more uniform treatment of syntax for types vs. consts;
wenzelm
parents:
35399
diff
changeset

1065 
in Context.mapping (Sign.type_notation add mode args') (type_notation add mode args') end; 
24949  1066 

47247  1067 
fun generic_notation add mode args phi = 
33537
06c87d2c5b5a
locale_const/target_notation: uniform use of Term.aconv_untyped;
wenzelm
parents:
33519
diff
changeset

1068 
let 
06c87d2c5b5a
locale_const/target_notation: uniform use of Term.aconv_untyped;
wenzelm
parents:
33519
diff
changeset

1069 
val args' = args > map_filter (fn (t, mx) => 
06c87d2c5b5a
locale_const/target_notation: uniform use of Term.aconv_untyped;
wenzelm
parents:
33519
diff
changeset

1070 
let val t' = Morphism.term phi t 
06c87d2c5b5a
locale_const/target_notation: uniform use of Term.aconv_untyped;
wenzelm
parents:
33519
diff
changeset

1071 
in if Term.aconv_untyped (t, t') then SOME (t', mx) else NONE end); 
24949  1072 
in Context.mapping (Sign.notation add mode args') (notation add mode args') end; 
1073 

35680  1074 
end; 
35412
b8dead547d9e
more uniform treatment of syntax for types vs. consts;
wenzelm
parents:
35399
diff
changeset

1075 

35680  1076 

1077 
(* aliases *) 

1078 

36450  1079 
fun class_alias b c ctxt = (map_tsig o apfst) (Type.class_alias (naming_of ctxt) b c) ctxt; 
1080 
fun type_alias b c ctxt = (map_tsig o apfst) (Type.type_alias (naming_of ctxt) b c) ctxt; 

35680  1081 
fun const_alias b c ctxt = (map_consts o apfst) (Consts.alias (naming_of ctxt) b c) ctxt; 
21744  1082 

1083 

24767  1084 
(* local constants *) 
1085 

1086 
fun add_const_constraint (c, opt_T) ctxt = 

1087 
let 

1088 
fun prepT raw_T = 

1089 
let val T = cert_typ ctxt raw_T 

1090 
in cert_term ctxt (Const (c, T)); T end; 

25039  1091 
in ctxt > (map_consts o apfst) (Consts.constrain (c, Option.map prepT opt_T)) end; 
19001  1092 

33173
b8ca12f6681a
eliminated obsolete tags for types/consts  now handled via name space, in strongly typed fashion;
wenzelm
parents:
33165
diff
changeset

1093 
fun add_abbrev mode (b, raw_t) ctxt = 
19001  1094 
let 
24675
2be1253a20d3
removed obsolete set_expand_abbrevs (superceded by mode_abbrev);
wenzelm
parents:
24612
diff
changeset

1095 
val t0 = cert_term (ctxt > set_mode mode_abbrev) raw_t 
42381
309ec68442c6
added Binding.print convenience, which includes quote already;
wenzelm
parents:
42379
diff
changeset

1096 
handle ERROR msg => cat_error msg ("in constant abbreviation " ^ Binding.print b); 
20008
8d9d770e1f06
add_abbrevs/polymorphic: Variable.exportT_terms avoids overgeneralization;
wenzelm
parents:
19916
diff
changeset

1097 
val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0]; 
21807
a59f083632a7
add_abbrev: removed Assumption.add_assms (danger of inconsistent naming);
wenzelm
parents:
21803
diff
changeset

1098 
val ((lhs, rhs), consts') = consts_of ctxt 
47005
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset

1099 
> Consts.abbreviate (Context.Proof ctxt) (tsig_of ctxt) mode (b, t); 
19001  1100 
in 
1101 
ctxt 

25039  1102 
> (map_consts o apfst) (K consts') 
21803  1103 
> Variable.declare_term rhs 
1104 
> pair (lhs, rhs) 

21704  1105 
end; 
19001  1106 

25052  1107 
fun revert_abbrev mode c = (map_consts o apfst) (Consts.revert_abbrev mode c); 
1108 

47275  1109 
fun generic_add_abbrev mode arg = 
1110 
Context.mapping_result (Sign.add_abbrev mode arg) (add_abbrev mode arg); 

1111 

1112 
fun generic_revert_abbrev mode arg = 

1113 
Context.mapping (Sign.revert_abbrev mode arg) (revert_abbrev mode arg); 

1114 

19001  1115 

18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1116 
(* fixes *) 
5819  1117 

30763
6976521b4263
renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
wenzelm
parents:
30761
diff
changeset

1118 
fun add_fixes raw_vars ctxt = 
8096  1119 
let 
42491
4bb5de0aae66
more precise position information via Variable.add_fixes_binding;
wenzelm
parents:
42488
diff
changeset

1120 
val thy = theory_of ctxt; 
4bb5de0aae66
more precise position information via Variable.add_fixes_binding;
wenzelm
parents:
42488
diff
changeset

1121 
val vars = #1 (cert_vars raw_vars ctxt); 
4bb5de0aae66
more precise position information via Variable.add_fixes_binding;
wenzelm
parents:
42488
diff
changeset

1122 
in 
4bb5de0aae66
more precise position information via Variable.add_fixes_binding;
wenzelm
parents:
42488
diff
changeset

1123 
ctxt 
4bb5de0aae66
more precise position information via Variable.add_fixes_binding;
wenzelm
parents:
42488
diff
changeset

1124 
> Variable.add_fixes_binding (map #1 vars) 
4bb5de0aae66
more precise position information via Variable.add_fixes_binding;
wenzelm
parents:
42488
diff
changeset

1125 
> (fn xs => 
4bb5de0aae66
more precise position information via Variable.add_fixes_binding;
wenzelm
parents:
42488
diff
changeset

1126 
fold_map declare_var (map2 (fn x => fn (_, T, mx) => (x, T, mx)) xs vars) 
4bb5de0aae66
more precise position information via Variable.add_fixes_binding;
wenzelm
parents:
42488
diff
changeset

1127 
#> (map_syntax o Local_Syntax.add_syntax thy o map (pair Local_Syntax.Fixed)) 
4bb5de0aae66
more precise position information via Variable.add_fixes_binding;
wenzelm
parents:
42488
diff
changeset

1128 
#> pair xs) 
4bb5de0aae66
more precise position information via Variable.add_fixes_binding;
wenzelm
parents:
42488
diff
changeset

1129 
end; 
5819  1130 

9291
23705d14be8f
"_i" arguments now expected to have skolems already internalized;
wenzelm
parents:
9274
diff
changeset

1131 

23705d14be8f
"_i" arguments now expected to have skolems already internalized;
wenzelm
parents:
9274
diff
changeset

1132 

18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1133 
(** assumptions **) 
18187  1134 

20209  1135 
local 
1136 

1137 
fun gen_assms prepp exp args ctxt = 

1138 
let 

20234
7e0693474bcd
added legacy_pretty_thm (with fallback on ProtoPure.thy);
wenzelm
parents:
20209
diff
changeset

1139 
val cert = Thm.cterm_of (theory_of ctxt); 
45327  1140 
val ((propss, _), ctxt1) = prepp (map snd args) ctxt; 
20234
7e0693474bcd
added legacy_pretty_thm (with fallback on ProtoPure.thy);
wenzelm
parents:
20209
diff
changeset

1141 
val _ = Variable.warn_extra_tfrees ctxt ctxt1; 
7e0693474bcd
added legacy_pretty_thm (with fallback on ProtoPure.thy);
wenzelm
parents:
20209
diff
changeset

1142 
val (premss, ctxt2) = fold_burrow (Assumption.add_assms exp o map cert) propss ctxt1; 
7e0693474bcd
added legacy_pretty_thm (with fallback on ProtoPure.thy);
wenzelm
parents:
20209
diff
changeset

1143 
in 
7e0693474bcd
added legacy_pretty_thm (with fallback on ProtoPure.thy);
wenzelm
parents:
20209
diff
changeset

1144 
ctxt2 
7e0693474bcd
added legacy_pretty_thm (with fallback on ProtoPure.thy);
wenzelm
parents:
20209
diff
changeset

1145 
> auto_bind_facts (flat propss) 
33644
5266a72e0889
eliminated slightly odd (unused) "axiom" and "assumption"  collapsed to unspecific "";
wenzelm
parents:
33537
diff
changeset

1146 
> note_thmss "" (map fst args ~~ map (map (fn th => ([th], []))) premss) 
20234
7e0693474bcd
added legacy_pretty_thm (with fallback on ProtoPure.thy);
wenzelm
parents:
20209
diff
changeset

1147 
end; 
20209  1148 

1149 
in 

1150 

45327  1151 
val add_assms = gen_assms bind_propp; 
1152 
val add_assms_i = gen_assms bind_propp_i; 

20209  1153 

1154 
end; 

1155 

1156 

5819  1157 

8373
e7237c8fe29e
handling of local contexts: print_cases, get_case, add_cases;
wenzelm
parents:
8186
diff
changeset

1158 
(** cases **) 
e7237c8fe29e
handling of local contexts: print_cases, get_case, add_cases;
wenzelm
parents:
8186
diff
changeset

1159 

53378
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

1160 
fun dest_cases ctxt = 
56025  1161 
Name_Space.fold_table (fn (a, (c, i)) => cons (i, (a, c))) (cases_of ctxt) [] 
53378
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

1162 
> sort (int_ord o pairself #1) > map #2; 
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

1163 

16147  1164 
local 
1165 

53378
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

1166 
fun update_case _ _ ("", _) res = res 
56025  1167 
 update_case _ _ (name, NONE) (cases, index) = 
1168 
(Name_Space.del_table name cases, index) 

53378
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

1169 
 update_case context is_proper (name, SOME c) (cases, index) = 
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

1170 
let 
56145
a200bffe4027
conceal improper cases, e.g. relevant for completion (and potentially for markup);
wenzelm
parents:
56143
diff
changeset

1171 
val binding = 
a200bffe4027
conceal improper cases, e.g. relevant for completion (and potentially for markup);
wenzelm
parents:
56143
diff
changeset

1172 
Binding.make (name, Position.none) 
a200bffe4027
conceal improper cases, e.g. relevant for completion (and potentially for markup);
wenzelm
parents:
56143
diff
changeset

1173 
> not is_proper ? Binding.conceal; 
a200bffe4027
conceal improper cases, e.g. relevant for completion (and potentially for markup);
wenzelm
parents:
56143
diff
changeset

1174 
val (_, cases') = cases 
a200bffe4027
conceal improper cases, e.g. relevant for completion (and potentially for markup);
wenzelm
parents:
56143
diff
changeset

1175 
> Name_Space.define context false (binding, ((c, is_proper), index)); 
53378
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

1176 
val index' = index + 1; 
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

1177 
in (cases', index') end; 
18609  1178 

42501
2b8c34f53388
eliminated slightly odd Proof_Context.bind_fixes;
wenzelm
parents:
42496
diff
changeset

1179 
fun fix (b, T) ctxt = 
2b8c34f53388
eliminated slightly odd Proof_Context.bind_fixes;
wenzelm
parents:
42496
diff
changeset

1180 
let val ([x], ctxt') = add_fixes [(b, SOME T, NoSyn)] ctxt 
2b8c34f53388
eliminated slightly odd Proof_Context.bind_fixes;
wenzelm
parents:
42496
diff
changeset

1181 
in (Free (x, T), ctxt') end; 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1182 

16147  1183 
in 
1184 

53378
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

1185 
fun update_cases is_proper args ctxt = 
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

1186 
let 
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

1187 
val context = Context.Proof ctxt > Name_Space.map_naming (K Name_Space.default_naming); 
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

1188 
val cases = cases_of ctxt; 
56025  1189 
val index = Name_Space.fold_table (fn _ => Integer.add 1) cases 0; 
53378
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

1190 
val (cases', _) = fold (update_case context is_proper) args (cases, index); 
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

1191 
in map_cases (K cases') ctxt end; 
18609  1192 

1193 
fun case_result c ctxt = 

1194 
let 

33368  1195 
val Rule_Cases.Case {fixes, ...} = c; 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1196 
val (ts, ctxt') = ctxt > fold_map fix fixes; 
33368  1197 
val Rule_Cases.Case {assumes, binds, cases, ...} = Rule_Cases.apply ts c; 
18609  1198 
in 
1199 
ctxt' 

30757
2d2076300185
replaced add_binds(_i) by bind_terms  internal version only;
wenzelm
parents:
30723
diff
changeset

1200 
> bind_terms (map drop_schematic binds) 
53378
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

1201 
> update_cases true (map (apsnd SOME) cases) 
18609  1202 
> pair (assumes, (binds, cases)) 
1203 
end; 

1204 

1205 
val apply_case = apfst fst oo case_result; 

1206 

53378
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

1207 
fun check_case ctxt (name, pos) fxs = 
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

1208 
let 
56202  1209 
val (_, ((Rule_Cases.Case {fixes, assumes, binds, cases}, is_proper), _)) = 
53378
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

1210 
Name_Space.check (Context.Proof ctxt) (cases_of ctxt) (name, pos); 
56202  1211 
val _ = if is_proper then () else Context_Position.report ctxt pos Markup.improper; 
53378
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

1212 

07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

1213 
fun replace (opt_x :: xs) ((y, T) :: ys) = (the_default y opt_x, T) :: replace xs ys 
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

1214 
 replace [] ys = ys 
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

1215 
 replace (_ :: _) [] = 
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

1216 
error ("Too many parameters for case " ^ quote name ^ Position.here pos); 
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

1217 
val fixes' = replace fxs fixes; 
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

1218 
val binds' = map drop_schematic binds; 
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

1219 
in 
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

1220 
if null (fold (Term.add_tvarsT o snd) fixes []) andalso 
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

1221 
null (fold (fold Term.add_vars o snd) assumes []) then 
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

1222 
Rule_Cases.Case {fixes = fixes', assumes = assumes, binds = binds', cases = cases} 
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

1223 
else error ("Illegal schematic variable(s) in case " ^ quote name ^ Position.here pos) 
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

1224 
end; 
8373
e7237c8fe29e
handling of local contexts: print_cases, get_case, add_cases;
wenzelm
parents:
8186
diff
changeset

1225 

16147  1226 
end; 
8373
e7237c8fe29e
handling of local contexts: print_cases, ge 