author  haftmann 
Wed, 02 Dec 2009 11:29:49 +0100  
changeset 33970  74db95c74f89 
parent 33969  src/HOL/Tools/Datatype/datatype.ML@1e7ca47c6c3d 
child 34911  771830d3bd5e 
permissions  rwrr 
33970  1 
(* Title: HOL/Tools/Datatype/datatype_data.ML 
11539  2 
Author: Stefan Berghofer, TU Muenchen 
5177  3 

33970  4 
Datatype package: bookkeeping; interpretation of existing types as datatypes. 
5177  5 
*) 
6 

33970  7 
signature DATATYPE_DATA = 
6360  8 
sig 
33970  9 
include DATATYPE_COMMON 
10 
val derive_datatype_props : config > string list > string list option 

11 
> descr list > (string * sort) list > thm > thm list list > thm list list 

12 
> theory > string list * theory 

13 
val rep_datatype : config > (string list > Proof.context > Proof.context) 

14 
> string list option > term list > theory > Proof.state 

15 
val rep_datatype_cmd : string list option > string list > theory > Proof.state 

16 
val get_info : theory > string > info option 

17 
val the_info : theory > string > info 

18 
val the_descr : theory > string list 

19 
> descr * (string * sort) list * string list 

20 
* string * (string list * string list) * (typ list * typ list) 

21 
val the_spec : theory > string > (string * sort) list * (string * typ list) list 

22 
val all_distincts : theory > typ list > thm list list 

23 
val get_constrs : theory > string > (string * typ) list option 

24 
val get_all : theory > info Symtab.table 

25 
val info_of_constr : theory > string * typ > info option 

26 
val info_of_case : theory > string > info option 

27 
val interpretation : (config > string list > theory > theory) > theory > theory 

28 
val make_case : Proof.context > Datatype_Case.config > string list > term > 

29 
(term * term) list > term * (term * (int * bool)) list 

30 
val strip_case : Proof.context > bool > term > (term * (term * term) list) option 

31 
val read_typ: theory > string > (string * sort) list > typ * (string * sort) list 

32 
val cert_typ: theory > typ > (string * sort) list > typ * (string * sort) list 

33 
val mk_case_names_induct: descr > attribute 

34 
val setup: theory > theory 

32717
0e787c721fa3
reestablished reasonable inner outline for module
haftmann
parents:
32712
diff
changeset

35 
end; 
0e787c721fa3
reestablished reasonable inner outline for module
haftmann
parents:
32712
diff
changeset

36 

33970  37 
structure Datatype_Data: DATATYPE_DATA = 
33963
977b94b64905
renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33959
diff
changeset

38 
struct 
5177  39 

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

40 
open Datatype_Aux; 
33970  41 

42 
(** theory data **) 

43 

44 
(* data management *) 

45 

46 
structure DatatypesData = Theory_Data 

47 
( 

48 
type T = 

49 
{types: info Symtab.table, 

50 
constrs: (string * info) list Symtab.table, 

51 
cases: info Symtab.table}; 

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

52 

33970  53 
val empty = 
54 
{types = Symtab.empty, constrs = Symtab.empty, cases = Symtab.empty}; 

55 
val extend = I; 

56 
fun merge 

57 
({types = types1, constrs = constrs1, cases = cases1}, 

58 
{types = types2, constrs = constrs2, cases = cases2}) : T = 

59 
{types = Symtab.merge (K true) (types1, types2), 

60 
constrs = Symtab.join (K (AList.merge (op =) (K true))) (constrs1, constrs2), 

61 
cases = Symtab.merge (K true) (cases1, cases2)}; 

62 
); 

63 

64 
val get_all = #types o DatatypesData.get; 

65 
val get_info = Symtab.lookup o get_all; 

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

66 

33970  67 
fun the_info thy name = 
68 
(case get_info thy name of 

69 
SOME info => info 

70 
 NONE => error ("Unknown datatype " ^ quote name)); 

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

71 

33970  72 
fun info_of_constr thy (c, T) = 
73 
let 

74 
val tab = Symtab.lookup_list ((#constrs o DatatypesData.get) thy) c; 

75 
val hint = case strip_type T of (_, Type (tyco, _)) => SOME tyco  _ => NONE; 

76 
val default = if null tab then NONE 

77 
else SOME (snd (Library.last_elem tab)) 

78 
(*conservative wrt. overloaded constructors*); 

79 
in case hint 

80 
of NONE => default 

81 
 SOME tyco => case AList.lookup (op =) tab tyco 

82 
of NONE => default (*permissive*) 

83 
 SOME info => SOME info 

84 
end; 

85 

86 
val info_of_case = Symtab.lookup o #cases o DatatypesData.get; 

87 

88 
fun register (dt_infos : (string * info) list) = 

89 
DatatypesData.map (fn {types, constrs, cases} => 

90 
{types = types > fold Symtab.update dt_infos, 

91 
constrs = constrs > fold (fn (constr, dtname_info) => 

92 
Symtab.map_default (constr, []) (cons dtname_info)) 

93 
(maps (fn (dtname, info as {descr, index, ...}) => 

94 
map (rpair (dtname, info) o fst) 

95 
(#3 (the (AList.lookup op = descr index)))) dt_infos), 

96 
cases = cases > fold Symtab.update 

97 
(map (fn (_, info as {case_name, ...}) => (case_name, info)) dt_infos)}); 

98 

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

99 

33970  100 
(* complex queries *) 
101 

102 
fun the_spec thy dtco = 

103 
let 

104 
val { descr, index, sorts = raw_sorts, ... } = the_info thy dtco; 

105 
val SOME (_, dtys, raw_cos) = AList.lookup (op =) descr index; 

106 
val sorts = map ((fn v => (v, (the o AList.lookup (op =) raw_sorts) v)) 

107 
o Datatype_Aux.dest_DtTFree) dtys; 

108 
val cos = map 

109 
(fn (co, tys) => (co, map (Datatype_Aux.typ_of_dtyp descr sorts) tys)) raw_cos; 

110 
in (sorts, cos) end; 

111 

112 
fun the_descr thy (raw_tycos as raw_tyco :: _) = 

113 
let 

114 
val info = the_info thy raw_tyco; 

115 
val descr = #descr info; 

116 

117 
val SOME (_, dtys, _) = AList.lookup (op =) descr (#index info); 

118 
val vs = map ((fn v => (v, (the o AList.lookup (op =) (#sorts info)) v)) 

119 
o dest_DtTFree) dtys; 

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

120 

33970  121 
fun is_DtTFree (DtTFree _) = true 
122 
 is_DtTFree _ = false 

123 
val k = find_index (fn (_, (_, dTs, _)) => not (forall is_DtTFree dTs)) descr; 

124 
val protoTs as (dataTs, _) = chop k descr 

125 
> (pairself o map) (fn (_, (tyco, dTs, _)) => (tyco, map (typ_of_dtyp descr vs) dTs)); 

126 

127 
val tycos = map fst dataTs; 

128 
val _ = if eq_set (op =) (tycos, raw_tycos) then () 

129 
else error ("Type constructors " ^ commas (map quote raw_tycos) 

130 
^ " do not belong exhaustively to one mutual recursive datatype"); 

131 

132 
val (Ts, Us) = (pairself o map) Type protoTs; 

133 

134 
val names = map Long_Name.base_name (the_default tycos (#alt_names info)); 

135 
val (auxnames, _) = Name.make_context names 

136 
> fold_map (yield_singleton Name.variants o name_of_typ) Us; 

137 
val prefix = space_implode "_" names; 

138 

139 
in (descr, vs, tycos, prefix, (names, auxnames), (Ts, Us)) end; 

140 

141 
fun all_distincts thy Ts = 

142 
let 

143 
fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts 

144 
 add_tycos _ = I; 

145 
val tycos = fold add_tycos Ts []; 

146 
in map_filter (Option.map #distinct o get_info thy) tycos end; 

147 

148 
fun get_constrs thy dtco = 

149 
case try (the_spec thy) dtco 

150 
of SOME (sorts, cos) => 

151 
let 

152 
fun subst (v, sort) = TVar ((v, 0), sort); 

153 
fun subst_ty (TFree v) = subst v 

154 
 subst_ty ty = ty; 

155 
val dty = Type (dtco, map subst sorts); 

156 
fun mk_co (co, tys) = (co, map (Term.map_atyps subst_ty) tys > dty); 

157 
in SOME (map mk_co cos) end 

158 
 NONE => NONE; 

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

159 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

160 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

161 

33970  162 
(** various auxiliary **) 
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

163 

33970  164 
(* prepare datatype specifications *) 
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

165 

33970  166 
fun read_typ thy str sorts = 
167 
let 

168 
val ctxt = ProofContext.init thy 

169 
> fold (Variable.declare_typ o TFree) sorts; 

170 
val T = Syntax.read_typ ctxt str; 

171 
in (T, Term.add_tfreesT T sorts) end; 

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

172 

33970  173 
fun cert_typ sign raw_T sorts = 
174 
let 

175 
val T = Type.no_tvars (Sign.certify_typ sign raw_T) 

176 
handle TYPE (msg, _, _) => error msg; 

177 
val sorts' = Term.add_tfreesT T sorts; 

178 
val _ = 

179 
case duplicates (op =) (map fst sorts') of 

180 
[] => () 

181 
 dups => error ("Inconsistent sort constraints for " ^ commas dups) 

182 
in (T, sorts') end; 

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

183 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

184 

33970  185 
(* case names *) 
186 

187 
local 

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

188 

33970  189 
fun dt_recs (DtTFree _) = [] 
190 
 dt_recs (DtType (_, dts)) = maps dt_recs dts 

191 
 dt_recs (DtRec i) = [i]; 

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

192 

33970  193 
fun dt_cases (descr: descr) (_, args, constrs) = 
194 
let 

195 
fun the_bname i = Long_Name.base_name (#1 (the (AList.lookup (op =) descr i))); 

196 
val bnames = map the_bname (distinct (op =) (maps dt_recs args)); 

197 
in map (fn (c, _) => space_implode "_" (Long_Name.base_name c :: bnames)) constrs end; 

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

198 

33970  199 
fun induct_cases descr = 
200 
Datatype_Prop.indexify_names (maps (dt_cases descr) (map #2 descr)); 

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

201 

33970  202 
fun exhaust_cases descr i = dt_cases descr (the (AList.lookup (op =) descr i)); 
203 

204 
in 

205 

206 
fun mk_case_names_induct descr = Rule_Cases.case_names (induct_cases descr); 

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

207 

33970  208 
fun mk_case_names_exhausts descr new = 
209 
map (Rule_Cases.case_names o exhaust_cases descr o #1) 

210 
(filter (fn ((_, (name, _, _))) => member (op =) new name) descr); 

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

211 

33970  212 
end; 
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

213 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

214 

33970  215 
(* translation rules for case *) 
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

216 

33970  217 
fun make_case ctxt = Datatype_Case.make_case 
218 
(info_of_constr (ProofContext.theory_of ctxt)) ctxt; 

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

219 

33970  220 
fun strip_case ctxt = Datatype_Case.strip_case 
221 
(info_of_case (ProofContext.theory_of ctxt)); 

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

222 

33970  223 
fun add_case_tr' case_names thy = 
224 
Sign.add_advanced_trfuns ([], [], 

225 
map (fn case_name => 

226 
let val case_name' = Sign.const_syntax_name thy case_name 

227 
in (case_name', Datatype_Case.case_tr' info_of_case case_name') 

228 
end) case_names, []) thy; 

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

229 

33970  230 
val trfun_setup = 
231 
Sign.add_advanced_trfuns ([], 

232 
[("_case_syntax", Datatype_Case.case_tr true info_of_constr)], 

233 
[], []); 

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

234 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

235 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

236 

33970  237 
(** document antiquotation **) 
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

238 

33970  239 
val _ = ThyOutput.antiquotation "datatype" Args.tyname 
240 
(fn {source = src, context = ctxt, ...} => fn dtco => 

241 
let 

242 
val thy = ProofContext.theory_of ctxt; 

243 
val (vs, cos) = the_spec thy dtco; 

244 
val ty = Type (dtco, map TFree vs); 

245 
fun pretty_typ_bracket (ty as Type (_, _ :: _)) = 

246 
Pretty.enclose "(" ")" [Syntax.pretty_typ ctxt ty] 

247 
 pretty_typ_bracket ty = 

248 
Syntax.pretty_typ ctxt ty; 

249 
fun pretty_constr (co, tys) = 

250 
(Pretty.block o Pretty.breaks) 

251 
(Syntax.pretty_term ctxt (Const (co, tys > ty)) :: 

252 
map pretty_typ_bracket tys); 

253 
val pretty_datatype = 

254 
Pretty.block 

255 
(Pretty.command "datatype" :: Pretty.brk 1 :: 

256 
Syntax.pretty_typ ctxt ty :: 

257 
Pretty.str " =" :: Pretty.brk 1 :: 

258 
flat (separate [Pretty.brk 1, Pretty.str " "] 

259 
(map (single o pretty_constr) cos))); 

260 
in ThyOutput.output (ThyOutput.maybe_pretty_source (K pretty_datatype) src [()]) end); 

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

261 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

262 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

263 

33970  264 
(** abstract theory extensions relative to a datatype characterisation **) 
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

265 

33970  266 
structure Datatype_Interpretation = Interpretation 
267 
(type T = config * string list val eq: T * T > bool = eq_snd op =); 

268 
fun interpretation f = Datatype_Interpretation.interpretation (uncurry f); 

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

269 

33970  270 
fun make_dt_info alt_names descr sorts induct inducts rec_names rec_rewrites 
271 
(index, (((((((((((_, (tname, _, _))), inject), distinct), 

272 
exhaust), nchotomy), case_name), case_rewrites), case_cong), weak_case_cong), 

273 
(split, split_asm))) = 

274 
(tname, 

275 
{index = index, 

276 
alt_names = alt_names, 

277 
descr = descr, 

278 
sorts = sorts, 

279 
inject = inject, 

280 
distinct = distinct, 

281 
induct = induct, 

282 
inducts = inducts, 

283 
exhaust = exhaust, 

284 
nchotomy = nchotomy, 

285 
rec_names = rec_names, 

286 
rec_rewrites = rec_rewrites, 

287 
case_name = case_name, 

288 
case_rewrites = case_rewrites, 

289 
case_cong = case_cong, 

290 
weak_case_cong = weak_case_cong, 

291 
split = split, 

292 
split_asm = split_asm}); 

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

293 

33970  294 
fun derive_datatype_props config dt_names alt_names descr sorts 
295 
induct inject distinct thy1 = 

296 
let 

297 
val thy2 = thy1 > Theory.checkpoint; 

298 
val flat_descr = flat descr; 

299 
val new_type_names = map Long_Name.base_name (the_default dt_names alt_names); 

300 
val _ = message config ("Deriving properties for datatype(s) " ^ commas_quote new_type_names); 

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

301 

33970  302 
val (exhaust, thy3) = Datatype_Abs_Proofs.prove_casedist_thms config new_type_names 
303 
descr sorts induct (mk_case_names_exhausts flat_descr dt_names) thy2; 

304 
val (nchotomys, thy4) = Datatype_Abs_Proofs.prove_nchotomys config new_type_names 

305 
descr sorts exhaust thy3; 

306 
val ((rec_names, rec_rewrites), thy5) = Datatype_Abs_Proofs.prove_primrec_thms 

307 
config new_type_names descr sorts (#inject o the o Symtab.lookup (get_all thy4)) 

308 
inject (distinct, all_distincts thy2 (get_rec_types flat_descr sorts)) 

309 
induct thy4; 

310 
val ((case_rewrites, case_names), thy6) = Datatype_Abs_Proofs.prove_case_thms 

311 
config new_type_names descr sorts rec_names rec_rewrites thy5; 

312 
val (case_congs, thy7) = Datatype_Abs_Proofs.prove_case_congs new_type_names 

313 
descr sorts nchotomys case_rewrites thy6; 

314 
val (weak_case_congs, thy8) = Datatype_Abs_Proofs.prove_weak_case_congs new_type_names 

315 
descr sorts thy7; 

316 
val (splits, thy9) = Datatype_Abs_Proofs.prove_split_thms 

317 
config new_type_names descr sorts inject distinct exhaust case_rewrites thy8; 

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

318 

33970  319 
val inducts = Project_Rule.projections (ProofContext.init thy2) induct; 
320 
val dt_infos = map_index 

321 
(make_dt_info alt_names flat_descr sorts induct inducts rec_names rec_rewrites) 

322 
(hd descr ~~ inject ~~ distinct ~~ exhaust ~~ nchotomys ~~ 

323 
case_names ~~ case_rewrites ~~ case_congs ~~ weak_case_congs ~~ splits); 

324 
val dt_names = map fst dt_infos; 

325 
val prfx = Binding.qualify true (space_implode "_" new_type_names); 

326 
val simps = flat (inject @ distinct @ case_rewrites) @ rec_rewrites; 

327 
val named_rules = flat (map_index (fn (index, tname) => 

328 
[((Binding.empty, [nth inducts index]), [Induct.induct_type tname]), 

329 
((Binding.empty, [nth exhaust index]), [Induct.cases_type tname])]) dt_names); 

330 
val unnamed_rules = map (fn induct => 

331 
((Binding.empty, [induct]), [Rule_Cases.inner_rule, Induct.induct_type ""])) 

332 
(drop (length dt_names) inducts); 

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

333 
in 
33970  334 
thy9 
335 
> PureThy.add_thmss ([((prfx (Binding.name "simps"), simps), []), 

336 
((prfx (Binding.name "inducts"), inducts), []), 

337 
((prfx (Binding.name "splits"), maps (fn (x, y) => [x, y]) splits), []), 

338 
((Binding.empty, flat case_rewrites @ flat distinct @ rec_rewrites), 

339 
[Simplifier.simp_add]), 

340 
((Binding.empty, rec_rewrites), [Code.add_default_eqn_attribute]), 

341 
((Binding.empty, flat inject), [iff_add]), 

342 
((Binding.empty, map (fn th => th RS notE) (flat distinct)), 

343 
[Classical.safe_elim NONE]), 

344 
((Binding.empty, weak_case_congs), [Simplifier.attrib (op addcongs)])] 

345 
@ named_rules @ unnamed_rules) 

346 
> snd 

347 
> add_case_tr' case_names 

348 
> register dt_infos 

349 
> Datatype_Interpretation.data (config, dt_names) 

350 
> pair dt_names 

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

351 
end; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

352 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

353 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

354 

33970  355 
(** declare existing type as datatype **) 
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

356 

33970  357 
fun prove_rep_datatype config dt_names alt_names descr sorts 
358 
raw_inject half_distinct raw_induct thy1 = 

359 
let 

360 
val raw_distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct; 

361 
val new_type_names = map Long_Name.base_name (the_default dt_names alt_names); 

362 
val (((inject, distinct), [induct]), thy2) = 

363 
thy1 

364 
> store_thmss "inject" new_type_names raw_inject 

365 
>> store_thmss "distinct" new_type_names raw_distinct 

366 
> Sign.add_path (space_implode "_" new_type_names) 

367 
>> PureThy.add_thms [((Binding.name "induct", raw_induct), [mk_case_names_induct descr])] 

368 
> Sign.restore_naming thy1; 

369 
in 

370 
thy2 

371 
> derive_datatype_props config dt_names alt_names [descr] sorts 

372 
induct inject distinct 

373 
end; 

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

374 

33970  375 
fun gen_rep_datatype prep_term config after_qed alt_names raw_ts thy = 
376 
let 

377 
fun constr_of_term (Const (c, T)) = (c, T) 

378 
 constr_of_term t = 

379 
error ("Not a constant: " ^ Syntax.string_of_term_global thy t); 

380 
fun no_constr (c, T) = error ("Bad constructor: " 

381 
^ Sign.extern_const thy c ^ "::" 

382 
^ Syntax.string_of_typ_global thy T); 

383 
fun type_of_constr (cT as (_, T)) = 

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

384 
let 
33970  385 
val frees = OldTerm.typ_tfrees T; 
386 
val (tyco, vs) = ((apsnd o map) (dest_TFree) o dest_Type o snd o strip_type) T 

387 
handle TYPE _ => no_constr cT 

388 
val _ = if has_duplicates (eq_fst (op =)) vs then no_constr cT else (); 

389 
val _ = if length frees <> length vs then no_constr cT else (); 

390 
in (tyco, (vs, cT)) end; 

391 

392 
val raw_cs = AList.group (op =) (map (type_of_constr o constr_of_term o prep_term thy) raw_ts); 

393 
val _ = case map_filter (fn (tyco, _) => 

394 
if Symtab.defined (get_all thy) tyco then SOME tyco else NONE) raw_cs 

395 
of [] => () 

396 
 tycos => error ("Type(s) " ^ commas (map quote tycos) 

397 
^ " already represented inductivly"); 

398 
val raw_vss = maps (map (map snd o fst) o snd) raw_cs; 

399 
val ms = case distinct (op =) (map length raw_vss) 

400 
of [n] => 0 upto n  1 

401 
 _ => error ("Different types in given constructors"); 

402 
fun inter_sort m = map (fn xs => nth xs m) raw_vss 

403 
> Library.foldr1 (Sorts.inter_sort (Sign.classes_of thy)) 

404 
val sorts = map inter_sort ms; 

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

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

406 

33970  407 
fun norm_constr (raw_vs, (c, T)) = (c, map_atyps 
408 
(TFree o (the o AList.lookup (op =) (map fst raw_vs ~~ vs)) o fst o dest_TFree) T); 

409 

410 
val cs = map (apsnd (map norm_constr)) raw_cs; 

411 
val dtyps_of_typ = map (dtyp_of_typ (map (rpair (map fst vs) o fst) cs)) 

412 
o fst o strip_type; 

413 
val dt_names = map fst cs; 

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

414 

33970  415 
fun mk_spec (i, (tyco, constr)) = (i, (tyco, 
416 
map (DtTFree o fst) vs, 

417 
(map o apsnd) dtyps_of_typ constr)) 

418 
val descr = map_index mk_spec cs; 

419 
val injs = Datatype_Prop.make_injs [descr] vs; 

420 
val half_distincts = map snd (Datatype_Prop.make_distincts [descr] vs); 

421 
val ind = Datatype_Prop.make_ind [descr] vs; 

422 
val rules = (map o map o map) Logic.close_form [[[ind]], injs, half_distincts]; 

423 

424 
fun after_qed' raw_thms = 

425 
let 

426 
val [[[raw_induct]], raw_inject, half_distinct] = 

427 
unflat rules (map Drule.zero_var_indexes_list raw_thms); 

428 
(*FIXME somehow dubious*) 

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

429 
in 
33970  430 
ProofContext.theory_result 
431 
(prove_rep_datatype config dt_names alt_names descr vs 

432 
raw_inject half_distinct raw_induct) 

433 
#> after_qed 

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

434 
end; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

435 
in 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

436 
thy 
33970  437 
> ProofContext.init 
438 
> Proof.theorem_i NONE after_qed' ((map o map) (rpair []) (flat rules)) 

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

439 
end; 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

440 

33970  441 
val rep_datatype = gen_rep_datatype Sign.cert_term; 
442 
val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global default_config (K I); 

443 

444 

445 

446 
(** package setup **) 

447 

448 
(* setup theory *) 

449 

450 
val setup = 

451 
trfun_setup #> 

452 
Datatype_Interpretation.init; 

453 

454 

455 
(* outer syntax *) 

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

456 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

457 
local 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

458 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

459 
structure P = OuterParse and K = OuterKeyword 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

460 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

461 
in 
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

462 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

463 
val _ = 
33970  464 
OuterSyntax.command "rep_datatype" "represent existing types inductively" K.thy_goal 
465 
(Scan.option (P.$$$ "("  Scan.repeat1 P.name  P.$$$ ")")  Scan.repeat1 P.term 

466 
>> (fn (alt_names, ts) => Toplevel.print 

467 
o Toplevel.theory_to_proof (rep_datatype_cmd alt_names ts))); 

6385
5a6570458d9e
rep_datatype: '_i' version, attributes, outer syntax;
wenzelm
parents:
6360
diff
changeset

468 

30391
d930432adb13
adapted to simplified ThyOutput.antiquotation interface;
wenzelm
parents:
30364
diff
changeset

469 
end; 
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

470 

f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

471 
end; 