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