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