author  wenzelm 
Tue, 05 Jan 2021 16:39:53 +0100  
changeset 73300  32618ae1b65d 
parent 72289  69880fdc8310 
child 74382  d0527bb2e590 
permissions  rwrr 
1526  1 
(* Title: Pure/theory.ML 
2 
Author: Lawrence C Paulson and Markus Wenzel 

3 

28290  4 
Logical theory content: axioms, definitions, and begin/end wrappers. 
1526  5 
*) 
16291  6 

26668
65023d4fd226
removed obsolete SIGN_THEORY  no name aliases in structure Theory;
wenzelm
parents:
26631
diff
changeset

7 
signature THEORY = 
3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

8 
sig 
22684  9 
val parents_of: theory > theory list 
10 
val ancestors_of: theory > theory list 

42425  11 
val nodes_of: theory > theory list 
53171  12 
val setup: (theory > theory) > unit 
59930  13 
val local_setup: (Proof.context > Proof.context) > unit 
67384  14 
val install_pure: theory > unit 
67380  15 
val get_pure: unit > theory 
70067  16 
val get_pure_bootstrap: unit > theory 
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48638
diff
changeset

17 
val get_markup: theory > Markup.T 
68482  18 
val check: {long: bool} > Proof.context > string * Position.T > theory 
56025  19 
val axiom_table: theory > term Name_Space.table 
33095
bbd52d2f8696
renamed NameSpace to Name_Space  also to emphasize its subtle change in semantics;
wenzelm
parents:
33092
diff
changeset

20 
val axiom_space: theory > Name_Space.T 
16339  21 
val all_axioms_of: theory > (string * term) list 
24666  22 
val defs_of: theory > Defs.T 
23 
val at_begin: (theory > theory option) > theory > theory 

24 
val at_end: (theory > theory option) > theory > theory 

70546
34b271c4f400
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents:
70067
diff
changeset

25 
val join_theory: theory list > theory 
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48638
diff
changeset

26 
val begin_theory: string * Position.T > theory list > theory 
24666  27 
val end_theory: theory > theory 
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42360
diff
changeset

28 
val add_axiom: Proof.context > binding * term > theory > theory 
61255
15865e0c5598
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents:
61249
diff
changeset

29 
val const_dep: theory > string * typ > Defs.entry 
15865e0c5598
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents:
61249
diff
changeset

30 
val type_dep: string * typ list > Defs.entry 
61261
ddb2da7cb2e4
more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents:
61256
diff
changeset

31 
val add_deps: Defs.context > string > Defs.entry > Defs.entry list > theory > theory 
61255
15865e0c5598
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents:
61249
diff
changeset

32 
val add_deps_global: string > Defs.entry > Defs.entry list > theory > theory 
61261
ddb2da7cb2e4
more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents:
61256
diff
changeset

33 
val add_def: Defs.context > bool > bool > binding * term > theory > theory 
33173
b8ca12f6681a
eliminated obsolete tags for types/consts  now handled via name space, in strongly typed fashion;
wenzelm
parents:
33168
diff
changeset

34 
val specify_const: (binding * typ) * mixfix > theory > term * theory 
46974
7ca3608146d8
eliminated odd 'finalconsts' / Theory.add_finals;
wenzelm
parents:
45632
diff
changeset

35 
val check_overloading: Proof.context > bool > string * typ > unit 
16495  36 
end 
1526  37 

24666  38 
structure Theory: THEORY = 
16443
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

39 
struct 
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

40 

19708
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

41 

24666  42 
(** theory context operations **) 
16443
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

43 

82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

44 
val parents_of = Context.parents_of; 
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

45 
val ancestors_of = Context.ancestors_of; 
42425  46 
fun nodes_of thy = thy :: ancestors_of thy; 
16443
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

47 

53171  48 
fun setup f = Context.>> (Context.map_theory f); 
59930  49 
fun local_setup f = Context.>> (Context.map_proof f); 
53171  50 

67384  51 

52 
(* implicit theory Pure *) 

53 

67380  54 
val pure: theory Single_Assignment.var = Single_Assignment.var "pure"; 
67384  55 

67380  56 
fun install_pure thy = Single_Assignment.assign pure thy; 
57 

67384  58 
fun get_pure () = 
59 
(case Single_Assignment.peek pure of 

60 
SOME thy => thy 

61 
 NONE => raise Fail "Theory Pure not present"); 

62 

70067  63 
fun get_pure_bootstrap () = 
64 
(case Single_Assignment.peek pure of 

65 
SOME thy => thy 

66 
 NONE => Context.the_global_context ()); 

67 

24666  68 

69 

25059  70 
(** datatype thy **) 
24666  71 

72 
type wrapper = (theory > theory option) * stamp; 

73 

74 
fun apply_wrappers (wrappers: wrapper list) = 

25059  75 
perhaps (perhaps_loop (perhaps_apply (map fst wrappers))); 
24666  76 

77 
datatype thy = Thy of 

48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48638
diff
changeset

78 
{pos: Position.T, 
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48638
diff
changeset

79 
id: serial, 
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48638
diff
changeset

80 
axioms: term Name_Space.table, 
24666  81 
defs: Defs.T, 
82 
wrappers: wrapper list * wrapper list}; 

83 

48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48638
diff
changeset

84 
fun make_thy (pos, id, axioms, defs, wrappers) = 
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48638
diff
changeset

85 
Thy {pos = pos, id = id, axioms = axioms, defs = defs, wrappers = wrappers}; 
24666  86 

61262
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61261
diff
changeset

87 
structure Thy = Theory_Data' 
24666  88 
( 
89 
type T = thy; 

72289  90 
val extend = I; 
71113
98d9b78b7f47
clarified axiom_table: uniform space (e.g. like consts), e.g. relevant for export of HOLex.Join_Theory;
wenzelm
parents:
70547
diff
changeset

91 
val empty = make_thy (Position.none, 0, Name_Space.empty_table "axiom", Defs.empty, ([], [])); 
61262
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61261
diff
changeset

92 
fun merge old_thys (thy1, thy2) = 
24666  93 
let 
72289  94 
val Thy {pos, id, axioms = axioms1, defs = defs1, wrappers = (bgs1, ens1)} = thy1; 
71113
98d9b78b7f47
clarified axiom_table: uniform space (e.g. like consts), e.g. relevant for export of HOLex.Join_Theory;
wenzelm
parents:
70547
diff
changeset

95 
val Thy {pos = _, id = _, axioms = axioms2, defs = defs2, wrappers = (bgs2, ens2)} = thy2; 
24666  96 

71113
98d9b78b7f47
clarified axiom_table: uniform space (e.g. like consts), e.g. relevant for export of HOLex.Join_Theory;
wenzelm
parents:
70547
diff
changeset

97 
val axioms' = Name_Space.merge_tables (axioms1, axioms2); 
61262
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61261
diff
changeset

98 
val defs' = Defs.merge (Defs.global_context (fst old_thys)) (defs1, defs2); 
24666  99 
val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2); 
100 
val ens' = Library.merge (eq_snd op =) (ens1, ens2); 

72289  101 
in make_thy (pos, id, axioms', defs', (bgs', ens')) end; 
24666  102 
); 
103 

42016  104 
fun rep_theory thy = Thy.get thy > (fn Thy args => args); 
24666  105 

48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48638
diff
changeset

106 
fun map_thy f = Thy.map (fn (Thy {pos, id, axioms, defs, wrappers}) => 
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48638
diff
changeset

107 
make_thy (f (pos, id, axioms, defs, wrappers))); 
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48638
diff
changeset

108 

ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48638
diff
changeset

109 
fun map_axioms f = 
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48638
diff
changeset

110 
map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, f axioms, defs, wrappers)); 
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48638
diff
changeset

111 

ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48638
diff
changeset

112 
fun map_defs f = 
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48638
diff
changeset

113 
map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, axioms, f defs, wrappers)); 
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48638
diff
changeset

114 

ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48638
diff
changeset

115 
fun map_wrappers f = 
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48638
diff
changeset

116 
map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, axioms, defs, f wrappers)); 
24666  117 

118 

48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48638
diff
changeset

119 
(* entity markup *) 
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48638
diff
changeset

120 

ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48638
diff
changeset

121 
fun theory_markup def name id pos = 
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48638
diff
changeset

122 
if id = 0 then Markup.empty 
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48638
diff
changeset

123 
else 
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48638
diff
changeset

124 
Markup.properties (Position.entity_properties_of def id pos) 
50201
c26369c9eda6
Isabellespecific implementation of quasiabstract markup elements  back to module arrangement before d83797ef0d2d;
wenzelm
parents:
48929
diff
changeset

125 
(Markup.entity Markup.theoryN name); 
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48638
diff
changeset

126 

48929
05d4e5f660ae
entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents:
48927
diff
changeset

127 
fun init_markup (name, pos) thy = 
05d4e5f660ae
entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents:
48927
diff
changeset

128 
let 
05d4e5f660ae
entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents:
48927
diff
changeset

129 
val id = serial (); 
71889  130 
val _ = Context_Position.reports_global thy [(pos, theory_markup true name id pos)]; 
48929
05d4e5f660ae
entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents:
48927
diff
changeset

131 
in map_thy (fn (_, _, axioms, defs, wrappers) => (pos, id, axioms, defs, wrappers)) thy end; 
05d4e5f660ae
entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents:
48927
diff
changeset

132 

48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48638
diff
changeset

133 
fun get_markup thy = 
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48638
diff
changeset

134 
let val {pos, id, ...} = rep_theory thy 
73300
32618ae1b65d
proper theory name, e.g. for HTML/PIDE presentation;
wenzelm
parents:
72289
diff
changeset

135 
in theory_markup false (Context.theory_long_name thy) id pos end; 
24666  136 

68482  137 
fun check long ctxt (name, pos) = 
60101  138 
let 
139 
val thy = Proof_Context.theory_of ctxt; 

140 
val thy' = 

68482  141 
Context.get_theory long thy name 
60101  142 
handle ERROR msg => 
143 
let 

69295  144 
val completion_report = 
145 
Completion.make_report (name, pos) 

60101  146 
(fn completed => 
68482  147 
map (Context.theory_name' long) (ancestors_of thy) 
68484  148 
> filter (completed o Long_Name.base_name) 
60101  149 
> sort_strings 
150 
> map (fn a => (a, (Markup.theoryN, a)))); 

69295  151 
in error (msg ^ Position.here pos ^ completion_report) end; 
60101  152 
val _ = Context_Position.report ctxt pos (get_markup thy'); 
153 
in thy' end; 

154 

24666  155 

156 
(* basic operations *) 

157 

56025  158 
val axiom_table = #axioms o rep_theory; 
159 
val axiom_space = Name_Space.space_of_table o axiom_table; 

24666  160 

71113
98d9b78b7f47
clarified axiom_table: uniform space (e.g. like consts), e.g. relevant for export of HOLex.Join_Theory;
wenzelm
parents:
70547
diff
changeset

161 
val all_axioms_of = Name_Space.dest_table o axiom_table; 
24666  162 

163 
val defs_of = #defs o rep_theory; 

164 

165 

70546
34b271c4f400
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents:
70067
diff
changeset

166 
(* join theory *) 
34b271c4f400
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents:
70067
diff
changeset

167 

70547
421727c19b23
proper theory naming after join (reset due to merge_data);
wenzelm
parents:
70546
diff
changeset

168 
fun join_theory [] = raise List.Empty 
421727c19b23
proper theory naming after join (reset due to merge_data);
wenzelm
parents:
70546
diff
changeset

169 
 join_theory [thy] = thy 
72283
4ed33ea8d957
prefer conservative extend/merge of theory naming;
wenzelm
parents:
71889
diff
changeset

170 
 join_theory thys = foldl1 Context.join_thys thys; 
70546
34b271c4f400
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents:
70067
diff
changeset

171 

34b271c4f400
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
wenzelm
parents:
70067
diff
changeset

172 

24666  173 
(* begin/end theory *) 
174 

175 
val begin_wrappers = rev o #1 o #wrappers o rep_theory; 

176 
val end_wrappers = rev o #2 o #wrappers o rep_theory; 

177 

178 
fun at_begin f = map_wrappers (apfst (cons (f, stamp ()))); 

179 
fun at_end f = map_wrappers (apsnd (cons (f, stamp ()))); 

180 

48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48638
diff
changeset

181 
fun begin_theory (name, pos) imports = 
48638  182 
if name = Context.PureN then 
48929
05d4e5f660ae
entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents:
48927
diff
changeset

183 
(case imports of 
05d4e5f660ae
entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents:
48927
diff
changeset

184 
[thy] => init_markup (name, pos) thy 
05d4e5f660ae
entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents:
48927
diff
changeset

185 
 _ => error "Bad bootstrapping of theory Pure") 
48638  186 
else 
187 
let 

61262
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61261
diff
changeset

188 
val thy = Context.begin_thy name imports; 
48638  189 
val wrappers = begin_wrappers thy; 
190 
in 

191 
thy 

48929
05d4e5f660ae
entity markup for theory Pure, to enable hyperlinks etc.;
wenzelm
parents:
48927
diff
changeset

192 
> init_markup (name, pos) 
72283
4ed33ea8d957
prefer conservative extend/merge of theory naming;
wenzelm
parents:
71889
diff
changeset

193 
> Sign.init_naming 
48638  194 
> Sign.local_path 
195 
> apply_wrappers wrappers 

196 
> tap (Syntax.force_syntax o Sign.syn_of) 

197 
end; 

24666  198 

199 
fun end_theory thy = 

56057
ad6bd8030d88
more explicit Sign.change_check  detect structural mistakes where they emerge, not at later theory merges;
wenzelm
parents:
56025
diff
changeset

200 
thy 
ad6bd8030d88
more explicit Sign.change_check  detect structural mistakes where they emerge, not at later theory merges;
wenzelm
parents:
56025
diff
changeset

201 
> apply_wrappers (end_wrappers thy) 
ad6bd8030d88
more explicit Sign.change_check  detect structural mistakes where they emerge, not at later theory merges;
wenzelm
parents:
56025
diff
changeset

202 
> Sign.change_check 
ad6bd8030d88
more explicit Sign.change_check  detect structural mistakes where they emerge, not at later theory merges;
wenzelm
parents:
56025
diff
changeset

203 
> Context.finish_thy; 
24666  204 

16443
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

205 

3996  206 

35985
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35857
diff
changeset

207 
(** primitive specifications **) 
3814  208 

35985
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35857
diff
changeset

209 
(* raw axioms *) 
1526  210 

42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42360
diff
changeset

211 
fun cert_axm ctxt (b, raw_tm) = 
1526  212 
let 
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42360
diff
changeset

213 
val thy = Proof_Context.theory_of ctxt; 
32789
d89327de0b3c
removed redundant Sign.certify_prop, use Sign.cert_prop instead;
wenzelm
parents:
30466
diff
changeset

214 
val t = Sign.cert_prop thy raw_tm 
2979  215 
handle TYPE (msg, _, _) => error msg 
16291  216 
 TERM (msg, _) => error msg; 
35987
7c728daf4876
disallow sort constraints in primitive Theory.add_axiom/add_def  handled in Thm.add_axiom/add_def;
wenzelm
parents:
35985
diff
changeset

217 
val _ = Term.no_dummy_patterns t handle TERM (msg, _) => error msg; 
7c728daf4876
disallow sort constraints in primitive Theory.add_axiom/add_def  handled in Thm.add_axiom/add_def;
wenzelm
parents:
35985
diff
changeset

218 

7c728daf4876
disallow sort constraints in primitive Theory.add_axiom/add_def  handled in Thm.add_axiom/add_def;
wenzelm
parents:
35985
diff
changeset

219 
val bad_sorts = 
7c728daf4876
disallow sort constraints in primitive Theory.add_axiom/add_def  handled in Thm.add_axiom/add_def;
wenzelm
parents:
35985
diff
changeset

220 
rev ((fold_types o fold_atyps_sorts) (fn (_, []) => I  (T, _) => insert (op =) T) t []); 
7c728daf4876
disallow sort constraints in primitive Theory.add_axiom/add_def  handled in Thm.add_axiom/add_def;
wenzelm
parents:
35985
diff
changeset

221 
val _ = null bad_sorts orelse 
7c728daf4876
disallow sort constraints in primitive Theory.add_axiom/add_def  handled in Thm.add_axiom/add_def;
wenzelm
parents:
35985
diff
changeset

222 
error ("Illegal sort constraints in primitive specification: " ^ 
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42360
diff
changeset

223 
commas (map (Syntax.string_of_typ (Config.put show_sorts true ctxt)) bad_sorts)); 
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42360
diff
changeset

224 
in (b, Sign.no_vars ctxt t) end 
42381
309ec68442c6
added Binding.print convenience, which includes quote already;
wenzelm
parents:
42375
diff
changeset

225 
handle ERROR msg => cat_error msg ("The error(s) above occurred in axiom " ^ Binding.print b); 
1526  226 

42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42360
diff
changeset

227 
fun add_axiom ctxt raw_axm thy = thy > map_axioms (fn axioms => 
1526  228 
let 
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42360
diff
changeset

229 
val axm = apsnd Logic.varify_global (cert_axm ctxt raw_axm); 
61949  230 
val context = ctxt 
231 
> Sign.inherit_naming thy 

232 
> Context_Position.set_visible_generic false; 

233 
val (_, axioms') = Name_Space.define context true axm axioms; 

16443
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

234 
in axioms' end); 
1526  235 

236 

19708
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

237 
(* dependencies *) 
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

238 

61256  239 
fun const_dep thy (c, T) = ((Defs.Const, c), Sign.const_typargs thy (c, T)); 
61255
15865e0c5598
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents:
61249
diff
changeset

240 
fun type_dep (c, args) = ((Defs.Type, c), args); 
61246
077b88f9ec16
HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07Jul2015, 16Jul2015, 30Jul2015;
wenzelm
parents:
61044
diff
changeset

241 

61261
ddb2da7cb2e4
more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents:
61256
diff
changeset

242 
fun dependencies (context as (ctxt, _)) unchecked def description lhs rhs = 
19708
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

243 
let 
61255
15865e0c5598
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents:
61249
diff
changeset

244 
fun prep (item, args) = 
15865e0c5598
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents:
61249
diff
changeset

245 
(case fold Term.add_tvarsT args [] of 
15865e0c5598
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents:
61249
diff
changeset

246 
[] => (item, map Logic.varifyT_global args) 
15865e0c5598
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents:
61249
diff
changeset

247 
 vs => raise TYPE ("Illegal schematic type variable(s)", map TVar vs, [])); 
61249  248 

61255
15865e0c5598
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents:
61249
diff
changeset

249 
val lhs_vars = fold Term.add_tfreesT (snd lhs) []; 
15865e0c5598
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents:
61249
diff
changeset

250 
val rhs_extras = 
15865e0c5598
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents:
61249
diff
changeset

251 
fold (fn (_, args) => args > (fold o Term.fold_atyps) (fn TFree v => 
15865e0c5598
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents:
61249
diff
changeset

252 
if member (op =) lhs_vars v then I else insert (op =) v)) rhs []; 
19708
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

253 
val _ = 
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

254 
if null rhs_extras then () 
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

255 
else error ("Specification depends on extra type variables: " ^ 
39133
70d3915c92f0
pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
wenzelm
parents:
36610
diff
changeset

256 
commas_quote (map (Syntax.string_of_typ ctxt o TFree) rhs_extras) ^ 
33701
9dd1079cec3a
primitive defs: clarified def (axiom name) vs. description;
wenzelm
parents:
33173
diff
changeset

257 
"\nThe error(s) above occurred in " ^ quote description); 
61261
ddb2da7cb2e4
more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents:
61256
diff
changeset

258 
in Defs.define context unchecked def description (prep lhs) (map prep rhs) end; 
19708
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

259 

61256  260 
fun cert_entry thy ((Defs.Const, c), args) = 
61255
15865e0c5598
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents:
61249
diff
changeset

261 
Sign.cert_term thy (Const (c, Sign.const_instance thy (c, args))) 
15865e0c5598
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents:
61249
diff
changeset

262 
> dest_Const > const_dep thy 
15865e0c5598
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents:
61249
diff
changeset

263 
 cert_entry thy ((Defs.Type, c), args) = 
15865e0c5598
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents:
61249
diff
changeset

264 
Sign.certify_typ thy (Type (c, args)) > dest_Type > type_dep; 
15865e0c5598
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents:
61249
diff
changeset

265 

61261
ddb2da7cb2e4
more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents:
61256
diff
changeset

266 
fun add_deps context a raw_lhs raw_rhs thy = 
19708
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

267 
let 
61255
15865e0c5598
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents:
61249
diff
changeset

268 
val (lhs as ((_, lhs_name), _)) :: rhs = map (cert_entry thy) (raw_lhs :: raw_rhs); 
15865e0c5598
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents:
61249
diff
changeset

269 
val description = if a = "" then lhs_name ^ " axiom" else a; 
61261
ddb2da7cb2e4
more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents:
61256
diff
changeset

270 
in thy > map_defs (dependencies context false NONE description lhs rhs) end; 
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42360
diff
changeset

271 

61255
15865e0c5598
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents:
61249
diff
changeset

272 
fun add_deps_global a x y thy = 
61262
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61261
diff
changeset

273 
add_deps (Defs.global_context thy) a x y thy; 
17706  274 

33173
b8ca12f6681a
eliminated obsolete tags for types/consts  now handled via name space, in strongly typed fashion;
wenzelm
parents:
33168
diff
changeset

275 
fun specify_const decl thy = 
61255
15865e0c5598
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents:
61249
diff
changeset

276 
let val (t, thy') = Sign.declare_const_global decl thy; 
15865e0c5598
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents:
61249
diff
changeset

277 
in (t, add_deps_global "" (const_dep thy' (dest_Const t)) [] thy') end; 
25017  278 

17706  279 

35985
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35857
diff
changeset

280 
(* overloading *) 
9280  281 

42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42360
diff
changeset

282 
fun check_overloading ctxt overloaded (c, T) = 
16291  283 
let 
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42360
diff
changeset

284 
val thy = Proof_Context.theory_of ctxt; 
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42360
diff
changeset

285 

24763  286 
val declT = Sign.the_const_constraint thy c 
287 
handle TYPE (msg, _, _) => error msg; 

35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
34259
diff
changeset

288 
val T' = Logic.varifyT_global T; 
16944  289 

39134
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39133
diff
changeset

290 
fun message sorts txt = 
16944  291 
[Pretty.block [Pretty.str "Specification of constant ", 
39134
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39133
diff
changeset

292 
Pretty.str c, Pretty.str " ::", Pretty.brk 1, 
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39133
diff
changeset

293 
Pretty.quote (Syntax.pretty_typ (Config.put show_sorts sorts ctxt) T)], 
16944  294 
Pretty.str txt] > Pretty.chunks > Pretty.string_of; 
16291  295 
in 
16944  296 
if Sign.typ_instance thy (declT, T') then () 
297 
else if Type.raw_instance (declT, T') then 

39134
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39133
diff
changeset

298 
error (message true "imposes additional sort constraints on the constant declaration") 
16944  299 
else if overloaded then () 
57510  300 
else 
301 
error (message false "is strictly less general than the declared type (overloading required)") 

9280  302 
end; 
303 

3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

304 

35985
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35857
diff
changeset

305 
(* definitional axioms *) 
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35857
diff
changeset

306 

0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35857
diff
changeset

307 
local 
16291  308 

61261
ddb2da7cb2e4
more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents:
61256
diff
changeset

309 
fun check_def (context as (ctxt, _)) thy unchecked overloaded (b, tm) defs = 
16291  310 
let 
29581  311 
val name = Sign.full_name thy b; 
63395  312 
val ((lhs, rhs), _, _) = 
63046  313 
Primitive_Defs.dest_def ctxt 
314 
{check_head = Term.is_Const, 

315 
check_free_lhs = K true, 

316 
check_free_rhs = K false, 

317 
check_tfree = K false} tm 

35988
76ca601c941e
disallow premises in primitive Theory.add_def  handle in Thm.add_def;
wenzelm
parents:
35987
diff
changeset

318 
handle TERM (msg, _) => error msg; 
76ca601c941e
disallow premises in primitive Theory.add_def  handle in Thm.add_def;
wenzelm
parents:
35987
diff
changeset

319 
val lhs_const = Term.dest_Const (Term.head_of lhs); 
61248  320 

61255
15865e0c5598
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents:
61249
diff
changeset

321 
val rhs_consts = 
15865e0c5598
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents:
61249
diff
changeset

322 
fold_aterms (fn Const const => insert (op =) (const_dep thy const)  _ => I) rhs []; 
61248  323 
val rhs_types = 
61255
15865e0c5598
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents:
61249
diff
changeset

324 
(fold_types o fold_subtypes) (fn Type t => insert (op =) (type_dep t)  _ => I) rhs []; 
61248  325 
val rhs_deps = rhs_consts @ rhs_types; 
326 

42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42360
diff
changeset

327 
val _ = check_overloading ctxt overloaded lhs_const; 
61261
ddb2da7cb2e4
more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents:
61256
diff
changeset

328 
in defs > dependencies context unchecked (SOME name) name (const_dep thy lhs_const) rhs_deps end 
18678  329 
handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block 
42381
309ec68442c6
added Binding.print convenience, which includes quote already;
wenzelm
parents:
42375
diff
changeset

330 
[Pretty.str ("The error(s) above occurred in definition " ^ Binding.print b ^ ":"), 
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42360
diff
changeset

331 
Pretty.fbrk, Pretty.quote (Syntax.pretty_term ctxt tm)])); 
3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

332 

16291  333 
in 
334 

61261
ddb2da7cb2e4
more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents:
61256
diff
changeset

335 
fun add_def (context as (ctxt, _)) unchecked overloaded raw_axm thy = 
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42360
diff
changeset

336 
let val axm = cert_axm ctxt raw_axm in 
35985
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35857
diff
changeset

337 
thy 
61261
ddb2da7cb2e4
more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents:
61256
diff
changeset

338 
> map_defs (check_def context thy unchecked overloaded axm) 
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42360
diff
changeset

339 
> add_axiom ctxt axm 
35985
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35857
diff
changeset

340 
end; 
16291  341 

342 
end; 

3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

343 

14223
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

344 
end; 