15 *} |
15 *} |
16 |
16 |
17 ML {* dest_Type @{typ rlam} *} |
17 ML {* dest_Type @{typ rlam} *} |
18 |
18 |
19 (* Bindings are given as a list which has a length being equal |
19 (* Bindings are given as a list which has a length being equal |
20 to the length of the number of constructors. Each element |
20 to the length of the number of constructors. |
21 is a specification of all the bindings n this constructor. |
21 |
22 The bindings are given as triples: function, bound argument, |
22 Each element is a list whose length is equal to the number |
23 and the argument in which it is bound. |
23 of arguents. |
|
24 |
|
25 Every element specifies bindings of this argument given as |
|
26 a tuple: function, bound argument. |
24 |
27 |
25 Eg: |
28 Eg: |
26 nominal_datatype |
29 nominal_datatype |
27 |
30 |
28 C1 |
31 C1 |
29 | C2 x y z bind x in z |
32 | C2 x y z bind x in z |
30 | C3 x y z bind f x in y bind g y in z |
33 | C3 x y z bind f x in z bind g y in z |
31 |
34 |
32 yields: |
35 yields: |
33 [[], [(NONE, 0, 2)], [(SOME (Const f), 0, 1), (Some (Const g), 1, 2)]] |
36 [ |
|
37 [], |
|
38 [[], [], [(NONE, 0)]], |
|
39 [[], [], [(SOME (Const f), 0), (Some (Const g), 1, 2)]]] |
34 *) |
40 *) |
35 |
41 |
36 ML {* |
42 ML {* |
37 val {descr, ...} = Datatype.the_info @{theory} "Fv.rlam"; |
43 val {descr, ...} = Datatype.the_info @{theory} "Fv.rlam"; |
38 val sorts = []; |
44 val sorts = []; |
39 |
45 val binds = [[], [[], []], [[], [(NONE, 0)]]]; |
40 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
46 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
41 val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
47 val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
42 "fv_" ^ name_of_typ (nth_dtyp i)) descr); |
48 "fv_" ^ name_of_typ (nth_dtyp i)) descr); |
43 val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; |
49 val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; |
44 val fv_frees = map Free (fv_names ~~ fv_types); |
50 val fv_frees = map Free (fv_names ~~ fv_types); |
45 (* TODO: should be optimized to avoid {}+{}+{} *) |
51 (* TODO: should be optimized to avoid {}+{}+{} *) |
46 fun mk_union sets = foldr1 (HOLogic.mk_binop @{const_name union}) sets; |
52 fun mk_union sets = foldr1 (HOLogic.mk_binop @{const_name union}) sets; |
47 |
53 |
48 fun fv_eq_constr i (cname, dts) = |
54 fun fv_eq_constr i (cname, dts) bind = |
49 let |
55 let |
50 val Ts = map (typ_of_dtyp descr sorts) dts; |
56 val Ts = map (typ_of_dtyp descr sorts) dts; |
51 val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); |
57 val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); |
52 val args = map Free (names ~~ Ts); |
58 val args = map Free (names ~~ Ts); |
53 val c = Const (cname, Ts ---> (nth_dtyp i)); |
59 val c = Const (cname, Ts ---> (nth_dtyp i)); |
54 val fv_c = Free (nth fv_names i, (nth_dtyp i) --> @{typ "atom set"}); |
60 val fv_c = Free (nth fv_names i, (nth_dtyp i) --> @{typ "atom set"}); |
55 fun fv_arg (dt, x) = |
61 fun fv_arg (dt, x) = |
56 if is_rec_type dt then |
62 let |
57 nth fv_frees (body_index dt) $ x |
63 val arg = |
58 (* TODO: we just assume everything is a 'name' *) |
64 if is_rec_type dt then nth fv_frees (body_index dt) $ x |
59 else HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x] |
65 (* TODO: we just assume everything is a 'name' *) |
|
66 else HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x] |
|
67 in |
|
68 arg |
|
69 end |
60 in |
70 in |
61 (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq |
71 (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq |
62 (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args))))) |
72 (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args))))) |
63 end; |
73 end; |
64 fun fv_eq (i, (_, _, constrs)) = map (fv_eq_constr i) constrs; |
74 fun fv_eq (i, (_, _, constrs)) = map2 (fv_eq_constr i) constrs binds; |
65 val fv_eqs = maps fv_eq descr |
75 val fv_eqs = maps fv_eq descr |
66 *} |
76 *} |
67 |
77 |
68 local_setup {* |
78 local_setup {* |
69 snd o (Primrec.add_primrec |
79 snd o (Primrec.add_primrec |