author  wenzelm 
Thu, 08 Nov 2007 14:51:29 +0100  
changeset 25344  00c2179db769 
parent 25326  e417a7236125 
child 25368  f12613fda79d 
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 
25311  21 
val init: class > theory > Proof.context 
25096  22 
val add_logical_const: string > Markup.property list 
25104  23 
> (string * mixfix) * term > theory > theory 
25096  24 
val add_syntactic_const: string > Syntax.mode > Markup.property list 
25104  25 
> (string * mixfix) * term > theory > theory 
25083  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 

25195
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

29 
val prove_subclass: class * class > thm list > Proof.context 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

30 
> theory > theory 
24589  31 
val print_classes: theory > unit 
25210  32 
val class_prefix: string > string 
25002  33 
val uncheck: bool ref 
24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

34 

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

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

37 
> (thm list > theory > theory) 
24218  38 
> theory > Proof.state 
24589  39 
val instance_cmd: (bstring * xstring list * xstring) list 
40 
> ((bstring * Attrib.src list) * xstring) list 

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

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

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

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

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

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

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

50 
val param_const: theory > string > (string * string) option 
24218  51 
end; 
52 

53 
structure Class : CLASS = 

54 
struct 

55 

56 
(** auxiliary **) 

57 

25062  58 
val classN = "class"; 
59 
val introN = "intro"; 

60 

25002  61 
fun prove_interpretation tac prfx_atts expr inst = 
62 
Locale.interpretation_i I prfx_atts expr inst 

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

65 
#> ProofContext.theory_of; 

66 

25195
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

67 
fun prove_interpretation_in tac after_qed (name, expr) = 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

68 
Locale.interpretation_in_locale 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

69 
(ProofContext.theory after_qed) (name, expr) 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

70 
#> Proof.global_terminal_proof 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

71 
(Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE) 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

72 
#> ProofContext.theory_of; 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

73 

25020  74 
fun OF_LAST thm1 thm2 = thm1 RSN (Thm.nprems_of thm2, thm2); 
24589  75 

76 
fun strip_all_ofclass thy sort = 

77 
let 

24847  78 
val typ = TVar ((Name.aT, 0), sort); 
24589  79 
fun prem_inclass t = 
80 
case Logic.strip_imp_prems t 

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

82 
 [] => NONE; 

83 
fun strip_ofclass class thm = 

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

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

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

87 
 NONE => thm; 

88 
in strip end; 

89 

25038  90 
fun get_remove_global_constraint c thy = 
91 
let 

92 
val ty = Sign.the_const_constraint thy c; 

93 
in 

94 
thy 

95 
> Sign.add_const_constraint (c, NONE) 

96 
> pair (c, Logic.unvarifyT ty) 

97 
end; 

98 

24589  99 

100 
(** axclass command **) 

101 

24218  102 
fun axclass_cmd (class, raw_superclasses) raw_specs thy = 
103 
let 

104 
val ctxt = ProofContext.init thy; 

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

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

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

109 
raw_specs) 

24218  110 
> snd 
111 
> (map o map) fst; 

24589  112 
in 
113 
AxClass.define_class (class, superclasses) [] 

114 
(name_atts ~~ axiomss) thy 

115 
end; 

24218  116 

117 
local 

118 

119 
fun gen_instance mk_prop add_thm after_qed insts thy = 

120 
let 

121 
fun after_qed' results = 

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

123 
in 

124 
thy 

125 
> ProofContext.init 

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

24218  128 
end; 
129 

130 
in 

131 

24589  132 
val instance_arity = 
24218  133 
gen_instance (Logic.mk_arities oo Sign.cert_arity) AxClass.add_arity; 
24589  134 
val classrel = 
24218  135 
gen_instance (single oo (Logic.mk_classrel oo AxClass.cert_classrel)) 
136 
AxClass.add_classrel I o single; 

24589  137 
val classrel_cmd = 
138 
gen_instance (single oo (Logic.mk_classrel oo AxClass.read_classrel)) 

139 
AxClass.add_classrel I o single; 

24218  140 

141 
end; (*local*) 

142 

143 

24589  144 
(** explicit constants for overloaded definitions **) 
24304  145 

146 
structure InstData = TheoryDataFun 

147 
( 

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

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

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

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

151 
val empty = (Symtab.empty, Symtab.empty); 
24304  152 
val copy = I; 
153 
val extend = I; 

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

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

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

156 
Symtab.merge (K true) (tabb1, tabb2)); 
24304  157 
); 
158 

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

162 
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

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

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

24304  167 

168 
fun inst_const thy (c, tyco) = 

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

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

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

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

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

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

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

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

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

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

179 

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

180 
val param_const = Symtab.lookup o snd o InstData.get; 
24304  181 

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

183 
let 

25024  184 
val tyco_base = Sign.base_name tyco; 
185 
val name_inst = Sign.base_name class ^ "_" ^ tyco_base ^ "_inst"; 

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

24304  187 
in 
188 
thy 

189 
> Sign.sticky_prefix name_inst 

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

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

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

193 
[((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

194 
#> (fn [thm] => add_inst (c, tyco) (c_inst, Thm.symmetric thm))) 
24435  195 
> Sign.restore_naming thy 
24304  196 
end; 
197 

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

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

199 
if case Symtab.lookup (fst (InstData.get thy)) c 
24304  200 
of NONE => true 
201 
 SOME tab => is_none (Symtab.lookup tab tyco) 

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

203 
else thy; 

204 

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

206 
let 

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

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

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

24701  213 
*) add_inst' _ t = add_inst_def (class, tyco) (c, ty); 
24304  214 
in 
215 
thy 

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

219 

220 

24589  221 
(** instances with implicit parameter handling **) 
24218  222 

223 
local 

224 

24707  225 
fun gen_read_def thy prep_att parse_prop ((raw_name, raw_atts), raw_t) = 
24218  226 
let 
24707  227 
val ctxt = ProofContext.init thy; 
228 
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

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

232 
val name = case raw_name 

233 
of "" => NONE 

234 
 _ => SOME raw_name; 

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

236 

24707  237 
fun read_def_cmd thy = gen_read_def thy Attrib.intern_src Syntax.parse_prop; 
24218  238 
fun read_def thy = gen_read_def thy (K I) (K I); 
239 

24589  240 
fun gen_instance prep_arity read_def do_proof raw_arities raw_defs after_qed theory = 
24218  241 
let 
242 
val arities = map (prep_arity theory) raw_arities; 

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

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

24218  248 
fun get_consts_class tyco ty class = 
249 
let 

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

250 
val cs = (these o try (#params o AxClass.get_info theory)) class; 
24218  251 
val subst_ty = map_type_tfree (K ty); 
252 
in 

24304  253 
map (fn (c, ty) => (c, ((class, tyco), subst_ty ty))) cs 
24218  254 
end; 
255 
fun get_consts_sort (tyco, asorts, sort) = 

256 
let 

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

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

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

264 
 NONE => NONE; 

265 
fun read_defs defs cs thy_read = 

266 
let 

267 
fun read raw_def cs = 

268 
let 

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

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

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

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

276 
 SOME name => name; 

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

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

281 
 SOME norm => map_types norm t 

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

283 
in fold_map read defs cs end; 

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

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

288 
#> after_qed defs; 
24218  289 
in 
290 
theory 

25038  291 
> fold_map get_remove_global_constraint (map fst cs > distinct (op =)) 
24304  292 
>> fold_map add_def defs 
293 
> 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

294 
> (fn (cs, defs) => do_proof (after_qed' cs defs) arities defs) 
24218  295 
end; 
296 

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

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

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

300 
#> pair defs; 
24218  301 

302 
in 

303 

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

306 
val instance_cmd = gen_instance Sign.read_arity read_def_cmd 

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

308 
fun prove_instance tac arities defs = 

309 
gen_instance Sign.cert_arity read_def 

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

24218  311 

312 
end; (*local*) 

313 

314 

315 

24589  316 
(** class data **) 
24218  317 

318 
datatype class_data = ClassData of { 

319 
consts: (string * string) list 

24836  320 
(*locale parameter ~> constant name*), 
25062  321 
base_sort: sort, 
25083  322 
inst: term option list 
323 
(*canonical interpretation*), 

25062  324 
morphism: morphism, 
325 
(*partial morphism of canonical interpretation*) 

24657  326 
intro: thm, 
327 
defs: thm list, 

25195
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

328 
operations: (string * (term * (typ * int))) list, 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

329 
(*constant name ~> (locale term, 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

330 
(constant constraint, instantiaton index of class typ))*) 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

331 
unchecks: (term * term) list 
24657  332 
}; 
24218  333 

24657  334 
fun rep_class_data (ClassData d) = d; 
25062  335 
fun mk_class_data ((consts, base_sort, inst, morphism, intro), 
25195
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

336 
(defs, (operations, unchecks))) = 
25062  337 
ClassData { consts = consts, base_sort = base_sort, inst = inst, 
338 
morphism = morphism, intro = intro, defs = defs, 

25195
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

339 
operations = operations, unchecks = unchecks }; 
25062  340 
fun map_class_data f (ClassData { consts, base_sort, inst, morphism, intro, 
25195
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

341 
defs, operations, unchecks }) = 
25062  342 
mk_class_data (f ((consts, base_sort, inst, morphism, intro), 
25195
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

343 
(defs, (operations, unchecks)))); 
25038  344 
fun merge_class_data _ (ClassData { consts = consts, 
25062  345 
base_sort = base_sort, inst = inst, morphism = morphism, intro = intro, 
25195
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

346 
defs = defs1, operations = operations1, unchecks = unchecks1 }, 
25062  347 
ClassData { consts = _, base_sort = _, inst = _, morphism = _, intro = _, 
25195
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

348 
defs = defs2, operations = operations2, unchecks = unchecks2 }) = 
25062  349 
mk_class_data ((consts, base_sort, inst, morphism, intro), 
24914
95cda5dd58d5
added proper subclass concept; improved class target
haftmann
parents:
24901
diff
changeset

350 
(Thm.merge_thms (defs1, defs2), 
25195
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

351 
(AList.merge (op =) (K true) (operations1, operations2), 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

352 
Library.merge (op aconv o pairself snd) (unchecks1, unchecks2)))); 
24218  353 

354 
structure ClassData = TheoryDataFun 

355 
( 

25038  356 
type T = class_data Graph.T 
357 
val empty = Graph.empty; 

24218  358 
val copy = I; 
359 
val extend = I; 

25038  360 
fun merge _ = Graph.join merge_class_data; 
24218  361 
); 
362 

363 

364 
(* queries *) 

365 

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

24589  368 
fun the_class_data thy class = case lookup_class_data thy class 
25020  369 
of NONE => error ("Undeclared class " ^ quote class) 
24589  370 
 SOME data => data; 
24218  371 

25038  372 
val is_class = is_some oo lookup_class_data; 
373 

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

24218  375 

25002  376 
fun these_params thy = 
24218  377 
let 
378 
fun params class = 

379 
let 

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

380 
val const_typs = (#params o AxClass.get_info thy) class; 
24657  381 
val const_names = (#consts o the_class_data thy) class; 
24218  382 
in 
383 
(map o apsnd) (fn c => (c, (the o AList.lookup (op =) const_typs) c)) const_names 

384 
end; 

385 
in maps params o ancestry thy end; 

386 

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

25062  389 
fun morphism thy = #morphism o the_class_data thy; 
390 

24218  391 
fun these_intros thy = 
24657  392 
Graph.fold (fn (_, (data, _)) => insert Thm.eq_thm ((#intro o rep_class_data) data)) 
25038  393 
(ClassData.get thy) []; 
24218  394 

24836  395 
fun these_operations thy = 
396 
maps (#operations o the_class_data thy) o ancestry thy; 

24657  397 

25195
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

398 
fun these_unchecks thy = 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

399 
maps (#unchecks o the_class_data thy) o ancestry thy; 
25002  400 

24218  401 
fun print_classes thy = 
402 
let 

24920  403 
val ctxt = ProofContext.init thy; 
24218  404 
val algebra = Sign.classes_of thy; 
405 
val arities = 

406 
Symtab.empty 

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

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

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

410 
val the_arities = these o Symtab.lookup arities; 

411 
fun mk_arity class tyco = 

412 
let 

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

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

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

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

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

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

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

429 
] 

430 
] 

431 
in 

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

24218  434 
end; 
435 

436 

437 
(* updaters *) 

438 

25163  439 
fun add_class_data ((class, superclasses), (cs, base_sort, inst, phi, intro)) thy = 
25002  440 
let 
25195
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

441 
val operations = map (fn (v_ty, (c, ty)) => 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

442 
(c, ((Free v_ty, (Logic.varifyT ty, 0))))) cs; 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

443 
val unchecks = map (fn ((v, ty'), (c, _)) => 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

444 
(Free (v, Type.strip_sorts ty'), Const (c, Type.strip_sorts ty'))) cs; 
25002  445 
val cs = (map o pairself) fst cs; 
25038  446 
val add_class = Graph.new_node (class, 
25195
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

447 
mk_class_data ((cs, base_sort, map (SOME o Const) inst, phi, intro), ([], (operations, unchecks)))) 
25002  448 
#> fold (curry Graph.add_edge class) superclasses; 
449 
in 

25038  450 
ClassData.map add_class thy 
25002  451 
end; 
24218  452 

25239  453 
fun register_operation class (c, ((t, t_rev), some_def)) thy = 
25062  454 
let 
455 
val ty = Sign.the_const_constraint thy c; 

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

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

25239  458 
val prep_typ = map_atyps 
459 
(fn TVar (vi as (v, _), _) => if Name.aT = v then TFree (v, []) else TVar (vi, [])) 

460 
val t_rev' = map_types prep_typ t_rev; 

461 
val ty' = Term.fastype_of t_rev'; 

25062  462 
in 
463 
thy 

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

25195
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

465 
(fn (defs, (operations, unchecks)) => 
25096  466 
(fold cons (the_list some_def) defs, 
25239  467 
((c, (t, (ty, typidx))) :: operations, (t_rev', Const (c, ty')) :: unchecks))) 
25062  468 
end; 
24218  469 

24589  470 

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

472 

25024  473 
val class_prefix = Logic.const_of_class o Sign.base_name; 
474 

25062  475 
fun calculate_morphism class cs = 
476 
let 

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

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

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

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

481 
 NONE => t) 

482 
 subst_aterm t = t; 

483 
val subst_term = map_aterms subst_aterm #> map_types subst_typ; 

484 
in 

25209  485 
Morphism.term_morphism subst_term 
25062  486 
$> Morphism.typ_morphism subst_typ 
487 
end; 

488 

25038  489 
fun class_intro thy class sups = 
24589  490 
let 
491 
fun class_elim class = 

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

24589  494 
 [] => NONE; 
25038  495 
val pred_intro = case Locale.intros thy class 
24589  496 
of ([ax_intro], [intro]) => intro > OF_LAST ax_intro > SOME 
497 
 ([intro], []) => SOME intro 

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

499 
 _ => NONE; 

500 
val pred_intro' = pred_intro 

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

502 
val class_intro = (#intro o AxClass.get_info thy) class; 
24589  503 
val raw_intro = case pred_intro' 
504 
of SOME pred_intro => class_intro > OF_LAST pred_intro 

505 
 NONE => class_intro; 

506 
val sort = Sign.super_classes thy class; 

24847  507 
val typ = TVar ((Name.aT, 0), sort); 
24589  508 
val defs = these_defs thy sups; 
509 
in 

510 
raw_intro 

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

512 
> strip_all_ofclass thy sort 

513 
> Thm.strip_shyps 

514 
> MetaSimplifier.rewrite_rule defs 

515 
> Drule.unconstrainTs 

516 
end; 

517 

518 
fun class_interpretation class facts defs thy = 

519 
let 

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

25094
ba43514068fd
Interpretation equations may have name and/or attribute.
ballarin
parents:
25083
diff
changeset

527 
> prove_interpretation tac ((false, prfx), []) (Locale.Locale class) 
ba43514068fd
Interpretation equations may have name and/or attribute.
ballarin
parents:
25083
diff
changeset

528 
(inst, map (fn def => (("", []), def)) defs) 
25038  529 
> (fn cs => fold (Sign.add_const_constraint o apsnd SOME) cs) 
24589  530 
end; 
24218  531 

532 
fun intro_classes_tac facts st = 

533 
let 

534 
val thy = Thm.theory_of_thm st; 

535 
val classes = Sign.all_classes thy; 

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

537 
val class_intros = these_intros thy; 

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

538 
val axclass_intros = map_filter (try (#intro o AxClass.get_info thy)) classes; 
24218  539 
in 
25268  540 
Method.intros_tac (class_trivs @ class_intros @ axclass_intros) facts st 
24218  541 
end; 
542 

543 
fun default_intro_classes_tac [] = intro_classes_tac [] 

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

544 
 default_intro_classes_tac _ = no_tac; 
24218  545 

546 
fun default_tac rules ctxt facts = 

547 
HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE 

548 
default_intro_classes_tac facts; 

549 

550 
val _ = Context.add_setup (Method.add_methods 

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

552 
"backchain introduction rules of classes"), 

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

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

555 

25195
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

556 
fun subclass_rule thy (sub, sup) = 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

557 
let 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

558 
val ctxt = Locale.init sub thy; 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

559 
val ctxt_thy = ProofContext.init thy; 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

560 
val props = 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

561 
Locale.global_asms_of thy sup 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

562 
> maps snd 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

563 
> map (ObjectLogic.ensure_propT thy); 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

564 
fun tac { prems, context } = 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

565 
Locale.intro_locales_tac true context prems 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

566 
ORELSE ALLGOALS assume_tac; 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

567 
in 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

568 
Goal.prove_multi ctxt [] [] props tac 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

569 
> map (Assumption.export false ctxt ctxt_thy) 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

570 
> Variable.export ctxt ctxt_thy 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

571 
end; 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

572 

62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

573 
fun prove_single_subclass (sub, sup) thms ctxt thy = 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

574 
let 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

575 
val ctxt_thy = ProofContext.init thy; 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

576 
val subclass_rule = Conjunction.intr_balanced thms 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

577 
> Assumption.export false ctxt ctxt_thy 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

578 
> singleton (Variable.export ctxt ctxt_thy); 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

579 
val sub_inst = Thm.ctyp_of thy (TVar ((Name.aT, 0), [sub])); 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

580 
val sub_ax = #axioms (AxClass.get_info thy sub); 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

581 
val classrel = 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

582 
#intro (AxClass.get_info thy sup) 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

583 
> Drule.instantiate' [SOME sub_inst] [] 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

584 
> OF_LAST (subclass_rule OF sub_ax) 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

585 
> strip_all_ofclass thy (Sign.super_classes thy sup) 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

586 
> Thm.strip_shyps 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

587 
in 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

588 
thy 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

589 
> AxClass.add_classrel classrel 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

590 
> prove_interpretation_in (ALLGOALS (ProofContext.fact_tac thms)) 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

591 
I (sub, Locale.Locale sup) 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

592 
> ClassData.map (Graph.add_edge (sub, sup)) 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

593 
end; 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

594 

62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

595 
fun prove_subclass (sub, sup) thms ctxt thy = 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

596 
let 
25268  597 
val classes = ClassData.get thy; 
598 
val is_sup = not o null o curry (Graph.irreducible_paths classes) sub; 

599 
val supclasses = Graph.all_succs classes [sup] > filter_out is_sup; 

25195
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

600 
fun transform sup' = subclass_rule thy (sup, sup') > map (fn thm => thm OF thms); 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

601 
in 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

602 
thy 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

603 
> fold_rev (fn sup' => prove_single_subclass (sub, sup') 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

604 
(transform sup') ctxt) supclasses 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

605 
end; 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

606 

24218  607 

24589  608 
(** classes and class target **) 
24218  609 

25002  610 
(* class context syntax *) 
24748  611 

25083  612 
structure ClassSyntax = ProofDataFun( 
613 
type T = { 

614 
constraints: (string * typ) list, 

615 
base_sort: sort, 

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

25195
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

617 
unchecks: (term * term) list, 
25083  618 
passed: bool 
619 
} option; 

620 
fun init _ = NONE; 

621 
); 

622 

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

623 
fun synchronize_syntax sups base_sort ctxt = 
24914
95cda5dd58d5
added proper subclass concept; improved class target
haftmann
parents:
24901
diff
changeset

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

625 
val thy = ProofContext.theory_of ctxt; 
00c2179db769
synchronize_syntax: improved declare_const (still inactive);
wenzelm
parents:
25326
diff
changeset

626 

25195
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

627 
(* constraints *) 
25083  628 
val operations = these_operations thy sups; 
25195
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

629 
fun local_constraint (c, (_, (ty, _))) = 
25083  630 
let 
631 
val ty' = ty 

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

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

634 
> SOME; 

635 
in (c, ty') end 

25195
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

636 
val constraints = (map o apsnd) (fst o snd) operations; 
25083  637 

638 
(* check phase *) 

25318
c8352b38d47d
synchronize_syntax: declare operations within the local scope of fixes/consts
wenzelm
parents:
25311
diff
changeset

639 
val consts = ProofContext.consts_of ctxt; 
c8352b38d47d
synchronize_syntax: declare operations within the local scope of fixes/consts
wenzelm
parents:
25311
diff
changeset

640 
fun declare_const (c, _) = 
c8352b38d47d
synchronize_syntax: declare operations within the local scope of fixes/consts
wenzelm
parents:
25311
diff
changeset

641 
let val b = Sign.base_name c 
25344
00c2179db769
synchronize_syntax: improved declare_const (still inactive);
wenzelm
parents:
25326
diff
changeset

642 
in Sign.intern_const thy b = c ? Variable.declare_const (b, c) end; 
25318
c8352b38d47d
synchronize_syntax: declare operations within the local scope of fixes/consts
wenzelm
parents:
25311
diff
changeset

643 
val typargs = Consts.typargs consts; 
25209  644 
fun check_const (c, ty) (t, (_, typidx)) = ((nth (typargs (c, ty)) typidx), t); 
25083  645 
fun local_operation (c_ty as (c, _)) = AList.lookup (op =) operations c 
646 
> Option.map (check_const c_ty); 

25002  647 

25083  648 
(* uncheck phase *) 
25195
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

649 
val basify = 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

650 
map_atyps (fn ty as TFree (v, _) => if Name.aT = v then TFree (v, base_sort) 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

651 
else ty  ty => ty); 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

652 
val unchecks = these_unchecks thy sups 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

653 
> (map o pairself o map_types) basify; 
25083  654 
in 
655 
ctxt 

25318
c8352b38d47d
synchronize_syntax: declare operations within the local scope of fixes/consts
wenzelm
parents:
25311
diff
changeset

656 
(* > fold declare_const operations FIXME *) 
25083  657 
> fold (ProofContext.add_const_constraint o local_constraint) operations 
25209  658 
> ClassSyntax.put (SOME { 
25083  659 
constraints = constraints, 
660 
base_sort = base_sort, 

661 
local_operation = local_operation, 

25195
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

662 
unchecks = unchecks, 
25083  663 
passed = false 
25209  664 
}) 
25083  665 
end; 
666 

667 
fun refresh_syntax class ctxt = 

25002  668 
let 
669 
val thy = ProofContext.theory_of ctxt; 

25062  670 
val base_sort = (#base_sort o the_class_data thy) class; 
25344
00c2179db769
synchronize_syntax: improved declare_const (still inactive);
wenzelm
parents:
25326
diff
changeset

671 
in synchronize_syntax [class] base_sort ctxt end; 
24914
95cda5dd58d5
added proper subclass concept; improved class target
haftmann
parents:
24901
diff
changeset

672 

25083  673 
val mark_passed = (ClassSyntax.map o Option.map) 
25195
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

674 
(fn { constraints, base_sort, local_operation, unchecks, passed } => 
25083  675 
{ constraints = constraints, base_sort = base_sort, 
25195
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

676 
local_operation = local_operation, unchecks = unchecks, passed = true }); 
25083  677 

678 
fun sort_term_check ts ctxt = 

24748  679 
let 
25083  680 
val { constraints, base_sort, local_operation, passed, ... } = 
681 
the (ClassSyntax.get ctxt); 

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

25062  683 
then apfst (AList.update (op =) ((c, ty), t)) else I 
25083  684 
 check_typ (c, ty) (TVar (vi, _), t) = if TypeInfer.is_param vi 
25062  685 
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

686 
#> apsnd (insert (op =) vi) else I 
25083  687 
 check_typ _ _ = I; 
688 
fun add_const (Const c_ty) = Option.map (check_typ c_ty) (local_operation c_ty) 

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

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

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

694 
val subst_term = map_aterms 

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

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

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

700 
ctxt 

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

702 
> mark_passed 

703 
> pair ts' 

704 
> SOME 

705 
end; 

24748  706 

25062  707 
val uncheck = ref true; 
25002  708 

25083  709 
fun sort_term_uncheck ts ctxt = 
25002  710 
let 
711 
val thy = ProofContext.theory_of ctxt; 

25195
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

712 
val unchecks = (#unchecks o the o ClassSyntax.get) ctxt; 
25062  713 
val ts' = if ! uncheck 
25195
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

714 
then map (Pattern.rewrite_term thy unchecks []) ts else ts; 
25060  715 
in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt) end; 
25002  716 

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

717 
fun init_ctxt sups base_sort ctxt = 
25083  718 
ctxt 
719 
> Variable.declare_term 

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

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

721 
> synchronize_syntax sups base_sort 
25083  722 
> Context.proof_map ( 
723 
Syntax.add_term_check 0 "class" sort_term_check 

25103  724 
#> Syntax.add_term_uncheck 0 "class" sort_term_uncheck) 
24901
d3cbf79769b9
added first version of userspace type system for class target
haftmann
parents:
24847
diff
changeset

725 

25311  726 
fun init class thy = 
727 
thy 

728 
> Locale.init class 

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

729 
> init_ctxt [class] ((#base_sort o the_class_data thy) class); 
24914
95cda5dd58d5
added proper subclass concept; improved class target
haftmann
parents:
24901
diff
changeset

730 

24748  731 

24589  732 
(* class definition *) 
24218  733 

734 
local 

735 

24748  736 
fun gen_class_spec prep_class prep_expr process_expr thy raw_supclasses raw_includes_elems = 
24218  737 
let 
24748  738 
val supclasses = map (prep_class thy) raw_supclasses; 
25209  739 
val sups = filter (is_class thy) supclasses; 
740 
fun the_base_sort class = lookup_class_data thy class 

741 
> Option.map #base_sort 

742 
> the_default [class]; 

743 
val base_sort = Sign.minimize_sort thy (maps the_base_sort supclasses); 

24748  744 
val supsort = Sign.minimize_sort thy supclasses; 
25038  745 
val suplocales = map Locale.Locale sups; 
24748  746 
val (raw_elems, includes) = fold_rev (fn Locale.Elem e => apfst (cons e) 
747 
 Locale.Expr i => apsnd (cons (prep_expr thy i))) raw_includes_elems ([], []); 

748 
val supexpr = Locale.Merge suplocales; 

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

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

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

24847  754 
(fn TFree (_, sort) => TFree (Name.aT, sort)) supparams); 
24748  755 
in 
756 
ProofContext.init thy 

757 
> Locale.cert_expr supexpr [constrain] 

758 
> snd 

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

759 
> init_ctxt sups base_sort 
24748  760 
> process_expr Locale.empty raw_elems 
761 
> fst 

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

765 

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

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

768 

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

769 
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

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

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

772 
val consts = (map o apfst o apsnd) (Sign.certify_typ thy) raw_consts; 
25083  773 
fun add_const ((c, ty), syn) = 
774 
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

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

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

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

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

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

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

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

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

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

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

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

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

788 
(map fst cs @ other_consts) axioms_prop 
25002  789 
#> (fn class => `(fn _ => constrain_typs class cs) 
790 
#> (fn cs' => `(fn thy => AxClass.get_info thy class) 

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

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

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

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

794 

25002  795 
fun gen_class prep_spec prep_param bname 
24748  796 
raw_supclasses raw_includes_elems raw_other_consts thy = 
797 
let 

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

801 
val other_consts = map (tap (Sign.the_const_type thy) o prep_param thy) raw_other_consts; 
25163  802 
fun mk_inst class cs = 
803 
(map o apsnd o Term.map_type_tfree) (fn (v, _) => TFree (v, [class])) cs; 

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

806 
#>> Element.Fixes 

807 
 fork_syntax x = pair x; 

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

25326  809 
fun globalize (c, ty) = 
25062  810 
((c, Term.map_type_tfree (K (TFree (Name.aT, base_sort))) ty), 
811 
(the_default NoSyn o AList.lookup (op =) global_syn) c); 

25038  812 
fun extract_params thy = 
24218  813 
let 
25062  814 
val params = map fst (Locale.parameters_of thy class); 
24218  815 
in 
25062  816 
(params, (map globalize o snd o chop (length supconsts)) params) 
24218  817 
end; 
25038  818 
fun extract_assumes params thy cs = 
24218  819 
let 
820 
val consts = supconsts @ (map (fst o fst) params ~~ cs); 

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

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

823 
 subst t = t; 

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

25024  825 
((Sign.base_name name, map (Attrib.attribute_i thy) atts), 
24589  826 
(map o map_aterms) subst ts); 
24218  827 
in 
25038  828 
Locale.global_asms_of thy class 
24218  829 
> map prep_asm 
830 
end; 

831 
in 

832 
thy 

24748  833 
> Locale.add_locale_i (SOME "") bname mergeexpr elems 
25038  834 
> snd 
25311  835 
> ProofContext.theory_of 
836 
> `extract_params 

837 
> (fn (all_params, params) => 

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

838 
define_class_params (bname, supsort) params 
25038  839 
(extract_assumes params) other_consts 
840 
#> (fn (_, (consts, axioms)) => 

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

24218  842 
#> (fn class_intro => 
25062  843 
PureThy.note_thmss_qualified "" (NameSpace.append class classN) 
844 
[((introN, []), [([class_intro], [])])] 

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

25038  846 
add_class_data ((class, sups), 
25062  847 
(map fst params ~~ consts, base_sort, 
25163  848 
mk_inst class (map snd supconsts @ consts), 
25062  849 
calculate_morphism class (supconsts @ (map (fst o fst) params ~~ consts)), class_intro)) 
25038  850 
#> class_interpretation class axioms [] 
25311  851 
)))) 
25268  852 
> init class 
25038  853 
> pair class 
24218  854 
end; 
855 

25326  856 
fun read_const thy = #1 o Term.dest_Const o ProofContext.read_const (ProofContext.init thy); 
857 

24218  858 
in 
859 

25326  860 
val class_cmd = gen_class read_class_spec read_const; 
24748  861 
val class = gen_class check_class_spec (K I); 
24218  862 

863 
end; (*local*) 

864 

865 

24589  866 
(* definition in class target *) 
24218  867 

25096  868 
fun add_logical_const class pos ((c, mx), dict) thy = 
24218  869 
let 
25024  870 
val prfx = class_prefix class; 
871 
val thy' = thy > Sign.add_path prfx; 

25062  872 
val phi = morphism thy' class; 
25024  873 

25062  874 
val c' = Sign.full_name thy' c; 
25239  875 
val dict' = Morphism.term phi dict; 
876 
val dict_def = map_types Logic.unvarifyT dict'; 

877 
val ty' = Term.fastype_of dict_def; 

25083  878 
val ty'' = Type.strip_sorts ty'; 
25239  879 
val def_eq = Logic.mk_equals (Const (c', ty'), dict_def); 
24218  880 
in 
25024  881 
thy' 
25096  882 
> Sign.declare_const pos (c, ty'', mx) > snd 
25318
c8352b38d47d
synchronize_syntax: declare operations within the local scope of fixes/consts
wenzelm
parents:
25311
diff
changeset

883 
> Thm.add_def false (c, def_eq) (* FIXME PureThy.add_defs_i *) 
25062  884 
>> Thm.symmetric 
25083  885 
> (fn def => class_interpretation class [def] [Thm.prop_of def] 
25239  886 
#> register_operation class (c', ((dict, dict'), SOME (Thm.varifyT def)))) 
24218  887 
> Sign.restore_naming thy 
25083  888 
> Sign.add_const_constraint (c', SOME ty') 
24218  889 
end; 
890 

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

891 

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

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

893 

25103  894 
fun add_syntactic_const class prmode pos ((c, mx), rhs) thy = 
24836  895 
let 
25024  896 
val prfx = class_prefix class; 
25096  897 
val thy' = thy > Sign.add_path prfx; 
25062  898 
val phi = morphism thy class; 
899 

25096  900 
val c' = Sign.full_name thy' c; 
25146  901 
val rews = map (Logic.dest_equals o Thm.prop_of) (these_defs thy' [class]) 
902 
val rhs' = (Pattern.rewrite_term thy rews [] o Morphism.term phi) rhs; 

25239  903 
val ty' = Logic.unvarifyT (Term.fastype_of rhs'); 
24836  904 
in 
25096  905 
thy' 
25146  906 
> Sign.add_abbrev (#1 prmode) pos (c, map_types Type.strip_sorts rhs') > snd 
25096  907 
> Sign.add_const_constraint (c', SOME ty') 
25024  908 
> Sign.notation true prmode [(Const (c', ty'), mx)] 
25239  909 
> register_operation class (c', ((rhs, rhs'), NONE)) 
25096  910 
> Sign.restore_naming thy 
24836  911 
end; 
912 

24218  913 
end; 