author | haftmann |
Fri, 24 Sep 2021 11:04:18 +0000 | |
changeset 74361 | 690928dd6f8f |
parent 74284 | 8d1e27a23dd1 |
child 74561 | 8e6c973003c8 |
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 |
|
60345
592806806494
completely separated canonical class abbreviations from abbreviations stemming from non-canonical morphisms -- these have no shared concept
haftmann
parents:
60344
diff
changeset
|
10 |
(*auxiliary*) |
592806806494
completely separated canonical class abbreviations from abbreviations stemming from non-canonical morphisms -- these have no shared concept
haftmann
parents:
60344
diff
changeset
|
11 |
val export_abbrev: Proof.context -> |
592806806494
completely separated canonical class abbreviations from abbreviations stemming from non-canonical morphisms -- these have no shared concept
haftmann
parents:
60344
diff
changeset
|
12 |
(term -> term) -> term -> term * ((string * sort) list * (term list * term list)) |
62764 | 13 |
val check_mixfix: Proof.context -> binding * (string * sort) list -> mixfix -> mixfix |
60345
592806806494
completely separated canonical class abbreviations from abbreviations stemming from non-canonical morphisms -- these have no shared concept
haftmann
parents:
60344
diff
changeset
|
14 |
val check_mixfix_global: binding * bool -> mixfix -> mixfix |
592806806494
completely separated canonical class abbreviations from abbreviations stemming from non-canonical morphisms -- these have no shared concept
haftmann
parents:
60344
diff
changeset
|
15 |
|
60340 | 16 |
(*background primitives*) |
57190
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
17 |
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
|
18 |
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
|
19 |
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
|
20 |
val background_abbrev: binding * term -> term list -> local_theory -> (term * term) * local_theory |
71788
ca3ac5238c41
hooks for foundational terms: protection of foundational terms during simplification
haftmann
parents:
71178
diff
changeset
|
21 |
val add_foundation_interpretation: (binding * (term * term list) -> Context.generic -> Context.generic) -> |
ca3ac5238c41
hooks for foundational terms: protection of foundational terms during simplification
haftmann
parents:
71178
diff
changeset
|
22 |
theory -> theory |
57190
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
23 |
|
60340 | 24 |
(*nested local theories primitives*) |
67652 | 25 |
val standard_facts: local_theory -> Proof.context -> Attrib.fact list -> Attrib.fact list |
26 |
val standard_notes: (int * int -> bool) -> string -> Attrib.fact list -> |
|
63269 | 27 |
local_theory -> local_theory |
28 |
val standard_declaration: (int * int -> bool) -> |
|
29 |
(morphism -> Context.generic -> Context.generic) -> local_theory -> local_theory |
|
60340 | 30 |
val standard_const: (int * int -> bool) -> Syntax.mode -> (binding * mixfix) * term -> |
31 |
local_theory -> local_theory |
|
73845 | 32 |
val local_interpretation: Locale.registration -> |
33 |
local_theory -> local_theory |
|
60340 | 34 |
|
35 |
(*lifting target primitives to local theory operations*) |
|
40782 | 36 |
val define: (((binding * typ) * mixfix) * (binding * term) -> |
37 |
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
|
38 |
bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory -> |
40782 | 39 |
(term * (string * thm)) * local_theory |
47250
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
40 |
val notes: |
67652 | 41 |
(string -> Attrib.fact list -> Attrib.fact list -> local_theory -> local_theory) -> |
42 |
string -> Attrib.fact list -> local_theory -> (string * thm list) list * local_theory |
|
60337 | 43 |
val abbrev: (Syntax.mode -> binding * mixfix -> term -> |
57160 | 44 |
term list * term list -> local_theory -> local_theory) -> |
60337 | 45 |
Syntax.mode -> (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
|
46 |
|
60341
fcbd7f0c52c3
clearly separated target primitives (target_foo) from self-contained target operations (foo)
haftmann
parents:
60340
diff
changeset
|
47 |
(*theory target primitives*) |
fcbd7f0c52c3
clearly separated target primitives (target_foo) from self-contained target operations (foo)
haftmann
parents:
60340
diff
changeset
|
48 |
val theory_target_foundation: ((binding * typ) * mixfix) * (binding * term) -> |
fcbd7f0c52c3
clearly separated target primitives (target_foo) from self-contained target operations (foo)
haftmann
parents:
60340
diff
changeset
|
49 |
term list * term list -> local_theory -> (term * thm) * local_theory |
67652 | 50 |
val theory_target_notes: string -> Attrib.fact list -> Attrib.fact list -> |
51 |
local_theory -> local_theory |
|
60341
fcbd7f0c52c3
clearly separated target primitives (target_foo) from self-contained target operations (foo)
haftmann
parents:
60340
diff
changeset
|
52 |
val theory_target_abbrev: Syntax.mode -> (binding * mixfix) -> term -> term list * term list -> |
fcbd7f0c52c3
clearly separated target primitives (target_foo) from self-contained target operations (foo)
haftmann
parents:
60340
diff
changeset
|
53 |
local_theory -> local_theory |
fcbd7f0c52c3
clearly separated target primitives (target_foo) from self-contained target operations (foo)
haftmann
parents:
60340
diff
changeset
|
54 |
|
fcbd7f0c52c3
clearly separated target primitives (target_foo) from self-contained target operations (foo)
haftmann
parents:
60340
diff
changeset
|
55 |
(*theory target operations*) |
60344
a40369ea3ba5
self-contained formulation of abbrev for named targets
haftmann
parents:
60342
diff
changeset
|
56 |
val theory_abbrev: Syntax.mode -> (binding * mixfix) * term -> |
a40369ea3ba5
self-contained formulation of abbrev for named targets
haftmann
parents:
60342
diff
changeset
|
57 |
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
|
58 |
val theory_declaration: declaration -> local_theory -> local_theory |
73845 | 59 |
val theory_registration: Locale.registration -> local_theory -> local_theory |
57190
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
60 |
|
60341
fcbd7f0c52c3
clearly separated target primitives (target_foo) from self-contained target operations (foo)
haftmann
parents:
60340
diff
changeset
|
61 |
(*locale target primitives*) |
67652 | 62 |
val locale_target_notes: string -> string -> Attrib.fact list -> Attrib.fact list -> |
63 |
local_theory -> local_theory |
|
63339 | 64 |
val locale_target_abbrev: string -> Syntax.mode -> |
65 |
(binding * mixfix) -> term -> term list * term list -> 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
|
66 |
val locale_target_declaration: string -> bool -> declaration -> local_theory -> local_theory |
60341
fcbd7f0c52c3
clearly separated target primitives (target_foo) from self-contained target operations (foo)
haftmann
parents:
60340
diff
changeset
|
67 |
val locale_target_const: string -> (morphism -> bool) -> Syntax.mode -> |
fcbd7f0c52c3
clearly separated target primitives (target_foo) from self-contained target operations (foo)
haftmann
parents:
60340
diff
changeset
|
68 |
(binding * mixfix) * term -> local_theory -> local_theory |
fcbd7f0c52c3
clearly separated target primitives (target_foo) from self-contained target operations (foo)
haftmann
parents:
60340
diff
changeset
|
69 |
|
fcbd7f0c52c3
clearly separated target primitives (target_foo) from self-contained target operations (foo)
haftmann
parents:
60340
diff
changeset
|
70 |
(*locale operations*) |
60344
a40369ea3ba5
self-contained formulation of abbrev for named targets
haftmann
parents:
60342
diff
changeset
|
71 |
val locale_abbrev: string -> Syntax.mode -> (binding * mixfix) * term -> |
a40369ea3ba5
self-contained formulation of abbrev for named targets
haftmann
parents:
60342
diff
changeset
|
72 |
local_theory -> (term * term) * local_theory |
57193 | 73 |
val locale_declaration: string -> {syntax: bool, pervasive: bool} -> declaration -> |
74 |
local_theory -> local_theory |
|
57190
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
75 |
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
|
76 |
local_theory -> local_theory |
73845 | 77 |
val locale_dependency: string -> Locale.registration -> |
78 |
local_theory -> local_theory |
|
45353 | 79 |
end |
38309 | 80 |
|
81 |
structure Generic_Target: GENERIC_TARGET = |
|
82 |
struct |
|
83 |
||
57190
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
84 |
(** consts **) |
38312
9dd57db3c0f2
moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents:
38311
diff
changeset
|
85 |
|
60345
592806806494
completely separated canonical class abbreviations from abbreviations stemming from non-canonical morphisms -- these have no shared concept
haftmann
parents:
60344
diff
changeset
|
86 |
fun export_abbrev lthy preprocess rhs = |
60342
df9b153d866b
separate function to compute exported abbreviation
haftmann
parents:
60341
diff
changeset
|
87 |
let |
df9b153d866b
separate function to compute exported abbreviation
haftmann
parents:
60341
diff
changeset
|
88 |
val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy); |
df9b153d866b
separate function to compute exported abbreviation
haftmann
parents:
60341
diff
changeset
|
89 |
|
df9b153d866b
separate function to compute exported abbreviation
haftmann
parents:
60341
diff
changeset
|
90 |
val rhs' = rhs |
df9b153d866b
separate function to compute exported abbreviation
haftmann
parents:
60341
diff
changeset
|
91 |
|> Assumption.export_term lthy (Local_Theory.target_of lthy) |
df9b153d866b
separate function to compute exported abbreviation
haftmann
parents:
60341
diff
changeset
|
92 |
|> preprocess; |
63339 | 93 |
val term_params = |
94 |
map Free (sort (Variable.fixed_ord lthy o apply2 #1) (Variable.add_fixed lthy rhs' [])); |
|
60342
df9b153d866b
separate function to compute exported abbreviation
haftmann
parents:
60341
diff
changeset
|
95 |
val u = fold_rev lambda term_params rhs'; |
df9b153d866b
separate function to compute exported abbreviation
haftmann
parents:
60341
diff
changeset
|
96 |
val global_rhs = singleton (Variable.polymorphic thy_ctxt) u; |
df9b153d866b
separate function to compute exported abbreviation
haftmann
parents:
60341
diff
changeset
|
97 |
|
74266 | 98 |
val type_tfrees = TFrees.build (TFrees.add_tfreesT (Term.fastype_of u)); |
60342
df9b153d866b
separate function to compute exported abbreviation
haftmann
parents:
60341
diff
changeset
|
99 |
val extra_tfrees = |
74278 | 100 |
TFrees.build (TFrees.add_tfrees_unless (TFrees.defined type_tfrees) u) |
74284
8d1e27a23dd1
clarified order of extra TFrees: underlying fast_string_ord coincides with Name.invent (e.g. from type inference);
wenzelm
parents:
74282
diff
changeset
|
101 |
|> TFrees.keys; |
60342
df9b153d866b
separate function to compute exported abbreviation
haftmann
parents:
60341
diff
changeset
|
102 |
val type_params = map (Logic.mk_type o TFree) extra_tfrees; |
60345
592806806494
completely separated canonical class abbreviations from abbreviations stemming from non-canonical morphisms -- these have no shared concept
haftmann
parents:
60344
diff
changeset
|
103 |
in (global_rhs, (extra_tfrees, (type_params, term_params))) end; |
60342
df9b153d866b
separate function to compute exported abbreviation
haftmann
parents:
60341
diff
changeset
|
104 |
|
38312
9dd57db3c0f2
moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents:
38311
diff
changeset
|
105 |
fun check_mixfix ctxt (b, extra_tfrees) mx = |
62767
d6b0d35b3aed
relevant check_mixfix happens further at the bottom, to avoid duplicate reports via Specification.prepare;
wenzelm
parents:
62764
diff
changeset
|
106 |
if null extra_tfrees then mx |
d6b0d35b3aed
relevant check_mixfix happens further at the bottom, to avoid duplicate reports via Specification.prepare;
wenzelm
parents:
62764
diff
changeset
|
107 |
else |
d6b0d35b3aed
relevant check_mixfix happens further at the bottom, to avoid duplicate reports via Specification.prepare;
wenzelm
parents:
62764
diff
changeset
|
108 |
(if Context_Position.is_visible ctxt then |
d6b0d35b3aed
relevant check_mixfix happens further at the bottom, to avoid duplicate reports via Specification.prepare;
wenzelm
parents:
62764
diff
changeset
|
109 |
warning |
d6b0d35b3aed
relevant check_mixfix happens further at the bottom, to avoid duplicate reports via Specification.prepare;
wenzelm
parents:
62764
diff
changeset
|
110 |
("Additional type variable(s) in specification of " ^ Binding.print b ^ ": " ^ |
74284
8d1e27a23dd1
clarified order of extra TFrees: underlying fast_string_ord coincides with Name.invent (e.g. from type inference);
wenzelm
parents:
74282
diff
changeset
|
111 |
commas (map (Syntax.string_of_typ ctxt o TFree) extra_tfrees) ^ |
62767
d6b0d35b3aed
relevant check_mixfix happens further at the bottom, to avoid duplicate reports via Specification.prepare;
wenzelm
parents:
62764
diff
changeset
|
112 |
(if Mixfix.is_empty mx then "" |
d6b0d35b3aed
relevant check_mixfix happens further at the bottom, to avoid duplicate reports via Specification.prepare;
wenzelm
parents:
62764
diff
changeset
|
113 |
else "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx))) |
d6b0d35b3aed
relevant check_mixfix happens further at the bottom, to avoid duplicate reports via Specification.prepare;
wenzelm
parents:
62764
diff
changeset
|
114 |
else (); NoSyn); |
38312
9dd57db3c0f2
moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents:
38311
diff
changeset
|
115 |
|
47291
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
47290
diff
changeset
|
116 |
fun check_mixfix_global (b, no_params) mx = |
62752 | 117 |
if no_params orelse Mixfix.is_empty mx then mx |
118 |
else |
|
119 |
(warning ("Dropping global mixfix syntax: " ^ Binding.print b ^ " " ^ |
|
62767
d6b0d35b3aed
relevant check_mixfix happens further at the bottom, to avoid duplicate reports via Specification.prepare;
wenzelm
parents:
62764
diff
changeset
|
120 |
Pretty.string_of (Mixfix.pretty_mixfix mx)); NoSyn); |
47291
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
47290
diff
changeset
|
121 |
|
61701
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61261
diff
changeset
|
122 |
fun same_const (Const (c, _), Const (c', _)) = c = c' |
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61261
diff
changeset
|
123 |
| same_const (t $ _, t' $ _) = same_const (t, t') |
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61261
diff
changeset
|
124 |
| same_const (_, _) = false; |
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61261
diff
changeset
|
125 |
|
57190
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
126 |
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
|
127 |
if phi_pred phi then |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
128 |
let |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
129 |
val b' = Morphism.binding phi b; |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
130 |
val rhs' = Morphism.term phi rhs; |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
131 |
val same_shape = Term.aconv_untyped (rhs, rhs'); |
61701
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61261
diff
changeset
|
132 |
val same_stem = same_shape orelse same_const (rhs, rhs'); |
57190
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
133 |
val const_alias = |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
134 |
if same_shape then |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
135 |
(case rhs' of |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
136 |
Const (c, T) => |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
137 |
let |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
138 |
val thy = Context.theory_of context; |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
139 |
val ctxt = Context.proof_of context; |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
140 |
in |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
141 |
(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
|
142 |
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
|
143 |
| NONE => NONE) |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
144 |
end |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
145 |
| _ => NONE) |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
146 |
else NONE; |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
147 |
in |
60283 | 148 |
(case const_alias of |
57190
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
149 |
SOME c => |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
150 |
context |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
151 |
|> 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
|
152 |
|> 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
|
153 |
| NONE => |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
154 |
context |
62764 | 155 |
|> Proof_Context.generic_add_abbrev Print_Mode.internal |
156 |
(b', Term.close_schematic_term rhs') |
|
61701
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61261
diff
changeset
|
157 |
|-> (fn (const as Const (c, _), _) => same_stem ? |
57190
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
158 |
(Proof_Context.generic_revert_abbrev (#1 prmode) c #> |
62764 | 159 |
same_shape ? |
160 |
Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)])))) |
|
57190
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
161 |
end |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
162 |
else context; |
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 |
|
60283 | 165 |
|
57190
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
166 |
(** background primitives **) |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
167 |
|
71788
ca3ac5238c41
hooks for foundational terms: protection of foundational terms during simplification
haftmann
parents:
71178
diff
changeset
|
168 |
structure Foundation_Interpretations = Theory_Data |
ca3ac5238c41
hooks for foundational terms: protection of foundational terms during simplification
haftmann
parents:
71178
diff
changeset
|
169 |
( |
ca3ac5238c41
hooks for foundational terms: protection of foundational terms during simplification
haftmann
parents:
71178
diff
changeset
|
170 |
type T = (binding * (term * term list) -> Context.generic -> Context.generic) Inttab.table; |
ca3ac5238c41
hooks for foundational terms: protection of foundational terms during simplification
haftmann
parents:
71178
diff
changeset
|
171 |
val empty = Inttab.empty; |
ca3ac5238c41
hooks for foundational terms: protection of foundational terms during simplification
haftmann
parents:
71178
diff
changeset
|
172 |
val extend = I; |
ca3ac5238c41
hooks for foundational terms: protection of foundational terms during simplification
haftmann
parents:
71178
diff
changeset
|
173 |
val merge = Inttab.merge (K true); |
ca3ac5238c41
hooks for foundational terms: protection of foundational terms during simplification
haftmann
parents:
71178
diff
changeset
|
174 |
); |
ca3ac5238c41
hooks for foundational terms: protection of foundational terms during simplification
haftmann
parents:
71178
diff
changeset
|
175 |
|
ca3ac5238c41
hooks for foundational terms: protection of foundational terms during simplification
haftmann
parents:
71178
diff
changeset
|
176 |
fun add_foundation_interpretation f = |
ca3ac5238c41
hooks for foundational terms: protection of foundational terms during simplification
haftmann
parents:
71178
diff
changeset
|
177 |
Foundation_Interpretations.map (Inttab.update_new (serial (), f)); |
ca3ac5238c41
hooks for foundational terms: protection of foundational terms during simplification
haftmann
parents:
71178
diff
changeset
|
178 |
|
ca3ac5238c41
hooks for foundational terms: protection of foundational terms during simplification
haftmann
parents:
71178
diff
changeset
|
179 |
fun foundation_interpretation binding_const_params lthy = |
ca3ac5238c41
hooks for foundational terms: protection of foundational terms during simplification
haftmann
parents:
71178
diff
changeset
|
180 |
let |
ca3ac5238c41
hooks for foundational terms: protection of foundational terms during simplification
haftmann
parents:
71178
diff
changeset
|
181 |
val interps = Foundation_Interpretations.get (Proof_Context.theory_of lthy); |
ca3ac5238c41
hooks for foundational terms: protection of foundational terms during simplification
haftmann
parents:
71178
diff
changeset
|
182 |
val interp = Inttab.fold (fn (_, f) => f binding_const_params) interps; |
ca3ac5238c41
hooks for foundational terms: protection of foundational terms during simplification
haftmann
parents:
71178
diff
changeset
|
183 |
in |
ca3ac5238c41
hooks for foundational terms: protection of foundational terms during simplification
haftmann
parents:
71178
diff
changeset
|
184 |
lthy |
ca3ac5238c41
hooks for foundational terms: protection of foundational terms during simplification
haftmann
parents:
71178
diff
changeset
|
185 |
|> Local_Theory.background_theory (Context.theory_map interp) |
ca3ac5238c41
hooks for foundational terms: protection of foundational terms during simplification
haftmann
parents:
71178
diff
changeset
|
186 |
|> Local_Theory.map_contexts (K (Context.proof_map interp)) |
ca3ac5238c41
hooks for foundational terms: protection of foundational terms during simplification
haftmann
parents:
71178
diff
changeset
|
187 |
end; |
ca3ac5238c41
hooks for foundational terms: protection of foundational terms during simplification
haftmann
parents:
71178
diff
changeset
|
188 |
|
57190
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
189 |
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
|
190 |
let |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
191 |
val params = type_params @ term_params; |
71788
ca3ac5238c41
hooks for foundational terms: protection of foundational terms during simplification
haftmann
parents:
71178
diff
changeset
|
192 |
val target_params = type_params |
ca3ac5238c41
hooks for foundational terms: protection of foundational terms during simplification
haftmann
parents:
71178
diff
changeset
|
193 |
@ take_prefix is_Free (Variable.export_terms lthy (Local_Theory.target_of lthy) term_params); |
57190
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
194 |
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
|
195 |
|
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
196 |
val (const, lthy2) = lthy |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
197 |
|> 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
|
198 |
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
|
199 |
|
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
200 |
val ((_, def), lthy3) = lthy2 |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
201 |
|> Local_Theory.background_theory_result |
61261
ddb2da7cb2e4
more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents:
60924
diff
changeset
|
202 |
(Thm.add_def (Proof_Context.defs_context lthy2) false false |
71788
ca3ac5238c41
hooks for foundational terms: protection of foundational terms during simplification
haftmann
parents:
71178
diff
changeset
|
203 |
(Thm.def_binding_optional b b_def, Logic.mk_equals (lhs, rhs))) |
ca3ac5238c41
hooks for foundational terms: protection of foundational terms during simplification
haftmann
parents:
71178
diff
changeset
|
204 |
||> foundation_interpretation (b, (const, target_params)); |
57190
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
205 |
in ((lhs, def), lthy3) end; |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
206 |
|
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
207 |
fun background_declaration decl lthy = |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
208 |
let |
71178 | 209 |
fun theory_decl context = |
57190
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
210 |
Local_Theory.standard_form lthy |
71178 | 211 |
(Proof_Context.init_global (Context.theory_of context)) decl context; |
57190
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
212 |
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
|
213 |
|
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
214 |
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
|
215 |
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
|
216 |
#>> 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
|
217 |
|
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
218 |
|
60283 | 219 |
|
60340 | 220 |
(** nested local theories primitives **) |
221 |
||
222 |
fun standard_facts lthy ctxt = |
|
223 |
Attrib.transform_facts (Local_Theory.standard_morphism lthy ctxt); |
|
224 |
||
225 |
fun standard_notes pred kind facts lthy = |
|
226 |
Local_Theory.map_contexts (fn level => fn ctxt => |
|
227 |
if pred (Local_Theory.level lthy, level) |
|
228 |
then Attrib.local_notes kind (standard_facts lthy ctxt facts) ctxt |> snd |
|
229 |
else ctxt) lthy; |
|
230 |
||
231 |
fun standard_declaration pred decl lthy = |
|
232 |
Local_Theory.map_contexts (fn level => fn ctxt => |
|
233 |
if pred (Local_Theory.level lthy, level) |
|
234 |
then Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt |
|
235 |
else ctxt) lthy; |
|
236 |
||
237 |
fun standard_const pred prmode ((b, mx), rhs) = |
|
238 |
standard_declaration pred (const_decl (K true) prmode ((b, mx), rhs)); |
|
239 |
||
73846 | 240 |
fun standard_registration pred registration lthy = |
241 |
Local_Theory.map_contexts (fn level => |
|
242 |
if pred (Local_Theory.level lthy, level) |
|
243 |
then Context.proof_map (Locale.add_registration registration) |
|
244 |
else I) lthy; |
|
245 |
||
74361
690928dd6f8f
apply declarations from interpretations in eigen context also
haftmann
parents:
74284
diff
changeset
|
246 |
val local_interpretation = standard_registration (fn (n, level) => level >= n - 1); |
73845 | 247 |
|
248 |
||
60340 | 249 |
|
250 |
(** lifting target primitives to local theory operations **) |
|
38312
9dd57db3c0f2
moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents:
38311
diff
changeset
|
251 |
|
38309 | 252 |
(* define *) |
253 |
||
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
|
254 |
fun define foundation internal ((b, mx), ((b_def, atts), rhs)) lthy = |
38309 | 255 |
let |
59616 | 256 |
val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy); |
38309 | 257 |
|
258 |
(*term and type parameters*) |
|
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59616
diff
changeset
|
259 |
val ((defs, _), rhs') = Thm.cterm_of lthy rhs |
47276 | 260 |
|> Local_Defs.export_cterm lthy thy_ctxt ||> Thm.term_of; |
38309 | 261 |
|
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
|
262 |
val xs = Variable.add_fixed lthy rhs' []; |
38309 | 263 |
val T = Term.fastype_of rhs; |
74266 | 264 |
val type_tfrees = TFrees.build (TFrees.add_tfreesT T #> fold (TFrees.add_tfreesT o #2) xs); |
74230 | 265 |
val extra_tfrees = |
74278 | 266 |
TFrees.build (rhs |> TFrees.add_tfrees_unless (TFrees.defined type_tfrees)) |
74284
8d1e27a23dd1
clarified order of extra TFrees: underlying fast_string_ord coincides with Name.invent (e.g. from type inference);
wenzelm
parents:
74282
diff
changeset
|
267 |
|> TFrees.keys; |
38312
9dd57db3c0f2
moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents:
38311
diff
changeset
|
268 |
val mx' = check_mixfix lthy (b, extra_tfrees) mx; |
38309 | 269 |
|
270 |
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
|
271 |
val term_params = map Free (sort (Variable.fixed_ord lthy o apply2 #1) xs); |
38309 | 272 |
val params = type_params @ term_params; |
273 |
||
274 |
val U = map Term.fastype_of params ---> T; |
|
275 |
||
276 |
(*foundation*) |
|
45353 | 277 |
val ((lhs', global_def), lthy2) = lthy |
278 |
|> foundation (((b, U), mx'), (b_def, rhs')) (type_params, term_params); |
|
38309 | 279 |
|
280 |
(*local definition*) |
|
63344 | 281 |
val ([(lhs, (_, local_def))], lthy3) = lthy2 |
63346 | 282 |
|> Context_Position.set_visible false |
63352 | 283 |
|> Local_Defs.define [((b, NoSyn), (Binding.empty_atts, lhs'))] |
63346 | 284 |
||> Context_Position.restore_visible lthy2; |
47240 | 285 |
|
286 |
(*result*) |
|
47238 | 287 |
val def = |
47240 | 288 |
Thm.transitive local_def global_def |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59616
diff
changeset
|
289 |
|> Local_Defs.contract lthy3 defs (Thm.cterm_of lthy3 (Logic.mk_equals (lhs, rhs))); |
38315 | 290 |
val ([(res_name, [res])], lthy4) = lthy3 |
47080 | 291 |
|> Local_Theory.notes [((if internal then Binding.empty else b_def, atts), [([def], [])])]; |
38315 | 292 |
in ((lhs, (res_name, res)), lthy4) end; |
38309 | 293 |
|
294 |
||
295 |
(* notes *) |
|
296 |
||
47250
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
297 |
local |
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
298 |
|
38309 | 299 |
fun import_export_proof ctxt (name, raw_th) = |
300 |
let |
|
59616 | 301 |
val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of ctxt); |
38309 | 302 |
|
303 |
(*export assumes/defines*) |
|
54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
54742
diff
changeset
|
304 |
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
|
305 |
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
|
306 |
val asms' = map (rewrite_rule ctxt (Drule.norm_hhf_eqs @ defs)) asms; |
38309 | 307 |
|
308 |
(*export fixes*) |
|
74281 | 309 |
val tfrees = |
310 |
TFrees.build (Thm.fold_terms {hyps = true} TFrees.add_tfrees th') |
|
74284
8d1e27a23dd1
clarified order of extra TFrees: underlying fast_string_ord coincides with Name.invent (e.g. from type inference);
wenzelm
parents:
74282
diff
changeset
|
311 |
|> TFrees.keys |> map TFree; |
74281 | 312 |
val frees = |
313 |
Frees.build (Thm.fold_terms {hyps = true} Frees.add_frees th') |
|
314 |
|> Frees.list_set_rev |> map Free; |
|
45352 | 315 |
val (th'' :: vs) = |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59616
diff
changeset
|
316 |
(th' :: map (Drule.mk_term o Thm.cterm_of ctxt) (map Logic.mk_type tfrees @ frees)) |
38309 | 317 |
|> Variable.export ctxt thy_ctxt |
318 |
|> Drule.zero_var_indexes_list; |
|
319 |
||
320 |
(*thm definition*) |
|
70427 | 321 |
val result = Global_Theory.name_thm Global_Theory.official1 name th''; |
38309 | 322 |
|
323 |
(*import fixes*) |
|
324 |
val (tvars, vars) = |
|
325 |
chop (length tfrees) (map (Thm.term_of o Drule.dest_term) vs) |
|
326 |
|>> map Logic.dest_type; |
|
327 |
||
74220
c49134ee16c1
more scalable data structure (but: rarely used many arguments);
wenzelm
parents:
73846
diff
changeset
|
328 |
val instT = |
74266 | 329 |
TVars.build (fold2 (fn a => fn b => |
330 |
(case a of TVar v => TVars.add (v, b) | _ => I)) tvars tfrees); |
|
74282 | 331 |
val cinstT = TVars.map (K (Thm.ctyp_of ctxt)) instT; |
74220
c49134ee16c1
more scalable data structure (but: rarely used many arguments);
wenzelm
parents:
73846
diff
changeset
|
332 |
val cinst = |
74282 | 333 |
Vars.build |
334 |
(fold2 (fn v => fn t => |
|
335 |
(case v of |
|
336 |
Var (xi, T) => |
|
337 |
Vars.add ((xi, Term_Subst.instantiateT instT T), |
|
338 |
Thm.cterm_of ctxt (Term.map_types (Term_Subst.instantiateT instT) t)) |
|
339 |
| _ => I)) vars frees); |
|
74220
c49134ee16c1
more scalable data structure (but: rarely used many arguments);
wenzelm
parents:
73846
diff
changeset
|
340 |
val result' = Thm.instantiate (cinstT, cinst) result; |
38309 | 341 |
|
342 |
(*import assumes/defines*) |
|
343 |
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
|
344 |
(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
|
345 |
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
|
346 |
|> Local_Defs.contract ctxt defs (Thm.cprop_of th) |
54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
54742
diff
changeset
|
347 |
|> Goal.norm_result ctxt |
70427 | 348 |
|> Global_Theory.name_thm Global_Theory.unofficial2 name; |
38309 | 349 |
|
350 |
in (result'', result) end; |
|
351 |
||
70494 | 352 |
fun bind_name lthy b = |
353 |
(Local_Theory.full_name lthy b, Binding.default_pos_of b); |
|
354 |
||
70544 | 355 |
fun map_facts f = map (apsnd (map (apfst (map f)))); |
356 |
||
47250
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
357 |
in |
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
358 |
|
60341
fcbd7f0c52c3
clearly separated target primitives (target_foo) from self-contained target operations (foo)
haftmann
parents:
60340
diff
changeset
|
359 |
fun notes target_notes kind facts lthy = |
38309 | 360 |
let |
361 |
val facts' = facts |
|
70494 | 362 |
|> map (fn (a, bs) => |
363 |
(a, Global_Theory.burrow_fact (Global_Theory.name_multi (bind_name lthy (fst a))) bs)) |
|
70544 | 364 |
|> map_facts (import_export_proof lthy); |
365 |
val local_facts = map_facts #1 facts'; |
|
366 |
val global_facts = map_facts #2 facts'; |
|
38309 | 367 |
in |
368 |
lthy |
|
60341
fcbd7f0c52c3
clearly separated target primitives (target_foo) from self-contained target operations (foo)
haftmann
parents:
60340
diff
changeset
|
369 |
|> 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
|
370 |
|> Attrib.local_notes kind local_facts |
38309 | 371 |
end; |
372 |
||
47250
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
373 |
end; |
6523a21076a8
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents:
47249
diff
changeset
|
374 |
|
38309 | 375 |
|
376 |
(* abbrev *) |
|
377 |
||
60341
fcbd7f0c52c3
clearly separated target primitives (target_foo) from self-contained target operations (foo)
haftmann
parents:
60340
diff
changeset
|
378 |
fun abbrev target_abbrev prmode ((b, mx), rhs) lthy = |
38309 | 379 |
let |
60345
592806806494
completely separated canonical class abbreviations from abbreviations stemming from non-canonical morphisms -- these have no shared concept
haftmann
parents:
60344
diff
changeset
|
380 |
val (global_rhs, (extra_tfrees, (type_params, term_params))) = export_abbrev lthy I rhs; |
38312
9dd57db3c0f2
moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents:
38311
diff
changeset
|
381 |
val mx' = check_mixfix lthy (b, extra_tfrees) mx; |
38309 | 382 |
in |
383 |
lthy |
|
60341
fcbd7f0c52c3
clearly separated target primitives (target_foo) from self-contained target operations (foo)
haftmann
parents:
60340
diff
changeset
|
384 |
|> target_abbrev prmode (b, mx') global_rhs (type_params, term_params) |
63346 | 385 |
|> Context_Position.set_visible false |
57109 | 386 |
|> Proof_Context.add_abbrev Print_Mode.internal (b, rhs) |> snd |
387 |
|> Local_Defs.fixed_abbrev ((b, NoSyn), rhs) |
|
62992 | 388 |
||> Context_Position.restore_visible lthy |
38309 | 389 |
end; |
390 |
||
38341
72dba5bd5f63
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38315
diff
changeset
|
391 |
|
60283 | 392 |
|
60341
fcbd7f0c52c3
clearly separated target primitives (target_foo) from self-contained target operations (foo)
haftmann
parents:
60340
diff
changeset
|
393 |
(** theory target primitives **) |
38341
72dba5bd5f63
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38315
diff
changeset
|
394 |
|
60341
fcbd7f0c52c3
clearly separated target primitives (target_foo) from self-contained target operations (foo)
haftmann
parents:
60340
diff
changeset
|
395 |
fun theory_target_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) = |
47284
0e65b6a016dc
clarified background_foundation vs. theory_foundation (with const_declaration);
wenzelm
parents:
47283
diff
changeset
|
396 |
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
|
397 |
#-> (fn (lhs, def) => standard_const (op <>) Syntax.mode_default ((b, mx), lhs) |
57057 | 398 |
#> pair (lhs, def)); |
47284
0e65b6a016dc
clarified background_foundation vs. theory_foundation (with const_declaration);
wenzelm
parents:
47283
diff
changeset
|
399 |
|
60341
fcbd7f0c52c3
clearly separated target primitives (target_foo) from self-contained target operations (foo)
haftmann
parents:
60340
diff
changeset
|
400 |
fun theory_target_notes kind global_facts local_facts = |
57191 | 401 |
Local_Theory.background_theory (Attrib.global_notes kind global_facts #> snd) |
402 |
#> 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
|
403 |
|
60341
fcbd7f0c52c3
clearly separated target primitives (target_foo) from self-contained target operations (foo)
haftmann
parents:
60340
diff
changeset
|
404 |
fun theory_target_abbrev prmode (b, mx) global_rhs params = |
47286
392c4cd97e5c
more uniform theory_abbrev with const_declaration;
wenzelm
parents:
47285
diff
changeset
|
405 |
Local_Theory.background_theory_result |
57109 | 406 |
(Sign.add_abbrev (#1 prmode) (b, global_rhs) #-> |
47291
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
47290
diff
changeset
|
407 |
(fn (lhs, _) => (* FIXME type_params!? *) |
63339 | 408 |
Sign.notation true prmode |
409 |
[(lhs, check_mixfix_global (b, null (snd params)) mx)] #> pair lhs)) |
|
62764 | 410 |
#-> (fn lhs => |
411 |
standard_const (op <>) prmode |
|
412 |
((b, if null (snd params) then NoSyn else mx), |
|
413 |
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
|
414 |
|
60341
fcbd7f0c52c3
clearly separated target primitives (target_foo) from self-contained target operations (foo)
haftmann
parents:
60340
diff
changeset
|
415 |
|
74361
690928dd6f8f
apply declarations from interpretations in eigen context also
haftmann
parents:
74284
diff
changeset
|
416 |
|
60341
fcbd7f0c52c3
clearly separated target primitives (target_foo) from self-contained target operations (foo)
haftmann
parents:
60340
diff
changeset
|
417 |
(** theory operations **) |
fcbd7f0c52c3
clearly separated target primitives (target_foo) from self-contained target operations (foo)
haftmann
parents:
60340
diff
changeset
|
418 |
|
60344
a40369ea3ba5
self-contained formulation of abbrev for named targets
haftmann
parents:
60342
diff
changeset
|
419 |
val theory_abbrev = abbrev theory_target_abbrev; |
a40369ea3ba5
self-contained formulation of abbrev for named targets
haftmann
parents:
60342
diff
changeset
|
420 |
|
60341
fcbd7f0c52c3
clearly separated target primitives (target_foo) from self-contained target operations (foo)
haftmann
parents:
60340
diff
changeset
|
421 |
fun theory_declaration decl = |
fcbd7f0c52c3
clearly separated target primitives (target_foo) from self-contained target operations (foo)
haftmann
parents:
60340
diff
changeset
|
422 |
background_declaration decl #> standard_declaration (K true) decl; |
fcbd7f0c52c3
clearly separated target primitives (target_foo) from self-contained target operations (foo)
haftmann
parents:
60340
diff
changeset
|
423 |
|
73846 | 424 |
fun target_registration lthy {inst, mixin, export} = |
425 |
{inst = inst, mixin = mixin, |
|
426 |
export = export $> Proof_Context.export_morphism lthy (Local_Theory.target_of lthy)}; |
|
427 |
||
428 |
fun theory_registration registration lthy = |
|
429 |
lthy |
|
430 |
|> (Local_Theory.raw_theory o Context.theory_map) |
|
431 |
(Locale.add_registration (target_registration lthy registration)) |
|
432 |
|> standard_registration (K true) registration; |
|
73845 | 433 |
|
60283 | 434 |
|
74361
690928dd6f8f
apply declarations from interpretations in eigen context also
haftmann
parents:
74284
diff
changeset
|
435 |
|
60341
fcbd7f0c52c3
clearly separated target primitives (target_foo) from self-contained target operations (foo)
haftmann
parents:
60340
diff
changeset
|
436 |
(** locale target primitives **) |
57190
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
437 |
|
60341
fcbd7f0c52c3
clearly separated target primitives (target_foo) from self-contained target operations (foo)
haftmann
parents:
60340
diff
changeset
|
438 |
fun locale_target_notes locale kind global_facts local_facts = |
57190
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
439 |
Local_Theory.background_theory |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
440 |
(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
|
441 |
(fn lthy => lthy |> |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
442 |
Local_Theory.target (fn ctxt => ctxt |> |
67654 | 443 |
Locale.add_facts locale kind (standard_facts lthy ctxt local_facts))) #> |
57191 | 444 |
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
|
445 |
|
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
|
446 |
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
|
447 |
|> Local_Theory.target (fn ctxt => ctxt |> |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
448 |
Locale.add_declaration locale syntax |
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
449 |
(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
|
450 |
|
60341
fcbd7f0c52c3
clearly separated target primitives (target_foo) from self-contained target operations (foo)
haftmann
parents:
60340
diff
changeset
|
451 |
fun locale_target_const locale phi_pred prmode ((b, mx), rhs) = |
fcbd7f0c52c3
clearly separated target primitives (target_foo) from self-contained target operations (foo)
haftmann
parents:
60340
diff
changeset
|
452 |
locale_target_declaration locale true (const_decl phi_pred prmode ((b, mx), rhs)) |
fcbd7f0c52c3
clearly separated target primitives (target_foo) from self-contained target operations (foo)
haftmann
parents:
60340
diff
changeset
|
453 |
|
fcbd7f0c52c3
clearly separated target primitives (target_foo) from self-contained target operations (foo)
haftmann
parents:
60340
diff
changeset
|
454 |
|
fcbd7f0c52c3
clearly separated target primitives (target_foo) from self-contained target operations (foo)
haftmann
parents:
60340
diff
changeset
|
455 |
(** locale operations **) |
fcbd7f0c52c3
clearly separated target primitives (target_foo) from self-contained target operations (foo)
haftmann
parents:
60340
diff
changeset
|
456 |
|
57193 | 457 |
fun locale_declaration locale {syntax, pervasive} decl = |
458 |
pervasive ? background_declaration decl |
|
459 |
#> locale_target_declaration locale syntax decl |
|
460 |
#> standard_declaration (fn (_, other) => other <> 0) decl; |
|
461 |
||
57190
05ad9aae4537
recovered structure of module, which got somehow convoluted due to incremental modifications
haftmann
parents:
57189
diff
changeset
|
462 |
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
|
463 |
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
|
464 |
#> 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
|
465 |
|
73846 | 466 |
fun locale_dependency loc registration lthy = |
467 |
lthy |
|
468 |
|> Local_Theory.raw_theory (Locale.add_dependency loc registration) |
|
469 |
|> standard_registration (K true) registration; |
|
73845 | 470 |
|
60344
a40369ea3ba5
self-contained formulation of abbrev for named targets
haftmann
parents:
60342
diff
changeset
|
471 |
|
a40369ea3ba5
self-contained formulation of abbrev for named targets
haftmann
parents:
60342
diff
changeset
|
472 |
(** locale abbreviations **) |
a40369ea3ba5
self-contained formulation of abbrev for named targets
haftmann
parents:
60342
diff
changeset
|
473 |
|
a40369ea3ba5
self-contained formulation of abbrev for named targets
haftmann
parents:
60342
diff
changeset
|
474 |
fun locale_target_abbrev locale prmode (b, mx) global_rhs params = |
a40369ea3ba5
self-contained formulation of abbrev for named targets
haftmann
parents:
60342
diff
changeset
|
475 |
background_abbrev (b, global_rhs) (snd params) |
a40369ea3ba5
self-contained formulation of abbrev for named targets
haftmann
parents:
60342
diff
changeset
|
476 |
#-> (fn (lhs, _) => locale_const locale prmode ((b, mx), lhs)); |
a40369ea3ba5
self-contained formulation of abbrev for named targets
haftmann
parents:
60342
diff
changeset
|
477 |
|
a40369ea3ba5
self-contained formulation of abbrev for named targets
haftmann
parents:
60342
diff
changeset
|
478 |
fun locale_abbrev locale = abbrev (locale_target_abbrev locale); |
a40369ea3ba5
self-contained formulation of abbrev for named targets
haftmann
parents:
60342
diff
changeset
|
479 |
|
38309 | 480 |
end; |