respect order of/additional type variables supplied by the user in fixed point constructions;
--- a/src/HOL/Codatatype/Examples/Misc_Codata.thy Thu Sep 06 12:21:33 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Misc_Codata.thy Thu Sep 06 16:06:22 2012 +0200
@@ -53,15 +53,10 @@
and ('a, 'b) trm = Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm"
and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp"
-codata_raw some_killing: 'A = "'a \<Rightarrow> 'b \<Rightarrow> ('A + 'B)"
- and in_here: 'B = "'b \<times> 'a + 'c"
-
-(* FIXME
codata ('a, 'b, 'c) some_killing =
SK "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) some_killing + ('a, 'b, 'c) in_here"
- and ('a, 'b, 'c) in_here =
+ and ('a, 'b, 'c) in_here =
IH1 'b 'a | IH2 'c
-*)
codata_raw some_killing': 'a = "'b \<Rightarrow> 'd \<Rightarrow> ('a + 'c)"
and in_here': 'c = "'d + 'e"
@@ -69,7 +64,7 @@
codata_raw some_killing'': 'a = "'b \<Rightarrow> 'c"
and in_here'': 'c = "'d \<times> 'b + 'e"
-codata_raw less_killing: 'a = "'b \<Rightarrow> 'c"
+codata ('b, 'c) less_killing = LK "'b \<Rightarrow> 'c"
codata 'b cps = CPS1 'b | CPS2 "'b \<Rightarrow> 'b cps"
@@ -95,6 +90,14 @@
and ('c, 'e, 'g) ind_wit =
IW1 | IW2 'c
+codata ('b, 'a) bar = BAR "'a \<Rightarrow> 'b"
+codata ('a, 'b, 'c, 'd) foo = FOO "'d + 'b \<Rightarrow> 'c + 'a"
+
+codata 'a dead_foo = A
+(* FIXME: handle unknown type constructors using DEADID?
+codata ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo"
+*)
+
(* SLOW, MEMORY-HUNGRY
codata ('a, 'c) D1 = A1 "('a, 'c) D2" | B1 "'a list"
and ('a, 'c) D2 = A2 "('a, 'c) D3" | B2 "'c list"
--- a/src/HOL/Codatatype/Examples/Misc_Data.thy Thu Sep 06 12:21:33 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Misc_Data.thy Thu Sep 06 16:06:22 2012 +0200
@@ -51,15 +51,10 @@
and ('a, 'b) trm = Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm"
and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp"
-data_raw some_killing: 'A = "'a \<Rightarrow> 'b \<Rightarrow> ('A + 'B)"
- and in_here: 'B = "'b \<times> 'a + 'c"
-
-(* FIXME
data ('a, 'b, 'c) some_killing =
SK "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) some_killing + ('a, 'b, 'c) in_here"
and ('a, 'b, 'c) in_here =
IH1 'b 'a | IH2 'c
-*)
data 'b nofail1 = NF11 "'b nofail1 \<times> 'b" | NF12 'b
data 'b nofail2 = NF2 "('b nofail2 \<times> 'b \<times> 'b nofail2 \<times> 'b) list"
@@ -150,4 +145,11 @@
and s8 = S8 nat
*)
+data ('a, 'b) bar = BAR "'b \<Rightarrow> 'a"
+data ('a, 'b, 'c, 'd) foo = FOO "'d + 'b \<Rightarrow> 'c + 'a"
+
+data 'a dead_foo = A
+(* FIXME: handle unknown type constructors using DEADID?
+data ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo"
+*)
end
--- a/src/HOL/Codatatype/Tools/bnf_comp.ML Thu Sep 06 12:21:33 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp.ML Thu Sep 06 16:06:22 2012 +0200
@@ -23,7 +23,7 @@
(''a list list -> ''a list) -> BNF_Def.BNF list -> unfold_thms -> Proof.context ->
(int list list * ''a list) * (BNF_Def.BNF list * (unfold_thms * Proof.context))
val seal_bnf: unfold_thms -> binding -> typ list -> BNF_Def.BNF -> Proof.context ->
- BNF_Def.BNF * local_theory
+ (BNF_Def.BNF * typ list) * local_theory
end;
structure BNF_Comp : BNF_COMP =
@@ -656,6 +656,7 @@
val bd_repT = fst (dest_relT (fastype_of bnf_bd));
val bdT_bind = Binding.suffix_name ("_" ^ bdTN) b;
val params = fold Term.add_tfreesT Ds [];
+ val deads = map TFree params;
val ((bdT_name, (bdT_glob_info, bdT_loc_info)), (lthy', lthy)) =
lthy
@@ -666,7 +667,7 @@
val phi = Proof_Context.export_morphism lthy lthy';
val bnf_bd' = mk_dir_image bnf_bd
- (Const (#Abs_name bdT_glob_info, bd_repT --> Type (bdT_name, map TFree params)))
+ (Const (#Abs_name bdT_glob_info, bd_repT --> Type (bdT_name, deads)))
val set_def = Morphism.thm phi (the (#set_def bdT_loc_info));
val Abs_inject = Morphism.thm phi (#Abs_inject bdT_loc_info);
@@ -701,8 +702,8 @@
fun wit_tac _ = mk_simple_wit_tac (map unfold_defs (wit_thms_of_bnf bnf));
- val (bnf', lthy') = bnf_def Hardly_Inline (K Derive_All_Facts) I tacs wit_tac NONE
- ((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits) lthy;
+ val (bnf', lthy') = bnf_def Hardly_Inline (K Derive_All_Facts) I tacs wit_tac (SOME deads)
+ ((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits) lthy;
val defs' = filter_refl (map_def_of_bnf bnf' :: set_defs_of_bnf bnf');
val unfold_defs' = unfold_defs o Local_Defs.unfold lthy' defs';
@@ -723,7 +724,7 @@
|> map (fn (thmN, thms) =>
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
in
- (bnf', lthy' |> Local_Theory.notes notes |> snd)
+ ((bnf', deads), lthy' |> Local_Theory.notes notes |> snd)
end;
fun bnf_of_typ _ _ _ _ (T as TFree _) (unfold, lthy) =
--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML Thu Sep 06 12:21:33 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML Thu Sep 06 16:06:22 2012 +0200
@@ -103,12 +103,12 @@
val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
- val fp_bnf: (binding list -> mixfix list -> (string * sort) list -> typ list list ->
- BNF_Def.BNF list -> local_theory -> 'a) ->
+ val fp_bnf: (mixfix list -> (string * sort) list option -> binding list ->
+ typ 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) ->
+ val fp_bnf_cmd: (mixfix list -> (string * sort) list option -> binding list ->
+ typ list * typ list list -> BNF_Def.BNF list -> local_theory -> 'a) ->
binding list * (string list * string list) -> local_theory -> 'a
end;
@@ -272,10 +272,12 @@
(* FIXME: because of "@ lhss", the output could contain type variables that are not in the input;
also, "fp_sort" should put the "resBs" first and in the order in which they appear *)
-fun fp_sort lhss Ass = Library.sort (Term_Ord.typ_ord o pairself TFree)
- (subtract (op =) lhss (fold (fold (insert (op =))) Ass [])) @ lhss;
+fun fp_sort lhss NONE Ass = Library.sort (Term_Ord.typ_ord o pairself TFree)
+ (subtract (op =) lhss (fold (fold (insert (op =))) Ass [])) @ lhss
+ | fp_sort lhss (SOME resBs) Ass =
+ (subtract (op =) lhss (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs)) @ lhss;
-fun mk_fp_bnf timer construct bs mixfixes resBs sort lhss bnfs deadss livess unfold lthy =
+fun mk_fp_bnf timer construct resBs bs 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 =
@@ -286,8 +288,8 @@
end;
val Ass = map (map dest_TFree) livess;
- val resDs = fold (subtract (op =)) Ass resBs;
- val Ds = fold (fold Term.add_tfreesT) deadss resDs;
+ val resDs = (case resBs of NONE => [] | SOME Ts => fold (subtract (op =)) Ass Ts);
+ val Ds = fold (fold Term.add_tfreesT) deadss [];
val _ = (case Library.inter (op =) Ds lhss of [] => ()
| A :: _ => error ("Nonadmissible type recursion (cannot take fixed point of dead type \
@@ -300,12 +302,13 @@
val Dss = map3 (append oo map o nth) livess kill_poss deadss;
- val (bnfs'', lthy'') =
- fold_map3 (seal_bnf unfold') (map (Binding.suffix_name "BNF") bs) Dss bnfs' lthy';
+ val ((bnfs'', deadss), lthy'') =
+ fold_map3 (seal_bnf unfold') (map (Binding.suffix_name "BNF") bs) Dss bnfs' lthy'
+ |>> split_list;
val timer = time (timer "Normalization & sealing of BNFs");
- val res = construct bs mixfixes resDs Dss bnfs'' lthy'';
+ val res = construct resBs bs (map TFree resDs, deadss) bnfs'' lthy'';
val timer = time (timer "FP construction in total");
in
@@ -316,25 +319,25 @@
let
val timer = time (Timer.startRealTimer ());
val (lhss, rhss) = split_list eqs;
- val sort = fp_sort lhss;
+ val sort = fp_sort lhss (SOME resBs);
val ((bnfs, (Dss, Ass)), (unfold, lthy')) = apfst (apsnd split_list o split_list)
(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 mixfixes resBs sort lhss bnfs Dss Ass unfold lthy'
+ mk_fp_bnf timer (construct mixfixes) (SOME resBs) bs sort lhss bnfs Dss Ass unfold lthy'
end;
fun fp_bnf_cmd construct (bs, (raw_lhss, raw_bnfs)) lthy =
let
val timer = time (Timer.startRealTimer ());
val lhss = map (dest_TFree o Syntax.read_typ lthy) raw_lhss;
- val sort = fp_sort lhss;
+ val sort = fp_sort lhss NONE;
val ((bnfs, (Dss, Ass)), (unfold, lthy')) = apfst (apsnd split_list o split_list)
(fold_map2 (fn b => fn rawT =>
(bnf_of_typ Smart_Inline (Binding.suffix_name "RAW" b) I sort (Syntax.read_typ lthy rawT)))
- bs raw_bnfs (empty_unfold, lthy));
+ bs raw_bnfs (empty_unfold, lthy));
in
- mk_fp_bnf timer construct bs (map (K NoSyn) bs) [] sort lhss bnfs Dss Ass unfold lthy'
+ mk_fp_bnf timer (construct (map (K NoSyn) bs)) NONE bs sort lhss bnfs Dss Ass unfold lthy'
end;
end;
--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Thu Sep 06 12:21:33 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Thu Sep 06 16:06:22 2012 +0200
@@ -9,8 +9,8 @@
signature BNF_GFP =
sig
- val bnf_gfp: binding list -> mixfix list -> (string * sort) list -> typ list list ->
- BNF_Def.BNF list -> local_theory ->
+ val bnf_gfp: mixfix list -> (string * sort) list option -> binding list ->
+ typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
(term list * term list * term list * term list * thm list * thm list * thm list) * local_theory
end;
@@ -53,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 mixfixes resDs Dss_insts bnfs lthy =
+fun bnf_gfp mixfixes resBs bs (resDs, Dss) bnfs lthy =
let
val timer = time (Timer.startRealTimer ());
@@ -66,8 +66,7 @@
(* TODO: check if m, n etc are sane *)
- val Dss = map (fn Ds => map TFree (fold Term.add_tfreesT Ds [])) Dss_insts;
- val deads = fold (union (op =)) Dss (map TFree resDs);
+ val deads = fold (union (op =)) Dss resDs;
val names_lthy = fold Variable.declare_typ deads lthy;
(* tvars *)
@@ -92,8 +91,16 @@
val Css' = replicate n allCs';
(* typs *)
+ val dead_poss =
+ (case resBs of
+ NONE => map SOME deads @ replicate m NONE
+ | SOME Ts => map (fn T => if member (op =) deads (TFree T) then SOME (TFree T) else NONE) Ts);
+ fun mk_param NONE passive = (hd passive, tl passive)
+ | mk_param (SOME a) passive = (a, passive);
+ val mk_params = fold_map mk_param dead_poss #> fst;
+
fun mk_FTs Ts = map2 (fn Ds => mk_T_of_bnf Ds Ts) Dss bnfs;
- val (params, params') = `(map Term.dest_TFree) (deads @ passiveAs);
+ val (params, params') = `(map Term.dest_TFree) (mk_params passiveAs);
val FTsAs = mk_FTs allAs;
val FTsBs = mk_FTs allBs;
val FTsCs = mk_FTs allCs;
@@ -1912,7 +1919,7 @@
(*transforms defined frees into consts*)
val phi = Proof_Context.export_morphism lthy_old lthy;
fun mk_unfs passive =
- map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ (deads @ passive)) o
+ map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ (mk_params passive)) o
Morphism.term phi) unf_frees;
val unfs = mk_unfs passiveAs;
val unf's = mk_unfs passiveBs;
--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML Thu Sep 06 12:21:33 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML Thu Sep 06 16:06:22 2012 +0200
@@ -8,8 +8,8 @@
signature BNF_LFP =
sig
- val bnf_lfp: binding list -> mixfix list -> (string * sort) list -> typ list list ->
- BNF_Def.BNF list -> local_theory ->
+ val bnf_lfp: mixfix list -> (string * sort) list option -> binding list ->
+ typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
(term list * term list * term list * term list * thm list * thm list * thm list) * local_theory
end;
@@ -24,7 +24,7 @@
open BNF_LFP_Tactics
(*all bnfs have the same lives*)
-fun bnf_lfp bs mixfixes resDs Dss_insts bnfs lthy =
+fun bnf_lfp mixfixes resBs bs (resDs, Dss) bnfs lthy =
let
val timer = time (Timer.startRealTimer ());
val live = live_of_bnf (hd bnfs);
@@ -35,8 +35,7 @@
(* TODO: check if m, n etc are sane *)
- val Dss = map (fn Ds => map TFree (fold Term.add_tfreesT Ds [])) Dss_insts;
- val deads = fold (union (op =)) Dss (map TFree resDs);
+ val deads = fold (union (op =)) Dss resDs;
val names_lthy = fold Variable.declare_typ deads lthy;
(* tvars *)
@@ -58,8 +57,16 @@
val Css' = replicate n allCs';
(* typs *)
+ val dead_poss =
+ (case resBs of
+ NONE => map SOME deads @ replicate m NONE
+ | SOME Ts => map (fn T => if member (op =) deads (TFree T) then SOME (TFree T) else NONE) Ts);
+ fun mk_param NONE passive = (hd passive, tl passive)
+ | mk_param (SOME a) passive = (a, passive);
+ val mk_params = fold_map mk_param dead_poss #> fst;
+
fun mk_FTs Ts = map2 (fn Ds => mk_T_of_bnf Ds Ts) Dss bnfs;
- val (params, params') = `(map Term.dest_TFree) (deads @ passiveAs);
+ val (params, params') = `(map Term.dest_TFree) (mk_params passiveAs);
val FTsAs = mk_FTs allAs;
val FTsBs = mk_FTs allBs;
val FTsCs = mk_FTs allCs;
@@ -1019,7 +1026,7 @@
(*transforms defined frees into consts*)
val phi = Proof_Context.export_morphism lthy_old lthy;
fun mk_flds passive =
- map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ (deads @ passive)) o
+ map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ (mk_params passive)) o
Morphism.term phi) fld_frees;
val flds = mk_flds passiveAs;
val fld's = mk_flds passiveBs;