| changeset 1177 | 6f01720fe520 |
| parent 1176 | 29c4a0cf9237 |
| child 1178 | 275a1cb3f2ba |
| 1176:29c4a0cf9237 | 1177:6f01720fe520 |
|---|---|
65 ML maps |
65 ML maps |
66 ML {* |
66 ML {* |
67 val {descr, ...} = Datatype.the_info @{theory} "Fv.rtrm1"; |
67 val {descr, ...} = Datatype.the_info @{theory} "Fv.rtrm1"; |
68 val sorts = []; |
68 val sorts = []; |
69 val bindsall = [ |
69 val bindsall = [ |
70 [[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [], [(SOME @{term bv1}, 0)]]], |
70 [[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(NONE, 0)], [], [(SOME @{term bv1}, 0)]]], |
71 [[], [[]], [[], []]] |
71 [[], [[]], [[], []]] |
72 ]; |
72 ]; |
73 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
73 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
74 val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
74 val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
75 "fv_" ^ name_of_typ (nth_dtyp i)) descr); |
75 "fv_" ^ name_of_typ (nth_dtyp i)) descr); |
80 val Ts = map (typ_of_dtyp descr sorts) dts; |
80 val Ts = map (typ_of_dtyp descr sorts) dts; |
81 val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); |
81 val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); |
82 val args = map Free (names ~~ Ts); |
82 val args = map Free (names ~~ Ts); |
83 val c = Const (cname, Ts ---> (nth_dtyp i)); |
83 val c = Const (cname, Ts ---> (nth_dtyp i)); |
84 val fv_c = Free (nth fv_names i, (nth_dtyp i) --> @{typ "atom set"}); |
84 val fv_c = Free (nth fv_names i, (nth_dtyp i) --> @{typ "atom set"}); |
85 (* TODO we assume that all can be 'atomized' *) |
85 fun fv_bind (NONE, i) = |
86 fun fv_bind (NONE, i) = mk_single_atom (nth args i) |
86 if is_rec_type (nth dts i) then (nth fv_frees (body_index (nth dts i))) $ (nth args i) else |
87 (* TODO we assume that all can be 'atomized' *) |
|
88 mk_single_atom (nth args i) |
|
87 | fv_bind (SOME f, i) = f $ (nth args i); |
89 | fv_bind (SOME f, i) = f $ (nth args i); |
88 fun fv_arg ((dt, x), bindxs) = |
90 fun fv_arg ((dt, x), bindxs) = |
89 let |
91 let |
90 val arg = |
92 val arg = |
91 if is_rec_type dt then nth fv_frees (body_index dt) $ x else |
93 if is_rec_type dt then nth fv_frees (body_index dt) $ x else |