equal
deleted
inserted
replaced
18 struct |
18 struct |
19 |
19 |
20 open BNF_Util |
20 open BNF_Util |
21 open BNF_Wrap_Tactics |
21 open BNF_Wrap_Tactics |
22 |
22 |
23 val is_N = "is_"; |
23 val isN = "is_"; |
24 val un_N = "un_"; |
24 val unN = "un_"; |
25 fun mk_un_N 1 1 suf = un_N ^ suf |
25 fun mk_unN 1 1 suf = unN ^ suf |
26 | mk_un_N _ l suf = un_N ^ suf ^ string_of_int l; |
26 | mk_unN _ l suf = unN ^ suf ^ string_of_int l; |
27 |
27 |
28 val case_congN = "case_cong"; |
28 val case_congN = "case_cong"; |
29 val case_eqN = "case_eq"; |
29 val case_eqN = "case_eq"; |
30 val casesN = "cases"; |
30 val casesN = "cases"; |
31 val collapseN = "collapse"; |
31 val collapseN = "collapse"; |
105 fun can_rely_on_disc k = |
105 fun can_rely_on_disc k = |
106 can_really_rely_on_disc k orelse (k = 1 andalso not (can_really_rely_on_disc 2)); |
106 can_really_rely_on_disc k orelse (k = 1 andalso not (can_really_rely_on_disc 2)); |
107 fun can_omit_disc_binder k m = |
107 fun can_omit_disc_binder k m = |
108 n = 1 orelse m = 0 orelse (n = 2 andalso can_rely_on_disc (3 - k)); |
108 n = 1 orelse m = 0 orelse (n = 2 andalso can_rely_on_disc (3 - k)); |
109 |
109 |
110 val fallback_disc_binder = Binding.name o prefix is_N o Long_Name.base_name o name_of_ctr; |
110 val fallback_disc_binder = Binding.name o prefix isN o Long_Name.base_name o name_of_ctr; |
111 |
111 |
112 val disc_binders = |
112 val disc_binders = |
113 raw_disc_binders' |
113 raw_disc_binders' |
114 |> map4 (fn k => fn m => fn ctr => fn disc => |
114 |> map4 (fn k => fn m => fn ctr => fn disc => |
115 if Binding.eq_name (disc, no_binder) then |
115 if Binding.eq_name (disc, no_binder) then |
120 SOME disc) ks ms ctrs0; |
120 SOME disc) ks ms ctrs0; |
121 |
121 |
122 val no_discs = map is_none disc_binders; |
122 val no_discs = map is_none disc_binders; |
123 val no_discs_at_all = forall I no_discs; |
123 val no_discs_at_all = forall I no_discs; |
124 |
124 |
125 fun fallback_sel_binder m l = Binding.name o mk_un_N m l o Long_Name.base_name o name_of_ctr; |
125 fun fallback_sel_binder m l = Binding.name o mk_unN m l o Long_Name.base_name o name_of_ctr; |
126 |
126 |
127 val sel_binderss = |
127 val sel_binderss = |
128 pad_list [] n raw_sel_binderss |
128 pad_list [] n raw_sel_binderss |
129 |> map3 (fn ctr => fn m => map2 (fn l => fn sel => |
129 |> map3 (fn ctr => fn m => map2 (fn l => fn sel => |
130 if Binding.eq_name (sel, no_binder) orelse Binding.eq_name (sel, fallback_binder) then |
130 if Binding.eq_name (sel, no_binder) orelse Binding.eq_name (sel, fallback_binder) then |