author  haftmann 
Wed, 28 Jun 2006 14:36:09 +0200  
changeset 19957  91ba241a1678 
parent 19953  2f54a51f1801 
child 19966  88bbe97ed0b0 
permissions  rwrr 
18168  1 
(* Title: Pure/Tools/class_package.ML 
2 
ID: $Id$ 

3 
Author: Florian Haftmann, TU Muenchen 

4 

19468  5 
Type classes derived from primitive axclasses and locales. 
18168  6 
*) 
7 

8 
signature CLASS_PACKAGE = 

9 
sig 

19150  10 
val class: bstring > class list > Element.context list > theory 
18515  11 
> ProofContext.context * theory 
19150  12 
val class_i: bstring > class list > Element.context_i list > theory 
18515  13 
> ProofContext.context * theory 
19150  14 
val instance_arity: (xstring * string list) * string 
19136  15 
> bstring * Attrib.src list > ((bstring * Attrib.src list) * string) list 
18575  16 
> theory > Proof.state 
19150  17 
val instance_arity_i: (string * sort list) * sort 
19136  18 
> bstring * attribute list > ((bstring * attribute list) * term) list 
18575  19 
> theory > Proof.state 
19150  20 
val prove_instance_arity: tactic > (string * sort list) * sort 
19136  21 
> bstring * attribute list > ((bstring * attribute list) * term) list 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

22 
> theory > theory 
19150  23 
val instance_sort: string * string > theory > Proof.state 
24 
val instance_sort_i: class * sort > theory > Proof.state 

25 
val prove_instance_sort: tactic > class * sort > theory > theory 

18168  26 

19253  27 
val use_cp_instance: bool ref; 
28 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

29 
val intern_class: theory > xstring > class 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

30 
val intern_sort: theory > sort > sort 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

31 
val extern_class: theory > class > xstring 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

32 
val extern_sort: theory > sort > sort 
18755  33 
val certify_class: theory > class > class 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

34 
val certify_sort: theory > sort > sort 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

35 
val read_sort: theory > string > sort 
18884  36 
val operational_sort_of: theory > sort > sort 
18702  37 
val the_superclasses: theory > class > class list 
38 
val the_consts_sign: theory > class > string * (string * typ) list 

39 
val the_inst_sign: theory > class * string > (string * sort) list * (string * typ) list 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

40 

18702  41 
val print_classes: theory > unit 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

42 
val intro_classes_tac: thm list > tactic 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

43 
val default_intro_classes_tac: thm list > tactic 
18168  44 

45 
type sortcontext = (string * sort) list 

18884  46 
datatype classlookup = Instance of (class * string) * classlookup list list 
19253  47 
 Lookup of class list * (string * (int * int)) 
19953
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19929
diff
changeset

48 
val sortcontext_of_typ: theory > typ > sortcontext 
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19929
diff
changeset

49 
val sortlookup: theory > sort * typ > classlookup list 
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19929
diff
changeset

50 
val sortlookups_const: theory > string * typ > classlookup list list 
18168  51 
end; 
52 

53 
structure ClassPackage: CLASS_PACKAGE = 

54 
struct 

55 

56 

19957  57 
(* auxiliary *) 
58 

59 
fun instantiations_of thy (ty, ty') = 

60 
let 

61 
val vartab = typ_tvars ty; 

62 
fun prep_vartab (v, (_, ty)) = 

63 
case (the o AList.lookup (op =) vartab) v 

64 
of [] => NONE 

65 
 sort => SOME ((v, sort), ty); 

66 
in case try (Sign.typ_match thy (ty, ty')) Vartab.empty 

67 
of NONE => NONE 

68 
 SOME vartab => 

69 
SOME ((map_filter prep_vartab o Vartab.dest) vartab) 

70 
end; 

71 

72 

18708  73 
(* theory data *) 
18168  74 

19456  75 
datatype class_data = ClassData of { 
18575  76 
name_locale: string, 
77 
name_axclass: string, 

78 
var: string, 

19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

79 
consts: (string * (string * typ)) list 
19957  80 
(*locale parameter ~> toplevel constant*) 
18168  81 
}; 
82 

19456  83 
fun rep_classdata (ClassData c) = c; 
84 

18575  85 
structure ClassData = TheoryDataFun ( 
18168  86 
struct 
87 
val name = "Pure/classes"; 

19957  88 
type T = class_data Graph.T; 
89 
val empty = Graph.empty; 

18168  90 
val copy = I; 
91 
val extend = I; 

19957  92 
fun merge _ = Graph.merge (K true); 
93 
fun print thy gr = 

18575  94 
let 
19928  95 
fun pretty_class gr (name, ClassData {name_locale, name_axclass, var, consts}) = 
18575  96 
(Pretty.block o Pretty.fbreaks) [ 
97 
Pretty.str ("class " ^ name ^ ":"), 

98 
(Pretty.block o Pretty.fbreaks) ( 

99 
Pretty.str "superclasses: " 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

100 
:: (map Pretty.str o Graph.imm_succs gr) name 
18575  101 
), 
102 
Pretty.str ("locale: " ^ name_locale), 

103 
Pretty.str ("axclass: " ^ name_axclass), 

104 
Pretty.str ("class variable: " ^ var), 

105 
(Pretty.block o Pretty.fbreaks) ( 

106 
Pretty.str "constants: " 

19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

107 
:: map (fn (_, (c, ty)) => Pretty.str (c ^ " :: " ^ Sign.string_of_typ thy ty)) consts 
18575  108 
) 
109 
] 

110 
in 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

111 
(Pretty.writeln o Pretty.chunks o map (pretty_class gr) 
19468  112 
o AList.make (Graph.get_node gr) o flat o Graph.strong_conn) gr 
18575  113 
end; 
18168  114 
end 
115 
); 

116 

18708  117 
val _ = Context.add_setup ClassData.init; 
18575  118 
val print_classes = ClassData.print; 
119 

19038  120 

121 
(* queries *) 

122 

19957  123 
val lookup_class_data = Option.map rep_classdata oo try o Graph.get_node o ClassData.get; 
18168  124 

19038  125 
fun the_class_data thy class = 
18168  126 
case lookup_class_data thy class 
18755  127 
of NONE => error ("undeclared operational class " ^ quote class) 
18168  128 
 SOME data => data; 
129 

19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

130 
val is_class = is_some oo lookup_class_data; 
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

131 

5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

132 
fun is_operational_class thy cls = 
18702  133 
lookup_class_data thy cls 
134 
> Option.map (not o null o #consts) 

135 
> the_default false; 

18168  136 

19953
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19929
diff
changeset

137 
fun operational_sort_of thy = 
18360  138 
let 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

139 
fun get_sort class = 
19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

140 
if is_operational_class thy class 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

141 
then [class] 
19412  142 
else operational_sort_of thy (Sign.super_classes thy class); 
19953
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19929
diff
changeset

143 
in Sign.certify_sort thy o maps get_sort end; 
18168  144 

18702  145 
fun the_superclasses thy class = 
18515  146 
if is_class thy class 
147 
then 

19412  148 
Sign.super_classes thy class 
18884  149 
> operational_sort_of thy 
18515  150 
else 
19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

151 
error ("no class: " ^ class); 
18168  152 

19038  153 
fun the_ancestry thy classes = 
154 
let 

155 
fun ancestry class anc = 

156 
anc 

157 
> cons class 

158 
> fold ancestry (the_superclasses thy class); 

159 
in fold ancestry classes [] end; 

160 

161 
fun subst_clsvar v ty_subst = 

162 
map_type_tfree (fn u as (w, _) => 

163 
if w = v then ty_subst else TFree u); 

164 

19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

165 
fun the_parm_map thy class = 
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

166 
let 
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

167 
val data = the_class_data thy class 
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

168 
in (#consts data) end; 
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

169 

18702  170 
fun the_consts_sign thy class = 
18168  171 
let 
19038  172 
val data = the_class_data thy class 
19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

173 
in (#var data, (map snd o #consts) data) end; 
18702  174 

175 
fun the_inst_sign thy (class, tyco) = 

18168  176 
let 
19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

177 
val _ = if is_operational_class thy class then () else error ("no operational class: " ^ class); 
19957  178 
val asorts = Sign.arity_sorts thy tyco [class]; 
19038  179 
val clsvar = (#var o the_class_data thy) class; 
18702  180 
val const_sign = (snd o the_consts_sign thy) class; 
181 
fun add_var sort used = 

182 
let 

183 
val v = hd (Term.invent_names used "'a" 1) 

184 
in ((v, sort), v::used) end; 

185 
val (vsorts, _) = 

19213  186 
[clsvar] 
18702  187 
> fold (fn (_, ty) => curry (gen_union (op =)) 
188 
((map (fst o fst) o typ_tvars) ty @ (map fst o typ_tfrees) ty)) const_sign 

19957  189 
> fold_map add_var asorts; 
19953
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19929
diff
changeset

190 
val ty_inst = Type (tyco, map TFree vsorts); 
18702  191 
val inst_signs = map (apsnd (subst_clsvar clsvar ty_inst)) const_sign; 
192 
in (vsorts, inst_signs) end; 

18168  193 

194 

19038  195 
(* updaters *) 
196 

19928  197 
fun add_class_data (class, (superclasses, name_locale, name_axclass, var, consts)) = 
19957  198 
ClassData.map ( 
199 
Graph.new_node (class, ClassData { 

200 
name_locale = name_locale, 

201 
name_axclass = name_axclass, 

202 
var = var, 

203 
consts = consts }) 

204 
#> fold (curry Graph.add_edge_acyclic class) superclasses 

205 
); 

19038  206 

207 

208 
(* name handling *) 

209 

210 
fun certify_class thy class = 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

211 
(fn class => (the_class_data thy class; class)) (Sign.certify_class thy class); 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

212 

4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

213 
fun certify_sort thy sort = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

214 
map (fn class => (the_class_data thy class; class)) (Sign.certify_sort thy sort); 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

215 

4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

216 
fun intern_class thy = 
19957  217 
certify_class thy o Sign.intern_class thy; 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

218 

4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

219 
fun intern_sort thy = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

220 
certify_sort thy o Sign.intern_sort thy; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

221 

4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

222 
fun extern_class thy = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

223 
Sign.extern_class thy o certify_class thy; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

224 

4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

225 
fun extern_sort thy = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

226 
Sign.extern_sort thy o certify_sort thy; 
19038  227 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

228 
fun read_sort thy = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

229 
certify_sort thy o Sign.read_sort thy; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

230 

4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

231 

4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

232 
(* tactics and methods *) 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

233 

4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

234 
fun intro_classes_tac facts st = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

235 
(ALLGOALS (Method.insert_tac facts THEN' 
19928  236 
REPEAT_ALL_NEW (resolve_tac (AxClass.class_intros (Thm.theory_of_thm st)))) 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

237 
THEN Tactic.distinct_subgoals_tac) st; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

238 

4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

239 
fun default_intro_classes_tac [] = intro_classes_tac [] 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

240 
 default_intro_classes_tac _ = Tactical.no_tac; (*no error message!*) 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

241 

4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

242 
fun default_tac rules ctxt facts = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

243 
HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

244 
default_intro_classes_tac facts; 
19038  245 

19468  246 
val _ = Context.add_setup (Method.add_methods 
247 
[("intro_classes", Method.no_args (Method.METHOD intro_classes_tac), 

248 
"backchain introduction rules of classes"), 

249 
("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), 

250 
"apply some intro/elim rule")]); 

251 

19038  252 

19246  253 
(* axclass instances *) 
254 

255 
local 

256 

19412  257 
fun gen_instance mk_prop add_thm after_qed inst thy = 
19246  258 
thy 
259 
> ProofContext.init 

19412  260 
> Proof.theorem_i PureThy.internalK NONE (after_qed oo (fold o fold) add_thm) NONE ("", []) 
19585  261 
(map (fn t => (("", []), [(t, [])])) (mk_prop thy inst)); 
19246  262 

263 
in 

264 

265 
val axclass_instance_subclass = 

19412  266 
gen_instance (single oo (Logic.mk_classrel oo AxClass.read_classrel)) AxClass.add_classrel I; 
19246  267 
val axclass_instance_arity = 
19412  268 
gen_instance (Logic.mk_arities oo Sign.read_arity) AxClass.add_arity; 
19246  269 
val axclass_instance_arity_i = 
19412  270 
gen_instance (Logic.mk_arities oo Sign.cert_arity) AxClass.add_arity; 
19246  271 

272 
end; 

273 

274 

19038  275 
(* classes and instances *) 
276 

277 
local 

278 

19957  279 
fun add_axclass_i (name, supsort) params axs thy = 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

280 
let 
19395  281 
val (c, thy') = thy 
19957  282 
> AxClass.define_class_i (name, supsort) params axs; 
19518  283 
val {intro, axioms, ...} = AxClass.get_definition thy' c; 
19395  284 
in ((c, (intro, axioms)), thy') end; 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

285 

4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

286 
fun prove_interpretation_i (prfx, atts) expr insts tac thy = 
19038  287 
let 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

288 
fun ad_hoc_term NONE = NONE 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

289 
 ad_hoc_term (SOME (Const (c, ty))) = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

290 
let 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

291 
val p = setmp show_types true (setmp show_sorts true (setmp print_mode [] (Sign.pretty_typ thy))) ty; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

292 
val s = c ^ "::" ^ Pretty.output p; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

293 
in SOME s end 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

294 
 ad_hoc_term (SOME t) = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

295 
let 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

296 
val p = setmp show_types true (setmp show_sorts true (setmp print_mode [] (Sign.pretty_term thy))) t; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

297 
val s = Pretty.output p; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

298 
in SOME s end; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

299 
in 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

300 
thy 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

301 
> Locale.interpretation (prfx, atts) expr (map ad_hoc_term insts) 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

302 
> Proof.global_terminal_proof (Method.Basic (fn _ => Method.SIMPLE_METHOD tac), NONE) 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

303 
> (fn _ => I) 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

304 
end; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

305 

19150  306 
fun gen_class add_locale prep_class bname raw_supclasses raw_elems thy = 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

307 
let 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

308 
val supclasses = map (prep_class thy) raw_supclasses; 
19038  309 
val supsort = 
310 
supclasses 

311 
> map (#name_axclass o the_class_data thy) 

19468  312 
> Sign.certify_sort thy 
19038  313 
> null ? K (Sign.defaultS thy); 
19468  314 
val expr = (Locale.Merge o map (Locale.Locale o #name_locale o the_class_data thy)) supclasses; 
19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

315 
val mapp_sup = AList.make 
19468  316 
(the o AList.lookup (op =) ((flat o map (the_parm_map thy) o the_ancestry thy) supclasses)) 
19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

317 
((map (fst o fst) o Locale.parameters_of_expr thy) expr); 
19038  318 
fun extract_tyvar_consts thy name_locale = 
319 
let 

320 
fun extract_tyvar_name thy tys = 

321 
fold (curry add_typ_tfrees) tys [] 

322 
> (fn [(v, sort)] => 

19468  323 
if Sign.subsort thy (supsort, sort) 
19038  324 
then v 
325 
else error ("illegal sort constraint on class type variable: " ^ Sign.string_of_sort thy sort) 

326 
 [] => error ("no class type variable") 

327 
 vs => error ("more than one type variable: " ^ (commas o map (Sign.string_of_typ thy o TFree)) vs)) 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

328 
val consts1 = 
19038  329 
Locale.parameters_of thy name_locale 
330 
> map (apsnd Syntax.unlocalize_mixfix) 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

331 
val v = (extract_tyvar_name thy o map (snd o fst)) consts1; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

332 
val consts2 = map ((apfst o apsnd) (subst_clsvar v (TFree (v, [])))) consts1; 
19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

333 
in (v, chop (length mapp_sup) consts2) end; 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

334 
fun add_consts v raw_cs_sup raw_cs_this thy = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

335 
let 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

336 
fun add_global_const ((c, ty), syn) thy = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

337 
thy 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

338 
> Sign.add_consts_i [(c, ty > subst_clsvar v (TFree (v, Sign.defaultS thy)), syn)] 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

339 
> `(fn thy => (c, (Sign.intern_const thy c, ty))) 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

340 
in 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

341 
thy 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

342 
> fold_map add_global_const raw_cs_this 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

343 
end; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

344 
fun extract_assumes thy name_locale cs_mapp = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

345 
let 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

346 
val subst_assume = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

347 
map_aterms (fn Free (c, ty) => Const ((fst o the o AList.lookup (op =) cs_mapp) c, ty) 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

348 
 t => t) 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

349 
fun prep_asm ((name, atts), ts) = 
19957  350 
((NameSpace.base name, map (Attrib.attribute thy) atts), map subst_assume ts) 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

351 
in 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

352 
(map prep_asm o Locale.local_asms_of thy) name_locale 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

353 
end; 
19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

354 
fun add_global_constraint v class (_, (c, ty)) thy = 
19038  355 
thy 
19136  356 
> Sign.add_const_constraint_i (c, SOME (subst_clsvar v (TFree (v, [class])) ty)); 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

357 
fun mk_const thy class v (c, ty) = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

358 
Const (c, subst_clsvar v (TFree (v, [class])) ty); 
19038  359 
in 
360 
thy 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

361 
> add_locale bname expr raw_elems 
19928  362 
> (fn (name_locale, ctxt) => 
19038  363 
`(fn thy => extract_tyvar_consts thy name_locale) 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

364 
#> (fn (v, (raw_cs_sup, raw_cs_this)) => 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

365 
add_consts v raw_cs_sup raw_cs_this 
19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

366 
#> (fn mapp_this => 
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

367 
`(fn thy => extract_assumes thy name_locale (mapp_sup @ mapp_this)) 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

368 
#> (fn loc_axioms => 
19957  369 
add_axclass_i (bname, supsort) (map (fst o snd) mapp_this) loc_axioms 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

370 
#> (fn (name_axclass, (_, ax_axioms)) => 
19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

371 
fold (add_global_constraint v name_axclass) mapp_this 
19928  372 
#> add_class_data (name_locale, (supclasses, name_locale, name_axclass, v, mapp_this)) 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

373 
#> prove_interpretation_i (NameSpace.base name_locale, []) 
19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

374 
(Locale.Locale name_locale) (map (SOME o mk_const thy name_axclass v) (map snd (mapp_sup @ mapp_this))) 
19929  375 
((ALLGOALS o ProofContext.fact_tac) ax_axioms) 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

376 
#> pair ctxt 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

377 
))))) 
19038  378 
end; 
379 

380 
in 

381 

19928  382 
val class = gen_class (Locale.add_locale false) intern_class; 
383 
val class_i = gen_class (Locale.add_locale_i false) certify_class; 

19038  384 

385 
end; (* local *) 

386 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

387 
local 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

388 

19957  389 
fun gen_read_def thy prep_att read_def tyco ((raw_name, raw_atts), raw_t) = 
19038  390 
let 
19957  391 
val (_, t) = read_def thy (raw_name, raw_t); 
392 
val ((c, ty), _) = Sign.cert_def (Sign.pp thy) t; 

393 
val atts = map (prep_att thy) raw_atts; 

394 
val name = case raw_name 

395 
of "" => Thm.def_name (NameSpace.base c ^ "_" ^ NameSpace.base tyco) 

396 
 _ => raw_name; 

397 
in (c, (Logic.varifyT ty, ((name, t), atts))) end; 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

398 

19957  399 
fun read_def thy = gen_read_def thy Attrib.attribute read_axm; 
400 
fun read_def_i thy = gen_read_def thy (K I) (K I); 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

401 

19957  402 
fun gen_instance_arity prep_arity prep_att read_def do_proof raw_arity (raw_name, raw_atts) raw_defs theory = 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

403 
let 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

404 
val pp = Sign.pp theory; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

405 
val arity as (tyco, asorts, sort) = prep_arity theory ((fn ((x, y), z) => (x, y, z)) raw_arity); 
19038  406 
val ty_inst = Type (tyco, map2 (curry TVar o rpair 0) (Term.invent_names [] "'a" (length asorts)) asorts) 
19136  407 
val name = case raw_name 
408 
of "" => Thm.def_name ((space_implode "_" o map NameSpace.base) sort ^ "_" ^ NameSpace.base tyco) 

409 
 _ => raw_name; 

410 
val atts = map (prep_att theory) raw_atts; 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

411 
fun get_consts class = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

412 
let 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

413 
val data = the_class_data theory class; 
19957  414 
fun defined c = 
415 
is_some (find_first (fn (_, { lhs = [ty], ...}) => 

416 
Sign.typ_instance theory (ty, ty_inst) orelse Sign.typ_instance theory (ty_inst, ty)) 

417 
(Defs.specifications_of (Theory.defs_of theory) c)) 

418 
val subst_ty = map_type_tfree (fn (v, sort) => 

419 
if #var data = v then ty_inst else TVar ((v, 0), sort)); 

420 
in 

421 
(map_filter (fn (_, (c, ty)) => 

422 
if defined c then NONE else SOME (c, subst_ty ty)) o #consts) data 

423 
end; 

424 
val cs = (maps get_consts o the_ancestry theory) sort; 

425 
fun read_defs defs cs = 

426 
let 

427 
val thy_read = (Sign.primitive_arity (tyco, asorts, sort) o Theory.copy) theory; 

428 
fun read raw_def cs = 

429 
let 

430 
val (c, (ty, def)) = read_def thy_read tyco raw_def; 

431 
val def' = case AList.lookup (op =) cs c 

432 
of NONE => error ("superfluous definition for constant " ^ quote c) 

433 
 SOME ty' => case instantiations_of thy_read (ty, ty') 

434 
of NONE => error ("superfluous definition for constant " ^ 

435 
quote c ^ "::" ^ Sign.string_of_typ thy_read ty) 

436 
 SOME insttab => 

437 
(apfst o apsnd o map_term_types) 

438 
(Logic.unvarifyT o Term.instantiateT insttab o Logic.varifyT) def 

439 
in (def', AList.delete (op =) c cs) end; 

440 
in fold_map read defs cs end; 

441 
val (defs, _) = read_defs raw_defs cs; 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

442 
fun get_remove_contraint c thy = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

443 
let 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

444 
val ty = Sign.the_const_constraint thy c; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

445 
in 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

446 
thy 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

447 
> Sign.add_const_constraint_i (c, NONE) 
19806  448 
> pair (c, Logic.legacy_unvarifyT ty) 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

449 
end; 
19957  450 
fun note_all thms thy = 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

451 
thy 
19136  452 
> PureThy.note_thmss_i PureThy.internalK [((name, atts), [(thms, [])])] 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

453 
> snd; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

454 
fun after_qed cs thy = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

455 
thy 
19412  456 
> fold Sign.add_const_constraint_i (map (apsnd SOME) cs); 
19038  457 
in 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

458 
theory 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

459 
> fold_map get_remove_contraint (map fst cs) 
19957  460 
>> PureThy.add_defs_i true defs 
461 
> (fn (cs, thms) => note_all thms #> pair cs) 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

462 
> (fn cs => do_proof (after_qed cs) arity) 
19038  463 
end; 
464 

19957  465 
fun instance_arity' do_proof = gen_instance_arity Sign.read_arity Attrib.attribute 
466 
read_def do_proof; 

467 
fun instance_arity_i' do_proof = gen_instance_arity Sign.cert_arity (K I) 

468 
read_def_i do_proof; 

19246  469 
fun tactic_proof tac after_qed arity = AxClass.prove_arity arity tac #> after_qed; 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

470 

4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

471 
in 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

472 

19957  473 
val instance_arity = instance_arity' axclass_instance_arity_i; 
474 
val instance_arity_i = instance_arity_i' axclass_instance_arity_i; 

19150  475 
val prove_instance_arity = instance_arity_i' o tactic_proof; 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

476 

4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

477 
end; (* local *) 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

478 

4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

479 
local 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

480 

19136  481 
fun fish_thms (name, expr) after_qed thy = 
482 
let 

483 
val _ = writeln ("sub " ^ name) 

484 
val suplocales = (fn Locale.Merge es => map (fn Locale.Locale n => n) es) expr; 

485 
val _ = writeln ("super " ^ commas suplocales) 

19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

486 
fun get_c name = 
19136  487 
(map (NameSpace.base o fst o fst) o Locale.parameters_of thy) name; 
488 
fun get_a name = 

489 
(map (NameSpace.base o fst o fst) o Locale.local_asms_of thy) name; 

490 
fun get_t supname = 

491 
map (NameSpace.append (NameSpace.append name ((space_implode "_" o get_c) supname)) o NameSpace.base) 

492 
(get_a name); 

493 
val names = map get_t suplocales; 

494 
val _ = writeln ("fishing for " ^ (commas o map commas) names); 

495 
in 

496 
thy 

497 
> after_qed ((map o map) (Drule.standard o get_thm thy o Name) names) 

498 
end; 

499 

500 
fun add_interpretation_in (after_qed : thm list list > theory > theory) (name, expr) thy = 

501 
thy 

502 
> Locale.interpretation_in_locale (name, expr); 

503 

504 
fun prove_interpretation_in tac (after_qed : thm list list > theory > theory) (name, expr) thy = 

505 
thy 

506 
> Locale.interpretation_in_locale (name, expr) 

507 
> Proof.global_terminal_proof (Method.Basic (fn _ => Method.SIMPLE_METHOD tac), NONE) 

508 
> (fn _ => I); 

19038  509 

19150  510 
fun gen_instance_sort prep_class prep_sort do_proof (raw_class, raw_sort) theory = 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

511 
let 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

512 
val class = prep_class theory raw_class; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

513 
val sort = prep_sort theory raw_sort; 
19136  514 
val loc_name = (#name_locale o the_class_data theory) class; 
19468  515 
val loc_expr = 
516 
(Locale.Merge o map (Locale.Locale o #name_locale o the_class_data theory)) sort; 

19136  517 
fun after_qed thmss thy = 
19468  518 
(writeln ""; (Pretty.writeln o Display.pretty_thms o flat) thmss; writeln ""; fold (fn supclass => 
19412  519 
AxClass.prove_classrel (class, supclass) 
19136  520 
(ALLGOALS (K (intro_classes_tac [])) THEN 
19468  521 
(ALLGOALS o resolve_tac o flat) thmss) 
19136  522 
) sort thy) 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

523 
in 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

524 
theory 
19136  525 
> do_proof after_qed (loc_name, loc_expr) 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

526 
end; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

527 

19150  528 
fun instance_sort' do_proof = gen_instance_sort intern_class read_sort do_proof; 
529 
fun instance_sort_i' do_proof = gen_instance_sort certify_class certify_sort do_proof; 

19136  530 
val setup_proof = add_interpretation_in; 
531 
val tactic_proof = prove_interpretation_in; 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

532 

4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

533 
in 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

534 

19150  535 
val instance_sort = instance_sort' setup_proof; 
536 
val instance_sort_i = instance_sort_i' setup_proof; 

537 
val prove_instance_sort = instance_sort_i' o tactic_proof; 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

538 

4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

539 
end; (* local *) 
19038  540 

19957  541 

18168  542 
(* extracting dictionary obligations from types *) 
543 

544 
type sortcontext = (string * sort) list; 

545 

19953
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19929
diff
changeset

546 
fun sortcontext_of_typ thy ty = 
18702  547 
(typ_tfrees o fst o Type.freeze_thaw_type) ty 
18884  548 
> map (apsnd (operational_sort_of thy)) 
18168  549 
> filter (not o null o snd); 
550 

18884  551 
datatype classlookup = Instance of (class * string) * classlookup list list 
19253  552 
 Lookup of class list * (string * (int * int)) 
19213  553 

554 
fun pretty_lookup' (Instance ((class, tyco), lss)) = 

555 
(Pretty.block o Pretty.breaks) ( 

556 
Pretty.enum "," "{" "}" [Pretty.str class, Pretty.str tyco] 

557 
:: map pretty_lookup lss 

558 
) 

19253  559 
 pretty_lookup' (Lookup (classes, (v, (i, j)))) = 
19953
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19929
diff
changeset

560 
Pretty.enum " <" "[" "]" (map Pretty.str classes @ 
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19929
diff
changeset

561 
[Pretty.str (v ^ "!" ^ string_of_int i ^ "/" ^ string_of_int j)]) 
19213  562 
and pretty_lookup ls = (Pretty.enum "," "(" ")" o map pretty_lookup') ls; 
18168  563 

19953
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19929
diff
changeset

564 
fun sortlookup thy (sort_decl, typ_ctxt) = 
18168  565 
let 
19953
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19929
diff
changeset

566 
val pp = Sign.pp thy; 
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19929
diff
changeset

567 
val algebra = Sorts.project_algebra pp (is_operational_class thy) 
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19929
diff
changeset

568 
(Sign.classes_of thy); 
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19929
diff
changeset

569 
fun classrel (l as Lookup (classes, p), _) class = 
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19929
diff
changeset

570 
Lookup (class :: classes, p) 
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19929
diff
changeset

571 
 classrel (Instance ((_, tyco), lss), _) class = 
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19929
diff
changeset

572 
Instance ((class, tyco), lss); 
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19929
diff
changeset

573 
fun constructor tyco lss class = 
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19929
diff
changeset

574 
Instance ((class, tyco), (map o map) fst lss) 
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19929
diff
changeset

575 
fun variable (TFree (v, sort)) = 
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19929
diff
changeset

576 
map_index (fn (n, class) => (Lookup ([], (v, (n, length sort))), class)) 
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19929
diff
changeset

577 
(operational_sort_of thy sort) 
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19929
diff
changeset

578 
 variable (TVar _) = error "TVar encountered while deriving sortlookup"; 
18864  579 
in 
19953
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19929
diff
changeset

580 
Sorts.of_sort_derivation pp algebra 
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19929
diff
changeset

581 
{classrel = classrel, constructor = constructor, variable = variable} 
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19929
diff
changeset

582 
(typ_ctxt, operational_sort_of thy sort_decl) 
18864  583 
end; 
584 

19953
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19929
diff
changeset

585 
fun sortlookups_const thy (c, typ_ctxt) = 
18864  586 
let 
19957  587 
val typ_decl = case AxClass.class_of thy c 
19953
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19929
diff
changeset

588 
of NONE => Sign.the_const_type thy c 
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19929
diff
changeset

589 
 SOME class => case the_consts_sign thy class of (v, cs) => 
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19929
diff
changeset

590 
(Logic.legacy_varifyT o subst_clsvar v (TFree (v, [class]))) 
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19929
diff
changeset

591 
((the o AList.lookup (op =) cs) c) 
18168  592 
in 
19957  593 
instantiations_of thy (typ_decl, typ_ctxt) 
594 
> the 

595 
> map (fn ((_, sort), ty) => sortlookup thy (sort, ty)) 

19953
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19929
diff
changeset

596 
> filter_out null 
18168  597 
end; 
598 

18884  599 

18515  600 
(* toplevel interface *) 
601 

602 
local 

603 

604 
structure P = OuterParse 

605 
and K = OuterKeyword 

606 

607 
in 

608 

18849
05a16861d3a5
added three times overloaded Isar instance command
haftmann
parents:
18829
diff
changeset

609 
val (classK, instanceK) = ("class", "instance") 
18515  610 

19253  611 
val use_cp_instance = ref false; 
612 

19136  613 
fun wrap_add_instance_subclass (class, sort) thy = 
614 
case Sign.read_sort thy sort 

615 
of [class'] => 

19253  616 
if ! use_cp_instance 
617 
andalso (is_some o lookup_class_data thy o Sign.intern_class thy) class 

19136  618 
andalso (is_some o lookup_class_data thy o Sign.intern_class thy) class' 
619 
then 

19150  620 
instance_sort (class, sort) thy 
19136  621 
else 
19246  622 
axclass_instance_subclass (class, sort) thy 
19150  623 
 _ => instance_sort (class, sort) thy; 
19136  624 

18911  625 
val parse_inst = 
19136  626 
(Scan.optional (P.$$$ "("  P.!!! (P.list1 P.sort  P.$$$ ")")) []  P.xname  P.$$$ "::"  P.sort) 
627 
>> (fn ((asorts, tyco), sort) => ((tyco, asorts), sort)) 

628 
 (P.xname  P.$$$ "::"  P.!!! P.arity) 

629 
>> (fn (tyco, (asorts, sort)) => ((tyco, asorts), sort)); 

18911  630 

19038  631 
val locale_val = 
632 
(P.locale_expr  

633 
Scan.optional (P.$$$ "+"  P.!!! (Scan.repeat1 P.context_element)) []  

634 
Scan.repeat1 P.context_element >> pair Locale.empty); 

635 

19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

636 
val class_subP = P.name  Scan.repeat (P.$$$ "+"  P.name) >> (op ::); 
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

637 
val class_bodyP = P.!!! (Scan.repeat1 P.context_element); 
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

638 

18515  639 
val classP = 
18849
05a16861d3a5
added three times overloaded Isar instance command
haftmann
parents:
18829
diff
changeset

640 
OuterSyntax.command classK "operational type classes" K.thy_decl ( 
05a16861d3a5
added three times overloaded Isar instance command
haftmann
parents:
18829
diff
changeset

641 
P.name  P.$$$ "=" 
19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

642 
 ( 
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

643 
class_subP  P.$$$ "+"  class_bodyP 
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

644 
 class_subP >> rpair [] 
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

645 
 class_bodyP >> pair [] 
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

646 
) >> (Toplevel.theory_context 
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

647 
o (fn (bname, (supclasses, elems)) => class bname supclasses elems))); 
18515  648 

18575  649 
val instanceP = 
18849
05a16861d3a5
added three times overloaded Isar instance command
haftmann
parents:
18829
diff
changeset

650 
OuterSyntax.command instanceK "prove type arity or subclass relation" K.thy_goal (( 
19136  651 
P.xname  ((P.$$$ "\\<subseteq>"  P.$$$ "<")  P.!!! P.xname) >> wrap_add_instance_subclass 
652 
 P.opt_thm_name ":"  (parse_inst  Scan.repeat (P.opt_thm_name ":"  P.prop)) 

19246  653 
>> (fn (("", []), (((tyco, asorts), sort), [])) => axclass_instance_arity I (tyco, asorts, sort) 
19150  654 
 (natts, (inst, defs)) => instance_arity inst natts defs) 
18849
05a16861d3a5
added three times overloaded Isar instance command
haftmann
parents:
18829
diff
changeset

655 
) >> (Toplevel.print oo Toplevel.theory_to_proof)); 
18575  656 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

657 
val _ = OuterSyntax.add_parsers [classP, instanceP]; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

658 

18515  659 
end; (* local *) 
660 

18168  661 
end; (* struct *) 