author | wenzelm |
Fri, 06 Mar 2015 15:58:56 +0100 | |
changeset 59621 | 291934bac95e |
parent 59616 | eb59c6968219 |
child 60283 | c927fa99d045 |
permissions | -rw-r--r-- |
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 |
|
57190
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
10 |
(* consts *) |
57192
180e955711cf
yet another attempt for terminology: foo_target_bar denotes an operation bar operating solely on the target context of target foo, foo_bar denotes a whole stack of operations to accomplish bar for target foo
haftmann
parents:
57191
diff
changeset
|
11 |
val standard_const: (int * int -> bool) -> Syntax.mode -> (binding * mixfix) * term -> |
57190
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
12 |
local_theory -> local_theory |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
13 |
|
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
14 |
(* background operations *) |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
15 |
val background_foundation: ((binding * typ) * mixfix) * (binding * term) -> |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
16 |
term list * term list -> local_theory -> (term * thm) * local_theory |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
17 |
val background_declaration: declaration -> local_theory -> local_theory |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
18 |
val background_abbrev: binding * term -> term list -> local_theory -> (term * term) * local_theory |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
19 |
|
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
20 |
(* lifting primitives to local theory operations *) |
40782 | 21 |
val define: (((binding * typ) * mixfix) * (binding * term) -> |
22 |
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
|
23 |
bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory -> |
40782 | 24 |
(term * (string * thm)) * local_theory |
47250
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
25 |
val notes: |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57926
diff
changeset
|
26 |
(string -> (Attrib.binding * (thm list * Token.src list) list) list -> |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57926
diff
changeset
|
27 |
(Attrib.binding * (thm list * Token.src list) list) list -> local_theory -> local_theory) -> |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57926
diff
changeset
|
28 |
string -> (Attrib.binding * (thm list * Token.src list) list) list -> local_theory -> |
40782 | 29 |
(string * thm list) list * local_theory |
57118 | 30 |
val abbrev: (string * bool -> binding * mixfix -> term -> |
57160 | 31 |
term list * term list -> local_theory -> local_theory) -> |
47250
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
32 |
string * bool -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory |
57190
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
33 |
|
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
34 |
(* theory operations *) |
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 -> |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57926
diff
changeset
|
38 |
(Attrib.binding * (thm list * Token.src list) list) list -> |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57926
diff
changeset
|
39 |
(Attrib.binding * (thm list * Token.src list) list) list -> |
40782 | 40 |
local_theory -> local_theory |
57190
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
41 |
val theory_declaration: declaration -> local_theory -> local_theory |
57160 | 42 |
val theory_abbrev: Syntax.mode -> (binding * mixfix) -> term -> term list * term list -> |
47286
392c4cd97e5c
more uniform theory_abbrev with const_declaration;
wenzelm
parents:
47285
diff
changeset
|
43 |
local_theory -> local_theory |
52153
f5773a46cf05
more specific structure for registration into theory and dependency onto locale
haftmann
parents:
47313
diff
changeset
|
44 |
val theory_registration: string * morphism -> (morphism * bool) option -> morphism -> |
f5773a46cf05
more specific structure for registration into theory and dependency onto locale
haftmann
parents:
47313
diff
changeset
|
45 |
local_theory -> local_theory |
57190
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
46 |
|
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
47 |
(* locale operations *) |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
48 |
val locale_notes: string -> string -> |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57926
diff
changeset
|
49 |
(Attrib.binding * (thm list * Token.src list) list) list -> |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57926
diff
changeset
|
50 |
(Attrib.binding * (thm list * Token.src list) list) list -> |
57190
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
51 |
local_theory -> local_theory |
57192
180e955711cf
yet another attempt for terminology: foo_target_bar denotes an operation bar operating solely on the target context of target foo, foo_bar denotes a whole stack of operations to accomplish bar for target foo
haftmann
parents:
57191
diff
changeset
|
52 |
val locale_target_declaration: string -> bool -> declaration -> local_theory -> local_theory |
57193 | 53 |
val locale_declaration: string -> {syntax: bool, pervasive: bool} -> declaration -> |
54 |
local_theory -> local_theory |
|
57192
180e955711cf
yet another attempt for terminology: foo_target_bar denotes an operation bar operating solely on the target context of target foo, foo_bar denotes a whole stack of operations to accomplish bar for target foo
haftmann
parents:
57191
diff
changeset
|
55 |
val locale_target_const: string -> (morphism -> bool) -> Syntax.mode -> |
57190
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
56 |
(binding * mixfix) * term -> local_theory -> local_theory |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
57 |
val locale_const: string -> Syntax.mode -> (binding * mixfix) * term -> |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
58 |
local_theory -> local_theory |
52153
f5773a46cf05
more specific structure for registration into theory and dependency onto locale
haftmann
parents:
47313
diff
changeset
|
59 |
val locale_dependency: string -> string * morphism -> (morphism * bool) option -> morphism -> |
f5773a46cf05
more specific structure for registration into theory and dependency onto locale
haftmann
parents:
47313
diff
changeset
|
60 |
local_theory -> local_theory |
45353 | 61 |
end |
38309 | 62 |
|
63 |
structure Generic_Target: GENERIC_TARGET = |
|
64 |
struct |
|
65 |
||
57191 | 66 |
(** notes **) |
57190
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
67 |
|
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
68 |
fun standard_facts lthy ctxt = |
58028
e4250d370657
tuned signature -- define some elementary operations earlier;
wenzelm
parents:
58011
diff
changeset
|
69 |
Attrib.transform_facts (Local_Theory.standard_morphism lthy ctxt); |
38341
72dba5bd5f63
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38315
diff
changeset
|
70 |
|
57191 | 71 |
fun standard_notes pred kind facts lthy = |
72 |
Local_Theory.map_contexts (fn level => fn ctxt => |
|
73 |
if pred (Local_Theory.level lthy, level) |
|
74 |
then Attrib.local_notes kind (standard_facts lthy ctxt facts) ctxt |> snd |
|
75 |
else ctxt) lthy; |
|
76 |
||
77 |
||
78 |
(** declarations **) |
|
79 |
||
57190
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
80 |
fun standard_declaration pred decl lthy = |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
81 |
Local_Theory.map_contexts (fn level => fn ctxt => |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
82 |
if pred (Local_Theory.level lthy, level) |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
83 |
then Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
84 |
else ctxt) lthy; |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
85 |
|
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
86 |
|
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
87 |
(** consts **) |
38312
9dd57db3c0f2
moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents:
38311
diff
changeset
|
88 |
|
9dd57db3c0f2
moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents:
38311
diff
changeset
|
89 |
fun check_mixfix ctxt (b, extra_tfrees) mx = |
9dd57db3c0f2
moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents:
38311
diff
changeset
|
90 |
if null extra_tfrees then mx |
9dd57db3c0f2
moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents:
38311
diff
changeset
|
91 |
else |
56294
85911b8a6868
prefer Context_Position where a context is available;
wenzelm
parents:
56141
diff
changeset
|
92 |
(if Context_Position.is_visible ctxt then |
85911b8a6868
prefer Context_Position where a context is available;
wenzelm
parents:
56141
diff
changeset
|
93 |
warning |
85911b8a6868
prefer Context_Position where a context is available;
wenzelm
parents:
56141
diff
changeset
|
94 |
("Additional type variable(s) in specification of " ^ Binding.print b ^ ": " ^ |
85911b8a6868
prefer Context_Position where a context is available;
wenzelm
parents:
56141
diff
changeset
|
95 |
commas (map (Syntax.string_of_typ ctxt o TFree) (sort_wrt #1 extra_tfrees)) ^ |
85911b8a6868
prefer Context_Position where a context is available;
wenzelm
parents:
56141
diff
changeset
|
96 |
(if mx = NoSyn then "" |
85911b8a6868
prefer Context_Position where a context is available;
wenzelm
parents:
56141
diff
changeset
|
97 |
else "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx))) |
85911b8a6868
prefer Context_Position where a context is available;
wenzelm
parents:
56141
diff
changeset
|
98 |
else (); NoSyn); |
38312
9dd57db3c0f2
moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents:
38311
diff
changeset
|
99 |
|
47291
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
47290
diff
changeset
|
100 |
fun check_mixfix_global (b, no_params) mx = |
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
47290
diff
changeset
|
101 |
if no_params orelse mx = NoSyn then mx |
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
47290
diff
changeset
|
102 |
else (warning ("Dropping global mixfix syntax: " ^ Binding.print b ^ " " ^ |
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
47290
diff
changeset
|
103 |
Pretty.string_of (Mixfix.pretty_mixfix mx)); NoSyn); |
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
47290
diff
changeset
|
104 |
|
57190
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
105 |
fun const_decl phi_pred prmode ((b, mx), rhs) phi context = |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
106 |
if phi_pred phi then |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
107 |
let |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
108 |
val b' = Morphism.binding phi b; |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
109 |
val rhs' = Morphism.term phi rhs; |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
110 |
val same_shape = Term.aconv_untyped (rhs, rhs'); |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
111 |
val const_alias = |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
112 |
if same_shape then |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
113 |
(case rhs' of |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
114 |
Const (c, T) => |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
115 |
let |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
116 |
val thy = Context.theory_of context; |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
117 |
val ctxt = Context.proof_of context; |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
118 |
in |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
119 |
(case Type_Infer_Context.const_type ctxt c of |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
120 |
SOME T' => if Sign.typ_equiv thy (T, T') then SOME c else NONE |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
121 |
| NONE => NONE) |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
122 |
end |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
123 |
| _ => NONE) |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
124 |
else NONE; |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
125 |
in |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
126 |
case const_alias of |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
127 |
SOME c => |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
128 |
context |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
129 |
|> Context.mapping (Sign.const_alias b' c) (Proof_Context.const_alias b' c) |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
130 |
|> Morphism.form (Proof_Context.generic_notation true prmode [(rhs', mx)]) |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
131 |
| NONE => |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
132 |
context |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
133 |
|> Proof_Context.generic_add_abbrev Print_Mode.internal (b', Term.close_schematic_term rhs') |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
134 |
|-> (fn (const as Const (c, _), _) => same_shape ? |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
135 |
(Proof_Context.generic_revert_abbrev (#1 prmode) c #> |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
136 |
Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)]))) |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
137 |
end |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
138 |
else context; |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
139 |
|
57192
180e955711cf
yet another attempt for terminology: foo_target_bar denotes an operation bar operating solely on the target context of target foo, foo_bar denotes a whole stack of operations to accomplish bar for target foo
haftmann
parents:
57191
diff
changeset
|
140 |
fun standard_const pred prmode ((b, mx), rhs) = |
57190
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
141 |
standard_declaration pred (const_decl (K true) prmode ((b, mx), rhs)); |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
142 |
|
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
143 |
|
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
144 |
(** background primitives **) |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
145 |
|
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
146 |
fun background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy = |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
147 |
let |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
148 |
val params = type_params @ term_params; |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
149 |
val mx' = check_mixfix_global (b, null params) mx; |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
150 |
|
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
151 |
val (const, lthy2) = lthy |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
152 |
|> Local_Theory.background_theory_result (Sign.declare_const lthy ((b, U), mx')); |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
153 |
val lhs = Term.list_comb (const, params); |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
154 |
|
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
155 |
val ((_, def), lthy3) = lthy2 |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
156 |
|> Local_Theory.background_theory_result |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
157 |
(Thm.add_def lthy2 false false |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
158 |
(Thm.def_binding_optional b b_def, Logic.mk_equals (lhs, rhs))); |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
159 |
in ((lhs, def), lthy3) end; |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
160 |
|
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
161 |
fun background_declaration decl lthy = |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
162 |
let |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
163 |
val theory_decl = |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
164 |
Local_Theory.standard_form lthy |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
165 |
(Proof_Context.init_global (Proof_Context.theory_of lthy)) decl; |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
166 |
in Local_Theory.background_theory (Context.theory_map theory_decl) lthy end; |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
167 |
|
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
168 |
fun background_abbrev (b, global_rhs) params = |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
169 |
Local_Theory.background_theory_result (Sign.add_abbrev Print_Mode.internal (b, global_rhs)) |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58028
diff
changeset
|
170 |
#>> apply2 (fn t => Term.list_comb (Logic.unvarify_global t, params)) |
57190
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
171 |
|
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
172 |
|
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
173 |
(** lifting primitive to local theory operations **) |
38312
9dd57db3c0f2
moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents:
38311
diff
changeset
|
174 |
|
38309 | 175 |
(* define *) |
176 |
||
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
|
177 |
fun define foundation internal ((b, mx), ((b_def, atts), rhs)) lthy = |
38309 | 178 |
let |
59616 | 179 |
val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy); |
38309 | 180 |
|
181 |
(*term and type parameters*) |
|
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59616
diff
changeset
|
182 |
val ((defs, _), rhs') = Thm.cterm_of lthy rhs |
47276 | 183 |
|> Local_Defs.export_cterm lthy thy_ctxt ||> Thm.term_of; |
38309 | 184 |
|
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
|
185 |
val xs = Variable.add_fixed lthy rhs' []; |
38309 | 186 |
val T = Term.fastype_of rhs; |
187 |
val tfreesT = Term.add_tfreesT T (fold (Term.add_tfreesT o #2) xs []); |
|
188 |
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
|
189 |
val mx' = check_mixfix lthy (b, extra_tfrees) mx; |
38309 | 190 |
|
191 |
val type_params = map (Logic.mk_type o TFree) extra_tfrees; |
|
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58028
diff
changeset
|
192 |
val term_params = map Free (sort (Variable.fixed_ord lthy o apply2 #1) xs); |
38309 | 193 |
val params = type_params @ term_params; |
194 |
||
195 |
val U = map Term.fastype_of params ---> T; |
|
196 |
||
197 |
(*foundation*) |
|
45353 | 198 |
val ((lhs', global_def), lthy2) = lthy |
199 |
|> foundation (((b, U), mx'), (b_def, rhs')) (type_params, term_params); |
|
38309 | 200 |
|
201 |
(*local definition*) |
|
38315 | 202 |
val ((lhs, local_def), lthy3) = lthy2 |
38309 | 203 |
|> Local_Defs.add_def ((b, NoSyn), lhs'); |
47240 | 204 |
|
205 |
(*result*) |
|
47238 | 206 |
val def = |
47240 | 207 |
Thm.transitive local_def global_def |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59616
diff
changeset
|
208 |
|> Local_Defs.contract lthy3 defs (Thm.cterm_of lthy3 (Logic.mk_equals (lhs, rhs))); |
38315 | 209 |
val ([(res_name, [res])], lthy4) = lthy3 |
47080 | 210 |
|> Local_Theory.notes [((if internal then Binding.empty else b_def, atts), [([def], [])])]; |
38315 | 211 |
in ((lhs, (res_name, res)), lthy4) end; |
38309 | 212 |
|
213 |
||
214 |
(* notes *) |
|
215 |
||
47250
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
216 |
local |
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
217 |
|
38309 | 218 |
fun import_export_proof ctxt (name, raw_th) = |
219 |
let |
|
59616 | 220 |
val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of ctxt); |
38309 | 221 |
|
222 |
(*export assumes/defines*) |
|
54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
54742
diff
changeset
|
223 |
val th = Goal.norm_result ctxt 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
|
224 |
val ((defs, asms), th') = Local_Defs.export ctxt thy_ctxt th; |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52230
diff
changeset
|
225 |
val asms' = map (rewrite_rule ctxt (Drule.norm_hhf_eqs @ defs)) asms; |
38309 | 226 |
|
227 |
(*export fixes*) |
|
228 |
val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []); |
|
229 |
val frees = map Free (Thm.fold_terms Term.add_frees th' []); |
|
45352 | 230 |
val (th'' :: vs) = |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59616
diff
changeset
|
231 |
(th' :: map (Drule.mk_term o Thm.cterm_of ctxt) (map Logic.mk_type tfrees @ frees)) |
38309 | 232 |
|> Variable.export ctxt thy_ctxt |
233 |
|> Drule.zero_var_indexes_list; |
|
234 |
||
235 |
(*thm definition*) |
|
45413
117ff038f8f7
disabled Thm.compress (again) -- costs for building tables tend to be higher than potential benefit;
wenzelm
parents:
45407
diff
changeset
|
236 |
val result = Global_Theory.name_thm true true name th''; |
38309 | 237 |
|
238 |
(*import fixes*) |
|
239 |
val (tvars, vars) = |
|
240 |
chop (length tfrees) (map (Thm.term_of o Drule.dest_term) vs) |
|
241 |
|>> map Logic.dest_type; |
|
242 |
||
243 |
val instT = map_filter (fn (TVar v, T) => SOME (v, T) | _ => NONE) (tvars ~~ tfrees); |
|
244 |
val inst = filter (is_Var o fst) (vars ~~ frees); |
|
59616 | 245 |
val cinstT = instT |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59616
diff
changeset
|
246 |
|> map (apply2 (Thm.ctyp_of ctxt) o apfst TVar); |
59616 | 247 |
val cinst = inst |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59616
diff
changeset
|
248 |
|> map (apply2 (Thm.cterm_of ctxt o Term.map_types (Term_Subst.instantiateT instT))); |
38309 | 249 |
val result' = Thm.instantiate (cinstT, cinst) result; |
250 |
||
251 |
(*import assumes/defines*) |
|
252 |
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
|
253 |
(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
|
254 |
handle THM _ => raise THM ("Failed to re-import result", 0, result' :: asms')) |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52230
diff
changeset
|
255 |
|> Local_Defs.contract ctxt defs (Thm.cprop_of th) |
54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
54742
diff
changeset
|
256 |
|> Goal.norm_result ctxt |
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
38831
diff
changeset
|
257 |
|> Global_Theory.name_thm false false name; |
38309 | 258 |
|
259 |
in (result'', result) end; |
|
260 |
||
47250
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
261 |
in |
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
262 |
|
57192
180e955711cf
yet another attempt for terminology: foo_target_bar denotes an operation bar operating solely on the target context of target foo, foo_bar denotes a whole stack of operations to accomplish bar for target foo
haftmann
parents:
57191
diff
changeset
|
263 |
fun notes notes' kind facts lthy = |
38309 | 264 |
let |
265 |
val facts' = facts |
|
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
38831
diff
changeset
|
266 |
|> map (fn (a, bs) => (a, Global_Theory.burrow_fact (Global_Theory.name_multi |
38309 | 267 |
(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 global-only;
wenzelm
parents:
38831
diff
changeset
|
268 |
|> 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 global-only;
wenzelm
parents:
38831
diff
changeset
|
269 |
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 global-only;
wenzelm
parents:
38831
diff
changeset
|
270 |
val global_facts = Global_Theory.map_facts #2 facts'; |
38309 | 271 |
in |
272 |
lthy |
|
57192
180e955711cf
yet another attempt for terminology: foo_target_bar denotes an operation bar operating solely on the target context of target foo, foo_bar denotes a whole stack of operations to accomplish bar for target foo
haftmann
parents:
57191
diff
changeset
|
273 |
|> 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
|
274 |
|> Attrib.local_notes kind local_facts |
38309 | 275 |
end; |
276 |
||
47250
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
277 |
end; |
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
278 |
|
38309 | 279 |
|
280 |
(* abbrev *) |
|
281 |
||
57192
180e955711cf
yet another attempt for terminology: foo_target_bar denotes an operation bar operating solely on the target context of target foo, foo_bar denotes a whole stack of operations to accomplish bar for target foo
haftmann
parents:
57191
diff
changeset
|
282 |
fun abbrev abbrev' prmode ((b, mx), rhs) lthy = |
38309 | 283 |
let |
42360 | 284 |
val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy); |
38309 | 285 |
|
57109 | 286 |
val rhs' = Assumption.export_term lthy (Local_Theory.target_of lthy) rhs; |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58028
diff
changeset
|
287 |
val term_params = map Free (sort (Variable.fixed_ord lthy o apply2 #1) (Variable.add_fixed lthy rhs' [])); |
57160 | 288 |
val u = fold_rev lambda term_params rhs'; |
47290 | 289 |
val global_rhs = singleton (Variable.polymorphic thy_ctxt) u; |
38309 | 290 |
|
291 |
val extra_tfrees = |
|
292 |
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
|
293 |
val mx' = check_mixfix lthy (b, extra_tfrees) mx; |
57160 | 294 |
val type_params = map (Logic.mk_type o TFree) extra_tfrees; |
38309 | 295 |
in |
296 |
lthy |
|
57192
180e955711cf
yet another attempt for terminology: foo_target_bar denotes an operation bar operating solely on the target context of target foo, foo_bar denotes a whole stack of operations to accomplish bar for target foo
haftmann
parents:
57191
diff
changeset
|
297 |
|> abbrev' prmode (b, mx') global_rhs (type_params, term_params) |
57109 | 298 |
|> Proof_Context.add_abbrev Print_Mode.internal (b, rhs) |> snd |
299 |
|> Local_Defs.fixed_abbrev ((b, NoSyn), rhs) |
|
38309 | 300 |
end; |
301 |
||
38341
72dba5bd5f63
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38315
diff
changeset
|
302 |
|
57190
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
303 |
(** theory operations **) |
38341
72dba5bd5f63
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38315
diff
changeset
|
304 |
|
47284
0e65b6a016dc
clarified background_foundation vs. theory_foundation (with const_declaration);
wenzelm
parents:
47283
diff
changeset
|
305 |
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
|
306 |
background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) |
57192
180e955711cf
yet another attempt for terminology: foo_target_bar denotes an operation bar operating solely on the target context of target foo, foo_bar denotes a whole stack of operations to accomplish bar for target foo
haftmann
parents:
57191
diff
changeset
|
307 |
#-> (fn (lhs, def) => standard_const (op <>) Syntax.mode_default ((b, mx), lhs) |
57057 | 308 |
#> pair (lhs, def)); |
47284
0e65b6a016dc
clarified background_foundation vs. theory_foundation (with const_declaration);
wenzelm
parents:
47283
diff
changeset
|
309 |
|
47250
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
310 |
fun theory_notes kind global_facts local_facts = |
57191 | 311 |
Local_Theory.background_theory (Attrib.global_notes kind global_facts #> snd) |
312 |
#> standard_notes (op <>) kind local_facts; |
|
38341
72dba5bd5f63
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38315
diff
changeset
|
313 |
|
57190
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
314 |
fun theory_declaration decl = |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
315 |
background_declaration decl #> standard_declaration (K true) decl; |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
316 |
|
57118 | 317 |
fun theory_abbrev prmode (b, mx) global_rhs params = |
47286
392c4cd97e5c
more uniform theory_abbrev with const_declaration;
wenzelm
parents:
47285
diff
changeset
|
318 |
Local_Theory.background_theory_result |
57109 | 319 |
(Sign.add_abbrev (#1 prmode) (b, global_rhs) #-> |
47291
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
47290
diff
changeset
|
320 |
(fn (lhs, _) => (* FIXME type_params!? *) |
57160 | 321 |
Sign.notation true prmode [(lhs, check_mixfix_global (b, null (snd params)) mx)] #> pair lhs)) |
57192
180e955711cf
yet another attempt for terminology: foo_target_bar denotes an operation bar operating solely on the target context of target foo, foo_bar denotes a whole stack of operations to accomplish bar for target foo
haftmann
parents:
57191
diff
changeset
|
322 |
#-> (fn lhs => standard_const (op <>) prmode |
57160 | 323 |
((b, if null (snd params) then NoSyn else mx), Term.list_comb (Logic.unvarify_global lhs, snd params))); |
38341
72dba5bd5f63
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38315
diff
changeset
|
324 |
|
57190
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
325 |
val theory_registration = |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
326 |
Local_Theory.raw_theory o Context.theory_map ooo Locale.add_registration; |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
327 |
|
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
328 |
|
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
329 |
(** locale operations **) |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
330 |
|
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
331 |
fun locale_notes locale kind global_facts local_facts = |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
332 |
Local_Theory.background_theory |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
333 |
(Attrib.global_notes kind (Attrib.map_facts (K []) global_facts) #> snd) #> |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
334 |
(fn lthy => lthy |> |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
335 |
Local_Theory.target (fn ctxt => ctxt |> |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
336 |
Locale.add_thmss locale kind (standard_facts lthy ctxt local_facts))) #> |
57191 | 337 |
standard_notes (fn (this, other) => other <> 0 andalso this <> other) kind local_facts; |
57190
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
338 |
|
57192
180e955711cf
yet another attempt for terminology: foo_target_bar denotes an operation bar operating solely on the target context of target foo, foo_bar denotes a whole stack of operations to accomplish bar for target foo
haftmann
parents:
57191
diff
changeset
|
339 |
fun locale_target_declaration locale syntax decl lthy = lthy |
57190
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
340 |
|> Local_Theory.target (fn ctxt => ctxt |> |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
341 |
Locale.add_declaration locale syntax |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
342 |
(Morphism.transform (Local_Theory.standard_morphism lthy ctxt) decl)); |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
343 |
|
57193 | 344 |
fun locale_declaration locale {syntax, pervasive} decl = |
345 |
pervasive ? background_declaration decl |
|
346 |
#> locale_target_declaration locale syntax decl |
|
347 |
#> standard_declaration (fn (_, other) => other <> 0) decl; |
|
348 |
||
57192
180e955711cf
yet another attempt for terminology: foo_target_bar denotes an operation bar operating solely on the target context of target foo, foo_bar denotes a whole stack of operations to accomplish bar for target foo
haftmann
parents:
57191
diff
changeset
|
349 |
fun locale_target_const locale phi_pred prmode ((b, mx), rhs) = |
180e955711cf
yet another attempt for terminology: foo_target_bar denotes an operation bar operating solely on the target context of target foo, foo_bar denotes a whole stack of operations to accomplish bar for target foo
haftmann
parents:
57191
diff
changeset
|
350 |
locale_target_declaration locale true (const_decl phi_pred prmode ((b, mx), rhs)) |
57190
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
351 |
|
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
352 |
fun locale_const locale prmode ((b, mx), rhs) = |
57192
180e955711cf
yet another attempt for terminology: foo_target_bar denotes an operation bar operating solely on the target context of target foo, foo_bar denotes a whole stack of operations to accomplish bar for target foo
haftmann
parents:
57191
diff
changeset
|
353 |
locale_target_const locale (K true) prmode ((b, mx), rhs) |
180e955711cf
yet another attempt for terminology: foo_target_bar denotes an operation bar operating solely on the target context of target foo, foo_bar denotes a whole stack of operations to accomplish bar for target foo
haftmann
parents:
57191
diff
changeset
|
354 |
#> standard_const (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, mx), rhs); |
57190
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
355 |
|
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
356 |
fun locale_dependency locale dep_morph mixin export = |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
357 |
(Local_Theory.raw_theory ooo Locale.add_dependency locale) dep_morph mixin export |
57926
59b2572e8e93
load local_theory.ML before attrib.ML, with subtle change of semantics due to canonical Local_Theory.map_contexts instead of private Local_Theory.map_top;
wenzelm
parents:
57193
diff
changeset
|
358 |
#> Locale.activate_fragment_nonbrittle dep_morph mixin export; |
47279
4bab649dedf0
clarified standard_declaration vs. theory_declaration;
wenzelm
parents:
47276
diff
changeset
|
359 |
|
38309 | 360 |
end; |