author | wenzelm |
Sun, 04 Feb 2007 22:02:20 +0100 | |
changeset 22240 | 36cc1875619f |
parent 22203 | efc0cdc01307 |
child 22846 | fb79144af9a3 |
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 |
21498
6382c3a1e7cf
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21433
diff
changeset
|
34 |
val type_syntax: (morphism -> Context.generic -> Context.generic) -> local_theory -> local_theory |
6382c3a1e7cf
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21433
diff
changeset
|
35 |
val term_syntax: (morphism -> Context.generic -> Context.generic) -> local_theory -> local_theory |
6382c3a1e7cf
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21433
diff
changeset
|
36 |
val declaration: (morphism -> Context.generic -> Context.generic) -> 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, |
|
21498
6382c3a1e7cf
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21433
diff
changeset
|
70 |
type_syntax: (morphism -> Context.generic -> Context.generic) -> local_theory -> local_theory, |
6382c3a1e7cf
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21433
diff
changeset
|
71 |
term_syntax: (morphism -> Context.generic -> Context.generic) -> local_theory -> local_theory, |
6382c3a1e7cf
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21433
diff
changeset
|
72 |
declaration: (morphism -> Context.generic -> Context.generic) -> 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 |
( |
|
18876 | 91 |
val name = "Pure/local_theory"; |
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
92 |
type T = lthy option; |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
93 |
fun init _ = NONE; |
18744 | 94 |
fun print _ _ = (); |
95 |
); |
|
96 |
val _ = Context.add_setup Data.init; |
|
97 |
||
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
98 |
fun get_lthy lthy = |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
99 |
(case Data.get lthy of |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
100 |
NONE => error "No local theory context" |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
101 |
| SOME (LThy data) => data); |
18951 | 102 |
|
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
103 |
fun map_lthy f lthy = |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
104 |
let val {theory_prefix, operations, target} = get_lthy lthy |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
105 |
in Data.put (SOME (make_lthy (f (theory_prefix, operations, target)))) lthy end; |
18767 | 106 |
|
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
107 |
val target_of = #target o get_lthy; |
21860 | 108 |
val affirm = tap target_of; |
18767 | 109 |
|
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
110 |
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
|
111 |
(theory_prefix, operations, f target)); |
18767 | 112 |
|
113 |
||
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
114 |
(* substructure mappings *) |
19661 | 115 |
|
20960 | 116 |
fun raw_theory_result f lthy = |
117 |
let |
|
118 |
val (res, thy') = f (ProofContext.theory_of lthy); |
|
119 |
val lthy' = lthy |
|
120 |
|> map_target (ProofContext.transfer thy') |
|
121 |
|> ProofContext.transfer thy'; |
|
122 |
in (res, lthy') end; |
|
123 |
||
124 |
fun raw_theory f = #2 o raw_theory_result (f #> pair ()); |
|
125 |
||
22240 | 126 |
fun full_naming lthy = |
127 |
Sign.naming_of (ProofContext.theory_of lthy) |
|
128 |
|> NameSpace.sticky_prefix (#theory_prefix (get_lthy lthy)) |
|
129 |
|> NameSpace.qualified_names; |
|
130 |
||
131 |
val full_name = NameSpace.full o full_naming; |
|
21614 | 132 |
|
21529 | 133 |
fun theory_result f lthy = lthy |> raw_theory_result (fn thy => thy |
134 |
|> Sign.sticky_prefix (#theory_prefix (get_lthy lthy)) |
|
135 |
|> Sign.qualified_names |
|
136 |
|> f |
|
137 |
||> Sign.restore_naming thy); |
|
19661 | 138 |
|
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
139 |
fun theory f = #2 o theory_result (f #> pair ()); |
19661 | 140 |
|
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
141 |
fun target_result f lthy = |
18744 | 142 |
let |
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
143 |
val (res, ctxt') = f (#target (get_lthy lthy)); |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
144 |
val thy' = ProofContext.theory_of ctxt'; |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
145 |
val lthy' = lthy |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
146 |
|> map_target (K ctxt') |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
147 |
|> ProofContext.transfer thy'; |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
148 |
in (res, lthy') end; |
18876 | 149 |
|
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
150 |
fun target f = #2 o target_result (f #> pair ()); |
18767 | 151 |
|
152 |
||
21664
dd4e89123359
notation/abbreviation: more serious handling of morphisms;
wenzelm
parents:
21614
diff
changeset
|
153 |
(* basic operations *) |
18781 | 154 |
|
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
155 |
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
|
156 |
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
|
157 |
fun operation2 f x y = operation (fn ops => f ops x y); |
18781 | 158 |
|
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
159 |
val pretty = operation #pretty; |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
160 |
val consts = operation2 #consts; |
21433 | 161 |
val axioms = operation2 #axioms; |
21743 | 162 |
val abbrev = operation2 #abbrev; |
21433 | 163 |
val defs = operation2 #defs; |
164 |
val notes = operation2 #notes; |
|
21498
6382c3a1e7cf
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21433
diff
changeset
|
165 |
val type_syntax = operation1 #type_syntax; |
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
166 |
val term_syntax = operation1 #term_syntax; |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
167 |
val declaration = operation1 #declaration; |
21529 | 168 |
val target_morphism = operation #target_morphism; |
22203 | 169 |
val target_naming = operation #target_naming; |
18781 | 170 |
|
21433 | 171 |
fun def kind arg lthy = lthy |> defs kind [arg] |>> hd; |
172 |
fun note kind (a, ths) lthy = lthy |> notes kind [(a, [(ths, [])])] |>> hd; |
|
18781 | 173 |
|
21743 | 174 |
fun notation mode raw_args lthy = |
175 |
let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args |
|
176 |
in term_syntax (ProofContext.target_notation mode args) lthy end; |
|
177 |
||
22203 | 178 |
val target_name = NameSpace.full o target_naming; |
179 |
||
21664
dd4e89123359
notation/abbreviation: more serious handling of morphisms;
wenzelm
parents:
21614
diff
changeset
|
180 |
|
20910 | 181 |
(* init -- exit *) |
182 |
||
183 |
fun init theory_prefix operations target = target |> Data.map |
|
184 |
(fn NONE => SOME (make_lthy (theory_prefix, operations, target)) |
|
185 |
| SOME _ => error "Local theory already initialized"); |
|
186 |
||
21273 | 187 |
fun restore lthy = |
20910 | 188 |
let val {theory_prefix, operations, target} = get_lthy lthy |
189 |
in init theory_prefix operations target end; |
|
190 |
||
21292 | 191 |
val reinit = operation #reinit; |
192 |
val exit = operation #exit; |
|
20910 | 193 |
|
18781 | 194 |
end; |