1.1 --- a/src/HOL/Codatatype/Tools/bnf_comp.ML Mon Sep 17 15:38:16 2012 +0200
1.2 +++ b/src/HOL/Codatatype/Tools/bnf_comp.ML Mon Sep 17 16:57:22 2012 +0200
1.3 @@ -15,7 +15,7 @@
1.4 val rel_unfolds_of: unfold_thms -> thm list
1.5 val pred_unfolds_of: unfold_thms -> thm list
1.6
1.7 - val bnf_of_typ: BNF_Def.const_policy -> binding -> (binding -> binding) ->
1.8 + val bnf_of_typ: BNF_Def.const_policy -> (binding -> binding) ->
1.9 ((string * sort) list list -> (string * sort) list) -> typ -> unfold_thms * Proof.context ->
1.10 (BNF_Def.BNF * (typ list * typ list)) * (unfold_thms * Proof.context)
1.11 val default_comp_sort: (string * sort) list list -> (string * sort) list
1.12 @@ -68,10 +68,10 @@
1.13
1.14 val bdTN = "bdT";
1.15
1.16 -fun mk_killN n = "kill" ^ string_of_int n ^ "_";
1.17 -fun mk_liftN n = "lift" ^ string_of_int n ^ "_";
1.18 +fun mk_killN n = "_kill" ^ string_of_int n;
1.19 +fun mk_liftN n = "_lift" ^ string_of_int n;
1.20 fun mk_permuteN src dest =
1.21 - "permute_" ^ implode (map string_of_int src) ^ "_" ^ implode (map string_of_int dest) ^ "_";
1.22 + "_permute_" ^ implode (map string_of_int src) ^ "_" ^ implode (map string_of_int dest);
1.23
1.24 val no_thm = refl;
1.25 val Collect_split_box_equals = box_equals RS @{thm Collect_split_cong};
1.26 @@ -286,7 +286,7 @@
1.27
1.28 fun kill_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else
1.29 let
1.30 - val b = Binding.prefix_name (mk_killN n) (name_of_bnf bnf);
1.31 + val b = Binding.suffix_name (mk_killN n) (name_of_bnf bnf);
1.32 val live = live_of_bnf bnf;
1.33 val dead = dead_of_bnf bnf;
1.34 val nwits = nwits_of_bnf bnf;
1.35 @@ -385,7 +385,7 @@
1.36
1.37 fun lift_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else
1.38 let
1.39 - val b = Binding.prefix_name (mk_liftN n) (name_of_bnf bnf);
1.40 + val b = Binding.suffix_name (mk_liftN n) (name_of_bnf bnf);
1.41 val live = live_of_bnf bnf;
1.42 val dead = dead_of_bnf bnf;
1.43 val nwits = nwits_of_bnf bnf;
1.44 @@ -474,7 +474,7 @@
1.45
1.46 fun permute_bnf qualify src dest bnf (unfold, lthy) = if src = dest then (bnf, (unfold, lthy)) else
1.47 let
1.48 - val b = Binding.prefix_name (mk_permuteN src dest) (name_of_bnf bnf);
1.49 + val b = Binding.suffix_name (mk_permuteN src dest) (name_of_bnf bnf);
1.50 val live = live_of_bnf bnf;
1.51 val dead = dead_of_bnf bnf;
1.52 val nwits = nwits_of_bnf bnf;
1.53 @@ -590,15 +590,9 @@
1.54 fun default_comp_sort Ass =
1.55 Library.sort (Term_Ord.typ_ord o pairself TFree) (fold (fold (insert (op =))) Ass []);
1.56
1.57 -fun compose_bnf const_policy qualify' b sort outer inners oDs Dss tfreess (unfold, lthy) =
1.58 +fun compose_bnf const_policy qualify sort outer inners oDs Dss tfreess (unfold, lthy) =
1.59 let
1.60 - val name = Binding.name_of b;
1.61 - fun qualify i bind =
1.62 - let val namei = if i > 0 then name ^ string_of_int i else name;
1.63 - in
1.64 - if member (op =) (#2 (Binding.dest bind)) (namei, true) then qualify' bind
1.65 - else qualify' (Binding.prefix_name namei bind)
1.66 - end;
1.67 + val b = name_of_bnf outer;
1.68
1.69 val Ass = map (map Term.dest_TFree) tfreess;
1.70 val Ds = fold (fold Term.add_tfreesT) (oDs :: Dss) [];
1.71 @@ -609,7 +603,8 @@
1.72 val Ds = oDs @ flat (map3 (append oo map o nth) tfreess kill_poss Dss);
1.73 val As = map TFree As;
1.74 in
1.75 - apfst (rpair (Ds, As)) (clean_compose_bnf const_policy I b outer inners' (unfold', lthy'))
1.76 + apfst (rpair (Ds, As))
1.77 + (clean_compose_bnf const_policy (qualify 0) b outer inners' (unfold', lthy'))
1.78 end;
1.79
1.80 (* Hide the type of the bound (optimization) and unfold the definitions (nicer to the user) *)
1.81 @@ -707,11 +702,11 @@
1.82 ((bnf', deads), lthy' |> Local_Theory.notes notes |> snd)
1.83 end;
1.84
1.85 -fun bnf_of_typ _ _ _ _ (T as TFree _) (unfold, lthy) =
1.86 +fun bnf_of_typ _ _ _ (T as TFree _) (unfold, lthy) =
1.87 ((Basic_BNFs.ID_bnf, ([], [T])), (add_to_unfold_opt NONE NONE
1.88 (SOME Basic_BNFs.ID_rel_def) (SOME Basic_BNFs.ID_pred_def) unfold, lthy))
1.89 - | bnf_of_typ _ _ _ _ (TVar _) _ = error "Unexpected schematic variable"
1.90 - | bnf_of_typ const_policy b qualify' sort (T as Type (C, Ts)) (unfold, lthy) =
1.91 + | bnf_of_typ _ _ _ (TVar _) _ = error "Unexpected schematic variable"
1.92 + | bnf_of_typ const_policy qualify' sort (T as Type (C, Ts)) (unfold, lthy) =
1.93 let
1.94 val tfrees = Term.add_tfreesT T [];
1.95 val bnf_opt = if null tfrees then NONE else bnf_of lthy C;
1.96 @@ -734,13 +729,10 @@
1.97 in ((bnf, deads_lives), (unfold', lthy)) end
1.98 else
1.99 let
1.100 - val name = Binding.name_of b;
1.101 - fun qualify i bind =
1.102 - let val namei = if i > 0 then name ^ string_of_int i else name;
1.103 - in
1.104 - if member (op =) (#2 (Binding.dest bind)) (namei, true) then qualify' bind
1.105 - else qualify' (Binding.prefix_name namei bind)
1.106 - end;
1.107 + val name = Long_Name.base_name C;
1.108 + fun qualify i =
1.109 + let val namei = name ^ nonzero_string_of_int i;
1.110 + in qualify' o Binding.qualify true namei end;
1.111 val odead = dead_of_bnf bnf;
1.112 val olive = live_of_bnf bnf;
1.113 val oDs_pos = find_indices [TFree ("dead", [])] (snd (Term.dest_Type
1.114 @@ -749,11 +741,10 @@
1.115 val Ts' = map (nth Ts) (subtract (op =) oDs_pos (0 upto length Ts - 1));
1.116 val ((inners, (Dss, Ass)), (unfold', lthy')) =
1.117 apfst (apsnd split_list o split_list)
1.118 - (fold_map2 (fn i =>
1.119 - bnf_of_typ Smart_Inline (Binding.name (name ^ string_of_int i)) (qualify i) sort)
1.120 + (fold_map2 (fn i => bnf_of_typ Smart_Inline (qualify i) sort)
1.121 (if length Ts' = 1 then [0] else (1 upto length Ts')) Ts' (unfold, lthy));
1.122 in
1.123 - compose_bnf const_policy (qualify 0) b sort bnf inners oDs Dss Ass (unfold', lthy')
1.124 + compose_bnf const_policy qualify sort bnf inners oDs Dss Ass (unfold', lthy')
1.125 end)
1.126 end;
1.127