author  haftmann 
Wed, 11 Aug 2010 17:59:32 +0200  
changeset 38382  8b02c5bf1d0e 
parent 38381  7d1e2a6831ec 
child 38384  07c33be08476 
permissions  rwrr 
38379
67d71449e85b
more convenient split of class modules: class and class_declaration
haftmann
parents:
38377
diff
changeset

1 
(* Title: Pure/Isar/class.ML 
24218  2 
Author: Florian Haftmann, TU Muenchen 
3 

38379
67d71449e85b
more convenient split of class modules: class and class_declaration
haftmann
parents:
38377
diff
changeset

4 
Type classes derived from primitive axclasses and locales. 
24218  5 
*) 
6 

38379
67d71449e85b
more convenient split of class modules: class and class_declaration
haftmann
parents:
38377
diff
changeset

7 
signature CLASS = 
24218  8 
sig 
25462  9 
(*classes*) 
29526  10 
val is_class: theory > class > bool 
11 
val these_params: theory > sort > (string * (class * (string * typ))) list 

38379
67d71449e85b
more convenient split of class modules: class and class_declaration
haftmann
parents:
38377
diff
changeset

12 
val base_sort: theory > class > sort 
67d71449e85b
more convenient split of class modules: class and class_declaration
haftmann
parents:
38377
diff
changeset

13 
val rules: theory > class > thm option * thm 
67d71449e85b
more convenient split of class modules: class and class_declaration
haftmann
parents:
38377
diff
changeset

14 
val these_defs: theory > sort > thm list 
67d71449e85b
more convenient split of class modules: class and class_declaration
haftmann
parents:
38377
diff
changeset

15 
val these_operations: theory > sort 
67d71449e85b
more convenient split of class modules: class and class_declaration
haftmann
parents:
38377
diff
changeset

16 
> (string * (class * (typ * term))) list 
29526  17 
val print_classes: theory > unit 
25311  18 
val init: class > theory > Proof.context 
38379
67d71449e85b
more convenient split of class modules: class and class_declaration
haftmann
parents:
38377
diff
changeset

19 
val begin: class list > sort > Proof.context > Proof.context 
35858
0d394a82337e
handle hidden polymorphism in class target (without class target syntax, though)
haftmann
parents:
35845
diff
changeset

20 
val declare: class > (binding * mixfix) * (term list * term) > theory > theory 
33173
b8ca12f6681a
eliminated obsolete tags for types/consts  now handled via name space, in strongly typed fashion;
wenzelm
parents:
32970
diff
changeset

21 
val abbrev: class > Syntax.mode > (binding * mixfix) * term > theory > theory 
38379
67d71449e85b
more convenient split of class modules: class and class_declaration
haftmann
parents:
38377
diff
changeset

22 
val refresh_syntax: class > Proof.context > Proof.context 
67d71449e85b
more convenient split of class modules: class and class_declaration
haftmann
parents:
38377
diff
changeset

23 
val redeclare_operations: theory > sort > Proof.context > Proof.context 
29526  24 
val class_prefix: string > string 
38379
67d71449e85b
more convenient split of class modules: class and class_declaration
haftmann
parents:
38377
diff
changeset

25 
val register: class > class list > ((string * typ) * (string * typ)) list 
67d71449e85b
more convenient split of class modules: class and class_declaration
haftmann
parents:
38377
diff
changeset

26 
> sort > morphism > morphism > thm option > thm option > thm 
67d71449e85b
more convenient split of class modules: class and class_declaration
haftmann
parents:
38377
diff
changeset

27 
> theory > theory 
25485  28 

25462  29 
(*instances*) 
38379
67d71449e85b
more convenient split of class modules: class and class_declaration
haftmann
parents:
38377
diff
changeset

30 
val instantiation: string list * (string * sort) list * sort > theory > local_theory 
26247  31 
val instantiation_instance: (local_theory > local_theory) 
32 
> local_theory > Proof.state 

33 
val prove_instantiation_instance: (Proof.context > tactic) 

34 
> local_theory > local_theory 

28666  35 
val prove_instantiation_exit: (Proof.context > tactic) 
36 
> local_theory > theory 

37 
val prove_instantiation_exit_result: (morphism > 'a > 'b) 

38 
> (Proof.context > 'b > tactic) > 'a > local_theory > 'b * theory 

31869  39 
val read_multi_arity: theory > xstring list * xstring list * xstring 
40 
> string list * (string * sort) list * sort 

26259  41 
val type_name: string > string 
38348
cf7b2121ad9d
moved instantiation target formally to class_target.ML
haftmann
parents:
38107
diff
changeset

42 
val instantiation_cmd: xstring list * xstring list * xstring > theory > local_theory 
38377  43 
val instance_arity_cmd: xstring list * xstring list * xstring > theory > Proof.state 
25485  44 

31635  45 
(*subclasses*) 
46 
val classrel: class * class > theory > Proof.state 

47 
val classrel_cmd: xstring * xstring > theory > Proof.state 

38379
67d71449e85b
more convenient split of class modules: class and class_declaration
haftmann
parents:
38377
diff
changeset

48 
val register_subclass: class * class > morphism option > Element.witness option 
67d71449e85b
more convenient split of class modules: class and class_declaration
haftmann
parents:
38377
diff
changeset

49 
> morphism > theory > theory 
31635  50 

51 
(*tactics*) 

29526  52 
val intro_classes_tac: thm list > tactic 
53 
val default_intro_tac: Proof.context > thm list > tactic 

24218  54 
end; 
55 

38379
67d71449e85b
more convenient split of class modules: class and class_declaration
haftmann
parents:
38377
diff
changeset

56 
structure Class: CLASS = 
24218  57 
struct 
58 

24589  59 
(** class data **) 
24218  60 

61 
datatype class_data = ClassData of { 

28715
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

62 

238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

63 
(* static part *) 
24218  64 
consts: (string * string) list 
24836  65 
(*locale parameter ~> constant name*), 
25062  66 
base_sort: sort, 
29545  67 
base_morph: morphism 
29439  68 
(*static part of canonical morphism*), 
32850  69 
export_morph: morphism, 
25618  70 
assm_intro: thm option, 
71 
of_class: thm, 

72 
axiom: thm option, 

28715
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

73 

238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

74 
(* dynamic part *) 
24657  75 
defs: thm list, 
25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

76 
operations: (string * (class * (typ * term))) list 
28715
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

77 

24657  78 
}; 
24218  79 

32850  80 
fun make_class_data ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom), 
25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

81 
(defs, operations)) = 
29526  82 
ClassData { consts = consts, base_sort = base_sort, 
32850  83 
base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro, 
84 
of_class = of_class, axiom = axiom, defs = defs, operations = operations }; 

85 
fun map_class_data f (ClassData { consts, base_sort, base_morph, export_morph, assm_intro, 

28715
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

86 
of_class, axiom, defs, operations }) = 
32850  87 
make_class_data (f ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom), 
25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

88 
(defs, operations))); 
25038  89 
fun merge_class_data _ (ClassData { consts = consts, 
32850  90 
base_sort = base_sort, base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro, 
25618  91 
of_class = of_class, axiom = axiom, defs = defs1, operations = operations1 }, 
32850  92 
ClassData { consts = _, base_sort = _, base_morph = _, export_morph = _, assm_intro = _, 
25618  93 
of_class = _, axiom = _, defs = defs2, operations = operations2 }) = 
32850  94 
make_class_data ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom), 
24914
95cda5dd58d5
added proper subclass concept; improved class target
haftmann
parents:
24901
diff
changeset

95 
(Thm.merge_thms (defs1, defs2), 
25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

96 
AList.merge (op =) (K true) (operations1, operations2))); 
24218  97 

33522  98 
structure ClassData = Theory_Data 
24218  99 
( 
25038  100 
type T = class_data Graph.T 
101 
val empty = Graph.empty; 

24218  102 
val extend = I; 
33522  103 
val merge = Graph.join merge_class_data; 
24218  104 
); 
105 

106 

107 
(* queries *) 

108 

31599  109 
fun lookup_class_data thy class = case try (Graph.get_node (ClassData.get thy)) class 
110 
of SOME (ClassData data) => SOME data 

111 
 NONE => NONE; 

24218  112 

24589  113 
fun the_class_data thy class = case lookup_class_data thy class 
25020  114 
of NONE => error ("Undeclared class " ^ quote class) 
24589  115 
 SOME data => data; 
24218  116 

25038  117 
val is_class = is_some oo lookup_class_data; 
118 

119 
val ancestry = Graph.all_succs o ClassData.get; 

29509
1ff0f3f08a7b
migrated class package to new locale implementation
haftmann
parents:
29439
diff
changeset

120 
val heritage = Graph.all_preds o ClassData.get; 
1ff0f3f08a7b
migrated class package to new locale implementation
haftmann
parents:
29439
diff
changeset

121 

25002  122 
fun these_params thy = 
24218  123 
let 
124 
fun params class = 

125 
let 

24930
cc2e0e8c81af
renamed AxClass.get_definition to AxClass.get_info (again);
wenzelm
parents:
24920
diff
changeset

126 
val const_typs = (#params o AxClass.get_info thy) class; 
24657  127 
val const_names = (#consts o the_class_data thy) class; 
24218  128 
in 
26518  129 
(map o apsnd) 
130 
(fn c => (class, (c, (the o AList.lookup (op =) const_typs) c))) const_names 

24218  131 
end; 
132 
in maps params o ancestry thy end; 

133 

29526  134 
val base_sort = #base_sort oo the_class_data; 
135 

136 
fun rules thy class = 

137 
let val { axiom, of_class, ... } = the_class_data thy class 

138 
in (axiom, of_class) end; 

139 

140 
fun all_assm_intros thy = 

31599  141 
Graph.fold (fn (_, (ClassData { assm_intro, ... }, _)) => fold (insert Thm.eq_thm) 
142 
(the_list assm_intro)) (ClassData.get thy) []; 

24218  143 

29526  144 
fun these_defs thy = maps (#defs o the_class_data thy) o ancestry thy; 
145 
fun these_operations thy = maps (#operations o the_class_data thy) o ancestry thy; 

29358  146 

29526  147 
val base_morphism = #base_morph oo the_class_data; 
36674
d95f39448121
eq_morphism is always optional: avoid trivial morphism for empty list of equations
haftmann
parents:
36672
diff
changeset

148 
fun morphism thy class = case Element.eq_morphism thy (these_defs thy [class]) 
d95f39448121
eq_morphism is always optional: avoid trivial morphism for empty list of equations
haftmann
parents:
36672
diff
changeset

149 
of SOME eq_morph => base_morphism thy class $> eq_morph 
d95f39448121
eq_morphism is always optional: avoid trivial morphism for empty list of equations
haftmann
parents:
36672
diff
changeset

150 
 NONE => base_morphism thy class; 
32850  151 
val export_morphism = #export_morph oo the_class_data; 
28715
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

152 

24218  153 
fun print_classes thy = 
154 
let 

36610
bafd82950e24
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
wenzelm
parents:
36462
diff
changeset

155 
val ctxt = ProofContext.init_global thy; 
24218  156 
val algebra = Sign.classes_of thy; 
157 
val arities = 

158 
Symtab.empty 

159 
> Symtab.fold (fn (tyco, arities) => fold (fn (class, _) => 

160 
Symtab.map_default (class, []) (insert (op =) tyco)) arities) 

36328
4d9deabf6474
replaced Sorts.rep_algebra by slightly more abstract selectors classes_of/arities_of;
wenzelm
parents:
36323
diff
changeset

161 
(Sorts.arities_of algebra); 
24218  162 
val the_arities = these o Symtab.lookup arities; 
163 
fun mk_arity class tyco = 

164 
let 

165 
val Ss = Sorts.mg_domain algebra tyco [class]; 

24920  166 
in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end; 
24218  167 
fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: " 
32966
5b21661fe618
indicate CRITICAL nature of various setmp combinators;
wenzelm
parents:
32850
diff
changeset

168 
^ setmp_CRITICAL show_sorts false (Syntax.string_of_typ ctxt o Type.strip_sorts) ty); 
24218  169 
fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [ 
25062  170 
(SOME o Pretty.str) ("class " ^ Sign.extern_class thy class ^ ":"), 
24218  171 
(SOME o Pretty.block) [Pretty.str "supersort: ", 
24920  172 
(Syntax.pretty_sort ctxt o Sign.minimize_sort thy o Sign.super_classes thy) class], 
25062  173 
((fn [] => NONE  ps => (SOME o Pretty.block o Pretty.fbreaks) 
174 
(Pretty.str "parameters:" :: ps)) o map mk_param 

24930
cc2e0e8c81af
renamed AxClass.get_definition to AxClass.get_info (again);
wenzelm
parents:
24920
diff
changeset

175 
o these o Option.map #params o try (AxClass.get_info thy)) class, 
24218  176 
(SOME o Pretty.block o Pretty.breaks) [ 
177 
Pretty.str "instances:", 

178 
Pretty.list "" "" (map (mk_arity class) (the_arities class)) 

179 
] 

180 
] 

181 
in 

24589  182 
(Pretty.writeln o Pretty.chunks o separate (Pretty.str "") 
183 
o map mk_entry o Sorts.all_classes) algebra 

24218  184 
end; 
185 

186 

187 
(* updaters *) 

188 

32850  189 
fun register class sups params base_sort base_morph export_morph 
29358  190 
axiom assm_intro of_class thy = 
25002  191 
let 
25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

192 
val operations = map (fn (v_ty as (_, ty), (c, _)) => 
25683  193 
(c, (class, (ty, Free v_ty)))) params; 
25038  194 
val add_class = Graph.new_node (class, 
31599  195 
make_class_data (((map o pairself) fst params, base_sort, 
32850  196 
base_morph, export_morph, assm_intro, of_class, axiom), ([], operations))) 
29526  197 
#> fold (curry Graph.add_edge class) sups; 
25618  198 
in ClassData.map add_class thy end; 
24218  199 

36674
d95f39448121
eq_morphism is always optional: avoid trivial morphism for empty list of equations
haftmann
parents:
36672
diff
changeset

200 
fun activate_defs class thms thy = case Element.eq_morphism thy thms 
d95f39448121
eq_morphism is always optional: avoid trivial morphism for empty list of equations
haftmann
parents:
36672
diff
changeset

201 
of SOME eq_morph => fold (fn cls => fn thy => 
38107  202 
Context.theory_map (Locale.amend_registration (cls, base_morphism thy cls) 
203 
(eq_morph, true) (export_morphism thy cls)) thy) (heritage thy [class]) thy 

36674
d95f39448121
eq_morphism is always optional: avoid trivial morphism for empty list of equations
haftmann
parents:
36672
diff
changeset

204 
 NONE => thy; 
29526  205 

25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

206 
fun register_operation class (c, (t, some_def)) thy = 
25062  207 
let 
29358  208 
val base_sort = base_sort thy class; 
29439  209 
val prep_typ = map_type_tfree 
210 
(fn (v, sort) => if Name.aT = v 

211 
then TFree (v, base_sort) else TVar ((v, 0), sort)); 

25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

212 
val t' = map_types prep_typ t; 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

213 
val ty' = Term.fastype_of t'; 
25062  214 
in 
215 
thy 

216 
> (ClassData.map o Graph.map_node class o map_class_data o apsnd) 

25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

217 
(fn (defs, operations) => 
25096  218 
(fold cons (the_list some_def) defs, 
25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

219 
(c, (class, (ty', t'))) :: operations)) 
36674
d95f39448121
eq_morphism is always optional: avoid trivial morphism for empty list of equations
haftmann
parents:
36672
diff
changeset

220 
> activate_defs class (the_list some_def) 
25062  221 
end; 
24218  222 

29558  223 
fun register_subclass (sub, sup) some_dep_morph some_wit export thy = 
25618  224 
let 
29558  225 
val intros = (snd o rules thy) sup :: map_filter I 
35021
c839a4c670c6
renamed oldstyle Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33969
diff
changeset

226 
[Option.map (Drule.export_without_context_open o Element.conclude_witness) some_wit, 
29558  227 
(fst o rules thy) sub]; 
29610  228 
val tac = EVERY (map (TRYALL o Tactic.rtac) intros); 
32970
fbd2bb2489a8
operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
wenzelm
parents:
32966
diff
changeset

229 
val classrel = Skip_Proof.prove_global thy [] [] (Logic.mk_classrel (sub, sup)) 
29558  230 
(K tac); 
29509
1ff0f3f08a7b
migrated class package to new locale implementation
haftmann
parents:
29439
diff
changeset

231 
val diff_sort = Sign.complete_sort thy [sup] 
31012  232 
> subtract (op =) (Sign.complete_sort thy [sub]) 
233 
> filter (is_class thy); 

32074  234 
val add_dependency = case some_dep_morph 
235 
of SOME dep_morph => Locale.add_dependency sub 

236 
(sup, dep_morph $> Element.satisfy_morphism (the_list some_wit)) export 

237 
 NONE => I 

25618  238 
in 
239 
thy 

37246  240 
> AxClass.add_classrel classrel 
25618  241 
> ClassData.map (Graph.add_edge (sub, sup)) 
29526  242 
> activate_defs sub (these_defs thy diff_sort) 
32074  243 
> add_dependency 
24218  244 
end; 
245 

246 

24589  247 
(** classes and class target **) 
24218  248 

25002  249 
(* class context syntax *) 
24748  250 

35858
0d394a82337e
handle hidden polymorphism in class target (without class target syntax, though)
haftmann
parents:
35845
diff
changeset

251 
fun these_unchecks thy = map (fn (c, (_, (ty, t))) => (t, Const (c, ty))) 
0d394a82337e
handle hidden polymorphism in class target (without class target syntax, though)
haftmann
parents:
35845
diff
changeset

252 
o these_operations thy; 
29577  253 

29632
c3d576157244
fixed reading of class specs: declare class operations in context
haftmann
parents:
29610
diff
changeset

254 
fun redeclare_const thy c = 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30344
diff
changeset

255 
let val b = Long_Name.base_name c 
29632
c3d576157244
fixed reading of class specs: declare class operations in context
haftmann
parents:
29610
diff
changeset

256 
in Sign.intern_const thy b = c ? Variable.declare_const (b, c) end; 
c3d576157244
fixed reading of class specs: declare class operations in context
haftmann
parents:
29610
diff
changeset

257 

29577  258 
fun synchronize_class_syntax sort base_sort ctxt = 
24914
95cda5dd58d5
added proper subclass concept; improved class target
haftmann
parents:
24901
diff
changeset

259 
let 
25344
00c2179db769
synchronize_syntax: improved declare_const (still inactive);
wenzelm
parents:
25326
diff
changeset

260 
val thy = ProofContext.theory_of ctxt; 
26596  261 
val algebra = Sign.classes_of thy; 
29577  262 
val operations = these_operations thy sort; 
26518  263 
fun subst_class_typ sort = map_type_tfree (K (TVar ((Name.aT, 0), sort))); 
264 
val primary_constraints = 

25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

265 
(map o apsnd) (subst_class_typ base_sort o fst o snd) operations; 
26518  266 
val secondary_constraints = 
25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

267 
(map o apsnd) (fn (class, (ty, _)) => subst_class_typ [class] ty) operations; 
26518  268 
fun improve (c, ty) = (case AList.lookup (op =) primary_constraints c 
26238  269 
of SOME ty' => (case try (Type.raw_match (ty', ty)) Vartab.empty 
270 
of SOME tyenv => (case Vartab.lookup tyenv (Name.aT, 0) 

33969  271 
of SOME (_, ty' as TVar (vi, sort)) => 
37145
01aa36932739
renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
wenzelm
parents:
36674
diff
changeset

272 
if Type_Infer.is_param vi 
26596  273 
andalso Sorts.sort_le algebra (base_sort, sort) 
274 
then SOME (ty', TFree (Name.aT, base_sort)) 

275 
else NONE 

26238  276 
 _ => NONE) 
277 
 NONE => NONE) 

278 
 NONE => NONE) 

279 
fun subst (c, ty) = Option.map snd (AList.lookup (op =) operations c); 

29577  280 
val unchecks = these_unchecks thy sort; 
25083  281 
in 
282 
ctxt 

29632
c3d576157244
fixed reading of class specs: declare class operations in context
haftmann
parents:
29610
diff
changeset

283 
> fold (redeclare_const thy o fst) primary_constraints 
26518  284 
> Overloading.map_improvable_syntax (K (((primary_constraints, secondary_constraints), 
26730  285 
(((improve, subst), true), unchecks)), false)) 
26518  286 
> Overloading.set_primary_constraints 
25083  287 
end; 
288 

289 
fun refresh_syntax class ctxt = 

25002  290 
let 
291 
val thy = ProofContext.theory_of ctxt; 

29358  292 
val base_sort = base_sort thy class; 
26238  293 
in synchronize_class_syntax [class] base_sort ctxt end; 
25002  294 

29632
c3d576157244
fixed reading of class specs: declare class operations in context
haftmann
parents:
29610
diff
changeset

295 
fun redeclare_operations thy sort = 
c3d576157244
fixed reading of class specs: declare class operations in context
haftmann
parents:
29610
diff
changeset

296 
fold (redeclare_const thy o fst) (these_operations thy sort); 
c3d576157244
fixed reading of class specs: declare class operations in context
haftmann
parents:
29610
diff
changeset

297 

29577  298 
fun begin sort base_sort ctxt = 
25083  299 
ctxt 
300 
> Variable.declare_term 

301 
(Logic.mk_type (TFree (Name.aT, base_sort))) 

29577  302 
> synchronize_class_syntax sort base_sort 
26238  303 
> Overloading.add_improvable_syntax; 
24901
d3cbf79769b9
added first version of userspace type system for class target
haftmann
parents:
24847
diff
changeset

304 

25311  305 
fun init class thy = 
306 
thy 

29509
1ff0f3f08a7b
migrated class package to new locale implementation
haftmann
parents:
29439
diff
changeset

307 
> Locale.init class 
29358  308 
> begin [class] (base_sort thy class); 
24914
95cda5dd58d5
added proper subclass concept; improved class target
haftmann
parents:
24901
diff
changeset

309 

24748  310 

27690
24738db98d34
some steps towards explicit class target for canonical interpretation
haftmann
parents:
27684
diff
changeset

311 
(* class target *) 
24738db98d34
some steps towards explicit class target for canonical interpretation
haftmann
parents:
27684
diff
changeset

312 

30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30344
diff
changeset

313 
val class_prefix = Logic.const_of_class o Long_Name.base_name; 
29526  314 

35858
0d394a82337e
handle hidden polymorphism in class target (without class target syntax, though)
haftmann
parents:
35845
diff
changeset

315 
fun declare class ((c, mx), (type_params, dict)) thy = 
27690
24738db98d34
some steps towards explicit class target for canonical interpretation
haftmann
parents:
27684
diff
changeset

316 
let 
29577  317 
val morph = morphism thy class; 
30344
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
30280
diff
changeset

318 
val b = Morphism.binding morph c; 
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
30280
diff
changeset

319 
val b_def = Morphism.binding morph (Binding.suffix_name "_dict" b); 
29577  320 
val c' = Sign.full_name thy b; 
29439  321 
val dict' = Morphism.term morph dict; 
35858
0d394a82337e
handle hidden polymorphism in class target (without class target syntax, though)
haftmann
parents:
35845
diff
changeset

322 
val ty' = map Term.fastype_of type_params > Term.fastype_of dict'; 
0d394a82337e
handle hidden polymorphism in class target (without class target syntax, though)
haftmann
parents:
35845
diff
changeset

323 
val def_eq = Logic.mk_equals (list_comb (Const (c', ty'), type_params), dict') 
29577  324 
> map_types Type.strip_sorts; 
27690
24738db98d34
some steps towards explicit class target for canonical interpretation
haftmann
parents:
27684
diff
changeset

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

327 
> Sign.declare_const ((b, Type.strip_sorts ty'), mx) 
29577  328 
> snd 
329 
> Thm.add_def false false (b_def, def_eq) 

36106
19deea200358
Thm.add_axiom/add_def: return internal name of foundational axiom;
wenzelm
parents:
35858
diff
changeset

330 
>> apsnd Thm.varifyT_global 
19deea200358
Thm.add_axiom/add_def: return internal name of foundational axiom;
wenzelm
parents:
35858
diff
changeset

331 
> (fn (_, def_thm) => PureThy.store_thm (b_def, def_thm) 
29577  332 
#> snd 
35858
0d394a82337e
handle hidden polymorphism in class target (without class target syntax, though)
haftmann
parents:
35845
diff
changeset

333 
#> null type_params ? register_operation class (c', (dict', SOME (Thm.symmetric def_thm)))) 
27690
24738db98d34
some steps towards explicit class target for canonical interpretation
haftmann
parents:
27684
diff
changeset

334 
> Sign.add_const_constraint (c', SOME ty') 
24738db98d34
some steps towards explicit class target for canonical interpretation
haftmann
parents:
27684
diff
changeset

335 
end; 
24738db98d34
some steps towards explicit class target for canonical interpretation
haftmann
parents:
27684
diff
changeset

336 

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

337 
fun abbrev class prmode ((c, mx), rhs) thy = 
27690
24738db98d34
some steps towards explicit class target for canonical interpretation
haftmann
parents:
27684
diff
changeset

338 
let 
29577  339 
val morph = morphism thy class; 
340 
val unchecks = these_unchecks thy [class]; 

30344
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
30280
diff
changeset

341 
val b = Morphism.binding morph c; 
29577  342 
val c' = Sign.full_name thy b; 
27690
24738db98d34
some steps towards explicit class target for canonical interpretation
haftmann
parents:
27684
diff
changeset

343 
val rhs' = Pattern.rewrite_term thy unchecks [] rhs; 
24738db98d34
some steps towards explicit class target for canonical interpretation
haftmann
parents:
27684
diff
changeset

344 
val ty' = Term.fastype_of rhs'; 
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35669
diff
changeset

345 
val rhs'' = map_types Logic.varifyT_global rhs'; 
27690
24738db98d34
some steps towards explicit class target for canonical interpretation
haftmann
parents:
27684
diff
changeset

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

348 
> Sign.add_abbrev (#1 prmode) (b, rhs'') 
29577  349 
> snd 
27690
24738db98d34
some steps towards explicit class target for canonical interpretation
haftmann
parents:
27684
diff
changeset

350 
> Sign.add_const_constraint (c', SOME ty') 
24738db98d34
some steps towards explicit class target for canonical interpretation
haftmann
parents:
27684
diff
changeset

351 
> Sign.notation true prmode [(Const (c', ty'), mx)] 
37146
f652333bbf8e
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
wenzelm
parents:
37145
diff
changeset

352 
> not (#1 prmode = Print_Mode.input) ? register_operation class (c', (rhs', NONE)) 
27690
24738db98d34
some steps towards explicit class target for canonical interpretation
haftmann
parents:
27684
diff
changeset

353 
end; 
24738db98d34
some steps towards explicit class target for canonical interpretation
haftmann
parents:
27684
diff
changeset

354 

24738db98d34
some steps towards explicit class target for canonical interpretation
haftmann
parents:
27684
diff
changeset

355 

31635  356 
(* simple subclasses *) 
357 

358 
local 

359 

360 
fun gen_classrel mk_prop classrel thy = 

361 
let 

362 
fun after_qed results = 

37246  363 
ProofContext.theory ((fold o fold) AxClass.add_classrel results); 
31635  364 
in 
365 
thy 

36610
bafd82950e24
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
wenzelm
parents:
36462
diff
changeset

366 
> ProofContext.init_global 
36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36106
diff
changeset

367 
> Proof.theorem NONE after_qed [[(mk_prop thy classrel, [])]] 
31635  368 
end; 
369 

370 
in 

371 

372 
val classrel = 

373 
gen_classrel (Logic.mk_classrel oo AxClass.cert_classrel); 

374 
val classrel_cmd = 

375 
gen_classrel (Logic.mk_classrel oo AxClass.read_classrel); 

376 

377 
end; (*local*) 

378 

379 

25462  380 
(** instantiation target **) 
381 

382 
(* bookkeeping *) 

383 

384 
datatype instantiation = Instantiation of { 

25864  385 
arities: string list * (string * sort) list * sort, 
25462  386 
params: ((string * string) * (string * typ)) list 
25603  387 
(*(instantiation parameter, type constructor), (local instantiation parameter, typ)*) 
25462  388 
} 
389 

33519  390 
structure Instantiation = Proof_Data 
25462  391 
( 
392 
type T = instantiation 

25536  393 
fun init _ = Instantiation { arities = ([], [], []), params = [] }; 
25462  394 
); 
395 

25485  396 
fun mk_instantiation (arities, params) = 
397 
Instantiation { arities = arities, params = params }; 

33671  398 
fun get_instantiation lthy = case Instantiation.get (Local_Theory.target_of lthy) 
25485  399 
of Instantiation data => data; 
33671  400 
fun map_instantiation f = (Local_Theory.target o Instantiation.map) 
25514  401 
(fn Instantiation { arities, params } => mk_instantiation (f (arities, params))); 
25462  402 

25514  403 
fun the_instantiation lthy = case get_instantiation lthy 
25536  404 
of { arities = ([], [], []), ... } => error "No instantiation target" 
25485  405 
 data => data; 
25462  406 

25485  407 
val instantiation_params = #params o get_instantiation; 
25462  408 

30519
c05c0199826f
coherent binding policy with primitive target operations
haftmann
parents:
30364
diff
changeset

409 
fun instantiation_param lthy b = instantiation_params lthy 
c05c0199826f
coherent binding policy with primitive target operations
haftmann
parents:
30364
diff
changeset

410 
> find_first (fn (_, (v, _)) => Binding.name_of b = v) 
25462  411 
> Option.map (fst o fst); 
412 

31869  413 
fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) = 
414 
let 

36610
bafd82950e24
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
wenzelm
parents:
36462
diff
changeset

415 
val ctxt = ProofContext.init_global thy; 
35669
a91c7ed801b8
added ProofContext.tsig_of  proforma version for local name space only, not logical content;
wenzelm
parents:
35315
diff
changeset

416 
val all_arities = map (fn raw_tyco => ProofContext.read_arity ctxt 
31869  417 
(raw_tyco, raw_sorts, raw_sort)) raw_tycos; 
418 
val tycos = map #1 all_arities; 

419 
val (_, sorts, sort) = hd all_arities; 

420 
val vs = Name.names Name.context Name.aT sorts; 

421 
in (tycos, vs, sort) end; 

422 

25462  423 

424 
(* syntax *) 

425 

26238  426 
fun synchronize_inst_syntax ctxt = 
25462  427 
let 
33969  428 
val Instantiation { params, ... } = Instantiation.get ctxt; 
31249  429 

33969  430 
val lookup_inst_param = AxClass.lookup_inst_param 
431 
(Sign.consts_of (ProofContext.theory_of ctxt)) params; 

31249  432 
fun subst (c, ty) = case lookup_inst_param (c, ty) 
433 
of SOME (v_ty as (_, ty)) => SOME (ty, Free v_ty) 

434 
 NONE => NONE; 

26238  435 
val unchecks = 
436 
map (fn ((c, _), v_ty as (_, ty)) => (Free v_ty, Const (c, ty))) params; 

437 
in 

438 
ctxt 

26259  439 
> Overloading.map_improvable_syntax 
26730  440 
(fn (((primary_constraints, _), (((improve, _), _), _)), _) => 
441 
(((primary_constraints, []), (((improve, subst), false), unchecks)), false)) 

26238  442 
end; 
25462  443 

38382  444 
fun resort_terms pp algebra consts constraints ts = 
445 
let 

446 
fun matchings (Const (c_ty as (c, _))) = (case constraints c 

447 
of NONE => I 

448 
 SOME sorts => fold2 (curry (Sorts.meet_sort algebra)) 

449 
(Consts.typargs consts c_ty) sorts) 

450 
 matchings _ = I 

451 
val tvartab = (fold o fold_aterms) matchings ts Vartab.empty 

452 
handle Sorts.CLASS_ERROR e => error (Sorts.class_error pp e); 

453 
val inst = map_type_tvar 

454 
(fn (vi, sort) => TVar (vi, the_default sort (Vartab.lookup tvartab vi))); 

455 
in if Vartab.is_empty tvartab then NONE else SOME ((map o map_types) inst ts) end; 

456 

25462  457 

458 
(* target *) 

459 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37393
diff
changeset

460 
val sanitize_name = (*necessary as long as "dirty" type identifiers are permitted*) 
25485  461 
let 
25574  462 
fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s 
463 
orelse s = "'" orelse s = "_"; 

25485  464 
val is_junk = not o is_valid andf Symbol.is_regular; 
465 
val junk = Scan.many is_junk; 

466 
val scan_valids = Symbol.scanner "Malformed input" 

467 
((junk  

468 
(Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.many is_valid >> implode) 

469 
 junk)) 

25999  470 
::: Scan.repeat ((Scan.many1 is_valid >> implode)  junk)); 
25485  471 
in 
472 
explode #> scan_valids #> implode 

473 
end; 

474 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37393
diff
changeset

475 
val type_name = sanitize_name o Long_Name.base_name; 
26259  476 

38382  477 
fun define_overloaded (c, U) v (b_def, rhs) = Local_Theory.theory_result 
478 
(AxClass.declare_overloaded (c, U) ##>> AxClass.define_overloaded b_def (c, rhs)) 

479 
##> (map_instantiation o apsnd) (filter_out (fn (_, (v', _)) => v' = v)) 

480 
##> Local_Theory.target synchronize_inst_syntax; 

481 

482 
fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy = 

483 
case instantiation_param lthy b 

484 
of SOME c => if mx <> NoSyn then error ("Illegal mixfix syntax for overloaded constant " ^ quote c) 

485 
else lthy > define_overloaded (c, U) (Binding.name_of b) (b_def, rhs) 

486 
 NONE => lthy > 

487 
Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params); 

488 

489 
fun pretty lthy = 

26518  490 
let 
38382  491 
val { arities = (tycos, vs, sort), params } = the_instantiation lthy; 
492 
val thy = ProofContext.theory_of lthy; 

493 
fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, map snd vs, sort); 

494 
fun pr_param ((c, _), (v, ty)) = 

495 
(Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==", 

496 
(Pretty.str o Sign.extern_const thy) c, Pretty.str "::", Syntax.pretty_typ_global thy ty]; 

497 
in Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params end; 

26518  498 

38382  499 
fun conclude lthy = 
500 
let 

501 
val (tycos, vs, sort) = (#arities o the_instantiation) lthy; 

502 
val thy = ProofContext.theory_of lthy; 

503 
val _ = map (fn tyco => if Sign.of_sort thy 

504 
(Type (tyco, map TFree vs), sort) 

505 
then () else error ("Missing instance proof for type " ^ quote (Sign.extern_type thy tyco))) 

506 
tycos; 

507 
in lthy end; 

508 

509 
fun instantiation (tycos, vs, sort) thy = 

25462  510 
let 
25536  511 
val _ = if null tycos then error "At least one arity must be given" else (); 
31249  512 
val class_params = these_params thy (filter (can (AxClass.get_info thy)) sort); 
29632
c3d576157244
fixed reading of class specs: declare class operations in context
haftmann
parents:
29610
diff
changeset

513 
fun get_param tyco (param, (_, (c, ty))) = 
c3d576157244
fixed reading of class specs: declare class operations in context
haftmann
parents:
29610
diff
changeset

514 
if can (AxClass.param_of_inst thy) (c, tyco) 
25603  515 
then NONE else SOME ((c, tyco), 
25864  516 
(param ^ "_" ^ type_name tyco, map_atyps (K (Type (tyco, map TFree vs))) ty)); 
31249  517 
val params = map_product get_param tycos class_params > map_filter I; 
26518  518 
val primary_constraints = map (apsnd 
31249  519 
(map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) class_params; 
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26761
diff
changeset

520 
val pp = Syntax.pp_global thy; 
26518  521 
val algebra = Sign.classes_of thy 
522 
> fold (fn tyco => Sorts.add_arities pp 

523 
(tyco, map (fn class => (class, map snd vs)) sort)) tycos; 

524 
val consts = Sign.consts_of thy; 

525 
val improve_constraints = AList.lookup (op =) 

31249  526 
(map (fn (_, (class, (c, _))) => (c, [[class]])) class_params); 
33967  527 
fun resort_check ts ctxt = case resort_terms (Syntax.pp ctxt) algebra consts improve_constraints ts 
26518  528 
of NONE => NONE 
529 
 SOME ts' => SOME (ts', ctxt); 

31249  530 
val lookup_inst_param = AxClass.lookup_inst_param consts params; 
31210  531 
val typ_instance = Type.typ_instance (Sign.tsig_of thy); 
31249  532 
fun improve (c, ty) = case lookup_inst_param (c, ty) 
533 
of SOME (_, ty') => if typ_instance (ty', ty) then SOME (ty, ty') else NONE 

26259  534 
 NONE => NONE; 
25485  535 
in 
536 
thy 

32379
a97e9caebd60
additional checkpoints avoid problems in error situations
haftmann
parents:
32074
diff
changeset

537 
> Theory.checkpoint 
36610
bafd82950e24
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
wenzelm
parents:
36462
diff
changeset

538 
> ProofContext.init_global 
31249  539 
> Instantiation.put (mk_instantiation ((tycos, vs, sort), params)) 
27281  540 
> fold (Variable.declare_typ o TFree) vs 
31249  541 
> fold (Variable.declare_names o Free o snd) params 
26259  542 
> (Overloading.map_improvable_syntax o apfst) 
29969
9dbb046136d0
more precise improvement in instantiation user space type system
haftmann
parents:
29632
diff
changeset

543 
(K ((primary_constraints, []), (((improve, K NONE), false), []))) 
26259  544 
> Overloading.add_improvable_syntax 
26518  545 
> Context.proof_map (Syntax.add_term_check 0 "resorting" resort_check) 
26238  546 
> synchronize_inst_syntax 
38382  547 
> Local_Theory.init NONE "" 
548 
{define = Generic_Target.define foundation, 

549 
notes = Generic_Target.notes 

550 
(fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts), 

551 
abbrev = Generic_Target.abbrev 

552 
(fn prmode => fn (b, mx) => fn (t, _) => fn _ => Generic_Target.theory_abbrev prmode ((b, mx), t)), 

553 
declaration = K Generic_Target.theory_declaration, 

554 
syntax_declaration = K Generic_Target.theory_declaration, 

555 
pretty = pretty, 

556 
exit = Local_Theory.target_of o conclude} 

25485  557 
end; 
558 

38382  559 
fun instantiation_cmd arities thy = 
560 
instantiation (read_multi_arity thy arities) thy; 

26238  561 

25485  562 
fun gen_instantiation_instance do_proof after_qed lthy = 
563 
let 

25864  564 
val (tycos, vs, sort) = (#arities o the_instantiation) lthy; 
565 
val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, map snd vs, sort)) tycos; 

25462  566 
fun after_qed' results = 
37246  567 
Local_Theory.theory (fold (AxClass.add_arity o Thm.varifyT_global) results) 
25462  568 
#> after_qed; 
569 
in 

570 
lthy 

571 
> do_proof after_qed' arities_proof 

572 
end; 

573 

25485  574 
val instantiation_instance = gen_instantiation_instance (fn after_qed => fn ts => 
36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36106
diff
changeset

575 
Proof.theorem NONE (after_qed o map the_single) (map (fn t => [(t, [])]) ts)); 
25462  576 

25485  577 
fun prove_instantiation_instance tac = gen_instantiation_instance (fn after_qed => 
25502  578 
fn ts => fn lthy => after_qed (map (fn t => Goal.prove lthy [] [] t 
579 
(fn {context, ...} => tac context)) ts) lthy) I; 

25462  580 

28666  581 
fun prove_instantiation_exit tac = prove_instantiation_instance tac 
33671  582 
#> Local_Theory.exit_global; 
28666  583 

584 
fun prove_instantiation_exit_result f tac x lthy = 

585 
let 

29439  586 
val morph = ProofContext.export_morphism lthy 
36610
bafd82950e24
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
wenzelm
parents:
36462
diff
changeset

587 
(ProofContext.init_global (ProofContext.theory_of lthy)); 
29439  588 
val y = f morph x; 
28666  589 
in 
590 
lthy 

591 
> prove_instantiation_exit (fn ctxt => tac ctxt y) 

592 
> pair y 

593 
end; 

594 

29526  595 

31635  596 
(* simplified instantiation interface with no class parameter *) 
597 

31869  598 
fun instance_arity_cmd raw_arities thy = 
31635  599 
let 
31869  600 
val (tycos, vs, sort) = read_multi_arity thy raw_arities; 
601 
val sorts = map snd vs; 

602 
val arities = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos; 

31635  603 
fun after_qed results = ProofContext.theory 
37246  604 
((fold o fold) AxClass.add_arity results); 
31635  605 
in 
606 
thy 

36610
bafd82950e24
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
wenzelm
parents:
36462
diff
changeset

607 
> ProofContext.init_global 
36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36106
diff
changeset

608 
> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) arities) 
31635  609 
end; 
610 

611 

29526  612 
(** tactics and methods **) 
613 

614 
fun intro_classes_tac facts st = 

615 
let 

616 
val thy = Thm.theory_of_thm st; 

617 
val classes = Sign.all_classes thy; 

618 
val class_trivs = map (Thm.class_triv thy) classes; 

619 
val class_intros = map_filter (try (#intro o AxClass.get_info thy)) classes; 

620 
val assm_intros = all_assm_intros thy; 

621 
in 

622 
Method.intros_tac (class_trivs @ class_intros @ assm_intros) facts st 

623 
end; 

624 

625 
fun default_intro_tac ctxt [] = 

29577  626 
intro_classes_tac [] ORELSE Locale.intro_locales_tac true ctxt [] 
29526  627 
 default_intro_tac _ _ = no_tac; 
628 

629 
fun default_tac rules ctxt facts = 

630 
HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE 

631 
default_intro_tac ctxt facts; 

632 

633 
val _ = Context.>> (Context.map_theory 

30515  634 
(Method.setup (Binding.name "intro_classes") (Scan.succeed (K (METHOD intro_classes_tac))) 
635 
"backchain introduction rules of classes" #> 

636 
Method.setup (Binding.name "default") (Attrib.thms >> (METHOD oo default_tac)) 

637 
"apply some intro/elim rule")); 

29526  638 

24218  639 
end; 
25683  640 