author  wenzelm 
Tue, 03 Apr 2012 16:27:32 +0200  
changeset 47292  1884d34e9aab 
parent 47291  6a641856a0e9 
child 47293  052cd5f1a591 
permissions  rwrr 
41959  1 
(* Title: Pure/Isar/generic_target.ML 
38309  2 
Author: Makarius 
3 
Author: Florian Haftmann, TU Muenchen 

4 

5 
Common target infrastructure. 

6 
*) 

7 

8 
signature GENERIC_TARGET = 

9 
sig 

40782  10 
val define: (((binding * typ) * mixfix) * (binding * term) > 
11 
term list * term list > local_theory > (term * thm) * local_theory) > 

46992
eeea81b86b70
refined Local_Theory.define vs. Local_Theory.define_internal, which allows to pass alternative name to the foundational axiom  expecially important for 'instantiation' or 'overloading', which loose name information due to Long_Name.base_name cooking etc.;
wenzelm
parents:
46916
diff
changeset

12 
bool > (binding * mixfix) * (Attrib.binding * term) > local_theory > 
40782  13 
(term * (string * thm)) * local_theory 
47250
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset

14 
val notes: 
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset

15 
(string > (Attrib.binding * (thm list * Args.src list) list) list > 
40782  16 
(Attrib.binding * (thm list * Args.src list) list) list > local_theory > local_theory) > 
17 
string > (Attrib.binding * (thm list * Args.src list) list) list > local_theory > 

18 
(string * thm list) list * local_theory 

47250
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset

19 
val locale_notes: string > string > 
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset

20 
(Attrib.binding * (thm list * Args.src list) list) list > 
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset

21 
(Attrib.binding * (thm list * Args.src list) list) list > 
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset

22 
local_theory > local_theory 
40782  23 
val abbrev: (string * bool > binding * mixfix > term * term > 
24 
term list > local_theory > local_theory) > 

47250
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset

25 
string * bool > (binding * mixfix) * term > local_theory > (term * term) * local_theory 
47081
5e70b457b704
uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
wenzelm
parents:
47080
diff
changeset

26 
val background_declaration: declaration > local_theory > local_theory 
47280  27 
val locale_declaration: string > bool > declaration > local_theory > local_theory 
47282  28 
val standard_declaration: (int > bool) > declaration > local_theory > local_theory 
29 
val generic_const: bool > Syntax.mode > (binding * mixfix) * term > 

30 
Context.generic > Context.generic 

31 
val const_declaration: (int > bool) > Syntax.mode > (binding * mixfix) * term > 

32 
local_theory > local_theory 

47284
0e65b6a016dc
clarified background_foundation vs. theory_foundation (with const_declaration);
wenzelm
parents:
47283
diff
changeset

33 
val background_foundation: ((binding * typ) * mixfix) * (binding * term) > 
0e65b6a016dc
clarified background_foundation vs. theory_foundation (with const_declaration);
wenzelm
parents:
47283
diff
changeset

34 
term list * term list > local_theory > (term * thm) * local_theory 
40782  35 
val theory_foundation: ((binding * typ) * mixfix) * (binding * term) > 
36 
term list * term list > local_theory > (term * thm) * local_theory 

47250
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset

37 
val theory_notes: string > 
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset

38 
(Attrib.binding * (thm list * Args.src list) list) list > 
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset

39 
(Attrib.binding * (thm list * Args.src list) list) list > 
40782  40 
local_theory > local_theory 
47286
392c4cd97e5c
more uniform theory_abbrev with const_declaration;
wenzelm
parents:
47285
diff
changeset

41 
val theory_abbrev: Syntax.mode > (binding * mixfix) > term * term > term list > 
392c4cd97e5c
more uniform theory_abbrev with const_declaration;
wenzelm
parents:
47285
diff
changeset

42 
local_theory > local_theory 
47279
4bab649dedf0
clarified standard_declaration vs. theory_declaration;
wenzelm
parents:
47276
diff
changeset

43 
val theory_declaration: declaration > local_theory > local_theory 
45353  44 
end 
38309  45 

46 
structure Generic_Target: GENERIC_TARGET = 

47 
struct 

48 

38341
72dba5bd5f63
moved theorylevel target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38315
diff
changeset

49 
(** lifting primitive to target operations **) 
72dba5bd5f63
moved theorylevel target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38315
diff
changeset

50 

38312
9dd57db3c0f2
moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents:
38311
diff
changeset

51 
(* mixfix syntax *) 
9dd57db3c0f2
moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents:
38311
diff
changeset

52 

9dd57db3c0f2
moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents:
38311
diff
changeset

53 
fun check_mixfix ctxt (b, extra_tfrees) mx = 
9dd57db3c0f2
moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents:
38311
diff
changeset

54 
if null extra_tfrees then mx 
9dd57db3c0f2
moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents:
38311
diff
changeset

55 
else 
38831
4933a3dfd745
more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents:
38757
diff
changeset

56 
(Context_Position.if_visible ctxt warning 
42381
309ec68442c6
added Binding.print convenience, which includes quote already;
wenzelm
parents:
42375
diff
changeset

57 
("Additional type variable(s) in specification of " ^ Binding.print b ^ ": " ^ 
38312
9dd57db3c0f2
moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents:
38311
diff
changeset

58 
commas (map (Syntax.string_of_typ ctxt o TFree) (sort_wrt #1 extra_tfrees)) ^ 
9dd57db3c0f2
moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents:
38311
diff
changeset

59 
(if mx = NoSyn then "" 
42287
d98eb048a2e4
discontinued special treatment of structure Mixfix;
wenzelm
parents:
41959
diff
changeset

60 
else "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx))); 
38312
9dd57db3c0f2
moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents:
38311
diff
changeset

61 
NoSyn); 
9dd57db3c0f2
moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents:
38311
diff
changeset

62 

47291
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
47290
diff
changeset

63 
fun check_mixfix_global (b, no_params) mx = 
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
47290
diff
changeset

64 
if no_params orelse mx = NoSyn then mx 
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
47290
diff
changeset

65 
else (warning ("Dropping global mixfix syntax: " ^ Binding.print b ^ " " ^ 
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
47290
diff
changeset

66 
Pretty.string_of (Mixfix.pretty_mixfix mx)); NoSyn); 
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
47290
diff
changeset

67 

38312
9dd57db3c0f2
moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents:
38311
diff
changeset

68 

38309  69 
(* define *) 
70 

46992
eeea81b86b70
refined Local_Theory.define vs. Local_Theory.define_internal, which allows to pass alternative name to the foundational axiom  expecially important for 'instantiation' or 'overloading', which loose name information due to Long_Name.base_name cooking etc.;
wenzelm
parents:
46916
diff
changeset

71 
fun define foundation internal ((b, mx), ((b_def, atts), rhs)) lthy = 
38309  72 
let 
42360  73 
val thy = Proof_Context.theory_of lthy; 
74 
val thy_ctxt = Proof_Context.init_global thy; 

38309  75 

76 
(*term and type parameters*) 

47276  77 
val ((defs, _), rhs') = Thm.cterm_of thy rhs 
78 
> Local_Defs.export_cterm lthy thy_ctxt > Thm.term_of; 

38309  79 

47272
ca31cfa509b1
refined define/abbrev: allow extra fixes in aux. context vs. bottom target (NB: export_term expands defined variables, leaving fixed ones);
wenzelm
parents:
47250
diff
changeset

80 
val xs = Variable.add_fixed lthy rhs' []; 
38309  81 
val T = Term.fastype_of rhs; 
82 
val tfreesT = Term.add_tfreesT T (fold (Term.add_tfreesT o #2) xs []); 

83 
val extra_tfrees = rev (subtract (op =) tfreesT (Term.add_tfrees rhs [])); 

38312
9dd57db3c0f2
moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents:
38311
diff
changeset

84 
val mx' = check_mixfix lthy (b, extra_tfrees) mx; 
38309  85 

86 
val type_params = map (Logic.mk_type o TFree) extra_tfrees; 

47272
ca31cfa509b1
refined define/abbrev: allow extra fixes in aux. context vs. bottom target (NB: export_term expands defined variables, leaving fixed ones);
wenzelm
parents:
47250
diff
changeset

87 
val term_params = map Free (sort (Variable.fixed_ord lthy o pairself #1) xs); 
38309  88 
val params = type_params @ term_params; 
89 

90 
val U = map Term.fastype_of params > T; 

91 

92 
(*foundation*) 

45353  93 
val ((lhs', global_def), lthy2) = lthy 
94 
> foundation (((b, U), mx'), (b_def, rhs')) (type_params, term_params); 

38309  95 

96 
(*local definition*) 

38315  97 
val ((lhs, local_def), lthy3) = lthy2 
38309  98 
> Local_Defs.add_def ((b, NoSyn), lhs'); 
47240  99 

100 
(*result*) 

47238  101 
val def = 
47240  102 
Thm.transitive local_def global_def 
103 
> Local_Defs.contract defs 

104 
(Thm.cterm_of (Proof_Context.theory_of lthy3) (Logic.mk_equals (lhs, rhs))); 

38315  105 
val ([(res_name, [res])], lthy4) = lthy3 
47080  106 
> Local_Theory.notes [((if internal then Binding.empty else b_def, atts), [([def], [])])]; 
38315  107 
in ((lhs, (res_name, res)), lthy4) end; 
38309  108 

109 

110 
(* notes *) 

111 

47250
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset

112 
local 
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset

113 

38309  114 
fun import_export_proof ctxt (name, raw_th) = 
115 
let 

42360  116 
val thy = Proof_Context.theory_of ctxt; 
117 
val thy_ctxt = Proof_Context.init_global thy; 

38309  118 
val certT = Thm.ctyp_of thy; 
119 
val cert = Thm.cterm_of thy; 

120 

121 
(*export assumes/defines*) 

122 
val th = Goal.norm_result raw_th; 

45407
a83574606719
more specific treatment of defines/assumes  avoid normalizing defs by themselves (NB: locale specifications and Local_Theory.define may lead to arbitrary mixture);
wenzelm
parents:
45390
diff
changeset

123 
val ((defs, asms), th') = Local_Defs.export ctxt thy_ctxt th; 
a83574606719
more specific treatment of defines/assumes  avoid normalizing defs by themselves (NB: locale specifications and Local_Theory.define may lead to arbitrary mixture);
wenzelm
parents:
45390
diff
changeset

124 
val asms' = map (Raw_Simplifier.rewrite_rule defs) asms; 
38309  125 

126 
(*export fixes*) 

127 
val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []); 

128 
val frees = map Free (Thm.fold_terms Term.add_frees th' []); 

45352  129 
val (th'' :: vs) = 
130 
(th' :: map (Drule.mk_term o cert) (map Logic.mk_type tfrees @ frees)) 

38309  131 
> Variable.export ctxt thy_ctxt 
132 
> Drule.zero_var_indexes_list; 

133 

134 
(*thm definition*) 

45413
117ff038f8f7
disabled Thm.compress (again)  costs for building tables tend to be higher than potential benefit;
wenzelm
parents:
45407
diff
changeset

135 
val result = Global_Theory.name_thm true true name th''; 
38309  136 

137 
(*import fixes*) 

138 
val (tvars, vars) = 

139 
chop (length tfrees) (map (Thm.term_of o Drule.dest_term) vs) 

140 
>> map Logic.dest_type; 

141 

142 
val instT = map_filter (fn (TVar v, T) => SOME (v, T)  _ => NONE) (tvars ~~ tfrees); 

143 
val inst = filter (is_Var o fst) (vars ~~ frees); 

144 
val cinstT = map (pairself certT o apfst TVar) instT; 

145 
val cinst = map (pairself (cert o Term.map_types (Term_Subst.instantiateT instT))) inst; 

146 
val result' = Thm.instantiate (cinstT, cinst) result; 

147 

148 
(*import assumes/defines*) 

149 
val result'' = 

45407
a83574606719
more specific treatment of defines/assumes  avoid normalizing defs by themselves (NB: locale specifications and Local_Theory.define may lead to arbitrary mixture);
wenzelm
parents:
45390
diff
changeset

150 
(fold (curry op COMP) asms' result' 
a83574606719
more specific treatment of defines/assumes  avoid normalizing defs by themselves (NB: locale specifications and Local_Theory.define may lead to arbitrary mixture);
wenzelm
parents:
45390
diff
changeset

151 
handle THM _ => raise THM ("Failed to reimport result", 0, result' :: asms')) 
47238  152 
> Local_Defs.contract defs (Thm.cprop_of th) 
38309  153 
> Goal.norm_result 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
38831
diff
changeset

154 
> Global_Theory.name_thm false false name; 
38309  155 

156 
in (result'', result) end; 

157 

47250
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset

158 
fun standard_facts lthy ctxt = 
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset

159 
Element.transform_facts (Local_Theory.standard_morphism lthy ctxt); 
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset

160 

6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset

161 
in 
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset

162 

38309  163 
fun notes target_notes kind facts lthy = 
164 
let 

165 
val facts' = facts 

39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
38831
diff
changeset

166 
> map (fn (a, bs) => (a, Global_Theory.burrow_fact (Global_Theory.name_multi 
38309  167 
(Local_Theory.full_name lthy (fst a))) bs)) 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
38831
diff
changeset

168 
> Global_Theory.map_facts (import_export_proof lthy); 
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
38831
diff
changeset

169 
val local_facts = Global_Theory.map_facts #1 facts'; 
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
38831
diff
changeset

170 
val global_facts = Global_Theory.map_facts #2 facts'; 
38309  171 
in 
172 
lthy 

47250
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset

173 
> target_notes kind global_facts (Attrib.partial_evaluation lthy local_facts) 
47249
c0481c3c2a6c
added Attrib.global_notes/local_notes/generic_notes convenience;
wenzelm
parents:
47246
diff
changeset

174 
> Attrib.local_notes kind local_facts 
38309  175 
end; 
176 

47250
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset

177 
fun locale_notes locale kind global_facts local_facts = 
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset

178 
Local_Theory.background_theory 
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset

179 
(Attrib.global_notes kind (Attrib.map_facts (K []) global_facts) #> snd) #> 
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset

180 
(fn lthy => lthy > 
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset

181 
Local_Theory.target (fn ctxt => ctxt > 
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset

182 
Locale.add_thmss locale kind (standard_facts lthy ctxt local_facts))) #> 
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset

183 
(fn lthy => lthy > 
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset

184 
Local_Theory.map_contexts (fn level => fn ctxt => 
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset

185 
if level = 0 orelse level = Local_Theory.level lthy then ctxt 
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset

186 
else ctxt > Attrib.local_notes kind (standard_facts lthy ctxt local_facts) > snd)); 
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset

187 

6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset

188 
end; 
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset

189 

38309  190 

191 
(* abbrev *) 

192 

193 
fun abbrev target_abbrev prmode ((b, mx), t) lthy = 

194 
let 

42360  195 
val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy); 
38309  196 

47292
1884d34e9aab
export into target context (again), to retain its 'defines' (e.g. abbreviation lcoeff in theory HOL/Algebra/UnivPoly);
wenzelm
parents:
47291
diff
changeset

197 
val t' = Assumption.export_term lthy (Local_Theory.target_of lthy) t; 
47290  198 
val xs = map Free (sort (Variable.fixed_ord lthy o pairself #1) (Variable.add_fixed lthy t' [])); 
38309  199 
val u = fold_rev lambda xs t'; 
47290  200 
val global_rhs = singleton (Variable.polymorphic thy_ctxt) u; 
38309  201 

202 
val extra_tfrees = 

203 
subtract (op =) (Term.add_tfreesT (Term.fastype_of u) []) (Term.add_tfrees u []); 

38312
9dd57db3c0f2
moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents:
38311
diff
changeset

204 
val mx' = check_mixfix lthy (b, extra_tfrees) mx; 
38309  205 
in 
206 
lthy 

38312
9dd57db3c0f2
moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents:
38311
diff
changeset

207 
> target_abbrev prmode (b, mx') (global_rhs, t') xs 
42360  208 
> Proof_Context.add_abbrev Print_Mode.internal (b, t) > snd 
38309  209 
> Local_Defs.fixed_abbrev ((b, NoSyn), t) 
210 
end; 

211 

38341
72dba5bd5f63
moved theorylevel target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38315
diff
changeset

212 

47081
5e70b457b704
uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
wenzelm
parents:
47080
diff
changeset

213 
(* declaration *) 
5e70b457b704
uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
wenzelm
parents:
47080
diff
changeset

214 

5e70b457b704
uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
wenzelm
parents:
47080
diff
changeset

215 
fun background_declaration decl lthy = 
5e70b457b704
uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
wenzelm
parents:
47080
diff
changeset

216 
let 
5e70b457b704
uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
wenzelm
parents:
47080
diff
changeset

217 
val theory_decl = 
5e70b457b704
uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
wenzelm
parents:
47080
diff
changeset

218 
Local_Theory.standard_form lthy 
5e70b457b704
uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
wenzelm
parents:
47080
diff
changeset

219 
(Proof_Context.init_global (Proof_Context.theory_of lthy)) decl; 
5e70b457b704
uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
wenzelm
parents:
47080
diff
changeset

220 
in Local_Theory.background_theory (Context.theory_map theory_decl) lthy end; 
5e70b457b704
uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
wenzelm
parents:
47080
diff
changeset

221 

47246
2bbab021c0e6
clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents:
47245
diff
changeset

222 
fun locale_declaration locale syntax decl lthy = lthy 
2bbab021c0e6
clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents:
47245
diff
changeset

223 
> Local_Theory.target (fn ctxt => ctxt > 
2bbab021c0e6
clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents:
47245
diff
changeset

224 
Locale.add_declaration locale syntax 
2bbab021c0e6
clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents:
47245
diff
changeset

225 
(Morphism.transform (Local_Theory.standard_morphism lthy ctxt) decl)); 
2bbab021c0e6
clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents:
47245
diff
changeset

226 

47282  227 
fun standard_declaration pred decl lthy = 
228 
Local_Theory.map_contexts (fn level => fn ctxt => 

229 
if pred level then Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt 

230 
else ctxt) lthy; 

231 

232 

233 
(* const declaration *) 

234 

235 
fun generic_const same_shape prmode ((b, mx), t) context = 

236 
let 

237 
val const_alias = 

238 
if same_shape then 

239 
(case t of 

240 
Const (c, T) => 

241 
let 

242 
val thy = Context.theory_of context; 

243 
val ctxt = Context.proof_of context; 

244 
in 

47291
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
47290
diff
changeset

245 
(case Type_Infer_Context.const_type ctxt c of 
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
47290
diff
changeset

246 
SOME T' => if Sign.typ_equiv thy (T, T') then SOME c else NONE 
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
47290
diff
changeset

247 
 NONE => NONE) 
47282  248 
end 
249 
 _ => NONE) 

250 
else NONE; 

251 
in 

252 
(case const_alias of 

253 
SOME c => 

254 
context 

255 
> Context.mapping (Sign.const_alias b c) (Proof_Context.const_alias b c) 

256 
> Morphism.form (Proof_Context.generic_notation true prmode [(t, mx)]) 

257 
 NONE => 

258 
context 

47288
b79bf8288b29
clarified generic_const vs. close_schematic_term;
wenzelm
parents:
47286
diff
changeset

259 
> Proof_Context.generic_add_abbrev Print_Mode.internal (b, Term.close_schematic_term t) 
47282  260 
> (fn (const as Const (c, _), _) => same_shape ? 
261 
(Proof_Context.generic_revert_abbrev (#1 prmode) c #> 

262 
Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)])))) 

263 
end; 

264 

265 
fun const_declaration pred prmode ((b, mx), rhs) = 

266 
standard_declaration pred (fn phi => 

267 
let 

268 
val b' = Morphism.binding phi b; 

269 
val rhs' = Morphism.term phi rhs; 

270 
val same_shape = Term.aconv_untyped (rhs, rhs'); 

47288
b79bf8288b29
clarified generic_const vs. close_schematic_term;
wenzelm
parents:
47286
diff
changeset

271 
in generic_const same_shape prmode ((b', mx), rhs') end); 
47280  272 

47081
5e70b457b704
uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
wenzelm
parents:
47080
diff
changeset

273 

45352  274 

38341
72dba5bd5f63
moved theorylevel target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38315
diff
changeset

275 
(** primitive theory operations **) 
72dba5bd5f63
moved theorylevel target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38315
diff
changeset

276 

47284
0e65b6a016dc
clarified background_foundation vs. theory_foundation (with const_declaration);
wenzelm
parents:
47283
diff
changeset

277 
fun background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy = 
38341
72dba5bd5f63
moved theorylevel target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38315
diff
changeset

278 
let 
47291
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
47290
diff
changeset

279 
val params = type_params @ term_params; 
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
47290
diff
changeset

280 
val mx' = check_mixfix_global (b, null params) mx; 
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
47290
diff
changeset

281 

42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42360
diff
changeset

282 
val (const, lthy2) = lthy 
47291
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
47290
diff
changeset

283 
> Local_Theory.background_theory_result (Sign.declare_const lthy ((b, U), mx')); 
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
47290
diff
changeset

284 
val lhs = Term.list_comb (const, params); 
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
47290
diff
changeset

285 

42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42360
diff
changeset

286 
val ((_, def), lthy3) = lthy2 
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42360
diff
changeset

287 
> Local_Theory.background_theory_result 
46916
e7ea35b41e2d
Local_Theory.define no longer hardwires default theorem name  targets/packages need to take care of it;
wenzelm
parents:
45413
diff
changeset

288 
(Thm.add_def lthy2 false false 
e7ea35b41e2d
Local_Theory.define no longer hardwires default theorem name  targets/packages need to take care of it;
wenzelm
parents:
45413
diff
changeset

289 
(Thm.def_binding_optional b b_def, Logic.mk_equals (lhs, rhs))); 
38341
72dba5bd5f63
moved theorylevel target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38315
diff
changeset

290 
in ((lhs, def), lthy3) end; 
72dba5bd5f63
moved theorylevel target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38315
diff
changeset

291 

47284
0e65b6a016dc
clarified background_foundation vs. theory_foundation (with const_declaration);
wenzelm
parents:
47283
diff
changeset

292 
fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) = 
0e65b6a016dc
clarified background_foundation vs. theory_foundation (with const_declaration);
wenzelm
parents:
47283
diff
changeset

293 
background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) 
47285
ca4cf5de366c
avoid const_declaration in aux. context (cf. locale_foundation);
wenzelm
parents:
47284
diff
changeset

294 
#> (fn (lhs, def) => fn lthy' => lthy' > 
ca4cf5de366c
avoid const_declaration in aux. context (cf. locale_foundation);
wenzelm
parents:
47284
diff
changeset

295 
const_declaration (fn level => level <> Local_Theory.level lthy') 
ca4cf5de366c
avoid const_declaration in aux. context (cf. locale_foundation);
wenzelm
parents:
47284
diff
changeset

296 
Syntax.mode_default ((b, mx), lhs) 
ca4cf5de366c
avoid const_declaration in aux. context (cf. locale_foundation);
wenzelm
parents:
47284
diff
changeset

297 
> pair (lhs, def)); 
47284
0e65b6a016dc
clarified background_foundation vs. theory_foundation (with const_declaration);
wenzelm
parents:
47283
diff
changeset

298 

47250
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset

299 
fun theory_notes kind global_facts local_facts = 
47249
c0481c3c2a6c
added Attrib.global_notes/local_notes/generic_notes convenience;
wenzelm
parents:
47246
diff
changeset

300 
Local_Theory.background_theory (Attrib.global_notes kind global_facts #> snd) #> 
47250
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset

301 
(fn lthy => lthy > Local_Theory.map_contexts (fn level => fn ctxt => 
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset

302 
if level = Local_Theory.level lthy then ctxt 
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset

303 
else 
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset

304 
ctxt > Attrib.local_notes kind 
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset

305 
(Element.transform_facts (Local_Theory.standard_morphism lthy ctxt) local_facts) > snd)); 
38341
72dba5bd5f63
moved theorylevel target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38315
diff
changeset

306 

47286
392c4cd97e5c
more uniform theory_abbrev with const_declaration;
wenzelm
parents:
47285
diff
changeset

307 
fun theory_abbrev prmode (b, mx) (t, _) xs = 
392c4cd97e5c
more uniform theory_abbrev with const_declaration;
wenzelm
parents:
47285
diff
changeset

308 
Local_Theory.background_theory_result 
38757
2b3e054ae6fc
renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in userspace tools;
wenzelm
parents:
38341
diff
changeset

309 
(Sign.add_abbrev (#1 prmode) (b, t) #> 
47291
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
47290
diff
changeset

310 
(fn (lhs, _) => (* FIXME type_params!? *) 
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
47290
diff
changeset

311 
Sign.notation true prmode [(lhs, check_mixfix_global (b, null xs) mx)] #> pair lhs)) 
47286
392c4cd97e5c
more uniform theory_abbrev with const_declaration;
wenzelm
parents:
47285
diff
changeset

312 
#> (fn lhs => fn lthy' => lthy' > 
392c4cd97e5c
more uniform theory_abbrev with const_declaration;
wenzelm
parents:
47285
diff
changeset

313 
const_declaration (fn level => level <> Local_Theory.level lthy') prmode 
392c4cd97e5c
more uniform theory_abbrev with const_declaration;
wenzelm
parents:
47285
diff
changeset

314 
((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs))); 
38341
72dba5bd5f63
moved theorylevel target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38315
diff
changeset

315 

47279
4bab649dedf0
clarified standard_declaration vs. theory_declaration;
wenzelm
parents:
47276
diff
changeset

316 
fun theory_declaration decl = 
47282  317 
background_declaration decl #> standard_declaration (K true) decl; 
47279
4bab649dedf0
clarified standard_declaration vs. theory_declaration;
wenzelm
parents:
47276
diff
changeset

318 

38309  319 
end; 