author | wenzelm |
Sun, 26 Nov 2006 18:07:24 +0100 | |
changeset 21529 | bfe99f603933 |
parent 21498 | 6382c3a1e7cf |
child 21614 | 89105c15b436 |
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 |
|
16 |
val theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory |
|
18951 | 17 |
val theory: (theory -> theory) -> local_theory -> local_theory |
20960 | 18 |
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
|
19 |
val target: (Proof.context -> Proof.context) -> local_theory -> local_theory |
21034 | 20 |
val assert: local_theory -> local_theory |
20960 | 21 |
val pretty: local_theory -> Pretty.T list |
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
22 |
val consts: (string * typ -> bool) -> |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
23 |
((bstring * typ) * mixfix) list -> local_theory -> (term * thm) list * local_theory |
21433 | 24 |
val axioms: string -> ((bstring * Attrib.src list) * term list) list -> local_theory -> |
18951 | 25 |
(bstring * thm list) list * local_theory |
21433 | 26 |
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
|
27 |
local_theory -> (term * (bstring * thm)) list * local_theory |
21433 | 28 |
val notes: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list -> |
18951 | 29 |
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
|
30 |
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
|
31 |
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
|
32 |
val declaration: (morphism -> Context.generic -> Context.generic) -> local_theory -> local_theory |
21433 | 33 |
val def: string -> (bstring * mixfix) * ((bstring * Attrib.src list) * term) -> |
18951 | 34 |
local_theory -> (term * (bstring * thm)) * local_theory |
21433 | 35 |
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
|
36 |
local_theory -> (bstring * thm list) * Proof.context |
21206
2af4c7b3f7ef
replaced const_syntax by notation, which operates on terms;
wenzelm
parents:
21034
diff
changeset
|
37 |
val notation: Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory |
21529 | 38 |
val abbrevs: Syntax.mode -> ((bstring * mixfix) * term) list -> local_theory -> local_theory |
39 |
val target_morphism: local_theory -> morphism |
|
40 |
val target_name: local_theory -> bstring -> string |
|
41 |
val init: string -> operations -> Proof.context -> local_theory |
|
21273 | 42 |
val restore: local_theory -> local_theory |
21292 | 43 |
val reinit: local_theory -> theory -> local_theory |
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, |
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
56 |
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
|
57 |
(term * thm) list * local_theory, |
21433 | 58 |
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
|
59 |
(bstring * thm list) list * local_theory, |
21433 | 60 |
defs: string -> ((bstring * mixfix) * ((bstring * Attrib.src list) * term)) list -> |
61 |
local_theory -> (term * (bstring * thm)) list * local_theory, |
|
62 |
notes: string -> |
|
63 |
((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list -> |
|
64 |
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
|
65 |
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
|
66 |
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
|
67 |
declaration: (morphism -> Context.generic -> Context.generic) -> local_theory -> local_theory, |
21529 | 68 |
target_morphism: local_theory -> morphism, |
69 |
target_name: local_theory -> bstring -> string, |
|
21292 | 70 |
reinit: local_theory -> theory -> local_theory, |
71 |
exit: local_theory -> Proof.context}; |
|
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
72 |
|
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
73 |
datatype lthy = LThy of |
21529 | 74 |
{theory_prefix: string, |
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
75 |
operations: operations, |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
76 |
target: Proof.context}; |
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 |
fun make_lthy (theory_prefix, operations, target) = |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
79 |
LThy {theory_prefix = theory_prefix, operations = operations, target = target}; |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
80 |
|
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
81 |
|
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
82 |
(* context data *) |
18744 | 83 |
|
84 |
structure Data = ProofDataFun |
|
85 |
( |
|
18876 | 86 |
val name = "Pure/local_theory"; |
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
87 |
type T = lthy option; |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
88 |
fun init _ = NONE; |
18744 | 89 |
fun print _ _ = (); |
90 |
); |
|
91 |
val _ = Context.add_setup Data.init; |
|
92 |
||
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
93 |
fun get_lthy lthy = |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
94 |
(case Data.get lthy of |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
95 |
NONE => error "No local theory context" |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
96 |
| SOME (LThy data) => data); |
18951 | 97 |
|
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
98 |
fun map_lthy f lthy = |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
99 |
let val {theory_prefix, operations, target} = get_lthy lthy |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
100 |
in Data.put (SOME (make_lthy (f (theory_prefix, operations, target)))) lthy end; |
18767 | 101 |
|
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
102 |
val target_of = #target o get_lthy; |
21034 | 103 |
val assert = tap target_of; |
18767 | 104 |
|
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
105 |
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
|
106 |
(theory_prefix, operations, f target)); |
18767 | 107 |
|
108 |
||
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
109 |
(* substructure mappings *) |
19661 | 110 |
|
20960 | 111 |
fun raw_theory_result f lthy = |
112 |
let |
|
113 |
val (res, thy') = f (ProofContext.theory_of lthy); |
|
114 |
val lthy' = lthy |
|
115 |
|> map_target (ProofContext.transfer thy') |
|
116 |
|> ProofContext.transfer thy'; |
|
117 |
in (res, lthy') end; |
|
118 |
||
119 |
fun raw_theory f = #2 o raw_theory_result (f #> pair ()); |
|
120 |
||
21529 | 121 |
fun theory_result f lthy = lthy |> raw_theory_result (fn thy => thy |
122 |
|> Sign.sticky_prefix (#theory_prefix (get_lthy lthy)) |
|
123 |
|> Sign.qualified_names |
|
124 |
|> f |
|
125 |
||> Sign.restore_naming thy); |
|
19661 | 126 |
|
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
127 |
fun theory f = #2 o theory_result (f #> pair ()); |
19661 | 128 |
|
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
129 |
fun target_result f lthy = |
18744 | 130 |
let |
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
131 |
val (res, ctxt') = f (#target (get_lthy lthy)); |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
132 |
val thy' = ProofContext.theory_of ctxt'; |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
133 |
val lthy' = lthy |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
134 |
|> map_target (K ctxt') |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
135 |
|> ProofContext.transfer thy'; |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
136 |
in (res, lthy') end; |
18876 | 137 |
|
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
138 |
fun target f = #2 o target_result (f #> pair ()); |
18767 | 139 |
|
140 |
||
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
141 |
(* primitive operations *) |
18781 | 142 |
|
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
143 |
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
|
144 |
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
|
145 |
fun operation2 f x y = operation (fn ops => f ops x y); |
18781 | 146 |
|
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
147 |
val pretty = operation #pretty; |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
148 |
val consts = operation2 #consts; |
21433 | 149 |
val axioms = operation2 #axioms; |
150 |
val defs = operation2 #defs; |
|
151 |
val notes = operation2 #notes; |
|
21498
6382c3a1e7cf
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21433
diff
changeset
|
152 |
val type_syntax = operation1 #type_syntax; |
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
153 |
val term_syntax = operation1 #term_syntax; |
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
154 |
val declaration = operation1 #declaration; |
21529 | 155 |
val target_morphism = operation #target_morphism; |
156 |
val target_name = operation #target_name; |
|
18781 | 157 |
|
158 |
||
20888
0ddd2f297ae7
turned into abstract wrapper module, cf. theory_target.ML;
wenzelm
parents:
20784
diff
changeset
|
159 |
(* derived operations *) |
18781 | 160 |
|
21433 | 161 |
fun def kind arg lthy = lthy |> defs kind [arg] |>> hd; |
18781 | 162 |
|
21433 | 163 |
fun note kind (a, ths) lthy = lthy |> notes kind [(a, [(ths, [])])] |>> hd; |
18781 | 164 |
|
21529 | 165 |
fun notation mode args = term_syntax (fn phi => |
166 |
let val args' = args |> map (fn (t, mx) => (Morphism.term phi t, mx)) |
|
167 |
in Context.mapping (Sign.add_notation mode args') (ProofContext.add_notation mode args') end); |
|
18781 | 168 |
|
21529 | 169 |
fun abbrevs mode args = term_syntax (fn phi => |
170 |
let val args' = args |> map (fn ((c, mx), t) => ((Morphism.name phi c, mx), Morphism.term phi t)) |
|
171 |
in |
|
172 |
Context.mapping |
|
173 |
(snd o Sign.add_abbrevs mode args') (snd o ProofContext.add_abbrevs mode args') |
|
174 |
end); |
|
18805
18863b33c831
improved 'notes', including proper treatment of locale results;
wenzelm
parents:
18781
diff
changeset
|
175 |
|
20910 | 176 |
|
177 |
(* init -- exit *) |
|
178 |
||
179 |
fun init theory_prefix operations target = target |> Data.map |
|
180 |
(fn NONE => SOME (make_lthy (theory_prefix, operations, target)) |
|
181 |
| SOME _ => error "Local theory already initialized"); |
|
182 |
||
21273 | 183 |
fun restore lthy = |
20910 | 184 |
let val {theory_prefix, operations, target} = get_lthy lthy |
185 |
in init theory_prefix operations target end; |
|
186 |
||
21292 | 187 |
val reinit = operation #reinit; |
188 |
val exit = operation #exit; |
|
20910 | 189 |
|
18781 | 190 |
end; |