author | wenzelm |
Sat, 28 Jul 2007 22:01:06 +0200 | |
changeset 24031 | e94e541346d7 |
parent 24020 | ed4d7abffee7 |
child 24554 | e9edafca311c |
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 |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
13 |
val target_of: local_theory -> Proof.context |
20960 | 14 |
val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory |
15 |
val raw_theory: (theory -> theory) -> local_theory -> local_theory |
|
22240 | 16 |
val full_naming: local_theory -> NameSpace.naming |
21614 | 17 |
val full_name: local_theory -> bstring -> string |
20960 | 18 |
val theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory |
18951 | 19 |
val theory: (theory -> theory) -> local_theory -> local_theory |
20960 | 20 |
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
|
21 |
val target: (Proof.context -> Proof.context) -> local_theory -> local_theory |
21860 | 22 |
val affirm: local_theory -> local_theory |
20960 | 23 |
val pretty: local_theory -> Pretty.T list |
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
24 |
val consts: (string * typ -> bool) -> |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
25 |
((bstring * typ) * mixfix) list -> local_theory -> (term * thm) list * local_theory |
21433 | 26 |
val axioms: string -> ((bstring * Attrib.src list) * term list) list -> local_theory -> |
18951 | 27 |
(bstring * thm list) list * local_theory |
21802 | 28 |
val abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory -> |
29 |
(term * term) * local_theory |
|
21433 | 30 |
val defs: string -> ((bstring * mixfix) * ((bstring * Attrib.src list) * term)) list -> |
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
31 |
local_theory -> (term * (bstring * thm)) list * local_theory |
21433 | 32 |
val notes: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list -> |
18951 | 33 |
local_theory -> (bstring * thm list) list * local_theory |
24020 | 34 |
val type_syntax: declaration -> local_theory -> local_theory |
35 |
val term_syntax: declaration -> local_theory -> local_theory |
|
36 |
val declaration: declaration -> local_theory -> local_theory |
|
21433 | 37 |
val def: string -> (bstring * mixfix) * ((bstring * Attrib.src list) * term) -> |
18951 | 38 |
local_theory -> (term * (bstring * thm)) * local_theory |
21433 | 39 |
val note: string -> (bstring * Attrib.src list) * thm list -> |
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
40 |
local_theory -> (bstring * thm list) * Proof.context |
21743 | 41 |
val notation: Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory |
21529 | 42 |
val target_morphism: local_theory -> morphism |
22203 | 43 |
val target_naming: local_theory -> NameSpace.naming |
21529 | 44 |
val target_name: local_theory -> bstring -> string |
45 |
val init: string -> operations -> Proof.context -> local_theory |
|
21273 | 46 |
val restore: local_theory -> local_theory |
21292 | 47 |
val reinit: local_theory -> theory -> local_theory |
48 |
val exit: local_theory -> Proof.context |
|
18744 | 49 |
end; |
50 |
||
51 |
structure LocalTheory: LOCAL_THEORY = |
|
52 |
struct |
|
53 |
||
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
54 |
(** local theory data **) |
19059
b4ca3100e818
init/exit no longer change the theory (no naming);
wenzelm
parents:
19032
diff
changeset
|
55 |
|
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
56 |
(* type lthy *) |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
57 |
|
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
58 |
type operations = |
20960 | 59 |
{pretty: local_theory -> Pretty.T list, |
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
60 |
consts: (string * typ -> bool) -> ((bstring * typ) * mixfix) list -> local_theory -> |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
61 |
(term * thm) list * local_theory, |
21433 | 62 |
axioms: string -> ((bstring * Attrib.src list) * term list) list -> local_theory -> |
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
63 |
(bstring * thm list) list * local_theory, |
21802 | 64 |
abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory -> (term * term) * local_theory, |
21433 | 65 |
defs: string -> ((bstring * mixfix) * ((bstring * Attrib.src list) * term)) list -> |
66 |
local_theory -> (term * (bstring * thm)) list * local_theory, |
|
67 |
notes: string -> |
|
68 |
((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list -> |
|
69 |
local_theory -> (bstring * thm list) list * local_theory, |
|
24020 | 70 |
type_syntax: declaration -> local_theory -> local_theory, |
71 |
term_syntax: declaration -> local_theory -> local_theory, |
|
72 |
declaration: declaration -> local_theory -> local_theory, |
|
21529 | 73 |
target_morphism: local_theory -> morphism, |
22203 | 74 |
target_naming: local_theory -> NameSpace.naming, |
21292 | 75 |
reinit: local_theory -> theory -> local_theory, |
76 |
exit: local_theory -> Proof.context}; |
|
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
77 |
|
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
78 |
datatype lthy = LThy of |
21529 | 79 |
{theory_prefix: string, |
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
80 |
operations: operations, |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
81 |
target: Proof.context}; |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
82 |
|
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
83 |
fun make_lthy (theory_prefix, operations, target) = |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
84 |
LThy {theory_prefix = theory_prefix, operations = operations, target = target}; |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
85 |
|
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
86 |
|
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
87 |
(* context data *) |
18744 | 88 |
|
89 |
structure Data = ProofDataFun |
|
90 |
( |
|
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
91 |
type T = lthy option; |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
92 |
fun init _ = NONE; |
18744 | 93 |
); |
94 |
||
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
95 |
fun get_lthy lthy = |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
96 |
(case Data.get lthy of |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
97 |
NONE => error "No local theory context" |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
98 |
| SOME (LThy data) => data); |
18951 | 99 |
|
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
100 |
fun map_lthy f lthy = |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
101 |
let val {theory_prefix, operations, target} = get_lthy lthy |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
102 |
in Data.put (SOME (make_lthy (f (theory_prefix, operations, target)))) lthy end; |
18767 | 103 |
|
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
104 |
val target_of = #target o get_lthy; |
21860 | 105 |
val affirm = tap target_of; |
18767 | 106 |
|
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
107 |
fun map_target f = map_lthy (fn (theory_prefix, operations, target) => |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
108 |
(theory_prefix, operations, f target)); |
18767 | 109 |
|
110 |
||
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
111 |
(* substructure mappings *) |
19661 | 112 |
|
20960 | 113 |
fun raw_theory_result f lthy = |
114 |
let |
|
115 |
val (res, thy') = f (ProofContext.theory_of lthy); |
|
116 |
val lthy' = lthy |
|
117 |
|> map_target (ProofContext.transfer thy') |
|
118 |
|> ProofContext.transfer thy'; |
|
119 |
in (res, lthy') end; |
|
120 |
||
121 |
fun raw_theory f = #2 o raw_theory_result (f #> pair ()); |
|
122 |
||
22240 | 123 |
fun full_naming lthy = |
124 |
Sign.naming_of (ProofContext.theory_of lthy) |
|
125 |
|> NameSpace.sticky_prefix (#theory_prefix (get_lthy lthy)) |
|
126 |
|> NameSpace.qualified_names; |
|
127 |
||
128 |
val full_name = NameSpace.full o full_naming; |
|
21614 | 129 |
|
21529 | 130 |
fun theory_result f lthy = lthy |> raw_theory_result (fn thy => thy |
131 |
|> Sign.sticky_prefix (#theory_prefix (get_lthy lthy)) |
|
132 |
|> Sign.qualified_names |
|
133 |
|> f |
|
134 |
||> Sign.restore_naming thy); |
|
19661 | 135 |
|
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
136 |
fun theory f = #2 o theory_result (f #> pair ()); |
19661 | 137 |
|
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
138 |
fun target_result f lthy = |
18744 | 139 |
let |
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
140 |
val (res, ctxt') = f (#target (get_lthy lthy)); |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
141 |
val thy' = ProofContext.theory_of ctxt'; |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
142 |
val lthy' = lthy |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
143 |
|> map_target (K ctxt') |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
144 |
|> ProofContext.transfer thy'; |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
145 |
in (res, lthy') end; |
18876 | 146 |
|
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
147 |
fun target f = #2 o target_result (f #> pair ()); |
18767 | 148 |
|
149 |
||
21664
dd4e89123359
notation/abbreviation: more serious handling of morphisms;
wenzelm
parents:
21614
diff
changeset
|
150 |
(* basic operations *) |
18781 | 151 |
|
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
152 |
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
|
153 |
fun operation1 f x = operation (fn ops => f ops x); |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
154 |
fun operation2 f x y = operation (fn ops => f ops x y); |
18781 | 155 |
|
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
156 |
val pretty = operation #pretty; |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
157 |
val consts = operation2 #consts; |
21433 | 158 |
val axioms = operation2 #axioms; |
21743 | 159 |
val abbrev = operation2 #abbrev; |
21433 | 160 |
val defs = operation2 #defs; |
161 |
val notes = operation2 #notes; |
|
21498
6382c3a1e7cf
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21433
diff
changeset
|
162 |
val type_syntax = operation1 #type_syntax; |
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
163 |
val term_syntax = operation1 #term_syntax; |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
164 |
val declaration = operation1 #declaration; |
21529 | 165 |
val target_morphism = operation #target_morphism; |
22203 | 166 |
val target_naming = operation #target_naming; |
18781 | 167 |
|
21433 | 168 |
fun def kind arg lthy = lthy |> defs kind [arg] |>> hd; |
169 |
fun note kind (a, ths) lthy = lthy |> notes kind [(a, [(ths, [])])] |>> hd; |
|
18781 | 170 |
|
21743 | 171 |
fun notation mode raw_args lthy = |
172 |
let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args |
|
173 |
in term_syntax (ProofContext.target_notation mode args) lthy end; |
|
174 |
||
22203 | 175 |
val target_name = NameSpace.full o target_naming; |
176 |
||
21664
dd4e89123359
notation/abbreviation: more serious handling of morphisms;
wenzelm
parents:
21614
diff
changeset
|
177 |
|
20910 | 178 |
(* init -- exit *) |
179 |
||
180 |
fun init theory_prefix operations target = target |> Data.map |
|
181 |
(fn NONE => SOME (make_lthy (theory_prefix, operations, target)) |
|
182 |
| SOME _ => error "Local theory already initialized"); |
|
183 |
||
21273 | 184 |
fun restore lthy = |
20910 | 185 |
let val {theory_prefix, operations, target} = get_lthy lthy |
186 |
in init theory_prefix operations target end; |
|
187 |
||
21292 | 188 |
val reinit = operation #reinit; |
189 |
val exit = operation #exit; |
|
20910 | 190 |
|
18781 | 191 |
end; |