42 val Abs_inject = thm "type_definition.Abs_inject"; |
43 val Abs_inject = thm "type_definition.Abs_inject"; |
43 val Rep_cases = thm "type_definition.Rep_cases"; |
44 val Rep_cases = thm "type_definition.Rep_cases"; |
44 val Abs_cases = thm "type_definition.Abs_cases"; |
45 val Abs_cases = thm "type_definition.Abs_cases"; |
45 val Rep_induct = thm "type_definition.Rep_induct"; |
46 val Rep_induct = thm "type_definition.Rep_induct"; |
46 val Abs_induct = thm "type_definition.Abs_induct"; |
47 val Abs_induct = thm "type_definition.Abs_induct"; |
|
48 |
|
49 |
|
50 |
|
51 (** theory data **) |
|
52 |
|
53 structure TypedefArgs = |
|
54 struct |
|
55 val name = "HOL/typedef"; |
|
56 type T = (typ * typ * string * string) Symtab.table; |
|
57 val empty = Symtab.empty; |
|
58 val copy = I; |
|
59 val prep_ext = I; |
|
60 val merge = Symtab.merge op =; |
|
61 fun print sg _ = (); |
|
62 end; |
|
63 |
|
64 structure TypedefData = TheoryDataFun(TypedefArgs); |
|
65 |
|
66 fun put_typedef newT oldT Abs_name Rep_name thy = |
|
67 TypedefData.put (Symtab.update_new |
|
68 ((fst (dest_Type newT), (newT, oldT, Abs_name, Rep_name)), |
|
69 TypedefData.get thy)) thy; |
47 |
70 |
48 |
71 |
49 |
72 |
50 (** type declarations **) |
73 (** type declarations **) |
51 |
74 |
141 val typedef_prop = |
164 val typedef_prop = |
142 Logic.mk_implies (goal, HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ set')); |
165 Logic.mk_implies (goal, HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ set')); |
143 |
166 |
144 fun typedef_result (theory, nonempty) = |
167 fun typedef_result (theory, nonempty) = |
145 theory |
168 theory |
|
169 |> put_typedef newT oldT (full Abs_name) (full Rep_name) |
146 |> add_typedecls [(t, vs, mx)] |
170 |> add_typedecls [(t, vs, mx)] |
147 |> Theory.add_consts_i |
171 |> Theory.add_consts_i |
148 ((if def then [(name, setT, NoSyn)] else []) @ |
172 ((if def then [(name, setT, NoSyn)] else []) @ |
149 [(Rep_name, newT --> oldT, NoSyn), |
173 [(Rep_name, newT --> oldT, NoSyn), |
150 (Abs_name, oldT --> newT, NoSyn)]) |
174 (Abs_name, oldT --> newT, NoSyn)]) |
248 val typedef_proof = gen_typedef_proof read_term; |
272 val typedef_proof = gen_typedef_proof read_term; |
249 val typedef_proof_i = gen_typedef_proof cert_term; |
273 val typedef_proof_i = gen_typedef_proof cert_term; |
250 |
274 |
251 |
275 |
252 |
276 |
|
277 (** trivial code generator **) |
|
278 |
|
279 fun typedef_codegen thy gr dep brack t = |
|
280 let |
|
281 fun mk_fun s T ts = |
|
282 let |
|
283 val (gr', _) = Codegen.invoke_tycodegen thy dep false (gr, T); |
|
284 val (gr'', ps) = |
|
285 foldl_map (Codegen.invoke_codegen thy dep true) (gr', ts); |
|
286 val id = Codegen.mk_const_id (sign_of thy) s |
|
287 in Some (gr'', Codegen.mk_app brack (Pretty.str id) ps) end; |
|
288 fun get_name (Type (tname, _)) = tname |
|
289 | get_name _ = ""; |
|
290 fun lookup f T = if_none (apsome f (Symtab.lookup |
|
291 (TypedefData.get thy, get_name T))) "" |
|
292 in |
|
293 (case strip_comb t of |
|
294 (Const (s, Type ("fun", [T, U])), ts) => |
|
295 if lookup #4 T = s andalso |
|
296 is_none (Codegen.get_assoc_type thy (get_name T)) |
|
297 then mk_fun s T ts |
|
298 else if lookup #3 U = s andalso |
|
299 is_none (Codegen.get_assoc_type thy (get_name U)) |
|
300 then mk_fun s U ts |
|
301 else None |
|
302 | _ => None) |
|
303 end; |
|
304 |
|
305 fun mk_tyexpr [] s = Pretty.str s |
|
306 | mk_tyexpr [p] s = Pretty.block [p, Pretty.str (" " ^ s)] |
|
307 | mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps; |
|
308 |
|
309 fun typedef_tycodegen thy gr dep brack (Type (s, Ts)) = |
|
310 (case Symtab.lookup (TypedefData.get thy, s) of |
|
311 None => None |
|
312 | Some (newT as Type (tname, Us), oldT, Abs_name, Rep_name) => |
|
313 if is_some (Codegen.get_assoc_type thy tname) then None else |
|
314 let |
|
315 val sg = sign_of thy; |
|
316 val Abs_id = Codegen.mk_const_id sg Abs_name; |
|
317 val Rep_id = Codegen.mk_const_id sg Rep_name; |
|
318 val ty_id = Codegen.mk_type_id sg s; |
|
319 val (gr', qs) = foldl_map |
|
320 (Codegen.invoke_tycodegen thy dep (length Ts = 1)) (gr, Ts); |
|
321 val gr'' = Graph.add_edge (Abs_id, dep) gr' handle Graph.UNDEF _ => |
|
322 let |
|
323 val (gr'', p :: ps) = foldl_map |
|
324 (Codegen.invoke_tycodegen thy Abs_id false) |
|
325 (Graph.add_edge (Abs_id, dep) |
|
326 (Graph.new_node (Abs_id, (None, "")) gr'), oldT :: Us); |
|
327 val s = |
|
328 Pretty.string_of (Pretty.block [Pretty.str "datatype ", |
|
329 mk_tyexpr ps ty_id, |
|
330 Pretty.str " =", Pretty.brk 1, Pretty.str (Abs_id ^ " of"), |
|
331 Pretty.brk 1, p, Pretty.str ";"]) ^ "\n\n" ^ |
|
332 Pretty.string_of (Pretty.block [Pretty.str ("fun " ^ Rep_id), |
|
333 Pretty.brk 1, Pretty.str ("(" ^ Abs_id), Pretty.brk 1, |
|
334 Pretty.str "x) = x;"]) ^ "\n\n" ^ |
|
335 (if "term_of" mem !Codegen.mode then |
|
336 Pretty.string_of (Pretty.block [Pretty.str "fun ", |
|
337 Codegen.mk_term_of sg false newT, Pretty.brk 1, |
|
338 Pretty.str ("(" ^ Abs_id), Pretty.brk 1, |
|
339 Pretty.str "x) =", Pretty.brk 1, |
|
340 Pretty.block [Pretty.str ("Const (\"" ^ Abs_name ^ "\","), |
|
341 Pretty.brk 1, Codegen.mk_type false (oldT --> newT), |
|
342 Pretty.str ")"], Pretty.str " $", Pretty.brk 1, |
|
343 Codegen.mk_term_of sg false oldT, Pretty.brk 1, |
|
344 Pretty.str "x;"]) ^ "\n\n" |
|
345 else "") ^ |
|
346 (if "test" mem !Codegen.mode then |
|
347 Pretty.string_of (Pretty.block [Pretty.str "fun ", |
|
348 Codegen.mk_gen sg false [] "" newT, Pretty.brk 1, |
|
349 Pretty.str "i =", Pretty.brk 1, |
|
350 Pretty.block [Pretty.str (Abs_id ^ " ("), |
|
351 Codegen.mk_gen sg false [] "" oldT, Pretty.brk 1, |
|
352 Pretty.str "i);"]]) ^ "\n\n" |
|
353 else "") |
|
354 in Graph.map_node Abs_id (K (None, s)) gr'' end |
|
355 in |
|
356 Some (gr'', mk_tyexpr qs ty_id) |
|
357 end) |
|
358 | typedef_tycodegen thy gr dep brack _ = None; |
|
359 |
|
360 val setup = |
|
361 [TypedefData.init, |
|
362 Codegen.add_codegen "typedef" typedef_codegen, |
|
363 Codegen.add_tycodegen "typedef" typedef_tycodegen]; |
|
364 |
|
365 |
|
366 |
253 (** outer syntax **) |
367 (** outer syntax **) |
254 |
368 |
255 local structure P = OuterParse and K = OuterSyntax.Keyword in |
369 local structure P = OuterParse and K = OuterSyntax.Keyword in |
256 |
370 |
257 val typedeclP = |
371 val typedeclP = |