author  wenzelm 
Wed, 05 Mar 2014 19:52:28 +0100  
changeset 55923  4bdae9403baf 
parent 55922  710bc66f432c 
child 55948  bb21b380f65d 
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 
26284  33 
val facts_of: Proof.context > Facts.T 
47005
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset

34 
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

35 
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

36 
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

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

40 
val const_space: Proof.context > Name_Space.T 

41 
val intern_class: Proof.context > xstring > string 

42 
val intern_type: Proof.context > xstring > string 

43 
val intern_const: Proof.context > xstring > string 

44 
val extern_class: Proof.context > string > xstring 

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

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

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

20310  53 
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

54 
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

55 
val background_theory_result: (theory > 'a * theory) > Proof.context > 'a * Proof.context 
28212  56 
val extern_fact: Proof.context > string > xstring 
21728  57 
val pretty_term_abbrev: Proof.context > term > Pretty.T 
49888  58 
val markup_fact: Proof.context > string > Markup.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 
55922
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55843
diff
changeset

71 
val check_type_name: Proof.context > bool > 
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 
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55843
diff
changeset

73 
val check_type_name_proper: Proof.context > bool > 
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55843
diff
changeset

74 
xstring * Position.T > typ * Position.report list 
35360
df2b2168e43a
clarified ProofContext.read_type_name/Args.type_name wrt strict logical constructors;
wenzelm
parents:
35262
diff
changeset

75 
val read_type_name: Proof.context > bool > string > typ 
35669
a91c7ed801b8
added ProofContext.tsig_of  proforma version for local name space only, not logical content;
wenzelm
parents:
35616
diff
changeset

76 
val read_type_name_proper: Proof.context > bool > string > typ 
35399
3881972fcfca
clarified ProofContext.read_const(_proper)/Args.const(_proper) wrt. strict logical consts;
wenzelm
parents:
35360
diff
changeset

77 
val read_const_proper: Proof.context > bool > string > term 
36505
79c1d2bbe5a9
ProofContext.read_const: allow for type constraint (for fixed variable);
wenzelm
parents:
36503
diff
changeset

78 
val read_const: Proof.context > bool > typ > string > term 
46922
3717f3878714
source positions for locale and class expressions;
wenzelm
parents:
46849
diff
changeset

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

80 
val cert_arity: Proof.context > arity > arity 
27259  81 
val allow_dummies: Proof.context > Proof.context 
49674
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

82 
val prepare_sortsT: Proof.context > typ list > string * typ list 
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

83 
val prepare_sorts: Proof.context > term list > string * term list 
36152  84 
val check_tfree: Proof.context > string * sort > string * sort 
42250
cc5ac538f991
eliminated odd objectoriented type_context/term_context;
wenzelm
parents:
42242
diff
changeset

85 
val intern_skolem: Proof.context > string > string option 
24684  86 
val read_term_pattern: Proof.context > string > term 
87 
val read_term_schematic: Proof.context > string > term 

88 
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

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

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

91 
val expand_abbrevs: Proof.context > term > term 
20310  92 
val cert_term: Proof.context > term > term 
93 
val cert_prop: Proof.context > term > term 

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

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

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

20310  98 
val goal_export: Proof.context > Proof.context > thm list > thm list 
99 
val export: Proof.context > Proof.context > thm list > thm list 

21531  100 
val export_morphism: Proof.context > Proof.context > morphism 
28396  101 
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

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

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

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

45327  107 
val read_propp: (string * string list) list list > Proof.context > 
108 
(term * term list) list list * Proof.context 

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

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

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

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

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

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

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

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

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

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

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

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

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

122 
(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

123 
val fact_tac: Proof.context > thm list > int > tactic 
20310  124 
val some_fact_tac: Proof.context > int > tactic 
26346
17debd2fff8e
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset

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

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

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

128 
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

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

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

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

135 
(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

136 
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

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

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

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

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

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

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

145 
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

146 
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

147 
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

148 
val type_notation: bool > Syntax.mode > (typ * mixfix) list > Proof.context > Proof.context 
24949  149 
val notation: bool > Syntax.mode > (term * mixfix) list > Proof.context > Proof.context 
47247  150 
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

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

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

24767  157 
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

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

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

20310  163 
val print_syntax: Proof.context > unit 
21728  164 
val print_abbrevs: Proof.context > unit 
20310  165 
val print_binds: Proof.context > unit 
166 
val print_lthms: Proof.context > unit 

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*) 

214 
facts: Facts.T, (*local 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 = 
47005
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset

224 
make_data (mode_default, Local_Syntax.init thy, 
35669
a91c7ed801b8
added ProofContext.tsig_of  proforma version for local name space only, not logical content;
wenzelm
parents:
35616
diff
changeset

225 
(Sign.tsig_of thy, Sign.tsig_of thy), 
53378
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

226 
(Sign.consts_of thy, Sign.consts_of thy), Facts.empty, empty_cases); 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

227 
); 
5819  228 

45650  229 
fun rep_data ctxt = Data.get ctxt > (fn Data rep => rep); 
5819  230 

45650  231 
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

232 
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

233 
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

234 

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

235 
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

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

237 

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

238 
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

239 
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

240 
(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

241 

19001  242 
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

243 
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

244 
(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

245 

36450  246 
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

247 
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

248 
(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

249 

19001  250 
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

251 
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

252 
(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

253 

26284  254 
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

255 
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

256 
(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

257 

19001  258 
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

259 
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

260 
(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

261 

45650  262 
val get_mode = #mode o rep_data; 
28407  263 
val restore_mode = set_mode o get_mode; 
27286  264 
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

265 

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

19001  268 

45650  269 
val syntax_of = #syntax o rep_data; 
33387  270 
val syn_of = Local_Syntax.syn_of o syntax_of; 
271 
val set_syntax_mode = map_syntax o Local_Syntax.set_mode; 

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

19001  273 

45650  274 
val tsig_of = #1 o #tsig o rep_data; 
36451  275 
val set_defsort = map_tsig o apfst o Type.set_defsort; 
35680  276 
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

277 

45650  278 
val consts_of = #1 o #consts o rep_data; 
279 
val facts_of = #facts o rep_data; 

280 
val cases_of = #cases o rep_data; 

5819  281 

282 

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

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

284 

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

285 
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

286 
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

287 
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

288 

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

289 
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

290 

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

291 

42359  292 
(* name spaces *) 
293 

294 
val class_space = Type.class_space o tsig_of; 

295 
val type_space = Type.type_space o tsig_of; 

296 
val const_space = Consts.space_of o consts_of; 

297 

298 
val intern_class = Name_Space.intern o class_space; 

299 
val intern_type = Name_Space.intern o type_space; 

300 
val intern_const = Name_Space.intern o const_space; 

301 

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

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

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

305 

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

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

309 

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

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

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

313 

42359  314 

20367  315 
(* theory transfer *) 
12093  316 

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

317 
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

318 
map_syntax (Local_Syntax.rebuild thy) > 
36450  319 
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

320 
let val thy_tsig = Sign.tsig_of thy in 
36450  321 
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

322 
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

323 
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

324 
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

325 
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

326 
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

327 
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

328 
end); 
17072  329 

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

330 
fun transfer thy = Context.raw_transfer thy #> transfer_syntax thy; 
17072  331 

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

332 
fun background_theory f ctxt = transfer (f (theory_of ctxt)) ctxt; 
20367  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_result f ctxt = 
20367  335 
let val (res, thy') = f (theory_of ctxt) 
336 
in (res, ctxt > transfer thy') end; 

19019  337 

12093  338 

339 

14828  340 
(** pretty printing **) 
341 

28212  342 
(* extern *) 
343 

42378  344 
fun which_facts ctxt name = 
28212  345 
let 
346 
val local_facts = facts_of 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

347 
val global_facts = Global_Theory.facts_of (theory_of ctxt); 
28212  348 
in 
349 
if is_some (Facts.lookup (Context.Proof ctxt) local_facts name) 

42378  350 
then local_facts else global_facts 
28212  351 
end; 
352 

42379  353 
fun markup_fact ctxt name = Name_Space.markup (Facts.space_of (which_facts ctxt name)) name; 
42378  354 

355 
fun extern_fact ctxt name = Facts.extern ctxt (which_facts ctxt name) name; 

356 

28212  357 

358 
(* pretty *) 

359 

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

42378  362 
fun pretty_fact_name ctxt a = 
363 
Pretty.block [Pretty.mark_str (markup_fact ctxt a, 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

364 

51583  365 
fun pretty_fact ctxt = 
366 
let 

367 
val pretty_thm = Display.pretty_thm ctxt; 

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

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

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

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

374 
end; 

14828  375 

376 

377 

5819  378 
(** prepare types **) 
379 

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

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

381 

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

382 
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

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

384 
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

385 
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

386 

ee71b2687c4b
more markup for read_class: imitate Name_Space.check despite lack of Name_Space.table;
wenzelm
parents:
55829
diff
changeset

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

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

389 
error (msg ^ Position.here pos ^ 
2982d233d798
consider completion report as part of error message  less stateful, may get handled;
wenzelm
parents:
55839
diff
changeset

390 
Markup.markup Markup.report 
2982d233d798
consider completion report as part of error message  less stateful, may get handled;
wenzelm
parents:
55839
diff
changeset

391 
(Completion.reported_text 
2982d233d798
consider completion report as part of error message  less stateful, may get handled;
wenzelm
parents:
55839
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 

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

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

426 

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

427 
(* check Skolem constants *) 
7679  428 

18678  429 
fun no_skolem internal x = 
20086
94ca946fb689
adapted to more efficient Name/Variable implementation;
wenzelm
parents:
20049
diff
changeset

430 
if can Name.dest_skolem x then 
18678  431 
error ("Illegal reference to internal Skolem constant: " ^ quote x) 
20086
94ca946fb689
adapted to more efficient Name/Variable implementation;
wenzelm
parents:
20049
diff
changeset

432 
else if not internal andalso can Name.dest_internal x then 
18678  433 
error ("Illegal reference to internal variable: " ^ quote x) 
7679  434 
else x; 
435 

436 

18187  437 

5819  438 
(** prepare terms and propositions **) 
439 

25328  440 
(* inferred types of parameters *) 
441 

442 
fun infer_type ctxt x = 

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

443 
Term.fastype_of (singleton (Syntax.check_terms (set_mode mode_schematic ctxt)) (Free x)); 
25328  444 

445 
fun inferred_param x ctxt = 

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

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

447 
in (T, ctxt > Variable.declare_term (Free (x, T))) end; 
25328  448 

449 
fun inferred_fixes ctxt = 

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

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

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

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

453 
in (xs ~~ Ts, ctxt') end; 
25328  454 

455 

55842  456 
(* type names *) 
25328  457 

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

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

459 
if Lexicon.is_tid c then 
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55843
diff
changeset

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

461 
val reports = 
55923  462 
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

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

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

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

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

467 
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

468 
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

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

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

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

472 
 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

473 
 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

474 
in (Type (d, replicate args dummyT), reports) end; 
25328  475 

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

476 
fun check_type_name_proper ctxt strict arg = 
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55843
diff
changeset

477 
(case check_type_name ctxt strict arg of 
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55843
diff
changeset

478 
res as (Type _, _) => res 
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55843
diff
changeset

479 
 (T, _) => error ("Not a type constructor: " ^ Syntax.string_of_typ ctxt T)); 
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55843
diff
changeset

480 

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

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

482 
Syntax.read_token #> Symbol_Pos.source_content #> check_type_name ctxt strict #> #1; 
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55843
diff
changeset

483 

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

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

485 
Syntax.read_token #> Symbol_Pos.source_content #> check_type_name_proper ctxt strict #> #1; 
35669
a91c7ed801b8
added ProofContext.tsig_of  proforma version for local name space only, not logical content;
wenzelm
parents:
35616
diff
changeset

486 

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

487 

55842  488 
(* constant names *) 
489 

490 
local 

491 

492 
fun prep_const_proper ctxt strict (c, pos) = 

493 
let 

494 
fun err msg = error (msg ^ Position.here pos); 

495 
val consts = consts_of ctxt; 

496 
val t as Const (d, _) = 

497 
(case Variable.lookup_const ctxt c of 

498 
SOME d => 

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

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

500 
val T = Consts.type_scheme (consts_of ctxt) d handle TYPE (msg, _, _) => err msg; 
3fa61f39d1f2
prefer Name_Space.check with its builtin reports (including completion);
wenzelm
parents:
55842
diff
changeset

501 
val _ = Context_Position.report ctxt pos (Name_Space.markup (Consts.space_of consts) d); 
3fa61f39d1f2
prefer Name_Space.check with its builtin reports (including completion);
wenzelm
parents:
55842
diff
changeset

502 
in Const (d, T) end 
3fa61f39d1f2
prefer Name_Space.check with its builtin reports (including completion);
wenzelm
parents:
55842
diff
changeset

503 
 NONE => Consts.check_const (Context.Proof ctxt) consts (c, pos)); 
55842  504 
val _ = 
55843
3fa61f39d1f2
prefer Name_Space.check with its builtin reports (including completion);
wenzelm
parents:
55842
diff
changeset

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

506 
then ignore (Consts.the_const consts d) handle TYPE (msg, _, _) => err msg 
55842  507 
else (); 
508 
in t end; 

509 

510 
in 

511 

55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55740
diff
changeset

512 
fun read_const_proper ctxt strict = 
55829  513 
prep_const_proper ctxt strict o Symbol_Pos.source_content o Syntax.read_token; 
27821  514 

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

515 
fun read_const ctxt strict ty text = 
36542
7cb6b40d19b2
read_const: disallow internal names as usual in visible Isar text;
wenzelm
parents:
36505
diff
changeset

516 
let 
55829  517 
val (c, pos) = Symbol_Pos.source_content (Syntax.read_token text); 
36542
7cb6b40d19b2
read_const: disallow internal names as usual in visible Isar text;
wenzelm
parents:
36505
diff
changeset

518 
val _ = no_skolem false c; 
7cb6b40d19b2
read_const: disallow internal names as usual in visible Isar text;
wenzelm
parents:
36505
diff
changeset

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

520 
(case (Variable.lookup_fixed ctxt c, Variable.is_const ctxt c) of 
27821  521 
(SOME x, false) => 
39507
839873937ddd
tuned signature of (Context_)Position.report variants;
wenzelm
parents:
39441
diff
changeset

522 
(Context_Position.report ctxt pos 
50201
c26369c9eda6
Isabellespecific implementation of quasiabstract markup elements  back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50126
diff
changeset

523 
(Markup.name x (if can Name.dest_skolem x then Markup.skolem else Markup.free)); 
36505
79c1d2bbe5a9
ProofContext.read_const: allow for type constraint (for fixed variable);
wenzelm
parents:
36503
diff
changeset

524 
Free (x, infer_type ctxt (x, ty))) 
35399
3881972fcfca
clarified ProofContext.read_const(_proper)/Args.const(_proper) wrt. strict logical consts;
wenzelm
parents:
35360
diff
changeset

525 
 _ => prep_const_proper ctxt strict (c, pos)) 
27821  526 
end; 
527 

528 
end; 

25328  529 

530 

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

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

532 

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

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

534 

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

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

536 
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

537 
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

538 

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

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

540 

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

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

542 
prep_arity (fn ctxt => #1 o dest_Type o read_type_name_proper ctxt 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

543 

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

544 
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

545 

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

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

547 

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

548 

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

549 
(* skolem variables *) 
cc5ac538f991
eliminated odd objectoriented type_context/term_context;
wenzelm
parents:
42242
diff
changeset

550 

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

551 
fun intern_skolem ctxt x = 
cc5ac538f991
eliminated odd objectoriented type_context/term_context;
wenzelm
parents:
42242
diff
changeset

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

553 
val _ = no_skolem false x; 
42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42469
diff
changeset

554 
val sko = Variable.lookup_fixed ctxt x; 
42250
cc5ac538f991
eliminated odd objectoriented type_context/term_context;
wenzelm
parents:
42242
diff
changeset

555 
val is_const = can (read_const_proper ctxt false) x orelse Long_Name.is_qualified x; 
cc5ac538f991
eliminated odd objectoriented type_context/term_context;
wenzelm
parents:
42242
diff
changeset

556 
val is_declared = is_some (Variable.def_type ctxt false (x, ~1)); 
cc5ac538f991
eliminated odd objectoriented type_context/term_context;
wenzelm
parents:
42242
diff
changeset

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

558 
if Variable.is_const ctxt x then NONE 
cc5ac538f991
eliminated odd objectoriented type_context/term_context;
wenzelm
parents:
42242
diff
changeset

559 
else if is_some sko then sko 
cc5ac538f991
eliminated odd objectoriented type_context/term_context;
wenzelm
parents:
42242
diff
changeset

560 
else if not is_const orelse is_declared then SOME x 
cc5ac538f991
eliminated odd objectoriented type_context/term_context;
wenzelm
parents:
42242
diff
changeset

561 
else NONE 
cc5ac538f991
eliminated odd objectoriented type_context/term_context;
wenzelm
parents:
42242
diff
changeset

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

563 

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

564 

24684  565 
(* read_term *) 
566 

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

568 

569 
val read_term_pattern = read_term_mode mode_pattern; 

570 
val read_term_schematic = read_term_mode mode_schematic; 

571 
val read_term_abbrev = read_term_mode mode_abbrev; 

572 

573 

19001  574 
(* local abbreviations *) 
5819  575 

24501  576 
local 
577 

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

578 
fun certify_consts ctxt = Consts.certify (Context.pretty ctxt) (tsig_of ctxt) 
27286  579 
(not (abbrev_mode ctxt)) (consts_of ctxt); 
19001  580 

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

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

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

583 
val Mode {pattern, schematic, ...} = get_mode ctxt; 
5819  584 

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

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

586 
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

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

588 
 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

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

590 
in 
24495  591 
if pattern then I 
592 
else Variable.expand_binds ctxt #> (if schematic then I else tap reject_schematic) 

593 
end; 

5819  594 

24501  595 
in 
596 

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

598 

599 
end; 

600 

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

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

602 
val show_abbrevs = Config.bool show_abbrevs_raw; 
5819  603 

24922  604 
fun contract_abbrevs ctxt t = 
605 
let 

606 
val thy = theory_of ctxt; 

607 
val consts = consts_of ctxt; 

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

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

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

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

612 
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

613 
else Pattern.rewrite_term_top thy [] [match_abbrev] t 
24922  614 
end; 
615 

616 

24518  617 
(* patterns *) 
618 

32003  619 
fun prepare_patternT ctxt T = 
620 
let 

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

622 
val _ = 

623 
pattern orelse schematic orelse 

624 
T > Term.exists_subtype 

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

625 
(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

626 
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

627 
error ("Illegal schematic type variable: " ^ Syntax.string_of_typ ctxt T) 
32003  628 
 _ => false) 
629 
in T end; 

24518  630 

22712  631 

24505  632 
local 
6550  633 

42360  634 
val dummies = Config.bool (Config.declare "Proof_Context.dummies" (K (Config.Bool false))); 
27259  635 

636 
fun check_dummies ctxt t = 

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

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

24767  640 
fun prepare_dummies ts = #1 (fold_map Term.replace_dummy_patterns ts 1); 
6762  641 

27259  642 
in 
6550  643 

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

644 
val allow_dummies = Config.put dummies true; 
24505  645 

24684  646 
fun prepare_patterns ctxt = 
24518  647 
let val Mode {pattern, ...} = get_mode ctxt in 
39296  648 
Type_Infer.fixate ctxt #> 
24767  649 
pattern ? Variable.polymorphic ctxt #> 
24684  650 
(map o Term.map_types) (prepare_patternT ctxt) #> 
27259  651 
(if pattern then prepare_dummies else map (check_dummies ctxt)) 
24505  652 
end; 
653 

654 
end; 

655 

6550  656 

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

657 
(* sort constraints *) 
27286  658 

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

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

660 

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

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

663 
val tsig = tsig_of ctxt; 
45453  664 
val defaultS = Type.defaultS tsig; 
27286  665 

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

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

667 

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

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

669 
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

670 
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

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

672 
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

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

674 
error ("Inconsistent sort constraints for type variable " ^ 
49691  675 
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

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

677 

45453  678 
val env = 
679 
(fold o fold_atyps) 

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

681 
 TVar v => constraint v 

682 
 _ => I) tys Vartab.empty; 

36152  683 

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

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

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

686 
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

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

688 
(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

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

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

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

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

693 
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

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

695 
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

696 
" 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

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

698 

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

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

700 
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

701 
(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

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

703 

49691  704 
fun get_sort_reports xi raw_S = 
705 
let 

706 
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

707 
val S = get_sort xi raw_S handle ERROR msg => error (msg ^ Position.here_list ps); 
49691  708 
in fold (add_report S) ps end; 
49674
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 
val reports = 
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

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

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

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

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

715 
(case T of 
49691  716 
TFree (x, raw_S) => get_sort_reports (x, ~1) raw_S 
717 
 TVar (xi, raw_S) => get_sort_reports xi raw_S 

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

718 
 _ => I)) tys []; 
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 
in (implode (map #2 reports), get_sort) end; 
27286  721 

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

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

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

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

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

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

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

728 
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

729 
 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

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

731 

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

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

733 

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

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

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

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

737 

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

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

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

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

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

742 
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

743 

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

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

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

746 
val (sorting_report, [TFree a]) = prepare_sortsT ctxt [TFree v]; 
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

747 
val _ = Context_Position.if_visible ctxt Output.report sorting_report; 
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48992
diff
changeset

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

749 

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

750 
end; 
36152  751 

5819  752 

753 
(* certify terms *) 

754 

10554  755 
local 
756 

24684  757 
fun gen_cert prop ctxt t = 
758 
t 

759 
> expand_abbrevs ctxt 

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

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

761 
#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

762 
handle TYPE (msg, _, _) => error msg  TERM (msg, _) => error msg); 
16501  763 

10554  764 
in 
8096  765 

24684  766 
val cert_term = gen_cert false; 
767 
val cert_prop = gen_cert true; 

10554  768 

769 
end; 

5819  770 

771 

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

772 
(* check/uncheck *) 
22701  773 

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

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

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

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

777 

24518  778 
fun standard_typ_check ctxt = 
45429  779 
map (cert_typ_mode (Type.get_mode ctxt) ctxt #> prepare_patternT ctxt); 
24922  780 

45429  781 
val standard_term_check_finish = prepare_patterns; 
24518  782 

45429  783 
fun standard_term_uncheck ctxt = map (contract_abbrevs ctxt); 
22701  784 

785 

9553  786 

21610  787 
(** export results **) 
21531  788 

20310  789 
fun common_export is_goal inner outer = 
790 
map (Assumption.export is_goal inner outer) #> 

791 
Variable.export inner outer; 

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

792 

20310  793 
val goal_export = common_export true; 
794 
val export = common_export false; 

12704  795 

21531  796 
fun export_morphism inner outer = 
797 
Assumption.export_morphism inner outer $> 

798 
Variable.export_morphism inner outer; 

799 

28396  800 
fun norm_export_morphism inner outer = 
801 
export_morphism inner outer $> 

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

802 
Morphism.thm_morphism "Proof_Context.norm_export" (Goal.norm_result outer); 
28396  803 

21531  804 

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

805 

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

806 
(** term bindings **) 
5819  807 

8096  808 
(* simult_matches *) 
809 

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

812 
NONE => error "Pattern match failed!" 

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

815 

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

816 
(* bind_terms *) 
7925  817 

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

818 
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

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

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

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

822 

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

823 
(* auto_bind *) 
10810  824 

20330  825 
fun drop_schematic (b as (xi, SOME t)) = if Term.exists_subterm is_Var t then (xi, NONE) else b 
10554  826 
 drop_schematic b = b; 
827 

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

828 
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

829 

33386  830 
val auto_bind_goal = auto_bind Auto_Bind.goal; 
831 
val auto_bind_facts = auto_bind Auto_Bind.facts; 

7925  832 

5819  833 

8096  834 
(* match_bind(_i) *) 
5819  835 

8096  836 
local 
837 

24684  838 
fun gen_bind prep_terms gen raw_binds ctxt = 
5819  839 
let 
24684  840 
fun prep_bind (raw_pats, t) ctxt1 = 
841 
let 

842 
val T = Term.fastype_of t; 

843 
val ctxt2 = Variable.declare_term t ctxt1; 

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

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

846 
in (binds, ctxt2) end; 

7670  847 

24686  848 
val ts = prep_terms ctxt dummyT (map snd raw_binds); 
849 
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

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

851 
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

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

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

857 
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

858 
else ctxt' > bind_terms binds''); 
18310  859 
in (ts, ctxt'') end; 
8096  860 

861 
in 

5935  862 

24684  863 
fun read_terms ctxt T = 
39288  864 
map (Syntax.parse_term ctxt #> Type.constraint T) #> Syntax.check_terms ctxt; 
24684  865 

866 
val match_bind = gen_bind read_terms; 

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

8096  868 

869 
end; 

5935  870 

871 

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

872 
(* propositions with patterns *) 
5935  873 

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

874 
local 
8096  875 

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

877 
let 
19585  878 
fun prep (_, raw_pats) (ctxt, prop :: props) = 
24684  879 
let val ctxt' = Variable.declare_term prop ctxt 
880 
in ((prop, prep_props (set_mode mode_pattern ctxt') raw_pats), (ctxt', props)) end; 

881 

45327  882 
val (propp, (context', _)) = 
883 
(fold_map o fold_map) prep args 

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

885 
in (propp, context') end; 

5935  886 

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

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

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

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

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

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

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

898 

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

901 
val read_propp_schematic = prep_propp mode_schematic Syntax.read_props; 

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

10554  903 

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

906 
val bind_propp_schematic = gen_bind_propp mode_schematic Syntax.read_props; 

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

6789  908 

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

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

910 

6789  911 

5819  912 

913 
(** theorems **) 

914 

18042  915 
(* fact_tac *) 
916 

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

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

918 

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

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

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

921 
(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

922 

27867  923 
fun comp_incr_tac [] _ = no_tac 
924 
 comp_incr_tac (th :: ths) i = 

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

925 
(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

926 

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

927 
in 
18042  928 

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

929 
fun fact_tac ctxt facts = Goal.norm_hhf_tac ctxt THEN' comp_incr_tac facts; 
18122  930 

27867  931 
fun potential_facts ctxt prop = 
932 
Facts.could_unify (facts_of ctxt) (Term.strip_all_body prop); 

933 

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

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

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

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

937 

18042  938 

6091  939 
(* get_thm(s) *) 
5819  940 

26361  941 
local 
942 

26687  943 
fun retrieve_thms pick ctxt (Facts.Fact s) = 
16501  944 
let 
46849  945 
val pos = Syntax.read_token_pos s; 
42502  946 
val prop = 
947 
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

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

42502  951 
val (prop', _) = Term.replace_dummy_patterns prop (Variable.maxidx_of ctxt + 1); 
27867  952 
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

953 
Goal.prove ctxt [] [] prop' (K (ALLGOALS (fact_tac ctxt [th]))); 
42502  954 
val results = map_filter (try prove_fact) (potential_facts ctxt prop'); 
27867  955 
val res = 
42502  956 
(case distinct Thm.eq_thm_prop results of 
957 
[res] => res 

958 
 [] => err "Failed to retrieve literal fact" 

959 
 _ => err "Ambiguous specification of literal fact"); 

55740  960 
in pick ("", Position.none) [res] end 
26687  961 
 retrieve_thms pick ctxt xthmref = 
18042  962 
let 
963 
val thy = theory_of ctxt; 

26284  964 
val local_facts = facts_of ctxt; 
26673  965 
val thmref = Facts.map_name_of_ref (Facts.intern local_facts) xthmref; 
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26321
diff
changeset

966 
val name = Facts.name_of_ref thmref; 
27821  967 
val pos = Facts.pos_of_ref xthmref; 
24012  968 
val thms = 
969 
if name = "" then [Thm.transfer thy Drule.dummy_thm] 

970 
else 

26393  971 
(case Facts.lookup (Context.Proof ctxt) local_facts name of 
39507
839873937ddd
tuned signature of (Context_)Position.report variants;
wenzelm
parents:
39441
diff
changeset

972 
SOME (_, ths) => 
42378  973 
(Context_Position.report ctxt pos 
42379  974 
(Name_Space.markup (Facts.space_of local_facts) name); 
42378  975 
map (Thm.transfer thy) (Facts.select thmref ths)) 
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

976 
 NONE => Global_Theory.get_fact (Context.Proof ctxt) thy xthmref); 
55740  977 
in pick (name, pos) thms end; 
5819  978 

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

980 

26687  981 
val get_fact = retrieve_thms (K I); 
982 
val get_fact_single = retrieve_thms Facts.the_single; 

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

983 

26361  984 
fun get_thms ctxt = get_fact ctxt o Facts.named; 
985 
fun get_thm ctxt = get_fact_single ctxt o Facts.named; 

986 

987 
end; 

5819  988 

989 

26284  990 
(* facts *) 
5819  991 

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

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

993 

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

5819  997 

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

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

999 

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

1000 
fun note_thmss kind = fold_map (fn ((b, more_atts), raw_facts) => fn ctxt => 
5819  1001 
let 
28965  1002 
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

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

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

1005 
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

1006 
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

1007 
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

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

49747  1011 
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

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

1017 

12711  1018 
end; 
9196  1019 

5819  1020 

1021 

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

1023 

8096  1024 
(* variables *) 
1025 

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

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

1027 
let val T = (case opt_T of SOME T => T  NONE => Mixfix.mixfixT mx) 
20163  1028 
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

1029 

10381  1030 
local 
1031 

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

1032 
fun prep_vars prep_typ internal = 
35129  1033 
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

1034 
let 
42494  1035 
val x = Variable.check_name b; 
50239  1036 
val _ = Symbol_Pos.is_identifier (no_skolem internal x) orelse 
42381
309ec68442c6
added Binding.print convenience, which includes quote already;
wenzelm
parents:
42379
diff
changeset

1037 
error ("Illegal variable name: " ^ Binding.print b); 
12504  1038 

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

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

1040 
if internal then T 
18678  1041 
else Type.no_tvars T handle TYPE (msg, _, _) => error msg; 
24277  1042 
val opt_T = Option.map (cond_tvars o cert_typ ctxt o prep_typ ctxt) raw_T; 
35129  1043 
val (_, ctxt') = ctxt > declare_var (x, opt_T, mx); 
1044 
in ((b, opt_T, mx), ctxt') end); 

8096  1045 

10381  1046 
in 
1047 

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

1048 
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

1049 
val cert_vars = prep_vars (K I) true; 
8096  1050 

10381  1051 
end; 
1052 

8096  1053 

21744  1054 
(* notation *) 
1055 

24949  1056 
local 
1057 

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

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

1059 
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

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

1061 

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

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

1065 
SOME T => SOME (Local_Syntax.Const, (Lexicon.mark_const c, T, mx)) 
35255  1066 
 NONE => NONE) 
24949  1067 
 const_syntax _ _ = NONE; 
1068 

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

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

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

1071 
(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

1072 

24949  1073 
in 
21744  1074 

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

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

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

1077 

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

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

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

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

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

1083 
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

1084 
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

1085 
in Context.mapping (Sign.type_notation add mode args') (type_notation add mode args') end; 
24949  1086 

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

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

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

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

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

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

1095 

35680  1096 

1097 
(* aliases *) 

1098 

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

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

1103 

24767  1104 
(* local constants *) 
1105 

1106 
fun add_const_constraint (c, opt_T) ctxt = 

1107 
let 

1108 
fun prepT raw_T = 

1109 
let val T = cert_typ ctxt raw_T 

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

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

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

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

1115 
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

1116 
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

1117 
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

1118 
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

1119 
> Consts.abbreviate (Context.Proof ctxt) (tsig_of ctxt) mode (b, t); 
19001  1120 
in 
1121 
ctxt 

25039  1122 
> (map_consts o apfst) (K consts') 
21803  1123 
> Variable.declare_term rhs 
1124 
> pair (lhs, rhs) 

21704  1125 
end; 
19001  1126 

25052  1127 
fun revert_abbrev mode c = (map_consts o apfst) (Consts.revert_abbrev mode c); 
1128 

47275  1129 
fun generic_add_abbrev mode arg = 
1130 
Context.mapping_result (Sign.add_abbrev mode arg) (add_abbrev mode arg); 

1131 

1132 
fun generic_revert_abbrev mode arg = 

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

1134 

19001  1135 

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

1136 
(* fixes *) 
5819  1137 

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

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

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

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

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

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

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

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

1146 
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

1147 
#> (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

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

1149 
end; 
5819  1150 

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

1151 

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

1152 

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

1153 
(** assumptions **) 
18187  1154 

20209  1155 
local 
1156 

1157 
fun gen_assms prepp exp args ctxt = 

1158 
let 

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

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

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

1162 
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

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

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

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

1166 
> 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

1167 
end; 
20209  1168 

1169 
in 

1170 

45327  1171 
val add_assms = gen_assms bind_propp; 
1172 
val add_assms_i = gen_assms bind_propp_i; 

20209  1173 

1174 
end; 

1175 

1176 

5819  1177 

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

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

1179 

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

1180 
fun dest_cases ctxt = 
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

1181 
Symtab.fold (fn (a, (c, i)) => cons (i, (a, c))) (#2 (cases_of ctxt)) [] 
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

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

1183 

16147  1184 
local 
1185 

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

1186 
fun update_case _ _ ("", _) res = res 
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

1187 
 update_case _ _ (name, NONE) ((space, tab), index) = 
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

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

1189 
val tab' = Symtab.delete_safe name tab; 
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

1190 
in ((space, tab'), index) end 
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

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

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

1193 
val (_, cases') = cases > Name_Space.define context false 
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

1194 
(Binding.make (name, Position.none), ((c, is_proper), index)); 
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

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

1196 
in (cases', index') end; 
18609  1197 

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

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

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

1200 
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

1201 

16147  1202 
in 
1203 

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

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

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

1206 
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

1207 
val cases = cases_of ctxt; 
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

1208 
val index = Symtab.fold (fn _ => Integer.add 1) (#2 cases) 0; 
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

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

1210 
in map_cases (K cases') ctxt end; 
18609  1211 

1212 
fun case_result c ctxt = 

1213 
let 

33368  1214 
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

1215 
val (ts, ctxt') = ctxt > fold_map fix fixes; 
33368  1216 
val Rule_Cases.Case {assumes, binds, cases, ...} = Rule_Cases.apply ts c; 
18609  1217 
in 
1218 
ctxt' 

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

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

1220 
> update_cases true (map (apsnd SOME) cases) 
18609  1221 
> pair (assumes, (binds, cases)) 
1222 
end; 

1223 

1224 
val apply_case = apfst fst oo case_result; 

1225 

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

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

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

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

1229 
Name_Space.check (Context.Proof ctxt) (cases_of ctxt) (name, pos); 
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
52223
diff
changeset

1230 

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

1231 
fun replace (opt_x :: xs) ((y, T) :: ys) = (the_default y opt_x, T) :: replace xs ys 