32 |
32 |
33 val live = live_of_bnf (hd bnfs); |
33 val live = live_of_bnf (hd bnfs); |
34 val n = length bnfs; (*active*) |
34 val n = length bnfs; (*active*) |
35 val ks = 1 upto n; |
35 val ks = 1 upto n; |
36 val m = live - n; (*passive, if 0 don't generate a new BNF*) |
36 val m = live - n; (*passive, if 0 don't generate a new BNF*) |
37 val b = Binding.name (mk_common_name (map Binding.name_of bs)); |
37 val b_names = map Binding.name_of bs; |
|
38 val b = Binding.name (mk_common_name b_names); |
38 |
39 |
39 (* TODO: check if m, n, etc., are sane *) |
40 (* TODO: check if m, n, etc., are sane *) |
40 |
41 |
41 val deads = fold (union (op =)) Dss resDs; |
42 val deads = fold (union (op =)) Dss resDs; |
42 val names_lthy = fold Variable.declare_typ deads lthy; |
43 val names_lthy = fold Variable.declare_typ deads lthy; |
|
44 val passives = map fst (subtract (op = o apsnd TFree) deads resBs); |
43 |
45 |
44 (* tvars *) |
46 (* tvars *) |
45 val ((((((passiveAs, activeAs), passiveBs), activeBs), activeCs), passiveXs), passiveYs) = |
47 val ((((((passiveAs, activeAs), passiveBs), activeBs), activeCs), passiveXs), passiveYs) = |
46 names_lthy |
48 names_lthy |
47 |> mk_TFrees m |
49 |> variant_tfrees passives |
48 ||>> mk_TFrees n |
50 ||>> mk_TFrees n |
49 ||>> mk_TFrees m |
51 ||>> variant_tfrees passives |
50 ||>> mk_TFrees n |
52 ||>> mk_TFrees n |
51 ||>> mk_TFrees n |
53 ||>> mk_TFrees n |
52 ||>> mk_TFrees m |
54 ||>> mk_TFrees m |
53 ||> fst o mk_TFrees m; |
55 ||> fst o mk_TFrees m; |
54 |
56 |
61 val allCs' = passiveBs @ activeCs; |
63 val allCs' = passiveBs @ activeCs; |
62 val Css' = replicate n allCs'; |
64 val Css' = replicate n allCs'; |
63 |
65 |
64 (* types *) |
66 (* types *) |
65 val dead_poss = |
67 val dead_poss = |
66 map (fn T => if member (op =) deads (TFree T) then SOME (TFree T) else NONE) resBs; |
68 map (fn x => if member (op =) deads (TFree x) then SOME (TFree x) else NONE) resBs; |
67 fun mk_param NONE passive = (hd passive, tl passive) |
69 fun mk_param NONE passive = (hd passive, tl passive) |
68 | mk_param (SOME a) passive = (a, passive); |
70 | mk_param (SOME a) passive = (a, passive); |
69 val mk_params = fold_map mk_param dead_poss #> fst; |
71 val mk_params = fold_map mk_param dead_poss #> fst; |
70 |
72 |
71 fun mk_FTs Ts = map2 (fn Ds => mk_T_of_bnf Ds Ts) Dss bnfs; |
73 fun mk_FTs Ts = map2 (fn Ds => mk_T_of_bnf Ds Ts) Dss bnfs; |
187 |
189 |
188 val timer = time (timer "Checked nonemptiness"); |
190 val timer = time (timer "Checked nonemptiness"); |
189 |
191 |
190 (* derived thms *) |
192 (* derived thms *) |
191 |
193 |
192 (*map g1 ... gm g(m+1) ... g(m+n) (map id ... id f(m+1) ... f(m+n) x)= |
194 (*map g1 ... gm g(m+1) ... g(m+n) (map id ... id f(m+1) ... f(m+n) x) = |
193 map g1 ... gm (g(m+1) o f(m+1)) ... (g(m+n) o f(m+n)) x*) |
195 map g1 ... gm (g(m+1) o f(m+1)) ... (g(m+n) o f(m+n)) x*) |
194 fun mk_map_comp_id x mapAsBs mapBsCs mapAsCs map_comp = |
196 fun mk_map_comp_id x mapAsBs mapBsCs mapAsCs map_comp = |
195 let |
197 let |
196 val lhs = Term.list_comb (mapBsCs, all_gs) $ |
198 val lhs = Term.list_comb (mapBsCs, all_gs) $ |
197 (Term.list_comb (mapAsBs, passive_ids @ fs) $ x); |
199 (Term.list_comb (mapAsBs, passive_ids @ fs) $ x); |