author | wenzelm |
Sat, 27 Sep 2008 15:20:39 +0200 | |
changeset 28379 | 0de8a35b866a |
parent 28115 | cd0d170d4dc6 |
child 28395 | 984fcc8feb24 |
permissions | -rw-r--r-- |
18744 | 1 |
(* Title: Pure/Isar/local_theory.ML |
2 |
ID: $Id$ |
|
3 |
Author: Makarius |
|
4 |
||
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
5 |
Local theory operations, with abstract target context. |
18744 | 6 |
*) |
7 |
||
18951 | 8 |
type local_theory = Proof.context; |
9 |
||
18744 | 10 |
signature LOCAL_THEORY = |
11 |
sig |
|
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
12 |
type operations |
26131
91024979b9eb
maintain group in lthy data, implicit use in operations;
wenzelm
parents:
25984
diff
changeset
|
13 |
val group_of: local_theory -> string |
28017 | 14 |
val group_properties_of: local_theory -> Properties.T |
15 |
val group_position_of: local_theory -> Properties.T |
|
26131
91024979b9eb
maintain group in lthy data, implicit use in operations;
wenzelm
parents:
25984
diff
changeset
|
16 |
val set_group: string -> local_theory -> local_theory |
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
17 |
val target_of: local_theory -> Proof.context |
20960 | 18 |
val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory |
19 |
val raw_theory: (theory -> theory) -> local_theory -> local_theory |
|
28379
0de8a35b866a
Theory.checkpoint for main operations, admits concurrent proofs;
wenzelm
parents:
28115
diff
changeset
|
20 |
val checkpoint: local_theory -> local_theory |
22240 | 21 |
val full_naming: local_theory -> NameSpace.naming |
21614 | 22 |
val full_name: local_theory -> bstring -> string |
20960 | 23 |
val theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory |
18951 | 24 |
val theory: (theory -> theory) -> local_theory -> local_theory |
20960 | 25 |
val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory |
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
26 |
val target: (Proof.context -> Proof.context) -> local_theory -> local_theory |
21860 | 27 |
val affirm: local_theory -> local_theory |
20960 | 28 |
val pretty: local_theory -> Pretty.T list |
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
28017
diff
changeset
|
29 |
val abbrev: Syntax.mode -> (Name.binding * mixfix) * term -> local_theory -> |
25120 | 30 |
(term * term) * local_theory |
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset
|
31 |
val define: string -> (Name.binding * mixfix) * (Attrib.binding * term) -> local_theory -> |
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
28017
diff
changeset
|
32 |
(term * (string * thm)) * local_theory |
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset
|
33 |
val note: string -> Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory |
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset
|
34 |
val notes: string -> (Attrib.binding * (thm list * Attrib.src list) list) list -> |
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
28017
diff
changeset
|
35 |
local_theory -> (string * thm list) list * local_theory |
24020 | 36 |
val type_syntax: declaration -> local_theory -> local_theory |
37 |
val term_syntax: declaration -> local_theory -> local_theory |
|
38 |
val declaration: declaration -> local_theory -> local_theory |
|
24949 | 39 |
val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory |
21529 | 40 |
val target_morphism: local_theory -> morphism |
41 |
val init: string -> operations -> Proof.context -> local_theory |
|
21273 | 42 |
val restore: local_theory -> local_theory |
25289 | 43 |
val reinit: local_theory -> local_theory |
21292 | 44 |
val exit: local_theory -> Proof.context |
18744 | 45 |
end; |
46 |
||
47 |
structure LocalTheory: LOCAL_THEORY = |
|
48 |
struct |
|
49 |
||
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
50 |
(** local theory data **) |
19059
b4ca3100e818
init/exit no longer change the theory (no naming);
wenzelm
parents:
19032
diff
changeset
|
51 |
|
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
52 |
(* type lthy *) |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
53 |
|
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
54 |
type operations = |
20960 | 55 |
{pretty: local_theory -> Pretty.T list, |
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset
|
56 |
abbrev: Syntax.mode -> (Name.binding * mixfix) * term -> local_theory -> |
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset
|
57 |
(term * term) * local_theory, |
26131
91024979b9eb
maintain group in lthy data, implicit use in operations;
wenzelm
parents:
25984
diff
changeset
|
58 |
define: string -> |
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset
|
59 |
(Name.binding * mixfix) * (Attrib.binding * term) -> local_theory -> |
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
28017
diff
changeset
|
60 |
(term * (string * thm)) * local_theory, |
26131
91024979b9eb
maintain group in lthy data, implicit use in operations;
wenzelm
parents:
25984
diff
changeset
|
61 |
notes: string -> |
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset
|
62 |
(Attrib.binding * (thm list * Attrib.src list) list) list -> |
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
28017
diff
changeset
|
63 |
local_theory -> (string * thm list) list * local_theory, |
24020 | 64 |
type_syntax: declaration -> local_theory -> local_theory, |
65 |
term_syntax: declaration -> local_theory -> local_theory, |
|
66 |
declaration: declaration -> local_theory -> local_theory, |
|
25289 | 67 |
reinit: local_theory -> local_theory, |
21292 | 68 |
exit: local_theory -> Proof.context}; |
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
69 |
|
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
70 |
datatype lthy = LThy of |
26131
91024979b9eb
maintain group in lthy data, implicit use in operations;
wenzelm
parents:
25984
diff
changeset
|
71 |
{group: string, |
91024979b9eb
maintain group in lthy data, implicit use in operations;
wenzelm
parents:
25984
diff
changeset
|
72 |
theory_prefix: string, |
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
73 |
operations: operations, |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
74 |
target: Proof.context}; |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
75 |
|
26131
91024979b9eb
maintain group in lthy data, implicit use in operations;
wenzelm
parents:
25984
diff
changeset
|
76 |
fun make_lthy (group, theory_prefix, operations, target) = |
91024979b9eb
maintain group in lthy data, implicit use in operations;
wenzelm
parents:
25984
diff
changeset
|
77 |
LThy {group = group, theory_prefix = theory_prefix, operations = operations, target = target}; |
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
78 |
|
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
79 |
|
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
80 |
(* context data *) |
18744 | 81 |
|
82 |
structure Data = ProofDataFun |
|
83 |
( |
|
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
84 |
type T = lthy option; |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
85 |
fun init _ = NONE; |
18744 | 86 |
); |
87 |
||
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
88 |
fun get_lthy lthy = |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
89 |
(case Data.get lthy of |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
90 |
NONE => error "No local theory context" |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
91 |
| SOME (LThy data) => data); |
18951 | 92 |
|
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
93 |
fun map_lthy f lthy = |
26131
91024979b9eb
maintain group in lthy data, implicit use in operations;
wenzelm
parents:
25984
diff
changeset
|
94 |
let val {group, theory_prefix, operations, target} = get_lthy lthy |
91024979b9eb
maintain group in lthy data, implicit use in operations;
wenzelm
parents:
25984
diff
changeset
|
95 |
in Data.put (SOME (make_lthy (f (group, theory_prefix, operations, target)))) lthy end; |
91024979b9eb
maintain group in lthy data, implicit use in operations;
wenzelm
parents:
25984
diff
changeset
|
96 |
|
91024979b9eb
maintain group in lthy data, implicit use in operations;
wenzelm
parents:
25984
diff
changeset
|
97 |
|
91024979b9eb
maintain group in lthy data, implicit use in operations;
wenzelm
parents:
25984
diff
changeset
|
98 |
(* group *) |
91024979b9eb
maintain group in lthy data, implicit use in operations;
wenzelm
parents:
25984
diff
changeset
|
99 |
|
91024979b9eb
maintain group in lthy data, implicit use in operations;
wenzelm
parents:
25984
diff
changeset
|
100 |
val group_of = #group o get_lthy; |
91024979b9eb
maintain group in lthy data, implicit use in operations;
wenzelm
parents:
25984
diff
changeset
|
101 |
|
91024979b9eb
maintain group in lthy data, implicit use in operations;
wenzelm
parents:
25984
diff
changeset
|
102 |
fun group_properties_of lthy = |
91024979b9eb
maintain group in lthy data, implicit use in operations;
wenzelm
parents:
25984
diff
changeset
|
103 |
(case group_of lthy of |
91024979b9eb
maintain group in lthy data, implicit use in operations;
wenzelm
parents:
25984
diff
changeset
|
104 |
"" => [] |
91024979b9eb
maintain group in lthy data, implicit use in operations;
wenzelm
parents:
25984
diff
changeset
|
105 |
| group => [(Markup.groupN, group)]); |
91024979b9eb
maintain group in lthy data, implicit use in operations;
wenzelm
parents:
25984
diff
changeset
|
106 |
|
91024979b9eb
maintain group in lthy data, implicit use in operations;
wenzelm
parents:
25984
diff
changeset
|
107 |
fun group_position_of lthy = |
91024979b9eb
maintain group in lthy data, implicit use in operations;
wenzelm
parents:
25984
diff
changeset
|
108 |
group_properties_of lthy @ Position.properties_of (Position.thread_data ()); |
91024979b9eb
maintain group in lthy data, implicit use in operations;
wenzelm
parents:
25984
diff
changeset
|
109 |
|
91024979b9eb
maintain group in lthy data, implicit use in operations;
wenzelm
parents:
25984
diff
changeset
|
110 |
fun set_group group = map_lthy (fn (_, theory_prefix, operations, target) => |
91024979b9eb
maintain group in lthy data, implicit use in operations;
wenzelm
parents:
25984
diff
changeset
|
111 |
(group, theory_prefix, operations, target)); |
91024979b9eb
maintain group in lthy data, implicit use in operations;
wenzelm
parents:
25984
diff
changeset
|
112 |
|
91024979b9eb
maintain group in lthy data, implicit use in operations;
wenzelm
parents:
25984
diff
changeset
|
113 |
|
91024979b9eb
maintain group in lthy data, implicit use in operations;
wenzelm
parents:
25984
diff
changeset
|
114 |
(* target *) |
18767 | 115 |
|
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
116 |
val target_of = #target o get_lthy; |
21860 | 117 |
val affirm = tap target_of; |
18767 | 118 |
|
26131
91024979b9eb
maintain group in lthy data, implicit use in operations;
wenzelm
parents:
25984
diff
changeset
|
119 |
fun map_target f = map_lthy (fn (group, theory_prefix, operations, target) => |
91024979b9eb
maintain group in lthy data, implicit use in operations;
wenzelm
parents:
25984
diff
changeset
|
120 |
(group, theory_prefix, operations, f target)); |
18767 | 121 |
|
122 |
||
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
123 |
(* substructure mappings *) |
19661 | 124 |
|
20960 | 125 |
fun raw_theory_result f lthy = |
126 |
let |
|
127 |
val (res, thy') = f (ProofContext.theory_of lthy); |
|
128 |
val lthy' = lthy |
|
129 |
|> map_target (ProofContext.transfer thy') |
|
130 |
|> ProofContext.transfer thy'; |
|
131 |
in (res, lthy') end; |
|
132 |
||
133 |
fun raw_theory f = #2 o raw_theory_result (f #> pair ()); |
|
134 |
||
28379
0de8a35b866a
Theory.checkpoint for main operations, admits concurrent proofs;
wenzelm
parents:
28115
diff
changeset
|
135 |
val checkpoint = raw_theory Theory.checkpoint; |
0de8a35b866a
Theory.checkpoint for main operations, admits concurrent proofs;
wenzelm
parents:
28115
diff
changeset
|
136 |
|
22240 | 137 |
fun full_naming lthy = |
138 |
Sign.naming_of (ProofContext.theory_of lthy) |
|
139 |
|> NameSpace.sticky_prefix (#theory_prefix (get_lthy lthy)) |
|
140 |
|> NameSpace.qualified_names; |
|
141 |
||
142 |
val full_name = NameSpace.full o full_naming; |
|
21614 | 143 |
|
21529 | 144 |
fun theory_result f lthy = lthy |> raw_theory_result (fn thy => thy |
145 |
|> Sign.sticky_prefix (#theory_prefix (get_lthy lthy)) |
|
146 |
|> Sign.qualified_names |
|
147 |
|> f |
|
148 |
||> Sign.restore_naming thy); |
|
19661 | 149 |
|
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
150 |
fun theory f = #2 o theory_result (f #> pair ()); |
19661 | 151 |
|
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
152 |
fun target_result f lthy = |
18744 | 153 |
let |
26131
91024979b9eb
maintain group in lthy data, implicit use in operations;
wenzelm
parents:
25984
diff
changeset
|
154 |
val (res, ctxt') = f (target_of lthy); |
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
155 |
val thy' = ProofContext.theory_of ctxt'; |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
156 |
val lthy' = lthy |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
157 |
|> map_target (K ctxt') |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
158 |
|> ProofContext.transfer thy'; |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
159 |
in (res, lthy') end; |
18876 | 160 |
|
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
161 |
fun target f = #2 o target_result (f #> pair ()); |
18767 | 162 |
|
163 |
||
21664
dd4e89123359
notation/abbreviation: more serious handling of morphisms;
wenzelm
parents:
21614
diff
changeset
|
164 |
(* basic operations *) |
18781 | 165 |
|
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
166 |
fun operation f lthy = f (#operations (get_lthy lthy)) lthy; |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
167 |
fun operation1 f x = operation (fn ops => f ops x); |
26131
91024979b9eb
maintain group in lthy data, implicit use in operations;
wenzelm
parents:
25984
diff
changeset
|
168 |
fun operation2 f x y lthy = operation (fn ops => f ops x y) lthy; |
18781 | 169 |
|
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
170 |
val pretty = operation #pretty; |
28379
0de8a35b866a
Theory.checkpoint for main operations, admits concurrent proofs;
wenzelm
parents:
28115
diff
changeset
|
171 |
val abbrev = apsnd checkpoint ooo operation2 #abbrev; |
0de8a35b866a
Theory.checkpoint for main operations, admits concurrent proofs;
wenzelm
parents:
28115
diff
changeset
|
172 |
val define = apsnd checkpoint ooo operation2 #define; |
0de8a35b866a
Theory.checkpoint for main operations, admits concurrent proofs;
wenzelm
parents:
28115
diff
changeset
|
173 |
val notes = apsnd checkpoint ooo operation2 #notes; |
0de8a35b866a
Theory.checkpoint for main operations, admits concurrent proofs;
wenzelm
parents:
28115
diff
changeset
|
174 |
val type_syntax = checkpoint oo operation1 #type_syntax; |
0de8a35b866a
Theory.checkpoint for main operations, admits concurrent proofs;
wenzelm
parents:
28115
diff
changeset
|
175 |
val term_syntax = checkpoint oo operation1 #term_syntax; |
0de8a35b866a
Theory.checkpoint for main operations, admits concurrent proofs;
wenzelm
parents:
28115
diff
changeset
|
176 |
val declaration = checkpoint oo operation1 #declaration; |
18781 | 177 |
|
26131
91024979b9eb
maintain group in lthy data, implicit use in operations;
wenzelm
parents:
25984
diff
changeset
|
178 |
fun note kind (a, ths) = notes kind [(a, [(ths, [])])] #>> the_single; |
18781 | 179 |
|
24933
5471b164813b
removed LocalTheory.defs/target_morphism operations;
wenzelm
parents:
24554
diff
changeset
|
180 |
fun target_morphism lthy = |
5471b164813b
removed LocalTheory.defs/target_morphism operations;
wenzelm
parents:
24554
diff
changeset
|
181 |
ProofContext.export_morphism lthy (target_of lthy) $> |
5471b164813b
removed LocalTheory.defs/target_morphism operations;
wenzelm
parents:
24554
diff
changeset
|
182 |
Morphism.thm_morphism Goal.norm_result; |
5471b164813b
removed LocalTheory.defs/target_morphism operations;
wenzelm
parents:
24554
diff
changeset
|
183 |
|
24949 | 184 |
fun notation add mode raw_args lthy = |
21743 | 185 |
let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args |
24949 | 186 |
in term_syntax (ProofContext.target_notation add mode args) lthy end; |
21743 | 187 |
|
21664
dd4e89123359
notation/abbreviation: more serious handling of morphisms;
wenzelm
parents:
21614
diff
changeset
|
188 |
|
20910 | 189 |
(* init -- exit *) |
190 |
||
191 |
fun init theory_prefix operations target = target |> Data.map |
|
26131
91024979b9eb
maintain group in lthy data, implicit use in operations;
wenzelm
parents:
25984
diff
changeset
|
192 |
(fn NONE => SOME (make_lthy ("", theory_prefix, operations, target)) |
28379
0de8a35b866a
Theory.checkpoint for main operations, admits concurrent proofs;
wenzelm
parents:
28115
diff
changeset
|
193 |
| SOME _ => error "Local theory already initialized") |
0de8a35b866a
Theory.checkpoint for main operations, admits concurrent proofs;
wenzelm
parents:
28115
diff
changeset
|
194 |
|> checkpoint; |
20910 | 195 |
|
21273 | 196 |
fun restore lthy = |
26131
91024979b9eb
maintain group in lthy data, implicit use in operations;
wenzelm
parents:
25984
diff
changeset
|
197 |
let val {group = _, theory_prefix, operations, target} = get_lthy lthy |
20910 | 198 |
in init theory_prefix operations target end; |
199 |
||
28379
0de8a35b866a
Theory.checkpoint for main operations, admits concurrent proofs;
wenzelm
parents:
28115
diff
changeset
|
200 |
val reinit = checkpoint o operation #reinit; |
0de8a35b866a
Theory.checkpoint for main operations, admits concurrent proofs;
wenzelm
parents:
28115
diff
changeset
|
201 |
val exit = ProofContext.theory Theory.checkpoint o operation #exit; |
20910 | 202 |
|
18781 | 203 |
end; |