--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Wed Sep 05 19:57:50 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Wed Sep 05 19:58:09 2012 +0200
@@ -67,7 +67,6 @@
| A :: _ => error ("Duplicate type parameter " ^ quote (Syntax.string_of_typ lthy A)));
(* TODO: use sort constraints on type args *)
- (* TODO: use mixfix *)
val N = length specs;
@@ -122,7 +121,7 @@
val eqs = map dest_TFree Bs ~~ sum_prod_TsBs;
val ((raw_unfs, raw_flds, unf_flds, fld_unfs, fld_injects), lthy') =
- fp_bnf (if gfp then bnf_gfp else bnf_lfp) bs As' eqs lthy;
+ fp_bnf (if gfp then bnf_gfp else bnf_lfp) bs mixfixes As' eqs lthy;
val timer = time (Timer.startRealTimer ());
@@ -137,8 +136,8 @@
val unfs = map (mk_unf As) raw_unfs;
val flds = map (mk_fld As) raw_flds;
- fun pour_sugar_on_type ((((((((((b, T), fld), unf), fld_unf), unf_fld), fld_inject),
- ctr_binders), ctr_Tss), disc_binders), sel_binderss) no_defs_lthy =
+ fun pour_sugar_on_type (((((((((((b, T), fld), unf), fld_unf), unf_fld), fld_inject),
+ ctr_binders), ctr_mixfixes), ctr_Tss), disc_binders), sel_binderss) no_defs_lthy =
let
val n = length ctr_binders;
val ks = 1 upto n;
@@ -165,9 +164,9 @@
fold_rev Term.lambda (fs @ [v]) (mk_sum_caseN (uncurry_fs fs xss) $ (unf $ v));
val (((raw_ctrs, raw_ctr_defs), (raw_case, raw_case_def)), (lthy', lthy)) = no_defs_lthy
- |> apfst split_list o fold_map2 (fn b => fn rhs =>
- Local_Theory.define ((b, NoSyn), ((Thm.def_binding b, []), rhs)) #>> apsnd snd)
- ctr_binders ctr_rhss
+ |> apfst split_list o fold_map3 (fn b => fn mx => fn rhs =>
+ Local_Theory.define ((b, mx), ((Thm.def_binding b, []), rhs)) #>> apsnd snd)
+ ctr_binders ctr_mixfixes ctr_rhss
||>> (Local_Theory.define ((case_binder, NoSyn), ((Thm.def_binding case_binder, []),
case_rhs)) #>> apsnd snd)
||> `Local_Theory.restore;
@@ -250,7 +249,7 @@
val lthy'' =
fold pour_sugar_on_type (bs ~~ Ts ~~ flds ~~ unfs ~~ fld_unfs ~~ unf_flds ~~ fld_injects ~~
- ctr_binderss ~~ ctr_Tsss ~~ disc_binderss ~~ sel_bindersss) lthy'
+ ctr_binderss ~~ ctr_mixfixess ~~ ctr_Tsss ~~ disc_binderss ~~ sel_bindersss) lthy';
val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^
(if gfp then "co" else "") ^ "datatype"));
--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML Wed Sep 05 19:57:50 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML Wed Sep 05 19:58:09 2012 +0200
@@ -98,11 +98,12 @@
val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
- val fp_bnf: (binding list -> (string * sort) list -> typ list list -> BNF_Def.BNF list ->
- local_theory -> 'a) ->
- binding list -> (string * sort) list -> ((string * sort) * typ) list -> local_theory -> 'a
- val fp_bnf_cmd: (binding list -> (string * sort) list -> typ list list -> BNF_Def.BNF list ->
- local_theory -> 'a) ->
+ val fp_bnf: (binding list -> mixfix list -> (string * sort) list -> typ list list ->
+ BNF_Def.BNF list -> local_theory -> 'a) ->
+ binding list -> mixfix list -> (string * sort) list -> ((string * sort) * typ) list ->
+ local_theory -> 'a
+ val fp_bnf_cmd: (binding list -> mixfix list -> (string * sort) list -> typ list list ->
+ BNF_Def.BNF list -> local_theory -> 'a) ->
binding list * (string list * string list) -> local_theory -> 'a
end;
@@ -259,7 +260,7 @@
fun fp_sort lhss Ass = Library.sort (Term_Ord.typ_ord o pairself TFree)
(subtract (op =) lhss (fold (fold (insert (op =))) Ass [])) @ lhss;
-fun mk_fp_bnf timer construct bs resBs sort lhss bnfs deadss livess unfold lthy =
+fun mk_fp_bnf timer construct bs mixfixes resBs sort lhss bnfs deadss livess unfold lthy =
let
val name = fold_rev (fn b => fn s => Binding.name_of b ^ s) bs "";
fun qualify i bind =
@@ -289,14 +290,14 @@
val timer = time (timer "Normalization & sealing of BNFs");
- val res = construct bs resDs Dss bnfs'' lthy'';
+ val res = construct bs mixfixes resDs Dss bnfs'' lthy'';
val timer = time (timer "FP construction in total");
in
res
end;
-fun fp_bnf construct bs resBs eqs lthy =
+fun fp_bnf construct bs mixfixes resBs eqs lthy =
let
val timer = time (Timer.startRealTimer ());
val (lhss, rhss) = split_list eqs;
@@ -305,7 +306,7 @@
(fold_map2 (fn b => bnf_of_typ Smart_Inline (Binding.suffix_name "RAW" b) I sort) bs rhss
(empty_unfold, lthy));
in
- mk_fp_bnf timer construct bs resBs sort lhss bnfs Dss Ass unfold lthy'
+ mk_fp_bnf timer construct bs mixfixes resBs sort lhss bnfs Dss Ass unfold lthy'
end;
fun fp_bnf_cmd construct (bs, (raw_lhss, raw_bnfs)) lthy =
@@ -318,7 +319,7 @@
(bnf_of_typ Smart_Inline (Binding.suffix_name "RAW" b) I sort (Syntax.read_typ lthy rawT)))
bs raw_bnfs (empty_unfold, lthy));
in
- mk_fp_bnf timer construct bs [] sort lhss bnfs Dss Ass unfold lthy'
+ mk_fp_bnf timer construct bs (map (K NoSyn) bs) [] sort lhss bnfs Dss Ass unfold lthy'
end;
end;
--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Wed Sep 05 19:57:50 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Wed Sep 05 19:58:09 2012 +0200
@@ -9,8 +9,9 @@
signature BNF_GFP =
sig
- val bnf_gfp: binding list -> (string * sort) list -> typ list list -> BNF_Def.BNF list ->
- local_theory -> (term list * term list * thm list * thm list * thm list) * local_theory
+ val bnf_gfp: binding list -> mixfix list -> (string * sort) list -> typ list list ->
+ BNF_Def.BNF list -> local_theory ->
+ (term list * term list * thm list * thm list * thm list) * local_theory
end;
structure BNF_GFP : BNF_GFP =
@@ -52,7 +53,7 @@
((i, I), nth (nth lwitss i) nwit) :: maps (tree_to_coind_wits lwitss) subtrees;
(*all bnfs have the same lives*)
-fun bnf_gfp bs resDs Dss_insts bnfs lthy =
+fun bnf_gfp bs mixfixes resDs Dss_insts bnfs lthy =
let
val timer = time (Timer.startRealTimer ());
@@ -1830,9 +1831,9 @@
val ((T_names, (T_glob_infos, T_loc_infos)), lthy) =
lthy
- |> fold_map3 (fn b => fn car_final => fn in_car_final =>
- typedef false NONE (b, params, NoSyn) car_final NONE
- (EVERY' [rtac exI, rtac in_car_final] 1)) bs car_finals in_car_final_thms
+ |> fold_map4 (fn b => fn mx => fn car_final => fn in_car_final =>
+ typedef false NONE (b, params, mx) car_final NONE
+ (EVERY' [rtac exI, rtac in_car_final] 1)) bs mixfixes car_finals in_car_final_thms
|>> apsnd split_list o split_list;
val Ts = map (fn name => Type (name, params')) T_names;
--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML Wed Sep 05 19:57:50 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML Wed Sep 05 19:58:09 2012 +0200
@@ -8,8 +8,9 @@
signature BNF_LFP =
sig
- val bnf_lfp: binding list -> (string * sort) list -> typ list list -> BNF_Def.BNF list ->
- local_theory -> (term list * term list * thm list * thm list * thm list) * local_theory
+ val bnf_lfp: binding list -> mixfix list -> (string * sort) list -> typ list list ->
+ BNF_Def.BNF list -> local_theory ->
+ (term list * term list * thm list * thm list * thm list) * local_theory
end;
structure BNF_LFP : BNF_LFP =
@@ -23,7 +24,7 @@
open BNF_LFP_Tactics
(*all bnfs have the same lives*)
-fun bnf_lfp bs resDs Dss_insts bnfs lthy =
+fun bnf_lfp bs mixfixes resDs Dss_insts bnfs lthy =
let
val timer = time (Timer.startRealTimer ());
val live = live_of_bnf (hd bnfs);
@@ -927,9 +928,9 @@
val ((T_names, (T_glob_infos, T_loc_infos)), lthy) =
lthy
- |> fold_map2 (fn b => fn car_init => typedef true NONE (b, params, NoSyn) car_init NONE
+ |> fold_map3 (fn b => fn mx => fn car_init => typedef true NONE (b, params, mx) car_init NONE
(EVERY' [rtac ssubst, rtac @{thm ex_in_conv}, resolve_tac alg_not_empty_thms,
- rtac alg_init_thm] 1)) bs car_inits
+ rtac alg_init_thm] 1)) bs mixfixes car_inits
|>> apsnd split_list o split_list;
val Ts = map (fn name => Type (name, params')) T_names;