author  ballarin 
Sat, 31 Jul 2010 21:14:20 +0200  
changeset 38107  3a46cebd7983 
parent 37678  0040bafffdef 
child 38348  cf7b2121ad9d 
permissions  rwrr 
29358  1 
(* Title: Pure/Isar/class_target.ML 
24218  2 
Author: Florian Haftmann, TU Muenchen 
3 

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

29358  7 
signature CLASS_TARGET = 
24218  8 
sig 
25462  9 
(*classes*) 
29358  10 
val register: class > class list > ((string * typ) * (string * typ)) list 
32850  11 
> sort > morphism > morphism > thm option > thm option > thm 
29526  12 
> theory > theory 
25485  13 

29526  14 
val is_class: theory > class > bool 
15 
val base_sort: theory > class > sort 

16 
val rules: theory > class > thm option * thm 

17 
val these_params: theory > sort > (string * (class * (string * typ))) list 

18 
val these_defs: theory > sort > thm list 

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

19 
val these_operations: theory > sort 
0d394a82337e
handle hidden polymorphism in class target (without class target syntax, though)
haftmann
parents:
35845
diff
changeset

20 
> (string * (class * (typ * term))) list 
29526  21 
val print_classes: theory > unit 
22 

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

25 
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

26 
val abbrev: class > Syntax.mode > (binding * mixfix) * term > theory > theory 
29526  27 
val class_prefix: string > string 
25083  28 
val refresh_syntax: class > Proof.context > Proof.context 
29632
c3d576157244
fixed reading of class specs: declare class operations in context
haftmann
parents:
29610
diff
changeset

29 
val redeclare_operations: theory > sort > Proof.context > Proof.context 
25485  30 

25462  31 
(*instances*) 
26247  32 
val init_instantiation: string list * (string * sort) list * sort 
35126  33 
> theory > Proof.context 
31869  34 
val instance_arity_cmd: xstring list * xstring list * xstring > theory > Proof.state 
26247  35 
val instantiation_instance: (local_theory > local_theory) 
36 
> local_theory > Proof.state 

37 
val prove_instantiation_instance: (Proof.context > tactic) 

38 
> local_theory > local_theory 

28666  39 
val prove_instantiation_exit: (Proof.context > tactic) 
40 
> local_theory > theory 

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

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

25485  43 
val conclude_instantiation: local_theory > local_theory 
30519
c05c0199826f
coherent binding policy with primitive target operations
haftmann
parents:
30364
diff
changeset

44 
val instantiation_param: local_theory > binding > string option 
c05c0199826f
coherent binding policy with primitive target operations
haftmann
parents:
30364
diff
changeset

45 
val confirm_declaration: binding > local_theory > local_theory 
25603  46 
val pretty_instantiation: local_theory > Pretty.T 
31869  47 
val read_multi_arity: theory > xstring list * xstring list * xstring 
48 
> string list * (string * sort) list * sort 

26259  49 
val type_name: string > string 
25485  50 

31635  51 
(*subclasses*) 
52 
val register_subclass: class * class > morphism option > Element.witness option 

53 
> morphism > theory > theory 

54 
val classrel: class * class > theory > Proof.state 

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

56 

57 
(*tactics*) 

29526  58 
val intro_classes_tac: thm list > tactic 
59 
val default_intro_tac: Proof.context > thm list > tactic 

24218  60 
end; 
61 

29358  62 
structure Class_Target : CLASS_TARGET = 
24218  63 
struct 
64 

24589  65 
(** class data **) 
24218  66 

67 
datatype class_data = ClassData of { 

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

68 

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

69 
(* static part *) 
24218  70 
consts: (string * string) list 
24836  71 
(*locale parameter ~> constant name*), 
25062  72 
base_sort: sort, 
29545  73 
base_morph: morphism 
29439  74 
(*static part of canonical morphism*), 
32850  75 
export_morph: morphism, 
25618  76 
assm_intro: thm option, 
77 
of_class: thm, 

78 
axiom: thm option, 

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

79 

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

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

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

83 

24657  84 
}; 
24218  85 

32850  86 
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

87 
(defs, operations)) = 
29526  88 
ClassData { consts = consts, base_sort = base_sort, 
32850  89 
base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro, 
90 
of_class = of_class, axiom = axiom, defs = defs, operations = operations }; 

91 
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

92 
of_class, axiom, defs, operations }) = 
32850  93 
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

94 
(defs, operations))); 
25038  95 
fun merge_class_data _ (ClassData { consts = consts, 
32850  96 
base_sort = base_sort, base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro, 
25618  97 
of_class = of_class, axiom = axiom, defs = defs1, operations = operations1 }, 
32850  98 
ClassData { consts = _, base_sort = _, base_morph = _, export_morph = _, assm_intro = _, 
25618  99 
of_class = _, axiom = _, defs = defs2, operations = operations2 }) = 
32850  100 
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

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

102 
AList.merge (op =) (K true) (operations1, operations2))); 
24218  103 

33522  104 
structure ClassData = Theory_Data 
24218  105 
( 
25038  106 
type T = class_data Graph.T 
107 
val empty = Graph.empty; 

24218  108 
val extend = I; 
33522  109 
val merge = Graph.join merge_class_data; 
24218  110 
); 
111 

112 

113 
(* queries *) 

114 

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

117 
 NONE => NONE; 

24218  118 

24589  119 
fun the_class_data thy class = case lookup_class_data thy class 
25020  120 
of NONE => error ("Undeclared class " ^ quote class) 
24589  121 
 SOME data => data; 
24218  122 

25038  123 
val is_class = is_some oo lookup_class_data; 
124 

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

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

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

127 

25002  128 
fun these_params thy = 
24218  129 
let 
130 
fun params class = 

131 
let 

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

132 
val const_typs = (#params o AxClass.get_info thy) class; 
24657  133 
val const_names = (#consts o the_class_data thy) class; 
24218  134 
in 
26518  135 
(map o apsnd) 
136 
(fn c => (class, (c, (the o AList.lookup (op =) const_typs) c))) const_names 

24218  137 
end; 
138 
in maps params o ancestry thy end; 

139 

29526  140 
val base_sort = #base_sort oo the_class_data; 
141 

142 
fun rules thy class = 

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

144 
in (axiom, of_class) end; 

145 

146 
fun all_assm_intros thy = 

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

24218  149 

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

29358  152 

29526  153 
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

154 
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

155 
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

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

158 

24218  159 
fun print_classes thy = 
160 
let 

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

161 
val ctxt = ProofContext.init_global thy; 
24218  162 
val algebra = Sign.classes_of thy; 
163 
val arities = 

164 
Symtab.empty 

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

166 
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

167 
(Sorts.arities_of algebra); 
24218  168 
val the_arities = these o Symtab.lookup arities; 
169 
fun mk_arity class tyco = 

170 
let 

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

24920  172 
in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end; 
24218  173 
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

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

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

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

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

185 
] 

186 
] 

187 
in 

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

24218  190 
end; 
191 

192 

193 
(* updaters *) 

194 

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

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

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

206 
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

207 
of SOME eq_morph => fold (fn cls => fn thy => 
38107  208 
Context.theory_map (Locale.amend_registration (cls, base_morphism thy cls) 
209 
(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

210 
 NONE => thy; 
29526  211 

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

212 
fun register_operation class (c, (t, some_def)) thy = 
25062  213 
let 
29358  214 
val base_sort = base_sort thy class; 
29439  215 
val prep_typ = map_type_tfree 
216 
(fn (v, sort) => if Name.aT = v 

217 
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

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

219 
val ty' = Term.fastype_of t'; 
25062  220 
in 
221 
thy 

222 
> (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

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

225 
(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

226 
> activate_defs class (the_list some_def) 
25062  227 
end; 
24218  228 

29558  229 
fun register_subclass (sub, sup) some_dep_morph some_wit export thy = 
25618  230 
let 
29558  231 
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

232 
[Option.map (Drule.export_without_context_open o Element.conclude_witness) some_wit, 
29558  233 
(fst o rules thy) sub]; 
29610  234 
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

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

237 
val diff_sort = Sign.complete_sort thy [sup] 
31012  238 
> subtract (op =) (Sign.complete_sort thy [sub]) 
239 
> filter (is_class thy); 

32074  240 
val add_dependency = case some_dep_morph 
241 
of SOME dep_morph => Locale.add_dependency sub 

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

243 
 NONE => I 

25618  244 
in 
245 
thy 

37246  246 
> AxClass.add_classrel classrel 
25618  247 
> ClassData.map (Graph.add_edge (sub, sup)) 
29526  248 
> activate_defs sub (these_defs thy diff_sort) 
32074  249 
> add_dependency 
24218  250 
end; 
251 

252 

24589  253 
(** classes and class target **) 
24218  254 

25002  255 
(* class context syntax *) 
24748  256 

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

257 
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

258 
o these_operations thy; 
29577  259 

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

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

261 
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

262 
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

263 

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

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

266 
val thy = ProofContext.theory_of ctxt; 
26596  267 
val algebra = Sign.classes_of thy; 
29577  268 
val operations = these_operations thy sort; 
26518  269 
fun subst_class_typ sort = map_type_tfree (K (TVar ((Name.aT, 0), sort))); 
270 
val primary_constraints = 

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

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

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

33969  277 
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

278 
if Type_Infer.is_param vi 
26596  279 
andalso Sorts.sort_le algebra (base_sort, sort) 
280 
then SOME (ty', TFree (Name.aT, base_sort)) 

281 
else NONE 

26238  282 
 _ => NONE) 
283 
 NONE => NONE) 

284 
 NONE => NONE) 

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

29577  286 
val unchecks = these_unchecks thy sort; 
25083  287 
in 
288 
ctxt 

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

289 
> fold (redeclare_const thy o fst) primary_constraints 
26518  290 
> Overloading.map_improvable_syntax (K (((primary_constraints, secondary_constraints), 
26730  291 
(((improve, subst), true), unchecks)), false)) 
26518  292 
> Overloading.set_primary_constraints 
25083  293 
end; 
294 

295 
fun refresh_syntax class ctxt = 

25002  296 
let 
297 
val thy = ProofContext.theory_of ctxt; 

29358  298 
val base_sort = base_sort thy class; 
26238  299 
in synchronize_class_syntax [class] base_sort ctxt end; 
25002  300 

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

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

302 
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

303 

29577  304 
fun begin sort base_sort ctxt = 
25083  305 
ctxt 
306 
> Variable.declare_term 

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

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

310 

25311  311 
fun init class thy = 
312 
thy 

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

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

315 

24748  316 

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

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

318 

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

319 
val class_prefix = Logic.const_of_class o Long_Name.base_name; 
29526  320 

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

321 
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

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

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

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

328 
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

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

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

333 
> Sign.declare_const ((b, Type.strip_sorts ty'), mx) 
29577  334 
> snd 
335 
> 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

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

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

339 
#> 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

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

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

342 

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

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

344 
let 
29577  345 
val morph = morphism thy class; 
346 
val unchecks = these_unchecks thy [class]; 

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

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

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

350 
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

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

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

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

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

357 
> 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

358 
> 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

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

360 

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

361 

31635  362 
(* simple subclasses *) 
363 

364 
local 

365 

366 
fun gen_classrel mk_prop classrel thy = 

367 
let 

368 
fun after_qed results = 

37246  369 
ProofContext.theory ((fold o fold) AxClass.add_classrel results); 
31635  370 
in 
371 
thy 

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

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

373 
> Proof.theorem NONE after_qed [[(mk_prop thy classrel, [])]] 
31635  374 
end; 
375 

376 
in 

377 

378 
val classrel = 

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

380 
val classrel_cmd = 

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

382 

383 
end; (*local*) 

384 

385 

25462  386 
(** instantiation target **) 
387 

388 
(* bookkeeping *) 

389 

390 
datatype instantiation = Instantiation of { 

25864  391 
arities: string list * (string * sort) list * sort, 
25462  392 
params: ((string * string) * (string * typ)) list 
25603  393 
(*(instantiation parameter, type constructor), (local instantiation parameter, typ)*) 
25462  394 
} 
395 

33519  396 
structure Instantiation = Proof_Data 
25462  397 
( 
398 
type T = instantiation 

25536  399 
fun init _ = Instantiation { arities = ([], [], []), params = [] }; 
25462  400 
); 
401 

25485  402 
fun mk_instantiation (arities, params) = 
403 
Instantiation { arities = arities, params = params }; 

33671  404 
fun get_instantiation lthy = case Instantiation.get (Local_Theory.target_of lthy) 
25485  405 
of Instantiation data => data; 
33671  406 
fun map_instantiation f = (Local_Theory.target o Instantiation.map) 
25514  407 
(fn Instantiation { arities, params } => mk_instantiation (f (arities, params))); 
25462  408 

25514  409 
fun the_instantiation lthy = case get_instantiation lthy 
25536  410 
of { arities = ([], [], []), ... } => error "No instantiation target" 
25485  411 
 data => data; 
25462  412 

25485  413 
val instantiation_params = #params o get_instantiation; 
25462  414 

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

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

416 
> find_first (fn (_, (v, _)) => Binding.name_of b = v) 
25462  417 
> Option.map (fst o fst); 
418 

31869  419 
fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) = 
420 
let 

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

421 
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

422 
val all_arities = map (fn raw_tyco => ProofContext.read_arity ctxt 
31869  423 
(raw_tyco, raw_sorts, raw_sort)) raw_tycos; 
424 
val tycos = map #1 all_arities; 

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

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

427 
in (tycos, vs, sort) end; 

428 

25462  429 

430 
(* syntax *) 

431 

26238  432 
fun synchronize_inst_syntax ctxt = 
25462  433 
let 
33969  434 
val Instantiation { params, ... } = Instantiation.get ctxt; 
31249  435 

33969  436 
val lookup_inst_param = AxClass.lookup_inst_param 
437 
(Sign.consts_of (ProofContext.theory_of ctxt)) params; 

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

440 
 NONE => NONE; 

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

443 
in 

444 
ctxt 

26259  445 
> Overloading.map_improvable_syntax 
26730  446 
(fn (((primary_constraints, _), (((improve, _), _), _)), _) => 
447 
(((primary_constraints, []), (((improve, subst), false), unchecks)), false)) 

26238  448 
end; 
25462  449 

450 

451 
(* target *) 

452 

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

453 
val sanitize_name = (*necessary as long as "dirty" type identifiers are permitted*) 
25485  454 
let 
25574  455 
fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s 
456 
orelse s = "'" orelse s = "_"; 

25485  457 
val is_junk = not o is_valid andf Symbol.is_regular; 
458 
val junk = Scan.many is_junk; 

459 
val scan_valids = Symbol.scanner "Malformed input" 

460 
((junk  

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

462 
 junk)) 

25999  463 
::: Scan.repeat ((Scan.many1 is_valid >> implode)  junk)); 
25485  464 
in 
465 
explode #> scan_valids #> implode 

466 
end; 

467 

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

468 
val type_name = sanitize_name o Long_Name.base_name; 
26259  469 

26518  470 
fun resort_terms pp algebra consts constraints ts = 
471 
let 

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

473 
of NONE => I 

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

475 
(Consts.typargs consts c_ty) sorts) 

476 
 matchings _ = I 

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

26642
454d11701fa4
Sorts.class_error: produce message only (formerly msg_class_error);
wenzelm
parents:
26628
diff
changeset

478 
handle Sorts.CLASS_ERROR e => error (Sorts.class_error pp e); 
27089
480f19078b65
fixed wrong treatment of type variables in instantiation target
haftmann
parents:
26995
diff
changeset

479 
val inst = map_type_tvar 
480f19078b65
fixed wrong treatment of type variables in instantiation target
haftmann
parents:
26995
diff
changeset

480 
(fn (vi, sort) => TVar (vi, the_default sort (Vartab.lookup tvartab vi))); 
26518  481 
in if Vartab.is_empty tvartab then NONE else SOME ((map o map_types) inst ts) end; 
482 

25864  483 
fun init_instantiation (tycos, vs, sort) thy = 
25462  484 
let 
25536  485 
val _ = if null tycos then error "At least one arity must be given" else (); 
31249  486 
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

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

488 
if can (AxClass.param_of_inst thy) (c, tyco) 
25603  489 
then NONE else SOME ((c, tyco), 
25864  490 
(param ^ "_" ^ type_name tyco, map_atyps (K (Type (tyco, map TFree vs))) ty)); 
31249  491 
val params = map_product get_param tycos class_params > map_filter I; 
26518  492 
val primary_constraints = map (apsnd 
31249  493 
(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

494 
val pp = Syntax.pp_global thy; 
26518  495 
val algebra = Sign.classes_of thy 
496 
> fold (fn tyco => Sorts.add_arities pp 

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

498 
val consts = Sign.consts_of thy; 

499 
val improve_constraints = AList.lookup (op =) 

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

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

26259  508 
 NONE => NONE; 
25485  509 
in 
510 
thy 

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

511 
> 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

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

517 
(K ((primary_constraints, []), (((improve, K NONE), false), []))) 
26259  518 
> Overloading.add_improvable_syntax 
26518  519 
> Context.proof_map (Syntax.add_term_check 0 "resorting" resort_check) 
26238  520 
> synchronize_inst_syntax 
25485  521 
end; 
522 

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

523 
fun confirm_declaration b = (map_instantiation o apsnd) 
c05c0199826f
coherent binding policy with primitive target operations
haftmann
parents:
30364
diff
changeset

524 
(filter_out (fn (_, (c', _)) => c' = Binding.name_of b)) 
33671  525 
#> Local_Theory.target synchronize_inst_syntax 
26238  526 

25485  527 
fun gen_instantiation_instance do_proof after_qed lthy = 
528 
let 

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

25462  531 
fun after_qed' results = 
37246  532 
Local_Theory.theory (fold (AxClass.add_arity o Thm.varifyT_global) results) 
25462  533 
#> after_qed; 
534 
in 

535 
lthy 

536 
> do_proof after_qed' arities_proof 

537 
end; 

538 

25485  539 
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

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

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

25462  545 

28666  546 
fun prove_instantiation_exit tac = prove_instantiation_instance tac 
33671  547 
#> Local_Theory.exit_global; 
28666  548 

549 
fun prove_instantiation_exit_result f tac x lthy = 

550 
let 

29439  551 
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

552 
(ProofContext.init_global (ProofContext.theory_of lthy)); 
29439  553 
val y = f morph x; 
28666  554 
in 
555 
lthy 

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

557 
> pair y 

558 
end; 

559 

25462  560 
fun conclude_instantiation lthy = 
561 
let 

33969  562 
val (tycos, vs, sort) = (#arities o the_instantiation) lthy; 
25462  563 
val thy = ProofContext.theory_of lthy; 
25597
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25574
diff
changeset

564 
val _ = map (fn tyco => if Sign.of_sort thy 
25864  565 
(Type (tyco, map TFree vs), sort) 
25462  566 
then () else error ("Missing instance proof for type " ^ quote (Sign.extern_type thy tyco))) 
25597
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25574
diff
changeset

567 
tycos; 
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25574
diff
changeset

568 
in lthy end; 
25462  569 

25603  570 
fun pretty_instantiation lthy = 
571 
let 

33969  572 
val { arities = (tycos, vs, sort), params } = the_instantiation lthy; 
25603  573 
val thy = ProofContext.theory_of lthy; 
25864  574 
fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, map snd vs, sort); 
25603  575 
fun pr_param ((c, _), (v, ty)) = 
25864  576 
(Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==", 
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26761
diff
changeset

577 
(Pretty.str o Sign.extern_const thy) c, Pretty.str "::", Syntax.pretty_typ_global thy ty]; 
25603  578 
in 
579 
(Pretty.block o Pretty.fbreaks) 

580 
(Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params) 

581 
end; 

582 

29526  583 

31635  584 
(* simplified instantiation interface with no class parameter *) 
585 

31869  586 
fun instance_arity_cmd raw_arities thy = 
31635  587 
let 
31869  588 
val (tycos, vs, sort) = read_multi_arity thy raw_arities; 
589 
val sorts = map snd vs; 

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

31635  591 
fun after_qed results = ProofContext.theory 
37246  592 
((fold o fold) AxClass.add_arity results); 
31635  593 
in 
594 
thy 

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

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

596 
> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) arities) 
31635  597 
end; 
598 

599 

29526  600 
(** tactics and methods **) 
601 

602 
fun intro_classes_tac facts st = 

603 
let 

604 
val thy = Thm.theory_of_thm st; 

605 
val classes = Sign.all_classes thy; 

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

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

608 
val assm_intros = all_assm_intros thy; 

609 
in 

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

611 
end; 

612 

613 
fun default_intro_tac ctxt [] = 

29577  614 
intro_classes_tac [] ORELSE Locale.intro_locales_tac true ctxt [] 
29526  615 
 default_intro_tac _ _ = no_tac; 
616 

617 
fun default_tac rules ctxt facts = 

618 
HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE 

619 
default_intro_tac ctxt facts; 

620 

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

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

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

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

29526  626 

24218  627 
end; 
25683  628 