49112
|
1 |
(* Title: HOL/Codatatype/Tools/bnf_fp_sugar.ML
|
|
2 |
Author: Jasmin Blanchette, TU Muenchen
|
|
3 |
Copyright 2012
|
|
4 |
|
|
5 |
Sugar for constructing LFPs and GFPs.
|
|
6 |
*)
|
|
7 |
|
|
8 |
signature BNF_FP_SUGAR =
|
|
9 |
sig
|
|
10 |
end;
|
|
11 |
|
|
12 |
structure BNF_FP_Sugar : BNF_FP_SUGAR =
|
|
13 |
struct
|
|
14 |
|
49119
|
15 |
open BNF_Util
|
|
16 |
open BNF_Wrap
|
|
17 |
open BNF_FP_Util
|
|
18 |
open BNF_LFP
|
|
19 |
open BNF_GFP
|
|
20 |
|
|
21 |
fun cannot_merge_types () = error "Mutually recursive (co)datatypes must have same type parameters";
|
|
22 |
|
|
23 |
fun merge_type_arg_constrained ctxt (T, c) (T', c') =
|
|
24 |
if T = T' then
|
|
25 |
(case (c, c') of
|
|
26 |
(_, NONE) => (T, c)
|
|
27 |
| (NONE, _) => (T, c')
|
|
28 |
| _ =>
|
|
29 |
if c = c' then
|
|
30 |
(T, c)
|
|
31 |
else
|
|
32 |
error ("Inconsistent sort constraints for type variable " ^
|
|
33 |
quote (Syntax.string_of_typ ctxt T)))
|
|
34 |
else
|
|
35 |
cannot_merge_types ();
|
|
36 |
|
|
37 |
fun merge_type_args_constrained ctxt (cAs, cAs') =
|
|
38 |
if length cAs = length cAs' then map2 (merge_type_arg_constrained ctxt) cAs cAs'
|
|
39 |
else cannot_merge_types ();
|
|
40 |
|
|
41 |
fun type_args_constrained_of_spec (((cAs, _), _), _) = cAs;
|
|
42 |
fun type_name_of_spec (((_, b), _), _) = b;
|
|
43 |
fun mixfix_of_spec ((_, mx), _) = mx;
|
|
44 |
fun ctr_specs_of_spec (_, ctr_specs) = ctr_specs;
|
|
45 |
|
|
46 |
fun disc_of_ctr_spec (((disc, _), _), _) = disc;
|
|
47 |
fun ctr_of_ctr_spec (((_, ctr), _), _) = ctr;
|
|
48 |
fun args_of_ctr_spec ((_, args), _) = args;
|
|
49 |
fun mixfix_of_ctr_spec (_, mx) = mx;
|
|
50 |
|
|
51 |
val mk_prod_sum = mk_sumTN o map HOLogic.mk_tupleT;
|
|
52 |
|
|
53 |
val lfp_info = bnf_lfp;
|
|
54 |
val gfp_info = bnf_gfp;
|
|
55 |
|
|
56 |
fun prepare_data prepare_typ construct specs lthy =
|
49112
|
57 |
let
|
49119
|
58 |
val constrained_passiveAs =
|
|
59 |
map (map (apfst (prepare_typ lthy)) o type_args_constrained_of_spec) specs
|
|
60 |
|> Library.foldr1 (merge_type_args_constrained lthy);
|
|
61 |
val passiveAs = map fst constrained_passiveAs;
|
|
62 |
|
|
63 |
val _ = (case duplicates (op =) passiveAs of [] => ()
|
|
64 |
| T :: _ => error ("Duplicate type parameter " ^ quote (Syntax.string_of_typ lthy T)));
|
|
65 |
|
|
66 |
(* TODO: check that no type variables occur in the rhss that's not in the lhss *)
|
|
67 |
(* TODO: use sort constraints on type args *)
|
|
68 |
|
|
69 |
val N = length specs;
|
|
70 |
|
|
71 |
val bs = map type_name_of_spec specs;
|
|
72 |
val mixfixes = map mixfix_of_spec specs;
|
|
73 |
|
|
74 |
val _ = (case duplicates Binding.eq_name bs of [] => ()
|
|
75 |
| b :: _ => error ("Duplicate type name declaration " ^ quote (Binding.name_of b)));
|
|
76 |
|
|
77 |
val ctr_specss = map ctr_specs_of_spec specs;
|
|
78 |
|
|
79 |
val disc_namess = map (map disc_of_ctr_spec) ctr_specss;
|
|
80 |
val raw_ctr_namess = map (map ctr_of_ctr_spec) ctr_specss;
|
|
81 |
val ctr_argsss = map (map args_of_ctr_spec) ctr_specss;
|
|
82 |
val ctr_mixfixess = map (map mixfix_of_ctr_spec) ctr_specss;
|
|
83 |
|
|
84 |
val sel_namesss = map (map (map fst)) ctr_argsss;
|
|
85 |
val ctr_Tsss = map (map (map (prepare_typ lthy o snd))) ctr_argsss;
|
|
86 |
|
|
87 |
val (activeAs, _) = lthy |> mk_TFrees N;
|
|
88 |
|
|
89 |
val eqs = map2 (fn TFree A => fn Tss => (A, mk_prod_sum Tss)) activeAs ctr_Tsss;
|
|
90 |
|
|
91 |
val lthy' = fp_bnf construct bs eqs lthy;
|
|
92 |
|
|
93 |
fun wrap_type ((b, disc_names), sel_namess) lthy =
|
|
94 |
let
|
|
95 |
val ctrs = [];
|
|
96 |
val caseof = @{term True};
|
|
97 |
val tacss = [];
|
|
98 |
in
|
|
99 |
wrap tacss ((ctrs, caseof), (disc_names, sel_namess)) lthy
|
|
100 |
end;
|
49112
|
101 |
in
|
49119
|
102 |
lthy' |> fold wrap_type (bs ~~ disc_namess ~~ sel_namesss)
|
49112
|
103 |
end;
|
|
104 |
|
49119
|
105 |
val data_cmd = prepare_data Syntax.read_typ;
|
|
106 |
|
|
107 |
val parse_opt_binding_colon = Scan.optional (Parse.binding --| Parse.$$$ ":") no_name
|
|
108 |
|
49112
|
109 |
val parse_ctr_arg =
|
49119
|
110 |
Parse.$$$ "(" |-- parse_opt_binding_colon -- Parse.typ --| Parse.$$$ ")" ||
|
|
111 |
(Parse.typ >> pair no_name);
|
49112
|
112 |
|
|
113 |
val parse_single_spec =
|
|
114 |
Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix --
|
49119
|
115 |
(@{keyword "="} |-- Parse.enum1 "|" (parse_opt_binding_colon -- Parse.binding --
|
|
116 |
Scan.repeat parse_ctr_arg -- Parse.opt_mixfix));
|
49112
|
117 |
|
|
118 |
val _ =
|
|
119 |
Outer_Syntax.local_theory @{command_spec "data"} "define BNF-based inductive datatypes"
|
49119
|
120 |
(Parse.and_list1 parse_single_spec >> data_cmd lfp_info);
|
49112
|
121 |
|
|
122 |
val _ =
|
|
123 |
Outer_Syntax.local_theory @{command_spec "codata"} "define BNF-based coinductive datatypes"
|
49119
|
124 |
(Parse.and_list1 parse_single_spec >> data_cmd gfp_info);
|
49112
|
125 |
|
|
126 |
end;
|