author  haftmann 
Thu, 18 Oct 2007 16:09:38 +0200  
changeset 25083  765528b4b419 
parent 25066  344b9611c150 
child 25094  ba43514068fd 
permissions  rwrr 
24218  1 
(* Title: Pure/Isar/class.ML 
2 
ID: $Id$ 

3 
Author: Florian Haftmann, TU Muenchen 

4 

5 
Type classes derived from primitive axclasses and locales. 

6 
*) 

7 

8 
signature CLASS = 

9 
sig 

10 
val axclass_cmd: bstring * xstring list 

24589  11 
> ((bstring * Attrib.src list) * string list) list 
12 
> theory > class * theory 

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

24914
95cda5dd58d5
added proper subclass concept; improved class target
haftmann
parents:
24901
diff
changeset

14 

25002  15 
val class: bstring > class list > Element.context_i Locale.element list 
24218  16 
> string list > theory > string * Proof.context 
25002  17 
val class_cmd: bstring > xstring list > Element.context Locale.element list 
24589  18 
> xstring list > theory > string * Proof.context 
25038  19 
val is_class: theory > class > bool 
25002  20 
val these_params: theory > sort > (string * (string * typ)) list 
25083  21 
val init: class > Proof.context > Proof.context 
22 
val add_logical_const: string > (string * mixfix) * term 

23 
> theory > string * theory 

24 
val add_syntactic_const: string > Syntax.mode > (string * mixfix) * term 

25 
> theory > string * theory 

26 
val refresh_syntax: class > Proof.context > Proof.context 

24589  27 
val intro_classes_tac: thm list > tactic 
28 
val default_intro_classes_tac: thm list > tactic 

29 
val print_classes: theory > unit 

25002  30 
val uncheck: bool ref 
24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

31 

24589  32 
val instance_arity: (theory > theory) > arity list > theory > Proof.state 
33 
val instance: arity list > ((bstring * Attrib.src list) * term) list 

24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

34 
> (thm list > theory > theory) 
24218  35 
> theory > Proof.state 
24589  36 
val instance_cmd: (bstring * xstring list * xstring) list 
37 
> ((bstring * Attrib.src list) * xstring) list 

24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

38 
> (thm list > theory > theory) 
24218  39 
> theory > Proof.state 
24589  40 
val prove_instance: tactic > arity list 
24218  41 
> ((bstring * Attrib.src list) * term) list 
24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

42 
> theory > thm list * theory 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

43 
val unoverload: theory > conv 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

44 
val overload: theory > conv 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

45 
val unoverload_const: theory > string * typ > string 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

46 
val inst_const: theory > string * string > string 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

47 
val param_const: theory > string > (string * string) option 
24218  48 
end; 
49 

50 
structure Class : CLASS = 

51 
struct 

52 

53 
(** auxiliary **) 

54 

25062  55 
val classN = "class"; 
56 
val introN = "intro"; 

57 

25002  58 
fun prove_interpretation tac prfx_atts expr inst = 
59 
Locale.interpretation_i I prfx_atts expr inst 

24589  60 
#> Proof.global_terminal_proof 
61 
(Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE) 

62 
#> ProofContext.theory_of; 

63 

25020  64 
fun OF_LAST thm1 thm2 = thm1 RSN (Thm.nprems_of thm2, thm2); 
24589  65 

66 
fun strip_all_ofclass thy sort = 

67 
let 

24847  68 
val typ = TVar ((Name.aT, 0), sort); 
24589  69 
fun prem_inclass t = 
70 
case Logic.strip_imp_prems t 

71 
of ofcls :: _ => try Logic.dest_inclass ofcls 

72 
 [] => NONE; 

73 
fun strip_ofclass class thm = 

74 
thm OF (fst o AxClass.of_sort thy (typ, [class])) AxClass.cache; 

75 
fun strip thm = case (prem_inclass o Thm.prop_of) thm 

76 
of SOME (_, class) => thm > strip_ofclass class > strip 

77 
 NONE => thm; 

78 
in strip end; 

79 

25038  80 
fun get_remove_global_constraint c thy = 
81 
let 

82 
val ty = Sign.the_const_constraint thy c; 

83 
in 

84 
thy 

85 
> Sign.add_const_constraint (c, NONE) 

86 
> pair (c, Logic.unvarifyT ty) 

87 
end; 

88 

24589  89 

90 
(** axclass command **) 

91 

24218  92 
fun axclass_cmd (class, raw_superclasses) raw_specs thy = 
93 
let 

94 
val ctxt = ProofContext.init thy; 

95 
val superclasses = map (Sign.read_class thy) raw_superclasses; 

24589  96 
val name_atts = map ((apsnd o map) (Attrib.attribute thy) o fst) 
97 
raw_specs; 

98 
val axiomss = ProofContext.read_propp (ctxt, map (map (rpair []) o snd) 

99 
raw_specs) 

24218  100 
> snd 
101 
> (map o map) fst; 

24589  102 
in 
103 
AxClass.define_class (class, superclasses) [] 

104 
(name_atts ~~ axiomss) thy 

105 
end; 

24218  106 

107 
local 

108 

109 
fun gen_instance mk_prop add_thm after_qed insts thy = 

110 
let 

111 
fun after_qed' results = 

112 
ProofContext.theory ((fold o fold) add_thm results #> after_qed); 

113 
in 

114 
thy 

115 
> ProofContext.init 

24589  116 
> Proof.theorem_i NONE after_qed' ((map (fn t => [(t, [])]) 
117 
o maps (mk_prop thy)) insts) 

24218  118 
end; 
119 

120 
in 

121 

24589  122 
val instance_arity = 
24218  123 
gen_instance (Logic.mk_arities oo Sign.cert_arity) AxClass.add_arity; 
24589  124 
val classrel = 
24218  125 
gen_instance (single oo (Logic.mk_classrel oo AxClass.cert_classrel)) 
126 
AxClass.add_classrel I o single; 

24589  127 
val classrel_cmd = 
128 
gen_instance (single oo (Logic.mk_classrel oo AxClass.read_classrel)) 

129 
AxClass.add_classrel I o single; 

24218  130 

131 
end; (*local*) 

132 

133 

24589  134 
(** explicit constants for overloaded definitions **) 
24304  135 

136 
structure InstData = TheoryDataFun 

137 
( 

24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

138 
type T = (string * thm) Symtab.table Symtab.table * (string * string) Symtab.table; 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

139 
(*constant name ~> type constructor ~> (constant name, equation), 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

140 
constant name ~> (constant name, type constructor)*) 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

141 
val empty = (Symtab.empty, Symtab.empty); 
24304  142 
val copy = I; 
143 
val extend = I; 

24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

144 
fun merge _ ((taba1, tabb1), (taba2, tabb2)) = 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

145 
(Symtab.join (K (Symtab.merge (K true))) (taba1, taba2), 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

146 
Symtab.merge (K true) (tabb1, tabb2)); 
24304  147 
); 
148 

25020  149 
fun inst_thms thy = (Symtab.fold (Symtab.fold (cons o snd o snd) o snd) o fst) 
24589  150 
(InstData.get thy) []; 
151 
fun add_inst (c, tyco) inst = (InstData.map o apfst 

152 
o Symtab.map_default (c, Symtab.empty)) (Symtab.update_new (tyco, inst)) 

24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

153 
#> (InstData.map o apsnd) (Symtab.update_new (fst inst, (c, tyco))); 
24304  154 

25020  155 
fun unoverload thy = MetaSimplifier.rewrite true (inst_thms thy); 
156 
fun overload thy = MetaSimplifier.rewrite true (map Thm.symmetric (inst_thms thy)); 

24304  157 

158 
fun inst_const thy (c, tyco) = 

24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

159 
(fst o the o Symtab.lookup ((the o Symtab.lookup (fst (InstData.get thy))) c)) tyco; 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

160 
fun unoverload_const thy (c_ty as (c, _)) = 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

161 
case AxClass.class_of_param thy c 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

162 
of SOME class => (case Sign.const_typargs thy c_ty 
24589  163 
of [Type (tyco, _)] => (case Symtab.lookup 
164 
((the o Symtab.lookup (fst (InstData.get thy))) c) tyco 

24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

165 
of SOME (c, _) => c 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

166 
 NONE => c) 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

167 
 [_] => c) 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

168 
 NONE => c; 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

169 

ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

170 
val param_const = Symtab.lookup o snd o InstData.get; 
24304  171 

172 
fun add_inst_def (class, tyco) (c, ty) thy = 

173 
let 

25024  174 
val tyco_base = Sign.base_name tyco; 
175 
val name_inst = Sign.base_name class ^ "_" ^ tyco_base ^ "_inst"; 

176 
val c_inst_base = Sign.base_name c ^ "_" ^ tyco_base; 

24304  177 
in 
178 
thy 

179 
> Sign.sticky_prefix name_inst 

25020  180 
> Sign.declare_const [] (c_inst_base, ty, NoSyn) 
24968
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

181 
> (fn const as Const (c_inst, _) => 
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

182 
PureThy.add_defs_i false 
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

183 
[((Thm.def_name c_inst_base, Logic.mk_equals (const, Const (c, ty))), [])] 
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

184 
#> (fn [thm] => add_inst (c, tyco) (c_inst, Thm.symmetric thm))) 
24435  185 
> Sign.restore_naming thy 
24304  186 
end; 
187 

188 
fun add_inst_def' (class, tyco) (c, ty) thy = 

24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

189 
if case Symtab.lookup (fst (InstData.get thy)) c 
24304  190 
of NONE => true 
191 
 SOME tab => is_none (Symtab.lookup tab tyco) 

192 
then add_inst_def (class, tyco) (c, Logic.unvarifyT ty) thy 

193 
else thy; 

194 

195 
fun add_def ((class, tyco), ((name, prop), atts)) thy = 

196 
let 

24589  197 
val ((lhs as Const (c, ty), args), rhs) = 
198 
(apfst Term.strip_comb o Logic.dest_equals) prop; 

24701  199 
fun (*add_inst' def ([], (Const (c_inst, ty))) = 
24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

200 
if forall (fn TFree _ => true  _ => false) (Sign.const_typargs thy (c_inst, ty)) 
24304  201 
then add_inst (c, tyco) (c_inst, def) 
202 
else add_inst_def (class, tyco) (c, ty) 

24701  203 
*) add_inst' _ t = add_inst_def (class, tyco) (c, ty); 
24304  204 
in 
205 
thy 

25020  206 
> PureThy.add_defs_i true [((name, prop), map (Attrib.attribute_i thy) atts)] 
24304  207 
> (fn [def] => add_inst' def (args, rhs) #> pair def) 
208 
end; 

209 

210 

24589  211 
(** instances with implicit parameter handling **) 
24218  212 

213 
local 

214 

24707  215 
fun gen_read_def thy prep_att parse_prop ((raw_name, raw_atts), raw_t) = 
24218  216 
let 
24707  217 
val ctxt = ProofContext.init thy; 
218 
val t = parse_prop ctxt raw_t > Syntax.check_prop ctxt; 

24981
4ec3f95190bf
dest/cert_def: replaced Pretty.pp by explicit Proof.context;
wenzelm
parents:
24968
diff
changeset

219 
val ((c, ty), _) = Sign.cert_def ctxt t; 
24218  220 
val atts = map (prep_att thy) raw_atts; 
221 
val insts = Consts.typargs (Sign.consts_of thy) (c, ty); 

222 
val name = case raw_name 

223 
of "" => NONE 

224 
 _ => SOME raw_name; 

225 
in (c, (insts, ((name, t), atts))) end; 

226 

24707  227 
fun read_def_cmd thy = gen_read_def thy Attrib.intern_src Syntax.parse_prop; 
24218  228 
fun read_def thy = gen_read_def thy (K I) (K I); 
229 

24589  230 
fun gen_instance prep_arity read_def do_proof raw_arities raw_defs after_qed theory = 
24218  231 
let 
232 
val arities = map (prep_arity theory) raw_arities; 

25020  233 
val _ = if null arities then error "At least one arity must be given" else (); 
24218  234 
val _ = case (duplicates (op =) o map #1) arities 
235 
of [] => () 

25020  236 
 dupl_tycos => error ("Type constructors occur more than once in arities: " 
237 
^ commas_quote dupl_tycos); 

24218  238 
fun get_consts_class tyco ty class = 
239 
let 

24968
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

240 
val cs = (these o try (#params o AxClass.get_info theory)) class; 
24218  241 
val subst_ty = map_type_tfree (K ty); 
242 
in 

24304  243 
map (fn (c, ty) => (c, ((class, tyco), subst_ty ty))) cs 
24218  244 
end; 
245 
fun get_consts_sort (tyco, asorts, sort) = 

246 
let 

24589  247 
val ty = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) 
24847  248 
(Name.names Name.context Name.aT asorts)) 
24731  249 
in maps (get_consts_class tyco ty) (Sign.complete_sort theory sort) end; 
24218  250 
val cs = maps get_consts_sort arities; 
251 
fun mk_typnorm thy (ty, ty_sc) = 

252 
case try (Sign.typ_match thy (Logic.varifyT ty_sc, ty)) Vartab.empty 

253 
of SOME env => SOME (Logic.varifyT #> Envir.typ_subst_TVars env #> Logic.unvarifyT) 

254 
 NONE => NONE; 

255 
fun read_defs defs cs thy_read = 

256 
let 

257 
fun read raw_def cs = 

258 
let 

259 
val (c, (inst, ((name_opt, t), atts))) = read_def thy_read raw_def; 

260 
val ty = Consts.instance (Sign.consts_of thy_read) (c, inst); 

24304  261 
val ((class, tyco), ty') = case AList.lookup (op =) cs c 
25020  262 
of NONE => error ("Illegal definition for constant " ^ quote c) 
24218  263 
 SOME class_ty => class_ty; 
264 
val name = case name_opt 

265 
of NONE => Thm.def_name (Logic.name_arity (tyco, [], c)) 

266 
 SOME name => name; 

267 
val t' = case mk_typnorm thy_read (ty', ty) 

25020  268 
of NONE => error ("Illegal definition for constant " ^ 
24218  269 
quote (c ^ "::" ^ setmp show_sorts true 
270 
(Sign.string_of_typ thy_read) ty)) 

271 
 SOME norm => map_types norm t 

272 
in (((class, tyco), ((name, t'), atts)), AList.delete (op =) c cs) end; 

273 
in fold_map read defs cs end; 

24304  274 
val (defs, other_cs) = read_defs raw_defs cs 
24218  275 
(fold Sign.primitive_arity arities (Theory.copy theory)); 
24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

276 
fun after_qed' cs defs = 
24766  277 
fold Sign.add_const_constraint (map (apsnd SOME) cs) 
24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

278 
#> after_qed defs; 
24218  279 
in 
280 
theory 

25038  281 
> fold_map get_remove_global_constraint (map fst cs > distinct (op =)) 
24304  282 
>> fold_map add_def defs 
283 
> fold (fn (c, ((class, tyco), ty)) => add_inst_def' (class, tyco) (c, ty)) other_cs 

24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

284 
> (fn (cs, defs) => do_proof (after_qed' cs defs) arities defs) 
24218  285 
end; 
286 

24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

287 
fun tactic_proof tac f arities defs = 
24218  288 
fold (fn arity => AxClass.prove_arity arity tac) arities 
24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

289 
#> f 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

290 
#> pair defs; 
24218  291 

292 
in 

293 

24589  294 
val instance = gen_instance Sign.cert_arity read_def 
295 
(fn f => fn arities => fn defs => instance_arity f arities); 

296 
val instance_cmd = gen_instance Sign.read_arity read_def_cmd 

297 
(fn f => fn arities => fn defs => instance_arity f arities); 

298 
fun prove_instance tac arities defs = 

299 
gen_instance Sign.cert_arity read_def 

300 
(tactic_proof tac) arities defs (K I); 

24218  301 

302 
end; (*local*) 

303 

304 

305 

24589  306 
(** class data **) 
24218  307 

308 
datatype class_data = ClassData of { 

309 
consts: (string * string) list 

24836  310 
(*locale parameter ~> constant name*), 
25062  311 
base_sort: sort, 
25083  312 
inst: term option list 
313 
(*canonical interpretation*), 

25062  314 
morphism: morphism, 
315 
(*partial morphism of canonical interpretation*) 

24657  316 
intro: thm, 
317 
defs: thm list, 

25062  318 
operations: (string * ((term * typ) * (typ * int))) list 
319 
(*constant name ~> (locale term & typ, 

320 
(constant constraint, instantiaton index of class typ))*) 

24657  321 
}; 
24218  322 

24657  323 
fun rep_class_data (ClassData d) = d; 
25062  324 
fun mk_class_data ((consts, base_sort, inst, morphism, intro), 
325 
(defs, operations)) = 

326 
ClassData { consts = consts, base_sort = base_sort, inst = inst, 

327 
morphism = morphism, intro = intro, defs = defs, 

328 
operations = operations }; 

329 
fun map_class_data f (ClassData { consts, base_sort, inst, morphism, intro, 

330 
defs, operations }) = 

331 
mk_class_data (f ((consts, base_sort, inst, morphism, intro), 

332 
(defs, operations))); 

25038  333 
fun merge_class_data _ (ClassData { consts = consts, 
25062  334 
base_sort = base_sort, inst = inst, morphism = morphism, intro = intro, 
335 
defs = defs1, operations = operations1 }, 

336 
ClassData { consts = _, base_sort = _, inst = _, morphism = _, intro = _, 

337 
defs = defs2, operations = operations2 }) = 

338 
mk_class_data ((consts, base_sort, inst, morphism, intro), 

24914
95cda5dd58d5
added proper subclass concept; improved class target
haftmann
parents:
24901
diff
changeset

339 
(Thm.merge_thms (defs1, defs2), 
25062  340 
AList.merge (op =) (K true) (operations1, operations2))); 
24218  341 

342 
structure ClassData = TheoryDataFun 

343 
( 

25038  344 
type T = class_data Graph.T 
345 
val empty = Graph.empty; 

24218  346 
val copy = I; 
347 
val extend = I; 

25038  348 
fun merge _ = Graph.join merge_class_data; 
24218  349 
); 
350 

351 

352 
(* queries *) 

353 

25038  354 
val lookup_class_data = Option.map rep_class_data oo try o Graph.get_node o ClassData.get; 
24218  355 

24589  356 
fun the_class_data thy class = case lookup_class_data thy class 
25020  357 
of NONE => error ("Undeclared class " ^ quote class) 
24589  358 
 SOME data => data; 
24218  359 

25038  360 
val is_class = is_some oo lookup_class_data; 
361 

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

24218  363 

25002  364 
fun these_params thy = 
24218  365 
let 
366 
fun params class = 

367 
let 

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

368 
val const_typs = (#params o AxClass.get_info thy) class; 
24657  369 
val const_names = (#consts o the_class_data thy) class; 
24218  370 
in 
371 
(map o apsnd) (fn c => (c, (the o AList.lookup (op =) const_typs) c)) const_names 

372 
end; 

373 
in maps params o ancestry thy end; 

374 

24657  375 
fun these_defs thy = maps (these o Option.map #defs o lookup_class_data thy) o ancestry thy; 
24218  376 

25062  377 
fun morphism thy = #morphism o the_class_data thy; 
378 

24218  379 
fun these_intros thy = 
24657  380 
Graph.fold (fn (_, (data, _)) => insert Thm.eq_thm ((#intro o rep_class_data) data)) 
25038  381 
(ClassData.get thy) []; 
24218  382 

24836  383 
fun these_operations thy = 
384 
maps (#operations o the_class_data thy) o ancestry thy; 

24657  385 

25002  386 
fun local_operation thy = AList.lookup (op =) o these_operations thy; 
387 

25062  388 
fun sups_base_sort thy sort = 
24901
d3cbf79769b9
added first version of userspace type system for class target
haftmann
parents:
24847
diff
changeset

389 
let 
25062  390 
val sups = filter (is_class thy) sort 
24901
d3cbf79769b9
added first version of userspace type system for class target
haftmann
parents:
24847
diff
changeset

391 
> Sign.minimize_sort thy; 
25062  392 
val base_sort = case sups 
393 
of _ :: _ => maps (#base_sort o the_class_data thy) sups 

394 
> Sign.minimize_sort thy 

24901
d3cbf79769b9
added first version of userspace type system for class target
haftmann
parents:
24847
diff
changeset

395 
 [] => sort; 
25062  396 
in (sups, base_sort) end; 
24901
d3cbf79769b9
added first version of userspace type system for class target
haftmann
parents:
24847
diff
changeset

397 

24218  398 
fun print_classes thy = 
399 
let 

24920  400 
val ctxt = ProofContext.init thy; 
24218  401 
val algebra = Sign.classes_of thy; 
402 
val arities = 

403 
Symtab.empty 

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

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

406 
((#arities o Sorts.rep_algebra) algebra); 

407 
val the_arities = these o Symtab.lookup arities; 

408 
fun mk_arity class tyco = 

409 
let 

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

24920  411 
in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end; 
24218  412 
fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: " 
24920  413 
^ setmp show_sorts false (Syntax.string_of_typ ctxt o Type.strip_sorts) ty); 
24218  414 
fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [ 
25062  415 
(SOME o Pretty.str) ("class " ^ Sign.extern_class thy class ^ ":"), 
24218  416 
(SOME o Pretty.block) [Pretty.str "supersort: ", 
24920  417 
(Syntax.pretty_sort ctxt o Sign.minimize_sort thy o Sign.super_classes thy) class], 
25062  418 
if is_class thy class then (SOME o Pretty.str) 
419 
("locale: " ^ Locale.extern thy class) else NONE, 

420 
((fn [] => NONE  ps => (SOME o Pretty.block o Pretty.fbreaks) 

421 
(Pretty.str "parameters:" :: ps)) o map mk_param 

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

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

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

426 
] 

427 
] 

428 
in 

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

24218  431 
end; 
432 

433 

434 
(* updaters *) 

435 

25083  436 
fun add_class_data ((class, superclasses), (cs, base_sort, insttab, phi, intro)) thy = 
25002  437 
let 
25083  438 
val inst = map 
439 
(SOME o the o Symtab.lookup insttab o fst o fst) 

25038  440 
(Locale.parameters_of_expr thy (Locale.Locale class)); 
25062  441 
val operations = map (fn (v_ty as (_, ty'), (c, ty)) => 
442 
(c, ((Free v_ty, ty'), (Logic.varifyT ty, 0)))) cs; 

25002  443 
val cs = (map o pairself) fst cs; 
25038  444 
val add_class = Graph.new_node (class, 
25083  445 
mk_class_data ((cs, base_sort, inst, phi, intro), ([], operations))) 
25002  446 
#> fold (curry Graph.add_edge class) superclasses; 
447 
in 

25038  448 
ClassData.map add_class thy 
25002  449 
end; 
24218  450 

25062  451 
fun register_operation class ((c, rhs), some_def) thy = 
452 
let 

453 
val ty = Sign.the_const_constraint thy c; 

454 
val typargs = Sign.const_typargs thy (c, ty); 

455 
val typidx = find_index (fn TVar ((v, _), _) => Name.aT = v  _ => false) typargs; 

456 
val ty' = Term.fastype_of rhs; 

457 
in 

458 
thy 

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

460 
(fn (defs, operations) => 

461 
(case some_def of NONE => defs  SOME def => def :: defs, 

462 
(c, ((rhs, ty'), (ty, typidx))) :: operations)) 

463 
end; 

24218  464 

24589  465 

466 
(** rule calculation, tactics and methods **) 

467 

25024  468 
val class_prefix = Logic.const_of_class o Sign.base_name; 
469 

25062  470 
fun calculate_morphism class cs = 
471 
let 

472 
val subst_typ = Term.map_type_tfree (fn var as (v, sort) => 

473 
if v = Name.aT then TVar ((v, 0), [class]) else TVar ((v, 0), sort)); 

474 
fun subst_aterm (t as Free (v, ty)) = (case AList.lookup (op =) cs v 

475 
of SOME (c, _) => Const (c, ty) 

476 
 NONE => t) 

477 
 subst_aterm t = t; 

478 
val subst_term = map_aterms subst_aterm #> map_types subst_typ; 

479 
in 

480 
Morphism.identity 

481 
$> Morphism.term_morphism subst_term 

482 
$> Morphism.typ_morphism subst_typ 

483 
end; 

484 

25038  485 
fun class_intro thy class sups = 
24589  486 
let 
487 
fun class_elim class = 

25020  488 
case (#axioms o AxClass.get_info thy) class 
489 
of [thm] => SOME (Drule.unconstrainTs thm) 

24589  490 
 [] => NONE; 
25038  491 
val pred_intro = case Locale.intros thy class 
24589  492 
of ([ax_intro], [intro]) => intro > OF_LAST ax_intro > SOME 
493 
 ([intro], []) => SOME intro 

494 
 ([], [intro]) => SOME intro 

495 
 _ => NONE; 

496 
val pred_intro' = pred_intro 

497 
> Option.map (fn intro => intro OF map_filter class_elim sups); 

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

498 
val class_intro = (#intro o AxClass.get_info thy) class; 
24589  499 
val raw_intro = case pred_intro' 
500 
of SOME pred_intro => class_intro > OF_LAST pred_intro 

501 
 NONE => class_intro; 

502 
val sort = Sign.super_classes thy class; 

24847  503 
val typ = TVar ((Name.aT, 0), sort); 
24589  504 
val defs = these_defs thy sups; 
505 
in 

506 
raw_intro 

507 
> Drule.instantiate' [SOME (Thm.ctyp_of thy typ)] [] 

508 
> strip_all_ofclass thy sort 

509 
> Thm.strip_shyps 

510 
> MetaSimplifier.rewrite_rule defs 

511 
> Drule.unconstrainTs 

512 
end; 

513 

514 
fun class_interpretation class facts defs thy = 

515 
let 

25038  516 
val params = these_params thy [class]; 
25083  517 
val inst = (#inst o the_class_data thy) class; 
25020  518 
val tac = ALLGOALS (ProofContext.fact_tac facts); 
25038  519 
val prfx = class_prefix class; 
24589  520 
in 
25038  521 
thy 
522 
> fold_map (get_remove_global_constraint o fst o snd) params 

523 
> prove_interpretation tac ((false, prfx), []) (Locale.Locale class) (inst, defs) 

524 
> (fn cs => fold (Sign.add_const_constraint o apsnd SOME) cs) 

24589  525 
end; 
24218  526 

527 
fun intro_classes_tac facts st = 

528 
let 

529 
val thy = Thm.theory_of_thm st; 

530 
val classes = Sign.all_classes thy; 

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

532 
val class_intros = these_intros thy; 

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

533 
val axclass_intros = map_filter (try (#intro o AxClass.get_info thy)) classes; 
24218  534 
in 
24930
cc2e0e8c81af
renamed AxClass.get_definition to AxClass.get_info (again);
wenzelm
parents:
24920
diff
changeset

535 
(ALLGOALS (Method.insert_tac facts THEN' 
cc2e0e8c81af
renamed AxClass.get_definition to AxClass.get_info (again);
wenzelm
parents:
24920
diff
changeset

536 
REPEAT_ALL_NEW (resolve_tac (class_trivs @ class_intros @ axclass_intros))) 
cc2e0e8c81af
renamed AxClass.get_definition to AxClass.get_info (again);
wenzelm
parents:
24920
diff
changeset

537 
THEN Tactic.distinct_subgoals_tac) st 
24218  538 
end; 
539 

540 
fun default_intro_classes_tac [] = intro_classes_tac [] 

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

541 
 default_intro_classes_tac _ = no_tac; 
24218  542 

543 
fun default_tac rules ctxt facts = 

544 
HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE 

545 
default_intro_classes_tac facts; 

546 

547 
val _ = Context.add_setup (Method.add_methods 

548 
[("intro_classes", Method.no_args (Method.METHOD intro_classes_tac), 

549 
"backchain introduction rules of classes"), 

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

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

552 

553 

24589  554 
(** classes and class target **) 
24218  555 

25002  556 
(* class context syntax *) 
24748  557 

25083  558 
structure ClassSyntax = ProofDataFun( 
559 
type T = { 

560 
constraints: (string * typ) list, 

561 
base_sort: sort, 

562 
local_operation: string * typ > (typ * term) option, 

563 
rews: (term * term) list, 

564 
passed: bool 

565 
} option; 

566 
fun init _ = NONE; 

567 
); 

568 

569 
fun synchronize_syntax thy sups base_sort ctxt = 

24914
95cda5dd58d5
added proper subclass concept; improved class target
haftmann
parents:
24901
diff
changeset

570 
let 
25083  571 
val operations = these_operations thy sups; 
572 

573 
(* constraints *) 

574 
fun local_constraint (c, (_, (ty, _))) = 

575 
let 

576 
val ty' = ty 

577 
> map_atyps (fn ty as TVar ((v, 0), _) => 

578 
if v = Name.aT then TVar ((v, 0), base_sort) else ty) 

579 
> SOME; 

580 
in (c, ty') end 

581 
val constraints = (map o apsnd) (fst o snd) operations; 

582 

583 
(* check phase *) 

584 
val typargs = Consts.typargs (ProofContext.consts_of ctxt); 

585 
fun check_const (c, ty) ((t, _), (_, idx)) = 

586 
((nth (typargs (c, ty)) idx), t); 

587 
fun local_operation (c_ty as (c, _)) = AList.lookup (op =) operations c 

588 
> Option.map (check_const c_ty); 

25002  589 

25083  590 
(* uncheck phase *) 
591 
val proto_rews = map (fn (c, ((t, ty), _)) => (t, Const (c, ty))) operations; 

592 
fun rew_app f (t1 $ t2) = rew_app f t1 $ f t2 

593 
 rew_app f t = t; 

594 
val rews = (map o apfst o rew_app) 

595 
(Pattern.rewrite_term thy proto_rews []) proto_rews; 

596 
in 

597 
ctxt 

598 
> fold (ProofContext.add_const_constraint o local_constraint) operations 

599 
> ClassSyntax.map (K (SOME { 

600 
constraints = constraints, 

601 
base_sort = base_sort, 

602 
local_operation = local_operation, 

603 
rews = rews, 

604 
passed = false 

605 
})) 

606 
end; 

607 

608 
fun refresh_syntax class ctxt = 

25002  609 
let 
610 
val thy = ProofContext.theory_of ctxt; 

25062  611 
val base_sort = (#base_sort o the_class_data thy) class; 
25083  612 
in synchronize_syntax thy [class] base_sort ctxt end; 
24914
95cda5dd58d5
added proper subclass concept; improved class target
haftmann
parents:
24901
diff
changeset

613 

25083  614 
val mark_passed = (ClassSyntax.map o Option.map) 
615 
(fn { constraints, base_sort, local_operation, rews, passed } => 

616 
{ constraints = constraints, base_sort = base_sort, 

617 
local_operation = local_operation, rews = rews, passed = true }); 

618 

619 
fun sort_term_check ts ctxt = 

24748  620 
let 
25083  621 
val { constraints, base_sort, local_operation, passed, ... } = 
622 
the (ClassSyntax.get ctxt); 

623 
fun check_typ (c, ty) (TFree (v, _), t) = if v = Name.aT 

25062  624 
then apfst (AList.update (op =) ((c, ty), t)) else I 
25083  625 
 check_typ (c, ty) (TVar (vi, _), t) = if TypeInfer.is_param vi 
25062  626 
then apfst (AList.update (op =) ((c, ty), t)) 
24901
d3cbf79769b9
added first version of userspace type system for class target
haftmann
parents:
24847
diff
changeset

627 
#> apsnd (insert (op =) vi) else I 
25083  628 
 check_typ _ _ = I; 
629 
fun add_const (Const c_ty) = Option.map (check_typ c_ty) (local_operation c_ty) 

25062  630 
> the_default I 
24901
d3cbf79769b9
added first version of userspace type system for class target
haftmann
parents:
24847
diff
changeset

631 
 add_const _ = I; 
d3cbf79769b9
added first version of userspace type system for class target
haftmann
parents:
24847
diff
changeset

632 
val (cs, typarams) = (fold o fold_aterms) add_const ts ([], []); 
25062  633 
val subst_typ = map_type_tvar (fn var as (vi, _) => 
634 
if member (op =) typarams vi then TFree (Name.aT, base_sort) else TVar var); 

635 
val subst_term = map_aterms 

24901
d3cbf79769b9
added first version of userspace type system for class target
haftmann
parents:
24847
diff
changeset

636 
(fn t as Const (c, ty) => the_default t (AList.lookup (op =) cs (c, ty))  t => t) 
25062  637 
#> map_types subst_typ; 
638 
val ts' = map subst_term ts; 

25083  639 
in if eq_list (op aconv) (ts, ts') andalso passed then NONE 
640 
else 

641 
ctxt 

642 
> fold (ProofContext.add_const_constraint o apsnd SOME) constraints 

643 
> mark_passed 

644 
> pair ts' 

645 
> SOME 

646 
end; 

24748  647 

25062  648 
val uncheck = ref true; 
25002  649 

25083  650 
fun sort_term_uncheck ts ctxt = 
25002  651 
let 
25062  652 
(*FIXME abbreviations*) 
25002  653 
val thy = ProofContext.theory_of ctxt; 
25083  654 
val rews = (#rews o the o ClassSyntax.get) ctxt; 
25062  655 
val ts' = if ! uncheck 
25083  656 
then map (Pattern.rewrite_term thy rews []) ts else ts; 
25060  657 
in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt) end; 
25002  658 

25083  659 
fun init_ctxt thy sups base_sort ctxt = 
660 
ctxt 

661 
> Variable.declare_term 

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

663 
> synchronize_syntax thy sups base_sort 

664 
> Context.proof_map ( 

665 
Syntax.add_term_check 0 "class" sort_term_check 

666 
#> Syntax.add_term_uncheck (~10) "class" sort_term_uncheck) 

24901
d3cbf79769b9
added first version of userspace type system for class target
haftmann
parents:
24847
diff
changeset

667 

d3cbf79769b9
added first version of userspace type system for class target
haftmann
parents:
24847
diff
changeset

668 
fun init class ctxt = 
25083  669 
let 
670 
val thy = ProofContext.theory_of ctxt; 

671 
in 

672 
init_ctxt thy [class] ((#base_sort o the_class_data thy) class) ctxt 

673 
end; 

24914
95cda5dd58d5
added proper subclass concept; improved class target
haftmann
parents:
24901
diff
changeset

674 

24748  675 

24589  676 
(* class definition *) 
24218  677 

678 
local 

679 

24748  680 
fun gen_class_spec prep_class prep_expr process_expr thy raw_supclasses raw_includes_elems = 
24218  681 
let 
24748  682 
val supclasses = map (prep_class thy) raw_supclasses; 
25062  683 
val (sups, base_sort) = sups_base_sort thy supclasses; 
24748  684 
val supsort = Sign.minimize_sort thy supclasses; 
25038  685 
val suplocales = map Locale.Locale sups; 
24748  686 
val (raw_elems, includes) = fold_rev (fn Locale.Elem e => apfst (cons e) 
687 
 Locale.Expr i => apsnd (cons (prep_expr thy i))) raw_includes_elems ([], []); 

688 
val supexpr = Locale.Merge suplocales; 

689 
val supparams = (map fst o Locale.parameters_of_expr thy) supexpr; 

25002  690 
val supconsts = AList.make (the o AList.lookup (op =) (these_params thy sups)) 
24748  691 
(map fst supparams); 
692 
val mergeexpr = Locale.Merge (suplocales @ includes); 

693 
val constrain = Element.Constrains ((map o apsnd o map_atyps) 

24847  694 
(fn TFree (_, sort) => TFree (Name.aT, sort)) supparams); 
24748  695 
in 
696 
ProofContext.init thy 

697 
> Locale.cert_expr supexpr [constrain] 

698 
> snd 

25083  699 
> init_ctxt thy sups base_sort 
24748  700 
> process_expr Locale.empty raw_elems 
701 
> fst 

25062  702 
> (fn elems => ((((sups, supconsts), (supsort, base_sort, mergeexpr)), 
24748  703 
(*FIXME*) if null includes then constrain :: elems else elems))) 
704 
end; 

705 

706 
val read_class_spec = gen_class_spec Sign.intern_class Locale.intern_expr Locale.read_expr; 

707 
val check_class_spec = gen_class_spec (K I) (K I) Locale.cert_expr; 

708 

24968
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

709 
fun define_class_params (name, raw_superclasses) raw_consts raw_dep_axioms other_consts thy = 
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

710 
let 
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

711 
val superclasses = map (Sign.certify_class thy) raw_superclasses; 
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

712 
val consts = (map o apfst o apsnd) (Sign.certify_typ thy) raw_consts; 
25083  713 
fun add_const ((c, ty), syn) = 
714 
Sign.declare_const [] (c, Type.strip_sorts ty, syn) #>> Term.dest_Const; 

24968
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

715 
fun mk_axioms cs thy = 
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

716 
raw_dep_axioms thy cs 
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

717 
> (map o apsnd o map) (Sign.cert_prop thy) 
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

718 
> rpair thy; 
25002  719 
fun constrain_typs class = (map o apsnd o Term.map_type_tfree) 
720 
(fn (v, _) => TFree (v, [class])) 

24968
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

721 
in 
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

722 
thy 
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

723 
> Sign.add_path (Logic.const_of_class name) 
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

724 
> fold_map add_const consts 
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

725 
> Sign.restore_naming thy 
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

726 
> (fn cs => mk_axioms cs 
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

727 
#> (fn axioms_prop => AxClass.define_class (name, superclasses) 
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

728 
(map fst cs @ other_consts) axioms_prop 
25002  729 
#> (fn class => `(fn _ => constrain_typs class cs) 
730 
#> (fn cs' => `(fn thy => AxClass.get_info thy class) 

731 
#> (fn {axioms, ...} => fold (Sign.add_const_constraint o apsnd SOME) cs' 

732 
#> pair (class, (cs', axioms))))))) 

24968
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

733 
end; 
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

734 

25002  735 
fun gen_class prep_spec prep_param bname 
24748  736 
raw_supclasses raw_includes_elems raw_other_consts thy = 
737 
let 

25038  738 
val class = Sign.full_name thy bname; 
25062  739 
val (((sups, supconsts), (supsort, base_sort, mergeexpr)), elems_syn) = 
24748  740 
prep_spec thy raw_supclasses raw_includes_elems; 
24968
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

741 
val other_consts = map (tap (Sign.the_const_type thy) o prep_param thy) raw_other_consts; 
24589  742 
fun mk_inst class param_names cs = 
743 
Symtab.empty 

744 
> fold2 (fn v => fn (c, ty) => Symtab.update (v, Const 

745 
(c, Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty))) param_names cs; 

25062  746 
fun fork_syntax (Element.Fixes xs) = 
747 
fold_map (fn (c, ty, syn) => cons (c, syn) #> pair (c, ty, NoSyn)) xs 

748 
#>> Element.Fixes 

749 
 fork_syntax x = pair x; 

750 
val (elems, global_syn) = fold_map fork_syntax elems_syn []; 

751 
fun globalize (c, ty) = 

752 
((c, Term.map_type_tfree (K (TFree (Name.aT, base_sort))) ty), 

753 
(the_default NoSyn o AList.lookup (op =) global_syn) c); 

25038  754 
fun extract_params thy = 
24218  755 
let 
25062  756 
val params = map fst (Locale.parameters_of thy class); 
24218  757 
in 
25062  758 
(params, (map globalize o snd o chop (length supconsts)) params) 
24218  759 
end; 
25038  760 
fun extract_assumes params thy cs = 
24218  761 
let 
762 
val consts = supconsts @ (map (fst o fst) params ~~ cs); 

763 
fun subst (Free (c, ty)) = 

764 
Const ((fst o the o AList.lookup (op =) consts) c, ty) 

765 
 subst t = t; 

766 
fun prep_asm ((name, atts), ts) = 

25024  767 
((Sign.base_name name, map (Attrib.attribute_i thy) atts), 
24589  768 
(map o map_aterms) subst ts); 
24218  769 
in 
25038  770 
Locale.global_asms_of thy class 
24218  771 
> map prep_asm 
772 
end; 

773 
in 

774 
thy 

24748  775 
> Locale.add_locale_i (SOME "") bname mergeexpr elems 
25038  776 
> snd 
777 
> ProofContext.theory (`extract_params 

25062  778 
#> (fn (all_params, params) => 
24968
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

779 
define_class_params (bname, supsort) params 
25038  780 
(extract_assumes params) other_consts 
781 
#> (fn (_, (consts, axioms)) => 

782 
`(fn thy => class_intro thy class sups) 

24218  783 
#> (fn class_intro => 
25062  784 
PureThy.note_thmss_qualified "" (NameSpace.append class classN) 
785 
[((introN, []), [([class_intro], [])])] 

786 
#> (fn [(_, [class_intro])] => 

25038  787 
add_class_data ((class, sups), 
25062  788 
(map fst params ~~ consts, base_sort, 
789 
mk_inst class (map fst all_params) (map snd supconsts @ consts), 

790 
calculate_morphism class (supconsts @ (map (fst o fst) params ~~ consts)), class_intro)) 

25038  791 
#> class_interpretation class axioms [] 
25062  792 
))))) 
25038  793 
> pair class 
24218  794 
end; 
795 

796 
in 

797 

24968
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

798 
val class_cmd = gen_class read_class_spec ((#1 o Term.dest_Const) oo Sign.read_const); 
24748  799 
val class = gen_class check_class_spec (K I); 
24218  800 

801 
end; (*local*) 

802 

803 

24589  804 
(* definition in class target *) 
24218  805 

25083  806 
fun add_logical_const class ((c, mx), dict) thy = 
24218  807 
let 
25024  808 
val prfx = class_prefix class; 
809 
val thy' = thy > Sign.add_path prfx; 

25062  810 
val phi = morphism thy' class; 
25024  811 

25062  812 
val c' = Sign.full_name thy' c; 
25083  813 
val dict' = (map_types Logic.unvarifyT o Morphism.term phi) dict; 
814 
val ty' = Term.fastype_of dict'; 

815 
val ty'' = Type.strip_sorts ty'; 

816 
val def_eq = Logic.mk_equals (Const (c', ty'), dict'); 

25062  817 
val c'' = NameSpace.full (Sign.naming_of thy' > NameSpace.add_path prfx) c; 
24218  818 
in 
25024  819 
thy' 
25038  820 
> Sign.hide_consts_i false [c''] 
25083  821 
> Sign.declare_const [] (c, ty'', mx) > snd 
24218  822 
> Sign.parent_path 
823 
> Sign.sticky_prefix prfx 

25083  824 
> Thm.add_def false (c, def_eq) 
25062  825 
>> Thm.symmetric 
25083  826 
> (fn def => class_interpretation class [def] [Thm.prop_of def] 
827 
#> register_operation class ((c', dict), SOME (Thm.varifyT def))) 

24218  828 
> Sign.restore_naming thy 
25083  829 
> Sign.add_const_constraint (c', SOME ty') 
24914
95cda5dd58d5
added proper subclass concept; improved class target
haftmann
parents:
24901
diff
changeset

830 
> pair c' 
24218  831 
end; 
832 

24901
d3cbf79769b9
added first version of userspace type system for class target
haftmann
parents:
24847
diff
changeset

833 

d3cbf79769b9
added first version of userspace type system for class target
haftmann
parents:
24847
diff
changeset

834 
(* abbreviation in class target *) 
d3cbf79769b9
added first version of userspace type system for class target
haftmann
parents:
24847
diff
changeset

835 

25083  836 
fun add_syntactic_const class prmode ((c, mx), rhs) thy = 
24836  837 
let 
25024  838 
val prfx = class_prefix class; 
25062  839 
val phi = morphism thy class; 
840 

25038  841 
val naming = Sign.naming_of thy > NameSpace.add_path prfx > NameSpace.add_path prfx; 
842 
(*FIXME*) 

25024  843 
val c' = NameSpace.full naming c; 
25062  844 
val rhs' = (map_types Logic.unvarifyT o Morphism.term phi) rhs; 
25020  845 
val ty' = Term.fastype_of rhs'; 
24836  846 
in 
847 
thy 

25024  848 
> Sign.notation true prmode [(Const (c', ty'), mx)] 
25062  849 
> register_operation class ((c', rhs), NONE) 
24914
95cda5dd58d5
added proper subclass concept; improved class target
haftmann
parents:
24901
diff
changeset

850 
> pair c' 
24836  851 
end; 
852 

24218  853 
end; 